Introduce ParsedIte

src/Data/Macaw/Discovery.hs

@@ -519,7 +519,6 @@ parseFetchAndExecute ctx lbl stmts regs s' = do
         newFunctionAddrs %= (++ addrs)
         pure ParsedBlock { pblockLabel = lbl_idx
                          , pblockStmts = toList prev_stmts
-                         , pblockState = regs'
                          , pblockTerm  = ParsedCall s' (Just ret)
                          }
 
@@ -529,7 +528,6 @@ parseFetchAndExecute ctx lbl stmts regs s' = do
 
         pure ParsedBlock { pblockLabel = lbl_idx
                          , pblockStmts = stmts
-                         , pblockState = regs'
                          , pblockTerm = ParsedReturn s'
                          }
 
@@ -547,7 +545,6 @@ parseFetchAndExecute ctx lbl stmts regs s' = do
          intraJumpTargets %= ((tgt_addr, abst'):)
          pure ParsedBlock { pblockLabel = lbl_idx
                           , pblockStmts = stmts
-                          , pblockState = regs'
                           , pblockTerm  = ParsedJump s' tgt_addr
                           }
       -- Block ends with what looks like a jump table.
@@ -560,7 +557,6 @@ parseFetchAndExecute ctx lbl stmts regs s' = do
             mapM_ (recordWriteStmt arch_info mem regs') stmts
             pure ParsedBlock { pblockLabel = lbl_idx
                              , pblockStmts = stmts
-                             , pblockState = regs'
                              , pblockTerm  = ClassifyFailure s'
                              }
           Right read_end -> do
@@ -600,7 +596,6 @@ parseFetchAndExecute ctx lbl stmts regs s' = do
             read_addrs <- resolveJump [] 0
             pure ParsedBlock { pblockLabel = lbl_idx
                              , pblockStmts = stmts
-                             , pblockState = regs'
                              , pblockTerm = ParsedLookupTable s' jump_idx (V.fromList read_addrs)
                              }
 
@@ -622,7 +617,6 @@ parseFetchAndExecute ctx lbl stmts regs s' = do
 
         pure ParsedBlock { pblockLabel = lbl_idx
                          , pblockStmts = stmts
-                         , pblockState = regs'
                          , pblockTerm  = ParsedCall s' Nothing
                          }
 
@@ -632,11 +626,10 @@ parseFetchAndExecute ctx lbl stmts regs s' = do
           mapM_ (recordWriteStmt arch_info mem regs') stmts
           pure ParsedBlock { pblockLabel = lbl_idx
                            , pblockStmts = stmts
-                           , pblockState = regs'
                            , pblockTerm  = ClassifyFailure s'
                            }
 
--- | This evalutes the statements in a block to expand the information known
+-- | this evalutes the statements in a block to expand the information known
 -- about control flow targets of this block.
 parseBlocks :: ParseContext arch ids
                -- ^ Context for parsing blocks.
@@ -675,7 +668,6 @@ parseBlocks ctx ((b,regs):rest) = do
 
       let pb = ParsedBlock { pblockLabel = idx
                            , pblockStmts = blockStmts b
-                           , pblockState = regs'
                            , pblockTerm  = ParsedBranch c (labelIndex lb) (labelIndex rb)
                            }
       pblockMap %= Map.insert idx pb
@@ -695,7 +687,6 @@ parseBlocks ctx ((b,regs):rest) = do
           intraJumpTargets %= ((addr, post):)
           let pb = ParsedBlock { pblockLabel = idx
                                , pblockStmts = blockStmts b
-                               , pblockState = regs'
                                , pblockTerm  = ParsedSyscall s' addr
                                }
           pblockMap %= Map.insert idx pb
@@ -710,10 +701,8 @@ parseBlocks ctx ((b,regs):rest) = do
 
     -- Do nothing when this block ends in a translation error.
     TranslateError _ msg -> do
-      let regs' = absEvalStmts arch_info regs (blockStmts b)
       let pb = ParsedBlock { pblockLabel = idx
                            , pblockStmts = blockStmts b
-                           , pblockState = regs'
                            , pblockTerm = ParsedTranslateError msg
                            }
       pblockMap %= Map.insert idx pb

src/Data/Macaw/Discovery/State.hs

@@ -189,6 +189,8 @@ data ParsedTermStmt arch ids
      -- ^ A return with the given registers.
    | ParsedBranch !(Value arch ids BoolType) !Word64 !Word64
      -- ^ A branch (i.e., BlockTerm is Branch)
+   | ParsedIte !(Value arch ids BoolType) !(ParsedBlock arch ids) !(ParsedBlock arch ids)
+     -- ^ An if-then-else
    | ParsedSyscall !(RegState (ArchReg arch) (Value arch ids))
                    !(ArchSegmentedAddr arch)
      -- ^ A system call with the registers prior to call and given return address.
@@ -199,7 +201,14 @@ data ParsedTermStmt arch ids
 
 deriving instance ArchConstraints arch => Show (ParsedTermStmt arch ids)
 
-instance (OrdF (ArchReg arch), ShowF (ArchReg arch)) => Pretty (ParsedTermStmt arch ids) where
+-- | Pretty print the block contents indented inside brackets.
+ppBlockIndented :: ArchConstraints arch => ParsedBlock arch ids -> Doc
+ppBlockIndented b =
+  text "{" <$$>
+  indent 2 (vcat (pretty <$> pblockStmts b) <$$> pretty (pblockTerm b)) <$$>
+  text "}"
+
+instance ArchConstraints arch => Pretty (ParsedTermStmt arch ids) where
   pretty (ParsedCall s Nothing) =
     text "tail call" <$$>
     indent 2 (pretty s)
@@ -218,6 +227,10 @@ instance (OrdF (ArchReg arch), ShowF (ArchReg arch)) => Pretty (ParsedTermStmt a
     indent 2 (pretty s)
   pretty (ParsedBranch c t f) =
     text "branch" <+> pretty c <+> text (show t) <+> text (show f)
+  pretty (ParsedIte c t f) =
+    text "ite" <+> pretty c <$$>
+    ppBlockIndented t <$$>
+    ppBlockIndented f
   pretty (ParsedSyscall s addr) =
     text "syscall, return to" <+> text (show addr) <$$>
     indent 2 (pretty s)
@@ -233,8 +246,6 @@ instance (OrdF (ArchReg arch), ShowF (ArchReg arch)) => Pretty (ParsedTermStmt a
 data ParsedBlock arch ids
    = ParsedBlock { pblockLabel :: !Word64
                  , pblockStmts :: !([Stmt arch ids])
-                 , pblockState :: !(AbsProcessorState (ArchReg arch) ids)
-                   -- ^ State of processor prior to term statement.
                  , pblockTerm  :: !(ParsedTermStmt arch ids)
                  }