v4.4.2 (August 2024 release)

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

• Improved Simplifier simplifies many additional expressions; new option determines whether simplification must preserve well-definedness viperproject/silver#810
• Chopper is now aware of opaque functions viperproject/silver#779
• Chopper has improved dependency analysis for axioms viperproject/silver#776
• Removed filtering of duplicate errors inside Viper (this is now left to frontends) viperproject/silver#778

Bug Fixes

• Fixed various issues with macro expansion:
  • Fixed incorrect variable renaming during macro expansion viperproject/silver#804
  • Disallowing nested macro declarations viperproject/silver#795
  • Fixed incorrect renaming of label statements during macro expansion viperproject/silver#793
• Fixed incorrect Simplifier handling of division and modulo expressions viperproject/silver#794
• Fixed crash in proof obligation computation for expressions viperproject/silver#783
• Termination plugin: Improved encoding of checks for unfolding-expressions viperproject/silver#773
• ADT plugin: Fixed crash when plugin is used with other AST extensions viperproject/silver#800

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:
  • Fixed unsound rewrite for --conditionalizePermissions option viperproject/silicon#853
  • Fixed unsound handling of quantified permissions with unsatisfiable condition viperproject/silicon#843
  • Fixed unsound handling of quantified permissions with trivial condition viperproject/silicon#834
  • Improved encoding of magic wand snapshots that prevents unsoundness for applying-expressions viperproject/silicon#836
  • Fixed incorrect order of function precondition assumptions viperproject/silicon#811
• Completeness improvements:
  • Recording missing constraints during function verification viperproject/silicon#852 and viperproject/silicon#825
  • Fixed treatment of snapshot maps defined while evaluating quantifiers viperproject/silicon#840
  • Avoiding using a quantifier for wildcard constraints for quantified resources when possible viperproject/silicon#817
• 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:
    • Added several new options for state consolidation behavior viperproject/silicon#827
    • The new annotation @stateConsolidationMode(n) allows configuring state consolidation on a per-method level viperproject/silicon#827
• Other improvements:
  • Fixed crash resulting from double-declarations of macros with --parallelizeBranches viperproject/silicon#813
  • Fixed error reporting for method call arguments viperproject/silicon#841
  • Silicon now tries to find the Z3 executable in PATH if no path is explicitly provided viperproject/silicon#818

Verification Condition Generation Backend (Carbon)

• Bug fixes:
  • Preventing Boogie crash when using annotations viperproject/carbon#505

Based on

• ViperServer release v.24.08-release
• Z3 4.8.7
• Boogie release 7449a7a899c02c95

Nightly Release v-2024-03-29-0722

Based on

• ViperServer release v-2024-03-29-0713
• Z3 4.8.7
• Boogie release latest

Nightly Release v-2024-03-27-0722

Based on

• ViperServer release v-2024-03-27-0713
• Z3 4.8.7
• Boogie release latest

Nightly Release v-2024-03-26-0721

Based on

• ViperServer release v-2024-03-26-0713
• Z3 4.8.7
• Boogie release latest

Nightly Release v-2024-03-24-0722

Based on

• ViperServer release v-2024-03-24-0713
• Z3 4.8.7
• Boogie release latest

Nightly Release v-2024-03-23-0722

Based on

• ViperServer release v-2024-03-23-0713
• Z3 4.8.7
• Boogie release latest

Nightly Release v-2024-03-18-0722

Based on

• ViperServer release v-2024-03-18-0713
• Z3 4.8.7
• Boogie release latest

Nightly Release v-2024-03-17-0721

Based on

• ViperServer release v-2024-03-17-0713
• Z3 4.8.7
• Boogie release latest

Nightly Release v-2024-03-15-0723

Based on

• ViperServer release v-2024-03-15-0713
• Z3 4.8.7
• Boogie release latest

v4.3.1 (January 2024 release)

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:
    • Improved encoding of the old state (Carbon#482)
    • Improved encoding of if statements (Carbon#478)
    • Improved encoding of method calls (Carbon#477)

Based on

• ViperServer release v.24.01-release
• Z3 4.8.7
• Boogie release latest