Avoiding Viper functions in hashsets and as keys in hashmaps

src/main/scala/interfaces/Verification.scala

@@ -6,7 +6,7 @@
 
 package viper.silicon.interfaces
 
-import viper.silicon.debugger.{DebugAxiom, DebugExp, DebugExpPrintConfiguration}
+import viper.silicon.debugger.{DebugAxiom, DebugExp}
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.interfaces.state.Chunk
 import viper.silicon.reporting._

src/main/scala/rules/Evaluator.scala

@@ -719,17 +719,17 @@ object evaluator extends EvaluationRules {
                       if (!Verifier.config.disableFunctionUnfoldTrigger()) {
                         val eArgsString = eArgsNew.mkString(", ")
                         val debugExp = Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eArgsString))", isInternal_ = true))
-                        v4.decider.assume(App(s.predicateData(predicate).triggerFunction, snap.get.convert(terms.sorts.Snap) +: tArgs), debugExp)
+                        v4.decider.assume(App(s.predicateData(predicate.name).triggerFunction, snap.get.convert(terms.sorts.Snap) +: tArgs), debugExp)
                       }
                       val body = predicate.body.get /* Only non-abstract predicates can be unfolded */
                       val s7 = s6.scalePermissionFactor(tPerm, ePermNew)
                       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)
 
-                      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) => {
+                      if (s7a.predicateData(predicate.name).predContents.isDefined) {
+                        val toReplace: silicon.Map[Term, Term] = silicon.Map.from(s7a.predicateData(predicate.name).params.get.zip(Seq(snap.get) ++ tArgs))
+                        predicateSupporter.producePredicateContents(s7a, s7a.predicateData(predicate.name).predContents.get, toReplace, v4, true)((s8, v5) => {
                           val s9 = s8.copy(g = s7.g,
                             functionRecorder = s8.functionRecorder.changeDepthBy(-1),
                             recordVisited = s3.recordVisited,

src/main/scala/rules/HeapSupporter.scala

@@ -474,7 +474,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
                 val predicate = resource.asInstanceOf[ast.Predicate]
                 val argsString = eArgs.mkString(", ")
                 val debugExp = Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($argsString))", isInternal_ = true))
-                v2.decider.assume(App(s2.predicateData(predicate).triggerFunction, snap1 +: tArgs), debugExp)
+                v2.decider.assume(App(s2.predicateData(predicate.name).triggerFunction, snap1 +: tArgs), debugExp)
               }
               Q(s2.copy(h = h2), v2)
             })
@@ -543,7 +543,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
       case f: ast.Field =>
         sf(sorts.FieldValueFunction(v.snapshotSupporter.optimalSnapshotSort(f, s, v), f.name), v)
       case p: ast.Predicate =>
-        sf(sorts.PredicateSnapFunction(s.predicateSnapMap(p), p.name), v)
+        sf(sorts.PredicateSnapFunction(s.predicateSnapMap(p.name), p.name), v)
       case _: ast.MagicWand =>
         sf(sorts.PredicateSnapFunction(sorts.Snap, qid), v)
     }

src/main/scala/rules/PredicateSupporter.scala

@@ -12,7 +12,7 @@ import viper.silicon.debugger.DebugExp
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.interfaces.VerificationResult
 import viper.silicon.interfaces.state.{ChunkIdentifer, GeneralChunk, NonQuantifiedChunk}
-import viper.silicon.resources.{FieldID, PredicateID}
+import viper.silicon.resources.FieldID
 import viper.silicon.state._
 import viper.silicon.state.terms._
 import viper.silicon.state.terms.predef.`?r`
@@ -21,7 +21,6 @@ import viper.silicon.utils.toSf
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
 import viper.silver.verifier.PartialVerificationError
-import viper.silver.verifier.reasons.InsufficientPermission
 
 trait PredicateSupportRules extends SymbolicExecutionRules {
   def fold(s: State,
@@ -78,7 +77,7 @@ object predicateSupporter extends PredicateSupportRules {
               .scalePermissionFactor(tPerm, ePerm)
     consume(s1, body, true, pve, v)((s1a, snap, v1) => {
       if (!Verifier.config.disableFunctionUnfoldTrigger()) {
-        val predTrigger = App(s1a.predicateData(predicate).triggerFunction,
+        val predTrigger = App(s1a.predicateData(predicate.name).triggerFunction,
           snap.get.convert(terms.sorts.Snap) +: tArgs)
         val eArgsString = eArgs.mkString(", ")
         v1.decider.assume(predTrigger, Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eArgsString))")))
@@ -88,7 +87,7 @@ object predicateSupporter extends PredicateSupportRules {
                         permissionScalingFactor = s.permissionScalingFactor,
                         permissionScalingFactorExp = s.permissionScalingFactorExp).setConstrainable(constrainableWildcards, false)
 
-      v1.heapSupporter.produceSingle(s2, predicate, tArgs, eArgs, snap.get.convert(s2.predicateSnapMap(predicate)), None, tPerm, ePerm, pve, true, v1)((s3, v3) => {
+      v1.heapSupporter.produceSingle(s2, predicate, tArgs, eArgs, snap.get.convert(s2.predicateSnapMap(predicate.name)), None, tPerm, ePerm, pve, true, v1)((s3, v3) => {
         val s4 = v3.heapSupporter.triggerResourceIfNeeded(s3, pa, tArgs, eArgs, v3)
         Q(s4, v3)
       })
@@ -119,7 +118,7 @@ object predicateSupporter extends PredicateSupportRules {
                 v.decider.assumeDefinition(smValueDef, None)
                 val codQvars = bc.resourceID match {
                   case FieldID => Seq(`?r`)
-                  case _ => s.predicateFormalVarMap(resource.asInstanceOf[ast.Predicate])
+                  case _ => s.predicateFormalVarMap(resource.asInstanceOf[ast.Predicate].name)
                 }
                 newFr = newFr.recordFvfAndDomain(SnapshotMapDefinition(resource, sm, Seq(smValueDef), Seq()))
                 quantifiedChunkSupporter.createSingletonQuantifiedChunk(codQvars, None, resource, bc.args, None, bc.perm, None, sm, s.program)
@@ -202,13 +201,13 @@ object predicateSupporter extends PredicateSupportRules {
     v.heapSupporter.consumeSingle(s1, s1.h, pa, tArgs, eArgs, tPerm, ePerm, true, pve, v)((s2, h2, snap, v1) => {
       val s3 = s2.copy(g = gIns, h = h2)
         .setConstrainable(constrainableWildcards, false)
-      if (s3.predicateData(predicate).predContents.isDefined) {
-        val toReplace: silicon.Map[Term, Term] = silicon.Map.from(s3.predicateData(predicate).params.get.zip(Seq(snap.get) ++ tArgs))
-        producePredicateContents(s3, s3.predicateData(predicate).predContents.get, toReplace, v1, false)((s4, v4) => {
+      if (s3.predicateData(predicate.name).predContents.isDefined) {
+        val toReplace: silicon.Map[Term, Term] = silicon.Map.from(s3.predicateData(predicate.name).params.get.zip(Seq(snap.get) ++ tArgs))
+        producePredicateContents(s3, s3.predicateData(predicate.name).predContents.get, toReplace, v1, false)((s4, v4) => {
           v4.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold)
           if (!Verifier.config.disableFunctionUnfoldTrigger()) {
             val predicateTrigger =
-              App(s4.predicateData(predicate).triggerFunction,
+              App(s4.predicateData(predicate.name).triggerFunction,
                 snap.get.convert(terms.sorts.Snap) +: tArgs)
             val eargs = eArgs.mkString(", ")
             v4.decider.assume(predicateTrigger, Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eargs))")))
@@ -223,7 +222,7 @@ object predicateSupporter extends PredicateSupportRules {
           v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold)
           if (!Verifier.config.disableFunctionUnfoldTrigger()) {
             val predicateTrigger =
-              App(s4.predicateData(predicate).triggerFunction,
+              App(s4.predicateData(predicate.name).triggerFunction,
                 snap.get.convert(terms.sorts.Snap) +: tArgs)
             val eargs = eArgs.mkString(", ")
             v2.decider.assume(predicateTrigger, Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eargs))")))

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -983,7 +983,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
               val codomainVars =
                 resource match {
                   case _: ast.Field => Seq(`?r`)
-                  case p: ast.Predicate => s.predicateFormalVarMap(p)
+                  case p: ast.Predicate => s.predicateFormalVarMap(p.name)
                   case w: ast.MagicWand =>
                     val bodyVars = w.subexpressionsToEvaluate(s.program)
                     bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))
@@ -1741,7 +1741,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
           sorts.FieldValueFunction(v.symbolConverter.toSort(field.typ), field.name)
         case predicate: ast.Predicate =>
           // TODO: Reconsider use of and general design behind s.predicateSnapMap
-          sorts.PredicateSnapFunction(s.predicateSnapMap(predicate), predicate.name)
+          sorts.PredicateSnapFunction(s.predicateSnapMap(predicate.name), predicate.name)
         case w: ast.MagicWand =>
           sorts.PredicateSnapFunction(sorts.Snap, MagicWandIdentifier(w, s.program).toString)
         case _ =>

src/main/scala/rules/StateConsolidator.scala

@@ -19,7 +19,6 @@ import viper.silicon.state.terms.predef.`?r`
 import viper.silicon.supporters.functions.FunctionRecorder
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
-import viper.silver.parser.PUnknown
 
 import scala.annotation.unused
 

src/main/scala/state/State.scala

@@ -30,8 +30,8 @@ final case class State(g: Store = Store(),
                        h: Heap = Heap(),
                        program: ast.Program,
                        currentMember: Option[ast.Member],
-                       predicateData: Map[ast.Predicate, PredicateData],
-                       functionData: Map[ast.Function, FunctionData],
+                       predicateData: Map[String, PredicateData],
+                       functionData: Map[String, FunctionData],
                        oldHeaps: OldHeaps = Map.empty,
 
                        parallelizeBranches: Boolean = false,
@@ -76,8 +76,8 @@ final case class State(g: Store = Store(),
                        pmCache: PmCache = Map.empty,
                        smDomainNeeded: Boolean = false,
                        /* TODO: Isn't this data stable, i.e. fully known after a preprocessing step? If so, move it to the appropriate supporter. */
-                       predicateSnapMap: Map[ast.Predicate, terms.Sort] = Map.empty,
-                       predicateFormalVarMap: Map[ast.Predicate, Seq[terms.Var]] = Map.empty,
+                       predicateSnapMap: Map[String, terms.Sort] = Map.empty,
+                       predicateFormalVarMap: Map[String, Seq[terms.Var]] = Map.empty,
                        retryLevel: Int = 0,
                        /* ast.Field, ast.Predicate, or MagicWandIdentifier */
                        heapDependentTriggers: InsertionOrderedSet[Any] = InsertionOrderedSet.empty,
@@ -109,7 +109,7 @@ final case class State(g: Store = Store(),
   def getFormalArgVars(res: ast.Resource, v: Verifier): Seq[Var] = {
     res match {
       case _: ast.Field => Seq(`?r`)
-      case p: ast.Predicate => predicateFormalVarMap(p)
+      case p: ast.Predicate => predicateFormalVarMap(p.name)
       case w: ast.MagicWand =>
         val bodyVars = w.subexpressionsToEvaluate(program)
         bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))

src/main/scala/supporters/MethodSupporter.scala

@@ -14,12 +14,11 @@ import viper.silicon.interfaces._
 import viper.silicon.decider.Decider
 import viper.silicon.logger.records.data.WellformednessCheckRecord
 import viper.silicon.rules.{consumer, executionFlowController, executor, producer}
-import viper.silicon.state.{Heap, State, Store}
+import viper.silicon.state.{State, Store}
 import viper.silicon.state.State.OldHeaps
 import viper.silicon.verifier.{Verifier, VerifierComponent}
 import viper.silicon.utils.freshSnap
-import viper.silver.reporter.AnnotationWarning
-import viper.silicon.{Map, toMap}
+import viper.silicon.Map
 
 /* TODO: Consider changing the DefaultMethodVerificationUnitProvider into a SymbolicExecutionRule */
 
@@ -109,9 +108,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif
 
     def start(): Unit = {}
 
-    def reset(): Unit = {
-      _units = Seq.empty
-    }
+    def reset(): Unit = {}
 
     def stop(): Unit = {}
   }

src/main/scala/supporters/PredicateVerificationUnit.scala

@@ -8,7 +8,6 @@ package viper.silicon.supporters
 
 import com.typesafe.scalalogging.Logger
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
-import viper.silicon.debugger.DebugExp
 import viper.silver.ast
 import viper.silver.ast.Program
 import viper.silver.components.StatefulComponent
@@ -25,7 +24,7 @@ import viper.silicon.supporters.functions.{ActualFunctionRecorder, FunctionRecor
 import viper.silicon.verifier.{Verifier, VerifierComponent}
 import viper.silicon.utils.{freshSnap, toSf}
 
-class PredicateData(predicate: ast.Predicate)
+class PredicateData(val predicate: ast.Predicate)
                    /* Note: Holding a reference to a fixed symbol converter (instead of going
                     *       through a verifier) is only safe if the converter is effectively
                     *       independent of the verifiers.
@@ -51,7 +50,7 @@ case class PredicateLeafNode(heap: Heap, assumptions: InsertionOrderedSet[Term])
 trait PredicateVerificationUnit
     extends VerifyingPreambleContributor[Sort, Decl, Term, ast.Predicate] {
 
-  def data: Map[ast.Predicate, PredicateData]
+  def data: Map[String, PredicateData]
 }
 
 trait DefaultPredicateVerificationUnitProvider extends VerifierComponent { v: Verifier =>
@@ -62,16 +61,15 @@ trait DefaultPredicateVerificationUnitProvider extends VerifierComponent { v: Ve
   object predicateSupporter extends PredicateVerificationUnit with StatefulComponent {
     import viper.silicon.rules.producer._
 
-    /*private*/ var predicateData: Map[ast.Predicate, PredicateData] = Map.empty
+    /*private*/ var predicateData: Map[String, PredicateData] = Map.empty
 
     def data = predicateData
-    def units = predicateData.keys.toSeq
-
+    def units = predicateData.values.map(_.predicate).toSeq
     /* Preamble contribution */
 
     def analyze(program: Program): Unit = {
       this.predicateData = toMap(
-        program.predicates map (pred => pred -> new PredicateData(pred)(symbolConverter)))
+        program.predicates map (pred => pred.name -> new PredicateData(pred)(symbolConverter)))
     }
 
     /* Predicate supporter generates no sorts */
@@ -141,9 +139,9 @@ trait DefaultPredicateVerificationUnitProvider extends VerifierComponent { v: Ve
       val overallResult = if (predicate.body.isDefined && !result.isFatal && Verifier.config.enableSimplifiedUnfolds())
         Some(makePredTree(branchResults)) else None
 
-      this.predicateData(predicate).predContents = overallResult
-      this.predicateData(predicate).params = Some(Seq(snap) ++ argVars.map(_._2._1))
-      this.predicateData(predicate).addRecorders(Seq(funcRecorder))
+      this.predicateData(predicate.name).predContents = overallResult
+      this.predicateData(predicate.name).params = Some(Seq(snap) ++ argVars.map(_._2._1))
+      this.predicateData(predicate.name).addRecorders(Seq(funcRecorder))
 
       symbExLog.closeMemberScope()
       Seq(result)

src/main/scala/supporters/SnapshotSupporter.scala

@@ -36,7 +36,7 @@ class DefaultSnapshotSupporter(symbolConverter: SymbolConverter) extends Snapsho
 
   def optimalSnapshotSort(r: Resource, s: State, v: Verifier): Sort = r match {
     case f: ast.Field => v.symbolConverter.toSort(f.typ)
-    case p: ast.Predicate if s.predicateSnapMap.contains(p) => s.predicateSnapMap(p)
+    case p: ast.Predicate if s.predicateSnapMap.contains(p.name) => s.predicateSnapMap(p.name)
     case p: ast.Predicate =>
       p.body.map(v.snapshotSupporter.optimalSnapshotSort(_, s.program)._1)
         .getOrElse(sorts.Snap)

src/main/scala/supporters/functions/FunctionData.scala

@@ -234,7 +234,7 @@ class FunctionData(val programFunction: ast.Function,
    * Properties resulting from phase 2 (verification)
    */
 
-  lazy val predicateTriggers: Map[ast.Predicate, App] = {
+  lazy val predicateTriggers: Map[String, App] = {
     val recursiveCallsAndUnfoldings: Seq[(ast.FuncApp, Seq[ast.Unfolding])] =
       Functions.recursiveCallsAndSurroundingUnfoldings(programFunction)
 
@@ -271,7 +271,7 @@ class FunctionData(val programFunction: ast.Function,
 
       val fapp = App(triggerFunction, args)
 
-      predicate -> fapp
+      predicate.name -> fapp
     }))
   }