Skip to content

Commit

Permalink
Merge pull request #1505 from GaloisInc/heapster/duplicate-read-membl…
Browse files Browse the repository at this point in the history
…ocks

Heapster: duplicate read memblocks
  • Loading branch information
mergify[bot] authored Nov 12, 2021
2 parents 99b783a + 255122d commit dd9026e
Show file tree
Hide file tree
Showing 6 changed files with 177 additions and 51 deletions.
Binary file modified heapster-saw/examples/rust_data.bc
Binary file not shown.
11 changes: 11 additions & 0 deletions heapster-saw/examples/rust_data.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 }

Expand Down
21 changes: 21 additions & 0 deletions heapster-saw/examples/rust_data.saw
Original file line number Diff line number Diff line change
Expand Up @@ -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, \
Expand Down Expand Up @@ -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"
Expand Down
131 changes: 81 additions & 50 deletions heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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 >>>
Expand All @@ -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
Expand All @@ -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,<len,*stride,fps,(i*stride+j):bs) where the jth element of fps
-- equals ptr((rw,j) |-> 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)
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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') >>>

Expand Down
40 changes: 39 additions & 1 deletion heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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


Expand Down Expand Up @@ -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))
Expand Down Expand Up @@ -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
Expand Down
25 changes: 25 additions & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 =>
Expand Down Expand Up @@ -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
Expand All @@ -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


Expand Down

0 comments on commit dd9026e

Please sign in to comment.