diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala index e00210531..3aa6fa4b5 100644 --- a/src/main/scala/viper/gobra/ast/frontend/Ast.scala +++ b/src/main/scala/viper/gobra/ast/frontend/Ast.scala @@ -898,6 +898,7 @@ case class PFunctionSpec( isPure: Boolean = false, isTrusted: Boolean = false, isOpaque: Boolean = false, + mayBeUsedInInit: Boolean, ) extends PSpecification case class PBackendAnnotation(key: String, values: Vector[String]) extends PGhostMisc diff --git a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala index 02ef3aac1..93045ebb0 100644 --- a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala +++ b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala @@ -137,6 +137,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter def showPure: Doc = "pure" <> line def showOpaque: Doc = "opaque" <> line def showTrusted: Doc = "trusted" <> line + def showMayInit: Doc = "mayInit" <> line def showPre(pre: PExpression): Doc = "requires" <+> showExpr(pre) def showPreserves(preserves: PExpression): Doc = "preserves" <+> showExpr(preserves) def showPost(post: PExpression): Doc = "ensures" <+> showExpr(post) @@ -151,10 +152,11 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter } def showSpec(spec: PSpecification): Doc = spec match { - case PFunctionSpec(pres, preserves, posts, measures, backendAnnotations, isPure, isTrusted, isOpaque) => + case PFunctionSpec(pres, preserves, posts, measures, backendAnnotations, isPure, isTrusted, isOpaque, mayInit) => (if (isPure) showPure else emptyDoc) <> (if (isOpaque) showOpaque else emptyDoc) <> (if (isTrusted) showTrusted else emptyDoc) <> + (if (mayInit) showMayInit else emptyDoc) <> hcat(pres map (showPre(_) <> line)) <> hcat(preserves map (showPreserves(_) <> line)) <> hcat(posts map (showPost(_) <> line)) <> diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index ec6fa7f3b..77215291a 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/src/main/scala/viper/gobra/frontend/Desugar.scala @@ -8,7 +8,6 @@ package viper.gobra.frontend import com.typesafe.scalalogging.LazyLogging import viper.gobra.ast.frontend.{PExpression, AstPattern => ap, _} -import viper.gobra.ast.internal.{MethodBody, MethodBodySeqn} import viper.gobra.ast.{internal => in} import viper.gobra.frontend.PackageResolver.RegularImport import viper.gobra.frontend.Source.TransformableSource @@ -3506,7 +3505,7 @@ object Desugar extends LazyLogging { posts = Vector(assertion, assertion), terminationMeasures = Vector.empty, backendAnnotations = Vector.empty, - body = Some(MethodBody.empty(src)) + body = Some(in.MethodBody.empty(src)) )(src) } @@ -4150,17 +4149,15 @@ object Desugar extends LazyLogging { case _ => for {e <- goA(exp)} yield in.Unfold(e.asInstanceOf[in.Access])(src) } case POpenDupPkgInv(pkgId) => + // TODO: drop the `pkgId` param, and skip this check. openDupPkgInv should only + // open the current package's invariant. val currPkgName = info.pkgName.name val thisPkg = info.tree.root val ppkg = pkgId match { case `currPkgName` => thisPkg case _ => - // TODO: explain this hack - we require the full path, getting the pkg - // from its qualifier is very hard because the desugarer does not know which - // PProgram it is currently looking at - // thisPkg.programs.flatMap(_.imports).filter(_.importPath == pkgId) - ??? + Violation.violation("Cannot use the openDupPkgInv statement to open the invariant of other packages. Use a ghost method instead.") } val dupInvs = initSpecs.get.dupPkgInvsOfPackage(ppkg) val inhales = dupInvs.map(i => in.Inhale(i)(src)) diff --git a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala index ba52838fc..d16d6455d 100644 --- a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala +++ b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala @@ -430,7 +430,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole val spec = if (ctx.specification() != null) visitSpecification(ctx.specification()) else - PFunctionSpec(Vector.empty,Vector.empty,Vector.empty, Vector.empty, Vector.empty).at(ctx) + PFunctionSpec(Vector.empty,Vector.empty,Vector.empty, Vector.empty, Vector.empty, mayBeUsedInInit = false).at(ctx) // TODO: drop // The name of each explicitly specified method must be unique and not blank. val id = idnDef.get(ctx.IDENTIFIER()) val args = visitNode[Vector[Vector[PParameter]]](ctx.parameters()) @@ -914,7 +914,8 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole annotations, isPure = ctx.pure, isTrusted = ctx.trusted, - isOpaque = ctx.opaque + isOpaque = ctx.opaque, + mayBeUsedInInit = ctx.mayInit, ) } diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala index 0f1e52641..15a9bc9d0 100644 --- a/src/main/scala/viper/gobra/frontend/Parser.scala +++ b/src/main/scala/viper/gobra/frontend/Parser.scala @@ -493,7 +493,7 @@ object Parser extends LazyLogging { case n@PTupleTerminationMeasure(_, cond) => PWildcardMeasure(cond).at(n) case t => t } - PFunctionSpec(spec.pres, spec.preserves, spec.posts, replacedMeasures, spec.backendAnnotations, spec.isPure, spec.isTrusted) + PFunctionSpec(spec.pres, spec.preserves, spec.posts, replacedMeasures, spec.backendAnnotations, spec.isPure, spec.isTrusted, mayBeUsedInInit = spec.mayBeUsedInInit) // TODO: drop } val replaceTerminationMeasuresForFunctionsAndMethods: Strategy = diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala index c25c4c9a3..9ce9c9cf6 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala @@ -84,12 +84,31 @@ trait Enclosing { this: TypeInfoImpl => lazy val tryEnclosingOutline: PNode => Option[POutline] = down[Option[POutline]](None) { case x: POutline => Some(x) } + lazy val tryEnclosingGlobalVarDeclaration: PNode => Option[PVarDecl] = + down[Option[PVarDecl]](None) { + case x: PVarDecl if isGlobalVarDeclaration(x) => Some(x) + case x: PVarDecl => tryEnclosingGlobalVarDeclaration(x) + } + lazy val isEnclosingExplicitGhost: PNode => Boolean = down(false){ case _: PGhostifier[_] => true } lazy val isEnclosingGhost: PNode => Boolean = down(false){ case _: PGhostifier[_] | _: PGhostNode => true } + def isEnclosingMayInit(n: PNode): Boolean = { + val cond1 = tryEnclosingFunctionOrMethod(n) match { + case Some(f: PFunctionDecl) => f.id.name == "init" || f.spec.mayBeUsedInInit + case Some(m: PMethodDecl) => m.spec.mayBeUsedInInit + case _ => false // TODO: change dflt? + } + val cond2 = tryEnclosingGlobalVarDeclaration(n) match { + case Some(_) => true + case _ => false + } + cond1 || cond2 + } + lazy val isEnclosingDomain: PNode => Boolean = down(false){ case _: PDomainType => true } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala index 8d5826598..bf3a78f37 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala @@ -252,11 +252,11 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => argWithinBounds case (Left(callee), Some(c: ap.FunctionCall)) => - val isOpaque = c.callee match { + val (isOpaque, isMayInit, isImported) = c.callee match { case base: ap.Symbolic => base.symb match { - case f: st.Function => f.isOpaque - case m: st.MethodImpl => m.isOpaque - case _ => false + case f: st.Function => (f.isOpaque, f.decl.spec.mayBeUsedInInit, f.context != this) + case m: st.MethodImpl => (m.isOpaque, m.decl.spec.mayBeUsedInInit, m.context != this) + case _ => (false, true, false) // TODO: check defaults } } val onlyRevealOpaqueFunc = @@ -273,7 +273,8 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case t: AbstractType => t.messages(n, n.args map exprType) case t => error(n, s"type error: got $t but expected function type or AbstractType") } - onlyRevealOpaqueFunc ++ isCallToInit ++ wellTypedArgs + val mayInitSeparation = error(n, "Function called from 'mayInit' context is not 'mayInit'.", !isImported && (isEnclosingMayInit(n) && !isMayInit)) + onlyRevealOpaqueFunc ++ isCallToInit ++ wellTypedArgs ++ mayInitSeparation case (Left(_), Some(_: ap.ClosureCall)) => error(n, "Only calls to pure functions and pure methods can be revealed: Cannot reveal a closure call.", n.reveal) ++ wellDefCallWithSpec(n) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala index d91a5f68b..ee01a4627 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala @@ -6,11 +6,12 @@ package viper.gobra.frontend.info.implementation.typing -import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages} +import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, check, checkUse, error, message, noMessages} import scala.collection.immutable.ListMap import viper.gobra.ast.frontend._ import viper.gobra.ast.frontend.{AstPattern => ap} +import viper.gobra.frontend.info.base.SymbolTable import viper.gobra.frontend.info.base.SymbolTable.{Embbed, Field} import viper.gobra.frontend.info.base.Type.{StructT, _} import viper.gobra.frontend.info.implementation.TypeInfoImpl @@ -68,7 +69,17 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => case t: PInterfaceType => val isRecursiveInterface = error(t, "invalid recursive interface", cyclicInterfaceDef(t)) if (isRecursiveInterface.isEmpty) { - addressableMethodSet(InterfaceT(t, this)).errors(t) ++ + val methodSet = addressableMethodSet(InterfaceT(t, this)) + val methodsContainMayInit = methodSet.exists { + case (_, (m, _)) => m match { + case m: SymbolTable.MethodSpec => + m.spec.spec.mayBeUsedInInit + case _ => false + } + } + + methodSet.errors(t) ++ + error(t, "Interface declaration contains methods annotated with 'mayInit'.", methodsContainMayInit) ++ containsRedeclarations(t) // temporary check } else { isRecursiveInterface diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala index d25b98706..74caeb0a5 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala @@ -49,7 +49,8 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => isSingleResultArg(member) ++ isSinglePureReturnExpr(member) ++ isPurePostcondition(member.spec) ++ - nonVariadicArguments(member.args) + nonVariadicArguments(member.args) ++ + error(member, "Pure functions cannot be annotated with 'mayInit'.", member.spec.mayBeUsedInInit) } else noMessages } @@ -64,7 +65,8 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => isSingleResultArg(member) ++ isSinglePureReturnExpr(member) ++ isPurePostcondition(member.spec) ++ - nonVariadicArguments(member.args) + nonVariadicArguments(member.args) ++ + error(member, "Pure functions cannot be annotated with 'mayInit'.", member.spec.mayBeUsedInInit) } else noMessages } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala index 198ce6433..241a98c10 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala @@ -150,7 +150,7 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => } implicit lazy val wellDefSpec: WellDefinedness[PSpecification] = createWellDef { - case n@ PFunctionSpec(pres, preserves, posts, terminationMeasures, _, isPure, _, isOpaque) => + case n@ PFunctionSpec(pres, preserves, posts, terminationMeasures, _, isPure, _, isOpaque, _) => pres.flatMap(assignableToSpec) ++ preserves.flatMap(assignableToSpec) ++ posts.flatMap(assignableToSpec) ++ preserves.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++ pres.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++ diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala index aea6b4dca..e10a8ec12 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala @@ -24,8 +24,17 @@ trait GhostStmtTyping extends BaseTyping { this: TypeInfoImpl => case PFold(acc) => wellDefFoldable(acc) case PUnfold(acc) => wellDefFoldable(acc) case POpenDupPkgInv(_) => - //TODO: add check that if it is '_', we are in a non-init fn - noMessages + // TODO: do the same for opening non-dup invs + tryEnclosingFunctionOrMethod(stmt) match { + case Some(m) => + val occursInInitMember = m match { + case f: PFunctionDecl if f.id.name == "init" || f.spec.mayBeUsedInInit => true + case m: PMethodDecl if m.spec.mayBeUsedInInit => true + case _ => false + } + error(stmt, "Trying to open the package invariant in a function that may execute during initialization is not allowed.", occursInInitMember) + case _ => noMessages + } case n@PPackageWand(wand, optBlock) => assignableToSpec(wand) ++ error(n, "ghost error: expected ghostifiable statement", !optBlock.forall(_.isInstanceOf[PGhostifiableStatement])) case PApplyWand(wand) => assignableToSpec(wand) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostLessPrinter.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostLessPrinter.scala index 8670e27d9..79ac2a072 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostLessPrinter.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostLessPrinter.scala @@ -21,7 +21,7 @@ class GhostLessPrinter(classifier: GhostClassifier) extends DefaultPrettyPrinter rec, filterParamList(args), filterResult(res), - PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty), + PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty, mayBeUsedInInit = false), // TODO: delete body.map( b => (PBodyParameterInfo(Vector.empty), b._2) ) ) ) @@ -32,7 +32,7 @@ class GhostLessPrinter(classifier: GhostClassifier) extends DefaultPrettyPrinter id, filterParamList(args), filterResult(res), - PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty), + PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty, mayBeUsedInInit = false), // TODO: delete body.map( b => (PBodyParameterInfo(Vector.empty), b._2) ) ) ) @@ -171,7 +171,7 @@ class GhostLessPrinter(classifier: GhostClassifier) extends DefaultPrettyPrinter case PFunctionLit(_, PClosureDecl(args, result, _, body)) => super.showMisc(PClosureDecl( filterParamList(args), filterResult(result), - PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty), + PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty, mayBeUsedInInit = false), // TODO: delete body.map( b => (PBodyParameterInfo(Vector.empty), b._2) ) )) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala index 8ec804f85..5fd361b5e 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala @@ -77,10 +77,11 @@ class GoifyingPrinter(info: TypeInfoImpl) extends DefaultPrettyPrinter { * Shows the Goified version of the function / method specification */ override def showSpec(spec: PSpecification): Doc = spec match { - case PFunctionSpec(pres, preserves, posts, measures, backendAnnotations, isPure, isTrusted, isOpaque) => + case PFunctionSpec(pres, preserves, posts, measures, backendAnnotations, isPure, isTrusted, isOpaque, mayInit) => (if (isPure) specComment <+> showPure else emptyDoc) <> (if (isOpaque) specComment <+> showOpaque else emptyDoc) <> (if (isTrusted) specComment <+> showTrusted else emptyDoc) <> + (if (mayInit) specComment <+> showMayInit else emptyDoc) <> hcat(pres map (p => specComment <+> showPre(p) <> line)) <> hcat(preserves map (p => specComment <+> showPreserves(p) <> line)) <> hcat(posts map (p => specComment <+> showPost(p) <> line)) <> @@ -126,7 +127,7 @@ class GoifyingPrinter(info: TypeInfoImpl) extends DefaultPrettyPrinter { rec, getActualParams(args), getActualResult(res), - PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty), + PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty, mayBeUsedInInit = false), // TODO: delete body ) ) @@ -138,7 +139,7 @@ class GoifyingPrinter(info: TypeInfoImpl) extends DefaultPrettyPrinter { id, getActualParams(args), getActualResult(res), - PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty), + PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty, mayBeUsedInInit = false), // TODO: delete body ) )