Merge branch 'master' into error-improvements

ReleaseNotes.md

@@ -1,3 +1,85 @@
+## Release 2023.7
+
+**Date 31/07/23**
+
+### Changes in Viper Language
+
+- Improved language flexibility ([Silver#685](https://github.com/viperproject/silver/pull/685)): The syntax of declarations and assignments is now more permissive, allowing, for example, multiple declarations at once:
+  ```
+  field n: Ref, m: Ref  // Declare multiple fields at once
+  var a: Ref, b: Ref, c: Int  // Declare multiple locals at once
+  ```
+  Additionally, method calls and new statements can now have fields or newly-declared local variables on their left hand side:
+  ```
+  var f: Ref := new(n)                   // Declare and initialise locals with `new`
+  a, f.n := get_refs()                   // Assign to field from method call
+  f.n := new(n)                          // Assign to field with `new`
+  ```
+  The Viper AST remains unchanged; the newly-supported syntax is desugared into equivalent code that uses the existing Viper AST.
+- Annotations ([Silver#666](https://github.com/viperproject/silver/pull/666)): The Viper language now has support for annotations on statements, expressions, and top-level declarations. The syntax for an annotation is ``@key("value", "value2", ...)``, i.e., they have a key which is preceded by an ``@`` sign and a sequence of values written as comma-separated string literals. A single expression/statement/declaration can have multiple annotations. If there are two annotations of the same key, their value sequences are concatenated. In the AST, annotations are represented in the ``info`` field of the annotated AST node using an ``AnnotationInfo`` object.
+  Currently, there are two supported annotations: ``@weight("n")`` on quantifiers, where ``n`` is a positive integer, sets the weight of the quantifier in the SMT solver.
+  The second annotation is exclusive to the Symbolic Execution backend (see below).
+  Unknown annotations are ignored.
+- Domain axioms may now refer to non-domain functions that do not have any preconditions ([Silver#698](https://github.com/viperproject/silver/pull/698)).
+- Support for chained comparisons ([Silver#713](https://github.com/viperproject/silver/pull/713)): expressions like ``e1 < e2 <= e3 > e4`` can now be parsed and will be desugared to ``(e1 < e2) && (e2 <= e3) && (e3 > e4)``. The AST nodes for comparison operations remain unchanged.
+- Two important changes in the termination plugin:
+  - The termination plugin now enforces that functions that refer to themselves (or to other functions that call the original function in a mutually-recursive way) in their own postconditions have a ``decreases`` clause ([Silver#711](https://github.com/viperproject/silver/pull/711)). That is, for such functions, one must either prove termination using a ``decreases`` clause, or explicitly state that termination should be assumed by writing ``decreases *``.
+    This change addresses frequent issues where users wrote functions that are not well-defined using such postconditions and subsequently reported seemingly unsound behavior (e.g., ([Silver#525](https://github.com/viperproject/silver/issues/525)) and ([Silver#668](https://github.com/viperproject/silver/issues/668))).
+  - The termination plugin now automatically imports the default definitions of well-founded orders if ``decreases``-clauses are used but no such definitions are present in the program ([Silver#710](https://github.com/viperproject/silver/pull/710)). That is, it is not longer necessary (but still possible) to write an import statement like ``import <decreases/int.vpr>`` when using a termination measure of type integer.
+- The ``Rational`` type, an alias for ``Perm``, is deprecated. Viper issues a warning whenever the type is used.
+
+### Viper API Changes
+
+- Introduced a new API for frontends to interact with Viper ([Silver#732](https://github.com/viperproject/silver/pull/732)). Frontends can create instances of ``ViperFrontendAPI``  and interact exclusively through those (instead of instances of ``Verifier`` or ``SilFrontend``), which saves some boilerplate code and lets Viper manage plugins. 
+
+### Other Viper-level Improvements
+
+- Improved error messages for parse errors ([Silver#702](https://github.com/viperproject/silver/pull/702)) and type errors (([Silver#684](https://github.com/viperproject/silver/pull/684)), ([Silver#724](https://github.com/viperproject/silver/pull/724)))
+- Fixed parsing and pretty-printing of scopes ([Silver#704](https://github.com/viperproject/silver/pull/704)), which were previously ommitted under some circumstances by both the pretty-printer and the parser, which could make otherwise valid Viper code invalid. 
+- Introduced caching to improve performance of common lookups on the AST (([Silver#659](https://github.com/viperproject/silver/pull/659)) and ([Silver#719](https://github.com/viperproject/silver/pull/719)))
+- Viper now reports inferred quantifiers using a ``QuantifierInstantiationsMessage`` ([Silver#653](https://github.com/viperproject/silver/pull/653))
+- Introduced various new consistency checks for invalid code that used to crash the backends or lead to unexpected behavior:
+  - ``perm``-expressions are no longer allowed in function postconditions ([Silver#681](https://github.com/viperproject/silver/pull/681))
+  - ``wildcard`` is no longer allowed as part of compound expressions ([Silver#700](https://github.com/viperproject/silver/pull/700))
+  - empty ADTs are rejected ([Silver#696](https://github.com/viperproject/silver/pull/696))
+  - predicate argument expressions must be pure ([Silver#721](https://github.com/viperproject/silver/pull/721))
+- Labelled ``old``-expressions may now be used as triggers ([Silver#695](https://github.com/viperproject/silver/pull/695))
+- Various small fixes for crashes or other incorrect behavior.
+
+### Backend-specific Upgrades/Changes
+
+#### Symbolic Execution Backend (Silicon)
+
+- The previously experimental mode ``--moreCompleteExhale`` is no longer experimental, but is now a supported mode that performs exhales and heap lookups in a way that is usually more complete (but possibly slower). However, Silicon's previous exhale mode remains the default. ([Silicon#682](https://github.com/viperproject/silicon/pull/682))
+  - The new flag ``--exhaleMode=n``, where ``n`` is 0, 1, or 2, can now be used to select the exhale mode. 0 is the default, 1 is the previous ``moreCompleteExhale`` mode.
+  - The new ``exhaleMode`` 2 uses the default exhale mode 0 throughout the program, until it encounters a verification error. When it does, it retries proving the failing assertion using the (more complete) mode 1. Since mode 0 is usually faster than mode 1, mode 2 often results in the best mix of performance and completeness.
+  - Additionally, one can now override the exhale mode selected via command line for individual methods using an annotation ``@exhaleMode("n")`` on the method ([Silicon#724](https://github.com/viperproject/silicon/pull/724))
+- Via the option ``--prover=Z3-API``, Silicon can now use Z3 as a library via its Java API (([Silicon#633](https://github.com/viperproject/silicon/pull/633)) and ([Silicon#692](https://github.com/viperproject/silicon/pull/692))). Note that this requires a native version of ``libz3java`` to be present on the path Java uses to look for native libraries (which can be set, e.g., via the environment variable``LD_LIBRARY_PATH`` on Linux or ``DYLD_LIBRARY_PATH`` on MacOS).
+  Depending on the OS and the Viper program, this option can lead to a significant speedup.
+- Silicon now emits warnings in cases where it cannot use the triggers specified by the user ([Silicon#687](https://github.com/viperproject/silicon/pull/687))
+- ``old``-expressions in triggers are now interpreted correctly ([Silicon#710](https://github.com/viperproject/silicon/pull/710)); previously, they were sometimes ignored.
+- Changed default options used for Z3; the new options have similar performance and completeness characteristics with the supported Z3 version 4.8.7, but perform better with newer versions (tested in particular with 4.12.1) ([Silicon#694](https://github.com/viperproject/silicon/pull/694))
+- Silicon no longer creates a ``tmp`` directory containing ``.smt2`` files that log its prover interactions by default ([Silicon#709](https://github.com/viperproject/silicon/pull/709)). The flag ``--disableTempDirectory`` no longer exists. Instead, one can use the new flag ``--enableTempDirectory`` or the flag ``--proverLogFile``. 
+- Improved heuristics for handling of quantified permissions, which improves performance in some cases ([Silicon#704](https://github.com/viperproject/silicon/pull/704))
+- Fixed some incorrect (too short) timeouts, which could lead to unstable verification results in some cases ([Silicon#705](https://github.com/viperproject/silicon/pull/705))
+- Added a new command line flag ``--reportReasonUnknown``, which instructs Silicon to report the reason the SMT solver names for not being able to prove a property (per error)  ([Silicon#701](https://github.com/viperproject/silicon/pull/701)). This flag can be useful to find out whether an error occurred due to non-linear arithmetic or timeouts.
+- Fixed five unsoundnesses:
+  - Incorrect handling of ``old``-expressions in postconditions of methods called inside a ``package`` statement ([Silicon#699](https://github.com/viperproject/silicon/pull/699))
+  - Incorrect handling of ``fold`` statements for predicates that are used inside a quantified permission in the current method ([Silicon#696](https://github.com/viperproject/silicon/pull/696))
+  - Incorrect behavior for quantifiers whose bodies have unreachable branches ([Silicon#690](https://github.com/viperproject/silicon/pull/690))
+  - Incorrectly terminating verification after using a ``refute`` ([Silicon#741](https://github.com/viperproject/silicon/pull/741))
+  - Exhale mode 1 now correctly checks permission amounts in function preconditions ([Silicon#682](https://github.com/viperproject/silicon/pull/682))
+- Fixed and generalized the experimental mode ``--conditionalizePermissions``, which avoids branching on conditional permission assertions (e.g., ``b ==> acc(x.f)``) by rewriting them to unconditional assertions with conditional permission amounts (e.g., ``acc(x.f, b ? write : none)`` whenever possible ([Silicon#685](https://github.com/viperproject/silicon/pull/685)). For programs with many branches, this option can improve performance.
+- Resource triggers on existentials now work correctly ([Silicon#679](https://github.com/viperproject/silicon/pull/679))
+- More complete computation of function footprints ([Silicon#684](https://github.com/viperproject/silicon/pull/684))
+- Various smaller bug fixes
+
+#### Verification Condition Generation Backend (Carbon)
+
+- Improved encoding of well-definedness checks for field accesses and permission division ([Carbon#451](https://github.com/viperproject/carbon/pull/451)). As a result, Carbon now emits well-definedness errors in the expected order in some cases where this was previously not the case.
+- Improved encoding of definedness checks during exhale ([Carbon#457](https://github.com/viperproject/carbon/pull/457)). This fixed both possible unsoundness and incompleteness issues.
+- Using stdin instead of a temporary file to communicate with Boogie ([Carbon#456](https://github.com/viperproject/carbon/pull/456))
+
 ## Release 2023.1
 
 **Date 25/01/23**

src/main/resources/import/decreases/all.vpr

@@ -5,7 +5,7 @@ import "bool.vpr"
 import "int.vpr"
 import "multiset.vpr"
 import "predicate_instance.vpr"
-import "rational.vpr"
+import "perm.vpr"
 import "ref.vpr"
 import "seq.vpr"
 import "set.vpr"

src/main/resources/import/decreases/multiset.vpr

@@ -3,7 +3,7 @@
 
 import "declaration.vpr"
 
-domain MuliSetWellFoundedOrder[S]{
+domain MultiSetWellFoundedOrder[S]{
     //MultiSet
     axiom multiset_ax_dec{
         forall mSet1: Multiset[S], mSet2: Multiset[S] :: {decreasing(mSet1, mSet2)}

src/main/resources/import/decreases/perm.vpr

@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import "declaration.vpr"
+
+domain PermWellFoundedOrder{
+	//Rationals
+    axiom rational_ax_dec{
+        forall int1: Perm, int2: Perm :: {decreasing(int1, int2)}
+            (int1 <= int2 - 1/1) ==> decreasing(int1, int2)
+    }
+    axiom rational_ax_bound{
+        forall int1: Perm :: {bounded(int1)}
+            int1 >= 0/1 ==> bounded(int1)
+    }
+}

src/main/scala/viper/silver/ast/utility/DomainInstances.scala

@@ -168,10 +168,13 @@ object DomainInstances {
           case Some(ps) =>
             ps.flatMap(f = pair => {
               //            assert(dfa.funcname==pair._1.funcname)
-              val d2 = p.findDomain(pair._2.domainName)
+              val d2 = p.findDomain(dfa.domainName)
               val tvs = d2.typVars
-              tryUnifyWithDefault(tvs, tvs.map(pair._1.typVarMap.getOrElse(_, Program.defaultType)), tvs.map(dfa.typVarMap.getOrElse(_, Program.defaultType))) match {
-                case Some(ts) => Set[Type](DomainType(pair._2.domainName, ts)(tvs))
+              val axDom = p.findDomain(pair._2.domainName)
+              val axTvs = axDom.typVars
+              tryUnifyWithDefault(axTvs, tvs.map(pair._1.typVarMap.get(_).get), tvs.map(dfa.typVarMap.get(_).get)) match {
+                case Some(ts) =>
+                  Set[Type](DomainType(pair._2.domainName, ts)(axTvs))
                 case None => Set[Type]()
               }
             }).toSet

src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala

@@ -165,6 +165,15 @@ abstract class GenericTriggerGenerator[Node <: AnyRef,
     val nestedBoundVars: Seq[Var] =
       deepCollect(toSearch){ case qe: Quantification => Quantification_vars(qe)}.flatten
 
+    val additionalRelevantVars: Seq[Var] = {
+      val additionalVarFinder = additionalRelevantVariables(vs, nestedBoundVars)
+      deepCollect(toSearch){
+        case n if additionalVarFinder.isDefinedAt(n) => additionalVarFinder(n)
+      }.flatten
+    }
+    val allRelevantVars = (vs ++ additionalRelevantVars).distinct
+    val modifyTriggers = modifyPossibleTriggers(allRelevantVars)
+
     /* Get all function applications */
     reduceTree(toSearch)((node: Node, results: Seq[Seq[(PossibleTrigger, Seq[Var], Seq[Var])]]) => node match {
       case possibleTrigger: PossibleTrigger if isPossibleTrigger(possibleTrigger) =>
@@ -187,18 +196,32 @@ abstract class GenericTriggerGenerator[Node <: AnyRef,
         processedArgs foreach (arg => visit(arg) {
           case v: Var =>
             if (nestedBoundVars.contains(v)) containsNestedBoundVars = true
-            if (vs.contains(v)) containedVars +:= v
+            if (allRelevantVars.contains(v)) containedVars +:= v
         })
 
         if (!containsNestedBoundVars && containedVars.nonEmpty)
           results.flatten ++ Seq((withArgs(possibleTrigger, processedArgs), containedVars, extraVars))
         else
           results.flatten
 
+      case e if modifyTriggers.isDefinedAt(e) => modifyTriggers.apply(e)(results)
+
       case _ => results.flatten
     })
   }
 
+  /*
+   * Hook for clients to add more cases to getFunctionAppsContaining to modify the found possible triggers.
+   * Used e.g. to wrap trigger expressions inferred from inside old-expression into old()
+   */
+  def modifyPossibleTriggers(relevantVars: Seq[Var]): PartialFunction[Node, Seq[Seq[(PossibleTrigger, Seq[Var], Seq[Var])]] =>
+    Seq[(PossibleTrigger, Seq[Var], Seq[Var])]] = PartialFunction.empty
+
+  /*
+   * Hook for clients to identify additional variables which can be covered by triggers.
+   */
+  def additionalRelevantVariables(relevantVars: Seq[Var], varsToAvoid: Seq[Var]): PartialFunction[Node, Seq[Var]] = PartialFunction.empty
+
   /* Precondition: if vars is non-empty then every (f,vs) pair in functs
    * satisfies the property that vars and vs are not disjoint.
    *

src/main/scala/viper/silver/ast/utility/Triggers.scala

@@ -57,6 +57,30 @@ object Triggers {
       case LabelledOld(pt: PossibleTrigger, _) => pt.getArgs
       case _ => sys.error(s"Unexpected expression $e")
     }
+
+    override def modifyPossibleTriggers(relevantVars: Seq[LocalVar]) = {
+      case ast.Old(_) => results =>
+        results.flatten.map(t => {
+          val exp = t._1
+          (ast.Old(exp)(exp.pos, exp.info, exp.errT), t._2, t._3)
+        })
+      case ast.LabelledOld(_, l) => results =>
+        results.flatten.map(t => {
+          val exp = t._1
+          (ast.LabelledOld(exp, l)(exp.pos, exp.info, exp.errT), t._2, t._3)
+        })
+      case ast.Let(v, e, _) => results =>
+        results.flatten.map(t => {
+          val exp = t._1
+          val coveredVars = t._2.filter(cv => cv != v.localVar) ++ relevantVars.filter(rv => e.contains(rv))
+          (exp.replace(v.localVar, e), coveredVars, t._3)
+        })
+    }
+
+    override def additionalRelevantVariables(relevantVars: Seq[LocalVar], varsToAvoid: Seq[LocalVar]): PartialFunction[Node, Seq[LocalVar]] = {
+      case ast.Let(v, e, _) if relevantVars.exists(v => e.contains(v)) && varsToAvoid.forall(v => !e.contains(v)) =>
+        Seq(v.localVar)
+    }
   }
 
   /**

src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala

@@ -82,6 +82,20 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     hidden = true
   )
 
+  val enableSmokeDetection = opt[Boolean]("enableSmokeDetection",
+    descr = "Enable smoke detection (if enabled, refute false statements are inserted in the code in order to detect unsound specifications).",
+    default = Some(false),
+    noshort = true,
+    hidden = false
+  )
+
+  val disableDefaultPlugins = opt[Boolean]("disableDefaultPlugins",
+    descr = "Deactivate all default plugins.",
+    default = Some(false),
+    noshort = true,
+    hidden = true
+  )
+
   val plugin = opt[String]("plugin",
     descr = "Load plugin(s) with given class name(s). Several plugins can be separated by ':'. " +
       "The fully qualified class name of the plugin should be specified.",
@@ -103,15 +117,15 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     case i => throw new IllegalArgumentException(s"Unsupported counterexample model provided. Expected 'native', 'variables' or 'mapped' but got $i")
   }))
 
-  val terminationPlugin = opt[Boolean]("disableTerminationPlugin",
+  val disableTerminationPlugin = opt[Boolean]("disableTerminationPlugin",
     descr = "Disable the termination plugin, which adds termination checks to functions, " +
       "methods and loops.",
     default = Some(false),
     noshort = true,
     hidden = true
   )
 
-  val adtPlugin = opt[Boolean]("disableAdtPlugin",
+  val disableAdtPlugin = opt[Boolean]("disableAdtPlugin",
     descr = "Disable the ADT plugin, which adds support for ADTs as a built-in type.",
     default = Some(false),
     noshort = true,