diff --git a/heapster-saw/examples/rust_data.bc b/heapster-saw/examples/rust_data.bc index 1affdcf4f1..8ea8b57a8e 100644 Binary files a/heapster-saw/examples/rust_data.bc and b/heapster-saw/examples/rust_data.bc differ diff --git a/heapster-saw/examples/rust_data.rs b/heapster-saw/examples/rust_data.rs index 479e45be2a..535af1eabb 100644 --- a/heapster-saw/examples/rust_data.rs +++ b/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 { + 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 { diff --git a/heapster-saw/examples/rust_data.saw b/heapster-saw/examples/rust_data.saw index cdc8b4a48d..e6d5b04a2b 100644 --- a/heapster-saw/examples/rust_data.saw +++ b/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>) -> Box>"; +// 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 -> (), 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"); + // ::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"; + 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 diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index 0dd85d5fbd..127f0bd8a3 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/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) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index 27224a5868..9bcb88952d 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/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) -> diff --git a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs index 44d355b727..2f0f477a94 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs +++ b/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