Heapster: niche optimization for sums with an uninhabited type

heapster-saw/examples/rust_data.rs

@@ -1,10 +1,13 @@
-use std::collections::{HashMap, HashSet};
+use std::collections::{HashMap};
 use std::fmt;
+use std::convert::{Infallible};
 
+/*
 /* A function that immediately panics */
 pub fn get_out () -> ! {
     panic!("Uh oh!")
 }
+*/
 
 /* The logical and operation as a function on bool */
 pub fn bool_and (x:bool, y:bool) -> bool {
@@ -37,6 +40,7 @@ pub fn bool_and_struct (xy:BoolStruct) -> bool {
 
 /* A struct containing 2 32-bit values, to test how structs that fit into 1
  * 64-bit value are represented */
+#[repr(C)]
 pub struct TwoValues(u32,u32);
 
 pub fn mk_two_values (x1:u32,x2:u32) -> TwoValues {
@@ -65,6 +69,7 @@ pub extern fn two_values_proj1_extern (x:TwoValues) -> u32 {
 
 /* A struct containing 3 32-bit values, to test how structs that fit but don't
  * fill up 2 64-bit values are represented */
+#[repr(C)]
 pub struct ThreeValues(u32,u32,u32);
 
 pub fn mk_three_values (x1:u32,x2:u32,x3:u32) -> ThreeValues {
@@ -90,6 +95,7 @@ pub extern fn three_values_proj1_extern (x:ThreeValues) -> u32 {
 
 /* A struct containing 4 32-bit values, to test how structs that fit into 2
  * 64-bit values are represented */
+#[repr(C)]
 pub struct FourValues(u32,u32,u32,u32);
 
 pub fn mk_four_values (x1:u32,x2:u32,x3:u32,x4:u32) -> FourValues {
@@ -115,6 +121,7 @@ pub extern fn four_values_proj1_extern (x:FourValues) -> u32 {
 
 /* A struct containing 5 32-bit values, to test how structs that do not quite
  * fit into 2 64-bit values are represented */
+#[repr(C)]
 pub struct FiveValues(u32,u32,u32,u32,u32);
 
 pub fn mk_five_values (x1:u32,x2:u32,x3:u32,x4:u32,x5:u32) -> FiveValues {
@@ -156,9 +163,23 @@ pub fn test_result <'a> (r:&'a Result<u64,u64>) -> bool {
     }
 }
 
+/* Make a Result whose other branch is uninhabited */
+pub fn mk_result_infallible (x:u64) -> Result<Infallible,u64> {
+  Err(x)
+}
+
+/* Extract a value from a Result whose other branch is uninhabited */
+pub fn extract_from_result_infallible <'a> (r:&'a Result<Infallible,u64>) -> u64 {
+    match r {
+        Ok(i) => match *i { },
+        Err(x) => *x,
+    }
+}
+
 /* Sum of two types; yes, this is like Result, but defined locally so we can
  * make an impl block on it */
 #[derive(Clone, Debug, PartialEq)]
+#[repr(C)]
 pub enum Sum<X,Y> {
     Left (X),
     Right (Y)
@@ -212,28 +233,37 @@ pub extern fn mk_sum_sum_left_asym_extern (x:Sum<u32,u64>) -> Sum<Sum<u32,u64>,u
 
 
 /* A struct containing a string */
+#[repr(C)]
 pub struct StrStruct(String);
 
 impl StrStruct {
     /* Constructor for StrStruct */
     pub fn new(name: &str) -> StrStruct {
         StrStruct(name.to_string())
     }
+
+    // &str not considered FFI safe, so Rust doesn't like extern here
+    /*
     pub extern fn new_extern(name: &str) -> StrStruct {
         StrStruct(name.to_string())
     }
+    */
 
     /* Accessor for StrStruct */
     pub fn name(&self) -> String {
         match self {
             StrStruct(s) => s.to_string(),
         }
     }
+
+    // String not considered FFI safe, so Rust doesn't like extern here
+    /*
     pub extern fn name_extern(&self) -> String {
         match self {
             StrStruct(s) => s.to_string(),
         }
     }
+     */
 
     /* Version of name that maps to &str */
     pub fn name_str (&self) -> &str {
@@ -242,15 +272,19 @@ impl StrStruct {
         }
     }
 
+    // &str not considered FFI safe, so Rust doesn't like extern here
+    /*
     pub extern fn name_str_extern (&self) -> &str {
         match self {
             StrStruct(s) => s.as_str(),
         }
     }
+     */
 }
 
 /* A struct with a mix of different field types */
 #[derive(Clone, Debug, PartialEq)]
+#[repr(C)]
 pub struct MixedStruct {
     pub s: String,
     pub i1: u64,
@@ -409,6 +443,7 @@ pub fn opt_hash_map_for_string_and_list64 (str:String,
     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;

heapster-saw/examples/rust_data.saw

@@ -27,6 +27,9 @@ heapster_define_llvmshape env "Box" 64 "T:llvmshape 64" "ptrsh(T)";
 // Result type
 heapster_define_rust_type env "pub enum Result<X,Y> { Ok (X), Err (Y) }";
 
+// Infallable type
+heapster_define_llvmshape env "Infallible" 64 "" "falsesh";
+
 // Sum type
 heapster_define_rust_type env "pub enum Sum<X,Y> { Left (X), Right (Y) }";
 
@@ -252,7 +255,7 @@ heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64"
 
 // 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"
+  "alloc..boxed..Box$LT$T$C$A$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>>";
@@ -328,7 +331,7 @@ heapster_assume_fun_rename_prim env panicking_panic_sym "panicking_panic"
 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 }(%\"std::collections::hash::map::HashMap<u64, u64>\"*,\
 \        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>";
@@ -346,7 +349,7 @@ heapster_assume_fun_rename_prim env hashmap_u64_u64_insert_sym "hashmap_u64_u64_
 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>\"*,\
+\     %\"std::collections::hash::map::HashMap<alloc::string::String, List64>\"*,\
 \     %\"alloc::string::String\"*, %List64*)";
 // FIXME: assume hashmap_String_List64_insert_sym
 
@@ -444,14 +447,18 @@ heapster_assume_fun_rename_prim env Formatter__write_fmt_sym "Formatter__write_f
   "<'a> fn (&'a mut fmt::Formatter, fmt::Arguments) -> fmt::Result";
 
 // std::panicking::begin_panic
-begin_panic_sym <- heapster_find_symbol env "3std9panicking11begin_panic17";
-heapster_assume_fun_rename_prim env begin_panic_sym "begin_panic" "<'a, 'b> fn(&'a str, &'b panic::Location) -> !";
+// FIXME: add this back in when we add get_out back
+//begin_panic_sym <- heapster_find_symbol env "3std9panicking11begin_panic17";
+//heapster_assume_fun_rename_prim env begin_panic_sym "begin_panic" "<'a, 'b> fn(&'a str, &'b panic::Location) -> !";
+
 
 /***
  *** Type-Checked Functions
  ***/
-get_out_sym <- heapster_find_symbol env "7get_out";
-heapster_typecheck_fun_rename env get_out_sym "get_out" "<> fn() -> !";
+
+// FIXME: SAW cannot currently handle get_out in the binary
+//get_out_sym <- heapster_find_symbol env "7get_out";
+//heapster_typecheck_fun_rename env get_out_sym "get_out" "<> fn() -> !";
 
 // bool_and
 bool_and_sym <- heapster_find_symbol env "8bool_and";
@@ -496,6 +503,17 @@ heapster_typecheck_fun_rename env test_result_sym "test_result"
 //heapster_typecheck_fun_rename env test_result_sym "test_result"
 //  "().arg0:memblock(R,0,16,Result<fieldsh(int64<>),fieldsh(int64<>)>) -o ret:int1<>";
 
+// mk_result_infallible
+mk_result_infallible_sym <- heapster_find_symbol env "20mk_result_infallible";
+heapster_typecheck_fun_rename env mk_result_infallible_sym "mk_result_infallible"
+  "<> fn (x:u64) -> Result<Infallible,u64>";
+
+// extract_from_result_infallible
+extract_from_result_infallible_sym <- heapster_find_symbol env "30extract_from_result_infallible";
+heapster_typecheck_fun_rename env extract_from_result_infallible_sym "extract_from_result_infallible"
+  "<'a> fn (r:&'a Result<Infallible,u64>) -> u64";
+
+
 // test_sum_impl
 test_sum_impl_sym <- heapster_find_symbol env "13test_sum_impl";
 heapster_typecheck_fun_rename env test_sum_impl_sym "test_sum_impl"

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

@@ -380,6 +380,19 @@ matchMbOptionLikeShape :: Mb ctx (PermExpr (LLVMShapeType w)) ->
 matchMbOptionLikeShape =
   mbMaybe . mbMapCl $(mkClosed [| matchOptionLikeShape |])
 
+-- | Test if a shape is a sum type where one branch is empty, i.e., a tagged
+-- union shape with two tags, one of which has the false shape as contents. If
+-- so, return the non-false shape @sh@.
+matchSumFalseShape :: PermExpr (LLVMShapeType w) ->
+                      Maybe (PermExpr (LLVMShapeType w))
+matchSumFalseShape top_sh = case asTaggedUnionShape $ simplifyShape top_sh of
+  Just (SomeTaggedUnionShape (taggedUnionDisjsNoTags -> [sh1, sh2]))
+    | PExpr_FalseShape <- simplifyShape sh1 -> Just sh2
+  Just (SomeTaggedUnionShape (taggedUnionDisjsNoTags -> [sh1, sh2]))
+    | PExpr_FalseShape <- simplifyShape sh2 -> Just sh1
+  _ -> Nothing
+
+
 -- | Build a `ShapeFun` from a `SomeNamedShape`
 namedShapeShapeFun :: (1 <= w, KnownNat w) => RustName -> NatRepr w ->
                       SomeNamedShape -> RustConvM (ShapeFun w)
@@ -410,8 +423,17 @@ namedShapeShapeFun nm w (SomeNamedShape nmsh)
 
 namedShapeShapeFun nm w (SomeNamedShape nmsh)
   | Just Refl <- testEquality w (natRepr nmsh) =
-    return $ mkShapeFun nm (namedShapeArgs nmsh) $
-    \exprs -> PExpr_NamedShape Nothing Nothing nmsh exprs
+    return $ mkShapeFun nm (namedShapeArgs nmsh) $ \exprs ->
+    case namedShapeBody nmsh of
+      -- Test if nmsh applied to exprs unfolds to a sum with false, and if so,
+      -- return just the non-false payload shape
+      DefinedShapeBody mb_sh
+        | unfolded_sh <- simplifyShape (subst (substOfExprs exprs) mb_sh)
+        , Just sh <- matchSumFalseShape unfolded_sh ->
+          sh
+      -- Otherwise just return the named shape applied to exprs
+      _ -> PExpr_NamedShape Nothing Nothing nmsh exprs
+
 namedShapeShapeFun _ w (SomeNamedShape nmsh) =
   fail $ renderDoc $ fillSep
   [pretty "Incorrect size of shape" <+> pretty (namedShapeName nmsh),