Merge branch 'master' into fabiopakk_update_scala_2.13.0

.github/workflows/scala.yml

@@ -0,0 +1,21 @@
+name: Scala CI
+
+on:
+  push:
+    branches: [ master ]
+  pull_request:
+    branches: [ master ]
+
+jobs:
+  build:
+
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v2
+    - name: Set up JDK 1.8
+      uses: actions/setup-java@v1
+      with:
+        java-version: 1.8
+    - name: Run tests
+      run: sbt test

.hgignore → .gitignore

@@ -1,4 +1,3 @@
-syntax: glob
 .cache
 project/project/**
 project/target/**
@@ -11,5 +10,5 @@ documentation/syntax/sil-syntax.pdf
 documentation/syntax/sil-syntax.out
 documentation/syntax/sil-syntax.log
 documentation/syntax/sil-syntax.aux
-*.iml
+*.iml
 .DS_Store

README.rst

@@ -4,8 +4,8 @@ Silver
 
 Silver is the intermediate verification language of the
 `Viper project <http://www.pm.inf.ethz.ch/research/viper.html>`_ by
-`Chair of Programming Methodology <http://www.pm.inf.ethz.ch/>`_
-at ETH Zürich, Department of Computer Science.
+`Programming Methodology Group <http://www.pm.inf.ethz.ch/>`_
+at the Department of Computer Science, ETH Zurich.
 
 Quick Start
 ===========
@@ -19,4 +19,4 @@ Syntax Highlighting
 ===================
 
 Files for LaTeX and various editors can be found under
-``silver/util/highlighting`` directory.
+``silver/util/highlighting`` directory.

ReleaseNotes.md

@@ -0,0 +1,89 @@
+## Release 2020.1
+#### Date 31/01/20     [Download](http://www.pm.inf.ethz.ch/research/viper/downloads.html)
+
+### Changes in Viper Language
+* Support for variable scopes. For example, now it is possible
+to define two variables with the same name in different branches:
+    ```
+	if (b) {
+        var x: Int := 5;
+    } else {
+        var x: Bool := true;
+    }
+	```
+* Added support for using field lookups and predicates as triggers, e.g.
+    ```
+	forall r: Ref :: {r.f} r in s ==> r.f > 0
+
+    forall r: Ref :: {P(r)} r in s ==> (unfolding P(r) in r.f > 0)
+	```
+    Note: this support still has some [issues](https://bitbucket.org/viperproject/carbon/issues/257) in Viper's VCG-based verifier.
+
+* Added support for trigger annotations on existential quantifiers. These are written and behave analogously to those already supported on forall quantifiers, and are relevant in the logically dual cases, typically when *proving* an existentially-quantified assertion [(189)](https://bitbucket.org/viperproject/silver/issues/189).
+* Extended support for Viper plugins (designed to make lightweight Viper front-end tools simple to write). In particular, extending the grammar of the parser via plugins is now possible.
+* Removed the experimental built-in function termination checking. An experimental
+termination plugin is available: https://bitbucket.org/viperproject/termination-plugin/
+Feedback is welcome; we plan support for termination checking in the next release.
+* Renamed all example files from .sil to .vpr [(287)](https://bitbucket.org/viperproject/silver/issues/287).
+* The unary plus operator has been removed [(108)](https://bitbucket.org/viperproject/silver/issues/271).
+* Whitespace between unary operations and their operands is no-longer allowed [(272)](https://bitbucket.org/viperproject/silver/issues/272).
+* The `fresh` statement was removed [(87)](https://bitbucket.org/viperproject/silver/issues/87).
+* Macros can now take field names as parameters [(170)](https://bitbucket.org/viperproject/silver/issues/170).
+* LHS of field assignment statements can now be a macro invocation [(214)](https://bitbucket.org/viperproject/silver/issues/214).
+* Warnings are now generated for unused macro parameters [(267)](https://bitbucket.org/viperproject/silver/issues/267).
+* Macro definitions are disallowed inside magic wand proof scripts [(215)](https://bitbucket.org/viperproject/silver/issues/215).
+
+### Bug fixes
+* Conditional assertions as part of quantified permissions are properly supported, e.g. 
+  `inhale forall j : Int :: (j == k ? acc(s.f) : true)` [(260)](https://bitbucket.org/viperproject/silver/issues/260).
+* Expression macros with missing bodies no-longer cause spurious parser errors (for next construct) [(273)](https://bitbucket.org/viperproject/silver/issues/273).
+* `new(..)` parameterised by identifiers which are present in the program but are not field names now produces an appropriate error message [(247)](https://bitbucket.org/viperproject/silver/issues/247).
+* Type checker no longer crashes on ASTs with sharing [(191)](https://bitbucket.org/viperproject/silver/issues/191).
+* Macro names are now checked for clashes [(167)](https://bitbucket.org/viperproject/silver/issues/167).
+* The AST utility method `Expressions.instantiateVariables` is now capture-avoiding (an additional parameter can be provided to exclude certain names from being chosen when renaming bound variables) [(286)](https://bitbucket.org/viperproject/silver/issues/286).
+* Eliminated spurious type error involving #E type when using empty Multisets via macros [(282)](https://bitbucket.org/viperproject/silver/issues/282).
+* AST transformation framework's Rewritable is no-longer limited w.r.t. collections of Rewritables [(225)](https://bitbucket.org/viperproject/silver/issues/225).
+
+### Viper Language API changes: 
+* `LocalVar` AST node no longer has type as an optional field [(281)](https://bitbucket.org/viperproject/silver/issues/281).
+* `Result` AST node no longer has type in its second parameter list [(283)](https://bitbucket.org/viperproject/silver/issues/283).
+* `Call` trait, `FuncApp` and `DomainFuncApp` AST nodes no longer have a `formalArgs` field; this information can be obtained from the enclosing `Program` [(241)](https://bitbucket.org/viperproject/silver/issues/241).
+* Upgraded all dependencies, libraries, plugins and development environment:
+    * SBT 1.2.6, rewriting all build files.
+	* Scala 2.12.7
+	* fastparse	1.0.0
+	* ScalaTest 3.0.5.
+	* scallop 3.1.3.
+	* jgrapht-core 1.2.0.
+	* scala-parser-combinators 1.1.1.
+	* commons-io 2.6.
+	* guava 26.0.
+	* slf4j-api 1.7.25.
+	* logback-classic 1.2.3.
+	* scala-logging 3.9.0
+	* sbt-assembly 0.14.7
+	* sbteclipse-plugin	5.2.4.
+  
+
+### Backend-specific upgrades/changes
+* [Symbolic Execution Verifier](https://bitbucket.org/viperproject/silicon/)
+    * Implemented an experimental feature that allows using the quantified
+permissions based handling of permissions for all permissions. This
+handling of permissions is expected to be more complete and may be faster;
+however, the implementation is still in beta state. The feature can be
+enabled with the ``--enableMoreCompleteExhale`` flag.
+    * (API) Uses logback library instead of log4j for logging.
+    * (API) Changed how the verifier reports errors: introduced a reporter class
+that is responsible for reporting errors to the user (before errors were
+reported via logging). Verification results of a particular method are
+reported via the reporter as soon as they become available without
+waiting for all methods to be verified.
+* [Verification Condition Generation Verifier](https://bitbucket.org/viperproject/carbon/)
+    * Quantified permissions with multiple forall-bound variables are now supported [(205)](https://bitbucket.org/viperproject/carbon/issues/205/).
+    * Experimental adjustments to the background axioms used for set, sequence and multiset support. These should   mostly add completeness; fewer scenarios should require user assertions to verify. Please report any bugs observed (particularly examples which exhibit poorer performance). In the next release, this will be stabilised, and migrated analogously to Viper's Symbolic Execution back-end. 
+    * Old expressions in triggers are now translated correctly [(236)](https://bitbucket.org/viperproject/carbon/issues/236/).
+    * Substitution of actuals for formals in method specifications, predicate unfoldings and function preconditions is now capture-avoiding [(262)](https://bitbucket.org/viperproject/carbon/issues/262), [(282)](https://bitbucket.org/viperproject/carbon/issues/282).
+    * Quantified predicates without arguments no-longer cause a crash [(279)](https://bitbucket.org/viperproject/carbon/issues/279).
+
+### Other Notes
+   * We observed that 'Out of memory' errors can occur for some larger examples if using a 32-bit (rather than 64-bit) version of Z3 [(286)](https://bitbucket.org/viperproject/carbon/issues/286). We recommend always using a 64-bit version.

build.sbt

@@ -8,19 +8,25 @@
 // Compilation settings
 ThisBuild / scalaVersion := "2.13.0"
 ThisBuild / scalacOptions ++= Seq(
+  "-encoding", "UTF-8",               // Enforce UTF-8, instead of relying on properly set locales
   "-deprecation",                     // Warn when using deprecated language features
   "-unchecked",                       // Warn on generated code assumptions
   "-feature",                         // Warn on features that requires explicit import
   "-Ywarn-unused-import",             // Warn on unused imports
   "-Ypatmat-exhaust-depth", "40"      // Increase depth of pattern matching analysis
 )
 
+// Enforce UTF-8, instead of relying on properly set locales
+ThisBuild / javacOptions ++= Seq("-encoding", "UTF-8", "-charset", "UTF-8", "-docencoding", "UTF-8")
+ThisBuild / javaOptions  ++= Seq("-Dfile.encoding=UTF-8")
+
 // Publishing settings
-ThisBuild / Test / publishArtifact := true
+
 // Allows 'publishLocal' SBT command to include test artifacts in a dedicated JAR file
 // (whose name is postfixed by 'test-source') and publish it in the local Ivy repository.
 // This JAR file contains all classes and resources for testing and projects like Carbon
 // and Silicon can rely on it to access the test suit implemented in Silver.
+ThisBuild / Test / publishArtifact := true
 
 // Silver specific project settings
 lazy val silver = (project in file("."))
@@ -30,6 +36,10 @@ lazy val silver = (project in file("."))
     organization := "viper",
     version := "0.1-SNAPSHOT",
 
+    // Fork test to a different JVM than SBT's, avoiding SBT's classpath interfering with
+    // classpath used by Scala's reflection.
+    Test / fork := true,
+
     // Compilation settings
     libraryDependencies += "org.scala-lang" % "scala-reflect" % scalaVersion.value,             // Scala
     libraryDependencies += "org.scalatest" %% "scalatest" % "3.0.5",                            // Testing

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

@@ -0,0 +1,11 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import "bool.vpr"
+import "int.vpr"
+import "multiset.vpr"
+import "predicate_instance.vpr"
+import "rational.vpr"
+import "ref.vpr"
+import "seq.vpr"
+import "set.vpr"

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

@@ -0,0 +1,15 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import "declaration.vpr"
+
+domain BoolWellFoundedOrder{
+    //Booleans
+    axiom bool_ax_dec{
+        decreasing(false, true)
+    }
+    axiom bool_ax_bound{
+        forall bool1: Bool :: {bounded(bool1)}
+            bounded(bool1)
+    }
+}

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

@@ -0,0 +1,8 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+domain WellFoundedOrder[T]{
+    // arg1 is smaller then arg2
+    function decreasing(arg1:T, arg2:T):Bool
+    function bounded(arg1:T):Bool
+}

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

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

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

@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import "declaration.vpr"
+
+domain MuliSetWellFoundedOrder[S]{
+    //MultiSet
+    axiom multiset_ax_dec{
+        forall mSet1: Multiset[S], mSet2: Multiset[S] :: {decreasing(mSet1, mSet2)}
+            (|mSet1| < |mSet2|) ==> decreasing(mSet1, mSet2)
+    }
+    axiom multiset_ax_bound{
+        forall mSet1: Multiset[S] :: {bounded(mSet1)}
+            bounded(mSet1)
+    }
+}

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

@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import "declaration.vpr"
+import "predicate_instance_nested.vpr"
+import <predicateinstance/pi.vpr>
+
+domain PredicateInstancesWellFoundedOrder {
+    axiom predicate_instances_ax_dec{
+        forall l1: PredicateInstance, l2: PredicateInstance :: {nestedPredicates(l1,l2)}
+            decreasing(l1, l2) <==> nestedPredicates(l1,l2)
+    }
+
+    axiom predicate_instances_ax_bound{
+        forall l1: PredicateInstance :: {bounded(l1)}
+            bounded(l1)
+    }
+}

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

@@ -0,0 +1,20 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <predicateinstance/pi.vpr>
+
+domain PredicateInstancesNestedRelation{
+    function nestedPredicates(l1: PredicateInstance, l2: PredicateInstance) : Bool
+
+    //Transitivity of the nested-Function
+    axiom nestedTrans{
+        forall l1: PredicateInstance, l2: PredicateInstance, l3: PredicateInstance :: {nestedPredicates(l1, l2), nestedPredicates(l2, l3)}
+            nestedPredicates(l1,l2) && nestedPredicates(l2,l3) ==> nestedPredicates(l1,l3)
+    }
+
+    //A predicate cannot be nested inside itself
+    axiom nestedReflex{
+        forall l1: PredicateInstance ::
+            !nestedPredicates(l1, l1)
+    }
+}

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

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

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

@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import "declaration.vpr"
+
+domain RefWellFoundedOrder{
+    //References
+	axiom ref_ax_dec{
+        forall ref1: Ref :: {decreasing(null,ref1)}
+            ref1 != null ==> decreasing(null, ref1)
+    }
+    axiom ref_ax_bound{
+        forall ref1: Ref :: {bounded(ref1)}
+            bounded(ref1)
+    }
+}

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

@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import "declaration.vpr"
+
+domain SeqWellFoundedOrder[S]{
+    //Sequences
+    axiom seq_ax_dec{
+        forall seq1: Seq[S], seq2: Seq[S] :: {decreasing(seq1,seq2)}
+            (|seq1| < |seq2|) ==> decreasing(seq1, seq2)
+    }
+    axiom seq_ax_bound{
+        forall seq1: Seq[S] :: {bounded(seq1)}
+            (|seq1| >= 0) ==> bounded(seq1)
+    }
+}

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

@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import "declaration.vpr"
+
+domain SetWellFoundedOrder[S]{
+    //Sets
+    axiom set_ax_dec{
+        forall set1: Set[S], set2: Set[S] :: {decreasing(set1, set2)}
+            (|set1| < |set2|) ==> decreasing(set1, set2)
+    }
+    axiom set_ax_bound{
+        forall set1: Set[S] ::  {bounded(set1)}
+            bounded(set1)
+    }
+}

src/test/resources/all/issues/silver/0168.sil → src/main/resources/import/predicateinstance/pi.vpr

@@ -1,6 +1,4 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-import "0168_lib.sil"
-
-method test() { assert P() }
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+domain PredicateInstance{}