Report block-level verification progress, port Prusti Assistant changes#57
Closed
trktby wants to merge 54 commits intoAurel300:rewrite-2023from
Closed
Report block-level verification progress, port Prusti Assistant changes#57trktby wants to merge 54 commits intoAurel300:rewrite-2023from
trktby wants to merge 54 commits intoAurel300:rewrite-2023from
Conversation
Also comment out a line that crashes when not run from the same directory. This was problematic for working with Prusti Assistant.
Ported change from PR viperproject#1334
Port basic functionality for the new prusti-server work flow according to PR viperproject#1334 .
Querying signatures, spans of call contract collection and call finding does not work yet. PR: viperproject#1334
Defpath only verification does not work since test_entrypoint currently just puts the entire program into the request regardless of the verification tasks at hand. Update the flags in the documentation. PR: viperproject#1334
Requires the viperserver backend to support these messages too.
Every body owner function that is not passed to be verified explicitly acts as though it were pure and trusted to skip the encoding of their bodies. Additionally, VERIFY_ONLY_DEFPATH now takes a vector of String instead of just a string.
`SpanOfCallContracts` now has a vector as it's `call_spans` field so only one object is created per function definition rather than one per call. `CallSpanFinder` now also collects local functions for call contract span emission. Functions that are never called need not be emitted.
A main goal here is that the vir-viper translation happens on the same thread that encodes the program in the local verification case. This should happen so the allocated arena, which is thread local, can be used. Additionally, the JVM reliant bits are a bit more hidden from the general procedure.
* Impure generics * Fixed bug due to type parameters not being encoded * Remove fractional perm * mk_bool doesn't need extra typarams
* domain fields don't need a full encoding of their type yet * type alias for do_encode_full result * parameterise TaskEncoderDependencies by the owning encoder * remove some dependency unwraps * remove 'tcx lifetime, use 'vir * check for cycles when requesting dependencies or emitting output ref * add try operators for some emit output refs
Move backtranslation to where server messages are processed. Move `EncodingInfo` to encoder crate.
- The viper program is now sent using a `GlobalRef`, so it actually compiles. - Cache usage no longer involves the `VerificationRequestProcessing` object. - The cache is now lazy, therefore only loads if the `ENABLE_CACHE` flag is set. - The `VerificationRequestProcessing` object is no longer constructed when all the requests are cache hits. The thread it holds is also not spawned as a result.
Also change backtranslation of viper identifiers. Note that caching may not work properly for now if the `GENERATE_VIPER_MESSAGES` flag is set. Fixing this is a WIP.
… rewrite-2023-assistant-features Also clean up some imports.
The same error with different positions used to produce the same hashes (generated using java's `hashCode` function).
This previously made it impossible to selectively verify in single file programs. It still does not work when running through x.py.
This reverts commit f3cf4ef.
Aurel300
changed the title
Merged
Owner
|
Superseded by #109. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR is part of a practical work supervised by @Aurel300. It is based on a previous work's PR.
The main changes are: