Provide jumptable layout info

base/src/Data/Macaw/Analysis/FunctionArgs.hs

@@ -683,7 +683,7 @@ summarizeBlock b = do
       -- Compute all transfers
       recordBlockTransfer blockAddr regs archRegs
 
-    ParsedLookupTable regs lookupIdx _vec -> do
+    ParsedLookupTable _layout regs lookupIdx _vec -> do
       demandValue blockAddr lookupIdx
       -- record all propagations
       recordBlockTransfer blockAddr regs archRegs

base/src/Data/Macaw/Analysis/RegisterUse.hs

@@ -1175,7 +1175,7 @@ blockStartConstraints rctx blockMap addr (BSC cns) lastMap frontierMap = do
       let (pvm, frontierMap') = foldl' (visitIntraJumpTarget lastFn ctx s regs) (Map.empty, frontierMap) [t,f]
       let m' = Map.insert addr (b, BSC cns, s, pvm) lastMap
       pure $ (m', frontierMap')
-    ParsedLookupTable regs _idx lbls -> do
+    ParsedLookupTable _layout regs _idx lbls -> do
       let (pvm, frontierMap') = foldl' (visitIntraJumpTarget lastFn ctx s regs) (Map.empty, frontierMap) lbls
       let m' = Map.insert addr (b, BSC cns, s, pvm) lastMap
       pure $ (m', frontierMap')
@@ -1616,7 +1616,7 @@ mkBlockUsageSummary ctx cns sis blk = do
       ParsedBranch regs cond _t _f  -> do
         demandValue cond
         recordRegMap (regStateMap regs)
-      ParsedLookupTable regs idx _tgts -> do
+      ParsedLookupTable _layout regs idx _tgts -> do
         demandValue idx
         recordRegMap (regStateMap regs)
       ParsedCall regs _mret -> do

base/src/Data/Macaw/Discovery.hs

@@ -62,6 +62,9 @@ module Data.Macaw.Discovery
        , State.pblockStmts
        , State.pblockTermStmt
        , State.ParsedTermStmt(..)
+       , State.JumpTableLayout
+       , State.jtlBackingAddr
+       , State.jtlBackingSize
          -- * Simplification
        , eliminateDeadStmts
        ) where
@@ -92,6 +95,7 @@ import           Data.Set (Set)
 import qualified Data.Set as Set
 import qualified Data.Text as Text
 import qualified Data.Vector as V
+import           Data.Word
 import           GHC.IO (ioToST)
 import           Numeric
 import           Numeric.Natural
@@ -117,7 +121,6 @@ import           Data.Macaw.Discovery.State as State
 import qualified Data.Macaw.Memory.Permissions as Perm
 import           Data.Macaw.Types
 
-
 ------------------------------------------------------------------------
 -- Utilities
 
@@ -214,7 +217,7 @@ addParsedBlockDemands b = do
       traverseF_ addValueDemands regs
     ParsedBranch regs _ _ _ -> do
       traverseF_ addValueDemands regs
-    ParsedLookupTable regs _idx _tbl  -> do
+    ParsedLookupTable _layout regs _idx _tbl  -> do
       traverseF_ addValueDemands regs
     ParsedReturn regs -> do
       traverseF_ addValueDemands regs
@@ -452,39 +455,7 @@ mergeIntraJump src (tgt, ab, bnds) = do
       foundAddrs %= Map.insert tgt found_info
 
 -------------------------------------------------------------------------------
--- BoundedMemArray
-
--- | This describes a region of memory dereferenced in some array read.
---
--- These regions may be be sparse, given an index `i`, the
--- the address given by 'arBase' + 'arIx'*'arStride'.
-data BoundedMemArray arch tp = BoundedMemArray
-  { arBase   :: !(MemSegmentOff (ArchAddrWidth arch))
-    -- ^ The base address for array accesses.
-  , arStride :: !Natural
-    -- ^ Space between elements of the array.
-    --
-    -- This will typically be the number of bytes denoted by `arEltType`,
-    -- but may be larger for sparse arrays.  `matchBoundedMemArray` will fail
-    -- if stride is less than the number of bytes read.
-  , arEltType   :: !(MemRepr tp)
-    -- ^ Resolved type of elements in this array.
-  , arSlices       :: !(V.Vector [MemChunk (ArchAddrWidth arch)])
-    -- ^ The slices of memory in the array.
-    --
-    -- The `i`th element in the vector corresponds to the first `size`
-    -- bytes at address `base + stride * i`.
-    --
-    -- This could be computed from the previous fields, but we check we
-    -- can create it when creating the array read, so we store it to
-    -- avoid recomputing it.
-  }
-
-deriving instance RegisterInfo (ArchReg arch) => Show (BoundedMemArray arch tp)
-
--- | Return true if the address stored is readable and not writable.
-isReadOnlyBoundedMemArray :: BoundedMemArray arch  tp -> Bool
-isReadOnlyBoundedMemArray = Perm.isReadonly . segmentFlags . segoffSegment . arBase
+-- BoundedMemArray recognition
 
 absValueAsSegmentOff
   :: forall w
@@ -590,14 +561,15 @@ matchBoundedMemArray mem aps jmpBounds val = do
    -- Check stride covers at least number of bytes read.
   when (memReprBytes tp > stride) $ do
     fail "Stride does not cover size of relocation."
-  -- Resolve a static upper bound to array.
-
+  -- Convert stride to word64 (must be lossless due to as memory is at most 64-bits)
+  let stridew :: Word64
+      stridew = fromIntegral stride
   -- Take the given number of bytes out of each slices
   slices <- extractJumpTableSlices jmpBounds base stride ixVal tp
 
   let r = BoundedMemArray
           { arBase     = base
-          , arStride   = stride
+          , arStride   = stridew
           , arEltType  = tp
           , arSlices   = slices
           }
@@ -606,16 +578,6 @@ matchBoundedMemArray mem aps jmpBounds val = do
 ------------------------------------------------------------------------
 -- Extension
 
--- | Information about a value that is the signed or unsigned extension of another
--- value.
---
--- This is used for jump tables, and only supports widths that are in memory
-data Extension w = Extension { _extIsSigned :: !Bool
-                             , _extWidth :: !(AddrWidthRepr w)
-                               -- ^ Width of argument. is to.
-                             }
-  deriving (Show)
-
 -- | Just like Some (BVValue arch ids), but doesn't run into trouble with
 -- partially applying the BVValue type synonym.
 data SomeExt arch ids = forall m . SomeExt !(BVValue arch ids m) !(Extension m)
@@ -647,29 +609,8 @@ extendDyn (Extension False Addr64) end bs  = toInteger (bsWord64 end bs)
 extendDyn (Extension True  Addr32) end bs = toInteger (fromIntegral (bsWord32 end bs) :: Int32)
 extendDyn (Extension True  Addr64) end bs = toInteger (fromIntegral (bsWord64 end bs) :: Int64)
 
-------------------------------------------------------------------------
--- JumpTableLayout
-
--- | This describes the layout of a jump table.
--- Beware: on some architectures, after reading from the jump table, the
--- resulting addresses must be aligned. See the IPAlignment class.
-data JumpTableLayout arch
-  = AbsoluteJumpTable !(BoundedMemArray arch (BVType (ArchAddrWidth arch)))
-  -- ^ `AbsoluteJumpTable r` describes a jump table where the jump
-  -- target is directly stored in the array read `r`.
-  | forall w . RelativeJumpTable !(ArchSegmentOff arch)
-                                 !(BoundedMemArray arch (BVType w))
-                                 !(Extension w)
-  -- ^ `RelativeJumpTable base read ext` describes information about a
-  -- jump table where all jump targets are relative to a fixed base
-  -- address.
-  --
-  -- The value is computed as `baseVal + readVal` where
-  --
-  -- `baseVal = fromMaybe 0 base`, `readVal` is the value stored at
-  -- the memory read described by `read` with the sign of `ext`.
-
-deriving instance RegisterInfo (ArchReg arch) => Show (JumpTableLayout arch)
+--------------------------------------------------------------------------------
+-- Jump table recognition
 
 -- This function resolves jump table entries.
 -- It is a recursive function that has an index into the jump table.
@@ -1301,13 +1242,13 @@ jumpTableClassifier = classifierName "Jump table" $ do
     let jumpTableClassifiers
           =   matchAbsoluteJumpTable
           <|> matchRelativeJumpTable
-    (_jt, entries, jumpIndex) <- lift $
+    (layout, entries, jumpIndex) <- lift $
       runReaderT jumpTableClassifiers bcc
 
     let abst :: AbsBlockState (ArchReg arch)
         abst = finalAbsBlockState (classifierAbsState bcc) (classifierFinalRegState bcc)
     let nextBnds = Jmp.postJumpBounds jmpBounds (classifierFinalRegState bcc)
-    let term = ParsedLookupTable (classifierFinalRegState bcc) jumpIndex entries
+    let term = ParsedLookupTable layout (classifierFinalRegState bcc) jumpIndex entries
     pure $ seq abst $
       ParsedContents { parsedNonterm = toList (classifierStmts bcc)
                      , parsedTerm = term

base/src/Data/Macaw/Discovery/State.hs

@@ -13,13 +13,8 @@ representing this information.
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Data.Macaw.Discovery.State
-  ( GlobalDataInfo(..)
-  , ParsedTermStmt(..)
-  , parsedTermSucc
-  , ParsedBlock(..)
-    -- * The interpreter state
-  , DiscoveryState
-  , NoReturnFunStatus(..)
+  ( -- * DiscoveryState
+    DiscoveryState
   , AddrSymMap
   , exploredFunctions
   , ppDiscoveryStateBlocks
@@ -27,15 +22,31 @@ module Data.Macaw.Discovery.State
   , memory
   , symbolNames
   , archInfo
+  , GlobalDataInfo(..)
   , globalDataMap
   , funInfo
   , unexploredFunctions
+  , NoReturnFunStatus(..)
   , trustedFunctionEntryPoints
   , exploreFnPred
     -- * DiscoveryFunInfo
   , DiscoveryFunInfo(..)
   , discoveredFunName
   , parsedBlocks
+    -- ** Parsed block
+  , ParsedBlock(..)
+    -- ** Block terminal statements
+  , ParsedTermStmt(..)
+  , parsedTermSucc
+    -- ** JumpTableLayout
+  , JumpTableLayout(..)
+  , Extension(..)
+  , jtlBackingAddr
+  , jtlBackingSize
+    -- * BoundedMemArray
+  , BoundedMemArray(..)
+  , arByteCount
+  , isReadOnlyBoundedMemArray
     -- * Reasons for exploring
   , FunctionExploreReason(..)
   , BlockExploreReason(..)
@@ -53,6 +64,7 @@ import qualified Data.Parameterized.Map as MapF
 import           Data.Parameterized.Some
 import           Data.Text (Text)
 import qualified Data.Vector as V
+import           Data.Word
 import           Numeric (showHex)
 import           Prettyprinter as PP
 
@@ -60,6 +72,7 @@ import           Data.Macaw.AbsDomain.AbsState
 import qualified Data.Macaw.AbsDomain.JumpBounds as Jmp
 import           Data.Macaw.Architecture.Info
 import           Data.Macaw.CFG
+import qualified Data.Macaw.Memory.Permissions as Perm
 import           Data.Macaw.Types
 
 ------------------------------------------------------------------------
@@ -121,6 +134,95 @@ instance (Integral w, Show w) => Show (GlobalDataInfo w) where
                             | otherwise = error "jump table with negative offset given"
   show ReferencedValue = "global addr"
 
+-------------------------------------------------------------------------------
+-- BoundedMemArray
+
+-- | This describes a region of memory dereferenced in some array read.
+--
+-- These regions may be be sparse, given an index `i`, the
+-- the address given by 'arBase' + 'arIx'*'arStride'.
+data BoundedMemArray arch tp = BoundedMemArray
+  { arBase   :: !(MemSegmentOff (ArchAddrWidth arch))
+    -- ^ The base address for array accesses.
+  , arStride :: !Word64
+    -- ^ Space between elements of the array.
+    --
+    -- This will typically be the number of bytes denoted by `arEltType`,
+    -- but may be larger for sparse arrays.  `matchBoundedMemArray` will fail
+    -- if stride is less than the number of bytes read.
+  , arEltType   :: !(MemRepr tp)
+    -- ^ Resolved type of elements in this array.
+  , arSlices       :: !(V.Vector [MemChunk (ArchAddrWidth arch)])
+    -- ^ The slices of memory in the array.
+    --
+    -- The `i`th element in the vector corresponds to the first `size`
+    -- bytes at address `base + stride * i`.
+    --
+    -- The number of elements is the length of the array.
+    --
+    -- N.B.  With the size could be computed from the previous fields,
+    -- but we check we can create it when creating the array read, so
+    -- we store it to avoid recomputing it.
+  }
+
+deriving instance RegisterInfo (ArchReg arch) => Show (BoundedMemArray arch tp)
+
+-- | Return number of bytes used by this array.
+arByteCount :: BoundedMemArray arch tp -> Word64
+arByteCount a = arStride a * fromIntegral (V.length (arSlices a))
+
+-- | Return true if the address stored is readable and not writable.
+isReadOnlyBoundedMemArray :: BoundedMemArray arch  tp -> Bool
+isReadOnlyBoundedMemArray = Perm.isReadonly . segmentFlags . segoffSegment . arBase
+
+------------------------------------------------------------------------
+-- Extension
+
+-- | Information about a value that is the signed or unsigned extension of another
+-- value.
+--
+-- This is used for jump tables, and only supports widths that are in memory
+data Extension w = Extension { _extIsSigned :: !Bool
+                             , _extWidth :: !(AddrWidthRepr w)
+                               -- ^ Width of argument. is to.
+                             }
+  deriving (Show)
+
+
+------------------------------------------------------------------------
+-- JumpTableLayout
+
+-- | This describes the layout of a jump table.
+-- Beware: on some architectures, after reading from the jump table, the
+-- resulting addresses must be aligned. See the IPAlignment class.
+data JumpTableLayout arch
+  = AbsoluteJumpTable !(BoundedMemArray arch (BVType (ArchAddrWidth arch)))
+  -- ^ `AbsoluteJumpTable r` describes a jump table where the jump
+  -- target is directly stored in the array read `r`.
+  | forall w . RelativeJumpTable !(ArchSegmentOff arch)
+                                 !(BoundedMemArray arch (BVType w))
+                                 !(Extension w)
+  -- ^ `RelativeJumpTable base read ext` describes information about a
+  -- jump table where all jump targets are relative to a fixed base
+  -- address.
+  --
+  -- The value is computed as `baseVal + readVal` where
+  --
+  -- `baseVal = fromMaybe 0 base`, `readVal` is the value stored at
+  -- the memory read described by `read` with the sign of `ext`.
+
+deriving instance RegisterInfo (ArchReg arch) => Show (JumpTableLayout arch)
+
+-- | Return base address of table storing contents of jump table.
+jtlBackingAddr :: JumpTableLayout arch ->  ArchSegmentOff arch
+jtlBackingAddr (AbsoluteJumpTable a) = arBase a
+jtlBackingAddr (RelativeJumpTable _ a _) = arBase a
+
+-- | Returns the number of bytes in the layout
+jtlBackingSize :: JumpTableLayout arch -> Word64
+jtlBackingSize (AbsoluteJumpTable a) = arByteCount a
+jtlBackingSize (RelativeJumpTable _ a _) = arByteCount a
+
 ------------------------------------------------------------------------
 -- ParsedTermStmt
 
@@ -175,7 +277,8 @@ data ParsedTermStmt arch ids
   -- to, and the possible addresses as a table.  If the index (when interpreted as
   -- an unsigned number) is larger than the number of entries in the vector, then the
   -- result is undefined.
-  | ParsedLookupTable !(RegState (ArchReg arch) (Value arch ids))
+  | ParsedLookupTable !(JumpTableLayout arch)
+                      !(RegState (ArchReg arch) (Value arch ids))
                       !(ArchAddrValue arch ids)
                       !(V.Vector (ArchSegmentOff arch))
   -- | A return with the given registers.
@@ -216,7 +319,7 @@ ppTermStmt tstmt =
       vcat
       [ "branch" <+> pretty c <+> viaShow t <+> viaShow f
       , indent 2 (pretty r) ]
-    ParsedLookupTable s idx entries ->
+    ParsedLookupTable _layout s idx entries ->
       vcat
       [ "ijump" <+> pretty idx
       , indent 2 (vcat (imap (\i v -> pretty i <+> ":->" <+> viaShow v)
@@ -254,7 +357,7 @@ parsedTermSucc ts = do
     PLTStub{} -> []
     ParsedJump _ tgt -> [tgt]
     ParsedBranch _ _ t f -> [t,f]
-    ParsedLookupTable _ _ v -> V.toList v
+    ParsedLookupTable _layout _ _ v -> V.toList v
     ParsedReturn{} -> []
     ParsedArchTermStmt _ _ ret -> maybeToList ret
     ParsedTranslateError{} -> []

deps/crucible

@@ -1 +1 @@
-Subproject commit c1da81f05e7a8ac80787e2f161ba341a312a6302
+Subproject commit 09532645133d39cda983bca67c2dbb91d05e4373

deps/dwarf

@@ -1 +1 @@
-Subproject commit 93648195d73fdbf45e982524663c66754ea468df
+Subproject commit ab74e6e73ec92cf3219823d5336f190a1464118b

deps/elf-edit

@@ -1 +1 @@
-Subproject commit fe018fbf6c2df56fc3f565d2732780c064228f1b
+Subproject commit 6a089cc6e84a35604168c10193c521fa1359481d

deps/llvm-pretty

@@ -1 +1 @@
-Subproject commit cf5c931061b48a4253e7eea15947eff7d9790f07
+Subproject commit f5e0ff3f3f6154842d3321031ca5a5031c91ecc6

deps/llvm-pretty-bc-parser

@@ -1 +1 @@
-Subproject commit 3d0d549486ceb101c38af3423426f3ff07aa966d
+Subproject commit c38b86b8b485c85181ab1bfc682fae194c8d4027

deps/macaw-loader

@@ -1 +1 @@
-Subproject commit de712a0cbd2a71d3e63c47f8bde3d72eb9d4e784
+Subproject commit 79c1a214de19677197f2b7e5f38562b3ba925be9

deps/semmc

@@ -1 +1 @@
-Subproject commit 906994d383b4d72e30cf479a255b0c5a884fc343
+Subproject commit a60ace5ab6036dcb0c63aec0dddd2324b288ef9c

deps/what4

@@ -1 +1 @@
-Subproject commit 3461006b5156904d82dedd32175849a6aa00059f
+Subproject commit cce1929ff63e48812993bf338a78533515b5ab77

refinement/src/Data/Macaw/Refinement/FuncBlockUtils.hs

@@ -70,7 +70,7 @@ blockTransferTo fi blkID =
           MDS.ParsedCall _ mbTgt | Just tgt <- mbTgt -> [tgt]
                                  | otherwise -> []
           MDS.ParsedJump _ tgt -> [tgt]
-          MDS.ParsedLookupTable _ _ tgts -> F.toList tgts
+          MDS.ParsedLookupTable _layout _ _ tgts -> F.toList tgts
           MDS.ParsedReturn {} -> []
           MDS.ParsedBranch _regs _cond trueTarget falseTarget -> [ trueTarget, falseTarget ]
           MDS.PLTStub _ tgt _ ->

refinement/src/Data/Macaw/Refinement/Path.hs

@@ -95,7 +95,7 @@ computeBackEdges cfg0 =
              addTargetsIfBackedges blockId blockAddr (addVisited acc) [target]
            MDS.ParsedBranch _ _ target1 target2 ->
              addTargetsIfBackedges blockId blockAddr (addVisited acc) [target1, target2]
-           MDS.ParsedLookupTable _ _ targets ->
+           MDS.ParsedLookupTable _layout _ _ targets ->
              addTargetsIfBackedges blockId blockAddr (addVisited acc) targets
            MDS.PLTStub _ retTarget _ ->
              addTargetsIfBackedges blockId blockAddr (addVisited acc) [retTarget]
@@ -169,7 +169,7 @@ mkPartialCFG fi = computeBackEdges graph
         MDS.ParsedBranch _ _ tgt1 tgt2 ->
           let g2 = F.foldl' (addEdge (cfgAddrNodes gr) nodeId) (cfg gr) [tgt1, tgt2]
           in gr { cfg = g2 }
-        MDS.ParsedLookupTable _ _ addrs ->
+        MDS.ParsedLookupTable _layout _ _ addrs ->
           let g2 = F.foldl' (addEdge (cfgAddrNodes gr) nodeId) (cfg gr) addrs
           in gr { cfg = g2 }
         MDS.ParsedCall _ (Just retAddr) ->
@@ -297,8 +297,8 @@ breakBackedges cfg0 slice =
           MDS.ParsedJump regs (replaceTarget backTargets tgt)
         MDS.ParsedBranch regs cond t1 t2 ->
           MDS.ParsedBranch regs cond (replaceTarget backTargets t1) (replaceTarget backTargets t2)
-        MDS.ParsedLookupTable regs val tgts ->
-          MDS.ParsedLookupTable regs val (fmap (replaceTarget backTargets) tgts)
+        MDS.ParsedLookupTable layout regs val tgts ->
+          MDS.ParsedLookupTable layout regs val (fmap (replaceTarget backTargets) tgts)
         MDS.ParsedReturn {} -> t
         MDS.ParsedArchTermStmt _ _ Nothing -> t
         MDS.ParsedArchTermStmt stmt regs (Just tgt) ->

symbolic/src/Data/Macaw/Symbolic.hs

@@ -404,7 +404,7 @@ termStmtToReturn tm0 =
     M.ParsedCall r _ -> M.ParsedReturn r
     M.ParsedJump r _ -> M.ParsedReturn r
     M.ParsedBranch r _ _ _ -> M.ParsedReturn r
-    M.ParsedLookupTable r _ _ -> M.ParsedReturn r
+    M.ParsedLookupTable _layout r _ _ -> M.ParsedReturn r
     M.ParsedArchTermStmt _ r _ -> M.ParsedReturn r
     M.ClassifyFailure r _ -> M.ParsedReturn r
     M.PLTStub{} -> tm0
@@ -422,7 +422,7 @@ termStmtToJump tm0 addr =
     M.ParsedBranch r _ _ _ -> M.ParsedJump r addr
     M.ParsedCall r _ -> M.ParsedJump r addr
     M.ParsedReturn r -> M.ParsedJump r addr
-    M.ParsedLookupTable r _ _ -> M.ParsedJump r addr
+    M.ParsedLookupTable _layout r _ _ -> M.ParsedJump r addr
     M.ParsedArchTermStmt _ r _ -> M.ParsedJump r addr
     M.ClassifyFailure r _ -> M.ParsedJump r addr
     M.PLTStub{} -> tm0
@@ -520,7 +520,7 @@ parsedTermTargets t =
     M.ParsedCall _ (Just ret) -> [ret]
     M.ParsedJump _ addr -> [addr]
     M.ParsedBranch _ _ taddr faddr -> [taddr, faddr]
-    M.ParsedLookupTable _ _ addrs -> F.toList addrs
+    M.ParsedLookupTable _layout _ _ addrs -> F.toList addrs
     M.ParsedReturn {} -> []
     M.ParsedArchTermStmt _ _ Nothing -> []
     M.ParsedArchTermStmt _ _ (Just addr) -> [addr]

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

@@ -1410,7 +1410,7 @@ addMacawParsedTermStmt blockLabelMap externalResolutions thisAddr tstmt = do
       let tlbl = parsedBlockLabel blockLabelMap trueAddr
       let flbl = parsedBlockLabel blockLabelMap falseAddr
       addTermStmt $! CR.Br crucCond tlbl flbl
-    M.ParsedLookupTable regs idx possibleAddrs -> do
+    M.ParsedLookupTable _layout regs idx possibleAddrs -> do
       setMachineRegs =<< createRegStruct regs
       addSwitch blockLabelMap idx possibleAddrs
     M.ParsedReturn regs -> do