Skip to content

Heapster/arrays seqsh blocks #1649

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

Merged
merged 3 commits into from
May 2, 2022
Merged

Heapster/arrays seqsh blocks #1649

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
50ddf87
Eliminate field-shaped blocks in the array prover.
abakst Apr 29, 2022
147d85c
Add test for blocks with sequence of field shapes
abakst Apr 29, 2022
9220cec
Fix broken testcase
abakst Apr 29, 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
11 changes: 11 additions & 0 deletions heapster-saw/proverTests/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,6 +138,16 @@ int64ArrayPerm off len = arrayPerm (toIdx off) (toIdx len) 8 (fieldShape (intVal
int32ArrayPerm :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> LLVMArrayPerm 64
int32ArrayPerm off len = arrayPerm (toIdx off) (toIdx len) 4 (fieldShape (intValuePerm @32))

charShape :: PermExpr (LLVMShapeType 64)
charShape = fieldShape (intValuePerm @8)

charArray :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> AtomicPerm (LLVMPointerType 64)
charArray off len = Perm_LLVMArray (arrayPerm (toIdx off) (toIdx len) 1 (fieldShape (intValuePerm @8)))

str3Block :: (ArrayIndexExpr a) => a -> AtomicPerm (LLVMPointerType 64)
str3Block off = Perm_LLVMBlock $
memblockPerm off 3 (PExpr_SeqShape charShape (PExpr_SeqShape charShape charShape))

arrayPerm ::
PermExpr (BVType w) ->
PermExpr (BVType w) ->
Expand Down Expand Up @@ -178,6 +188,7 @@ arrayTests =
[ int64field 0, int64field 8, int64field 16 ] ===> int64array 8 3
, testCase "insufficient fields (2)" $ fails $
[ int64field 0, int64field 8, int64field 16 ] ===> int64array 0 4
, testCase "string" $ passes $ str3Block 0 ===> charArray 0 3
]

, testGroup "mix of permission types"
Expand Down
9 changes: 9 additions & 0 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 @@ -6689,6 +6689,15 @@ proveVarLLVMArrayH x p psubst ps mb_ap
| PExpr_ArrayShape {} <- llvmBlockShape bp = True
arrayBlock _ = False

proveVarLLVMArrayH x p psubst ps mb_ap
| Just i <- findIndex seqFieldBlock ps =
implElimAppendIthLLVMBlock x ps i >>>= \ps' ->
proveVarLLVMArrayH x p psubst ps' mb_ap
where
seqFieldBlock (Perm_LLVMBlock bp)
| Just flds <- matchLLVMFieldShapeSeq (llvmBlockShape bp) = length flds > 1
seqFieldBlock _ = False

-- Otherwise, try and build a completely borrowed array that references existing
-- permissions that cover the range of mb_ap, and recurse (hitting the special
-- case above).
Expand Down