diff --git a/intTests/test2049/.gitignore b/intTests/test2049/.gitignore new file mode 100644 index 000000000..4619758de --- /dev/null +++ b/intTests/test2049/.gitignore @@ -0,0 +1,3 @@ +*.rawlog +*.log +*.diff diff --git a/intTests/test2049/Makefile b/intTests/test2049/Makefile new file mode 100644 index 000000000..6039a6b05 --- /dev/null +++ b/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 diff --git a/intTests/test2049/Test.cry b/intTests/test2049/Test.cry new file mode 100644 index 000000000..6dab7d7b9 --- /dev/null +++ b/intTests/test2049/Test.cry @@ -0,0 +1,2 @@ +import Array +type Table = Array [8] [8] diff --git a/intTests/test2049/test.bc b/intTests/test2049/test.bc new file mode 100644 index 000000000..32d9f86fc Binary files /dev/null and b/intTests/test2049/test.bc differ diff --git a/intTests/test2049/test.c b/intTests/test2049/test.c new file mode 100644 index 000000000..42c357212 --- /dev/null +++ b/intTests/test2049/test.c @@ -0,0 +1,12 @@ +#include + +static uint8_t table[256]; + +void assign(uint8_t k, uint8_t v) { + table[k] = v; +} + +void zero(uint8_t k) { + assign(k, 0); +} + diff --git a/intTests/test2049/test.log.1.good b/intTests/test2049/test.log.1.good new file mode 100644 index 000000000..c355ee4da --- /dev/null +++ b/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, := 0] + zero::k: 1 + ---------------------------------- + Stack trace: +"llvm_verify" (test.saw:60:1-60:12) +Proof failed. + +FAILED diff --git a/intTests/test2049/test.log.2.good b/intTests/test2049/test.log.2.good new file mode 100644 index 000000000..1388b1fc8 --- /dev/null +++ b/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, := 1] + zero::k: 1 + ---------------------------------- + Stack trace: +"llvm_verify" (test.saw:60:1-60:12) +Proof failed. + +FAILED diff --git a/intTests/test2049/test.saw b/intTests/test2049/test.saw new file mode 100644 index 000000000..eb03abcbd --- /dev/null +++ b/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; diff --git a/intTests/test2049/test.sh b/intTests/test2049/test.sh new file mode 100755 index 000000000..a427e68de --- /dev/null +++ b/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 <