Pointer cast

CHANGES.md

@@ -26,6 +26,13 @@
   command.) For more details on how each of these commands should be used,
   consult the "Bitfields" section of the SAW manual.
 
+* A new `llvm_cast_pointer` function has been added that allows users
+  to directly specify that a pointer should be treated as pointing to
+  a particular type. This mainly affects the results of subsequent
+  `llvm_field` and `llvm_elem` calls.  This is especially useful for
+  dealing with C `union` types, as the type information provided by
+  LLVM is imprecise in these cases.
+
 # Version 0.9
 
 ## New Features

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

@@ -1,3 +1,4 @@
+{-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -611,6 +612,7 @@ substMethodSpec sc sm ms = do
         MS.SetupArray b svs -> MS.SetupArray b <$> mapM goSetupValue svs
         MS.SetupElem b sv idx -> MS.SetupElem b <$> goSetupValue sv <*> pure idx
         MS.SetupField b sv name -> MS.SetupField b <$> goSetupValue sv <*> pure name
+        MS.SetupCast v _ _ -> case v of {}
         MS.SetupGlobal _ _ -> return sv
         MS.SetupGlobalInitializer _ _ -> return sv
 

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

@@ -29,6 +29,7 @@ type instance MS.HasSetupStruct MIR = 'True
 type instance MS.HasSetupArray MIR = 'True
 type instance MS.HasSetupElem MIR = 'True
 type instance MS.HasSetupField MIR = 'True
+type instance MS.HasSetupCast MIR = 'False
 type instance MS.HasSetupGlobalInitializer MIR = 'False
 
 type instance MS.HasGhostState MIR = 'False
@@ -39,6 +40,8 @@ type instance MS.ExtType MIR = M.Ty
 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
 

doc/manual/manual.md

@@ -2199,7 +2199,8 @@ pointer points to a value that does not agree with its static type.
 CrucibleSetup ()` works like `llvm_points_to` but omits type
 checking. Rather than omitting type checking across the board, we
 introduced this additional function to make it clear when a type
-reinterpretation is intentional.
+reinterpretation is intentional. As an alternative, one
+may instead use `llvm_cast_pointer` to line up the static types.
 
 ## Working with Compound Types
 
@@ -2213,7 +2214,7 @@ is the array index. For `struct` values, it is the field index.
 
 * `llvm_field : SetupValue -> String -> SetupValue` yields a pointer
 to a particular named `struct` field, if debugging information is
-available in the bitcode
+available in the bitcode.
 
 Either of these functions can be used with `llvm_points_to` to
 specify the value of a particular array element or `struct` field.
@@ -2240,6 +2241,22 @@ following command will create values of such types:
 
 * `llvm_packed_struct_value : [SetupValue] -> SetupValue`
 
+C programs will sometimes make use of pointer casting to implement
+various kinds of polymorphic behaviors, either via direct pointer
+casts, or by using `union` types to codify the pattern. To reason
+about such cases, the following operation is useful.
+
+* `llvm_cast_pointer : SetupValue -> LLVMType -> SetupValue`
+
+This function function casts the type of the input value (which must be a
+pointer) so that it points to values of the given type.  This mainly
+affects the results of subsequent `llvm_field` and `llvm_elem` calls,
+and any eventual `points_to` statements that the resulting pointer
+flows into.  This is especially useful for dealing with C `union`
+types, as the type information provided by LLVM is imprecise in these
+cases.
+
+
 In the experimental Java verification implementation, the following
 functions can be used to state the equivalent of a combination of
 `llvm_points_to` and either `llvm_elem` or `llvm_field`.

intTests/test_llvm_union/Makefile

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

intTests/test_llvm_union/README

@@ -0,0 +1,4 @@
+This example is derived from an older union example
+from `examples/llvm/union`.  It is intended to demonstrate
+the use of the `llvm_pointer_cast` operation for selecting
+the branches of unions.

intTests/test_llvm_union/test.c

@@ -0,0 +1,35 @@
+#include <stdint.h>
+
+typedef enum { INC_1 , INC_2 } alg;
+
+typedef struct {
+  uint32_t x;
+} inc_1_st;
+
+typedef struct {
+  uint32_t x;
+  uint32_t y;
+} inc_2_st;
+
+typedef struct {
+  alg alg;
+  union {
+    inc_1_st inc_1_st;
+    inc_2_st inc_2_st;
+  } inc_st;
+} st;
+
+uint32_t inc(st *st) {
+  switch (st->alg) {
+  case INC_1:
+    st->inc_st.inc_1_st.x += 1;
+    break;
+  case INC_2:
+    st->inc_st.inc_2_st.x += 1;
+    st->inc_st.inc_2_st.y += 1;
+    break;
+  default:
+    return 1/0;
+  }
+  return 0;
+}

intTests/test_llvm_union/test.saw

@@ -0,0 +1,52 @@
+m <- llvm_load_module "test.bc";
+
+let {{
+INC_1 = 0 : [32]
+INC_2 = 1 : [32]
+}};
+
+
+// The argument 'INC' specifies which 'alg' enum to test.
+let inc_spec INC = do {
+
+  stp <- llvm_alloc (llvm_alias "struct.st");
+  llvm_points_to (llvm_field stp "alg") (llvm_term {{ INC }});
+
+  if eval_bool {{ INC == INC_1 }} then
+    do {
+      let p = llvm_cast_pointer (llvm_field stp "inc_st") (llvm_alias "struct.inc_1_st");
+
+      x0 <- llvm_fresh_var "x0" (llvm_int 32);
+      llvm_points_to (llvm_field p "x") (llvm_term x0);
+
+      llvm_execute_func [stp];
+
+      llvm_points_to (llvm_field p "x") (llvm_term {{ x0 + 1 }});
+    }
+  else if eval_bool {{ INC == INC_2 }} then
+    do {
+      let p = llvm_cast_pointer (llvm_field stp "inc_st") (llvm_alias "struct.inc_2_st");
+
+      x0 <- llvm_fresh_var "x0" (llvm_int 32);
+      y0 <- llvm_fresh_var "y0" (llvm_int 32);
+
+      llvm_points_to (llvm_field p "x") (llvm_term x0);
+      llvm_points_to (llvm_field p "y") (llvm_term y0);
+
+      llvm_execute_func [stp];
+
+      llvm_points_to (llvm_field p "x") (llvm_term {{ x0 + 1 }});
+      llvm_points_to (llvm_field p "y") (llvm_term {{ y0 + 1 }});
+    }
+  else return (); // Unknown INC value
+
+  llvm_return (llvm_term {{ 0 : [32] }});
+};
+
+print "Verifying 'inc_1' using 'llvm_verify':";
+llvm_verify m "inc" [] true (inc_spec {{ INC_1 }}) abc;
+print "";
+
+print "Verifying 'inc_2' using 'llvm_verify':";
+llvm_verify m "inc" [] true (inc_spec {{ INC_2 }}) abc;
+print "";

intTests/test_llvm_union/test.sh

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

saw-remote-api/src/SAWServer.hs

@@ -87,40 +87,40 @@ instance Show SAWTask where
   show (JVMSetup n) = "(JVMSetup" ++ show n ++ ")"
 
 
-data CrucibleSetupVal e
+data CrucibleSetupVal ty e
   = NullValue
-  | ArrayValue [CrucibleSetupVal e]
-  | TupleValue [CrucibleSetupVal e]
+  | ArrayValue [CrucibleSetupVal ty e]
+  | TupleValue [CrucibleSetupVal ty e]
   -- | RecordValue [(String, CrucibleSetupVal e)]
-  | FieldLValue (CrucibleSetupVal e) String
-  | ElementLValue (CrucibleSetupVal e) Int
+  | FieldLValue (CrucibleSetupVal ty e) String
+  | CastLValue (CrucibleSetupVal ty e) ty
+  | ElementLValue (CrucibleSetupVal ty e) Int
   | GlobalInitializer String
   | GlobalLValue String
   | NamedValue ServerName
   | CryptolExpr e
   deriving stock (Foldable, Functor, Traversable)
 
 data SetupStep ty
-  = SetupReturn (CrucibleSetupVal CryptolAST) -- ^ The return value
+  = SetupReturn (CrucibleSetupVal ty CryptolAST) -- ^ The return value
   | SetupFresh ServerName Text ty -- ^ Server name to save in, debug name, fresh variable type
   | SetupAlloc ServerName ty Bool (Maybe Int) -- ^ Server name to save in, type of allocation, mutability, alignment
   | SetupGhostValue ServerName Text CryptolAST -- ^ Variable, term
-  | SetupPointsTo (CrucibleSetupVal CryptolAST)
-                  (CrucibleSetupVal CryptolAST)
+  | SetupPointsTo (CrucibleSetupVal ty CryptolAST)
+                  (CrucibleSetupVal ty CryptolAST)
                   (Maybe (CheckPointsToType ty))
                   (Maybe CryptolAST)
                   -- ^ The source, the target, the type to check the target,
                   --   and the condition that must hold in order for the source to point to the target
-  | SetupPointsToBitfield (CrucibleSetupVal CryptolAST)
+  | SetupPointsToBitfield (CrucibleSetupVal ty CryptolAST)
                           Text
-                          (CrucibleSetupVal CryptolAST)
+                          (CrucibleSetupVal ty CryptolAST)
                           -- ^ The source bitfield,
                           --   the name of the field within the bitfield,
                           --   and the target.
-  | SetupExecuteFunction [CrucibleSetupVal CryptolAST] -- ^ Function's arguments
+  | SetupExecuteFunction [CrucibleSetupVal ty CryptolAST] -- ^ Function's arguments
   | SetupPrecond CryptolAST -- ^ Function's precondition
   | SetupPostcond CryptolAST -- ^ Function's postcondition
-  deriving stock (Foldable, Functor, Traversable)
 
 instance Show (SetupStep ty) where
   show _ = "⟨SetupStep⟩" -- TODO

saw-remote-api/src/SAWServer/Data/Contract.hs

@@ -35,15 +35,15 @@ data Contract ty cryptolExpr =
     , preAllocated  :: [Allocated ty]
     , preGhostValues  :: [GhostValue cryptolExpr]
     , prePointsTos  :: [PointsTo ty cryptolExpr]
-    , prePointsToBitfields :: [PointsToBitfield cryptolExpr]
-    , argumentVals  :: [CrucibleSetupVal cryptolExpr]
+    , prePointsToBitfields :: [PointsToBitfield ty cryptolExpr]
+    , argumentVals  :: [CrucibleSetupVal ty cryptolExpr]
     , postVars      :: [ContractVar ty]
     , postConds     :: [cryptolExpr]
     , postAllocated :: [Allocated ty]
     , postGhostValues :: [GhostValue cryptolExpr]
     , postPointsTos :: [PointsTo ty cryptolExpr]
-    , postPointsToBitfields :: [PointsToBitfield cryptolExpr]
-    , returnVal     :: Maybe (CrucibleSetupVal cryptolExpr)
+    , postPointsToBitfields :: [PointsToBitfield ty cryptolExpr]
+    , returnVal     :: Maybe (CrucibleSetupVal ty cryptolExpr)
     }
     deriving stock (Functor, Foldable, Traversable)
 
@@ -64,17 +64,17 @@ data Allocated ty =
 
 data PointsTo ty cryptolExpr =
   PointsTo
-    { pointer           :: CrucibleSetupVal cryptolExpr
-    , pointsTo          :: CrucibleSetupVal cryptolExpr
+    { pointer           :: CrucibleSetupVal ty cryptolExpr
+    , pointsTo          :: CrucibleSetupVal ty cryptolExpr
     , checkPointsToType :: Maybe (CheckPointsToType ty)
     , condition         :: Maybe cryptolExpr
     } deriving stock (Functor, Foldable, Traversable)
 
-data PointsToBitfield cryptolExpr =
+data PointsToBitfield ty cryptolExpr =
   PointsToBitfield
-    { bfPointer   :: CrucibleSetupVal cryptolExpr
+    { bfPointer   :: CrucibleSetupVal ty cryptolExpr
     , bfFieldName :: Text
-    , bfPointsTo  :: CrucibleSetupVal cryptolExpr
+    , bfPointsTo  :: CrucibleSetupVal ty cryptolExpr
     } deriving stock (Functor, Foldable, Traversable)
 
 data CheckAgainstTag
@@ -96,7 +96,7 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (PointsTo ty cryptolExp
                <*> o .:? "check points to type"
                <*> o .:? "condition"
 
-instance FromJSON cryptolExpr => FromJSON (PointsToBitfield cryptolExpr) where
+instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (PointsToBitfield ty cryptolExpr) where
   parseJSON =
     withObject "Points-to-bitfield relationship" $ \o ->
       PointsToBitfield <$> o .: "pointer"

saw-remote-api/src/SAWServer/Data/SetupValue.hs

@@ -15,6 +15,7 @@ data SetupValTag
   | TagArrayValue
   | TagTupleValue
   | TagFieldLValue
+  | TagCastLValue
   | TagElemLValue
   | TagGlobalInit
   | TagGlobalLValue
@@ -29,12 +30,13 @@ instance FromJSON SetupValTag where
       "array" -> pure TagArrayValue
       "tuple" -> pure TagTupleValue
       "field" -> pure TagFieldLValue
+      "cast"  -> pure TagCastLValue
       "element lvalue" -> pure TagElemLValue
       "global initializer" -> pure TagGlobalInit
       "global lvalue" -> pure TagGlobalLValue
       _ -> empty
 
-instance FromJSON cryptolExpr => FromJSON (CrucibleSetupVal cryptolExpr) where
+instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cryptolExpr) where
   parseJSON v = fromObject v
     where
       fromObject = withObject "saved value or Cryptol expression" $ \o ->
@@ -46,6 +48,7 @@ instance FromJSON cryptolExpr => FromJSON (CrucibleSetupVal cryptolExpr) where
           TagArrayValue -> ArrayValue <$> o .: "elements"
           TagTupleValue -> TupleValue <$> o .: "elements"
           TagFieldLValue -> FieldLValue <$> o .: "base" <*> o .: "field"
+          TagCastLValue -> CastLValue <$> o .: "base" <*> o .: "type"
           TagElemLValue -> ElementLValue <$> o .: "base" <*> o .: "index"
           TagGlobalInit -> GlobalInitializer <$> o .: "name"
           TagGlobalLValue -> GlobalLValue <$> o .: "name"

saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs

@@ -145,7 +145,7 @@ compileJVMContract fileReader bic cenv0 c =
            GlobalLValue name -> jvm_static_field_is name sv
            _ -> JVMSetupM $ fail "Invalid points-to statement."
 
-    setupPointsToBitfields :: PointsToBitfield (P.Expr P.PName) -> JVMSetupM ()
+    setupPointsToBitfields :: PointsToBitfield JavaType (P.Expr P.PName) -> JVMSetupM ()
     setupPointsToBitfields _ =
       JVMSetupM $ fail "Points-to-bitfield not supported in JVM API."
 
@@ -173,7 +173,7 @@ compileJVMContract fileReader bic cenv0 c =
 
     getSetupVal ::
       (Map ServerName ServerSetupVal, CryptolEnv) ->
-      CrucibleSetupVal (P.Expr P.PName) ->
+      CrucibleSetupVal JavaType (P.Expr P.PName) ->
       JVMSetupM (MS.SetupValue CJ.JVM)
     getSetupVal _ NullValue = JVMSetupM $ return (MS.SetupNull ())
     getSetupVal (env, _) (NamedValue n) =
@@ -186,6 +186,8 @@ compileJVMContract fileReader bic cenv0 c =
       JVMSetupM $ fail "Tuple setup values unsupported in JVM API."
     getSetupVal _ (FieldLValue _ _) =
       JVMSetupM $ fail "Field l-values unsupported in JVM API."
+    getSetupVal _ (CastLValue _ _) =
+      JVMSetupM $ fail "Cast l-values unsupported in JVM API."
     getSetupVal _ (ElementLValue _ _) =
       JVMSetupM $ fail "Element l-values unsupported in JVM API."
     getSetupVal _ (GlobalInitializer _) =

saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs

@@ -138,7 +138,7 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
 
     setupPointsToBitfield ::
       (Map ServerName ServerSetupVal, CryptolEnv) ->
-      PointsToBitfield (P.Expr P.PName) ->
+      PointsToBitfield JSONLLVMType (P.Expr P.PName) ->
       LLVMCrucibleSetupM ()
     setupPointsToBitfield env (PointsToBitfield p fieldName v) =
       do ptr <- getSetupVal env p
@@ -173,7 +173,7 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
 
     getSetupVal ::
       (Map ServerName ServerSetupVal, CryptolEnv) ->
-      CrucibleSetupVal (P.Expr P.PName) ->
+      CrucibleSetupVal JSONLLVMType (P.Expr P.PName) ->
       LLVMCrucibleSetupM (CMS.AllLLVM MS.SetupValue)
     getSetupVal _ NullValue = LLVMCrucibleSetupM $ return CMS.anySetupNull
     getSetupVal env (ArrayValue elts) =
@@ -185,6 +185,9 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
     getSetupVal env (FieldLValue base fld) =
       do base' <- getSetupVal env base
          LLVMCrucibleSetupM $ return $ CMS.anySetupField base' fld
+    getSetupVal env (CastLValue base ty) =
+      do base' <- getSetupVal env base
+         LLVMCrucibleSetupM $ return $ CMS.anySetupCast base' (llvmType ty)
     getSetupVal env (ElementLValue base idx) =
       do base' <- getSetupVal env base
          LLVMCrucibleSetupM $ return $ CMS.anySetupElem base' idx