Heapster Rust layout optimization for option-like types

heapster-saw/examples/rust_data.rs

@@ -371,6 +371,14 @@ pub fn list64_is_empty (l: &List64) -> bool {
     }
 }
 
+/* Return the tail of a List64, or None if it is the empty list */
+pub fn list64_tail (l: List64) -> Option<List64> {
+    match l {
+        List64::Nil64 => None,
+        List64::Cons64 (_,tl) => Some (*tl)
+    }
+}
+
 /* Sum the elements of a List64 */
 pub fn list64_sum(l:&List64) -> u64 {
     match l {
@@ -379,6 +387,15 @@ pub fn list64_sum(l:&List64) -> u64 {
     }
 }
 
+/* Find an element in a List64 and return a mutable reference to it */
+pub fn list64_find_mut <'a> (x:u64, l:&'a mut List64) -> Option<&'a mut u64> {
+    match l {
+        List64::Nil64 => None,
+        List64::Cons64 (y,rest) =>
+            if x == *y { Some (y) } else { list64_find_mut (x,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> {

heapster-saw/examples/rust_data.saw

@@ -257,6 +257,22 @@ box_list20_u64_clone_sym <- heapster_find_symbol_with_type env
 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>>";
 
+// alloc::box_free
+BoxFree_funs <- heapster_find_symbols_with_type env "alloc8box_free" "void(i64*)";
+for BoxFree_funs
+  (\ x ->
+     // FIXME: this should have type memblock(W,0,len,emptysh) -o empty, but the
+     // length len is given by the type at which this is instantiated, i.e., the
+     // T at which this instance of box_free has type Unique<T> -> (), and there
+     // is no way to reconstruct T from the symbol name or its type, so we give
+     // it the weaker type saying it consumes no permissions, and assume that
+     // the code which calls it, generated by rustc, drops the pointer it passes
+     // to boxfree before using it again. We could have it take in a memblock
+     // permission with existential length and shape, but that would require
+     // handling existential lengths...
+     heapster_assume_fun_rename_prim env x x
+       "(). empty -o empty");
+
 // <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";
@@ -557,6 +573,11 @@ 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";
 
+// list64_tail
+list64_tail_sym <- heapster_find_symbol env "11list64_tail";
+heapster_typecheck_fun_rename env list64_tail_sym "list64_tail"
+  "<> fn (l:List64) -> Option<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

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

@@ -67,7 +67,6 @@ import Verifier.SAW.Heapster.GenMonad
 import GHC.Stack
 import Unsafe.Coerce
 import Data.Functor.Constant (Constant(..))
-import What4.Protocol.VerilogWriter.ABCVerilog (inputDoc)
 
 
 -- * Helper functions (should be moved to Hobbits)

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

@@ -3550,6 +3550,14 @@ isLLVMBlockPerm :: AtomicPerm a -> Bool
 isLLVMBlockPerm (Perm_LLVMBlock _) = True
 isLLVMBlockPerm _ = False
 
+-- | Test if an 'AtomicPerm' is any form of pointer permission
+isLLVMPointerPerm :: AtomicPerm a -> Bool
+isLLVMPointerPerm (Perm_LLVMField _) = True
+isLLVMPointerPerm (Perm_LLVMArray _) = True
+isLLVMPointerPerm (Perm_LLVMBlock _) = True
+isLLVMPointerPerm (Perm_LLVMFunPtr _ _) = True
+isLLVMPointerPerm _ = False
+
 -- | Test if an 'AtomicPerm' is a lifetime permission
 isLifetimePerm :: AtomicPerm a -> Maybe (a :~: LifetimeType)
 isLifetimePerm (Perm_LOwned _ _ _) = Just Refl
@@ -3686,6 +3694,13 @@ mkPermLLVMFunPtrs (_w :: f w) fun_perms@(SomeFunPerm fun_perm:_) =
                        (funPermRet fun_perm))
       (ValPerm_Conj $ map (\(SomeFunPerm fp) -> Perm_Fun fp) fun_perms)
 
+-- | The shape for an @eq(llvmword(w))@ permission
+llvmEqWordShape :: (1 <= w, KnownNat w) => prx w -> Integer ->
+                   PermExpr (LLVMShapeType w)
+llvmEqWordShape w i =
+  PExpr_FieldShape $ LLVMFieldShape $ ValPerm_Eq $
+  PExpr_LLVMWord $ bvIntOfSize w i
+
 -- | Existential permission @x:eq(word(e))@ for some @e@
 llvmExEqWord :: (1 <= w, KnownNat w) => prx w ->
                 Binding (BVType w) (ValuePerm (LLVMPointerType w))
@@ -4044,6 +4059,23 @@ llvmBlockEndOffset = bvRangeEnd . llvmBlockRange
 llvmFieldShapeLength :: LLVMFieldShape w -> Integer
 llvmFieldShapeLength (LLVMFieldShape p) = exprLLVMTypeBytes p
 
+-- | Simplify a shape, removing any trailing empty shapes and unfolding any
+-- unfoldable named shapes
+simplifyShape :: PermExpr (LLVMShapeType w) -> PermExpr (LLVMShapeType w)
+simplifyShape (PExpr_SeqShape sh PExpr_EmptyShape) = simplifyShape sh
+simplifyShape (PExpr_NamedShape rw l nmsh args)
+  | TrueRepr <- namedShapeCanUnfoldRepr nmsh
+  , Just sh <- unfoldModalizeNamedShape rw l nmsh args =
+    simplifyShape sh
+simplifyShape sh = sh
+
+-- | Test if a shape describes a pointer
+isLLVMPointerShape :: PermExpr (LLVMShapeType w) -> Bool
+isLLVMPointerShape (PExpr_FieldShape (LLVMFieldShape (ValPerm_Conj1 p))) =
+  isLLVMPointerPerm p
+isLLVMPointerShape (PExpr_PtrShape _ _ _) = True
+isLLVMPointerShape _ = False
+
 -- | Return the expression for the length of a shape if there is one
 llvmShapeLength :: (1 <= w, KnownNat w) => PermExpr (LLVMShapeType w) ->
                    Maybe (PermExpr (BVType w))
@@ -4196,6 +4228,17 @@ modalizeBlockShape (LLVMBlockPerm {..}) =
   maybe (error "modalizeBlockShape") id $
   modalizeShape (Just llvmBlockRW) (Just llvmBlockLifetime) llvmBlockShape
 
+-- | Extract the shape-in-bindings for an unfoldable shape
+namedShapeBodyShape :: KnownNat w => NamedShape 'True args w ->
+                       Mb args (PermExpr (LLVMShapeType w))
+namedShapeBodyShape (NamedShape _ _ (DefinedShapeBody mb_sh)) = mb_sh
+namedShapeBodyShape sh@(NamedShape _ _ (RecShapeBody mb_sh _ _)) =
+  let (prxs :>: _) = mbToProxy mb_sh in
+  nuMulti prxs $ \ns ->
+  subst (substOfExprs (namesToExprs ns :>:
+                       PExpr_NamedShape Nothing Nothing sh (namesToExprs ns)))
+  mb_sh
+
 -- | Unfold a named shape
 unfoldNamedShape :: KnownNat w => NamedShape 'True args w -> PermExprs args ->
                     PermExpr (LLVMShapeType w)
@@ -4451,6 +4494,20 @@ getShapeBVTag sh | Just some_bv <- shapeToTag sh = Just some_bv
 getShapeBVTag (PExpr_SeqShape sh1 _) = getShapeBVTag sh1
 getShapeBVTag _ = Nothing
 
+-- | Remove the leading tag from a shape where 'getShapeBVTag' succeeded
+shapeRemoveTag :: PermExpr (LLVMShapeType w) -> PermExpr (LLVMShapeType w)
+shapeRemoveTag (PExpr_SeqShape sh1 sh2) | isJust (shapeToTag sh1) = sh2
+shapeRemoveTag (PExpr_SeqShape sh1 sh2) =
+  PExpr_SeqShape (shapeRemoveTag sh1) sh2
+shapeRemoveTag sh | isJust (shapeToTag sh) = PExpr_EmptyShape
+shapeRemoveTag sh =
+  error ("shapeRemoveTag: " ++ permPrettyString emptyPPInfo sh)
+
+-- | Extract the disjunctive shapes from a 'TaggedUnionShape' but removing the
+-- leading tags
+taggedUnionDisjsNoTags :: TaggedUnionShape w sz -> [PermExpr (LLVMShapeType w)]
+taggedUnionDisjsNoTags = map shapeRemoveTag . taggedUnionDisjs
+
 -- | Test if a shape is a tagged union shape and, if so, convert it to the
 -- 'TaggedUnionShape' representation
 asTaggedUnionShape :: PermExpr (LLVMShapeType w) ->

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

@@ -33,6 +33,7 @@ import Prelude hiding (span)
 import Data.Maybe
 import Data.List hiding (span)
 import GHC.TypeLits
+import qualified Data.BitVector.Sized as BV
 import Data.Functor.Constant
 import Data.Functor.Product
 import Control.Applicative
@@ -303,11 +304,10 @@ class RsConvert w a b | w a -> b where
 -- * Converting Named Rust Types
 ----------------------------------------------------------------------
 
--- FIXME HERE: I think we no longer need SomeShapeFun
-
--- | A shape function with existentially quantified arguments
-data SomeShapeFun w =
-  forall args. SomeShapeFun (CruCtx args) (Mb args (PermExpr (LLVMShapeType w)))
+-- | A function that builds a shape from a sequence of 'PermExpr' arguments and
+-- a 'String' representation of them for printing errors
+type ShapeFun w =
+  Some TypedPermExprs -> String -> RustConvM (PermExpr (LLVMShapeType w))
 
 -- | A sequence of 'PermExprs' along with their types
 type TypedPermExprs = RAssign (Typed PermExpr)
@@ -333,33 +333,86 @@ typedExprsOfList :: TypeRepr a -> [PermExpr a] -> Some TypedPermExprs
 typedExprsOfList tp =
   foldl (\(Some es) e -> Some (es :>: Typed tp e)) (Some MNil)
 
--- | Apply a 'SomeShapeFun', if possible
-tryApplySomeShapeFun :: SomeShapeFun w -> Some TypedPermExprs ->
+-- | Build a 'ShapeFun' for the given 'RustName' from a function on permission
+-- expressions of the supplied types
+mkShapeFun :: RustName -> CruCtx ctx ->
+              (PermExprs ctx -> PermExpr (LLVMShapeType w)) -> ShapeFun w
+mkShapeFun nm ctx f = \some_exprs exprs_str -> case some_exprs of
+  Some exprs
+    | Just Refl <- testEquality ctx (typedPermExprsCtx exprs) ->
+      return $ f (typedPermExprsExprs exprs)
+  _ ->
+    fail $ renderDoc $ fillSep
+    [ pretty "Converting application of type:" <+> pretty (show nm)
+    , pretty "To arguments:" <+> pretty exprs_str
+    , pretty "Arguments not of expected types:" <+> pretty ctx ]
+
+-- | Build a 'ShapeFun' with no arguments
+constShapeFun :: RustName -> PermExpr (LLVMShapeType w) -> ShapeFun w
+constShapeFun nm sh = mkShapeFun nm CruCtxNil (const sh)
+
+-- | Test if a shape is "option-like", meaning it is a tagged union shape with
+-- two tags, one of which has contents and one which has no contents; i.e., it
+-- is of the form
+--
+-- > (fieldsh(eq(llvmword(bv1)));sh) orsh (fieldsh(eq(llvmword(bv2))))
+--
+-- or
+--
+-- > (fieldsh(eq(llvmword(bv1)))) orsh (fieldsh(eq(llvmword(bv2)));sh)
+--
+-- where @sh@ is non-empty. If so, return the non-empty shape @sh@, called the
+-- "payload" shape.
+matchOptionLikeShape :: PermExpr (LLVMShapeType w) ->
                         Maybe (PermExpr (LLVMShapeType w))
-tryApplySomeShapeFun (SomeShapeFun ctx mb_sh) (Some exprs)
-  | Just Refl <- testEquality ctx (typedPermExprsCtx exprs) =
-    Just $ subst (substOfExprs $ typedPermExprsExprs exprs) mb_sh
-tryApplySomeShapeFun _ _ = Nothing
-
--- | Build a 'SomeShapeFun' with no arguments
-constShapeFun :: PermExpr (LLVMShapeType w) -> SomeShapeFun w
-constShapeFun sh = SomeShapeFun CruCtxNil (emptyMb sh)
-
--- | Build the shape @fieldsh(exists z:bv sz.eq(llvmword(z))@
-sizedIntShapeFun :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) =>
-                    prx1 w -> prx2 sz -> SomeShapeFun w
-sizedIntShapeFun _ sz =
-  constShapeFun $ PExpr_FieldShape (LLVMFieldShape $
-                                    ValPerm_Exists $ llvmExEqWord sz)
-
--- | Build a `SomeShapeFun` from `SomeNamedShape`
-namedShapeShapeFun :: NatRepr w -> SomeNamedShape -> RustConvM (SomeShapeFun w)
-namedShapeShapeFun w (SomeNamedShape nmsh)
-  | Just Refl <- testEquality w (natRepr nmsh) = return $
-    SomeShapeFun (namedShapeArgs nmsh)
-                 (nuMulti (cruCtxProxies (namedShapeArgs nmsh))
-                          (\ns -> PExpr_NamedShape Nothing Nothing nmsh (namesToExprs ns)))
-namedShapeShapeFun w (SomeNamedShape nmsh) =
+matchOptionLikeShape top_sh = case asTaggedUnionShape top_sh of
+  Just (SomeTaggedUnionShape (taggedUnionDisjsNoTags ->
+                              [PExpr_EmptyShape, PExpr_EmptyShape])) -> Nothing
+  Just (SomeTaggedUnionShape (taggedUnionDisjsNoTags ->
+                              [PExpr_EmptyShape, sh])) -> Just sh
+  Just (SomeTaggedUnionShape (taggedUnionDisjsNoTags ->
+                              [sh, PExpr_EmptyShape])) -> Just sh
+  _ -> Nothing
+
+-- | Test if a shape-in-binding is "option-like" as per 'matchOptionLikeShape'
+matchMbOptionLikeShape :: Mb ctx (PermExpr (LLVMShapeType w)) ->
+                          Maybe (Mb ctx (PermExpr (LLVMShapeType w)))
+matchMbOptionLikeShape =
+  mbMaybe . mbMapCl $(mkClosed [| matchOptionLikeShape |])
+
+-- | Build a `ShapeFun` from a `SomeNamedShape`
+namedShapeShapeFun :: (1 <= w, KnownNat w) => RustName -> NatRepr w ->
+                      SomeNamedShape -> RustConvM (ShapeFun w)
+-- For an option-like shape, try to do discriminant elision
+namedShapeShapeFun nm w (SomeNamedShape nmsh)
+  | Just Refl <- testEquality w (natRepr nmsh)
+  , DefinedShapeBody mb_sh <- namedShapeBody nmsh
+  , Just mb_payload_sh <- matchMbOptionLikeShape mb_sh =
+    return $ mkShapeFun nm (namedShapeArgs nmsh) $ \exprs ->
+    case simplifyShape (subst (substOfExprs exprs) mb_payload_sh) of
+
+      -- If the payload is a pointer shape, return payload orsh eq(0)
+      payload_sh@(isLLVMPointerShape -> True) ->
+        PExpr_OrShape payload_sh $ llvmEqWordShape w 0
+
+      -- If the payload is a tagged union shape, add an extra tag with an empty
+      -- shape for its argument
+      (asTaggedUnionShape -> Just (SomeTaggedUnionShape tag_u)) ->
+        let new_tag =
+              foldr max 0 $ map ((1+) . BV.asUnsigned) $
+              taggedUnionTags tag_u in
+        taggedUnionToShape $
+        taggedUnionCons (BV.mkBV knownNat new_tag) (llvmEqWordShape w new_tag)
+        tag_u
+
+      -- Otherwise, just use the named shape itself
+      _ -> PExpr_NamedShape Nothing Nothing nmsh exprs
+
+namedShapeShapeFun nm w (SomeNamedShape nmsh)
+  | Just Refl <- testEquality w (natRepr nmsh) =
+    return $ mkShapeFun nm (namedShapeArgs nmsh) $
+    \exprs -> PExpr_NamedShape Nothing Nothing nmsh exprs
+namedShapeShapeFun _ w (SomeNamedShape nmsh) =
   fail $ renderDoc $ fillSep
   [pretty "Incorrect size of shape" <+> pretty (namedShapeName nmsh),
    pretty "Expected:" <+> pretty (intValue w),
@@ -376,15 +429,15 @@ flattenRustName (RustName ids) = concat $ intersperse "::" $ map name ids
 instance Show RustName where
   show = show . flattenRustName
 
-instance RsConvert w RustName (SomeShapeFun w) where
+instance RsConvert w RustName (ShapeFun w) where
   rsConvert w nm =
     do let str = flattenRustName nm
        env <- rciPermEnv <$> ask
        case lookupNamedShape env str of
-         Just nmsh -> namedShapeShapeFun (natRepr w) nmsh
+         Just nmsh -> namedShapeShapeFun nm (natRepr w) nmsh
          Nothing ->
            do n <- lookupName str (LLVMShapeRepr (natRepr w))
-              return $ constShapeFun (PExpr_Var n)
+              return $ constShapeFun nm (PExpr_Var n)
 
 -- | Get the "name" = sequence of identifiers out of a Rust path
 rsPathName :: Path a -> RustName
@@ -538,17 +591,9 @@ instance RsConvert w (Ty Span) (PermExpr (LLVMShapeType w)) where
          Just (rec_n, _, _)
            | rec_n == rsPathName path -> fail "Arguments do not match"
          _ ->
-           do someShapeFn@(SomeShapeFun expected _ ) <- rsConvert w (rsPathName path)
-              someTypedArgs@(Some tyArgs) <- rsConvert w (rsPathParams path)
-              let actual = typedPermExprsCtx tyArgs
-              case tryApplySomeShapeFun someShapeFn someTypedArgs of
-                Just shTp -> return shTp
-                Nothing ->
-                  fail $ renderDoc $ fillSep
-                  [ pretty "Converting PathTy: " <+> pretty (show $ rsPathName path)
-                  , pretty "Expected arguments:" <+> pretty expected
-                  , pretty "Actual arguments:" <+> pretty actual
-                  ]
+           do shapeFn <- rsConvert w (rsPathName path)
+              someTypedArgs <- rsConvert w (rsPathParams path)
+              shapeFn someTypedArgs $ show (RustPP.prettyUnresolved path)
   rsConvert (w :: prx w) (BareFn _ abi rust_ls2 fn_tp span) =
     do Some3FunPerm fun_perm <- rsConvertMonoFun w span abi rust_ls2 fn_tp
        let args = funPermArgs fun_perm