Renamed command line arg, allowing wildcard inside compound expressio…

…ns in functions

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

@@ -288,15 +288,15 @@ object 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, 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 =
@@ -185,19 +197,24 @@ object Consistency {
   }
 
   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
     }
-    val preWarnings = f.pres.collect(pre => pre.collect{
-      case ap: AccessPredicate if hasSpecificPermAmounts(ap.perm) =>
-        ConsistencyError("Function precondition contains specific permission amount that will be treated like write/wildcard.", ap.pos, false)
-    }).flatten
-    val bodyWarnings = f.body.toSeq.map(body => body.collect{
-      case ap: AccessPredicate if hasSpecificPermAmounts(ap.perm) =>
-        ConsistencyError("Function body contains specific permission amount that will be treated like write/wildcard.", ap.pos, false)
-    }).flatten
+    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
   }
 
@@ -213,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/frontend/SilFrontEndConfig.scala

@@ -139,7 +139,7 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     hidden = false
   )
 
-  val respectFunctionPrecPermAmounts = opt[Boolean]("respectFunctionPrecPermAmounts",
+  val respectFunctionPrePermAmounts = opt[Boolean]("respectFunctionPrePermAmounts",
     descr = "Respects precise permission amounts in function preconditions instead of only checking read access.",
     default = Some(false),
     noshort = true,

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

@@ -374,6 +374,9 @@ 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)