Merge pull request #1574 from GaloisInc/heapster/more-rust-bugfixes

Heapster: more rust bugfixes

heapster-saw/examples/c_data.c

@@ -1,5 +1,6 @@
 #include <stdlib.h>
 #include <stdint.h>
+#include <stdio.h>
 
 /* Increment the first byte pointed to by a 64-bit word pointer */
 void incr_u64_ptr_byte (uint64_t *x) {
@@ -31,3 +32,14 @@ void padded_struct_incr_all (padded_struct *p) {
   p->padded3++;
   p->padded4++;
 }
+
+/* Test endianness by reading the first byte of a word */
+int64_t is_little_endian () {
+  int64_t x = 1;
+  int8_t is_le = *(int8_t*)(&x);
+  return is_le;
+}
+
+int main (int argc, char **argv) {
+  printf ("Little endian test: %lli\n", is_little_endian());
+}

heapster-saw/examples/c_data.saw

@@ -46,6 +46,10 @@ heapster_typecheck_fun env "alloc_padded_struct"
 heapster_typecheck_fun env "padded_struct_incr_all"
   "(). arg0:memblock(W,0,32,padded_struct<>) -o arg0:memblock(W,0,32,padded_struct<>)";
 
+// is_little_endian
+heapster_typecheck_fun env "is_little_endian"
+  "(). empty -o ret:int64<>";
+
 /***
  *** Export to Coq
  ***/

heapster-saw/examples/memcpy.saw

@@ -7,9 +7,9 @@ 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)), \
+  \ arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(len,b)), \
   \ arg2:eq(llvmword(len)) -o \
-  \ arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))"
+  \ arg0:[l1]memblock(W,0,len,eqsh(len,b)), arg1:[l2]memblock(rw,0,len,eqsh(len,b))"
   "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
 
 

heapster-saw/examples/rust_data.rs

@@ -47,6 +47,10 @@ pub extern fn mk_two_values_extern (x1:u32,x2:u32) -> TwoValues {
     TwoValues(x1,x2)
 }
 
+pub fn mk_two_values_opt (x1:u32,x2:u32) -> Option<TwoValues> {
+    Some(TwoValues(x1,x2))
+}
+
 pub fn two_values_proj1 (x:TwoValues) -> u32 {
     match x {
         TwoValues(x1,_) => x1
@@ -122,6 +126,27 @@ pub extern fn mk_five_values_extern (x1:u32,x2:u32,x3:u32,x4:u32,x5:u32)
     FiveValues(x1,x2,x3,x4,x5)
 }
 
+pub fn mk_five_values_opt (x1:u32,x2:u32,x3:u32,x4:u32,x5:u32) -> Option<FiveValues> {
+    Some(FiveValues(x1,x2,x3,x4,x5))
+}
+
+pub fn proj_five_values (i:u64, fvs:FiveValues) -> u32 {
+    match fvs {
+        FiveValues(x0,x1,x2,x3,x4) =>
+            match i {
+                0 => x0,
+                1 => x1,
+                2 => x2,
+                3 => x3,
+                _ => x4
+            }
+    }
+}
+
+pub fn mk_proj0_five_values (x1:u32,x2:u32,x3:u32,x4:u32,x5:u32) -> u32 {
+    proj_five_values (0, mk_five_values (x1,x2,x3,x4,x5))
+}
+
 
 /* Test if a Result is Ok or Err */
 pub fn test_result <'a> (r:&'a Result<u64,u64>) -> bool {
@@ -346,6 +371,36 @@ pub fn list64_is_empty (l: &List64) -> bool {
     }
 }
 
+/* Sum the elements of a List64 */
+pub fn list64_sum(l:&List64) -> u64 {
+    match l {
+        List64::Nil64 => 0,
+        List64::Cons64 (x,rest) => x + list64_sum (rest),
+    }
+}
+
+/* Build a HashMap with a String key already mapped to a list */
+pub fn hash_map_for_string_and_list64 (str:String,
+                                       l:List64) -> HashMap<String,List64> {
+    let mut map = HashMap::new();
+    map.insert (str, l);
+    return map;
+}
+
+pub fn opt_hash_map_for_string_and_list64 (str:String,
+                                           l:List64) -> Option<HashMap<String,List64>> {
+    Some(hash_map_for_string_and_list64 (str,l))
+}
+
+/* Sum the List64s in a HashMap */
+pub fn sum_hash_map_string_list64 (map:&HashMap<String,List64>) -> u64 {
+    let mut ret:u64 = 0;
+    for (_,l) in map.iter() {
+        ret += list64_sum (l);
+    }
+    return ret;
+}
+
 /* 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 {

heapster-saw/examples/rust_data.saw

@@ -71,6 +71,11 @@ heapster_define_rust_type env "pub enum List<X> { Nil, Cons (X,Box<List<X>>) }";
 // instead just make Void an opaque type
 heapster_define_opaque_llvmshape env "Void" 64 "" "64" "#()";
 
+ // Location type from std::panic
+heapster_define_llvmshape env "panic::Location" 64 ""
+  "exsh len:bv 64.ptrsh(arraysh(<len,*1,fieldsh(8,int8<>))); \
+                \ fieldsh(eq(llvmword(len))); u32<>; u32<>";
+
 // List64 type
 heapster_define_rust_type env "pub enum List64 { Nil64, Cons64 (u64,Box<List64>) }";
 
@@ -132,7 +137,7 @@ heapster_define_rust_type env
 // List20 type
 heapster_define_rust_type env
   "pub enum List20<X> { \
-  \ List20_Head(X,Box<List20<X>>), List20_0(X,Box<List20<X>>), \
+  \ List20Head(X), List20_0(X,Box<List20<X>>), \
   \ List20_1(X,Box<List20<X>>), List20_2(X,Box<List20<X>>), \
   \ List20_3(X,Box<List20<X>>), List20_4(X,Box<List20<X>>), \
   \ List20_5(X,Box<List20<X>>), List20_6(X,Box<List20<X>>), \
@@ -240,17 +245,30 @@ heapster_assume_fun env "llvm.expect.i1"
 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)), \
+  \ arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(len,b)), \
   \ arg2:eq(llvmword(len)) -o \
-  \ arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))"
+  \ arg0:[l1]memblock(W,0,len,eqsh(len,b)), arg1:[l2]memblock(rw,0,len,eqsh(len,b))"
   "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
 
+// Box<List20<u64>>::clone
+box_list20_u64_clone_sym <- heapster_find_symbol_with_type env
+  "alloc..boxed..Box$LT$T$GT$$u20$as$u20$core..clone..Clone$GT$5clone"
+  "%\"List20<u64>\"*(%\"List20<u64>\"**)";
+heapster_assume_fun_rename_prim env box_list20_u64_clone_sym "box_list20_u64_clone"
+  "<'a> fn(x:&'a Box<List20<u64>>) -> Box<List20<u64>>";
+
 // <str as alloc::string::ToString>::to_string
 to_string_str <- heapster_find_symbol env
     "$LT$str$u20$as$u20$alloc..string..ToString$GT$9to_string";
 heapster_assume_fun_rename_prim env to_string_str "to_string_str"
   "<'a> fn (&'a str) -> String";
 
+// core::panicking::panic
+panicking_panic_sym <- heapster_find_symbol env "9panicking5panic";
+heapster_assume_fun_rename_prim env panicking_panic_sym "panicking_panic"
+  "<'a, 'b> fn (&'a str, &'b panic::Location) -> !";
+// FIXME: the above should use the 'static lifetime, which needs Heapster support
+
 // NOTE: this is the more incorrect version, with no lifetime argument and no shapes
 //heapster_assume_fun_rename env to_string_str "to_string_str"
 //  "(len:bv 64). arg0:memblock(W,0,24,emptysh),
@@ -291,8 +309,11 @@ heapster_assume_fun_rename_prim env to_string_str "to_string_str"
 
 // HashMap::insert
 // FIXME: we currently pretend this always returns None
-hashmap_u64_u64_insert_sym <- heapster_find_symbol env
-  "std11collections4hash3map24HashMap$LT$K$C$V$C$S$GT$6insert";
+hashmap_u64_u64_insert_sym <- heapster_find_symbol_with_type env
+  "std11collections4hash3map24HashMap$LT$K$C$V$C$S$GT$6insert"
+  "{ i64,\
+\  i64 }(%\"std::collections::hash::map::HashMap<u64, u64, std::collections::hash::map::RandomState>\"*,\
+\        i64, i64)";
 heapster_assume_fun_rename_prim env hashmap_u64_u64_insert_sym "hashmap_u64_u64_insert"
   "<'a> fn (&'a mut HashMap<u64,u64>,u64,u64) -> Option<u64>";
 //heapster_assume_fun_rename env hashmap_u64_u64_insert_sym "hashmap_u64_u64_insert"
@@ -306,6 +327,13 @@ heapster_assume_fun_rename_prim env hashmap_u64_u64_insert_sym "hashmap_u64_u64_
 //    \                                 (Cons (Vec 64 Bool * Vec 64 Bool) (k,v) h, ())), \
 //    \          Left #() (Vec 64 Bool) (), ())";
 
+hashmap_String_List64_insert_sym <- heapster_find_symbol_with_type env
+  "std11collections4hash3map24HashMap$LT$K$C$V$C$S$GT$6insert"
+  "void(%\"core::option::Option<List64>\"*,\
+\     %\"std::collections::hash::map::HashMap<alloc::string::String, List64, std::collections::hash::map::RandomState>\"*,\
+\     %\"alloc::string::String\"*, %List64*)";
+// FIXME: assume hashmap_String_List64_insert_sym
+
 // String::deref
 string_deref <- heapster_find_trait_method_symbol env
   "core::ops::deref::Deref::deref<String>";
@@ -420,6 +448,21 @@ mk_two_values_sym <- heapster_find_symbol env "13mk_two_values";
 heapster_typecheck_fun_rename env mk_two_values_sym "mk_two_values" "<> fn (u32,u32) -> TwoValues";
 */
 
+// mk_five_values
+mk_five_values_sym <- heapster_find_symbol env "14mk_five_values";
+heapster_typecheck_fun_rename env mk_five_values_sym "mk_five_values"
+  "<> fn (x1:u32,x2:u32,x3:u32,x4:u32,x5:u32) -> FiveValues";
+
+// proj_five_values
+proj_five_values_sym <- heapster_find_symbol env "16proj_five_values";
+heapster_typecheck_fun_rename env proj_five_values_sym "proj_five_values"
+  "<> fn (i:u64, fvs:FiveValues) -> u32";
+
+// mk_proj0_five_values
+mk_proj0_five_values_sym <- heapster_find_symbol env "20mk_proj0_five_values";
+heapster_typecheck_fun_rename env mk_proj0_five_values_sym "mk_proj0_five_values"
+  "<> fn (x1:u32,x2:u32,x3:u32,x4:u32,x5:u32) -> u32";
+
 // ref_sum
 ref_sum_sym <- heapster_find_symbol env "7ref_sum";
 heapster_typecheck_fun_rename env ref_sum_sym "ref_sum"

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

@@ -155,6 +155,7 @@ instance ContainsIRTRecName (AtomicPerm a) where
   containsIRTRecName n (Perm_LLVMFrame fperm) =
     containsIRTRecName n (map fst fperm)
   containsIRTRecName _ (Perm_LOwned _ _ _) = False
+  containsIRTRecName _ (Perm_LOwnedSimple _) = False
   containsIRTRecName _ (Perm_LCurrent _) = False
   containsIRTRecName _ Perm_LFinished = False
   containsIRTRecName n (Perm_Struct ps) = containsIRTRecName n ps
@@ -415,6 +416,8 @@ instance IRTTyVars (AtomicPerm a) where
     [nuMP| Perm_LLVMFrame _ |] -> return ([], IRTVarsNil)
     [nuMP| Perm_LOwned _ _ _ |] ->
       throwError "lowned permission in an IRT definition!"
+    [nuMP| Perm_LOwnedSimple _ |] ->
+      throwError "lowned permission in an IRT definition!"
     [nuMP| Perm_LCurrent _ |] -> return ([], IRTVarsNil)
     [nuMP| Perm_LFinished |] -> return ([], IRTVarsNil)
     [nuMP| Perm_Struct ps |] -> irtTyVars ps
@@ -457,7 +460,7 @@ instance IRTTyVars (PermExpr (LLVMShapeType w)) where
                   _ -> do sh' <- irtTSubstExt mb_sh
                           let sh_trans = transTupleTerm <$> translate sh'
                           return ([sh_trans], IRTVar ())
-    [nuMP| PExpr_EqShape _ |] -> return ([], IRTVarsNil)
+    [nuMP| PExpr_EqShape _ _ |] -> return ([], IRTVarsNil)
     [nuMP| PExpr_PtrShape _ _ sh |] -> irtTyVars sh
     [nuMP| PExpr_FieldShape fsh |] -> irtTyVars fsh
     [nuMP| PExpr_ArrayShape _ _ sh |] -> irtTyVars sh
@@ -663,6 +666,8 @@ instance IRTDescs (AtomicPerm a) where
     ([nuMP| Perm_LLVMFrame _ |], _) -> return []
     ([nuMP| Perm_LOwned _ _ _ |], _) ->
       error "lowned permission made it to IRTDesc translation"
+    ([nuMP| Perm_LOwnedSimple _ |], _) ->
+      error "lowned permission made it to IRTDesc translation"
     ([nuMP| Perm_LCurrent _ |], _) -> return []
     ([nuMP| Perm_LFinished |], _) -> return []
     ([nuMP| Perm_Struct ps |], _) ->
@@ -677,7 +682,7 @@ instance IRTDescs (PermExpr (LLVMShapeType w)) where
   irtDescs mb_expr ixs = case (mbMatch mb_expr, ixs) of
     ([nuMP| PExpr_Var _ |], _) -> irtVarTDesc ixs
     ([nuMP| PExpr_EmptyShape |], _) -> return []
-    ([nuMP| PExpr_EqShape _ |], _) -> return []
+    ([nuMP| PExpr_EqShape _ _ |], _) -> return []
     ([nuMP| PExpr_NamedShape _ _ nmsh args |], _) ->
       case (mbMatch $ namedShapeBody <$> nmsh, ixs) of
         (_, IRTRecVar) ->