initial attempt to support upper bounds for predicates

silver

@@ -0,0 +1 @@
+../silver

src/main/scala/resources/NonQuantifiedPropertyInterpreter.scala

@@ -9,12 +9,12 @@ package viper.silicon.resources
 import viper.silicon.Map
 import viper.silicon.interfaces.state._
 import viper.silicon.state.terms.Term
-import viper.silicon.state.{QuantifiedBasicChunk, terms}
+import viper.silicon.state.{QuantifiedBasicChunk, State, terms}
 import viper.silicon.utils.ast.{BigAnd, replaceVarsInExp}
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
 
-class NonQuantifiedPropertyInterpreter(heap: Iterable[Chunk], verifier: Verifier) extends PropertyInterpreter {
+class NonQuantifiedPropertyInterpreter(heap: Iterable[Chunk], verifier: Verifier, state: State) extends PropertyInterpreter {
 
   protected case class Info(pm: Map[ChunkPlaceholder, GeneralChunk], resourceID: ResourceID) {
     def addMapping(cp: ChunkPlaceholder, ch: GeneralChunk) = Info(pm + (cp -> ch), resourceID)
@@ -114,6 +114,36 @@ class NonQuantifiedPropertyInterpreter(heap: Iterable[Chunk], verifier: Verifier
     }
   }
 
+  protected def buildPrHasUpperBound(chunkPlaceholder: ChunkPlaceholder, info: Info) = {
+    val chunk = info.pm(chunkPlaceholder)
+    val pred = state.program.findPredicate(chunk.id.toString)
+    if (state.predicateData(pred).upperBoundTerm.isDefined)
+      buildPathCondition(True(), info)
+    else
+      buildPathCondition(False(), info)
+  }
+
+  protected def buildUpperBoundAccess(chunkPlaceholder: ChunkPlaceholder, info: Info) = {
+    val chunk = info.pm(chunkPlaceholder)
+    val pred = state.program.findPredicate(chunk.id.toString)
+    val ubData = (state.predicateData(pred).upperBoundTerm, state.predicateData(pred).upperBoundExp)
+    require(ubData._1.isDefined)
+    chunk match {
+      case _: NonQuantifiedChunk =>
+        if(withExp)
+          (ubData._1.get, ubData._2)
+        else
+          (ubData._1.get, None)
+      // TODO: remove once singleton quantified chunks are not used anymore
+      case c: QuantifiedBasicChunk =>
+        val permTerm = ubData._1.get.replace(c.quantifiedVars, c.singletonArguments.get)
+        if (withExp)
+          (permTerm, Some(replaceVarsInExp(ubData._2.get, c.quantifiedVarExps.get.map(_.name), c.singletonArgumentExps.get)))
+        else
+          (permTerm, None)
+    }
+  }
+
   override protected def buildCheck[K <: IteUsableKind]
                                    (condition: PropertyExpression[kinds.Boolean],
                                     thenDo: PropertyExpression[K],

src/main/scala/resources/PropertyExpressions.scala

@@ -90,5 +90,7 @@ case class This() extends ChunkPlaceholder {
 case class ArgumentAccess(chunk: ChunkPlaceholder) extends PropertyExpression[kinds.Argument]
 case class PermissionAccess(chunk: ChunkPlaceholder) extends PropertyExpression[kinds.Permission]
 case class ValueAccess(chunk: ChunkPlaceholder) extends PropertyExpression[kinds.Value]
+case class UpperBoundAccess(chunk: ChunkPlaceholder) extends PropertyExpression[kinds.Permission]
+case class PrHasUpperBound(chunk: ChunkPlaceholder) extends PropertyExpression[kinds.Boolean]
 
 case class Null() extends PropertyExpression[kinds.Argument]

src/main/scala/resources/PropertyInterpreter.scala

@@ -56,6 +56,8 @@ abstract class PropertyInterpreter {
       // Chunk accessors
       case PermissionAccess(cv) => buildPermissionAccess(cv, info)
       case ValueAccess(cv) => buildValueAccess(cv, info)
+      case PrHasUpperBound(cv) => buildPrHasUpperBound(cv, info)
+      case UpperBoundAccess(cv) => buildUpperBoundAccess(cv, info)
 
       // decider / heap interaction
       case Check(condition, thenDo, otherwise) => buildCheck(condition, thenDo, otherwise, info)
@@ -72,6 +74,8 @@ abstract class PropertyInterpreter {
 
   protected def buildPermissionAccess(chunkVariable: ChunkPlaceholder, info: Info): (Term, Option[ast.Exp])
   protected def buildValueAccess(chunkVariable: ChunkPlaceholder, info: Info): (Term, Option[ast.Exp])
+  protected def buildUpperBoundAccess(chunkVariable: ChunkPlaceholder, info: Info): (Term, Option[ast.Exp])
+  protected def buildPrHasUpperBound(chunkVariable: ChunkPlaceholder, info: Info): (Term, Option[ast.Exp])
 
   /* Assures that if the left-hand side is known to be false without a prover check,
    the right-hand side is not evaluated. */

src/main/scala/resources/QuantifiedPropertyInterpreter.scala

@@ -55,6 +55,12 @@ class QuantifiedPropertyInterpreter extends PropertyInterpreter {
     (info.args, info.argsExp)
   }
 
+  override protected def buildUpperBoundAccess(chunkPlaceholder: ChunkPlaceholder, info: Info) = {
+    sys.error("UpperBoundAccess clauses are not supported in quantified properties.")
+  }
+  override protected def buildPrHasUpperBound(chunkPlaceholder: ChunkPlaceholder, info: Info) = buildPathCondition(False(), info)
+
+
   override protected def buildCheck[K <: IteUsableKind]
                                    (condition: PropertyExpression[kinds.Boolean],
                                     thenDo: PropertyExpression[K],

src/main/scala/resources/ResourceDescriptions.scala

@@ -43,7 +43,32 @@ abstract class BasicDescription extends ResourceDescription {
 }
 
 class PredicateDescription extends BasicDescription {
+  override val instanceProperties = Seq(permAtLeastZero, permAtMostN)
+  override val delayedProperties = Seq(permUpperBoundDiseq, valNeqImpliesLocNeq)
   override def toString = "Predicate"
+
+  def permAtMostN: Property = {
+    val description = "Predicate permissions are at most n"
+    val name = "permAtMostN"
+    val cond = PrHasUpperBound(This())
+    val thenDo = And(cond, LessThanEquals(PermissionAccess(This()), UpperBoundAccess(This())))
+    Property(Or(Not(cond), thenDo), name, description)
+  }
+
+  def permUpperBoundDiseq: Property = {
+    val description = "Permission sum greater than n implies non-equal receivers"
+    val name = "permUpperBoundDiseq"
+    val c1 = ChunkVariable("c1")
+    val c2 = ChunkVariable("c2")
+    val perm1 = PermissionAccess(c1)
+    val perm2 = PermissionAccess(c2)
+    val greaterThan = GreaterThan(Plus(perm1, perm2), UpperBoundAccess(c1))
+    val neq = Not(Equals(ArgumentAccess(c1), ArgumentAccess(c2)))
+    val cond = PrHasUpperBound(c1)
+    val thenDo = And(cond, Check(greaterThan, neq, True()))
+    Property(ForEach(Seq(c1, c2), Or(Not(cond), thenDo)), name, description)
+  }
+
 }
 
 class FieldDescription extends BasicDescription {

src/main/scala/rules/ChunkSupporter.scala

@@ -9,7 +9,8 @@ package viper.silicon.rules
 import viper.silicon.debugger.DebugExp
 import viper.silicon.interfaces.state._
 import viper.silicon.interfaces.{Success, VerificationResult}
-import viper.silicon.resources.{NonQuantifiedPropertyInterpreter, Resources}
+import viper.silicon.resources.{NonQuantifiedPropertyInterpreter, PredicateID, Resources}
+import viper.silicon.Map
 import viper.silicon.state._
 import viper.silicon.state.terms._
 import viper.silicon.state.terms.perms.IsPositive
@@ -152,8 +153,8 @@ object chunkSupporter extends ChunkSupportRules {
 
     val consumeExact = terms.utils.consumeExactRead(perms, s.constrainableARPs)
 
-    def assumeProperties(chunk: NonQuantifiedChunk, heap: Heap): Unit = {
-      val interpreter = new NonQuantifiedPropertyInterpreter(heap.values, v)
+    def assumeProperties(chunk: NonQuantifiedChunk, heap: Heap, s: State): Unit = {
+      val interpreter = new NonQuantifiedPropertyInterpreter(heap.values, v, s)
       val resource = Resources.resourceDescriptions(chunk.resourceID)
       val pathCond = interpreter.buildPathConditionsForChunk(chunk, resource.instanceProperties)
       pathCond.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2))))
@@ -170,7 +171,7 @@ object chunkSupporter extends ChunkSupportRules {
           var newHeap = h - ch
           if (!v.decider.check(newChunk.perm === NoPerm, Verifier.config.checkTimeout())) {
             newHeap = newHeap + newChunk
-            assumeProperties(newChunk, newHeap)
+            assumeProperties(newChunk, newHeap, s)
           }
           val remainingExp = permsExp.map(pe => ast.PermSub(pe, toTakeExp.get)(pe.pos, pe.info, pe.errT))
           (ConsumptionResult(PermMinus(perms, toTake), remainingExp, Seq(), v, 0), s, newHeap, takenChunk)
@@ -182,7 +183,7 @@ object chunkSupporter extends ChunkSupportRules {
             val newChunk = ch.withPerm(PermMinus(ch.perm, perms), newPermExp)
             val takenChunk = ch.withPerm(perms, permsExp)
             val newHeap = h - ch + newChunk
-            assumeProperties(newChunk, newHeap)
+            assumeProperties(newChunk, newHeap, s)
             (Complete(), s, newHeap, Some(takenChunk))
           } else {
             (Incomplete(perms, permsExp), s, h, None)

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -333,7 +333,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         val allChunks = otherChunks ++ newChunks
         // TODO: Since no permissions were gained, I don't see why the PropertyInterpreter would yield any new assumptions.
         //       See if it can be removed here.
-        val interpreter = new NonQuantifiedPropertyInterpreter(allChunks, v)
+        val interpreter = new NonQuantifiedPropertyInterpreter(allChunks, v, s)
         newChunks foreach { ch =>
           val resource = Resources.resourceDescriptions(ch.resourceID)
           val pathCond = interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties)

src/main/scala/rules/Producer.scala

@@ -354,7 +354,19 @@ object producer extends ProductionRules {
                 val formalArgs = s2.predicateFormalVarMap(predicate)
                 val trigger = (sm: Term) => PredicateTrigger(predicate.name, sm, tArgs)
                 quantifiedChunkSupporter.produceSingleLocation(
-                  s2, predicate, formalArgs, Option.when(withExp)(predicate.formalArgs), tArgs, eArgsNew, snap, gain, gainExp, trigger, v2)(Q)
+                  s2, predicate, formalArgs, Option.when(withExp)(predicate.formalArgs), tArgs, eArgsNew, snap, gain, gainExp, trigger, v2)((s3, v3) => {
+                val predData = s3.predicateData(predicate)
+                (predData.upperBoundExp, predData.upperBoundTerm) match {
+                  case (Some(ub), None) => eval(s3, ub, pve, v3)((s4a, tUb, eUbNew, v4a) => {
+                    permissionSupporter.assertNotNegative(s4a, tUb, ub, eUbNew, pve, v4a)((s5, v5) => {
+                      val tmp = s5.predicateData(predicate)
+                      tmp.upperBoundTerm = Some(tUb)
+                      Q(s5.copy(predicateData = s5.predicateData + (predicate -> tmp)), v5)
+                    })
+                  })
+                  case (_, _) => Q(s3, v3)
+                }
+                })
               } else {
                 val snap1 = snap.convert(sorts.Snap)
                 val ch = BasicChunk(PredicateID, BasicChunkIdentifier(predicate.name), tArgs, eArgsNew, snap1, gain, gainExp)
@@ -365,7 +377,18 @@ object producer extends ProductionRules {
                     val debugExp = Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($argsString))", isInternal_ = true))
                     v3.decider.assume(App(s3.predicateData(predicate).triggerFunction, snap1 +: tArgs), debugExp)
                   }
-                  Q(s3.copy(h = h3), v3)})
+                  val predData = s3.predicateData(predicate)
+                  (predData.upperBoundExp, predData.upperBoundTerm) match {
+                    case (Some(ub), None) => eval(s3.copy(h = h3), ub, pve, v3)((s4a, tUb, eUbNew, v4a) => {
+                      permissionSupporter.assertNotNegative(s4a, tUb, ub, eUbNew, pve, v4a)((s5, v5) => {
+                        val tmp = s5.predicateData(predicate)
+                        tmp.upperBoundTerm = Some(tUb)
+                        Q(s5.copy(predicateData = s5.predicateData + (predicate -> tmp)), v5)
+                      })
+                    })
+                    case (_, _) => Q(s3.copy(h = h3), v3)
+                  }
+                })
               }})))
 
       case wand: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(wand, s.program)) =>
@@ -488,7 +511,19 @@ object producer extends ProductionRules {
               NegativePermission(acc.perm),
               QPAssertionNotInjective(acc.loc),
               v1
-            )(Q)
+            )((s2, v2) => {
+              val predData = s2.predicateData(predicate)
+              (predData.upperBoundExp, predData.upperBoundTerm) match {
+                case (Some(ub), None) => eval(s2, ub, pve, v2)((s4a, tUb, eUbNew, v4a) => {
+                  permissionSupporter.assertNotNegative(s4a, tUb, ub, eUbNew, pve, v4a)((s5, v5) => {
+                    val tmp = s5.predicateData(predicate)
+                    tmp.upperBoundTerm = Some(tUb)
+                    Q(s5.copy(predicateData = s5.predicateData + (predicate -> tmp)), v5)
+                  })
+                })
+                case (_, _) => Q(s2, v2)
+              }
+            })
           case (s1, _, _, _, _, None, v1) => Q(s1, v1)
         }
 

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -1102,7 +1102,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalQVars, formalQVarsExp, resource, tArgs, eArgs, tPerm, ePerm, sm, s.program)
     val (fr1, h1) = v.stateConsolidator(s).merge(s.functionRecorder, s, s.h, Heap(Seq(ch)), v)
 
-    val interpreter = new NonQuantifiedPropertyInterpreter(h1.values, v)
+    val interpreter = new NonQuantifiedPropertyInterpreter(h1.values, v, s)
     val resourceDescription = Resources.resourceDescriptions(ch.resourceID)
     val pcs = interpreter.buildPathConditionsForChunk(ch, resourceDescription.instanceProperties)
     pcs.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2))))