Pull master into cvc5

.github/workflows/ci.yml

@@ -6,7 +6,7 @@
 
 name: ci
 
-on: [push, pull_request]
+on: [push, pull_request, workflow_dispatch]
 
 env:
   RELEASE_DIR: tmp_release
@@ -25,13 +25,8 @@ jobs:
       # Checkout Silicon (note: all checkouts delete the contents of their working directory)
       - name: Checkout Silicon
         uses: actions/checkout@v2
-
-      # Checkout Viper dependencies (just Silver)
-      - name: Checkout Silver
-        uses: actions/checkout@v2
         with:
-          repository: viperproject/silver
-          path: silver
+          submodules: true
 
       # Query versions, and other details that may help with reconstructing a built. 
       # Results are displayed on stdio, and written to buildinfo.log
@@ -91,6 +86,8 @@ jobs:
       # Checkout Silicon (deletes content of working directory)
       - name: Checkout Silicon
         uses: actions/checkout@v2
+        with:
+          submodules: true
 
       - name: Download artifacts from job test-and-assemble
         uses: actions/download-artifact@v2

.gitignore

@@ -18,8 +18,9 @@ utils/tidy_smtlib/tidy_smtlib.jar
 utils/scripts/tidy_smtlib.jar
 silicon_classpath.txt
 lib/
-silver
 src/test/resources/symbExLogTests/*.alog
 .DS_Store
 viper_tutorial_examples
 .bsp/
+.bloop/
+.metals/

.gitmodules

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

README.md

@@ -129,13 +129,22 @@ method main() {
 
 # Build Instructions
 
+> See [the documentation wiki](https://github.com/viperproject/documentation/wiki) for instructions on how to try out or install the Viper tools.
+
 * You need recent installations of
   1. the [sbt build tool](https://www.scala-sbt.org/)
   2. the [Z3 SMT solver](https://github.com/Z3Prover/z3/releases)
   3. the [cvc5 SMT solver](https://github.com/cvc5/cvc5/releases)
-* Clone [Silver](https://github.com/viperproject/silver), e.g. into `~/silver`
-* Clone Silicon (this repository), e.g. into `~/silicon`
-* From within the directory where you installed Silicon, create a symbolic link to the directory where you installed Silver. E.g. there should be a symbolic link from `~/silicon/silver` to `~/silver`. Alternatively, directly clone Silver into, e.g. `~/silicon/silver`.
-* Open a console, change directory to `~/silicon`
-* Compile by running `sbt compile`, or run all tests via `sbt test`
-* We recommend IDEA IntelliJ for Scala development, but any IDE that supports sbt will do
+* Clone this repository *recursively* by running:  
+`git clone --recursive https://github.com/viperproject/silicon`
+
+And then, from the cloned directory, with the `Z3_EXE` environment variable set appropriately;  
+* Compile and run with:  
+  `sbt "run [options] <path to Viper file>"`  
+  Or run all tests via `sbt test`
+* Alternatively, for a faster startup without compilation each time, build a `.jar` file:  
+  `sbt assembly`  
+  And then run with:  
+  `java -jar ./target/scala-*/silicon.jar [options] <path to Viper file>`
+
+> We recommend IDEA IntelliJ for Scala development, but any IDE that supports sbt will do

annotation/Terms.example.scala

@@ -1971,6 +1971,7 @@ object utils {
     case PermTimes(t0, t1) => consumeExactRead(t0, constrainableARPs) && consumeExactRead(t1, constrainableARPs)
     case IntPermTimes(_, t1) => consumeExactRead(t1, constrainableARPs)
     case PermIntDiv(t0, _) => consumeExactRead(t0, constrainableARPs)
+    case PermPermDiv(t0, t1) => consumeExactRead(t0, constrainableARPs) && consumeExactRead(t1, constrainableARPs)
     case PermMin(t0 ,t1) => consumeExactRead(t0, constrainableARPs) || consumeExactRead(t1, constrainableARPs)
     case Ite(_, t0, t1) => consumeExactRead(t0, constrainableARPs) || consumeExactRead(t1, constrainableARPs)
     case _ => true

bors.toml

@@ -0,0 +1 @@
+status = ["test-and-assemble"]

silicon.bat

@@ -4,7 +4,7 @@ set CURR_DIR=%cd%
 set BASE_DIR=%~dp0
 
 :: switch to repository root to check for classpath file and possibly call sbt.
-cd %BASE_DIR%
+cd "%BASE_DIR%"
 
 :: Only call sbt if the classpath file is missing.
 if not exist silicon_classpath.txt (
@@ -22,12 +22,8 @@ if not exist silicon_classpath.txt (
 for /f "delims=" %%x in (silicon_classpath.txt) do set CP=%%x
 
 :: switch back to original directory
-cd %CURR_DIR%
+cd "%CURR_DIR%"
 
-set JAVA_EXE=java
-set JVM_OPTS=-Dlogback.configurationFile="%BASE_DIR%\src\main\resources\logback.xml" -Xss16m -Dfile.encoding=UTF-8
-set SILICON_MAIN=viper.silicon.SiliconRunner
-set FWD_ARGS= %*
-set CMD=%JAVA_EXE% %JVM_OPTS% -cp "%CP%" %SILICON_MAIN% %FWD_ARGS%
+set JVM_OPTS=-Xss16m -Dlogback.configurationFile="%BASE_DIR%\src\main\resources\logback.xml" -Dfile.encoding=UTF-8
 
-call %CMD%
+call java %JVM_OPTS% -cp "%CP%" viper.silicon.SiliconRunner %*

silicon.sh

@@ -4,14 +4,12 @@
 
 set -e
 
-set -e
-
-BASEDIR="$(realpath `dirname $0`)"
+BASEDIR="$(realpath "$(dirname "$0")")"
 
 CP_FILE="$BASEDIR/silicon_classpath.txt"
 
-if [ ! -f $CP_FILE ]; then
-    (cd $BASEDIR; sbt "export runtime:dependencyClasspath" | tail -n1 > $CP_FILE)
+if [ ! -f "$CP_FILE" ]; then
+    (cd "$BASEDIR"; sbt "export runtime:dependencyClasspath" | tail -n1 > "$CP_FILE")
 fi
 
-java -Xss30M -Dlogback.configurationFile="$BASEDIR/src/main/resources/logback.xml" -cp "`cat $CP_FILE`" viper.silicon.SiliconRunner $@
+exec java -Xss30M -Dlogback.configurationFile="$BASEDIR/src/main/resources/logback.xml" -cp "$(cat "$CP_FILE")" viper.silicon.SiliconRunner "$@"

src/main/resources/dafny_axioms/sequences.vpr

@@ -53,7 +53,9 @@ domain $Seq[E] {
   }
 
   axiom seq_index_over_singleton {
-    forall e: E :: {Seq_index(Seq_singleton(e), 0)}
+    forall e: E ::
+        // {Seq_index(Seq_singleton(e), 0)}
+        {Seq_singleton(e)} // [2022-03-08 Malte] Weaker trigger to resolve Silicon issue #601
       Seq_index(Seq_singleton(e), 0) == e
   }
 

src/main/scala/Config.scala

@@ -43,22 +43,11 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 //    val argType: ArgType.V = org.rogach.scallop.ArgType.LIST
 //  }
 
-  private val forwardArgumentsConverter: ValueConverter[String] = new ValueConverter[String] {
-    def parse(s: List[(String, List[String])]): Either[String, Option[String]] = s match {
-      case (_, str :: Nil) :: Nil if str.head == '"' && str.last == '"' => Right(Some(str.substring(1, str.length - 1)))
-      case Nil => Right(None)
-      case _ => Left(s"unexpected arguments")
-    }
-
-    val argType: ArgType.V = org.rogach.scallop.ArgType.LIST
-  }
-
   private val smtlibOptionsConverter: ValueConverter[Map[String, String]] = new ValueConverter[Map[String, String]] {
     def parse(s: List[(String, List[String])]): Either[String, Option[Map[String, String]]] = s match {
-      case (_, str :: Nil) :: Nil if str.head == '"' && str.last == '"' =>
+      case (_, str :: Nil) :: Nil =>
         val config = toMap(
-          str.substring(1, str.length - 1) /* Drop leading and trailing quotation mark */
-             .split(' ') /* Separate individual key=value pairs */
+          str.split(' ') /* Separate individual key=value pairs */
              .map(_.trim)
              .filter(_.nonEmpty)
              .map(_.split('=')) /* Split key=value pairs */
@@ -503,18 +492,18 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   private val rawProverArgs: ScallopOption[String] = opt[String]("proverArgs",
     descr = (  "Command-line arguments which should be forwarded to the prover. "
-             + "The expected format is \"<opt> <opt> ... <opt>\", including the quotation marks."),
+             + "The expected format is \"<opt> <opt> ... <opt>\", excluding the quotation marks."),
     default = None,
     noshort = true
-  )(forwardArgumentsConverter)
+  )
 
   // DEPRECATED and replaced by proverArgs
   // but continues to work for now for backwards compatibility.
   private val rawZ3Args: ScallopOption[String] = opt[String]("z3Args",
     descr = (  "Warning: This option is deprecated due to standardization in option naming."
              + " Please use 'proverArgs' instead... "
              + "Command-line arguments which should be forwarded to Z3. "
-             + "The expected format is \"<opt> <opt> ... <opt>\", including the quotation marks."),
+             + "The expected format is \"<opt> <opt> ... <opt>\", excluding the quotation marks."),
     default = None,
     noshort = true
   )(forwardArgumentsConverter)
@@ -540,7 +529,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
              + " Please use 'proverConfigArgs' instead... "
              + "Configuration options which should be forwarded to Z3. "
              + "The expected format is \"<key>=<val> <key>=<val> ... <key>=<val>\", "
-             + "including the quotation marks. "
+             + "excluding the quotation marks. "
              + "The configuration options given here will override those from Silicon's Z3 preamble."),
     default = Some(Map()),
     noshort = true
@@ -678,7 +667,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     default = Some(false),
     noshort = true
   )
-  val enableBranchconditionReporting: ScallopOption[Boolean] = opt[Boolean]("enableBranchconditionReorting",
+  val enableBranchconditionReporting: ScallopOption[Boolean] = opt[Boolean]("enableBranchconditionReporting",
     descr = "Report branch conditions (can be useful for assertions that fail on multiple branches)",
     default = Some(false),
     noshort = true
@@ -765,6 +754,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     case other =>
       sys.error(s"Unexpected combination: $other")
   }
+
+  validateOpt(counterexample, enableMoreCompleteExhale) {
+    case (Some(_), Some(false)) => Left(  s"Option ${counterexample.name} requires setting "
+                                        + s"flag ${enableMoreCompleteExhale.name}")
+    case _ => Right(())
+  }
 
   validateFileOpt(logConfig)
   validateFileOpt(setAxiomatizationFile)

src/main/scala/Silicon.scala

@@ -17,7 +17,7 @@ import org.slf4j.LoggerFactory
 import viper.silver.ast
 import viper.silver.frontend.{DefaultStates, SilFrontend}
 import viper.silver.reporter._
-import viper.silver.verifier.{Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier}
+import viper.silver.verifier.{AbstractVerificationError => SilAbstractVerificationError, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier}
 import viper.silicon.interfaces.Failure
 import viper.silicon.logger.SymbExLogger
 import viper.silicon.reporting.condenseToViperResult
@@ -253,16 +253,13 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
           *  of all failures that report the same error (but on different branches, with different CounterExample)
           *  and put those into one failure */
           if (config.enableBranchconditionReporting())
-            allResults.groupBy(_.message.readableMessage(withId = true, withPosition = true)).map{case (_: String, fs:List[Failure]) =>
+            allResults.groupBy(failureFilterAndGroupingCriterion).map{case (_: String, fs:List[Failure]) =>
               fs.head.message.failureContexts = fs.flatMap(_.message.failureContexts)
               Failure(fs.head.message)
             }.toList
-             else allResults.distinctBy(f => f.message.readableMessage(withId = true, withPosition = true))
-        })
-        .sortBy(_.message.pos match { /* Order failures according to source position */
-          case pos: ast.HasLineColumn => (pos.line, pos.column)
-          case _ => (-1, -1)
+             else allResults.distinctBy(failureFilterAndGroupingCriterion)
         })
+        .sortBy(failureSortingCriterion)
 
 //    if (config.showStatistics.isDefined) {
 //      val proverStats = verifier.decider.statistics()
@@ -293,6 +290,28 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
     failures
   }
 
+  private def failureFilterAndGroupingCriterion(f: Failure): String = {
+    // apply transformers if available:
+    val transformedError = f.message match {
+      case e: SilAbstractVerificationError => e.transformedError()
+      case e => e
+    }
+    // create a string that identifies the given failure:
+    transformedError.readableMessage(withId = true, withPosition = true)
+  }
+
+  private def failureSortingCriterion(f: Failure): (Int, Int) = {
+    // apply transformers if available:
+    val transformedError = f.message match {
+      case e: SilAbstractVerificationError => e.transformedError()
+      case e => e
+    }
+    transformedError.pos match { /* Order failures according to source position */
+      case pos: ast.HasLineColumn => (pos.line, pos.column)
+      case _ => (-1, -1)
+    }
+  }
+
   private def logFailure(failure: Failure, log: String => Unit): Unit = { //TODO:J log context?
     log("\n" + failure.message.readableMessage(withId = true, withPosition = true))
   }

src/main/scala/decider/TermToSMTLib2Converter.scala

@@ -203,6 +203,7 @@ class TermToSMTLib2Converter
     case PermTimes(t0, t1) => renderBinaryOp("*", renderAsReal(t0), renderAsReal(t1))
     case IntPermTimes(t0, t1) => renderBinaryOp("*", renderAsReal(t0), renderAsReal(t1))
     case PermIntDiv(t0, t1) => renderBinaryOp("/", renderAsReal(t0), renderAsReal(t1))
+    case PermPermDiv(t0, t1) => renderBinaryOp("/", renderAsReal(t0), renderAsReal(t1))
     case PermMin(t0, t1) => renderBinaryOp("$Perm.min", render(t0), render(t1))
     case IsValidPermVar(v) => parens(text("$Perm.isValidVar") <+> render(v))
     case IsReadPermVar(v, ub) => parens(text("$Perm.isReadVar") <+> render(v) <+> render(ub))

src/main/scala/logger/writer/TermWriter.scala

@@ -57,8 +57,8 @@ object TermWriter {
 
   def toJSON(term: Term): JsValue = term match {
 
-    case b: BinaryOp[Term] => binary(b.op, toJSON(b.p0), toJSON(b.p1))
-    case u: UnaryOp[Term] => unary(u.op, toJSON(u.p))
+    case b: BinaryOp[Term@unchecked] => binary(b.op, toJSON(b.p0), toJSON(b.p1))
+    case u: UnaryOp[Term@unchecked] => unary(u.op, toJSON(u.p))
 
     // TODO: do we need triggers and isGlobal?
     case Quantification(quantifier, vars, body, _, name, _) =>

src/main/scala/rules/ChunkSupporter.scala

@@ -38,8 +38,7 @@ trait ChunkSupportRules extends SymbolicExecutionRules {
              resource: ast.Resource,
              args: Seq[Term],
              ve: VerificationError,
-             v: Verifier,
-             description: String)
+             v: Verifier)
             (Q: (State, Heap, Term, Verifier) => VerificationResult)
             : VerificationResult
 
@@ -74,32 +73,33 @@ object chunkSupporter extends ChunkSupportRules {
              (Q: (State, Heap, Term, Verifier) => VerificationResult)
              : VerificationResult = {
 
-    heuristicsSupporter.tryOperation[Heap, Term](description)(s, h, v)((s1, h1, v1, QS) => {
-      consume(s1, h1, resource, args, perms, ve, v1)((s2, h2, optSnap, v2) =>
-        optSnap match {
-          case Some(snap) =>
-            QS(s2, h2, snap.convert(sorts.Snap), v2)
-          case None =>
-            /* Not having consumed anything could mean that we are in an infeasible
-             * branch, or that the permission amount to consume was zero.
-             * Returning a fresh snapshot in these cases should not lose any information.
-             */
-            val fresh = v2.decider.fresh(sorts.Snap)
-            val s3 = s2.copy(functionRecorder = s2.functionRecorder.recordFreshSnapshot(fresh.applicable))
-            QS(s3, h2, fresh, v2)
-        })
-    })(Q)
+    consume2(s, h, resource, args, perms, ve, v)((s2, h2, optSnap, v2) =>
+      optSnap match {
+        case Some(snap) =>
+          Q(s2, h2, snap.convert(sorts.Snap), v2)
+        case None =>
+          /* Not having consumed anything could mean that we are in an infeasible
+           * branch, or that the permission amount to consume was zero.
+           *
+           * [MS 2022-01-28] Previously, a a fresh snapshot was retured, which also had to be
+           * registered with the function recorder. However, since nothing was consumed,
+           * returning the unit snapshot seems more appropriate.
+           */
+          val fresh = v2.decider.fresh(sorts.Snap)
+          val s3 = s2.copy(functionRecorder = s2.functionRecorder.recordFreshSnapshot(fresh.applicable))
+          Q(s3, h2, fresh, v2)
+      })
   }
 
-  private def consume(s: State,
-                      h: Heap,
-                      resource: ast.Resource,
-                      args: Seq[Term],
-                      perms: Term,
-                      ve: VerificationError,
-                      v: Verifier)
-                     (Q: (State, Heap, Option[Term], Verifier) => VerificationResult)
-                     : VerificationResult = {
+  private def consume2(s: State,
+                       h: Heap,
+                       resource: ast.Resource,
+                       args: Seq[Term],
+                       perms: Term,
+                       ve: VerificationError,
+                       v: Verifier)
+                      (Q: (State, Heap, Option[Term], Verifier) => VerificationResult)
+                      : VerificationResult = {
 
     val id = ChunkIdentifier(resource, Verifier.program)
     if (s.exhaleExt) {
@@ -185,31 +185,15 @@ object chunkSupporter extends ChunkSupportRules {
     Q(s.copy(functionRecorder = fr1), h1, v)
   }
 
-  @inline
   def lookup(s: State,
              h: Heap,
              resource: ast.Resource,
              args: Seq[Term],
              ve: VerificationError,
-             v: Verifier,
-             description: String)
+             v: Verifier)
             (Q: (State, Heap, Term, Verifier) => VerificationResult)
             : VerificationResult = {
 
-    heuristicsSupporter.tryOperation[Heap, Term](description)(s, h, v)((s1, h1, v1, QS) => {
-      lookup(s1, h1, resource, args, ve, v1)(QS)
-    })(Q)
-  }
-
-  private def lookup(s: State,
-                     h: Heap,
-                     resource: ast.Resource,
-                     args: Seq[Term],
-                     ve: VerificationError,
-                     v: Verifier)
-                    (Q: (State, Heap, Term, Verifier) => VerificationResult)
-                    : VerificationResult = {
-
     executionFlowController.tryOrFail2[Heap, Term](s.copy(h = h), v)((s1, v1, QS) => {
       val lookupFunction =
         if (s.isMethodVerification && Verifier.config.enableMoreCompleteExhale()) moreCompleteExhaleSupporter.lookupComplete _