Checking only read permissions when asserting function preconditions (#816)

Author: marcoeilers

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
 }
 

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) ++

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 =
@@ -196,18 +208,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

@@ -193,7 +193,7 @@ 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))

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,7 +80,7 @@ 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)

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/cfg/CfgTest.scala

@@ -23,7 +23,7 @@ object CfgTest {
 
     val parsed = parse(string, file).get
     val resolver = Resolver(parsed)
-    val resolved = resolver.run.get
+    val resolved = resolver.run(false).get
     val translator = Translator(resolved)
     val program = translator.translate.get
 

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

@@ -333,7 +333,7 @@ trait SilFrontend extends DefaultFrontend {
         val r = Resolver(inputPlugin)
         FrontendStateCache.resolver = r
         FrontendStateCache.pprogram = inputPlugin
-        val analysisResult = r.run
+        val analysisResult = r.run(if (config == null) true else !config.respectFunctionPrePermAmounts())
         val warnings = for (m <- FastMessaging.sortmessages(r.messages) if !m.error) yield {
           TypecheckerWarning(m.label, m.pos)
         }
@@ -374,12 +374,16 @@ 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) {
       Succ(input)
-    } else
+    } else {
       Fail(errors)
+    }
   }
 }