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.

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

[WIP] Various IDE improvements and new features #1334

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

Conversation

cedihegi
Copy link
Contributor

@cedihegi cedihegi commented Feb 22, 2023

Changes to support various new features in prusti-assistant.

@Aurel300
@jthomme1

cedihegi and others added 30 commits November 8, 2022 21:51
(this commit is not compiling however!)
… by simply creating a fake error in the case

that no_verify and show_ide_info are set.
…ps, even though they introduce some new problems
…ocket. Report quantifier instantiations split by methods.
Joseph Thommes and others added 3 commits February 25, 2023 13:34
In general, when skipping verification, we introduced a so called
fake_error to make sure the compiler does not just cache this
as successful verification and then skip later verifications even
if that's not intended. Same issue occured for selective verification,
when verifying a single method that is "correct", this would be cached.
Now we throw a fake error in this case too, to avoid this.
Prusti Assistant offers a few new features, and it checks for this version
for them to be available.
@fpoli fpoli changed the title (WIP) various IDE improvements and new features Various IDE improvements and new features Mar 3, 2023
@fpoli fpoli changed the title Various IDE improvements and new features [WIP] Various IDE improvements and new features Mar 3, 2023
viper/src/verification_result.rs Outdated Show resolved Hide resolved
viper/src/verification_result.rs Outdated Show resolved Hide resolved
prusti/src/verifier.rs Outdated Show resolved Hide resolved
Comment on lines 105 to 106
settings.set_default("smt_qi_profile", true).unwrap();
settings.set_default("smt_qi_profile_freq", 10000).unwrap();
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Will these be passed to Z3 when not using the IDE? And in such a case, will the messages not be reported to the user? If so, QI profiling should be disabled by default.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(After looking at how they are used in the other file:) please make these be Option<_>, such that they are only passed as arguments when a value is set. The IDE can set these if they are needed.

prusti-utils/src/config.rs Outdated Show resolved Hide resolved
prusti/src/ide_helper/compiler_info.rs Outdated Show resolved Hide resolved
prusti/src/ide_helper/query_signature.rs Outdated Show resolved Hide resolved
prusti/src/ide_helper/query_signature.rs Outdated Show resolved Hide resolved
}
None => {
// function is a Trait (or something else?)
// are there other cases for AssocFns?
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think so.

Comment on lines 375 to 377
// can a single generic type have the same traitbound
// more than once with different arguments?
// I would imagine yes.. may be a todo
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Like T: Foo<i32> + Foo<u32>? Yes, this is possible.

Joseph Thommes and others added 12 commits March 5, 2023 01:05
Also add some debug statements.
In 2 places we throw fake errors to avoid caching of successes when we
should not. This lead to problems with local dependencies, since they are
verified too and the fake_error ended up being thrown too early. This
bug is resolved now.
First of all we separated trait bounds from generic args, since for
example for a function signature within an impl block, the trait bounds
at the function level can still refer to the generic args defined in the
impl block.
Secondly, we had a problem if a generic had duplicate traitbounds, with
different generics, e.g.: `T: Foo<u32> + Foo<String>`, this is now
handled correctly, under the assumption that the predicates occurr in a
certain order, i.e. projections come after their respective trait. So
far this seems to be always the case, if it's not I don't see how this
problem can be solved.
trktby added a commit to trktby/prusti-dev that referenced this pull request Aug 12, 2024
trktby added a commit to trktby/prusti-dev that referenced this pull request Aug 12, 2024
Port basic functionality for the new prusti-server work flow according
to PR viperproject#1334 .
trktby added a commit to trktby/prusti-dev that referenced this pull request Aug 12, 2024
Querying signatures, spans of call contract collection and call finding
does not work yet.
PR: viperproject#1334
trktby added a commit to trktby/prusti-dev that referenced this pull request Aug 12, 2024
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants