Simplify wildcard multiplication

src/main/scala/Config.scala

@@ -683,6 +683,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
       ExhaleMode.Greedy
   }
 
+  val unsafeWildcardOptimization: ScallopOption[Boolean] = opt[Boolean]("unsafeWildcardOptimization",
+    descr = "Simplify wildcard terms in a way that is very very rarely unsafe. See Silicon PR #756 for details.",
+    default = Some(false),
+    noshort = true
+  )
+
   val numberOfErrorsToReport: ScallopOption[Int] = opt[Int]("numberOfErrorsToReport",
     descr = "Number of errors per member before the verifier stops. If this number is set to 0, all errors are reported.",
     default = Some(1),

src/main/scala/decider/Decider.scala

@@ -337,17 +337,17 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     /* Fresh symbols */
 
     def fresh(id: String, argSorts: Seq[Sort], resultSort: Sort): Function =
-      prover_fresh[Fun](id, argSorts, resultSort)
+      prover_fresh[Fun](id, argSorts, resultSort, false)
 
-    def fresh(id: String, sort: Sort): Var = prover_fresh[Var](id, Nil, sort)
+    def fresh(id: String, sort: Sort): Var = prover_fresh[Var](id, Nil, sort, false)
 
-    def fresh(s: Sort): Var = prover_fresh[Var]("$t", Nil, s)
+    def fresh(s: Sort): Var = prover_fresh[Var]("$t", Nil, s, false)
 
     def fresh(v: ast.AbstractLocalVar): Var =
-      prover_fresh[Var](v.name, Nil, symbolConverter.toSort(v.typ))
+      prover_fresh[Var](v.name, Nil, symbolConverter.toSort(v.typ), false)
 
     def freshARP(id: String = "$k"): (Var, Term) = {
-      val permVar = prover_fresh[Var](id, Nil, sorts.Perm)
+      val permVar = prover_fresh[Var](id, Nil, sorts.Perm, true)
       val permVarConstraints = IsReadPermVar(permVar)
 
       (permVar, permVarConstraints)
@@ -373,7 +373,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     }
 
     private def prover_fresh[F <: Function : ClassTag]
-                            (id: String, argSorts: Seq[Sort], resultSort: Sort)
+                            (id: String, argSorts: Seq[Sort], resultSort: Sort, isARP: Boolean)
                             : F = {
 //      context.bookkeeper.freshSymbols += 1
 
@@ -388,7 +388,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
           destClass match {
             case c if c == classOf[Var] =>
               Predef.assert(proverFun.argSorts.isEmpty)
-              Var(proverFun.id, proverFun.resultSort).asInstanceOf[F]
+              Var(proverFun.id, proverFun.resultSort, isARP).asInstanceOf[F]
             case c if c == classOf[Fun] => proverFun.asInstanceOf[F]
             case c if c == classOf[DomainFun] =>
               DomainFun(proverFun.id, proverFun.argSorts, proverFun.resultSort).asInstanceOf[F]

src/main/scala/logger/writer/TermWriter.scala

@@ -6,7 +6,7 @@
 
 package viper.silicon.logger.writer
 
-import spray.json.{JsArray, JsNull, JsObject, JsString, JsValue}
+import spray.json.{JsArray, JsBoolean, JsNull, JsObject, JsString, JsValue}
 import viper.silicon.state.Identifier
 import viper.silicon.state.terms._
 
@@ -30,11 +30,12 @@ object TermWriter {
       "p" -> p
     )
 
-  private def variable(id: Identifier, sort: Sort) =
+  private def variable(id: Identifier, sort: Sort, isWildcard: Boolean) =
     JsObject(
       "type" -> JsString("variable"),
       "id" -> JsString(id.name),
-      "sort" -> toJSON(sort)
+      "sort" -> toJSON(sort),
+      "isWildcard" -> JsBoolean(isWildcard)
     )
 
   def toJSON(sort: Sort): JsValue = {
@@ -112,7 +113,7 @@ object TermWriter {
         "elseBranch" -> toJSON(elseBranch)
       )
 
-    case Var(id, sort) => variable(id, sort)
+    case Var(id, sort, arp) => variable(id, sort, arp)
     case SortWrapper(t, sort) =>
       JsObject(
         "type" -> JsString("sortWrapper"),

src/main/scala/reporting/Converter.scala

@@ -255,7 +255,7 @@ object Converter {
       case IntLiteral(x)     => LitIntEntry(x)
       case t: BooleanLiteral => LitBoolEntry(t.value)
       case Null              => VarEntry(model.entries(nullRefId).toString, sorts.Ref)
-      case Var(_, sort) =>
+      case Var(_, sort, _) =>
         val key: String = term.toString
         val entry: Option[ModelEntry] = model.entries.get(key)
         entry

src/main/scala/rules/Consumer.scala

@@ -294,7 +294,7 @@ object consumer extends ConsumptionRules {
 
       case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) =>
         val bodyVars = wand.subexpressionsToEvaluate(s.program)
-        val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ)))
+        val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))
         val qid = MagicWandIdentifier(wand, s.program).toString
         val optTrigger =
           if (forall.triggers.isEmpty) None
@@ -341,7 +341,10 @@ object consumer extends ConsumptionRules {
             } else {
               s2
             }
-            val loss = PermTimes(tPerm, s2.permissionScalingFactor)
+            val loss = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(field))
+              PermTimes(tPerm, s2.permissionScalingFactor)
+            else
+              WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor)
             quantifiedChunkSupporter.consumeSingleLocation(
               s2p,
               h,
@@ -377,7 +380,10 @@ object consumer extends ConsumptionRules {
               s2
             }
 
-            val loss = PermTimes(tPerm, s2.permissionScalingFactor)
+            val loss = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(loc.loc(s2.program)))
+              PermTimes(tPerm, s2.permissionScalingFactor)
+            else
+              WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor)
             quantifiedChunkSupporter.consumeSingleLocation(
               s2p,
               h,
@@ -403,7 +409,10 @@ object consumer extends ConsumptionRules {
           evalLocationAccess(s1, locacc, pve, v1)((s2, _, tArgs, v2) =>
             permissionSupporter.assertNotNegative(s2, tPerm, perm, pve, v2)((s3, v3) => {
               val resource = locacc.res(s.program)
-              val loss = PermTimes(tPerm, s3.permissionScalingFactor)
+              val loss = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(locacc.loc(s2.program)))
+                PermTimes(tPerm, s2.permissionScalingFactor)
+              else
+                WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor)
               val ve = pve dueTo InsufficientPermission(locacc)
               val description = s"consume ${a.pos}: $a"
               chunkSupporter.consume(s3, h, resource, tArgs, loss, ve, v3, description)((s4, h1, snap1, v4) => {
@@ -417,7 +426,7 @@ object consumer extends ConsumptionRules {
       /* Handle wands */
       case wand: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(wand, s.program)) =>
         val bodyVars = wand.subexpressionsToEvaluate(s.program)
-        val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ)))
+        val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))
 
         evals(s, bodyVars, _ => pve, v)((s1, tArgs, v1) => {
           val s1p = if (s1.heapDependentTriggers.contains(MagicWandIdentifier(wand, s.program))){
@@ -431,7 +440,7 @@ object consumer extends ConsumptionRules {
           } else {
             s1
           }
-          val loss = PermTimes(FullPerm, s1.permissionScalingFactor)
+          val loss = s1.permissionScalingFactor
           quantifiedChunkSupporter.consumeSingleLocation(
             s1p,
             h,

src/main/scala/rules/Evaluator.scala

@@ -465,7 +465,7 @@ object evaluator extends EvaluationRules {
                   val (relevantChunks, _) =
                     quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](h, identifier)
                   val bodyVars = wand.subexpressionsToEvaluate(s.program)
-                  val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v1.symbolConverter.toSort(bodyVars(i).typ)))
+                  val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v1.symbolConverter.toSort(bodyVars(i).typ), false))
                   val (s2, pmDef) = if (s1.heapDependentTriggers.contains(MagicWandIdentifier(wand, s1.program))) {
                     val (s2, smDef, pmDef) = quantifiedChunkSupporter.heapSummarisingMaps(s1, wand, formalVars, relevantChunks, v1)
                     v1.decider.assume(PredicateTrigger(identifier.toString, smDef.sm, args))
@@ -1581,7 +1581,7 @@ object evaluator extends EvaluationRules {
     var mostRecentTrig: PredicateTrigger = null
     val wandHoles = wand.subexpressionsToEvaluate(s.program)
     val codomainQVars =
-      wandHoles.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(wandHoles(i).typ)))
+      wandHoles.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(wandHoles(i).typ), false))
     val (relevantChunks, _) =
       quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](s.h, MagicWandIdentifier(wand, s.program))
     val optSmDomainDefinitionCondition =

src/main/scala/rules/Executor.scala

@@ -624,7 +624,7 @@ object executor extends ExecutionRules {
                 val (relevantChunks, _) =
                   quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](s2.h, ch.id)
                 val bodyVars = wand.subexpressionsToEvaluate(s.program)
-                val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v1.symbolConverter.toSort(bodyVars(i).typ)))
+                val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v1.symbolConverter.toSort(bodyVars(i).typ), false))
                 val (smDef, smCache) =
                   quantifiedChunkSupporter.summarisingSnapshotMap(
                     s2, wand, formalVars, relevantChunks, v1)

src/main/scala/rules/HavocSupporter.scala

@@ -322,7 +322,7 @@ object havocSupporter extends SymbolicExecutionRules {
         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)))
+              Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))
     }
   }
 

src/main/scala/rules/MagicWandSupporter.scala

@@ -283,7 +283,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
       val preMark = v3.decider.setPathConditionMark()
       if (s4.qpMagicWands.contains(MagicWandIdentifier(wand, s.program))) {
         val bodyVars = wand.subexpressionsToEvaluate(s.program)
-        val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ)))
+        val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))
         evals(s4, bodyVars, _ => pve, v3)((s5, args, v4) => {
           val (sm, smValueDef) =
             quantifiedChunkSupporter.singletonSnapshotMap(s5, wand, args, MagicWandSnapshot(freshSnapRoot, snap), v4)

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -58,7 +58,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         case _: ast.MagicWand => sorts.Snap
       }
 
-    val `?s` = Var(Identifier("?s"), sort)
+    val `?s` = Var(Identifier("?s"), sort, false)
     var summarisingSnapshotDefinitions: Seq[Term] = Vector.empty
     var permissionSum: Term = NoPerm
 
@@ -386,7 +386,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
   }
 
 
-  private val freeReceiver = Var(Identifier("?rcvr"), sorts.Ref)
+  private val freeReceiver = Var(Identifier("?rcvr"), sorts.Ref, false)
 
   def assumeFieldPermissionUpperBounds(h: Heap, v: Verifier): Unit = {
     // TODO: Instead of "manually" assuming such upper bounds, appropriate PropertyInterpreters

src/main/scala/rules/Producer.scala

@@ -319,7 +319,10 @@ object producer extends ProductionRules {
           eval(s1, perm, pve, v1)((s2, tPerm, v2) =>
             permissionSupporter.assertNotNegative(s2, tPerm, perm, pve, v2)((s3, v3) => {
               val snap = sf(v3.symbolConverter.toSort(field.typ), v3)
-              val gain = PermTimes(tPerm, s3.permissionScalingFactor)
+              val gain = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(field))
+                PermTimes(tPerm, s3.permissionScalingFactor)
+              else
+                WildcardSimplifyingPermTimes(tPerm, s3.permissionScalingFactor)
               if (s3.qpFields.contains(field)) {
                 val trigger = (sm: Term) => FieldTrigger(field.name, sm, tRcvr)
                 quantifiedChunkSupporter.produceSingleLocation(s3, field, Seq(`?r`), Seq(tRcvr), snap, gain, trigger, v3)(Q)
@@ -337,7 +340,10 @@ object producer extends ProductionRules {
               val snap = sf(
                 predicate.body.map(v2.snapshotSupporter.optimalSnapshotSort(_, s.program)._1)
                               .getOrElse(sorts.Snap), v2)
-              val gain = PermTimes(tPerm, s2.permissionScalingFactor)
+              val gain = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(predicate))
+                PermTimes(tPerm, s2.permissionScalingFactor)
+              else
+                WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor)
               if (s2.qpPredicates.contains(predicate)) {
                 val formalArgs = s2.predicateFormalVarMap(predicate)
                 val trigger = (sm: Term) => PredicateTrigger(predicate.name, sm, tArgs)
@@ -356,7 +362,7 @@ object producer extends ProductionRules {
 
       case wand: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(wand, s.program)) =>
         val bodyVars = wand.subexpressionsToEvaluate(s.program)
-        val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ)))
+        val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))
         evals(s, bodyVars, _ => pve, v)((s1, args,v1) => {
           val (sm, smValueDef) =
             quantifiedChunkSupporter.singletonSnapshotMap(s1, wand, args, sf(sorts.Snap, v1), v1)
@@ -460,7 +466,7 @@ object producer extends ProductionRules {
 
       case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) =>
         val bodyVars = wand.subexpressionsToEvaluate(s.program)
-        val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ)))
+        val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))
         val optTrigger =
           if (forall.triggers.isEmpty) None
           else Some(forall.triggers)

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -794,7 +794,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
              (Q: (State, Verifier) => VerificationResult)
              : VerificationResult = {
 
-    val gain = PermTimes(tPerm, s.permissionScalingFactor)
+    val gain = if (!Verifier.config.unsafeWildcardOptimization() ||
+        (resource.isInstanceOf[ast.Location] && s.permLocations.contains(resource.asInstanceOf[ast.Location])))
+      PermTimes(tPerm, s.permissionScalingFactor)
+    else
+      WildcardSimplifyingPermTimes(tPerm, s.permissionScalingFactor)
     val (ch: QuantifiedBasicChunk, inverseFunctions) =
       quantifiedChunkSupporter.createQuantifiedChunk(
         qvars                = qvars,
@@ -925,7 +929,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                   case p: ast.Predicate => s.predicateFormalVarMap(p)
                   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)))
+                    bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))
                 }
 
               val (relevantChunks, _) =
@@ -1072,7 +1076,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         val hints = quantifiedChunkSupporter.extractHints(Some(tCond), tArgs)
         val chunkOrderHeuristics =
           qpAppChunkOrderHeuristics(inverseFunctions.invertibles, qvars, hints, v)
-        val loss = PermTimes(tPerm, s.permissionScalingFactor)
+        val loss = if (!Verifier.config.unsafeWildcardOptimization() ||
+            (resource.isInstanceOf[ast.Location] && s.permLocations.contains(resource.asInstanceOf[ast.Location])))
+          PermTimes(tPerm, s.permissionScalingFactor)
+        else
+          WildcardSimplifyingPermTimes(tPerm, s.permissionScalingFactor)
         val (relevantChunks, otherChunks) =
           quantifiedChunkSupporter.splitHeap[QuantifiedBasicChunk](
             h, ChunkIdentifier(resource, s.program))