From 54904aca1205cd373985120edb17d9512249a70c Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 14 Jan 2025 12:36:12 -0500 Subject: [PATCH] stubs-common: Use the lazy macaw-symbolic memory model Much of the memory model code that `stubs-common` sits on top of has since been upstreamed to `macaw-symbolic` as part of its lazy memory model. This patch rips out the copy that `stubs-common` uses and replaces it with equivalent functionality found in `Data.Macaw.Symbolic.Memory.Lazy`. Fixes #12. --- stubs-common/src/Stubs/Extensions.hs | 416 ++---------- stubs-common/src/Stubs/Extensions/Memory.hs | 602 ------------------ stubs-common/src/Stubs/Memory.hs | 3 +- .../src/Stubs/Memory/AArch32/Linux.hs | 10 +- stubs-common/src/Stubs/Memory/PPC/Linux.hs | 10 +- stubs-common/src/Stubs/Memory/X86_64/Linux.hs | 36 +- stubs-common/stubs-common.cabal | 1 - 7 files changed, 65 insertions(+), 1013 deletions(-) delete mode 100644 stubs-common/src/Stubs/Extensions/Memory.hs diff --git a/stubs-common/src/Stubs/Extensions.hs b/stubs-common/src/Stubs/Extensions.hs index a9f3ab2..79e8f63 100644 --- a/stubs-common/src/Stubs/Extensions.hs +++ b/stubs-common/src/Stubs/Extensions.hs @@ -1,13 +1,16 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} -- | Defines verifier-specific extensions for Macaw's simulation functionality. @@ -29,39 +32,29 @@ module Stubs.Extensions , functionAddrOvHandles , syscallOvHandles , discoveredFunctionHandles - , populatedMemChunks , simulationStats , overrideLookupFunctionHandle , sharedMemoryState + , macawLazySimulatorState ) where import qualified Control.Exception as X -import Control.Lens ( Lens', (^.), lens, over, (&), (+~)) -import Control.Monad ( when ) +import Control.Lens ( Lens', (^.), lens, (&), (+~)) import Control.Monad.IO.Class ( MonadIO(liftIO) ) import qualified Control.Monad.State as CMS import qualified Data.Aeson as DA import qualified Data.BitVector.Sized as BV -import qualified Data.Foldable as F -import qualified Data.Foldable.WithIndex as FWI -import qualified Data.IntervalMap.Interval as IMI -import qualified Data.IntervalMap.Strict as IM -import qualified Data.IntervalSet as IS -import qualified Data.List as L import qualified Data.Map.Strict as Map import Data.Maybe ( isNothing ) -import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.Map as MapF -import qualified Data.Sequence as Seq -import qualified Data.Vector as DV import Data.Word ( Word8 ) import GHC.Generics ( Generic ) import qualified GHC.Stack as GHC -import Text.Printf ( printf ) import qualified Data.Macaw.CFG as DMC import qualified Data.Macaw.Memory as DMM import qualified Data.Macaw.Symbolic as DMS +import qualified Data.Macaw.Symbolic.Memory.Lazy as DMSM import qualified Data.Macaw.Symbolic.Backend as DMSB import qualified Data.Macaw.Symbolic.MemOps as DMSMO import Data.Macaw.Symbolic.MemOps () @@ -71,16 +64,12 @@ import qualified Lang.Crucible.LLVM.MemModel as LCLM import qualified Lang.Crucible.LLVM.MemModel.Pointer as LCLMP import qualified Lang.Crucible.Simulator as LCS import qualified Lang.Crucible.Simulator.ExecutionTree as LCSE -import qualified Lang.Crucible.Types as LCT -import qualified What4.Expr.BoolMap as WEBM -import qualified What4.Expr.Builder as WEB import qualified What4.Expr as WE import qualified What4.FunctionName as WF import qualified What4.Interface as WI import qualified What4.Protocol.Online as WPO import qualified Stubs.Exception as AE -import qualified Stubs.Extensions.Memory as AEM import qualified Stubs.Memory.SharedMemory as AMS import qualified Stubs.Verifier.Concretize as AVC import qualified Stubs.Syscall as ASy @@ -99,7 +88,7 @@ ambientExtensions :: , DMM.MemWidth w , SM.MemType DMS.LLVMMemory arch ~ LCLM.Mem, SM.IsStubsMemoryModel DMS.LLVMMemory arch , SM.MemMap sym arch ~ DMSMO.GlobalMap sym LCLM.Mem w, SM.PtrType DMS.LLVMMemory arch ~ LCLMP.LLVMPointerType w - , SM.MemTable sym DMS.LLVMMemory arch ~ AEM.MemPtrTable sym arch + , SM.MemTable sym DMS.LLVMMemory arch ~ DMSM.MemPtrTable sym (DMC.ArchAddrWidth arch) ,?memOpts::LCLM.MemOptions ,?recordLLVMAnnotation::Lang.Crucible.LLVM.MemModel.CallStack.CallStack -> LCLMP.BoolAnn sym @@ -180,8 +169,8 @@ resolveAndPopulate -> LCS.RegEntry sym (LCLM.LLVMPointerType w) -> LCS.SimState p sym ext rtp f args -> IO (LCLM.LLVMPtr sym w, LCS.SimState p sym ext rtp f args) -resolveAndPopulate bak memImpl initialMem readSizeBV ptr st = do - (ptr', resolveEffect) <- +resolveAndPopulate bak memImpl initialMem _readSizeBV ptr st = do + (ptr', _resolveEffect) <- resolvePointer bak memImpl (SM.imGlobalMap initialMem) ptr -- st' <- lazilyPopulateGlobalMemArr bak -- (AM.imMemPtrTable initialMem) -- will maybe be an issue @@ -203,12 +192,14 @@ readMem :: forall sym scope st fs bak solver arch p w ext rtp f args ty. , ?memOpts :: LCLM.MemOptions , SM.IsStubsMemoryModel DMS.LLVMMemory arch , SM.MemMap sym arch ~ DMSMO.GlobalMap sym LCLM.Mem w, - SM.MemTable sym DMS.LLVMMemory arch ~ AEM.MemPtrTable sym arch + SM.MemTable sym DMS.LLVMMemory arch ~ DMSM.MemPtrTable sym (DMC.ArchAddrWidth arch) ) => bak -> LCLM.MemImpl sym -> SM.InitialMemory sym DMS.LLVMMemory arch -- ^ Initial memory state for symbolic execution + -> DMS.MemModelConfig (AmbientSimulatorState sym arch) sym arch LCLM.Mem + -- ^ Configuration options for the memory model -> Map.Map (DMM.MemWord w) String -- ^ Mapping from unsupported relocation addresses to the names of the -- unsupported relocation types. @@ -220,22 +211,18 @@ readMem :: forall sym scope st fs bak solver arch p w ext rtp f args ty. -- ^ Pointer to read from -> IO ( LCS.RegValue sym (DMS.ToCrucibleType ty) , LCS.SimState p sym ext rtp f args ) -readMem bak memImpl initialMem unsupportedRelocs st addrWidth memRep ptr0 = +readMem bak memImpl initialMem mmConf unsupportedRelocs st addrWidth memRep ptr0 = DMM.addrWidthClass addrWidth $ do let sym = LCB.backendGetSym bak - let mpt = SM.imMemTable initialMem (ptr1, resolveEffect) <- resolvePointer bak memImpl (SM.imGlobalMap initialMem) ptr0 assertRelocSupported ptr1 unsupportedRelocs - case concreteImmutableGlobalRead memRep ptr1 mpt of - Just bytes -> do - readVal <- AEM.readBytesAsRegValue sym memRep bytes + mbReadVal <- DMS.concreteImmutableGlobalRead mmConf memRep ptr1 + case mbReadVal of + Just readVal -> do let st' = incrementSimStat lensNumReads st pure (readVal, st') Nothing -> do - let w = DMM.memWidthNatRepr @w - memReprBytesBV <- WI.bvLit sym w $ BV.mkBV w $ - toInteger $ DMC.memReprBytes memRep let puse = DMS.PointerUse (st ^. LCSE.stateLocation) DMS.PointerRead mGlobalPtrValid <- (\_ _ _ _->return Nothing) sym puse Nothing ptr0 case mGlobalPtrValid of @@ -279,7 +266,6 @@ writeMem bak memImpl initialMem st addrWidth memRep ptr0 v = memReprBytesBV <- WI.bvLit sym w $ BV.mkBV w $ toInteger $ DMC.memReprBytes memRep (ptr1, st1) <- resolveAndPopulate bak memImpl initialMem memReprBytesBV ptr0 st - let puse = DMS.PointerUse (st1 ^. LCSE.stateLocation) DMS.PointerWrite mGlobalPtrValid <- return Nothing case mGlobalPtrValid of Just globalPtrValid -> LCB.addAssertion bak globalPtrValid @@ -316,7 +302,7 @@ loadString , sym ~ WE.ExprBuilder scope st fs , bak ~ LCBO.OnlineBackend solver scope st fs , WPO.OnlineSolver solver, SM.IsStubsMemoryModel DMS.LLVMMemory arch - , SM.MemTable sym DMS.LLVMMemory arch ~ AEM.MemPtrTable sym arch + , SM.MemTable sym DMS.LLVMMemory arch ~ DMSM.MemPtrTable sym (DMC.ArchAddrWidth arch) , SM.MemMap sym arch ~ DMSMO.GlobalMap sym LCLM.Mem w ) => bak @@ -324,6 +310,8 @@ loadString -- ^ memory to read from -> SM.InitialMemory sym DMS.LLVMMemory arch -- ^ Initial memory state for symbolic execution + -> DMS.MemModelConfig (AmbientSimulatorState sym arch) sym arch LCLM.Mem + -- ^ Configuration options for the memory model -> Map.Map (DMC.MemWord w) String -- ^ Mapping from unsupported relocation addresses to the names of the -- unsupported relocation types. @@ -332,7 +320,7 @@ loadString -> Maybe Int -- ^ maximum characters to read -> m [WI.SymBV sym 8] -loadString bak memImpl initialMem unsupportedRelocs = go id +loadString bak memImpl initialMem mmConf unsupportedRelocs = go id where sym = LCB.backendGetSym bak @@ -344,7 +332,7 @@ loadString bak memImpl initialMem unsupportedRelocs = go id go f p maxChars = do let readInfo = DMC.BVMemRepr (WI.knownNat @1) DMC.LittleEndian st <- CMS.get - (v, st') <- liftIO $ readMem bak memImpl initialMem unsupportedRelocs st (DMC.addrWidthRepr ?ptrWidth) readInfo p + (v, st') <- liftIO $ readMem bak memImpl initialMem mmConf unsupportedRelocs st (DMC.addrWidthRepr ?ptrWidth) readInfo p CMS.put st' x <- liftIO $ LCLM.projectLLVM_bv bak v if (BV.asUnsigned <$> WI.asBV x) == Just 0 @@ -370,7 +358,7 @@ loadConcreteString , sym ~ WE.ExprBuilder scope st fs , bak ~ LCBO.OnlineBackend solver scope st fs , WPO.OnlineSolver solver, SM.IsStubsMemoryModel DMS.LLVMMemory arch - , SM.MemTable sym DMS.LLVMMemory arch ~ AEM.MemPtrTable sym arch + , SM.MemTable sym DMS.LLVMMemory arch ~ DMSM.MemPtrTable sym (DMC.ArchAddrWidth arch) , SM.MemMap sym arch ~ DMSMO.GlobalMap sym LCLM.Mem w ) => bak @@ -378,6 +366,8 @@ loadConcreteString -- ^ memory to read from -> SM.InitialMemory sym DMS.LLVMMemory arch -- ^ Initial memory state for symbolic execution + -> DMS.MemModelConfig (AmbientSimulatorState sym arch) sym arch LCLM.Mem + -- ^ Configuration options for the memory model -> Map.Map (DMC.MemWord w) String -- ^ Mapping from unsupported relocation addresses to the names of the -- unsupported relocation types. @@ -386,8 +376,8 @@ loadConcreteString -> Maybe Int -- ^ maximum characters to read -> m [Word8] -loadConcreteString bak memImpl initialMem unsupportedRelocs p maxChars = do - symBytes <- loadString bak memImpl initialMem unsupportedRelocs p maxChars +loadConcreteString bak memImpl initialMem mmConf unsupportedRelocs p maxChars = do + symBytes <- loadString bak memImpl initialMem mmConf unsupportedRelocs p maxChars traverse concretizeByte symBytes where concretizeByte :: WI.SymBV sym 8 -> m Word8 @@ -568,7 +558,7 @@ execAmbientStmtExtension :: forall sym scope st fs bak solver arch p w. , SM.MemType DMS.LLVMMemory arch ~ LCLM.Mem ,SM.IsStubsMemoryModel DMS.LLVMMemory arch, SM.PtrType DMS.LLVMMemory arch ~ LCLM.LLVMPointerType (DMC.ArchAddrWidth arch) - , SM.MemTable sym DMS.LLVMMemory arch ~ AEM.MemPtrTable sym arch + , SM.MemTable sym DMS.LLVMMemory arch ~ DMSM.MemPtrTable sym (DMC.ArchAddrWidth arch) , SM.MemMap sym arch ~ DMSMO.GlobalMap sym LCLM.Mem w ) => bak @@ -590,22 +580,19 @@ execAmbientStmtExtension bak f initialMem mmConf unsupportedRelocs s0 st = case s0 of DMS.MacawReadMem addrWidth memRep ptr0 -> do memImpl <- DMSMO.getMem st mvar - readMem bak memImpl initialMem unsupportedRelocs st addrWidth memRep ptr0 + readMem bak memImpl initialMem mmConf unsupportedRelocs st addrWidth memRep ptr0 DMS.MacawCondReadMem addrWidth memRep cond ptr0 condFalseValue -> DMM.addrWidthClass addrWidth $ do memImpl <- DMSMO.getMem st mvar (ptr1, resolveEffect) <- resolvePointer bak memImpl globs ptr0 assertRelocSupported ptr1 unsupportedRelocs - case concreteImmutableGlobalRead memRep ptr1 mpt of - Just bytes -> do - readVal <- AEM.readBytesAsRegValue sym memRep bytes - readVal' <- muxMemReprValue sym memRep (LCS.regValue cond) readVal (LCS.regValue condFalseValue) + mbReadVal <- DMS.concreteImmutableGlobalRead mmConf memRep ptr1 + case mbReadVal of + Just readVal -> do + readVal' <- DMSMO.muxMemReprValue sym memRep (LCS.regValue cond) readVal (LCS.regValue condFalseValue) let st' = incrementSimStat lensNumReads st pure (readVal', st') Nothing -> do - let w = DMM.memWidthNatRepr - memReprBytesBV <- WI.bvLit sym w $ BV.mkBV w $ - toInteger $ DMC.memReprBytes memRep - st1 <- lazilyPopulateGlobalMemArr bak mpt memReprBytesBV ptr1 st + st1 <- DMS.lazilyPopulateGlobalMem mmConf memRep ptr1 st let puse = DMS.PointerUse (st1 ^. LCSE.stateLocation) DMS.PointerRead mGlobalPtrValid <- toMemPred sym puse (Just cond) ptr0 case mGlobalPtrValid of @@ -649,7 +636,6 @@ execAmbientStmtExtension bak f initialMem mmConf unsupportedRelocs s0 st = where sym = LCB.backendGetSym bak mvar = SM.imMemVar initialMem - mpt = SM.imMemTable initialMem globs = SM.imGlobalMap initialMem toMemPred :: DMS.MkGlobalPointerValidityAssertion sym w @@ -720,54 +706,6 @@ updateBoundsRefined resolveEffect state = AVC.UnchangedBounds -> state AVC.RefinedBounds -> incrementSimStat lensNumBoundsRefined state --- Return @Just bytes@ if we can be absolutely sure that this is a concrete --- read from a contiguous region of immutable, global memory, where @bytes@ --- are the bytes backing the global memory. Return @Nothing@ otherwise. --- See @Note [Lazy memory initialization]@ in Ambient.Extensions.Memory. -concreteImmutableGlobalRead :: - (LCB.IsSymInterface sym, DMM.MemWidth w, DMM.MemWidth (DMC.RegAddrWidth (DMC.ArchReg arch))) => - DMC.MemRepr ty -> - LCLM.LLVMPtr sym w -> - AEM.MemPtrTable sym arch -> - Maybe [WI.SymBV sym 8] -concreteImmutableGlobalRead memRep ptr mpt - | -- First, check that the pointer being read from is concrete. - Just ptrBlkNat <- WI.asNat ptrBlk - , Just addrBV <- WI.asBV ptrOff - - -- Next, check that the pointer block is the same as the block of the - -- pointer backing global memory. - , Just memPtrBlkNat <- WI.asNat memPtrBlk - , ptrBlkNat == memPtrBlkNat - - -- Next, check that we are attempting to read from a contiguous region - -- of memory. - , let addr = fromInteger $ BV.asUnsigned addrBV - , Just (addrBaseInterval, smc) <- - combineChunksIfContiguous $ IM.toAscList $ - AEM.memPtrTable mpt `IM.intersecting` - IMI.ClosedInterval addr (addr + fromIntegral numBytes) - - -- Next, check that the memory is immutable. - , AEM.smcMutability smc == LCLM.Immutable - - -- Finally, check that the region of memory is large enough to cover - -- the number of bytes we are attempting to read. - , let addrOffset = fromIntegral $ addr - IMI.lowerBound addrBaseInterval - , numBytes <= (length (AEM.smcBytes smc) - addrOffset) - = let bytes = Seq.take numBytes $ - Seq.drop addrOffset $ - AEM.smcBytes smc in - Just $ F.toList bytes - - | otherwise - = Nothing - where - numBytes = fromIntegral $ DMC.memReprBytes memRep - (ptrBlk, ptrOff) = LCLM.llvmPointerView ptr - memPtrBlk = LCLMP.llvmPointerBlock (AEM.memPtr mpt) - - -- | Check whether a pointer points to a relocation address, and if so, -- assert that the underlying relocation type is supported. If not, throw -- an UnsupportedRelocation exception. This is a best effort attempt: if @@ -792,268 +730,6 @@ assertRelocSupported (LCLM.LLVMPointer _base offset) unsupportedRelocs = X.throwIO $ AE.UnsupportedRelocation relTypeName Nothing -> return () --- | Given a Boolean condition and two symbolic values associated with --- a Macaw type, return a value denoting the first value if condition --- is true and second value otherwise. --- --- arg1 : Symbolic interface --- arg2 : Description of memory layout of value --- arg3 : Condition --- arg4 : Value if condition is true --- arg5 : Value if condition is false. - --- NB: This taken from a non-exported function in macaw-symbolic: --- https://github.com/GaloisInc/macaw/blob/a43151963da70e4d4c3d69f9605e82e44ff30731/symbolic/src/Data/Macaw/Symbolic/MemOps.hs#L961-L988 --- Should we upstream the lazy memory initialization work to macaw-symbolic --- (see Note [Lazy memory initialization] in Ambient.Extensions.Memory), we --- will no longer have a need to redefine this function here. -muxMemReprValue :: - LCB.IsSymInterface sym => - sym -> - DMC.MemRepr ty -> - LCS.RegValue sym LCT.BoolType -> - LCS.RegValue sym (DMS.ToCrucibleType ty) -> - LCS.RegValue sym (DMS.ToCrucibleType ty) -> - IO (LCS.RegValue sym (DMS.ToCrucibleType ty)) -muxMemReprValue sym memRep cond x y = - case memRep of - DMC.BVMemRepr bytes _endian -> - case WI.leqMulPos (WI.knownNat @8) bytes of - WI.LeqProof -> LCLMP.muxLLVMPtr sym cond x y - DMC.FloatMemRepr _floatRep _endian -> - WI.baseTypeIte sym cond x y - DMC.PackedVecMemRepr _ eltMemRepr -> do - when (DV.length x /= DV.length y) $ do - X.throwIO $ userError $ "Expected vectors to have same length" - DV.zipWithM (muxMemReprValue sym eltMemRepr cond) x y - --- | If this is a global read, initialize the region of memory in the SMT array --- that backs global memory. See @Note [Lazy memory initialization]@ in --- "Ambient.Extensions.Memory". -lazilyPopulateGlobalMemArr :: - forall sym bak arch w t st fs p ext rtp f args. - ( LCB.IsSymBackend sym bak - , sym ~ WEB.ExprBuilder t st fs - , w ~ DMC.ArchAddrWidth arch - , p ~ AmbientSimulatorState sym arch - , DMM.MemWidth w - ) => - bak -> - AEM.MemPtrTable sym arch -> - -- ^ The global memory - WI.SymBV sym w -> - -- ^ The amount of memory to read - LCLM.LLVMPtr sym w -> - -- ^ The pointer being read from - LCS.SimState p sym ext rtp f args -> - -- ^ State to update if this is a global read - IO (LCS.SimState p sym ext rtp f args) -lazilyPopulateGlobalMemArr bak mpt readSizeBV ptr state - | -- We only wish to populate the array backing global memory if we know for - -- sure that we are reading from the global pointer. If we're reading from a - -- different pointer, there's no need to bother populating the array. - WI.asNat (LCLMP.llvmPointerBlock (AEM.memPtr mpt)) == - WI.asNat (LCLMP.llvmPointerBlock ptr) - = do pleatM state tbl $ \st (addr, smc) -> - if addr `IS.notMember` (st^.chunksL) - then do assumeMemArr bak (AEM.memPtrArray mpt) - (IMI.lowerBound addr) (AEM.smcBytes smc) - pure $ over chunksL (IS.insert addr) st - else pure st - - | otherwise - = pure state - where - sym = LCB.backendGetSym bak - - -- The regions of global memory that would need to be accessed as a result - -- of reading from the pointer. We build an interval [ptr, ptr+read_size] - -- and load all of the chunks in global memory that overlap with the - -- interval. - tbl = IM.toAscList $ AEM.memPtrTable mpt `IM.intersecting` - (ptrInterval `extendUpperBound` maxReadSize) - - -- ptrInterval is an interval representing the possible values that ptr - -- could be, and maxReadSize is the largest possible value that readSizeBV - -- could be. From these we can build an interval (ptrInterval - -- `extendUpperBound` maxReadSize) that contains all possible global memory - -- addresses that the read could encompass. - ptrInterval = symBVInterval sym (LCLMP.llvmPointerOffset ptr) - maxReadSize = IMI.upperBound (symBVInterval sym readSizeBV) - - chunksL :: Lens' (LCS.SimState p sym ext rtp f args) - (IS.IntervalSet (IMI.Interval (DMM.MemWord w))) - chunksL = LCS.stateContext . LCS.cruciblePersonality . populatedMemChunks - --- | Given a list of memory regions and the symbolic bytes backing them, --- attempt to combine them into a single region. Return 'Just' if the memory --- can be combined into a single, contiguous region with no overlap and the --- backing memory has the same 'LCLM.Mutability. Return 'Nothing' otherwise. -combineChunksIfContiguous :: - forall a sym. - (Eq a, Integral a) => - [(IMI.Interval a, AEM.SymbolicMemChunk sym)] -> - Maybe (IMI.Interval a, AEM.SymbolicMemChunk sym) -combineChunksIfContiguous ichunks = - case L.uncons ichunks of - Nothing -> Nothing - Just (ichunkHead, ichunkTail) -> F.foldl' f (Just ichunkHead) ichunkTail - where - f :: - Maybe (IMI.Interval a, AEM.SymbolicMemChunk sym) -> - (IMI.Interval a, AEM.SymbolicMemChunk sym) -> - Maybe (IMI.Interval a, AEM.SymbolicMemChunk sym) - f acc (i2, chunk2) = do - (i1, chunk1) <- acc - combinedI <- combineIfContiguous i1 i2 - combinedChunk <- AEM.combineSymbolicMemChunks chunk1 chunk2 - pure (combinedI, combinedChunk) - --- | @'combineIfContiguous' i1 i2@ returns 'Just' an interval with the lower --- bound of @i1@ and the upper bound of @i2@ when one of the following criteria --- are met: --- --- * If @i1@ has an open upper bound, then @i2@ has a closed lower bound of the --- same integral value. --- --- * If @i1@ has a closed upper bound and @i2@ has an open lower bound, then --- these bounds have the same integral value. --- --- * If @i1@ has a closed upper bound and @i2@ has a closed lower bound, then --- @i2@'s lower bound is equal to the integral value of @i1@'s upper bound --- plus one. --- --- * It is not the case that both @i1@'s upper bound and @i2@'s lower bound are --- open. --- --- Otherwise, this returns 'Nothing'. --- --- Less formally, this captures the notion of combining two non-overlapping --- 'IMI.Interval's that when would form a single, contiguous range when --- overlaid. (Contrast this with 'IMI.combine', which only returns 'Just' if --- the two 'IMI.Interval's are overlapping.) -combineIfContiguous :: (Eq a, Integral a) => IMI.Interval a -> IMI.Interval a -> Maybe (IMI.Interval a) -combineIfContiguous i1 i2 = - case (i1, i2) of - (IMI.IntervalOC lo1 hi1, IMI.IntervalOC lo2 hi2) - | hi1 == lo2 -> Just $ IMI.IntervalOC lo1 hi2 - | otherwise -> Nothing - (IMI.IntervalOC lo1 hi1, IMI.OpenInterval lo2 hi2) - | hi1 == lo2 -> Just $ IMI.OpenInterval lo1 hi2 - | otherwise -> Nothing - (IMI.OpenInterval lo1 hi1, IMI.IntervalCO lo2 hi2) - | hi1 == lo2 -> Just $ IMI.OpenInterval lo1 hi2 - | otherwise -> Nothing - (IMI.OpenInterval lo1 hi1, IMI.ClosedInterval lo2 hi2) - | hi1 == lo2 -> Just $ IMI.IntervalOC lo1 hi2 - | otherwise -> Nothing - (IMI.IntervalCO lo1 hi1, IMI.IntervalCO lo2 hi2) - | hi1 == lo2 -> Just $ IMI.IntervalCO lo1 hi2 - | otherwise -> Nothing - (IMI.IntervalCO lo1 hi1, IMI.ClosedInterval lo2 hi2) - | hi1 == lo2 -> Just $ IMI.ClosedInterval lo1 hi2 - | otherwise -> Nothing - (IMI.ClosedInterval lo1 hi1, IMI.IntervalOC lo2 hi2) - | hi1 == lo2 -> Just $ IMI.ClosedInterval lo1 hi2 - | otherwise -> Nothing - (IMI.ClosedInterval lo1 hi1, IMI.OpenInterval lo2 hi2) - | hi1 == lo2 -> Just $ IMI.IntervalCO lo1 hi2 - | otherwise -> Nothing - - (IMI.IntervalOC lo1 hi1, IMI.IntervalCO lo2 hi2) - | hi1 + 1 == lo2 -> Just $ IMI.OpenInterval lo1 hi2 - | otherwise -> Nothing - (IMI.IntervalOC lo1 hi1, IMI.ClosedInterval lo2 hi2) - | hi1 + 1 == lo2 -> Just $ IMI.IntervalOC lo1 hi2 - | otherwise -> Nothing - (IMI.ClosedInterval lo1 hi1, IMI.IntervalCO lo2 hi2) - | hi1 + 1 == lo2 -> Just $ IMI.IntervalCO lo1 hi2 - | otherwise -> Nothing - (IMI.ClosedInterval lo1 hi1, IMI.ClosedInterval lo2 hi2) - | hi1 + 1 == lo2 -> Just $ IMI.ClosedInterval lo1 hi2 - | otherwise -> Nothing - - (IMI.IntervalCO{}, IMI.IntervalOC{}) - -> Nothing - (IMI.IntervalCO{}, IMI.OpenInterval{}) - -> Nothing - (IMI.OpenInterval{}, IMI.IntervalOC{}) - -> Nothing - (IMI.OpenInterval{}, IMI.OpenInterval{}) - -> Nothing - --- | Extend the upper bound of an 'IMI.Interval' by the given amount. -extendUpperBound :: Num a => IMI.Interval a -> a -> IMI.Interval a -extendUpperBound i extendBy = - case i of - IMI.IntervalCO lo hi -> IMI.IntervalCO lo (hi + extendBy) - IMI.IntervalOC lo hi -> IMI.IntervalOC lo (hi + extendBy) - IMI.OpenInterval lo hi -> IMI.OpenInterval lo (hi + extendBy) - IMI.ClosedInterval lo hi -> IMI.ClosedInterval lo (hi + extendBy) - --- -- | Initialize the memory backing global memory by assuming that the elements --- -- of the array are equal to the appropriate bytes. --- -- See @Note [Lazy memory initialization]@ in "Ambient.Extensions.Memory". - --- NB: This is the same code as in this part of macaw-symbolic: --- https://github.com/GaloisInc/macaw/blob/ef0ece6a726217fe6231b9ddf523868e491e6ef0/symbolic/src/Data/Macaw/Symbolic/Memory.hs#L474-L496 -assumeMemArr :: - forall sym bak w t st fs. - ( LCB.IsSymBackend sym bak - , sym ~ WEB.ExprBuilder t st fs - , DMM.MemWidth w - ) => - bak -> - WI.SymArray sym (Ctx.SingleCtx (WI.BaseBVType w)) (WI.BaseBVType 8) -> - DMM.MemWord w -> - Seq.Seq (WI.SymBV sym 8) -> - IO () -assumeMemArr bak symArray absAddr bytes = do - initVals <- ipleatM [] bytes $ \idx bmvals byte -> do - let absByteAddr = fromIntegral idx + absAddr - index_bv <- liftIO $ WI.bvLit sym w (BV.mkBV w (toInteger absByteAddr)) - eq_pred <- liftIO $ WI.bvEq sym byte =<< WI.arrayLookup sym symArray (Ctx.singleton index_bv) - return (eq_pred : bmvals) - let desc = printf "Bytes@[addr=%s,nbytes=%s]" (show absAddr) (show bytes) - prog_loc <- liftIO $ WI.getCurrentProgramLoc sym - byteEqualityAssertion <- liftIO $ WEB.sbMakeExpr sym (WE.ConjPred (WEBM.fromVars [(e, WEBM.Positive) | e <- initVals])) - liftIO $ LCB.addAssumption bak (LCB.GenericAssumption prog_loc desc byteEqualityAssertion) - where - sym = LCB.backendGetSym bak - w = DMM.memWidthNatRepr @w - --- | Return an 'IMI.Interval' representing the possible range of addresses that --- a 'WI.SymBV' can lie between. If this is a concrete bitvector, the interval --- will consist of a single point, but if this is a symbolic bitvector, then --- the range can span multiple addresses. -symBVInterval :: - (WI.IsExprBuilder sym, DMM.MemWidth w) => - sym -> - WI.SymBV sym w -> - IMI.Interval (DMM.MemWord w) -symBVInterval _ bv = - case WI.unsignedBVBounds bv of - Just (lo, hi) -> IMI.ClosedInterval (fromInteger lo) (fromInteger hi) - Nothing -> IMI.ClosedInterval minBound maxBound - --- | The 'pleatM' function is 'F.foldM' with the arguments switched so --- that the function is last. -pleatM :: (Monad m, F.Foldable t) - => b - -> t a - -> (b -> a -> m b) - -> m b -pleatM s l f = F.foldlM f s l - --- | The 'ipleatM' function is 'FWI.ifoldM' with the arguments switched so --- that the function is last. -ipleatM :: (Monad m, FWI.FoldableWithIndex i t) - => b - -> t a - -> (i -> b -> a -> m b) - -> m b -ipleatM s l f = FWI.ifoldlM f s l - -- | Statistics gathered during simulation data AmbientSimulationStats = AmbientSimulationStats { numOvsApplied :: Integer @@ -1128,13 +804,6 @@ data AmbientSimulatorState sym arch = AmbientSimulatorState -- those sorts of layouts, we would run the risk of addresses from -- different address spaces being mapped to the same 'DMC.ArchSegmentOff', -- which will make a 'Map.Map' insufficient means of storage. See #86. - , _populatedMemChunks :: IS.IntervalSet (IMI.Interval (DMM.MemWord (DMC.ArchAddrWidth arch))) - -- ^ The regions of memory which we have populated with symbolic bytes in - -- the 'AEM.MemPtrTable' backing global memory. - -- See @Note [Lazy memory initialization@ in "Ambient.Extensions.Memory". - -- ^ A map from registered socket file descriptors to their corresponding - -- metadata. See @Note [The networking story]@ in - -- "Ambient.Syscall.Overrides.Networking". , _simulationStats :: AmbientSimulationStats -- ^ Metrics from the Ambient simulator , _overrideLookupFunctionHandle :: Maybe (DMSMO.LookupFunctionHandle (AmbientSimulatorState sym arch) sym arch) @@ -1147,6 +816,9 @@ data AmbientSimulatorState sym arch = AmbientSimulatorState -- unbalance the stack (which prevents Macaw from detecting them properly). , _sharedMemoryState :: AMS.AmbientSharedMemoryState sym (DMC.ArchAddrWidth arch) -- ^ Manages shared memory allocated during simulation. + , _macawLazySimulatorState :: DMS.MacawLazySimulatorState sym (DMC.ArchAddrWidth arch) + -- ^ The state used in the lazy @macaw-symbolic@ memory model, on top of + -- which @grease@ is built. } -- | An initial value for 'AmbientSimulatorState'. @@ -1156,12 +828,17 @@ emptyAmbientSimulatorState = AmbientSimulatorState , _functionAddrOvHandles = Map.empty , _syscallOvHandles = MapF.empty , _discoveredFunctionHandles = Map.empty - , _populatedMemChunks = IS.empty , _simulationStats = emptyAmbientSimulationStats , _overrideLookupFunctionHandle = Nothing , _sharedMemoryState = AMS.emptyAmbientSharedMemoryState + , _macawLazySimulatorState = DMS.emptyMacawLazySimulatorState } +instance (DMC.ArchAddrWidth arch ~ w) => + DMS.HasMacawLazySimulatorState + (AmbientSimulatorState sym arch) sym w where + macawLazySimulatorState = macawLazySimulatorState + functionOvHandles :: Lens' (AmbientSimulatorState sym arch) (Map.Map WF.FunctionName (AF.FunctionOverrideHandle arch)) functionOvHandles = lens _functionOvHandles @@ -1183,11 +860,6 @@ discoveredFunctionHandles :: Lens' (AmbientSimulatorState sym arch) discoveredFunctionHandles = lens _discoveredFunctionHandles (\s v -> s { _discoveredFunctionHandles = v }) -populatedMemChunks :: Lens' (AmbientSimulatorState sym arch) - (IS.IntervalSet (IMI.Interval (DMM.MemWord (DMC.ArchAddrWidth arch)))) -populatedMemChunks = lens _populatedMemChunks - (\s v -> s { _populatedMemChunks = v }) - -- serverSocketFDs :: Lens' (AmbientSimulatorState sym arch) -- (Map.Map Integer (Some ASONT.ServerSocketInfo)) -- serverSocketFDs = lens _serverSocketFDs @@ -1196,6 +868,10 @@ populatedMemChunks = lens _populatedMemChunks simulationStats :: Lens' (AmbientSimulatorState sym arch) AmbientSimulationStats simulationStats = lens _simulationStats (\s v -> s { _simulationStats = v }) +macawLazySimulatorState :: Lens' (AmbientSimulatorState sym arch) + (DMS.MacawLazySimulatorState sym (DMC.ArchAddrWidth arch)) +macawLazySimulatorState = lens _macawLazySimulatorState (\s v -> s { _macawLazySimulatorState = v }) + overrideLookupFunctionHandle :: Lens' (AmbientSimulatorState sym arch) (Maybe (DMSMO.LookupFunctionHandle (AmbientSimulatorState sym arch) sym arch)) diff --git a/stubs-common/src/Stubs/Extensions/Memory.hs b/stubs-common/src/Stubs/Extensions/Memory.hs deleted file mode 100644 index 6195599..0000000 --- a/stubs-common/src/Stubs/Extensions/Memory.hs +++ /dev/null @@ -1,602 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE EmptyCase #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE NoStarIsType #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeOperators #-} - -module Stubs.Extensions.Memory - ( MemPtrTable(..) - , SymbolicMemChunk(..) - , combineSymbolicMemChunks - , newMemPtrTable - , mapRegionPointers - , mkGlobalPointerValidityPred - , readBytesAsRegValue - ) where - -import qualified Control.Exception as X -import Control.Lens ( folded ) -import Control.Monad.IO.Class ( MonadIO(liftIO) ) -import qualified Data.BitVector.Sized as BV -import qualified Data.ByteString as BS -import qualified Data.IntervalMap.Interval as IMI -import qualified Data.IntervalMap.Strict as IM -import qualified Data.List.Split as Split -import qualified Data.Parameterized.Context as Ctx -import qualified Data.Parameterized.Vector as PV -import qualified Data.Sequence as Seq -import Text.Printf ( printf ) -import GHC.TypeNats ( KnownNat ) - -import qualified Data.Macaw.CFG as DMC -import qualified Data.Macaw.Memory as DMM -import qualified Data.Macaw.Memory.Permissions as DMMP -import qualified Data.Macaw.Symbolic as DMS -import qualified Data.Macaw.Symbolic.Memory as DMSM -import qualified Lang.Crucible.Backend as LCB -import qualified Lang.Crucible.LLVM.DataLayout as LCLD -import qualified Lang.Crucible.LLVM.MemModel as LCLM -import qualified Lang.Crucible.Simulator as LCS -import qualified What4.Interface as WI - -import qualified Stubs.Panic as AP - --- | An index of all of the (statically) mapped memory in a program, suitable --- for pointer translation. This is much like the @MemPtrTable@ in --- @macaw-symbolic@, except that: --- --- 1. This one doesn't have a @memRepr@, since it's not needed. (The --- @MemPtrTable@ in @macaw-symbolic@ probably doesn't need one either, for --- that matter.) --- --- 2. This one separately stores the 'memPtrArray' that gets written into the --- 'memPtr', since we need to add additional assertions to the array as we --- lazily initialize memory. See @Note [Lazy memory initialization]@@. -data MemPtrTable sym arch = - MemPtrTable { memPtrTable :: IM.IntervalMap (DMM.MemWord (DMC.ArchAddrWidth arch)) (SymbolicMemChunk sym) - -- ^ The ranges of (static) allocations that are mapped - , memPtr :: LCLM.LLVMPtr sym (DMC.ArchAddrWidth arch) - -- ^ The pointer to the allocation backing all of memory - , memPtrArray :: WI.SymArray sym (Ctx.SingleCtx (WI.BaseBVType (DMC.ArchAddrWidth arch))) (WI.BaseBVType 8) - -- ^ The SMT array mapping addresses to symbolic bytes - } - --- | A discrete chunk of a memory segment within global memory. Memory is --- lazily initialized one 'SymbolicMemChunk' at a time. See --- @Note [Lazy memory initialization]@. -data SymbolicMemChunk sym = SymbolicMemChunk - { smcBytes :: Seq.Seq (WI.SymBV sym 8) - -- ^ A contiguous region of symbolic bytes backing global memory. - -- The size of this region is no larger than 'chunkSize'. We represent - -- this as a 'Seq.Seq' since we frequently need to append it to other - -- regions (see 'combineSymbolicMemChunks'). - , smcMutability :: LCLM.Mutability - -- ^ Whether the region of memory is mutable or immutable. - } - --- | If two 'SymbolicMemChunk's have the same 'LCLM.Mutability', then return --- @'Just' chunk@, where @chunk@ contains the two arguments' bytes concatenated --- together. Otherwise, return 'Nothing'. -combineSymbolicMemChunks :: - SymbolicMemChunk sym -> - SymbolicMemChunk sym -> - Maybe (SymbolicMemChunk sym) -combineSymbolicMemChunks - (SymbolicMemChunk{smcBytes = bytes1, smcMutability = mutability1}) - (SymbolicMemChunk{smcBytes = bytes2, smcMutability = mutability2}) - | mutability1 == mutability2 - = Just $ SymbolicMemChunk - { smcBytes = bytes1 <> bytes2 - , smcMutability = mutability1 - } - | otherwise - = Nothing - --- | Create a new 'MemPtrTable'. The type signature for this function is very --- similar to that of 'DMS.newGlobalMemory' in @macaw-symbolic@, but unlike --- that function, this one does not initialize the array backing the --- 'MemPtrTable'. Instead, the initialization is deferred until simulation --- begins. See @Note [Lazy memory initialization]@. -newMemPtrTable :: - forall sym bak m t arch w - . ( 16 WI.<= w - , DMM.MemWidth w - , KnownNat w - , w ~ DMC.ArchAddrWidth arch - , LCB.IsSymBackend sym bak - , LCLM.HasLLVMAnn sym - , MonadIO m - , ?memOpts :: LCLM.MemOptions - , Traversable t - ) - => DMSM.GlobalMemoryHooks w - -- ^ Hooks customizing the memory setup - -> bak - -- ^ The symbolic backend used to construct terms - -> LCLD.EndianForm - -- ^ The endianness of values in memory - -> t (DMC.Memory w) - -- ^ The macaw memories - -> m (LCLM.MemImpl sym, MemPtrTable sym arch) -newMemPtrTable hooks bak endian mems = do - let sym = LCB.backendGetSym bak - let ?ptrWidth = DMC.memWidthNatRepr @w - - memImpl1 <- liftIO $ LCLM.emptyMem endian - - let allocName = WI.safeSymbol "globalMemoryBytes" - symArray <- liftIO $ WI.freshConstant sym allocName WI.knownRepr - sizeBV <- liftIO $ WI.maxUnsignedBV sym ?ptrWidth - (ptr, memImpl2) <- liftIO $ LCLM.doMalloc bak LCLM.GlobalAlloc LCLM.Mutable - "Global memory for ambient-verifier" - memImpl1 sizeBV LCLD.noAlignment - - tbl <- liftIO $ mergedMemorySymbolicMemChunks bak hooks mems - memImpl3 <- liftIO $ LCLM.doArrayStore bak memImpl2 ptr LCLD.noAlignment symArray sizeBV - let memPtrTbl = MemPtrTable { memPtrTable = tbl - , memPtr = ptr - , memPtrArray = symArray - } - pure (memImpl3, memPtrTbl) - --- | Construct an 'IM.IntervalMap' mapping regions of memory to their bytes, --- representing as 'SymbolicMemChunk's. The regions of memory are split apart --- to be in units no larger than 'chunkSize' bytes. --- See @Note [Lazy memory initialization]@. -mergedMemorySymbolicMemChunks :: - forall sym bak t w. - ( LCB.IsSymBackend sym bak - , DMM.MemWidth w - , Traversable t - ) => - bak -> - DMSM.GlobalMemoryHooks w -> - t (DMM.Memory w) -> - IO (IM.IntervalMap (DMM.MemWord w) (SymbolicMemChunk sym)) -mergedMemorySymbolicMemChunks bak hooks mems = - fmap (IM.fromList . concat) $ traverse memorySymbolicMemChunks mems - where - sym = LCB.backendGetSym bak - w8 = WI.knownNat @8 - - memorySymbolicMemChunks :: - DMM.Memory w -> - IO [(IM.Interval (DMM.MemWord w), SymbolicMemChunk sym)] - memorySymbolicMemChunks mem = concat <$> - traverse (segmentSymbolicMemChunks mem) (DMM.memSegments mem) - - segmentSymbolicMemChunks :: - DMM.Memory w -> - DMM.MemSegment w -> - IO [(IM.Interval (DMM.MemWord w), SymbolicMemChunk sym)] - segmentSymbolicMemChunks mem seg = concat <$> - traverse (\(addr, chunk) -> - do allBytes <- mkSymbolicMemChunkBytes mem seg addr chunk - let mut | DMMP.isReadonly (DMM.segmentFlags seg) = LCLM.Immutable - | otherwise = LCLM.Mutable - let absAddr = - case DMM.resolveRegionOff mem (DMM.addrBase addr) (DMM.addrOffset addr) of - Just addrOff -> DMM.segmentOffset seg + DMM.segoffOffset addrOff - Nothing -> AP.panic AP.Extensions "segmentSymbolicMemChunks" - ["Failed to resolve function address: " ++ show addr] - let size = length allBytes - let interval = IM.IntervalCO absAddr (absAddr + fromIntegral size) - let intervalChunks = chunksOfInterval (fromIntegral chunkSize) interval - let smcChunks = map (\bytes -> SymbolicMemChunk - { smcBytes = Seq.fromList bytes - , smcMutability = mut - }) - (Split.chunksOf chunkSize allBytes) - -- The length of these two lists should be the same, as - -- @chunksOfInterval size@ should return a list of the same - -- size as @Split.chunksOf size@. - pure $ X.assert (length intervalChunks == length smcChunks) - $ zip intervalChunks smcChunks) - (DMM.relativeSegmentContents [seg]) - - -- NB: This is the same code as in this part of macaw-symbolic: - -- https://github.com/GaloisInc/macaw/blob/ef0ece6a726217fe6231b9ddf523868e491e6ef0/symbolic/src/Data/Macaw/Symbolic/Memory.hs#L373-L378 - mkSymbolicMemChunkBytes :: - DMM.Memory w - -> DMM.MemSegment w - -> DMM.MemAddr w - -> DMM.MemChunk w - -> IO [WI.SymBV sym 8] - mkSymbolicMemChunkBytes mem seg addr memChunk = - liftIO $ case memChunk of - DMM.RelocationRegion reloc -> - DMSM.populateRelocation hooks bak mem seg addr reloc - DMM.BSSRegion sz -> - replicate (fromIntegral sz) <$> WI.bvLit sym w8 (BV.zero w8) - DMM.ByteRegion bytes -> - traverse (WI.bvLit sym w8 . BV.word8) $ BS.unpack bytes - --- | The maximum size of a 'SymbolicMemChunk', which determines the granularity --- at which the regions of memory in a 'memPtrTable' are chunked up. --- See @Note [Lazy memory initialization]@. --- --- Currently, `chunkSize` is 1024, which is a relatively small number --- that is the right value to be properly aligned on most architectures. -chunkSize :: Int -chunkSize = 1024 - --- | @'splitInterval' x i@ returns @'Just' (i1, i2)@ if @hi - lo@ is strictly --- greater than @x@, where: --- --- * @lo@ is @l@'s lower bound and @hi@ is @l@'s upper bound. --- --- * @i1@ is the subinterval of @i@ starting from @i@'s lower bound and going up --- to (but not including) @lo + x@. --- --- * @i2@ is the subinterval of @i@ starting from @lo + x@ and going up to @hi@. --- --- Otherwise, this returns 'Nothing'. -splitInterval :: (Integral a, Ord a) => a -> IMI.Interval a -> Maybe (IMI.Interval a, IMI.Interval a) -splitInterval x i - | x <= 0 - = AP.panic AP.Extensions "splitInterval" - [ "chunk size must be positive, got " ++ show (toInteger x) ] - | x < (IMI.upperBound i - IMI.lowerBound i) - = Just $ case i of - IMI.OpenInterval lo hi -> (IMI.OpenInterval lo (lo + x), IMI.IntervalCO (lo + x) hi) - IMI.ClosedInterval lo hi -> (IMI.IntervalCO lo (lo + x), IMI.ClosedInterval (lo + x) hi) - IMI.IntervalCO lo hi -> (IMI.IntervalCO lo (lo + x), IMI.IntervalCO (lo + x) hi) - IMI.IntervalOC lo hi -> (IMI.OpenInterval lo (lo + x), IMI.ClosedInterval (lo + x) hi) - | otherwise - = Nothing - --- | Like the 'L.chunksOf' function, but over an 'IMI.Interval' instead of a --- list. -chunksOfInterval :: (Integral a, Ord a) => a -> IMI.Interval a -> [IMI.Interval a] -chunksOfInterval x = go - where - go i = case splitInterval x i of - Just (i1, i2) -> i1 : go i2 - Nothing -> [i] - --- | Construct a translator for machine addresses into LLVM memory model pointers. --- --- This translator is used by the symbolic simulator to resolve memory addresses. - --- NB: This is nearly identical to the function of the same name in --- macaw-symbolic, the only difference being that we use a different --- MemPtrTable data type. -mapRegionPointers :: ( DMM.MemWidth w - , 16 WI.<= w - , LCB.IsSymInterface sym - , LCLM.HasLLVMAnn sym - , ?memOpts :: LCLM.MemOptions - , DMC.ArchAddrWidth arch ~ w - ) - => MemPtrTable sym arch - -> DMS.GlobalMap sym LCLM.Mem w -mapRegionPointers mpt = DMS.GlobalMap $ \bak mem regionNum offsetVal -> - let sym = LCB.backendGetSym bak in - case WI.asNat regionNum of - Just 0 -> do - let ?ptrWidth = WI.bvWidth offsetVal - LCLM.doPtrAddOffset bak mem (memPtr mpt) offsetVal - Just _ -> - -- This is the case where the region number is concrete and non-zero, - -- meaning that it is already an LLVM pointer - -- - -- NOTE: This case is not possible because we only call this from - -- 'tryGlobPtr', which handles this case separately - return (LCLM.LLVMPointer regionNum offsetVal) - Nothing -> do - -- In this case, the region number is symbolic, so we need to be very - -- careful to handle the possibility that it is zero (and thus must be - -- conditionally mapped to one or all of our statically-allocated regions. - -- - -- NOTE: We can avoid making a huge static mux over all regions: the - -- low-level memory model code already handles building the mux tree as it - -- walks backwards over all allocations that are live. - -- - -- We just need to add one top-level mux: - -- - -- > ite (blockid == 0) (translate base) (leave alone) - let ?ptrWidth = WI.bvWidth offsetVal - zeroNat <- WI.natLit sym 0 - isZeroRegion <- WI.natEq sym zeroNat regionNum - -- The pointer mapped to global memory (if the region number is zero) - globalPtr <- LCLM.doPtrAddOffset bak mem (memPtr mpt) offsetVal - LCLM.muxLLVMPtr sym isZeroRegion globalPtr (LCLM.LLVMPointer regionNum offsetVal) - --- | Create a function that computes a validity predicate for an LLVMPointer --- that may point to the static global memory region. --- --- We represent all of the statically allocated storage in a binary in a single --- LLVM array. This array is sparse, meaning that large ranges of the address --- space are not actually mapped. Whenever we use a pointer into this memory --- region, we want to assert that it is inside one of the mapped regions and --- that it does not violate any mutability constraints. --- --- The mapped regions are recorded in the MemPtrTable. --- --- We need to be a little careful: if the BlockID of the pointer is definitely --- zero, we make a direct assertion. Otherwise, if the pointer is symbolic, we --- have to conditionally assert the range validity. --- --- Note that we pass in an indication of the use of the pointer: if the pointer --- is used to write, it must only be within the writable portion of the address --- space (which is also recorded in the MemPtrTable). If the write is --- conditional, we must additionally mix in the predicate. --- --- This is intended as a reasonable implementation of the --- 'MS.MkGlobalPointerValidityPred'. - --- NB: This is nearly identical to the function of the same name in --- macaw-symbolic, the only difference being that we use a different --- MemPtrTable data type. -mkGlobalPointerValidityPred :: forall sym w arch - . ( LCB.IsSymInterface sym - , DMM.MemWidth w - , w ~ DMC.ArchAddrWidth arch - ) - => MemPtrTable sym arch - -> DMS.MkGlobalPointerValidityAssertion sym w -mkGlobalPointerValidityPred mpt = \sym puse mcond ptr -> do - let w = DMM.memWidthNatRepr @w - -- If this is a write, the pointer cannot be in an immutable range (so just - -- return False for the predicate on that range). - -- - -- Otherwise, the pointer is allowed to be between the lo/hi range - let inMappedRange off (range, mut) - | DMS.pointerUseTag puse == DMS.PointerWrite && mut == LCLM.Immutable = return (WI.falsePred sym) - | otherwise = - case range of - IM.IntervalCO lo hi -> do - lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo)) - hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi)) - lob <- WI.bvUle sym lobv off - hib <- WI.bvUlt sym off hibv - WI.andPred sym lob hib - IM.ClosedInterval lo hi -> do - lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo)) - hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi)) - lob <- WI.bvUle sym lobv off - hib <- WI.bvUle sym off hibv - WI.andPred sym lob hib - IM.OpenInterval lo hi -> do - lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo)) - hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi)) - lob <- WI.bvUlt sym lobv off - hib <- WI.bvUlt sym off hibv - WI.andPred sym lob hib - IM.IntervalOC lo hi -> do - lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo)) - hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi)) - lob <- WI.bvUlt sym lobv off - hib <- WI.bvUle sym off hibv - WI.andPred sym lob hib - - let mkPred off = do - ps <- mapM (inMappedRange off) $ IM.toList $ fmap smcMutability $ memPtrTable mpt - ps' <- WI.orOneOf sym (folded . id) ps - -- Add the condition from a conditional write - WI.itePred sym (maybe (WI.truePred sym) LCS.regValue mcond) ps' (WI.truePred sym) - - - let ptrVal = LCS.regValue ptr - let (ptrBase, ptrOff) = LCLM.llvmPointerView ptrVal - case WI.asNat ptrBase of - Just 0 -> do - p <- mkPred ptrOff - let msg = printf "%s outside of static memory range (known BlockID 0): %s" (show (DMS.pointerUseTag puse)) (show (WI.printSymExpr ptrOff)) - let loc = DMS.pointerUseLocation puse - let assertion = LCB.LabeledPred p (LCS.SimError loc (LCS.GenericSimError msg)) - return (Just assertion) - Just _ -> return Nothing - Nothing -> do - -- In this case, we don't know for sure if the block id is 0, but it could - -- be (it is symbolic). The assertion has to be conditioned on the equality. - p <- mkPred ptrOff - zeroNat <- WI.natLit sym 0 - isZeroBase <- WI.natEq sym zeroNat ptrBase - p' <- WI.itePred sym isZeroBase p (WI.truePred sym) - let msg = printf "%s outside of static memory range (unknown BlockID): %s" (show (DMS.pointerUseTag puse)) (show (WI.printSymExpr ptrOff)) - let loc = DMS.pointerUseLocation puse - let assertion = LCB.LabeledPred p' (LCS.SimError loc (LCS.GenericSimError msg)) - return (Just assertion) - --- | @'readBytesAsRegValue' sym repr bytes@ reads symbolic bytes from @bytes@ --- and interprets it as a 'LCS.RegValue' of the appropriate type, which is --- determined by @repr@. --- --- This function checks that the length of @bytes@ is equal to --- @'DMC.memReprBytes' repr@, throwing a panic if this is not the case. -readBytesAsRegValue :: - LCB.IsSymInterface sym => - sym -> - DMC.MemRepr ty -> - [WI.SymBV sym 8] -> - IO (LCS.RegValue sym (DMS.ToCrucibleType ty)) -readBytesAsRegValue sym repr bytes = - case repr of - DMC.BVMemRepr byteWidth endianness -> do - bytesV <- maybe (panic [ "Expected " ++ show byteWidth ++ " symbolic bytes," - , "Received " ++ show (length bytes) ++ " bytes" - ]) pure $ - PV.fromList byteWidth bytes - bytesBV <- readBytesAsBV sym endianness bytesV - LCLM.llvmPointer_bv sym bytesBV - DMC.FloatMemRepr {} -> - panic ["Reading floating point values is not currently supported"] - DMC.PackedVecMemRepr {} -> - panic ["Reading packed vector values is not currently supported"] - where - panic = AP.panic AP.Extensions "readBytesAsRegValue" - --- | Read @numBytes@ worth of symbolic bytes and concatenate them into a single --- 'WI.SymBV', respecting endianness. This is used to service concrete reads of --- immutable global memory. See @Note [Lazy memory initialization]@. -readBytesAsBV - :: forall sym numBytes - . ( LCB.IsSymInterface sym - , 1 WI.<= numBytes - ) - => sym - -> DMM.Endianness - -> PV.Vector numBytes (WI.SymBV sym 8) - -> IO (WI.SymBV sym (8 WI.* numBytes)) -readBytesAsBV sym endianness = go - where - -- Iterate through the bytes one at a time, concatenating each byte along - -- the way. The implementation of this function looks larger than it - -- actually is due to needing to perform type-level Nat arithmetic to make - -- things typecheck. The details of the type-level arithmetic were copied - -- from PATE (https://github.com/GaloisInc/pate/blob/815d906243fef33993e340b8965567abe5bfcde0/src/Pate/Memory/MemTrace.hs#L1204-L1229), - -- which is licensed under the 3-Clause BSD license. - go :: forall bytesLeft - . (1 WI.<= bytesLeft) - => PV.Vector bytesLeft (WI.SymBV sym 8) - -> IO (WI.SymBV sym (8 WI.* bytesLeft)) - go bytesV = - let resWidth = PV.length bytesV in - let (headByte, unconsRes) = PV.uncons bytesV in - case WI.isZeroOrGT1 (WI.decNat resWidth) of - -- We have only one byte left, so return it. - Left WI.Refl -> do - WI.Refl <- return $ zeroSubEq resWidth (WI.knownNat @1) - pure headByte - -- We have more than one byte left, so recurse. - Right WI.LeqProof -> - case unconsRes of - -- If this were Left, that would mean that there would only be - -- one byte left, which is impossible due to the assumptions above. - -- That is, this case is unreachable. Thankfully, GHC's constraint - -- solver is smart enough to realize this in conjunction with - -- EmptyCase. - Left x -> case x of {} - Right tailV -> do - let recByteWidth = WI.decNat resWidth - tailBytes <- go tailV - - WI.Refl <- return $ WI.lemmaMul (WI.knownNat @8) resWidth - WI.Refl <- return $ WI.mulComm (WI.knownNat @8) recByteWidth - WI.Refl <- return $ WI.mulComm (WI.knownNat @8) resWidth - WI.LeqProof <- return $ mulMono (WI.knownNat @8) recByteWidth - concatBytes sym endianness headByte tailBytes - --- | Concat a byte onto a larger word, respecting endianness. -concatBytes - :: ( LCB.IsSymInterface sym - , 1 WI.<= w - ) - => sym - -> DMM.Endianness - -> WI.SymBV sym 8 - -> WI.SymBV sym w - -> IO (WI.SymBV sym (8 WI.+ w)) -concatBytes sym endianness byte bytes = - case endianness of - DMM.BigEndian -> WI.bvConcat sym byte bytes - DMM.LittleEndian -> do - WI.Refl <- return $ WI.plusComm (WI.bvWidth byte) (WI.bvWidth bytes) - WI.bvConcat sym bytes byte - --- Additional proof combinators - -mulMono :: forall p q x w. (1 WI.<= x, 1 WI.<= w) => p x -> q w -> WI.LeqProof 1 (x WI.* w) -mulMono x w = WI.leqTrans (WI.LeqProof @1 @w) (WI.leqMulMono x w) - -zeroSubEq :: forall p q w n. (n WI.<= w, 0 ~ (w WI.- n)) => p w -> q n -> w WI.:~: n -zeroSubEq w n - | WI.Refl <- WI.minusPlusCancel w n - = WI.Refl - -{- -Note [Lazy memory initialization] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We back the global memory in a binary with an SMT array of symbolic bytes. One -issue with this approach is that initializing the elements of this array is -expensive. Despite our best efforts to optimize how SMT array initialization -takes places, filling in each byte of a large (i.e., several megabytes or more) -binary upfront is usually enough eat up all the RAM on your machine. - -For this reason, we deliberately avoid populating the entire array upfront. -Instead, we initialize memory lazily. Here is a first approximation of how this -works: - -* When the verifier starts, we create an empty SMT array to back global memory - but do not initialize any of its elements. (See `newMemPtrTable` for how this - is implemented.) We store this array in a MemPtrTable for later use. - -* At the same time, we also store an IntervalMap in the MemPtrTable - that maps the addresses in each memory segment to the corresponding bytes. - (See the `SymbolicMemChunk` data type, which stores these bytes.) - -* During simulation, if we attempt to access global memory, we first check - to see if we have previously accessed the memory segment(s) corresponding to - the addresses that were are accessing. If we haven't, we then initialize the - bytes corresponding to those memory segments (and _only_ those memory - segments) in the SMT array. We then record the fact that we have accessed - these segments in the `populatedMemChunks` field of the - `AmbientSimulatorState`. - -* How do we determine which memory segments correspond to a particular read or - write? If it is a concrete read or write, this is straightforward, as we need - only look up a single address in the IntervalMap. If it is a symbolic read or - write, then things are trickier, since it could potentially access different - memory regions. To accommodate this, we construct an interval spanning all of - the possible addresses that the read/write could access (see - Ambient.Extensions.ptrOffsetInterval and retrieve all parts of the - IntervalMap that intersect with the interval. This is costly, but it ensures - that the approach is sound. - -This approach ensures that we only pay the cost of memory initialization when -it is absolutely necessary. In order to make it less costly, we also implement -two important optimizations: - -1. Even if the memory is only initialized one memory segment at a time, that - can still be expensive if one accesses memory in a very large segment. - What's more, one usually only needs to access a small portion of the - large segment, but with the approach described above, you'd still have to pay - the cost of initializing the entire segment. - - For this reason, we split up the memory addresses at an even finer - granularity than just the memory segments when creating the IntervalMap. - We go further and split up each segment into chunks of `chunkSize` bytes - each. This way, most memory accesses will only require initializing small - chunks of the array, even if they happen to reside within large memory - segments. - - Currently, `chunkSize` is 1024, which is a relatively small number - that is the right value to be properly aligned on most architectures. - -2. While tracking the writable global memory in an SMT array is important in - case the memory gets updated, there's really no need to track the - read-only global memory in an SMT array. After all, read-only memory can - never be updated, so we can determine what read-only memory will be by - looking up the corresponding bytes in the IntervalMap, bypassing the SMT - array completely. - - To determine which parts of memory are read-only, each `SymbolicMemChunk` - tracks whether its bytes are mutable or immutable. When performing a memory - read, if we can conclude that all of the memory to be read is immutable - (i.e., read-only), then we can convert the symbolic bytes to a bitvector. - (See `readBytesAsRegValue` for how this is implemented.) - - There are several criteria that must be met in order for this to be - possible: - - * The read must be concrete. - - * The amount of bytes to be read must lie within a contiguous part of - read-only memory. - - * There must be enough bytes within this part of memory to cover the number - of bytes that must be read. - - If one of these critera are not met, we fall back on the SMT array approach. - -At some point, we would like to upstream this work to macaw-symbolic, as -nothing here is specific to AMBIENT. See -https://github.com/GaloisInc/macaw/issues/282. Much of the code that implements -was copied from macaw-symbolic itself, which is licensed under the 3-Clause BSD -license. --} diff --git a/stubs-common/src/Stubs/Memory.hs b/stubs-common/src/Stubs/Memory.hs index 6db6db7..754e63d 100644 --- a/stubs-common/src/Stubs/Memory.hs +++ b/stubs-common/src/Stubs/Memory.hs @@ -36,6 +36,7 @@ import qualified Text.Megaparsec as TM import qualified Text.Megaparsec.Char as TMC import qualified Data.Macaw.Symbolic as DMS +import qualified Data.Macaw.Symbolic.Memory.Lazy as DMSM import qualified Lang.Crucible.Simulator as LCS import qualified Lang.Crucible.Simulator.GlobalState as LCSG @@ -129,7 +130,7 @@ data (IsStubsMemoryModel mem arch) => InitialMemory sym mem arch = -- ^ Initial global variables , imStackBasePtr :: LCS.RegValue sym (PtrType mem arch) -- ^ Stack memory base pointer - , imMemTable :: MemTable sym mem arch + , imMemTable :: DMSM.MemPtrTable sym (DMC.ArchAddrWidth arch) , imGlobalMap :: MemMap sym arch } diff --git a/stubs-common/src/Stubs/Memory/AArch32/Linux.hs b/stubs-common/src/Stubs/Memory/AArch32/Linux.hs index 52a9172..b9f4fdd 100644 --- a/stubs-common/src/Stubs/Memory/AArch32/Linux.hs +++ b/stubs-common/src/Stubs/Memory/AArch32/Linux.hs @@ -20,6 +20,7 @@ module Stubs.Memory.AArch32.Linux ( ) where import qualified Data.BitVector.Sized as BVS +import Data.Proxy (Proxy(..)) import qualified Data.Text as DT import qualified Data.Macaw.ARM as DMA @@ -46,7 +47,7 @@ import qualified Lang.Crucible.LLVM.MemModel.Partial as LCLMP import qualified Lang.Crucible.LLVM.Errors as LCLE import qualified Lang.Crucible.LLVM.MemModel.CallStack import qualified Lang.Crucible.Types as LCT -import qualified Data.Macaw.Symbolic.Memory as DMSM +import qualified Data.Macaw.Symbolic.Memory.Lazy as DMSM import qualified Data.Macaw.Architecture.Info as DMA import qualified Data.Parameterized.NatRepr as PN import qualified Stubs.Memory as SM @@ -55,7 +56,6 @@ import Control.Monad.IO.Class (MonadIO(..)) import Data.Macaw.AArch32.Symbolic () import qualified Stubs.Extensions as SE import qualified Data.Macaw.Symbolic.MemOps as DMSMO -import qualified Stubs.Extensions.Memory as AEM import qualified Data.Macaw.BinaryLoader as DMB import qualified Stubs.Loader.BinaryConfig as SLB import qualified Stubs.Memory.Common as SMC @@ -64,7 +64,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory SAA.AArch32 where type instance PtrType DMS.LLVMMemory SAA.AArch32 = LCLM.LLVMPointerType (DMC.ArchAddrWidth SAA.AArch32) type instance MemType DMS.LLVMMemory SAA.AArch32 = LCLM.Mem type instance BVToPtrTy w DMS.LLVMMemory SAA.AArch32 = LCLM.LLVMPointerType w - type instance MemTable sym DMS.LLVMMemory SAA.AArch32 = AEM.MemPtrTable sym SAA.AArch32 + type instance MemTable sym DMS.LLVMMemory SAA.AArch32 = DMSM.MemPtrTable sym 32 type instance MemMap sym SAA.AArch32 = DMSMO.GlobalMap sym LCLM.Mem (DMC.ArchAddrWidth SAA.AArch32) type instance VerifierState sym DMS.LLVMMemory SAA.AArch32 = (SE.AmbientSimulatorState sym SAA.AArch32) @@ -115,7 +115,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory SAA.AArch32 where (recordFn, _) <- liftIO SM.buildRecordLLVMAnnotation let ?recordLLVMAnnotation = recordFn let ?memOpts = LCLM.defaultMemOptions - (mem, memPtrTbl) <- AEM.newMemPtrTable (SMC.globalMemoryHooks mems mempty mempty) bak endian mems + (mem, memPtrTbl) <- DMSM.newMergedGlobalMemoryWith (SMC.globalMemoryHooks mems mempty mempty) (Proxy @SAA.AArch32) bak endian DMSM.ConcreteMutable mems stackSizeBV <- liftIO $ WI.bvLit sym WI.knownRepr (BVS.mkBV WI.knownRepr stackSize) (stackBasePtr, mem1) <- liftIO $ LCLM.doMalloc bak LCLM.StackAlloc LCLM.Mutable "stack_alloc" mem stackSizeBV LCLD.noAlignment @@ -127,7 +127,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory SAA.AArch32 where (mem3, globals0) <- liftIO $ aarch32LinuxInitGlobals tlsvar (SC.Sym sym bak) mem2 memVar <- liftIO $ LCLM.mkMemVar (DT.pack "stubs::memory") halloc let globals1 = LCSG.insertGlobal memVar mem3 globals0 - let globalMap = AEM.mapRegionPointers memPtrTbl + let globalMap = DMSM.mapRegionPointers memPtrTbl return SM.InitialMemory{ SM.imMemVar=memVar, diff --git a/stubs-common/src/Stubs/Memory/PPC/Linux.hs b/stubs-common/src/Stubs/Memory/PPC/Linux.hs index 14e4521..dcb4f13 100644 --- a/stubs-common/src/Stubs/Memory/PPC/Linux.hs +++ b/stubs-common/src/Stubs/Memory/PPC/Linux.hs @@ -19,6 +19,7 @@ module Stubs.Memory.PPC.Linux (ppcLinuxStmtExtensionOverride) where import qualified Data.BitVector.Sized as BVS +import Data.Proxy (Proxy(..)) import qualified Data.Text as DT import qualified Data.Macaw.Symbolic as DMS @@ -32,7 +33,7 @@ import qualified Stubs.Memory as AM import qualified Stubs.Common as SC import qualified Lang.Crucible.FunctionHandle as LCF import qualified Lang.Crucible.Types as LCT -import qualified Data.Macaw.Symbolic.Memory as DMSM +import qualified Data.Macaw.Symbolic.Memory.Lazy as DMSM import qualified Data.Macaw.Architecture.Info as DMA import qualified Data.Parameterized.NatRepr as PN import qualified Stubs.Memory as SM @@ -42,7 +43,6 @@ import qualified Data.Macaw.PPC as DMP import Data.Macaw.PPC.Symbolic () import qualified Stubs.Extensions as SE import qualified Data.Macaw.Symbolic.MemOps as DMSMO -import qualified Stubs.Extensions.Memory as AEM import qualified Data.Macaw.BinaryLoader as DMB import qualified Stubs.Loader.BinaryConfig as SLB import qualified Stubs.Memory.Common as SMC @@ -52,7 +52,7 @@ instance (DMS.SymArchConstraints (DMP.AnyPPC v), 16 WI.<= SAP.AddrWidth v) => type instance PtrType DMS.LLVMMemory (DMP.AnyPPC v) = LCLM.LLVMPointerType (SAP.AddrWidth v) type instance MemType DMS.LLVMMemory (DMP.AnyPPC v) = LCLM.Mem type instance BVToPtrTy w DMS.LLVMMemory (DMP.AnyPPC v) = LCLM.LLVMPointerType w - type instance MemTable sym DMS.LLVMMemory (DMP.AnyPPC v) = AEM.MemPtrTable sym (DMP.AnyPPC v) + type instance MemTable sym DMS.LLVMMemory (DMP.AnyPPC v) = DMSM.MemPtrTable sym (SAP.AddrWidth v) type instance MemMap sym (DMP.AnyPPC v) = DMSMO.GlobalMap sym LCLM.Mem (SAP.AddrWidth v) type instance VerifierState sym DMS.LLVMMemory (DMP.AnyPPC v) = SE.AmbientSimulatorState sym (DMP.AnyPPC v) @@ -103,7 +103,7 @@ instance (DMS.SymArchConstraints (DMP.AnyPPC v), 16 WI.<= SAP.AddrWidth v) => (recordFn, _) <- liftIO SM.buildRecordLLVMAnnotation let ?recordLLVMAnnotation = recordFn let ?memOpts = LCLM.defaultMemOptions - (mem, memPtrTbl) <- AEM.newMemPtrTable (SMC.globalMemoryHooks mems mempty mempty) bak endian mems + (mem, memPtrTbl) <- DMSM.newMergedGlobalMemoryWith (SMC.globalMemoryHooks mems mempty mempty) (Proxy @(DMP.AnyPPC v)) bak endian DMSM.ConcreteMutable mems stackSizeBV <- liftIO $ WI.bvLit sym WI.knownRepr (BVS.mkBV WI.knownRepr stackSize) (stackBasePtr, mem1) <- liftIO $ LCLM.doMalloc bak LCLM.StackAlloc LCLM.Mutable "stack_alloc" mem stackSizeBV LCLD.noAlignment @@ -113,7 +113,7 @@ instance (DMS.SymArchConstraints (DMP.AnyPPC v), 16 WI.<= SAP.AddrWidth v) => memVar <- liftIO $ LCLM.mkMemVar (DT.pack "stubs::memory") halloc let globals = LCSG.insertGlobal memVar mem2 LCSG.emptyGlobals - let globalMap = AEM.mapRegionPointers memPtrTbl + let globalMap = DMSM.mapRegionPointers memPtrTbl return SM.InitialMemory{ SM.imMemVar=memVar, diff --git a/stubs-common/src/Stubs/Memory/X86_64/Linux.hs b/stubs-common/src/Stubs/Memory/X86_64/Linux.hs index f20d166..d32cba6 100644 --- a/stubs-common/src/Stubs/Memory/X86_64/Linux.hs +++ b/stubs-common/src/Stubs/Memory/X86_64/Linux.hs @@ -24,6 +24,7 @@ module Stubs.Memory.X86_64.Linux ( import Control.Lens ((^.)) import qualified Data.BitVector.Sized as BVS +import Data.Proxy (Proxy(..)) import qualified Data.Macaw.CFG as DMC import qualified Data.Macaw.Symbolic as DMS @@ -47,7 +48,7 @@ import qualified Stubs.Panic as AP import qualified Stubs.Memory as SM import qualified Lang.Crucible.Types as LCT import qualified Stubs.Common as SC -import qualified Data.Macaw.Symbolic.Memory as DMSM +import qualified Data.Macaw.Symbolic.Memory.Lazy as DMSM import qualified Data.Macaw.X86 as DMA import qualified Data.Macaw.X86.Symbolic () import Control.Monad.IO.Class (liftIO, MonadIO) @@ -59,7 +60,6 @@ import qualified Lang.Crucible.LLVM.MemModel.Partial as LCLMP import qualified Stubs.Memory.Common as SMC import qualified Stubs.Logging as SL import qualified Stubs.Extensions as SE -import qualified Stubs.Extensions.Memory as AEM import qualified Data.Macaw.Symbolic as DMSMO import qualified Stubs.Loader.BinaryConfig as SLB import qualified Data.Macaw.BinaryLoader as DMB @@ -69,7 +69,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory DMX.X86_64 where type instance PtrType DMS.LLVMMemory DMX.X86_64 = LCLM.LLVMPointerType (DMC.ArchAddrWidth DMX.X86_64) type instance MemType DMS.LLVMMemory DMX.X86_64 = LCLM.Mem type instance BVToPtrTy w DMS.LLVMMemory DMX.X86_64 = LCLM.LLVMPointerType w - type instance MemTable sym DMS.LLVMMemory DMX.X86_64 = AEM.MemPtrTable sym DMX.X86_64 + type instance MemTable sym DMS.LLVMMemory DMX.X86_64 = DMSM.MemPtrTable sym 64 type instance MemMap sym DMX.X86_64 = DMSMO.GlobalMap sym LCLM.Mem (DMC.ArchAddrWidth DMX.X86_64) type instance VerifierState sym DMS.LLVMMemory DMX.X86_64 = (SE.AmbientSimulatorState sym DMX.X86_64) @@ -92,35 +92,13 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory DMX.X86_64 where (re, _) <- liftIO $ SM.buildRecordLLVMAnnotation @sym let ?recordLLVMAnnotation = re let mpt = SM.imMemTable initialMem - -- This MemModelConfig is very nearly the same as the memModelConfig that - -- Data.Macaw.Symbolic.Memory provides, but we have to duplicate some logic - -- here since `stubs` uses a different MemPtrTable data type than - -- `macaw-symbolic`. Note that some of these fields (e.g., the - -- `mkGlobalPointerValidityAssertion` field) will effectively go unused, as - -- `stubs-common`'s memory model overrides certain operations that would - -- otherwise use these fields. - -- - -- In the future, it would be preferable to build on top of the - -- `macaw-symbolic` lazy memory model, whose functionality largely overlaps - -- with the `stubs-common` memory model. See - -- https://github.com/GaloisInc/stubs/issues/12. let mmConf = - DMS.MemModelConfig - { DMS.globalMemMap = - AEM.mapRegionPointers mpt - , DMS.lookupFunctionHandle = + (DMSM.memModelConfig bak mpt) + { DMS.lookupFunctionHandle = SMC.symExLookupFunction SL.emptyLogger bak initialMem archVals binconf functionABI halloc archInfo Nothing , DMS.lookupSyscallHandle = SMC.symExLookupSyscall bak syscallABI halloc - , DMS.mkGlobalPointerValidityAssertion = - AEM.mkGlobalPointerValidityPred mpt - , DMS.resolvePointer = - pure - , DMS.concreteImmutableGlobalRead = - \_ _ -> pure Nothing - , DMS.lazilyPopulateGlobalMem = - \_ _ -> pure } return $ SE.ambientExtensions @sym @DMX.X86_64 bak f initialMem mmConf mempty @@ -178,7 +156,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory DMX.X86_64 where let supportedRelocs = SLB.bcSupportedRelocations binConf let globs = SLB.bcDynamicGlobalVarAddrs binConf - (mem, memPtrTbl) <- AEM.newMemPtrTable (SMC.globalMemoryHooks mems globs supportedRelocs) bak endian mems + (mem, memPtrTbl) <- DMSM.newMergedGlobalMemoryWith (SMC.globalMemoryHooks mems globs supportedRelocs) (Proxy @DMX.X86_64) bak endian DMSM.ConcreteMutable mems (stackBasePtr, mem1) <- liftIO $ LCLM.doMalloc bak LCLM.StackAlloc LCLM.Mutable "stack_alloc" mem stackSizeBV LCLD.noAlignment fsvar <- liftIO $ freshFSBaseGlobalVar halloc gsvar <- liftIO $ freshGSBaseGlobalVar halloc @@ -188,7 +166,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory DMX.X86_64 where memVar <- liftIO $ LCLM.mkMemVar (DT.pack "stubs::memory") halloc let globals1 = LCSG.insertGlobal memVar mem3 globals0 - let globalMap = AEM.mapRegionPointers memPtrTbl + let globalMap = DMSM.mapRegionPointers memPtrTbl return SM.InitialMemory{ SM.imMemVar=memVar, SM.imGlobals=globals1, diff --git a/stubs-common/stubs-common.cabal b/stubs-common/stubs-common.cabal index 00a5493..be90971 100644 --- a/stubs-common/stubs-common.cabal +++ b/stubs-common/stubs-common.cabal @@ -53,7 +53,6 @@ library Stubs.EnvVar, Stubs.Exception, Stubs.Extensions, - Stubs.Extensions.Memory, Stubs.FunctionOverride, Stubs.FunctionOverride.ArgumentMapping, Stubs.FunctionOverride.Common,