Heapster array field implications

heapster-saw/examples/arrays.saw

@@ -1,29 +1,28 @@
 enable_experimental;
 env <- heapster_init_env_from_file "arrays.sawcore" "arrays.bc";
 
-heapster_typecheck_fun env "contains0_rec_" "(len:bv 64).arg0:eq(llvmword(len)), arg1:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg2:(exists z:bv 64.eq(llvmword(z))) -o arg0:true, arg1:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg2:true, ret:exists z:(bv 64).eq(llvmword(z))";
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))";
+
+heapster_define_perm env "int64array" "len:bv 64" "llvmptr 64" "array(0,<len,*8,[(W,0) |-> int64<>])";
+
+
+heapster_typecheck_fun env "contains0_rec_" "(len:bv 64).arg0:eq(llvmword(len)), arg1:int64array<len>, arg2:int64<> -o arg0:true, arg1:int64array<len>, arg2:true, ret:int64<>";
 
 // the old way using a block entry hint
 // heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 // heapster_block_entry_hint env "contains0" 9 "top0:bv 64, top1:llvmptr 64, top2:llvmptr 64" "frm:llvmframe 64, x0:llvmptr 64, x1:llvmptr 64" "top0:true, top1:array(0,<top0,*1,[(W,0) |-> int64<>]), top2:eq(llvmword(top0)), arg0:ptr((W,0) |-> true), arg1:ptr((W,0) |-> eq(x1)), arg2:ptr((W,0) |-> eq(x0)), arg3:ptr((W,0) |-> int64<>), frm:llvmframe [arg3:8, arg2:8, arg1:8, arg0:8], x0:eq(top2), x1:eq(top1)";
 // heapster_typecheck_fun env "contains0" "(len:bv 64).arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:eq(llvmword(len)) -o arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:true, ret:int64<>";
 
-// the new way using a gen perms hint
-heapster_gen_block_perms_hint env "contains0" []; // Note that we could give specific block numbers here (e.g. [9]), but giving nothing will just add a hint to every block, which works just fine for this function.
-heapster_typecheck_fun env "contains0" "(len:bv 64).arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:eq(llvmword(len)) -o arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:true, ret:exists z:(bv 64).eq(llvmword(z))";
+heapster_typecheck_fun env "contains0" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:int64<>";
 
-// the new way using a gen perms hint
-heapster_gen_block_perms_hint env "zero_array" [];
-heapster_typecheck_fun env "zero_array" "(len:bv 64).arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:eq(llvmword(len)) -o arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:true, ret:true";
+heapster_typecheck_fun env "zero_array" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:true";
 
-heapster_gen_block_perms_hint env "zero_array_from" [];
-heapster_typecheck_fun env "zero_array_from" "(len:bv 64, off:bv 64).arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:eq(llvmword(len)), arg2:eq(llvmword(off)) -o arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:true, ret:true";
+heapster_typecheck_fun env "zero_array_from" "(len:bv 64, off:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)), arg2:eq(llvmword(off)) -o arg0:int64array<len>, arg1:true, ret:true";
 
-heapster_gen_block_perms_hint env "filter_and_sum_pos" [];
 heapster_join_point_hint env "filter_and_sum_pos" [];
-heapster_typecheck_fun env "filter_and_sum_pos" "(len:bv 64).arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:eq(llvmword(len)) -o arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:true, ret:exists x:bv 64.eq(llvmword(x))";
+heapster_typecheck_fun env "filter_and_sum_pos" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:int64<>";
 
-heapster_gen_block_perms_hint env "sum_2d" [];
-heapster_typecheck_fun env "sum_2d" "(l1:bv 64,l2:bv 64).arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:eq(llvmword(l1)), arg2:eq(llvmword(l2)) -o arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:true, arg2:true, ret:exists x:bv 64.eq(llvmword(x))";
+heapster_typecheck_fun env "sum_2d" "(l1:bv 64,l2:bv 64).arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:eq(llvmword(l1)), arg2:eq(llvmword(l2)) -o arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:true, arg2:true, ret:int64<>";
 
 heapster_export_coq env "arrays_gen.v";

heapster-saw/examples/clearbufs.sawcore

@@ -25,9 +25,9 @@ Mbox_def = Mbox;
             (m:Mbox) -> P m;
 Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m; -}
 
---unfoldMbox : Mbox -> Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #());
+--unfoldMbox : Mbox -> Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool));
 primitive
-unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool) * #()));
+unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool)));
 
 {-unfoldMbox m =
   Mbox__rec (\ (_:Mbox) -> Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()))
@@ -38,7 +38,7 @@ unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 l
   -}
 
 primitive
-foldMbox : Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool) * #())) -> Mbox;
+foldMbox : Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool))) -> Mbox;
 
 --(Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #()) -> Mbox;
 {-

heapster-saw/examples/iter_linked_list.sawcore

@@ -27,20 +27,20 @@ ListF__rec : (a b:sort 0) -> (P : ListF a b -> sort 0) ->
              (l:ListF a b) -> P l;
 ListF__rec a b P f1 f2 l = ListF#rec a b P f1 f2 l;
 
-unfoldListF : (a b:sort 0) -> ListF a b -> Either b (a * ListF a b * #());
+unfoldListF : (a b:sort 0) -> ListF a b -> Either b (a * ListF a b);
 unfoldListF a b l =
-  ListF__rec a b (\ (_:ListF a b) -> Either b (a * ListF a b * #()))
-  (\ (x:b) -> Left b (a * ListF a b * #()) x)
-  (\ (x:a) (l:ListF a b) (_:Either b (a * ListF a b * #())) ->
-     Right b (a * ListF a b * #()) (x, l, ()))
+  ListF__rec a b (\ (_:ListF a b) -> Either b (a * ListF a b))
+  (\ (x:b) -> Left b (a * ListF a b) x)
+  (\ (x:a) (l:ListF a b) (_:Either b (a * ListF a b)) ->
+     Right b (a * ListF a b) (x, l))
   l;
 
-foldListF : (a b:sort 0) -> Either b (a * ListF a b * #()) -> ListF a b;
+foldListF : (a b:sort 0) -> Either b (a * ListF a b) -> ListF a b;
 foldListF a b =
-  either b (a * ListF a b * #()) (ListF a b)
+  either b (a * ListF a b) (ListF a b)
          (\ (x : b) -> NilF a b x)
-         (\ (tup : (a * ListF a b * #())) ->
-            ConsF a b tup.(1) tup.(2).(1));
+         (\ (tup : (a * ListF a b)) ->
+            ConsF a b tup.(1) tup.(2));
 
 getListF : (a b:sort 0) -> ListF a b -> b;
 getListF a b =

heapster-saw/examples/mbox.saw

@@ -43,7 +43,7 @@ heapster_define_perm env "boolean" " " "llvmptr 1" "exists x:bv 1.eq(llvmword(x)
 
 heapster_assume_fun env "llvm.objectsize.i64.p0i8" "().empty -o empty" "returnM #() ()";
 
-heapster_assume_fun env "__memcpy_chk" "(len:bv 64).arg0:byte_array<W,len>,arg1:byte_array<W,len>,arg2:eq(llvmword (len)) -o arg0:byte_array<W,len>,arg1:byte_array<W,len>" "\\ (len:Vec 64 Bool) (_ src : BVVec 64 len (Vec 8 Bool)) -> returnM (BVVec 64 len (Vec 8 Bool) * BVVec 64 len (Vec 8 Bool) * #()) (src, src, ())";
+heapster_assume_fun env "__memcpy_chk" "(len:bv 64).arg0:byte_array<W,len>,arg1:byte_array<W,len>,arg2:eq(llvmword (len)) -o arg0:byte_array<W,len>,arg1:byte_array<W,len>" "\\ (len:Vec 64 Bool) (_ src : BVVec 64 len (Vec 8 Bool)) -> returnM (BVVec 64 len (Vec 8 Bool) * BVVec 64 len (Vec 8 Bool)) (src, src)";
 
 
 //------------------------------------------------------------------------------

heapster-saw/examples/mbox.sawcore

@@ -31,20 +31,20 @@ Mbox__rec : (P : Mbox -> sort 0) ->
             (m:Mbox) -> P m;
 Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m;
 
-unfoldMbox : Mbox -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool) * #());
+unfoldMbox : Mbox -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool));
 unfoldMbox m =
-  Mbox__rec (\ (_:Mbox) -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool) * #()))
-  (Left #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool) * #()) ())
-  (\ (strt:Vec 64 Bool) (len:Vec 64 Bool) (m:Mbox) (_:Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool) * #())) (d:BVVec 64 bv64_128 (Vec 8 Bool)) ->
-     Right #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool) * #()) (strt, len, m, d, ()))
+  Mbox__rec (\ (_:Mbox) -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)))
+  (Left #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) ())
+  (\ (strt:Vec 64 Bool) (len:Vec 64 Bool) (m:Mbox) (_:Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool))) (d:BVVec 64 bv64_128 (Vec 8 Bool)) ->
+     Right #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) (strt, len, m, d))
   m;
 
-foldMbox : Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * (BVVec 64 bv64_128 (Vec 8 Bool)) * #()) -> Mbox;
+foldMbox : Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) -> Mbox;
 foldMbox =
-  either #() (Vec 64 Bool * Vec 64 Bool * Mbox * (BVVec 64 bv64_128 (Vec 8 Bool)) * #()) Mbox
+  either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) Mbox
          (\ (_:#()) -> Mbox_nil)
-         (\ (tup : (Vec 64 Bool * Vec 64 Bool * Mbox * (BVVec 64 bv64_128 (Vec 8 Bool)) * #())) ->
-            Mbox_cons tup.1 tup.2 tup.3 tup.4);
+         (\ (tup : (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool))) ->
+            Mbox_cons tup.1 tup.2 tup.3 tup.(2).(2).(2));
 
 {-
 getMbox : (a : sort 0) -> Mbox a -> a;

heapster-saw/examples/mbox_proofs.v

@@ -26,7 +26,7 @@ Definition unfoldMbox_nil :
   unfoldMbox Mbox_nil = Left _ _ tt :=
   reflexivity _.
 Definition unfoldMbox_cons strt len m d :
-  unfoldMbox (Mbox_cons strt len m d) = Right _ _ (strt, (len, (m, (d, tt)))) :=
+  unfoldMbox (Mbox_cons strt len m d) = Right _ _ (strt, (len, (m, d))) :=
   reflexivity _.
 
 Ltac Mbox_destruct m m' := destruct m as [| ?strt ?len m' ?d].
@@ -40,7 +40,7 @@ Lemma refinesM_either_unfoldMbox_nil_l {C} f g (P : CompM C) :
 Proof. eauto. Qed.
 
 Lemma refinesM_either_unfoldMbox_cons_l {C} strt len m d f g (P : CompM C) :
-  g (strt, (len, (m, (d, tt)))) |= P ->
+  g (strt, (len, (m, d))) |= P ->
   SAWCorePrelude.either _ _ _ f g (unfoldMbox (Mbox_cons strt len m d)) |= P.
 Proof. eauto. Qed.
 
@@ -196,9 +196,9 @@ Proof.
   (* Show Ltac Profile. Reset Ltac Profile. *)
 Time Qed.
 
-Definition mbox_detach_spec : Mbox -> Mbox * (Mbox * unit) :=
-  Mbox__rec _ (Mbox_nil, (Mbox_nil, tt))
-            (fun strt len next _ d => (next, (Mbox_cons strt len Mbox_nil d, tt))).
+Definition mbox_detach_spec : Mbox -> Mbox * Mbox :=
+  Mbox__rec _ (Mbox_nil, Mbox_nil)
+            (fun strt len next _ d => (next, (Mbox_cons strt len Mbox_nil d))).
 
 Lemma mbox_detach_spec_ref
   : refinesFun mbox_detach (fun x => returnM (mbox_detach_spec x)).
@@ -234,19 +234,19 @@ Definition mbox_len_spec : Mbox -> bitvector 64 :=
           (fun strt len m rec d => bvAdd 64 rec len).
 
 Lemma mbox_len_spec_ref
-  : refinesFun mbox_len (fun m => returnM (m, (mbox_len_spec m, tt))).
+  : refinesFun mbox_len (fun m => returnM (m, mbox_len_spec m)).
 Proof.
   unfold mbox_len, mbox_len__tuple_fun.
   prove_refinement_match_letRecM_l.
-  - exact (fun m1 rec m2 => returnM (transMbox m1 m2, (bvAdd 64 rec (mbox_len_spec m2), tt))).
+  - exact (fun m1 rec m2 => returnM (transMbox m1 m2, bvAdd 64 rec (mbox_len_spec m2))).
   unfold mbox_len_spec.
   (* Set Ltac Profiling. *)
   time "mbox_len_spec_ref" prove_refinement.
   (* Show Ltac Profile. Reset Ltac Profile. *)
   (* Most of the remaining cases are taken care of with just bvAdd_id_l and bvAdd_id_r *)
   all: try rewrite bvAdd_id_r; try rewrite bvAdd_id_l; try reflexivity.
   (* The remaining case just needs a few more rewrites *)
-  - do 2 f_equal.
+  - f_equal.
     rewrite bvAdd_assoc; f_equal.
     rewrite bvAdd_comm; reflexivity.
   - cbn; rewrite transMbox_Mbox_nil_r; reflexivity.
@@ -300,17 +300,17 @@ Definition conjSliceBVVec (strt len : bitvector 64) pf0 pf1 d0 d1 : BVVec 64 bv6
 (* Given a `start`, `len`, and `dat` of a single Mbox, return an mbox chain consisting of
    a single mbox with `id` 0,  the given `start` and `len`, and the given `dat` with the
    range 0 to `start` zeroed out. *)
-Definition mbox_copy_spec_cons strt len m d : CompM (Mbox * (Mbox * unit)) :=
+Definition mbox_copy_spec_cons strt len m d : CompM (Mbox * Mbox) :=
   assumingM (isBvslt 64 (intToBv 64 0) strt)
     (forallM (fun pf0 : isBvule 64 strt (intToBv 64 128) =>
       (forallM (fun pf1 : isBvule 64 len (bvSub 64 (intToBv 64 128) strt) =>
         returnM (Mbox_cons strt len m
                            (conjSliceBVVec strt len pf0 pf1 d d),
                 (Mbox_cons strt len Mbox_nil
-                           (conjSliceBVVec strt len pf0 pf1 empty_mbox_d d), tt)))))).
+                           (conjSliceBVVec strt len pf0 pf1 empty_mbox_d d))))))).
 
-Definition mbox_copy_spec : Mbox -> CompM (Mbox * (Mbox * unit)) :=
-  Mbox__rec (fun _ => CompM  (Mbox * (Mbox * unit))) (returnM (Mbox_nil, (Mbox_nil, tt)))
+Definition mbox_copy_spec : Mbox -> CompM (Mbox * Mbox) :=
+  Mbox__rec (fun _ => CompM  (Mbox * Mbox)) (returnM (Mbox_nil, Mbox_nil))
           (fun strt len m _ d => mbox_copy_spec_cons strt len m d).
 
 Lemma mbox_copy_spec_ref : refinesFun mbox_copy mbox_copy_spec.

heapster-saw/examples/memcpy.saw

@@ -3,7 +3,7 @@ env <- heapster_init_env_from_file "memcpy.sawcore" "memcpy.bc";
 
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
-heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, b:llvmblock 64, len:bv 64).arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), arg2:eq(llvmword(len))  -o  arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))" "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #() * #()) ((),(),())";
+heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, b:llvmblock 64, len:bv 64).arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), arg2:eq(llvmword(len))  -o  arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))" "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
 
 heapster_typecheck_fun env "copy_int" "().arg0:int64<> -o ret:int64<>";