favor ArchAddrWidth over RegAddrWidth (ArchReg ...)

GaloisInc · Dec 9, 2023 · b34111d · b34111d
1 parent 35b5fcd
commit b34111d
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 15 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.

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/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
@@ -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)