Skip to content

Commit

Permalink
Draft: Invalidate memory properly with laxLoadsAndStores
Browse files Browse the repository at this point in the history
Prior to this change, invalidated memory would always result in an error when
read from. This isn't quite the semantics that we would want when
`laxLoadsAndStores` is enabled, however, since reading should always result in
a symbolic value of some sort. This patch changes the mechanics of
`doInvalidate` and `readMemInvalidate` such that when `laxLoadsAndStores` is
enabled, the memory is given the appropriate semantics depending on whether
`indeterminateLoadBehavior` is `StableSymbolic` or `UnstableSymbolic`.

This adds a `?memOpts :: MemOptions` constraint to `doInvalidate`, which is a
breaking API change. That being said, the only call site that I am aware of for
the `doInvalidate` function is SAW, so the breakage should be relatively minor.
Furthermore, there were no test cases for `doInvalidate` before this, so this
patch adds some.
  • Loading branch information
RyanGlScott committed Nov 24, 2021
1 parent 0bd1eb0 commit d7e54ab
Show file tree
Hide file tree
Showing 4 changed files with 106 additions and 16 deletions.
4 changes: 2 additions & 2 deletions crucible-llvm/CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,5 +12,5 @@
`initializeAllMemory`, `initializeMemoryConstGlobals`, `populateGlobals`,
`populateAllGlobals`, and `populateConstGlobals`
* `Lang.Crucible.LLVM.MemModel`:
`doAlloca`, `doCalloc`, `doMalloc`, `doMallocUnbounded`, `mallocRaw`,
`mallocConstRaw`, `allocGlobals`, and `allocGlobal`
`doAlloca`, `doCalloc`, `doInvalidate`, `doMalloc`, `doMallocUnbounded`,
`mallocRaw`, `mallocConstRaw`, `allocGlobals`, and `allocGlobal`
41 changes: 29 additions & 12 deletions crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
Original file line number Diff line number Diff line change
Expand Up @@ -566,10 +566,7 @@ doAlloca sym mem sz alignment loc = do
let mem' = mem{ memImplHeap = heap' }
mem'' <- if laxLoadsAndStores ?memOpts
&& indeterminateLoadBehavior ?memOpts == StableSymbolic
then do bytes <- freshConstant sym emptySymbol
(BaseArrayRepr (Ctx.singleton $ BaseBVRepr ?ptrWidth)
(BaseBVRepr (knownNat @8)))
doArrayStore sym mem' ptr alignment bytes sz
then doStoreStableSymbolic sym mem' ptr (Just sz) alignment
else pure mem'
pure (ptr, mem'')

Expand Down Expand Up @@ -710,12 +707,7 @@ doMallocSize sz sym allocType mut loc mem alignment = do
&& mut == G.Mutable
&& allocType == G.HeapAlloc
&& indeterminateLoadBehavior ?memOpts == StableSymbolic
then do bytes <- freshConstant sym emptySymbol
(BaseArrayRepr (Ctx.singleton $ BaseBVRepr ?ptrWidth)
(BaseBVRepr (knownNat @8)))
case sz of
Just sz' -> doArrayStore sym mem' ptr alignment bytes sz'
Nothing -> doArrayStoreUnbounded sym mem' ptr alignment bytes
then doStoreStableSymbolic sym mem' ptr sz alignment
else pure mem'
return (ptr, mem'')

Expand Down Expand Up @@ -854,7 +846,8 @@ doMemset sym w mem dest val len = do
return mem{ memImplHeap = heap' }

doInvalidate ::
(1 <= w, IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym) =>
( 1 <= w, IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym
, ?memOpts :: MemOptions ) =>
sym ->
NatRepr w ->
MemImpl sym ->
Expand All @@ -865,7 +858,12 @@ doInvalidate ::
doInvalidate sym w mem dest msg len = do
len' <- sextendBVTo sym w PtrWidth len

(heap', p) <- G.invalidateMem sym PtrWidth dest msg len' (memImplHeap mem)
(heap', p) <- if laxLoadsAndStores ?memOpts &&
indeterminateLoadBehavior ?memOpts == StableSymbolic
then do p <- G.isAllocatedMutable sym PtrWidth noAlignment dest (Just len') (memImplHeap mem)
mem' <- doStoreStableSymbolic sym mem dest (Just len') noAlignment
pure (memImplHeap mem', p)
else G.invalidateMem sym PtrWidth dest msg len' (memImplHeap mem)

let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) dest
let mop = MemInvalidateOp msg gsym dest len (memImplHeap mem)
Expand Down Expand Up @@ -1038,6 +1036,25 @@ doPtrAddOffset sym m x@(LLVMPointer blk _) off = do
in assertUndefined sym callStack v (UB.PtrAddOffsetOutOfBounds (RV x) (RV off))
return x'

-- | Store a fresh symbolic value of the appropriate size in the supplied
-- pointer. This is used in various spots whenever 'laxLoadsAndStores' is
-- enabled and 'indeterminateLoadBehavior' is set to 'StableSymbolic'.
doStoreStableSymbolic ::
(IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym) =>
sym ->
MemImpl sym ->
LLVMPtr sym wptr {- ^ destination -} ->
Maybe (SymBV sym wptr) {- ^ allocation size -} ->
Alignment {- ^ pointer alignment -} ->
IO (MemImpl sym)
doStoreStableSymbolic sym mem ptr mbSz alignment = do
bytes <- freshConstant sym emptySymbol
(BaseArrayRepr (Ctx.singleton (BaseBVRepr ?ptrWidth))
(BaseBVRepr (knownNat @8)))
case mbSz of
Just sz -> doArrayStore sym mem ptr alignment bytes sz
Nothing -> doArrayStoreUnbounded sym mem ptr alignment bytes

-- | This predicate tests if the pointer is a valid, live pointer
-- into the heap, OR is the distinguished NULL pointer.
isValidPointer ::
Expand Down
11 changes: 9 additions & 2 deletions crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ module Lang.Crucible.LLVM.MemModel.Generic
, allocAndWriteMem
, readMem
, isValidPointer
, isAllocatedMutable
, isAllocatedAlignedPointer
, notAliasable
, writeMem
Expand Down Expand Up @@ -634,7 +635,8 @@ readMemArrayStore sym w end mop (LLVMPointer blk read_off) tp write_off arr size

readMemInvalidate ::
forall sym w .
(1 <= w, IsSymInterface sym, HasLLVMAnn sym) =>
( 1 <= w, IsSymInterface sym, HasLLVMAnn sym
, ?memOpts :: MemOptions ) =>
sym -> NatRepr w ->
EndianForm ->
MemoryOp sym w ->
Expand All @@ -645,7 +647,12 @@ readMemInvalidate ::
SymBV sym w {- ^ The length of the set region -} ->
(StorageType -> LLVMPtr sym w -> ReadMem sym (PartLLVMVal sym)) ->
ReadMem sym (PartLLVMVal sym)
readMemInvalidate sym w end mop (LLVMPointer blk off) tp d msg sz readPrev =
readMemInvalidate sym w end mop (LLVMPointer blk off) tp d msg sz readPrev
| laxLoadsAndStores ?memOpts &&
indeterminateLoadBehavior ?memOpts == UnstableSymbolic =
liftIO (Partial.totalLLVMVal sym <$> freshLLVMVal sym tp)

| otherwise =
do let ld = BV.asUnsigned <$> asBV off
let dd = BV.asUnsigned <$> asBV d
let varFn = ExprEnv off d (Just sz)
Expand Down
66 changes: 66 additions & 0 deletions crucible-llvm/test/TestMemory.hs
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module TestMemory
Expand Down Expand Up @@ -36,6 +38,7 @@ import Lang.Crucible.LLVM.DataLayout ( noAlignment )
import qualified Lang.Crucible.LLVM.DataLayout as LLVMD
import Lang.Crucible.LLVM.MemModel ( doLoad, doStore, projectLLVM_bv, ptrAdd )
import qualified Lang.Crucible.LLVM.MemModel as LLVMMem
import qualified Lang.Crucible.LLVM.MemModel.Generic as LLVMMemG


memoryTests :: T.TestTree
Expand All @@ -49,6 +52,7 @@ memoryTests = T.testGroup "Memory"
, testPointerStore
, testMemArrayCopy
, testMemArraySet
, testMemInvalidate
]


Expand Down Expand Up @@ -429,6 +433,68 @@ testMemAllocs =
res <- checkSat sym =<< What4.notPred sym assertion
True @=? W4Sat.isUnsat res

-- | This test case checks that 'doInvalidate' behaves as expected with and
-- without 'laxLoadsAndStores' enabled.
testMemInvalidate :: T.TestTree
testMemInvalidate =
testCase "memory invalidation" $ withMem LLVMD.BigEndian $ \(sym :: sym) mem0 ->
do sz <- What4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth 64
let long_type_repr = Crucible.baseToType $ What4.BaseBVRepr $ knownNat @64
long_storage_type = LLVMMem.bitvectorType 8
zero_val <- What4.bvLit sym (knownNat @64) (BV.zero knownNat)

let withInvalidatedReadVal :: LLVMMem.MemOptions
-> (LLVMMem.PartLLVMVal sym -> IO a)
-> IO a
withInvalidatedReadVal memOpts k = do
let ?memOpts = memOpts
-- First, allocate some memory on the stack...
(ptr, mem1) <- LLVMMem.doAlloca sym mem0 sz noAlignment "<alloca>"
-- ...write some value to it (the exact value is unimportant)...
mem2 <- LLVMMem.doStore sym mem1 ptr
long_type_repr long_storage_type
noAlignment zero_val
-- ...invalidate the memory...
mem3 <- LLVMMem.doInvalidate sym ?ptrWidth mem2 ptr "<invalidate>" sz
-- ...and finally, read from the invalidated memory.
partVal <- LLVMMemG.readMem sym ?ptrWidth Nothing ptr
long_storage_type noAlignment
(LLVMMem.memImplHeap mem3)
k partVal

testLaxInvalidatedRead :: String -> LLVMMem.IndeterminateLoadBehavior -> IO ()
testLaxInvalidatedRead stability indeterminateLoadBehavior =
withInvalidatedReadVal (?memOpts{ LLVMMem.laxLoadsAndStores = True
, LLVMMem.indeterminateLoadBehavior = indeterminateLoadBehavior
}) $ \partVal ->
case partVal of
LLVMMem.NoErr p _val -> do
res <- checkSat sym p
True @=? W4Sat.isSat res
LLVMMem.Err p -> assertFailure $ unlines
[ "Reading from invalidated, " ++ stability ++ "-symbolic memory unexpectedly failed"
, "Predicate: " ++ show p
]

-- Test with laxLoadsAndStores disabled, where reading from invalidated
-- memory should result in an error.
withInvalidatedReadVal (?memOpts{LLVMMem.laxLoadsAndStores = False}) $ \partVal ->
case partVal of
LLVMMem.Err p -> do
res <- checkSat sym p
True @=? W4Sat.isUnsat res
LLVMMem.NoErr p val -> assertFailure $ unlines
[ "Reading from invalidated memory unexpectedly succeeded"
, "Predicate: " ++ show p
, "LLVM value read: " ++ show val
]

-- Test with laxLoadsAndStores enabled, using both the
-- StableSymbolic and UnstableSymbolic settings for
-- indeterminateLoadBehavior. Here, reading from invalidated memory should succeed.
testLaxInvalidatedRead "stable" LLVMMem.StableSymbolic
testLaxInvalidatedRead "unstable" LLVMMem.UnstableSymbolic

-- | Test storing and retrieving pointer in an SMT-backed array memory model
testPointerStore :: T.TestTree
testPointerStore = testCase "pointer store" $ withMem LLVMD.BigEndian $ \sym mem0 -> do
Expand Down

0 comments on commit d7e54ab

Please sign in to comment.