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

@@ -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

intTests/test1703/test.c

@@ -0,0 +1,5 @@
+#include <stdint.h>
+
+uint32_t weird(uint32_t cv[8], uint8_t i) {
+    return cv[i % 8];
+}

intTests/test1703/test.cry

@@ -0,0 +1,5 @@
+weird : [8][32] -> [8] -> [32]
+weird cv i = k
+    where
+        k = cvs @ i
+        cvs = cv # cvs

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 []);

intTests/test1703/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

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

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