From 372d7d72086328c3fd7648885495463779ffaca6 Mon Sep 17 00:00:00 2001
From: Jason Dagit <dagit@galois.com>
Date: Tue, 12 Dec 2017 17:27:19 -0800
Subject: [PATCH] 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 | 1 +
 base/src/Data/Macaw/CFG/Core.hs              | 8 ++++++++
 base/src/Data/Macaw/CFG/DemandSet.hs         | 4 ++++
 base/src/Data/Macaw/CFG/Rewriter.hs          | 3 +++
 base/src/Data/Macaw/Discovery/AbsEval.hs     | 2 ++
 symbolic/src/Data/Macaw/Symbolic/CrucGen.hs  | 5 +++++
 6 files changed, 23 insertions(+)

diff --git a/base/src/Data/Macaw/Analysis/FunctionArgs.hs b/base/src/Data/Macaw/Analysis/FunctionArgs.hs
index a934446b..8131c4ec 100644
--- a/base/src/Data/Macaw/Analysis/FunctionArgs.hs
+++ b/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
diff --git a/base/src/Data/Macaw/CFG/Core.hs b/base/src/Data/Macaw/CFG/Core.hs
index 83f09357..aed1af3b 100644
--- a/base/src/Data/Macaw/CFG/Core.hs
+++ b/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))
diff --git a/base/src/Data/Macaw/CFG/DemandSet.hs b/base/src/Data/Macaw/CFG/DemandSet.hs
index fcae688a..367cc336 100644
--- a/base/src/Data/Macaw/CFG/DemandSet.hs
+++ b/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
diff --git a/base/src/Data/Macaw/CFG/Rewriter.hs b/base/src/Data/Macaw/CFG/Rewriter.hs
index 4d37a355..b4d41e4e 100644
--- a/base/src/Data/Macaw/CFG/Rewriter.hs
+++ b/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
diff --git a/base/src/Data/Macaw/Discovery/AbsEval.hs b/base/src/Data/Macaw/Discovery/AbsEval.hs
index 3727e715..00a6e7c9 100644
--- a/base/src/Data/Macaw/Discovery/AbsEval.hs
+++ b/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
diff --git a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
index 7ed52824..fed723fe 100644
--- a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
+++ b/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