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

Credit Specification Parsing & Encoding #559

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

Credit Specification Parsing & Encoding #559

wants to merge 77 commits into from

Commits on Jun 15, 2021

  1. First version of preparser addition for credit polynomials

    ELowis committed Jun 15, 2021
    Configuration menu
    Copy the full SHA
    093f07e View commit details
    Browse the repository at this point in the history

  2. bug fix nested parse_terminated

    ELowis committed Jun 15, 2021
    Configuration menu
    Copy the full SHA
    29996e3 View commit details
    Browse the repository at this point in the history

  3. added credit polynomial to untyped & json

    ELowis committed Jun 15, 2021
    Configuration menu
    Copy the full SHA
    daa4d37 View commit details
    Browse the repository at this point in the history

  4. structural to typed conversion for credit polynomial

    ELowis committed Jun 15, 2021
    Configuration menu
    Copy the full SHA
    0c27106 View commit details
    Browse the repository at this point in the history

  5. removed TODO

    ELowis committed Jun 15, 2021
    Configuration menu
    Copy the full SHA
    7838a3e View commit details
    Browse the repository at this point in the history

Commits on Jun 19, 2021

  1. added first encoding of credit specifications

    @ELowis
    ELowis committed Jun 19, 2021
    Configuration menu
    Copy the full SHA
    ef2ee2c View commit details
    Browse the repository at this point in the history

Commits on Jun 21, 2021

  1. removed artifacts from older changes

    @ELowis
    ELowis committed Jun 21, 2021
    Configuration menu
    Copy the full SHA
    de2c26e View commit details
    Browse the repository at this point in the history

  2. resolved linter issues

    @ELowis
    ELowis committed Jun 21, 2021
    Configuration menu
    Copy the full SHA
    e147bb9 View commit details
    Browse the repository at this point in the history

Commits on Jun 22, 2021

  1. fixed more linter issues

    @ELowis
    ELowis committed Jun 22, 2021
    Configuration menu
    Copy the full SHA
    162a430 View commit details
    Browse the repository at this point in the history

Commits on Jul 2, 2021

  1. exhale precondition for call, removed TODOs & credits function in pru… 

    …sti-contracts
    @ELowis
    ELowis committed Jul 2, 2021
    Configuration menu
    Copy the full SHA
    8146ccb View commit details
    Browse the repository at this point in the history

Commits on Jul 6, 2021

  1. added unexpected errorctxt for type spec exhale

    @ELowis
    ELowis committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    434c7fb View commit details
    Browse the repository at this point in the history

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

    # Conflicts:
#	prusti-specs/src/specifications/preparser.rs
    @ELowis
    ELowis committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    baa73ea View commit details
    Browse the repository at this point in the history

Commits on Jul 7, 2021

  1. finish merging with new parser

    @ELowis
    ELowis committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    fd3881e View commit details
    Browse the repository at this point in the history

  2. fix minor merge issues

    @ELowis
    ELowis committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    531873e View commit details
    Browse the repository at this point in the history

Commits on Jul 13, 2021

  1. added assertion folder

    @ELowis
    ELowis committed Jul 13, 2021
    Configuration menu
    Copy the full SHA
    2f0b5c3 View commit details
    Browse the repository at this point in the history

  2. first prototype with exhale of abstract terms

    @ELowis
    ELowis committed Jul 13, 2021
    Configuration menu
    Copy the full SHA
    1787bdc View commit details
    Browse the repository at this point in the history

  3. use user-provided ids for coefficient functions

    @ELowis
    ELowis committed Jul 13, 2021
    Configuration menu
    Copy the full SHA
    073bc92 View commit details
    Browse the repository at this point in the history

Commits on Jul 14, 2021

  1. added support to use abstract coefficients in annotations

    @ELowis
    ELowis committed Jul 14, 2021
    Configuration menu
    Copy the full SHA
    1e01bd5 View commit details
    Browse the repository at this point in the history

  2. bug fix flag for precondition

    @ELowis
    ELowis committed Jul 14, 2021
    Configuration menu
    Copy the full SHA
    7040daa View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'upstream/master' into abstract_precondi… 

    …tions
    @ELowis
    ELowis committed Jul 14, 2021
    Configuration menu
    Copy the full SHA
    03daa2f View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2021

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

    # Conflicts:
#	prusti-interface/src/specs/typed.rs
#	prusti-specs/src/specifications/preparser.rs
    @ELowis
    ELowis committed Jul 18, 2021
    Configuration menu
    Copy the full SHA
    40f7d53 View commit details
    Browse the repository at this point in the history

  2. adapted to merge changes

    @ELowis
    ELowis committed Jul 18, 2021
    Configuration menu
    Copy the full SHA
    317b53b View commit details
    Browse the repository at this point in the history

Commits on Jul 28, 2021

  1. fix construction of abstract terms (ALL smaller exponents)

    @ELowis
    ELowis committed Jul 28, 2021
    Configuration menu
    Copy the full SHA
    e8c9d2d View commit details
    Browse the repository at this point in the history

  2. fix credit power variable transfer into typed assertion; use expressi… 

    …on instead of Arg
    @ELowis
    ELowis committed Jul 28, 2021
    Configuration menu
    Copy the full SHA
    ea5dcf0 View commit details
    Browse the repository at this point in the history

Commits on Aug 9, 2021

  1. First cost encoder version with type map

    @ELowis
    ELowis committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    7e3690e View commit details
    Browse the repository at this point in the history

Commits on Aug 11, 2021

  1. cost encoder with condition -> type mapping to fix empty branches & u… 

    …se ordered maps for deterministic behaviour
    @ELowis
    ELowis committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    39db16e View commit details
    Browse the repository at this point in the history

  2. fix predicate def to exclude negative perm amount

    @ELowis
    ELowis committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    2c2df6f View commit details
    Browse the repository at this point in the history

  3. Extended VIR Exprs for asymp bound check (predicate instance & perm e… 

    …quality)
    @ELowis
    ELowis committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    19c1193 View commit details
    Browse the repository at this point in the history

  4. supertype for mir interpreter with substitution

    @ELowis
    ELowis committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    bbd2819 View commit details
    Browse the repository at this point in the history

  5. lib & mod

    @ELowis
    ELowis committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    d067753 View commit details
    Browse the repository at this point in the history

  6. removed 1 TODO

    @ELowis
    ELowis committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    2be41ac View commit details
    Browse the repository at this point in the history

  7. added cost encoder to precondition encoding

    @ELowis
    ELowis committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    b6089fc View commit details
    Browse the repository at this point in the history

  8. cleanup procedure encoder

    @ELowis
    ELowis committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    86e5c88 View commit details
    Browse the repository at this point in the history

  9. Merge remote-tracking branch 'upstream/master' into cost_inference 

    # Conflicts:
#	prusti-common/src/vir/to_viper.rs
#	prusti-viper/src/encoder/encoder.rs
#	prusti-viper/src/encoder/mod.rs
#	prusti-viper/src/encoder/procedure_encoder.rs
#	prusti-viper/src/encoder/pure_function_encoder.rs
#	vir/src/legacy/ast/expr.rs
#	vir/src/legacy/ast/predicate.rs
    @ELowis
    ELowis committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    5399624 View commit details
    Browse the repository at this point in the history

Commits on Aug 12, 2021

  1. adapt to merge changes

    @ELowis
    ELowis committed Aug 12, 2021
    Configuration menu
    Copy the full SHA
    8ec3689 View commit details
    Browse the repository at this point in the history

  2. comment unused in cost_encoder

    @ELowis
    ELowis committed Aug 12, 2021
    Configuration menu
    Copy the full SHA
    cc4ad2a View commit details
    Browse the repository at this point in the history

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

    # Conflicts:
#	prusti-common/src/vir/to_viper.rs
    @ELowis
    ELowis committed Aug 12, 2021
    Configuration menu
    Copy the full SHA
    85c9efa View commit details
    Browse the repository at this point in the history

  4. fix some linter issues

    @ELowis
    ELowis committed Aug 12, 2021
    Configuration menu
    Copy the full SHA
    288e515 View commit details
    Browse the repository at this point in the history

Commits on Aug 13, 2021

  1. fix more linter issues

    @ELowis
    ELowis committed Aug 13, 2021
    Configuration menu
    Copy the full SHA
    b14348b View commit details
    Browse the repository at this point in the history

  2. Allow encoding error in substitution & use single substitution fn

    @ELowis
    ELowis committed Aug 13, 2021
    Configuration menu
    Copy the full SHA
    d8b2811 View commit details
    Browse the repository at this point in the history

Commits on Aug 17, 2021

  1. added more substitutions to cost inference

    @ELowis
    ELowis committed Aug 17, 2021
    Configuration menu
    Copy the full SHA
    65f954b View commit details
    Browse the repository at this point in the history

  2. added credit access predicate to more visitors in expr

    @ELowis
    ELowis committed Aug 17, 2021
    Configuration menu
    Copy the full SHA
    331e777 View commit details
    Browse the repository at this point in the history

  3. remove post condition from coeff functions

    @ELowis
    ELowis committed Aug 17, 2021
    Configuration menu
    Copy the full SHA
    ccbbeb3 View commit details
    Browse the repository at this point in the history

  4. collect required permissions inside new expressions, removed some TOD… 

    …Os in footprint
    @ELowis
    ELowis committed Aug 17, 2021
    Configuration menu
    Copy the full SHA
    c187967 View commit details
    Browse the repository at this point in the history

  5. added commas for fmt checker

    @ELowis
    ELowis committed Aug 17, 2021
    Configuration menu
    Copy the full SHA
    d86bc29 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'upstream/master' into cost_folding

    @ELowis
    ELowis committed Aug 17, 2021
    Configuration menu
    Copy the full SHA
    4d56f72 View commit details
    Browse the repository at this point in the history

Commits on Aug 18, 2021

  1. remove SnapApps

    @ELowis
    ELowis committed Aug 18, 2021
    Configuration menu
    Copy the full SHA
    a0502ca View commit details
    Browse the repository at this point in the history

Commits on Aug 19, 2021

  1. store credit conversions for each substitution

    @ELowis
    ELowis committed Aug 19, 2021
    Configuration menu
    Copy the full SHA
    c1dfbb3 View commit details
    Browse the repository at this point in the history

  2. change cost encoder interface, store results for use in procedure enc… 

    …oder
    @ELowis
    ELowis committed Aug 19, 2021
    Configuration menu
    Copy the full SHA
    96bc2f1 View commit details
    Browse the repository at this point in the history

Commits on Aug 27, 2021

  1. ErrorCtxt for asymp bound check & fix checked exponents

    @ELowis
    ELowis committed Aug 27, 2021
    Configuration menu
    Copy the full SHA
    032cb10 View commit details
    Browse the repository at this point in the history

  2. (temporarily) extend CfgMethod with viper pre- & postconditions & for… 

    …mal_args
    @ELowis
    ELowis committed Aug 27, 2021
    Configuration menu
    Copy the full SHA
    be86187 View commit details
    Browse the repository at this point in the history

  3. (temporarily) allow CfgMethod to have no body

    @ELowis
    ELowis committed Aug 27, 2021
    Configuration menu
    Copy the full SHA
    81fcf53 View commit details
    Browse the repository at this point in the history

  4. allow method calls to have arguments & no target

    @ELowis
    ELowis committed Aug 27, 2021
    Configuration menu
    Copy the full SHA
    edad115 View commit details
    Browse the repository at this point in the history

  5. move sorting of credit predicate args to method side

    @ELowis
    ELowis committed Aug 27, 2021
    Configuration menu
    Copy the full SHA
    6bac4c7 View commit details
    Browse the repository at this point in the history

  6. simplify credit predicate hierarchy & add _ in name

    @ELowis
    ELowis committed Aug 27, 2021
    Configuration menu
    Copy the full SHA
    2734034 View commit details
    Browse the repository at this point in the history

  7. fix: add predicate instance to used predicate collector

    @ELowis
    ELowis committed Aug 27, 2021
    Configuration menu
    Copy the full SHA
    2c5d2af View commit details
    Browse the repository at this point in the history

  8. add stmts to fold & unfold credits

    @ELowis
    ELowis committed Aug 27, 2021
    Configuration menu
    Copy the full SHA
    38055b2 View commit details
    Browse the repository at this point in the history

  9. store partial conversion & const_val & fix replacement

    @ELowis
    ELowis committed Aug 27, 2021
    Configuration menu
    Copy the full SHA
    011c70f View commit details
    Browse the repository at this point in the history

  10. fix func preconditions for call

    @ELowis
    ELowis committed Aug 27, 2021
    Configuration menu
    Copy the full SHA
    945d09e View commit details
    Browse the repository at this point in the history

  11. fix overwrite of conversions if multiple substititutions at 1 location

    @ELowis
    ELowis committed Aug 27, 2021
    Configuration menu
    Copy the full SHA
    f7171ff View commit details
    Browse the repository at this point in the history

  12. encode credit conversions

    @ELowis
    ELowis committed Aug 27, 2021
    Configuration menu
    Copy the full SHA
    bfad5e8 View commit details
    Browse the repository at this point in the history

Commits on Aug 29, 2021

  1. remove unnecessary comments

    @ELowis
    ELowis committed Aug 29, 2021
    Configuration menu
    Copy the full SHA
    6ebe60b View commit details
    Browse the repository at this point in the history

  2. fix unconditional bound combinations

    @ELowis
    ELowis committed Aug 29, 2021
    Configuration menu
    Copy the full SHA
    993268e View commit details
    Browse the repository at this point in the history

  3. add config flags for conditional inference & verify conversions

    @ELowis
    ELowis committed Aug 29, 2021
    Configuration menu
    Copy the full SHA
    64b9cdc View commit details
    Browse the repository at this point in the history

  4. added parser support for asymptotic spec

    @ELowis
    ELowis committed Aug 29, 2021
    Configuration menu
    Copy the full SHA
    5025736 View commit details
    Browse the repository at this point in the history

  5. fix coeff id & allow O(1)

    @ELowis
    ELowis committed Aug 29, 2021
    Configuration menu
    Copy the full SHA
    e15c777 View commit details
    Browse the repository at this point in the history

  6. bug fix: also union conversions from otherwise branch

    @ELowis
    ELowis committed Aug 29, 2021
    Configuration menu
    Copy the full SHA
    52601ed View commit details
    Browse the repository at this point in the history

  7. bug fix: added conditional conversions

    @ELowis
    ELowis committed Aug 29, 2021
    Configuration menu
    Copy the full SHA
    0c64436 View commit details
    Browse the repository at this point in the history

Commits on Aug 30, 2021

  1. bug fix: also detect constants inside SnapApps

    @ELowis
    ELowis committed Aug 30, 2021
    Configuration menu
    Copy the full SHA
    218f7f7 View commit details
    Browse the repository at this point in the history

Commits on Aug 31, 2021

  1. added proper support for constant subtractions with neg predicates

    @ELowis
    ELowis committed Aug 31, 2021
    Configuration menu
    Copy the full SHA
    91b50de View commit details
    Browse the repository at this point in the history

  2. cleanup & comments

    @ELowis
    ELowis committed Aug 31, 2021
    Configuration menu
    Copy the full SHA
    2525632 View commit details
    Browse the repository at this point in the history

Commits on Sep 1, 2021

  1. only run conditional inference if there is a conditional annotation

    @ELowis
    ELowis committed Sep 1, 2021
    Configuration menu
    Copy the full SHA
    df1fbc7 View commit details
    Browse the repository at this point in the history

  2. added termination check with existential (not really working)

    @ELowis
    ELowis committed Sep 1, 2021
    Configuration menu
    Copy the full SHA
    6c0daa6 View commit details
    Browse the repository at this point in the history

Commits on Oct 7, 2021

  1. more tracing in cost encoder

    @ELowis
    ELowis committed Oct 7, 2021
    Configuration menu
    Copy the full SHA
    060128e View commit details
    Browse the repository at this point in the history

  2. conditional control only via flag

    @ELowis
    ELowis committed Oct 7, 2021
    Configuration menu
    Copy the full SHA
    ce3459f View commit details
    Browse the repository at this point in the history

  3. added sub place-place conversion & inlining conversions (ugly)

    @ELowis
    ELowis committed Oct 7, 2021
    Configuration menu
    Copy the full SHA
    0f0e3f3 View commit details
    Browse the repository at this point in the history

  4. (bug fix): substitute pure function calls in conditions

    @ELowis
    ELowis committed Oct 7, 2021
    Configuration menu
    Copy the full SHA
    3836f06 View commit details
    Browse the repository at this point in the history