Merge pull request #970 from GaloisInc/points-to-at-type

Implement new saw-script function `crucible_points_to_at_type`.

intTests/test_llvm_points_to_at_type/Makefile

@@ -0,0 +1,2 @@
+test.bc : test.c
+	clang -c -emit-llvm -g -o test.bc test.c

intTests/test_llvm_points_to_at_type/test.c

@@ -0,0 +1,4 @@
+void f (int *p) {
+    p[2] = p[0];
+    p[3] = p[1];
+}

intTests/test_llvm_points_to_at_type/test.saw

@@ -0,0 +1,49 @@
+// This is a test to demonstrate the use of the saw-script LLVM setup
+// declaration `llvm_points_to_at_type`.
+
+bc <- llvm_load_module "test.bc";
+
+let i32 = llvm_int 32;
+
+// The function `f` copies the first half of an array into the second
+// half. So the full array needs to be allocated, but only the first
+// half needs to be initialized.
+
+// This first example fails because the types don't match in the first
+// `llvm_points_to` declaration.
+fails (
+  llvm_verify bc "f" [] false
+    do {
+      x <- llvm_fresh_var "x" (llvm_array 2 i32);
+      p <- llvm_alloc (llvm_array 4 i32);
+      llvm_points_to p (llvm_term x);
+      llvm_execute_func [p];
+      llvm_points_to p (llvm_term {{ x # x }});
+    }
+    z3);
+
+// Changing `llvm_points_to` to `llvm_points_to_at_type` will work, as
+// long as the specified type matches the type of the rhs.
+f_ov <-
+  llvm_verify bc "f" [] false
+    do {
+      x <- llvm_fresh_var "x" (llvm_array 2 i32);
+      p <- llvm_alloc (llvm_array 4 i32);
+      llvm_points_to_at_type p (llvm_array 2 i32) (llvm_term x);
+      llvm_execute_func [p];
+      llvm_points_to p (llvm_term {{ x # x }});
+    }
+    z3;
+
+// But if the specified type does not match the rhs, the declaration
+// will fail with another type mismatch error.
+fails (
+  llvm_verify bc "f" [] false
+    do {
+      x <- llvm_fresh_var "x" (llvm_array 2 i32);
+      p <- llvm_alloc (llvm_array 4 i32);
+      llvm_points_to_at_type p (llvm_array 3 i32) (llvm_term x);
+      llvm_execute_func [p];
+      llvm_points_to p (llvm_term {{ x # x }});
+    }
+    z3);

intTests/test_llvm_points_to_at_type/test.sh

@@ -0,0 +1 @@
+$SAW test.saw

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)
 

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