diff --git a/base/src/Data/Macaw/AbsDomain/AbsState.hs b/base/src/Data/Macaw/AbsDomain/AbsState.hs index f6eb1bf2..af26dce0 100644 --- a/base/src/Data/Macaw/AbsDomain/AbsState.hs +++ b/base/src/Data/Macaw/AbsDomain/AbsState.hs @@ -1180,7 +1180,7 @@ setAbsIP a b -- | The absolute value associated with a given architecture. -- -- This is only a function of the address width. -type ArchAbsValue arch = AbsValue (RegAddrWidth (ArchReg arch)) +type ArchAbsValue arch = AbsValue (ArchAddrWidth arch) -- | This stores the abstract state of the system which may be within -- a block. @@ -1458,7 +1458,7 @@ absEvalCall :: forall arch ids -> AbsProcessorState (ArchReg arch) ids -- ^ State before call -> RegState (ArchReg arch) (Value arch ids) - -> MemSegmentOff (ArchAddrWidth arch) + -> ArchSegmentOff arch -- ^ Address we are jumping to -> AbsBlockState (ArchReg arch) absEvalCall params ab0 regs addr = diff --git a/base/src/Data/Macaw/AbsDomain/JumpBounds.hs b/base/src/Data/Macaw/AbsDomain/JumpBounds.hs index f22f7263..84dd4ce3 100644 --- a/base/src/Data/Macaw/AbsDomain/JumpBounds.hs +++ b/base/src/Data/Macaw/AbsDomain/JumpBounds.hs @@ -859,4 +859,4 @@ postCallBounds params cns regs = -- -- Note: This is defined here (despite not being used here) to avoid import cycles elsewhere type IntraJumpTarget arch = - (MemSegmentOff (ArchAddrWidth arch), AbsBlockState (ArchReg arch), InitJumpBounds arch) + (ArchSegmentOff arch, AbsBlockState (ArchReg arch), InitJumpBounds arch) diff --git a/base/src/Data/Macaw/Analysis/FunctionArgs.hs b/base/src/Data/Macaw/Analysis/FunctionArgs.hs index b278e321..8112ff52 100644 --- a/base/src/Data/Macaw/Analysis/FunctionArgs.hs +++ b/base/src/Data/Macaw/Analysis/FunctionArgs.hs @@ -311,7 +311,7 @@ data ArchDemandInfo arch = ArchDemandInfo -- Takes address of callsite and registers. type ResolveCallArgsFn arch = forall ids - . MemSegmentOff (ArchAddrWidth arch) + . ArchSegmentOff arch -> RegState (ArchReg arch) (Value arch ids) -> Either String [Some (Value arch ids)] @@ -607,7 +607,7 @@ summarizeCall blockAddr callOff finalRegs mReturnAddr = do pure mempty recordStmtsDemands :: OrdF (ArchReg arch) - => MemSegmentOff (ArchAddrWidth arch) -- ^ Address of block + => ArchSegmentOff arch -- ^ Address of block -> ArchAddrWord arch -- ^ Offset from start of block of current instruction. -> [Stmt arch ids] -> FunctionArgsM arch ids (ArchAddrWord arch) diff --git a/base/src/Data/Macaw/Analysis/RegisterUse.hs b/base/src/Data/Macaw/Analysis/RegisterUse.hs index d523120d..a53ff1a3 100644 --- a/base/src/Data/Macaw/Analysis/RegisterUse.hs +++ b/base/src/Data/Macaw/Analysis/RegisterUse.hs @@ -511,7 +511,7 @@ data InferStackValue arch ids tp where -- | Read-only information needed to infer successor start -- constraints for a lbok. data StartInferContext arch = - SIC { sicAddr :: !(MemSegmentOff (ArchAddrWidth arch)) + SIC { sicAddr :: !(ArchSegmentOff arch) -- ^ Address of block we are inferring state for. , sicRegs :: !(MapF (ArchReg arch) (InitInferValue arch)) -- ^ Map rep register to rheir initial domain information. diff --git a/base/src/Data/Macaw/Architecture/Info.hs b/base/src/Data/Macaw/Architecture/Info.hs index bcbdaa97..4600a13f 100644 --- a/base/src/Data/Macaw/Architecture/Info.hs +++ b/base/src/Data/Macaw/Architecture/Info.hs @@ -231,7 +231,7 @@ data ArchitectureInfo arch { withArchConstraints :: forall a . (ArchConstraints arch => a) -> a -- ^ Provides the architecture constraints to any computation -- that needs it. - , archAddrWidth :: !(AddrWidthRepr (RegAddrWidth (ArchReg arch))) + , archAddrWidth :: !(AddrWidthRepr (ArchAddrWidth arch)) -- ^ Architecture address width. , archEndianness :: !Endianness -- ^ The byte order values are stored in. @@ -247,7 +247,7 @@ data ArchitectureInfo arch -- ^ Create initial registers from address and precondition. , disassembleFn :: !(DisassembleFn arch) -- ^ Function for disassembling a block. - , mkInitialAbsState :: !(Memory (RegAddrWidth (ArchReg arch)) + , mkInitialAbsState :: !(Memory (ArchAddrWidth arch) -> ArchSegmentOff arch -> AbsBlockState (ArchReg arch)) -- ^ Creates an abstract block state for representing the beginning of a @@ -257,7 +257,7 @@ data ArchitectureInfo arch , absEvalArchFn :: !(forall ids tp . AbsProcessorState (ArchReg arch) ids -> ArchFn arch (Value arch ids) tp - -> AbsValue (RegAddrWidth (ArchReg arch)) tp) + -> AbsValue (ArchAddrWidth arch) tp) -- ^ Evaluates an architecture-specific function , absEvalArchStmt :: !(forall ids . AbsProcessorState (ArchReg arch) ids diff --git a/base/src/Data/Macaw/Discovery.hs b/base/src/Data/Macaw/Discovery.hs index 8027f07d..e665dba0 100644 --- a/base/src/Data/Macaw/Discovery.hs +++ b/base/src/Data/Macaw/Discovery.hs @@ -460,7 +460,7 @@ recordWriteStmts ainfo mem absState writtenAddrs (stmt:stmts) = -- | Get the memory representation associated with pointers in the -- given architecture. -addrMemRepr :: ArchitectureInfo arch -> MemRepr (BVType (RegAddrWidth (ArchReg arch))) +addrMemRepr :: ArchitectureInfo arch -> MemRepr (BVType (ArchAddrWidth arch)) addrMemRepr arch_info = case archAddrWidth arch_info of Addr32 -> BVMemRepr n4 (archEndianness arch_info) diff --git a/base/src/Data/Macaw/Discovery/Classifier.hs b/base/src/Data/Macaw/Discovery/Classifier.hs index 8e1ab266..1b8ffc73 100644 --- a/base/src/Data/Macaw/Discovery/Classifier.hs +++ b/base/src/Data/Macaw/Discovery/Classifier.hs @@ -120,7 +120,7 @@ classifyDirectJump :: RegisterInfo (ArchReg arch) => ParseContext arch ids -> String -> Value arch ids (BVType (ArchAddrWidth arch)) - -> BlockClassifierM arch ids (MemSegmentOff (ArchAddrWidth arch)) + -> BlockClassifierM arch ids (ArchSegmentOff arch) classifyDirectJump ctx nm v = do ma <- case valueAsMemAddr v of Nothing -> fail $ nm ++ " value " ++ show v ++ " is not a valid address." diff --git a/base/src/Data/Macaw/Discovery/Classifier/JumpTable.hs b/base/src/Data/Macaw/Discovery/Classifier/JumpTable.hs index 498f28ac..49e0c0ac 100644 --- a/base/src/Data/Macaw/Discovery/Classifier/JumpTable.hs +++ b/base/src/Data/Macaw/Discovery/Classifier/JumpTable.hs @@ -220,7 +220,7 @@ type JumpTableClassifier arch ids s = extractJumpTableSlices :: ArchConstraints arch => Jmp.IntraJumpBounds arch ids -- ^ Bounds for jump table - -> MemSegmentOff (ArchAddrWidth arch) -- ^ Base address + -> ArchSegmentOff arch -- ^ Base address -> Natural -- ^ Stride -> BVValue arch ids idxWidth -> MemRepr tp -- ^ Type of values @@ -306,7 +306,7 @@ matchAbsoluteJumpTable = Info.classifierName "Absolute jump table" $ do BVMemRepr _arByteCount e -> pure e let go :: Int -> [MemChunk (ArchAddrWidth arch)] - -> Info.Classifier (MemSegmentOff (ArchAddrWidth arch)) + -> Info.Classifier (ArchSegmentOff arch) go entryIndex contents = do addr <- case resolveAsAddr mem endianness contents of Just a -> pure a diff --git a/base/src/Data/Macaw/Discovery/ParsedContents.hs b/base/src/Data/Macaw/Discovery/ParsedContents.hs index a794fb4d..b7f45145 100644 --- a/base/src/Data/Macaw/Discovery/ParsedContents.hs +++ b/base/src/Data/Macaw/Discovery/ParsedContents.hs @@ -82,7 +82,7 @@ instance MemWidth w => PP.Pretty (BlockExploreReason w) where -- 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)) + { arBase :: !(ArchSegmentOff arch) -- ^ The base address for array accesses. , arStride :: !Word64 -- ^ Space between elements of the array. diff --git a/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs b/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs index df2d02a0..2be17845 100644 --- a/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs +++ b/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs @@ -74,7 +74,7 @@ data Expr arch ids tp where data PreBlock arch ids = PreBlock { pBlockIndex :: !Word64 - , pBlockAddr :: MM.MemSegmentOff (ArchAddrWidth arch) + , pBlockAddr :: ArchSegmentOff arch , _pBlockStmts :: !(Seq.Seq (Stmt arch ids)) , _pBlockState :: !(RegState (ArchReg arch) (Value arch ids)) } @@ -90,7 +90,7 @@ pBlockState = lens _pBlockState (\s v -> s { _pBlockState = v }) data GenState arch ids s = GenState { assignIdGen :: NC.NonceGenerator (ST s) ids , _blockState :: !(PreBlock arch ids) - , genAddr :: MM.MemSegmentOff (ArchAddrWidth arch) + , genAddr :: ArchSegmentOff arch , genRegUpdates :: MapF.MapF (ArchReg arch) (Value arch ids) , _blockStateSnapshot :: !(RegState (ArchReg arch) (Value arch ids)) , appCache :: !(MapF.MapF (App (Value arch ids)) (Value arch ids)) @@ -102,7 +102,7 @@ data GenState arch ids s = emptyPreBlock :: RegState (ArchReg arch) (Value arch ids) -> Word64 - -> MM.MemSegmentOff (RegAddrWidth (ArchReg arch)) + -> MM.MemSegmentOff (ArchAddrWidth arch) -> PreBlock arch ids emptyPreBlock s0 idx addr = PreBlock { pBlockIndex = idx @@ -112,7 +112,7 @@ emptyPreBlock s0 idx addr = } initGenState :: NC.NonceGenerator (ST s) ids - -> MM.MemSegmentOff (ArchAddrWidth arch) + -> ArchSegmentOff arch -> RegState (ArchReg arch) (Value arch ids) -> GenState arch ids s initGenState nonceGen addr st = @@ -126,11 +126,11 @@ initGenState nonceGen addr st = where s0 = emptyPreBlock st 0 addr -initRegState :: (KnownNat (RegAddrWidth (ArchReg arch)), - 1 <= RegAddrWidth (ArchReg arch), +initRegState :: (KnownNat (ArchAddrWidth arch), + 1 <= ArchAddrWidth arch, RegisterInfo (ArchReg arch), - MM.MemWidth (RegAddrWidth (ArchReg arch))) - => MM.MemSegmentOff (RegAddrWidth (ArchReg arch)) + MM.MemWidth (ArchAddrWidth arch)) + => MM.MemSegmentOff (ArchAddrWidth arch) -> RegState (ArchReg arch) (Value arch ids) initRegState startIP = mkRegState Initial & curIP .~ RelocatableValue (addrWidthRepr startIP) (MM.segoffAddr startIP) @@ -196,7 +196,7 @@ getRegSnapshotVal reg = do -- the value first, if possible. setRegVal :: ( MSS.SimplifierExtension arch , OrdF (ArchReg arch) - , MM.MemWidth (RegAddrWidth (ArchReg arch)) + , MM.MemWidth (ArchAddrWidth arch) ) => ArchReg arch tp -> Value arch ids tp @@ -219,7 +219,7 @@ cacheAppValue a v = addExpr :: ( MSS.SimplifierExtension arch , OrdF (ArchReg arch) - , MM.MemWidth (RegAddrWidth (ArchReg arch)) + , MM.MemWidth (ArchAddrWidth arch) , ShowF (ArchReg arch) ) => Expr arch ids tp @@ -403,4 +403,3 @@ finishBlock' preBlock term = Block { blockStmts = F.toList (preBlock ^. pBlockStmts) , blockTerm = term (preBlock ^. pBlockState) } - diff --git a/macaw-semmc/src/Data/Macaw/SemMC/Translations.hs b/macaw-semmc/src/Data/Macaw/SemMC/Translations.hs index a7932fea..2f285e4c 100644 --- a/macaw-semmc/src/Data/Macaw/SemMC/Translations.hs +++ b/macaw-semmc/src/Data/Macaw/SemMC/Translations.hs @@ -24,7 +24,7 @@ import qualified Data.Macaw.SemMC.Simplify as MSS -- -- We pull this out to reduce the amount of code generated by TH bvconcat :: ( OrdF (ArchReg arch) - , MM.MemWidth (RegAddrWidth (ArchReg arch)) + , MM.MemWidth (ArchAddrWidth arch) , MSS.SimplifierExtension arch , ShowF (ArchReg arch) ) @@ -51,7 +51,7 @@ bvconcat bv1Val bv2Val repV repU repW = do -- This code is factored out of the TH module to improve compilation times. bvselect :: ( MSS.SimplifierExtension arch , OrdF (ArchReg arch) - , MM.MemWidth (RegAddrWidth (ArchReg arch)) + , MM.MemWidth (ArchAddrWidth arch) , ShowF (ArchReg arch) ) => (1 <= w, 1 <= n, i + n <= w)