From 6d1e47623d6de3b6c4009b36a4a1cf0af5d1a2a6 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 27 Jan 2021 15:20:17 -0800 Subject: [PATCH] Provide jumptable layout info --- base/src/Data/Macaw/Analysis/FunctionArgs.hs | 2 +- base/src/Data/Macaw/Analysis/RegisterUse.hs | 4 +- base/src/Data/Macaw/Discovery.hs | 87 ++----------- base/src/Data/Macaw/Discovery/State.hs | 123 ++++++++++++++++-- deps/crucible | 2 +- deps/dwarf | 2 +- deps/elf-edit | 2 +- deps/llvm-pretty | 2 +- deps/llvm-pretty-bc-parser | 2 +- deps/macaw-loader | 2 +- deps/semmc | 2 +- deps/what4 | 2 +- .../Data/Macaw/Refinement/FuncBlockUtils.hs | 2 +- refinement/src/Data/Macaw/Refinement/Path.hs | 8 +- symbolic/src/Data/Macaw/Symbolic.hs | 6 +- symbolic/src/Data/Macaw/Symbolic/CrucGen.hs | 2 +- 16 files changed, 147 insertions(+), 103 deletions(-) diff --git a/base/src/Data/Macaw/Analysis/FunctionArgs.hs b/base/src/Data/Macaw/Analysis/FunctionArgs.hs index 3c2bd77c..eee4a896 100644 --- a/base/src/Data/Macaw/Analysis/FunctionArgs.hs +++ b/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 diff --git a/base/src/Data/Macaw/Analysis/RegisterUse.hs b/base/src/Data/Macaw/Analysis/RegisterUse.hs index 61ddf205..16a40e4a 100644 --- a/base/src/Data/Macaw/Analysis/RegisterUse.hs +++ b/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 diff --git a/base/src/Data/Macaw/Discovery.hs b/base/src/Data/Macaw/Discovery.hs index d63f10dd..4fd7ac32 100644 --- a/base/src/Data/Macaw/Discovery.hs +++ b/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 diff --git a/base/src/Data/Macaw/Discovery/State.hs b/base/src/Data/Macaw/Discovery/State.hs index e30285b5..eaf92de6 100644 --- a/base/src/Data/Macaw/Discovery/State.hs +++ b/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{} -> [] diff --git a/deps/crucible b/deps/crucible index c1da81f0..09532645 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit c1da81f05e7a8ac80787e2f161ba341a312a6302 +Subproject commit 09532645133d39cda983bca67c2dbb91d05e4373 diff --git a/deps/dwarf b/deps/dwarf index 93648195..ab74e6e7 160000 --- a/deps/dwarf +++ b/deps/dwarf @@ -1 +1 @@ -Subproject commit 93648195d73fdbf45e982524663c66754ea468df +Subproject commit ab74e6e73ec92cf3219823d5336f190a1464118b diff --git a/deps/elf-edit b/deps/elf-edit index fe018fbf..6a089cc6 160000 --- a/deps/elf-edit +++ b/deps/elf-edit @@ -1 +1 @@ -Subproject commit fe018fbf6c2df56fc3f565d2732780c064228f1b +Subproject commit 6a089cc6e84a35604168c10193c521fa1359481d diff --git a/deps/llvm-pretty b/deps/llvm-pretty index cf5c9310..f5e0ff3f 160000 --- a/deps/llvm-pretty +++ b/deps/llvm-pretty @@ -1 +1 @@ -Subproject commit cf5c931061b48a4253e7eea15947eff7d9790f07 +Subproject commit f5e0ff3f3f6154842d3321031ca5a5031c91ecc6 diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser index 3d0d5494..c38b86b8 160000 --- a/deps/llvm-pretty-bc-parser +++ b/deps/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit 3d0d549486ceb101c38af3423426f3ff07aa966d +Subproject commit c38b86b8b485c85181ab1bfc682fae194c8d4027 diff --git a/deps/macaw-loader b/deps/macaw-loader index de712a0c..79c1a214 160000 --- a/deps/macaw-loader +++ b/deps/macaw-loader @@ -1 +1 @@ -Subproject commit de712a0cbd2a71d3e63c47f8bde3d72eb9d4e784 +Subproject commit 79c1a214de19677197f2b7e5f38562b3ba925be9 diff --git a/deps/semmc b/deps/semmc index 906994d3..a60ace5a 160000 --- a/deps/semmc +++ b/deps/semmc @@ -1 +1 @@ -Subproject commit 906994d383b4d72e30cf479a255b0c5a884fc343 +Subproject commit a60ace5ab6036dcb0c63aec0dddd2324b288ef9c diff --git a/deps/what4 b/deps/what4 index 3461006b..cce1929f 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit 3461006b5156904d82dedd32175849a6aa00059f +Subproject commit cce1929ff63e48812993bf338a78533515b5ab77 diff --git a/refinement/src/Data/Macaw/Refinement/FuncBlockUtils.hs b/refinement/src/Data/Macaw/Refinement/FuncBlockUtils.hs index 8665d755..82075249 100644 --- a/refinement/src/Data/Macaw/Refinement/FuncBlockUtils.hs +++ b/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 _ -> diff --git a/refinement/src/Data/Macaw/Refinement/Path.hs b/refinement/src/Data/Macaw/Refinement/Path.hs index c918b4e2..d01a193b 100644 --- a/refinement/src/Data/Macaw/Refinement/Path.hs +++ b/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) -> diff --git a/symbolic/src/Data/Macaw/Symbolic.hs b/symbolic/src/Data/Macaw/Symbolic.hs index 3ba2fe06..2ccccab7 100644 --- a/symbolic/src/Data/Macaw/Symbolic.hs +++ b/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] diff --git a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs index deaeb1a7..b42c7f6e 100644 --- a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs +++ b/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