From b34111df84ecd1d056b7e8bf5f4f1aaf78e39d55 Mon Sep 17 00:00:00 2001 From: Valentin Robert Date: Fri, 8 Dec 2023 17:58:15 -0800 Subject: [PATCH] favor `ArchAddrWidth` over `RegAddrWidth (ArchReg ...)` --- base/src/Data/Macaw/AbsDomain/AbsState.hs | 2 +- base/src/Data/Macaw/Architecture/Info.hs | 6 +++--- base/src/Data/Macaw/Discovery.hs | 2 +- macaw-semmc/src/Data/Macaw/SemMC/Generator.hs | 15 +++++++-------- macaw-semmc/src/Data/Macaw/SemMC/Translations.hs | 4 ++-- 5 files changed, 14 insertions(+), 15 deletions(-) diff --git a/base/src/Data/Macaw/AbsDomain/AbsState.hs b/base/src/Data/Macaw/AbsDomain/AbsState.hs index f6eb1bf27..060878dc2 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. diff --git a/base/src/Data/Macaw/Architecture/Info.hs b/base/src/Data/Macaw/Architecture/Info.hs index bcbdaa97b..4600a13f4 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 8027f07d1..e665dba02 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/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs b/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs index df2d02a03..51b068138 100644 --- a/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs +++ b/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs @@ -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 @@ -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 a7932feaa..2f285e4ce 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)