Merge

Author: marcoeilers

silver

@@ -11,24 +11,22 @@
 ; The axiom therefore needs to be emitted after the sort wrappers have
 ; been emitted.
 
-(assert (forall ((vs $FVF<$T$>) (ws $FVF<$T$>)) (!
+(assert (forall ((vs $FVF<$FLD$>) (ws $FVF<$FLD$>)) (!
     (=>
       (and
         (Set_equal ($FVF.domain_$FLD$ vs) ($FVF.domain_$FLD$ ws))
         (forall ((x $Ref)) (!
           (=>
             (Set_in x ($FVF.domain_$FLD$ vs))
             (= ($FVF.lookup_$FLD$ vs x) ($FVF.lookup_$FLD$ ws x)))
-          ; :pattern ((Set_in x ($FVF.domain_$FLD$ vs)))
           :pattern (($FVF.lookup_$FLD$ vs x) ($FVF.lookup_$FLD$ ws x))
-          :qid |qp.$FVF<$T$>-eq-inner|
+          :qid |qp.$FVF<$FLD$>-eq-inner|
           )))
       (= vs ws))
-    :pattern (($SortWrappers.$FVF<$T$>To$Snap vs)
-              ($SortWrappers.$FVF<$T$>To$Snap ws)
-;              ($FVF.after_$FLD$ vs ws)
+    :pattern (($SortWrappers.$FVF<$FLD$>To$Snap vs)
+              ($SortWrappers.$FVF<$FLD$>To$Snap ws)
               )
-    :qid |qp.$FVF<$T$>-eq-outer|
+    :qid |qp.$FVF<$FLD$>-eq-outer|
     )))
 
 (assert (forall ((r $Ref) (pm $FPM)) (!

src/main/resources/field_value_functions_axioms.smt2

@@ -7,9 +7,9 @@
 ;   - $S$ is the sort corresponding to the type of the field
 ;   - $T$ is the sanitized name of the sort corresponding to the type of the field
 
-(declare-fun $FVF.domain_$FLD$ ($FVF<$T$>) Set<$Ref>)
-(declare-fun $FVF.lookup_$FLD$ ($FVF<$T$> $Ref) $S$)
-(declare-fun $FVF.after_$FLD$ ($FVF<$T$> $FVF<$T$>) Bool)
+(declare-fun $FVF.domain_$FLD$ ($FVF<$FLD$>) Set<$Ref>)
+(declare-fun $FVF.lookup_$FLD$ ($FVF<$FLD$> $Ref) $S$)
+(declare-fun $FVF.after_$FLD$ ($FVF<$FLD$> $FVF<$FLD$>) Bool)
 (declare-fun $FVF.loc_$FLD$ ($S$ $Ref) Bool)
 (declare-fun $FVF.perm_$FLD$ ($FPM $Ref) $Perm)
-(declare-const $fvfTOP_$FLD$ $FVF<$T$>)
+(declare-const $fvfTOP_$FLD$ $FVF<$FLD$>)

src/main/resources/field_value_functions_declarations.smt2

@@ -10,7 +10,7 @@
 ; The axiom therefore needs to be emitted after the sort wrappers have
 ; been emitted.
 
-(assert (forall ((vs $PSF<$S$>) (ws $PSF<$S$>)) (!
+(assert (forall ((vs $PSF<$PRD$>) (ws $PSF<$PRD$>)) (!
     (=>
       (and
         (Set_equal ($PSF.domain_$PRD$ vs) ($PSF.domain_$PRD$ ws))
@@ -20,14 +20,14 @@
             (= ($PSF.lookup_$PRD$ vs x) ($PSF.lookup_$PRD$ ws x)))
           ; :pattern ((Set_in x ($PSF.domain_$PRD$ vs)))
           :pattern (($PSF.lookup_$PRD$ vs x) ($PSF.lookup_$PRD$ ws x))
-          :qid |qp.$PSF<$S$>-eq-inner|
+          :qid |qp.$PSF<$PRD$>-eq-inner|
           )))
       (= vs ws))
-    :pattern (($SortWrappers.$PSF<$S$>To$Snap vs)
-              ($SortWrappers.$PSF<$S$>To$Snap ws)
+    :pattern (($SortWrappers.$PSF<$PRD$>To$Snap vs)
+              ($SortWrappers.$PSF<$PRD$>To$Snap ws)
 ;              ($PSF.after_$PRD$ vs ws)
               )
-    :qid |qp.$PSF<$S$>-eq-outer|
+    :qid |qp.$PSF<$PRD$>-eq-outer|
     )))
 
 (assert (forall ((s $Snap) (pm $PPM)) (!

src/main/resources/predicate_snap_functions_axioms.smt2

@@ -6,9 +6,9 @@
 ;   - $PRD$ is a Silver predicate name
 ;   - $S$ is the sort corresponding to the type of the predicate arguments
 
-(declare-fun $PSF.domain_$PRD$ ($PSF<$S$>) Set<$Snap>)
-(declare-fun $PSF.lookup_$PRD$ ($PSF<$S$> $Snap) $S$)
-(declare-fun $PSF.after_$PRD$ ($PSF<$S$> $PSF<$S$>) Bool)
+(declare-fun $PSF.domain_$PRD$ ($PSF<$PRD$>) Set<$Snap>)
+(declare-fun $PSF.lookup_$PRD$ ($PSF<$PRD$> $Snap) $S$)
+(declare-fun $PSF.after_$PRD$ ($PSF<$PRD$> $PSF<$PRD$>) Bool)
 (declare-fun $PSF.loc_$PRD$ ($S$ $Snap) Bool)
 (declare-fun $PSF.perm_$PRD$ ($PPM $Snap) $Perm)
-(declare-const $psfTOP_$PRD$ $PSF<$S$>)
+(declare-const $psfTOP_$PRD$ $PSF<$PRD$>)

src/main/resources/predicate_snap_functions_declarations.smt2

@@ -565,7 +565,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   val assertionMode: ScallopOption[AssertionMode] = opt[AssertionMode]("assertionMode",
     descr = (  "Determines how assertion checks are encoded in SMTLIB. Options are "
-             + "'pp' (push-pop) and 'cs' (soft constraints) (default: cs)."),
+             + "'pp' (push-pop) and 'sc' (soft constraints) (default: pp)."),
     default = Some(AssertionMode.PushPop),
     noshort = true
   )(assertionModeConverter)
@@ -643,7 +643,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   val numberOfParallelVerifiers: ScallopOption[Int] = opt[Int]("numberOfParallelVerifiers",
     descr = (  "Number of verifiers run in parallel. This number plus one is the number of provers "
-             + s"run in parallel (default: ${Runtime.getRuntime.availableProcessors()}"),
+             + s"run in parallel (default: ${Runtime.getRuntime.availableProcessors()})"),
     default = Some(Runtime.getRuntime.availableProcessors()),
     noshort = true
   )
@@ -754,19 +754,21 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     case _ => Right(())
   }
 
-  validateOpt(ideModeAdvanced, numberOfParallelVerifiers) {
-    case (Some(false), _) =>
-      Right(())
-    case (Some(true), Some(n)) =>
-      if (n == 1)
-        Right(())
-      else
-        Left(  s"Option ${ideModeAdvanced.name} requires setting "
-             + s"${numberOfParallelVerifiers.name} to 1")
+  validateOpt(ideModeAdvanced, parallelizeBranches) {
+    case (Some(false), _) => Right(())
+    case (_, Some(false)) => Right(())
+    case (Some(true), Some(true)) =>
+      Left(s"Option ${ideModeAdvanced.name} is not supported in combination with ${parallelizeBranches.name}")
     case other =>
       sys.error(s"Unexpected combination: $other")
   }
-  
+
+  validateOpt(assertionMode, parallelizeBranches) {
+    case (Some(AssertionMode.SoftConstraints), Some(true)) =>
+      Left(s"Assertion mode SoftConstraints is not supported in combination with ${parallelizeBranches.name}")
+    case _ => Right()
+  }
+
   validateOpt(counterexample, enableMoreCompleteExhale) {
     case (Some(_), Some(false)) => Left(  s"Option ${counterexample.name} requires setting "
                                         + s"flag ${enableMoreCompleteExhale.name}")

src/main/scala/Config.scala

@@ -8,7 +8,6 @@ package viper.silicon
 
 import java.text.SimpleDateFormat
 import java.util.concurrent.{Callable, Executors, TimeUnit, TimeoutException}
-
 import scala.collection.immutable.ArraySeq
 import scala.util.{Left, Right}
 import ch.qos.logback.classic.{Level, Logger}
@@ -19,7 +18,7 @@ import viper.silver.frontend.{DefaultStates, SilFrontend}
 import viper.silver.reporter._
 import viper.silver.verifier.{AbstractVerificationError => SilAbstractVerificationError, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier}
 import viper.silicon.interfaces.Failure
-import viper.silicon.logger.SymbExLogger
+import viper.silicon.logger.{MemberSymbExLogger, SymbExLogger}
 import viper.silicon.reporting.{MultiRunRecorders, condenseToViperResult}
 import viper.silicon.verifier.DefaultMainVerifier
 import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverStdIO}
@@ -93,6 +92,10 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
   private var _config: Config = _
   final def config = _config
 
+  private var _symbExLog: SymbExLogger[_ <: MemberSymbExLogger] = _
+  final def symbExLog = _symbExLog
+  final def symbExLog_=(log: SymbExLogger[_ <: MemberSymbExLogger]) = { _symbExLog = log }
+
   private sealed trait LifetimeState
 
   private object LifetimeState {
@@ -113,6 +116,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
     lifetimeState = LifetimeState.Configured
 
     _config = new Config(args)
+    _symbExLog = SymbExLogger.ofConfig(_config)
   }
 
   def debugInfo(debugInfo: Seq[(String, Any)]): Unit = { this.debugInfo = debugInfo }
@@ -129,7 +133,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
 
     setLogLevelsFromConfig()
 
-    verifier = new DefaultMainVerifier(config, reporter)
+    verifier = new DefaultMainVerifier(config, reporter, symbExLog)
     verifier.start()
   }
 
@@ -202,10 +206,9 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
         result = Some(condenseToViperResult(failures))
       } catch { /* Catch exceptions thrown during verification (errors are not caught) */
         case _: TimeoutException =>
-          // verification was interrupted, therefore close the current member's scope:
-          SymbExLogger.currentLog().closeMemberScope()
           if (config.ideModeAdvanced()) {
-            reporter report ExecutionTraceReport(SymbExLogger.memberList, List(), List())
+            symbExLog.close()
+            reporter report ExecutionTraceReport(symbExLog.logs.toSeq, List(), List())
           }
           result = Some(SilFailure(SilTimeoutOccurred(config.timeout(), "second(s)") :: Nil))
         case exception: Exception if !config.disableCatchingExceptions() =>
@@ -240,21 +243,23 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
 
     /*verifier.bookkeeper.*/elapsedMillis = System.currentTimeMillis() - /*verifier.bookkeeper.*/startTime
 
-    val failures =
-      results.flatMap(r => r :: r.previous.toList)
-        .collect{ case f: Failure => f } /* Ignore successes */
-        .pipe(allResults => {
-          /* If branchconditions are to be reported we collect the different failure contexts
-          *  of all failures that report the same error (but on different branches, with different CounterExample)
-          *  and put those into one failure */
-          if (config.enableBranchconditionReporting())
-            allResults.groupBy(failureFilterAndGroupingCriterion).map{case (_: String, fs:List[Failure]) =>
-              fs.head.message.failureContexts = fs.flatMap(_.message.failureContexts)
-              Failure(fs.head.message)
-            }.toList
-             else allResults.distinctBy(failureFilterAndGroupingCriterion)
-        })
-        .sortBy(failureSortingCriterion)
+    val failures = results
+      // note that we do not extract 'previous' verification errors from VerificationResult's `previous` field
+      // because this is expected to have already been done in `verifier.verify` (for each member).
+      .collect{ case f: Failure => f } /* Ignore successes */
+      .pipe(allResults => {
+        /* If branchconditions are to be reported we collect the different failure contexts
+         *  of all failures that report the same error (but on different branches, with different CounterExample)
+         *  and put those into one failure
+         */
+        if (config.enableBranchconditionReporting())
+          allResults.groupBy(failureFilterAndGroupingCriterion).map{case (_: String, fs:List[Failure]) =>
+            fs.head.message.failureContexts = fs.flatMap(_.message.failureContexts)
+            Failure(fs.head.message)
+          }.toList
+        else allResults.distinctBy(failureFilterAndGroupingCriterion)
+      })
+      .sortBy(failureSortingCriterion)
 
 //    if (config.showStatistics.isDefined) {
 //      val proverStats = verifier.decider.statistics()
@@ -335,6 +340,8 @@ class SiliconFrontend(override val reporter: Reporter,
 
   protected var siliconInstance: Silicon = _
 
+  override def backendTypeFormat: Option[String] = Some("SMTLIB")
+
   def createVerifier(fullCmd: String) = {
     siliconInstance = new Silicon(reporter, Seq("args" -> fullCmd))
 
@@ -344,7 +351,7 @@ class SiliconFrontend(override val reporter: Reporter,
   def configureVerifier(args: Seq[String]) = {
     siliconInstance.parseCommandLine(args)
 
-    if (siliconInstance.config.error.isEmpty) {
+    if (siliconInstance.config.error.isEmpty && !siliconInstance.config.exit) {
       /** Parsing the provided command-line options might fail, in which the resulting error
         * is recorded in `siliconInstance.config.error`
         * (see also [[viper.silver.frontend.SilFrontendConfig.onError]]).

src/main/scala/Silicon.scala

@@ -15,7 +15,6 @@ import viper.silicon._
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.interfaces._
 import viper.silicon.interfaces.decider._
-import viper.silicon.logger.SymbExLogger
 import viper.silicon.logger.records.data.{DeciderAssertRecord, DeciderAssumeRecord, ProverAssertRecord}
 import viper.silicon.state._
 import viper.silicon.state.terms._
@@ -183,18 +182,18 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def pushScope(): Unit = {
       //val commentRecord = new CommentRecord("push", null, null)
-      //val sepIdentifier = SymbExLogger.currentLog().openScope(commentRecord)
+      //val sepIdentifier = symbExLog.openScope(commentRecord)
       pathConditions.pushScope()
       _prover.push(timeout = Verifier.config.pushTimeout.toOption)
-      //SymbExLogger.currentLog().closeScope(sepIdentifier)
+      //symbExLog.closeScope(sepIdentifier)
     }
 
     def popScope(): Unit = {
       //val commentRecord = new CommentRecord("pop", null, null)
-      //val sepIdentifier = SymbExLogger.currentLog().openScope(commentRecord)
+      //val sepIdentifier = symbExLog.openScope(commentRecord)
       _prover.pop()
       pathConditions.popScope()
-      //SymbExLogger.currentLog().closeScope(sepIdentifier)
+      //symbExLog.closeScope(sepIdentifier)
     }
 
     def setCurrentBranchCondition(t: Term, te: Option[ast.Exp] = None): Unit = {
@@ -223,15 +222,15 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     private def assumeWithoutSmokeChecks(terms: InsertionOrderedSet[Term]) = {
       val assumeRecord = new DeciderAssumeRecord(terms)
-      val sepIdentifier = SymbExLogger.currentLog().openScope(assumeRecord)
+      val sepIdentifier = symbExLog.openScope(assumeRecord)
 
       /* Add terms to Silicon-managed path conditions */
       terms foreach pathConditions.add
 
       /* Add terms to the prover's assumptions */
       terms foreach prover.assume
 
-      SymbExLogger.currentLog().closeScope(sepIdentifier)
+      symbExLog.closeScope(sepIdentifier)
       None
     }
 
@@ -252,21 +251,21 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
       // previously (it did not cause a verification failure) and ignore the
       // current one, because it cannot cause a verification error.
       if (success)
-        SymbExLogger.currentLog().discardSMTQuery()
+        symbExLog.discardSMTQuery()
       else
-        SymbExLogger.currentLog().setSMTQuery(t)
+        symbExLog.setSMTQuery(t)
 
       Q(success)
     }
 
     private def deciderAssert(t: Term, timeout: Option[Int]) = {
       val assertRecord = new DeciderAssertRecord(t, timeout)
-      val sepIdentifier = SymbExLogger.currentLog().openScope(assertRecord)
+      val sepIdentifier = symbExLog.openScope(assertRecord)
 
       val asserted = isKnownToBeTrue(t)
       val result = asserted || proverAssert(t, timeout)
 
-      SymbExLogger.currentLog().closeScope(sepIdentifier)
+      symbExLog.closeScope(sepIdentifier)
       result
     }
 
@@ -280,17 +279,15 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     private def proverAssert(t: Term, timeout: Option[Int]) = {
       val assertRecord = new ProverAssertRecord(t, timeout)
-      val sepIdentifier = SymbExLogger.currentLog().openScope(assertRecord)
+      val sepIdentifier = symbExLog.openScope(assertRecord)
 
       val result = prover.assert(t, timeout)
 
-      if (SymbExLogger.enabled) {
-        val statistics = prover.statistics()
-        val deltaStatistics = SymbExLogger.getDeltaSmtStatistics(statistics)
-        assertRecord.statistics = Some(statistics ++ deltaStatistics)
+      symbExLog.whenEnabled {
+        assertRecord.statistics = Some(symbExLog.deltaStatistics(prover.statistics()))
       }
 
-      SymbExLogger.currentLog().closeScope(sepIdentifier)
+      symbExLog.closeScope(sepIdentifier)
 
       result
     }

src/main/scala/decider/Decider.scala

@@ -297,12 +297,13 @@ abstract class ProverStdIO(uniqueId: String,
     setTimeout(timeout)
 
     val guard = fresh("grd", Nil, sorts.Bool)
+    val guardApp = App(guard, Nil)
 
-    writeLine(s"(assert (=> $guard (not $goal)))")
+    writeLine(s"(assert (=> $guardApp (not $goal)))")
     readSuccess()
 
     val startTime = System.currentTimeMillis()
-    writeLine(s"(check-sat $guard)")
+    writeLine(s"(check-sat $guardApp)")
     val result = readUnsat()
     val endTime = System.currentTimeMillis()