From c62181de9f9aaaf7b7ead50537bab70f1900ef38 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 12 Jan 2021 17:44:22 -0800
Subject: [PATCH] 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 | 37 +++++++++++++++++++++----
 src/SAWScript/Interpreter.hs            | 16 +++++++++++
 2 files changed, 48 insertions(+), 5 deletions(-)

diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index c49388e51f..4878c0254d 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -42,6 +42,8 @@ module SAWScript.Crucible.LLVM.Builtins
     , llvm_equal
     , llvm_points_to
     , llvm_conditional_points_to
+    , llvm_points_to_at_type
+    , llvm_conditional_points_to_at_type
     , llvm_points_to_array_prefix
     , llvm_fresh_pointer
     , llvm_unsafe_assume_spec
@@ -1979,7 +1981,7 @@ llvm_points_to ::
   AllLLVM SetupValue     ->
   LLVMCrucibleSetupM ()
 llvm_points_to typed =
-  llvm_points_to_internal typed Nothing
+  llvm_points_to_internal typed Nothing Nothing
 
 llvm_conditional_points_to ::
   Bool {- ^ whether to check type compatibility -} ->
@@ -1988,15 +1990,33 @@ llvm_conditional_points_to ::
   AllLLVM SetupValue ->
   LLVMCrucibleSetupM ()
 llvm_conditional_points_to typed cond =
-  llvm_points_to_internal typed (Just cond)
+  llvm_points_to_internal typed Nothing (Just cond)
+
+llvm_points_to_at_type ::
+  AllLLVM SetupValue ->
+  L.Type             ->
+  AllLLVM SetupValue ->
+  LLVMCrucibleSetupM ()
+llvm_points_to_at_type ptr ty val =
+  llvm_points_to_internal False (Just ty) Nothing ptr val
+
+llvm_conditional_points_to_at_type ::
+  TypedTerm ->
+  AllLLVM SetupValue ->
+  L.Type             ->
+  AllLLVM SetupValue ->
+  LLVMCrucibleSetupM ()
+llvm_conditional_points_to_at_type cond ptr ty val =
+  llvm_points_to_internal False (Just ty) (Just cond) ptr val
 
 llvm_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 ()
-llvm_points_to_internal typed cond (getAllLLVM -> ptr) (getAllLLVM -> val) =
+llvm_points_to_internal typed rhsTy cond (getAllLLVM -> ptr) (getAllLLVM -> val) =
   LLVMCrucibleSetupM $
   do cc <- getLLVMCrucibleContext
      loc <- getW4Position "llvm_points_to"
@@ -2021,7 +2041,14 @@ llvm_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)
 
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 4fd4f388e6..4b3c7a0521 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -2328,6 +2328,22 @@ primitives = Map.fromList
     Current
     [ "Legacy alternative name for `llvm_conditional_points_to`." ]
 
+  , prim "llvm_points_to_at_type" "SetupValue -> LLVMType -> SetupValue -> LLVMSetup ()"
+    (pureVal llvm_points_to_at_type)
+    Current
+    [ "A variant of `llvm_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 "llvm_conditional_points_to_at_type" "Term -> SetupValue -> LLVMType -> SetupValue -> LLVMSetup ()"
+    (pureVal llvm_conditional_points_to_at_type)
+    Current
+    [ "A variant of `llvm_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 "llvm_points_to_untyped" "SetupValue -> SetupValue -> LLVMSetup ()"
     (pureVal (llvm_points_to False))
     Current