Implement new saw-script function crucible_points_to_at_type.

Also `crucible_conditional_points_to_at_type`.

Fixes #930.

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -42,6 +42,8 @@ module SAWScript.Crucible.LLVM.Builtins
     , crucible_equal
     , crucible_points_to
     , crucible_conditional_points_to
+    , crucible_points_to_at_type
+    , crucible_conditional_points_to_at_type
     , crucible_points_to_array_prefix
     , crucible_fresh_pointer
     , crucible_llvm_unsafe_assume_spec
@@ -1915,7 +1917,7 @@ crucible_points_to ::
   AllLLVM SetupValue     ->
   LLVMCrucibleSetupM ()
 crucible_points_to typed =
-  crucible_points_to_internal typed Nothing
+  crucible_points_to_internal typed Nothing Nothing
 
 crucible_conditional_points_to ::
   Bool {- ^ whether to check type compatibility -} ->
@@ -1924,15 +1926,33 @@ crucible_conditional_points_to ::
   AllLLVM SetupValue ->
   LLVMCrucibleSetupM ()
 crucible_conditional_points_to typed cond =
-  crucible_points_to_internal typed (Just cond)
+  crucible_points_to_internal typed Nothing (Just cond)
+
+crucible_points_to_at_type ::
+  AllLLVM SetupValue ->
+  L.Type             ->
+  AllLLVM SetupValue ->
+  LLVMCrucibleSetupM ()
+crucible_points_to_at_type ptr ty val =
+  crucible_points_to_internal False (Just ty) Nothing ptr val
+
+crucible_conditional_points_to_at_type ::
+  TypedTerm ->
+  AllLLVM SetupValue ->
+  L.Type             ->
+  AllLLVM SetupValue ->
+  LLVMCrucibleSetupM ()
+crucible_conditional_points_to_at_type cond ptr ty val =
+  crucible_points_to_internal False (Just ty) (Just cond) ptr val
 
 crucible_points_to_internal ::
   Bool {- ^ whether to check type compatibility -} ->
+  Maybe L.Type {- ^ optional type constraint for rhs -} ->
   Maybe TypedTerm ->
-  AllLLVM SetupValue ->
-  AllLLVM SetupValue ->
+  AllLLVM SetupValue {- ^ lhs pointer -} ->
+  AllLLVM SetupValue {- ^ rhs value -} ->
   LLVMCrucibleSetupM ()
-crucible_points_to_internal typed cond (getAllLLVM -> ptr) (getAllLLVM -> val) =
+crucible_points_to_internal typed rhsTy cond (getAllLLVM -> ptr) (getAllLLVM -> val) =
   LLVMCrucibleSetupM $
   do cc <- getLLVMCrucibleContext
      loc <- getW4Position "crucible_points_to"
@@ -1957,7 +1977,14 @@ crucible_points_to_internal typed cond (getAllLLVM -> ptr) (getAllLLVM -> val) =
                   ]
 
             _ -> throwCrucibleSetup loc $ "lhs not a pointer type: " ++ show ptrTy
+
           valTy <- typeOfSetupValue cc env nameEnv val
+          case rhsTy of
+            Nothing -> pure ()
+            Just ty ->
+              do ty' <- memTypeForLLVMType loc ty
+                 checkMemTypeCompatibility loc ty' valTy
+
           when typed (checkMemTypeCompatibility loc lhsTy valTy)
           Setup.addPointsTo (LLVMPointsTo loc cond ptr $ ConcreteSizeValue val)
 

src/SAWScript/Interpreter.hs

@@ -2152,6 +2152,22 @@ primitives = Map.fromList
     , "about the final memory state after running the function."
     ]
 
+  , prim "crucible_points_to_at_type" "SetupValue -> LLVMType -> SetupValue -> CrucibleSetup ()"
+    (pureVal crucible_points_to_at_type)
+    Current
+    [ "A variant of crucible_points_to that casts the pointer to another"
+    , "type. This may be useful when reading or writing a prefix of larger"
+    , "array, for example."
+    ]
+
+  , prim "crucible_conditional_points_to_at_type" "Term -> SetupValue -> LLVMType -> SetupValue -> CrucibleSetup ()"
+    (pureVal crucible_conditional_points_to_at_type)
+    Current
+    [ "A variant of crucible_conditional_points_to that casts the pointer"
+    , "to another type. This may be useful when reading or writing a prefix"
+    , "of larger array, for example."
+    ]
+
   , prim "crucible_points_to_untyped" "SetupValue -> SetupValue -> CrucibleSetup ()"
     (pureVal (crucible_points_to False))
     Current