Parallel branch verification

build.sbt

@@ -30,6 +30,7 @@ lazy val silicon = (project in file("."))
     libraryDependencies += "com.typesafe.scala-logging" %% "scala-logging" % "3.9.2",
     libraryDependencies += "org.apache.commons" % "commons-pool2" % "2.9.0",
     libraryDependencies += "io.spray" %%  "spray-json" % "1.3.6",
+    libraryDependencies += "com.microsoft.z3" % "z3" % "4.8.7" from "https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/com.microsoft.z3-4.8.7.jar",
 
     // Only get a few compilation errors at once
     maxErrors := 5,

src/main/scala/Config.scala

@@ -12,7 +12,7 @@ import scala.util.matching.Regex
 import scala.util.Properties._
 import org.rogach.scallop._
 import viper.silicon.Config.StateConsolidationMode.StateConsolidationMode
-import viper.silicon.decider.{Z3ProverStdIO, Cvc5ProverStdIO}
+import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverAPI, Z3ProverStdIO}
 import viper.silver.frontend.SilFrontendConfig
 
 class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
@@ -635,6 +635,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val parallelizeBranches= opt[Boolean]("parallelizeBranches",
+    descr = "Verify different branches in parallel.",
+    default = Some(false),
+    noshort = true
+  )
+
   val printTranslatedProgram: ScallopOption[Boolean] = opt[Boolean]("printTranslatedProgram",
     descr ="Print the final program that is going to be verified to stdout.",
     default = Some(false),
@@ -717,7 +723,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   )
 
   val prover: ScallopOption[String] = opt[String]("prover",
-    descr = s"One of the provers ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}. " +
+    descr = s"One of the provers ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}, ${Z3ProverAPI.name}. " +
             s"(default: ${Z3ProverStdIO.name}).",
     default = Some(Z3ProverStdIO.name),
     noshort = true
@@ -726,8 +732,8 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   /* Option validation (trailing file argument is validated by parent class) */
 
   validateOpt(prover) {
-    case Some(Z3ProverStdIO.name) | Some(Cvc5ProverStdIO.name) => Right(())
-    case prover => Left(s"Unknown prover '$prover' provided. Expected one of ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}.")
+    case Some(Z3ProverStdIO.name) | Some(Cvc5ProverStdIO.name) | Some(Z3ProverAPI.name) => Right(())
+    case prover => Left(s"Unknown prover '$prover' provided. Expected one of ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}, ${Z3ProverAPI.name}.")
   }
 
   validateOpt(timeout) {

src/main/scala/decider/CVC5ProverStdIO.scala

@@ -45,4 +45,6 @@ class Cvc5ProverStdIO(uniqueId: String,
   protected def getProverPath: Path = {
     Paths.get(Verifier.config.cvc5Exe)
   }
+
+  override def emitSettings(contents: Iterable[String]): Unit = emit(contents)
 }

src/main/scala/decider/Decider.scala

@@ -10,11 +10,11 @@ import scala.reflect.{ClassTag, classTag}
 import com.typesafe.scalalogging.Logger
 import viper.silver.ast
 import viper.silver.components.StatefulComponent
-import viper.silver.verifier.DependencyNotFoundError
+import viper.silver.verifier.{DependencyNotFoundError, Model}
 import viper.silicon._
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.interfaces._
-import viper.silicon.interfaces.decider.{Prover, Unsat}
+import viper.silicon.interfaces.decider._
 import viper.silicon.logger.SymbExLogger
 import viper.silicon.logger.records.data.{DeciderAssertRecord, DeciderAssumeRecord, ProverAssertRecord}
 import viper.silicon.state._
@@ -60,15 +60,17 @@ trait Decider {
   def appliedFresh(id: String, sort: Sort, appliedArgs: Seq[Term]): App
 
   def generateModel(): Unit
-  def getModel(): String
+  def getModel(): Model
   def clearModel(): Unit
+  def hasModel(): Boolean
+  def isModelValid(): Boolean
 
 /* [BRANCH-PARALLELISATION] */
-//  def freshFunctions: InsertionOrderedSet[FunctionDecl]
-//  def freshMacros: Vector[MacroDecl]
-//  def declareAndRecordAsFreshFunctions(functions: InsertionOrderedSet[FunctionDecl]): Unit
-//  def declareAndRecordAsFreshMacros(functions: Vector[MacroDecl]): Unit
-//  def setPcs(other: PathConditionStack): Unit
+  def freshFunctions: InsertionOrderedSet[FunctionDecl]
+  def freshMacros: Vector[MacroDecl]
+  def declareAndRecordAsFreshFunctions(functions: InsertionOrderedSet[FunctionDecl]): Unit
+  def declareAndRecordAsFreshMacros(functions: Vector[MacroDecl]): Unit
+  def setPcs(other: PathConditionStack): Unit
 
   def statistics(): Map[String, String]
 }
@@ -87,23 +89,33 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
   def identifierFactory: IdentifierFactory
 
   object decider extends Decider with StatefulComponent {
-    private var proverStdIO: ProverStdIO = _
+    private var proverStdIO: Prover = _
     private var pathConditions: PathConditionStack = _
 
-//    private var _freshFunctions: InsertionOrderedSet[FunctionDecl] = _ /* [BRANCH-PARALLELISATION] */
-//    private var _freshMacros: Vector[MacroDecl] = _
+    private var _freshFunctions: InsertionOrderedSet[FunctionDecl] = _ /* [BRANCH-PARALLELISATION] */
+    private var _freshMacros: Vector[MacroDecl] = _
 
-    def prover: ProverStdIO = proverStdIO
+    def prover: Prover = proverStdIO
 
     def pcs: PathConditionStack = pathConditions
 
-//    def setPcs(other: PathConditionStack) = { /* [BRANCH-PARALLELISATION] */
-//      pathConditions = other
-//      pathConditions.assumptions foreach prover.assume
-//    }
-    private def getProverStdIO(prover: String): ProverStdIO = prover match {
+    def setPcs(other: PathConditionStack) = {
+      /* [BRANCH-PARALLELISATION] */
+      pathConditions = other
+      while (prover.pushPopScopeDepth > 1){
+        prover.pop()
+      }
+      val layeredStack = other.asInstanceOf[LayeredPathConditionStack]
+      layeredStack.layers.reverse.foreach(l => {
+        l.assumptions foreach prover.assume
+        prover.push()
+      })
+    }
+
+    private def getProverStdIO(prover: String): Prover = prover match {
       case Z3ProverStdIO.name => new Z3ProverStdIO(uniqueId, termConverter, identifierFactory, reporter)
       case Cvc5ProverStdIO.name => new Cvc5ProverStdIO(uniqueId, termConverter, identifierFactory, reporter)
+      case Z3ProverAPI.name => new Z3ProverAPI(uniqueId, new TermToZ3APIConverter(), identifierFactory, reporter)
       case prover =>
         val msg1 = s"Unknown prover '$prover' provided. Defaulting to ${Z3ProverStdIO.name}."
         logger warn msg1
@@ -118,7 +130,11 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
       val proverStdIOVersion = proverStdIO.version()
       // One can pass some options. This allows to check whether they have been received.
 
-      val msg = s"Using ${proverStdIO.name} $proverStdIOVersion located at ${proverStdIO.proverPath}"
+      val path = prover match {
+        case pio: ProverStdIO => pio.proverPath
+        case _ => "No Path"
+      }
+      val msg = s"Using ${proverStdIO.name} $proverStdIOVersion located at ${path}"
       reporter report ConfigurationConfirmation(msg)
       logger debug msg
 
@@ -141,16 +157,16 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def start(): Unit = {
       pathConditions = new LayeredPathConditionStack()
-//      _freshFunctions = InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
-//      _freshMacros = Vector.empty
+      _freshFunctions = InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
+      _freshMacros = Vector.empty
       createProver()
     }
 
     def reset(): Unit = {
       proverStdIO.reset()
       pathConditions = new LayeredPathConditionStack()
-//      _freshFunctions = InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
-//      _freshMacros = Vector.empty
+      _freshFunctions = InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
+      _freshMacros = Vector.empty
     }
 
     def stop(): Unit = {
@@ -298,7 +314,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
       prover.declare(macroDecl)
 
-//      _freshMacros = _freshMacros :+ macroDecl /* [BRANCH-PARALLELISATION] */
+      _freshMacros = _freshMacros :+ macroDecl /* [BRANCH-PARALLELISATION] */
 
       macroDecl
     }
@@ -334,35 +350,39 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
               HeapDepFun(proverFun.id, proverFun.argSorts, proverFun.resultSort).asInstanceOf[F]
           }
 
-//      _freshFunctions = _freshFunctions + FunctionDecl(fun) /* [BRANCH-PARALLELISATION] */
+      _freshFunctions = _freshFunctions + FunctionDecl(fun) /* [BRANCH-PARALLELISATION] */
 
       fun
     }
 
 
 /* [BRANCH-PARALLELISATION] */
-//    def freshFunctions: InsertionOrderedSet[FunctionDecl] = _freshFunctions
-//    def freshMacros: Vector[MacroDecl] = _freshMacros
-//
-//    def declareAndRecordAsFreshFunctions(functions: InsertionOrderedSet[FunctionDecl]): Unit = {
-//      functions foreach prover.declare
-//
-//      _freshFunctions = _freshFunctions ++ functions
-//    }
-//
-//    def declareAndRecordAsFreshMacros(macros: Vector[MacroDecl]): Unit = {
-//      macros foreach prover.declare
-//
-//      _freshMacros = _freshMacros ++ macros
-//    }
+    def freshFunctions: InsertionOrderedSet[FunctionDecl] = _freshFunctions
+    def freshMacros: Vector[MacroDecl] = _freshMacros
+
+    def declareAndRecordAsFreshFunctions(functions: InsertionOrderedSet[FunctionDecl]): Unit = {
+      functions foreach prover.declare
+
+      _freshFunctions = _freshFunctions ++ functions
+    }
+
+    def declareAndRecordAsFreshMacros(macros: Vector[MacroDecl]): Unit = {
+      macros foreach prover.declare
+
+      _freshMacros = _freshMacros ++ macros
+    }
 
     /* Misc */
 
     def statistics(): Map[String, String] = prover.statistics()
 
     override def generateModel(): Unit = proverAssert(False(), None)
 
-    override def getModel(): String = prover.getLastModel()
+    override def getModel(): Model = prover.getModel()
+
+    override def hasModel(): Boolean = prover.hasModel()
+
+    override def isModelValid(): Boolean = prover.isModelValid()
 
     override def clearModel(): Unit = prover.clearLastModel()
   }

src/main/scala/decider/PathConditions.scala

@@ -221,7 +221,7 @@ private[decider] class LayeredPathConditionStack
        with PathConditionStack
        with Cloneable {
 
-  private var layers: Stack[PathConditionStackLayer] = Stack.empty
+  var layers: Stack[PathConditionStackLayer] = Stack.empty
   private var markToLength: Map[Mark, Int] = Map.empty
   private var scopeMarks: List[Mark] = List.empty
   private var markCounter = new Counter(0)

src/main/scala/decider/ProverStdIO.scala

@@ -20,6 +20,7 @@ import viper.silicon.verifier.Verifier
 import viper.silver.verifier.{DefaultDependency => SilDefaultDependency}
 import viper.silicon.{Config, Map, toMap}
 import viper.silver.reporter.{ConfigurationConfirmation, InternalWarningMessage, Reporter}
+import viper.silver.verifier.Model
 
 import scala.collection.mutable
 
@@ -30,7 +31,7 @@ abstract class ProverStdIO(uniqueId: String,
     extends Prover
        with LazyLogging {
 
-  protected var pushPopScopeDepth = 0
+  var pushPopScopeDepth = 0
   protected var lastTimeout: Int = -1
   protected var logfileWriter: PrintWriter = _
   protected var prover: Process = _
@@ -41,14 +42,9 @@ abstract class ProverStdIO(uniqueId: String,
   var proverPath: Path = _
   var lastModel : String = _
 
-  def name: String
-  def minVersion: Version
-  def maxVersion: Option[Version]
   def exeEnvironmentalVariable: String
   def dependencies: Seq[SilDefaultDependency]
-  def staticPreamble: String
   def startUpArgs: Seq[String]
-  def randomizeSeedsOptions: Seq[String]
 
   protected def setTimeout(timeout: Option[Int]): Unit
   protected def getProverPath: Path
@@ -289,6 +285,14 @@ abstract class ProverStdIO(uniqueId: String,
     }
   }
 
+  override def hasModel(): Boolean = {
+    lastModel != null
+  }
+
+  override def isModelValid(): Boolean = {
+    lastModel != null && !lastModel.contains("model is not available")
+  }
+
   protected def assertUsingSoftConstraints(goal: String): (Boolean, Long) = {
     val guard = fresh("grd", Nil, sorts.Bool)
 
@@ -457,7 +461,7 @@ abstract class ProverStdIO(uniqueId: String,
     output.println(out)
   }
 
-  override def getLastModel(): String = lastModel
+  override def getModel(): Model = Model(lastModel)
 
   override def clearLastModel(): Unit = lastModel = null
 }

src/main/scala/decider/SMTLib2PreambleReader.scala

@@ -54,15 +54,18 @@ class SMTLib2PreambleReader extends PreambleReader[String, String] {
         lineAcc.replace(orig, repl)})
   }
 
-  def emitPreamble(preamble: Iterable[String], sink: ProverLike): Unit = {
-    sink.emit(preamble)
+  def emitPreamble(preamble: Iterable[String], sink: ProverLike, isOptions: Boolean): Unit = {
+    if (isOptions)
+      sink.emitSettings(preamble)
+    else
+      sink.emit(preamble)
   }
 
   def emitParametricPreamble(resource: String,
                              substitutions: Map[String, String],
                              sink: ProverLike)
                             : Unit = {
 
-    emitPreamble(readParametricPreamble(resource, substitutions), sink)
+    emitPreamble(readParametricPreamble(resource, substitutions), sink, false)
   }
 }

src/main/scala/decider/TermToSMTLib2Converter.scala

@@ -380,7 +380,7 @@ class TermToSMTLib2Converter
     else
       render(t)
 
-  protected def render(id: Identifier, sanitizeIdentifier: Boolean = true): String = {
+  def render(id: Identifier, sanitizeIdentifier: Boolean = true): String = {
     val repr: String = id match {
       case SimpleIdentifier(name) => name
       case SuffixedIdentifier(prefix, separator, suffix) => s"${render(prefix, false)}$separator$suffix"