Fix Heapster type-checking bugs for Rust

cabal.project

@@ -43,4 +43,4 @@ packages:
 source-repository-package
     type: git
     location: https://github.com/eddywestbrook/hobbits.git
-    tag: 20b6d18758312deaf6a544d474483e537d5f018f
+    tag: e2df7a85ea8dfebce2be8065afdca96cbaef12ae

heapster-saw/examples/_CoqProject

@@ -8,6 +8,8 @@ xor_swap_gen.v
 xor_swap_proofs.v
 xor_swap_rust_gen.v
 xor_swap_rust_proofs.v
+c_data_gen.v
+c_data_proofs.v
 string_set_gen.v
 string_set_proofs.v
 loops_gen.v

heapster-saw/examples/c_data.c

@@ -0,0 +1,33 @@
+#include <stdlib.h>
+#include <stdint.h>
+
+/* Increment the first byte pointed to by a 64-bit word pointer */
+void incr_u64_ptr_byte (uint64_t *x) {
+  uint8_t *x_byte = (uint8_t*)x;
+  (*x_byte)++;
+}
+
+typedef struct padded_struct {
+  uint64_t padded1;
+  uint8_t padded2;
+  uint64_t padded3;
+  uint8_t padded4;
+} padded_struct;
+
+/* Allocated a padded_struct */
+padded_struct *alloc_padded_struct (void) {
+  padded_struct *ret = malloc (sizeof(padded_struct));
+  ret->padded1 = 0;
+  ret->padded2 = 0;
+  ret->padded3 = 0;
+  ret->padded4 = 0;
+  return ret;
+}
+
+/* Increment all fields of a padded_struct */
+void padded_struct_incr_all (padded_struct *p) {
+  p->padded1++;
+  p->padded2++;
+  p->padded3++;
+  p->padded4++;
+}

heapster-saw/examples/c_data.saw

@@ -0,0 +1,53 @@
+
+enable_experimental;
+env <- heapster_init_env "c_data" "c_data.bc";
+
+/***
+ *** Type Definitions
+ ***/
+
+// Integer types
+heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))";
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+
+// padded_struct type
+heapster_define_llvmshape env "u64" 64 "" "fieldsh(int64<>)";
+
+heapster_define_llvmshape env "padded_struct" 64 ""
+  "fieldsh(int64<>);fieldsh(8,int8<>);fieldsh(56,true); \
+  \ fieldsh(int64<>);fieldsh(8,int8<>);fieldsh(56,true)";
+
+
+/***
+ *** Assumed Functions
+ ***/
+
+heapster_assume_fun env "malloc"
+  "(sz:bv 64). arg0:eq(llvmword(8*sz)) -o \
+             \ arg0:true, ret:array(W,0,<sz,*8,fieldsh(true))"
+  "\\ (sz:Vec 64 Bool) -> \
+    \ returnM (BVVec 64 sz #()) \
+            \ (genBVVec 64 sz #() (\\ (i:Vec 64 Bool) (_:is_bvult 64 i sz) -> ()))";
+
+
+/***
+ *** Type-Checked Functions
+ ***/
+
+// incr_u64_ptr_byte
+heapster_typecheck_fun env "incr_u64_ptr_byte"
+  "(). arg0:ptr((W,0) |-> int64<>) -o arg0:ptr((W,0) |-> int64<>)";
+
+// alloc_padded_struct
+heapster_typecheck_fun env "alloc_padded_struct"
+  "(). empty -o ret:memblock(W,0,32,padded_struct<>)";
+
+// padded_struct_incr_all
+heapster_typecheck_fun env "padded_struct_incr_all"
+  "(). arg0:memblock(W,0,32,padded_struct<>) -o arg0:memblock(W,0,32,padded_struct<>)";
+
+/***
+ *** Export to Coq
+ ***/
+
+heapster_export_coq env "c_data_gen.v";

heapster-saw/examples/c_data_proofs.v

@@ -0,0 +1,32 @@
+From Coq          Require Import Lists.List.
+From Coq          Require Import String.
+From Coq          Require Import Vectors.Vector.
+From CryptolToCoq Require Import SAWCoreScaffolding.
+From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
+From CryptolToCoq Require Import SAWCoreBitvectors.
+
+From CryptolToCoq Require Import SAWCorePrelude.
+From CryptolToCoq Require Import CompMExtra.
+
+Require Import Examples.c_data_gen.
+Import c_data.
+
+Import SAWCorePrelude.
+
+Lemma no_errors_incr_u64_ptr_byte :
+  refinesFun incr_u64_ptr_byte (fun _ => noErrorsSpec).
+  unfold incr_u64_ptr_byte, incr_u64_ptr_byte__tuple_fun, noErrorsSpec.
+  time "no_errors_incr_u64_ptr_byte" prove_refinement.
+Qed.
+
+Lemma no_errors_alloc_padded_struct :
+  refinesFun alloc_padded_struct noErrorsSpec.
+  unfold alloc_padded_struct, alloc_padded_struct__tuple_fun, noErrorsSpec, malloc.
+  time "no_errors_alloc_padded_struct" prove_refinement.
+Qed.
+
+Lemma no_errors_padded_struct_incr_all :
+  refinesFun padded_struct_incr_all (fun _ => noErrorsSpec).
+  unfold padded_struct_incr_all, padded_struct_incr_all__tuple_fun, noErrorsSpec.
+  time "no_errors_padded_struct_incr_all" prove_refinement.
+Qed.

heapster-saw/examples/rust_data.rs

@@ -323,6 +323,17 @@ pub enum List64 {
     Cons64 (u64,Box<List64>)
 }
 
+pub fn box_list64_clone<'a>(x:&'a Box<List64>) -> Box<List64> {
+    return x.clone();
+}
+
+pub fn list64_clone<'a>(x:&'a List64) -> List64 {
+    match &x {
+        List64::Nil64 => List64::Nil64,
+        List64::Cons64(h,t) => List64::Cons64(*h,box_list64_clone(t)),
+    }
+}
+
 /* Test if a List64 is empty */
 pub fn list64_is_empty (l: &List64) -> bool {
     match l {
@@ -516,3 +527,31 @@ pub fn list20_head<'a> (x:&'a List20<List<u64>>) -> &'a List<u64> {
       List20::List20_19(l,_) => l,
   }
 }
+
+impl Clone for List20<u64> {
+    fn clone<'a>(&'a self) -> Self {
+        match &self {
+            List20::List20Head(b) => List20::List20Head(*b),
+            List20::List20_0(h,t) => List20::List20_0(*h,t.clone()),
+            List20::List20_1(h,t) => List20::List20_1(*h,t.clone()),
+            List20::List20_2(h,t) => List20::List20_2(*h,t.clone()),
+            List20::List20_3(h,t) => List20::List20_3(*h,t.clone()),
+            List20::List20_4(h,t) => List20::List20_4(*h,t.clone()),
+            List20::List20_5(h,t) => List20::List20_5(*h,t.clone()),
+            List20::List20_6(h,t) => List20::List20_6(*h,t.clone()),
+            List20::List20_7(h,t) => List20::List20_7(*h,t.clone()),
+            List20::List20_8(h,t) => List20::List20_8(*h,t.clone()),
+            List20::List20_9(h,t) => List20::List20_9(*h,t.clone()),
+            List20::List20_10(h,t) => List20::List20_10(*h,t.clone()),
+            List20::List20_11(h,t) => List20::List20_11(*h,t.clone()),
+            List20::List20_12(h,t) => List20::List20_12(*h,t.clone()),
+            List20::List20_13(h,t) => List20::List20_13(*h,t.clone()),
+            List20::List20_14(h,t) => List20::List20_14(*h,t.clone()),
+            List20::List20_15(h,t) => List20::List20_15(*h,t.clone()),
+            List20::List20_16(h,t) => List20::List20_16(*h,t.clone()),
+            List20::List20_17(h,t) => List20::List20_17(*h,t.clone()),
+            List20::List20_18(h,t) => List20::List20_18(*h,t.clone()),
+            List20::List20_19(h,t) => List20::List20_19(*h,t.clone()),
+        }
+    }
+}

heapster-saw/examples/rust_data.saw

@@ -495,6 +495,16 @@ 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";
 
+// box_list64_clone
+box_list64_clone_sym <- heapster_find_symbol env "16box_list64_clone";
+heapster_assume_fun_rename_prim env box_list64_clone_sym "box_list64_clone"
+  "<'a> fn(x:&'a Box<List64>) -> Box<List64>";
+
+// list64_clone
+list64_clone_sym <- heapster_find_symbol env "12list64_clone";
+heapster_typecheck_fun_rename env list64_clone_sym "list64_clone"
+  "<'a> fn (x:&'a List64) -> List64";
+
 hash_map_insert_gt_to_le_sym <- heapster_find_symbol env "hash_map_insert_gt_to_le";
 heapster_typecheck_fun_rename
   env hash_map_insert_gt_to_le_sym
@@ -518,10 +528,16 @@ list10_head_sym <- heapster_find_symbol env "11list10_head";
 //heapster_typecheck_fun_rename env list10_head_sym "list10_head"
   "<'a> fn (x:&'a List10<List<u64>>) -> &'a List<u64>";
 
+list20_u64_clone_sym <- heapster_find_symbol env
+  "List20$LT$u64$GT$$u20$as$u20$core..clone..Clone$GT$5clone";
+heapster_typecheck_fun_rename env list20_u64_clone_sym "list20_u64_clone"
+  "<'a> fn (&'a List20<u64>) -> List20<u64>";
+
+/*
 list20_head_sym <- heapster_find_symbol env "11list20_head";
 heapster_typecheck_fun_rename env list20_head_sym "list20_head"
   "<'a> fn (x:&'a List20<List<u64>>) -> &'a List<u64>";
-
+*/
 
 /***
  *** Export to Coq

heapster-saw/examples/rust_lifetimes.rs

@@ -30,3 +30,30 @@ pub fn use_mux_mut_refs2 <'a,'b> (x1: &'a mut u64, x2: &'b mut u64) -> u64 {
     *x1 = *x1 + *x2;
     return *x1;
 }
+
+pub fn mux3_mut_refs_u64 <'a> (x1: &'a mut u64, x2: &'a mut u64,
+                               x3: &'a mut u64, i: u64) -> &'a mut u64 {
+    if i == 0 {
+        return x1;
+    } else if i == 1 {
+        return x2;
+    } else {
+        return x3;
+    }
+}
+
+pub fn use_mux3_mut_refs <'a,'b,'c> (x1: &'a mut u64, x2: &'b mut u64,
+                                     x3: &'c mut u64) -> u64 {
+    let r = mux3_mut_refs_u64 (x1,x2,x3,2);
+    *r = *r + 1;
+    *x1 = *x1 + *x2 + *x3;
+    return *x1;
+}
+
+pub fn use_mux3_mut_refs_onel <'a> (x1: &'a mut u64, x2: &'a mut u64,
+                                    x3: &'a mut u64) -> u64 {
+    let r = mux3_mut_refs_u64 (x1,x2,x3,2);
+    *r = *r + 1;
+    *x1 = *x1 + *x2 + *x3;
+    return *x1;
+}

heapster-saw/examples/rust_lifetimes.saw

@@ -13,6 +13,9 @@ heapster_define_perm env "int1" " " "llvmptr 1" "exists x:bv 1.eq(llvmword(x))";
 // Integer shapes
 heapster_define_llvmshape env "u64" 64 "" "fieldsh(int64<>)";
 
+// bool type
+heapster_define_llvmshape env "bool" 64 "" "fieldsh(1,int1<>)";
+
 
 /***
  *** Assumed Functions
@@ -43,19 +46,46 @@ heapster_assume_fun env "llvm.expect.i1"
 // mux_mut_refs_u64
 mux_mut_refs_u64_sym <- heapster_find_symbol env "16mux_mut_refs_u64";
 heapster_typecheck_fun_rename env mux_mut_refs_u64_sym "mux_mut_refs_u64"
-  "(l:lifetime, l1:lifetime ,l2:lifetime). \
-  \ l:lowned(arg0:[l]memblock(R,0,8,u64<>), arg1:[l]memblock(R,0,8,u64<>) -o \
-  \          arg0:[l1]memblock(W,0,8,u64<>), arg1:[l2]memblock(W,0,8,u64<>)), \
-  \ arg0:[l]memblock(W,0,8,u64<>), arg1:[l]memblock(W,0,8,u64<>), arg2:int1<> -o \
-  \ l:lowned (ret:[l]memblock(R,0,8,u64<>) -o \
-  \ arg0:[l1]memblock(W,0,8,u64<>), arg1:[l2]memblock(W,0,8,u64<>)), \
-  \ ret:[l]memblock(W,0,8,u64<>)";
+  "<'a> fn (x1: &'a mut u64, x2: &'a mut u64, b: bool) -> &'a mut u64";
+  // "(l:lifetime, l1:lifetime ,l2:lifetime). \
+  // \ l:lowned(arg0:[l]memblock(R,0,8,u64<>), arg1:[l]memblock(R,0,8,u64<>) -o \
+  // \          arg0:[l1]memblock(W,0,8,u64<>), arg1:[l2]memblock(W,0,8,u64<>)), \
+  // \ arg0:[l]memblock(W,0,8,u64<>), arg1:[l]memblock(W,0,8,u64<>), arg2:int1<> -o \
+  // \ l:lowned (ret:[l]memblock(R,0,8,u64<>) -o \
+  // \ arg0:[l1]memblock(W,0,8,u64<>), arg1:[l2]memblock(W,0,8,u64<>)), \
+  // \ ret:[l]memblock(W,0,8,u64<>)";
+
+// mux_mut_refs_poly
+mux_mut_refs_poly_u64_sym <- heapster_find_symbol env "17mux_mut_refs_poly";
+heapster_typecheck_fun_rename env mux_mut_refs_poly_u64_sym "mux_mut_refs_poly_u64"
+  "<'a> fn (x1: &'a mut u64, x2: &'a mut u64, b: bool) -> &'a mut u64";
 
 // use_mux_mut_refs
 use_mux_mut_refs_sym <- heapster_find_symbol env "16use_mux_mut_refs";
 heapster_typecheck_fun_rename env use_mux_mut_refs_sym "use_mux_mut_refs"
   "(). empty -o ret:int64<>";
 
+// use_mux_mut_refs2
+use_mux_mut_refs2_sym <- heapster_find_symbol env "17use_mux_mut_refs2";
+heapster_typecheck_fun_rename env use_mux_mut_refs2_sym "use_mux_mut_refs2"
+  "<'a,'b> fn (x1: &'a mut u64, x2: &'b mut u64) -> u64";
+
+// mux3_mut_refs_u64
+mux3_mut_refs_u64_sym <- heapster_find_symbol env "17mux3_mut_refs_u64";
+heapster_typecheck_fun_rename env mux3_mut_refs_u64_sym "mux3_mut_refs_u64"
+  "<'a> fn (x1: &'a mut u64, x2: &'a mut u64, \
+          \ x3: &'a mut u64, i: u64) -> &'a mut u64";
+
+// use_mux3_mut_refs
+use_mux3_mut_refs_sym <- heapster_find_symbol env "17use_mux3_mut_refs";
+heapster_typecheck_fun_rename env use_mux3_mut_refs_sym "use_mux3_mut_refs"
+  "<'a,'b,'c> fn (x1: &'a mut u64, x2: &'b mut u64, x3: &'c mut u64) -> u64";
+
+// use_mux3_mut_refs_onel
+use_mux3_mut_refs_onel_sym <- heapster_find_symbol env "22use_mux3_mut_refs_onel";
+heapster_typecheck_fun_rename env use_mux3_mut_refs_onel_sym
+  "use_mux3_mut_refs_onel"
+  "<'a> fn (x1: &'a mut u64, x2: &'a mut u64, x3: &'a mut u64) -> u64";
 
 /***
  *** Export to Coq