Merge

src/main/scala/Config.scala

@@ -823,8 +823,7 @@ 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 =>

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/TermToZ3APIConverter.scala

@@ -31,6 +31,7 @@ class TermToZ3APIConverter
 
   val sortCache = mutable.HashMap[Sort, Z3Sort]()
   val funcDeclCache = mutable.HashMap[(String, Seq[Sort], Sort), Z3FuncDecl]()
+  val smtFuncDeclCache = mutable.HashMap[(String, Seq[Sort]), (Z3FuncDecl, Seq[Z3Expr])]()
   val termCache = mutable.HashMap[Term, Z3Expr]()
 
   def convert(s: Sort): Z3Sort = convertSort(s)
@@ -532,19 +533,37 @@ class TermToZ3APIConverter
     // workaround: since we cannot create a function application with just the name, we let Z3 parse
     // a string that uses the function, take the AST, and get the func decl from there, so that we can
     // programmatically create a func app.
-    val decls = args.zipWithIndex.map{case (a, i) => s"(declare-const workaround${i} ${smtlibConverter.convert(a.sort)})"}.mkString(" ")
-    val funcAppString = if (args.isEmpty) functionName else s"(${functionName} ${(0 until args.length).map(i => "workaround" + i).mkString(" ")})"
-    val assertion = decls + s" (assert (= ${funcAppString} ${funcAppString}))"
-    val workaround = ctx.parseSMTLIB2String(assertion, null, null, null, null)
-    val app = workaround(0).getArgs()(0)
-    val decl = app.getFuncDecl
-    val actualArgs =  if (decl.getArity > args.length){
-      // the function name we got wasn't just a function name but also contained a first argument.
-      // this happens with float operations where functionName contains a rounding mode.
-      app.getArgs.toSeq.slice(0, decl.getArity - args.length) ++ args.map(convertTerm(_))
-    }else {
-      args.map(convertTerm(_))
+
+    val cacheKey = (functionName, args.map(_.sort))
+    val (decl, additionalArgs: Seq[Z3Expr]) = if (smtFuncDeclCache.contains(cacheKey)) {
+      smtFuncDeclCache(cacheKey)
+    } else {
+      val declPreamble = "(define-sort $Perm () Real) " // ME: Re-declare the Perm sort.
+      // ME: The parsing happens in a fresh context that doesn't know any of our current declarations.
+      // In principle, it might be necessary to re-declare all sorts we're using anywhere. However, I don't see how there
+      // could be any Z3 internal functions that exist for those custom sorts. For the Real (i.e., Perm) sort, however,
+      // such functions exist. So we re-declare *only* this sort.
+      val decls = declPreamble + args.zipWithIndex.map { case (a, i) => s"(declare-const workaround${i} ${smtlibConverter.convert(a.sort)})" }.mkString(" ")
+      val funcAppString = if (args.nonEmpty)
+        s"(${functionName} ${(0 until args.length).map(i => "workaround" + i).mkString(" ")})"
+      else
+        functionName
+      val assertion = decls + s" (assert (= ${funcAppString} ${funcAppString}))"
+      val workaround = ctx.parseSMTLIB2String(assertion, null, null, null, null)
+      val app = workaround(0).getArgs()(0)
+      val decl = app.getFuncDecl
+      val additionalArgs = if (decl.getArity > args.length) {
+        // the function name we got wasn't just a function name but also contained a first argument.
+        // this happens with float operations where functionName contains a rounding mode.
+        app.getArgs.toSeq.slice(0, decl.getArity - args.length)
+      } else {
+        Seq()
+      }
+      smtFuncDeclCache.put(cacheKey, (decl, additionalArgs))
+      (decl, additionalArgs)
     }
+
+    val actualArgs = additionalArgs ++ args.map(convertTerm(_))
     ctx.mkApp(decl, actualArgs.toArray : _*)
   }
 
@@ -583,6 +602,7 @@ class TermToZ3APIConverter
     sanitizedNamesCache.clear()
     macros.clear()
     funcDeclCache.clear()
+    smtFuncDeclCache.clear()
     sortCache.clear()
     termCache.clear()
     unitConstructor = null

src/main/scala/decider/Z3ProverAPI.scala

@@ -10,7 +10,7 @@ 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, MacroDecl, Not, Quantification, Sort, SortDecl, SortWrapperDecl, Term, TriggerGenerator, sorts}
+import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, MacroDecl, Not, Quantification, Sort, SortDecl, SortWrapperDecl, Term, TriggerGenerator, Var, sorts}
 import viper.silicon.{Config, Map}
 import viper.silicon.verifier.Verifier
 import viper.silver.reporter.{InternalWarningMessage, Reporter}
@@ -261,11 +261,12 @@ class Z3ProverAPI(uniqueId: String,
     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 {
+        val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn =>
+          ptrn.isInstanceOf[Var] || ptrn.shallowCollect {
           case t => triggerGenerator.isForbiddenInTrigger(t)
         }.nonEmpty))
         q.copy(triggers = goodTriggers)
-    }()
+    }(_ => true)
     cleanTerm
   }
 

src/main/scala/rules/Evaluator.scala

@@ -1517,9 +1517,10 @@ object evaluator extends EvaluationRules {
           Success()
         })
       case pa: ast.PredicateAccess if s.heapDependentTriggers.contains(pa.loc(s.program)) && !Verifier.config.maskHeapMode() =>
-        val (axioms, trigs, _) = generatePredicateTrigger(pa, s, pve, v)
+        val (axioms, trigs, _, smDef) = generatePredicateTrigger(pa, s, pve, v)
         triggers = triggers.map(ts => ts ++ trigs)
         triggerAxioms = triggerAxioms ++ axioms
+        smDefs = smDefs ++ smDef
       case pa: ast.PredicateAccess =>
         val chunk = maskHeapSupporter.findMaskHeapChunk(s.h, pa.res(s.program))
         evals(s.copy(triggerExp = true), pa.args, _ => pve, v)((_, tArgs, _) => {
@@ -1530,9 +1531,10 @@ object evaluator extends EvaluationRules {
           Success()
         })
       case wand: ast.MagicWand if s.heapDependentTriggers.contains(MagicWandIdentifier(wand, s.program)) && !Verifier.config.maskHeapMode() =>
-        val (axioms, trigs, _) = generateWandTrigger(wand, s, pve, v)
+        val (axioms, trigs, _, smDef) = generateWandTrigger(wand, s, pve, v)
         triggers = triggers.map(ts => ts ++ trigs)
         triggerAxioms = triggerAxioms ++ axioms
+        smDefs = smDefs ++ smDef
       case wand: ast.MagicWand =>
         val mwi = MagicWandIdentifier(wand, s.program)
         val (hNew, chunk) = maskHeapSupporter.findOrCreateMaskHeapChunk(s.h, mwi, v)
@@ -1623,7 +1625,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
@@ -1645,11 +1651,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
@@ -1673,7 +1683,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/Executor.scala

@@ -214,20 +214,20 @@ object executor extends ExecutionRules {
                                               v1.decider.freshFunctions /* [BRANCH-PARALLELISATION] */)
                   v1.decider.prover.comment("Loop head block: Check well-definedness of edge conditions")
                   edgeConditions.foldLeft(Success(): VerificationResult) {
-                    case (fatalResult: FatalResult, _) => fatalResult
+                    case (result, _) if !result.continueVerification => result
                     case (intermediateResult, eCond) =>
-                      intermediateResult && executionFlowController.locally(s1, v1)((s2, v2) => {
+                      intermediateResult combine executionFlowController.locally(s1, v1)((s2, v2) => {
                         eval(s2, eCond, WhileFailed(eCond), v2)((_, _, _) =>
                           Success())})}})})
             && executionFlowController.locally(s, v)((s0, v0) => {
                 v0.decider.prover.comment("Loop head block: Establish invariant")
                 consumes(s0, invs, LoopInvariantNotEstablished, v0)((sLeftover, _, v1) => {
                   v1.decider.prover.comment("Loop head block: Execute statements of loop head block (in invariant state)")
                   phase1data.foldLeft(Success(): VerificationResult) {
-                    case (fatalResult: FatalResult, _) => fatalResult
+                    case (result, _) if !result.continueVerification => result
                     case (intermediateResult, (s1, pcs, ff1)) => /* [BRANCH-PARALLELISATION] ff1 */
                       val s2 = s1.copy(invariantContexts = sLeftover.h +: s1.invariantContexts)
-                      intermediateResult && executionFlowController.locally(s2, v1)((s3, v2) => {
+                      intermediateResult combine executionFlowController.locally(s2, v1)((s3, v2) => {
                         v2.decider.declareAndRecordAsFreshFunctions(ff1 -- v2.decider.freshFunctions) /* [BRANCH-PARALLELISATION] */
                         v2.decider.assume(pcs.assumptions)
                         v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
@@ -342,7 +342,7 @@ object executor extends ExecutionRules {
             val (relevantChunks, otherChunks) =
               quantifiedChunkSupporter.splitHeap[QuantifiedFieldChunk](s2.h, BasicChunkIdentifier(field.name))
             val hints = quantifiedChunkSupporter.extractHints(None, Seq(tRcvr))
-            val chunkOrderHeuristics = quantifiedChunkSupporter.hintBasedChunkOrderHeuristic(hints)
+            val chunkOrderHeuristics = quantifiedChunkSupporter.singleReceiverChunkOrderHeuristic(Seq(tRcvr), hints, v2)
             val s2p = if (s2.heapDependentTriggers.contains(field)){
               val (smDef1, smCache1) =
                 quantifiedChunkSupporter.summarisingSnapshotMap(

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -1231,8 +1231,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       case Some(heuristics) =>
         heuristics
       case None =>
-        quantifiedChunkSupporter.hintBasedChunkOrderHeuristic(
-          quantifiedChunkSupporter.extractHints(None, arguments))
+        quantifiedChunkSupporter.singleReceiverChunkOrderHeuristic(arguments,
+          quantifiedChunkSupporter.extractHints(None, arguments), v)
     }
 
     if (s.exhaleExt) {
@@ -1737,6 +1737,38 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       matchingChunks ++ otherChunks
     }
 
+  def singleReceiverChunkOrderHeuristic(receiver: Seq[Term], hints: Seq[Term], v: Verifier)
+                                       : Seq[QuantifiedBasicChunk] => Seq[QuantifiedBasicChunk] = {
+    // Heuristic that emulates greedy Silicon behavior for consuming single-receiver permissions.
+    // First:  Find singleton chunks that have the same receiver syntactically.
+    //         If so, consider those first, then all others.
+    // Second: If nothing matches syntactically, try to find a chunk that matches the receiver using the decider.
+    //         If that's the case, consider that chunk first, then all others.
+    // Third:  As a fallback, use the standard hint based heuristics.
+    val fallback = hintBasedChunkOrderHeuristic(hints)
+
+    (chunks: Seq[QuantifiedBasicChunk]) => {
+      val (syntacticMatches, others) = chunks.partition(c => c.singletonArguments.contains(receiver))
+      if (syntacticMatches.nonEmpty) {
+        syntacticMatches ++ others
+      } else {
+        val greedyMatch = chunks.find(c => c.singletonArguments match {
+          case Some(args) if args.length == receiver.length =>
+            args.zip(receiver).forall(ts => v.decider.check(ts._1 === ts._2, Verifier.config.checkTimeout()))
+          case _ =>
+            false
+        }).toSeq
+        if (greedyMatch.nonEmpty) {
+          greedyMatch ++ chunks.diff(greedyMatch)
+        } else {
+          // It doesn't seem to be any of the singletons. Use the fallback on the non-singletons.
+          val (qpChunks, singletons) = chunks.partition(_.singletonArguments.isEmpty)
+          fallback(qpChunks) ++ singletons
+        }
+      }
+    }
+  }
+
   def extractHints(cond: Option[Term], arguments: Seq[Term]): Seq[Term] = {
     var hints =
       arguments.flatMap {

src/main/scala/supporters/MethodSupporter.scala

@@ -84,6 +84,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif
           new java.io.File(s"${Verifier.config.tempDirectory()}/${method.name}.dot"))
       }
 
+      errorsReportedSoFar.set(0)
       val result =
         /* Combined the well-formedness check and the execution of the body, which are two separate
          * rules in Smans' paper.

src/main/scala/supporters/functions/FunctionData.scala

@@ -334,18 +334,27 @@ class FunctionData(val programFunction: ast.Function,
       })
   }
 
-  lazy val preconditionPropagationAxiom: Seq[Term] = {
+  lazy val bodyPreconditionPropagationAxiom: Seq[Term] = {
     val pre = preconditionFunctionApplication
     val bodyPreconditions = if (programFunction.body.isDefined) optBody.map(translatedBody => {
       val body = Implies(pre, FunctionPreconditionTransformer.transform(translatedBody, program))
       Forall(arguments, body, Seq(Trigger(functionApplication)))
     }) else None
+    val res = bodyPreconditions.toSeq
+    if (Verifier.config.heapFunctionEncoding())
+      res.map(t => transformToHeapVersion(t))
+    else
+      res
+  }
+
+  lazy val postPreconditionPropagationAxiom: Seq[Term] = {
+    val pre = preconditionFunctionApplication
     val postPreconditions = if (programFunction.posts.nonEmpty) {
       val bodyBindings: Map[Var, Term] = Map(formalResult -> limitedFunctionApplication)
       val bodies = translatedPosts.map(tPost => Let(bodyBindings, Implies(pre, FunctionPreconditionTransformer.transform(tPost, program))))
       bodies.map(b => Forall(arguments, b, Seq(Trigger(limitedFunctionApplication))))
     } else Seq()
-    val res = bodyPreconditions.toSeq ++ postPreconditions
+    val res = postPreconditions
     if (Verifier.config.heapFunctionEncoding())
       res.map(t => transformToHeapVersion(t))
     else

src/main/scala/supporters/functions/FunctionVerificationUnit.scala

@@ -191,10 +191,10 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
             emitAndRecordFunctionAxioms(data.qpFrameAxioms: _*)
           }
           emitAndRecordFunctionAxioms(data.postAxiom.toSeq: _*)
+          emitAndRecordFunctionAxioms(data.postPreconditionPropagationAxiom: _*)
           this.postConditionAxioms = this.postConditionAxioms ++ data.postAxiom.toSeq
 
           if (function.body.isEmpty) {
-            emitAndRecordFunctionAxioms(data.preconditionPropagationAxiom.toSeq: _*)
             result1
           } else {
             /* Phase 2: Verify the function's postcondition */
@@ -205,7 +205,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
                 data.verificationFailures = data.verificationFailures :+ fatalResult
               case _ =>
                 emitAndRecordFunctionAxioms(data.definitionalAxiom.toSeq: _*)
-                emitAndRecordFunctionAxioms(data.preconditionPropagationAxiom.toSeq: _*)
+                emitAndRecordFunctionAxioms(data.bodyPreconditionPropagationAxiom: _*)
             }
 
             result1 && result2