Improvements for SVCOMP 2025 (#765)

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com> Co-authored-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
hernanponcedeleon · Nov 2, 2024 · c128407 · c128407
1 parent 347661e
commit c128407
Show file tree

Hide file tree

Showing 6 changed files with 11 additions and 6 deletions.
diff --git a/Dartagnan-SVCOMP.sh b/Dartagnan-SVCOMP.sh
@@ -21,8 +21,6 @@ else
     export DAT3M_HOME=$(pwd)
     export DAT3M_OUTPUT=$DAT3M_HOME/output
 
-    export OPTFLAGS="-mem2reg -sroa -early-cse -indvars -loop-unroll -fix-irreducible -loop-simplify -simplifycfg -gvn"
-
     skip_assertions_of_type="--program.processing.skipAssertionsOfType=USER"
     if [[ $propertypath == *"no-overflow.prp"* ]]; then
         export CFLAGS="-fgnu89-inline -fsanitize=signed-integer-overflow"

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
@@ -251,7 +251,7 @@ private static void generateWitnessIfAble(VerificationTask task, ProverEnvironme
         // ------------------ Generate Witness, if possible ------------------
         final EnumSet<Property> properties = task.getProperty();
         if (task.getProgram().getFormat().equals(SourceLanguage.LLVM) && modelChecker.hasModel()
-                && properties.contains(PROGRAM_SPEC) && properties.size() == 1
+                && (properties.contains(PROGRAM_SPEC) || properties.contains(DATARACEFREEDOM)) && properties.size() == 1
                 && modelChecker.getResult() != UNKNOWN) {
             try {
                 WitnessBuilder w = WitnessBuilder.of(modelChecker.getEncodingContext(), prover,
@@ -319,6 +319,10 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
                     }
                     summary.append("=================================================\n");
                 }
+                if (props.contains(DATARACEFREEDOM) && FALSE.equals(model.evaluate(DATARACEFREEDOM.getSMTVariable(encCtx)))) {
+                    summary.append("============= SVCOMP data race found ============\n");
+                    summary.append("=================================================\n");
+                }
                 final List<Axiom> violatedCATSpecs = task.getMemoryModel().getAxioms().stream()
                         .filter(Axiom::isFlagged)
                         .filter(ax -> props.contains(CAT_SPEC)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java
@@ -664,9 +664,9 @@ private List<Event> inlinePthreadMutexUnlock(FunctionCall call) {
         final Expression lockAddress = call.getArguments().get(0);
         final Expression locked = expressions.makeOne(type);
         final Expression unlocked = expressions.makeZero(type);
-        return List.of(
+        return EventFactory.eventSequence(
                 EventFactory.Llvm.newLoad(oldValueRegister, lockAddress, Tag.C11.MO_RELAXED),
-                EventFactory.newAssert(expressions.makeEQ(oldValueRegister, locked), "Unlocking an already unlocked mutex"),
+                notToInline.contains(AssertionType.USER) ? null : EventFactory.newAssert(expressions.makeEQ(oldValueRegister, locked), "Unlocking an already unlocked mutex"),
                 EventFactory.Llvm.newStore(lockAddress, unlocked, Tag.C11.MO_RELEASE),
                 assignSuccess(errorRegister)
         );

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java
@@ -84,6 +84,9 @@ private static String getLtlPropertyFromSummary(String summary) {
         if (summary.contains("user assertion")) {
             return "CHECK( init(main()), LTL(G ! call(reach_error())))";
         }
+        if (summary.contains("SVCOMP data race found")) {
+            return "CHECK( init(main()), LTL(G ! data-race) )";
+        }
         throw new UnsupportedOperationException("Violation found for unsupported property");
     }
 

diff --git a/svcomp.properties b/svcomp.properties
@@ -2,3 +2,4 @@ method=eager
 encoding.integers=true
 svcomp.step=5
 svcomp.umax=27
+witness=graphml
diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java
@@ -127,7 +127,6 @@ public static void main(String[] args) throws Exception {
             cmd.add("svcomp.properties");
             cmd.add(String.format("--%s=%s", PROPERTY, r.property.asStringOption()));
             cmd.add(String.format("--%s=%s", BOUND, bound));
-            cmd.add(String.format("--%s=%s", WITNESS, GRAPHML.asStringOption()));
             cmd.add(String.format("--%s=%s", WITNESS_ORIGINAL_PROGRAM_PATH, programPath));
             cmd.addAll(filterOptions(config));