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

Resources, Obligations, Time Reasoning #1408

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

Resources, Obligations, Time Reasoning #1408

wants to merge 90 commits into from

Commits on Jun 27, 2023

  1. Add resource predicates 

    For now it only handles `time_credits` and `time_receipts`.
    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    09e39b3 View commit details
    Browse the repository at this point in the history

  2. Add tests for time resources

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    412f1d2 View commit details
    Browse the repository at this point in the history

  3. Fix unfolding issue

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    14f7b3c View commit details
    Browse the repository at this point in the history

  4. Add resource predicates generation

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    4d249ad View commit details
    Browse the repository at this point in the history

  5. Feedback

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    73ea7bc View commit details
    Browse the repository at this point in the history

  6. Add flag to enable time reasoning

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    2d10a22 View commit details
    Browse the repository at this point in the history

  7. Add more test for time reasoning

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    7830d6c View commit details
    Browse the repository at this point in the history

  8. Add new tick builtin method

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    9d94c35 View commit details
    Browse the repository at this point in the history

  9. Add calls to tick in loops

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    a4e7fdb View commit details
    Browse the repository at this point in the history

  10. Update tests

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    69a868c View commit details
    Browse the repository at this point in the history

  11. Add more tests

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    c6e8686 View commit details
    Browse the repository at this point in the history

  12. Remove calls to tick to an exhale and an inhale for error reporting

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    f9f093a View commit details
    Browse the repository at this point in the history

  13. More tests and add an expression simplifier for methods 

    Implications are brocken with time credits and receipts contraints as they
are impure but Prusti translate them into ors which viper doesn't accept.
Simplifying those expression solve this issue as they are changed back to an implication.
    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    cec311f View commit details
    Browse the repository at this point in the history

  14. Formating

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    72de7d2 View commit details
    Browse the repository at this point in the history

  15. Add position to time credits/receipts expr

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    c44f07c View commit details
    Browse the repository at this point in the history

  16. Add temporary error reporting

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    637c27e View commit details
    Browse the repository at this point in the history

  17. Add more complex tests

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    6e463fa View commit details
    Browse the repository at this point in the history

  18. Fix position for error reporting

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    b6a2b5f View commit details
    Browse the repository at this point in the history

  19. Fix rebase

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    284fb6e View commit details
    Browse the repository at this point in the history

  20. Fix clippy error

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    98b18c8 View commit details
    Browse the repository at this point in the history

  21. Pull request reviews

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    4773f98 View commit details
    Browse the repository at this point in the history

  22. Add scope id to resource predicate for loop body

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    4994088 View commit details
    Browse the repository at this point in the history

  23. Add functions to modify resource predicate scope

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    9f4d2bd View commit details
    Browse the repository at this point in the history

  24. Add loop cost

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    a9a52b5 View commit details
    Browse the repository at this point in the history

  25. More quadratic loops in a seperate test

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    4fafe78 View commit details
    Browse the repository at this point in the history

  26. Clippy

    @Pialex99 @vfukala
    Pialex99 authored and vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    6fe96ed View commit details
    Browse the repository at this point in the history

  27. Fix small issues from rebase

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    51df834 View commit details
    Browse the repository at this point in the history

  28. Implement hardcoded PyRefObligation without leak checks yet

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    7dcdba2 View commit details
    Browse the repository at this point in the history

  29. Add forperm expressions and (very hacky) leak checks

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    722091e View commit details
    Browse the repository at this point in the history

  30. Replace PyRefObligations with generic obligations in VIR

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    f3ab30e View commit details
    Browse the repository at this point in the history

  31. Add general obligations (quite hacky so far)

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    6720901 View commit details
    Browse the repository at this point in the history

  32. Fix obligation access with struct arguments by also patching it in sn… 

    …apshot patcher
    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    cd5b895 View commit details
    Browse the repository at this point in the history

  33. Add amount and scope_id to obligations

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    d686cce View commit details
    Browse the repository at this point in the history

  34. Add a few demo programs

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    1c9da0e View commit details
    Browse the repository at this point in the history

  35. Add alloc-dealloc demo program

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    384a9ee View commit details
    Browse the repository at this point in the history

  36. Add demos, preprocess quantifiers, disable fix_quantifiers optimization

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    d0e938f View commit details
    Browse the repository at this point in the history

  37. Add a simple demo with struct as an argument to an obligation

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    7b52866 View commit details
    Browse the repository at this point in the history

  38. Add leak checks to poly. VIR and generate them also in loops

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    1aab38c View commit details
    Browse the repository at this point in the history

  39. Fix compile errors from last update

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    0ef8d03 View commit details
    Browse the repository at this point in the history

  40. Revert import reformatting in procedure encoder

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    a3a5802 View commit details
    Browse the repository at this point in the history

  41. Revert reformatting of the first half of the procedure encoder

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    efefb87 View commit details
    Browse the repository at this point in the history

  42. A few things missed in last commit

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    8d8bcfb View commit details
    Browse the repository at this point in the history

  43. Revert the rest of reformatting in procedure encoder

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    1543569 View commit details
    Browse the repository at this point in the history

  44. Revert remaining reformatting

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    5c397d7 View commit details
    Browse the repository at this point in the history

  45. Add back an accidentally removed trace! invocation

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    3cd5691 View commit details
    Browse the repository at this point in the history

  46. Don't include guard in loop invariant if it inhales an impure expression

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    3042a5a View commit details
    Browse the repository at this point in the history

  47. Fix folding optimization for obligations, add pass tests for obligations

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    0e67084 View commit details
    Browse the repository at this point in the history

  48. Replace leak check statements by leak check expressions

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    cb9563b View commit details
    Browse the repository at this point in the history

  49. Remove commented code from obligation parsing

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    44c17cd View commit details
    Browse the repository at this point in the history

  50. Autoformat

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    45eb0f7 View commit details
    Browse the repository at this point in the history

  51. Satisfy Clippy

    @vfukala
    vfukala committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    088df18 View commit details
    Browse the repository at this point in the history

Commits on Jun 29, 2023

  1. Fix method purifier crash due to forperm

    @vfukala
    vfukala committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    e9be356 View commit details
    Browse the repository at this point in the history

Commits on Jul 2, 2023

  1. Revert back to leak check statements in VIR; correctly report obligat… 

    …ion verification errors
    @vfukala
    vfukala committed Jul 2, 2023
    Configuration menu
    Copy the full SHA
    6bb8e38 View commit details
    Browse the repository at this point in the history

  2. Fix a missing check before adding a loop guard to the invariant

    @vfukala
    vfukala committed Jul 2, 2023
    Configuration menu
    Copy the full SHA
    c132824 View commit details
    Browse the repository at this point in the history

Commits on Jul 3, 2023

  1. Only split quantifiers if body impure; check for and report misplaced… 

    … impure exprs
    @vfukala
    vfukala committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    52d4641 View commit details
    Browse the repository at this point in the history

Commits on Jul 4, 2023

  1. Properly attach position info to float backend functions; move viperp… 

    …roject#729 to pass; bump specs version
    @vfukala
    vfukala committed Jul 4, 2023
    Configuration menu
    Copy the full SHA
    cab9aa2 View commit details
    Browse the repository at this point in the history

Commits on Jul 6, 2023

  1. Proper error reporting for 'not enough resources' verification errors

    @vfukala
    vfukala committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    4007982 View commit details
    Browse the repository at this point in the history

  2. Fix err. mngr. misconfig, improve obl. arg. err. msg, add simple obl.… 

    … fail tests
    @vfukala
    vfukala committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    935fa33 View commit details
    Browse the repository at this point in the history

Commits on Jul 7, 2023

  1. Add some obligation loop fail tests, fix error manager for TR

    @vfukala
    vfukala committed Jul 7, 2023
    Configuration menu
    Copy the full SHA
    ea06554 View commit details
    Browse the repository at this point in the history

  2. Fix error manager

    @vfukala
    vfukala committed Jul 7, 2023
    Configuration menu
    Copy the full SHA
    7d2a265 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'upstream/master' into simplest-obligation

    @vfukala
    vfukala committed Jul 7, 2023
    Configuration menu
    Copy the full SHA
    78f7664 View commit details
    Browse the repository at this point in the history

  4. Fix error manager again?

    @vfukala
    vfukala committed Jul 7, 2023
    Configuration menu
    Copy the full SHA
    70882ce View commit details
    Browse the repository at this point in the history

  5. Try disabling verification cache

    @vfukala
    vfukala committed Jul 7, 2023
    Configuration menu
    Copy the full SHA
    b5e2447 View commit details
    Browse the repository at this point in the history

  6. Revert supposed error managers fixes

    @vfukala
    vfukala committed Jul 7, 2023
    Configuration menu
    Copy the full SHA
    1294196 View commit details
    Browse the repository at this point in the history

  7. Add not enough resources for precondition err. msg., add obl. tests

    @vfukala
    vfukala committed Jul 7, 2023
    Configuration menu
    Copy the full SHA
    78b83f5 View commit details
    Browse the repository at this point in the history

Commits on Jul 8, 2023

  1. Correctly report quantified-resource-not-injective errors

    @vfukala
    vfukala committed Jul 8, 2023
    Configuration menu
    Copy the full SHA
    c7b13e8 View commit details
    Browse the repository at this point in the history

  2. Autoformat

    @vfukala
    vfukala committed Jul 8, 2023
    Configuration menu
    Copy the full SHA
    1a54d12 View commit details
    Browse the repository at this point in the history

  3. Remove mistakenly added file

    @vfukala
    vfukala committed Jul 8, 2023
    Configuration menu
    Copy the full SHA
    1e86dc5 View commit details
    Browse the repository at this point in the history

Commits on Jul 9, 2023

  1. Generate Viper assumes instead of inhales for prusti_assume!

    @vfukala
    vfukala committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    654049f View commit details
    Browse the repository at this point in the history

  2. Add prusti_exhale and prusti_inhale (no error reporting yet)

    @vfukala
    vfukala committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    006413e View commit details
    Browse the repository at this point in the history

  3. Consolidate direct specs, add error reporting and tests for them

    @vfukala
    vfukala committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    0463263 View commit details
    Browse the repository at this point in the history

  4. Autoformat

    @vfukala
    vfukala committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    281e5b7 View commit details
    Browse the repository at this point in the history

  5. Rewrite QP desugaring, tweak SwichInt terminator encoding

    @vfukala
    vfukala committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    8eeaf4c View commit details
    Browse the repository at this point in the history

  6. Copy elimination of double Not in spec encoding from viperproject#1411

    @vfukala
    vfukala committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    197eeab View commit details
    Browse the repository at this point in the history

Commits on Jul 10, 2023

  1. Tweak generation of conditionals for better misplaced impure err. rep.

    @vfukala
    vfukala committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    130364a View commit details
    Browse the repository at this point in the history

  2. Temporarily revert double Not elimination; wait for viperproject#1411 … 

    …to fix errors

This reverts commit 197eeab.
    @vfukala
    vfukala committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    b1ea85f View commit details
    Browse the repository at this point in the history

Commits on Jul 13, 2023

  1. Unify with TR

    @vfukala
    vfukala committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    57a2032 View commit details
    Browse the repository at this point in the history

  2. Allow doc attributes in resources/obligations

    @vfukala
    vfukala committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    4314482 View commit details
    Browse the repository at this point in the history

Commits on Jul 14, 2023

  1. More misplaced impr. checks; move QR desugaring to a separate module

    @vfukala
    vfukala committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    133a75f View commit details
    Browse the repository at this point in the history

  2. Report spec-only items in non-spec code

    @vfukala
    vfukala committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    ce05b40 View commit details
    Browse the repository at this point in the history

  3. Update tests for predicates in non-spec code

    @vfukala
    vfukala committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    64aff6d View commit details
    Browse the repository at this point in the history

Commits on Jul 15, 2023

  1. Fix a test with time_credits in non-spec code

    @vfukala
    vfukala committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    10d977f View commit details
    Browse the repository at this point in the history

  2. Add resources, obligations, and time reasoning to user guide

    @vfukala
    vfukala committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    600a4b0 View commit details
    Browse the repository at this point in the history

  3. Add missing ignore to snippets in the user guide

    @vfukala
    vfukala committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    e114508 View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2023

  1. Temporarily remove snap from spec-only checks

    @vfukala
    vfukala committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    7b772d1 View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2023

  1. Patch resources in pure function contracts

    @vfukala
    vfukala committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    5ce5d14 View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2023

  1. Fix stack overflow for non-trusted functions calling themselves in th… 

    …eir contracts
    @vfukala
    vfukala committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    aeeea30 View commit details
    Browse the repository at this point in the history

Commits on Jul 28, 2023

  1. Merge remote-tracking branch 'upstream/master' into simplest-obligation

    @vfukala
    vfukala committed Jul 28, 2023
    Configuration menu
    Copy the full SHA
    54e0d9b View commit details
    Browse the repository at this point in the history

  2. Bump prusti-contracts versions

    @vfukala
    vfukala committed Jul 28, 2023
    Configuration menu
    Copy the full SHA
    6a625e6 View commit details
    Browse the repository at this point in the history

  3. Cleanup

    @vfukala
    vfukala committed Jul 28, 2023
    Configuration menu
    Copy the full SHA
    79d4868 View commit details
    Browse the repository at this point in the history