-------------------------------------------------------------------- -- | -- Module : Lang.Crucible.LLVM.MemModel -- Description : Core definitions of the symbolic C memory model -- Copyright : (c) Galois, Inc 2015-2016 -- License : BSD3 -- Maintainer : Rob Dockins -- Stability : provisional ------------------------------------------------------------------------ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances, FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Lang.Crucible.LLVM.MemModel ( -- * Memories Mem , memRepr , mkMemVar , MemImpl(..) , SomePointer(..) , GlobalMap , emptyMem , memEndian , memAllocCount , memWriteCount , G.ppMem , doDumpMem , BlockSource(..) , nextBlock , MemOptions(..) , IndeterminateLoadBehavior(..) , defaultMemOptions , laxPointerMemOptions -- * Pointers , LLVMPointerType , pattern LLVMPointerRepr , pattern PtrRepr , pattern SizeT , LLVMPtr , pattern LLVMPointer , llvmPointerView , ptrWidth , G.ppPtr , G.ppTermExpr , llvmPointer_bv , Partial.projectLLVM_bv -- * Memory operations , doMalloc , doMallocUnbounded , G.AllocType(..) , G.Mutability(..) , doMallocHandle , ME.FuncLookupError(..) , ME.ppFuncLookupError , doLookupHandle , doInstallHandle , doMemcpy , doMemset , doInvalidate , doCalloc , doFree , doAlloca , doLoad , doStore , doArrayStore , doArrayStoreUnbounded , doArrayConstStore , doArrayConstStoreUnbounded , loadString , loadMaybeString , strLen , uncheckedMemcpy , bindLLVMFunPtr -- * \"Raw\" operations with LLVMVal , LLVMVal(..) , ppLLVMValWithGlobals , FloatSize(..) , unpackMemValue , packMemValue , loadRaw , storeRaw , condStoreRaw , storeConstRaw , mallocRaw , mallocConstRaw , constToLLVMVal , constToLLVMValP , ptrMessage , Partial.PartLLVMVal(..) , Partial.assertSafe , explodeStringValue -- Re-exports from MemModel.Value , isZero , testEqual , llvmValStorableType -- * Storage types , StorageType , storageTypeF , StorageTypeF(..) , Field , storageTypeSize , fieldVal , fieldPad , fieldOffset , bitvectorType , arrayType , mkStructType , floatType , doubleType , x86_fp80Type , toStorableType -- * Pointer operations , ptrToPtrVal , mkNullPointer , ptrIsNull , ptrEq , ptrAdd , ptrSub , ptrDiff , doPtrAddOffset , doPtrSubtract , isValidPointer , isAllocatedAlignedPointer , muxLLVMPtr , G.isAligned -- * Disjointness , assertDisjointRegions , buildDisjointRegionsAssertion , buildDisjointRegionsAssertionWithSub -- * Globals , GlobalSymbol(..) , doResolveGlobal , registerGlobal , allocGlobals , allocGlobal , isGlobalPointer -- * Misc , llvmStatementExec , G.pushStackFrameMem , G.popStackFrameMem , G.asMemAllocationArrayStore , SomeFnHandle(..) , G.SomeAlloc(..) , G.possibleAllocs , G.ppSomeAlloc , doConditionalWriteOperation , mergeWriteOperations , Partial.HasLLVMAnn , Partial.LLVMAnnMap , Partial.CexExplanation(..) , Partial.explainCex -- * PtrWidth (re-exports) , HasPtrWidth , pattern PtrWidth , withPtrWidth -- * Concretization , ML.concPtr , ML.concLLVMVal , ML.concMem , concMemImpl ) where import Prelude hiding (seq) import Control.Lens hiding (Empty, (:>)) import Control.Monad import Control.Monad.IO.Class import Control.Monad.Trans (lift) import Control.Monad.Trans.State import Data.Dynamic import Data.IORef import Data.Map (Map) import qualified Data.Map as Map import Data.Maybe import Data.Text (Text) import Data.Word import qualified GHC.Stack as GHC import Numeric.Natural (Natural) import System.IO (Handle, hPutStrLn) import qualified Data.BitVector.Sized as BV import Data.Parameterized.Classes import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.NatRepr import Data.Parameterized.Some import qualified Data.Vector as V import qualified Text.LLVM.AST as L import What4.Interface import What4.Expr( GroundValue ) import What4.InterpretedFloatingPoint import What4.ProgramLoc import Lang.Crucible.Backend import Lang.Crucible.CFG.Common import Lang.Crucible.FunctionHandle import Lang.Crucible.Types import Lang.Crucible.Simulator.ExecutionTree import Lang.Crucible.Simulator.GlobalState import Lang.Crucible.Simulator.Intrinsics import Lang.Crucible.Simulator.RegMap import Lang.Crucible.Simulator.SimError import Lang.Crucible.LLVM.DataLayout import Lang.Crucible.LLVM.Extension import Lang.Crucible.LLVM.Bytes import Lang.Crucible.LLVM.Errors.MemoryError (MemErrContext, MemoryErrorReason(..), MemoryOp(..), ppMemoryErrorReason) import qualified Lang.Crucible.LLVM.Errors.MemoryError as ME import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB import Lang.Crucible.LLVM.MemType import Lang.Crucible.LLVM.MemModel.CallStack (CallStack, getCallStack) import qualified Lang.Crucible.LLVM.MemModel.MemLog as ML import Lang.Crucible.LLVM.MemModel.Type import qualified Lang.Crucible.LLVM.MemModel.Partial as Partial import qualified Lang.Crucible.LLVM.MemModel.Generic as G import Lang.Crucible.LLVM.MemModel.Pointer import Lang.Crucible.LLVM.MemModel.Options import Lang.Crucible.LLVM.MemModel.Value import Lang.Crucible.LLVM.Translation.Constant import Lang.Crucible.LLVM.Types import Lang.Crucible.LLVM.Utils import Lang.Crucible.Panic (panic) import GHC.Stack (HasCallStack) ---------------------------------------------------------------------- -- The MemImpl type newtype BlockSource = BlockSource (IORef Natural) type GlobalMap sym = Map L.Symbol (SomePointer sym) nextBlock :: BlockSource -> IO Natural nextBlock (BlockSource ref) = atomicModifyIORef' ref (\n -> (n+1, n)) -- | The implementation of an LLVM memory, containing an -- allocation-block source, global map, handle map, and heap. data MemImpl sym = MemImpl { memImplBlockSource :: BlockSource , memImplGlobalMap :: GlobalMap sym , memImplSymbolMap :: Map Natural L.Symbol -- inverse mapping to 'memImplGlobalMap' , memImplHandleMap :: Map Natural Dynamic , memImplHeap :: G.Mem sym } memEndian :: MemImpl sym -> EndianForm memEndian = G.memEndian . memImplHeap memAllocCount :: MemImpl sym -> Int memAllocCount = G.memAllocCount . memImplHeap memWriteCount :: MemImpl sym -> Int memWriteCount = G.memWriteCount . memImplHeap -- | Produce a fresh empty memory. -- NB, we start counting allocation blocks at '1'. -- Block number 0 is reserved for representing raw bitvectors. emptyMem :: EndianForm -> IO (MemImpl sym) emptyMem endianness = do blkRef <- newIORef 1 return $ MemImpl (BlockSource blkRef) Map.empty Map.empty Map.empty (G.emptyMem endianness) -- | Pretty print a memory state to the given handle. doDumpMem :: IsExprBuilder sym => Handle -> MemImpl sym -> IO () doDumpMem h mem = do hPutStrLn h (show (G.ppMem (memImplHeap mem))) ---------------------------------------------------------------------- -- Memory operations -- -- | Assert that some undefined behavior doesn't occur when performing memory -- model operations assertUndefined :: (IsSymBackend sym bak, Partial.HasLLVMAnn sym) => bak -> CallStack -> Pred sym -> (UB.UndefinedBehavior (RegValue' sym)) {- ^ The undesirable behavior -} -> IO () assertUndefined bak callStack p ub = do let sym = backendGetSym bak p' <- Partial.annotateUB sym callStack ub p assert bak p' $ AssertFailureSimError "Undefined behavior encountered" (show (UB.explain ub)) assertStoreError :: (IsSymBackend sym bak, Partial.HasLLVMAnn sym, 1 <= wptr) => bak -> MemErrContext sym wptr -> MemoryErrorReason -> Pred sym -> IO () assertStoreError bak errCtx rsn p = do let sym = backendGetSym bak p' <- Partial.annotateME sym errCtx rsn p assert bak p' $ AssertFailureSimError "Memory store failed" (show (ppMemoryErrorReason rsn)) instance IsSymInterface sym => IntrinsicClass sym "LLVM_memory" where type Intrinsic sym "LLVM_memory" ctx = MemImpl sym -- NB: Here we are assuming the global maps of both memories are identical. -- This should be the case as memories are only supposed to allocate globals at -- startup, not during program execution. We could check that the maps match, -- but that would be expensive... muxIntrinsic _sym _iTypes _nm _ p mem1 mem2 = do let MemImpl blockSource gMap1 sMap1 hMap1 m1 = mem1 let MemImpl _blockSource _gMap2 _sMap2 hMap2 m2 = mem2 --putStrLn "MEM MERGE" return $ MemImpl blockSource gMap1 sMap1 (Map.union hMap1 hMap2) (G.mergeMem p m1 m2) pushBranchIntrinsic _sym _iTypes _nm _ctx mem = do let MemImpl nxt gMap sMap hMap m = mem --putStrLn "MEM PUSH BRANCH" return $ MemImpl nxt gMap sMap hMap $ G.branchMem m abortBranchIntrinsic _sym _iTypes _nm _ctx mem = do let MemImpl nxt gMap sMap hMap m = mem --putStrLn "MEM ABORT BRANCH" return $ MemImpl nxt gMap sMap hMap $ G.branchAbortMem m -- | Top-level evaluation function for LLVM extension statements. -- LLVM extension statements are used to implement the memory model operations. llvmStatementExec :: (Partial.HasLLVMAnn sym, ?memOpts :: MemOptions) => EvalStmtFunc p sym LLVM llvmStatementExec stmt cst = let simCtx = cst^.stateContext in withBackend simCtx $ \bak -> runStateT (evalStmt bak stmt) cst type EvalM p sym ext rtp blocks ret args a = StateT (CrucibleState p sym ext rtp blocks ret args) IO a -- | Actual workhorse function for evaluating LLVM extension statements. -- The semantics are explicitly organized as a state transformer monad -- that modifies the global state of the simulator; this captures the -- memory accessing effects of these statements. evalStmt :: forall p sym bak ext rtp blocks ret args tp. (IsSymBackend sym bak, Partial.HasLLVMAnn sym, GHC.HasCallStack, ?memOpts :: MemOptions) => bak -> LLVMStmt (RegEntry sym) tp -> EvalM p sym ext rtp blocks ret args (RegValue sym tp) evalStmt bak = eval where sym = backendGetSym bak getMem :: GlobalVar Mem -> EvalM p sym ext rtp blocks ret args (MemImpl sym) getMem mvar = do gs <- use (stateTree.actFrame.gpGlobals) case lookupGlobal mvar gs of Just mem -> return mem Nothing -> panic "MemModel.evalStmt.getMem" [ "Global heap value not initialized." , "*** Global heap variable: " ++ show mvar ] setMem :: GlobalVar Mem -> MemImpl sym -> EvalM p sym ext rtp blocks ret args () setMem mvar mem = stateTree.actFrame.gpGlobals %= insertGlobal mvar mem failedAssert :: String -> String -> EvalM p sym ext rtp blocks ret args a failedAssert msg details = lift $ addFailedAssertion bak $ AssertFailureSimError msg details eval :: LLVMStmt (RegEntry sym) tp -> EvalM p sym ext rtp blocks ret args (RegValue sym tp) eval (LLVM_PushFrame nm mvar) = do mem <- getMem mvar let heap' = G.pushStackFrameMem nm (memImplHeap mem) setMem mvar mem{ memImplHeap = heap' } eval (LLVM_PopFrame mvar) = do mem <- getMem mvar let heap' = G.popStackFrameMem (memImplHeap mem) setMem mvar mem{ memImplHeap = heap' } eval (LLVM_Alloca _w mvar (regValue -> sz) alignment loc) = do mem <- getMem mvar (ptr, mem') <- liftIO $ doAlloca bak mem sz alignment loc setMem mvar mem' return ptr eval (LLVM_Load mvar (regValue -> ptr) tpr valType alignment) = do mem <- getMem mvar liftIO $ doLoad bak mem ptr valType tpr alignment eval (LLVM_MemClear mvar (regValue -> ptr) bytes) = do mem <- getMem mvar z <- liftIO $ bvLit sym knownNat (BV.zero knownNat) len <- liftIO $ bvLit sym PtrWidth (bytesToBV PtrWidth bytes) mem' <- liftIO $ doMemset bak PtrWidth mem ptr z len setMem mvar mem' eval (LLVM_Store mvar (regValue -> ptr) tpr valType alignment (regValue -> val)) = do mem <- getMem mvar mem' <- liftIO $ doStore bak mem ptr tpr valType alignment val setMem mvar mem' eval (LLVM_LoadHandle mvar ltp (regValue -> ptr) args ret) = do mem <- getMem mvar let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr mhandle <- liftIO $ doLookupHandle sym mem ptr let mop = MemLoadHandleOp ltp gsym ptr (memImplHeap mem) let expectedTp = FunctionHandleRepr args ret case mhandle of Left lookupErr -> lift $ do p <- Partial.annotateME sym mop (BadFunctionPointer lookupErr) (falsePred sym) loc <- getCurrentProgramLoc sym let err = SimError loc (AssertFailureSimError "Failed to load function handle" (show (ME.ppFuncLookupError lookupErr))) addProofObligation bak (LabeledPred p err) abortExecBecause (AssertionFailure err) Right (VarargsFnHandle h) -> let err = failedAssert "Failed to load function handle" (unlines ["Expected function handle of type " <> show expectedTp ,"for call to function " <> show (handleName h) ,"but found varargs handle of non-matching type " ++ show (handleType h) ]) in case handleArgTypes h of prefix Ctx.:> VectorRepr AnyRepr | Just Refl <- testEquality ret (handleReturnType h) -> Ctx.dropPrefix args prefix err (return . VarargsFnVal h) _ -> err Right (SomeFnHandle h) | Just Refl <- testEquality (handleType h) expectedTp -> return (HandleFnVal h) | otherwise -> failedAssert "Failed to load function handle" (unlines ["Expected function handle of type " <> show expectedTp , "for call to function " <> show (handleName h) , "but found calling handle of type " ++ show (handleType h)]) eval (LLVM_ResolveGlobal _w mvar (GlobalSymbol symbol)) = do mem <- getMem mvar liftIO $ doResolveGlobal bak mem symbol eval (LLVM_PtrEq mvar (regValue -> x) (regValue -> y)) = do mem <- getMem mvar liftIO $ do v1 <- isValidPointer sym x mem v2 <- isValidPointer sym y mem v3 <- G.notAliasable sym x y (memImplHeap mem) let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) assertUndefined bak callStack v1 $ UB.CompareInvalidPointer UB.Eq (RV x) (RV y) assertUndefined bak callStack v2 $ UB.CompareInvalidPointer UB.Eq (RV x) (RV y) unless (laxConstantEquality ?memOpts) $ do let allocs_doc = G.ppAllocs (G.memAllocs (memImplHeap mem)) let x_doc = G.ppPtr x let y_doc = G.ppPtr y -- TODO: Is this undefined behavior? If so, add to the UB module assert bak v3 $ AssertFailureSimError "Const pointers compared for equality" (unlines [ show x_doc , show y_doc , show allocs_doc ]) ptrEq sym PtrWidth x y eval (LLVM_PtrLe mvar (regValue -> x) (regValue -> y)) = do mem <- getMem mvar liftIO $ do v1 <- isValidPointer sym x mem v2 <- isValidPointer sym y mem let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) assertUndefined bak callStack v1 (UB.CompareInvalidPointer UB.Leq (RV x) (RV y)) assertUndefined bak callStack v2 (UB.CompareInvalidPointer UB.Leq (RV x) (RV y)) (le, valid) <- ptrLe sym PtrWidth x y assertUndefined bak callStack valid (UB.CompareDifferentAllocs (RV x) (RV y)) pure le eval (LLVM_PtrAddOffset _w mvar (regValue -> x) (regValue -> y)) = do mem <- getMem mvar liftIO $ doPtrAddOffset bak mem x y eval (LLVM_PtrSubtract _w mvar (regValue -> x) (regValue -> y)) = do mem <- getMem mvar liftIO $ doPtrSubtract bak mem x y eval LLVM_Debug{} = pure () mkMemVar :: Text -> HandleAllocator -> IO (GlobalVar Mem) mkMemVar memName halloc = freshGlobalVar halloc memName knownRepr -- | For now, the core message should be on the first line, with details -- on further lines. Later we should make it more structured. ptrMessage :: (IsSymInterface sym) => String -> LLVMPtr sym wptr {- ^ pointer involved in message -} -> StorageType {- ^ type of value pointed to -} -> String ptrMessage msg ptr ty = unlines [ msg , " address " ++ show (G.ppPtr ptr) , " at type " ++ show (G.ppType ty) ] -- | Allocate memory on the stack frame of the currently executing function. doAlloca :: ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> MemImpl sym -> SymBV sym wptr {- ^ allocation size -} -> Alignment {- ^ pointer alignment -} -> String {- ^ source location for use in error messages -} -> IO (LLVMPtr sym wptr, MemImpl sym) doAlloca bak mem sz alignment loc = do let sym = backendGetSym bak blkNum <- liftIO $ nextBlock (memImplBlockSource mem) blk <- liftIO $ natLit sym blkNum z <- liftIO $ bvLit sym PtrWidth (BV.zero PtrWidth) let heap' = G.allocMem G.StackAlloc blkNum (Just sz) alignment G.Mutable loc (memImplHeap mem) let ptr = LLVMPointer blk z let mem' = mem{ memImplHeap = heap' } mem'' <- if laxLoadsAndStores ?memOpts && indeterminateLoadBehavior ?memOpts == StableSymbolic then doConstStoreStableSymbolic bak mem' ptr (Just sz) alignment else pure mem' pure (ptr, mem'') -- | Load a 'RegValue' from memory. Both the 'StorageType' and 'TypeRepr' -- arguments should be computed from a single 'MemType' using -- 'toStorableType' and 'Lang.Crucible.LLVM.Translation.Types.llvmTypeAsRepr' -- respectively. -- -- Precondition: the pointer is valid and aligned, and the loaded value is defined. doLoad :: ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> MemImpl sym -> LLVMPtr sym wptr {- ^ pointer to load from -} -> StorageType {- ^ type of value to load -} -> TypeRepr tp {- ^ crucible type of the result -} -> Alignment {- ^ assumed pointer alignment -} -> IO (RegValue sym tp) doLoad bak mem ptr valType tpr alignment = do let sym = backendGetSym bak unpackMemValue sym tpr =<< Partial.assertSafe bak =<< loadRaw sym mem ptr valType alignment -- | Store a 'RegValue' in memory. Both the 'StorageType' and 'TypeRepr' -- arguments should be computed from a single 'MemType' using -- 'toStorableType' and 'Lang.Crucible.LLVM.Translation.Types.llvmTypeAsRepr' -- respectively. -- -- Precondition: the pointer is valid and points to a mutable memory region. doStore :: ( IsSymBackend sym bak , HasPtrWidth wptr , Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> MemImpl sym -> LLVMPtr sym wptr {- ^ pointer to store into -} -> TypeRepr tp -> StorageType {- ^ type of value to store -} -> Alignment -> RegValue sym tp {- ^ value to store -} -> IO (MemImpl sym) doStore bak mem ptr tpr valType alignment val = do --putStrLn "MEM STORE" let sym = backendGetSym bak val' <- packMemValue sym valType tpr val storeRaw bak mem ptr valType alignment val' data SomeFnHandle where SomeFnHandle :: FnHandle args ret -> SomeFnHandle VarargsFnHandle :: FnHandle (args ::> VectorType AnyType) ret -> SomeFnHandle sextendBVTo :: (1 <= w, 1 <= w', IsSymInterface sym) => sym -> NatRepr w -> NatRepr w' -> SymExpr sym (BaseBVType w) -> IO (SymExpr sym (BaseBVType w')) sextendBVTo sym w w' x | Just Refl <- testEquality w w' = return x | Just LeqProof <- testLeq (incNat w) w' = bvSext sym w' x | Just LeqProof <- testLeq (incNat w') w = bvTrunc sym w' x | otherwise = panic "sextendBVTo" [ "Impossible widths!" , show w , show w' ] -- | Allocate and zero a memory region with /size * number/ bytes. -- -- Precondition: the multiplication /size * number/ does not overflow. doCalloc :: ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> MemImpl sym -> SymBV sym wptr {- ^ size -} -> SymBV sym wptr {- ^ number -} -> Alignment {- ^ Minimum alignment of the resulting allocation -} -> IO (LLVMPtr sym wptr, MemImpl sym) doCalloc bak mem sz num alignment = do let sym = backendGetSym bak (ov, sz') <- unsignedWideMultiplyBV sym sz num ov_iszero <- notPred sym =<< bvIsNonzero sym ov -- TODO, this probably shouldn't be UB assert bak ov_iszero (AssertFailureSimError "Multiplication overflow in calloc()" "") loc <- plSourceLoc <$> getCurrentProgramLoc sym let displayString = " " ++ show loc z <- bvLit sym knownNat (BV.zero knownNat) (ptr, mem') <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz' alignment mem'' <- doMemset bak PtrWidth mem' ptr z sz' return (ptr, mem'') -- | Allocate a memory region. doMalloc :: ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> G.AllocType {- ^ stack, heap, or global -} -> G.Mutability {- ^ whether region is read-only -} -> String {- ^ source location for use in error messages -} -> MemImpl sym -> SymBV sym wptr {- ^ allocation size -} -> Alignment -> IO (LLVMPtr sym wptr, MemImpl sym) doMalloc bak allocType mut loc mem sz alignment = doMallocSize (Just sz) bak allocType mut loc mem alignment -- | Allocate a memory region of unbounded size. doMallocUnbounded :: ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> G.AllocType {- ^ stack, heap, or global -} -> G.Mutability {- ^ whether region is read-only -} -> String {- ^ source location for use in error messages -} -> MemImpl sym -> Alignment -> IO (LLVMPtr sym wptr, MemImpl sym) doMallocUnbounded = doMallocSize Nothing doMallocSize :: ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => Maybe (SymBV sym wptr) {- ^ allocation size -} -> bak -> G.AllocType {- ^ stack, heap, or global -} -> G.Mutability {- ^ whether region is read-only -} -> String {- ^ source location for use in error messages -} -> MemImpl sym -> Alignment -> IO (LLVMPtr sym wptr, MemImpl sym) doMallocSize sz bak allocType mut loc mem alignment = do let sym = backendGetSym bak blkNum <- nextBlock (memImplBlockSource mem) blk <- natLit sym blkNum z <- bvLit sym PtrWidth (BV.zero PtrWidth) let heap' = G.allocMem allocType blkNum sz alignment mut loc (memImplHeap mem) let ptr = LLVMPointer blk z let mem' = mem{ memImplHeap = heap' } mem'' <- if laxLoadsAndStores ?memOpts && allocType == G.HeapAlloc && indeterminateLoadBehavior ?memOpts == StableSymbolic then doConstStoreStableSymbolic bak mem' ptr sz alignment else pure mem' return (ptr, mem'') bindLLVMFunPtr :: (IsSymBackend sym bak, HasPtrWidth wptr) => bak -> L.Symbol -> FnHandle args ret -> MemImpl sym -> IO (MemImpl sym) bindLLVMFunPtr bak nm h mem | (_ Ctx.:> VectorRepr AnyRepr) <- handleArgTypes h = do ptr <- doResolveGlobal bak mem nm doInstallHandle bak ptr (VarargsFnHandle h) mem | otherwise = do ptr <- doResolveGlobal bak mem nm doInstallHandle bak ptr (SomeFnHandle h) mem doInstallHandle :: (Typeable a, IsSymBackend sym bak) => bak -> LLVMPtr sym wptr -> a {- ^ handle -} -> MemImpl sym -> IO (MemImpl sym) doInstallHandle _bak ptr x mem = case asNat (llvmPointerBlock ptr) of Just blkNum -> do let hMap' = Map.insert blkNum (toDyn x) (memImplHandleMap mem) return mem{ memImplHandleMap = hMap' } Nothing -> panic "MemModel.doInstallHandle" [ "Attempted to install handle for symbolic pointer" , " " ++ show (ppPtr ptr) ] -- | Allocate a memory region for the given handle. doMallocHandle :: (Typeable a, IsSymInterface sym, HasPtrWidth wptr) => sym -> G.AllocType {- ^ stack, heap, or global -} -> String {- ^ source location for use in error messages -} -> MemImpl sym -> a {- ^ handle -} -> IO (LLVMPtr sym wptr, MemImpl sym) doMallocHandle sym allocType loc mem x = do blkNum <- nextBlock (memImplBlockSource mem) blk <- natLit sym blkNum z <- bvLit sym PtrWidth (BV.zero PtrWidth) let heap' = G.allocMem allocType blkNum (Just z) noAlignment G.Immutable loc (memImplHeap mem) let hMap' = Map.insert blkNum (toDyn x) (memImplHandleMap mem) let ptr = LLVMPointer blk z return (ptr, mem{ memImplHeap = heap', memImplHandleMap = hMap' }) -- | Look up the handle associated with the given pointer, if any. doLookupHandle :: (Typeable a, IsSymInterface sym) => sym -> MemImpl sym -> LLVMPtr sym wptr -> IO (Either ME.FuncLookupError a) doLookupHandle _sym mem ptr = do let LLVMPointer blk _ = ptr case asNat blk of Nothing -> return (Left ME.SymbolicPointer) Just i | i == 0 -> return (Left ME.RawBitvector) | otherwise -> case Map.lookup i (memImplHandleMap mem) of Nothing -> return (Left ME.NoOverride) Just x -> case fromDynamic x of Nothing -> return (Left (ME.Uncallable (dynTypeRep x))) Just a -> return (Right a) -- | Free the memory region pointed to by the given pointer. -- -- Precondition: the pointer either points to the beginning of an allocated -- region, or is null. Freeing a null pointer has no effect. doFree :: (IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym) => bak -> MemImpl sym -> LLVMPtr sym wptr -> IO (MemImpl sym) doFree bak mem ptr = do let sym = backendGetSym bak let LLVMPointer blk _off = ptr loc <- show . plSourceLoc <$> getCurrentProgramLoc sym (heap', p1, p2, notFreed) <- G.freeMem sym PtrWidth ptr (memImplHeap mem) loc -- If this pointer is a handle pointer, remove the associated data let hMap' = case asNat blk of Just i -> Map.delete i (memImplHandleMap mem) Nothing -> memImplHandleMap mem -- NB: free is defined and has no effect if passed a null pointer isNull <- ptrIsNull sym PtrWidth ptr p1' <- orPred sym p1 isNull p2' <- orPred sym p2 isNull notFreed' <- orPred sym notFreed isNull let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) assertUndefined bak callStack p1' (UB.FreeBadOffset (RV ptr)) assertUndefined bak callStack p2' (UB.FreeUnallocated (RV ptr)) assertUndefined bak callStack notFreed' (UB.DoubleFree (RV ptr)) return mem{ memImplHeap = heap', memImplHandleMap = hMap' } -- | Fill a memory range with copies of the specified byte. -- -- Precondition: the memory range falls within a valid allocated region. doMemset :: (1 <= w, IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym) => bak -> NatRepr w -> MemImpl sym -> LLVMPtr sym wptr {- ^ destination -} -> SymBV sym 8 {- ^ fill byte -} -> SymBV sym w {- ^ length -} -> IO (MemImpl sym) doMemset bak w mem dest val len = do let sym = backendGetSym bak len' <- sextendBVTo sym w PtrWidth len (heap', p) <- G.setMem sym PtrWidth dest val len' (memImplHeap mem) let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) assertUndefined bak callStack p $ UB.MemsetInvalidRegion (RV dest) (RV val) (RV len) return mem{ memImplHeap = heap' } doInvalidate :: ( 1 <= w, IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> NatRepr w -> MemImpl sym -> LLVMPtr sym wptr {- ^ destination -} -> Text {- ^ message -} -> SymBV sym w {- ^ length -} -> IO (MemImpl sym) doInvalidate bak w mem dest msg len = do let sym = backendGetSym bak len' <- sextendBVTo sym w PtrWidth len (heap', p) <- if laxLoadsAndStores ?memOpts && indeterminateLoadBehavior ?memOpts == StableSymbolic then do p <- G.isAllocatedMutable sym PtrWidth noAlignment dest (Just len') (memImplHeap mem) mem' <- doStoreStableSymbolic bak 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) p' <- Partial.annotateME sym mop UnwritableRegion p assert bak p' $ AssertFailureSimError "Invalidation of unallocated or readonly region" "" return mem{ memImplHeap = heap' } -- | Store an array in memory. -- -- Precondition: the pointer is valid and points to a mutable memory region. doArrayStore :: (IsSymBackend sym bak, HasPtrWidth w, Partial.HasLLVMAnn sym) => bak -> MemImpl sym -> LLVMPtr sym w {- ^ destination -} -> Alignment -> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8) {- ^ array value -} -> SymBV sym w {- ^ array length -} -> IO (MemImpl sym) doArrayStore bak mem ptr alignment arr len = doArrayStoreSize (Just len) bak mem ptr alignment arr -- | Store an array of unbounded length in memory. -- -- Precondition: the pointer is valid and points to a mutable memory region. doArrayStoreUnbounded :: (IsSymBackend sym bak, HasPtrWidth w, Partial.HasLLVMAnn sym) => bak -> MemImpl sym -> LLVMPtr sym w {- ^ destination -} -> Alignment -> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8) {- ^ array value -} -> IO (MemImpl sym) doArrayStoreUnbounded = doArrayStoreSize Nothing doArrayStoreSize :: (IsSymBackend sym bak, HasPtrWidth w, Partial.HasLLVMAnn sym) => Maybe (SymBV sym w) {- ^ possibly-unbounded array length -} -> bak -> MemImpl sym -> LLVMPtr sym w {- ^ destination -} -> Alignment -> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8) {- ^ array value -} -> IO (MemImpl sym) doArrayStoreSize len bak mem ptr alignment arr = do let sym = backendGetSym bak (heap', p1, p2) <- G.writeArrayMem sym PtrWidth ptr alignment arr len (memImplHeap mem) let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr let mop = MemStoreBytesOp gsym ptr len (memImplHeap mem) assertStoreError bak mop UnwritableRegion p1 let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) assertUndefined bak callStack p2 (UB.WriteBadAlignment (RV ptr) alignment) return mem { memImplHeap = heap' } -- | Store an array in memory. -- -- Precondition: the pointer is valid and points to a mutable or immutable memory region. -- Therefore it can be used to initialize read-only memory regions. doArrayConstStore :: (IsSymBackend sym bak, HasPtrWidth w, Partial.HasLLVMAnn sym) => bak -> MemImpl sym -> LLVMPtr sym w {- ^ destination -} -> Alignment -> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8) {- ^ array value -} -> SymBV sym w {- ^ array length -} -> IO (MemImpl sym) doArrayConstStore bak mem ptr alignment arr len = doArrayConstStoreSize (Just len) bak mem ptr alignment arr -- | Store an array of unbounded length in memory. -- -- Precondition: the pointer is valid and points to a mutable or immutable memory region. -- Therefore it can be used to initialize read-only memory regions. doArrayConstStoreUnbounded :: (IsSymBackend sym bak, HasPtrWidth w, Partial.HasLLVMAnn sym) => bak -> MemImpl sym -> LLVMPtr sym w {- ^ destination -} -> Alignment -> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8) {- ^ array value -} -> IO (MemImpl sym) doArrayConstStoreUnbounded = doArrayConstStoreSize Nothing -- | The workhorse for 'doArrayConstStore' (if the first argument is -- @'Just' len@) or 'doArrayConstStoreUnbounded' (if the first argument is -- 'Nothing'). doArrayConstStoreSize :: (IsSymBackend sym bak, HasPtrWidth w, Partial.HasLLVMAnn sym) => Maybe (SymBV sym w) {- ^ possibly-unbounded array length -} -> bak -> MemImpl sym -> LLVMPtr sym w {- ^ destination -} -> Alignment -> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8) {- ^ array value -} -> IO (MemImpl sym) doArrayConstStoreSize len bak mem ptr alignment arr = do let sym = backendGetSym bak (heap', p1, p2) <- G.writeArrayConstMem sym PtrWidth ptr alignment arr len (memImplHeap mem) let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr let mop = MemStoreBytesOp gsym ptr len (memImplHeap mem) assertStoreError bak mop UnwritableRegion p1 let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) assertUndefined bak callStack p2 (UB.WriteBadAlignment (RV ptr) alignment) return mem { memImplHeap = heap' } -- | Copy memory from source to destination. -- -- Precondition: the source and destination pointers fall within valid allocated -- regions. doMemcpy :: ( 1 <= w, IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> NatRepr w -> MemImpl sym -> Bool {- ^ if true, require disjoint memory regions -} -> LLVMPtr sym wptr {- ^ destination -} -> LLVMPtr sym wptr {- ^ source -} -> SymBV sym w {- ^ length -} -> IO (MemImpl sym) doMemcpy bak w mem mustBeDisjoint dest src len = do let sym = backendGetSym bak len' <- sextendBVTo sym w PtrWidth len (heap', p1, p2) <- G.copyMem sym PtrWidth dest src len' (memImplHeap mem) let gsym_dest = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) dest let gsym_src = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) src let mop = MemCopyOp (gsym_dest, dest) (gsym_src, src) len (memImplHeap mem) p1' <- applyUnless (laxLoadsAndStores ?memOpts) (Partial.annotateME sym mop UnreadableRegion) p1 p2' <- Partial.annotateME sym mop UnwritableRegion p2 assert bak p1' $ AssertFailureSimError "Mem copy failed" "Invalid copy source" assert bak p2' $ AssertFailureSimError "Mem copy failed" "Invalid copy destination" when mustBeDisjoint (assertDisjointRegions bak mop (bvWidth len) dest len src len) return mem{ memImplHeap = heap' } unsymbol :: L.Symbol -> String unsymbol (L.Symbol s) = s -- | Copy memory from source to destination. This version does -- no checks to verify that the source and destination allocations -- are allocated and appropriately sized. uncheckedMemcpy :: (IsSymInterface sym, HasPtrWidth wptr) => sym -> MemImpl sym -> LLVMPtr sym wptr {- ^ destination -} -> LLVMPtr sym wptr {- ^ source -} -> SymBV sym wptr {- ^ length -} -> IO (MemImpl sym) uncheckedMemcpy sym mem dest src len = do (heap', _p1, _p2) <- G.copyMem sym PtrWidth dest src len (memImplHeap mem) return mem{ memImplHeap = heap' } doPtrSubtract :: (IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym) => bak -> MemImpl sym -> LLVMPtr sym wptr -> LLVMPtr sym wptr -> IO (SymBV sym wptr) doPtrSubtract bak mem x y = do let sym = backendGetSym bak (diff, valid) <- ptrDiff sym PtrWidth x y let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) assertUndefined bak callStack valid $ UB.PtrSubDifferentAllocs (RV x) (RV y) pure diff -- | Add an offset to a pointer and asserts that the result is a valid pointer. doPtrAddOffset :: ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> MemImpl sym -> LLVMPtr sym wptr {- ^ base pointer -} -> SymBV sym wptr {- ^ offset -} -> IO (LLVMPtr sym wptr) doPtrAddOffset bak m x@(LLVMPointer blk _) off = do let sym = backendGetSym bak isBV <- natEq sym blk =<< natLit sym 0 x' <- ptrAdd sym PtrWidth x off v <- case asConstantPred isBV of Just True -> return isBV _ -> orPred sym isBV =<< G.isValidPointer sym PtrWidth x' (memImplHeap m) unless (laxLoadsAndStores ?memOpts) $ let callStack = getCallStack (m ^. to memImplHeap . ML.memState) in assertUndefined bak 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 :: (IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym) => bak -> MemImpl sym -> LLVMPtr sym wptr {- ^ destination -} -> Maybe (SymBV sym wptr) {- ^ allocation size -} -> Alignment {- ^ pointer alignment -} -> IO (MemImpl sym) doStoreStableSymbolic bak mem ptr mbSz alignment = do let sym = backendGetSym bak bytes <- freshConstant sym emptySymbol (BaseArrayRepr (Ctx.singleton (BaseBVRepr ?ptrWidth)) (BaseBVRepr (knownNat @8))) case mbSz of Just sz -> doArrayStore bak mem ptr alignment bytes sz Nothing -> doArrayStoreUnbounded bak mem ptr alignment bytes -- | 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'. -- -- Precondition: the pointer is valid and points to a mutable or immutable -- memory region. Therefore it can be used to initialize read-only memory -- regions. doConstStoreStableSymbolic :: (IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym) => bak -> MemImpl sym -> LLVMPtr sym wptr {- ^ destination -} -> Maybe (SymBV sym wptr) {- ^ allocation size -} -> Alignment {- ^ pointer alignment -} -> IO (MemImpl sym) doConstStoreStableSymbolic bak mem ptr mbSz alignment = do let sym = backendGetSym bak bytes <- freshConstant sym emptySymbol (BaseArrayRepr (Ctx.singleton (BaseBVRepr ?ptrWidth)) (BaseBVRepr (knownNat @8))) case mbSz of Just sz -> doArrayConstStore bak mem ptr alignment bytes sz Nothing -> doArrayConstStoreUnbounded bak 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 :: (IsSymInterface sym, HasPtrWidth wptr) => sym -> LLVMPtr sym wptr -> MemImpl sym -> IO (Pred sym) isValidPointer sym p mem = do np <- ptrIsNull sym PtrWidth p case asConstantPred np of Just True -> return np Just False -> G.isValidPointer sym PtrWidth p (memImplHeap mem) _ -> orPred sym np =<< G.isValidPointer sym PtrWidth p (memImplHeap mem) -- | Return the condition required to prove that the pointer points to -- a range of 'size' bytes that falls within an allocated region of -- the appropriate mutability, and also that the pointer is -- sufficiently aligned. isAllocatedAlignedPointer :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> Alignment {- ^ minimum required pointer alignment -} -> G.Mutability {- ^ 'Mutable' means pointed-to region must be writable -} -> LLVMPtr sym w {- ^ pointer -} -> Maybe (SymBV sym w) {- ^ size (@Nothing@ means entire address space) -} -> MemImpl sym {- ^ memory -} -> IO (Pred sym) isAllocatedAlignedPointer sym w alignment mutability ptr size mem = G.isAllocatedAlignedPointer sym w alignment mutability ptr size (memImplHeap mem) -- | Compute the length of a null-terminated string. -- -- The pointer to read from must be concrete and nonnull. The contents -- of the string may be symbolic; HOWEVER, this function will not terminate -- until it eventually reaches a concete null-terminator or a load error. strLen :: ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> MemImpl sym {- ^ memory to read from -} -> LLVMPtr sym wptr {- ^ pointer to string value -} -> IO (SymBV sym wptr) strLen bak mem = go (BV.zero PtrWidth) (truePred sym) where sym = backendGetSym bak go !n cond p = loadRaw sym mem p (bitvectorType 1) noAlignment >>= \case Partial.Err pe -> do ast <- impliesPred sym cond pe assert bak ast $ AssertFailureSimError "Error during memory load: strlen" "" bvLit sym PtrWidth (BV.zero PtrWidth) -- bogus value, but have to return something... Partial.NoErr loadok llvmval -> do ast <- impliesPred sym cond loadok assert bak ast $ AssertFailureSimError "Error during memory load: strlen" "" v <- unpackMemValue sym (LLVMPointerRepr (knownNat @8)) llvmval test <- bvIsNonzero sym =<< Partial.projectLLVM_bv bak v iteM bvIte sym test (do cond' <- andPred sym cond test p' <- doPtrAddOffset bak mem p =<< bvLit sym PtrWidth (BV.one PtrWidth) case BV.succUnsigned PtrWidth n of Just n_1 -> go n_1 cond' p' Nothing -> panic "Lang.Crucible.LLVM.MemModel.strLen" ["string length exceeds pointer width"]) (bvLit sym PtrWidth n) -- | Load a null-terminated string from the memory. -- -- The pointer to read from must be concrete and nonnull. Moreover, -- we require all the characters in the string to be concrete. -- Otherwise it is very difficult to tell when the string has -- terminated. If a maximum number of characters is provided, no more -- than that number of charcters will be read. In either case, -- `loadString` will stop reading if it encounters a null-terminator. loadString :: forall sym bak wptr. ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions, GHC.HasCallStack ) => bak -> MemImpl sym {- ^ memory to read from -} -> LLVMPtr sym wptr {- ^ pointer to string value -} -> Maybe Int {- ^ maximum characters to read -} -> IO [Word8] loadString bak mem = go id where sym = backendGetSym bak go :: ([Word8] -> [Word8]) -> LLVMPtr sym wptr -> Maybe Int -> IO [Word8] go f _ (Just 0) = return $ f [] go f p maxChars = do v <- doLoad bak mem p (bitvectorType 1) (LLVMPointerRepr (knownNat :: NatRepr 8)) noAlignment x <- Partial.projectLLVM_bv bak v case BV.asUnsigned <$> asBV x of Just 0 -> return $ f [] Just c -> do let c' :: Word8 = toEnum $ fromInteger c p' <- doPtrAddOffset bak mem p =<< bvLit sym PtrWidth (BV.one PtrWidth) go (f . (c':)) p' (fmap (\n -> n - 1) maxChars) Nothing -> addFailedAssertion bak $ Unsupported GHC.callStack "Symbolic value encountered when loading a string" -- | Like 'loadString', except the pointer to load may be null. If -- the pointer is null, we return Nothing. Otherwise we load -- the string as with 'loadString' and return it. loadMaybeString :: ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions, GHC.HasCallStack ) => bak -> MemImpl sym {- ^ memory to read from -} -> LLVMPtr sym wptr {- ^ pointer to string value -} -> Maybe Int {- ^ maximum characters to read -} -> IO (Maybe [Word8]) loadMaybeString bak mem ptr n = do let sym = backendGetSym bak isnull <- ptrIsNull sym PtrWidth ptr case asConstantPred isnull of Nothing -> addFailedAssertion bak $ Unsupported GHC.callStack "Symbolic pointer encountered when loading a string" Just True -> return Nothing Just False -> Just <$> loadString bak mem ptr n toStorableType :: (MonadFail m, HasPtrWidth wptr) => MemType -> m StorageType toStorableType mt = case mt of IntType n -> return $ bitvectorType (bitsToBytes n) PtrType _ -> return $ bitvectorType (bitsToBytes (natValue PtrWidth)) PtrOpaqueType -> return $ bitvectorType (bitsToBytes (natValue PtrWidth)) FloatType -> return $ floatType DoubleType -> return $ doubleType X86_FP80Type -> return $ x86_fp80Type ArrayType n x -> arrayType (fromIntegral n) <$> toStorableType x VecType n x -> arrayType (fromIntegral n) <$> toStorableType x MetadataType -> fail "toStorableType: Cannot store metadata values" StructType si -> mkStructType <$> traverse transField (siFields si) where transField :: MonadFail m => FieldInfo -> m (StorageType, Bytes) transField fi = do t <- toStorableType $ fiType fi return (t, fiPadding fi) ---------------------------------------------------------------------- -- "Raw" operations -- -- | Load an LLVM value from memory. Asserts that the pointer is valid and the -- result value is not undefined. loadRaw :: ( IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => sym -> MemImpl sym -> LLVMPtr sym wptr -> StorageType -> Alignment -> IO (Partial.PartLLVMVal sym) loadRaw sym mem ptr valType alignment = do let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr G.readMem sym PtrWidth gsym ptr valType alignment (memImplHeap mem) -- | Store an LLVM value in memory. Asserts that the pointer is valid and points -- to a mutable memory region. storeRaw :: ( IsSymBackend sym bak , HasPtrWidth wptr , Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> MemImpl sym -> LLVMPtr sym wptr {- ^ pointer to store into -} -> StorageType {- ^ type of value to store -} -> Alignment -> LLVMVal sym {- ^ value to store -} -> IO (MemImpl sym) storeRaw bak mem ptr valType alignment val = do let sym = backendGetSym bak let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr (heap', p1, p2) <- G.writeMem sym PtrWidth gsym ptr valType alignment val (memImplHeap mem) let mop = MemStoreOp valType gsym ptr (memImplHeap mem) assertStoreError bak mop UnwritableRegion p1 let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) assertUndefined bak callStack p2 (UB.WriteBadAlignment (RV ptr) alignment) return mem{ memImplHeap = heap' } -- | Perform a memory write operation if the condition is true, -- do not change the memory otherwise. -- -- Asserts that the write operation is valid when cond is true. doConditionalWriteOperation :: (IsSymBackend sym bak) => bak -> MemImpl sym -> Pred sym {- ^ write condition -} -> (MemImpl sym -> IO (MemImpl sym)) {- ^ memory write operation -} -> IO (MemImpl sym) doConditionalWriteOperation bak mem cond write_op = mergeWriteOperations bak mem cond write_op return -- | Merge memory write operations on condition: if the condition is true, -- perform the true branch write operation, otherwise perform the false branch -- write operation. -- -- Asserts that the true branch write operation is valid when cond is true, and -- that the false branch write operation is valid when cond is not true. mergeWriteOperations :: (IsSymBackend sym bak) => bak -> MemImpl sym -> Pred sym {- ^ merge condition -} -> (MemImpl sym -> IO (MemImpl sym)) {- ^ true branch memory write operation -} -> (MemImpl sym -> IO (MemImpl sym)) {- ^ false branch memory write operation -} -> IO (MemImpl sym) mergeWriteOperations bak mem cond true_write_op false_write_op = do let sym = backendGetSym bak let branched_mem = mem { memImplHeap = G.branchMem $ memImplHeap mem } loc <- getCurrentProgramLoc sym true_frame_id <- pushAssumptionFrame bak addAssumption bak (GenericAssumption loc "conditional memory write predicate" cond) true_mutated_heap <- memImplHeap <$> true_write_op branched_mem _ <- popAssumptionFrame bak true_frame_id false_frame_id <- pushAssumptionFrame bak not_cond <- notPred sym cond addAssumption bak (GenericAssumption loc "conditional memory write predicate" not_cond) false_mutated_heap <- memImplHeap <$> false_write_op branched_mem _ <- popAssumptionFrame bak false_frame_id return $! mem { memImplHeap = G.mergeMem cond true_mutated_heap false_mutated_heap } -- | Store an LLVM value in memory if the condition is true, and -- otherwise leaves memory unchanged. -- -- Asserts that the pointer is valid and points to a mutable memory -- region when cond is true. condStoreRaw :: ( IsSymBackend sym bak , HasPtrWidth wptr , Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> MemImpl sym -> Pred sym {- ^ Predicate that determines if we actually write. -} -> LLVMPtr sym wptr {- ^ pointer to store into -} -> StorageType {- ^ type of value to store -} -> Alignment -> LLVMVal sym {- ^ value to store -} -> IO (MemImpl sym) condStoreRaw bak mem cond ptr valType alignment val = do let sym = backendGetSym bak let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr -- Get current heap let preBranchHeap = memImplHeap mem -- Push a branch to the heap let postBranchHeap = G.branchMem preBranchHeap let mop = MemStoreOp valType gsym ptr preBranchHeap -- Write to the heap (postWriteHeap, isAllocated, isAligned) <- G.writeMem sym PtrWidth gsym ptr valType alignment val (memImplHeap mem) -- Assert is allocated if write executes do condIsAllocated <- impliesPred sym cond isAllocated assertStoreError bak mop UnwritableRegion condIsAllocated -- Assert is aligned if write executes do condIsAligned <- impliesPred sym cond isAligned let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) assertUndefined bak callStack condIsAligned (UB.WriteBadAlignment (RV ptr) alignment) -- Merge the write heap and non-write heap let mergedHeap = G.mergeMem cond postWriteHeap postBranchHeap -- Return new memory return $! mem{ memImplHeap = mergedHeap } -- | Store an LLVM value in memory. The pointed-to memory region may -- be either mutable or immutable; thus 'storeConstRaw' can be used to -- initialize read-only memory regions. storeConstRaw :: ( IsSymBackend sym bak , HasPtrWidth wptr , Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> MemImpl sym -> LLVMPtr sym wptr {- ^ pointer to store into -} -> StorageType {- ^ type of value to store -} -> Alignment -> LLVMVal sym {- ^ value to store -} -> IO (MemImpl sym) storeConstRaw bak mem ptr valType alignment val = do let sym = backendGetSym bak let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr (heap', p1, p2) <- G.writeConstMem sym PtrWidth gsym ptr valType alignment val (memImplHeap mem) let mop = MemStoreOp valType gsym ptr (memImplHeap mem) assertStoreError bak mop UnwritableRegion p1 let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) assertUndefined bak callStack p2 (UB.WriteBadAlignment (RV ptr) alignment) return mem{ memImplHeap = heap' } -- | Allocate a memory region on the heap, with no source location info. mallocRaw :: ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> MemImpl sym -> SymBV sym wptr {- ^ size in bytes -} -> Alignment -> IO (LLVMPtr sym wptr, MemImpl sym) mallocRaw bak mem sz alignment = doMalloc bak G.HeapAlloc G.Mutable "" mem sz alignment -- | Allocate a read-only memory region on the heap, with no source location info. mallocConstRaw :: ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> MemImpl sym -> SymBV sym wptr -> Alignment -> IO (LLVMPtr sym wptr, MemImpl sym) mallocConstRaw bak mem sz alignment = doMalloc bak G.HeapAlloc G.Immutable "" mem sz alignment ---------------------------------------------------------------------- -- Packing and unpacking -- unpackZero :: (HasCallStack, IsSymInterface sym) => sym -> StorageType -> TypeRepr tp {- ^ Crucible type -} -> IO (RegValue sym tp) unpackZero sym tp tpr = let mismatch = storageTypeMismatch "MemModel.unpackZero" tp tpr in case storageTypeF tp of Bitvector bytes -> zeroInt sym bytes $ \case Nothing -> fail ("Improper storable type: " ++ show tp) Just (blk, bv) -> case tpr of LLVMPointerRepr w | Just Refl <- testEquality (bvWidth bv) w -> return (LLVMPointer blk bv) _ -> mismatch Float -> case tpr of FloatRepr SingleFloatRepr -> iFloatLitRational sym SingleFloatRepr 0 _ -> mismatch Double -> case tpr of FloatRepr DoubleFloatRepr -> iFloatLitRational sym DoubleFloatRepr 0 _ -> mismatch X86_FP80 -> case tpr of FloatRepr X86_80FloatRepr -> iFloatLitRational sym X86_80FloatRepr 0 _ -> mismatch Array n tp' -> case tpr of VectorRepr tpr' -> do v <- unpackZero sym tp' tpr' return $ V.replicate (fromIntegral n) v _ -> mismatch Struct flds -> case tpr of StructRepr fldCtx | V.length flds == Ctx.sizeInt (Ctx.size fldCtx) -> Ctx.traverseWithIndex (\i tpr' -> RV <$> unpackZero sym (flds V.! (Ctx.indexVal i) ^. fieldVal) tpr') fldCtx _ -> mismatch storageTypeMismatch :: String -> StorageType -> TypeRepr tp -> IO a storageTypeMismatch nm tp tpr = panic nm [ "Storage type mismatch in " ++ nm , " Storage type: " ++ show tp , " Crucible type: " ++ show tpr ] -- | Unpack an 'LLVMVal' to produce a 'RegValue'. unpackMemValue :: (HasCallStack, IsSymInterface sym) => sym -> TypeRepr tp -> LLVMVal sym -> IO (RegValue sym tp) unpackMemValue sym tpr (LLVMValZero tp) = unpackZero sym tp tpr unpackMemValue _sym (LLVMPointerRepr w) (LLVMValInt blk bv) | Just Refl <- testEquality (bvWidth bv) w = return $ LLVMPointer blk bv unpackMemValue _ (FloatRepr SingleFloatRepr) (LLVMValFloat SingleSize x) = return x unpackMemValue _ (FloatRepr DoubleFloatRepr) (LLVMValFloat DoubleSize x) = return x unpackMemValue _ (FloatRepr X86_80FloatRepr) (LLVMValFloat X86_FP80Size x) = return x unpackMemValue sym (StructRepr ctx) (LLVMValStruct xs) | V.length xs == Ctx.sizeInt (Ctx.size ctx) = Ctx.traverseWithIndex (\i tpr -> RV <$> unpackMemValue sym tpr (xs V.! Ctx.indexVal i ^. _2)) ctx unpackMemValue sym (VectorRepr tpr) (LLVMValArray _tp xs) = traverse (unpackMemValue sym tpr) xs unpackMemValue _sym ctp@(BVRepr _) lval@(LLVMValInt _ _) = panic "MemModel.unpackMemValue" [ "Cannot unpack an integer LLVM value to a crucible bitvector type" , "*** Crucible type: " ++ show ctp , "*** LLVM value: " ++ show lval ] unpackMemValue _ tpr v@(LLVMValUndef _) = panic "MemModel.unpackMemValue" [ "Cannot unpack an `undef` value" , "*** Crucible type: " ++ show tpr , "*** Undef value: " ++ show v ] unpackMemValue _ tpr v = panic "MemModel.unpackMemValue" [ "Crucible type mismatch when unpacking LLVM value" , "*** Crucible type: " ++ show tpr , "*** LLVM value: " ++ show v ] -- | Pack a 'RegValue' into an 'LLVMVal'. The LLVM storage type and -- the Crucible type must be compatible. packMemValue :: IsSymInterface sym => sym -> StorageType {- ^ LLVM storage type -} -> TypeRepr tp {- ^ Crucible type -} -> RegValue sym tp -> IO (LLVMVal sym) packMemValue _ (StorageType Float _) (FloatRepr SingleFloatRepr) x = return $ LLVMValFloat SingleSize x packMemValue _ (StorageType Double _) (FloatRepr DoubleFloatRepr) x = return $ LLVMValFloat DoubleSize x packMemValue _ (StorageType X86_FP80 _) (FloatRepr X86_80FloatRepr) x = return $ LLVMValFloat X86_FP80Size x packMemValue sym (StorageType (Bitvector bytes) _) (BVRepr w) bv | bitsToBytes (natValue w) == bytes = do blk0 <- natLit sym 0 return $ LLVMValInt blk0 bv packMemValue _sym (StorageType (Bitvector bytes) _) (LLVMPointerRepr w) (LLVMPointer blk off) | bitsToBytes (natValue w) == bytes = return $ LLVMValInt blk off packMemValue sym (StorageType (Array sz tp) _) (VectorRepr tpr) vec | V.length vec == fromIntegral sz = do vec' <- traverse (packMemValue sym tp tpr) vec return $ LLVMValArray tp vec' packMemValue sym (StorageType (Struct fls) _) (StructRepr ctx) xs = do fls' <- V.generateM (V.length fls) $ \i -> do let fl = fls V.! i case Ctx.intIndex i (Ctx.size ctx) of Just (Some idx) -> do let tpr = ctx Ctx.! idx let RV val = xs Ctx.! idx val' <- packMemValue sym (fl^.fieldVal) tpr val return (fl, val') _ -> panic "MemModel.packMemValue" [ "Mismatch between LLVM and Crucible types" , "*** Filed out of bounds: " ++ show i ] return $ LLVMValStruct fls' packMemValue _ stTy crTy _ = panic "MemModel.packMemValue" [ "Type mismatch when storing value." , "*** Expected storable type: " ++ show stTy , "*** Given crucible type: " ++ show crTy ] ---------------------------------------------------------------------- -- Disjointness -- -- | Assert that two memory regions are disjoint. -- Two memory regions are disjoint if any of the following are true: -- -- 1. Their block pointers are different -- 2. Their blocks are the same, but /dest+dlen/ <= /src/ -- 3. Their blocks are the same, but /src+slen/ <= /dest/ assertDisjointRegions :: (1 <= w, HasPtrWidth wptr, IsSymBackend sym bak, Partial.HasLLVMAnn sym) => bak -> MemoryOp sym wptr -> NatRepr w -> LLVMPtr sym wptr {- ^ pointer to region 1 -} -> SymBV sym w {- ^ length of region 1 -} -> LLVMPtr sym wptr {- ^ pointer to region 2 -} -> SymBV sym w {- ^ length of region 2 -} -> IO () assertDisjointRegions bak mop w dest dlen src slen = do let sym = backendGetSym bak c <- buildDisjointRegionsAssertion sym w dest dlen src slen c' <- Partial.annotateME sym mop OverlappingRegions c assert bak c' (AssertFailureSimError "Memory regions not disjoint" "") buildDisjointRegionsAssertion :: (1 <= w, HasPtrWidth wptr, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym wptr {- ^ pointer to region 1 -} -> SymBV sym w {- ^ length of region 1 -} -> LLVMPtr sym wptr {- ^ pointer to region 2 -} -> SymBV sym w {- ^ length of region 2 -} -> IO (Pred sym) buildDisjointRegionsAssertion sym w dest dlen src slen = do let LLVMPointer dblk doff = dest let LLVMPointer sblk soff = src dend <- bvAdd sym doff =<< sextendBVTo sym w PtrWidth dlen send <- bvAdd sym soff =<< sextendBVTo sym w PtrWidth slen diffBlk <- notPred sym =<< natEq sym dblk sblk destfirst <- bvSle sym dend soff srcfirst <- bvSle sym send doff orPred sym diffBlk =<< orPred sym destfirst srcfirst -- | Build the condition that two memory regions are disjoint, using -- subtraction and comparison to zero instead of direct comparison (that is, -- 0 <= y - x instead of x <= y). This enables semiring and abstract domain -- simplifications. The result if false if any offset is not positive when -- interpreted as signed bitvector. buildDisjointRegionsAssertionWithSub :: (HasPtrWidth wptr, IsSymInterface sym) => sym -> LLVMPtr sym wptr {- ^ pointer to region 1 -} -> SymBV sym wptr {- ^ length of region 1 -} -> LLVMPtr sym wptr {- ^ pointer to region 2 -} -> SymBV sym wptr {- ^ length of region 2 -} -> IO (Pred sym) buildDisjointRegionsAssertionWithSub sym dest dlen src slen = do let LLVMPointer dblk doff = dest let LLVMPointer sblk soff = src dend <- bvAdd sym doff dlen send <- bvAdd sym soff slen zero_bv <- bvLit sym PtrWidth $ BV.zero PtrWidth diffBlk <- notPred sym =<< natEq sym dblk sblk allPos <- andAllOf sym folded =<< mapM (bvSle sym zero_bv) [doff, dend, soff, send] destfirst <- bvSle sym zero_bv =<< bvSub sym soff dend srcfirst <- bvSle sym zero_bv =<< bvSub sym doff send orPred sym diffBlk =<< andPred sym allPos =<< orPred sym destfirst srcfirst ---------------------------------------------------------------------- -- constToLLVMVal -- -- | This is used (by saw-script) to initialize globals. -- -- In this translation, we lose the distinction between pointers and ints. -- -- This is parameterized (hence, \"P\") over a function for looking up the -- pointer values of global symbols. This parameter is used by @populateGlobal@ -- to recursively populate globals that may reference one another. constToLLVMValP :: forall wptr sym io. ( MonadIO io , MonadFail io , HasPtrWidth wptr , IsSymInterface sym , HasCallStack ) => sym -- ^ The symbolic backend -> (L.Symbol -> io (LLVMPtr sym wptr)) -- ^ How to look up global symbols -> LLVMConst -- ^ Constant expression to translate -> io (LLVMVal sym) -- See comment on @LLVMVal@ on why we use a literal 0. constToLLVMValP sym _ (IntConst w i) = liftIO $ LLVMValInt <$> natLit sym 0 <*> bvLit sym w i constToLLVMValP sym _ (FloatConst f) = liftIO $ LLVMValFloat SingleSize <$> iFloatLitSingle sym f constToLLVMValP sym _ (DoubleConst d) = liftIO $ LLVMValFloat DoubleSize <$> iFloatLitDouble sym d constToLLVMValP sym _ (LongDoubleConst (L.FP80_LongDouble e s)) = liftIO $ LLVMValFloat X86_FP80Size <$> iFloatLitLongDouble sym (X86_80Val e s) constToLLVMValP _ _ (StringConst bs) = pure (LLVMValString bs) constToLLVMValP sym look (ArrayConst memty xs) = LLVMValArray <$> liftIO (toStorableType memty) <*> (V.fromList <$> traverse (constToLLVMValP sym look) xs) -- Same as the array case constToLLVMValP sym look (VectorConst memty xs) = LLVMValArray <$> liftIO (toStorableType memty) <*> (V.fromList <$> traverse (constToLLVMValP sym look) xs) constToLLVMValP sym look (StructConst sInfo xs) = LLVMValStruct <$> V.zipWithM (\x y -> (,) <$> liftIO (fiToFT x) <*> constToLLVMValP sym look y) (siFields sInfo) (V.fromList xs) -- SymbolConsts are offsets from global pointers. We translate them into the -- pointer they represent. constToLLVMValP sym look (SymbolConst symb i) = do -- Pointer to the global "symb" ptr <- look symb -- Offset to be added, as a bitvector ibv <- liftIO $ bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth i) -- blk is the allocation number that this global is stored in. -- In contrast to the case for @IntConst@ above, it is non-zero. let (blk, offset) = llvmPointerView ptr LLVMValInt blk <$> liftIO (bvAdd sym offset ibv) constToLLVMValP _sym _look (ZeroConst memty) = liftIO $ LLVMValZero <$> toStorableType memty constToLLVMValP _sym _look (UndefConst memty) = liftIO $ LLVMValUndef <$> toStorableType memty -- | Translate a constant into an LLVM runtime value. Assumes all necessary -- globals have already been populated into the @'MemImpl'@. constToLLVMVal :: forall wptr sym bak io. ( MonadIO io , MonadFail io , HasPtrWidth wptr , IsSymBackend sym bak , HasCallStack ) => bak -- ^ The symbolic backend -> MemImpl sym -- ^ The current memory state, for looking up globals -> LLVMConst -- ^ Constant expression to translate -> io (LLVMVal sym) -- ^ Runtime representation of the constant expression -- See comment on @LLVMVal@ on why we use a literal 0. constToLLVMVal bak mem = constToLLVMValP (backendGetSym bak) (\symb -> liftIO $ doResolveGlobal bak mem symb) -- TODO are these types just identical? Maybe we should combine them. fiToFT :: (HasPtrWidth wptr, MonadFail m) => FieldInfo -> m (Field StorageType) fiToFT fi = fmap (\t -> mkField (fiOffset fi) t (fiPadding fi)) (toStorableType $ fiType fi) ---------------------------------------------------------------------- -- Globals -- -- | Look up a 'Symbol' in the global map of the given 'MemImpl'. -- Panic if the symbol is not present in the global map. doResolveGlobal :: (IsSymBackend sym bak, HasPtrWidth wptr, HasCallStack) => bak -> MemImpl sym -> L.Symbol {- ^ name of global -} -> IO (LLVMPtr sym wptr) doResolveGlobal bak mem symbol@(L.Symbol name) = let lookedUp = Map.lookup symbol (memImplGlobalMap mem) msg1 = "Global allocation has incorrect width" msg1Details = mconcat [ "Allocation associated with global symbol \"" , name , "\" is not a pointer of the correct width" ] msg2 = "Global symbol not allocated" msg2Details = mconcat [ "Global symbol \"" , name , "\" has no associated allocation" ] in case lookedUp of Just (SomePointer ptr) | PtrWidth <- ptrWidth ptr -> return ptr _ -> addFailedAssertion bak $ if isJust lookedUp then AssertFailureSimError msg1 msg1Details else AssertFailureSimError msg2 msg2Details -- | Add an entry to the global map of the given 'MemImpl'. -- -- This takes a list of symbols because there may be aliases to a global. registerGlobal :: (IsExprBuilder sym, 1 <= wptr) => MemImpl sym -> [L.Symbol] -> LLVMPtr sym wptr -> MemImpl sym registerGlobal (MemImpl blockSource gMap sMap hMap mem) symbols ptr = MemImpl blockSource gMap' sMap' hMap mem where gMap' = foldr (\s m -> Map.insert s (SomePointer ptr) m) gMap symbols sMap' = fromMaybe sMap $ do symbol <- listToMaybe symbols n <- asNat (llvmPointerBlock ptr) z <- asBV (llvmPointerOffset ptr) guard (BV.asUnsigned z == 0) Just (Map.insert n symbol sMap) -- | Allocate memory for each global, and register all the resulting -- pointers in the global map. allocGlobals :: ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> [(L.Global, [L.Symbol], Bytes, Alignment)] -> MemImpl sym -> IO (MemImpl sym) allocGlobals bak gs mem = foldM (allocGlobal bak) mem gs allocGlobal :: ( IsSymBackend sym bak, HasPtrWidth wptr, Partial.HasLLVMAnn sym , ?memOpts :: MemOptions ) => bak -> MemImpl sym -> (L.Global, [L.Symbol], Bytes, Alignment) -> IO (MemImpl sym) allocGlobal bak mem (g, aliases, sz, alignment) = do let sym = backendGetSym bak let symbol@(L.Symbol sym_str) = L.globalSym g let displayName = "[global variable ] " ++ sym_str let mut = if L.gaConstant (L.globalAttrs g) then G.Immutable else G.Mutable sz' <- bvLit sym PtrWidth (bytesToBV PtrWidth sz) -- TODO: Aliases are not propagated to doMalloc for error messages (ptr, mem') <- doMalloc bak G.GlobalAlloc mut displayName mem sz' alignment return (registerGlobal mem' (symbol:aliases) ptr) concSomePointer :: IsSymInterface sym => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> SomePointer sym -> IO (SomePointer sym) concSomePointer sym conc (SomePointer ptr) = SomePointer <$> ML.concPtr sym conc ptr concMemImpl :: IsSymInterface sym => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> MemImpl sym -> IO (MemImpl sym) concMemImpl sym conc mem = do heap' <- ML.concMem sym conc (memImplHeap mem) gm' <- traverse (concSomePointer sym conc) (memImplGlobalMap mem) pure mem{ memImplHeap = heap', memImplGlobalMap = gm' }