Emw4/opaque shapes (#1356)

* added heapster_define_opaque_llvmshape

* tweaked some error message printing

* added a few more Rust example functions to rust_data.rs

* added yet another example, and started trying to write Heapster types for some of the recently added examples

heapster-saw/examples/rust_data.rs

@@ -142,6 +142,10 @@ impl Sum<u64,u64> {
     pub extern fn mk_u64_sum_left_extern (x:u64) -> Self {
         Sum::Left (x)
     }
+
+    pub fn mk_u64_sum_left_add3 (x:&u64, y:u64, z:u64) -> Self {
+        Sum::Left (*x+y+z)
+    }
 }
 
 pub fn mk_string_sum_left (x:&str) -> Sum<String,u64> {
@@ -274,3 +278,25 @@ impl List<u64> {
         }
     }
 }
+
+/* Dummy function to figure out the size of a HashMap */
+pub fn test_hash_map_size (x:(HashMap<u64,u64>, u64)) -> u64 {
+    let (_,u) = x; return u;
+}
+
+pub fn my_hash_insert (m: &mut HashMap<u64,u64>, x:u64, y:u64) -> Option<u64> {
+    return m.insert (x,y);
+}
+
+pub fn my_hash_insert_void (m: &mut HashMap<u64,u64>, x:u64, y:u64) -> () {
+    m.insert (x,y);
+}
+
+/* Insert a mapping into m from the greatest of x and y to the other */
+pub fn hash_map_insert_gt_to_le (m: &mut HashMap<u64,u64>, x:u64, y:u64) -> () {
+    if x > y {
+        m.insert (x, y);
+    } else {
+        m.insert (y, x);
+    }
+}

heapster-saw/examples/rust_data.saw

@@ -23,6 +23,9 @@ heapster_define_rust_type env "pub enum Result<X,Y> { Ok (X), Err (Y) }";
 // Sum type
 heapster_define_rust_type env "pub enum Sum<X,Y> { Left (X), Right (Y) }";
 
+// The Option type
+heapster_define_rust_type env "pub enum Option<X> { None, Some (X) }";
+
 // List type
 heapster_define_llvmshape env "List" 64 "L:perm(llvmptr 64),X:llvmshape 64" "(fieldsh(eq(llvmword(0)))) orsh (fieldsh(eq(llvmword(1)));X;fieldsh(L))";
 heapster_define_recursive_perm env "ListPerm" "X:llvmshape 64, Xlen:bv 64, rw:rwmodality, l:lifetime" "llvmptr 64" ["[l]memblock(rw,0,Xlen + 16,List<ListPerm<X,Xlen,rw,l>,X>)"] "\\ (X:sort 0) (_:Vec 64 Bool) -> List X" "\\ (X:sort 0) (_:Vec 64 Bool) -> foldListPermH X" "\\ (X:sort 0) (_:Vec 64 Bool) -> unfoldListPermH X";
@@ -43,6 +46,10 @@ heapster_define_rust_type env "pub struct MixedStruct { pub s: String, pub i1: u
 // TrueEnum type
 heapster_define_rust_type env "pub enum TrueEnum { Foo, Bar, Baz }";
 
+// Opaque type for HashMap<T,U>
+heapster_define_opaque_llvmshape env "HashMap" 64 "T:llvmshape 64, U:llvmshape 64" "56" "\\ (T:sort 0) (U:sort 0) -> List (T * U)";
+
+
 /***
  *** Assumed Functions
  ***/
@@ -67,6 +74,24 @@ heapster_assume_fun_rename env to_string_str "to_string_str" "(len:bv 64). arg0:
 //heapster_assume_fun_rename env to_string_str "to_string_str" "(ps:lowned_perm,l:lifetime,len:bv 64). l:lowned ps, arg0:[l]memblock(W,0,24,emptysh), arg1:array(0,<len,*1,[[l](R,0,8) |-> int8<>]), arg2:eq(llvmword(len)) -o l:lowned ps, arg0:[l]memblock(W,0,24,String<>)" "\\ (len:Vec 64 Bool) (_:#()) (str:BVVec 64 len int8Trans) -> returnM (Sigma (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> BVVec 64 len' int8Trans * int64Trans * #())) (exists (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> BVVec 64 len' int8Trans * int64Trans * #()) len (str, mkInt64Trans len, ()))";
 
 
+// HashMap::insert
+/*
+my_hash_insert_void_sym <- heapster_find_symbol env "19my_hash_insert_void";
+heapster_assume_fun_rename env my_hash_insert_void_sym "hashmap_u64_u64_insert_void" "<'a> fn (&'a mut HashMap<u64,u64>,u64,u64) -> ()" "\\ (l,k,v) -> Cons (k,v) l";
+*/
+
+/*
+// FIXME: we currently pretend this always returns None
+// FIXME: also, the layout is currently broken for return type of Option<u64>
+my_hash_insert_sym <- heapster_find_symbol env "14my_hash_insert";
+heapster_assume_fun_rename env my_hash_insert_sym "hashmap_u64_u64_insert" "<'a> fn (&'a mut HashMap<u64,u64>,u64,u64) -> Option<u64>" "\\ (l,k,v) -> Cons (k,v) l";
+*/
+
+/*
+hashmap_u64_u64_insert_sym <- heapster_find_symbol env "std11collections4hash3map24HashMap$LT$K$C$V$C$S$GT$6insert";
+heapster_assume_fun_rename env hashmap_u64_u64_insert_sym "hashmap_u64_u64_insert" "<'a> fn (&'a mut HashMap<u64,u64>,u64,u64) -> Option<u64>" "\\ (l,k,v) -> Cons (k,v) l";
+*/
+
 /***
  *** Type-Checked Functions
  ***/

heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs

@@ -6200,6 +6200,15 @@ permEnvAddDefinedShape env nm args mb_sh =
           SomeNamedShape (NamedShape nm args $
                           DefinedShapeBody mb_sh) : permEnvNamedShapes env }
 
+-- | Add an opaque LLVM shape to a permission environment
+permEnvAddOpaqueShape :: (1 <= w, KnownNat w) => PermEnv -> String ->
+                         CruCtx args -> Mb args (PermExpr (BVType w)) ->
+                         Ident -> PermEnv
+permEnvAddOpaqueShape env nm args mb_len tp_id =
+  env { permEnvNamedShapes =
+          SomeNamedShape (NamedShape nm args $
+                          OpaqueShapeBody mb_len tp_id) : permEnvNamedShapes env }
+
 -- | Add a global symbol with a function permission to a 'PermEnv'
 permEnvAddGlobalSymFun :: (1 <= w, KnownNat w) => PermEnv -> GlobalSymbol ->
                           f w -> FunPerm ghosts args ret -> OpenTerm -> PermEnv

heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs

@@ -506,16 +506,16 @@ un3SomeFunPerm args ret (Some3FunPerm fun_perm)
   , Just Refl <- testEquality ret (funPermRet fun_perm) =
     return $ SomeFunPerm fun_perm
 un3SomeFunPerm args ret (Some3FunPerm fun_perm) =
-  fail $ renderDoc $ fillSep
-  [pretty "Incorrect LLVM type for function permission:",
-   permPretty emptyPPInfo fun_perm,
-   pretty "Expected type:"
-   <+> permPretty emptyPPInfo args <+> pretty "=>"
-   <+> permPretty emptyPPInfo ret,
-   pretty "Actual type:"
-   <+> permPretty emptyPPInfo (funPermArgs fun_perm)
-   <+> pretty "=>" <+> permPretty emptyPPInfo (funPermRet fun_perm)
-   ]
+  fail $ renderDoc $ vsep
+  [ pretty "Incorrect LLVM type for function permission:"
+  , permPretty emptyPPInfo fun_perm
+  , pretty "Expected type:"
+    <+> PP.group (permPretty emptyPPInfo args) <+> pretty "=>"
+    <+> PP.group (permPretty emptyPPInfo ret)
+  , pretty "Actual type:"
+    <+> PP.group (permPretty emptyPPInfo (funPermArgs fun_perm))
+    <+> pretty "=>"
+    <+> PP.group (permPretty emptyPPInfo (funPermRet fun_perm)) ]
 
 -- | Build a function permission from an 'ArgLayout' plus return permission
 funPerm3FromArgLayout :: ArgLayout -> TypeRepr ret -> ValuePerm ret ->

src/SAWScript/HeapsterBuiltins.hs

@@ -29,6 +29,7 @@ module SAWScript.HeapsterBuiltins
        , heapster_define_reachability_perm
        , heapster_define_perm
        , heapster_define_llvmshape
+       , heapster_define_opaque_llvmshape
        , heapster_define_rust_type
        , heapster_block_entry_hint
        , heapster_gen_block_perms_hint
@@ -617,7 +618,8 @@ heapster_define_perm _bic _opts henv nm args_str tp_str perm_string =
      let env' = permEnvAddDefinedPerm env nm args tp_perm perm
      liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'
 
--- | Define a new named llvm shape with the given name, arguments, and width
+-- | Define a new named llvm shape with the given name, pointer width,
+-- arguments, and definition as a shape
 heapster_define_llvmshape :: BuiltinContext -> Options -> HeapsterEnv ->
                              String -> Int -> String -> String ->
                              TopLevel ()
@@ -631,6 +633,29 @@ heapster_define_llvmshape _bic _opts henv nm w_int args_str sh_str =
      let env' = withKnownNat w $ permEnvAddDefinedShape env nm args mb_sh
      liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'
 
+-- | Define a new opaque llvm shape with the given name, pointer width,
+-- arguments, expression for the length in bytes, and SAW core expression for a
+-- type-level function from the Heapster translations of the argument types to a
+-- SAW core type
+heapster_define_opaque_llvmshape :: BuiltinContext -> Options -> HeapsterEnv ->
+                                    String -> Int -> String -> String -> String ->
+                                    TopLevel ()
+heapster_define_opaque_llvmshape _bic _opts henv nm w_int args_str len_str tp_str =
+  do env <- liftIO $ readIORef $ heapsterEnvPermEnvRef henv
+     (Some (Pair w LeqProof)) <-
+       failOnNothing "Shape width must be positive" $ someNatGeq1 w_int
+     Some args_ctx <- parseParsedCtxString "argument types" env args_str
+     let args = parsedCtxCtx args_ctx
+     mb_len <- parseExprInCtxString env (BVRepr w) args_ctx len_str
+     sc <- getSharedContext
+     tp_tp <- liftIO $
+       translateCompleteTypeInCtx sc env args (nus (cruCtxProxies args) $
+                                               const $ ValuePermRepr $
+                                               LLVMShapeRepr w)
+     tp_id <- parseAndInsDef henv nm tp_tp tp_str
+     let env' = withKnownNat w $ permEnvAddOpaqueShape env nm args mb_len tp_id
+     liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'
+
 -- | Define a new named LLVM shape from a Rust type declaration
 heapster_define_rust_type :: BuiltinContext -> Options -> HeapsterEnv ->
                              String -> TopLevel ()

src/SAWScript/Interpreter.hs

@@ -3048,6 +3048,23 @@ primitives = Map.fromList
     , " such that nm<x1,...,xn> is equivalent to the permission p."
     ]
 
+  , prim "heapster_define_opaque_llvmshape"
+    "HeapsterEnv -> String -> Int -> String -> String -> String -> TopLevel HeapsterEnv"
+    (bicVal heapster_define_opaque_llvmshape)
+    Experimental
+    [ "heapster_define_opaque_llvmshape henv nm w args len tp defines a Heapster"
+    , " LLVM shape that is opaque, meaning it acts as a sort of shape axiom, where"
+    , " Heapster does not know or care about the contents of memory of this shape"
+    , " but instead treats that memory as an opaque object, defined only by its"
+    , " length and its translation to a SAW core type."
+    , ""
+    , " The henv argument is the Heapster environment this new shape is added to,"
+    , " nm is its name, args is a context of argument variables for this shape,"
+    , " len is an expression for the length of the shape in terms of the arguments,"
+    , " and tp gives the translation of the shape as a SAW core type over the"
+    , " translation of the arguments to SAW core variables."
+    ]
+
   , prim "heapster_define_rust_type"
     "HeapsterEnv -> String -> TopLevel HeapsterEnv"
     (bicVal heapster_define_rust_type)