add trace-constraints test

tests/TestBase.hs

@@ -159,7 +159,7 @@ doTest mwb cfg _sv fp = do
       logs <- IOR.readIORef logsRef
       T.assertFailure (msg ++ "\n" ++ (intercalate "\n" (reverse logs)))
 
-  (dir, rcfg) <- case argFileExists of
+  (dir, rcfg) <- case argFileExists && not (isJust mwb) of
     True -> do
       rawOpts <- readFile (fp <.> "args")
       let optsList = filter (\s -> s /= "") $ (concat ((map (splitOn " ") (splitOn "\n" rawOpts))))

tests/aarch32/trace-constraints.args

@@ -0,0 +1,5 @@
+-o trace-constraints.original.exe
+-p trace-constraints.patched.exe
+-b trace-constraints.toml
+--script trace-constraints.pate
+--add-trace-constraints

tests/aarch32/trace-constraints.expect

@@ -0,0 +1 @@
+ConditionallyEquivalent

tests/aarch32/trace-constraints.pate

@@ -0,0 +1,29 @@
+Choose Entry Point
+    > Function Entry "_start"
+
+Function Entry "_start"
+    Handle observable difference:
+    > Avoid difference with equivalence condition
+
+Verification Finished
+    Continue verification?
+    > Finish and view final result
+
+
+Final Result
+    Assumed Equivalence Conditions
+        ? Function Entry "_start"
+
+    Regenerate result with new trace constraints?
+        > True
+
+    Waiting for constraints..
+        > [ [ { "var": { "symbolic_ident" : 239 }, "op" : "EQ", "const" : "0" }, { "var": { "symbolic_ident" : -904 }, "op" : "EQ", "const" : "0" }, { "var": { "symbolic_ident" : 190 }, "op" : "EQ", "const" : "0" }, { "var": { "symbolic_ident" : 223 }, "op" : "EQ", "const" : "0" } ] ]
+
+    // above constraint satisfies the equivalence relation
+    Assumed Equivalence Conditions
+        Function Entry "_start"
+        ? true
+
+    Regenerate result with new trace constraints?
+        > False

tests/aarch32/trace-constraints.toml

@@ -0,0 +1 @@
+observable-memory = [ { start-address = 0x0003f000, length=4000 } ]

tests/src/trace-constraints.original.c

@@ -0,0 +1,20 @@
+#include "util.h"
+
+void _start();
+
+int h;
+int f;
+int i;
+int dump;
+int g __attribute__((section(".output"))) = -12;
+int j __attribute__((section(".output"))) = -12;
+
+void _start() {
+  dump = h;
+  dump = i;
+
+  if (h == 0){
+    g = f;
+  }
+  j = i;
+}

tests/src/trace-constraints.patched-bad.c

@@ -0,0 +1,20 @@
+#include "util.h"
+
+void _start();
+
+int h;
+int f;
+int i;
+int dump;
+int g __attribute__((section(".output"))) = -12;
+int j __attribute__((section(".output"))) = -12;
+
+void _start() {
+  dump = h;
+  dump = i;
+
+  if (h == 1){
+    g = f;
+  }
+  j = i;
+}

tests/src/trace-constraints.patched.c

@@ -0,0 +1,20 @@
+#include "util.h"
+
+void _start();
+
+int h;
+int f;
+int i;
+int dump;
+int g __attribute__((section(".output"))) = -12;
+int j __attribute__((section(".output"))) = -12;
+
+void _start() {
+  dump = h;
+  dump = i;
+
+  if (i == 0){
+    g = f;
+  }
+  j = i;
+}

tests/template.mk

@@ -44,9 +44,11 @@ malloc-%.exe: ./build/malloc-%.s ./build/link.ld
 	diff ./dumps/$(basename $@).original.dump ./dumps/$(basename $@).patched-bad.dump || true
 
 %.test_run: %.original.exe %.patched.exe
-	../../pate.sh -o $(basename $@).original.exe -p $(basename $@).patched.exe \
-		`( (test -f $(basename $@).toml && echo "-b $(basename $@).toml") || echo "")` \
-		`( (test -f $(basename $@).pate && echo "--script $(basename $@).pate") || echo "")` \
+	../../pate.sh \
+	    `( (!(test -f $(basename $@).args) && echo "-o $(basename $@).original.exe -p $(basename $@).patched.exe") || echo "")` \
+		`( (!(test -f $(basename $@).args) && (test -f $(basename $@).toml && echo "-b $(basename $@).toml")) || echo "")` \
+		`( (!(test -f $(basename $@).args) && (test -f $(basename $@).pate && echo "--script $(basename $@).pate")) || echo "")` \
+		`( (test -f $(basename $@).args && cat $(basename $@).args) || echo "")` \
 		--no-assume-stack-scope
 
 .PRECIOUS: ./build/%.s ./build/%.i %.exe malloc-%.exe ./unequal/%.original.exe ./unequal/%.patched.exe