From 761ee4fd0e856974d9daeeaf1067398cd2fe5f44 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 20 Jan 2023 08:33:34 -0500 Subject: [PATCH] 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 | 11 ++++ intTests/test1807/test.bc | Bin 0 -> 2912 bytes intTests/test1807/test.c | 5 ++ intTests/test1807/test.saw | 23 +++++++ intTests/test1807/test.sh | 3 + .../src/Verifier/SAW/Simulator/SBV.hs | 26 +++++--- .../src/Verifier/SAW/Simulator/What4.hs | 26 +++++--- saw-core/src/Verifier/SAW/Simulator/Prims.hs | 62 ++++++++++++++---- 8 files changed, 124 insertions(+), 32 deletions(-) create mode 100644 intTests/test1807/Makefile create mode 100644 intTests/test1807/test.bc create mode 100644 intTests/test1807/test.c create mode 100644 intTests/test1807/test.saw create mode 100755 intTests/test1807/test.sh 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 0000000000000000000000000000000000000000..7a361c4b31a40d69fdbefc189b49d82af05e3562 GIT binary patch literal 2912 zcma)8e{5679lsYlzDIDL4MgBH&*nLS$Z9cuNoYuLQaN#2%$lhQV;j?$V#ju3m&9@2 zvt!4w=^49yZtG5lA=Oj)!&%WpwSU4uh;7vr;xtPm3k8NymPIHLfwB!)w6cn7XxsN} zV45~fJL|r8-@E&M-}lGod*@F3)UB7R5GqFq^{e?EU;ECl2fqHdi*Ib~mAWZdGpZ3f zU53!cG9!WkZH12GbtgOKlm}GW#@16*QoXaBt~My&>zA~zmUW)m*qPKeR<+Q&*DD%3 zQ;y(_v94>goYr=nD)Y?I=c_pTYbowCs%V`gN(<3UKwub$v0-;_VLT5m} zW~Tn}KcG=Tw85m{)Tz-Z9?!^v4#%AGai3y5D#wCYFk!)`5FGfJ1LksbR*q(H%%>0~ zx!ETNb2x+wMt0FtPp(G#<;!0;0u?9Q4Vc zGa8jcK^!yTaYW8g+~Nd#*JW5jhP4TH7F12JOH=I1gnl~CJ{M1oIdH_M7&FO4p-*wl zB#-9gNJehHEQdH8vtfwMwEosa<@GE20%#)|DwmAxJxc#v2_1>b%{_9=hoe44jK-r* zS;*okVk&&JB))89m;aY|Rt~k`NHI9y2N$C9_wa1Fk-0HIq)97J_(m7R|pAh0VF26TK%Vf87jIfVpD zGO}nYrp5$$kz7jmHT8`J^@yd41Ck=oeuwoO;BRH7~Q#QMkO)?A`ll1Cw_klJ(jxGy0F<=CRL z;?9EVK@J05=Wqn!7>|V<7CAhOG(r%M7UyKKbO4g?#GxD>v*FfkdAUV zx}bU};g}YWl?02s7qnQA@C!z@zdO0-tLaRIO<6J$>_jwD>JAz+lu{yGu}Nrijq=@o zs3K3CEU2J28nWu@P2HLFhWh=pO8c~6O4gbZo6&jj_eZebL`&?Uvs|%Z$`x$1H*93UY?R93ohiTHz=x;$e8uimI!vOz|^^=5k!QOgN(e_EAEvc{; z)~m*x_?QpxB_)XWN(41QCmu85vB%}0HX_M=v^=Tr zLy=9Zwwr3`TJ@+uQvpqahJ6ylI$svG=!GlKddloJ*9;Yx1-;GIP-wu zb&m)hvwLKC*cI@Yhx`FAXMTg{%xBy}B4H=K~FfNQu>#b1SB zY1@E6o3@o}X~Zk|yrlh1ojACwNu54f(5jo1a#~q$+Sc6stLANu=bJt_|I6O8`Z~gX zaB1()_g!k-)^us|!Y_K?#_t|ye)yIw=-6+<%Ul(7h*_lNj zL)~wJ&uy%L_c8)k&f#Fz-VS9kX>VP~pSa7;!t2;U%KffUU&86uJ-40A=RE*_%^E2J z&F4MLBVzJ3ZRw7|g|@Q^>lr92MSCvM1_hSMlm8tq4xu27Ta+Db@D~KV3cYs!T&B0y z(G64NVA(e_d&;RnZ>Vp`C5DQz_XpfVVUO1mZE5an-b11qj+zGpVMqjITMT(1^X4#+ zz-}KITKfJUxzKpfEAIC7^*t2{2Sop1!0X{i;$4E^8YjsIn|^jS|1lagB`6!x`q2s{ zb(A|P#GgYvLSM3|+DA+1y%(nDUui;9#0RwXWhp$a(~`RuO`f9+FftK3Wd&;5MD=H;yOok|f*-QcN-C{m5q%;) zktUCn^Y1|HUjflHsXmQr9)gW>X`Qzwas~1q^7ELx@Zo8EtJ6{S+Rd zQu9JmcfxeD;}cquJ=-U9a{gI+ zwogXlG1^g*0SFdl$w=1eT_uU{fo%lmU|WQ&Ji{2N-QAx4!QCD&RJGtOT@+8j7Igm$ KZ>170D*Go0Y`b&- literal 0 HcmV?d00001 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"