Merge pull request #1576 from GaloisInc/guess-unions

Add a new `llvm_union` command that uses DWARF debug information

CHANGES.md

@@ -33,6 +33,13 @@
   dealing with C `union` types, as the type information provided by
   LLVM is imprecise in these cases.
 
+* A new `llvm_union` function has been added that uses debug
+  information to allow users to select fields from `union` types by
+  name. This automates the process of manually applying
+  `llvm_cast_pointer` with the type of the selected union field. Just
+  as with `llvm_field`, debug symbols are required for `llvm_union` to
+  work correctly.
+
 # Version 0.9
 
 ## New Features

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

@@ -613,6 +613,7 @@ substMethodSpec sc sm ms = do
         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.SetupUnion v _ _ -> case v of {}
         MS.SetupGlobal _ _ -> return sv
         MS.SetupGlobalInitializer _ _ -> return sv
 

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

@@ -30,6 +30,7 @@ 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.HasSetupUnion MIR = 'False
 type instance MS.HasSetupGlobalInitializer MIR = 'False
 
 type instance MS.HasGhostState MIR = 'False

doc/manual/manual.md

@@ -2256,6 +2256,18 @@ flows into.  This is especially useful for dealing with C `union`
 types, as the type information provided by LLVM is imprecise in these
 cases.
 
+We can automate the process of applying pointer casts if we have debug
+information avaliable:
+
+* `llvm_union : SetupValue -> String -> SetupValue`
+
+Given a pointer setup value, this attempts to select the named union
+branch and cast the type of the pointer. For this to work, debug
+symbols must be included; moreover, the process of correlating LLVM
+type information with information contained in debug symbols is a bit
+heuristic. If `llvm_union` cannot figure out how to cast a pointer,
+one can fall back on the more manual `llvm_cast_pointer` instead.
+
 
 In the experimental Java verification implementation, the following
 functions can be used to state the equivalent of a combination of

intTests/test_llvm_union2/Makefile

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

intTests/test_llvm_union2/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_union` operation for selecting
+the branches of unions.

intTests/test_llvm_union2/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_union2/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_union (llvm_field stp "inc_st") "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_union (llvm_field stp "inc_st") "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_union2/test.sh

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

saw-remote-api/src/SAWServer.hs

@@ -94,6 +94,7 @@ data CrucibleSetupVal ty e
   -- | RecordValue [(String, CrucibleSetupVal e)]
   | FieldLValue (CrucibleSetupVal ty e) String
   | CastLValue (CrucibleSetupVal ty e) ty
+  | UnionLValue (CrucibleSetupVal ty e) String
   | ElementLValue (CrucibleSetupVal ty e) Int
   | GlobalInitializer String
   | GlobalLValue String

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

@@ -16,6 +16,7 @@ data SetupValTag
   | TagTupleValue
   | TagFieldLValue
   | TagCastLValue
+  | TagUnionLValue
   | TagElemLValue
   | TagGlobalInit
   | TagGlobalLValue
@@ -31,6 +32,7 @@ instance FromJSON SetupValTag where
       "tuple" -> pure TagTupleValue
       "field" -> pure TagFieldLValue
       "cast"  -> pure TagCastLValue
+      "union" -> pure TagUnionLValue
       "element lvalue" -> pure TagElemLValue
       "global initializer" -> pure TagGlobalInit
       "global lvalue" -> pure TagGlobalLValue
@@ -49,6 +51,7 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cr
           TagTupleValue -> TupleValue <$> o .: "elements"
           TagFieldLValue -> FieldLValue <$> o .: "base" <*> o .: "field"
           TagCastLValue -> CastLValue <$> o .: "base" <*> o .: "type"
+          TagUnionLValue -> UnionLValue <$> o .: "base" <*> o .: "field"
           TagElemLValue -> ElementLValue <$> o .: "base" <*> o .: "index"
           TagGlobalInit -> GlobalInitializer <$> o .: "name"
           TagGlobalLValue -> GlobalLValue <$> o .: "name"

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

@@ -188,6 +188,8 @@ compileJVMContract fileReader bic cenv0 c =
       JVMSetupM $ fail "Field l-values unsupported in JVM API."
     getSetupVal _ (CastLValue _ _) =
       JVMSetupM $ fail "Cast l-values unsupported in JVM API."
+    getSetupVal _ (UnionLValue _ _) =
+      JVMSetupM $ fail "Union 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

@@ -188,6 +188,9 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
     getSetupVal env (CastLValue base ty) =
       do base' <- getSetupVal env base
          LLVMCrucibleSetupM $ return $ CMS.anySetupCast base' (llvmType ty)
+    getSetupVal env (UnionLValue base fld) =
+      do base' <- getSetupVal env base
+         LLVMCrucibleSetupM $ return $ CMS.anySetupUnion base' fld
     getSetupVal env (ElementLValue base idx) =
       do base' <- getSetupVal env base
          LLVMCrucibleSetupM $ return $ CMS.anySetupElem base' idx

saw-script.cabal

@@ -48,6 +48,7 @@ library
     , haskeline
     , heapster-saw
     , hobbits >= 1.3.1
+    , galois-dwarf >= 0.2.2
     , IfElse
     , jvm-parser
     , lens

src/SAWScript/Crucible/Common/MethodSpec.hs

@@ -112,6 +112,7 @@ type family HasSetupElem ext :: Bool
 type family HasSetupField ext :: Bool
 type family HasSetupGlobal ext :: Bool
 type family HasSetupCast ext :: Bool
+type family HasSetupUnion ext :: Bool
 type family HasSetupGlobalInitializer ext :: Bool
 
 -- | From the manual: \"The SetupValue type corresponds to values that can occur
@@ -127,6 +128,7 @@ data SetupValue ext where
   SetupElem   :: B (HasSetupElem ext) -> SetupValue ext -> Int -> SetupValue ext
   SetupField  :: B (HasSetupField ext) -> SetupValue ext -> String -> SetupValue ext
   SetupCast   :: B (HasSetupCast ext) -> SetupValue ext -> CastType ext -> SetupValue ext
+  SetupUnion  :: B (HasSetupUnion ext) -> SetupValue ext -> String -> SetupValue ext
 
   -- | A pointer to a global variable
   SetupGlobal :: B (HasSetupGlobal ext) -> String -> SetupValue ext
@@ -144,6 +146,7 @@ type SetupValueHas (c :: Type -> Constraint) ext =
   , c (B (HasSetupElem ext))
   , c (B (HasSetupField ext))
   , c (B (HasSetupCast ext))
+  , c (B (HasSetupUnion ext))
   , c (B (HasSetupGlobal ext))
   , c (B (HasSetupGlobalInitializer ext))
   , c (CastType ext)
@@ -170,6 +173,7 @@ ppSetupValue setupval = case setupval of
   SetupArray _ vs  -> PP.brackets (commaList (map ppSetupValue vs))
   SetupElem _ v i  -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ show i)
   SetupField _ v f -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ f)
+  SetupUnion _ v u -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ u)
   SetupCast _ v tp -> PP.parens (ppSetupValue v) PP.<> PP.pretty (" AS " ++ show tp)
   SetupGlobal _ nm -> PP.pretty ("global(" ++ nm ++ ")")
   SetupGlobalInitializer _ nm -> PP.pretty ("global_initializer(" ++ nm ++ ")")

src/SAWScript/Crucible/JVM/MethodSpecIR.hs

@@ -59,6 +59,7 @@ type instance MS.HasSetupArray CJ.JVM = 'False
 type instance MS.HasSetupElem CJ.JVM = 'False
 type instance MS.HasSetupField CJ.JVM = 'False
 type instance MS.HasSetupCast CJ.JVM = 'False
+type instance MS.HasSetupUnion CJ.JVM = 'False
 type instance MS.HasSetupGlobalInitializer CJ.JVM = 'False
 
 type instance MS.HasGhostState CJ.JVM = 'False

src/SAWScript/Crucible/JVM/Override.hs

@@ -964,6 +964,7 @@ instantiateSetupValue sc s v =
     MS.SetupElem empty _ _            -> absurd empty
     MS.SetupField empty _ _           -> absurd empty
     MS.SetupCast empty _ _            -> absurd empty
+    MS.SetupUnion empty _ _           -> absurd empty
     MS.SetupGlobalInitializer empty _ -> absurd empty
   where
     doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t

src/SAWScript/Crucible/JVM/ResolveSetupValue.hs

@@ -145,6 +145,7 @@ typeOfSetupValue _cc env _nameEnv val =
     MS.SetupElem empty _ _            -> absurd empty
     MS.SetupField empty _ _           -> absurd empty
     MS.SetupCast empty _ _            -> absurd empty
+    MS.SetupUnion empty _ _           -> absurd empty
     MS.SetupGlobalInitializer empty _ -> absurd empty
 
 lookupAllocIndex :: Map AllocIndex a -> AllocIndex -> a
@@ -175,6 +176,7 @@ resolveSetupVal cc env _tyenv _nameEnv val =
     MS.SetupElem empty _ _            -> absurd empty
     MS.SetupField empty _ _           -> absurd empty
     MS.SetupCast empty _ _            -> absurd empty
+    MS.SetupUnion empty _ _           -> absurd empty
     MS.SetupGlobalInitializer empty _ -> absurd empty
   where
     sym = cc^.jccSym

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -697,7 +697,7 @@ checkSpecArgumentTypes cc mspec = mapM_ resolveArg [0..(nArgs-1)]
     resolveArg i =
       case Map.lookup i (mspec ^. MS.csArgBindings) of
         Just (mt, sv) -> do
-          mt' <- typeOfSetupValue cc tyenv nameEnv sv
+          mt' <- exceptToFail (typeOfSetupValue cc tyenv nameEnv sv)
           checkArgTy i mt mt'
         Nothing -> throwMethodSpec mspec $ unwords
           ["Argument", show i, "unspecified when verifying", show nm]
@@ -721,7 +721,7 @@ checkSpecReturnType cc mspec =
              " has void return type"
            ]
     (Just sv, Just retTy) ->
-      do retTy' <-
+      do retTy' <- exceptToFail $
            typeOfSetupValue cc
              (MS.csAllocations mspec) -- map allocation indices to allocations
              (mspec ^. MS.csPreState . MS.csVarTypeNames) -- map alloc indices to var names
@@ -2206,7 +2206,7 @@ llvm_points_to_internal mbCheckType cond (getAllLLVM -> ptr) (getAllLLVM -> val)
           let path = []
           lhsTy <- llvm_points_to_check_lhs_validity ptr loc path
 
-          valTy <- typeOfSetupValue cc env nameEnv val
+          valTy <- exceptToFail $ typeOfSetupValue cc env nameEnv val
           case mbCheckType of
             Nothing                          -> pure ()
             Just CheckAgainstPointerType     -> checkMemTypeCompatibility loc lhsTy valTy
@@ -2243,9 +2243,9 @@ llvm_points_to_bitfield (getAllLLVM -> ptr) fieldName (getAllLLVM -> val) =
           let path = [ResolvedField fieldName]
           _ <- llvm_points_to_check_lhs_validity ptr loc path
 
-          bfIndex <- resolveSetupBitfieldIndexOrFail cc env nameEnv ptr fieldName
+          bfIndex <- exceptToFail $ resolveSetupBitfield cc env nameEnv ptr fieldName
           let lhsFieldTy = Crucible.IntType $ fromIntegral $ biFieldSize bfIndex
-          valTy <- typeOfSetupValue cc env nameEnv val
+          valTy <- exceptToFail $ typeOfSetupValue cc env nameEnv val
           -- Currently, we require the type of the RHS value to precisely match
           -- the type of the field within the bitfield. One could imagine
           -- having finer-grained control over this (e.g.,
@@ -2279,7 +2279,7 @@ llvm_points_to_check_lhs_validity ptr loc path =
        else Setup.csResolvedState %= markResolved ptr path
      let env = MS.csAllocations (st ^. Setup.csMethodSpec)
          nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
-     ptrTy <- typeOfSetupValue cc env nameEnv ptr
+     ptrTy <- exceptToFail $ typeOfSetupValue cc env nameEnv ptr
      case ptrTy of
        Crucible.PtrType symTy ->
          case Crucible.asMemType symTy of
@@ -2326,7 +2326,7 @@ llvm_points_to_array_prefix (getAllLLVM -> ptr) arr sz =
             else Setup.csResolvedState %= markResolved ptr []
           let env = MS.csAllocations (st ^. Setup.csMethodSpec)
               nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
-          ptrTy <- typeOfSetupValue cc env nameEnv ptr
+          ptrTy <- exceptToFail $ typeOfSetupValue cc env nameEnv ptr
           _ <- case ptrTy of
             Crucible.PtrType symTy ->
               case Crucible.asMemType symTy of
@@ -2351,8 +2351,8 @@ llvm_equal (getAllLLVM -> val1) (getAllLLVM -> val2) =
      st <- get
      let env = MS.csAllocations (st ^. Setup.csMethodSpec)
          nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
-     ty1 <- typeOfSetupValue cc env nameEnv val1
-     ty2 <- typeOfSetupValue cc env nameEnv val2
+     ty1 <- exceptToFail $ typeOfSetupValue cc env nameEnv val1
+     ty2 <- exceptToFail $ typeOfSetupValue cc env nameEnv val2
 
      b <- liftIO $ checkRegisterCompatibility ty1 ty2
      unless b $ throwCrucibleSetup loc $ unlines

src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

@@ -98,6 +98,7 @@ module SAWScript.Crucible.LLVM.MethodSpecIR
   , anySetupStruct
   , anySetupElem
   , anySetupField
+  , anySetupUnion
   , anySetupNull
   , anySetupGlobal
   , anySetupGlobalInitializer
@@ -173,6 +174,7 @@ type instance MS.HasSetupArray (LLVM _) = 'True
 type instance MS.HasSetupElem (LLVM _) = 'True
 type instance MS.HasSetupField (LLVM _) = 'True
 type instance MS.HasSetupCast (LLVM _) = 'True
+type instance MS.HasSetupUnion (LLVM _) = 'True
 type instance MS.HasSetupGlobal (LLVM _) = 'True
 type instance MS.HasSetupGlobalInitializer (LLVM _) = 'True
 
@@ -582,6 +584,9 @@ anySetupCast val ty = mkAllLLVM (MS.SetupCast () (getAllLLVM val) ty)
 anySetupField :: AllLLVM MS.SetupValue -> String -> AllLLVM MS.SetupValue
 anySetupField val field = mkAllLLVM (MS.SetupField () (getAllLLVM val) field)
 
+anySetupUnion :: AllLLVM MS.SetupValue -> String -> AllLLVM MS.SetupValue
+anySetupUnion val uname = mkAllLLVM (MS.SetupUnion () (getAllLLVM val) uname)
+
 anySetupNull :: AllLLVM MS.SetupValue
 anySetupNull = mkAllLLVM (MS.SetupNull ())