Skip to content

Releases: viperproject/viper-ide

v4.4.2 (August 2024 release)

11 Sep 18:38
6395b51
Compare
Choose a tag to compare

Release 2024.8

Date 31/08/24

Changes in Viper Language

  • Domain axioms can now refer to functions that have decreases clauses (but no preconditions) viperproject/silver#802

API Changes and Internal Improvements

Bug Fixes

Backend-specific Upgrades/Changes

Symbolic Execution Backend (Silicon)

  • Added experimental support for (command line) verification debugging. With the new option --enableDebugging, users can see the state (store, heap, branch conditions and assumptions) in a format that that can be understood on the Viper level (avoiding internal Silicon concepts) at the point where a verification error occurs, locally assert or assume expressions to debug the error, and change SMT solver options. viperproject/silicon#863
  • Soundness fixes:
  • Completeness improvements:
  • Performance improvements:
    • Improved snapshot map caching for quantified permissions (also improves completeness) viperproject/silicon#846
    • Avoiding creating new snapshot maps for quantified resources when unnecessary viperproject/silicon#839
    • Eagerly assuming non-aliasing for quantified field chunks viperproject/silicon#835
    • More efficient function axiomatization for functions with many branches viperproject/silicon#808
    • Flexible path joining options:
      • With command line argument --moreJoins=1, Silicon joins only branches stemming from impure implications (immediately after branching). With --moreJoins=2 it joins all branches, including branches stemming from program control flow, at the earliest possible point. viperproject/silicon#823
      • The new annotation @moreJoins(n), with n bein 1 or 2 as just described, can be used to enable path joining on a per-method level viperproject/silicon#823
    • More flexible state consolidation:
  • Other improvements:

Verification Condition Generation Backend (Carbon)

Based on

Nightly Release v-2024-03-29-0722

29 Mar 07:22
18c97cd
Compare
Choose a tag to compare
Pre-release

Based on

Nightly Release v-2024-03-27-0722

27 Mar 07:22
18c97cd
Compare
Choose a tag to compare
Pre-release

Based on

Nightly Release v-2024-03-26-0721

26 Mar 07:21
f6f1009
Compare
Choose a tag to compare
Pre-release

Based on

Nightly Release v-2024-03-24-0722

24 Mar 07:22
f6f1009
Compare
Choose a tag to compare
Pre-release

Based on

Nightly Release v-2024-03-23-0722

23 Mar 07:22
f6f1009
Compare
Choose a tag to compare
Pre-release

Based on

Nightly Release v-2024-03-18-0722

18 Mar 07:22
f6f1009
Compare
Choose a tag to compare
Pre-release

Based on

Nightly Release v-2024-03-17-0721

17 Mar 07:21
f6f1009
Compare
Choose a tag to compare
Pre-release

Based on

Nightly Release v-2024-03-15-0723

15 Mar 07:23
f6f1009
Compare
Choose a tag to compare
Pre-release

Based on

v4.3.1 (January 2024 release)

19 Feb 21:01
197805c
Compare
Choose a tag to compare

Release 2024.1

Date 19/02/24

Changes in Viper Language

  • unfold, fold, and unfolding now require a strictly positive permission amount (i.e., none is no longer allowed) (Silicon#754) and (Carbon#469). This fixes an unsoundness (Silver#444). A new error reason NonPositivePermission is reported if this condition is not satisfied (Silver#744).
  • When generic functions are used inside axioms of their own domain and the type arguments are not constrained, Viper no longer uses Int as the type argument, but instead uses the domain's type parameter itself (i.e., it states that the axiom must hold for all type arguments). (Silver#758)
  • Functions can be annotated as @opaque(), which means that their definitions are not available by default. For opaque functions, any use of the function can be annotated with @reveal() to make the definition available for that specific function application. (Silicon#767) and (Carbon#474)

API changes:

  • The classes ErrorReason and VerificationError are now sealed. Code that extended them must now extend ExtensionAbstractVerificationError and ExtensionAbstractErrorReason, respectively. (Silver#749)
  • The ParseAST has been heavily reworked, which may require adaptations in plugins that work on the ParseAST level. Additionally, the order of constructor arguments of the PredicateInstance class in the predicate instance plugin has been switched. (Silver#764)

Changes in plugins:

  • Viper now includes a new smoke detection plugin that automatically checks if e.g. preconditions are unsatisfiable or branches are reachable by inserting refute false in various locations in the program. The plugin is not enabled by default. (Silver#762)
  • The ADT plugin now automatically generates well-foundedness axioms for each declared ADT type if the termination plugin is used, s.t. ADT values can be used as termination measures without the user having to declare them. (Silver#743)
  • Two bug fixes in the termination plugin:
    • An incompleteness in the termination plugin affecting functions whose preconditions contain quantified permissions has been fixed (Silver#754)
    • decreases clauses with predicate instances can now be written anywhere in function specifications (previously could not be after the postcondition) (Silver#738)
  • Fixed a bug in the refute plugin that prevented it from working inside loops in Carbon (Silver#736)

Other Viper-level improvements:

  • Substantially improved parsing and type checking errors (as well as parsing performance) (Silver#764)
  • Fixed a bug where domain axioms were not instantiated for all relevant cases (Silver#742)
  • Two improvements in trigger inference:
    • Proper treatment of let-expressions when generating triggers (Silver#753)
    • Trigger inference no longer incorrectly omits old (Silver#747)

Backend-specific Upgrades/Changes

Symbolic Execution Backend (Silicon)

  • Soundness fixes:
    • Fixed a long-standing unsoundness and incompleteness related to packaging magic wands (Silicon#757)
    • Fixed an incorrect well-definedness check of branch conditions inside goto-loops (Silicon#774)
    • Fixed a missing check for map lookups (Silicon#770)
  • Completeness improvements:
    • Silicon now uses Carbon's more complete axiomatization for sequences, sets and multisets. This usually comes with little or no performance cost, but we have observed individual examples where the new axioms caused non-termination or significantly worse verification time. We would be very grateful if users who observe additional examples where the new axiomatization leads to severe problems filed issues or sent us the problematic examples in some other way. Silicon's old axiomatization is still available and can be used via the command line option --useOldAxiomatization. (Silicon#642)
    • Fixed an incompleteness when exhaling a quantified permission with a permission amount that depends on the quantified variable inside a package block (Silicon#797)
    • Fixed an issue where a function definition was available too late (Silicon#744)
    • Two completeness improvements of exhale mode 1 (aka moreCompleteExhale) (Silicon#760) and (Silicon#795)
  • Fixed crashes:
    • when using Z3 via its API and interpreted functions (Silicon#752)
    • when using predicate or wand triggers inside functions (Silicon#759)
  • Performance improvements
    • More consistent caching for quantified permissions (Silicon#792)
    • Better heuristics for quantified permissions (Silicon#789)
  • Other improvements
    • Added a command line flag --disableNL to easily disable non-linear integer arithmetic reasoning in Z3 (Silicon#783)
    • Added support for an experimental method annotation @proverArgs(key=value) that allows setting Z3 configuration parameters on a per-method basis (Silicon#784)
    • Fixed incorrect branch conditions in symbolic execution log (Silicon#790)

Verification Condition Generation Backend (Carbon)

  • Soundness fixes:

    • Exhaling quantified magic wands is now sound (Carbon#473)
  • Other improvements:

    • Added support for several missing features: (Carbon#473)
      • quantified magic wands
      • magic wands as triggers
      • perm for magic wands
      • forperm with more than one quantified variable
      • forperm for magic wands
    • Added a command line option --timeout=n to set an overall verification timeout (in seconds) (Carbon#483)
    • Several internal encoding improvements:

Based on