diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index c05e0d738..141efe9a4 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -816,12 +816,6 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { 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) diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 29e284443..145fcceb0 100644 --- a/src/main/scala/decider/Decider.scala +++ b/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() diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index febf77bea..d5b9dfe77 100644 --- a/src/main/scala/decider/Z3ProverAPI.scala +++ b/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) + } + } } } @@ -342,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]) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 45d4fe43c..610cc514e 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -291,9 +291,9 @@ object evaluator extends EvaluationRules { case ast.Let(x, e0, e1) => eval(s, e0, pve, v)((s1, t0, v1) => { - val t = v1.decider.fresh(v1.symbolConverter.toSort(x.typ)) + val t = v1.decider.appliedFresh("letvar", v1.symbolConverter.toSort(x.typ), s1.relevantQuantifiedVariables) v1.decider.assume(t === t0) - val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t) + val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t.applicable.asInstanceOf[Function]) eval(s1.copy(g = s1.g + (x.localVar, t0), functionRecorder = newFuncRec), e1, pve, v1)(Q) }) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 857bacb02..c1a03b2d4 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1362,9 +1362,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { // ME: When using Z3 via API, it is beneficial to not use macros, since macro-terms will *always* be different // (leading to new terms that have to be translated), whereas without macros, we can usually use a term // that already exists. + // ME: Update: Actually, it seems better to use macros even with the API since Silicon terms can grow so large + // that e.g. the instantiate call in createPermissionConstraintAndDepletedCheck takes forever, before even + // converting to a Z3 term. // During function verification, we should not define macros, since they could contain resullt, which is not // defined elsewhere. - val declareMacro = s.functionRecorder == NoopFunctionRecorder && !Verifier.config.useFlyweight + val declareMacro = s.functionRecorder == NoopFunctionRecorder // && !Verifier.config.useFlyweight val permsProvided = ch.perm val permsTaken = if (declareMacro) { diff --git a/src/main/scala/supporters/Domains.scala b/src/main/scala/supporters/Domains.scala index 131ebb696..192cb10f6 100644 --- a/src/main/scala/supporters/Domains.scala +++ b/src/main/scala/supporters/Domains.scala @@ -12,9 +12,9 @@ import viper.silicon.common.collections.immutable.MultiMap._ import viper.silicon.toMap import viper.silicon.interfaces.PreambleContributor import viper.silicon.interfaces.decider.ProverLike -import viper.silicon.state.{SymbolConverter, terms} +import viper.silicon.state.{FunctionPreconditionTransformer, SymbolConverter, terms} import viper.silicon.state.terms.{Distinct, DomainFun, Sort, Term} -import viper.silver.ast.{NamedDomainAxiom} +import viper.silver.ast.NamedDomainAxiom trait DomainsContributor[SO, SY, AX, UA] extends PreambleContributor[SO, SY, AX] { def uniquenessAssumptionsAfterAnalysis: Iterable[UA] @@ -100,7 +100,8 @@ class DefaultDomainsContributor(symbolConverter: SymbolConverter, domain.axioms foreach (axiom => { val tAx = domainTranslator.translateAxiom(axiom, symbolConverter.toSort) - collectedAxioms += tAx + val tAxPres = FunctionPreconditionTransformer.transform(tAx, program) + collectedAxioms += terms.And(tAxPres, tAx) }) }) } diff --git a/src/main/scala/supporters/ExpressionTranslator.scala b/src/main/scala/supporters/ExpressionTranslator.scala index b8356e0b7..22077d182 100644 --- a/src/main/scala/supporters/ExpressionTranslator.scala +++ b/src/main/scala/supporters/ExpressionTranslator.scala @@ -162,7 +162,7 @@ trait ExpressionTranslator { val df = Fun(id, inSorts, outSort) App(df, tArgs) - case bfa@ast.BackendFuncApp(func, args) => + case bfa@ast.BackendFuncApp(_, args) => val tArgs = args map f val inSorts = tArgs map (_.sort) val outSort = toSort(bfa.typ) @@ -170,6 +170,15 @@ trait ExpressionTranslator { val sf = SMTFun(id, inSorts, outSort) App(sf, tArgs) + case fa@ast.FuncApp(name, args) => + // We are assuming here that only functions with empty preconditions are used. + val tArgs = Unit +: (args map f) + val inSorts = tArgs map (_.sort) + val outSort = toSort(fa.typ) + val id = Identifier(name) + val df = HeapDepFun(id, inSorts, outSort) + App(df, tArgs) + /* Permissions */ case _: ast.FullPerm => FullPerm