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

Slice and array indexing should be supported in triggers #812

Open
vakaras opened this issue Dec 25, 2021 · 4 comments
Open

Slice and array indexing should be supported in triggers #812

vakaras opened this issue Dec 25, 2021 · 4 comments
Labels
bug Something isn't working

Comments

@vakaras
Copy link
Contributor

vakaras commented Dec 25, 2021

Currently, using s[i] in a trigger where s is an array or a slice causes Prusti to crash.
@fpoli fpoli added bug Something isn't working crash labels Jan 4, 2022
@fpoli fpoli mentioned this issue Jan 7, 2022
Open
@Pointerbender Pointerbender mentioned this issue Feb 3, 2022
Merged
bors bot added a commit that referenced this issue Feb 3, 2022
@bors @Pointerbender
Merge #848
a3f5d80 
848: partial fix for #819 r=vakaras a=Pointerbender

In issue #819 the `prusti-tests/tests/verify/pass/arrays/selection_sort.rs` test was entirely disabled in anticipation of some future fixes. Those future fixes have not landed yet, but PRs #831 and #844 opened a window for a temporary work-around. I was curious if I could get it to work and was able to achieve a stable test run for `selection_sort` (consistently finishes in under 60 seconds on my PC). 

The changes I made were to selectively disable the `fix_quantifiers` and `optimize_folding` optimization passes and use wrapper functions for array accesses instead of using array indices directly (those are blocked by #812 for now).

I don't consider this a proper fix for #819, but I think it could still be a nice regression test and now that its execution time has stabilized I think it's safe to turn back on. Let's keep #819 open to track implementing a proper fix in the future.

Co-authored-by: Pointerbender <[email protected]>
@Pointerbender
Copy link
Contributor

@vakaras In case the refactoring is not a blocker for adding support for triggers on domain functions, and if it's not a super non-trivial fix, maybe I could take a stab at implementing this one? :)

@vakaras
Copy link
Contributor Author

vakaras commented Feb 10, 2022 •
edited
Loading

Thanks! This code is likely to be rewritten during the refactoring, but I think it would be still worth trying to figure out how to actually do it.

Pointerbender added a commit to Pointerbender/prusti-dev that referenced this issue Feb 12, 2022
@Pointerbender
add support for array/slice accesses in quantifier triggers viperproj…
452ab51 
…ect#812
@Pointerbender Pointerbender mentioned this issue Feb 12, 2022
Merged
Pointerbender added a commit to Pointerbender/prusti-dev that referenced this issue Feb 13, 2022
@Pointerbender
some minor improvements and fixes for trigger encoding viperproject#812
78a371a
Pointerbender added a commit to Pointerbender/prusti-dev that referenced this issue Feb 14, 2022
@Pointerbender
fix corner cases where is_encoding_trigger might not be set back to…
e64aa54 
… `false` viperproject#812
@fpoli fpoli removed the crash label Feb 16, 2022
fpoli pushed a commit to Pointerbender/prusti-dev that referenced this issue Feb 17, 2022
@Pointerbender @fpoli
add support for array/slice accesses in quantifier triggers viperproj…
74924a9 
…ect#812
fpoli pushed a commit to Pointerbender/prusti-dev that referenced this issue Feb 17, 2022
@Pointerbender @fpoli
some minor improvements and fixes for trigger encoding viperproject#812
7d9f8ed
fpoli pushed a commit to Pointerbender/prusti-dev that referenced this issue Feb 17, 2022
@Pointerbender @fpoli
fix corner cases where is_encoding_trigger might not be set back to…
d5e4a9c 
… `false` viperproject#812
bors bot added a commit that referenced this issue Feb 17, 2022
@bors @Pointerbender @fpoli
Merge #858
2c7765e 
858: add support for array/slice accesses in quantifier triggers r=fpoli a=Pointerbender

This PR adds support for using slice/array access in quantifier triggers (issue #812). These are encoded including bound checks, but the bound checks are not needed (nor allowed) inside the triggers. The fix/hack applied here removes those bound checks from the triggers.

This seems to fix the encoding problem, but it doesn't appear to be a full solution for `prusti-tests/tests/verify/pass/arrays/selection_sort.rs` (see #819). If I replace all the triggers there with direct array accesses (but not the lookup and the assignment statements in the loop body wrapped in `get`/`set`), then the verification time for this test jumps from 1 minute to 4 minutes on my PC. If I also replace the lookup and assign statements in the loop bodies with direct array accesses, then the verification times out. I suspect this is a matter of adding a few dummy assert statements here and there, but as long as #796 hasn't landed yet this does not seem to improve the situation (it still times out, even with dummy assertions atm). I tried adding `body_invariant`s instead of assert statements, but this also still results in timeouts. For these reasons, I decided not to include the updated version of `selection_sort.rs`. Using a custom pure lookup function such as `get` still yields superior performance over interactions with `lookup_pure` array/slice accesses, even with the fix from this PR, unfortunately :)

The test `prusti-tests/tests/verify/pass/issues/issue-812-4.rs` is currently ignored because it triggers a `todo!()` in the new vir high encoder here:

https://github.com/viperproject/prusti-dev/blob/66c90d5dae9040eb68b2f0d2689faa480b10e8d6/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs#L26-L35

I included the test anyway so that it can be enabled later when that part is implemented during the refactoring.

I'd like to investigate deeper what is the best way to trigger the quantifiers (which are snap encoded) from a Viper method body (where Rust statements are not snap encoded, unless routed through a pure Rust function), but I thought I'd first do a check-in first to see if the proposed fix is heading in the right direction and inquire about if there are any other alternatives than #796 or custom pure lookup functions to work-around the performance issues that seem to be caused by the mixed snap/non-snap encoding :) 

Thanks!





Co-authored-by: Pointerbender <[email protected]>
Co-authored-by: Federico Poli <[email protected]>
@fpoli
Copy link
Member

fpoli commented Feb 17, 2022

Implemented in #858 by @Pointerbender. Thanks!

@vakaras Do you prefer to keep this issue open because of the following todo, or can I close?

The test prusti-tests/tests/verify/pass/issues/issue-812-4.rs is currently ignored because it triggers a todo!() in the new vir high encoder here:

prusti-dev/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs

Lines 26 to 35 in 66c90d5

fn inline_closure_high<'tcx>(
_encoder: &Encoder<'_, 'tcx>,
_def_id: DefId,
_cl_expr: Expression,
_args: Vec<VariableDecl>,
_parent_def_id: DefId,
_substs_map: &SubstMap<'tcx>,
) -> SpannedEncodingResult<Expression> {
todo!()
}

@vakaras
Copy link
Contributor Author

vakaras commented Feb 17, 2022

@vakaras Do you prefer to keep this issue open because of the following todo, or can I close?

The test prusti-tests/tests/verify/pass/issues/issue-812-4.rs is currently ignored because it triggers a todo!() in the new vir high encoder here:

prusti-dev/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs

Lines 26 to 35 in 66c90d5

fn inline_closure_high<'tcx>(
_encoder: &Encoder<'_, 'tcx>,
_def_id: DefId,
_cl_expr: Expression,
_args: Vec<VariableDecl>,
_parent_def_id: DefId,
_substs_map: &SubstMap<'tcx>,
) -> SpannedEncodingResult<Expression> {
todo!()
}

Let's keep it open.

@Pointerbender Pointerbender mentioned this issue Feb 19, 2022
Merged
bors bot added a commit that referenced this issue Feb 19, 2022
@bors @Pointerbender
Merge #876
00fa0d0 
876: use array indices as quantifier triggers for `selection_sort` test r=vakaras a=Pointerbender

Now that there is support for array/slice indices in quantifier triggers (#812), I updated the `selection_sort.rs` test case to make use of this. This results in a ~15 second faster verification time 🎉 increasing performance further per #819.

Prusti can't verify this test yet when using array assignments instead of `set()`, so there are still 2 calls to `set()` in the test with a FIXME to address these later. Will post a separate comment with some ideas about what that would take.

Co-authored-by: Pointerbender <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@vakaras @fpoli @Pointerbender