saw-core: Fix bug involving incorrect maximum values in selectV

intTests/test1807/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/test1807/test.c

@@ -0,0 +1,5 @@
+#include <stdint.h>
+
+uint8_t get_last(uint8_t* array, uint8_t size) {
+    return array[size - 1];
+}

intTests/test1807/test.saw

@@ -0,0 +1,23 @@
+m <- llvm_load_module "test.bc";
+
+let ptr_to_fresh_readonly (name : String) (type : LLVMType) = do {
+    x <- llvm_fresh_var name type;
+    p <- llvm_alloc_readonly type;
+    llvm_points_to p (llvm_term x);
+    return (x, p);
+};
+
+let get_spec size pos = do {
+    // Generate a fresh array and pointer to that array
+    (x, xp) <- ptr_to_fresh_readonly "x" (llvm_array size (llvm_int 8));
+
+    // Call the C function
+    llvm_execute_func [xp, llvm_term {{`size : [8]}}];
+
+    // Use Cryptol to access the correct position
+    let ret = {{x @ (`pos : [8])}};
+    // Return it using llvm_return
+    llvm_return (llvm_term ret);
+};
+
+last_100_ov <- llvm_verify m "get_last"  [] true (get_spec 100 100) z3;

intTests/test1807/test.sh

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

saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs

@@ -314,21 +314,27 @@ lazyMux muxFn c tm fm =
       f <- fm
       muxFn c t f
 
--- @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 =
+-- @selectV merger valueFn vx@ treats @vx@ as an index, represented
+-- as a big-endian list of bits. It does a binary lookup by constructing a mux
+-- tree, using @merger@ as an if-then-else operator.
+--
+-- This is very similar to @selectV@ in @saw-core:Verifier.SAW.Simulator.Prims@,
+-- but specialized to SBV's needs. For more information on how this works, see
+-- the comments for @selectV@ in @saw-core@.
+selectV :: forall b. (SBool -> b -> b -> b) -> (Natural -> b) -> SWord -> b
+selectV merger valueFn vx =
   case svAsInteger vx of
     Just i
       | i >= 0    -> valueFn (fromInteger i)
       | otherwise -> panic "selectV" ["expected nonnegative integer", show i]
     Nothing -> impl (intSizeOf vx) 0
   where
-    impl _ x | x > maxValue || x < 0 = valueFn maxValue
-    impl 0 y = valueFn y
-    impl i y =
+    -- INVARIANT: @y@ will never exceed @(2 ^ intSizeOf vx) - 1@ at any point,
+    -- as this is the maximum possible value that can be attained by setting all
+    -- @intSizeOf vx@ bits in the bitmask.
+    impl :: Int -> Natural -> b
+    impl 0 !y = valueFn y
+    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
@@ -531,7 +537,7 @@ streamGetOp =
     VNat n -> lookupSStream xs n
     VBVToNat _ w ->
       do ilv <- toWord w
-         selectV (lazyMux (muxBVal tp)) ((2 ^ intSizeOf ilv) - 1) (lookupSStream xs) ilv
+         selectV (lazyMux (muxBVal tp)) (lookupSStream xs) ilv
     v -> panic "SBV.streamGetOp" ["Expected Nat value", show v]
 
 

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

@@ -11,6 +11,7 @@
 -- (This module is derived from Verifier.SAW.Simulator.SBV)
 ------------------------------------------------------------------------
 
+{-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ConstraintKinds#-}
 {-# LANGUAGE DataKinds #-}
@@ -539,7 +540,7 @@ streamGetOp sym =
       VNat n -> lookupSStream xs n
       VBVToNat _ w ->
         do ilv <- toWord sym w
-           selectV sym (lazyMux @sym (muxBVal sym tp)) ((2 ^ SW.bvWidth ilv) - 1) (lookupSStream xs) ilv
+           selectV sym (lazyMux @sym (muxBVal sym tp)) (lookupSStream xs) ilv
       v -> panic "streamGetOp" ["Expected Nat value", show v]
 
 lookupSStream :: SValue sym -> Natural -> IO (SValue sym)
@@ -580,23 +581,28 @@ lazyMux muxFn c tm fm =
       f <- fm
       muxFn c t f
 
--- @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 sym merger valueFn vx@ treats @vx@ as an index, represented
+-- as a big-endian list of bits. It does a binary lookup by constructing a mux
+-- tree, using @merger@ as an if-then-else operator.
+--
+-- This is very similar to @selectV@ in @saw-core:Verifier.SAW.Simulator.Prims@,
+-- but specialized to What4's needs. For more information on how this works,
+-- see the comments for @selectV@ in @saw-core@.
 selectV :: forall sym b.
   Sym sym =>
   sym ->
-  (SBool sym -> IO b -> IO b -> IO b) -> Natural -> (Natural -> IO b) -> SWord sym -> IO b
-selectV sym merger maxValue valueFn vx =
+  (SBool sym -> IO b -> IO b -> IO b) -> (Natural -> IO b) -> SWord sym -> IO b
+selectV sym merger valueFn vx =
   case SW.bvAsUnsignedInteger vx of
     Just i  -> valueFn (fromInteger i :: Natural)
     Nothing -> impl (swBvWidth vx) 0
   where
+    -- INVARIANT: @y@ will never exceed @(2 ^ bvWidth vx) - 1@ at any point, as
+    -- this is the maximum possible value that can be attained by setting all
+    -- @bvWidth vx@ bits in the bitmask.
     impl :: Int -> Natural -> IO b
-    impl _ x | x > maxValue || x < 0 = valueFn maxValue
-    impl 0 y = valueFn y
-    impl i y = do
+    impl 0 !y = valueFn y
+    impl i !y = do
       -- 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

saw-core/src/Verifier/SAW/Simulator/Prims.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DoAndIfThenElse #-}
 {-# LANGUAGE ExistentialQuantification #-}
@@ -484,18 +485,55 @@ wordBinRel pack op =
 ------------------------------------------------------------
 -- Utility functions
 
--- @selectV mux maxValue valueFn v@ treats the vector @v@ as an
--- index, represented as a big-endian list of bits. It does a binary
--- lookup, using @mux@ as an if-then-else operator. If the index is
--- greater than @maxValue@, then it returns @valueFn maxValue@.
-selectV :: (b -> a -> a -> a) -> Int -> (Int -> a) -> Vector b -> a
-selectV mux maxValue valueFn v = impl len 0
+-- @selectV mux valueFn v@ treats the vector @v@ as an index, represented as a
+-- big-endian list of bits. It does a binary lookup by constructing a mux tree,
+-- using @mux@ as an if-then-else operator.
+--
+-- The leaves of the mux tree contain @valueFn x@, where each @x@ is a bitmask
+-- representing the path from the root to that particular leaf. For example,
+-- here is what a mux tree would look like for a vector @v@ of length 2:
+--
+--                              /\
+--                             /  \
+--                            /    \
+--                           /      \
+-- MSB of @x@:              0        1
+--                         /\        /\
+--                        /  \      /  \
+-- LSB of @x@:           0    1    0    1
+--                       |    |    |    |
+--                       |    |    |    |
+-- Value of @x@ in     0b00 0b01 0b10 0b11
+-- @valueFn x@          (0)  (1)  (2)  (3)
+selectV :: forall b a. (b -> a -> a -> a) -> (Int -> a) -> Vector b -> a
+selectV mux valueFn v = impl len 0
   where
     len = V.length v
     err = panic "selectV: impossible"
-    impl _ x | x > maxValue || x < 0 = valueFn maxValue
-    impl 0 x = valueFn x
-    impl i x = mux (vecIdx err v (len - i)) (impl j (x `setBit` j)) (impl j x) where j = i - 1
+
+    -- @impl i x@ recursively constructs the mux tree, where:
+    --
+    -- * @i@ counts down from @length v@ (the root of the tree) to @0@ (the
+    --   leaves of the tree)
+    --
+    -- * @x@ is the partial bitmask that has been computed thus far. Each
+    --   call to @impl i@ will set the @(i - 1)@th bit if @mux@ computes the
+    --   true branch, and will not set the @(i - 1)@th bit if @mux@ computes
+    --   the false branch.
+    --
+    -- INVARIANTS:
+    --
+    -- * @x@ will always be non-negative, as it starts at @0@ and increases
+    --   in value monotonically with each recursive call to @impl@. (We could
+    --   give @x@ the type 'Natural' to enforce this, but each of @selectV@'s
+    --   call sites expect an 'Int', using an 'Int' here is more convenient.)
+    --
+    -- * @x@ will never exceed @(2 ^ length v) - 1@ at any point, as this is the
+    --   maximum possible value that can be attained by setting all @length v@
+    --   bits in the bitmask.
+    impl :: Int -> Int -> a
+    impl 0 !x = valueFn x
+    impl i !x = mux (vecIdx err v (len - i)) (impl j (x `setBit` j)) (impl j x) where j = i - 1
 
 ------------------------------------------------------------
 -- Values for common primitives
@@ -775,9 +813,9 @@ atWithDefaultOp bp =
         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
+            lift $ selectV (lazyMuxValue bp tp) (force . vecIdx d xv) iv
           VWord xw ->
-            lift $ selectV (lazyMuxValue bp tp) (fromIntegral n - 1) (bpBvAtWithDefault bp (fromIntegral n) (force d) xw) iv -- FIXME dangerous fromIntegral
+            lift $ selectV (lazyMuxValue bp tp) (bpBvAtWithDefault bp (fromIntegral n) (force d) xw) iv -- FIXME dangerous fromIntegral
           _ -> throwE "atOp: expected vector"
 
       VIntToNat _i | bpIsSymbolicEvaluator bp -> panic "atWithDefault: symbolic integer TODO"
@@ -825,7 +863,7 @@ updOp bp =
       VBVToNat _sz (VVector iv) | bpIsSymbolicEvaluator bp -> lift $
         do let update i = return (VVector (xv V.// [(i, y)]))
            iv' <- V.mapM (liftM toBool . force) iv
-           selectV (lazyMuxValue bp (VVecType n tp)) (fromIntegral n - 1) update iv' -- FIXME dangerous fromIntegral
+           selectV (lazyMuxValue bp (VVecType n tp)) update iv'
 
       VIntToNat _ | bpIsSymbolicEvaluator bp -> panic "updOp: symbolic integer TODO"