Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Change Borrowed Array input permissions check #1625

Merged
merged 3 commits into from
Apr 15, 2022
Merged

Change Borrowed Array input permissions check #1625

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ebe6913
Check an array is totally borrowed by walking the borrowed cell ranges.
abakst Apr 5, 2022
0791cbc
Merge branch 'master' into heapster/array-borrow-check
Apr 14, 2022
ad75241
Merge branch 'master' into heapster/array-borrow-check
Apr 15, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 1 addition & 12 deletions heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1960,21 +1960,10 @@ simplImplIn (SImpl_LLVMArrayEmpty _ ap) =
simplImplIn (SImpl_LLVMArrayBorrowed x bp ap) =
if bvIsZero (llvmArrayLen ap) then
error "simplImplIn: SImpl_LLVMArrayBorrowed: empty array permission"
else if not totallyBorrowed then
else if not (llvmArrayIsBorrowed ap) then
error "simplImplIn: SImpl_LLVMArrayBorrowed: array permission not completely borrowed"
else
distPerms1 x (ValPerm_Conj1 $ Perm_LLVMBlock bp)
where
-- If all the subtractions below could be empty, then we've subtracted the
-- whole array
totallyBorrowed = all (bvCouldEqual (bvInt 0)) (bvRangeLength <$> remaining)

remaining =
-- iteratively subtract each borrow from the total range of array indices
foldr (\b xs -> xs >>= (`bvRangeDelete` llvmArrayBorrowCells b))
[llvmArrayCells ap]
(llvmArrayBorrows ap)


simplImplIn (SImpl_LLVMArrayFromBlock x bp) =
distPerms1 x $ ValPerm_LLVMBlock bp
Expand Down
18 changes: 18 additions & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4795,7 +4795,25 @@ llvmArrayBorrowRangeDelete borrow rng =
| otherwise =
error "llvmArrayBorrowRangeDelete: found non unit new_range for FieldBorrow"

-- | Return whether or not the borrows in @ap@ cover the range of cells [0, len). Specifically,
-- if the borrowed cells (as ranges) can be arranged in as a sequence of non-overlapping but contiguous
-- ranges (in the sense of @bvCouldEqual@) that extends at least as far as @len@ (in the sense of @bvLeq@)
llvmArrayIsBorrowed ::
(HasCallStack, 1 <= w, KnownNat w) =>
LLVMArrayPerm w ->
Bool
llvmArrayIsBorrowed ap =
go (bvInt 0) (llvmArrayBorrowCells <$> llvmArrayBorrows ap)
where
end = bvRangeEnd (llvmArrayCells ap)

go off borrows
| bvLeq end off
= True
| Just i <- findIndex (permForOff off) borrows
= go (bvAdd off (bvRangeLength (borrows!!i))) (deleteNth i borrows)

permForOff o b = bvCouldEqual o (bvRangeOffset b)

-- | Test if a byte offset @o@ statically aligns with a statically-known offset
-- into some array cell, i.e., whether
Expand Down