Missing changes to fully support svcomp properties

Dartagnan-SVCOMP.sh

@@ -22,9 +22,17 @@ else
 
     export DAT3M_HOME=$(pwd)
     export DAT3M_OUTPUT=$DAT3M_HOME/output
-    export CFLAGS="-fgnu89-inline"
+
     export OPTFLAGS="-mem2reg -sroa -early-cse -indvars -loop-unroll -fix-irreducible -loop-simplify -simplifycfg -gvn"
 
+    if [[ $propertypath == *"no-overflow.prp"* ]]; then
+        export CFLAGS="-fgnu89-inline -fsanitize=signed-integer-overflow"
+    elif [[ $propertypath == *"valid-memsafety.prp"* ]]; then
+        export CFLAGS="-fgnu89-inline -fsanitize=null"
+    else
+        export CFLAGS="-fgnu89-inline"
+    fi
+
     cmd="java -jar svcomp/target/svcomp.jar --method=assume --program.processing.constantPropagation=false --encoding.integers=true --svcomp.step=5 --svcomp.umax=27 cat/svcomp.cat --svcomp.property="$propertypath" "$programpath" "$witness
     $cmd
-fi
+fi

dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java

@@ -195,12 +195,13 @@ public static void main(String[] args) throws Exception {
                 }
 
                 long endTime = System.currentTimeMillis();
-                System.out.print(generateResultSummary(task, prover, modelChecker));
+                String summary = generateResultSummary(task, prover, modelChecker);
+                System.out.print(summary);
                 System.out.println("Total verification time(ms): " + (endTime - startTime));
 
                 if (!o.runValidator()) {
                     // We only generate witnesses if we are not validating one.
-                    generateWitnessIfAble(task, prover, modelChecker);
+                    generateWitnessIfAble(task, prover, modelChecker, summary);
                 }
             }
         } catch (InterruptedException e) {
@@ -214,12 +215,13 @@ public static void main(String[] args) throws Exception {
         }
     }
 
-    private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker) {
+    private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker, String summary) {
         // ------------------ Generate Witness, if possible ------------------
         final EnumSet<Property> properties = task.getProperty();
         if (modelChecker.hasModel() && properties.contains(PROGRAM_SPEC)) {
             try {
-                WitnessBuilder w = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, modelChecker.getResult());
+                String ltlProperty = getLtlPropertyFromSummary(summary);
+                WitnessBuilder w = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, modelChecker.getResult(), ltlProperty);
                 if (w.canBeBuilt()) {
                     //  We can only write witnesses if the path to the original C file was given.
                     w.build().write();
@@ -230,6 +232,19 @@ private static void generateWitnessIfAble(VerificationTask task, ProverEnvironme
         }
     }
 
+    private static String getLtlPropertyFromSummary(String summary) {
+        if(summary.contains("integer overflow")) {
+            return "CHECK( init(main()), LTL(G ! overflow))";
+        }
+        if(summary.contains("invalid dereference")) {
+            return "CHECK( init(main()), LTL(G valid-deref))";
+        }
+        if(summary.contains("user assertion")) {
+            return "CHECK( init(main()), LTL(G ! call(reach_error())))";
+        }
+        throw new UnsupportedOperationException("Violation found for unsupported property");
+    }
+
     public static String generateResultSummary(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker) throws SolverException {
         // ----------------- Generate output of verification result -----------------
         final Program p = task.getProgram();

dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java

@@ -44,6 +44,7 @@ public class WitnessBuilder {
 	private final EncodingContext context;
 	private final ProverEnvironment prover;
 	private final String type;
+    private final String ltlProperty;
 
     // =========================== Configurables ===========================
 
@@ -59,14 +60,15 @@ public class WitnessBuilder {
 
 	private final Map<Event, Integer> eventThreadMap = new HashMap<>();
 
-	private WitnessBuilder(EncodingContext c, ProverEnvironment p, Result r) {
+	private WitnessBuilder(EncodingContext c, ProverEnvironment p, Result r, String ltl) {
 		context = checkNotNull(c);
 		prover = checkNotNull(p);
 		type = r.equals(FAIL) ? "violation" : "correctness";
+        ltlProperty = ltl;
 	}
 
-	public static WitnessBuilder of(EncodingContext context, ProverEnvironment prover, Result result) throws InvalidConfigurationException {
-		WitnessBuilder b = new WitnessBuilder(context, prover, result);
+	public static WitnessBuilder of(EncodingContext context, ProverEnvironment prover, Result result, String ltlProperty) throws InvalidConfigurationException {
+		WitnessBuilder b = new WitnessBuilder(context, prover, result, ltlProperty);
 		context.getTask().getConfig().inject(b);
 		return b;
 	}
@@ -83,7 +85,7 @@ public WitnessGraph build() {
 		graph.addAttribute(WITNESSTYPE.toString(), type + "_witness");
 		graph.addAttribute(SOURCECODELANG.toString(), "C");
 		graph.addAttribute(PRODUCER.toString(), "Dartagnan");
-		graph.addAttribute(SPECIFICATION.toString(), "CHECK( init(main()), LTL(G ! call(reach_error())))");
+		graph.addAttribute(SPECIFICATION.toString(), ltlProperty);
 		graph.addAttribute(PROGRAMFILE.toString(), originalProgramFilePath);
 		graph.addAttribute(PROGRAMHASH.toString(), getFileSHA256(new File(originalProgramFilePath)));
 		graph.addAttribute(ARCHITECTURE.toString(), "32bit");

dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java

@@ -44,7 +44,7 @@ public void BuildWriteEncode() throws Exception {
              ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
             IncrementalSolver modelChecker = IncrementalSolver.run(ctx, prover, task);
             Result res = modelChecker.getResult();
-            WitnessBuilder witnessBuilder = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, res);
+            WitnessBuilder witnessBuilder = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, res, "user assertion");
             config.inject(witnessBuilder);
             WitnessGraph graph = witnessBuilder.build();
             File witnessFile = new File(getOutputDirectory() + "/witness.graphml");

svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java

@@ -43,12 +43,10 @@ private void property(String p) {
         //TODO process the property file instead of assuming its contents based of its name
         if(p.contains("no-data-race")) {
             property = Property.DATARACEFREEDOM;
-        } else if(p.contains("unreach-call")) {
+        } else if(p.contains("unreach-call") || p.contains("no-overflow") || p.contains("valid-memsafety")) {
             property = Property.PROGRAM_SPEC;
         } else {
-            // To comply with SVCOMP qualification rules, we should return UNKNOWN
-            // instead of throwing an exception for unhandled properties
-            property = null;
+            throw new IllegalArgumentException("Unrecognized property " + p);
         }
     }