Merge branch 'master' into meilers_seq_set_axioms

src/main/scala/Config.scala

@@ -431,6 +431,10 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  lazy val outputProverLog: Boolean = {
+    enableTempDirectory.isSupplied || rawProverLogFile.isSupplied || rawZ3LogFile.isSupplied
+  }
+
   private val rawZ3Exe = opt[String]("z3Exe",
     descr = (s"Z3 executable. The environment variable ${Z3ProverStdIO.exeEnvironmentalVariable}"
              + " can also be used to specify the path of the executable."),
@@ -810,21 +814,14 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   validateOpt(counterexample, moreCompleteExhale, exhaleModeOption) {
     case (Some(_), Some(false), None) |
-         (Some(_), Some(_), Some(ExhaleMode.Greedy)) |
-         (Some(_), Some(_), Some(ExhaleMode.MoreCompleteOnDemand)) =>
+         (Some(_), Some(_), Some(ExhaleMode.Greedy)) =>
       Left(s"Option ${counterexample.name} requires setting "
         + s"${exhaleModeOption.name} to 1 (more complete exhale)")
     case (_, Some(true), Some(m)) if m != ExhaleMode.MoreComplete =>
       Left(s"Contradictory values given for options ${moreCompleteExhale.name} and ${exhaleModeOption.name}")
     case _ => Right(())
   }
 
-  validateOpt(assertionMode, parallelizeBranches) {
-    case (Some(AssertionMode.SoftConstraints), Some(true)) =>
-      Left(s"Assertion mode SoftConstraints is not supported in combination with ${parallelizeBranches.name}")
-    case _ => Right()
-  }
-
   validateFileOpt(logConfig)
   validateFileOpt(setAxiomatizationFile)
   validateFileOpt(multisetAxiomatizationFile)

src/main/scala/Silicon.scala

@@ -14,7 +14,7 @@ import ch.qos.logback.classic.{Level, Logger}
 import com.typesafe.scalalogging.LazyLogging
 import org.slf4j.LoggerFactory
 import viper.silver.ast
-import viper.silver.frontend.{DefaultStates, SilFrontend}
+import viper.silver.frontend.{DefaultStates, MinimalViperFrontendAPI, SilFrontend, ViperFrontendAPI}
 import viper.silver.reporter._
 import viper.silver.verifier.{AbstractVerificationError => SilAbstractVerificationError, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier}
 import viper.silicon.interfaces.Failure
@@ -377,6 +377,23 @@ class SiliconFrontend(override val reporter: Reporter,
   }
 }
 
+/**
+  * Silicon "frontend" for use by actual Viper frontends.
+  * Performs consistency check and verification.
+  * See [[viper.silver.frontend.ViperFrontendAPI]] for usage information.
+  */
+class SiliconFrontendAPI(override val reporter: Reporter)
+  extends SiliconFrontend(reporter) with ViperFrontendAPI
+
+/**
+  * Silicon "frontend" for use by actual Viper frontends.
+  * Performs only verification (no consistency check).
+  * See [[viper.silver.frontend.ViperFrontendAPI]] for usage information.
+  */
+class MinimalSiliconFrontendAPI(override val reporter: Reporter)
+  extends SiliconFrontend(reporter) with MinimalViperFrontendAPI
+
+
 object SiliconRunner extends SiliconRunnerInstance {
   def main(args: Array[String]): Unit = {
     runMain(args)

src/main/scala/decider/Decider.scala

@@ -382,7 +382,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def statistics(): Map[String, String] = prover.statistics()
 
-    override def generateModel(): Unit = proverAssert(False, None)
+    override def generateModel(): Unit = proverAssert(False, Verifier.config.assertTimeout.toOption)
 
     override def getModel(): Model = prover.getModel()
 

src/main/scala/decider/ProverStdIO.scala

@@ -83,7 +83,7 @@ abstract class ProverStdIO(uniqueId: String,
     }
     pushPopScopeDepth = 0
     lastTimeout = -1
-    logfileWriter = if (!Verifier.config.enableTempDirectory()) null else viper.silver.utility.Common.PrintWriter(Verifier.config.proverLogFile(uniqueId).toFile)
+    logfileWriter = if (!Verifier.config.outputProverLog) null else viper.silver.utility.Common.PrintWriter(Verifier.config.proverLogFile(uniqueId).toFile)
     proverPath = getProverPath
     prover = createProverInstance()
     input = new BufferedReader(new InputStreamReader(prover.getInputStream))

src/main/scala/decider/Z3ProverAPI.scala

@@ -9,19 +9,17 @@ package viper.silicon.decider
 import com.typesafe.scalalogging.LazyLogging
 import viper.silicon.common.config.Version
 import viper.silicon.interfaces.decider.{Prover, Result, Sat, Unknown, Unsat}
-import viper.silicon.state.{IdentifierFactory, State}
-import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, Ite, MacroDecl, Quantification, Sort, SortDecl, SortWrapperDecl, Term, Trigger, TriggerGenerator, sorts}
+import viper.silicon.state.IdentifierFactory
+import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, MacroDecl, Not, Quantification, Sort, SortDecl, SortWrapperDecl, Term, TriggerGenerator, sorts}
 import viper.silicon.{Config, Map}
 import viper.silicon.verifier.Verifier
 import viper.silver.reporter.{InternalWarningMessage, Reporter}
 import viper.silver.verifier.{MapEntry, ModelEntry, ModelParser, ValueEntry, DefaultDependency => SilDefaultDependency, Model => ViperModel}
 
-import java.io.PrintWriter
 import java.nio.file.Path
 import scala.collection.mutable
 import com.microsoft.z3._
 import com.microsoft.z3.enumerations.Z3_param_kind
-import viper.silicon.decider.Z3ProverAPI.oldVersionOnlyParams
 import viper.silicon.reporting.ExternalToolError
 
 import scala.jdk.CollectionConverters.MapHasAsJava
@@ -64,7 +62,6 @@ object Z3ProverAPI {
     "smt.qi.eager_threshold" -> 100.0,
   )
   val allParams = boolParams ++ intParams ++ stringParams ++ doubleParams
-  val oldVersionOnlyParams = Set("smt.arith.solver")
 }
 
 
@@ -122,26 +119,21 @@ class Z3ProverAPI(uniqueId: String,
         s
     }
 
-    val useOldVersionParams = version() <= Version("4.8.7.0")
     Z3ProverAPI.boolParams.foreach{
       case (k, v) =>
-        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
-          params.add(removeSmtPrefix(k), v)
+        params.add(removeSmtPrefix(k), v)
     }
     Z3ProverAPI.intParams.foreach{
       case (k, v) =>
-        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
-          params.add(removeSmtPrefix(k), v)
+        params.add(removeSmtPrefix(k), v)
     }
     Z3ProverAPI.doubleParams.foreach{
       case (k, v) =>
-        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
-          params.add(removeSmtPrefix(k), v)
+        params.add(removeSmtPrefix(k), v)
     }
     Z3ProverAPI.stringParams.foreach{
       case (k, v) =>
-        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
-          params.add(removeSmtPrefix(k), v)
+        params.add(removeSmtPrefix(k), v)
     }
     val userProvidedArgs = Verifier.config.proverConfigArgs
     prover = ctx.mkSolver()
@@ -256,19 +248,24 @@ class Z3ProverAPI(uniqueId: String,
         // When used via API, Z3 completely discards assumptions that contain invalid triggers (whereas it just ignores
         // the invalid trigger when used via stdio). Thus, to make sure our assumption is not discarded, we manually
         // walk through all quantifiers and remove invalid terms inside the trigger.
-        triggerGenerator.setCustomIsForbiddenInTrigger(triggerGenerator.advancedIsForbiddenInTrigger)
-        val cleanTerm = term.transform{
-          case q@Quantification(_, _, _, triggers, _, _, _) if triggers.nonEmpty =>
-            val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn => ptrn.shallowCollect{
-              case t => triggerGenerator.isForbiddenInTrigger(t)
-            }.nonEmpty))
-            q.copy(triggers = goodTriggers)
-        }()
+        val cleanTerm = cleanTriggers(term)
         prover.add(termConverter.convert(cleanTerm).asInstanceOf[BoolExpr])
         reporter.report(InternalWarningMessage("Z3 error: " + e.getMessage))
     }
   }
 
+  def cleanTriggers(term: Term): Term = {
+    triggerGenerator.setCustomIsForbiddenInTrigger(triggerGenerator.advancedIsForbiddenInTrigger)
+    val cleanTerm = term.transform {
+      case q@Quantification(_, _, _, triggers, _, _, _) if triggers.nonEmpty =>
+        val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn => ptrn.shallowCollect {
+          case t => triggerGenerator.isForbiddenInTrigger(t)
+        }.nonEmpty))
+        q.copy(triggers = goodTriggers)
+    }()
+    cleanTerm
+  }
+
   def assert(goal: Term, timeout: Option[Int]): Boolean = {
     endPreamblePhase()
 
@@ -279,7 +276,14 @@ class Z3ProverAPI(uniqueId: String,
       }
       result
     } catch {
-      case e: Z3Exception => throw ExternalToolError("Prover", "Z3 error: " + e.getMessage)
+      case e: Z3Exception => {
+        val cleanGoal = cleanTriggers(goal)
+        if (cleanGoal == goal) {
+          throw ExternalToolError("Prover", "Z3 error: " + e.getMessage)
+        } else {
+          assert(cleanGoal, timeout)
+        }
+      }
     }
   }
 
@@ -320,8 +324,13 @@ class Z3ProverAPI(uniqueId: String,
 
   protected def retrieveAndSaveModel(): Unit = {
     if (Verifier.config.counterexample.toOption.isDefined) {
-      val model = prover.getModel
-      lastModel = model
+      try {
+        val model = prover.getModel
+        lastModel = model
+      } catch {
+        case _: Z3Exception =>
+          lastModel = null
+      }
     }
   }
 
@@ -337,7 +346,7 @@ class Z3ProverAPI(uniqueId: String,
 
     val guard = fresh("grd", Nil, sorts.Bool)
     val guardApp = App(guard, Nil)
-    val goalImplication = Implies(guardApp, goal)
+    val goalImplication = Implies(guardApp, Not(goal))
 
     prover.add(termConverter.convertTerm(goalImplication).asInstanceOf[BoolExpr])
 
@@ -451,7 +460,11 @@ class Z3ProverAPI(uniqueId: String,
     for (constDecl <- lastModel.getConstDecls){
       val constInterp = lastModel.getConstInterp(constDecl)
       val constName = constDecl.getName.toString
-      val entry = fastparse.parse(constInterp.toString, ModelParser.value(_)).get.value
+      val constInterpString = constInterp match {
+        case rn: RatNum => s"(/ ${rn.getBigIntNumerator} ${rn.getBigIntDenominator})"
+        case _ => constInterp.toString
+      }
+      val entry = fastparse.parse(constInterpString, ModelParser.value(_)).get.value
       entries.update(constName, entry)
     }
     for (funcDecl <- lastModel.getFuncDecls) {

src/main/scala/rules/Evaluator.scala

@@ -7,7 +7,7 @@
 package viper.silicon.rules
 
 import viper.silver.ast
-import viper.silver.verifier.{CounterexampleTransformer, PartialVerificationError, TypecheckerWarning}
+import viper.silver.verifier.{CounterexampleTransformer, PartialVerificationError, VerifierWarning}
 import viper.silver.verifier.errors.{ErrorWrapperWithExampleTransformer, PreconditionInAppFalse}
 import viper.silver.verifier.reasons._
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
@@ -23,8 +23,8 @@ import viper.silicon.verifier.Verifier
 import viper.silicon.{Map, TriggerSets}
 import viper.silicon.interfaces.state.{ChunkIdentifer, NonQuantifiedChunk}
 import viper.silicon.logger.records.data.{CondExpRecord, EvaluateRecord, ImpliesRecord}
-import viper.silver.reporter.WarningsDuringTypechecking
-import viper.silver.ast.WeightedQuantifier
+import viper.silver.reporter.{AnnotationWarning, WarningsDuringVerification}
+import viper.silver.ast.{AnnotationInfo, WeightedQuantifier}
 
 /* TODO: With the current design w.r.t. parallelism, eval should never "move" an execution
  *       to a different verifier. Hence, consider not passing the verifier to continuations
@@ -290,8 +290,12 @@ object evaluator extends EvaluationRules {
             evalInOldState(s, lbl, e0, pve, v)(Q)}
 
       case ast.Let(x, e0, e1) =>
-        eval(s, e0, pve, v)((s1, t0, v1) =>
-          eval(s1.copy(g = s1.g + (x.localVar, t0)), e1, pve, v1)(Q))
+        eval(s, e0, pve, v)((s1, t0, v1) => {
+          val t = v1.decider.appliedFresh("letvar", v1.symbolConverter.toSort(x.typ), s1.relevantQuantifiedVariables)
+          v1.decider.assume(t === t0)
+          val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t.applicable.asInstanceOf[Function])
+          eval(s1.copy(g = s1.g + (x.localVar, t0), functionRecorder = newFuncRec), e1, pve, v1)(Q)
+        })
 
       /* Strict evaluation of AND */
       case ast.And(e0, e1) if Verifier.config.disableShortCircuitingEvaluations() =>
@@ -642,9 +646,25 @@ object evaluator extends EvaluationRules {
             (exists, Exists, exists.triggers)
           case _: ast.ForPerm => sys.error(s"Unexpected quantified expression $sourceQuant")
         }
-        val quantWeight = sourceQuant.info match {
-          case w: WeightedQuantifier => Some(w.weight)
-          case _ => None
+        val quantWeight = sourceQuant.info.getUniqueInfo[WeightedQuantifier] match {
+          case Some(w) =>
+            if (w.weight >= 0) {
+              Some(w.weight)
+            } else {
+              v.reporter.report(AnnotationWarning(s"Invalid quantifier weight annotation: ${w}"))
+              None
+            }
+          case None => sourceQuant.info.getUniqueInfo[AnnotationInfo] match {
+            case Some(ai) if ai.values.contains("weight") =>
+              ai.values("weight") match {
+                case Seq(w) if w.toIntOption.exists(w => w >= 0) =>
+                  Some(w.toInt)
+                case s =>
+                  v.reporter.report(AnnotationWarning(s"Invalid quantifier weight annotation: ${s}"))
+                  None
+              }
+            case _ => None
+          }
         }
 
         val body = eQuant.exp
@@ -1345,8 +1365,8 @@ object evaluator extends EvaluationRules {
         Q(s, cachedTriggerTerms ++ remainingTriggerTerms, v)
       case _ =>
         for (e <- remainingTriggerExpressions)
-          v.reporter.report(WarningsDuringTypechecking(Seq(
-            TypecheckerWarning(s"Might not be able to use trigger $e, since it is not evaluated while evaluating the body of the quantifier", e.pos))))
+          v.reporter.report(WarningsDuringVerification(Seq(
+            VerifierWarning(s"Might not be able to use trigger $e, since it is not evaluated while evaluating the body of the quantifier", e.pos))))
         Q(s, cachedTriggerTerms, v)
     }
   }
@@ -1396,13 +1416,15 @@ object evaluator extends EvaluationRules {
         triggerAxioms = triggerAxioms ++ axioms
         smDefs = smDefs ++ smDef
       case pa: ast.PredicateAccess if s.heapDependentTriggers.contains(pa.loc(s.program)) =>
-        val (axioms, trigs, _) = generatePredicateTrigger(pa, s, pve, v)
+        val (axioms, trigs, _, smDef) = generatePredicateTrigger(pa, s, pve, v)
         triggers = triggers ++ trigs
         triggerAxioms = triggerAxioms ++ axioms
+        smDefs = smDefs ++ smDef
       case wand: ast.MagicWand if s.heapDependentTriggers.contains(MagicWandIdentifier(wand, s.program)) =>
-        val (axioms, trigs, _) = generateWandTrigger(wand, s, pve, v)
+        val (axioms, trigs, _, smDef) = generateWandTrigger(wand, s, pve, v)
         triggers = triggers ++ trigs
         triggerAxioms = triggerAxioms ++ axioms
+        smDefs = smDefs ++ smDef
       case e => evalTrigger(s, Seq(e), pve, v)((_, t, _) => {
         triggers = triggers ++ t
         Success()
@@ -1482,7 +1504,11 @@ object evaluator extends EvaluationRules {
   }
 
   /* TODO: Try to unify with generateFieldTrigger above, or at least with generateWandTrigger below */
-  private def generatePredicateTrigger(pa: ast.PredicateAccess, s: State, pve: PartialVerificationError, v: Verifier): (Seq[Term], Seq[Term], PredicateTrigger) = {
+  private def generatePredicateTrigger(pa: ast.PredicateAccess,
+                                       s: State,
+                                       pve: PartialVerificationError,
+                                       v: Verifier)
+                                      : (Seq[Term], Seq[Term], PredicateTrigger, Seq[SnapshotMapDefinition]) = {
     var axioms = Seq.empty[Term]
     var triggers = Seq.empty[Term]
     var mostRecentTrig: PredicateTrigger = null
@@ -1504,11 +1530,15 @@ object evaluator extends EvaluationRules {
       Success()
     })
 
-    (axioms, triggers, mostRecentTrig)
+    (axioms, triggers, mostRecentTrig, Seq(smDef1))
   }
 
   /* TODO: See comments for generatePredicateTrigger above */
-  private def generateWandTrigger(wand: ast.MagicWand, s: State, pve: PartialVerificationError, v: Verifier): (Seq[Term], Seq[Term], PredicateTrigger) = {
+  private def generateWandTrigger(wand: ast.MagicWand,
+                                  s: State,
+                                  pve: PartialVerificationError,
+                                  v: Verifier)
+                                 : (Seq[Term], Seq[Term], PredicateTrigger, Seq[SnapshotMapDefinition]) = {
     var axioms = Seq.empty[Term]
     var triggers = Seq.empty[Term]
     var mostRecentTrig: PredicateTrigger = null
@@ -1532,7 +1562,7 @@ object evaluator extends EvaluationRules {
       Success()
     })
 
-    (axioms, triggers, mostRecentTrig)
+    (axioms, triggers, mostRecentTrig, Seq(smDef1))
   }
 
   /* Evaluate a sequence of expressions in Order

src/main/scala/rules/ExecutionFlowController.scala

@@ -6,6 +6,7 @@
 
 package viper.silicon.rules
 
+import viper.silver.ast
 import viper.silicon.Config.ExhaleMode
 import viper.silicon.interfaces._
 import viper.silicon.logger.records.data.CommentRecord
@@ -129,7 +130,19 @@ object executionFlowController extends ExecutionFlowRules {
 
         val comLog = new CommentRecord("Retry", s0, v.decider.pcs)
         val sepIdentifier = v.symbExLog.openScope(comLog)
-        val temporaryMCE = Verifier.config.exhaleMode != ExhaleMode.Greedy
+        val temporaryMCE = s0.currentMember.map(_.info.getUniqueInfo[ast.AnnotationInfo]) match {
+          case Some(Some(ai)) if ai.values.contains("exhaleMode") =>
+            ai.values("exhaleMode") match {
+              case Seq("0") | Seq("greedy") =>
+                false
+              case Seq("1") | Seq("mce") | Seq("moreCompleteExhale") | Seq("2") | Seq("mceOnDemand") => true
+              case _ =>
+                // Invalid annotation was already reported when creating the initial state.
+                Verifier.config.exhaleMode != ExhaleMode.Greedy
+            }
+          case _ => Verifier.config.exhaleMode != ExhaleMode.Greedy
+        }
+
         action(s0.copy(retrying = true, retryLevel = s.retryLevel, moreCompleteExhale = temporaryMCE), v, (s1, r, v1) => {
           v1.symbExLog.closeScope(sepIdentifier)
           Q(s1.copy(retrying = false, moreCompleteExhale = s0.moreCompleteExhale), r, v1)