diff --git a/heapster-saw/examples/rust_data.bc b/heapster-saw/examples/rust_data.bc index 05b3c11a68..f1ace2bb16 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 1077ba7993..408958c0a7 100644 --- a/heapster-saw/examples/rust_data.rs +++ b/heapster-saw/examples/rust_data.rs @@ -12,6 +12,17 @@ pub fn bool_and_pair (xy:(bool,bool)) -> bool { xy.0 & xy.1 } +/* Read two integers from references and return their sum */ +pub fn ref_sum <'a,'b> (x:&'a u64, y:&'a u64) -> u64 { + return *x + *y; +} + +/* Double the integer pointed to by a reference by duplicating the reference and + * passing it to ref_sum */ +pub fn double_dup_ref <'a> (x:&'a u64) -> u64 { + return ref_sum (x, x); +} + #[repr(C)] pub struct BoolStruct { fst_bool:bool,snd_bool:bool } diff --git a/heapster-saw/examples/rust_data.saw b/heapster-saw/examples/rust_data.saw index 26d32a0b5e..09e622f4cf 100644 --- a/heapster-saw/examples/rust_data.saw +++ b/heapster-saw/examples/rust_data.saw @@ -221,6 +221,17 @@ heapster_assume_fun_rename env exchange_malloc_sym "exchange_malloc" \ ret:memblock(W,0,len,emptysh)" "\\ (len:Vec 64 Bool) -> returnM #() ()"; +// llvm.uadd.with.overflow.i64 +heapster_assume_fun env "llvm.uadd.with.overflow.i64" + "(). arg0:int64<>, arg1:int64<> -o ret:struct(int64<>,int1<>)" + "\\ (x y:Vec 64 Bool) -> \ + \ returnM (Vec 64 Bool * Vec 1 Bool) (bvAdd 64 x y, single Bool (bvCarry 64 x y))"; + +// llvm.expect.i1 +heapster_assume_fun env "llvm.expect.i1" + "().arg0:int1<>, arg1:int1<> -o ret:int1<>" "\\ (x y:Vec 1 Bool) -> returnM (Vec 1 Bool) x"; + + // memcpy heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, \ @@ -395,6 +406,16 @@ 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"; */ +// ref_sum +ref_sum_sym <- heapster_find_symbol env "7ref_sum"; +heapster_typecheck_fun_rename env ref_sum_sym "ref_sum" + "<'a,'b> fn (x:&'a u64, y:&'a u64) -> u64"; + +// double_dup_ref +double_dup_ref_sym <- heapster_find_symbol env "14double_dup_ref"; +heapster_typecheck_fun_rename env double_dup_ref_sym "double_dup_ref" + "<'a,'b> fn (x:&'a u64) -> u64"; + // test_result test_result_sym <- heapster_find_symbol env "11test_result"; heapster_typecheck_fun_rename env test_result_sym "test_result" diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index d4a7578f94..1b14689737 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -3920,9 +3920,36 @@ implEndLifetimeM ps l ps_in ps_out@(lownedPermsToDistPerms -> Just dps_out) | isJust (lownedPermsToDistPerms ps_in) = implSimplM ps (SImpl_EndLifetime l ps_in ps_out) >>> implTraceM (\i -> pretty "Ending lifetime:" <+> permPretty i l) >>> + implDropLifetimePermsM l >>> recombinePermsPartial ps (DistPermsCons dps_out l ValPerm_LFinished) implEndLifetimeM _ _ _ _ = implFailM "implEndLifetimeM: lownedPermsToDistPerms" +-- | Drop any permissions of the form @x:[l]p@ in the primary permissions for +-- @x@, which are supplied as an argument +implDropLifetimeConjsM :: NuMatchingAny1 r => ExprVar LifetimeType -> + ExprVar a -> [AtomicPerm a] -> + ImplM vars s r ps ps () +implDropLifetimeConjsM l x ps + | Just i <- findIndex (\p -> atomicPermLifetime p == Just (PExpr_Var l)) ps = + implPushM x (ValPerm_Conj ps) >>> + implExtractSwapConjM x ps i >>> + implDropM x (ValPerm_Conj1 (ps!!i)) >>> + let ps' = deleteNth i ps in + implPopM x (ValPerm_Conj ps') >>> + implDropLifetimeConjsM l x ps' +implDropLifetimeConjsM _ _ _ = return () + +-- | Find all primary permissions of the form @x:[l]p@ and drop them, assuming +-- that we have just ended lifetime @l@ +implDropLifetimePermsM :: NuMatchingAny1 r => ExprVar LifetimeType -> + ImplM vars s r ps ps () +implDropLifetimePermsM l = + (NameMap.assocs <$> view varPermMap <$> getPerms) >>>= \vars_and_perms -> + forM_ vars_and_perms $ \case + NameAndElem x (ValPerm_Conj ps) -> + implDropLifetimeConjsM l x ps + _ -> return () + -- | Save a permission for later by splitting it into part that is in the -- current lifetime and part that is saved in the lifetime for later. Assume -- permissions @@ -3941,6 +3968,7 @@ implSplitLifetimeM :: (KnownRepr TypeRepr a, NuMatchingAny1 r) => implSplitLifetimeM x f args l l2 sub_ls ps_in ps_out = implTraceM (\i -> sep [pretty "Splitting lifetime to" <+> permPretty i l2 <> colon, + permPretty i x <> colon <> permPretty i (ltFuncMinApply f l)]) >>> implSimplM Proxy (SImpl_SplitLifetime x f args l l2 sub_ls ps_in ps_out) >>> getTopDistPerm l2 >>>= implPopM l2 @@ -4758,8 +4786,8 @@ recombinePerm' x x_p@(ValPerm_Exists _) p = recombinePerm' x (ValPerm_Conj x_ps) (ValPerm_Conj (p:ps)) = implExtractConjM x (p:ps) 0 >>> implSwapM x (ValPerm_Conj1 p) x (ValPerm_Conj ps) >>> - recombinePermConj x x_ps p >>>= \x_ps' -> - recombinePermExpl x (ValPerm_Conj x_ps') (ValPerm_Conj ps) + recombinePermConj x x_ps p >>> + recombinePerm x (ValPerm_Conj ps) recombinePerm' x x_p (ValPerm_Named npn args off) | TrueRepr <- nameIsConjRepr npn = implNamedToConjM x npn args off >>> @@ -4770,18 +4798,16 @@ recombinePerm' x _ p = implDropM x p -- conjuctive permission @x_p1 * ... * x_pn@ for @x@, returning the resulting -- permission conjucts for @x@ recombinePermConj :: NuMatchingAny1 r => ExprVar a -> [AtomicPerm a] -> - AtomicPerm a -> ImplM vars s r as (as :> a) [AtomicPerm a] + AtomicPerm a -> ImplM vars s r as (as :> a) () --- If p is a field read permission that is already in x_ps, drop it -recombinePermConj x x_ps p@(Perm_LLVMField fp) - | Just (Perm_LLVMField fp') <- - find (\case Perm_LLVMField fp' -> - bvEq (llvmFieldOffset fp') (llvmFieldOffset fp) - _ -> False) x_ps - , PExpr_Read <- llvmFieldRW fp - , PExpr_Read <- llvmFieldRW fp' = - implDropM x (ValPerm_Conj1 p) >>> - pure x_ps +-- If p is a field permission whose range is a subset of that of a permission we +-- already hold, drop it +recombinePermConj x x_ps (Perm_LLVMField fp) + | any (llvmAtomicPermContainsRange $ llvmFieldRange fp) x_ps = + implDropM x $ ValPerm_LLVMField fp + +-- FIXME: if p is a field permission whose range overlaps with but is not wholly +-- contained in a permission we already hold, split it and recombine parts of it -- If p is an array read permission whose offsets match an existing array -- permission, drop it @@ -4792,41 +4818,17 @@ recombinePermConj x x_ps p@(Perm_LLVMArray ap) bvEq (llvmArrayLen ap') (llvmArrayLen ap) _ -> False) x_ps , PExpr_Read <- llvmArrayRW ap = - implDropM x (ValPerm_Conj1 p) >>> - pure x_ps - + implDropM x (ValPerm_Conj1 p) -- If p is an is_llvmptr permission and x_ps already contains one, drop it recombinePermConj x x_ps p@Perm_IsLLVMPtr | elem Perm_IsLLVMPtr x_ps = - implDropM x (ValPerm_Conj1 p) >>> - pure x_ps + implDropM x (ValPerm_Conj1 p) --- NOTE: the following is old, but it would never match anyway, because if we +-- NOTE: we do not return a field that was borrowed from an array, because if we -- have a field (or block) that was borrowed from an array, it almost certainly --- was borrowed because we accessed it, so it will contain eq permissions and --- its shape will not equal that of the array it was borrowed from -{- --- If p is a field that was borrowed from an array, return it; i.e., if we are --- returning x:ptr((rw,off+i*stride+j) |-> p) and x has a permission of the form --- x:array(off, p), then remove (i*stride+j) from bs -recombinePermConj x x_ps (Perm_LLVMField fp) - | (ap,i,ix):_ <- - flip mapMaybe (zip x_ps [0::Int ..]) $ - \case (Perm_LLVMArray ap, i) - | Just ix <- matchLLVMArrayField ap (llvmFieldOffset fp) - , elem (FieldBorrow ix) (llvmArrayBorrows ap) -> - Just (ap,i,ix) - _ -> Nothing - , LLVMArrayField fp == llvmArrayFieldWithOffset ap ix = - implPushM x (ValPerm_Conj x_ps) >>> implExtractConjM x x_ps i >>> - let x_ps' = deleteNth i x_ps in - implPopM x (ValPerm_Conj x_ps') >>> - implLLVMArrayIndexReturn x ap ix >>> - recombinePermConj x x_ps' (Perm_LLVMArray $ - llvmArrayRemBorrow (FieldBorrow ix) ap) --} +-- was borrowed because we accessed it, so it will contain eq permissions, which +-- make it a stronger permission than the cell permission in the array -- If p is an array that was borrowed from some other array, return it recombinePermConj x x_ps (Perm_LLVMArray ap) @@ -4845,12 +4847,29 @@ recombinePermConj x x_ps (Perm_LLVMArray ap) implLLVMArrayReturn x ap_bigger ap >>>= \ap_bigger' -> recombinePermConj x x_ps' (Perm_LLVMArray ap_bigger') +-- If p is a memblock permission whose range is a subset of that of a permission +-- we already hold, drop it +recombinePermConj x x_ps (Perm_LLVMBlock bp) + | any (llvmAtomicPermContainsRange $ llvmBlockRange bp) x_ps = + implDropM x $ ValPerm_LLVMBlock bp + +-- If p is a memblock permission whose range overlaps with but is not wholly +-- contained in a permission we already hold, eliminate it and recombine +-- +-- FIXME: if the elimination fails, this shouldn't fail, it should just +-- recombine without eliminating, so we should special case those shapes where +-- the elimination will fail +recombinePermConj x x_ps (Perm_LLVMBlock bp) + | any (llvmAtomicPermOverlapsRange $ llvmBlockRange bp) x_ps = + implElimLLVMBlock x bp >>> + getTopDistPerm x >>>= \p -> + recombinePerm x p + -- Default case: insert p at the end of the x_ps recombinePermConj x x_ps p = implPushM x (ValPerm_Conj x_ps) >>> implInsertConjM x p x_ps (length x_ps) >>> - implPopM x (ValPerm_Conj (x_ps ++ [p])) >>> - pure (x_ps ++ [p]) + implPopM x (ValPerm_Conj (x_ps ++ [p])) -- | Recombine the permissions on the stack back into the permission set @@ -5424,7 +5443,15 @@ proveVarLLVMFieldH2 x (Perm_LLVMField fp) off mb_fp -- the lifetime so that the original modality is recovered after any borrow -- performed above is over. equalizeRWs x (\rw -> ValPerm_LLVMField $ fp''' { llvmFieldRW = rw }) - (llvmFieldRW fp) (mbLLVMFieldRW mb_fp) (SImpl_DemoteLLVMFieldRW x fp''') >>> + (llvmFieldRW fp) (mbLLVMFieldRW mb_fp) + (SImpl_DemoteLLVMFieldRW x fp''') >>>= \rw' -> + + -- Step 5: duplicate the field permission if it is copyable, and then return + let fp'''' = fp''' { llvmFieldRW = rw' } in + (if atomicPermIsCopyable (Perm_LLVMField fp'''') then + implCopyM x (ValPerm_LLVMField fp'''') >>> + recombinePerm x (ValPerm_LLVMField fp'''') + else return ()) >>> return () -- If we have a field permission with the correct offset that is bigger than the @@ -5958,10 +5985,8 @@ proveVarLLVMBlock x ps mb_bp = do psubst <- getPSubst proveVarLLVMBlocks x ps psubst [mb_bp] --- | Prove a conjunction of block and atomic permissions for @x@, assuming all --- of the permissions for @x@ are on the top of the stack and given by the --- second argument. The block permissions are the ones that we are currently --- working on, and when they are all proved we bottom out to 'proveVarConjImpl'. +-- | Prove a conjunction of block and atomic permissions for @x@ from the +-- permissions on top of the stack, which are given by the second argument. -- -- A central motivation of this algorithm is to do as little elimination on the -- left or introduction on the right as possible, in order to build the smallest @@ -6056,7 +6081,7 @@ proveVarLLVMBlocks1 :: -- We are done, yay! Pop ps and build a true permission proveVarLLVMBlocks1 x ps _ [] = - implPopM x (ValPerm_Conj ps) >>> introConjM x + recombinePerm x (ValPerm_Conj ps) >>> introConjM x -- If the offset, length, and shape of the top block matches one that we already -- have, just cast the rwmodality and lifetime and prove the remaining perms @@ -6079,6 +6104,12 @@ proveVarLLVMBlocks1 x ps psubst (mb_bp:mb_bps) -- Make the input block have the required modalities equalizeBlockModalities x bp mb_bp >>>= \bp' -> + -- Duplicate and save the block permission if it is copyable + (if atomicPermIsCopyable (Perm_LLVMBlock bp') then + implCopyM x (ValPerm_LLVMBlock bp') >>> + recombinePerm x (ValPerm_LLVMBlock bp') + else return ()) >>> + -- Move it down below ps' implSwapM x (ValPerm_Conj ps') x (ValPerm_LLVMBlock bp') >>> diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index 34819a615f..a8fa38b6f0 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -1874,7 +1874,7 @@ data LLVMArrayBorrow w -- ^ Borrow a specific cell of an array permission | RangeBorrow (BVRange w) -- ^ Borrow a range of array cells, where each cell is 'llvmArrayStride' - -- machine words long + -- bytes long deriving Eq @@ -3553,6 +3553,13 @@ llvmAtomicPermToSomeBlock (Perm_LLVMBlock bp) = Just $ SomeLLVMBlockPerm $ bp llvmAtomicPermToSomeBlock _ = Nothing +-- | Get the lifetime of an atomic perm if it is a field, array, or memblock +atomicPermLifetime :: AtomicPerm a -> Maybe (PermExpr LifetimeType) +atomicPermLifetime (Perm_LLVMField fp) = Just $ llvmFieldLifetime fp +atomicPermLifetime (Perm_LLVMArray ap) = Just $ llvmArrayLifetime ap +atomicPermLifetime (Perm_LLVMBlock bp) = Just $ llvmBlockLifetime bp +atomicPermLifetime _ = Nothing + -- | Get the offset of an atomic permission, if it has one llvmAtomicPermOffset :: AtomicPerm (LLVMPointerType w) -> Maybe (PermExpr (BVType w)) @@ -4306,6 +4313,37 @@ llvmPermContainsOffset off (Perm_LLVMBlock bp) Just ([prop], bvPropHolds prop) llvmPermContainsOffset _ _ = Nothing +-- | Test if an atomic LLVM permission contains (in the sense of 'bvPropHolds') +-- all offsets in a given range +llvmAtomicPermContainsRange :: (1 <= w, KnownNat w) => BVRange w -> + AtomicPerm (LLVMPointerType w) -> Bool +llvmAtomicPermContainsRange rng (Perm_LLVMArray ap) + | Just ix1 <- matchLLVMArrayIndex ap (bvRangeOffset rng) + , Just ix2 <- matchLLVMArrayIndex ap (bvRangeEnd rng) + , props <- llvmArrayBorrowInArray ap (RangeBorrow $ BVRange + (llvmArrayIndexCell ix1) + (llvmArrayIndexCell ix2)) = + all bvPropHolds props +llvmAtomicPermContainsRange rng (Perm_LLVMField fp) = + bvRangeSubset rng (llvmFieldRange fp) +llvmAtomicPermContainsRange rng (Perm_LLVMBlock bp) = + bvRangeSubset rng (llvmBlockRange bp) +llvmAtomicPermContainsRange _ _ = False + +-- | Test if an atomic LLVM permission has a range that overlaps with (in the +-- sense of 'bvPropHolds') the offsets in a given range +llvmAtomicPermOverlapsRange :: (1 <= w, KnownNat w) => BVRange w -> + AtomicPerm (LLVMPointerType w) -> Bool +llvmAtomicPermOverlapsRange rng (Perm_LLVMArray ap) = + bvRangesOverlap rng (llvmArrayAbsOffsets ap) && + not (null $ bvRangesDelete rng $ + map (llvmArrayBorrowOffsets ap) (llvmArrayBorrows ap)) +llvmAtomicPermOverlapsRange rng (Perm_LLVMField fp) = + bvRangesOverlap rng (llvmFieldRange fp) +llvmAtomicPermOverlapsRange rng (Perm_LLVMBlock bp) = + bvRangesOverlap rng (llvmBlockRange bp) +llvmAtomicPermOverlapsRange _ _ = False + -- | Search through a list of permissions for either some permission that -- definitely contains (as in 'bvPropHolds') the given offset or, failing that, -- and if the supplied 'Bool' flag is 'True', for all permissions that could (as diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs index 704554e121..661b6d130a 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs @@ -3601,6 +3601,23 @@ tcEmitLLVMStmt _arch _ctx _loc stmt = -- * Permission Checking for Jump Targets and Termination Statements ---------------------------------------------------------------------- +-- | Cast the primary permission for @x@ using any equality permissions on +-- variables *not* in the supplied list of determined variables. The idea here +-- is that we are trying to simplify out and remove un-determined variables. +castUnDetVarsForVar :: NuMatchingAny1 r => NameSet CrucibleType -> ExprVar a -> + ImplM vars s r RNil RNil () +castUnDetVarsForVar det_vars x = + (view varPermMap <$> getPerms) >>>= \var_perm_map -> + getPerm x >>>= \p -> + let nondet_perms = + NameMap.fromList $ + filter (\(NameMap.NameAndElem y _) -> not $ NameSet.member y det_vars) $ + NameMap.assocs var_perm_map in + let eqp = someEqProofFromSubst nondet_perms p in + implPushM x p >>> + implCastPermM x eqp >>> + implPopM x (someEqProofRHS eqp) + -- | Simplify and drop permissions @p@ on variable @x@ so they only depend on -- the determined variables given in the supplied list simplify1PermForDetVars :: NuMatchingAny1 r => @@ -3648,6 +3665,13 @@ simplify1PermForDetVars det_vars l (ValPerm_LOwned ls _ _) simplify1PermForDetVars det_vars _ p | nameSetIsSubsetOf (freeVars p) det_vars = pure () +-- If p is an equality permission to a word with undetermined variables, +-- existentially quantify over the word +simplify1PermForDetVars _ x p@(ValPerm_Eq (PExpr_LLVMWord e)) = + let mb_p = nu $ \z -> ValPerm_Eq $ PExpr_LLVMWord $ PExpr_Var z in + implPushM x p >>> introExistsM x e mb_p >>> + implPopM x (ValPerm_Exists mb_p) + -- Otherwise, drop p, because it is not determined simplify1PermForDetVars _det_vars x p = implPushM x p >>> implDropM x p @@ -3661,6 +3685,7 @@ simplifyPermsForDetVars det_vars_list = let det_vars = NameSet.fromList det_vars_list in (permSetVars <$> getPerms) >>>= \vars -> mapM_ (\(SomeName x) -> + castUnDetVarsForVar det_vars x >>> getPerm x >>>= simplify1PermForDetVars det_vars x) vars