Skip to content

Commit 80e5091

Browse files
RyanGlScottRyanGlScott
committed
Don't treat struct padding as invalid memory with stable-symbolic
When `laxLoadsAndStores` + `stable-symbolic` are enabled, all allocations are backed by fresh SMT arrays. When writing a struct to one of these arrays, we traverse through the array byte-by-byte, loading each byte in the struct and updating the array's value accordingly. Things went awry in the case where the struct has padding, however, as the code in `crucible-llvm` assumed that loading struct padding should always be an error. Not only is this possible with `stable-symbolic`, it has a sensible interpretation: whenever loading a byte of struct padding, just skip updating the array value corresponding to that byte. See GaloisInc/saw-script#1684 for the motivation behind this bugfix. I haven't found a way to trigger the same bug with `crux-llvm`, but I can trigger it programatically using the `crucible-llvm` API. I've added a test case to the `crucible-llvm` test suite to ensure that the bug remains fixed.
1 parent de7372e commit 80e5091

File tree

4 files changed

+119
-30
lines changed

4 files changed

+119
-30
lines changed

‎crucible-llvm/crucible-llvm.cabal

+1
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,7 @@ test-suite crucible-llvm-tests
135135
crucible-llvm,
136136
directory,
137137
filepath,
138+
lens,
138139
llvm-pretty,
139140
llvm-pretty-bc-parser,
140141
mtl,

‎crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Common.hs

+2-1
Original file line numberDiff line numberDiff line change
@@ -446,7 +446,8 @@ data ValueLoad v
446446
| LastStore ValueView
447447
-- ^ Load consists of valid bytes within the stored value.
448448
| InvalidMemory StorageType
449-
-- ^ Load touches invalid memory (e.g. trying to read struct padding bytes as a bitvector).
449+
-- ^ Load touches invalid memory. Currently, this can only arise when
450+
-- trying to read struct padding bytes as a bitvector.
450451
deriving (Functor,Show)
451452

452453
loadBitvector :: Addr -> Bytes -> Addr -> ValueView -> ValueCtor (ValueLoad Addr)

‎crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs

+53-29
Original file line numberDiff line numberDiff line change
@@ -1259,52 +1259,76 @@ writeMemWithAllocationCheck is_allocated sym w gsym ptr tp alignment val mem = d
12591259
, case val of
12601260
LLVMValInt block _ -> (asNat block) == (Just 0)
12611261
_ -> True -> do
1262-
let subFn :: ValueLoad Addr -> IO (PartLLVMVal sym)
1262+
let -- Return @Just value@ if we have successfully loaded a value and
1263+
-- should update the corresponding index in the array with that
1264+
-- value. Return @Nothing@ otherwise.
1265+
subFn :: ValueLoad Addr -> IO (Maybe (PartLLVMVal sym))
12631266
subFn = \case
1264-
LastStore val_view -> applyView
1267+
LastStore val_view -> fmap Just $ applyView
12651268
sym
12661269
(memEndianForm mem)
12671270
mop
12681271
(Partial.totalLLVMVal sym val)
12691272
val_view
1270-
InvalidMemory tp'-> Partial.partErr sym mop $ Invalid tp'
1273+
InvalidMemory tp'
1274+
| -- With stable-symbolic, loading struct padding is
1275+
-- permissible. This is the only case that can return
1276+
-- Nothing.
1277+
laxLoadsAndStores ?memOpts
1278+
, indeterminateLoadBehavior ?memOpts == StableSymbolic
1279+
-> pure Nothing
1280+
1281+
| otherwise
1282+
-> fmap Just $ Partial.partErr sym mop $ Invalid tp'
12711283
OldMemory off _ -> panic "Generic.writeMemWithAllocationCheck"
12721284
[ "Unexpected offset in storage type"
12731285
, "*** Offset: " ++ show off
12741286
, "*** StorageType: " ++ show tp
12751287
]
12761288

1289+
-- Given a symbolic array and an index into the array, load a byte
1290+
-- from the corresponding position in memory and store the byte into
1291+
-- the array at that index.
12771292
storeArrayByteFn ::
12781293
SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8) ->
12791294
Offset ->
12801295
IO (SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))
12811296
storeArrayByteFn acc_arr off = do
1282-
partial_byte <- genValueCtor sym (memEndianForm mem) mop
1283-
=<< traverse subFn (loadBitvector off 1 0 (ValueViewVar tp))
1284-
1285-
case partial_byte of
1286-
Partial.NoErr _ (LLVMValInt _ byte)
1287-
| Just Refl <- testEquality (knownNat @8) (bvWidth byte) -> do
1288-
idx <- bvAdd sym (llvmPointerOffset ptr)
1289-
=<< bvLit sym w (bytesToBV w off)
1290-
arrayUpdate sym acc_arr (Ctx.singleton idx) byte
1291-
1292-
Partial.NoErr _ (LLVMValZero _) -> do
1293-
byte <- bvLit sym knownRepr (BV.zero knownRepr)
1294-
idx <- bvAdd sym (llvmPointerOffset ptr)
1295-
=<< bvLit sym w (bytesToBV w off)
1296-
arrayUpdate sym acc_arr (Ctx.singleton idx) byte
1297-
1298-
Partial.NoErr _ v ->
1299-
panic "wrietMemWithAllocationCheck"
1300-
[ "Expected byte value when updating SMT array, but got:"
1301-
, show v
1302-
]
1303-
Partial.Err _ ->
1304-
panic "wrietMemWithAllocationCheck"
1305-
[ "Expected succesful byte load when updating SMT array"
1306-
, "but got an error instead"
1307-
]
1297+
vc <- traverse subFn (loadBitvector off 1 0 (ValueViewVar tp))
1298+
mb_partial_byte <- traverse (genValueCtor sym (memEndianForm mem) mop)
1299+
(sequenceA vc)
1300+
1301+
case mb_partial_byte of
1302+
Nothing ->
1303+
-- If we cannot load the byte from memory, skip updating the
1304+
-- array. Currently, the only way that this can arise is when
1305+
-- a byte of struct padding is loaded with StableSymbolic
1306+
-- enabled.
1307+
pure acc_arr
1308+
Just partial_byte ->
1309+
case partial_byte of
1310+
Partial.NoErr _ (LLVMValInt _ byte)
1311+
| Just Refl <- testEquality (knownNat @8) (bvWidth byte) -> do
1312+
idx <- bvAdd sym (llvmPointerOffset ptr)
1313+
=<< bvLit sym w (bytesToBV w off)
1314+
arrayUpdate sym acc_arr (Ctx.singleton idx) byte
1315+
1316+
Partial.NoErr _ (LLVMValZero _) -> do
1317+
byte <- bvLit sym knownRepr (BV.zero knownRepr)
1318+
idx <- bvAdd sym (llvmPointerOffset ptr)
1319+
=<< bvLit sym w (bytesToBV w off)
1320+
arrayUpdate sym acc_arr (Ctx.singleton idx) byte
1321+
1322+
Partial.NoErr _ v ->
1323+
panic "writeMemWithAllocationCheck"
1324+
[ "Expected byte value when updating SMT array, but got:"
1325+
, show v
1326+
]
1327+
Partial.Err _ ->
1328+
panic "writeMemWithAllocationCheck"
1329+
[ "Expected succesful byte load when updating SMT array"
1330+
, "but got an error instead"
1331+
]
13081332

13091333
res_arr <- foldM storeArrayByteFn arr [0 .. (sz - 1)]
13101334
overwriteArrayMem sym w ptr res_arr arr_sz mem

‎crucible-llvm/test/TestMemory.hs

+63
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ module TestMemory
1212
)
1313
where
1414

15+
import Control.Lens ( (^.), _1, _2 )
1516
import Control.Monad ( foldM, forM_, void )
1617
import Data.Foldable ( foldlM )
1718
import qualified Data.Vector as V
@@ -33,6 +34,7 @@ import qualified What4.SatResult as W4Sat
3334

3435
import qualified Lang.Crucible.Backend as CB
3536
import qualified Lang.Crucible.Backend.Online as CBO
37+
import qualified Lang.Crucible.Simulator as CS
3638
import qualified Lang.Crucible.Types as Crucible
3739

3840
import Lang.Crucible.LLVM.DataLayout ( noAlignment )
@@ -51,6 +53,7 @@ memoryTests = T.testGroup "Memory"
5153
, testMemArrayWithConstants
5254
, testMemArray
5355
, testPointerStore
56+
, testStructStore
5457
, testMemArrayCopy
5558
, testMemArraySet
5659
, testMemInvalidate
@@ -538,3 +541,63 @@ testPointerStore = testCase "pointer store" $ withMem LLVMD.BigEndian $ \bak mem
538541
goal <- What4.notPred sym p
539542
res <- checkSat bak goal
540543
True @=? W4Sat.isUnsat res
544+
545+
-- | Test storing and retrieving a struct with and without 'laxLoadsAndStores'
546+
-- enabled.
547+
testStructStore :: T.TestTree
548+
testStructStore = testCase "struct store" $ withMem LLVMD.BigEndian $ \bak mem0 ->
549+
do let sym = CB.backendGetSym bak
550+
sz <- What4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth 64
551+
let struct_storage_type = LLVMMem.mkStructType $ V.fromList
552+
[ (LLVMMem.bitvectorType 2, 2)
553+
, (LLVMMem.bitvectorType 4, 0)
554+
]
555+
let w16 = knownNat @16
556+
let w32 = knownNat @32
557+
let struct_type_repr = Crucible.StructRepr $
558+
Ctx.Empty Ctx.:>
559+
LLVMMem.LLVMPointerRepr w16 Ctx.:>
560+
LLVMMem.LLVMPointerRepr w32
561+
let struct_bv1 = BV.mkBV w16 27
562+
let struct_bv2 = BV.mkBV w32 42
563+
struct_sym_bv1 <- What4.bvLit sym w16 struct_bv1
564+
struct_sym_bv2 <- What4.bvLit sym w32 struct_bv2
565+
struct_field1 <- LLVMMem.llvmPointer_bv sym struct_sym_bv1
566+
struct_field2 <- LLVMMem.llvmPointer_bv sym struct_sym_bv2
567+
let struct_val = Ctx.Empty Ctx.:>
568+
CS.RV struct_field1 Ctx.:>
569+
CS.RV struct_field2
570+
571+
let testWithOpts memOpts = do
572+
let ?memOpts = memOpts
573+
-- First, allocate some memory on the stack...
574+
(ptr, mem1) <- LLVMMem.doAlloca bak mem0 sz noAlignment "<alloca>"
575+
-- ...write a struct to it...
576+
mem2 <- LLVMMem.doStore bak mem1 ptr
577+
struct_type_repr struct_storage_type
578+
noAlignment struct_val
579+
-- ...read back the struct...
580+
struct_val' <- LLVMMem.doLoad bak mem2 ptr
581+
struct_storage_type struct_type_repr noAlignment
582+
-- ...and finally, check that the struct read from memory is the
583+
-- same as the original struct.
584+
let checkField ::
585+
forall w sym bak.
586+
CB.IsSymBackend sym bak =>
587+
bak ->
588+
BV.BV w ->
589+
CS.RegValue' sym (LLVMMem.LLVMPointerType w) ->
590+
IO ()
591+
checkField bak' expectedBV actualPtrRV = do
592+
actualSymBV <- projectLLVM_bv bak' $ CS.unRV actualPtrRV
593+
Just expectedBV @=? What4.asBV actualSymBV
594+
checkField bak struct_bv1 (struct_val'^._1)
595+
checkField bak struct_bv2 (struct_val'^._2)
596+
597+
testWithOpts (?memOpts{ LLVMMem.laxLoadsAndStores = False })
598+
testWithOpts (?memOpts{ LLVMMem.laxLoadsAndStores = True
599+
, LLVMMem.indeterminateLoadBehavior = LLVMMem.StableSymbolic
600+
})
601+
testWithOpts (?memOpts{ LLVMMem.laxLoadsAndStores = True
602+
, LLVMMem.indeterminateLoadBehavior = LLVMMem.UnstableSymbolic
603+
})

0 commit comments

Comments
 (0)