Merge branch 'refinement' of github.com:GaloisInc/macaw into refinement

2024-12-27 16:15:12 +03:00 · 2019-02-06 17:51:21 -08:00 · 2019-02-06 17:51:21 -08:00 · 36a8be1c4e
commit 36a8be1c4e
parent eb3bc794c1 72c54dcf15
13 changed files with 407 additions and 280 deletions
--- a/base/src/Data/Macaw/Discovery.hs
+++ b/base/src/Data/Macaw/Discovery.hs
@ -245,13 +245,21 @@ filterStmtList stmtPred s = do
        , stmtsTerm = term'
        }

+-- | Force each nonterminal statement in the list.
+seqStmtList :: StatementList arch ids -> ()
+seqStmtList stmts = foldr seq () (stmtsNonterm stmts)
+
 -- | Eliminate all dead statements in blocks
 dropUnusedCodeInParsedBlock :: ArchitectureInfo arch
                          -> ParsedBlock arch ids
                          -> ParsedBlock arch ids
 dropUnusedCodeInParsedBlock ainfo b =
-    b { blockStatementList = filterStmtList stmtPred l }
-  where l = blockStatementList b
+    -- Important to force the result list here, since otherwise we
+    -- hold onto the entire input list
+    seqStmtList stmtList' `seq`
+    b { blockStatementList = stmtList' }
+  where stmtList' = filterStmtList stmtPred l
+        l = blockStatementList b
        demandSet =
          runDemandComp (archDemandContext ainfo) $ do
            addStatementListDemands l
--- a/refinement/src/Data/Macaw/Refinement.hs
+++ b/refinement/src/Data/Macaw/Refinement.hs
@ -16,6 +16,7 @@ import           GHC.TypeLits
 import           Control.Lens
 import           Control.Monad.IO.Class (MonadIO)
 import qualified Data.Macaw.Architecture.Info as MA
+import qualified Data.Macaw.BinaryLoader as MBL
 import           Data.Macaw.CFG.AssignRhs
 import qualified Data.Macaw.CFG as MC
 import qualified Data.Macaw.Discovery as MD
@ -38,7 +39,8 @@ import           Data.Parameterized.Classes
 -- alternative to the same named function in Data.Macaw.Discovery.
 cfgFromAddrsAndState
  :: (MS.SymArchConstraints arch, 16 <= MC.ArchAddrWidth arch, MonadIO m)
-  => MD.DiscoveryState arch
+  => MBL.LoadedBinary arch bin
+  -> MD.DiscoveryState arch
  -> [ArchSegmentOff arch]
  -- ^ Initial function entry points.
  -> [(ArchSegmentOff arch, ArchSegmentOff arch)]
@ -47,9 +49,9 @@ cfgFromAddrsAndState
  --
  -- Each entry contains an address and the value stored in it.
  -> m (DiscoveryState arch)
-cfgFromAddrsAndState initial_state init_addrs mem_words =
+cfgFromAddrsAndState bin initial_state init_addrs mem_words =
  MD.cfgFromAddrsAndState initial_state init_addrs mem_words
-    & refineDiscovery
+    & refineDiscovery bin

 -- | Construct an empty discovery state and populate it by exploring
 -- from a given set of function entry points.  This can be used as an
@ -57,7 +59,8 @@ cfgFromAddrsAndState initial_state init_addrs mem_words =
 -- Data.Macaw.Discovery.
 cfgFromAddrs
  :: (MS.SymArchConstraints arch, 16 <= MC.ArchAddrWidth arch, MonadIO m)
-  => MA.ArchitectureInfo arch
+  => MBL.LoadedBinary arch bin
+  -> MA.ArchitectureInfo arch
  -- ^ Architecture-specific information needed for doing
  -- control-flow exploration.
  -> MM.Memory (ArchAddrWidth arch)
@ -72,8 +75,8 @@ cfgFromAddrs
  --
  -- Each entry contains an address and the value stored in it.
  -> m (DiscoveryState arch)
-cfgFromAddrs ainfo mem addrSymMap =
-  cfgFromAddrsAndState (emptyDiscoveryState mem addrSymMap ainfo)
+cfgFromAddrs bin ainfo mem addrSymMap =
+  cfgFromAddrsAndState bin (emptyDiscoveryState mem addrSymMap ainfo)


 ----------------------------------------------------------------------
@ -89,7 +92,8 @@ cfgFromAddrs ainfo mem addrSymMap =
 -- perform additional discovery for incomplete blocks.
 refineDiscovery
  :: (MS.SymArchConstraints arch, 16 <= MC.ArchAddrWidth arch, MonadIO m)
-  => DiscoveryState arch
+  => MBL.LoadedBinary arch bin
+  -> DiscoveryState arch
  -> m (DiscoveryState arch)
-refineDiscovery =
-  symbolicUnkTransferRefinement . symbolicTargetRefinement
+refineDiscovery bin =
+  symbolicUnkTransferRefinement bin . symbolicTargetRefinement
--- a/refinement/src/Data/Macaw/Refinement/FuncBlockUtils.hs
+++ b/refinement/src/Data/Macaw/Refinement/FuncBlockUtils.hs
@ -1,10 +1,9 @@
 module Data.Macaw.Refinement.FuncBlockUtils
-  ( BlockIdentifier
+  ( BlockIdentifier(..)
  , blockID
  , blockInFunction
  , blockTransferTo
  , funBlockIDs
-  , funForBlock
  , getBlock
  )
 where
@ -13,16 +12,12 @@ import           Control.Lens
 import qualified Data.Foldable as F
 import           Data.Macaw.CFG.AssignRhs ( ArchSegmentOff )
 import           Data.Macaw.Discovery.State ( DiscoveryFunInfo
-                                            , DiscoveryState
                                            , ParsedBlock(..)
                                            , ParsedTermStmt(..)
-                                            , funInfo
                                            , parsedBlocks
                                            , stmtsTerm
                                            )
 import qualified Data.Map as Map
-import           Data.Maybe ( isJust )
-import           Data.Parameterized.Some
 import           Data.Semigroup

 import           Prelude
@ -31,48 +26,31 @@ import           Prelude
 -- | The local type used to identify blocks.  Using a local
 -- abstraction for this allows this code to be more independent of the
 -- underlying block information.
-type BlockIdentifier arch = ArchSegmentOff arch
+newtype BlockIdentifier arch ids = BlockIdentifier
+  { biArchSegmentOff :: ArchSegmentOff arch
+  }
+  deriving (Eq, Ord)

 -- | Obtain the local 'BlockIdentifier' value for a block.
-blockID :: Some (ParsedBlock arch) -> BlockIdentifier arch
-blockID = viewSome pblockAddr
+blockID :: ParsedBlock arch ids -> BlockIdentifier arch ids
+blockID =  BlockIdentifier . pblockAddr


 -- | Return the ID's for all blocks in the function
-funBlockIDs :: Some (DiscoveryFunInfo arch) -> [BlockIdentifier arch]
-funBlockIDs (Some fi) = blockID . Some <$> Map.elems (fi ^. parsedBlocks)
-
-- | Given a block determine which function that block is a part of.
-funForBlock :: Some (ParsedBlock arch)
-            -> DiscoveryState arch
-            -> Maybe (Some (DiscoveryFunInfo arch))
-funForBlock pb ds =
-  let blkID = blockID pb
-      blkFuns = ds ^. funInfo ^.. folded . filtered (funIncludesBlock blkID)
-  in case blkFuns of
-       [Some f] -> Just $ Some f
-       _ -> Nothing  -- should not be possible
+funBlockIDs :: DiscoveryFunInfo arch ids -> [BlockIdentifier arch ids]
+funBlockIDs fi = map blockID $ Map.elems (fi ^. parsedBlocks)

 blockInFunction :: DiscoveryFunInfo arch ids
                -> ArchSegmentOff arch
-                -> Maybe (BlockIdentifier arch)
-blockInFunction fi addr = blockID . Some <$> (fi ^. parsedBlocks) Map.!? addr
-
-funIncludesBlock :: BlockIdentifier arch
-                 -> Some (DiscoveryFunInfo arch)
-                 -> Bool
-funIncludesBlock blkID (Some fi) =
-  isJust ((fi ^. parsedBlocks) Map.!? blkID)
+                -> Maybe (BlockIdentifier arch ids)
+blockInFunction fi addr = blockID <$> (fi ^. parsedBlocks) Map.!? addr

 -- | Returns the actual block (if it exists) from the Discovery State
 -- (in the first function for which it exists).
-getBlock :: DiscoveryState arch
-         -> BlockIdentifier arch
-         -> Maybe (Some (ParsedBlock arch))
-getBlock ds blkID =
-  case filter (funIncludesBlock blkID) (ds ^. funInfo ^.. folded) of
-    ((Some fi):_) -> Some <$> (fi ^. parsedBlocks) Map.!? blkID
-    [] -> Nothing
+getBlock :: DiscoveryFunInfo arch ids
+         -> BlockIdentifier arch ids
+         -> Maybe (ParsedBlock arch ids)
+getBlock fi blkID = (fi ^. parsedBlocks) Map.!? biArchSegmentOff blkID

 -- | This function identifies the possible target addresses (of other
 -- blocks within this function) from the terminal statement in the
@ -82,11 +60,10 @@ getBlock ds blkID =
 -- function, but it is not required to, nor will it return other
 -- external targets.
 blockTransferTo :: DiscoveryFunInfo arch ids
-                -> BlockIdentifier arch
+                -> BlockIdentifier arch ids
                -> [ArchSegmentOff arch]
-blockTransferTo fi frm =
-  let frmBlk = (fi ^. parsedBlocks) Map.!? frm
-      lclTgtAddrs termStmt =
+blockTransferTo fi blkID =
+  let lclTgtAddrs termStmt =
        case termStmt of
          ParsedCall _ mbTgt | Just tgt <- mbTgt -> [tgt]
                             | otherwise -> []
@ -100,6 +77,6 @@ blockTransferTo fi frm =
                                       | otherwise -> []
          ParsedTranslateError {} -> []
          ClassifyFailure {} -> []
-  in case frmBlk of
+  in case getBlock fi blkID of
       Just fBlk -> lclTgtAddrs $ stmtsTerm $ blockStatementList fBlk
       Nothing -> error "block ID not valid" -- impossible
--- a/refinement/src/Data/Macaw/Refinement/Path.hs
+++ b/refinement/src/Data/Macaw/Refinement/Path.hs
@ -14,12 +14,11 @@ import           Control.Applicative
 import           Data.Macaw.CFG.AssignRhs ( ArchAddrWidth, ArchSegmentOff )
 import           Data.Macaw.Discovery.State ( DiscoveryFunInfo )
 import           Data.Macaw.Memory ( MemWidth )
-import           Data.Macaw.Refinement.FuncBlockUtils ( BlockIdentifier
+import           Data.Macaw.Refinement.FuncBlockUtils ( BlockIdentifier(..)
                                                      , blockInFunction
                                                      , blockTransferTo
                                                      , funBlockIDs
                                                      )
-import           Data.Parameterized.Some
 import           Data.Text.Prettyprint.Doc
 import qualified Text.PrettyPrint.ANSI.Leijen as PP

@ -27,17 +26,16 @@ import qualified Text.PrettyPrint.ANSI.Leijen as PP
 -- | This is the datatype that represents the back-path of blocks in
 -- the function from the exit point(s) to either the entry point or a
 -- loop point.
-data FuncBlockPath arch =
-  Path
-  (BlockIdentifier arch) -- ^ current block identifier
-  [FuncBlockPath arch]   -- ^ next non-loop path elements (callees for
-                         -- a ForwardPath, callers for a BackwardPath)
-  [BlockIdentifier arch] -- ^ next elements which would form a path
-                         -- loop.
+data FuncBlockPath arch ids = Path (BlockIdentifier arch ids) [FuncBlockPath arch ids] [BlockIdentifier arch ids]
+  -- (BlockIdentifier arch) -- ^ current block identifier
+  -- [FuncBlockPath arch]   -- ^ next non-loop path elements (callees for
+  --                        -- a ForwardPath, callers for a BackwardPath)
+  -- [BlockIdentifier arch] -- ^ next elements which would form a path
+  --                        -- loop.


 instance ( MemWidth (ArchAddrWidth arch) ) =>
-         Pretty (FuncBlockPath arch) where
+         Pretty (FuncBlockPath arch ids) where
  pretty (Path bid anc loop) =
    let label = [ pretty "Path", prettyBlkId bid
                , parens $ hsep [ pretty $ length anc, pretty " callers" ]
@ -45,7 +43,7 @@ instance ( MemWidth (ArchAddrWidth arch) ) =>
        looptxt = if null loop then []
                  else [parens (hsep [ pretty "loops from:"
                                     , list ( prettyBlkId <$> loop )])]
-        prettyBlkId = pretty . show . PP.pretty
+        prettyBlkId = pretty . show . PP.pretty . biArchSegmentOff
    in vsep [ hsep (label <> looptxt)
            , nest 4 $ vsep (pretty <$> anc)
            ]
@ -60,9 +58,9 @@ instance ( MemWidth (ArchAddrWidth arch) ) =>
 -- JMP targets; at the present time it is assumed that the latter
 -- targets cannot be a mix of function-internal and function-external
 -- targets.
-buildFuncPath :: Some (DiscoveryFunInfo arch) -> [FuncBlockPath arch]
-buildFuncPath sfi@(Some fi) =
-  let blks = funBlockIDs sfi
+buildFuncPath :: DiscoveryFunInfo arch ids -> [FuncBlockPath arch ids]
+buildFuncPath fi =
+  let blks = funBlockIDs fi
  in fst $ bldFPath fi ([], blks)


@ -74,8 +72,8 @@ buildFuncPath sfi@(Some fi) =
 -- recursive invocation takes the next BlockIdentifier and adds it to
 -- an existing path or starts a new path for that BlockIdentifier.
 bldFPath :: DiscoveryFunInfo arch ids
-         -> ([FuncBlockPath arch], [BlockIdentifier arch])
-         -> ([FuncBlockPath arch], [BlockIdentifier arch])
+         -> ([FuncBlockPath arch ids], [BlockIdentifier arch ids])
+         -> ([FuncBlockPath arch ids], [BlockIdentifier arch ids])
 bldFPath _fi x@(_, []) = x
 bldFPath fi (fs, b:bs) =
  let nextBlkAddrs = blockTransferTo fi b
@ -90,10 +88,10 @@ bldFPath fi (fs, b:bs) =


 bldFPath' :: DiscoveryFunInfo arch ids
-          -> BlockIdentifier arch
+          -> BlockIdentifier arch ids
          -> ArchSegmentOff arch
-          -> [FuncBlockPath arch]
-          -> [FuncBlockPath arch]
+          -> [FuncBlockPath arch ids]
+          -> [FuncBlockPath arch ids]
 bldFPath' fi b nextAddr fs =
  let nextBlkID = blockInFunction fi nextAddr

@ -138,7 +136,9 @@ bldFPath' fi b nextAddr fs =
 -- block might be reachable backward from several exit points, but the
 -- inbound paths (i.e. above/forward to) the specified block must be
 -- the same for all outbound paths (loops are elided).
-pathTo :: BlockIdentifier arch -> [FuncBlockPath arch] -> Maybe (FuncBlockPath arch)
+pathTo :: BlockIdentifier arch ids
+       -> [FuncBlockPath arch ids]
+       -> Maybe (FuncBlockPath arch ids)
 pathTo blkID (p@(Path i anc _):ps) =
  if blkID == i
  then Just p
@ -150,7 +150,7 @@ pathTo _ [] = Nothing

 -- | Returns the first n levels (callers) for the specified Block path
 -- in the Function.
-takePath :: Int -> FuncBlockPath arch -> FuncBlockPath arch
+takePath :: Int -> FuncBlockPath arch ids -> FuncBlockPath arch ids
 takePath n (Path blkid anc loop) =
  if n > 0
  then Path blkid (takePath (n-1) <$> anc) loop
@ -159,7 +159,7 @@ takePath n (Path blkid anc loop) =

 -- | Returns the maximum length (depth) of all paths through the
 -- function (ignoring loops)
-pathDepth :: FuncBlockPath arch -> Int
+pathDepth :: FuncBlockPath arch ids -> Int
 pathDepth (Path _ [] _) = 0
 pathDepth (Path _ anc _) = 1 + maximum (pathDepth <$> anc)

@ -186,7 +186,7 @@ pathDepth (Path _ anc _) = 1 + maximum (pathDepth <$> anc)
 -- >  , [ 3, 7, 5, 4, 1 ]
 -- >  ]
 --
-pathForwardTrails :: FuncBlockPath arch -> [ [BlockIdentifier arch] ]
+pathForwardTrails :: FuncBlockPath arch ids -> [ [BlockIdentifier arch ids] ]
 pathForwardTrails (Path i [] _) = [[i]]
 pathForwardTrails (Path i anc _) = let ft = concatMap pathForwardTrails anc
                                       appendTo v l = l <> [v]
--- a/refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs
+++ b/refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs
@ -117,8 +117,10 @@ where
 import           GHC.TypeLits

 import Control.Lens
+import Control.Monad ( foldM, forM )
 import Control.Monad.ST ( RealWorld, stToIO )
 import Control.Monad.IO.Class ( MonadIO, liftIO )
+import qualified Data.Macaw.BinaryLoader as MBL
 import qualified Data.Macaw.CFG as MC
 import Data.Macaw.CFG.AssignRhs ( ArchSegmentOff )
 import qualified Data.Macaw.CFG.Rewriter as RW
@ -135,23 +137,19 @@ import Data.Macaw.Discovery ( DiscoveryFunInfo
                            , parsedBlocks
                            , stmtsTerm
                            )
-import Data.Macaw.Refinement.FuncBlockUtils ( BlockIdentifier, blockID
+import Data.Macaw.Refinement.FuncBlockUtils ( BlockIdentifier(..), blockID
                                            , funForBlock, getBlock )
 import Data.Macaw.Refinement.Path ( FuncBlockPath(..)
                                  , buildFuncPath, pathDepth, pathForwardTrails
                                  , pathTo, takePath )
 import qualified Data.Macaw.Symbolic as MS
-import Data.Map (Map)
+import qualified Data.Macaw.Symbolic.Memory as MSM
 import Data.Maybe
 import qualified Data.Map as Map
 import qualified Data.Parameterized.Context as Ctx
-import Data.Parameterized.Ctx (Ctx)
 import Data.Parameterized.Nonce
 import Data.Parameterized.Some
 import Data.Proxy ( Proxy(..) )
-import Data.Semigroup
-import Data.Text (Text)
-import qualified Data.Text as Text
 import qualified Lang.Crucible.Backend as C
 import qualified Lang.Crucible.Backend.Online as C
 import qualified Lang.Crucible.CFG.Core as C
@ -179,9 +177,13 @@ import           Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>))
 -- information.
 symbolicUnkTransferRefinement
  :: (MS.SymArchConstraints arch, 16 <= MC.ArchAddrWidth arch, MonadIO m)
-  => DiscoveryState arch
+  => MBL.LoadedBinary arch bin
+  -> DiscoveryState arch
  -> m (DiscoveryState arch)
-symbolicUnkTransferRefinement = refineTransfers []
+symbolicUnkTransferRefinement bin inpDS = foldM
+  (\accDS (Some fi) -> refineTransfers bin accDS fi [])
+  inpDS
+  (inpDS ^. funInfo)


 -- | The main loop for transfer discovery refinement.  The first
@ -194,37 +196,26 @@ symbolicUnkTransferRefinement = refineTransfers []
 -- failure accumulation array.
 refineTransfers
  :: (MS.SymArchConstraints arch, 16 <= MC.ArchAddrWidth arch, MonadIO m)
-  => [BlockIdentifier arch]
-     -- ^ attempted blocks
+  => MBL.LoadedBinary arch bin
  -> DiscoveryState arch
-     -- ^ input DiscoveryState
+  -> DiscoveryFunInfo arch ids
+  -> [BlockIdentifier arch ids]
  -> m (DiscoveryState arch)
-     -- ^ Possibly updated DiscoveryState
-refineTransfers failedRefine inpDS = do
+refineTransfers bin inpDS fi failedRefine = do
  let unrefineable = flip elem failedRefine . blockID
-      unkTransfers = inpDS ^. funInfo
-                     . to getAllFunctionsTransfers
-                     ^..folded
-                     . filtered (not . unrefineable)
+      unkTransfers = filter (not . unrefineable) $ getUnknownTransfers fi
      thisUnkTransfer = head unkTransfers
      thisId = blockID thisUnkTransfer
  if null unkTransfers
-     then return inpDS
-     else refineBlockTransfer inpDS thisUnkTransfer >>= \case
-            Nothing    -> refineTransfers (thisId : failedRefine) inpDS
-            Just updDS -> refineTransfers failedRefine updDS
+  then return inpDS
+  else refineBlockTransfer bin inpDS fi thisUnkTransfer >>= \case
+        Nothing    -> refineTransfers bin inpDS fi (thisId : failedRefine)
+        Just updDS -> refineTransfers bin updDS fi failedRefine

-
-getAllFunctionsTransfers :: Map (ArchSegmentOff arch)
-                                  (Some (DiscoveryFunInfo arch))
-                         -> [Some (ParsedBlock arch)]
-getAllFunctionsTransfers = concatMap getUnknownTransfers . Map.elems
-
-
-getUnknownTransfers :: (Some (DiscoveryFunInfo arch))
-                    -> [Some (ParsedBlock arch)]
-getUnknownTransfers (Some fi) =
-  Some <$> (filter isUnknownTransfer $ Map.elems $ fi ^. parsedBlocks)
+getUnknownTransfers :: DiscoveryFunInfo arch ids
+                    -> [ParsedBlock arch ids]
+getUnknownTransfers fi =
+  filter isUnknownTransfer $ Map.elems $ fi ^. parsedBlocks

 isUnknownTransfer :: ParsedBlock arch ids -> Bool
 isUnknownTransfer pb =
@ -243,16 +234,17 @@ refineBlockTransfer
     , 16 <= MC.ArchAddrWidth arch
     , MonadIO m
     ) =>
-     DiscoveryState arch
-  -> Some (ParsedBlock arch)
+     MBL.LoadedBinary arch bin
+  -> DiscoveryState arch
+  -> DiscoveryFunInfo arch ids
+  -> ParsedBlock arch ids
  -> m (Maybe (DiscoveryState arch))
-refineBlockTransfer inpDS blk =
-  let path = buildFuncPath <$> funForBlock blk inpDS
-      tgtPath = path >>= pathTo (blockID blk)
-  in case tgtPath of
-       Nothing -> error "unable to find function path for block" -- internal error
-       Just p -> do soln <- refinePath inpDS p (pathDepth p) 0 Nothing
-                    return $ maybe Nothing (Just . updateDiscovery inpDS blk) soln
+refineBlockTransfer bin inpDS fi blk =
+  case pathTo (blockID blk) $ buildFuncPath fi of
+    Nothing -> error "unable to find function path for block" -- internal error
+    Just p -> do soln <- refinePath bin inpDS fi p (pathDepth p) 1
+                 return $ maybe Nothing (Just . updateDiscovery inpDS blk) soln
+


 updateDiscovery :: ( MC.RegisterInfo (MC.ArchReg arch)
@ -260,7 +252,7 @@ updateDiscovery :: ( MC.RegisterInfo (MC.ArchReg arch)
                   , MC.ArchConstraints arch
                   ) =>
                   DiscoveryState arch
-                -> Some (ParsedBlock arch)
+                -> ParsedBlock arch ids
                -> Solution arch
                -> DiscoveryState arch
 updateDiscovery inpDS b@(Some pblk) soln =
@ -334,35 +326,32 @@ refinePath :: ( MS.SymArchConstraints arch
              , 16 <= MC.ArchAddrWidth arch
              , MonadIO m
              ) =>
-              DiscoveryState arch
-           -> FuncBlockPath arch
+              MBL.LoadedBinary arch bin
+           -> DiscoveryState arch
+           -> DiscoveryFunInfo arch ids
+           -> FuncBlockPath arch ids
           -> Int
           -> Int
-           -> Maybe (Solution arch)
           -> m (Maybe (Solution arch))
-refinePath inpDS path maxlevel numlevels prevResult =
+refinePath bin inpDS fi path maxlevel numlevels =
  let thispath = takePath numlevels path
-      smtEquation = equationFor inpDS thispath
-  in solve smtEquation >>= \case
-       Nothing -> return prevResult -- divergent, stop here
-       s@(Just soln) -> let nextlevel = numlevels + 1
-                            bestResult = case prevResult of
-                                           Nothing -> s
-                                           Just prevSoln ->
-                                             if soln < prevSoln
-                                             then s
-                                             else prevResult
-                    in if numlevels > maxlevel
-                       then return bestResult
-                       else refinePath inpDS path maxlevel nextlevel bestResult
+      smtEquation = equationFor inpDS fi thispath
+  in solve bin smtEquation >>= \case
+       Nothing -> return Nothing -- divergent, stop here
+       soln@(Just{}) -> if numlevels >= maxlevel
+                          then return soln
+                          else refinePath bin inpDS fi path maxlevel (numlevels + 1)

-data Equation arch = Equation (DiscoveryState arch) [[Some (ParsedBlock arch)]]
+data Equation arch ids = Equation (DiscoveryState arch) [[ParsedBlock arch ids]]
 type Solution arch = [ArchSegmentOff arch]  -- identified transfers

-equationFor :: DiscoveryState arch -> FuncBlockPath arch -> Equation arch
-equationFor inpDS p =
+equationFor :: DiscoveryState arch
+            -> DiscoveryFunInfo arch ids
+            -> FuncBlockPath arch ids
+            -> Equation arch ids
+equationFor inpDS fi p =
  let pTrails = pathForwardTrails p
-      pTrailBlocks = map (getBlock inpDS) <$> pTrails
+      pTrailBlocks = map (getBlock fi) <$> pTrails
  in if and (any (not . isJust) <$> pTrailBlocks)
     then error "did not find requested block in discovery results!" -- internal
       else Equation inpDS (catMaybes <$> pTrailBlocks)
@ -371,10 +360,13 @@ solve :: ( MS.SymArchConstraints arch
         , 16 <= MC.ArchAddrWidth arch
         , MonadIO m
         ) =>
-         Equation arch -> m (Maybe (Solution arch))
-solve (Equation inpDS blk) = do
-  blockAddrs <- liftIO (withDefaultRefinementContext $ \context ->
-                           smtSolveTransfer context inpDS blk)
+         MBL.LoadedBinary arch bin
+      -> Equation arch ids
+      -> m (Maybe (Solution arch))
+solve bin (Equation inpDS paths) = do
+  blockAddrs <- concat <$> forM paths
+    (\path -> liftIO $ withDefaultRefinementContext bin $ \context ->
+      smtSolveTransfer context inpDS path)
  return $ if null blockAddrs then Nothing else Just blockAddrs

 --isBetterSolution :: Solution arch -> Solution arch -> Bool
@ -396,39 +388,54 @@ data RefinementContext arch t solver fp = RefinementContext
  }

 withDefaultRefinementContext
-  :: forall arch a m
+  :: forall arch a bin
   . (MS.SymArchConstraints arch, 16 <= MC.ArchAddrWidth arch)
-  => (forall t . RefinementContext arch t (W.Writer W.Z3) (C.Flags C.FloatIEEE) -> IO a)
+  => MBL.LoadedBinary arch bin
+  -> (forall t . RefinementContext arch t (W.Writer W.Z3) (C.Flags C.FloatIEEE) -> IO a)
  -> IO a
-withDefaultRefinementContext k = do
+withDefaultRefinementContext loaded_binary k = do
  handle_alloc <- C.newHandleAllocator
  withIONonceGenerator $ \nonce_gen ->
    C.withZ3OnlineBackend nonce_gen C.NoUnsatFeatures $ \sym ->
      case MS.archVals (Proxy @arch) of
        Just arch_vals -> do
+          -- path_setter <- W.getOptionSetting W.z3Path (W.getConfiguration sym)
+          -- _ <- W.setOpt path_setter "z3-tee"
+
          mem_var <- stToIO $ LLVM.mkMemVar handle_alloc
-          empty_mem <- LLVM.emptyMem LLVM.LittleEndian
-          let ?ptrWidth = W.knownNat
-          (base_ptr, allocated_mem) <- LLVM.doMallocUnbounded
+          -- empty_mem <- LLVM.emptyMem LLVM.LittleEndian
+          -- let ?ptrWidth = W.knownNat
+          -- (base_ptr, allocated_mem) <- LLVM.doMallocUnbounded
+          --   sym
+          --   LLVM.GlobalAlloc
+          --   LLVM.Mutable
+          --   "flat memory"
+          --   empty_mem
+          --   LLVM.noAlignment
+          -- let Right mem_name = W.userSymbol "mem"
+          -- mem_array <- W.freshConstant sym mem_name W.knownRepr
+          -- initialized_mem <- LLVM.doArrayStoreUnbounded
+          --   sym
+          --   allocated_mem
+          --   base_ptr
+          --   LLVM.noAlignment
+          --   mem_array
+          (mem, mapped_memory) <- MSM.newGlobalMemory
+            (Proxy @arch)
            sym
-            LLVM.GlobalAlloc
-            LLVM.Mutable
-            "flat memory"
-            empty_mem
-            LLVM.noAlignment
-          let Right mem_name = W.userSymbol "mem"
-          mem_array <- W.freshConstant sym mem_name W.knownRepr
-          initialized_mem <- LLVM.doArrayStoreUnbounded
-            sym
-            allocated_mem
-            base_ptr
-            LLVM.noAlignment
-            mem_array
+            LLVM.LittleEndian
+            MSM.ConcreteMutable
+            (MBL.memoryImage loaded_binary)
          MS.withArchEval arch_vals sym $ \arch_eval_fns -> do
            let ext_impl = MS.macawExtensions
                  arch_eval_fns
                  mem_var
-                  (\_ _ _ off -> Just <$> LLVM.ptrAdd sym W.knownNat base_ptr off)
+                  -- (\_ _ _ off -> Just <$> LLVM.ptrAdd sym W.knownNat base_ptr off)
+                  -- (\_ _ base off -> return $ Just $ LLVM.LLVMPointer base off)
+                  (\sym' mem' base off ->
+                    MSM.mapRegionPointers mapped_memory sym' mem' base off >>= \case
+                      Just ptr -> return $ Just ptr
+                      Nothing -> return $ Just $ LLVM.LLVMPointer base off)
                  (MS.LookupFunctionHandle $ \_ _ _ -> undefined)
            k $ RefinementContext
              { symbolicBackend = sym
@ -437,7 +444,8 @@ withDefaultRefinementContext k = do
              , nonceGenerator = nonce_gen
              , extensionImpl = ext_impl
              , memVar = mem_var
-              , mem = initialized_mem
+              -- , mem = empty_mem
+              , mem = mem
              }
        Nothing -> fail $ "unsupported architecture"

@ -465,53 +473,65 @@ initRegs
  => MS.ArchVals arch
  -> sym
  -> C.RegValue sym (LLVM.LLVMPointerType (MC.ArchAddrWidth arch))
+  -> C.RegValue sym (LLVM.LLVMPointerType (MC.ArchAddrWidth arch))
  -> m (C.RegMap sym (MS.MacawFunctionArgs arch))
-initRegs arch_vals sym ip_val = do
+initRegs arch_vals sym ip_val sp_val = do
  let reg_types = MS.crucArchRegTypes $ MS.archFunctions $ arch_vals
  reg_vals <- Ctx.traverseWithIndex (freshSymVar sym "reg") reg_types
  let reg_struct = C.RegEntry (C.StructRepr reg_types) reg_vals
  return $ C.RegMap $ Ctx.singleton $
-    (MS.updateReg arch_vals) reg_struct MC.ip_reg ip_val
+    (MS.updateReg arch_vals)
+      ((MS.updateReg arch_vals) reg_struct MC.ip_reg ip_val)
+      MC.sp_reg
+      sp_val

 smtSolveTransfer
-  :: forall arch t solver fp m
-   . ( MS.SymArchConstraints arch
+  :: ( MS.SymArchConstraints arch
+     , 16 <= MC.ArchAddrWidth arch
     , C.IsSymInterface (C.OnlineBackend t solver fp)
     , W.OnlineSolver t solver
     , MonadIO m
     )
  => RefinementContext arch t solver fp
  -> DiscoveryState arch
-  -> [[Some (ParsedBlock arch)]]
+  -> [ParsedBlock arch ids]
  -> m [ArchSegmentOff arch]
-smtSolveTransfer rc ds blockPaths =
-  -- wrong thing: fix the handling of blockPaths
-  smtSolveTransfer' rc ds $ head $ head blockPaths
+smtSolveTransfer RefinementContext{..} discovery_state blocks = do
+  let ?ptrWidth = W.knownNat

-smtSolveTransfer'
-  :: forall arch t solver fp m
-   . ( MS.SymArchConstraints arch
-     , C.IsSymInterface (C.OnlineBackend t solver fp)
-     , W.OnlineSolver t solver
-     , MonadIO m
-     )
-  => RefinementContext arch t solver fp
-  -> DiscoveryState arch
-  -> Some (ParsedBlock arch)
-  -> m [ArchSegmentOff arch]
-smtSolveTransfer' RefinementContext{..} discovery_state (Some block) = do
-  let arch = Proxy @arch
-  block_ip_val <- case MC.segoffAsAbsoluteAddr (pblockAddr block) of
+  let Right stack_name = W.userSymbol "stack"
+  stack_array <- liftIO $ W.freshConstant symbolicBackend stack_name C.knownRepr
+  stack_size <- liftIO $ W.bvLit symbolicBackend ?ptrWidth $ 2 * 1024 * 1024
+  (stack_base_ptr, mem1) <- liftIO $ LLVM.doMalloc
+    symbolicBackend
+    LLVM.StackAlloc
+    LLVM.Mutable
+    "stack_alloc"
+    mem
+    stack_size
+    LLVM.noAlignment
+
+  mem2 <- liftIO $ LLVM.doArrayStore
+    symbolicBackend
+    mem1
+    stack_base_ptr
+    LLVM.noAlignment
+    stack_array
+    stack_size
+  init_sp_val <- liftIO $ LLVM.ptrAdd symbolicBackend C.knownRepr stack_base_ptr stack_size
+
+  entry_ip_val <- case MC.segoffAsAbsoluteAddr $ pblockAddr $ head blocks of
    Just addr -> liftIO $ LLVM.llvmPointer_bv symbolicBackend
      =<< W.bvLit symbolicBackend W.knownNat (fromIntegral addr)
-    Nothing -> fail $ "unexpected block address: " ++ show (pblockAddr block)
-  init_regs <- initRegs archVals symbolicBackend block_ip_val
+    Nothing ->
+      fail $ "unexpected block address: " ++ show (pblockAddr $ head blocks)
+  init_regs <- initRegs archVals symbolicBackend entry_ip_val init_sp_val
  some_cfg <- liftIO $ stToIO $ MS.mkBlockPathCFG
    (MS.archFunctions archVals)
    handleAllocator
    Map.empty
    (W.BinaryPos "" . maybe 0 fromIntegral . MC.segoffAsAbsoluteAddr)
-    block
+    blocks
  case some_cfg of
    C.SomeCFG cfg -> do
      let sim_context = C.initSimContext
@ -522,7 +542,7 @@ smtSolveTransfer' RefinementContext{..} discovery_state (Some block) = do
            C.emptyHandleMap
            extensionImpl
            MS.MacawSimulatorState
-      let global_state = C.insertGlobal memVar mem C.emptyGlobals
+      let global_state = C.insertGlobal memVar mem2 C.emptyGlobals
      let simulation = C.regValue <$> C.callCFG cfg init_regs
      let handle_return_type = C.handleReturnType $ C.cfgHandle cfg
      let initial_state = C.InitialState
--- a/refinement/tests/RefinementTests.hs
+++ b/refinement/tests/RefinementTests.hs
@ -265,7 +265,7 @@ withBinaryDiscoveredInfo testinp useRefinement expFile arch_info bin = do
  let baseCFG = MD.cfgFromAddrs arch_info (memoryImage bin) M.empty entries []
      actualBase = cfgToExpected testinp bin (Just baseCFG) Nothing
  if useRefinement
-    then do refinedCFG <- refineDiscovery baseCFG
+    then do refinedCFG <- refineDiscovery bin baseCFG
            let refinedBase = cfgToExpected testinp bin Nothing (Just refinedCFG)
            compareToExpected "refined" refinedBase expFile
    else compareToExpected "base" actualBase expFile
--- a/symbolic/src/Data/Macaw/Symbolic.hs
+++ b/symbolic/src/Data/Macaw/Symbolic.hs
@ -378,7 +378,7 @@ termStmtToJump sl addr = sl { M.stmtsTerm = tm }
  where
    tm :: M.ParsedTermStmt arch ids
    tm = case M.stmtsTerm sl of
-      tm0@M.ParsedJump{} -> tm0
+      M.ParsedJump r _ -> M.ParsedJump r addr
      M.ParsedCall r _ -> M.ParsedJump r addr
      M.ParsedReturn r -> M.ParsedJump r addr
      M.ParsedLookupTable r _ _ -> M.ParsedJump r addr
@ -586,12 +586,12 @@ mkBlockPathCFG
  -- ^ Map from region indices to their address
  -> (M.ArchSegmentOff arch -> C.Position)
  -- ^ Function that maps function address to Crucible position
-  -> M.ParsedBlock arch ids
+  -> [M.ParsedBlock arch ids]
  -- ^ Block to translate
  -> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
 mkBlockPathCFG arch_fns halloc mem_base_var_map pos_fn blocks =
  toCoreCFG arch_fns <$>
-    mkParsedBlockRegCFG arch_fns halloc mem_base_var_map pos_fn blocks
+    mkBlockPathRegCFG arch_fns halloc mem_base_var_map pos_fn blocks

 -- | Translate a macaw function (passed as a 'M.DiscoveryFunInfo') into a
 -- registerized Crucible CFG
--- a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
@ -4,6 +4,7 @@ Maintainer       : Joe Hendrix <jhendrix@galois.com>

 This defines the core operations for mapping from Reopt to Crucible.
 -}
+{-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
@ -13,6 +14,7 @@ This defines the core operations for mapping from Reopt to Crucible.
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PolyKinds #-}
@ -74,6 +76,7 @@ module Data.Macaw.Symbolic.CrucGen
  ) where

 import           Control.Lens hiding (Empty, (:>))
+import           Control.Monad ( foldM )
 import           Control.Monad.Except
 import           Control.Monad.ST
 import           Control.Monad.State.Strict
@ -92,6 +95,7 @@ import           Data.Parameterized.Map (MapF)
 import qualified Data.Parameterized.Map as MapF
 import           Data.Parameterized.NatRepr
 import           Data.Parameterized.Nonce (Nonce, NonceGenerator, freshNonce)
+import           Data.Parameterized.Pair
 import           Data.Parameterized.Some
 import qualified Data.Parameterized.TH.GADT as U
 import           Data.Parameterized.TraversableF
@ -180,6 +184,10 @@ data MacawSymbolicArchFunctions arch
    :: !(forall a . ((M.RegisterInfo (M.ArchReg arch), MacawArchConstraints arch) => a) -> a)
  , crucGenRegAssignment :: !(Ctx.Assignment (M.ArchReg arch) (ArchRegContext arch))
    -- ^ Map from indices in the ArchRegContext to the associated register.
+  , crucGenRegStructType :: !(C.TypeRepr (ArchRegStruct arch))
+    -- ^ Type of structure with arch regs.  This can be computed from
+    -- @crucGenRegAssignment@, but is cached here to save memory (A
+    -- LOT of memory---TypeReprs were dominating the heap).
  , crucGenArchRegName :: !(forall tp . M.ArchReg arch tp -> C.SolverSymbol)
    -- ^ Provides a solver name to use for referring to register.
  , crucGenArchFn :: !(forall ids h s tp
@ -204,8 +212,8 @@ crucGenAddrWidth fns =
 crucArchRegTypes
  :: MacawSymbolicArchFunctions arch
  -> Assignment C.TypeRepr (MacawCrucibleRegTypes arch)
-crucArchRegTypes arch_fns = crucGenArchConstraints arch_fns $
-  typeCtxToCrucible $ fmapFC M.typeRepr $ crucGenRegAssignment arch_fns
+crucArchRegTypes arch_fns = case crucGenRegStructType arch_fns of
+  C.StructRepr tps -> tps

 ------------------------------------------------------------------------
 -- MacawExprExtension
@ -550,14 +558,52 @@ data CrucGenState arch ids h s
     -- ^ Label for this block we are translating
   , codeOff    :: !(M.ArchAddrWord arch)
     -- ^ Offset
+   , codePos    :: !C.Position
+     -- ^ Position (cached from 'codeOff')
   , prevStmts  :: ![C.Posd (CR.Stmt (MacawExt arch) s)]
     -- ^ List of states in reverse order
+   , toBitsCache :: !(MapF (PtrAtom s) (BVAtom s))
+   , fromBitsCache :: !(MapF (BVAtom s) (PtrAtom s))
   }

+newtype PtrAtom s w = PtrAtom { getPtrAtom :: CR.Atom s (MM.LLVMPointerType w) }
+
+instance TestEquality (PtrAtom s) where
+  testEquality x y =
+    testEquality (getPtrAtom x) (getPtrAtom y) <&> \Refl -> Refl
+
+instance OrdF (PtrAtom s) where
+  compareF x y =
+    case compareF (getPtrAtom x) (getPtrAtom y) of
+      LTF -> LTF
+      EQF -> EQF
+      GTF -> GTF
+
+newtype BVAtom s w = BVAtom { getBVAtom :: CR.Atom s (C.BVType w) }
+
+instance TestEquality (BVAtom s) where
+  testEquality x y =
+    testEquality (getBVAtom x) (getBVAtom y) <&> \Refl -> Refl
+
+instance OrdF (BVAtom s) where
+  compareF x y =
+    case compareF (getBVAtom x) (getBVAtom y) of
+      LTF -> LTF
+      EQF -> EQF
+      GTF -> GTF
+
 crucPStateLens ::
  Simple Lens (CrucGenState arch ids h s) (CrucPersistentState ids h s)
 crucPStateLens = lens crucPState (\s v -> s { crucPState = v })

+toBitsCacheLens ::
+  Simple Lens (CrucGenState arch ids h s) (MapF (PtrAtom s) (BVAtom s))
+toBitsCacheLens = lens toBitsCache (\s v -> s { toBitsCache = v })
+
+fromBitsCacheLens ::
+  Simple Lens (CrucGenState arch ids h s) (MapF (BVAtom s) (PtrAtom s))
+fromBitsCacheLens = lens fromBitsCache (\s v -> s { fromBitsCache = v })
+
 assignValueMapLens ::
  Simple Lens (CrucPersistentState ids h s)
              (MapF (M.AssignId ids) (MacawCrucibleValue (CR.Atom s)))
@ -585,7 +631,7 @@ instance Functor (CrucGen arch ids h s) where

 instance Applicative (CrucGen arch ids h s) where
  {-# INLINE pure #-}
-  pure r = CrucGen $ \s cont -> cont s r
+  pure !r = CrucGen $ \s cont -> cont s r
  {-# INLINE (<*>) #-}
  mf <*> ma = CrucGen $ \s0 cont -> unCrucGen mf s0
                      $ \s1 f -> unCrucGen ma s1
@ -608,15 +654,16 @@ archAddrWidth = crucGenAddrWidth . translateFns <$> get

 -- | Get current position
 getPos :: CrucGen arch ids h s C.Position
-getPos = gets $ \s -> macawPositionFn s (codeOff s)
+getPos = gets codePos

 addStmt :: CR.Stmt (MacawExt arch) s -> CrucGen arch ids h s ()
 addStmt stmt = seq stmt $ do
  p <- getPos
  s <- get
  let pstmt = C.Posd p stmt
-  seq pstmt $ do
-  put $! s { prevStmts = pstmt : prevStmts s }
+  let prev = prevStmts s
+  seq pstmt $ seq prev $ do
+  put $! s { prevStmts = pstmt : prev }

 addTermStmt :: CR.TermStmt s (MacawFunctionResult arch)
            -> CrucGen arch ids h s a
@ -654,10 +701,11 @@ evalAtom av = do
  p <- getPos
  i <- freshValueIndex
  -- Make atom
+  let !tp = CR.typeOfAtomValue av
  let atom = CR.Atom { CR.atomPosition = p
                     , CR.atomId = i
                     , CR.atomSource = CR.Assigned
-                     , CR.typeOfAtom = CR.typeOfAtomValue av
+                     , CR.typeOfAtom = tp
                     }
  addStmt $ CR.DefineAtom atom av
  pure $! atom
@ -676,7 +724,15 @@ toBits ::
  NatRepr w ->
  CR.Atom s (MM.LLVMPointerType w) ->
  CrucGen arch ids h s (CR.Atom s (C.BVType w))
-toBits w x = evalMacawExt (PtrToBits w x)
+toBits w x =
+  use (toBitsCacheLens . atF (PtrAtom x)) >>= \case
+    Just (BVAtom x') ->
+      return x'
+    Nothing -> do
+      x' <- evalMacawExt (PtrToBits w x)
+      assign (toBitsCacheLens . atF (PtrAtom x)) (Just (BVAtom x'))
+      assign (fromBitsCacheLens . atF (BVAtom x')) (Just (PtrAtom x))
+      return x'

 -- | Treat a bit-vector as a register value.
 fromBits ::
@ -684,7 +740,15 @@ fromBits ::
  NatRepr w ->
  CR.Atom s (C.BVType w) ->
  CrucGen arch ids h s (CR.Atom s (MM.LLVMPointerType w))
-fromBits w x = evalMacawExt (BitsToPtr w x)
+fromBits w x =
+  use (fromBitsCacheLens . atF (BVAtom x)) >>= \case
+    Just (PtrAtom x') ->
+      return x'
+    Nothing -> do
+      x' <- evalMacawExt (BitsToPtr w x)
+      assign (fromBitsCacheLens . atF (BVAtom x)) (Just (PtrAtom x'))
+      assign (toBitsCacheLens . atF (PtrAtom x')) (Just (BVAtom x))
+      return x'

 getRegs :: CrucGen arch ids h s (CR.Atom s (ArchRegStruct arch))
 getRegs = gets crucRegisterReg >>= evalAtom . CR.ReadReg
@ -701,9 +765,8 @@ getRegValue r = do
    Just idx -> do
      reg <- gets crucRegisterReg
      regStruct <- evalAtom (CR.ReadReg reg)
-      let tp = M.typeRepr (crucGenRegAssignment archFns Ctx.! macawIndex idx)
-      crucibleValue (C.GetStruct regStruct (crucibleIndex idx)
-                    (typeToCrucible tp))
+      let tp = crucArchRegTypes archFns Ctx.! crucibleIndex idx
+      crucibleValue (C.GetStruct regStruct (crucibleIndex idx) tp)

 v2c :: M.Value arch ids tp
    -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp))
@ -1077,7 +1140,9 @@ addMacawStmt baddr stmt =
      void $ evalMacawStmt (MacawWriteMem w repr caddr cval)
    M.InstructionStart off t -> do
      -- Update the position
-      modify $ \s -> s { codeOff = off }
+      modify' $ \s -> s { codeOff = off
+                        , codePos = macawPositionFn s off
+                        }
      let crucStmt :: MacawStmtExtension arch (CR.Atom s) C.UnitType
          crucStmt = MacawInstructionStart baddr off t
      void $ evalMacawStmt crucStmt
@ -1107,21 +1172,37 @@ createRegStruct :: forall arch ids h s
                .  M.RegState (M.ArchReg arch) (M.Value arch ids)
                -> CrucGen arch ids h s (CR.Atom s (ArchRegStruct arch))
 createRegStruct regs = do
-  (tps, fields) <- createRegStructAssignment regs
-  crucibleValue (C.MkStruct tps fields)
-
-createRegStructAssignment :: forall arch ids h s
-                           .  M.RegState (M.ArchReg arch) (M.Value arch ids)
-                          -> CrucGen arch ids h s (C.CtxRepr (CtxToCrucibleType (ArchRegContext arch)),
-                                                 Assignment (CR.Atom s) (CtxToCrucibleType (ArchRegContext arch)))
-createRegStructAssignment regs = do
  archFns <- gets translateFns
+
+  -- IMPORTANT: The registers are never changed in the middle of the
+  -- block, ONLY at the ends.  So 'startingVals' will have the value
+  -- of each register as it was at the beginning of the block.
+  startingVals <- do
+    regReg <- gets crucRegisterReg
+    evalAtom (CR.ReadReg regReg)
+
+  let addUpdate vals (Pair idx val) = do
+        let tps = crucArchRegTypes archFns
+        crucibleValue $ C.SetStruct tps vals idx val
+
+  updates <- createRegUpdates regs
+  foldM addUpdate startingVals updates
+
+createRegUpdates :: forall arch ids h s
+                 .  M.RegState (M.ArchReg arch) (M.Value arch ids)
+                 -> CrucGen arch ids h s
+                      [Pair (Ctx.Index (MacawCrucibleRegTypes arch)) (CR.Atom s)]
+createRegUpdates regs = do
+  archFns <- gets translateFns
+  idxMap <- gets crucRegIndexMap
  crucGenArchConstraints archFns $ do
-  let regAssign = crucGenRegAssignment archFns
-  let tps = fmapFC M.typeRepr regAssign
-  let a = fmapFC (\r -> regs ^. M.boundValue r) regAssign
-  fields <- macawAssignToCrucM valueToCrucible a
-  return (typeCtxToCrucible tps, fields)
+    fmap catMaybes $ forM (M.regStateMap regs & MapF.toList) $ \(Pair reg val) ->
+      case val of
+        M.Initial _ ->
+          return Nothing
+        _ -> case MapF.lookup reg idxMap of
+          Nothing -> fail "internal: Register is not bound."
+          Just idx -> Just . Pair (crucibleIndex idx) <$> valueToCrucible val

 addMacawTermStmt :: Map Word64 (CR.Label s)
                    -- ^ Map from block index to Crucible label
@ -1190,7 +1271,10 @@ runCrucGen archFns baseAddrMap posFn off lbl regReg action = crucGenArchConstrai
                        , macawPositionFn = posFn
                        , blockLabel = lbl
                        , codeOff    = off
+                        , codePos    = posFn off
                        , prevStmts  = []
+                        , toBitsCache = MapF.empty
+                        , fromBitsCache = MapF.empty
                        }
  let cont _s () = fail "Unterminated crucible block"
  (s, tstmt)  <- mmExecST $ unCrucGen action s0 cont
@ -1249,6 +1333,8 @@ parsedBlockLabel blockLabelMap addr idx =
  fromMaybe (error $ "Could not find entry point: " ++ show addr) $
  Map.lookup (addr, idx) blockLabelMap

+-- | DO NOT CALL THIS FROM USER CODE.  We count on the registers not
+-- changing until the end of the block.
 setMachineRegs :: CR.Atom s (ArchRegStruct arch) -> CrucGen arch ids h s ()
 setMachineRegs newRegs = do
  regReg <- gets crucRegisterReg
@ -1268,8 +1354,8 @@ addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
 crucGenArchConstraints archFns $ do
  case tstmt of
    M.ParsedCall regs mret -> do
-      (tps, fields) <- createRegStructAssignment regs
-      curRegs <- crucibleValue (C.MkStruct tps fields)
+      curRegs <- createRegStruct regs
+      let tps = typeCtxToCrucible $ fmapFC M.typeRepr $ crucGenRegAssignment archFns
      fh <- evalMacawStmt (MacawLookupFunctionHandle (crucArchRegTypes archFns) curRegs)
      newRegs <- evalAtom $ CR.Call fh (Ctx.singleton curRegs) (C.StructRepr tps)
      case mret of
--- a/symbolic/src/Data/Macaw/Symbolic/Memory.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/Memory.hs
@ -97,15 +97,16 @@ module Data.Macaw.Symbolic.Memory (

 import           GHC.TypeLits

+import           Control.Monad
 import           Control.Monad.IO.Class ( MonadIO, liftIO )
 import qualified Data.ByteString as BS
 import qualified Data.Foldable as F
 import qualified Data.IntervalMap.Strict as IM
 import qualified Data.Map.Strict as Map
 import           Data.Semigroup
-import qualified Data.Vector as V

 import qualified Data.Parameterized.NatRepr as PN
+import qualified Data.Parameterized.Context as Ctx
 import qualified Data.Macaw.CFG as MC
 import qualified Data.Macaw.Memory.Permissions as MMP
 import qualified Lang.Crucible.Backend as CB
@ -120,6 +121,7 @@ import qualified Data.Macaw.Symbolic as MS

 import Prelude

+import Debug.Trace

 -- | A configuration knob controlling how the initial contents of the memory
 -- model are populated
@ -217,32 +219,21 @@ populateMemory :: ( CB.IsSymInterface sym
               -- ^ The initial memory model (e.g., it might have a stack allocated)
               -> m (CL.MemImpl sym, IM.IntervalMap (MC.MemWord (MC.ArchAddrWidth arch)) (Allocation sym (MC.ArchAddrWidth arch)))
 populateMemory _ sym mmc mem memImpl0 = do
-  memImpl1 <- pleatM (memImpl0, IM.empty) (MC.memSegments mem) $ \impl1 seg -> do
-    pleatM impl1 (MC.relativeSegmentContents [seg]) $ \impl2 (addr, memChunk) ->
-      case memChunk of
-        MC.RelocationRegion {} -> error ("SymbolicRef SegmentRanges are not supported yet: " ++ show memChunk)
-        MC.BSSRegion sz -> do
-          nzero <- liftIO $ WI.natLit sym 0
-          bvzero <- liftIO $ WI.bvLit sym (PN.knownNat @8) 0
-          let val = CL.LLVMValArray (CL.bitvectorType 1) (V.fromList (replicate (fromIntegral sz) (CL.LLVMValInt nzero bvzero)))
-          addValueAt sym mmc mem seg addr sz val impl2
-        MC.ByteRegion bytes -> do
-          let sz = BS.length bytes
-          nzero <- liftIO $ WI.natLit sym 0
-          let fromWord8 w = do
-                llw <- liftIO $ WI.bvLit sym (PN.knownNat @8) (fromIntegral w)
-                return (CL.LLVMValInt nzero llw)
-          llvmWords <- mapM fromWord8 (BS.unpack bytes)
-          let val = CL.LLVMValArray (CL.bitvectorType 1) (V.fromList llvmWords)
-          addValueAt sym mmc mem seg addr sz val impl2
-  return memImpl1
+  pleatM (memImpl0, IM.empty) (MC.memSegments mem) $ \impl1 seg -> do
+    pleatM impl1 (MC.relativeSegmentContents [seg]) $ \impl2 (addr, memChunk) -> do
+      bytes <- case memChunk of
+        MC.RelocationRegion {} -> error $
+          "SymbolicRef SegmentRanges are not supported yet: " ++ show memChunk
+        MC.BSSRegion sz -> liftIO $
+          replicate (fromIntegral sz) <$> WI.bvLit sym PN.knownNat 0
+        MC.ByteRegion bytes -> liftIO $
+          mapM (WI.bvLit sym PN.knownNat . fromIntegral) $ BS.unpack bytes
+      addSegment sym mmc mem seg addr bytes impl2

 -- | Add a new value (which is an LLVM array of bytes) of a given length at the given address.
-addValueAt :: ( 16 <= w
+addSegment :: ( 16 <= w
              , MC.MemWidth w
              , KnownNat w
-              , Integral a
-              , Show a
              , CB.IsSymInterface sym
              , MonadIO m
              )
@ -251,39 +242,63 @@ addValueAt :: ( 16 <= w
           -> MC.Memory w
           -> MC.MemSegment w
           -> MC.MemAddr w
-           -> a
-           -> CL.LLVMVal sym
+           -> [WI.SymBV sym 8]
           -> (CL.MemImpl sym, IM.IntervalMap (MC.MemWord w) (Allocation sym w))
           -> m (CL.MemImpl sym, IM.IntervalMap (MC.MemWord w) (Allocation sym w))
-addValueAt sym mmc mem seg addr sz val (impl, ptrtable) = do
+addSegment sym mmc mem seg addr bytes (impl, ptrtable) = do
  -- We only support statically-linked binaries for now, so fail if we have a
  -- segment-relative address (which should only occur for an object file or
  -- shared library)
-  let Just absAddr = MC.asAbsoluteAddr addr
-  let ty = CL.arrayType (fromIntegral sz) (CL.bitvectorType 1)
-  szVal <- liftIO $ WI.bvLit sym (MC.memWidth mem) (fromIntegral sz)
  let ?ptrWidth = MC.memWidth mem
-  let interval = IM.IntervalCO absAddr (absAddr + fromIntegral sz)
-  case MMP.isReadonly (MC.segmentFlags seg) of
-    True -> do
-      (ptr, impl1) <- liftIO $ CL.doMalloc sym CL.GlobalAlloc CL.Immutable ("Read only memory at " ++ show addr) impl szVal CLD.noAlignment
-      let alloc = Allocation { allocationPtr = ptr, allocationBase = absAddr }
-      impl2 <- liftIO $ CL.storeConstRaw sym impl1 ptr ty CLD.noAlignment val
-      return (impl2, IM.insert interval alloc ptrtable)
-    False ->
-      case mmc of
-        ConcreteMutable -> do
-          (ptr, impl1) <- liftIO $ CL.doMalloc sym CL.GlobalAlloc CL.Mutable ("Mutable (concrete) memory at " ++ show addr) impl szVal CLD.noAlignment
-          let alloc = Allocation { allocationPtr = ptr, allocationBase = absAddr }
-          impl2 <- liftIO $ CL.storeRaw sym impl1 ptr ty CLD.noAlignment val
-          return (impl2, IM.insert interval alloc ptrtable)
-        SymbolicMutable -> do
-          let Right alloc_name = WI.userSymbol ("symbolicAllocBytes_" <> show addr)
-          array <- liftIO $ WI.freshConstant sym alloc_name CT.knownRepr
-          (ptr, impl1) <- liftIO $ CL.doMalloc sym CL.GlobalAlloc CL.Mutable ("Mutable (symbolic) memory at " ++ show addr) impl szVal CLD.noAlignment
-          let alloc = Allocation { allocationPtr = ptr, allocationBase = absAddr }
-          impl2 <- liftIO $ CL.doArrayStore sym impl1 ptr CLD.noAlignment array szVal
-          return (impl2, IM.insert interval alloc ptrtable)
+  let Just abs_addr = MC.asAbsoluteAddr addr
+  let size = length bytes
+  let interval = IM.IntervalCO abs_addr (abs_addr + fromIntegral size)
+  let (store_fn, mut_flag, conc_flag, desc) =
+        case MMP.isReadonly (MC.segmentFlags seg) of
+          True ->
+            ( CL.doArrayConstStore
+            , CL.Immutable
+            , True
+            , "Mutable (concrete) memory at " ++ show addr
+            )
+          False -> case mmc of
+            ConcreteMutable ->
+              ( CL.doArrayStore
+              , CL.Mutable
+              , True
+              , "Mutable (concrete) memory at " ++ show addr
+              )
+            SymbolicMutable ->
+              ( CL.doArrayStore
+              , CL.Mutable
+              , False
+              , "Mutable (symbolic) memory at " ++ show addr
+              )
+  let Right alloc_name = WI.userSymbol ("symbolicAllocBytes_" <> show addr)
+  array <- liftIO $ WI.freshConstant sym alloc_name CT.knownRepr
+  size_bv <- liftIO $ WI.bvLit sym (MC.memWidth mem) (fromIntegral size)
+  when conc_flag $
+    F.forM_ (zip [0 .. size - 1] bytes) $ \(idx, byte) -> do
+      index_bv <- liftIO $ WI.bvLit sym (MC.memWidth mem) (fromIntegral idx)
+      eq_pred <- liftIO $ WI.bvEq sym byte
+        =<< WI.arrayLookup sym array (Ctx.singleton index_bv)
+      prog_loc <- liftIO $ WI.getCurrentProgramLoc sym
+      liftIO $ CB.addAssumption sym $
+        CB.LabeledPred eq_pred $ CB.AssumptionReason prog_loc desc
+  (ptr, impl1) <- liftIO $ CL.doMalloc
+    sym
+    CL.GlobalAlloc
+    mut_flag
+    desc
+    impl
+    size_bv
+    CLD.noAlignment
+  let alloc = Allocation
+        { allocationPtr = ptr
+        , allocationBase = abs_addr
+        }
+  impl2 <- liftIO $ store_fn sym impl1 ptr CLD.noAlignment array size_bv
+  return (impl2, IM.insert interval alloc ptrtable)

 -- | The 'pleatM' function is 'foldM' with the arguments switched so
 -- that the function is last.
--- a/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
@ -208,7 +208,7 @@ mkRegIndexMap (a :> r) csz =
 -- Misc types

 -- | A Crucible value with a Macaw type.
-data MacawCrucibleValue f tp = MacawCrucibleValue (f (ToCrucibleType tp))
+newtype MacawCrucibleValue f tp = MacawCrucibleValue (f (ToCrucibleType tp))

 instance FunctorFC MacawCrucibleValue where
  fmapFC f (MacawCrucibleValue v) = MacawCrucibleValue (f v)
--- a/x86/src/Data/Macaw/X86/Generator.hs
+++ b/x86/src/Data/Macaw/X86/Generator.hs
@ -20,6 +20,7 @@ module Data.Macaw.X86.Generator
  , runX86Generator
  , X86GCont
  , addStmt
+  , addTermStmt
  , addArchStmt
  , addArchTermStmt
  , asAtomicStateUpdate
@ -335,13 +336,16 @@ addArchStmt = addStmt . ExecArchStmt

 -- | execute a primitive instruction.
 addArchTermStmt :: X86TermStmt ids -> X86Generator st ids ()
-addArchTermStmt ts = do
+addArchTermStmt ts = addTermStmt (ArchTermStmt ts)
+
+-- | Terminate the current block immediately
+--
+-- This can be used to signal an error (e.g., by using the TranslateError terminator)
+addTermStmt :: (RegState (ArchReg X86_64) (Value X86_64 ids) -> TermStmt X86_64 ids) -> X86Generator st ids a
+addTermStmt ts =
  X86G $ ContT $ \_ -> ReaderT $ \s0 -> do
-    -- Get last block.
    let p_b = s0 ^. blockState
-    -- Create finished block.
-    let fin_b = finishBlock p_b $ ArchTermStmt ts
-    -- Return early
+    let fin_b = finishBlock p_b ts
    return $! FinishedPartialBlock fin_b

 -- | Are we in AVX mode?
--- a/x86/src/Data/Macaw/X86/Getters.hs
+++ b/x86/src/Data/Macaw/X86/Getters.hs
@ -51,10 +51,12 @@ module Data.Macaw.X86.Getters
 import           Control.Lens ((&))
 import           Data.Parameterized.NatRepr
 import           Data.Parameterized.Some
+import qualified Data.Text as T
 import qualified Flexdis86 as F
 import           GHC.TypeLits (KnownNat)

 import           Data.Macaw.CFG
+import           Data.Macaw.CFG.Block ( TermStmt(TranslateError) )
 import           Data.Macaw.Types
 import           Data.Macaw.X86.Generator
 import           Data.Macaw.X86.Monad
@ -389,7 +391,10 @@ getCallTarget v =
    F.JumpOffset _ joff -> do
      s <- getState
      pure $! resolveJumpOffset s joff
-    _ -> fail "Unexpected argument"
+    _ -> do
+      ipVal <- eval =<< get rip
+      let msg = "Data.Macaw.X86.Getters.getCallTarget: Unexpected argument: " ++ show v ++ " at " ++ show ipVal
+      addTermStmt (\regs -> TranslateError regs (T.pack msg))

 -- | Return the target of a call or jump instruction.
 doJump :: Expr ids BoolType -> F.Value -> X86Generator st ids ()
@ -413,7 +418,10 @@ doJump cond v =
      rip .= ipVal
    F.QWordImm w -> do
      modify rip $ mux cond $ bvKLit (toInteger w)
-    _ -> fail "Unexpected argument"
+    _ -> do
+      ipVal <- eval =<< get rip
+      let msg = "Data.Macaw.X86.Getters.doJump: Unexpected argument: " ++ show v ++ " at " ++ show ipVal
+      addTermStmt (\regs -> TranslateError regs (T.pack msg))

 ------------------------------------------------------------------------
 -- Standard memory values
--- a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
+++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
@ -145,6 +145,10 @@ x86RegAssignment =
  <++> (repeatAssign (M.X86_YMMReg . F.ymmReg . fromIntegral) :: Assignment M.X86Reg (CtxRepeat 16 (M.BVType 256)))


+x86RegStructType :: C.TypeRepr (ArchRegStruct M.X86_64)
+x86RegStructType =
+  C.StructRepr (typeCtxToCrucible $ fmapFC M.typeRepr x86RegAssignment)
+
 regIndexMap :: RegIndexMap M.X86_64
 regIndexMap = mkRegIndexMap x86RegAssignment
            $ Ctx.size $ crucArchRegTypes x86_64MacawSymbolicFns
@ -306,6 +310,7 @@ x86_64MacawSymbolicFns =
  MacawSymbolicArchFunctions
  { crucGenArchConstraints = \x -> x
  , crucGenRegAssignment = x86RegAssignment
+  , crucGenRegStructType = x86RegStructType
  , crucGenArchRegName  = x86RegName
  , crucGenArchFn = crucGenX86Fn
  , crucGenArchStmt = crucGenX86Stmt