Update Gobra to the newest Viper version

.github/workflows/test.yml

@@ -26,7 +26,13 @@ jobs:
     steps:
       - name: Checkout Gobra
         uses: actions/checkout@v2
-
+        with:
+          submodules: 'recursive'
+      - name: Check that silicon & carbon reference same silver commit
+        run: |
+          SILICON_SILVER_REF=$(git -C viperserver/silicon/silver rev-parse HEAD) && \
+          CARBON_SILVER_REF=$(git -C viperserver/carbon/silver rev-parse HEAD) && \
+          if [ "$SILICON_SILVER_REF" != "$CARBON_SILVER_REF" ]; then echo "Silicon and Carbon reference different Silver commits ($SILICON_SILVER_REF and $CARBON_SILVER_REF)" && exit 1 ; fi
       - name: Create image tag
         run: |
           IMAGE_ID=ghcr.io/${{ github.repository_owner }}/$IMAGE_NAME
@@ -45,13 +51,6 @@ jobs:
       - name: Set up Docker Buildx
         uses: docker/setup-buildx-action@v1
 
-      - name: Get dependency versions
-        run: |
-          source viper-toolchain-versions.sh
-          echo "SILICON_REF=$SILICON_REF" >> $GITHUB_ENV
-          echo "CARBON_REF=$CARBON_REF" >> $GITHUB_ENV
-          echo "VIPERSERVER_REF=$VIPERSERVER_REF" >> $GITHUB_ENV
-
       - name: Build image up to including stage 'build'
         # note that the action's name is misleading: this step does NOT push
         uses: docker/build-push-action@v2
@@ -60,10 +59,6 @@ jobs:
           load: true # make the built image available in docker (locally)
           target: build # only build up to and including stage 'build'
           file: workflow-container/Dockerfile
-          build-args: |
-            SILICON_REF=${{ env.SILICON_REF }}
-            CARBON_REF=${{ env.CARBON_REF }}
-            VIPERSERVER_REF=${{ env.VIPERSERVER_REF }}
           tags: ${{ env.IMAGE_TAG }}
           labels: "runnumber=${{ github.run_id }}"
           push: false
@@ -177,11 +172,6 @@ jobs:
           context: .
           load: true # make the built image available in docker (locally)
           file: workflow-container/Dockerfile
-          build-args: |
-            SILICON_REF=${{ env.SILICON_REF }}
-            CARBON_REF=${{ env.CARBON_REF }}
-            VIPERSERVER_REF=${{ env.VIPERSERVER_REF }}
-
           tags: ${{ env.IMAGE_TAG }}
           labels: "runnumber=${{ github.run_id }}"
           push: false
@@ -225,10 +215,6 @@ jobs:
         with:
           context: .
           file: workflow-container/Dockerfile
-          build-args: |
-            SILICON_REF=${{ env.SILICON_REF }}
-            CARBON_REF=${{ env.CARBON_REF }}
-            VIPERSERVER_REF=${{ env.VIPERSERVER_REF }}
           tags: ${{ env.IMAGE_TAG }}
           labels: "runnumber=${{ github.run_id }}"
           push: true

.gitignore

@@ -6,10 +6,6 @@ target/
 tmp/
 sync/
 
-carbon
-silver
-silicon
-viperserver
 logger.log
 
 *.go.*

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "viperserver"]
+	path = viperserver
+	url = https://github.com/viperproject/viperserver

README.md

@@ -14,58 +14,39 @@ We call annotated Go programs Gobra programs and use the file extension `.gobra`
 - Git
 
 ### Installation
-1. Create a folder for your Gobra development. We will refer to this folder as `gobraHome`.
-2. Clone Gobra and Viper dependencies
-    - Change directory to `gobraHome`
-    - [silicon](https://github.com/viperproject/silicon) (commit `47e74c64b75f1c186a1307c07f21198e61103334`)
-    - [carbon](https://github.com/viperproject/carbon) (commit `f9c4027cd3bd82f202e7fe78866f8ff794a47232`)
-    - [viperserver](https://github.com/viperproject/viperserver) (commit `4f441dff43bb1ce698fb40fa50fbaf0ed203aec2`)
-    - Gobra
-    > To switch to tag `X`, execute the command ```git checkout X``` inside the cloned repository.
-3. Get submodules and add symbolic links
-    - Change directory to `gobraHome/silicon` and fetch & update submodules:
-        - `git submodule init; git submodule update`
-    - Change directory to `gobraHome/carbon` and fetch & update submodules:
-        - `git submodule init; git submodule update`
-   - To create a symbolic link from A to B, you have to run
-      - `mklink /D A B` (Windows (as admin)) resp.
-      - `ln -s B A` (Linux & macOS) (use forward instead of backward slashes in the following)
-    - Change directory to `gobraHome/viperserver` and create the symbolic links:
-        - silicon -> ..\silicon
-        - carbon -> ..\carbon
-    - Change to `gobraHome/gobra` and create the links:
-        - silicon -> ..\silicon
-        - carbon -> ..\carbon
-        - viperserver -> ..\viperserver
-4. Install Z3 and Boogie. 
+1. Install Z3 and Boogie.
     Steps (iii) and (iv) are specific to Boogie and only necessary when using Carbon as verification backend. Gobra uses the Silicon verification backend by default.
-    1. Get a Z3 executable. A precompiled executable can be downloaded [here](https://github.com/Z3Prover/z3/releases). 
+    1. Get a Z3 executable. A precompiled executable can be downloaded [here](https://github.com/Z3Prover/z3/releases).
       We tested version 4.8.7 64-Bit.
     2. Set the environment variable `Z3_EXE` to the path of your Z3 executable.
     3. Get a Boogie executable. Instructions for compilation are given [here](https://github.com/boogie-org/boogie).
         [Mono](https://www.mono-project.com/download/stable/) is required on Linux and macOS to run Boogie.
         Alternatively, extract a compiled version from the Viper release tools
         ([Windows](http://viper.ethz.ch/downloads/ViperToolsReleaseWin.zip), [Linux](http://viper.ethz.ch/downloads/ViperToolsReleaseLinux.zip), [macOS](http://viper.ethz.ch/downloads/ViperToolsReleaseMac.zip)).
     4. Set the environment variable `BOOGIE_EXE` to the path of your Boogie executable.
+2. Clone `gobra` (this repository) in your computer.
+3. Change directory to the `gobra` directory created in the previous step.
+4. Run `git submodule update --init --recursive` to fetch `viperserver` and its transitive dependencies (`carbon`, `silicon` and `silver`).
+5. Run `sbt compile` to compile Gobra.
 
-### Compilation
-1. Change directory to `gobraHome/gobra`
-2. Start an sbt shell by running `sbt`
-3. Compile gobra by running `compile` in the sbt shell
-    - **Important**: Do not compile silver, silicon, or carbon separately. 
-    If you have compiled them separately, then delete all target folders in these projects.
-4. Check your installation by executing all tests (`test` in the sbt shell)
-5. A file can be verified with `run -i path/to/file` in the sbt shell
-    - e.g. `run -i src/test/resources/regressions/examples/swap.gobra`
-6. All command line arguments can be shown by running `run --help` in the sbt shell
+The command `sbt assembly` can also be used to produce a fat jar file, which is located by default in `target/scala`.
 
-### Assembly
-1. In an sbt shell, run `assembly`. The fat jar is then located in the target/scala folder.
-2. To verify a file, run `java -jar -Xss128m gobra.jar -i path/to/file`
+### Running Gobra
+Gobra can be run either from sbt or from a compiled jar:
+- running from sbt:
+    1. change directory to the `gobra` directory obtained from cloning this repository.
+    2. run `sbt`.
+    3. inside the sbt shell, run `run - i path/to/file` (e.g., `run -i src/test/resources/regressions/examples/swap.gobra`)
+- running from a compiled jar:
+    1. run `java -jar -Xss128m path/to/gobra.jar -i path/to/file`.
 
+More information about the available options in Gobra can be found by running `run --help` in an sbt shell or `java -jar path/to/gobra.jar --help` if you assembled Gobra.
+
+### Running the Tests
+In the `gobra` directory, run the command `sbt test`.
 
 ## Licensing
-Most Gobra sources are licensed under the Mozilla Public License Version 2.0. 
+Most Gobra sources are licensed under the Mozilla Public License Version 2.0.
 The [LICENSE](./LICENSE) lists the exceptions to this rule.
 Note that source files (whenever possible) should list their license in a short header.
 Continuous integration checks these file headers.

build.sbt

@@ -7,20 +7,12 @@
 import scala.sys.process.Process
 import scala.util.Try
 
-// Import general settings from Silver, Silicon and Carbon
-
+// Import general settings from viperserver and, transitively, from carbon, silicon and silver.
 // we assume that carbon/silver and silicon/silver point to the same version of the silver repo
-lazy val silver = project in file("silicon/silver")
-lazy val silicon = project in file("silicon")
-lazy val carbon = project in file("carbon")
 lazy val server = project in file("viperserver")
 
-
 // Gobra specific project settings
 lazy val gobra = (project in file("."))
-  .dependsOn(silver % "compile->compile;test->test")
-  .dependsOn(silicon % "compile->compile;test->test")
-  .dependsOn(carbon % "compile->compile;test->test")
   .dependsOn(server % "compile->compile;test->test")
   .settings(
     // General settings
@@ -31,8 +23,6 @@ lazy val gobra = (project in file("."))
     licenses := Seq("MPL-2.0 License" -> url("https://opensource.org/licenses/MPL-2.0")),
 
     // Compilation settings
-    silicon / excludeFilter := "logback.xml", /* Ignore Silicon's Logback configuration */
-    carbon / excludeFilter := "logback.xml", /* Ignore Carbon's Logback configuration */
     Compile / unmanagedResourceDirectories += baseDirectory.value / "conf",
 
     libraryDependencies +=

src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala

@@ -67,8 +67,8 @@ object DefaultErrorBackTranslator {
       //      case vprrea.InvalidPermMultiplication(offendingNode) =>
       case vprrea.MagicWandChunkNotFound(CertainSource(info)) =>
         MagicWandChunkNotFound(info)
-      case vprrea.ReceiverNotInjective(CertainSource(info)) =>
-        ReceiverNotInjectiveReason(info)
+      case vprrea.QPAssertionNotInjective(CertainSource(info)) =>
+        QPAssertionNotInjective(info)
       case vprrea.LabelledStateNotReached(CertainSource(info)) =>
         LabelledStateNotReached(info)
       case termination.TerminationConditionFalse(CertainSource(info)) =>

src/main/scala/viper/gobra/reporting/StatsCollector.scala

@@ -13,8 +13,8 @@ import viper.gobra.ast.internal.BuiltInMember
 import viper.gobra.frontend.Config
 import viper.gobra.frontend.info.{Info, TypeInfo}
 import viper.gobra.util.Violation
-import viper.gobra.util.ViperChopper.{Edges, Vertex}
 import viper.silver.ast.{Function, Member, Method, Predicate}
+import viper.silver.ast.utility.Chopper.{Edges, Vertex}
 import viper.silver.reporter.Time
 
 import scala.collection.concurrent.{Map, TrieMap}

src/main/scala/viper/gobra/reporting/VerifierError.scala

@@ -450,9 +450,9 @@ case class NegativePermissionReason(info: Source.Verifier.Info) extends Verifica
   override def message: String = s"Expression ${info.origin.tag.trim} might be negative."
 }
 
-case class ReceiverNotInjectiveReason(info: Source.Verifier.Info) extends VerificationErrorReason {
-  override def id: String = "receiver_not_injective"
-  override def message: String = s"Receiver ${info.origin.tag.trim} might not be injective."
+case class QPAssertionNotInjective(info: Source.Verifier.Info) extends VerificationErrorReason {
+  override def id: String = "qp_assertion_not_injective"
+  override def message: String = s"Quantified resource ${info.origin.tag.trim} might not be injective."
 }
 
 case class GoCallPreconditionReason(node: Source.Verifier.Info) extends VerificationErrorReason {

src/main/scala/viper/gobra/util/ChopperUtil.scala

@@ -12,6 +12,7 @@ import java.nio.file.Files
 import java.util.Properties
 import viper.silver.{ast => vpr}
 import viper.silver.ast.SourcePosition
+import viper.silver.ast.utility.Chopper
 import viper.gobra.frontend.{Config, PackageInfo}
 import viper.gobra.reporting.ChoppedViperMessage
 import viper.gobra.backend.BackendVerifier.Task
@@ -24,8 +25,8 @@ object ChopperUtil {
   def computeChoppedPrograms(task: Task, pkgInfo: PackageInfo)(config: Config): Vector[vpr.Program] = {
 
 
-    val programs = ViperChopper.chop(task.program)(
-      isolate = computeIsolateMap(config, pkgInfo),
+    val programs = Chopper.chop(task.program)(
+      selection = computeIsolateMap(config, pkgInfo),
       bound = Some(config.choppingUpperBound),
       penalty = getPenalty
     )
@@ -70,9 +71,9 @@ object ChopperUtil {
     * then a penalty object using this configuration is created and returned.
     * Otherwise, if no configuration is present, the default configuration is returned.
     * */
-  def getPenalty: ViperChopper.Penalty[ViperChopper.Vertex] = {
+  def getPenalty: Chopper.Penalty[Chopper.Vertex] = {
     import scala.io.Source
-    import viper.gobra.util.ViperChopper.Penalty
+    import viper.silver.ast.utility.Chopper.Penalty
 
     val file = new File(GobraChopperFileLocation)
     if (!file.exists()) {