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

Add block granularity progress indication #262

Draft
wants to merge 99 commits into
base: master
Choose a base branch
from
Draft

Add block granularity progress indication #262

wants to merge 99 commits into from

Conversation

trktby
Copy link

@trktby trktby commented Sep 3, 2024

This PR is part of a practical work supervised by @Aurel300. It is based on a previous work's PR.
The main changes are:

  • Adding new block-level gutter decorators, inspired by Dafny. Their purpose is to be able to track verification progress with a higher granularity than before. This includes a current block decorator to see on which basic block a program might be hanging during verification.
  • Persisting partial results of a verification across selective verification runs - selectively verifying a method no longer wipes the results of the other, unmodified ones (they are marked as stale however).
  • Refactoring of the storage of decorators. They are now stored and generated per method. Mainly for ease of organization of block-based decorators.

cedihegi and others added 30 commits October 23, 2022 14:15
@cedihegi
small changes
8c56c94
@cedihegi
small fix
9fa5ae6
@cedihegi
invoking prusti correctly now
6141e56
@cedihegi
just slight adjustements according to changes in prusti-dev
ef1402b
@cedihegi
parsing IDE Info and passing the flag, for some reason just passing a…
4ebe83c 
… flag is f*ing hard
@cedihegi
working codelenses and codeactions
51adf3d
@cedihegi
not sure what I changed, rebase this at some point :)
d0615eb
@cedihegi
Fixing problems such as IdeInfo only saving information for one file …
cfc86b5 
…or crate

and codelenses only updating after reloading a file or editing it.
@cedihegi
IDE info is now persistent across files, i.e. when
3984ed3 
verifying different files or crates, not just the info
of the most recent one is stored.
@cedihegi
starting to refactor
9dc4347
@cedihegi
adjusted what happens on save, on open, etc, better behavior when col…
0d69e03 
…lecting information but not verifying
initial quantifier inlays working
9dc3a83
@cedihegi
various changes, now able to query signatures for extern specifications
9b3125d
@cedihegi
adjusted ide-info
d86e81c
Add hovering and splitting by function that caused the quantifier ins…
5e7011f 
…tantiations
@cedihegi
refactoring, error handling, and some fixes
eca362e
@cedihegi
new snippets
4dda223
@cedihegi
Displaying checkmarks next to methods.
dde8a60 
Not yet actually depending on the verification's result.
Merge remote-tracking branch 'cedric/proto' into quant
f7fe789
@cedihegi
WIP: refactored large portions and parse verification info, some bug …
5f2aa6a 
…with displaying it
@cedihegi
failed and successful verifications are now displayed correctly
805c450
@cedihegi
Displaying verification time and whether results were cached now work…
707bd46 
…s. However the textual decorators just stack in subsequent verifications so they will have to be removed at some point
@cedihegi
Avoid parsing all messages 3 times :)
e71bd1a
Add compilation and verification error differentiation. Do not show a…
e9b63d9 
… crash message upon kill.
Merge remote-tracking branch 'cedric/proto' into quant
3f707d6
@cedihegi
Some formatting + documenting
75fac62
@cedihegi
Reworked underlying data structure for many features, now they all se…
df461c8 
…em to be working
@cedihegi
Cleaned up some unnecessary logs
ca999e0
@cedihegi
Merge remote-tracking branch 'joseph/quant' into proto
3d37f65
@cedihegi
fixed minor bug
b85e0c7
cedihegi and others added 30 commits March 5, 2023 16:55
@cedihegi
Adjust environment variable to change in prusti-dev and small fix
56350e0
@cedihegi
Add more logging messages to find reason for failing CI
8ec2df6
@cedihegi
Debug CI by adding a timer between opening and verifying
55fd637
@cedihegi
Take out timeout for further debugging
9bb29f4
@cedihegi
Display a better decoration message when verification fails
5d338da
@cedihegi
Change text for codeLens of selective verification
265afbf
Add the newly needed env flags to the server
7fae6eb
@cedihegi
Another attempt to resolve the timing problems with OnOpen
8e664a7
@cedihegi
Merge branch 'master' of github.com:cedihegi/prusti-assistant
9ff32e7
@cedihegi
Fix linter errors and uninstall / remove unused library 'mutex'
aea6a5f
@cedihegi
New pledges and add new configuration options to README
bcbb897
Improve quantifier markdown strings
2daf308
Adjust the quantifier reporting frequency
80ab5d7
Make the Z3 smt.qi.profile_freq configurable
4992db2
@trktby
Add (incomplete) initial infrastructure for blockwise verification
5107365 
Includes a draft of new icons.
@trktby
Reformat selective verification argument, add back quantifier flags
51a2771
@trktby
Fix up some flags, add extension settings, parse block messages
04eec45
@trktby
Display block based decorators
798af9e
@trktby
Revamp decorator management
cc66a15 
This includes:
- retaining information between selective runs
- overhaul of the decorator related storage structure
- processing of block messages
- some bug fixes
@trktby
Add current block indicator, move method specific data
7b0aa10
@trktby
Fix current block display bug, add silicon extra arg option
da37e3d 
Before, the current block may have been misleading. In the case of all
paths through all methods currently being verified being stuck on a
block, and those last block messages not having triggered the UI update
(i.e. if they all arrived within the update interval), the last
displayed blocks are not actually the hanging ones. Now anothe
configurable interval forces an update.
A new option for passing extra silicon arguments is added. In
particular, when reporting block messages, the
`--numberOfErrorsToReport` option is set to 0 by default.
@trktby
Compare methods by hash of trimmed string, improve decorator wiping
e02e34e
@trktby
Fix tab change not fetching decorators
5e50d46
@trktby
Various small fixes
41a8a90 
- extra silicon args is an array now
- keep providing code lens if the file is not dirty (mainly for tab changes)
- simplify verification result parsing (since the filename prefix seems to not be useful)
- mark verification results of methods as stale if they were not selected for the last verification run
- only force update when there has been data and take tab changes into account
@trktby
use setTimeout instead of setInterval
22e2050
@trktby
Add decorations which may or may not be used
8c38340
@trktby
Fix decorator display bugs
cd46292 
The ranges extracted from the line masks were off.
Also some inputs to the extractor function were wrong.
Path results that are "Unreachable" are treated as success for now.
@trktby
Add support for blockFailureMessages
4614459
@trktby
Some cleaning
9525208
@trktby
Fix bugs
9c39423 
- First range of a bitmasks was always interpreted as 0
- Information retention had some edge cases mishandled
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@trktby @cedihegi