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.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
  , 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 doStoreStableSymbolic 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) =>
  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 = "<calloc> " ++ 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
                && mut == G.Mutable
                && allocType == G.HeapAlloc
                && indeterminateLoadBehavior ?memOpts == StableSymbolic
           then doStoreStableSymbolic bak mem' ptr sz alignment
           else pure mem'
  return (ptr, mem'')



bindLLVMFunPtr ::
  (IsSymBackend sym bak, HasPtrWidth wptr) =>
  bak ->
  L.Declare ->
  FnHandle args ret ->
  MemImpl sym ->
  IO (MemImpl sym)
bindLLVMFunPtr bak dec h mem
  | L.decVarArgs dec
  , (_ Ctx.:> VectorRepr AnyRepr) <- handleArgTypes h

  = do ptr <- doResolveGlobal bak mem (L.decName dec)
       doInstallHandle bak ptr (VarargsFnHandle h) mem

  | otherwise
  = do ptr <- doResolveGlobal bak mem (L.decName dec)
       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 = do
  let sym = backendGetSym bak
  (heap', p1, p2) <-
    G.writeArrayConstMem sym PtrWidth ptr alignment arr (Just len) (memImplHeap mem)

  let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr
  let mop = MemStoreBytesOp gsym ptr (Just 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

-- | 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))
    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)
  => 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)
  => 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)
  => 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 =<< 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' }