backup

src/main/antlr4/GobraLexer.g4

@@ -85,6 +85,8 @@ WRITEPERM   : 'writePerm' -> mode(NLSEMI);
 NOPERM      : 'noPerm' -> mode(NLSEMI);
 TRUSTED     : 'trusted' -> mode(NLSEMI);
 OUTLINE     : 'outline';
+DUPLICABLE  : 'duplicable';
+PKG_INV     : 'pkgInvariant';
 INIT_POST   : 'initEnsures';
 IMPORT_PRE  : 'importRequires';
 PROOF       : 'proof';

src/main/antlr4/GobraParser.g4

@@ -32,9 +32,8 @@ maybeAddressableIdentifierList: maybeAddressableIdentifier (COMMA maybeAddressab
 maybeAddressableIdentifier: IDENTIFIER ADDR_MOD?;
 
 // Ghost members
-
 sourceFile:
-  (initPost eos)* packageClause eos (importDecl eos)* (
+  ((initPost eos) | (pkgInvariant eos))* packageClause eos (importDecl eos)* (
     (specMember | declaration | ghostMember) eos
   )* EOF;
 
@@ -46,6 +45,8 @@ initPost: INIT_POST expression;
 
 importPre: IMPORT_PRE expression;
 
+pkgInvariant: DUPLICABLE? PKG_INV assertion;
+
 importSpec: (importPre eos)* alias = (DOT | IDENTIFIER)? importPath;
 
 importDecl: (importPre eos)* (IMPORT importSpec | IMPORT L_PAREN (importSpec eos)* R_PAREN);

src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java

@@ -1,4 +1,4 @@
-// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
+// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
 
@@ -75,6 +75,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitImportPre(GobraParser.ImportPreContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitPkgInvariant(GobraParser.PkgInvariantContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *

src/main/java/viper/gobra/frontend/GobraParserVisitor.java

@@ -1,4 +1,4 @@
-// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
+// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.ParseTreeVisitor;
 
@@ -64,6 +64,12 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitImportPre(GobraParser.ImportPreContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#pkgInvariant}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitPkgInvariant(GobraParser.PkgInvariantContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#importSpec}.
 	 * @param ctx the parse tree

src/main/scala/viper/gobra/frontend/Config.scala

@@ -77,6 +77,7 @@ object ConfigDefaults {
   val DefaultDisableCheckTerminationPureFns: Boolean = false
   val DefaultUnsafeWildcardOptimization: Boolean = false
   val DefaultMoreJoins: MoreJoins.Mode = MoreJoins.Disabled
+  val DefaultEnableModularInit: Boolean = false
 }
 
 // More-complete exhale modes
@@ -172,6 +173,7 @@ case class Config(
                    disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns,
                    unsafeWildcardOptimization: Boolean = ConfigDefaults.DefaultUnsafeWildcardOptimization,
                    moreJoins: MoreJoins.Mode = ConfigDefaults.DefaultMoreJoins,
+                   enableModularInit: Boolean = ConfigDefaults.DefaultEnableModularInit,
 
 ) {
 
@@ -227,6 +229,7 @@ case class Config(
       disableCheckTerminationPureFns = disableCheckTerminationPureFns || other.disableCheckTerminationPureFns,
       unsafeWildcardOptimization = unsafeWildcardOptimization && other.unsafeWildcardOptimization,
       moreJoins = MoreJoins.merge(moreJoins, other.moreJoins),
+      enableModularInit = enableModularInit && other.enableModularInit,
     )
   }
 
@@ -247,6 +250,9 @@ object Config {
 
   val enableLazyImportOptionName = "enableLazyImport"
   val enableLazyImportOptionPrettyPrinted = s"--$enableLazyImportOptionName"
+
+  val enableModularInitOptionName = "enableModularInit"
+  val enableModularInitOptionNamePrettyPrinted = s"--$enableModularInitOptionName"
 }
 
 // have a look at `Config` to see an inline description of some of these parameters
@@ -285,6 +291,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns,
                       unsafeWildcardOptimization: Boolean = ConfigDefaults.DefaultUnsafeWildcardOptimization,
                       moreJoins: MoreJoins.Mode = ConfigDefaults.DefaultMoreJoins,
+                      enableModularInit: Boolean = ConfigDefaults.DefaultEnableModularInit,
                      ) {
   def shouldParse: Boolean = true
   def shouldTypeCheck: Boolean = !shouldParseOnly
@@ -347,6 +354,7 @@ trait RawConfig {
     disableCheckTerminationPureFns = baseConfig.disableCheckTerminationPureFns,
     unsafeWildcardOptimization = baseConfig.unsafeWildcardOptimization,
     moreJoins = baseConfig.moreJoins,
+    enableModularInit = baseConfig.enableModularInit,
   )
 }
 
@@ -778,6 +786,13 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     noshort = true,
   )
 
+  val enableModularInit: ScallopOption[Boolean] = opt[Boolean](
+    name = Config.enableModularInitOptionName,
+    descr = s"Use the modular algorithms for checking the correctness of static initializers.",
+    default = Some(ConfigDefaults.DefaultEnableLazyImports),
+    noshort = true,
+  )
+
   val requireTriggers: ScallopOption[Boolean] = opt[Boolean](
     name = "requireTriggers",
     descr = s"Enforces that all quantifiers have a user-provided trigger.",
@@ -862,6 +877,16 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     }
   }
 
+  addValidation {
+    val enableModularInitOn = enableModularInit.toOption.contains(true)
+    val enableLazyImportsOn = enableLazyImports.toOption.contains(true)
+    if (enableModularInitOn && enableLazyImportsOn) {
+      Left(s"Unsupported combination of features: ${Config.enableModularInitOptionNamePrettyPrinted} and ${Config.enableLazyImportOptionPrettyPrinted}.")
+    } else {
+      Right(())
+    }
+  }
+
   addValidation {
     val conditionalizePermissionsOn = conditionalizePermissions.toOption.contains(true)
     if (conditionalizePermissionsOn && !isSiliconBasedBackend) {
@@ -1026,5 +1051,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     disableCheckTerminationPureFns = disableCheckTerminationPureFns(),
     unsafeWildcardOptimization = unsafeWildcardOptimization(),
     moreJoins = moreJoins(),
+    enableModularInit = enableModularInit(),
   )
 }

src/main/scala/viper/gobra/frontend/info/implementation/typing/ProgramTyping.scala

@@ -19,7 +19,7 @@ import viper.gobra.util.Violation
 trait ProgramTyping extends BaseTyping { this: TypeInfoImpl =>
 
   lazy val wellDefProgram: WellDefinedness[PProgram] = createWellDef {
-    case PProgram(_, posts, imports, members) =>
+    case p@PProgram(_, posts, imports, members) =>
       if (config.enableLazyImports) {
         posts.flatMap(post => message(post, s"Init postconditions are not allowed when executing ${GoVerifier.name} with ${Config.enableLazyImportOptionPrettyPrinted}"))
       } else {
@@ -42,9 +42,13 @@ trait ProgramTyping extends BaseTyping { this: TypeInfoImpl =>
         //       assume that the ids are well-defined.
         val idsOkMsgs = sortedByPosDecls.flatMap(d => d.left).flatMap(l => wellDefID(l).out)
         if (idsOkMsgs.isEmpty) {
-          globalDeclSatisfiesDepOrder(sortedByPosDecls) ++
-            hasOldExpression(posts) ++
-            hasOldExpression(imports.flatMap(_.importPres))
+          val globalDeclsInRightOrder = globalDeclSatisfiesDepOrder(sortedByPosDecls)
+          globalDeclsInRightOrder ++ (if (config.enableModularInit) {
+            error(p, s"Init-postconditions are not allowed when using the flag ${Config.enableModularInitOptionNamePrettyPrinted}", posts.nonEmpty) ++
+              error(p, s"Import-preconditions are not allowed when using the flag ${Config.enableModularInitOptionNamePrettyPrinted}", imports.flatMap(_.importPres).nonEmpty)
+          } else {
+            hasOldExpression(posts) ++ hasOldExpression(imports.flatMap(_.importPres))
+          })
         } else {
           idsOkMsgs
         }