Add JumpTable bounds; remove code discovery dependency on syscall.

macaw.cabal

@@ -43,6 +43,7 @@ library
     Data.Macaw.DebugLogging
     Data.Macaw.Discovery
     Data.Macaw.Discovery.Info
+    Data.Macaw.Discovery.JumpBounds
     Data.Macaw.Dwarf
     Data.Macaw.Memory
     Data.Macaw.Memory.ElfLoader

src/Data/Macaw/AbsDomain/AbsState.hs

@@ -16,9 +16,10 @@
 module Data.Macaw.AbsDomain.AbsState
   ( AbsBlockState
   , setAbsIP
-  , mkAbsBlockState
   , absRegState
   , absStackHasReturnAddr
+  , CallParams(..)
+  , postCallAbsState
   , AbsBlockStack
   , StackEntry(..)
   , ArchAbsValue
@@ -62,6 +63,7 @@ import           Control.Lens
 import           Control.Monad.State.Strict
 import           Data.Bits
 import           Data.Foldable
+import           Data.Functor
 import           Data.Int
 import           Data.Map (Map)
 import qualified Data.Map.Strict as Map
@@ -78,6 +80,7 @@ import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 import qualified Data.Macaw.AbsDomain.StridedInterval as SI
 import           Data.Macaw.CFG
 import           Data.Macaw.DebugLogging
+import           Data.Macaw.Discovery.JumpBounds
 import           Data.Macaw.Memory
 import qualified Data.Macaw.Memory.Permissions as Perm
 import           Data.Macaw.Types
@@ -91,6 +94,10 @@ addOff w o v = toUnsigned w (o + v)
 ------------------------------------------------------------------------
 -- AbsDomain
 
+-- | This represents an lattice order.
+--
+-- Elements are comparable for equality, have a partial order, a top element,
+-- and the ability to join to elements.
 class Eq d => AbsDomain d where
   -- | The top element
   top :: d
@@ -317,15 +324,6 @@ isEmpty (CodePointers s b) = Set.null s && not b
 isEmpty (FinSet s) = Set.null s
 isEmpty _ = False
 
--- -----------------------------------------------------------------------------
--- Instances
-
-{-
--- | Returns true if set just contains 0.
-isZeroPtr :: Set Word64 -> Bool
-isZeroPtr s = Set.size s == 1 && Set.findMin s == 0
--}
-
 -------------------------------------------------------------------------------
 -- Joining abstract values
 
@@ -907,6 +905,7 @@ ppAbsStack m = vcat (pp <$> Map.toDescList m)
 data AbsBlockState r
    = AbsBlockState { _absRegState :: !(RegState r (AbsValue (RegAddrWidth r)))
                    , _startAbsStack :: !(AbsBlockStack (RegAddrWidth r))
+                   , _initIndexBounds :: !(InitialIndexBounds r)
                    }
 
 deriving instance MapF.OrdF r => Eq (AbsBlockState r)
@@ -919,10 +918,8 @@ absRegState = lens _absRegState (\s v -> s { _absRegState = v })
 startAbsStack :: Simple Lens (AbsBlockState r) (AbsBlockStack (RegAddrWidth r))
 startAbsStack = lens _startAbsStack (\s v -> s { _startAbsStack = v })
 
-traceUnless :: Bool -> String -> a -> a
-traceUnless True _ = id
-traceUnless False msg = debug DAbsInt msg
-
+initIndexBounds :: Simple Lens (AbsBlockState r) (InitialIndexBounds r)
+initIndexBounds = lens _initIndexBounds (\s v -> s { _initIndexBounds = v })
 
 instance ( RegisterInfo r
          )
@@ -930,6 +927,7 @@ instance ( RegisterInfo r
 
   top = AbsBlockState { _absRegState = mkRegState (\_ -> TopV)
                       , _startAbsStack = Map.empty
+                      , _initIndexBounds = arbitraryInitialBounds
                       }
 
   joinD x y | regs_changed = Just $! z
@@ -940,7 +938,7 @@ instance ( RegisterInfo r
           x_stk = x^.startAbsStack
           y_stk = y^.startAbsStack
 
-          (zs,(regs_changed,dropped)) = flip runState (False, Set.empty) $ do
+          (z,(regs_changed,_dropped)) = flip runState (False, Set.empty) $ do
             z_regs <- mkRegStateM $ \r -> do
               let xr = xs^.boundValue r
               (c,s) <- get
@@ -952,14 +950,15 @@ instance ( RegisterInfo r
                   seq s' $ put $ (True,s')
                   return $! zr
             z_stk <- absStackJoinD x_stk y_stk
-            return $ AbsBlockState { _absRegState   = z_regs
-                                   , _startAbsStack = z_stk
-                                   }
+            z_bnds <-
+              case joinInitialBounds (x^.initIndexBounds) (y^.initIndexBounds) of
+                Just z_bnds  -> (_1 .= True) $> z_bnds
+                Nothing -> pure (x^.initIndexBounds)
 
-          z = traceUnless (Set.null dropped)
-                ("dropped abs " ++ show (ppSegAddrSet dropped) ++ "\n"
-                                ++ show x ++ "\n" ++ show y) $
-              zs
+            return $ AbsBlockState { _absRegState     = z_regs
+                                   , _startAbsStack   = z_stk
+                                   , _initIndexBounds = z_bnds
+                                   }
 
 instance ( ShowF r
          ) => Pretty (AbsBlockState r) where
@@ -1000,10 +999,7 @@ type ArchAbsValue arch = AbsValue (RegAddrWidth (ArchReg arch))
 
 -- | This stores the abstract state of the system at a given point in time.
 data AbsProcessorState r ids
-   = AbsProcessorState { absCodeWidth    :: !(NatRepr (RegAddrWidth r))
-                         -- ^ The width of a code pointer; the 'NatRepr' type
-                         -- connects the type-level nat with the value
-                       , absMem       :: !(Memory (RegAddrWidth r))
+   = AbsProcessorState { absMem       :: !(Memory (RegAddrWidth r))
                          -- ^ Recognizer for code addresses.
                        , _absInitialRegs
                          :: !(RegState r (AbsValue (RegAddrWidth r)))
@@ -1013,8 +1009,13 @@ data AbsProcessorState r ids
                          -- symbolic values associated with them
                        , _curAbsStack    :: !(AbsBlockStack (RegAddrWidth r))
                          -- ^ The current symbolic state of the stack
+                       ,  _indexBounds :: !(IndexBounds r ids)
                        }
 
+-- | The width of an address
+absCodeWidth :: AbsProcessorState r ids -> NatRepr (RegAddrWidth r)
+absCodeWidth = memWidth . absMem
+
 absInitialRegs :: Simple Lens (AbsProcessorState r ids)
                               (RegState r (AbsValue (RegAddrWidth r)))
 absInitialRegs = lens _absInitialRegs (\s v -> s { _absInitialRegs = v })
@@ -1026,6 +1027,10 @@ absAssignments = lens _absAssignments (\s v -> s { _absAssignments = v })
 curAbsStack :: Simple Lens (AbsProcessorState r ids) (AbsBlockStack (RegAddrWidth r))
 curAbsStack = lens _curAbsStack (\s v -> s { _curAbsStack = v })
 
+-- | Return the index
+indexBounds :: Simple Lens (AbsProcessorState r ids) (IndexBounds r ids)
+indexBounds = lens _indexBounds (\s v -> s { _indexBounds = v })
+
 instance ShowF r
       => Show (AbsProcessorState r ids) where
   show = show . pretty
@@ -1033,22 +1038,27 @@ instance ShowF r
 -- FIXME
 instance (ShowF r)
       => Pretty (AbsProcessorState r ids) where
-  pretty regs = pretty (AbsBlockState { _absRegState   = regs ^. absInitialRegs
-                                      , _startAbsStack = regs ^. curAbsStack })
+  pretty s =
+      text "registers:" <$$>
+      indent 2 (pretty (s^.absInitialRegs)) <$$>
+      stack_d
+    where stack = s^.curAbsStack
+          stack_d | Map.null stack = empty
+                  | otherwise = text "stack:" <$$>
+                                indent 2 (ppAbsStack stack)
 
-initAbsProcessorState :: NatRepr (RegAddrWidth r)
-                      -> Memory (RegAddrWidth r)
+initAbsProcessorState :: Memory (RegAddrWidth r)
                          -- ^ Current state of memory in the processor.
                          --
                          -- Used for checking code segment status.
                       -> AbsBlockState r
                       -> AbsProcessorState r ids
-initAbsProcessorState code_width mem s =
-  AbsProcessorState { absCodeWidth = code_width
-                    , absMem = mem
+initAbsProcessorState mem s =
+  AbsProcessorState { absMem = mem
                     , _absInitialRegs = s^.absRegState
                     , _absAssignments = MapF.empty
                     , _curAbsStack = s^.startAbsStack
+                    , _indexBounds = mkIndexBounds (s^.initIndexBounds)
                     }
 
 -- | A lens that allows one to lookup and update the value of an assignment in
@@ -1178,18 +1188,6 @@ addMemWrite cur_ip a v r =
     -- FIXME: nuke stack on an unknown address or Top?
     _ -> r
 
--- subOff :: NatRepr w -> Integer -> Integer -> Integer
--- subOff w o v = toUnsigned w (o - v)
-
-mkAbsBlockState :: RegisterInfo r
-                => (forall tp . r tp -> AbsValue (RegAddrWidth r) tp)
-                -> AbsBlockStack (RegAddrWidth r)
-                -> AbsBlockState r
-mkAbsBlockState trans newStack =
-  AbsBlockState { _absRegState = mkRegState trans
-                , _startAbsStack = newStack
-                }
-
 absStackHasReturnAddr :: AbsBlockState r -> Bool
 absStackHasReturnAddr s = isJust $ find isReturnAddr (Map.elems (s^.startAbsStack))
   where isReturnAddr (StackEntry _ ReturnAddr) = True
@@ -1203,11 +1201,15 @@ finalAbsBlockState :: forall a ids
                       )
                    => AbsProcessorState (ArchReg a) ids
                    -> RegState (ArchReg a) (Value a ids)
+                      -- ^  Final values for abstract processor state
                    -> AbsBlockState (ArchReg a)
 finalAbsBlockState c s =
   let transferReg :: ArchReg a tp -> ArchAbsValue a tp
       transferReg r = transferValue c (s^.boundValue r)
-   in mkAbsBlockState transferReg (c^.curAbsStack)
+   in AbsBlockState { _absRegState = mkRegState transferReg
+                    , _startAbsStack = c^.curAbsStack
+                    , _initIndexBounds = nextBlockBounds s (c^.indexBounds)
+                    }
 
 ------------------------------------------------------------------------
 -- Transfer functions
@@ -1229,3 +1231,41 @@ transferApp r a =
     BVAnd w x y -> bitop (.&.) w (transferValue r x) (transferValue r y)
     BVOr w x y  -> bitop (.|.) w (transferValue r x) (transferValue r y)
     _ -> TopV
+
+-- | Minimal information needed to parse a function call/system call
+data CallParams (r :: Type -> *)
+   = CallParams { postCallStackDelta :: Integer
+                  -- ^ Amount stack should shift by when going before/after call.
+                , preserveReg        :: forall tp . r tp -> Bool
+                  -- ^ Return true if a register value is preserved by a call.
+                }
+
+-- | Return state post call
+postCallAbsState :: forall r
+                 .  ( RegisterInfo r
+                    , HasRepr r TypeRepr
+                    )
+                 => CallParams r
+                 -> AbsBlockState r
+                 -> SegmentedAddr (RegAddrWidth r)
+                    -- ^ Address we are jumping to
+                 -> AbsBlockState r
+postCallAbsState params ab0 addr =
+    AbsBlockState { _absRegState = mkRegState regFn
+                  , _startAbsStack = ab0^.startAbsStack
+                  , _initIndexBounds = arbitraryInitialBounds
+                  }
+  where regFn :: r tp -> AbsValue (RegAddrWidth r) tp
+        regFn r
+          -- We set IPReg
+          | Just Refl <- testEquality r ip_reg =
+              CodePointers (Set.singleton addr) False
+          | Just Refl <- testEquality r sp_reg =
+              let w = type_width (typeRepr r)
+               in bvadd w (ab0^.absRegState^.boundValue r) (FinSet (Set.singleton (postCallStackDelta params)))
+            -- Copy callee saved registers
+          | preserveReg params r =
+            ab0^.absRegState^.boundValue r
+            -- We know nothing about other registers.
+          | otherwise =
+            TopV

src/Data/Macaw/Architecture/Info.hs

@@ -5,12 +5,15 @@ Maintainer : jhendrix@galois.com
 This defines the architecture-specific information needed for code discovery.
 -}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 module Data.Macaw.Architecture.Info
   ( ArchitectureInfo(..)
   , ReadAddrFn
   , DisassembleFn
+  , archPostCallAbsState
+  , archPostSyscallAbsState
   ) where
 
 import Control.Monad.ST
@@ -19,6 +22,7 @@ import Data.Parameterized.Nonce
 import Data.Macaw.AbsDomain.AbsState
 import Data.Macaw.CFG
 import Data.Macaw.Memory
+import Data.Macaw.Types
 
 ------------------------------------------------------------------------
 -- ArchitectureInfo
@@ -66,26 +70,46 @@ data ArchitectureInfo arch
        -- ^ The shift that the stack moves with a call.
      , disassembleFn :: !(DisassembleFn arch)
        -- ^ Function for disasembling a block.
+     , preserveRegAcrossCall :: !(forall tp . ArchReg arch tp -> Bool)
+       -- ^ Return true if architecture register should be preserved across a call.
+     , preserveRegAcrossSyscall :: !(forall tp . ArchReg arch tp -> Bool)
+       -- ^ Return true if architecture register should be preserved across a system call.
      , fnBlockStateFn :: !(Memory (RegAddrWidth (ArchReg arch))
                            -> SegmentedAddr (RegAddrWidth (ArchReg arch))
                            -> AbsBlockState (ArchReg arch))
        -- ^ Creates an abstract block state for representing the beginning of a
        -- function.
-     , postSyscallFn :: !(AbsBlockState (ArchReg arch)
-                          -> ArchSegmentedAddr arch
-                          -> AbsBlockState (ArchReg arch))
-       -- ^ Transfer function that maps abstract state before system call to
-       -- abstract state after system call.
-       --
-       -- The first argument contains the first abstract state, and the
-       -- second contains the address that we are jumping to.
-     , postCallAbsStateFn :: !(AbsBlockState (ArchReg arch)
-                               -> ArchSegmentedAddr arch
-                               -> AbsBlockState (ArchReg arch))
-       -- ^ Abstract state after a function call.
      , absEvalArchFn :: !(forall ids tp
                           .  AbsProcessorState (ArchReg arch) ids
                           -> ArchFn arch ids tp
                           -> AbsValue (RegAddrWidth (ArchReg arch)) tp)
        -- ^ Evaluates an architecture-specific function
      }
+
+-- | Return state post call
+archPostCallAbsState :: ( RegisterInfo (ArchReg arch)
+                        , HasRepr (ArchReg arch) TypeRepr
+                        )
+                     => ArchitectureInfo arch
+                        -- ^ Architecture information
+                     -> AbsBlockState (ArchReg arch)
+                     -> SegmentedAddr (RegAddrWidth (ArchReg arch))
+                     -> AbsBlockState (ArchReg arch)
+archPostCallAbsState archInfo = postCallAbsState params
+  where params = CallParams { postCallStackDelta = negate (callStackDelta archInfo)
+                            , preserveReg = preserveRegAcrossCall archInfo
+                            }
+
+-- | Return state post call
+archPostSyscallAbsState :: ( RegisterInfo (ArchReg arch)
+                           , HasRepr (ArchReg arch) TypeRepr
+                           )
+                        => ArchitectureInfo arch
+                           -- ^ Architecture information
+                        -> AbsBlockState (ArchReg arch)
+                        -> SegmentedAddr (RegAddrWidth (ArchReg arch))
+                        -> AbsBlockState (ArchReg arch)
+archPostSyscallAbsState archInfo = postCallAbsState params
+  where params = CallParams { postCallStackDelta = 0
+                            , preserveReg = preserveRegAcrossSyscall archInfo
+                            }

src/Data/Macaw/Architecture/Syscall.hs

@@ -25,7 +25,6 @@ data SyscallArgType = VoidArgType | WordArgType
 type SyscallTypeInfo = (String, SyscallArgType, [SyscallArgType])
 
 data SyscallPersonality arch =
-  SyscallPersonality { spName     :: String
-                     , spTypeInfo :: Map.Map Word64 SyscallTypeInfo
+  SyscallPersonality { spTypeInfo :: Map.Map Word64 SyscallTypeInfo
                      , spResultRegisters :: [Some (ArchReg arch)]
                      }

src/Data/Macaw/CFG.hs

@@ -64,7 +64,7 @@ module Data.Macaw.CFG
   , foldApp
   , traverseApp
   -- * RegState
-  , RegState(..)
+  , RegState
   , boundValue
   , cmpRegState
   , curIP
@@ -750,7 +750,7 @@ data Value arch ids tp
      -- ^ A constant bitvector
    | ( tp ~ BVType (ArchAddrWidth arch))
    => RelocatableValue !(NatRepr (ArchAddrWidth arch)) !(ArchSegmentedAddr arch)
-     -- ^ A value that can be relocated.
+     -- ^ A given memory address.
    | AssignedValue !(Assignment arch ids tp)
      -- ^ Value from an assignment statement.
    | Initial !(ArchReg arch tp)
@@ -995,13 +995,14 @@ asBaseOffset x
 ------------------------------------------------------------------------
 -- RegState
 
--- | This represents the state of the processor registers after some
--- execution.
-newtype RegState (r :: k -> *) (f :: k -> *)   = RegState (MapF.MapF r f)
---  deriving (FunctorF, FoldableF)
+-- | This represents the state of the processor registers.
+newtype RegState (r :: k -> *) (f :: k -> *) = RegState (MapF.MapF r f)
 
-deriving instance FunctorF (RegState r)
+deriving instance (OrdF r, EqF f) => Eq (RegState r f)
+
+deriving instance FunctorF  (RegState r)
 deriving instance FoldableF (RegState r)
+
 instance TraversableF (RegState r) where
   traverseF f (RegState m) = RegState <$> traverseF f m
 
@@ -1024,11 +1025,11 @@ boundValue r = lens getter setter
             Nothing -> error "internal error in boundValue given unexpected reg"
         setter (RegState m) v = RegState (MapF.insert r v m)
 
-instance (OrdF r, EqF f) => Eq (RegState r f) where
-  s == s' = cmpRegState eqF s s'
 
+-- | Compares if two register states are equal.
 cmpRegState :: OrdF r
             => (forall u. f u -> g u -> Bool)
+               -- ^ Function for checking if two values are equal.
             -> RegState r f
             -> RegState r g
             -> Bool

src/Data/Macaw/Discovery.hs

@@ -52,10 +52,10 @@ import           Data.Macaw.AbsDomain.AbsState
 import           Data.Macaw.AbsDomain.Refine
 import qualified Data.Macaw.AbsDomain.StridedInterval as SI
 import           Data.Macaw.Architecture.Info
-import           Data.Macaw.Architecture.Syscall
 import           Data.Macaw.CFG
 import           Data.Macaw.DebugLogging
 import           Data.Macaw.Discovery.Info
+--import           Data.Macaw.Discovery.JumpBounds
 import           Data.Macaw.Memory
 import qualified Data.Macaw.Memory.Permissions as Perm
 import           Data.Macaw.Types
@@ -184,14 +184,12 @@ runCFGM :: ArchitectureInfo arch
            -- ^ Memory to use when decoding instructions.
         -> Map (ArchSegmentedAddr arch) BS.ByteString
            -- ^ Names for (some) function entry points
-        -> SyscallPersonality arch
-           -- ^ Syscall personality
         -> (forall ids . CFGM arch ids ())
            -- ^ Computation to run.
         -> Some (DiscoveryInfo arch)
-runCFGM arch_info mem symbols sysp m = do
+runCFGM arch_info mem symbols m = do
   withGlobalSTNonceGenerator $ \nonce_gen -> do
-    let init_info = emptyDiscoveryInfo nonce_gen mem symbols sysp arch_info
+    let init_info = emptyDiscoveryInfo nonce_gen mem symbols arch_info
     Some <$> execStateT (unCFGM m) init_info
 
 printAddrBacktrace :: Map (ArchSegmentedAddr arch) (BlockRegion arch ids)
@@ -300,8 +298,8 @@ markCodeAddrBlock rsn addr ab = do
       -- Get block for addr
       tryDisassembleAddr rsn addr ab
       -- Get block for old block
-      let Just old_ab = Map.lookup l (s^.absState)
-      tryDisassembleAddr (brReason br) l old_ab
+      let Just old_code_info = Map.lookup l (s^.codeInfoMap)
+      tryDisassembleAddr (brReason br) l (old_code_info^.addrAbsBlockState)
       -- Add function starts to split to frontier
       -- This will result in us re-exploring l_start and a_start
       -- once the current function is done.
@@ -365,9 +363,12 @@ markAddrAsFunction rsn addr = do
     -- Get abstract state associated with function begining at address
     let abstState = fnBlockStateFn (archInfo s) mem addr
     markCodeAddrBlock rsn addr abstState
-    modify $ \s0 -> s0 & absState          %~ Map.insert addr abstState
+    let cInfo = CodeInfo { _addrAbsBlockState = abstState
+                         }
+    modify $ \s0 -> s0 & codeInfoMap       %~ Map.insert addr cInfo
                        & functionEntries   %~ Set.insert addr
-                       & function_frontier %~ maybeMapInsert low (SplitAt addr) . Map.insert addr rsn
+                       & function_frontier %~ maybeMapInsert low (SplitAt addr)
+                                           .  Map.insert addr rsn
 
 maybeMapInsert :: Ord a => Maybe a -> b -> Map a b -> Map a b
 maybeMapInsert mk v = maybe id (\k -> Map.insert k v) mk
@@ -412,7 +413,7 @@ assignmentAbsValues :: forall arch ids
                     => ArchitectureInfo arch
                     -> Memory (ArchAddrWidth arch)
                     -> CFG arch ids
-                    -> AbsStateMap arch
+                    -> Map (ArchSegmentedAddr arch) (CodeInfo arch)
                     -> MapF (AssignId ids) (ArchAbsValue arch)
 assignmentAbsValues info mem g absm =
      foldl' go MapF.empty (Map.elems (g^.cfgBlocks))
@@ -422,10 +423,12 @@ assignmentAbsValues info mem g absm =
         go m0 b =
           case blockLabel b of
             GeneratedBlock a 0 -> do
-              let w = addrWidthNatRepr (archAddrWidth info)
-              let Just ab = Map.lookup a absm
-              let abs_state = initAbsProcessorState w mem ab
-              insBlock b abs_state m0
+              case Map.lookup a absm of
+                Nothing -> do
+                  error $ "assignmentAbsValues could not find code infomation for block " ++ show a
+                Just codeInfo -> do
+                  let abs_state = initAbsProcessorState mem (codeInfo^.addrAbsBlockState)
+                  insBlock b abs_state m0
             _ -> m0
 
         insBlock :: Block arch ids
@@ -471,19 +474,21 @@ mergeIntraJump src ab tgt = do
   let upd new s = do
         -- Add reverse edge
         s & reverseEdges %~ Map.insertWith Set.union tgt (Set.singleton (labelAddr src))
-          & absState %~ Map.insert tgt new
-          & frontier %~ Map.insert tgt rsn
+          & codeInfoMap  %~ Map.insert tgt new
+          & frontier     %~ Map.insert tgt rsn
   s0 <- get
-  case Map.lookup tgt (s0^.absState) of
+  let cinfo_new = CodeInfo { _addrAbsBlockState = ab
+                           }
+  case Map.lookup tgt (s0^.codeInfoMap) of
     -- We have seen this block before, so need to join and see if
     -- the results is changed.
-    Just ab_old ->
-      case joinD ab_old ab of
+    Just cinfo_old ->
+      case unionCodeInfo cinfo_old cinfo_new of
         Nothing  -> return ()
         Just new -> modify $ upd new
     -- We haven't seen this block before
     Nothing -> do
-      modify $ upd ab
+      modify $ upd cinfo_new
       markCodeAddrBlock rsn tgt ab
 
 -- -----------------------------------------------------------------------------
@@ -563,7 +568,7 @@ fetchAndExecute b regs' s' = do
         let abst = finalAbsBlockState regs' s'
         seq abst $ do
         -- Merge caller return information
-        mergeIntraJump lbl (postCallAbsStateFn arch_info abst ret) ret
+        mergeIntraJump lbl (archPostCallAbsState arch_info abst ret) ret
         -- Look for new ips.
         let addrs = concretizeAbsCodePointers mem (abst^.absRegState^.curIP)
         mapM_ (markAddrAsFunction (CallTarget src)) addrs
@@ -629,7 +634,10 @@ fetchAndExecute b regs' s' = do
             mapM_ (recordWriteStmt src regs') (blockStmts b)
 
             -- Try to compute jump table bounds
-            let mread_end = getJumpTableBounds regs' base jump_idx
+            read_end <-
+              case getJumpTableBounds regs' base jump_idx of
+                Just e -> pure e
+                Nothing -> error $ "Could not compute jump bounds."
 
             let abst :: AbsBlockState (ArchReg arch)
                 abst = finalAbsBlockState regs' s'
@@ -644,7 +652,7 @@ fetchAndExecute b regs' s' = do
                             -> ArchAddr arch
                                -- /\ Current index
                             -> CFGM arch ids [ArchSegmentedAddr arch]
-                resolveJump prev idx | Just idx == mread_end = do
+                resolveJump prev idx | idx == read_end = do
                   -- Stop jump table when we have reached computed bounds.
                   return (reverse prev)
                 resolveJump prev idx = do
@@ -660,7 +668,7 @@ fetchAndExecute b regs' s' = do
                         mergeIntraJump lbl abst' tgt_addr
                         resolveJump (tgt_addr:prev) (idx+1)
                     _ -> do
-                      debug DCFG ("Stop jump table: " ++ show idx ++ " " ++ show mread_end) $ do
+                      debug DCFG ("Stop jump table: " ++ show idx ++ " " ++ show read_end) $ do
                       return (reverse prev)
             read_addrs <- resolveJump [] 0
             let last_index = fromIntegral (length read_addrs)
@@ -696,7 +704,6 @@ transferBlock :: TransferConstraints arch
 transferBlock b regs = do
   let lbl = blockLabel b
   let src = labelAddr lbl
-  debugM DCFG ("transferBlock " ++ show lbl)
   mem <- gets memory
   arch_info <- gets archInfo
   let regs' = transferStmts arch_info regs (blockStmts b)
@@ -722,7 +729,7 @@ transferBlock b regs = do
       let ips = concretizeAbsCodePointers mem (abst^.absRegState^.curIP)
       -- Merge system call result with possible next IPs.
       Fold.forM_ ips $ \addr -> do
-        mergeIntraJump lbl (postSyscallFn arch_info abst addr)  addr
+        mergeIntraJump lbl (archPostSyscallAbsState arch_info abst addr)  addr
 
     FetchAndExecute s' -> do
       fetchAndExecute b regs' s'
@@ -739,13 +746,12 @@ transfer addr = do
   case mroot of
     Nothing -> return ()
     Just root -> do
-      addrWidth <- gets $ addrWidthNatRepr . archAddrWidth . archInfo
-      mab <- uses absState $ Map.lookup addr
-      case mab of
+      minfo <- use $ codeInfoMap . at addr
+      case minfo of
         Nothing -> error $ "Could not find block " ++ show addr ++ "."
-        Just ab -> do
+        Just info -> do
           transferBlock root $
-            initAbsProcessorState addrWidth mem ab
+            initAbsProcessorState mem (info^.addrAbsBlockState)
 
 ------------------------------------------------------------------------
 -- Main loop
@@ -765,7 +771,7 @@ explore_frontier = do
                          -- Delete any entries we previously discovered for function.
                        & reverseEdges    %~ deleteMapRange (Just addr) high
                          -- Delete any entries we previously discovered for function.
-                       & absState        %~ deleteMapRange (Just addr) high
+                       & codeInfoMap     %~ deleteMapRange (Just addr) high
           put st'
           explore_frontier
     Just ((addr,_rsn), next_roots) -> do
@@ -789,8 +795,6 @@ cfgFromAddrs :: forall arch
                 -- ^ Memory to use when decoding instructions.
              -> Map (ArchSegmentedAddr arch) BS.ByteString
                 -- ^ Names for (some) function entry points
-             -> SyscallPersonality arch
-                -- ^ Syscall personality
              -> [ArchSegmentedAddr arch]
                 -- ^ Initial function entry points.
              -> [(ArchSegmentedAddr arch, ArchSegmentedAddr arch)]
@@ -799,8 +803,8 @@ cfgFromAddrs :: forall arch
                 --
                 -- Each entry contains an address and the value stored in it.
              -> Some (DiscoveryInfo arch)
-cfgFromAddrs arch_info mem symbols sysp init_addrs mem_words =
-  runCFGM arch_info mem symbols sysp $ do
+cfgFromAddrs arch_info mem symbols init_addrs mem_words =
+  runCFGM arch_info mem symbols $ do
     -- Set abstract state for initial functions
     mapM_ (markAddrAsFunction InitAddr) init_addrs
     explore_frontier

src/Data/Macaw/Discovery/Info.hs

@@ -23,7 +23,6 @@ module Data.Macaw.Discovery.Info
     -- * The interpreter state
   , DiscoveryInfo
   , emptyDiscoveryInfo
-  , syscallPersonality
   , nonceGen
   , archInfo
   , memory
@@ -39,8 +38,10 @@ module Data.Macaw.Discovery.Info
   , frontier
   , function_frontier
     -- ** Abstract state information
-  , absState
-  , AbsStateMap
+  , CodeInfo(..)
+  , addrAbsBlockState
+  , codeInfoMap
+  , unionCodeInfo
     -- ** DiscoveryInfo utilities
   , getFunctionEntryPoint
   , inSameFunction
@@ -57,18 +58,17 @@ import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Nonce
-import           Data.Sequence (Seq)
-import qualified Data.Sequence as Seq
 import           Data.Set (Set)
 import qualified Data.Set as Set
 import           Data.Text (Text)
+import           Data.Sequence (Seq)
+import qualified Data.Sequence as Seq
 import qualified Data.Vector as V
 import           Data.Word
 import           Numeric (showHex)
 
 import           Data.Macaw.AbsDomain.AbsState
 import           Data.Macaw.Architecture.Info
-import           Data.Macaw.Architecture.Syscall
 import           Data.Macaw.CFG
 import           Data.Macaw.Memory
 import qualified Data.Macaw.Memory.Permissions as Perm
@@ -77,8 +77,29 @@ import           Data.Macaw.Types
 ------------------------------------------------------------------------
 -- AbsStateMap
 
+-- | All information specifc about a discovered code address.
+data CodeInfo arch = CodeInfo
+  { _addrAbsBlockState :: !(AbsBlockState (ArchReg arch))
+  }
+
+-- | The abstract state at the beginning of the code block.
+addrAbsBlockState :: Simple Lens (CodeInfo arch) (AbsBlockState (ArchReg arch))
+addrAbsBlockState = lens _addrAbsBlockState (\s v -> s { _addrAbsBlockState = v })
+
+-- | 'joinCodeInfo x y' returns 'Nothing' if all states represented by 'y' are
+-- also in 'x', and 'Just z' where 'z' represents an overapproximation
+-- of the union of the states 'x' and 'y'.
+unionCodeInfo :: RegisterInfo (ArchReg arch)
+              => CodeInfo arch
+              -> CodeInfo arch
+              -> Maybe (CodeInfo arch)
+unionCodeInfo x y =
+  case joinD (x^.addrAbsBlockState) (y^.addrAbsBlockState) of
+    Just z -> Just CodeInfo { _addrAbsBlockState = z }
+    Nothing -> Nothing
+
 -- | Maps each code address to a set of abstract states
-type AbsStateMap arch = Map (ArchSegmentedAddr arch) (AbsBlockState (ArchReg arch))
+--type AbsStateMap arch = Map (ArchSegmentedAddr arch) (CodeInfo arch))
 
 ------------------------------------------------------------------------
 -- BlockRegion
@@ -187,8 +208,6 @@ data DiscoveryInfo arch ids
                      -- ^ The initial memory when disassembly started.
                    , symbolNames :: !(Map (ArchSegmentedAddr arch) BS.ByteString)
                      -- ^ The set of symbol names (not necessarily complete)
-                   , syscallPersonality :: !(SyscallPersonality arch)
-                     -- ^ Syscall personality, mainly used by classifyBlock etc.
                    , archInfo :: !(ArchitectureInfo arch)
                      -- ^ Architecture-specific information needed for discovery.
                    , _blocks   :: !(Map (ArchSegmentedAddr arch) (BlockRegion arch ids))
@@ -205,14 +224,14 @@ data DiscoveryInfo arch ids
                      -- inferred about it.
                    , _frontier :: !(Map (ArchSegmentedAddr arch)
                                         (CodeAddrReason (ArchAddrWidth arch)))
-                     -- ^ Set of addresses to explore next.
+                     -- ^ Addresses to explore next.
                      --
-                     -- This is a map so that we can associate a reason why a code address
-                     -- was added to the frontier.
+                     -- This is a map so that we can associate a reason why a code
+                     -- address was added to the frontier.
                    , _function_frontier :: !(Map (ArchSegmentedAddr arch)
                                                  (CodeAddrReason (ArchAddrWidth arch)))
                      -- ^ Set of functions to explore next.
-                   , _absState :: !(AbsStateMap arch)
+                   , _codeInfoMap :: !(Map (ArchSegmentedAddr arch) (CodeInfo arch))
                      -- ^ Map from code addresses to the abstract state at the start of
                      -- the block.
                    }
@@ -221,15 +240,13 @@ data DiscoveryInfo arch ids
 emptyDiscoveryInfo :: NonceGenerator (ST ids) ids
                    -> Memory (ArchAddrWidth arch)
                    -> Map (ArchSegmentedAddr arch) BS.ByteString
-                   -> SyscallPersonality arch
                    -> ArchitectureInfo arch
-                      -- ^ Stack delta
+                      -- ^ architecture/OS specific information
                    -> DiscoveryInfo arch ids
-emptyDiscoveryInfo ng mem symbols sysp info = DiscoveryInfo
+emptyDiscoveryInfo ng mem symbols info = DiscoveryInfo
       { nonceGen           = ng
       , memory             = mem
       , symbolNames        = symbols
-      , syscallPersonality = sysp
       , archInfo           = info
       , _blocks            = Map.empty
       , _functionEntries   = Set.empty
@@ -237,7 +254,7 @@ emptyDiscoveryInfo ng mem symbols sysp info = DiscoveryInfo
       , _globalDataMap     = Map.empty
       , _frontier          = Map.empty
       , _function_frontier = Map.empty
-      , _absState          = Map.empty
+      , _codeInfoMap       = Map.empty
       }
 
 blocks :: Simple Lens (DiscoveryInfo arch ids)
@@ -272,8 +289,9 @@ function_frontier :: Simple Lens (DiscoveryInfo arch ids)
                                       (CodeAddrReason (ArchAddrWidth arch)))
 function_frontier = lens _function_frontier (\s v -> s { _function_frontier = v })
 
-absState :: Simple Lens (DiscoveryInfo arch ids) (AbsStateMap arch)
-absState = lens _absState (\s v -> s { _absState = v })
+codeInfoMap :: Simple Lens (DiscoveryInfo arch ids)
+                        (Map (ArchSegmentedAddr arch) (CodeInfo arch))
+codeInfoMap = lens _codeInfoMap (\s v -> s { _codeInfoMap = v })
 
 ------------------------------------------------------------------------
 -- DiscoveryInfo utilities
@@ -440,8 +458,8 @@ tryGetStaticSyscallNo interp_state block_addr proc_state
   | BVValue _ call_no <- proc_state^.boundValue syscall_num_reg =
     Just call_no
   | Initial r <- proc_state^.boundValue syscall_num_reg
-  , Just absSt <- Map.lookup block_addr (interp_state ^. absState) =
-    asConcreteSingleton (absSt ^. absRegState ^. boundValue r)
+  , Just absSt <- interp_state^.codeInfoMap^.at block_addr =
+    asConcreteSingleton (absSt^.addrAbsBlockState^.absRegState^.boundValue r)
   | otherwise =
     Nothing
 

src/Data/Macaw/Discovery/JumpBounds.hs

@@ -0,0 +1,152 @@
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Data.Macaw.Discovery.JumpBounds
+  ( InitialIndexBounds
+  , arbitraryInitialBounds
+  , joinInitialBounds
+  , IndexBounds
+  , mkIndexBounds
+  , addUpperBounds
+  , lookupUpperBound
+  , nextBlockBounds
+  ) where
+
+import           Control.Lens
+import           Control.Monad.State
+import           Data.Functor
+import           Data.Parameterized.Map (MapF)
+import qualified Data.Parameterized.Map as MapF
+import           Data.Parameterized.NatRepr (maxUnsigned)
+
+import           Data.Macaw.CFG
+import           Data.Macaw.Types
+
+-- | An upper bound on a value.
+data UpperBounds tp = forall w . (tp ~ BVType w) => IntegerUpperBound Integer
+
+instance Eq (UpperBounds tp) where
+  IntegerUpperBound x == IntegerUpperBound y = x == y
+
+instance MapF.EqF UpperBounds where
+  eqF = (==)
+
+instance Ord (UpperBounds tp) where
+  compare (IntegerUpperBound x) (IntegerUpperBound y) = compare x y
+
+-- | Bounds for a function as the start of a block.
+data InitialIndexBounds r
+   = InitialIndexBounds { initialRegUpperBounds :: !(MapF r UpperBounds)
+                        }
+
+instance MapF.TestEquality r => Eq (InitialIndexBounds r) where
+   x == y = initialRegUpperBounds x == initialRegUpperBounds y
+
+-- | Create initial index bounds that can represent any system state.
+arbitraryInitialBounds :: InitialIndexBounds reg
+arbitraryInitialBounds = InitialIndexBounds { initialRegUpperBounds = MapF.empty }
+
+
+type Changed = State Bool
+
+markChanged :: Bool -> Changed ()
+markChanged b = modify (|| b)
+
+runChanged :: Changed a -> Maybe a
+runChanged action =
+  case runState action False of
+    (r, True)  -> Just r
+    (_, False) -> Nothing
+
+-- | Take the union of two index bounds
+joinInitialBounds :: forall r
+                  .  MapF.OrdF r
+                  => InitialIndexBounds r
+                  -> InitialIndexBounds r
+                  -> Maybe (InitialIndexBounds r)
+joinInitialBounds old new = runChanged $ do
+  let combineF :: r tp -> UpperBounds tp -> UpperBounds tp -> Changed (Maybe (UpperBounds tp))
+      combineF _ (IntegerUpperBound x) (IntegerUpperBound y) =
+        markChanged (x < y) $> Just (IntegerUpperBound (max x y))
+
+      -- Mark upper bounds exclusively in old set.
+      -- If we have any only-old bounds add mark value as changed.
+      oldF :: MapF r UpperBounds -> Changed (MapF r UpperBounds)
+      oldF m = markChanged (not (MapF.null m)) $> MapF.empty
+
+      -- How to upper bounds exclusively in new set.
+      -- Drop any only-new bounds.
+      newF :: MapF r UpperBounds -> Changed (MapF r UpperBounds)
+      newF _ = pure MapF.empty
+
+  z <- MapF.mergeWithKeyM combineF oldF newF (initialRegUpperBounds old) (initialRegUpperBounds new)
+  pure InitialIndexBounds { initialRegUpperBounds = z }
+
+-- | Information about bounds for a particular value within a block.
+data IndexBounds reg ids
+   = IndexBounds { _regBounds :: !(MapF reg UpperBounds)
+                 , _assignUpperBounds :: !(MapF (AssignId ids) UpperBounds)
+                 }
+
+-- | Maps assignment ids to the associated upper bounds
+regBounds :: Simple Lens (IndexBounds reg ids) (MapF reg UpperBounds)
+regBounds = lens _regBounds (\s v -> s { _regBounds = v })
+
+-- | Maps assignment ids to the associated upper bounds
+assignUpperBounds :: Simple Lens (IndexBounds reg ids) (MapF (AssignId ids) UpperBounds)
+assignUpperBounds = lens _assignUpperBounds (\s v -> s { _assignUpperBounds = v })
+
+-- | Create index bounds from initial index bounds.
+mkIndexBounds :: InitialIndexBounds reg -> IndexBounds reg ids
+mkIndexBounds i = IndexBounds { _regBounds = initialRegUpperBounds i
+                              , _assignUpperBounds = MapF.empty
+                              }
+
+addUpperBounds :: ( MapF.OrdF (ArchReg arch)
+                  , HasRepr (ArchReg arch) TypeRepr
+                  )
+               => BVValue arch ids w
+               -> Integer -- ^ Upper bound as an unsigned number
+               -> IndexBounds (ArchReg arch) ids
+               -> Either String (IndexBounds (ArchReg arch) ids)
+addUpperBounds v u bnds
+    -- Do nothing if upper bounds equals or exceeds function
+  | u >= maxUnsigned (valueWidth v) = Right bnds
+  | u < 0 = error "addUpperBounds given negative value."
+  | otherwise =
+  case v of
+    BVValue _ c | c <= u -> Right bnds
+                | otherwise -> Left "Constant given upper bound that is statically less than given bounds"
+    RelocatableValue{} -> Left "Relocatable value does not have upper bounds."
+    AssignedValue a ->
+      Right $ bnds & assignUpperBounds %~ MapF.insertWith min (assignId a) (IntegerUpperBound u)
+    Initial r ->
+      Right $ bnds & regBounds %~ MapF.insertWith min r (IntegerUpperBound u)
+
+lookupUpperBound :: ( MapF.OrdF (ArchReg arch)
+                    , Show (ArchReg arch (BVType w))
+                    )
+                 => BVValue arch ids w
+                 -> IndexBounds (ArchReg arch) ids
+                 -> Either String Integer
+lookupUpperBound v bnds =
+  case v of
+    BVValue _ i -> Right i
+    RelocatableValue{} -> Left "Relocatable values do not have bounds."
+    AssignedValue a ->
+      case MapF.lookup (assignId a) (bnds^.assignUpperBounds) of
+        Just (IntegerUpperBound bnd) -> Right bnd
+        Nothing -> Left $ "Could not find upper bounds for " ++ show (assignId a) ++ "."
+    Initial r ->
+      case MapF.lookup r (bnds^.regBounds) of
+        Just (IntegerUpperBound bnd) -> Right bnd
+        Nothing -> Left $ "Could not find upper bounds for " ++ show r ++ "."
+
+nextBlockBounds :: RegState r (Value arch ids)
+                -> IndexBounds (ArchReg arch) ids
+                -> InitialIndexBounds (ArchReg arch)
+nextBlockBounds _regs _bnds =
+  let m = undefined
+   in InitialIndexBounds { initialRegUpperBounds = m
+                         }