From 6cef40687b04ef43049a3e990da3fe129eb97929 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 9 Nov 2023 16:40:06 +0100 Subject: [PATCH] Experimental proverArgs annotation for methods --- src/main/scala/decider/ProverStdIO.scala | 9 +++++++++ src/main/scala/decider/Z3ProverAPI.scala | 6 +++++- .../scala/interfaces/decider/Prover.scala | 1 + .../scala/supporters/MethodSupporter.scala | 20 +++++++++++++++++++ .../scala/verifier/DefaultMainVerifier.scala | 5 +++++ .../verifier/VerificationPoolManager.scala | 3 +++ 6 files changed, 43 insertions(+), 1 deletion(-) diff --git a/src/main/scala/decider/ProverStdIO.scala b/src/main/scala/decider/ProverStdIO.scala index 4bc4507a4..585bf2235 100644 --- a/src/main/scala/decider/ProverStdIO.scala +++ b/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 = { diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index c0cdbe12f..01f060220 100644 --- a/src/main/scala/decider/Z3ProverAPI.scala +++ b/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 @@ -236,6 +236,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) diff --git a/src/main/scala/interfaces/decider/Prover.scala b/src/main/scala/interfaces/decider/Prover.scala index 6aab1b422..0cfa19a70 100644 --- a/src/main/scala/interfaces/decider/Prover.scala +++ b/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 diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index a99cbb17e..a029b0f65 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -18,6 +18,7 @@ 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 /* TODO: Consider changing the DefaultMethodVerificationUnitProvider into a SymbolicExecutionRule */ @@ -44,6 +45,23 @@ 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 toReset = method.info.getUniqueInfo[ast.AnnotationInfo] match { + case Some(ai) if ai.values.contains("proverArgs") => + ai.values("proverArgs").flatMap(o => { + val index = o.indexOf("=") + if (index == -1) { + reporter report AnnotationWarning(s"Invalid proverArgs annotation ${o} on method ${method.name}. Required format for each option is optionName=value.") + None + } else { + val (name, value) = (o.take(index), o.drop(index + 1)) + val oldVal = v.decider.prover.setOption(name, value) + Some((name, oldVal)) + } + }) + case _ => + Seq() + } + openSymbExLogger(method) val pres = method.pres @@ -94,6 +112,8 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif consumes(s4, posts, postViolated, v4)((_, _, _) => Success()))}) } )})}) + toReset.foreach(o => v.decider.prover.setOption(o._1, o._2)) + symbExLog.closeMemberScope() Seq(result) } diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index c2d41d192..0db992bea 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/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 */ diff --git a/src/main/scala/verifier/VerificationPoolManager.scala b/src/main/scala/verifier/VerificationPoolManager.scala index 142442891..50c90b109 100644 --- a/src/main/scala/verifier/VerificationPoolManager.scala +++ b/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 */