Optionally skip re-verification of well-definedness

src/main/scala/Config.scala

@@ -160,6 +160,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val avoidReverifyingWelldefinedness: ScallopOption[Boolean] = opt[Boolean]("avoidReverifyingWelldefinedness",
+    descr = "Do not re-verify well-definedness of contracts or predicates when using them",
+    default = Some(false),
+    noshort = true
+  )
+
   val includeMethods: ScallopOption[String] = opt[String]("includeMethods",
     descr = "Include methods in verification (default: '*'). Wildcard characters are '?' and '*'. ",
     default = Some(".*"),

src/main/scala/decider/Decider.scala

@@ -49,7 +49,10 @@ trait Decider {
    *         1. It passes State and Operations to the continuation
    *         2. The implementation reacts to a failing assertion by e.g. a state consolidation
    */
-  def assert(t: Term, timeout: Option[Int] = None)(Q:  Boolean => VerificationResult): VerificationResult
+  def assertRaw(t: Term, timeout: Option[Int] = None)(Q:  Boolean => VerificationResult): VerificationResult
+
+  def assertWD(t: Term, s: State, v: Verifier, timeout: Option[Int] = None)(Q:  Boolean => VerificationResult): VerificationResult
+  def assertC(t: Term, s: State, v: Verifier, timeout: Option[Int] = None)(Q:  Boolean => VerificationResult): VerificationResult
 
   def fresh(id: String, sort: Sort): Var
   def fresh(id: String, argSorts: Seq[Sort], resultSort: Sort): Function
@@ -243,9 +246,30 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def check(t: Term, timeout: Int): Boolean = deciderAssert(t, Some(timeout))
 
-    def assert(t: Term, timeout: Option[Int] = Verifier.config.assertTimeout.toOption)
-              (Q: Boolean => VerificationResult)
-              : VerificationResult = {
+    def assertC(t: Term, s: State, v: Verifier, timeout: Option[Int] = Verifier.config.assertTimeout.toOption)
+               (Q: Boolean => VerificationResult)
+               : VerificationResult = {
+      if (s.isKnownCorrect) {
+        Q(true)
+      } else {
+        assertRaw(t, timeout)(Q)
+      }
+    }
+
+    def assertWD(t: Term, s: State, v: Verifier, timeout: Option[Int] = Verifier.config.assertTimeout.toOption)
+                (Q: Boolean => VerificationResult)
+                : VerificationResult = {
+      if ((Verifier.config.avoidReverifyingWelldefinedness() && s.isKnownWelldefined) || s.isKnownCorrect) {
+        // TODO: ME: We could assume(t) here, should we?
+        Q(true)
+      } else {
+        assertRaw(t, timeout)(Q)
+      }
+    }
+
+    def assertRaw(t: Term, timeout: Option[Int] = Verifier.config.assertTimeout.toOption)
+                 (Q: Boolean => VerificationResult)
+                 : VerificationResult = {
 
       val success = deciderAssert(t, timeout)
 

src/main/scala/rules/Consumer.scala

@@ -480,7 +480,7 @@ object consumer extends ConsumptionRules {
             Quantification(q, vars, Implies(transformed, body), trgs, name, isGlob, weight)
           case _ => t
         }
-        v2.decider.assert(termToAssert) {
+        v2.decider.assertC(termToAssert, s2, v2) {
           case true =>
             v2.decider.assume(t)
             QS(s3, v2)

src/main/scala/rules/Evaluator.scala

@@ -213,7 +213,7 @@ object evaluator extends EvaluationRules {
                 val s2 = s1.copy(functionRecorder = fr1)
                 Q(s2, fvfLookup, v1)
               } else {
-                v1.decider.assert(IsPositive(totalPermissions.replace(`?r`, tRcvr))) {
+                v1.decider.assertWD(IsPositive(totalPermissions.replace(`?r`, tRcvr)), s1, v1) {
                   case false =>
                     createFailure(pve dueTo InsufficientPermission(fa), v1, s1)
                   case true =>
@@ -247,7 +247,7 @@ object evaluator extends EvaluationRules {
                   val totalPermissions = PermLookup(fa.field.name, pmDef1.pm, tRcvr)
                   IsPositive(totalPermissions)
                 }
-              v1.decider.assert(permCheck) {
+              v1.decider.assertWD(permCheck, s1, v1) {
                 case false =>
                   createFailure(pve dueTo InsufficientPermission(fa), v1, s1)
                 case true =>
@@ -719,6 +719,7 @@ object evaluator extends EvaluationRules {
                 reasonOffendingNode.replace(formalsToActuals)), exampleTrafo)
             val s3 = s2.copy(g = Store(fargs.zip(tArgs)),
                              recordVisited = true,
+                             isKnownWelldefined= true,
                              functionRecorder = s2.functionRecorder.changeDepthBy(+1),
                                 /* Temporarily disable the recorder: when recording (to later on
                                  * translate a particular function fun) and a function application
@@ -756,6 +757,7 @@ object evaluator extends EvaluationRules {
                                recordVisited = s2.recordVisited,
                                functionRecorder = fr5,
                                smDomainNeeded = s2.smDomainNeeded,
+                               isKnownWelldefined = s2.isKnownWelldefined,
                                hackIssue387DisablePermissionConsumption = s.hackIssue387DisablePermissionConsumption)
               QB(s5, tFApp, v3)})
             /* TODO: The join-function is heap-independent, and it is not obvious how a
@@ -771,7 +773,7 @@ object evaluator extends EvaluationRules {
         if (s.cycles(predicate) < Verifier.config.recursivePredicateUnfoldings()) {
           evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) =>
             eval(s1, ePerm, pve, v1)((s2, tPerm, v2) =>
-              v2.decider.assert(IsNonNegative(tPerm)) { // TODO: Replace with permissionSupporter.assertNotNegative
+              v2.decider.assertWD(IsNonNegative(tPerm), s2, v2) { // TODO: Replace with permissionSupporter.assertNotNegative
                 case true =>
                   joiner.join[Term, Term](s2, v2)((s3, v3, QB) => {
                     val s4 = s3.incCycleCounter(predicate)
@@ -801,11 +803,12 @@ object evaluator extends EvaluationRules {
                       val body = predicate.body.get /* Only non-abstract predicates can be unfolded */
                       val s7 = s6.scalePermissionFactor(tPerm)
                       val insg = s7.g + Store(predicate.formalArgs map (_.localVar) zip tArgs)
-                      val s7a = s7.copy(g = insg)
+                      val s7a = s7.copy(g = insg, isKnownWelldefined = true)
                       produce(s7a, toSf(snap), body, pve, v4)((s8, v5) => {
                         val s9 = s8.copy(g = s7.g,
                                          functionRecorder = s8.functionRecorder.changeDepthBy(-1),
                                          recordVisited = s3.recordVisited,
+                                         isKnownWelldefined = s7.isKnownWelldefined,
                                          permissionScalingFactor = s6.permissionScalingFactor)
                                    .decCycleCounter(predicate)
                         val s10 = v5.stateConsolidator.consolidateIfRetrying(s9, v5)
@@ -834,9 +837,9 @@ object evaluator extends EvaluationRules {
           if (s1.triggerExp) {
             Q(s1, SeqAt(t0, t1), v1)
           } else {
-            v1.decider.assert(AtLeast(t1, IntLiteral(0))) {
+            v1.decider.assertWD(AtLeast(t1, IntLiteral(0)), s1, v1) {
               case true =>
-                v1.decider.assert(Less(t1, SeqLength(t0))) {
+                v1.decider.assertWD(Less(t1, SeqLength(t0)), s1, v1) {
                   case true =>
                     Q(s1, SeqAt(t0, t1), v1)
                   case false =>
@@ -849,7 +852,7 @@ object evaluator extends EvaluationRules {
                 val failure1 = createFailure(pve dueTo SeqIndexNegative(e0, e1), v1, s1)
                 if (s1.retryLevel == 0) {
                   v1.decider.assume(AtLeast(t1, IntLiteral(0)))
-                  v1.decider.assert(Less(t1, SeqLength(t0))) {
+                  v1.decider.assertWD(Less(t1, SeqLength(t0)), s1, v1) {
                     case true =>
                       failure1 combine Q(s1, SeqAt(t0, t1), v1)
                     case false =>
@@ -872,9 +875,9 @@ object evaluator extends EvaluationRules {
           if (s1.triggerExp) {
             Q(s1, SeqUpdate(t0, t1, t2), v1)
           } else {
-            v1.decider.assert(AtLeast(t1, IntLiteral(0))) {
+            v1.decider.assertWD(AtLeast(t1, IntLiteral(0)), s1, v1) {
               case true =>
-                v1.decider.assert(Less(t1, SeqLength(t0))) {
+                v1.decider.assertWD(Less(t1, SeqLength(t0)), s1, v1) {
                   case true =>
                     Q(s1, SeqUpdate(t0, t1, t2), v1)
                   case false =>
@@ -887,7 +890,7 @@ object evaluator extends EvaluationRules {
                 val failure1 = createFailure(pve dueTo SeqIndexNegative(e0, e1), v1, s1)
                 if (s1.retryLevel == 0) {
                   v1.decider.assume(AtLeast(t1, IntLiteral(0)))
-                  v1.decider.assert(Less(t1, SeqLength(t0))) {
+                  v1.decider.assertWD(Less(t1, SeqLength(t0)), s1, v1) {
                     case true =>
                       failure1 combine Q(s1, SeqUpdate(t0, t1, t2), v1)
                     case false =>
@@ -983,7 +986,7 @@ object evaluator extends EvaluationRules {
       case ast.MapLookup(base, key) =>
         evals2(s, Seq(base, key), Nil, _ => pve, v)({
           case (s1, Seq(baseT, keyT), v1) if s1.triggerExp => Q(s1, MapLookup(baseT, keyT), v1)
-          case (s1, Seq(baseT, keyT), v1) => v1.decider.assert(SetIn(keyT, MapDomain(baseT))) {
+          case (s1, Seq(baseT, keyT), v1) => v1.decider.assertWD(SetIn(keyT, MapDomain(baseT)), s1, v1) {
             case true => Q(s1, MapLookup(baseT, keyT), v1)
             case false =>
               v1.decider.assume(SetIn(keyT, MapDomain(baseT)))
@@ -1159,7 +1162,7 @@ object evaluator extends EvaluationRules {
                              (Q: (State, Term, Verifier) => VerificationResult)
                              : VerificationResult = {
 
-    v.decider.assert(tDivisor !== tZero){
+    v.decider.assertWD(tDivisor !== tZero, s, v){
       case true => Q(s, t, v)
       case false =>
         val failure = createFailure(pve dueTo DivisionByZero(eDivisor), v, s)

src/main/scala/rules/Executor.scala

@@ -483,7 +483,7 @@ object executor extends ExecutionRules {
           val preCondLog = new CommentRecord("Precondition", s1, v1.decider.pcs)
           val preCondId = v1.symbExLog.openScope(preCondLog)
           val s2 = s1.copy(g = Store(fargs.zip(tArgs)),
-                           recordVisited = true)
+                           recordVisited = true, isKnownWelldefined = true)
           consumes(s2, meth.pres, _ => pvePre, v1)((s3, _, v2) => {
             v2.symbExLog.closeScope(preCondId)
             val postCondLog = new CommentRecord("Postcondition", s3, v2.decider.pcs)
@@ -498,7 +498,8 @@ object executor extends ExecutionRules {
                               .map(p => (p._1, s5.g(p._2))).toMap)
               val s6 = s5.copy(g = s1.g + gLhs,
                                oldHeaps = s1.oldHeaps,
-                               recordVisited = s1.recordVisited)
+                               recordVisited = s1.recordVisited,
+                               isKnownWelldefined = s1.isKnownWelldefined)
               v3.symbExLog.closeScope(sepIdentifier)
               Q(s6, v3)})})})
 

src/main/scala/rules/HavocSupporter.scala

@@ -125,7 +125,7 @@ object havocSupporter extends SymbolicExecutionRules {
         v.decider.prover.comment("Check havocall receiver injectivity")
         val notInjectiveReason = QuasihavocallNotInjective(havocall)
 
-        v.decider.assert(receiverInjectivityCheck) {
+        v.decider.assertWD(receiverInjectivityCheck, s1, v) {
           case false => createFailure(pve dueTo notInjectiveReason, v, s1)
           case true =>
             // Generate the inverse axioms

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -151,7 +151,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
       }
     } else {
       summarise(s, relevantChunks, resource, args, v)((s1, snap, _, permSum, v1) =>
-        v.decider.assert(IsPositive(permSum)) {
+        v.decider.assertWD(IsPositive(permSum), s1, v) {
           case true =>
             Q(s1, snap, v1)
           case false =>
@@ -189,7 +189,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     val relevantChunks = findChunksWithID[NonQuantifiedChunk](h.values, id).toSeq
 
     summarise(s, relevantChunks, resource, args, v)((s1, snap, _, permSum, v1) =>
-      v.decider.assert(IsPositive(permSum)) {
+      v.decider.assertWD(IsPositive(permSum), s1, v) {
         case true =>
           Q(s1, h, Some(snap), v1)
         case false =>
@@ -217,7 +217,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
     if (relevantChunks.isEmpty) {
       // if no permission is exhaled, return none
-      v.decider.assert(perms === NoPerm()){
+      v.decider.assertC(perms === NoPerm(), s, v){
         case true => Q(s, h, None, v)
         case false => createFailure(ve, v, s)
       }
@@ -289,7 +289,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
           if (!moreNeeded) {
             Q(s1, newHeap, Some(condSnap), v1)
           } else {
-            v1.decider.assert(pNeeded === NoPerm()) {
+            v1.decider.assertC(pNeeded === NoPerm(), s1, v1) {
               case true =>
                 Q(s1, newHeap, Some(condSnap), v1)
               case false =>
@@ -342,7 +342,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
     val s1 = s.copy(functionRecorder = newFr)
 
-    v.decider.assert(totalPermTaken !== NoPerm()) {
+    v.decider.assertC(totalPermTaken !== NoPerm(), s1, v) {
       case true =>
         v.decider.assume(perms === totalPermTaken)
         summarise(s1, relevantChunks.toSeq, resource, args, v)((s2, snap, _, _, v1) =>

src/main/scala/rules/PermissionSupporter.scala

@@ -23,7 +23,7 @@ object permissionSupporter extends SymbolicExecutionRules {
       case k: Var if s.constrainableARPs.contains(k) =>
         Q(s, v)
       case _ =>
-        v.decider.assert(perms.IsNonNegative(tPerm)) {
+        v.decider.assertWD(perms.IsNonNegative(tPerm), s, v) {
           case true => Q(s, v)
           case false => createFailure(pve dueTo NegativePermission(ePerm), v, s)
         }

src/main/scala/rules/PredicateSupporter.scala

@@ -57,15 +57,15 @@ object predicateSupporter extends PredicateSupportRules {
     val body = predicate.body.get /* Only non-abstract predicates can be unfolded */
     val gIns = s.g + Store(predicate.formalArgs map (_.localVar) zip tArgs)
     val s1 = s.copy(g = gIns,
-                    smDomainNeeded = true)
+                    smDomainNeeded = true, isKnownWelldefined = true)
               .scalePermissionFactor(tPerm)
     consume(s1, body, pve, v)((s1a, snap, v1) => {
       if (!Verifier.config.disableFunctionUnfoldTrigger()) {
         val predTrigger = App(s1a.predicateData(predicate).triggerFunction,
           snap.convert(terms.sorts.Snap) +: tArgs)
         v1.decider.assume(predTrigger)
       }
-      val s2 = s1a.setConstrainable(constrainableWildcards, false)
+      val s2 = s1a.copy(isKnownWelldefined = s.isKnownWelldefined).setConstrainable(constrainableWildcards, false)
       if (s2.qpPredicates.contains(predicate)) {
         val predSnap = snap.convert(s2.predicateSnapMap(predicate))
         val formalArgs = s2.predicateFormalVarMap(predicate)
@@ -134,7 +134,7 @@ object predicateSupporter extends PredicateSupportRules {
         pve,
         v
       )((s2, h2, snap, v1) => {
-        val s3 = s2.copy(g = gIns, h = h2)
+        val s3 = s2.copy(g = gIns, h = h2, isKnownWelldefined = true)
                    .setConstrainable(constrainableWildcards, false)
         produce(s3, toSf(snap), body, pve, v1)((s4, v2) => {
           v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold)
@@ -145,14 +145,15 @@ object predicateSupporter extends PredicateSupportRules {
             v2.decider.assume(predicateTrigger)
           }
           Q(s4.copy(g = s.g,
-                    permissionScalingFactor = s.permissionScalingFactor),
+                    permissionScalingFactor = s.permissionScalingFactor,
+                    isKnownWelldefined = s.isKnownWelldefined),
             v2)})
       })
     } else {
       val ve = pve dueTo InsufficientPermission(pa)
       val description = s"consume ${pa.pos}: $pa"
       chunkSupporter.consume(s1, s1.h, predicate, tArgs, s1.permissionScalingFactor, ve, v, description)((s2, h1, snap, v1) => {
-        val s3 = s2.copy(g = gIns, h = h1)
+        val s3 = s2.copy(g = gIns, h = h1, isKnownWelldefined = true)
                    .setConstrainable(constrainableWildcards, false)
         produce(s3, toSf(snap), body, pve, v1)((s4, v2) => {
           v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold)
@@ -162,7 +163,8 @@ object predicateSupporter extends PredicateSupportRules {
             v2.decider.assume(predicateTrigger)
           }
           val s5 = s4.copy(g = s.g,
-                           permissionScalingFactor = s.permissionScalingFactor)
+                           permissionScalingFactor = s.permissionScalingFactor,
+                           isKnownWelldefined = s.isKnownWelldefined)
           Q(s5, v2)})})
     }
   }

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -861,7 +861,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     val nonNegImplication = Implies(tCond, perms.IsNonNegative(tPerm))
     val nonNegTerm = Forall(qvars, Implies(FunctionPreconditionTransformer.transform(nonNegImplication, s.program), nonNegImplication), Nil)
     // TODO: Replace by QP-analogue of permissionSupporter.assertNotNegative
-    v.decider.assert(nonNegTerm) {
+    v.decider.assertWD(nonNegTerm, s, v) {
       case true =>
 
         /* TODO: Can we omit/simplify the injectivity check in certain situations? */
@@ -881,7 +881,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
           }
         v.decider.prover.comment("Check receiver injectivity")
         v.decider.assume(FunctionPreconditionTransformer.transform(receiverInjectivityCheck, s.program))
-        v.decider.assert(receiverInjectivityCheck) {
+        v.decider.assertWD(receiverInjectivityCheck, s, v) {
           case true =>
             val ax = inverseFunctions.axiomInversesOfInvertibles
             val inv = inverseFunctions.copy(axiomInversesOfInvertibles = Forall(ax.vars, ax.body, effectiveTriggers))
@@ -1066,7 +1066,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     val nonNegImplication = Implies(tCond, perms.IsNonNegative(tPerm))
     val nonNegTerm = Forall(qvars, Implies(FunctionPreconditionTransformer.transform(nonNegImplication, s.program), nonNegImplication), Nil)
     // TODO: Replace by QP-analogue of permissionSupporter.assertNotNegative
-    v.decider.assert(nonNegTerm) {
+    v.decider.assertWD(nonNegTerm, s, v) {
       case true =>
         val hints = quantifiedChunkSupporter.extractHints(Some(tCond), tArgs)
         val chunkOrderHeuristics =
@@ -1099,7 +1099,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             qidPrefix = qid,
             program = s.program)
         v.decider.prover.comment("Check receiver injectivity")
-        v.decider.assert(receiverInjectivityCheck) {
+        v.decider.assertWD(receiverInjectivityCheck, s, v) {
           case true =>
             val qvarsToInvOfLoc = inverseFunctions.qvarsToInversesOf(formalQVars)
             val condOfInvOfLoc = tCond.replace(qvarsToInvOfLoc)