Heapster array field implications (#1459)

* fixed the IRT description generation to match the recent change that made the translation of bitvector permissions to just be bitvectors

* updated xor_swap_rust example to use the Rust type in the SAW script

* added a case to the Rust to Heapster translator to handle function types with no return value

* whoops, forgot to update the bitcode file for xor_swap_rust

* bugfix in the Rust to Heapster translator: empty return types need to be converted to unit, not to the empty struct

* tweaked the error message for when Rust types do not translate correctly to the expected LLVM type

* started adding support for string literals by moving all creation of a HeapsterEnv into a single function which iterates through the globals and adds those it can handle

* added a formatting example in Rust, and started defining the necessary types for it

* started trying to figure out how Rust stores string literals in its generated LLVM files

* fixed the prtty-printing for constant values

* changed TrueEnum::fmt to use the fmt method rather than the write! macro

* whoops, changed the fmt method for TrueEnum back to using the write! macro, because that seems to be the proper way to do things

* whoops, forgot to add the repr(u64) pragma to the TrueEnum type

* added a type-checking command for TrueEnum::fmt

* moved some OpenTerm operators from SAWTranslation.hs to OpenTerm.hs

* added llvmReadBlockOfShape

* more work trying to translate globals

* got string literals translated, but now there is some translation bug...

* whoops, translating a shape always yields exactly one term

* added helper function exprLLVMTypeBytes

* added support for Rust slice types

* whoops, combined the two cases for translating shared vs mutable references into one

* updated funPerm3FromArgLayout to handle layouts with existential permissions

* updated the rust_data example to use string literals

* added mapM and mapBVVecM

* added support for proving array permissions from other array permissions with different fields using the SImpl_LLVMArrayContents rule; to get the translation of the SImpl_LLVMArrayContents to work correctly, I had to change local implications to not use strict tuples, which in turn required changing the translation of lowned permissions (which are themselves local implications) to not use strict tuples as well

* added more definitions to the arrays example now that the implication prover can map array permission contents

* moved the LLVM globals code to a new file LLVMGlobalConst.hs

* fixed the translation of LLVM array constants to generate SAW core BVVecs instead of SAW core Vecs

* regenerated Coq files for saw-core-coq

* added support for the Crucible BVZext and BVTrunc instructions, and fixed up that for BVSext

* added heapster_init_env_debug and heapster_init_env_from_file_debug commands

* small tweaks to rust_data.saw to get it to work

* added another formatting example that we cannot handle yet...

* RecurseFlag to Permissions.hs; added requireNamedPerm

* widening now unfolds defined and recursive permissions

* whoops, forgot to insert a bindM into the translation of SImpl_LLVMArrayContents

* removed the old gen_block_perms hints that are no longer used anyway from arrays.saw

* changed tupleTypeTrans to no longer having the trailing unit type on tuples of 2 or more types; updated foldList and unfoldList in the SAW core Prelude to fit this new approach; regenerated the resulting Coq files

* small tweak to the expression type-checker to type-check the bodies of existential shapes as arbitrary expressions

* expanded the translation of Rust slices to allow multiple fields

* updated mbox proof script to work with the recent changes, though not all the mbox proofs work...

* started updating the mbox proofs, but I got stuck...

* moved formatting-related types in the rust_data example to their own section

* finished updating mbox proofs

* updated examples to match the change to the SAW translation

* updated the IRT translation to match the updates to the SAW translation

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<>";