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