diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala index 7df446050..68d179f4c 100644 --- a/src/main/scala/viper/silver/ast/Expression.scala +++ b/src/main/scala/viper/silver/ast/Expression.scala @@ -288,7 +288,7 @@ 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 } @@ -296,7 +296,7 @@ case class FieldAccessPredicate(loc: FieldAccess, permExp: Option[Exp])(val pos: 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 } diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala index e8c3227ff..367edc4b9 100644 --- a/src/main/scala/viper/silver/ast/Program.scala +++ b/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) ++ diff --git a/src/main/scala/viper/silver/ast/utility/Consistency.scala b/src/main/scala/viper/silver/ast/utility/Consistency.scala index da06ed6f8..7e18f152c 100644 --- a/src/main/scala/viper/silver/ast/utility/Consistency.scala +++ b/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 */ diff --git a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala index 1ddcf82df..3462335e6 100644 --- a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala +++ b/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, diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala index ef779af25..486b27282 100644 --- a/src/main/scala/viper/silver/frontend/SilFrontend.scala +++ b/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)