Fix issue in architecture-specific statement addresses.

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

@@ -128,15 +128,20 @@ data ArchitectureInfo arch
        -- ^ Provides architecture-specific information for computing which arguments must be
        -- evaluated when evaluating a statement.
      , postArchTermStmtAbsState :: !(forall ids
+                                     .  Memory (ArchAddrWidth arch)
                                         -- The abstract state when block terminates.
-                                     .  AbsBlockState (ArchReg arch)
+                                     -> AbsBlockState (ArchReg arch)
+                                        -- The registers before executing terminal statement
+                                     -> (RegState (ArchReg arch) (Value arch ids))
                                         -- The architecture-specific statement
                                      -> ArchTermStmt arch ids
-                                        -- The IP we are going to next.
-                                     -> ArchSegmentOff arch
-                                     -> AbsBlockState (ArchReg arch))
-       -- ^ Returns the abstract state after executing an architecture-specific
-       -- terminal statement.
+                                     -> Maybe (ArchSegmentOff arch, AbsBlockState (ArchReg arch)))
+       -- ^ This takes an abstract state from before executing an abs state, and an
+       -- architecture-specific terminal statement, and returns the next address within
+       -- the procedure that the statement jumps to along with the updated abstract state.
+       --
+       -- Note that per their documentation, architecture specific statements may return to at
+       -- most one location within a function.
      }
 
 -- | Apply optimizations to a terminal statement.
@@ -157,10 +162,9 @@ rewriteTermStmt info tstmt = do
     TranslateError regs msg ->
       TranslateError <$> traverseF rewriteValue regs
                      <*> pure msg
-    ArchTermStmt ts regs addr ->
+    ArchTermStmt ts regs ->
       ArchTermStmt <$> rewriteArchTermStmt info ts
                    <*> traverseF rewriteValue regs
-                   <*> pure addr
 
 -- | Apply optimizations to code in the block
 rewriteBlock :: ArchitectureInfo arch

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

@@ -46,7 +46,6 @@ data TermStmt arch ids
     -- statement could return to (if any)
   | ArchTermStmt !(ArchTermStmt arch ids)
                  !(RegState (ArchReg arch) (Value arch ids))
-                 !(Maybe (ArchSegmentOff arch))
 
 instance ArchConstraints arch
       => Pretty (TermStmt arch ids) where
@@ -58,7 +57,7 @@ instance ArchConstraints arch
   pretty (TranslateError s msg) =
     text "ERROR: " <+> text (Text.unpack msg) <$$>
     indent 2 (pretty s)
-  pretty (ArchTermStmt ts regs _) =
+  pretty (ArchTermStmt ts regs) =
     prettyF ts <$$> indent 2 (pretty regs)
 
 ------------------------------------------------------------------------

base/src/Data/Macaw/Discovery.hs

@@ -195,7 +195,7 @@ addTermDemands t = do
       addValueDemands v
     TranslateError regs _ -> do
       traverseF_ addValueDemands regs
-    ArchTermStmt _ regs _ -> do
+    ArchTermStmt _ regs -> do
       traverseF_ addValueDemands regs
 
 -- | Add any assignments needed to evaluate statements with side
@@ -747,18 +747,18 @@ parseBlock ctx b regs = do
                             , stmtsTerm = ParsedTranslateError msg
                             , stmtsAbsState = absProcState'
                             }
-    ArchTermStmt ts s' maddr -> do
+    ArchTermStmt ts s' -> do
       mapM_ (recordWriteStmt arch_info mem absProcState') (blockStmts b)
       let abst = finalAbsBlockState absProcState' s'
       -- Compute possible next IPS.
-      case maddr of
-        Just addr -> do
-          let post = postArchTermStmtAbsState arch_info abst ts addr
+      let r = postArchTermStmtAbsState arch_info mem abst s' ts
+      case r of
+        Just (addr,post) ->
           intraJumpTargets %= ((addr, post):)
         Nothing -> pure ()
       pure $! StatementList { stmtsIdent = idx
                             , stmtsNonterm = blockStmts b
-                            , stmtsTerm  = ParsedArchTermStmt ts s' maddr
+                            , stmtsTerm  = ParsedArchTermStmt ts s' (fst <$> r)
                             , stmtsAbsState = absProcState'
                             }
 

x86/src/Data/Macaw/X86.hs

@@ -1073,16 +1073,12 @@ instance S.Semantics (X86Generator st_s ids) where
       -- Get last block.
       let p_b = s0 ^. blockState
       -- Create finished block.
-      let mem = genMemory s0
-      case s0^.curX86State^.curIP of
-        RelocatableValue _ addr | Just segOff <- asSegmentOff mem addr -> do
-          let fin_b = finishBlock' p_b $ \s -> ArchTermStmt X86Syscall s (Just segOff)
-          seq fin_b $ do
-          -- Return early
-          return $ GenResult { resBlockSeq = s0 ^.blockSeq & frontierBlocks %~ (Seq.|> fin_b)
-                             , resState = Nothing
-                             }
-        _ -> error $ "Sycall could not interpret next IP"
+      let fin_b = finishBlock' p_b $ ArchTermStmt X86Syscall
+      seq fin_b $ do
+      -- Return early
+      return $ GenResult { resBlockSeq = s0 ^.blockSeq & frontierBlocks %~ (Seq.|> fin_b)
+                         , resState = Nothing
+                         }
 
   primitive S.CPUID = do
     rax_val <- getReg RAX
@@ -1484,17 +1480,21 @@ x86DemandContext =
                 }
 
 postX86TermStmtAbsState :: (forall tp . X86Reg tp -> Bool)
+                        -> Memory 64
                         -> AbsBlockState X86Reg
+                        -> RegState X86Reg (Value X86_64 ids)
                         -> X86TermStmt ids
-                        -> MemSegmentOff 64
-                        -> AbsBlockState X86Reg
-postX86TermStmtAbsState preservePred s tstmt nextIP =
+                        -> Maybe (MemSegmentOff 64, AbsBlockState X86Reg)
+postX86TermStmtAbsState preservePred mem s regs tstmt =
   case tstmt of
     X86Syscall ->
-      let params = CallParams { postCallStackDelta = 0
-                              , preserveReg = preservePred
-                              }
-       in absEvalCall params s nextIP
+      case regs^.curIP of
+        RelocatableValue _ addr | Just nextIP <- asSegmentOff mem addr -> do
+          let params = CallParams { postCallStackDelta = 0
+                                  , preserveReg = preservePred
+                                  }
+          Just (nextIP, absEvalCall params s nextIP)
+        _ -> error $ "Sycall could not interpret next IP"
 
 
 -- | Common architecture information for X86_64