From 938d7f7ceb1e47481583afdb7ef8266311f07154 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sat, 3 Dec 2022 17:25:26 -0500 Subject: [PATCH] saw-core-what4: Build muxes of symbolic indexes in big-endian order SAWCore assumes the invariant that when indexing into an infinite stream using a symbolic index, the mux tree constructed over the index will test each bit in big-endian order. This is the responsibility of the `selectV` function found in `saw-core`, `saw-core-sbv`, and `saw-core-what4`. All of these functions save for `saw-core-what4`'s `selectV` were upholding this invariant, as `saw-core-what4`'s was testing each bit in little-endian order, resulting in the oddities observed in #1703. This corrects the mistake in `saw-core-what4'`s implementation, fixing #1703. It also leaves some more documentation to make the fact that each `selectV` should be proceeding in big-endian order more apparent. --- intTests/test1703/Makefile | 11 +++++++++++ intTests/test1703/test.bc | Bin 0 -> 2988 bytes intTests/test1703/test.c | 5 +++++ intTests/test1703/test.cry | 5 +++++ intTests/test1703/test.saw | 15 +++++++++++++++ intTests/test1703/test.sh | 3 +++ saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs | 14 +++++++++++--- .../src/Verifier/SAW/Simulator/What4.hs | 13 ++++++++++--- 8 files changed, 60 insertions(+), 6 deletions(-) create mode 100644 intTests/test1703/Makefile create mode 100644 intTests/test1703/test.bc create mode 100644 intTests/test1703/test.c create mode 100644 intTests/test1703/test.cry create mode 100644 intTests/test1703/test.saw create mode 100755 intTests/test1703/test.sh diff --git a/intTests/test1703/Makefile b/intTests/test1703/Makefile new file mode 100644 index 0000000000..f7abdbe50b --- /dev/null +++ b/intTests/test1703/Makefile @@ -0,0 +1,11 @@ +CC = clang +CFLAGS = -g -emit-llvm -frecord-command-line -O0 + +all: test.bc + +test.bc: test.c + $(CC) $(CFLAGS) -c $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc diff --git a/intTests/test1703/test.bc b/intTests/test1703/test.bc new file mode 100644 index 0000000000000000000000000000000000000000..cd5a518c33ace577f151340f63b8bd9b5e3e1ec8 GIT binary patch literal 2988 zcma)8Z%kX)6~B*Xd>vw*9|>(td3K&d6Io4+pG`&}hR()mLRO|i*KOI_iD!(#Zon8n z8yhE^p0V3UJ8yEjNVTSZFl{uY+85GBRkn2#;FM8hWi*N+#!zGwl6F%Xv9;?mty*`k z-DDp&O}p0pbM86!yz}RG?sb=Y?#5T@5voQA4QPc&zxJKq41N6{7oXbRC-+dWXVM~c zz6zo3RVD-zdKfxRHl1-TsgA2zd;2R?TD!Me(_mEna6o3CsOoxUdsmvZ*SBf(PuAGG zrn^IzO-)C3C>hrEO4ZKzI$Ilqe5t#ndY_A<8eHhRl<6l5S7z@dNQsgLO5*3VLu)2#;3Yrt+eKpcorx8 zv?MF7ekGL05mYpBs~+Pr#V?r*w@uvTq+xlc_9GK_HECEAxrL+wxJc6AiJTHf8Y!!U z{0iud$CXG3C(L*f5gCeKo#AeKjBCiaIm0c2su^x=jw{U=7Lwe9N>DxjD%cK-ZnHq`ZGGu!qZTU5EH!shfIb7}{=0RH|2_$?ZlyS%{-)l;3*?zVIx({ujY0-8;v;h^|kWgI~OEnhh&LwwehVCrJGf*I>G}A6ZC_|HB!DAc}UUIyfa;&)9FVY?FraIEJqqtQ+ zA>vbhe2A1DJ|q*gghV`H#uN9dL2XP{`Zdb99x$U!=8^~QZZUUD%wOl2I|4nh1PGbo zisf+6{lAj6?dq zwpsV#*HVsR@1tKj0@#b=c&@MK)2xm}!1%mz*~5KgGTfLq{D2~NNYP~2@~EGAA=Oqa zIA-0Q5RlIoIyT*oX&?)k_iDgXB?k5YhM|yi$>(me%$+&rRxk63&@_M5W!&7@wYp)r z0S0t8IA&9w7gLStLR-e&UMzH6nr~k!fR7!;?u+Aa7m0Wr0(e4c_`@P|N7Q{>0{H4~ z3A$Un?z3Jd$TBwt2FOoJ>OYp4&0gl7;NDm(-*Q`2*>ca(YrikFL9%8G)>Zf6qWkc) z`!IOD;(i=W@(2Y0Q(ya^UbkrA&NY-wT_hcYA46}67H!@}hz|3|gF|EYcVb?@C)_Uu5eli
$6LlKs{t=+(#XOT(l%+3Z3@)`WxG}{ zT!Emm9WX#!a8|P#B+x=ZX5ZJQo<7i`&73K++7^|PQSCGDYHj^h>n{6+mRB$Qvaf1i z6Cq!H=g?b+-?8s%d1vjsZe7oH}`OyVT@;Qrh3R zH;3MY`mck}ZLfj%G6q-AiBQhn3FR^CZeJ-(-R2hIb##%kzil#9@cQt}$_qux4ZtJB*cvBD(`{)zj z*85QdA%GQ!X&J#^HY9gqr`k}(6ZtlqK$jlKKdTqfBW3v)XS7AWwzaM*ub#Vf1kt~1 zDDp^-CT-1ib0z7;gDeuKvgVyCAH=SujuNvAJ!zz$5k{PvYAU1WkY;NB!o7dOv&WKw zCV#ASE$a8ONeXEjS*i{-sWF-oLkE5hoUeXPgb*1D8J8_j0b;hfhO{+P6peV-LdNCl z5D{u{_UO?reXF;Zt + +uint32_t weird(uint32_t cv[8], uint8_t i) { + return cv[i % 8]; +} diff --git a/intTests/test1703/test.cry b/intTests/test1703/test.cry new file mode 100644 index 0000000000..3bc9c7e1a6 --- /dev/null +++ b/intTests/test1703/test.cry @@ -0,0 +1,5 @@ +weird : [8][32] -> [8] -> [32] +weird cv i = k + where + k = cvs @ i + cvs = cv # cvs diff --git a/intTests/test1703/test.saw b/intTests/test1703/test.saw new file mode 100644 index 0000000000..46915636e5 --- /dev/null +++ b/intTests/test1703/test.saw @@ -0,0 +1,15 @@ +import "test.cry"; + +let weird_spec = do { + cv <- llvm_fresh_var "cv" (llvm_array 8 (llvm_int 32)); + cv_p <- llvm_alloc (llvm_array 8 (llvm_int 32)); + llvm_points_to cv_p (llvm_term {{ cv }}); + i <- llvm_fresh_var "i" (llvm_int 8); + + llvm_execute_func [cv_p, llvm_term i]; + + llvm_return (llvm_term {{ weird cv i }}); +}; + +m <- llvm_load_module "test.bc"; +llvm_verify m "weird" [] false weird_spec (w4_unint_z3 []); diff --git a/intTests/test1703/test.sh b/intTests/test1703/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test1703/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs index 9dc2bcb09b..979bb21af2 100644 --- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs +++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs @@ -314,8 +314,10 @@ lazyMux muxFn c tm fm = f <- fm muxFn c t f --- selectV merger maxValue valueFn index returns valueFn v when index has value v --- if index is greater than maxValue, it returns valueFn maxValue. Use the ite op from merger. +-- @selectV merger maxValue valueFn vx@ treats @vx@ as an index, represented +-- as a big-endian list of bits. It does a binary lookup, using @merger@ as an +-- if-then-else operator. If the index is greater than @maxValue@, then it +-- returns @valueFn maxValue@. selectV :: (SBool -> b -> b -> b) -> Natural -> (Natural -> b) -> SWord -> b selectV merger maxValue valueFn vx = case svAsInteger vx of @@ -326,7 +328,13 @@ selectV merger maxValue valueFn vx = where impl _ x | x > maxValue || x < 0 = valueFn maxValue impl 0 y = valueFn y - impl i y = merger (svTestBit vx j) (impl j (y `setBit` j)) (impl j y) where j = i - 1 + impl i y = + -- NB: `i` counts down in each iteration, so we use svTestBit (a + -- little-endian indexing function) to ensure that the bits are processed + -- in big-endian order. Alternatively, we could have `i` count up and use + -- svAt (a big-endian indexing function), but we use svTestBit as it is + -- slightly cheaper to compute. + merger (svTestBit vx j) (impl j (y `setBit` j)) (impl j y) where j = i - 1 -- Big-endian version of svTestBit svAt :: SWord -> Int -> SBool diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index e5789d8525..9205af1b23 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -580,8 +580,10 @@ lazyMux muxFn c tm fm = f <- fm muxFn c t f --- selectV merger maxValue valueFn index returns valueFn v when index has value v --- if index is greater than maxValue, it returns valueFn maxValue. Use the ite op from merger. +-- @selectV sym merger maxValue valueFn vx@ treats @vx@ as an index, represented +-- as a big-endian list of bits. It does a binary lookup, using @merger@ as an +-- if-then-else operator. If the index is greater than @maxValue@, then it +-- returns @valueFn maxValue@. selectV :: forall sym b. Sym sym => sym -> @@ -595,7 +597,12 @@ selectV sym merger maxValue valueFn vx = impl _ x | x > maxValue || x < 0 = valueFn maxValue impl 0 y = valueFn y impl i y = do - p <- SW.bvAtBE sym vx (toInteger j) + -- NB: `i` counts down in each iteration, so we use bvAtLE (a + -- little-endian indexing function) to ensure that the bits are processed + -- in big-endian order. Alternatively, we could have `i` count up and use + -- bvAtBE (a big-endian indexing function), but we use bvAtLE as it is + -- slightly cheaper to compute. + p <- SW.bvAtLE sym vx (toInteger j) merger p (impl j (y `setBit` j)) (impl j y) where j = i - 1 instance Show (SArray sym) where