Skip to content

Commit

Permalink
favor ArchAddrWidth and ArchSegmentOff type synonyms
Browse files Browse the repository at this point in the history
  • Loading branch information
Ptival committed Dec 11, 2023
1 parent 35b5fcd commit d2f7028
Show file tree
Hide file tree
Showing 11 changed files with 26 additions and 27 deletions.
4 changes: 2 additions & 2 deletions base/src/Data/Macaw/AbsDomain/AbsState.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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 =
Expand Down
2 changes: 1 addition & 1 deletion base/src/Data/Macaw/AbsDomain/JumpBounds.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
4 changes: 2 additions & 2 deletions base/src/Data/Macaw/Analysis/FunctionArgs.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)]

Expand Down Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion base/src/Data/Macaw/Analysis/RegisterUse.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
6 changes: 3 additions & 3 deletions base/src/Data/Macaw/Architecture/Info.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion base/src/Data/Macaw/Discovery.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion base/src/Data/Macaw/Discovery/Classifier.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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."
Expand Down
4 changes: 2 additions & 2 deletions base/src/Data/Macaw/Discovery/Classifier/JumpTable.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion base/src/Data/Macaw/Discovery/ParsedContents.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
21 changes: 10 additions & 11 deletions macaw-semmc/src/Data/Macaw/SemMC/Generator.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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))
}
Expand All @@ -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))
Expand All @@ -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
Expand All @@ -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 =
Expand All @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -403,4 +403,3 @@ finishBlock' preBlock term =
Block { blockStmts = F.toList (preBlock ^. pBlockStmts)
, blockTerm = term (preBlock ^. pBlockState)
}

4 changes: 2 additions & 2 deletions macaw-semmc/src/Data/Macaw/SemMC/Translations.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
)
Expand All @@ -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)
Expand Down

0 comments on commit d2f7028

Please sign in to comment.