Merge pull request #705 from viperproject/meilers_check_timeout_and_failure_gen

Fix timeouts and failure generation

Author: marcoeilers

src/main/scala/decider/Decider.scala

@@ -34,7 +34,7 @@ trait Decider {
   def pushScope(): Unit
   def popScope(): Unit
 
-  def checkSmoke(): Boolean
+  def checkSmoke(isAssert: Boolean = false): Boolean
 
   def setCurrentBranchCondition(t: Term, te: Option[ast.Exp] = None): Unit
   def setPathConditionMark(): Mark
@@ -236,7 +236,10 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     /* Asserting facts */
 
-    def checkSmoke(): Boolean = prover.check(Verifier.config.checkTimeout.toOption) == Unsat
+    def checkSmoke(isAssert: Boolean = false): Boolean = {
+      val timeout = if (isAssert) Verifier.config.assertTimeout.toOption else Verifier.config.checkTimeout.toOption
+      prover.check(timeout) == Unsat
+    }
 
     def check(t: Term, timeout: Int): Boolean = deciderAssert(t, Some(timeout))
 

src/main/scala/rules/ChunkSupporter.scala

@@ -126,7 +126,7 @@ object chunkSupporter extends ChunkSupportRules {
                   }
               }
               QS(s2.copy(h = s.h), h2, snap, v1)
-            case _ if v1.decider.checkSmoke() =>
+            case _ if v1.decider.checkSmoke(true) =>
               Success() // TODO: Mark branch as dead?
             case _ =>
               createFailure(ve, v1, s1, true)
@@ -227,7 +227,7 @@ object chunkSupporter extends ChunkSupportRules {
     findChunk[NonQuantifiedChunk](h.values, id, args, v) match {
       case Some(ch) if v.decider.check(IsPositive(ch.perm), Verifier.config.checkTimeout()) =>
         Q(s, ch.snap, v)
-      case _ if v.decider.checkSmoke() =>
+      case _ if v.decider.checkSmoke(true) =>
         Success() // TODO: Mark branch as dead?
       case _ =>
         createFailure(ve, v, s, true)

src/main/scala/rules/Executor.scala

@@ -403,7 +403,7 @@ object executor extends ExecutionRules {
       case assert @ ast.Assert(a: ast.FalseLit) =>
         /* "assert false" triggers a smoke check. If successful, we backtrack. */
         executionFlowController.tryOrFail0(s.copy(h = magicWandSupporter.getEvalHeap(s)), v)((s1, v1, QS) => {
-          if (v1.decider.checkSmoke())
+          if (v1.decider.checkSmoke(true))
             QS(s1.copy(h = s.h), v1)
           else
             createFailure(AssertFailed(assert) dueTo AssertionFalse(a), v1, s1, true)

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -144,10 +144,10 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     val relevantChunks = findChunksWithID[NonQuantifiedChunk](h.values, id).toSeq
 
     if (relevantChunks.isEmpty) {
-      if (v.decider.checkSmoke()) {
+      if (v.decider.checkSmoke(true)) {
         Success() // TODO: Mark branch as dead?
       } else {
-        createFailure(ve, v, s, true)
+        createFailure(ve, v, s)
       }
     } else {
       summarise(s, relevantChunks, resource, args, v)((s1, snap, _, permSum, v1) =>
@@ -217,10 +217,9 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
     if (relevantChunks.isEmpty) {
       // if no permission is exhaled, return none
-      if (v.decider.check(perms === NoPerm(), Verifier.config.checkTimeout())) {
-        Q(s, h, None, v)
-      } else {
-        createFailure(ve, v, s)
+      v.decider.assert(perms === NoPerm()){
+        case true => Q(s, h, None, v)
+        case false => createFailure(ve, v, s)
       }
     } else {
       if (!terms.utils.consumeExactRead(perms, s.constrainableARPs)) {

src/main/scala/rules/Producer.scala

@@ -160,7 +160,7 @@ object producer extends ProductionRules {
           // We will get an IllegalArgumentException from createSnapshotPair if sf(...) returns Unit.
           // This should never happen if we're in a reachable state, so here we check for that
           // (without timeout, since there is no fallback) and stop verifying the current branch.
-          case _: IllegalArgumentException if v.decider.check(False(), 0) =>
+          case _: IllegalArgumentException if v.decider.check(False(), Verifier.config.assertTimeout.getOrElse(0)) =>
             Unreachable()
         }
 

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -1224,11 +1224,6 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                            : VerificationResult = {
 
     val resource = resourceAccess.res(s.program)
-    val failure = resourceAccess match {
-      case locAcc: ast.LocationAccess => createFailure(pve dueTo InsufficientPermission(locAcc), v, s)
-      case wand: ast.MagicWand => createFailure(pve dueTo MagicWandChunkNotFound(wand), v, s)
-      case _ => sys.error(s"Found resource $resourceAccess, which is not yet supported as a quantified resource.")
-    }
     val chunkIdentifier = ChunkIdentifier(resource, s.program)
 
     val chunkOrderHeuristics = optChunkOrderHeuristic match {
@@ -1240,6 +1235,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     }
 
     if (s.exhaleExt) {
+      val failure = resourceAccess match {
+        case locAcc: ast.LocationAccess => createFailure(pve dueTo InsufficientPermission(locAcc), v, s)
+        case wand: ast.MagicWand => createFailure(pve dueTo MagicWandChunkNotFound(wand), v, s)
+        case _ => sys.error(s"Found resource $resourceAccess, which is not yet supported as a quantified resource.")
+      }
       magicWandSupporter.transfer(s, permissions, failure, v)((s1, h1, rPerm, v1) => {
         val (relevantChunks, otherChunks) =
           quantifiedChunkSupporter.splitHeap[QuantifiedBasicChunk](h1, chunkIdentifier)
@@ -1313,7 +1313,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
           val snap = ResourceLookup(resource, smDef1.sm, arguments, s2.program).convert(sorts.Snap)
           Q(s2, h1, snap, v)
         case (Incomplete(_), _, _) =>
-          failure
+          resourceAccess match {
+            case locAcc: ast.LocationAccess => createFailure(pve dueTo InsufficientPermission(locAcc), v, s)
+            case wand: ast.MagicWand => createFailure(pve dueTo MagicWandChunkNotFound(wand), v, s)
+            case _ => sys.error(s"Found resource $resourceAccess, which is not yet supported as a quantified resource.")
+          }
       }
     }
   }
@@ -1417,7 +1421,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
     v.decider.prover.comment("Final check if taken enough permissions")
     success =
-      if (success.isComplete || v.decider.check(tookEnoughCheck, 0) /* This check is a must-check, i.e. an assert */)
+      if (success.isComplete || v.decider.check(tookEnoughCheck, Verifier.config.assertTimeout.getOrElse(0)) /* This check is a must-check, i.e. an assert */)
         Complete()
       else
         success