backup

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

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

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

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,
     )
   }
 

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 =

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 }
 

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)

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

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
   }
 

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

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)

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

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