Merge

src/main/scala/Config.scala

@@ -172,6 +172,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val reportReasonUnknown: ScallopOption[Boolean] = opt[Boolean]("reportReasonUnknown",
+    descr = "For every verification error, include the reason the SMT solver reported unknown.",
+    default = Some(false),
+    noshort = true
+  )
+
   val recursivePredicateUnfoldings: ScallopOption[Int] = opt[Int]("recursivePredicateUnfoldings",
     descr = (  "Evaluate n unfolding expressions in the body of predicates that (transitively) unfold "
              + "other instances of themselves (default: 1)"),
@@ -435,8 +441,8 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
-  val disableTempDirectory: ScallopOption[Boolean] = opt[Boolean]("disableTempDirectory",
-    descr = "Disable the creation of temporary data (default: ./tmp)",
+  val enableTempDirectory: ScallopOption[Boolean] = opt[Boolean]("enableTempDirectory",
+    descr = "Enable the creation of temporary directory to log prover interactions (default: ./tmp)",
     default = Some(false),
     noshort = true
   )

src/main/scala/decider/Decider.scala

@@ -34,7 +34,7 @@ trait Decider {
   def pushScope(): Unit
   def popScope(): Unit
 
-  def checkSmoke(): Boolean
+  def checkSmoke(isAssert: Boolean = false): Boolean
 
   def setCurrentBranchCondition(t: Term, te: Option[ast.Exp] = None): Unit
   def setPathConditionMark(): Mark
@@ -120,7 +120,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     private def getProver(prover: String): Prover = prover match {
       case Z3ProverStdIO.name => new Z3ProverStdIO(uniqueId, termConverter, identifierFactory, reporter)
       case Cvc5ProverStdIO.name => new Cvc5ProverStdIO(uniqueId, termConverter, identifierFactory, reporter)
-      case Z3ProverAPI.name => new Z3ProverAPI(uniqueId, new TermToZ3APIConverter(), identifierFactory, reporter)
+      case Z3ProverAPI.name => new Z3ProverAPI(uniqueId, new TermToZ3APIConverter(), identifierFactory, reporter, triggerGenerator)
       case prover =>
         val msg1 = s"Unknown prover '$prover' provided. Defaulting to ${Z3ProverStdIO.name}."
         logger warn msg1
@@ -236,7 +236,10 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     /* Asserting facts */
 
-    def checkSmoke(): Boolean = prover.check(Verifier.config.checkTimeout.toOption) == Unsat
+    def checkSmoke(isAssert: Boolean = false): Boolean = {
+      val timeout = if (isAssert) Verifier.config.assertTimeout.toOption else Verifier.config.checkTimeout.toOption
+      prover.check(timeout) == Unsat
+    }
 
     def check(t: Term, timeout: Int): Boolean = deciderAssert(t, Some(timeout))
 

src/main/scala/decider/ProverStdIO.scala

@@ -83,7 +83,7 @@ abstract class ProverStdIO(uniqueId: String,
     }
     pushPopScopeDepth = 0
     lastTimeout = -1
-    logfileWriter = if (Verifier.config.disableTempDirectory()) null else viper.silver.utility.Common.PrintWriter(Verifier.config.proverLogFile(uniqueId).toFile)
+    logfileWriter = if (!Verifier.config.enableTempDirectory()) null else viper.silver.utility.Common.PrintWriter(Verifier.config.proverLogFile(uniqueId).toFile)
     proverPath = getProverPath
     prover = createProverInstance()
     input = new BufferedReader(new InputStreamReader(prover.getInputStream))
@@ -254,6 +254,7 @@ abstract class ProverStdIO(uniqueId: String,
     if (!result) {
       retrieveReasonUnknown()
       retrieveAndSaveModel()
+      retrieveReasonUnknown()
     }
 
     pop()
@@ -288,8 +289,13 @@ abstract class ProverStdIO(uniqueId: String,
   }
 
   protected def retrieveReasonUnknown(): Unit = {
-    writeLine("(get-info :reason-unknown)")
-    lastReasonUnknown = readLine()
+    if (Verifier.config.reportReasonUnknown()) {
+      writeLine("(get-info :reason-unknown)")
+      var result = readLine()
+      if (result.startsWith("(:reason-unknown \""))
+        result = result.substring(18, result.length - 2)
+      lastReasonUnknown = result
+    }
   }
 
   override def hasModel(): Boolean = {
@@ -484,7 +490,7 @@ abstract class ProverStdIO(uniqueId: String,
   override def getReasonUnknown(): String = lastReasonUnknown
 
   override def clearLastAssert(): Unit = {
-    lastModel = null
     lastReasonUnknown = null
+    lastModel = null
   }
 }

src/main/scala/decider/TermToSMTLib2Converter.scala

@@ -419,7 +419,7 @@ class TermToSMTLib2Converter
     if (args.nonEmpty)
       parens(docAppNoParens)
     else
-      parens(text("as") <+> docAppNoParens <+> render(outSort))
+      docAppNoParens
   }
 
   protected def render(q: Quantifier): Cont = q match {

src/main/scala/decider/Z3ProverAPI.scala

@@ -9,19 +9,18 @@ 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
-import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, Ite, MacroDecl, Quantification, Sort, SortDecl, SortWrapperDecl, Term, sorts}
+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.{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.{boolParams, doubleParams, intParams, oldVersionOnlyParams, stringParams}
+import viper.silicon.decider.Z3ProverAPI.oldVersionOnlyParams
 import viper.silicon.reporting.ExternalToolError
 
 import scala.jdk.CollectionConverters.MapHasAsJava
@@ -49,7 +48,7 @@ object Z3ProverAPI {
   val boolParams = Map(
     "smt.delay_units" -> true,
     "smt.mbqi" -> false,
-    // "pp.bv_literals" -> false,
+    //"pp.bv_literals" -> false,  // This is part of z3config.smt2 but Z3 won't accept it via API.
     "model.v2" -> true
   )
   val intParams = Map(
@@ -63,28 +62,29 @@ object Z3ProverAPI {
   val doubleParams: Map[String, Double] = Map(
     "smt.qi.eager_threshold" -> 100.0,
   )
+  val allParams = boolParams ++ intParams ++ stringParams ++ doubleParams
   val oldVersionOnlyParams = Set("smt.arith.solver")
 }
 
 
 class Z3ProverAPI(uniqueId: String,
                   termConverter: TermToZ3APIConverter,
                   identifierFactory: IdentifierFactory,
-                  reporter: Reporter)
+                  reporter: Reporter,
+                  triggerGenerator: TriggerGenerator)
     extends Prover
       with LazyLogging
 {
 
   /* protected */ var pushPopScopeDepth = 0
   protected var lastTimeout: Int = -1
-  protected var logfileWriter: PrintWriter = _
   protected var prover: Solver = _
   protected var ctx: Context = _
   protected var params: Params = _
 
   var proverPath: Path = _
+  var lastReasonUnknown : String = _
   var lastModel : Model = _
-  var lastReasonUnknown: String = _
 
   var emittedPreambleString = mutable.Queue[String]()
   var preamblePhaseOver = false
@@ -111,16 +111,20 @@ class Z3ProverAPI(uniqueId: String,
   def start(): Unit = {
     pushPopScopeDepth = 0
     lastTimeout = -1
-    logfileWriter = if (Verifier.config.disableTempDirectory()) null else viper.silver.utility.Common.PrintWriter(Verifier.config.proverLogFile(uniqueId).toFile)
     ctx = new Context(Z3ProverAPI.initialOptions.asJava)
-    val useOldVersionParams = version() <= Version("4.8.7.0")
+
+    val params = ctx.mkParams()
+
+    // When setting parameters via API, we have to remove the smt. prefix
     def removeSmtPrefix(s: String) = {
       if (s.startsWith("smt."))
         s.substring(4)
       else
         s
     }
-    params = ctx.mkParams()
+
+
+    val useOldVersionParams = version() <= Version("4.8.7.0")
     Z3ProverAPI.boolParams.foreach{
       case (k, v) =>
         if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
@@ -163,7 +167,6 @@ class Z3ProverAPI(uniqueId: String,
           params.add(key, vl)
         case _ =>
           reporter.report(InternalWarningMessage("Z3 error: unknown parameter" + key))
-
       }
     }
     prover.setParameters(params)
@@ -256,11 +259,11 @@ 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 i: Ite => i
-              case i: Implies => i
+              case t => triggerGenerator.isForbiddenInTrigger(t)
             }.nonEmpty))
             q.copy(triggers = goodTriggers)
         }()
@@ -326,7 +329,9 @@ class Z3ProverAPI(uniqueId: String,
   }
 
   protected def retrieveReasonUnknown(): Unit = {
-    lastReasonUnknown = prover.getReasonUnknown
+    if (Verifier.config.reportReasonUnknown()) {
+      lastReasonUnknown = prover.getReasonUnknown
+    }
   }
 
   protected def assertUsingSoftConstraints(goal: Term, timeout: Option[Int]): (Boolean, Long) = {
@@ -367,12 +372,10 @@ class Z3ProverAPI(uniqueId: String,
     if (!preamblePhaseOver) {
       preamblePhaseOver = true
 
-      // Setting all options again, since otherwise some of them seem to get lost.
+      // Setting all options again , since otherwise some of them seem to get lost.
       val standardOptionPrefix = Seq("(set-option :auto_config false)", "(set-option :type_check true)") ++
-        boolParams.map(bp => s"(set-option :${bp._1} ${bp._2})") ++
-        intParams.map(bp => s"(set-option :${bp._1} ${bp._2})") ++
-        doubleParams.map(bp => s"(set-option :${bp._1} ${bp._2})") ++
-        stringParams.map(bp => s"(set-option :${bp._1} ${bp._2})")
+        Z3ProverAPI.allParams.map(bp => s"(set-option :${bp._1} ${bp._2})")
+
       val customOptionPrefix = Verifier.config.proverConfigArgs.map(a => s"(set-option :${a._1} ${a._2})")
 
       val merged = (standardOptionPrefix ++ customOptionPrefix ++ emittedPreambleString).mkString("\n")
@@ -446,12 +449,6 @@ class Z3ProverAPI(uniqueId: String,
     }
   }
 
-  protected def logToFile(str: String): Unit = {
-    if (logfileWriter != null) {
-      logfileWriter.println(str)
-    }
-  }
-
   override def getModel(): ViperModel = {
     val entries = new mutable.HashMap[String, ModelEntry]()
     for (constDecl <- lastModel.getConstDecls){
@@ -485,8 +482,8 @@ class Z3ProverAPI(uniqueId: String,
   }
 
   override def clearLastAssert(): Unit = {
-    lastModel = null
     lastReasonUnknown = null
+    lastModel = null
   }
 
   protected def setTimeout(timeout: Option[Int]): Unit = {

src/main/scala/interfaces/Verification.scala

@@ -26,6 +26,7 @@ import viper.silver.ast.Program
 sealed abstract class VerificationResult {
   var previous: Vector[VerificationResult] = Vector() //Sets had problems with equality
   val continueVerification: Boolean = true
+  var isReported: Boolean = false
 
   def isFatal: Boolean
   def &&(other: => VerificationResult): VerificationResult
@@ -100,7 +101,10 @@ case class Failure/*[ST <: Store[ST],
   override lazy val toString: String = message.readableMessage
 }
 
-case class SiliconFailureContext(branchConditions: Seq[ast.Exp], counterExample: Option[Counterexample], reasonUnknown: Option[String]) extends FailureContext {
+
+case class SiliconFailureContext(branchConditions: Seq[ast.Exp],
+                                 counterExample: Option[Counterexample],
+                                 reasonUnknown: Option[String]) extends FailureContext {
   lazy val branchConditionString: String = {
     if(branchConditions.nonEmpty) {
       val branchConditionsString =
@@ -118,7 +122,15 @@ case class SiliconFailureContext(branchConditions: Seq[ast.Exp], counterExample:
     counterExample.fold("")(ce => s"\n\t\tcounterexample:\n$ce")
   }
 
-  override lazy val toString: String = branchConditionString + counterExampleString + s"\nPotential incompleteness: ${reasonUnknown}"
+  lazy val reasonUnknownString: String = {
+    if (reasonUnknown.isDefined) {
+      s"\nPotential prover incompleteness: ${reasonUnknown.get}"
+    } else {
+      ""
+    }
+  }
+
+  override lazy val toString: String = branchConditionString + counterExampleString + reasonUnknownString
 }
 
 trait SiliconCounterexample extends Counterexample {

src/main/scala/interfaces/decider/Prover.scala

@@ -39,7 +39,6 @@ trait Prover extends ProverLike with StatefulComponent {
   def getModel(): Model
   def getReasonUnknown(): String
   def clearLastAssert(): Unit
-
   def name: String
   def minVersion: Version
   def maxVersion: Option[Version]

src/main/scala/reporting/Converter.scala

@@ -254,7 +254,7 @@ object Converter {
       case Unit              => UnprocessedModelEntry(ConstantEntry(snapUnitId))
       case IntLiteral(x)     => LitIntEntry(x)
       case t: BooleanLiteral => LitBoolEntry(t.value)
-      case Null            => VarEntry(model.entries(nullRefId).toString, sorts.Ref)
+      case Null              => VarEntry(model.entries(nullRefId).toString, sorts.Ref)
       case Var(_, sort) =>
         val key: String = term.toString
         val entry: Option[ModelEntry] = model.entries.get(key)

src/main/scala/rules/Brancher.scala

@@ -10,10 +10,13 @@ import java.util.concurrent._
 import viper.silicon.common.concurrency._
 import viper.silicon.decider.PathConditionStack
 import viper.silicon.interfaces.{Unreachable, VerificationResult}
+import viper.silicon.reporting.condenseToViperResult
 import viper.silicon.state.State
 import viper.silicon.state.terms.{FunctionDecl, MacroDecl, Not, Term}
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
+import viper.silver.reporter.{BranchFailureMessage}
+import viper.silver.verifier.Failure
 
 trait BranchingRules extends SymbolicExecutionRules {
   def branch(s: State,
@@ -151,17 +154,25 @@ object brancher extends BranchingRules {
         CompletableFuture.completedFuture(Seq(Unreachable()))
       }
 
-    val res = (if (executeThenBranch) {
-      v.symbExLog.markReachable(uidBranchPoint)
-      executionFlowController.locally(s, v)((s1, v1) => {
-        v1.decider.prover.comment(s"[then-branch: $cnt | $condition]")
-        v1.decider.setCurrentBranchCondition(condition, conditionExp)
+    val res = {
+      val thenRes = if (executeThenBranch) {
+          v.symbExLog.markReachable(uidBranchPoint)
+          executionFlowController.locally(s, v)((s1, v1) => {
+            v1.decider.prover.comment(s"[then-branch: $cnt | $condition]")
+            v1.decider.setCurrentBranchCondition(condition, conditionExp)
 
-        fThen(v1.stateConsolidator.consolidateIfRetrying(s1, v1), v1)
-      })
-    } else {
-      Unreachable()
-    }).combine({
+            fThen(v1.stateConsolidator.consolidateIfRetrying(s1, v1), v1)
+          })
+        } else {
+          Unreachable()
+        }
+      if (thenRes.isFatal && !thenRes.isReported && s.parallelizeBranches && s.isLastRetry) {
+        thenRes.isReported = true
+        v.reporter.report(BranchFailureMessage("silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable],
+          condenseToViperResult(Seq(thenRes)).asInstanceOf[Failure]))
+      }
+      thenRes
+    }.combine({
 
       /* [BRANCH-PARALLELISATION] */
       var rs: Seq[VerificationResult] = null
@@ -189,6 +200,11 @@ object brancher extends BranchingRules {
       }
 
       assert(rs.length == 1, s"Expected a single verification result but found ${rs.length}")
+      if (rs.head.isFatal && !rs.head.isReported && s.parallelizeBranches && s.isLastRetry) {
+        rs.head.isReported = true
+        v.reporter.report(BranchFailureMessage("silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable],
+          condenseToViperResult(Seq(rs.head)).asInstanceOf[Failure]))
+      }
       rs.head
 
     }, alwaysWaitForOther = parallelizeElseBranch)