Merge pull request #784 from viperproject/meilers_proverArgs_annotation

Adding an annotation to set prover arguments per method

Author: marcoeilers

src/main/scala/decider/Decider.scala

@@ -30,6 +30,10 @@ import scala.collection.mutable
 
 trait Decider {
   def prover: Prover
+  def setProverOptions(options: Map[String, String]): Unit
+  def getProverOptions(): Map[String, String]
+  def resetProverOptions(): Unit
+
   def pcs: PathConditionStack
 
   def pushScope(): Unit
@@ -106,6 +110,9 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     private var _freshFunctionStack: Stack[mutable.HashSet[FunctionDecl]] = _
     private var _freshMacroStack: Stack[mutable.ListBuffer[MacroDecl]] = _
 
+    private var _proverOptions: Map[String, String] = Map.empty
+    private var _proverResetOptions: Map[String, String] = Map.empty
+
     def prover: Prover = _prover
 
     def pcs: PathConditionStack = pathConditions
@@ -165,6 +172,20 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
       None
     }
 
+    override def setProverOptions(options: Map[String, String]): Unit = {
+      _proverOptions = _proverOptions ++ options
+      val resetOptions = _proverOptions.map { case (k, v) => (k, _prover.setOption(k, v)) }
+      _proverResetOptions = resetOptions ++ _proverResetOptions
+    }
+
+    override def getProverOptions(): Map[String, String] = _proverOptions
+
+    override def resetProverOptions(): Unit = {
+      _proverResetOptions.foreach { case (k, v) => _prover.setOption(k, v) }
+      _proverResetOptions = Map.empty
+      _proverOptions = Map.empty
+    }
+
     /* Life cycle */
 
     def start(): Unit = {

src/main/scala/decider/ProverStdIO.scala

@@ -195,6 +195,15 @@ abstract class ProverStdIO(uniqueId: String,
     readSuccess()
   }
 
+  override def setOption(name: String, value: String): String = {
+    writeLine(s"(get-option :${name})")
+    val oldVal = readLine()
+    if (oldVal == "unsupported")
+      throw ProverInteractionFailed(uniqueId, s"Prover does not support option $name")
+    emit(s"(set-option :$name $value)")
+    oldVal
+  }
+
 //  private val quantificationLogger = bookkeeper.logfiles("quantification-problems")
 
   def assume(term: Term): Unit = {

src/main/scala/decider/Z3ProverAPI.scala

@@ -20,7 +20,7 @@ import java.nio.file.Path
 import scala.collection.mutable
 import com.microsoft.z3._
 import com.microsoft.z3.enumerations.Z3_param_kind
-import viper.silicon.reporting.ExternalToolError
+import viper.silicon.reporting.{ExternalToolError, ProverInteractionFailed}
 
 import scala.jdk.CollectionConverters.MapHasAsJava
 import scala.util.Random
@@ -239,6 +239,10 @@ class Z3ProverAPI(uniqueId: String,
     }
   }
 
+  override def setOption(name: String, value: String): String = {
+    throw new ProverInteractionFailed(uniqueId, "Dynamically setting prover options via Z3 API is currently not supported.")
+  }
+
   def assume(term: Term): Unit = {
     try {
       if (preamblePhaseOver)

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

@@ -22,6 +22,7 @@ trait ProverLike {
   def emit(content: String): Unit
   def emit(contents: Iterable[String]): Unit = { contents foreach emit }
   def emitSettings(contents: Iterable[String]): Unit
+  def setOption(name: String, value: String): String
   def assume(term: Term): Unit
   def declare(decl: Decl): Unit
   def comment(content: String): Unit

src/main/scala/rules/Brancher.scala

@@ -85,8 +85,10 @@ object brancher extends BranchingRules {
     val uidBranchPoint = v.symbExLog.insertBranchPoint(2, Some(condition), conditionExp)
     var functionsOfCurrentDecider: Set[FunctionDecl] = null
     var macrosOfCurrentDecider: Vector[MacroDecl] = null
+    var proverArgsOfCurrentDecider: viper.silicon.Map[String, String] = null
     var wasElseExecutedOnDifferentVerifier = false
     var functionsOfElseBranchDecider: Set[FunctionDecl] = null
+    var proverArgsOfElseBranchDecider: viper.silicon.Map[String, String] = null
     var macrosOfElseBranchDecider: Seq[MacroDecl] = null
     var pcsForElseBranch: PathConditionStack = null
     var noOfErrors = 0
@@ -104,6 +106,7 @@ object brancher extends BranchingRules {
         if (parallelizeElseBranch){
           functionsOfCurrentDecider = v.decider.freshFunctions
           macrosOfCurrentDecider = v.decider.freshMacros
+          proverArgsOfCurrentDecider = v.decider.getProverOptions()
           pcsForElseBranch = v.decider.pcs.duplicate()
           noOfErrors = v.errorsReportedSoFar.get()
         }
@@ -122,6 +125,9 @@ object brancher extends BranchingRules {
             val newMacros = macrosOfCurrentDecider.diff(v0.decider.freshMacros)
 
             v0.decider.prover.comment(s"[Shifting execution from ${v.uniqueId} to ${v0.uniqueId}]")
+            proverArgsOfElseBranchDecider = v0.decider.getProverOptions()
+            v0.decider.resetProverOptions()
+            v0.decider.setProverOptions(proverArgsOfCurrentDecider)
             v0.decider.prover.comment(s"Bulk-declaring functions")
             v0.decider.declareAndRecordAsFreshFunctions(newFunctions, false)
             v0.decider.prover.comment(s"Bulk-declaring macros")
@@ -141,10 +147,14 @@ object brancher extends BranchingRules {
               v1.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
 
             val result = fElse(v1.stateConsolidator.consolidateIfRetrying(s1, v1), v1)
-            if (wasElseExecutedOnDifferentVerifier && s.underJoin) {
-              val newSymbols = v1.decider.popSymbolStack()
-              functionsOfElseBranchDecider = newSymbols._1
-              macrosOfElseBranchDecider = newSymbols._2
+            if (wasElseExecutedOnDifferentVerifier) {
+              v1.decider.resetProverOptions()
+              v1.decider.setProverOptions(proverArgsOfElseBranchDecider)
+              if (s.underJoin) {
+                val newSymbols = v1.decider.popSymbolStack()
+                functionsOfElseBranchDecider = newSymbols._1
+                macrosOfElseBranchDecider = newSymbols._2
+              }
             }
             result
           })
@@ -206,6 +216,8 @@ object brancher extends BranchingRules {
             v.decider.setPcs(pcsAfterThenBranch)
             v.errorsReportedSoFar.set(noOfErrorsAfterThenBranch)
             v.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
+            v.decider.resetProverOptions()
+            v.decider.setProverOptions(proverArgsOfCurrentDecider)
           }
         }else{
           rs = elseBranchFuture.get()

src/main/scala/supporters/MethodSupporter.scala

@@ -18,6 +18,8 @@ import viper.silicon.state.{Heap, State, Store}
 import viper.silicon.state.State.OldHeaps
 import viper.silicon.verifier.{Verifier, VerifierComponent}
 import viper.silicon.utils.freshSnap
+import viper.silver.reporter.AnnotationWarning
+import viper.silicon.{Map, toMap}
 
 /* TODO: Consider changing the DefaultMethodVerificationUnitProvider into a SymbolicExecutionRule */
 
@@ -44,6 +46,24 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif
       logger.debug("\n\n" + "-" * 10 + " METHOD " + method.name + "-" * 10 + "\n")
       decider.prover.comment("%s %s %s".format("-" * 10, method.name, "-" * 10))
 
+      val proverOptions: Map[String, String] = method.info.getUniqueInfo[ast.AnnotationInfo] match {
+        case Some(ai) if ai.values.contains("proverArgs") =>
+          toMap(ai.values("proverArgs").flatMap(o => {
+            val index = o.indexOf("=")
+            if (index == -1) {
+              reporter report AnnotationWarning(s"Invalid proverArgs annotation ${o} on method ${method.name}. " +
+                s"Required format for each option is optionName=value.")
+              None
+            } else {
+              val (name, value) = (o.take(index), o.drop(index + 1))
+              Some((name, value))
+            }
+          }))
+        case _ =>
+          Map.empty
+      }
+      v.decider.setProverOptions(proverOptions)
+
       openSymbExLogger(method)
 
       val pres = method.pres
@@ -94,6 +114,8 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif
                     consumes(s4, posts, postViolated, v4)((_, _, _) =>
                       Success()))}) }  )})})
 
+      v.decider.resetProverOptions()
+
       symbExLog.closeMemberScope()
       Seq(result)
     }

src/main/scala/verifier/DefaultMainVerifier.scala

@@ -150,6 +150,11 @@ class DefaultMainVerifier(config: Config,
       decider.prover.emitSettings(contents)
       _verificationPoolManager.pooledVerifiers.emitSettings(contents)
     }
+
+    override def setOption(name: String, value: String): String = {
+      decider.prover.setOption(name, value)
+      _verificationPoolManager.pooledVerifiers.setOption(name, value)
+    }
   }
 
   /* Program verification */

src/main/scala/verifier/VerificationPoolManager.scala

@@ -37,6 +37,9 @@ class VerificationPoolManager(mainVerifier: MainVerifier) extends StatefulCompon
 
     override def emitSettings(contents: Iterable[String]): Unit =
       workerVerifiers foreach (_.decider.prover.emitSettings(contents))
+
+    override def setOption(name: String, value: String): String =
+      (workerVerifiers map (_.decider.prover.setOption(name, value))).head
   }
 
   /* Verifier pool management */