Merge pull request #2030 from GaloisInc/heapster/fix-reach-perms

Fix Heapster reachability permissions examples

heapster-saw/examples/clearbufs.saw

@@ -5,7 +5,6 @@ env <- heapster_init_env_from_file "clearbufs.sawcore" "clearbufs.bc";
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
 // FIXME: get reachability perms working again!
-/*
 heapster_define_reachability_perm env "Bufs"
   "x:llvmptr 64" "llvmptr 64"
   "eq(x) or exists len:(bv 64).ptr((W,0) |-> Bufs) * \
@@ -22,6 +21,5 @@ heapster_block_entry_hint env "clearbufs" 3
 
 heapster_typecheck_fun env "clearbufs"
   "(). arg0:Bufs<llvmword(0)> -o arg0:Bufs<llvmword(0)>";
-*/
 
 heapster_export_coq env "clearbufs_gen.v";

heapster-saw/examples/iter_linked_list.saw

@@ -4,8 +4,6 @@ env <- heapster_init_env_from_file "iter_linked_list.sawcore" "iter_linked_list.
 // Integer types
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
-// FIXME: get reachability perms working again!
-/*
 heapster_define_reachability_perm env "ListF"
   "X:perm(llvmptr 64), l:lifetime, rw:rwmodality, y:llvmptr 64"
   "llvmptr 64"
@@ -46,6 +44,5 @@ heapster_block_entry_hint env "length" 3
 heapster_typecheck_fun env "length"
   "(). arg0:ListF<int64<>,always,W,llvmword(0)> -o \
      \ arg0:true, ret:int64<>";
-*/
 
 heapster_export_coq env "iter_linked_list_gen.v";

heapster-saw/examples/iter_linked_list.sawcore

@@ -3,6 +3,24 @@ module iter_linked_list where
 
 import SpecM;
 
+-- Type description for the List type over a single free variable for a type
+-- description that describes the elements
+ListDesc : TpDesc;
+ListDesc =
+    (Tp_Sum
+       Tp_Unit
+       (Tp_Pair
+          (varKindExpr Kind_Tp 1)
+          (varKindExpr Kind_Tp 0)));
+
+-- The type described by ListDesc
+ListTpF : TpDesc -> sort 0;
+ListTpF T = indElem (unfoldIndTpDesc (envConsElem Kind_Tp T nilTpEnv) ListDesc);
+
+primitive appendList : (T:TpDesc) -> ListTpF T -> ListTpF T -> ListTpF T;
+
+-- FIXME: get the following definitions working
+{-
 List_def : (a:sort 0) -> sort 0;
 List_def a = List a;
 
@@ -61,3 +79,4 @@ transListF a b l1 l2 =
   (\ (_:#()) -> l2)
   (\ (x:a) (_:ListF a #()) (rec:ListF a b) -> ConsF a b x rec)
   l1;
+-}

heapster-saw/examples/mbox.saw

@@ -28,7 +28,6 @@ heapster_define_perm env "aes_sw_ctx"
   "array(rw1, 0, <240, *1, fieldsh (int64<>)) * ptr((rw2, 1920) |-> int64<>)";
 
 // FIXME: get reachability perms working again!
-/*
 heapster_define_reachability_perm env "mbox"
   "rw:rwmodality, x:llvmptr 64"
   "llvmptr 64"
@@ -275,7 +274,7 @@ heapster_typecheck_fun env "mbox_randomize"
 heapster_typecheck_fun env "mbox_drop"
   "(). arg0:mbox<W,llvmword(0)>, arg1:int64<> -o \
      \ arg0:mbox<W,llvmword(0)>, arg1:true";
-*/
+
 
 //------------------------------------------------------------------------------
 // Export to coq for verification

heapster-saw/examples/mbox.sawcore

@@ -17,15 +17,32 @@ bv64_128 : Vec 64 Bool;
 bv64_128 = [False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,True,False,False,False,False,False,False,False];
 
 
-data Mbox : sort 0 where {
-  Mbox_nil : Mbox;
-  Mbox_cons : Vec 64 Bool -> Vec 64 Bool -> Mbox -> BVVec 64 bv64_128 (Vec 8 Bool) -> Mbox;
+-- An inductive type formulation of the Mbox type; this is just for
+-- documentation purposes, and isn't used in the below
+data Mbox_Ind : sort 0 where {
+  Mbox_Ind_nil : Mbox_Ind;
+  Mbox_Ind_cons : Vec 64 Bool -> Vec 64 Bool -> Mbox_Ind ->
+                  BVVec 64 bv64_128 (Vec 8 Bool) -> Mbox_Ind;
 }
 
--- A definition for the Mbox datatype; currently needed as a workaround in Heapster
-Mbox_def : sort 0;
-Mbox_def = Mbox;
+-- Type description for the Mbox type, which is equivalent to Mbox_Ind
+MboxDesc : TpDesc;
+MboxDesc =
+    (Tp_Sum
+       Tp_Unit
+       (Tp_Pair (Tp_bitvector 64)
+          (Tp_Pair (Tp_bitvector 64)
+             (Tp_Pair (varKindExpr Kind_Tp 0)
+                (Tp_BVVec 64 (TpExpr_Const (Kind_bv 64) bv64_128) (Tp_bitvector 8))))));
 
+-- The type described by MboxDesc
+Mbox : sort 0;
+Mbox = indElem (unfoldIndTpDesc nilTpEnv MboxDesc);
+
+primitive transMbox : Mbox -> Mbox -> Mbox;
+
+-- FIXME: figure out how to write some of these using the TpDesc version of Mbox
+{-
 Mbox__rec : (P : Mbox -> sort 0) ->
             (P Mbox_nil) ->
             ((strt:Vec 64 Bool) -> (len:Vec 64 Bool) -> (m:Mbox) -> P m -> (d:BVVec 64 bv64_128 (Vec 8 Bool)) -> P (Mbox_cons strt len m d)) ->
@@ -68,11 +85,17 @@ transMbox m1 m2 =
   m2
   (\ (strt : Vec 64 Bool) (len : Vec 64 Bool) (_ : Mbox) (rec : Mbox) (vec : BVVec 64 bv64_128 (Vec 8 Bool)) -> Mbox_cons strt len rec vec)
   m1;
+-}
 
+{-
 mboxNewSpec : SpecM VoidEv (Mbox);
 mboxNewSpec =
   retS VoidEv Mbox
        (Mbox_cons (bvNat 64 0) (bvNat 64 0) Mbox_nil (genBVVec 64 bv64_128 (Vec 8 Bool) (\ (i:Vec 64 Bool) (_:is_bvult 64 i bv64_128) -> (bvNat 8 0))));
+-}
+
+primitive
+mboxNewSpec : SpecM VoidEv Mbox;
 
 mboxFreeSpec : BVVec 64 bv64_128 (Vec 8 Bool) ->
                SpecM VoidEv (Vec 32 Bool);

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

@@ -801,7 +801,7 @@ sigmaElimTransM x tp_l tp_r_mF _tp_ret_m f sigma =
        sigma
        (\ts -> let (ts_l, ts_r) = splitAt (length (typeTransTypes tp_l)) ts
                    trL = typeTransF tp_l ts_l
-                   tp_r = tp_r_f ts_l in
+                   tp_r = tupleTypeTrans $ tp_r_f ts_l in
                flip runTransM info $ f trL (typeTransF tp_r ts_r))