favor ArchAddrWidth and ArchSegmentOff type synonyms

GaloisInc · Dec 11, 2023 · 416fb2d · 416fb2d
1 parent 35b5fcd
commit 416fb2d
Show file tree

Hide file tree

Showing 11 changed files with 26 additions and 27 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -74,7 +74,7 @@ data Expr arch ids tp where
 
 data PreBlock arch ids =
   PreBlock { pBlockIndex :: !Word64
-           , pBlockAddr :: MM.MemSegmentOff (ArchAddrWidth arch)
+           , pBlockAddr :: MM.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 :: MM.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)
+             -> MM.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
@@ -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)