crucible-llvm-0.7: src/Lang/Crucible/LLVM/MemModel.hs
--------------------------------------------------------------------
-- |
-- 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 <rdockins@galois.com>
-- 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.ptrToBv
, Partial.projectLLVM_bv
-- * Memory operations
, doMalloc
, doMallocUnbounded
, G.AllocType(..)
, G.Mutability(..)
, ME.FuncLookupError(..)
, ME.ppFuncLookupError
, doLookupHandle
, doInstallHandle
, doMemcpy
, doMemset
, doInvalidate
, doCalloc
, doFree
, doAlloca
, doLoad
, doStore
, doArrayStore
, doArrayStoreUnbounded
, doArrayConstStore
, doArrayConstStoreUnbounded
, loadString
, loadMaybeString
, strLen
, uncheckedMemcpy
-- * \"Raw\" operations with LLVMVal
, LLVMVal(..)
, ppLLVMValWithGlobals
, FloatSize(..)
, unpackMemValue
, packMemValue
, loadRaw
, loadArrayConcreteSizeRaw
, 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
, G.asMemMatchingArrayStore
, 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 qualified What4.Expr.ArrayUpdateMap as AUM
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 $ bvZero sym 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 $ bvZero sym 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
-- | 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 = "<calloc> " ++ show loc
z <- bvZero sym 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 <- bvZero sym 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'')
-- | Associate a function handle with an existing allocation.
--
-- This can overwrite existing allocation/handle associations, and is used to do
-- so when registering lazily-translated CFGs.
--
-- See also "Lang.Crucible.LLVM.Functions".
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)
]
-- | 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 off = do
let sym = backendGetSym bak
isBV <- ptrIsBv sym x
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" ""
bvZero sym 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
let err = AssertFailureSimError "Found pointer instead of byte in string passed to `strlen`" ""
test <- bvIsNonzero sym =<< Partial.ptrToBv bak err v
iteM bvIte sym
test
(do cond' <- andPred sym cond test
p' <- doPtrAddOffset bak mem p =<< bvOne sym 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
let err = AssertFailureSimError "Found pointer instead of byte when loading string" ""
x <- Partial.ptrToBv bak err 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 =<< bvOne sym 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)
-- | Load an array with concrete size from memory.
loadArrayConcreteSizeRaw ::
forall sym wptr .
(IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym, ?memOpts :: MemOptions) =>
sym ->
MemImpl sym ->
LLVMPtr sym wptr ->
Natural ->
Alignment ->
IO (Either (Pred sym) (Pred sym, SymArray sym (SingleCtx (BaseBVType wptr)) (BaseBVType 8)))
loadArrayConcreteSizeRaw sym mem ptr sz alignment
| sz == 0 = do
zero_bv <- bvZero sym knownNat
zero_arr <- constantArray sym (Ctx.singleton $ BaseBVRepr PtrWidth) zero_bv
return $ Right (truePred sym, zero_arr)
| otherwise = do
let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr
res <- G.readMem sym PtrWidth gsym ptr (arrayType sz $ bitvectorType 1) alignment (memImplHeap mem)
case res of
Partial.NoErr ok llvm_val_arr -> do
case llvm_val_arr of
LLVMValArray _ llvm_vals -> do
let aum = AUM.fromAscList knownRepr $ V.toList $ V.imap
(\i -> \case
LLVMValInt _ byte | Just Refl <- testEquality (knownNat @8) (bvWidth byte) ->
(Ctx.singleton $ BVIndexLit PtrWidth $ BV.mkBV PtrWidth $ fromIntegral i, byte)
_ -> panic "MemModel.loadArrayRaw" ["expected LLVMValInt"])
llvm_vals
zero_bv <- bvZero sym knownNat
arr <- arrayFromMap sym (Ctx.singleton $ BaseBVRepr PtrWidth) aum zero_bv
return $ Right (ok, arr)
_ -> panic "MemModel.loadArrayRaw" ["expected LLVMValArray"]
Partial.Err err -> return $ Left err
-- | 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 "<malloc>" 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 "<malloc>" 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 =<< ptrSameAlloc sym dest src
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 <- bvZero sym PtrWidth
diffBlk <- notPred sym =<< ptrSameAlloc sym dest src
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' }