Add a test.

intTests/test2049/.gitignore

@@ -0,0 +1,3 @@
+*.rawlog
+*.log
+*.diff

intTests/test2049/Makefile

@@ -0,0 +1,12 @@
+CC = clang
+#CFLAGS = -g -frecord-command-line -O0
+CFLAGS = -g -O0
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c -emit-llvm $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc

intTests/test2049/Test.cry

@@ -0,0 +1,2 @@
+import Array
+type Table = Array [8] [8]

intTests/test2049/test.c

@@ -0,0 +1,12 @@
+#include <stdint.h>
+
+static uint8_t table[256];
+
+void assign(uint8_t k, uint8_t v) {
+   table[k] = v;
+}
+
+void zero(uint8_t k) {
+  assign(k, 0);
+}
+

intTests/test2049/test.log.1.good

@@ -0,0 +1,23 @@
+ Loading file "test.saw"
+ Assume override assign
+ Verifying zero ...
+ Simulating zero ...
+ Registering overrides for `assign`
+   variant `Symbol "assign"`
+ Matching 1 overrides of  assign ...
+ Branching on 1 override variants of assign ...
+ Applied override! assign
+ Checking proof obligations zero ...
+ Subgoal failed: zero test.saw:60:1: error: in ghost_value
+Literal equality postcondition
+
+ SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 334}
+ ----------Counterexample----------
+   zero::table: [1 := 1, <default> := 0]
+   zero::k: 1
+ ----------------------------------
+ Stack trace:
+"llvm_verify" (test.saw:60:1-60:12)
+Proof failed.
+
+FAILED

intTests/test2049/test.log.2.good

@@ -0,0 +1,23 @@
+ Loading file "test.saw"
+ Assume override assign
+ Verifying zero ...
+ Simulating zero ...
+ Registering overrides for `assign`
+   variant `Symbol "assign"`
+ Matching 1 overrides of  assign ...
+ Branching on 1 override variants of assign ...
+ Applied override! assign
+ Checking proof obligations zero ...
+ Subgoal failed: zero test.saw:60:1: error: in ghost_value
+Literal equality postcondition
+
+ SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 334}
+ ----------Counterexample----------
+   zero::table: [0 := 0, <default> := 1]
+   zero::k: 1
+ ----------------------------------
+ Stack trace:
+"llvm_verify" (test.saw:60:1-60:12)
+Proof failed.
+
+FAILED

intTests/test2049/test.saw

@@ -0,0 +1,60 @@
+// Test printing a counterexample that contains an array.
+
+enable_experimental;
+import "Test.cry";
+
+// make some ghost state
+casper <- declare_ghost_state "casper";
+
+// write a (correct) spec for assign; it updates the table with k := v
+let assign_spec = do {
+   // initial state
+   table <- llvm_fresh_cryptol_var "assign::table" {| Table |};
+
+   // get args
+   k <- llvm_fresh_var "k" (llvm_int 8);
+   v <- llvm_fresh_var "v" (llvm_int 8);
+
+   // updated state
+   let table' = {{ arrayUpdate table k v }};
+
+   // run the function
+   llvm_ghost_value casper table;
+   llvm_execute_func [crucible_term k, crucible_term v];
+   llvm_ghost_value casper table';
+};
+
+// write a (wrong) spec for zero; it sets an entry of the table to zero
+let zero_spec = do {
+   // make an initial state
+   table <- llvm_fresh_cryptol_var "zero::table" {| Table |};
+
+   // make an arg
+   k <- llvm_fresh_var "zero::k" (llvm_int 8);
+
+
+   // Restrict the args and initial state so the output is more
+   // deterministic. (There are still two possible counterexamples
+   // and we can't distinguish them without being able to assert
+   // equality of arrays, which Cryptol rejects.) (And actually
+   // there's infinitely many more but it's reasonable to assume
+   // the solver will return a minimal array model.)
+   llvm_assert {{ k == 1 }};
+   llvm_assert {{ arrayLookup table 0 == 0 }};
+   llvm_assert {{ arrayLookup table 1 == 1 }};
+
+   // use a wrong final state
+   let table' = table;
+
+   // run the function
+   llvm_ghost_value casper table;
+   llvm_execute_func [crucible_term k];
+   llvm_ghost_value casper table';
+};
+
+mod <- llvm_load_module "test.bc";
+
+// (we could verify assign, but it's giving me noise about the static
+// allocation and that's not the point here)
+assign <- llvm_unsafe_assume_spec mod "assign" assign_spec;
+llvm_verify mod "zero" [assign] false zero_spec w4;

intTests/test2049/test.sh

@@ -0,0 +1,47 @@
+# Don't exit randomly
+set +e
+
+#
+# This is a hacked subset of what's in support/test-and-diff.sh
+# because we need to be able to check either of two reference outputs.
+# FUTURE: update test-and-diff to support that.
+#
+# to clean: rm -f test.log test.rawlog *.diff
+# 
+
+# run the test
+$SAW test.saw > test.rawlog 2>&1 || echo FAILED >> test.rawlog
+
+# Prune the timestamps and the current directory
+CURDIR=$(pwd -P || pwd)
+sed < test.rawlog > test.log '
+    /^\[[0-9][0-9]:[0-9][0-9]:[0-9][0-9]\.[0-9][0-9][0-9]\] /{
+        s/^..............//
+    }
+    s,'"$CURDIR"'/,,
+'
+
+# diff
+diff -u test.log.1.good test.log > test.log.1.diff 2>&1
+diff -u test.log.1.good test.log > test.log.2.diff 2>&1
+
+# If both diffs are nonempty, we failed.
+if [ -s test.log.1.diff ] && [ -s test.log.2.diff ]; then
+    echo "*** diff 1:"
+    cat test.log.1.diff
+    echo "*** diff 2:"
+    cat test.log.2.diff
+
+    cat 1>&2 <<EOF
+Unexpected test diffs.
+If the new output is correct, update the reference outputs, but
+please don't do so without thinking. Be sure to make corresponding
+updates to all the reference outputs.
+EOF
+
+    # We failed.
+    exit 1
+fi
+
+# done
+exit 0