Move Pointer' type family to SAWScript.Crucible.Common.Setup.Value

This is purely a refactor. This will become useful in a subsequent commit in
order to avoid import cycles.

Author: RyanGlScott

src/SAWScript/Crucible/Common/Override.hs

@@ -20,7 +20,7 @@ Stability   : provisional
 
 module SAWScript.Crucible.Common.Override
   ( Pointer
-  , Pointer'
+  , MS.Pointer'
   , OverrideState
   , OverrideState'(..)
   , osAsserts
@@ -68,7 +68,6 @@ import qualified Control.Monad.Fail as Fail
 import           Control.Monad.Trans.Except
 import           Control.Monad.Trans.Class
 import           Control.Monad.IO.Class
-import           Data.Kind (Type)
 import qualified Data.Map as Map
 import           Data.Map (Map)
 import           Data.Set (Set)
@@ -96,6 +95,7 @@ import qualified What4.ProgramLoc as W4
 import           SAWScript.Exceptions
 import           SAWScript.Crucible.Common (Sym)
 import           SAWScript.Crucible.Common.MethodSpec as MS
+import           SAWScript.Crucible.Common.Setup.Value as MS
 
 -- TODO, not sure this is the best place for this definition
 type MetadataMap =
@@ -106,13 +106,11 @@ type MetadataMap =
 
 type LabeledPred sym = W4.LabeledPred (W4.Pred sym) Crucible.SimError
 
-type family Pointer' ext sym :: Type
-
-type Pointer ext = Pointer' ext Sym
+type Pointer ext = MS.Pointer' ext Sym
 
 data OverrideState' sym ext = OverrideState
   { -- | Substitution for memory allocations
-    _setupValueSub :: Map AllocIndex (Pointer' ext sym)
+    _setupValueSub :: Map AllocIndex (MS.Pointer' ext sym)
 
     -- | Substitution for SAW Core external constants
   , _termSub :: Map VarIndex Term

src/SAWScript/Crucible/Common/Setup/Value.hs

@@ -59,6 +59,8 @@ module SAWScript.Crucible.Common.Setup.Value
 
   , MethodId
   , Codebase
+
+  , Pointer'
   ) where
 
 import           Data.Constraint (Constraint)
@@ -200,3 +202,8 @@ type family MethodId ext :: Type
 --
 -- Examples: An 'LLVMModule', a Java 'Codebase'
 type family Codebase ext :: Type
+
+--------------------------------------------------------------------------------
+-- *** Pointers
+
+type family Pointer' ext sym :: Type

src/SAWScript/Crucible/JVM/Override.hs

@@ -109,6 +109,7 @@ import qualified SAWScript.Crucible.Common.Override as Ov (getSymInterface)
 import qualified SAWScript.Crucible.Common.MethodSpec as MS
 import           SAWScript.Crucible.JVM.MethodSpecIR
 import           SAWScript.Crucible.JVM.ResolveSetupValue
+import           SAWScript.Crucible.JVM.Setup.Value ()
 import           SAWScript.Options
 import           SAWScript.Panic
 import           SAWScript.Utils (handleException)
@@ -121,7 +122,6 @@ type SetupValue = MS.SetupValue CJ.JVM
 type CrucibleMethodSpecIR = MS.CrucibleMethodSpecIR CJ.JVM
 type StateSpec = MS.StateSpec CJ.JVM
 type SetupCondition = MS.SetupCondition CJ.JVM
-type instance Pointer' CJ.JVM Sym = JVMRefVal
 
 -- TODO: Improve?
 ppJVMVal :: JVMVal -> PP.Doc ann

src/SAWScript/Crucible/JVM/ResolveSetupValue.hs

@@ -68,6 +68,7 @@ import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..))
 
 import SAWScript.Panic
 import SAWScript.Crucible.JVM.MethodSpecIR
+import SAWScript.Crucible.JVM.Setup.Value (JVMRefVal)
 import qualified SAWScript.Crucible.Common.MethodSpec as MS
 import SAWScript.Crucible.Common.ResolveSetupValue (resolveBoolTerm)
 
@@ -82,8 +83,6 @@ instance Show JVMVal where
   show (IVal _) = "IVal"
   show (LVal _) = "LVal"
 
-type JVMRefVal = Crucible.RegValue Sym CJ.JVMRefType
-
 type SetupValue = MS.SetupValue CJ.JVM
 
 data JVMTypeOfError

src/SAWScript/Crucible/JVM/Setup/Value.hs

@@ -28,6 +28,7 @@ module, plus additional functionality) instead.
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ViewPatterns #-}
 
 module SAWScript.Crucible.JVM.Setup.Value
@@ -47,6 +48,8 @@ module SAWScript.Crucible.JVM.Setup.Value
   , jccJVMContext
   , jccBackend
   , jccHandleAllocator
+
+  , JVMRefVal
   ) where
 
 import           Control.Lens
@@ -55,6 +58,7 @@ import qualified Prettyprinter as PPL
 import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator)
 
 -- crucible-jvm
+import qualified Lang.Crucible.Simulator as CS
 import qualified Lang.Crucible.JVM as CJ
 import qualified Lang.JVM.Codebase as CB
 
@@ -65,7 +69,7 @@ import qualified Language.JVM.Parser as J
 import           Verifier.SAW.TypedTerm (TypedTerm)
 
 import           SAWScript.Crucible.Common
-import qualified SAWScript.Crucible.Common.MethodSpec as MS
+import qualified SAWScript.Crucible.Common.Setup.Value as MS
 
 --------------------------------------------------------------------------------
 -- ** Language features
@@ -148,3 +152,10 @@ data JVMCrucibleContext =
 makeLenses ''JVMCrucibleContext
 
 type instance MS.CrucibleContext CJ.JVM = JVMCrucibleContext
+
+--------------------------------------------------------------------------------
+-- *** Pointers
+
+type instance MS.Pointer' CJ.JVM Sym = JVMRefVal
+
+type JVMRefVal = CS.RegValue Sym CJ.JVMRefType

src/SAWScript/Crucible/LLVM/Override.hs

@@ -134,14 +134,13 @@ import           SAWScript.Crucible.Common.Override hiding (getSymInterface)
 import qualified SAWScript.Crucible.Common.Override as Ov (getSymInterface)
 import           SAWScript.Crucible.LLVM.MethodSpecIR
 import           SAWScript.Crucible.LLVM.ResolveSetupValue
+import           SAWScript.Crucible.LLVM.Setup.Value ()
 import           SAWScript.Options
 import           SAWScript.Panic
 import           SAWScript.Utils (bullets, handleException)
 
 type LabeledPred sym = W4.LabeledPred (W4.Pred sym) Crucible.SimError
 
-type instance Pointer' (LLVM arch) Sym = LLVMPtr (Crucible.ArchWidth arch)
-
 -- | An override packaged together with its preconditions, labeled with some
 --   human-readable info about each condition.
 data OverrideWithPreconditions arch =

src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -84,11 +84,11 @@ import           SAWScript.Crucible.Common (Sym, sawCoreState, HasSymInterface(.
 import           SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), SetupValue(..), ppTypedTermType)
 
 import SAWScript.Crucible.LLVM.MethodSpecIR
+import SAWScript.Crucible.LLVM.Setup.Value (LLVMPtr)
 import qualified SAWScript.Proof as SP
 
 
 type LLVMVal = Crucible.LLVMVal Sym
-type LLVMPtr wptr = Crucible.LLVMPtr Sym wptr
 
 
 

src/SAWScript/Crucible/LLVM/Setup/Value.hs

@@ -30,6 +30,7 @@ module, plus additional functionality) instead.
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ViewPatterns #-}
 
 module SAWScript.Crucible.LLVM.Setup.Value
@@ -75,6 +76,8 @@ module SAWScript.Crucible.LLVM.Setup.Value
   , emptyResolvedState
   , rsAllocs
   , rsGlobals
+    -- * @LLVMPtr@
+  , LLVMPtr
   ) where
 
 import           Control.Lens
@@ -338,3 +341,10 @@ emptyResolvedState :: LLVMResolvedState
 emptyResolvedState = ResolvedState Map.empty Map.empty
 
 makeLenses ''LLVMResolvedState
+
+--------------------------------------------------------------------------------
+-- *** Pointers
+
+type instance Setup.Pointer' (LLVM arch) Sym = LLVMPtr (CL.ArchWidth arch)
+
+type LLVMPtr wptr = CL.LLVMPtr Sym wptr