Heapster bugfix to update IRT wrt recent changes

heapster-saw/examples/rust_data.rs

@@ -279,6 +279,23 @@ impl List<u64> {
     }
 }
 
+/* A linked list specialized to 64-bit elements */
+#[derive(Clone, Debug, PartialEq)]
+#[repr(C,u64)]
+pub enum List64 {
+    Nil64,
+    Cons64 (u64,Box<List64>)
+}
+
+/* Test if a List64 is empty */
+pub fn list64_is_empty (l: &List64) -> bool {
+    match l {
+        List64::Nil64 => true,
+        List64::Cons64 (_,_) => false
+    }
+}
+
+
 /* 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 {
@@ -288,6 +305,20 @@ pub fn hash_map_insert_gt_to_le (m: &mut HashMap<u64,u64>, x:u64, y:u64) -> () {
     }
 }
 
+/* A binary tree */
+pub enum BinTree<X> {
+    BinLeaf (X),
+    BinNode (Box<BinTree<X>>,Box<BinTree<X>>)
+}
+
+pub fn bintree_is_leaf (t: &BinTree<u64>) -> bool {
+    match *t {
+        BinTree::BinLeaf (_) => true,
+        BinTree::BinNode (_,_) => false
+    }
+}
+
+
 /* A tree whose internal nodes contain vectors of children */
 pub enum Tree<X> {
     Leaf (X),

heapster-saw/examples/rust_data.saw

@@ -34,6 +34,9 @@ heapster_define_rust_type env "pub enum Option<X> { None, Some (X) }";
 //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";
 heapster_define_rust_type env "pub enum List<X> { Nil, Cons (X,Box<List<X>>) }";
 
+// List64 type
+heapster_define_rust_type env "pub enum List64 { Nil64, Cons64 (u64,Box<List64>) }";
+
 // The String type
 heapster_define_llvmshape env "String" 64 "" "exsh cap:bv 64. ptrsh(arraysh(cap,1,[(8,int8<>)]));fieldsh(int64<>);fieldsh(eq(llvmword(cap)))";
 
@@ -56,6 +59,9 @@ heapster_define_opaque_llvmshape env "Vec" 64 "T:llvmshape 64" "24" "\\ (T:sort
 // 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)";
 
+// BinTree<X> type
+heapster_define_rust_type env "pub enum BinTree<X> { BinLeaf (X), BinNode (Box<BinTree<X>>,Box<BinTree<X>>) }";
+
 // Tree<X> type
 // FIXME: this does not work yet because Heapster cannot yet handle recursive types
 // where the type being defined is passed to an opaque or recursvie type
@@ -157,6 +163,10 @@ 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" "(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))";
 
+// list64_is_empty
+list64_is_empty_sym <- heapster_find_symbol env "15list64_is_empty";
+heapster_typecheck_fun_rename env list_is_empty_sym "list64_is_empty" "<'a> fn (l: &'a List64<>) -> bool";
+
 // StrStruct::new
 str_struct_new <- heapster_find_symbol env "9StrStruct3new";
 
@@ -166,6 +176,9 @@ str_struct_new <- heapster_find_symbol env "9StrStruct3new";
 // FIXME: this is the correct version, with the String shape
 heapster_typecheck_fun_rename env str_struct_new "str_struct_new" "(len:bv 64).arg0:memblock(W,0,24,emptysh), arg1:array(0,<len,*1,[(R,0,8) |-> int8<>]), arg2:eq(llvmword(len)) -o arg0:memblock(W,0,24,String<>)";
 
+bintree_is_leaf_sym <- heapster_find_symbol env "15bintree_is_leaf";
+heapster_typecheck_fun_rename env bintree_is_leaf_sym "bintree_is_leaf" "<'a> fn (t: &'a BinTree<u64>) -> bool";
+
 enum20_list_proj_sym <- heapster_find_symbol env "16enum20_list_proj";
 //heapster_typecheck_fun_rename env enum20_list_proj_sym "enum20_list_proj" "<'a> fn (x:&'a Enum20<List<u64>>) -> &'a List<u64>";
 

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

@@ -599,6 +599,9 @@ instance IRTDescs (ValuePerm a) where
       do x1 <- irtDesc p1 ixs1
          x2 <- irtDesc p2 ixs2
          irtCtor "Prelude.IRT_Either" [x1, x2]
+    ([nuMP| ValPerm_Exists p |], IRTVarsCons ix _)
+      | [nuMP| ValPerm_Eq _ |] <- mbMatch (mbCombine RL.typeCtxProxies p) ->
+        irtCtor "Prelude.IRT_varT" [natOpenTerm ix]
     ([nuMP| ValPerm_Exists p |], IRTVarsCons ix ixs') ->
       do let tp = mbBindingType p
          tp_trans <- tupleTypeTrans <$> translateClosed tp