From 3d7a31615a2f1d1153e35ed2216cb67cdb26d3d9 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Sun, 29 Dec 2024 03:56:26 +0100 Subject: [PATCH] Adding consistency checks to forbid inhale-exhale-assertions in function preconditions and predicate bodies --- src/main/scala/viper/silver/ast/Program.scala | 2 ++ src/main/scala/viper/silver/ast/utility/Consistency.scala | 8 ++++++++ 2 files changed, 10 insertions(+) diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala index 733fbee1b..b5013bc1c 100644 --- a/src/main/scala/viper/silver/ast/Program.scala +++ b/src/main/scala/viper/silver/ast/Program.scala @@ -362,6 +362,7 @@ case class Field(name: String, typ: Type)(val pos: Position = NoPosition, val in 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) ++ Consistency.checkWildcardUsage(body.get, false) else Seq()) ++ + (if (body.isDefined) Consistency.checkNoInhaleExhale(body.get, "predicates") else Seq()) ++ (if (body.isDefined && !Consistency.noOld(body.get)) Seq(ConsistencyError("Predicates must not contain old expressions.",body.get.pos)) else Seq()) ++ @@ -455,6 +456,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 flatMap (pre => Consistency.checkNoInhaleExhale(pre, "function preconditions"))) ++ (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() )) ++ diff --git a/src/main/scala/viper/silver/ast/utility/Consistency.scala b/src/main/scala/viper/silver/ast/utility/Consistency.scala index 7d112ff34..c997622a7 100644 --- a/src/main/scala/viper/silver/ast/utility/Consistency.scala +++ b/src/main/scala/viper/silver/ast/utility/Consistency.scala @@ -161,6 +161,14 @@ object Consistency { }) } + /** Checks that no inhale/exhale assertions occur in the given node. */ + def checkNoInhaleExhale(e: Exp, locationDescription: String) : Seq[ConsistencyError] = { + e.deepCollect({ + case ie: InhaleExhaleExp => + ConsistencyError(s"Inhale-exhale expressions are not allowed in ${locationDescription}.", ie.pos) + }) + } + /** Check all properties required for a function body. */ def checkFunctionBody(e: Exp) : Seq[ConsistencyError] = { var s = Seq.empty[ConsistencyError]