Checking only read permissions when asserting function preconditions

src/main/scala/viper/silver/ast/Expression.scala

@@ -285,16 +285,18 @@ object AccessPredicate {
 }
 
 /** An accessibility predicate for a field location. */
-case class FieldAccessPredicate(loc: FieldAccess, perm: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
+case class FieldAccessPredicate(loc: FieldAccess, permExp: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
+  val perm = permExp.getOrElse(FullPerm()(pos, NoInfo, NoTrafos))
   override lazy val check : Seq[ConsistencyError] =
-    (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq()) ++ Consistency.checkWildcardUsage(perm)
+    (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq())
   val typ: Bool.type = Bool
 }
 
 /** An accessibility predicate for a predicate location. */
-case class PredicateAccessPredicate(loc: PredicateAccess, perm: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
+case class PredicateAccessPredicate(loc: PredicateAccess, permExp: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
+  val perm = permExp.getOrElse(FullPerm()(pos, NoInfo, NoTrafos))
   override lazy val check : Seq[ConsistencyError] =
-    (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq()) ++ Consistency.checkWildcardUsage(perm)
+    (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq())
   val typ: Bool.type = Bool
 }
 
@@ -499,6 +501,11 @@ case class Applying(wand: MagicWand, body: Exp)(val pos: Position = NoPosition,
   lazy val typ = body.typ
 }
 
+case class Asserting(a: Exp, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Exp {
+  override lazy val check: Seq[ConsistencyError] = Consistency.checkPure(body)
+  lazy val typ = body.typ
+}
+
 // --- Old expressions
 
 sealed trait OldExp extends UnExp {

src/main/scala/viper/silver/ast/Program.scala

@@ -361,7 +361,7 @@ case class Field(name: String, typ: Type)(val pos: Position = NoPosition, val in
 /** A predicate declaration. */
 case class Predicate(name: String, formalArgs: Seq[LocalVarDecl], body: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Location {
   override lazy val check : Seq[ConsistencyError] =
-    (if (body.isDefined) Consistency.checkNonPostContract(body.get) else Seq()) ++
+    (if (body.isDefined) Consistency.checkNonPostContract(body.get) ++ Consistency.checkWildcardUsage(body.get, false) else Seq()) ++
     (if (body.isDefined && !Consistency.noOld(body.get))
       Seq(ConsistencyError("Predicates must not contain old expressions.",body.get.pos))
      else Seq()) ++
@@ -426,7 +426,8 @@ case class Method(name: String, formalArgs: Seq[LocalVarDecl], formalReturns: Se
     body.fold(Seq.empty[ConsistencyError])(Consistency.checkNoArgsReassigned(formalArgs, _)) ++
     (if (!((formalArgs ++ formalReturns) forall (_.typ.isConcrete))) Seq(ConsistencyError("Formal args and returns must have concrete types.", pos)) else Seq()) ++
     (pres ++ posts).flatMap(Consistency.checkNoPermForpermExceptInhaleExhale) ++
-    checkReturnsNotUsedInPreconditions
+    checkReturnsNotUsedInPreconditions ++
+    (pres ++ posts ++ body.toSeq).flatMap(Consistency.checkWildcardUsage(_, false))
 
   lazy val checkReturnsNotUsedInPreconditions: Seq[ConsistencyError] = {
     val varsInPreconditions: Seq[LocalVar] = pres flatMap {_.deepCollect {case l: LocalVar => l}}
@@ -454,6 +455,7 @@ case class Function(name: String, formalArgs: Seq[LocalVarDecl], typ: Type, pres
     posts.flatMap(p=>{ if(!Consistency.noOld(p))
       Seq(ConsistencyError("Function post-conditions must not have old expressions.", p.pos)) else Seq()}) ++
     (pres ++ posts).flatMap(Consistency.checkNoPermForpermExceptInhaleExhale) ++
+    (pres ++ posts ++ body.toSeq).flatMap(Consistency.checkWildcardUsage(_, true)) ++
     (if(!(body forall (_ isSubtype typ))) Seq(ConsistencyError("Type of function body must match function type.", pos)) else Seq() ) ++
     (posts flatMap (p => if (!Consistency.noPerm(p) || !Consistency.noForPerm(p)) Seq(ConsistencyError("perm and forperm expressions are not allowed in function postconditions", p.pos)) else Seq() )) ++
     pres.flatMap(Consistency.checkPre) ++
@@ -471,7 +473,8 @@ case class Function(name: String, formalArgs: Seq[LocalVarDecl], typ: Type, pres
         }).execute[Node](pre)
       })
       errors
-    }
+    } ++
+    Consistency.warnAboutFunctionPermissionAmounts(this)
 
   val scopedDecls: Seq[Declaration] = formalArgs
   /**

src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala

@@ -771,6 +771,8 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
         group(parens(text("unfolding") <+> nest(defaultIndent, show(acc)) <+> "in" <> nest(defaultIndent, line <> show(exp))))
       case Applying(wand, exp) =>
         parens(text("applying") <+> nest(defaultIndent, show(wand)) <+> "in" <> nest(defaultIndent, line <> show(exp)))
+      case Asserting(ass, exp) =>
+        parens(text("asserting") <+> nest(defaultIndent, parens(show(ass))) <+> "in" <> nest(defaultIndent, line <> show(exp)))
       case Old(exp) =>
         text("old") <> parens(show(exp))
       case LabelledOld(exp,label) =>

src/main/scala/viper/silver/ast/utility/Consistency.scala

@@ -15,6 +15,10 @@ import viper.silver.{FastMessage, FastMessaging}
 /** An utility object for consistency checking. */
 object Consistency {
   var messages: FastMessaging.Messages = Nil
+
+  // Set to enable legacy mode where permission amounts in function preconditions have their usual meaning instead
+  // of just just being treated as a kind of wildcard.
+  private var respectFunctionPrePermAmounts: Boolean = false
   def recordIfNot(suspect: Positioned, property: Boolean, message: String): Unit = {
     if (!property) {
       val pos = suspect.pos
@@ -23,6 +27,14 @@ object Consistency {
     }
   }
 
+  /** Use this method to enable consistency checks suitable for the legacy mode where permission amounts in function
+    * preconditions have their standard meaning, instead of always meaning a kind of wildcard.
+    * In other words, this should be set iff the command line flag "--respectFunctionPrePermAmounts" is set.
+    * */
+  def setFunctionPreconditionLegacyMode(enableLegacyMode: Boolean) = {
+    respectFunctionPrePermAmounts = enableLegacyMode
+  }
+
   def resetMessages(): Unit = { this.messages = Nil }
   @inline
   def recordIf(suspect: Positioned, property: Boolean, message: String): Unit =
@@ -184,6 +196,28 @@ object Consistency {
     (if(!noResult(e)) Seq(ConsistencyError("Result variables are only allowed in postconditions of functions.", e.pos)) else Seq())
   }
 
+  def warnAboutFunctionPermissionAmounts(f: Function): Seq[ConsistencyError] = {
+    if (respectFunctionPrePermAmounts)
+      return Seq()
+    def hasSpecificPermAmounts(e: Exp): Boolean = e match {
+      case CondExp(_, thn, els) => hasSpecificPermAmounts(thn) || hasSpecificPermAmounts(els)
+      case _: FractionalPerm => true
+      case _: FullPerm => true
+      case _: PermAdd | _: PermSub | _: PermMinus | _: PermMul | _: IntPermMul | _: PermDiv | _: PermPermDiv => true
+      case _ => false
+    }
+    def collectWarnings(e: Exp): Seq[ConsistencyError] = e.collect{
+      case FieldAccessPredicate(_, Some(perm)) if hasSpecificPermAmounts(perm) =>
+        ConsistencyError("Function contains specific permission amount that will be treated like wildcard.", perm.pos, false)
+      case PredicateAccessPredicate(_, Some(perm)) if hasSpecificPermAmounts(perm) =>
+        ConsistencyError("Function contains specific permission amount that will be treated like wildcard.", perm.pos, false)
+    }.toSeq
+
+    val preWarnings = f.pres.flatMap(collectWarnings)
+    val bodyWarnings = f.body.toSeq.flatMap(collectWarnings)
+    preWarnings ++ bodyWarnings
+  }
+
   /** Check all properties required for a contract expression that is not a postcondition (precondition, invariant, predicate) */
   def checkNonPostContract(e: Exp) : Seq[ConsistencyError]  = {
     (if(!(e isSubtype Bool)) Seq(ConsistencyError(s"Contract $e: ${e.typ} must be boolean.", e.pos)) else Seq()) ++
@@ -196,18 +230,28 @@ object Consistency {
     (if(!noLabelledOld(e)) Seq(ConsistencyError("Labelled-old expressions are not allowed in postconditions.", e.pos)) else Seq())
   }
 
-  def checkWildcardUsage(e: Exp): Seq[ConsistencyError] = {
-    val containedWildcards = e.shallowCollect{
-      case w: WildcardPerm => w
-    }
-    if (containedWildcards.nonEmpty) {
-      e match {
-        case _: WildcardPerm => Seq()
-        case _ => Seq(ConsistencyError("Wildcard occurs inside compound expression (should only occur directly in an accessibility predicate).", e.pos))
+  def checkWildcardUsage(n: Node, inFunction: Boolean): Seq[ConsistencyError] = {
+    if (!respectFunctionPrePermAmounts && inFunction)
+      return Seq()
+
+    def checkValidUse(e: Exp): Seq[ConsistencyError] = {
+      val containedWildcards = e.shallowCollect {
+        case w: WildcardPerm => w
+      }
+      if (containedWildcards.nonEmpty) {
+        e match {
+          case _: WildcardPerm => Seq()
+          case _ => Seq(ConsistencyError("Wildcard occurs inside compound expression (should only occur directly in an accessibility predicate).", e.pos))
+        }
+      } else {
+        Seq()
       }
-    } else {
-      Seq()
     }
+
+    n.collect{
+      case FieldAccessPredicate(_, Some(prm)) => checkValidUse(prm)
+      case PredicateAccessPredicate(_, Some(prm)) => checkValidUse(prm)
+    }.flatten.toSeq
   }
 
   /** checks that all quantified variables appear in all triggers */

src/main/scala/viper/silver/ast/utility/Expressions.scala

@@ -25,6 +25,7 @@ object Expressions {
     case CondExp(cnd, thn, els) => isPure(cnd) && isPure(thn) && isPure(els)
     case unf: Unfolding => isPure(unf.body)
     case app: Applying => isPure(app.body)
+    case Asserting(a, e) => isPure(e)
     case QuantifiedExp(_, e0) => isPure(e0)
     case Let(_, _, body) => isPure(body)
     case e: ExtensionExp => e.extensionIsPure
@@ -96,9 +97,10 @@ object Expressions {
   def asBooleanExp(e: Exp): Exp = {
     e.transform({
       case _: AccessPredicate | _: MagicWand => TrueLit()()
-      case fa@Forall(vs,ts,body) => Forall(vs,ts,asBooleanExp(body))(fa.pos,fa.info)
+      case fa@Forall(vs,ts,body) => Forall(vs, ts, asBooleanExp(body))(fa.pos, fa.info, fa.errT)
       case Unfolding(_, exp) => asBooleanExp(exp)
       case Applying(_, exp) => asBooleanExp(exp)
+      case ass@Asserting(a, exp) => Asserting(asBooleanExp(a), asBooleanExp(exp))(ass.pos, ass.info, ass.errT)
     })
   }
 
@@ -191,14 +193,15 @@ object Expressions {
         }
         // Conditions for the current node.
         val conds: Seq[Exp] = n match {
-          case f@FieldAccess(rcv, _) => List(NeCmp(rcv, NullLit()(p))(p), FieldAccessPredicate(f, WildcardPerm()(p))(p))
+          case f@FieldAccess(rcv, _) => List(NeCmp(rcv, NullLit()(p))(p), FieldAccessPredicate(f, Some(WildcardPerm()(p)))(p))
           case f: FuncApp => prog.findFunction(f.funcname).pres
           case Div(_, q) => List(NeCmp(q, IntLit(0)(p))(p))
           case Mod(_, q) => List(NeCmp(q, IntLit(0)(p))(p))
           case SeqIndex(s, idx) => List(GeCmp(idx, IntLit(0)(p))(p), LtCmp(idx, SeqLength(s)(p))(p))
           case MapLookup(m, k) => List(MapContains(k, m)(p))
           case Unfolding(pred, _) => List(pred)
           case Applying(wand, _) => List(wand)
+          case Asserting(a, _) => List(a)
           case _ => Nil
         }
         // Only use non-trivial conditions for the subnodes.

src/main/scala/viper/silver/ast/utility/InverseFunctions.scala

@@ -37,11 +37,11 @@ object InverseFunctions {
             val axiom1 = Forall(qvars, forall.triggers, Implies(cond, equalities)(pos, info, errT))(pos, info, errT)
             var condReplaced = cond
             var rcvReplaced = fap.loc.rcv
-            var permReplaced = fap.perm
+            var permReplaced = fap.permExp
             for (i <- 0 until qvars.length){
               condReplaced = condReplaced.replace(qvars(i).localVar, invsOfR(i))
               rcvReplaced = rcvReplaced.replace(qvars(i).localVar, invsOfR(i))
-              permReplaced = permReplaced.replace(qvars(i).localVar, invsOfR(i))
+              permReplaced = permReplaced.map(_.replace(qvars(i).localVar, invsOfR(i)))
             }
             val axiom2 = Forall(Seq(r), Seq(Trigger(invsOfR)(pos, info, errT)), Implies(condReplaced, EqCmp(rcvReplaced, r.localVar)(pos, info, errT))(pos, info, errT))(pos, info, errT)
             val acc1 = FieldAccessPredicate(FieldAccess(r.localVar, fap.loc.field)(), permReplaced)()
@@ -65,7 +65,7 @@ object InverseFunctions {
             val axiom2 = Forall(formalArgs, Seq(Trigger(invsOfFormalArgs)(pos, info, errT)), Implies(cond.replace((qvars map (_.localVar) zip invsOfFormalArgs).toMap), invArgsConj)(pos, info, errT))(pos, info, errT)
 
             val cond1 = cond.replace((qvars map (_.localVar) zip invsOfFormalArgs).toMap)
-            val acc1 = PredicateAccessPredicate(PredicateAccess(formalArgs map (_.localVar), pred.name)(pos, info, errT), pap.perm.replace((qvars map (_.localVar) zip invsOfFormalArgs).toMap))(pos, info, errT)
+            val acc1 = PredicateAccessPredicate(PredicateAccess(formalArgs map (_.localVar), pred.name)(pos, info, errT), pap.permExp.map(_.replace((qvars map (_.localVar) zip invsOfFormalArgs).toMap)))(pos, info, errT)
             val forall1 = Forall(formalArgs, Seq(Trigger(invsOfFormalArgs)(pos, info, errT)), Implies(cond1, acc1)(pos, info, errT))(pos, info, errT)
 
             val domain = Domain(domName, invs, Seq())(pos, info, errT)

src/main/scala/viper/silver/ast/utility/Nodes.scala

@@ -80,9 +80,10 @@ object Nodes {
           case _: AbstractLocalVar => Nil
           case FieldAccess(rcv, _) => Seq(rcv)
           case PredicateAccess(params, _) => params
-          case PredicateAccessPredicate(pred_acc, perm) => Seq(pred_acc, perm)
+          case PredicateAccessPredicate(pred_acc, perm) => Seq(pred_acc) ++ perm.toSeq
           case Unfolding(acc, body) => Seq(acc, body)
           case Applying(wand, body) => Seq(wand, body)
+          case Asserting(ass, body) => Seq(ass, body)
           case Old(exp) => Seq(exp)
           case CondExp(cond, thn, els) => Seq(cond, thn, els)
           case Let(v, exp, body) => Seq(v, exp, body)

src/main/scala/viper/silver/ast/utility/Permissions.scala

@@ -31,12 +31,21 @@ object Permissions {
            "Internal error: attempted to permission-scale expression " + e.toString +
                " by non-permission-typed expression " + permFactor.toString)
 
-    if(permFactor.isInstanceOf[FullPerm])
+    def multiplyPermOpt(op: Option[Exp]): Option[Exp] = op match {
+      case Some(p) => Some(PermMul(p, permFactor)(p.pos, p.info))
+      case None => Some(permFactor)
+    }
+
+    if (permFactor.isInstanceOf[FullPerm]) {
       e
-    else
-      e.transform({
-        case fa@FieldAccessPredicate(loc,p) => FieldAccessPredicate(loc,PermMul(p,permFactor)(p.pos,p.info))(fa.pos,fa.info)
-        case pa@PredicateAccessPredicate(loc,p) => PredicateAccessPredicate(loc,PermMul(p,permFactor)(p.pos,p.info))(pa.pos,pa.info)
+    } else {
+      e.transform{
+        case fa@FieldAccessPredicate(loc, p) =>
+          FieldAccessPredicate(loc, multiplyPermOpt(p))(fa.pos, fa.info)
+        case pa@PredicateAccessPredicate(loc, p) =>
+          PredicateAccessPredicate(loc, multiplyPermOpt(p))(pa.pos, pa.info)
         case _: MagicWand => sys.error("Cannot yet permission-scale magic wands")
-      })}
+      }
+    }
+  }
 }

src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala

@@ -139,6 +139,13 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     hidden = false
   )
 
+  val respectFunctionPrePermAmounts = opt[Boolean]("respectFunctionPrePermAmounts",
+    descr = "Respects precise permission amounts in function preconditions instead of only checking read access.",
+    default = Some(false),
+    noshort = true,
+    hidden = false
+  )
+
   val submitForEvaluation = opt[Boolean](name = "submitForEvaluation",
     descr = "Whether to allow storing the current program for future evaluation.",
     default = Some(false),

src/main/scala/viper/silver/frontend/SilFrontend.scala

@@ -374,12 +374,18 @@ trait SilFrontend extends DefaultFrontend {
   }
 
   def doConsistencyCheck(input: Program): Result[Program] = {
+    if (config != null) {
+      Consistency.setFunctionPreconditionLegacyMode(config.respectFunctionPrePermAmounts())
+    }
     var errors = input.checkTransitively
     if (backendTypeFormat.isDefined)
       errors = errors ++ Consistency.checkBackendTypes(input, backendTypeFormat.get)
-    if (errors.isEmpty) {
+    val (actualErrors, warnings) = errors partition (_.isError)
+    if (warnings.nonEmpty)
+      reporter.report(ConsistencyWarnings(warnings))
+    if (actualErrors.isEmpty) {
       Succ(input)
     } else
-      Fail(errors)
+      Fail(actualErrors)
   }
 }

src/main/scala/viper/silver/parser/FastParser.scala

@@ -152,7 +152,7 @@ object FastParserCompanion {
     // maps
     PKw.Map, PKwOp.Range, PKwOp.Domain,
     // prover hint expressions
-    PKwOp.Unfolding, PKwOp.In, PKwOp.Applying,
+    PKwOp.Unfolding, PKwOp.In, PKwOp.Applying, PKwOp.Asserting,
     // old expression
     PKwOp.Old, PKw.Lhs,
     // other expressions
@@ -365,7 +365,7 @@ class FastParser {
   def atomReservedKw[$: P]: P[PExp] = {
     reservedKwMany(
       StringIn("true", "false", "null", "old", "result", "acc", "none", "wildcard", "write", "epsilon", "perm", "let", "forall", "exists", "forperm",
-        "unfolding", "applying", "Set", "Seq", "Multiset", "Map", "range", "domain", "new"),
+        "unfolding", "applying", "asserting", "Set", "Seq", "Multiset", "Map", "range", "domain", "new"),
       str => pos => str match {
         case "true" => Pass.map(_ => PBoolLit(PReserved(PKw.True)(pos))(_))
         case "false" => Pass.map(_ => PBoolLit(PReserved(PKw.False)(pos))(_))
@@ -384,6 +384,7 @@ class FastParser {
         case "forperm" => forperm.map(_(PReserved(PKw.Forperm)(pos)))
         case "unfolding" => unfolding.map(_(PReserved(PKwOp.Unfolding)(pos)))
         case "applying" => applying.map(_(PReserved(PKwOp.Applying)(pos)))
+        case "asserting" => asserting.map(_(PReserved(PKwOp.Asserting)(pos)))
         case "Set" => setConstructor.map(_(PReserved(PKwOp.Set)(pos)))
         case "Seq" => seqConstructor.map(_(PReserved(PKwOp.Seq)(pos)))
         case "Multiset" => multisetConstructor.map(_(PReserved(PKwOp.Multiset)(pos)))
@@ -652,6 +653,10 @@ class FastParser {
       PApplying(_, wand.inner, op, b)
   }
 
+  def asserting[$: P]: P[PKwOp.Asserting => Pos => PExp] = P(exp.parens ~ PKwOp.In ~ exp).map {
+    case (a, in, b) => PAsserting(_, a.inner, in, b)
+  }
+
   def predicateAccessAssertion[$: P]: P[PAccAssertion] = P(accessPred | predAcc)
 
   def setConstructor[$: P]: P[PKwOp.Set => Pos => PExp] =

src/main/scala/viper/silver/parser/ParseAst.scala

@@ -1080,6 +1080,12 @@ case class PApplying(applying: PKwOp.Applying, wand: PExp, in: PKwOp.In, exp: PE
     List(Map(POpApp.pArgS(0) -> Wand, POpApp.pResS -> POpApp.pArg(1)))
 }
 
+case class PAsserting(asserting: PKwOp.Asserting, a: PExp, in: PKwOp.In, exp: PExp)(val pos: (Position, Position)) extends PHeapOpApp {
+  override val args = Seq(a, exp)
+  override val signatures: List[PTypeSubstitution] =
+    List(Map(POpApp.pArgS(0) -> Impure, POpApp.pResS -> POpApp.pArg(1)))
+}
+
 sealed trait PBinder extends PExp with PScope {
   def boundVars: Seq[PLogicalVarDecl]
 
@@ -1198,7 +1204,8 @@ case class PAccPred(op: PKwOp.Acc, amount: PGrouped.Paren[PMaybePairArgument[PLo
     Map(POpApp.pArgS(1) -> Perm, POpApp.pResS -> Impure),
   )
   def loc = amount.inner.first
-  def perm = amount.inner.second.map(_._2).getOrElse(PFullPerm.implied())
+  def perm = permExp.getOrElse(PFullPerm.implied())
+  def permExp: Option[PExp] = amount.inner.second.map(_._2)
   override val args = Seq(loc, perm)
 }