Fix Heapster Rust translation

heapster-saw/examples/rust_data.rs

@@ -279,19 +279,6 @@ 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 {

heapster-saw/examples/rust_data.saw

@@ -50,6 +50,9 @@ 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 Vec<T>
+//heapster_define_opaque_llvmshape env "Vec" 64 "T:llvmshape 64" "24" "\\ (T:sort 0) -> List T";
+
 // 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)";
 
@@ -79,22 +82,10 @@ heapster_assume_fun_rename env to_string_str "to_string_str" "(len:bv 64). arg0:
 
 
 // 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";
-*/
+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>" "\\ (endl:HashMap int64Trans int64Trans * #() -> CompM (HashMap int64Trans int64Trans * #())) (h:HashMap int64Trans int64Trans) (k:int64Trans) (v:int64Trans) -> returnM ((#() -> CompM (HashMap int64Trans int64Trans * #())) * Either #() int64Trans * #()) ((\\ (_:#()) -> returnM (HashMap int64Trans int64Trans * #()) (Cons (int64Trans * int64Trans) (k,v) h, ())), Left #() int64Trans (), ())";
+
 
 /***
  *** Type-Checked Functions
@@ -149,7 +140,7 @@ heapster_typecheck_fun_rename env list_head_sym "list_head" "<'a> fn (l: &'a Lis
 
 // list_head_impl
 list_head_impl_sym <- heapster_find_symbol env "14list_head_impl";
-//heapster_typecheck_fun_rename env list_head_impl_sym "list_head_impl" "<'a> fn (l: &'a List<u64>) -> Result<u64,()>";
+heapster_typecheck_fun_rename env list_head_impl_sym "list_head_impl" "<'a> fn (l: &'a List<u64>) -> Result<u64,()>";
 //heapster_typecheck_fun_rename env list_head_impl_sym "list_head_impl" "(rw:rwmodality).arg0:List<fieldsh(int64<>),8,rw,always> -o ret:(struct(eq(llvmword(0)),exists z:bv 64. eq(llvmword(z)))) or (struct(eq(llvmword(1)),true))";
 
 // StrStruct::new

heapster-saw/examples/rust_data_proofs.v

@@ -23,7 +23,7 @@ Print list_is_empty__tuple_fun.
 
 Print list_head__tuple_fun.
 
-(* Print list_head_impl__tuple_fun. *)
+Print list_head_impl__tuple_fun.
 
 Print str_struct_new__tuple_fun.
 

heapster-saw/examples/rust_lifetimes.v

@@ -41,9 +41,10 @@ Definition unfoldListPermH : forall (a : Type), @Datatypes.list a -> @SAWCorePre
 Definition foldListPermH : forall (a : Type), @SAWCorePrelude.Either unit (prod unit (prod a (@Datatypes.list a))) -> @Datatypes.list a :=
   fun (a : Type) => @SAWCorePrelude.either unit (prod unit (prod a (@Datatypes.list a))) (@Datatypes.list a) (fun (_1 : unit) => @Datatypes.nil a) (fun (tup : prod unit (prod a (@Datatypes.list a))) => @Datatypes.cons a (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd tup)) (SAWCoreScaffolding.snd (SAWCoreScaffolding.snd tup))).
 
-Definition llvm__x2euadd__x2ewith__x2eoverflow__x2ei64 : forall (p0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)), forall (p1 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
-  let var__1   := @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool) in
-  CompM (prod (@sigT var__0 (fun (x_ex0 : var__0) => unit)) (prod (@sigT var__1 (fun (x_ex0 : var__1) => unit)) unit)) :=
+Definition llvm__x2euadd__x2ewith__x2eoverflow__x2ei64 : forall (p0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)), forall (p1 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)), let var__0   := forall (a : Type), forall (b : a -> Type), Type in
+  let var__1   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  let var__2   := @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@sigT var__1 (fun (x_ex0 : var__1) => unit)) (prod (@sigT var__2 (fun (x_ex0 : var__2) => unit)) unit)) :=
   fun (x : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (y : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) => @returnM CompM _ (prod int64Trans (prod int1Trans unit)) (pair (@mkInt64Trans (@SAWCoreVectorsAsCoqVectors.bvAdd 64 (@unInt64Trans x) (@unInt64Trans y))) (pair (@mkInt1Trans (@SAWCoreVectorsAsCoqVectors.gen 1 (@SAWCoreScaffolding.Bool) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.bvCarry 64 (@unInt64Trans x) (@unInt64Trans y)))) tt)).
 
 Definition llvm__x2eexpect__x2ei1 : forall (p0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)), forall (p1 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool) in

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

@@ -489,6 +489,22 @@ assignToRList asgn = case viewAssign asgn of
   AssignEmpty -> MNil
   AssignExtend asgn' f -> assignToRList asgn' :>: f
 
+-- | Invert 'assignToRList', converting a Hobbits 'RAssign' over a Hobbits
+-- context generated by 'CtxToRList' back to a Crucible 'Assignment'
+unAssignToRList :: Assignment prx ctx -> RAssign f (CtxToRList ctx) ->
+                   Assignment f ctx
+unAssignToRList ctx fs =
+  let sz = Ctx.size ctx in
+  Ctx.generate sz $ \ix -> RL.get (indexToMember sz ix) fs
+
+-- | Append two Hobbits 'RAssign's that have been generated by 'assignToRList'
+assignToRListAppend :: Assignment prx1 ctx1 -> Assignment prx2 ctx2 ->
+                       RAssign f (CtxToRList ctx1) ->
+                       RAssign f (CtxToRList ctx2) ->
+                       RAssign f (CtxToRList (ctx1 <+> ctx2))
+assignToRListAppend ctx1 ctx2 fs1 fs2 =
+  assignToRList (unAssignToRList ctx1 fs1 Ctx.<++> unAssignToRList ctx2 fs2)
+
 -- | Convert a Crucible 'Assignment' over a context of contexts to an 'RAssign'
 -- over a right-list of right-lists
 assignToRListRList :: (forall c. f c -> g (CtxToRList c)) ->

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

@@ -2964,6 +2964,57 @@ isConjPerm (ValPerm_Named n _ _) = nameSortIsConj (namedPermNameSort n)
 isConjPerm (ValPerm_Var _ _) = False
 isConjPerm (ValPerm_Conj _) = True
 
+-- | Return a struct permission where all fields have @true@ permissions
+trueStructAtomicPerm :: Assignment prx ctx -> AtomicPerm (StructType ctx)
+trueStructAtomicPerm =
+  Perm_Struct . RL.map (const ValPerm_True). assignToRList
+
+-- | Take two list of atomic struct permissions, one for structs with fields
+-- given by @ctx1@ and one with those given by @ctx2@, and append them pointwise
+-- to get a list of atomic struct permissions whose fields are given by the
+-- append @ctx1 <+> ctx2@. If one list is shorter than the other, fill it out
+-- with struct permissions @struct (true, ..., true)@ of all @true@ permissions.
+-- This only works if both lists have only 'Perm_Struct' permissions, and
+-- otherwise return 'Nothing'.
+tryAppendStructAPerms :: Assignment prx1 ctx1 -> Assignment prx2 ctx2 ->
+                         [AtomicPerm (StructType ctx1)] ->
+                         [AtomicPerm (StructType ctx2)] ->
+                         Maybe [AtomicPerm (StructType (ctx1 <+> ctx2))]
+tryAppendStructAPerms _ _ [] [] = return []
+tryAppendStructAPerms ctx1 ctx2 (Perm_Struct fs_ps:ps) (Perm_Struct fs_qs:qs) =
+  (Perm_Struct (assignToRListAppend ctx1 ctx2 fs_ps fs_qs) :) <$>
+  tryAppendStructAPerms ctx1 ctx2 ps qs
+tryAppendStructAPerms ctx1 ctx2 [] qs =
+  tryAppendStructAPerms ctx1 ctx2 [trueStructAtomicPerm ctx1] qs
+tryAppendStructAPerms ctx1 ctx2 ps [] =
+  tryAppendStructAPerms ctx1 ctx2 ps [trueStructAtomicPerm ctx2]
+tryAppendStructAPerms _ _ _ _ = mzero
+
+-- | Try to append struct permissions for structs with fields given by @ctx1@
+-- and @ctx2@ to get a permission for structs with fields given by the append
+-- @ctx1 <+> ctx2@ of these two contexts. Return 'Nothing' if this is not
+-- possible.
+tryAppendStructPerms :: Assignment prx1 ctx1 -> Assignment prx2 ctx2 ->
+                        ValuePerm (StructType ctx1) ->
+                        ValuePerm (StructType ctx2) ->
+                        Maybe (ValuePerm (StructType (ctx1 <+> ctx2)))
+tryAppendStructPerms ctx1 ctx2 (ValPerm_Or p1 p2) q =
+  ValPerm_Or <$> tryAppendStructPerms ctx1 ctx2 p1 q <*>
+  tryAppendStructPerms ctx1 ctx2 p2 q
+tryAppendStructPerms ctx1 ctx2 p (ValPerm_Or q1 q2) =
+  ValPerm_Or <$> tryAppendStructPerms ctx1 ctx2 p q1 <*>
+  tryAppendStructPerms ctx1 ctx2 p q2
+tryAppendStructPerms ctx1 ctx2 (ValPerm_Exists mb_p) q =
+  ValPerm_Exists <$> mbMaybe (flip fmap mb_p $ \p ->
+                               tryAppendStructPerms ctx1 ctx2 p q)
+tryAppendStructPerms ctx1 ctx2 p (ValPerm_Exists mb_q) =
+  ValPerm_Exists <$> mbMaybe (flip fmap mb_q $ \q ->
+                               tryAppendStructPerms ctx1 ctx2 p q)
+tryAppendStructPerms ctx1 ctx2 (ValPerm_Conj ps) (ValPerm_Conj qs) =
+  ValPerm_Conj <$> tryAppendStructAPerms ctx1 ctx2 ps qs
+tryAppendStructPerms _ _ _ _ = mzero
+
+
 -- | Helper function to build a 'Perm_LLVMFunPtr' from a 'FunPerm'
 mkPermLLVMFunPtr :: (1 <= w, KnownNat w) => f w -> FunPerm ghosts args ret ->
                     AtomicPerm (LLVMPointerType w)