Delay the resolution of casts so that llvm_pointer_cast can be a pu…

…re function,

similar to `llvm_field`, `llvm_elem`, etc.

crux-mir-comp/src/Mir/Compositional/MethodSpec.hs

@@ -41,6 +41,7 @@ type instance MS.MethodId MIR = DefId
 type instance MS.AllocSpec MIR = Some MirAllocSpec
 type instance MS.PointsTo MIR = MirPointsTo
 type instance MS.ResolvedState MIR = ()
+type instance MS.CastType MIR = ()
 
 type instance MS.Codebase MIR = CollectionState
 

src/SAWScript/Crucible/Common/MethodSpec.hs

@@ -81,6 +81,9 @@ type family TypeName ext :: Type
 -- | The type of types of the syntax extension we're dealing with
 type family ExtType ext :: Type
 
+-- | The types that can appear in casts
+type family CastType ext :: Type
+
 -- | The type of points-to assertions
 type family PointsTo ext :: Type
 
@@ -123,7 +126,7 @@ data SetupValue ext where
   SetupArray  :: B (HasSetupArray ext) -> [SetupValue ext] -> SetupValue ext
   SetupElem   :: B (HasSetupElem ext) -> SetupValue ext -> Int -> SetupValue ext
   SetupField  :: B (HasSetupField ext) -> SetupValue ext -> String -> SetupValue ext
-  SetupCast   :: B (HasSetupCast ext) -> SetupValue ext -> ExtType ext -> SetupValue ext
+  SetupCast   :: B (HasSetupCast ext) -> SetupValue ext -> CastType ext -> SetupValue ext
 
   -- | A pointer to a global variable
   SetupGlobal :: B (HasSetupGlobal ext) -> String -> SetupValue ext
@@ -143,7 +146,7 @@ type SetupValueHas (c :: Type -> Constraint) ext =
   , c (B (HasSetupCast ext))
   , c (B (HasSetupGlobal ext))
   , c (B (HasSetupGlobalInitializer ext))
-  , c (ExtType ext)
+  , c (CastType ext)
   )
 
 deriving instance (SetupValueHas Show ext) => Show (SetupValue ext)
@@ -156,7 +159,7 @@ deriving instance (SetupValueHas Show ext) => Show (SetupValue ext)
 --   are implementation details and won't be familiar to users.
 --   Consider using 'resolveSetupValue' and printing an 'LLVMVal'
 --   with @PP.pretty@ instead.
-ppSetupValue :: Show (ExtType ext) => SetupValue ext -> PP.Doc ann
+ppSetupValue :: Show (CastType ext) => SetupValue ext -> PP.Doc ann
 ppSetupValue setupval = case setupval of
   SetupTerm tm   -> ppTypedTerm tm
   SetupVar i     -> ppAllocIndex i

src/SAWScript/Crucible/JVM/MethodSpecIR.hs

@@ -68,7 +68,7 @@ type JIdent = String -- FIXME(huffman): what to put here?
 type instance MS.TypeName CJ.JVM = JIdent
 
 type instance MS.ExtType CJ.JVM = J.Type
-
+type instance MS.CastType CJ.JVM = ()
 type instance MS.ResolvedState CJ.JVM = ()
 
 --------------------------------------------------------------------------------

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -2103,14 +2103,8 @@ llvm_fresh_pointer lty =
      memTy <- memTypeForLLVMType loc lty
      constructFreshPointer (llvmTypeAlias lty) loc memTy
 
-llvm_cast_pointer :: AllLLVM SetupValue -> L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue)
-llvm_cast_pointer ptr lty =
-  LLVMCrucibleSetupM $
-  do cctx <- getLLVMCrucibleContext
-     let ?lc = ccTypeCtx cctx
-     loc <- getW4Position "llvm_cast_pointer"
-     memTy <- memTypeForLLVMType loc (L.PtrTo lty)
-     pure (mkAllLLVM (SetupCast () (getAllLLVM ptr) memTy))
+llvm_cast_pointer :: AllLLVM SetupValue -> L.Type -> AllLLVM SetupValue
+llvm_cast_pointer ptr lty = mkAllLLVM (SetupCast () (getAllLLVM ptr) lty)
 
 constructFreshPointer ::
   Crucible.HasPtrWidth (Crucible.ArchWidth arch) =>

src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

@@ -179,7 +179,7 @@ type instance MS.HasGhostState (LLVM _) = 'True
 
 type instance MS.TypeName (LLVM arch) = CL.Ident
 type instance MS.ExtType (LLVM arch) = CL.MemType
-
+type instance MS.CastType (LLVM arch) = L.Type
 
 --------------------------------------------------------------------------------
 -- *** LLVMMethodId
@@ -619,7 +619,7 @@ type instance MS.ResolvedState (LLVM arch) = LLVMResolvedState
 data ResolvedPathItem
   = ResolvedField String
   | ResolvedElem Int
-  | ResolvedCast CL.MemType
+  | ResolvedCast L.Type
  deriving (Show, Eq, Ord)
 
 type ResolvedPath = [ResolvedPathItem]

src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -109,7 +109,7 @@ resolveSetupValueInfo cc env nameEnv v =
       | Just alias <- Map.lookup i nameEnv
       -> L.Pointer (L.guessAliasInfo mdMap alias)
 
-    SetupCast () _ (Crucible.PtrType (Crucible.Alias alias))
+    SetupCast () _ (L.Alias alias)
       -> L.Pointer (L.guessAliasInfo mdMap alias)
 
     SetupField () a n ->
@@ -332,10 +332,17 @@ typeOfSetupValue' cc env nameEnv val =
                              , "instead got:"
                              , show (ppTypedTermType tp)
                              ]
-    SetupCast () v tp -> -- INVARIANT: tp is a pointer type
+    SetupCast () v ltp ->
       do memTy <- typeOfSetupValue cc env nameEnv v
          case memTy of
-           Crucible.PtrType _symTy -> return tp
+           Crucible.PtrType _symTy ->
+             case let ?lc = lc in Crucible.liftMemType (L.PtrTo ltp) of
+               Left err -> fail $ unlines [ "typeOfSetupValue: invalid type " ++ show ltp
+                                          , "Details:"
+                                          , err
+                                          ]
+               Right mt -> return mt
+
            _ -> fail $ unwords $
                   [ "typeOfSetupValue: tried to cast the type of a non-pointer value"
                   , "actual type of value: " ++ show memTy

src/SAWScript/Interpreter.hs

@@ -2603,7 +2603,7 @@ primitives = Map.fromList
     Current
     [ "Legacy alternative name for `llvm_return`." ]
 
-  , prim "llvm_cast_pointer" "SetupValue -> LLVMType -> LLVMSetup SetupValue"
+  , prim "llvm_cast_pointer" "SetupValue -> LLVMType -> SetupValue"
     (pureVal llvm_cast_pointer)
     Current
     [ "Cast the type of the given setup value (which must be a pointer value)."