[WIP] Various IDE improvements and new features#1334

Draft

cedihegi wants to merge 90 commits into

viperproject:masterfrom

cedihegi:master

Commits on Nov 8, 2022

collecting information
hegglinc
committed

Commits on Nov 11, 2022

some updates, had a lot of problems with just passing flags...
hegglinc
committed

Commits on Nov 22, 2022

passing method calls and verification items to ide
hegglinc
committed

Commits on Dec 4, 2022

fixed duplicate method calls
hegglinc
committed
Fixed the issue of no_verify causing subsequent verifications to fail by simply creating a fake error in the case
hegglinc
committed

Commits on Dec 10, 2022

now finding correct defpath for function calls and also handling binops, even though they introduce some new problems
hegglinc
committed

Commits on Dec 11, 2022

Fixed a bug for calls where the DefId can not be found apparently.
hegglinc
committed

Commits on Dec 12, 2022

fixed minor bug and formatting
hegglinc
committed
now finding defpath's for MethodCalls too
hegglinc
committed

Commits on Dec 19, 2022

Figured out how to resolve MethodCalls, but we are still in trouble..
hegglinc
committed
Commit finally to own fork
Joseph Thommes
committed

Commits on Dec 29, 2022

Finally catching all relevant method calls as far as I can tell..
hegglinc
committed

Commits on Jan 3, 2023

initial quantifier instantiations working
Joseph Thommes
committed

Commits on Jan 5, 2023

generating signatures correctly in some cases, struggling with traitbounds
hegglinc
committed
successfully resolving projections (it seems)
hegglinc
committed

Commits on Jan 6, 2023

started on generating external specs for traits
hegglinc
committed

Commits on Jan 8, 2023

WIP: stream messages from server to client
Joseph Thommes
committed

Commits on Jan 19, 2023

Managed to subst EarlyBinders
hegglinc
committed
Merge remote-tracking branch 'upstream/master'
hegglinc
committed
Merge branch 'master' into proto-extspec
hegglinc
committed
upgraded my parts to current rust version
hegglinc
committed

Commits on Jan 31, 2023

Asynchronously report messages from the server to the client via WebSocket. Report quantifier instantiations split by methods.
Joseph Thommes
committed

Commits on Feb 4, 2023

refactored extern spec generation to try and make it more readable.
hegglinc
committed

Commits on Feb 7, 2023

renamed stuff
hegglinc
committed
Merge branch 'joseph_quant' into proto-extspec
hegglinc
committed
Merge remote-tracking branch 'upstream/master' into proto-extspec
hegglinc
committed

Commits on Feb 8, 2023

Adjusted viper VerificationResult so we can passe times, and whether is was cached to clients.
hegglinc
committed
WIP: restructure the process verification a bit
Joseph Thommes
committed
Fixed warnings and a bug.
cedric
committed

Commits on Feb 12, 2023

Commits on Feb 13, 2023

Changed message for fake errors and adjusted names of CompilerInfo procedures.
hegglinc
committed

Commits on Feb 15, 2023

Merge remote-tracking branch 'jthomme1/quant' into proto-extspec
hegglinc
committed
Add QuantifierChosenTriggersMessage reporting
Joseph Thommes
committed
Merge remote-tracking branch 'cedric/proto-extspec' into quant
Joseph Thommes
committed

Commits on Feb 16, 2023

passing information about specifications of calls to IDE now, called EncodingInfo
hegglinc
committed
WIP: async processing of verification info
Joseph Thommes
committed

Commits on Feb 19, 2023

Commits on Feb 20, 2023

Some minor output changes
Joseph Thommes
committed
Merge cedric's branch
Joseph Thommes
committed
Minor fixes
Joseph Thommes
committed
Merge remote-tracking branch 'upstream/master' into quant
Joseph Thommes
committed

Commits on Feb 21, 2023

give spans of pledges to IDE and filter out trusted methods and predicates from items offered for selective verification
hegglinc
committed
Merge remote-tracking branch 'joseph/quant' into proto-extspec
cedric
committed
updated ide-parts to new compiler version
cedric
committed
Emit everything in a compiler note/message
Joseph Thommes
committed
Make every token CamelCase
Joseph Thommes
committed
Set config variable for viper message reporting to default false.
Joseph Thommes
committed

Commits on Feb 22, 2023

Proper camelCase messages
Joseph Thommes
committed
Can not automatically generate extern_specs for local methods anymore
hegglinc
committed
Fix GlobalRef detaching warning. Add a few comments. Remove some debugging leftovers.
Joseph Thommes
committed
Better comment for the VerificationRequestProcessing global variable.
Joseph Thommes
committed
Remove leftover comment.
Joseph Thommes
committed
Merge remote-tracking branch 'jthomme1/quant'
hegglinc
committed
Correct formatting and removed all clippy warnings except for 2
hegglinc
committed
Fix last 2 clippy warnings
Joseph Thommes
committed
Updated viper-toolchain, added various comments / documentation, addressed a few reviews
hegglinc
committed
corrected tag for recent viper-ide nightly release
hegglinc
committed

Commits on Feb 23, 2023

updated viper-toolchain again, this time to a compatible version
hegglinc
committed
fixed error due to new scala version
hegglinc
committed
made testcases compile at least, but one is hard to update to new structure of verifier
hegglinc
committed
Fixed prusti-server test. Why do we get a 255 exit code on a successful verification?
Joseph Thommes
committed
Adjusted ui testcase that has additional note about existential quantifier now
hegglinc
committed
Bugfixes for 2 testcases. All tests should be passing now
hegglinc
committed

Commits on Feb 24, 2023

Add debug output
Joseph Thommes
committed
Merge remote-tracking branch 'cedric/master' into quant
Joseph Thommes
committed
Merge remote-tracking branch 'jthomme1/quant'
hegglinc
committed

Commits on Feb 25, 2023

Make cache save when not using a server
Joseph Thommes
committed
Merge remote-tracking branch 'jthomme1/quant'
hegglinc
committed
Gracefully close also the receiving end of the websocket.
Joseph Thommes
committed
Close the websocket connection correctly
Joseph Thommes
committed
Merge remote-tracking branch 'jthomme1/quant'
hegglinc
committed
Fix bug where successful selective verification is still cached
hegglinc
committed

Commits on Feb 27, 2023

Fix bug in translation of spans to vscode-spans
hegglinc
committed

Commits on Mar 1, 2023

Bump prusti version to 0.3.0
hegglinc
committed

Commits on Mar 4, 2023

Update viper-toolchain version
Joseph Thommes
committed

Commits on Mar 5, 2023

Implement some comments (untested)
Joseph Thommes
committed
Fix Z3 arguments
Joseph Thommes
committed
Fix test and formatting error
Joseph Thommes
committed
Refactor / Fix according to code reviews
cedric
committed
Format and move old comment to right location
cedric
committed
Address reviews and add comments
cedric
committed

Commits on Mar 6, 2023

Merge remote-tracking branch 'upstream/master'
Joseph Thommes
committed

Commits on Mar 7, 2023

Improve displaying of generated extern spec block for trait
hegglinc
committed
Fix some quantifier reporting weirdness
Joseph Thommes
committed

Commits on Mar 8, 2023

Make QI etc. also work for existential quantifiers
Joseph Thommes
committed

Commits on Mar 9, 2023

Check if current package is primary package before throwing fake_error
hegglinc
committed

Commits on Mar 13, 2023

Separate trait bounds from generic args and handle bad case
hegglinc
committed