Improvements for SVCOMP 2025

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"

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)

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)
         );

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");
     }
 

svcomp.properties

@@ -2,3 +2,4 @@ method=eager
 encoding.integers=true
 svcomp.step=5
 svcomp.umax=27
+witness=graphml

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));