Merge pull request #701 from viperproject/meilers_reason_unknown

Add option to report reason-unknown

Author: marcoeilers

src/main/scala/Config.scala

@@ -172,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)"),

src/main/scala/decider/Decider.scala

@@ -387,6 +387,6 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     override def isModelValid(): Boolean = prover.isModelValid()
 
-    override def clearModel(): Unit = prover.clearLastModel()
+    override def clearModel(): Unit = prover.clearLastAssert()
   }
 }

src/main/scala/decider/ProverStdIO.scala

@@ -40,6 +40,7 @@ abstract class ProverStdIO(uniqueId: String,
   protected var output: PrintWriter = _
 
   var proverPath: Path = _
+  var lastReasonUnknown : String = _
   var lastModel : String = _
 
   def exeEnvironmentalVariable: String
@@ -252,6 +253,7 @@ abstract class ProverStdIO(uniqueId: String,
 
     if (!result) {
       retrieveAndSaveModel()
+      retrieveReasonUnknown()
     }
 
     pop()
@@ -285,6 +287,16 @@ abstract class ProverStdIO(uniqueId: String,
     }
   }
 
+  protected def retrieveReasonUnknown(): Unit = {
+    if (Verifier.config.reportReasonUnknown()) {
+      writeLine("(get-info :reason-unknown)")
+      var result = readLine()
+      if (result.startsWith("(:reason-unknown \""))
+        result = result.substring(18, result.length - 2)
+      lastReasonUnknown = result
+    }
+  }
+
   override def hasModel(): Boolean = {
     lastModel != null
   }
@@ -474,5 +486,10 @@ abstract class ProverStdIO(uniqueId: String,
 
   override def getModel(): Model = Model(lastModel)
 
-  override def clearLastModel(): Unit = lastModel = null
+  override def getReasonUnknown(): String = lastReasonUnknown
+
+  override def clearLastAssert(): Unit = {
+    lastReasonUnknown = null
+    lastModel = null
+  }
 }

src/main/scala/decider/Z3ProverAPI.scala

@@ -85,6 +85,7 @@ class Z3ProverAPI(uniqueId: String,
   protected var ctx: Context = _
 
   var proverPath: Path = _
+  var lastReasonUnknown : String = _
   var lastModel : Model = _
 
   var emittedPreambleString = mutable.Queue[String]()
@@ -246,6 +247,7 @@ class Z3ProverAPI(uniqueId: String,
 
     if (!result) {
       retrieveAndSaveModel()
+      retrieveReasonUnknown()
     }
 
     (result, endTime - startTime)
@@ -272,6 +274,12 @@ class Z3ProverAPI(uniqueId: String,
     }
   }
 
+  protected def retrieveReasonUnknown(): Unit = {
+    if (Verifier.config.reportReasonUnknown()) {
+      lastReasonUnknown = prover.getReasonUnknown
+    }
+  }
+
   protected def assertUsingSoftConstraints(goal: Term, timeout: Option[Int]): (Boolean, Long) = {
     endPreamblePhase()
     setTimeout(timeout)
@@ -417,7 +425,12 @@ class Z3ProverAPI(uniqueId: String,
     lastModel != null
   }
 
-  override def clearLastModel(): Unit = lastModel = null
+  override def getReasonUnknown(): String = lastReasonUnknown
+
+  override def clearLastAssert(): Unit = {
+    lastReasonUnknown = null
+    lastModel = null
+  }
 
   protected def setTimeout(timeout: Option[Int]): Unit = {
     val effectiveTimeout = timeout.getOrElse(Verifier.config.proverTimeout)

src/main/scala/interfaces/Verification.scala

@@ -100,7 +100,9 @@ case class Failure/*[ST <: Store[ST],
   override lazy val toString: String = message.readableMessage
 }
 
-case class SiliconFailureContext(branchConditions: Seq[ast.Exp], counterExample: Option[Counterexample]) extends FailureContext {
+case class SiliconFailureContext(branchConditions: Seq[ast.Exp],
+                                 counterExample: Option[Counterexample],
+                                 reasonUnknown: Option[String]) extends FailureContext {
   lazy val branchConditionString: String = {
     if(branchConditions.nonEmpty) {
       val branchConditionsString =
@@ -118,7 +120,15 @@ case class SiliconFailureContext(branchConditions: Seq[ast.Exp], counterExample:
     counterExample.fold("")(ce => s"\n\t\tcounterexample:\n$ce")
   }
 
-  override lazy val toString: String = branchConditionString + counterExampleString
+  lazy val reasonUnknownString: String = {
+    if (reasonUnknown.isDefined) {
+      s"\nPotential prover incompleteness: ${reasonUnknown.get}"
+    } else {
+      ""
+    }
+  }
+
+  override lazy val toString: String = branchConditionString + counterExampleString + reasonUnknownString
 }
 
 trait SiliconCounterexample extends Counterexample {

src/main/scala/interfaces/decider/Prover.scala

@@ -37,8 +37,8 @@ trait Prover extends ProverLike with StatefulComponent {
   def hasModel(): Boolean
   def isModelValid(): Boolean
   def getModel(): Model
-  def clearLastModel(): Unit
-
+  def getReasonUnknown(): String
+  def clearLastAssert(): Unit
   def name: String
   def minVersion: Version
   def maxVersion: Option[Version]

src/main/scala/rules/SymbolicExecutionRules.scala

@@ -23,10 +23,12 @@ trait SymbolicExecutionRules {
         wrapped
       case _ => ve
     }
-    val counterexample: Option[Counterexample] = if (v != null && Verifier.config.counterexample.toOption.isDefined) {
+    if (v != null && (Verifier.config.reportReasonUnknown() || Verifier.config.counterexample.toOption.isDefined)) {
       if (generateNewModel || !v.decider.hasModel()) {
         v.decider.generateModel()
       }
+    }
+    val counterexample: Option[Counterexample] = if (v != null && Verifier.config.counterexample.toOption.isDefined) {
       if (v.decider.isModelValid()) {
         val nativeModel = v.decider.getModel()
         val ce_type = Verifier.config.counterexample()
@@ -47,6 +49,12 @@ trait SymbolicExecutionRules {
       } else None
     } else None
 
+    val reasonUnknown = if (v != null && Verifier.config.reportReasonUnknown()) {
+      Some(v.decider.prover.getReasonUnknown())
+    } else {
+      None
+    }
+
     val branchconditions = if (Verifier.config.enableBranchconditionReporting()) {
       v.decider.pcs.branchConditionExps.flatten
         .filterNot(e => e.isInstanceOf[viper.silver.ast.TrueLit]) /* remove "true" bcs introduced by viper.silicon.utils.ast.BigAnd */
@@ -56,7 +64,7 @@ trait SymbolicExecutionRules {
           case _ => (-1, -1)
         })
     } else Seq()
-    res.failureContexts = Seq(SiliconFailureContext(branchconditions, counterexample))
+    res.failureContexts = Seq(SiliconFailureContext(branchconditions, counterexample, reasonUnknown))
     Failure(res, v.reportFurtherErrors())
 
   }