[refinement] Add MemWidth constraint.

refinement/src/Data/Macaw/Refinement.hs

@@ -28,7 +28,10 @@ import           Data.Parameterized.Classes
 -- | Expand an initial discovery state by exploring from a given set
 -- of function entry points.  This entry point can be used as an
 -- alternative to the same named function in Data.Macaw.Discovery.
-cfgFromAddrsAndState :: forall arch . ShowF (ArchReg arch) =>
+cfgFromAddrsAndState :: forall arch .
+                        ( MM.MemWidth (ArchAddrWidth arch)
+                        , ShowF (ArchReg arch)
+                        ) =>
                         MD.DiscoveryState arch
                      -> [ArchSegmentOff arch]
                      -- ^ Initial function entry points.
@@ -47,7 +50,10 @@ cfgFromAddrsAndState initial_state init_addrs mem_words =
 -- alternate entry point from the same named function in
 -- Data.Macaw.Discovery.
 cfgFromAddrs ::
-     forall arch . ShowF (ArchReg arch) =>
+  forall arch .
+  ( MM.MemWidth (ArchAddrWidth arch)
+  , ShowF (ArchReg arch)
+  ) =>
      MA.ArchitectureInfo arch
      -- ^ Architecture-specific information needed for doing
      -- control-flow exploration.
@@ -78,6 +84,8 @@ cfgFromAddrs ainfo mem addrSymMap =
 
 -- | Refine an existing discovery state by using a symbolic backend to
 -- perform additional discovery for incomplete blocks.
-refineDiscovery :: DiscoveryState arch -> DiscoveryState arch
+refineDiscovery :: ( MM.MemWidth (ArchAddrWidth arch)
+                   ) =>
+                   DiscoveryState arch -> DiscoveryState arch
 refineDiscovery = symbolicUnkTransferRefinement
                   . symbolicTargetRefinement

refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs

@@ -158,7 +158,9 @@ import qualified What4.Solver.Z3 as W
 -- information and which attempts to resolve UnknownTransfer
 -- classification failures, returning (possibly updated) Discovery
 -- information.
-symbolicUnkTransferRefinement :: DiscoveryState arch -> DiscoveryState arch
+symbolicUnkTransferRefinement :: ( MC.MemWidth (MC.ArchAddrWidth arch)
+                                 ) =>
+                                 DiscoveryState arch -> DiscoveryState arch
 symbolicUnkTransferRefinement = refineTransfers []
 
 
@@ -170,7 +172,9 @@ symbolicUnkTransferRefinement = refineTransfers []
 -- function recurses until there are no more UnknownTransfer failure
 -- blocks in the input discovery state that are not also in the
 -- failure accumulation array.
-refineTransfers :: [BlockIdentifier arch]
+refineTransfers :: ( MC.MemWidth (MC.ArchAddrWidth arch)
+                   ) =>
+                   [BlockIdentifier arch]
                    -- ^ attempted blocks
                 -> DiscoveryState arch
                    -- ^ input DiscoveryState
@@ -214,7 +218,9 @@ isUnknownTransfer pb =
 -- blocks newly discovered via the transfer resolution) and return
 -- that.  If it was unable to refine the transfer, it will return
 -- Nothing and this block will be added to the "unresolvable" list.
-refineBlockTransfer :: DiscoveryState arch
+refineBlockTransfer :: ( MC.MemWidth (MC.ArchAddrWidth arch)
+                       ) =>
+                       DiscoveryState arch
                     -> Some (ParsedBlock arch)
                     -> Maybe (DiscoveryState arch)
 refineBlockTransfer inpDS blk =