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

[WIP] Various IDE improvements and new features #1334

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

[WIP] Various IDE improvements and new features #1334

wants to merge 90 commits into from

Commits on Nov 8, 2022

  1. collecting information

    @cedihegi
    cedihegi committed Nov 8, 2022
    Configuration menu
    Copy the full SHA
    ddb4779 View commit details
    Browse the repository at this point in the history

Commits on Nov 11, 2022

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

    @cedihegi
    cedihegi committed Nov 11, 2022
    Configuration menu
    Copy the full SHA
    bbc07cc View commit details
    Browse the repository at this point in the history

Commits on Nov 22, 2022

  1. passing method calls and verification items to ide

    @cedihegi
    cedihegi committed Nov 22, 2022
    Configuration menu
    Copy the full SHA
    dc4b1d5 View commit details
    Browse the repository at this point in the history

Commits on Dec 4, 2022

  1. fixed duplicate method calls 

    (this commit is not compiling however!)
    @cedihegi
    cedihegi committed Dec 4, 2022
    Configuration menu
    Copy the full SHA
    dc079fa View commit details
    Browse the repository at this point in the history

  2. Fixed the issue of no_verify causing subsequent verifications to fail… 

    … by simply creating a fake error in the case

that no_verify and show_ide_info are set.
    @cedihegi
    cedihegi committed Dec 4, 2022
    Configuration menu
    Copy the full SHA
    c1d86d2 View commit details
    Browse the repository at this point in the history

Commits on Dec 10, 2022

  1. now finding correct defpath for function calls and also handling bino… 

    …ps, even though they introduce some new problems
    @cedihegi
    cedihegi committed Dec 10, 2022
    Configuration menu
    Copy the full SHA
    207a4ad View commit details
    Browse the repository at this point in the history

Commits on Dec 11, 2022

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

    @cedihegi
    cedihegi committed Dec 11, 2022
    Configuration menu
    Copy the full SHA
    4636373 View commit details
    Browse the repository at this point in the history

Commits on Dec 12, 2022

  1. fixed minor bug and formatting

    @cedihegi
    cedihegi committed Dec 12, 2022
    Configuration menu
    Copy the full SHA
    e311df9 View commit details
    Browse the repository at this point in the history

  2. now finding defpath's for MethodCalls too

    @cedihegi
    cedihegi committed Dec 12, 2022
    Configuration menu
    Copy the full SHA
    3780ce1 View commit details
    Browse the repository at this point in the history

Commits on Dec 19, 2022

  1. Figured out how to resolve MethodCalls, but we are still in trouble..

    @cedihegi
    cedihegi committed Dec 19, 2022
    Configuration menu
    Copy the full SHA
    e518ef4 View commit details
    Browse the repository at this point in the history

  2. Commit finally to own fork

    Joseph Thommes committed Dec 19, 2022
    Configuration menu
    Copy the full SHA
    295040c View commit details
    Browse the repository at this point in the history

Commits on Dec 29, 2022

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

    @cedihegi
    cedihegi committed Dec 29, 2022
    Configuration menu
    Copy the full SHA
    7adf64e View commit details
    Browse the repository at this point in the history

Commits on Jan 3, 2023

  1. initial quantifier instantiations working

    Joseph Thommes committed Jan 3, 2023
    Configuration menu
    Copy the full SHA
    4943255 View commit details
    Browse the repository at this point in the history

Commits on Jan 5, 2023

  1. generating signatures correctly in some cases, struggling with traitb… 

    …ounds
    @cedihegi
    cedihegi committed Jan 5, 2023
    Configuration menu
    Copy the full SHA
    0bd03b9 View commit details
    Browse the repository at this point in the history

  2. successfully resolving projections (it seems)

    @cedihegi
    cedihegi committed Jan 5, 2023
    Configuration menu
    Copy the full SHA
    fe577dc View commit details
    Browse the repository at this point in the history

Commits on Jan 6, 2023

  1. started on generating external specs for traits

    @cedihegi
    cedihegi committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    dedc17b View commit details
    Browse the repository at this point in the history

Commits on Jan 8, 2023

  1. WIP: stream messages from server to client

    Joseph Thommes committed Jan 8, 2023
    Configuration menu
    Copy the full SHA
    8812f3d View commit details
    Browse the repository at this point in the history

Commits on Jan 19, 2023

  1. Managed to subst EarlyBinders

    @cedihegi
    cedihegi committed Jan 19, 2023
    Configuration menu
    Copy the full SHA
    c1cbde9 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/master'

    @cedihegi
    cedihegi committed Jan 19, 2023
    Configuration menu
    Copy the full SHA
    b4f93ae View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into proto-extspec

    @cedihegi
    cedihegi committed Jan 19, 2023
    Configuration menu
    Copy the full SHA
    41e1964 View commit details
    Browse the repository at this point in the history

  4. upgraded my parts to current rust version

    @cedihegi
    cedihegi committed Jan 19, 2023
    Configuration menu
    Copy the full SHA
    6facfce View commit details
    Browse the repository at this point in the history

Commits on Jan 31, 2023

  1. Asynchronously report messages from the server to the client via WebS… 

    …ocket. Report quantifier instantiations split by methods.
    Joseph Thommes committed Jan 31, 2023
    Configuration menu
    Copy the full SHA
    3ac17ee View commit details
    Browse the repository at this point in the history

Commits on Feb 4, 2023

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

    @cedihegi
    cedihegi committed Feb 4, 2023
    Configuration menu
    Copy the full SHA
    24ad838 View commit details
    Browse the repository at this point in the history

Commits on Feb 7, 2023

  1. renamed stuff

    @cedihegi
    cedihegi committed Feb 7, 2023
    Configuration menu
    Copy the full SHA
    5d141eb View commit details
    Browse the repository at this point in the history

  2. Merge branch 'joseph_quant' into proto-extspec

    @cedihegi
    cedihegi committed Feb 7, 2023
    Configuration menu
    Copy the full SHA
    95b78ca View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'upstream/master' into proto-extspec

    @cedihegi
    cedihegi committed Feb 7, 2023
    Configuration menu
    Copy the full SHA
    9b0b5ad View commit details
    Browse the repository at this point in the history

Commits on Feb 8, 2023

  1. Adjusted viper VerificationResult so we can passe times, and whether … 

    …is was cached to clients.
    @cedihegi
    cedihegi committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    bb6ddb2 View commit details
    Browse the repository at this point in the history

  2. WIP: restructure the process verification a bit

    Joseph Thommes committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    a4dce76 View commit details
    Browse the repository at this point in the history

  3. Fixed warnings and a bug.

    @cedihegi
    cedihegi committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    f84219c View commit details
    Browse the repository at this point in the history

Commits on Feb 12, 2023

  1. renamed a file and adjusted text for IDE information output

    @cedihegi
    cedihegi committed Feb 12, 2023
    Configuration menu
    Copy the full SHA
    d9e067c View commit details
    Browse the repository at this point in the history

  2. Finish process_verification restructuring. Add a parameter for qi.pro… 

    …file_freq. Encode the quantifier ID in the line of the position in order to not having to modify the silver way of encoding a quantifier.
    Joseph Thommes committed Feb 12, 2023
    Configuration menu
    Copy the full SHA
    a069cef View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'cedric/proto-extspec' into quant

    Joseph Thommes committed Feb 12, 2023
    Configuration menu
    Copy the full SHA
    92c92c3 View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2023

  1. Changed message for fake errors and adjusted names of CompilerInfo pr… 

    …ocedures.
    @cedihegi
    cedihegi committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    ca86115 View commit details
    Browse the repository at this point in the history

Commits on Feb 15, 2023

  1. Merge remote-tracking branch 'jthomme1/quant' into proto-extspec

    @cedihegi
    cedihegi committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    4e1a547 View commit details
    Browse the repository at this point in the history

  2. Add QuantifierChosenTriggersMessage reporting

    Joseph Thommes committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    26ea0af View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'cedric/proto-extspec' into quant

    Joseph Thommes committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    872b3c1 View commit details
    Browse the repository at this point in the history

Commits on Feb 16, 2023

  1. passing information about specifications of calls to IDE now, called … 

    …EncodingInfo
    @cedihegi
    cedihegi committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    2cbc865 View commit details
    Browse the repository at this point in the history

  2. WIP: async processing of verification info

    Joseph Thommes committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    c3a2c6f View commit details
    Browse the repository at this point in the history

Commits on Feb 19, 2023

  1. (IDE) Contract Spans are now also collected for pedges and termatinat… 

    …ions (altough ranges are not always accurate)
    @cedihegi
    cedihegi committed Feb 19, 2023
    Configuration menu
    Copy the full SHA
    5ed232e View commit details
    Browse the repository at this point in the history

  2. Cleaning up unused imports and debugging print statements

    @cedihegi
    cedihegi committed Feb 19, 2023
    Configuration menu
    Copy the full SHA
    91b91c4 View commit details
    Browse the repository at this point in the history

Commits on Feb 20, 2023

  1. Some minor output changes

    Joseph Thommes committed Feb 20, 2023
    Configuration menu
    Copy the full SHA
    ba54ed7 View commit details
    Browse the repository at this point in the history

  2. Merge cedric's branch

    Joseph Thommes committed Feb 20, 2023
    Configuration menu
    Copy the full SHA
    e4810ec View commit details
    Browse the repository at this point in the history

  3. Minor fixes

    Joseph Thommes committed Feb 20, 2023
    Configuration menu
    Copy the full SHA
    f886f8b View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'upstream/master' into quant

    Joseph Thommes committed Feb 20, 2023
    Configuration menu
    Copy the full SHA
    93a78c7 View commit details
    Browse the repository at this point in the history

Commits on Feb 21, 2023

  1. give spans of pledges to IDE and filter out trusted methods and predi… 

    …cates from items offered for selective verification
    @cedihegi
    cedihegi committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    9ef451a View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'joseph/quant' into proto-extspec

    @cedihegi
    cedihegi committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    5df2a04 View commit details
    Browse the repository at this point in the history

  3. updated ide-parts to new compiler version

    @cedihegi
    cedihegi committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    b6ba6f6 View commit details
    Browse the repository at this point in the history

  4. Emit everything in a compiler note/message

    Joseph Thommes committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    f27499c View commit details
    Browse the repository at this point in the history

  5. Make every token CamelCase

    Joseph Thommes committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    cf53b8e View commit details
    Browse the repository at this point in the history

  6. Set config variable for viper message reporting to default false.

    Joseph Thommes committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    158b9ad View commit details
    Browse the repository at this point in the history

Commits on Feb 22, 2023

  1. Proper camelCase messages

    Joseph Thommes committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    195af4d View commit details
    Browse the repository at this point in the history

  2. Can not automatically generate extern_specs for local methods anymore

    @cedihegi
    cedihegi committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    91f4ff9 View commit details
    Browse the repository at this point in the history

  3. Fix GlobalRef detaching warning. Add a few comments. Remove some debu… 

    …gging leftovers.
    Joseph Thommes committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    82e6063 View commit details
    Browse the repository at this point in the history

  4. Better comment for the VerificationRequestProcessing global variable.

    Joseph Thommes committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    849b18d View commit details
    Browse the repository at this point in the history

  5. Remove leftover comment.

    Joseph Thommes committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    33a2e63 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'jthomme1/quant'

    @cedihegi
    cedihegi committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    ed8b1b6 View commit details
    Browse the repository at this point in the history

  7. Correct formatting and removed all clippy warnings except for 2

    @cedihegi
    cedihegi committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    1b1242d View commit details
    Browse the repository at this point in the history

  8. Fix last 2 clippy warnings

    Joseph Thommes committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    ebfdd1b View commit details
    Browse the repository at this point in the history

  9. Updated viper-toolchain, added various comments / documentation, addr… 

    …essed a few reviews
    @cedihegi
    cedihegi committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    ca1d9d6 View commit details
    Browse the repository at this point in the history

  10. corrected tag for recent viper-ide nightly release

    @cedihegi
    cedihegi committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    137f9a2 View commit details
    Browse the repository at this point in the history

Commits on Feb 23, 2023

  1. updated viper-toolchain again, this time to a compatible version

    @cedihegi
    cedihegi committed Feb 23, 2023
    Configuration menu
    Copy the full SHA
    f79e966 View commit details
    Browse the repository at this point in the history

  2. fixed error due to new scala version

    @cedihegi
    cedihegi committed Feb 23, 2023
    Configuration menu
    Copy the full SHA
    f2fa93a View commit details
    Browse the repository at this point in the history

  3. made testcases compile at least, but one is hard to update to new str… 

    …ucture of verifier
    @cedihegi
    cedihegi committed Feb 23, 2023
    Configuration menu
    Copy the full SHA
    5600499 View commit details
    Browse the repository at this point in the history

  4. Fixed prusti-server test. Why do we get a 255 exit code on a successf… 

    …ul verification?
    Joseph Thommes committed Feb 23, 2023
    Configuration menu
    Copy the full SHA
    7e6ceaf View commit details
    Browse the repository at this point in the history

  5. Adjusted ui testcase that has additional note about existential quant… 

    …ifier now
    @cedihegi
    cedihegi committed Feb 23, 2023
    Configuration menu
    Copy the full SHA
    e8bddf0 View commit details
    Browse the repository at this point in the history

  6. Bugfixes for 2 testcases. All tests should be passing now

    @cedihegi
    cedihegi committed Feb 23, 2023
    Configuration menu
    Copy the full SHA
    ede8451 View commit details
    Browse the repository at this point in the history

Commits on Feb 24, 2023

  1. Add debug output

    Joseph Thommes committed Feb 24, 2023
    Configuration menu
    Copy the full SHA
    3572fea View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'cedric/master' into quant

    Joseph Thommes committed Feb 24, 2023
    Configuration menu
    Copy the full SHA
    be04342 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'jthomme1/quant'

    @cedihegi
    cedihegi committed Feb 24, 2023
    Configuration menu
    Copy the full SHA
    7d434b5 View commit details
    Browse the repository at this point in the history

Commits on Feb 25, 2023

  1. Make cache save when not using a server

    Joseph Thommes committed Feb 25, 2023
    Configuration menu
    Copy the full SHA
    bac27bf View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'jthomme1/quant'

    @cedihegi
    cedihegi committed Feb 25, 2023
    Configuration menu
    Copy the full SHA
    9ca7602 View commit details
    Browse the repository at this point in the history

  3. Gracefully close also the receiving end of the websocket.

    Joseph Thommes committed Feb 25, 2023
    Configuration menu
    Copy the full SHA
    b373c14 View commit details
    Browse the repository at this point in the history

  4. Close the websocket connection correctly

    Joseph Thommes committed Feb 25, 2023
    Configuration menu
    Copy the full SHA
    e84688f View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'jthomme1/quant'

    @cedihegi
    cedihegi committed Feb 25, 2023
    Configuration menu
    Copy the full SHA
    2cc9233 View commit details
    Browse the repository at this point in the history

  6. Fix bug where successful selective verification is still cached 

    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.
    @cedihegi
    cedihegi committed Feb 25, 2023
    Configuration menu
    Copy the full SHA
    c39ece5 View commit details
    Browse the repository at this point in the history

Commits on Feb 27, 2023

  1. Fix bug in translation of spans to vscode-spans

    @cedihegi
    cedihegi committed Feb 27, 2023
    Configuration menu
    Copy the full SHA
    f83a088 View commit details
    Browse the repository at this point in the history

Commits on Mar 1, 2023

  1. Bump prusti version to 0.3.0 

    Prusti Assistant offers a few new features, and it checks for this version
for them to be available.
    @cedihegi
    cedihegi committed Mar 1, 2023
    Configuration menu
    Copy the full SHA
    8b4563f View commit details
    Browse the repository at this point in the history

Commits on Mar 4, 2023

  1. Update viper-toolchain version

    Joseph Thommes committed Mar 4, 2023
    Configuration menu
    Copy the full SHA
    eaeef45 View commit details
    Browse the repository at this point in the history

Commits on Mar 5, 2023

  1. Implement some comments (untested)

    Joseph Thommes committed Mar 5, 2023
    Configuration menu
    Copy the full SHA
    82b0eb8 View commit details
    Browse the repository at this point in the history

  2. Fix Z3 arguments

    Joseph Thommes committed Mar 5, 2023
    Configuration menu
    Copy the full SHA
    a492472 View commit details
    Browse the repository at this point in the history

  3. Fix test and formatting error

    Joseph Thommes committed Mar 5, 2023
    Configuration menu
    Copy the full SHA
    f50a367 View commit details
    Browse the repository at this point in the history

  4. Refactor / Fix according to code reviews

    @cedihegi
    cedihegi committed Mar 5, 2023
    Configuration menu
    Copy the full SHA
    a1e6d9f View commit details
    Browse the repository at this point in the history

  5. Format and move old comment to right location

    @cedihegi
    cedihegi committed Mar 5, 2023
    Configuration menu
    Copy the full SHA
    b144843 View commit details
    Browse the repository at this point in the history

  6. Address reviews and add comments

    @cedihegi
    cedihegi committed Mar 5, 2023
    Configuration menu
    Copy the full SHA
    aaa3ea5 View commit details
    Browse the repository at this point in the history

Commits on Mar 6, 2023

  1. Merge remote-tracking branch 'upstream/master'

    Joseph Thommes committed Mar 6, 2023
    Configuration menu
    Copy the full SHA
    dc6ead0 View commit details
    Browse the repository at this point in the history

Commits on Mar 7, 2023

  1. Improve displaying of generated extern spec block for trait

    @cedihegi
    cedihegi committed Mar 7, 2023
    Configuration menu
    Copy the full SHA
    1f0ae07 View commit details
    Browse the repository at this point in the history

  2. Fix some quantifier reporting weirdness 

    Also add some debug statements.
    Joseph Thommes committed Mar 7, 2023
    Configuration menu
    Copy the full SHA
    e562bca View commit details
    Browse the repository at this point in the history

Commits on Mar 8, 2023

  1. Make QI etc. also work for existential quantifiers

    Joseph Thommes committed Mar 8, 2023
    Configuration menu
    Copy the full SHA
    65c99d9 View commit details
    Browse the repository at this point in the history

Commits on Mar 9, 2023

  1. Check if current package is primary package before throwing fake_error 

    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.
    @cedihegi
    cedihegi committed Mar 9, 2023
    Configuration menu
    Copy the full SHA
    a299c14 View commit details
    Browse the repository at this point in the history

Commits on Mar 13, 2023

  1. Separate trait bounds from generic args and handle bad case 

    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.
    @cedihegi
    cedihegi committed Mar 13, 2023
    Configuration menu
    Copy the full SHA
    eb05efc View commit details
    Browse the repository at this point in the history