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

The `selectV` function had a `maxValue` argument that, in principle, was
supposed to represent the largest possible value of the index argument (treated
as a big-endian list of bits). In practice, however, this was always given the
length of the vector being indexed into minus 1! This led to subtle issues
where indexing vectors with seemingly out-of-bounds indices would succeed,
since the index value would be clamped to the length of the vector minus 1,
which is always in bounds.

This patch fixes the bug. Moreover, it turns out that the `maxValue` argument
is not actually needed to do `selectV`'s job, as its implementation always
upholds the invariant that the bitmask that it computes never exceeds the
largest possible value of the index argument. To make the code simpler, I have
removed the `maxValue` argument entirely, and I have added some more comments
in `selectV` in `saw-core`, as well as its cousins in `saw-core-sbv` and
`saw-core-what4`, to explain why this works.

Fixes #1807.

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"