Simplify unfolds by reusing results of predicate verification (#929)

Author: marcoeilers

src/main/scala/Config.scala

@@ -193,6 +193,13 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val enableSimplifiedUnfolds: ScallopOption[Boolean] = opt[Boolean]("enableSimplifiedUnfolds",
+    descr = (  "Enable an optimization that reuses the results of verifying a predicate to simplify the process "
+             + "of unfolding it (via an unfold statement or an unfolding expression)."),
+    default = Some(false),
+    noshort = true
+  )
+
   val logLevel: ScallopOption[String] = opt[String]("logLevel",
     descr = "One of the log levels ALL, TRACE, DEBUG, INFO, WARN, ERROR, OFF",
     default = None,

src/main/scala/interfaces/Preamble.scala

@@ -29,10 +29,8 @@ trait PreambleContributor[+SO, +SY, +AX] extends StatefulComponent {
   def sortsAfterAnalysis: Iterable[SO]
   def declareSortsAfterAnalysis(sink: ProverLike): Unit
 
-  def symbolsAfterAnalysis: Iterable[SY]
   def declareSymbolsAfterAnalysis(sink: ProverLike): Unit
 
-  def axiomsAfterAnalysis: Iterable[AX]
   def emitAxiomsAfterAnalysis(sink: ProverLike): Unit
 }
 

src/main/scala/interfaces/state/Chunks.scala

@@ -6,12 +6,14 @@
 
 package viper.silicon.interfaces.state
 
+import viper.silicon
 import viper.silicon.resources.ResourceID
 import viper.silicon.state.terms.{Term, Var}
 import viper.silver.ast
 
-trait Chunk
-
+trait Chunk {
+  def substitute(terms: silicon.Map[Term, Term]): Chunk
+}
 trait ChunkIdentifer
 
 trait GeneralChunk extends Chunk {
@@ -22,6 +24,8 @@ trait GeneralChunk extends Chunk {
   def permMinus(perm: Term, permExp: Option[ast.Exp]): GeneralChunk
   def permPlus(perm: Term, permExp: Option[ast.Exp]): GeneralChunk
 
+  def permScale(perm: Term, permExp: Option[ast.Exp]): GeneralChunk
+
   val permExp: Option[ast.Exp]
 }
 

src/main/scala/rules/Consumer.scala

@@ -383,7 +383,7 @@ object consumer extends ConsumptionRules {
               val debugExp = Option.when(withExp)(DebugExp.createInstance(s"Field Trigger: ${eRcvrNew.get.toString}.${field.name}"))
               v2.decider.assume(FieldTrigger(field.name, smDef1.sm, tRcvr), debugExp)
               //            v2.decider.assume(PermAtMost(tPerm, FullPerm()))
-              s2.copy(smCache = smCache1)
+              s2.copy(smCache = smCache1, functionRecorder = s2.functionRecorder.recordFvfAndDomain(smDef1))
             } else {
               s2
             }
@@ -427,7 +427,7 @@ object consumer extends ConsumptionRules {
                   s2, predicate, s2.predicateFormalVarMap(predicate), relevantChunks, v2)
               val debugExp = Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}(${eArgsNew.mkString(", ")}))", isInternal_ = true))
               v2.decider.assume(PredicateTrigger(predicate.name, smDef1.sm, tArgs), debugExp)
-              s2.copy(smCache = smCache1)
+              s2.copy(smCache = smCache1, functionRecorder = s2.functionRecorder.recordFvfAndDomain(smDef1))
             } else {
               s2
             }
@@ -497,7 +497,7 @@ object consumer extends ConsumptionRules {
             val predName = MagicWandIdentifier(wand, s.program).toString
             val debugExp = Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger($predName($argsString))", isInternal_ = true))
             v1.decider.assume(PredicateTrigger(predName, smDef1.sm, tArgs), debugExp)
-            s1.copy(smCache = smCache1)
+            s1.copy(smCache = smCache1, functionRecorder = s1.functionRecorder.recordFvfAndDomain(smDef1))
           } else {
             s1
           }

src/main/scala/rules/Evaluator.scala

@@ -6,6 +6,7 @@
 
 package viper.silicon.rules
 
+import viper.silicon
 import viper.silicon.debugger.DebugExp
 import viper.silicon.Config.JoinMode
 import viper.silver.ast
@@ -316,7 +317,7 @@ object evaluator extends EvaluationRules {
                     val smLookup = Lookup(fa.field.name, smDef1.sm, tRcvr)
                     val fr2 =
                       s2.functionRecorder.recordSnapshot(fa, v1.decider.pcs.branchConditions, smLookup)
-                        .recordFvfAndDomain(smDef1)
+                        .recordFvfAndDomain(smDef1).recordPermMap(pmDef1)
                     val s3 = s2.copy(functionRecorder = fr2)
                     Q(s3, smLookup, newFa, v1)
                 }
@@ -578,7 +579,8 @@ object evaluator extends EvaluationRules {
                       quantifiedChunkSupporter.summarisingPermissionMap(
                         s1, wand, formalVars, relevantChunks, null, v1)
 
-                    (s1.copy(pmCache = pmCache), pmDef)
+                    val newFr = s1.functionRecorder.recordPermMap(pmDef)
+                    (s1.copy(pmCache = pmCache, functionRecorder = newFr), pmDef)
                   }
                   (s2, PredicatePermLookup(identifier.toString, pmDef.pm, args))
 
@@ -594,8 +596,8 @@ object evaluator extends EvaluationRules {
                     val (pmDef, pmCache) =
                       quantifiedChunkSupporter.summarisingPermissionMap(
                         s1, field, Seq(`?r`), relevantChunks, null, v1)
-
-                    (s1.copy(pmCache = pmCache), pmDef)
+                    val newFr = s1.functionRecorder.recordPermMap(pmDef)
+                    (s1.copy(pmCache = pmCache, functionRecorder = newFr), pmDef)
                   }
                   val currentPermAmount = PermLookup(field.name, pmDef.pm, args.head)
                   v1.decider.prover.comment(s"perm($resacc)  ~~>  assume upper permission bound")
@@ -1029,16 +1031,33 @@ object evaluator extends EvaluationRules {
                       val argsPairs: List[(Term, Option[ast.Exp])] = if (withExp) tArgs zip eArgsNew.get.map(Some(_)) else tArgs zip Seq.fill(tArgs.size)(None)
                       val insg = s7.g + Store(predicate.formalArgs map (_.localVar) zip argsPairs)
                       val s7a = s7.copy(g = insg).setConstrainable(s7.constrainableARPs, false)
-                      produce(s7a, toSf(snap.get), body, pve, v4)((s8, v5) => {
-                        val s9 = s8.copy(g = s7.g,
-                                         functionRecorder = s8.functionRecorder.changeDepthBy(-1),
-                                         recordVisited = s3.recordVisited,
-                                         permissionScalingFactor = s6.permissionScalingFactor,
-                                         permissionScalingFactorExp = s6.permissionScalingFactorExp,
-                                         constrainableARPs = s1.constrainableARPs)
-                                   .decCycleCounter(predicate)
-                        val s10 = v5.stateConsolidator(s9).consolidateOptionally(s9, v5)
-                        eval(s10, eIn, pve, v5)((s9, t9, e9, v9) => QB(s9, (t9, e9), v9))})})
+
+                      if (s7a.predicateData(predicate).predContents.isDefined) {
+                        val toReplace: silicon.Map[Term, Term] = silicon.Map.from(s7a.predicateData(predicate).params.get.zip(Seq(snap.get) ++ tArgs))
+                        predicateSupporter.producePredicateContents(s7a, s7a.predicateData(predicate).predContents.get, toReplace, v4, true)((s8, v5) => {
+                          val s9 = s8.copy(g = s7.g,
+                            functionRecorder = s8.functionRecorder.changeDepthBy(-1),
+                            recordVisited = s3.recordVisited,
+                            permissionScalingFactor = s6.permissionScalingFactor,
+                            permissionScalingFactorExp = s6.permissionScalingFactorExp,
+                            constrainableARPs = s1.constrainableARPs)
+                            .decCycleCounter(predicate)
+                          val s10 = v5.stateConsolidator(s9).consolidateOptionally(s9, v5)
+                          eval(s10, eIn, pve, v5)((s9, t9, e9, v9) => QB(s9, (t9, e9), v9))
+                        })
+                      } else {
+                        produce(s7a, toSf(snap.get), body, pve, v4)((s8, v5) => {
+                          val s9 = s8.copy(g = s7.g,
+                                           functionRecorder = s8.functionRecorder.changeDepthBy(-1),
+                                           recordVisited = s3.recordVisited,
+                                           permissionScalingFactor = s6.permissionScalingFactor,
+                                           permissionScalingFactorExp = s6.permissionScalingFactorExp,
+                                           constrainableARPs = s1.constrainableARPs)
+                                     .decCycleCounter(predicate)
+                          val s10 = v5.stateConsolidator(s9).consolidateOptionally(s9, v5)
+                          eval(s10, eIn, pve, v5)((s9, t9, e9, v9) => QB(s9, (t9, e9), v9))})
+                      }
+                    })
                   })(join(eIn.typ, "joined_unfolding", s2.relevantQuantifiedVariables.map(_._1),
                     Option.when(withExp)(s2.relevantQuantifiedVariables.map(_._2.get)), v2))((s12, r12, v7)
                     => {
@@ -1049,7 +1068,8 @@ object evaluator extends EvaluationRules {
                   createFailure(pve dueTo NonPositivePermission(ePerm.get), v2, s2, IsPositive(tPerm), ePermNew.map(p => ast.PermGtCmp(p, ast.NoPerm()())(p.pos, p.info, p.errT)))}))
         } else {
           val unknownValue = v.decider.appliedFresh("recunf", v.symbolConverter.toSort(eIn.typ), s.relevantQuantifiedVariables.map(_._1))
-          Q(s, unknownValue, Option.when(withExp)(ast.LocalVarWithVersion("unknownValue", eIn.typ)(eIn.pos, eIn.info, eIn.errT)), v)
+          val newFuncRec = s.functionRecorder.recordFreshSnapshot(unknownValue.applicable.asInstanceOf[Function])
+          Q(s.copy(functionRecorder = newFuncRec), unknownValue, Option.when(withExp)(ast.LocalVarWithVersion("unknownValue", eIn.typ)(eIn.pos, eIn.info, eIn.errT)), v)
         }
 
       case ast.Applying(wand, eIn) =>