diff --git a/intTests/test1807/Makefile b/intTests/test1807/Makefile new file mode 100644 index 0000000000..f7abdbe50b --- /dev/null +++ b/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 diff --git a/intTests/test1807/test.bc b/intTests/test1807/test.bc new file mode 100644 index 0000000000..7a361c4b31 Binary files /dev/null and b/intTests/test1807/test.bc differ diff --git a/intTests/test1807/test.c b/intTests/test1807/test.c new file mode 100644 index 0000000000..b8578e7158 --- /dev/null +++ b/intTests/test1807/test.c @@ -0,0 +1,5 @@ +#include + +uint8_t get_last(uint8_t* array, uint8_t size) { + return array[size - 1]; +} diff --git a/intTests/test1807/test.saw b/intTests/test1807/test.saw new file mode 100644 index 0000000000..f9f0dcea32 --- /dev/null +++ b/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; diff --git a/intTests/test1807/test.sh b/intTests/test1807/test.sh new file mode 100755 index 0000000000..adf8b97c7a --- /dev/null +++ b/intTests/test1807/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 979bb21af2..b9db4d08c9 100644 --- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs +++ b/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] diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index 9205af1b23..9d50d07e0b 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Simulator/Prims.hs b/saw-core/src/Verifier/SAW/Simulator/Prims.hs index a226e66e30..99f6582837 100644 --- a/saw-core/src/Verifier/SAW/Simulator/Prims.hs +++ b/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"