Drop support for branches within blocks.

.travis.yml

@@ -28,8 +28,7 @@ install:
 
 # Here starts the actual work to be performed for the package under test;
 # any command which exits with a non-zero exit code causes the build to fail.
-script:
- # Build crucible with no -Werror
+ # Build packages that we do not want to check warnings on.
  - stack build crucible
  # Build packages
  - stack build --ghc-options="-Wall -Werror"

base/macaw-base.cabal

@@ -1,5 +1,5 @@
 name: macaw-base
-version: 0.3.5
+version: 0.3.6
 author: Galois, Inc.
 maintainer: jhendrix@galois.com
 build-type: Simple

base/src/Data/Macaw/Architecture/Info.hs

@@ -1,7 +1,4 @@
 {-|
-Copyright  : (c) Galois, Inc 2016
-Maintainer : jhendrix@galois.com
-
 This defines the architecture-specific information needed for code discovery.
 -}
 {-# LANGUAGE FlexibleContexts #-}
@@ -19,11 +16,9 @@ module Data.Macaw.Architecture.Info
 import           Control.Monad.ST
 import           Data.Parameterized.Nonce
 import           Data.Parameterized.TraversableF
-import           Data.Semigroup ( (<>) )
 import           Data.Sequence (Seq)
 
 import           Data.Macaw.AbsDomain.AbsState as AbsState
-import           Data.Macaw.CFG.App
 import           Data.Macaw.CFG.Block
 import           Data.Macaw.CFG.Core
 import           Data.Macaw.CFG.DemandSet
@@ -51,7 +46,7 @@ type DisassembleFn arch
       -- ^ Initial values to use for registers.
    -> Int
       -- ^ Maximum offset for this to read from.
-   -> ST s ([Block arch ids], Int, Maybe String)
+   -> ST s (Block arch ids, Int)
 
 -- | This records architecture specific functions for analysis.
 data ArchitectureInfo arch
@@ -174,13 +169,6 @@ rewriteTermStmt info tstmt = do
   case tstmt of
     FetchAndExecute regs ->
       FetchAndExecute <$> traverseF rewriteValue regs
-    Branch c t f -> do
-      tgtCond <- rewriteValue c
-      case () of
-        _ | Just (NotApp cn) <- valueAsApp tgtCond -> do
-              pure $ Branch cn f t
-          | otherwise ->
-              pure $ Branch tgtCond t f
     TranslateError regs msg ->
       TranslateError <$> traverseF rewriteValue regs
                      <*> pure msg
@@ -190,16 +178,15 @@ rewriteTermStmt info tstmt = do
 
 -- | Apply optimizations to code in the block
 rewriteBlock :: ArchitectureInfo arch
-             -> (RewriteContext arch s src tgt, [Block arch tgt])
+             -> RewriteContext arch s src tgt
              -> Block arch src
-             -> ST s (RewriteContext arch s src tgt, [Block arch tgt])
-rewriteBlock info (rwctx,blks) b = do
-  (rwctx', newBlks, tgtStmts, tgtTermStmt) <- runRewriter rwctx $ do
+             -> ST s (RewriteContext arch s src tgt, Block arch tgt)
+rewriteBlock info rwctx b = do
+  (rwctx', tgtStmts, tgtTermStmt) <- runRewriter rwctx $ do
     mapM_ rewriteStmt (blockStmts b)
     rewriteTermStmt info (blockTerm b)
   -- Return rewritten block and any new blocks
-  let rwBlock = Block { blockLabel = blockLabel b
-                      , blockStmts = tgtStmts
+  let rwBlock = Block { blockStmts = tgtStmts
                       , blockTerm  = tgtTermStmt
                       }
-    in pure (rwctx', rwBlock : (newBlks <> blks))
+  pure (rwctx', rwBlock)

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

@@ -9,18 +9,16 @@ types.
 {-# LANGUAGE UndecidableInstances #-}
 
 module Data.Macaw.CFG.Block
-  ( Block(..), BlockLabel
+  ( Block(..)
   , ppBlock
   , TermStmt(..)
   ) where
 
 import           Data.Text (Text)
 import qualified Data.Text as Text
-import           Data.Word
 import           Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>))
 
 import           Data.Macaw.CFG.Core
-import           Data.Macaw.Types
 
 ------------------------------------------------------------------------
 -- TermStmt
@@ -32,8 +30,6 @@ import           Data.Macaw.Types
 data TermStmt arch ids
      -- | Fetch and execute the next instruction from the given processor state.
   = FetchAndExecute !(RegState (ArchReg arch) (Value arch ids))
-    -- | Branch and execute one block or another.
-  | Branch !(Value arch ids BoolType) !BlockLabel !BlockLabel
     -- | The block ended prematurely due to an error in instruction
     -- decoding or translation.
     --
@@ -52,8 +48,6 @@ instance ArchConstraints arch
   pretty (FetchAndExecute s) =
     text "fetch_and_execute" <$$>
     indent 2 (pretty s)
-  pretty (Branch c x y) =
-    text "branch" <+> ppValue 0 c <+> text (show x) <+> text (show y)
   pretty (TranslateError s msg) =
     text "ERROR: " <+> text (Text.unpack msg) <$$>
     indent 2 (pretty s)
@@ -63,22 +57,15 @@ instance ArchConstraints arch
 ------------------------------------------------------------------------
 -- Block
 
--- | The type of labels for each block
-type BlockLabel = Word64
-
 -- | The type for code blocks returned by the disassembler.
 --
 -- The discovery process will attempt to map each block to a suitable ParsedBlock.
 data Block arch ids
-   = Block { blockLabel :: !BlockLabel
-             -- ^ Index of this block
-           , blockStmts :: !([Stmt arch ids])
+   = Block { blockStmts :: !([Stmt arch ids])
              -- ^ List of statements in the block.
            , blockTerm :: !(TermStmt arch ids)
              -- ^ The last statement in the block.
            }
 
 ppBlock :: ArchConstraints arch => Block arch ids -> Doc
-ppBlock b =
-  text (show (blockLabel b)) PP.<> text ":" <$$>
-  indent 2 (vcat (ppStmt (text . show) <$> blockStmts b) <$$> pretty (blockTerm b))
+ppBlock b = vcat (ppStmt (text . show) <$> blockStmts b) <$$> pretty (blockTerm b)

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

@@ -31,7 +31,6 @@ module Data.Macaw.CFG.Rewriter
   , rewriteApp
   , evalRewrittenArchFn
   , appendRewrittenArchStmt
-  , addNewBlockFromRewrite
   ) where
 
 import           Control.Lens
@@ -51,7 +50,7 @@ import           Data.STRef
 
 import           Data.Macaw.CFG
 import           Data.Macaw.Types
-import           Data.Macaw.CFG.Block ( TermStmt, Block(..), BlockLabel )
+import           Data.Macaw.CFG.Block (TermStmt)
 
 -- | Information needed for rewriting.
 data RewriteContext arch s src tgt
@@ -90,11 +89,6 @@ data RewriteContext arch s src tgt
                       -- of the assignments can be eliminated this
                       -- should be done via a dead code elimination step
                       -- rather than during rewriting.
-
-                    , rwctxBlockLabel :: BlockLabel
-                      -- ^ The next assignable BlockLabel (used for
-                      -- rewrites that create new blocks, as would be
-                      -- needed for Branch TermStmts.
                     }
 
 mkRewriteContext :: RegisterInfo (ArchReg arch)
@@ -112,10 +106,8 @@ mkRewriteContext :: RegisterInfo (ArchReg arch)
                     -- Discovery.hs.
                  -> Map SectionIndex (ArchSegmentOff arch)
                     -- ^ Map from loaded section indices to their address.
-                 -> BlockLabel
-                 -- ^ next BlockLabel (useable for creating new Block entries)
                  -> ST s (RewriteContext arch s src tgt)
-mkRewriteContext nonceGen archFn archStmt termStmt secAddrMap nextBlockLabel = do
+mkRewriteContext nonceGen archFn archStmt termStmt secAddrMap = do
   ref <- newSTRef MapF.empty
   pure $! RewriteContext { rwctxNonceGen = nonceGen
                          , rwctxArchFn = archFn
@@ -124,7 +116,6 @@ mkRewriteContext nonceGen archFn archStmt termStmt secAddrMap nextBlockLabel = d
                          , rwctxConstraints = \a -> a
                          , rwctxSectionAddrMap = secAddrMap
                          , rwctxCache = ref
-                         , rwctxBlockLabel = nextBlockLabel
                          }
 
 -- | State used by rewriter for tracking states
@@ -132,21 +123,12 @@ data RewriteState arch s src tgt
    = RewriteState { -- | Access to the context for the rewriter
                     rwContext        :: !(RewriteContext arch s src tgt)
                   , _rwRevStmts      :: ![Stmt arch tgt]
-                  , _rwNewBlocks      :: ![Block arch tgt]
                   }
 
 -- | A list of statements in the current block in reverse order.
 rwRevStmts :: Simple Lens (RewriteState arch s src tgt) [Stmt arch tgt]
 rwRevStmts = lens _rwRevStmts (\s v -> s { _rwRevStmts = v })
 
--- | A list of newly created Blocks generated during the rewrite operation.
-rwNewBlocks :: Simple Lens (RewriteState arch s src tgt) [Block arch tgt]
-rwNewBlocks = lens _rwNewBlocks (\s v -> s { _rwNewBlocks = v })
-
--- | The next BlockLabel to use for newly created Blocks generated during the rewrite.
-rwBlockLabel :: Simple Lens (RewriteState arch s src tgt) BlockLabel
-rwBlockLabel = lens (rwctxBlockLabel . rwContext) (\s v -> s { rwContext = (rwContext s) { rwctxBlockLabel = v }})
-
 -- | Monad for constant propagation within a block.
 newtype Rewriter arch s src tgt a = Rewriter { unRewriter :: StateT (RewriteState arch s src tgt) (ST s) a }
   deriving (Functor, Applicative, Monad)
@@ -156,17 +138,15 @@ newtype Rewriter arch s src tgt a = Rewriter { unRewriter :: StateT (RewriteStat
 runRewriter :: RewriteContext arch s src tgt
             -> Rewriter arch s src tgt (TermStmt arch tgt)
             -> ST s ( RewriteContext arch s src tgt
-                    , [Block arch tgt]
                     , [Stmt arch tgt]
                     , (TermStmt arch tgt))
 runRewriter ctx m = do
   let s = RewriteState { rwContext = ctx
                        , _rwRevStmts = []
-                       , _rwNewBlocks = []
                        }
       m' = rwctxTermStmt ctx =<< m
   (r, s') <- runStateT (unRewriter m') s
-  pure (rwContext s', _rwNewBlocks s', reverse (_rwRevStmts s'), r)
+  pure (rwContext s', reverse (_rwRevStmts s'), r)
 
 -- | Add a statement to the list
 appendRewrittenStmt :: Stmt arch tgt -> Rewriter arch s src tgt ()
@@ -180,23 +160,6 @@ appendRewrittenStmt stmt = Rewriter $ do
 appendRewrittenArchStmt :: ArchStmt arch (Value arch tgt) -> Rewriter arch s src tgt ()
 appendRewrittenArchStmt = appendRewrittenStmt . ExecArchStmt
 
-
--- | If the rewriting needs to add a new 'Block' (e.g. for a 'Branch'
--- target) it does so by calling this function with that 'Block'.
-addNewBlockFromRewrite :: [Stmt arch tgt]
-                       -> TermStmt arch tgt
-                       -> Rewriter arch s src tgt (BlockLabel)
-addNewBlockFromRewrite stmts termstmt = Rewriter $ do
-  blkLabel <- use rwBlockLabel
-  let blk = Block { blockLabel = blkLabel
-                  , blockStmts = stmts
-                  , blockTerm = termstmt
-                  }
-  rwNewBlocks %= (:) blk
-  rwBlockLabel += 1
-  return blkLabel
-
-
 -- | Add an assignment statement that evaluates the right hand side and return the resulting value.
 evalRewrittenRhs :: AssignRhs arch (Value arch tgt) tp -> Rewriter arch s src tgt (Value arch tgt tp)
 evalRewrittenRhs rhs = Rewriter $ do

base/src/Data/Macaw/Discovery.hs

@@ -169,8 +169,6 @@ addTermDemands t = do
   case t of
     FetchAndExecute regs -> do
       traverseF_ addValueDemands regs
-    Branch v _ _ -> do
-      addValueDemands v
     TranslateError regs _ -> do
       traverseF_ addValueDemands regs
     ArchTermStmt _ regs -> do
@@ -812,8 +810,6 @@ data ParseContext arch ids =
                  -- ^ Address of function this block is being parsed as
                , pctxAddr           :: !(ArchSegmentOff arch)
                  -- ^ Address of the current block
-               , pctxBlockMap       :: !(Map BlockLabel (Block arch ids))
-                 -- ^ Map from block indices to block code at address.
                }
 
 -- | Get the memory representation associated with pointers in the
@@ -1142,30 +1138,6 @@ parseBlock ctx idx initRegs b absProcState = do
   let ainfo = pctxArchInfo ctx
   withArchConstraints ainfo $ do
    case blockTerm b of
-    Branch c lb rb -> do
-      let blockMap = pctxBlockMap ctx
-      -- FIXME: we should propagate c back to the initial block, not just b
-      let absProcState' = absEvalStmts ainfo absProcState (blockStmts b)
-      mapM_ (recordWriteStmt ainfo mem absProcState') (blockStmts b)
-
-      let Just l = Map.lookup lb blockMap
-      let l_regs = refineProcStateBounds c True $ refineProcState c absTrue absProcState'
-      let Just r = Map.lookup rb blockMap
-      let r_regs = refineProcStateBounds c False $ refineProcState c absFalse absProcState'
-
-      let l_regs' = absEvalStmts ainfo l_regs (blockStmts b)
-      let r_regs' = absEvalStmts ainfo r_regs (blockStmts b)
-
-      (parsedTrueBlock,trueIdx)   <- parseBlock ctx (idx+1) initRegs l l_regs'
-      (parsedFalseBlock,falseIdx) <- parseBlock ctx trueIdx initRegs r r_regs'
-
-      let ret = StatementList { stmtsIdent = idx
-                              , stmtsNonterm = blockStmts b
-                              , stmtsTerm  = ParsedIte c parsedTrueBlock parsedFalseBlock
-                              , stmtsAbsState = absProcState'
-                              }
-      pure (ret, falseIdx)
-
     FetchAndExecute finalRegs -> do
       parseFetchAndExecute ctx idx initRegs (Seq.fromList (blockStmts b)) absProcState finalRegs
 
@@ -1200,49 +1172,44 @@ parseBlock ctx idx initRegs b absProcState = do
 
 -- | This evaluates the statements in a block to expand the information known
 -- about control flow targets of this block.
-addBlocks :: ArchSegmentOff arch
-             -- ^ Address of these blocks
-          -> FoundAddr arch
-             -- ^ State leading to explore block
-          -> RegState (ArchReg arch) (Value arch ids)
-          -> Int
-             -- ^ Number of blocks covered
-          -> Map BlockLabel (Block arch ids)
-             -- ^ Map from labelIndex to associated block
-          -> FunM arch s ids ()
-addBlocks src finfo initRegs sz blockMap =
-  case Map.lookup 0 blockMap of
-    Nothing -> do
-      error $ "addBlocks given empty blockRegion."
-    Just b -> do
-      mem       <- uses curFunCtx memory
-      let regs = initAbsProcessorState mem (foundAbstractState finfo)
-      funAddr <- gets curFunAddr
-      s <- use curFunCtx
+addBlock :: ArchSegmentOff arch
+            -- ^ Address of these blocks
+         -> FoundAddr arch
+            -- ^ State leading to explore block
+         -> RegState (ArchReg arch) (Value arch ids)
+         -> Int
+            -- ^ Number of bytes in block
+         -> Block arch ids
+            -- ^ Map from labelIndex to associated block
+         -> FunM arch s ids ()
+addBlock src finfo initRegs sz b = do
+  s <- use curFunCtx
+  let mem = memory s
+  let regs = initAbsProcessorState mem (foundAbstractState finfo)
+  funAddr <- gets curFunAddr
 
-      let ctx = ParseContext { pctxMemory         = memory s
-                             , pctxArchInfo       = archInfo s
-                             , pctxKnownFnEntries = s^.trustedFunctionEntryPoints
-                             , pctxFunAddr        = funAddr
-                             , pctxAddr           = src
-                             , pctxBlockMap       = blockMap
-                             }
-      let ps0 = ParseState { _writtenCodeAddrs = []
-                           , _intraJumpTargets = []
-                           , _newFunctionAddrs = []
-                           }
-      let ((pblock,_), ps) = runState (parseBlock ctx 0 initRegs b regs) ps0
-      let pb = ParsedBlock { pblockAddr = src
-                           , blockSize = sz
-                           , blockReason = foundReason finfo
-                           , blockAbstractState = foundAbstractState finfo
-                           , blockStatementList = pblock
-                           }
-      let pb' = dropUnusedCodeInParsedBlock (archInfo s) pb
-      id %= addFunBlock src pb'
-      curFunCtx %= markAddrsAsFunction (PossibleWriteEntry src) (ps^.writtenCodeAddrs)
-                .  markAddrsAsFunction (CallTarget src)         (ps^.newFunctionAddrs)
-      mapM_ (\(addr, abs_state) -> mergeIntraJump src abs_state addr) (ps^.intraJumpTargets)
+  let ctx = ParseContext { pctxMemory         = memory s
+                         , pctxArchInfo       = archInfo s
+                         , pctxKnownFnEntries = s^.trustedFunctionEntryPoints
+                         , pctxFunAddr        = funAddr
+                         , pctxAddr           = src
+                         }
+  let ps0 = ParseState { _writtenCodeAddrs = []
+                       , _intraJumpTargets = []
+                       , _newFunctionAddrs = []
+                       }
+  let ((pblock,_), ps) = runState (parseBlock ctx 0 initRegs b regs) ps0
+  let pb = ParsedBlock { pblockAddr = src
+                       , blockSize = sz
+                       , blockReason = foundReason finfo
+                       , blockAbstractState = foundAbstractState finfo
+                       , blockStatementList = pblock
+                       }
+  let pb' = dropUnusedCodeInParsedBlock (archInfo s) pb
+  id %= addFunBlock src pb'
+  curFunCtx %= markAddrsAsFunction (PossibleWriteEntry src) (ps^.writtenCodeAddrs)
+            .  markAddrsAsFunction (CallTarget src)         (ps^.newFunctionAddrs)
+  mapM_ (\(addr, abs_state) -> mergeIntraJump src abs_state addr) (ps^.intraJumpTargets)
 
 -- | Record an error block with no statements for the given address.
 recordErrorBlock :: ArchSegmentOff arch -> FoundAddr arch -> Maybe String -> FunM arch s ids ()
@@ -1286,30 +1253,22 @@ transfer addr = do
       Left msg -> do
         recordErrorBlock addr finfo (Just msg)
       Right initRegs -> do
-        (bs0, sz, maybeError) <- liftST $ disassembleFn ainfo nonceGen addr initRegs maxSize
+        (b0, sz) <- liftST $ disassembleFn ainfo nonceGen addr initRegs maxSize
         -- If no blocks are returned, then we just add an empty parsed block.
-        if null bs0 then do
-          recordErrorBlock addr finfo maybeError
-         else do
-          -- Rewrite returned blocks to simplify expressions
+        -- Rewrite returned blocks to simplify expressions
 #ifdef USE_REWRITER
-          bs1 <- snd <$> do
-            let archStmt = rewriteArchStmt ainfo
-            let secAddrMap = memSectionIndexMap mem
-            termStmt <- gets termStmtRewriter <*> pure addr
-            let maxBlockLabel = maximum $ map blockLabel bs0
-            liftST $ do
-              ctx <- mkRewriteContext nonceGen (rewriteArchFn ainfo)
-                     archStmt termStmt secAddrMap (maxBlockLabel + 1)
-              foldM (rewriteBlock ainfo) (ctx, []) bs0
+        (_,b) <- do
+          let archStmt = rewriteArchStmt ainfo
+          let secAddrMap = memSectionIndexMap mem
+          termStmt <- gets termStmtRewriter <*> pure addr
+          liftST $ do
+            ctx <- mkRewriteContext nonceGen (rewriteArchFn ainfo) archStmt termStmt secAddrMap
+            rewriteBlock ainfo ctx b0
 #else
-          bs1 <- pure bs0
+        b <- pure b0
 #endif
-          -- Compute demand set
-          let bs = bs1 -- eliminateDeadStmts ainfo bs1
-          -- Call transfer blocks to calculate parsedblocks
-          let blockMap = Map.fromList [ (blockLabel b, b) | b <- bs ]
-          addBlocks addr finfo initRegs sz blockMap
+        -- Call transfer blocks to calculate parsedblocks
+        addBlock addr finfo initRegs sz b
 
 ------------------------------------------------------------------------
 -- Main loop

symbolic/src/Data/Macaw/Symbolic.hs

@@ -264,22 +264,15 @@ addBlocksCFG :: forall h s arch ids
                  -- ^ Address of start of block
              ->  (M.ArchAddrWord arch -> C.Position)
              -- ^ Function that maps offsets from start of block to Crucible position.
-             -> [M.Block arch ids]
-             -- ^ List of blocks for this region.
+             -> M.Block arch ids
+             -- ^ Macaw block for this region.
              -> MacawMonad arch ids h s (CR.Label s, [CR.Block (MacawExt arch) s (MacawFunctionResult arch)])
-addBlocksCFG archFns baseAddrMap addr posFn macawBlocks = do
+addBlocksCFG archFns baseAddrMap addr posFn macawBlock = do
   crucGenArchConstraints archFns $ do
    -- Map block map to Crucible CFG
-  blockLabelMap <- fmap Map.fromList $ sequence $
-                     [ mmFreshNonce >>= \n -> return (w, CR.Label n)
-                     | w <- M.blockLabel <$> macawBlocks ]
-  entry <-
-    case Map.lookup 0 blockLabelMap of
-      Just lbl -> return lbl
-      Nothing -> fail "Unable to find initial block"
-  blks <- forM macawBlocks $ \b -> do
-    addMacawBlock archFns baseAddrMap addr blockLabelMap posFn b
-  return (entry, concatMap (uncurry (:)) blks)
+  entry <- CR.Label <$> mmFreshNonce
+  (blk,blks) <- addMacawBlock archFns baseAddrMap addr entry posFn macawBlock
+  return (entry, blk:blks)
 
 -- | Create a registerized Crucible CFG from an arbitrary list of macaw blocks
 --
@@ -303,12 +296,12 @@ mkBlocksRegCFG :: forall s arch ids
                -- ^ Address for start of block.
             -> (M.ArchAddrWord arch -> C.Position)
             -- ^ Function that maps offsets from start of block to Crucible position.
-            -> [M.Block arch ids]
+            -> M.Block arch ids
             -- ^ List of blocks for this region.
             -> ST s (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
-mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlocks = do
+mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlock = do
   mkCrucRegCFG archFns halloc nm $ do
-    addBlocksCFG archFns memBaseVarMap addr posFn macawBlocks
+    addBlocksCFG archFns memBaseVarMap addr posFn macawBlock
 
 -- | Create a Crucible CFG from an arbitrary list of macaw blocks
 --
@@ -332,12 +325,12 @@ mkBlocksCFG :: forall s arch ids
                -- ^ Address for start of block.
             -> (M.ArchAddrWord arch -> C.Position)
             -- ^ Function that maps offsets from start of block to Crucible position.
-            -> [M.Block arch ids]
+            -> M.Block arch ids
             -- ^ List of blocks for this region.
             -> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
-mkBlocksCFG archFns halloc memBaseVarMap nm addr posFn macawBlocks =
+mkBlocksCFG archFns halloc memBaseVarMap nm addr posFn macawBlock =
   toCoreCFG archFns <$>
-  mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlocks
+  mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlock
 
 -- | Create a map from Macaw @(address, index)@ pairs to Crucible labels
 mkBlockLabelMap :: [M.ParsedBlock arch ids] -> MacawMonad arch ids h s (BlockLabelMap arch s)

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

@@ -1215,16 +1215,6 @@ addMacawStmt baddr stmt =
           crucStmt = MacawArchStateUpdate addr m
       void $ evalMacawStmt crucStmt
 
-lookupCrucibleLabel :: Map Word64 (CR.Label s)
-                       -- ^ Map from block index to Crucible label
-                    -> Word64
-                       -- ^ Index of crucible block
-                    -> CrucGen arch ids h s (CR.Label s)
-lookupCrucibleLabel m idx = do
-  case Map.lookup idx m of
-    Nothing -> fail $ "Could not find label for block " ++ show idx
-    Just l -> pure l
-
 -- | Create a crucible struct for registers from a register state.
 createRegStruct :: forall arch ids h s
                 .  M.RegState (M.ArchReg arch) (M.Value arch ids)
@@ -1261,20 +1251,13 @@ createRegUpdates regs = do
           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
-                 -> M.TermStmt arch ids
+addMacawTermStmt :: M.TermStmt arch ids
                  -> CrucGen arch ids h s ()
-addMacawTermStmt blockLabelMap tstmt =
+addMacawTermStmt tstmt =
   case tstmt of
     M.FetchAndExecute regs -> do
       s <- createRegStruct regs
       addTermStmt (CR.Return s)
-    M.Branch macawPred macawTrueLbl macawFalseLbl -> do
-      p <- valueToCrucible macawPred
-      t <- lookupCrucibleLabel blockLabelMap macawTrueLbl
-      f <- lookupCrucibleLabel blockLabelMap macawFalseLbl
-      addTermStmt (CR.Br p t f)
     M.ArchTermStmt ts regs -> do
       fns <- translateFns <$> get
       crucGenArchTermStmt fns ts regs
@@ -1356,8 +1339,8 @@ addMacawBlock :: M.MemWidth (M.ArchAddrWidth arch)
               -- ^ Base address map
               -> M.ArchSegmentOff arch
                  -- ^ Address of start of block
-              -> Map Word64 (CR.Label s)
-                 -- ^ Map from block index to Crucible label
+              -> CR.Label s
+                 -- ^ Crucible label for this bloclk.
               -> (M.ArchAddrWord arch -> C.Position)
                  -- ^ Function for generating position from offset from start of this block.
               -> M.Block arch ids
@@ -1365,14 +1348,7 @@ addMacawBlock :: M.MemWidth (M.ArchAddrWidth arch)
                    ( CR.Block (MacawExt arch) s (MacawFunctionResult arch)
                    , [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]
                    )
-addMacawBlock archFns baseAddrMap addr blockLabelMap posFn b = do
-  let idx = M.blockLabel b
-  lbl <-
-    case Map.lookup idx blockLabelMap of
-      Just lbl ->
-        pure lbl
-      Nothing ->
-        throwError $ "Internal: Could not find block with index " ++ show idx
+addMacawBlock archFns baseAddrMap addr lbl posFn b = do
   let archRegStructRepr = C.StructRepr (crucArchRegTypes archFns)
   ng <- gets nonceGen
   regRegId <- mmExecST $ freshNonce ng
@@ -1389,7 +1365,7 @@ addMacawBlock archFns baseAddrMap addr blockLabelMap posFn b = do
   fmap (\(b', bs, _) -> (b', bs)) $ runCrucGen archFns baseAddrMap posFn 0 lbl regReg $ do
     addStmt $ CR.SetReg regReg regStruct
     mapM_ (addMacawStmt addr)  (M.blockStmts b)
-    addMacawTermStmt blockLabelMap (M.blockTerm b)
+    addMacawTermStmt (M.blockTerm b)
 
 parsedBlockLabel :: (Ord addr, Show addr)
                  => Map (addr, Word64) (CR.Label s)

x86/src/Data/Macaw/X86.hs

@@ -171,13 +171,12 @@ instance MemWidth w => Show (X86TranslateError w) where
 initError :: MemSegmentOff 64 -- ^ Location to explore from.
           -> RegState X86Reg (Value X86_64 ids)
           -> X86TranslateError 64
-          -> ST st_s (Block X86_64 ids, MemWord 64, Maybe (X86TranslateError 64))
+          -> ST st_s (Block X86_64 ids, MemWord 64)
 initError addr s err = do
-  let b = Block { blockLabel = 0
-                , blockStmts = []
+  let b = Block { blockStmts = []
                 , blockTerm  = TranslateError s (Text.pack (show err))
                 }
-  return (b, segoffOffset addr, Just err)
+  return (b, segoffOffset addr)
 
 -- | Disassemble memory contents using flexdis.
 disassembleInstruction :: MemSegmentOff 64
@@ -310,19 +309,17 @@ translateBlockImpl :: forall st_s ids
                          -- ^ Maximum offset for this addr from start of block.
                      -> [MemChunk 64]
                         -- ^ List of contents to read next.
-                     -> ST st_s (Block X86_64 ids
+                     -> ST st_s ( Block X86_64 ids
                                 , MemWord 64
-                                , Maybe (X86TranslateError 64)
                                 )
 translateBlockImpl gen pblock curIPAddr blockOff maxSize contents = do
   r <- runExceptT $ translateStep gen pblock blockOff curIPAddr contents
   case r of
     Left err -> do
-      let b = Block { blockLabel = pBlockIndex pblock
-                    , blockStmts = toList (pblock^.pBlockStmts)
+      let b = Block { blockStmts = toList (pblock^.pBlockStmts)
                     , blockTerm  = TranslateError (pblock^.pBlockState) (Text.pack (show err))
                     }
-      pure (b, blockOff, Just err)
+      pure (b, blockOff)
     Right (_, res, instSize, nextIP, nextContents) -> do
       let blockOff' = blockOff + fromIntegral instSize
       case unfinishedAtAddr res nextIP of
@@ -331,7 +328,7 @@ translateBlockImpl gen pblock curIPAddr blockOff maxSize contents = do
           , Just nextIPSegOff <- incSegmentOff curIPAddr (toInteger instSize) -> do
               translateBlockImpl gen pblock' nextIPSegOff blockOff' maxSize nextContents
         _ ->
-          pure (finishPartialBlock res, blockOff', Nothing)
+          pure (finishPartialBlock res, blockOff')
 
 {-# DEPRECATED disassembleBlock "Planned for removal." #-}
 
@@ -342,7 +339,7 @@ disassembleBlock :: forall s
                  -> ExploreLoc
                  -> MemWord 64
                     -- ^ Maximum number of bytes in ths block.
-                 -> ST s (Block X86_64 s, MemWord 64, Maybe (X86TranslateError 64))
+                 -> ST s (Block X86_64 s, MemWord 64)
 disassembleBlock gen loc maxSize = do
   let addr = loc_ip loc
   let regs = initX86State loc
@@ -469,13 +466,13 @@ tryDisassembleBlock :: forall s ids
                        -- ^ Maximum size of this block
                     -> ExceptT String (ST s) (Block X86_64 ids, Int, Maybe String)
 tryDisassembleBlock gen addr initRegs maxSize = lift $ do
-  (b, sz, maybeError) <-
+  (b, sz) <-
     case segoffContentsAfter addr of
       Left msg -> do
         initError addr initRegs (FlexdisMemoryError msg)
       Right contents -> do
         translateBlockImpl gen (emptyPreBlock addr initRegs) addr 0 (fromIntegral maxSize) contents
-  pure $! (b, fromIntegral sz, show <$> maybeError)
+  pure $! (b, fromIntegral sz, Nothing)
 
 -- | Disassemble block, returning either an error, or a list of blocks
 -- and ending PC.
@@ -488,15 +485,15 @@ translateBlockWithRegs :: forall s ids
                          -> Int
                             -- ^ Maximum size of this block
                             -- ^ Abstract state of processor for defining state.
-                         -> ST s ([Block X86_64 ids], Int, Maybe String)
+                         -> ST s (Block X86_64 ids, Int)
 translateBlockWithRegs gen addr initRegs maxSize = do
-  (b, sz, maybeError) <-
+  (b, sz) <-
     case segoffContentsAfter addr of
       Left msg -> do
         initError addr initRegs (FlexdisMemoryError msg)
       Right contents -> do
         translateBlockImpl gen (emptyPreBlock addr initRegs) addr 0 (fromIntegral maxSize) contents
-  pure $! ([b], fromIntegral sz, show <$> maybeError)
+  pure $! (b, fromIntegral sz)
 
 -- | Attempt to identify the write to a stack return address, returning
 -- instructions prior to that write and return  values.

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

@@ -36,7 +36,6 @@ module Data.Macaw.X86.Generator
     -- * PreBlock
   , PreBlock
   , emptyPreBlock
-  , pBlockIndex
   , pBlockState
   , pBlockStmts
   , pBlockApps
@@ -87,7 +86,6 @@ import           Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
 import           Data.Text (Text)
 import qualified Data.Text as Text
-import           Data.Word
 
 import           Data.Macaw.X86.ArchTypes
 import           Data.Macaw.X86.X86Reg
@@ -153,8 +151,7 @@ asSignedBVLit _ = Nothing
 -- PreBlock
 
 -- | A block that we have not yet finished.
-data PreBlock ids = PreBlock { pBlockIndex :: !Word64
-                             , _pBlockStmts :: !(Seq (Stmt X86_64 ids))
+data PreBlock ids = PreBlock { _pBlockStmts :: !(Seq (Stmt X86_64 ids))
                              , _pBlockState :: !(RegState X86Reg (Value X86_64 ids))
                              , _pBlockApps  :: !(MapF (App (Value X86_64 ids)) (Assignment X86_64 ids))
                              , pBlockStart  :: !(ArchSegmentOff X86_64)
@@ -165,8 +162,7 @@ emptyPreBlock :: ArchSegmentOff X86_64
               -> RegState X86Reg (Value X86_64 ids)
               -> PreBlock ids
 emptyPreBlock startAddr s  =
-  PreBlock { pBlockIndex  = 0
-           , _pBlockStmts = Seq.empty
+  PreBlock { _pBlockStmts = Seq.empty
            , _pBlockApps  = MapF.empty
            , _pBlockState = s
            , pBlockStart  = startAddr
@@ -186,8 +182,7 @@ finishBlock :: PreBlock ids
              -> (RegState X86Reg (Value X86_64 ids) -> TermStmt X86_64 ids)
              -> Block X86_64 ids
 finishBlock preBlock term =
-  Block { blockLabel = pBlockIndex preBlock
-        , blockStmts = toList (preBlock^.pBlockStmts)
+  Block { blockStmts = toList (preBlock^.pBlockStmts)
         , blockTerm  = term (preBlock^.pBlockState)
         }