Skip to content

Commit

Permalink
Pure SC mode without push/pop, hacky Solver cloning
Browse files Browse the repository at this point in the history
  • Loading branch information
@marcoeilers
marcoeilers committed Jun 27, 2023
1 parent 2952f94 commit 22bf25a
Show file tree
Hide file tree
Showing 4 changed files with 123 additions and 51 deletions.
4 changes: 2 additions & 2 deletions src/main/scala/Config.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -816,11 +816,11 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
case _ => Right(())
}

validateOpt(assertionMode, parallelizeBranches) {
/*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)
Expand Down
23 changes: 13 additions & 10 deletions src/main/scala/decider/Decider.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ trait Decider {
def freshMacros: Vector[MacroDecl]
def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl]): Unit
def declareAndRecordAsFreshMacros(functions: Vector[MacroDecl]): Unit
def setPcs(other: PathConditionStack): Unit
def setPcs(other: PathConditionStack, setInProver: Boolean): Unit

def statistics(): Map[String, String]
}
Expand Down Expand Up @@ -103,18 +103,21 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>

def pcs: PathConditionStack = pathConditions

def setPcs(other: PathConditionStack) = {
def setPcs(other: PathConditionStack, setInProver: Boolean) = {
/* [BRANCH-PARALLELISATION] */
pathConditions = other
while (prover.pushPopScopeDepth > 1){
prover.pop()

if (setInProver) {
while (prover.pushPopScopeDepth > 1) {
prover.pop()
}
// TODO: Change interface to make the cast unnecessary?
val layeredStack = other.asInstanceOf[LayeredPathConditionStack]
layeredStack.layers.reverse.foreach(l => {
l.assumptions foreach prover.assume
prover.push(timeout = Verifier.config.pushTimeout.toOption)
})
}
// TODO: Change interface to make the cast unnecessary?
val layeredStack = other.asInstanceOf[LayeredPathConditionStack]
layeredStack.layers.reverse.foreach(l => {
l.assumptions foreach prover.assume
prover.push(timeout = Verifier.config.pushTimeout.toOption)
})
}

private def getProver(prover: String): Prover = prover match {
Expand Down
94 changes: 69 additions & 25 deletions src/main/scala/decider/Z3ProverAPI.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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, 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.terms.{And, App, Decl, Fun, FunctionDecl, Implies, Ite, MacroDecl, Not, Quantification, Sort, SortDecl, SortWrapperDecl, Term, Trigger, TriggerGenerator, sorts}
import viper.silicon.{Config, Map}
import viper.silicon.verifier.Verifier
import viper.silver.reporter.{InternalWarningMessage, Reporter}
Expand Down Expand Up @@ -81,6 +81,7 @@ class Z3ProverAPI(uniqueId: String,
protected var lastTimeout: Int = -1
protected var prover: Solver = _
protected var ctx: Context = _
protected var usePushPop: Boolean = true

var proverPath: Path = _
var lastReasonUnknown : String = _
Expand All @@ -94,13 +95,27 @@ class Z3ProverAPI(uniqueId: String,
val emittedFuncs = mutable.LinkedHashSet[FuncDecl]()
val emittedFuncSymbols = mutable.Queue[Symbol]()

var guardStack = List[App]()
var curGuards: Array[Expr] = _

// If true, we do not define macros on the Z3 level, but perform macro expansion ourselves on Silicon Terms.
// Otherwise, we define a function on the Z3 level and axiomatize it according to the macro definition.
// In terms of performance, I could not measure any substantial difference.
val expandMacros = true



def getSolver(c: Context) = (prover.translate(ctx), guardStack)

def setSolver(arg: (Solver, List[App])) = {
val (s, _guardStack) = arg
prover = s.translate(ctx)
guardStack = _guardStack
curGuards = _guardStack.map(termConverter.convert(_)).toArray
}



def version(): Version = {
var versString = com.microsoft.z3.Version.getFullVersion
if (versString.startsWith("Z3 "))
Expand All @@ -109,6 +124,8 @@ class Z3ProverAPI(uniqueId: String,
}

def start(): Unit = {
usePushPop = Verifier.config.assertionMode() == Config.AssertionMode.PushPop
curGuards = new Array[Expr](0)
pushPopScopeDepth = 0
lastTimeout = -1
ctx = new Context(Z3ProverAPI.initialOptions.asJava)
Expand Down Expand Up @@ -190,6 +207,8 @@ class Z3ProverAPI(uniqueId: String,
emittedSorts.clear()
emittedFuncSymbols.clear()
emittedSortSymbols.clear()
guardStack = Nil
curGuards = new Array[Expr](0)
prover = null
lastModel = null
if (ctx != null){
Expand All @@ -202,18 +221,30 @@ class Z3ProverAPI(uniqueId: String,
endPreamblePhase()
setTimeout(timeout)
pushPopScopeDepth += n
if (n == 1) {
// the normal case; we handle this without invoking a bunch of higher order functions
prover.push()
if (usePushPop) {
if (n == 1) {
// the normal case; we handle this without invoking a bunch of higher order functions
prover.push()
} else {
// this might never actually happen
(0 until n).foreach(_ => prover.push())
}
} else {
// this might never actually happen
(0 until n).foreach(_ => prover.push())
val guard = fresh("lvl", Nil, sorts.Bool)
val guardApp = App(guard, Nil)
guardStack = guardApp :: guardStack
curGuards = termConverter.convert(guardApp) +: curGuards
}
}

def pop(n: Int = 1): Unit = {
endPreamblePhase()
prover.pop(n)
if (usePushPop) {
prover.pop(n)
} else {
guardStack = guardStack.tail
curGuards = curGuards.tail
}
pushPopScopeDepth -= n
}

Expand Down Expand Up @@ -244,7 +275,8 @@ class Z3ProverAPI(uniqueId: String,
}
}

def assume(term: Term): Unit = {
def assume(trm: Term): Unit = {
val term = if (usePushPop || guardStack.isEmpty) trm else Implies(guardStack.head, trm)
try {
if (preamblePhaseOver)
prover.add(termConverter.convert(term).asInstanceOf[BoolExpr])
Expand All @@ -256,30 +288,42 @@ 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()

try {
val (result, _) = Verifier.config.assertionMode() match {
case Config.AssertionMode.SoftConstraints => assertUsingSoftConstraints(goal, timeout)
case Config.AssertionMode.PushPop => assertUsingPushPop(goal, timeout)
val (result, _) = usePushPop match {
case false => assertUsingSoftConstraints(goal, timeout)
case true => assertUsingPushPop(goal, timeout)
}
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)
}
}
}
}

Expand Down Expand Up @@ -340,14 +384,14 @@ class Z3ProverAPI(uniqueId: String,
endPreamblePhase()
setTimeout(timeout)

val guard = fresh("grd", Nil, sorts.Bool)
val guardApp = App(guard, Nil)
val goalImplication = Implies(guardApp, goal)
//val guard = fresh("grd", Nil, sorts.Bool)
//val guardApp = App(guard, Nil)
//val goalImplication = Implies(guardApp, goal)

prover.add(termConverter.convertTerm(goalImplication).asInstanceOf[BoolExpr])
//prover.add(termConverter.convertTerm(goalImplication).asInstanceOf[BoolExpr])

val startTime = System.currentTimeMillis()
val res = prover.check(termConverter.convertTerm(guardApp))
val res = prover.check(termConverter.convertTerm(Not(goal)) +: curGuards : _*)
val endTime = System.currentTimeMillis()
val result = res == Status.UNSATISFIABLE
if (!result) {
Expand Down
53 changes: 39 additions & 14 deletions src/main/scala/rules/Brancher.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,18 +6,22 @@

package viper.silicon.rules

import com.microsoft.z3.{Context, Solver}

import java.util.concurrent._
import viper.silicon.common.concurrency._
import viper.silicon.decider.PathConditionStack
import viper.silicon.decider.{PathConditionStack, Z3ProverAPI}
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.reporter.BranchFailureMessage
import viper.silver.verifier.Failure

import scala.jdk.CollectionConverters.MapHasAsJava

trait BranchingRules extends SymbolicExecutionRules {
def branch(s: State,
condition: Term,
Expand Down Expand Up @@ -85,8 +89,14 @@ object brancher extends BranchingRules {
val uidBranchPoint = v.symbExLog.insertBranchPoint(2, Some(condition), conditionExp)
var functionsOfCurrentDecider: Set[FunctionDecl] = null
var macrosOfCurrentDecider: Vector[MacroDecl] = null

var pcsForElseBranch: PathConditionStack = null

var proverOfCurrentDecider: (Solver, List[viper.silicon.state.terms.App]) = null
var tempContext: Context = null

val cloneSolver = parallelizeElseBranch && v.decider.prover.isInstanceOf[Z3ProverAPI]

val elseBranchVerificationTask: Verifier => VerificationResult =
if (executeElseBranch) {
/* [BRANCH-PARALLELISATION] */
Expand All @@ -98,9 +108,14 @@ object brancher extends BranchingRules {
* "offloading" verifier are captured.
*/
if (parallelizeElseBranch){
functionsOfCurrentDecider = v.decider.freshFunctions
macrosOfCurrentDecider = v.decider.freshMacros
pcsForElseBranch = v.decider.pcs.duplicate()
if (cloneSolver) {
tempContext = new Context(Z3ProverAPI.initialOptions.asJava)
proverOfCurrentDecider = v.decider.prover.asInstanceOf[Z3ProverAPI].getSolver(tempContext)
} else {
functionsOfCurrentDecider = v.decider.freshFunctions
macrosOfCurrentDecider = v.decider.freshMacros
}
}

(v0: Verifier) => {
Expand All @@ -110,17 +125,22 @@ object brancher extends BranchingRules {
/* [BRANCH-PARALLELISATION] */
// executing the else branch on a different verifier, need to adapt the state

val newFunctions = functionsOfCurrentDecider -- v0.decider.freshFunctions
val newMacros = macrosOfCurrentDecider.diff(v0.decider.freshMacros)
if (cloneSolver) {
v0.decider.prover.asInstanceOf[Z3ProverAPI].setSolver(proverOfCurrentDecider)
} else {
val newFunctions = functionsOfCurrentDecider -- v0.decider.freshFunctions
val newMacros = macrosOfCurrentDecider.diff(v0.decider.freshMacros)

v0.decider.prover.comment(s"[Shifting execution from ${v.uniqueId} to ${v0.uniqueId}]")
v0.decider.prover.comment(s"Bulk-declaring functions")
v0.decider.declareAndRecordAsFreshFunctions(newFunctions)
v0.decider.prover.comment(s"Bulk-declaring macros")
v0.decider.declareAndRecordAsFreshMacros(newMacros)

v0.decider.prover.comment(s"[Shifting execution from ${v.uniqueId} to ${v0.uniqueId}]")
v0.decider.prover.comment(s"Bulk-declaring functions")
v0.decider.declareAndRecordAsFreshFunctions(newFunctions)
v0.decider.prover.comment(s"Bulk-declaring macros")
v0.decider.declareAndRecordAsFreshMacros(newMacros)
v0.decider.prover.comment(s"Taking path conditions from source verifier ${v.uniqueId}")
}

v0.decider.prover.comment(s"Taking path conditions from source verifier ${v.uniqueId}")
v0.decider.setPcs(pcsForElseBranch)
v0.decider.setPcs(pcsForElseBranch, !cloneSolver)
}
elseBranchVerifier = v0.uniqueId

Expand Down Expand Up @@ -187,7 +207,12 @@ object brancher extends BranchingRules {
if (v.decider.pcs != pcsBefore && v.uniqueId != elseBranchVerifier){
// we have done other work during the join, need to reset
v.decider.prover.comment(s"Resetting path conditions after interruption")
v.decider.setPcs(pcsAfterThenBranch)

if (cloneSolver) {
v.decider.prover.asInstanceOf[Z3ProverAPI].setSolver(proverOfCurrentDecider)
}

v.decider.setPcs(pcsAfterThenBranch, !cloneSolver)
v.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
}
}else{
Expand Down

0 comments on commit 22bf25a

Please sign in to comment.