Merge branch 'master' of github.com:GaloisInc/macaw

base/src/Data/Macaw/Dwarf.hs

@@ -817,8 +817,21 @@ parseVariable :: V.Vector FilePath
               -> Map DieID Type
               -> DIE
               -> Parser Variable
-parseVariable file_vec typeMap d = runDIEParser "parseVariable" d $ do
+parseVariable = parseVariableOrParameter DW_TAG_variable
-  checkTag DW_TAG_variable
+
+parseParameter :: V.Vector FilePath
+               -> Map DieID Type
+               -> DIE
+               -> Parser Variable
+parseParameter = parseVariableOrParameter DW_TAG_formal_parameter
+
+parseVariableOrParameter :: Dwarf.DW_TAG
+                         -> V.Vector FilePath
+                         -> Map DieID Type
+                         -> DIE
+                         -> Parser Variable
+parseVariableOrParameter tag file_vec typeMap d = runDIEParser "parseVariable" d $ do
+  checkTag tag
 
   mloc       <- getMaybeAttribute DW_AT_location $ \case
                   DW_ATVAL_BLOB b -> ComputedLoc <$> parseDwarfExpr b
@@ -911,6 +924,8 @@ data Subprogram = Subprogram { subExternal   :: !Bool
                              , subPrototyped :: !Bool
                              , subDef        :: !(Maybe SubprogramDef)
                              , subVars :: !(Map DieID Variable)
+                             , subParams :: !(Map DieID Variable)
+                             , subRetType :: !(Maybe Type)
                              }
 
 
@@ -923,6 +938,8 @@ instance Pretty Subprogram where
          , text "prototyped: " <+> text (show (subPrototyped sub))
          , maybe (text "") pretty (subDef sub)
          , ppList "variables" (pretty <$> Map.elems (subVars sub))
+         , ppList "parameters" (pretty <$> Map.elems (subParams sub))
+         , text "return type: " <+> text (show (subRetType sub))
          ]
 
 instance Show Subprogram where
@@ -963,6 +980,10 @@ parseSubprogram file_vec typeMap d = runDIEParser "parseSubprogram" d $ do
   typeMap' <- Map.union typeMap <$> parseTypeMap file_vec
 
   vars <- parseChildrenList DW_TAG_variable (parseVariable file_vec typeMap')
+  params <- parseChildrenList DW_TAG_formal_parameter $
+    parseParameter file_vec typeMap'
+  retType <- getMaybeAttribute DW_AT_type $
+    parseType typeMap' <=< attributeAsDieID
 
   ignoreAttribute DW_AT_GNU_all_tail_call_sites
   ignoreAttribute DW_AT_sibling
@@ -979,6 +1000,8 @@ parseSubprogram file_vec typeMap d = runDIEParser "parseSubprogram" d $ do
                   , subPrototyped = fromMaybe False prototyped
                   , subDef        = def
                   , subVars       = Map.fromList [ (varDieID v, v) | v <- vars ]
+                  , subParams     = Map.fromList [ (varDieID p, p) | p <- params ]
+                  , subRetType    = retType
                   }
 
 ------------------------------------------------------------------------

base/src/Data/Macaw/SCFG.hs

@@ -43,28 +43,28 @@ newtype BlockIndex = BlockIndex Word64
 newtype AssignId ids (tp::Type) = AssignId (Nonce ids tp)
 
 data Value arch ids tp where
+  -- | A constant bitvector
+  --
+  -- The integer should be between 0 and 2^n-1.
   BVValue :: (1 <= n)
           => !(NatRepr n)
           -> !Integer
           -> Value arch ids (BVType n)
-  -- ^ A constant bitvector
+  -- | A constant Boolean
-  --
-  -- The integer should be between 0 and 2^n-1.
   BoolValue :: !Bool -> Value arch ids BoolType
-  -- ^ A constant Boolean
+  -- | A memory address
   RelocatableValue :: !(AddrWidthRepr (ArchAddrWidth arch))
                    -> !(ArchMemAddr arch)
                    -> Value arch ids (BVType (ArchAddrWidth arch))
-  -- ^ A memory address
+  -- | Reference to a symbol identifier.
+  --
+  -- This appears when dealing with relocations.
   SymbolValue :: !(AddrWidthRepr (ArchAddrWidth arch))
               -> !SymbolIdentifier
               -> Value arch ids (BVType (ArchAddrWidth arch))
-  -- ^ Reference to a symbol identifier.
+  -- | Value from an assignment statement.
-  --
-  -- This appears when dealing with relocations.
   AssignedValue :: !(AssignId ids tp)
                 -> Value arch ids tp
-  -- ^ Value from an assignment statement.
 
 type BVValue arch ids w = Value arch ids (BVType w)
 
@@ -75,26 +75,26 @@ data Stmt arch ids where
   AssignStmt :: !(AssignId ids tp)
              -> !(AssignRhs arch (Value arch ids) tp)
              -> Stmt arch ids
+  -- | This denotes a write to memory, and consists of an address to write to, a `MemRepr` defining
+  -- how the value should be stored in memory, and the value to be written.
   WriteMem :: !(ArchAddrValue arch ids)
            -> !(MemRepr tp)
            -> !(Value arch ids tp)
            -> Stmt arch ids
-  -- ^ This denotes a write to memory, and consists of an address to write to, a `MemRepr` defining
+  -- | The start of an instruction
-  -- how the value should be stored in memory, and the value to be written.
-  InstructionStart :: !(ArchAddrWord arch)
-                   -> !Text
-                   -> Stmt arch ids
-  -- ^ The start of an instruction
   --
   -- The information includes the offset relative to the start of the block and the
   -- disassembler output if available (or empty string if unavailable)
+  InstructionStart :: !(ArchAddrWord arch)
+                   -> !Text
+                   -> Stmt arch ids
+  -- | A user-level comment
   Comment :: !Text -> Stmt arch ids
-  -- ^ A user-level comment
+  -- | Execute an architecture specific statement
   ExecArchStmt :: !(ArchStmt arch (Value arch ids)) -> Stmt arch ids
-  -- ^ Execute an architecture specific statement
+  -- /\ A call statement.
   --  RegCall :: !(RegState (ArchReg arch) (Value arch ids))
   --          -> Stmt arch ids
-  -- ^ A call statement.
 
 -- | This is a calling convention that explains how the linear list of
 -- arguments should be stored for the ABI.
@@ -104,39 +104,39 @@ type family CallingConvention arch
 -- of how block ending with a a FetchAndExecute statement should be
 -- interpreted.
 data TermStmt arch ids where
+  -- | A call with the current register values and location to return to or 'Nothing'  if this is a tail call.
   TailCall :: !(CallingConvention arch)
            -> !(BVValue arch ids (ArchAddrWidth arch))
               -- /\ IP to call
            -> ![Some (Value arch ids)]
            -> TermStmt arch ids
-  -- ^ A call with the current register values and location to return to or 'Nothing'  if this is a tail call.
+  -- | A jump to an explicit address within a function.
   Jump :: !BlockIndex
        -> TermStmt arch ids
-  -- ^ A jump to an explicit address within a function.
+  -- | A lookup table that branches to one of a vector of addresses.
-  LookupTable :: !(BVValue arch ids (ArchAddrWidth arch))
-              -> !(V.Vector BlockIndex)
-              -> TermStmt arch ids
-  -- ^ A lookup table that branches to one of a vector of addresses.
   --
   -- The value contains the index to jump to as an unsigned bitvector, and the
   -- possible addresses as a table.  If the index (when interpreted as
   -- an unsigned number) is larger than the number of entries in the vector, then the
   -- result is undefined.
+  LookupTable :: !(BVValue arch ids (ArchAddrWidth arch))
+              -> !(V.Vector BlockIndex)
+              -> TermStmt arch ids
+  -- | A return with the given registers.
   Return :: !(MapF (ArchReg arch) (Value arch ids))
          -> TermStmt arch ids
-  -- ^ A return with the given registers.
+  -- | An if-then-else
   Ite :: !(Value arch ids BoolType)
       -> !BlockIndex
       -> !BlockIndex
       -> TermStmt arch ids
-  -- ^ An if-then-else
+  -- | An architecture-specific statement with the registers prior to execution, and
+  -- the given next control flow address.
   ArchTermStmt :: !(ArchTermStmt arch ids)
                -> !(MapF (ArchReg arch) (Value arch ids))
                -> !(MapF (ArchReg arch) (Value arch ids))
                -> !(Maybe BlockIndex)
                -> TermStmt arch ids
-  -- ^ An architecture-specific statement with the registers prior to execution, and
-  -- the given next control flow address.
 
 
 data SCFGBlock arch ids

symbolic/src/Data/Macaw/Symbolic.hs

@@ -36,7 +36,7 @@ module Data.Macaw.Symbolic
   , Data.Macaw.Symbolic.CrucGen.MacawArchConstraints
   , MacawArchEvalFn
   , EvalStmtFunc
-  , LookupFunctionHandle
+  , LookupFunctionHandle(..)
   , Regs
   , freshValue
   , GlobalMap
@@ -84,7 +84,6 @@ import           Data.Macaw.Symbolic.CrucGen
 import           Data.Macaw.Symbolic.PersistentState
 import           Data.Macaw.Symbolic.MemOps
 
-data MacawSimulatorState sym = MacawSimulatorState
 
 {-
 mkMemSegmentBinding :: (1 <= w)
@@ -391,21 +390,16 @@ type EvalStmtFunc f p sym ext =
 type MacawArchEvalFn sym arch =
   EvalStmtFunc (MacawArchStmtExtension arch) (MacawSimulatorState sym) sym (MacawExt arch)
 
-type Regs sym arch = Ctx.Assignment (C.RegValue' sym)
-                                    (MacawCrucibleRegTypes arch)
-
-type LookupFunctionHandle sym arch =
-  MM.MemImpl sym -> Regs sym arch -> IO (C.FnHandle (Ctx.EmptyCtx Ctx.::> ArchRegStruct arch) (ArchRegStruct arch))
 
 -- | This evaluates a  Macaw statement extension in the simulator.
 execMacawStmtExtension ::
   IsSymInterface sym =>
   MacawArchEvalFn sym arch {- ^ Function for executing -} ->
   C.GlobalVar MM.Mem ->
-  GlobalMap sym arch ->
+  GlobalMap sym (M.ArchAddrWidth arch) ->
   LookupFunctionHandle sym arch ->
   EvalStmtFunc (MacawStmtExtension arch) (MacawSimulatorState sym) sym (MacawExt arch)
-execMacawStmtExtension archStmtFn mvar globs lookupH s0 st =
+execMacawStmtExtension archStmtFn mvar globs (LFH lookupH) s0 st =
   case s0 of
     MacawReadMem w mr x         -> doReadMem st mvar globs w mr x
     MacawCondReadMem w mr p x d -> doCondReadMem st mvar globs w mr p x d
@@ -424,8 +418,8 @@ execMacawStmtExtension archStmtFn mvar globs lookupH s0 st =
       where sym = st^.C.stateSymInterface
 
     MacawLookupFunctionHandle _ args -> do
-      hv <- C.HandleFnVal <$> doLookupFunctionHandle lookupH st mvar (C.regValue args)
+      (hv, st') <- doLookupFunctionHandle lookupH st mvar (C.regValue args)
-      return (hv, st)
+      return (C.HandleFnVal hv, st')
 
     MacawArchStmtExtension s    -> archStmtFn s st
     MacawArchStateUpdate {}     -> return ((), st)
@@ -489,7 +483,7 @@ macawExtensions ::
   IsSymInterface sym =>
   MacawArchEvalFn sym arch ->
   C.GlobalVar MM.Mem ->
-  GlobalMap sym arch ->
+  GlobalMap sym (M.ArchAddrWidth arch) ->
   LookupFunctionHandle sym arch ->
   C.ExtensionImpl (MacawSimulatorState sym) sym (MacawExt arch)
 macawExtensions f mvar globs lookupH =
@@ -497,13 +491,6 @@ macawExtensions f mvar globs lookupH =
                   , C.extensionExec = execMacawStmtExtension f mvar globs lookupH
                   }
 
-
--- | Maps region indexes to the pointers representing them.
-type GlobalMap sym arch = Map M.RegionIndex
-                              (MM.LLVMPtr sym (M.ArchAddrWidth arch))
-
-
-
 -- | Run the simulator over a contiguous set of code.
 runCodeBlock :: forall sym arch blocks
            .  (C.IsSyntaxExtension (MacawExt arch), IsSymInterface sym)
@@ -512,7 +499,7 @@ runCodeBlock :: forall sym arch blocks
               -- ^ Translation functions
            -> MacawArchEvalFn sym arch
            -> C.HandleAllocator RealWorld
-           -> (MM.MemImpl sym, GlobalMap sym arch)
+           -> (MM.MemImpl sym, GlobalMap sym (M.ArchAddrWidth arch))
            -> LookupFunctionHandle sym arch
            -> C.CFG (MacawExt arch) blocks (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)
            -> Ctx.Assignment (C.RegValue' sym) (MacawCrucibleRegTypes arch)

symbolic/src/Data/Macaw/Symbolic/MemOps.hs

@@ -11,6 +11,7 @@
 {-# Language PatternGuards #-}
 module Data.Macaw.Symbolic.MemOps
   ( PtrOp
+  , GlobalMap
   , doPtrAdd
   , doPtrSub
   , doPtrMux
@@ -24,21 +25,26 @@ module Data.Macaw.Symbolic.MemOps
   , doGetGlobal
   , doLookupFunctionHandle
   , doPtrToBits
+  , Regs
+  , MacawSimulatorState(..)
+  , LookupFunctionHandle(..)
   ) where
 
 import           Control.Lens ((^.),(&),(%~))
 import           Control.Monad (guard)
 import           Data.Bits (testBit)
-import           Data.Map (Map)
+import           Data.Maybe ( fromMaybe )
-import qualified Data.Map as Map
 
 import           Data.Parameterized (Some(..))
+import qualified Data.Parameterized.Context as Ctx
 
 import           What4.Interface
 import           What4.Symbol (userSymbol)
 
 import           Lang.Crucible.Backend
 import           Lang.Crucible.CFG.Common (GlobalVar)
+import qualified Lang.Crucible.FunctionHandle as C
+import qualified Lang.Crucible.Simulator.RegMap as C
 import           Lang.Crucible.Simulator.ExecutionTree
           ( CrucibleState
           , stateSymInterface
@@ -58,7 +64,6 @@ import           Lang.Crucible.LLVM.MemModel
           , loadRaw
           , loadRawWithCondition
           , storeRaw
-          , doPtrAddOffset
           )
 import           Lang.Crucible.LLVM.MemModel.Pointer
           ( llvmPointerView, muxLLVMPtr, llvmPointer_bv, ptrAdd, ptrSub, ptrEq
@@ -70,10 +75,69 @@ import           Lang.Crucible.LLVM.MemModel.Generic (ppPtr)
 import           Lang.Crucible.LLVM.DataLayout (EndianForm(..))
 import           Lang.Crucible.LLVM.Bytes (toBytes)
 
-import           Data.Macaw.Symbolic.CrucGen (addrWidthIsPos)
+import           Data.Macaw.Symbolic.CrucGen (addrWidthIsPos, ArchRegStruct, MacawExt, MacawCrucibleRegTypes)
 import           Data.Macaw.Symbolic.PersistentState (ToCrucibleType)
 import           Data.Macaw.CFG.Core (MemRepr(BVMemRepr))
-import qualified Data.Macaw.Memory as M
+import qualified Data.Macaw.CFG as M
+
+-- | The 'GlobalMap' is a function that maps from (possibly segmented) program
+-- virtual addresses into pointers into the LLVM memory model heap (the
+-- 'LLVMPtr' type).
+--
+-- There are two types of value translated here:
+--
+-- 1. Bitvectors treated as pointers, and
+-- 2. Segmented addresses (e.g., from object files or shared libraries)
+--
+-- To set up the memory model to verify parts of a program, callers need to
+-- allocate regions of memory to store data including the initial program state.
+-- The user-facing API for allocating memory is the 'doMalloc' primitive from
+-- Lang.Crucible.LLVM.MemModel.  This allocates fresh memory that is distinct
+-- from all other memory in the system.  The distinctness is guaranteed because
+-- each allocation has a unique region identifier.  Each freshly allocated
+-- region of memory has a base address of zero and a size.
+--
+-- In a machine code program, there are a few different kinds of memory to map
+-- into the address space: 1) a *stack*, 2) the *data* segment, 3) and the
+-- program *text* segment.
+--
+-- The *stack* should be logically separate from everything else, so an
+-- allocation with 'doMalloc' is natural.  It is the responsibility of the
+-- caller to place the pointer to the stack (that is the LLVM memory model
+-- pointer) into the appropriate register in the machine state for their
+-- architecture.
+--
+-- The *data* and *text* segments are static data in the original binary image
+-- being analyzed.  They are usually disjoint, so it usually makes sense to
+-- allocate one region of memory for each one using 'doMalloc'.  To resolve a
+-- computed address (which will be a bitvector, i.e., an LLVMPtr value with a
+-- zero region index) that refers to either, a typical workflow in the
+-- 'GlobalMap' function is:
+--
+-- 1. Inspect the region index (the @'RegValue' sym 'NatType'@ parameter)
+-- 2. If the region index is zero, it is a bitvector to translate into an
+--    LLVM memory model pointer ('LLVMPtr')
+-- 3. Look up the offset of the pointer from zero (the @'RegValue' sym ('BVType'
+--    w)@) in a map (probably an IntervalMap); that map should return the base
+--    address of the allocation (which is an 'LLVMPtr')
+-- 4. Depending on the representation of that pointer chosen by the
+--    frontend/setup code, the 'LLVMPtr' may need to be corrected to rebase it,
+--    as the segment being represented by that allocation may not actually start
+--    at address 0 (while the LLVM offset does start at 0).
+--
+-- That discussion describes the translation of raw bitvectors into pointers.
+-- This mapping is also used in another case (see 'doGetGlobal'): translating
+-- the address of a relocatable value (which doesn't necessarily have a
+-- well-defined absolute address) into an address in the LLVM memory model.
+-- Relocatable values in this setting have a non-zero region index as an input.
+-- The 'GlobalMap' is responsible for 1) determining which LLVM allocation
+-- contains the relocatable value, and 2) returning the corresponding address in
+-- that allocation.
+type GlobalMap sym w = sym                        {-^ The symbolic backend -} ->
+                       RegValue sym Mem           {-^ The global handle to the memory model -} ->
+                       RegValue sym NatType       {-^ The region index of the pointer being translated -} ->
+                       RegValue sym (BVType w)    {-^ The offset of the pointer into the region -} ->
+                       IO (Maybe (LLVMPtr sym w))
 
 -- | This is called whenever a (bit-vector/pointer) is used as a bit-vector.
 -- The result is undefined (i.e., a fresh unknown value) if it is given
@@ -90,16 +154,28 @@ doPtrToBits sym w p =
      notPtr <- natEq sym base =<< natLit sym 0
      bvIte sym notPtr (asBits p) undef
 
+data MacawSimulatorState sym = MacawSimulatorState
+
+type Regs sym arch = Ctx.Assignment (C.RegValue' sym)
+                                    (MacawCrucibleRegTypes arch)
+
+data LookupFunctionHandle sym arch = LFH
+     (forall rtp blocks r ctx
+   . CrucibleState (MacawSimulatorState sym) sym (MacawExt arch) rtp blocks r ctx
+  -> MemImpl sym
+  -> Regs sym arch
+  -> IO (C.FnHandle (Ctx.EmptyCtx Ctx.::> ArchRegStruct arch) (ArchRegStruct arch), CrucibleState (MacawSimulatorState sym) sym (MacawExt arch) rtp blocks r ctx))
+
 --------------------------------------------------------------------------------
 doLookupFunctionHandle :: (IsSymInterface sym)
-                       => (MemImpl sym -> regs -> IO a)
+                       => (CrucibleState s sym ext trp blocks r ctx -> MemImpl sym -> regs -> IO (a, CrucibleState s sym ext trp blocks r ctx))
                        -> CrucibleState s sym ext trp blocks r ctx
                        -> GlobalVar Mem
                        -> regs
-                       -> IO a
+                       -> IO (a, CrucibleState s sym ext trp blocks r ctx)
 doLookupFunctionHandle k st mvar regs = do
   mem <- getMem st mvar
-  k mem regs
+  k st mem regs
 --------------------------------------------------------------------------------
 
 
@@ -112,27 +188,36 @@ doGetGlobal ::
   (IsSymInterface sym, M.MemWidth w) =>
   CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state   -} ->
   GlobalVar Mem                            {- ^ Model of memory   -} ->
-  Map M.RegionIndex (RegValue sym (LLVMPointerType w)) {- ^ Region ptrs -} ->
+  GlobalMap sym w ->
   M.MemAddr w                              {- ^ Address identifier -} ->
   IO ( RegValue sym (LLVMPointerType w)
      , CrucibleState s sym ext rtp blocks r ctx
      )
-doGetGlobal st mvar globs addr =
+doGetGlobal st mvar globs addr = do
-  case Map.lookup (M.addrBase addr) globs of
+  let sym = st^.stateSymInterface
+  mem <- getMem st mvar
+  regionNum <- natLit sym (fromIntegral (M.addrBase addr))
+  offset <- bvLit sym (M.addrWidthNatRepr (M.addrWidthRepr addr)) (M.memWordInteger (M.addrOffset addr))
+  mptr <- globs sym mem regionNum offset
+  case mptr of
     Nothing -> fail $ unlines
                         [ "[doGetGlobal] Undefined global region:"
                         , "*** Region:  " ++ show (M.addrBase addr)
                         , "*** Address: " ++ show addr
                         ]
-    Just region ->
+-- <<<<<<< HEAD
-      do mem <- getMem st mvar
+    Just ptr -> return (ptr, st)
-         let sym = st^.stateSymInterface
+-- =======
-         let w = M.addrWidthRepr addr
+--     Just region ->
-         LeqProof <- pure $ addrWidthAtLeast16 w
+--       do mem <- getMem st mvar
-         let ?ptrWidth = M.addrWidthNatRepr w
+--          let sym = st^.stateSymInterface
-         off <- bvLit sym ?ptrWidth (M.memWordInteger (M.addrOffset addr))
+--          let w = M.addrWidthRepr addr
-         res <- doPtrAddOffset sym mem region off
+--          LeqProof <- pure $ addrWidthAtLeast16 w
-         return (res, st)
+--          let ?ptrWidth = M.addrWidthNatRepr w
+--          off <- bvLit sym ?ptrWidth (M.memWordInteger (M.addrOffset addr))
+--          res <- doPtrAddOffset sym mem region off
+--          return (res, st)
+-- >>>>>>> master
 
 --------------------------------------------------------------------------------
 
@@ -317,7 +402,7 @@ doReadMem ::
   IsSymInterface sym =>
   CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state   -} ->
   GlobalVar Mem ->
-  Map M.RegionIndex (RegValue sym (LLVMPointerType ptrW)) {- ^ Region ptrs -} ->
+  GlobalMap sym ptrW ->
   M.AddrWidthRepr ptrW ->
   MemRepr ty ->
   RegEntry sym (LLVMPointerType ptrW) ->
@@ -333,8 +418,7 @@ doReadMem st mvar globs w (BVMemRepr bytes endian) ptr0 =
          bitw  = natMultiply (knownNat @8) bytes
 
      LeqProof <- return (leqMulPos (knownNat @8) bytes)
-
+     ptr <- tryGlobPtr sym mem globs (regValue ptr0)
-     ptr <- tryGlobPtr sym mem globs w (regValue ptr0)
 
      let ?ptrWidth = M.addrWidthNatRepr w
      ok <- isValidPtr sym mem w ptr
@@ -347,7 +431,6 @@ doReadMem st mvar globs w (BVMemRepr bytes endian) ptr0 =
      a   <- case valToBits bitw val of
               Just a  -> return a
               Nothing -> fail "[doReadMem] We read an unexpected value"
-
      return (a,st)
 
 
@@ -356,7 +439,7 @@ doCondReadMem ::
   IsSymInterface sym =>
   CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state   -} ->
   GlobalVar Mem                            {- ^ Memory model -} ->
-  Map M.RegionIndex (RegValue sym (LLVMPointerType ptrW)) {- ^ Region ptrs -} ->
+  GlobalMap sym ptrW                       {- ^ Translate machine addresses to memory model addresses -} ->
   M.AddrWidthRepr ptrW                     {- ^ Width of ptr -} ->
   MemRepr ty                               {- ^ What/how we are reading -} ->
   RegEntry sym BoolType                    {- ^ Condition -} ->
@@ -376,7 +459,7 @@ doCondReadMem st mvar globs w (BVMemRepr bytes endian) cond0 ptr0 def0 =
 
      LeqProof <- return (leqMulPos (knownNat @8) bytes)
 
-     ptr <- tryGlobPtr sym mem globs w (regValue ptr0)
+     ptr <- tryGlobPtr sym mem globs (regValue ptr0)
      ok  <- isValidPtr sym mem w ptr
      check sym ok "doCondReadMem"
                 $ "Conditional read through an invalid pointer: " ++
@@ -407,7 +490,7 @@ doWriteMem ::
   IsSymInterface sym =>
   CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state   -} ->
   GlobalVar Mem                            {- ^ Memory model -} ->
-  Map M.RegionIndex (RegValue sym (LLVMPointerType ptrW)) {- ^ Region ptrs -} ->
+  GlobalMap sym ptrW ->
   M.AddrWidthRepr ptrW                     {- ^ Width of ptr -} ->
   MemRepr ty                               {- ^ What/how we are writing -} ->
   RegEntry sym (LLVMPointerType ptrW)      {- ^ Pointer -} ->
@@ -425,8 +508,7 @@ doWriteMem st mvar globs w (BVMemRepr bytes endian) ptr0 val =
      LeqProof <- pure $ addrWidthIsPos w
      LeqProof <- pure $ addrWidthAtLeast16 w
      LeqProof <- return (leqMulPos (knownNat @8) bytes)
-
+     ptr <- tryGlobPtr sym mem globs (regValue ptr0)
-     ptr <- tryGlobPtr sym mem globs w (regValue ptr0)
      ok <- isValidPtr sym mem w ptr
      check sym ok "doWriteMem"
                   $ "Write to an invalid location: " ++ show (ppPtr ptr)
@@ -606,33 +688,30 @@ mkName x = case userSymbol x of
 
 
 
-{- | Every now and then we encoutner memory opperations that
+{- | Every now and then we encounter memory opperations that
 just read/write to some constant.  Normally, we do not allow
 such things as we want memory to be allocated first.
 However we need to make an exception for globals.
 So, if we ever try to manipulate memory at some address
 which is statically known to be a constant, we consult
 the global map to see if we know about a correpsonding
-addres..  If so, we use that for the memory operation. -}
+address.  If so, we use that for the memory operation.
+
+See the documentation of 'GlobalMap' for details about how that translation can
+be handled.
+-}
 tryGlobPtr ::
   IsSymInterface sym =>
   sym ->
   RegValue sym Mem ->
-  Map M.RegionIndex (RegValue sym (LLVMPointerType w)) {- ^ Region ptrs -} ->
+  GlobalMap sym w ->
-  M.AddrWidthRepr w ->
   LLVMPtr sym w ->
   IO (LLVMPtr sym w)
-tryGlobPtr sym mem globs w val
+tryGlobPtr sym mem mapBVAddress val
-  | Just 0 <- asNat (ptrBase val)
+  | Just 0 <- asNat (ptrBase val) = do
-  , Just r <- Map.lookup literalAddrRegion globs
+      maddr <- mapBVAddress sym mem (ptrBase val) (asBits val)
-  , LeqProof <- addrWidthIsPos w
+      return (fromMaybe val maddr)
-  , LeqProof <- addrWidthAtLeast16 w =
-     let ?ptrWidth = M.addrWidthNatRepr w
-      in doPtrAddOffset sym mem r (asBits val)
   | otherwise = return val
-  where
-  literalAddrRegion = 0
-
 
 isAlignMask :: (IsSymInterface sym) => LLVMPtr sym w -> Maybe Integer
 isAlignMask v =

x86/src/Data/Macaw/X86/ArchTypes.hs

@@ -323,15 +323,15 @@ data X86PrimFn f tp where
   --   else
   --     return (false, trunc 32 temp64, trunc 32 (temp64 >> 32))
   CMPXCHG8B :: !(f (BVType 64))
-               -- ^ Address to read
+               -- Address to read
             -> !(f (BVType 32))
-               -- ^ Value in EAX
+               -- Value in EAX
             -> !(f (BVType 32))
-               -- ^ Value in EBX
+               -- Value in EBX
             -> !(f (BVType 32))
-               -- ^ Value in ECX
+               -- Value in ECX
             -> !(f (BVType 32))
-               -- ^ Value in EDX
+               -- Value in EDX
             -> X86PrimFn f (TupleType [BoolType, BVType 32, BVType 32])
 
   -- | The RDTSC instruction.
@@ -828,6 +828,7 @@ data X86Stmt (v :: Type -> *) where
   -- * @dir@ is a flag that indicates whether direction of move:
   --   * 'True' means we should decrement buffer pointers after each copy.
   --   * 'False' means we should increment the buffer pointers after each copy.
+
   RepStos :: !(RepValSize w)
           -> !(v (BVType 64))
              -- /\ Address to start assigning to.
@@ -851,6 +852,7 @@ data X86Stmt (v :: Type -> *) where
 
   EMMS :: X86Stmt v
   -- ^ Empty MMX technology State. Sets the x87 FPU tag word to empty.
+  --
   -- Probably OK to use this for both EMMS FEMMS, the second being a a
   -- faster version from AMD 3D now.