Add a new macaw statement to record updates to machine registers

The new statement is called `ArchState`, and has two fields: an address and a
map.  The address is the address of the instruction it is standing in for.  The
map contains a mapping from the *machine registers* that the instruction updated
to the *macaw values* that were assigned to those locations.

This is useful metadata for debugging, but is also required to do some types of
architecture-independent analysis (where we can still reason about machine
register contents).

base/src/Data/Macaw/Analysis/FunctionArgs.hs

@@ -485,6 +485,7 @@ stmtDemandedValues ctx stmt = demandConstraints ctx $
     -- Comment statements have no specific value.
     Comment _ -> []
     ExecArchStmt astmt -> foldMapF (\v -> [Some v]) astmt
+    ArchState _addr assn -> foldMapF (\v -> [Some v]) assn
 
 -- | This function figures out what the block requires
 -- (i.e., addresses that are stored to, and the value stored), along

base/src/Data/Macaw/CFG/Core.hs

@@ -779,6 +779,10 @@ data Stmt arch ids
      -- ^ A user-level comment
    | ExecArchStmt !(ArchStmt arch (Value arch ids))
      -- ^ Execute an architecture specific statement
+   | ArchState !(ArchAddrWord arch) !(MapF.MapF (ArchReg arch) (Value arch ids))
+     -- ^ Address of an instruction and the *machine* registers that it updates
+     -- (with their associated macaw values after the execution of the
+     -- instruction).
 
 ppStmt :: ArchConstraints arch
        => (ArchAddrWord arch -> Doc)
@@ -795,6 +799,10 @@ ppStmt ppOff stmt =
     InstructionStart off mnem -> text "#" <+> ppOff off <+> text (Text.unpack mnem)
     Comment s -> text $ "# " ++ Text.unpack s
     ExecArchStmt s -> ppArchStmt (ppValue 10) s
+    ArchState a m -> hang (length (show prefix)) (prefix PP.<> vcat (MapF.foldrWithKey ppUpdate [] m))
+      where
+      prefix = text "#" <+> ppOff a PP.<> text ": "
+      ppUpdate key val acc = text (showF key) <+> text ":=" <+> ppValue 0 val : acc
 
 instance ArchConstraints arch => Show (Stmt arch ids) where
   show = show . ppStmt (\w -> text (show w))

base/src/Data/Macaw/CFG/DemandSet.hs

@@ -18,6 +18,7 @@ import           Control.Monad.State.Strict
 import           Data.Parameterized.Some
 import           Data.Parameterized.TraversableF
 import           Data.Parameterized.TraversableFC
+import           Data.Parameterized.Map as MapF
 import           Data.Set (Set)
 import qualified Data.Set as Set
 
@@ -110,6 +111,8 @@ addStmtDemands s =
       ctx <- DemandComp $ gets $ demandContext
       demandConstraints ctx $
         traverseF_ addValueDemands astmt
+    ArchState _a updates ->
+      MapF.traverseWithKey_ (const addValueDemands) updates
 
 ------------------------------------------------------------------------
 -- Functions for computing demanded values
@@ -124,3 +127,4 @@ stmtNeeded demandSet stmt =
     InstructionStart{} -> True
     Comment{} -> True
     ExecArchStmt{} -> True
+    ArchState{} -> True

base/src/Data/Macaw/CFG/Rewriter.hs

@@ -440,3 +440,6 @@ rewriteStmt s =
     ExecArchStmt astmt -> do
       f <- Rewriter $ gets $ rwctxArchStmt . rwContext
       f astmt
+    ArchState addr updates -> do
+      tgtUpdates <- MapF.traverseWithKey (const rewriteValue) updates
+      appendRewrittenStmt $ ArchState addr tgtUpdates

base/src/Data/Macaw/Discovery/AbsEval.hs

@@ -86,6 +86,8 @@ absEvalStmt info stmt = withArchConstraints info $
       pure ()
     ExecArchStmt astmt ->
       modify $ \r -> absEvalArchStmt info r astmt
+    ArchState{} ->
+      pure ()
 
 -- This takes a processor state and updates it based on executing each statement.
 absEvalStmts :: ArchitectureInfo arch

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

@@ -916,6 +916,11 @@ addMacawStmt stmt =
     M.ExecArchStmt astmt -> do
       fns <- translateFns <$> get
       crucGenArchStmt fns astmt
+    M.ArchState {} -> do
+      -- FIXME: We want to translate the metadata in ArchState into equivalent
+      -- metadata in crucible.  We'll need to use a syntax extension to capture
+      -- it.
+      pure ()
 
 lookupCrucibleLabel :: Map Word64 (CR.Label s)
                        -- ^ Map from block index to Crucible label