Merge

src/main/resources/field_value_functions_axioms.smt2

@@ -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_declarations.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/predicate_snap_functions_axioms.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_declarations.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/z3config.smt2

@@ -2,7 +2,7 @@
 ; License, v. 2.0. If a copy of the MPL was not distributed with this
 ; file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-; Requires Z3 >= 4.3.2
+; Tested with Z3 4.8.7 and 4.12.1
 
 ; ATTENTION: Continuing multi-line statements must be indented with at least
 ;            one tab or two spaces. All other lines must not start with tabs
@@ -12,53 +12,19 @@
 ; setting options, is answered by a success (or error) reply from Z3. Silicon currently relies on
 ; these replies when it interacts with Z3 via stdio.
 (set-option :print-success true) ; Boogie: false
+(set-option :global-decls true) ; Necessary for push pop mode
 
-(set-option :global-decls true) ; Boogie: default
-(set-option :auto_config false) ; Usually a good idea
-
-(set-option :smt.restart_strategy 0)
-(set-option :smt.restart_factor |1.5|)
+; These options are taken from Dafny 4.0.0 and proven to work decently well with up-to-date Z3 (currently 4.12.1),
+; unlike the options used previously.
+(set-option :auto_config false)
 (set-option :smt.case_split 3)
 (set-option :smt.delay_units true)
-(set-option :smt.delay_units_threshold 16)
-(set-option :nnf.sk_hack true)
 (set-option :type_check true)
-(set-option :smt.bv.reflect true)
-
 (set-option :smt.mbqi false)
+(set-option :pp.bv_literals false)
 (set-option :smt.qi.eager_threshold 100)
-; (set-option :smt.qi.lazy_threshold 1000000000)
-(set-option :smt.qi.cost "(+ weight generation)")
-(set-option :smt.qi.max_multi_patterns 1000)
-; (set-option :smt.qi.profile true)
-; (set-option :smt.qi.profile_freq 100000)
-
-;; [2019-07-31 Malte] The next block of options are all randomness-related options that I could
-;; find in the description Z3 -pd emits. If not stated otherwise, the options are merely explicitly
-;; set to their default values.
-(set-option :smt.phase_selection 0) ; default: 3, Boogie: 0
-(set-option :sat.phase caching)
-(set-option :sat.random_seed 0)
-(set-option :nlsat.randomize true)
-(set-option :nlsat.seed 0)
-(set-option :nlsat.shuffle_vars false)
-(set-option :fp.spacer.order_children 0) ; Not available with Z3 4.5
-(set-option :fp.spacer.random_seed 0) ; Not available with Z3 4.5
-(set-option :smt.arith.random_initial_value true) ; Boogie: true
-(set-option :smt.random_seed 0)
-(set-option :sls.random_offset true)
-(set-option :sls.random_seed 0)
-(set-option :sls.restart_init false)
-(set-option :sls.walksat_ucb true)
-
-; (set-option :smt.macro_finder true)
-; (set-option :combined_solver.solver2_timeout 500)
-; (set-option :combined_solver.solver2_unknown 2)
-; (set-option :smt.arith.nl false)
-; (set-option :smt.arith.nl.gb false)
-    ; See http://stackoverflow.com/questions/28210673
-
-; (set-option :produce-models true)
-; (set-option :model false)
+(set-option :smt.arith.solver 2)
 (set-option :model.v2 true)
-; (set-option :model.compact true)
+
+; We want unlimited multipatterns
+(set-option :smt.qi.max_multi_patterns 1000)

src/main/scala/Config.scala

@@ -82,6 +82,18 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     val argType: ArgType.V = org.rogach.scallop.ArgType.LIST
   }
 
+  private val exhaleModeConverter: ValueConverter[ExhaleMode] = new ValueConverter[ExhaleMode] {
+    def parse(s: List[(String, List[String])]): Either[String, Option[ExhaleMode]] = s match {
+      case Seq((_, Seq("0"))) => Right(Some(ExhaleMode.Greedy))
+      case Seq((_, Seq("1"))) => Right(Some(ExhaleMode.MoreComplete))
+      case Seq((_, Seq("2"))) => Right(Some(ExhaleMode.MoreCompleteOnDemand))
+      case Seq() => Right(None)
+      case _ => Left(s"unexpected arguments")
+    }
+
+    val argType: ArgType.V = org.rogach.scallop.ArgType.LIST
+  }
+
   private val saturationTimeoutWeightsConverter: ValueConverter[ProverSaturationTimeoutWeights] = new ValueConverter[ProverSaturationTimeoutWeights] {
     def parse(s: List[(String, List[String])]): Either[String, Option[ProverSaturationTimeoutWeights]] = s match {
       case Seq((_, Seq(rawString))) =>
@@ -160,6 +172,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val reportReasonUnknown: ScallopOption[Boolean] = opt[Boolean]("reportReasonUnknown",
+    descr = "For every verification error, include the reason the SMT solver reported unknown.",
+    default = Some(false),
+    noshort = true
+  )
+
   val recursivePredicateUnfoldings: ScallopOption[Int] = opt[Int]("recursivePredicateUnfoldings",
     descr = (  "Evaluate n unfolding expressions in the body of predicates that (transitively) unfold "
              + "other instances of themselves (default: 1)"),
@@ -407,8 +425,8 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
-  val disableTempDirectory: ScallopOption[Boolean] = opt[Boolean]("disableTempDirectory",
-    descr = "Disable the creation of temporary data (default: ./tmp)",
+  val enableTempDirectory: ScallopOption[Boolean] = opt[Boolean]("enableTempDirectory",
+    descr = "Enable the creation of temporary directory to log prover interactions (default: ./tmp)",
     default = Some(false),
     noshort = true
   )
@@ -550,6 +568,8 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
             proverArgs.flatMap(args => proverTimeoutArg findFirstMatchIn args map(_.group(1).toInt))}
         .getOrElse(0)
 
+  lazy val useFlyweight: Boolean = prover() == "Z3-API"
+
   val maxHeuristicsDepth: ScallopOption[Int] = opt[Int]("maxHeuristicsDepth",
     descr = "Maximal number of nested heuristics applications (default: 3)",
     default = Some(3),
@@ -565,7 +585,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: pp)."),
+             + "'pp' (push-pop) and 'sc' (soft constraints) (default: pp)."),
     default = Some(AssertionMode.PushPop),
     noshort = true
   )(assertionModeConverter)
@@ -623,12 +643,30 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     case _ => opt
   }
 
-  val enableMoreCompleteExhale: ScallopOption[Boolean] = opt[Boolean]("enableMoreCompleteExhale",
-    descr = "Enable a more complete exhale version.",
+  // DEPRECATED and replaced by exhaleMode.
+  val moreCompleteExhale: ScallopOption[Boolean] = opt[Boolean]("enableMoreCompleteExhale",
+    descr =  "Warning: This option is deprecated. "
+           + "Please use 'exhaleMode' instead. "
+           + "Enables a more complete exhale version.",
     default = Some(false),
     noshort = true
   )
 
+  val exhaleModeOption: ScallopOption[ExhaleMode] = opt[ExhaleMode]("exhaleMode",
+    descr = "Exhale mode. Options are 0 (greedy, default), 1 (more complete exhale), 2 (more complete exhale on demand).",
+    default = None,
+    noshort = true
+  )(exhaleModeConverter)
+
+  lazy val exhaleMode: ExhaleMode = {
+    if (exhaleModeOption.isDefined)
+      exhaleModeOption()
+    else if (moreCompleteExhale())
+      ExhaleMode.MoreComplete
+    else
+      ExhaleMode.Greedy
+  }
+
   val numberOfErrorsToReport: ScallopOption[Int] = opt[Int]("numberOfErrorsToReport",
     descr = "Number of errors per member before the verifier stops. If this number is set to 0, all errors are reported.",
     default = Some(1),
@@ -763,12 +801,23 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
       sys.error(s"Unexpected combination: $other")
   }
 
-  validateOpt(counterexample, enableMoreCompleteExhale) {
-    case (Some(_), Some(false)) => Left(  s"Option ${counterexample.name} requires setting "
-                                        + s"flag ${enableMoreCompleteExhale.name}")
+  validateOpt(counterexample, moreCompleteExhale, exhaleModeOption) {
+    case (Some(_), Some(false), None) |
+         (Some(_), Some(_), Some(ExhaleMode.Greedy)) |
+         (Some(_), Some(_), Some(ExhaleMode.MoreCompleteOnDemand)) =>
+      Left(s"Option ${counterexample.name} requires setting "
+        + s"${exhaleModeOption.name} to 1 (more complete exhale)")
+    case (_, Some(true), Some(m)) if m != ExhaleMode.MoreComplete =>
+      Left(s"Contradictory values given for options ${moreCompleteExhale.name} and ${exhaleModeOption.name}")
     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)
@@ -804,6 +853,13 @@ object Config {
     case object SoftConstraints extends AssertionMode
   }
 
+  sealed trait ExhaleMode
+  object ExhaleMode {
+    case object Greedy extends ExhaleMode
+    case object MoreComplete extends ExhaleMode
+    case object MoreCompleteOnDemand extends ExhaleMode
+  }
+
   case class ProverStateSaturationTimeout(timeout: Int, comment: String)
 
   object StateConsolidationMode extends Enumeration {

src/main/scala/Silicon.scala

@@ -243,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()
@@ -338,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))