From 7746cc18837b217749ff75cfc5c8a3a25e94be97 Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 4 Sep 2024 23:25:02 -0400 Subject: [PATCH] Add a test. --- intTests/test2049/.gitignore | 3 ++ intTests/test2049/Makefile | 12 ++++++ intTests/test2049/Test.cry | 2 + intTests/test2049/test.bc | Bin 0 -> 3520 bytes intTests/test2049/test.c | 12 ++++++ intTests/test2049/test.log.1.good | 23 ++++++++++++ intTests/test2049/test.log.2.good | 23 ++++++++++++ intTests/test2049/test.saw | 60 ++++++++++++++++++++++++++++++ intTests/test2049/test.sh | 47 +++++++++++++++++++++++ 9 files changed, 182 insertions(+) create mode 100644 intTests/test2049/.gitignore create mode 100644 intTests/test2049/Makefile create mode 100644 intTests/test2049/Test.cry create mode 100644 intTests/test2049/test.bc create mode 100644 intTests/test2049/test.c create mode 100644 intTests/test2049/test.log.1.good create mode 100644 intTests/test2049/test.log.2.good create mode 100644 intTests/test2049/test.saw create mode 100755 intTests/test2049/test.sh 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 0000000000000000000000000000000000000000..32d9f86fc21577ef5bd0476094b8a33cee44296d GIT binary patch literal 3520 zcmbUkZERE5^*%qx?~ypq4rIkyp3O6c)};_T2?-8PG&>H|luUI7Lz&7Jzc>y~$;XSI z6>QI!FKtn}o+R}}w)w**X zXsi9)mCwEBoOkZI=bU@)x!3bk>x&SyQh;7o{?nLx;_MW~QOs7Pf-Dv*5yfJ#`7yJyvVH2SK#6U2yia{*mu zQvar1((h6=o+xS@(N~o^Xv5yZs>V^TFk`kftyPkG_X$Z=h;2VT_UO)M+{r6 zTT+$JO&&bX&CG({V;n+y7^^nYYq<8^$o#~nalLsnbY+iekDf~T8#@kin>vR5XX;c< zL_xcHO1rL7?;kz0#nPNBkrIUqEMbNDEe3>S7|RcCzK?w+1hmFVx{5L!mvfsk6UNIE z#S4qZE7Qj133iDPltDqM^($eT647YXOAUs|s8tbZDjFh>Se5>?GMG|o&nXd(8gfyH zK^f!xMDa4HB1{Wrb!Ou1?HvfK2b-*m;j;W9Br zN}wvGh*oMSB=<|o5W=e`urD8)88mDHo$pMr%M-=92^Ng`#0}a^QVp$y$En&@xj&`! z`{fz~6`!SI;1S@QGMJ{YsT>H9qNLQ)R6Il-nIcz7$0R9+s3=IA`5-!peUVCFe|{*>VmqVpu~3jN+UT^fD56E+7j5s!VV~N}5y2HIF`dLG3wFf-)P^>|Q~g30p_1tchW6n+u=a*C7UP!dOj9 z?93wDSxPjFdK@F!WTQmIW0W}Fuf2tIpX!-=5>u^hG-alZkWroXg1neqo+BG(Jq<~+ zAs0(V1nLN6i&qf@YDgfXF-72%vRnysC&et(j9SKo8LJ)dthlG<{fMl~$(fb9Uc2H8b9aIHYKpmIC);P?{7$ft@X%l9*~?~j22KR8xtj9S&3fv_^ZmK3W6a}#%pJ?x zV9{@eo$r&*$*lHbmm;((VL^_B@Ww|BN+hk6y|Yhu7wNw6F-s}thD*1|F?YZV&T70q zjgQzBGkZN@y1u|JEgC-|Or3@n$E0WHN!gk6ZF=B{Um1*1vGJDXdnp}`fa%%%xi%Z; zr;RTVCTy_TxWa4pAC(=staH-S00H?XQ@`YKjslrYzEudGDuZATO$}M8@Oa|j4Lx&b zin-}yzO-AWueeQ1i|el~8t1_PZ<%vaZa6EKk7ON5PhBose{Q;NHVZ!1=e%e8p@{jZ zeh6TzQudDv%pJe((*?~6r@Lv_-Q;xt^fA49=7yaC^2-Iy?FDAZ$K1DDKDxt04KZF@ zTz|)Gyk$1dn2oT5%jON8+$+xWo`!Q|-I!dLYdsIU56%vOon9yfO4;8&W2@iYa#w2ecm;0QLme~X8aT~%ZVK3$MZCW{ zP;%4mG0Ou6O7tpiY2`Ty=Dt2g)F-p`V_Cg#P9 zL)@O;&c277!9a))w~1XtLEjz^*Bp!ny9Wj%e0z7WGtBn{w+Ve+y^&xz z5)>m90o%_-P-^Q4^>ugiy&X0o-1lrS5D{%rVE5U?&_KIQQo0jwz)<9meepy(E$=K`ST5QnFOsa$1Eg}uVgS@Ya&l{I#IMI~^mDrz3jn`CS5 zY7g__xUC7>*(U_UHcwwq517*2)f?R3*VirDz;)5~Q$FzYzSat{rij7gTul2KNk6Zxx)x`9)L}QW*?SHE%dR5rRzI_^yU4B~%hm88nerW&N+zJ3!ArppRS-$2eoiZwHdkxMd~e&m za!pn!`9Mn^@B*X%ZM*McjgR2gpyu_4eHt=-d|K-+)9y#`tof2fWe!?G>l&mFPEJ#4 zP!4Tsd%D`CAR zmkZteC9i+Dsy*<=VX^Co<+Z>QVr8Jn`EvQqYvcE3d3;G!cEgEjKkT($EI#BJA8}1u=)y_#z%BHUtb>C ze#6gv?1QqUTf)Ul_py(;Hz_5kxHVr@V+vFRTvJ+wlUc`E!g)$=7|W^-LxE=D9dn&y zmw4PS=ieoB6YT72A>gM8-91jX=+nX7P&Ar9kof6{-i2+zv7vJHr)1|zD6(WjTCRtJ zo66#V@*F}#9)Ly{}4S6q+|!^pKx&8ezOh~JN7 znwuo+guUBE??Oofi|FA5@zsCeX|VD&bXnZ#sx`Y>-Xf5;Tu+oBi-tnOe!uHHeEG@! zyd>_jNq39nW)UhV>C_h9I7XthIg@nr)_#P_LODaJri4Os!P7~91{rEO)kXwjuY%ZI znfwtASGTGitk2)*+;_@MC|LKT4jFfOGJ;)3IpkBdgF!f%D4V7TvLOq!UrKZps3 zx+ah5B?r3jxQcBGq)xdZfz?C|?)ZERCW#U)VQ&`@M{8bu5Bn^Ch8_PD`v|sQQd7v~ z9x0O>TNV)7t<|d3(~>mIUr75j4uoE*w7vu;bDZXZ{R{B#VYT&h2;sV0#ppMV5Wg#M zpkL)b1mR#+0=AYMi{ZV-G8+JJjx+;cUMm1@c*Opl!vwU=00w{t04!esfZN0G7{~Is zc>r(%Vi_z84t?yj4~`?|(_0aG25>A}4uEw$l=lOU=i`RI=lOXGp1 XC$z0jZ~Nc*ZCF8Det`#z|6uqp>vwK1 literal 0 HcmV?d00001 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 <