Merge pull request #1773 from GaloisInc/T1768

Fix two bugs in SAWCore's handing of infinite streams

Author: mergify[bot]

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.bc

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

intTests/test1703/test.c

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

intTests/test1703/test.cry

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

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

intTests/test1703/test.sh

@@ -0,0 +1,4 @@
+f : [2] -> [10]
+f x = take y
+  where
+    y = x # y

intTests/test1768/test.cry

@@ -0,0 +1,5 @@
+import "test.cry";
+print {{ f 0b11 }};
+print {{ f 0b10 }};
+print {{ f 0b00 }};
+sat z3 {{ \x -> f x == zero }};

intTests/test1768/test.saw

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

intTests/test1768/test.sh

@@ -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-sbv/src/Verifier/SAW/Simulator/SBV.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

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

@@ -769,21 +769,38 @@ atWithDefaultOp bp =
       VNat i ->
         case x of
           VVector xv -> lift (force (vecIdx d xv (fromIntegral i))) -- FIXME dangerous fromIntegral
-          VWord xw -> lift (VBool <$> bpBvAt bp xw (fromIntegral i)) -- FIXME dangerous fromIntegral
+          VWord xw -> lift (bpBvAtWithDefault bp (fromIntegral n) (force d) xw (fromIntegral i)) -- FIXME dangerous fromIntegral
           _ -> throwE "atOp: expected vector"
       VBVToNat _sz i | bpIsSymbolicEvaluator bp -> do
         iv <- lift (toBits (bpUnpack bp) i)
         case x of
           VVector xv ->
             lift $ selectV (lazyMuxValue bp tp) (fromIntegral n - 1) (force . vecIdx d xv) iv -- FIXME dangerous fromIntegral
           VWord xw ->
-            lift $ selectV (lazyMuxValue bp tp) (fromIntegral n - 1) (liftM VBool . bpBvAt bp xw) iv -- FIXME dangerous fromIntegral
+            lift $ selectV (lazyMuxValue bp tp) (fromIntegral n - 1) (bpBvAtWithDefault bp (fromIntegral n) (force d) xw) iv -- FIXME dangerous fromIntegral
           _ -> throwE "atOp: expected vector"
 
       VIntToNat _i | bpIsSymbolicEvaluator bp -> panic "atWithDefault: symbolic integer TODO"
 
       _ -> throwE $ "atOp: expected Nat, got " <> Text.pack (show idx)
 
+-- | @bpBvAtWithDefault bp w d vw i@ returns @bpBvAt bp vw i@ if @i@ is between
+-- @0@ (inclusive) and @w@ (exclusive), the bit width of @vw@. Otherwise, it
+-- returns @d@.
+bpBvAtWithDefault ::
+  VMonad l =>
+  BasePrims l ->
+  Int ->
+  MValue l ->
+  VWord l ->
+  Int ->
+  MValue l
+bpBvAtWithDefault bp w d vw i
+  | 0 <= i && i < w
+  = VBool <$> bpBvAt bp vw i
+  | otherwise
+  = d
+
 -- upd :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Nat -> a -> Vec n a;
 updOp :: (VMonadLazy l, Show (Extra l)) => BasePrims l -> Prim l
 updOp bp =