Package invariants

.gitignore

@@ -5,6 +5,7 @@ project/target/
 target/
 tmp/
 sync/
+gobra_tmp/
 
 logger.log
 .DS_Store

src/main/antlr4/GobraLexer.g4

@@ -86,13 +86,18 @@ WRITEPERM   : 'writePerm' -> mode(NLSEMI);
 NOPERM      : 'noPerm' -> mode(NLSEMI);
 TRUSTED     : 'trusted' -> mode(NLSEMI);
 OUTLINE     : 'outline';
+DUPLICABLE  : 'dup';
+PKG_INV     : 'pkgInvariant';
+OPEN_DUP_SINV : 'openDupPkgInv' -> mode(NLSEMI);
 INIT_POST   : 'initEnsures';
 IMPORT_PRE  : 'importRequires';
 PROOF       : 'proof';
 GHOST_EQUALS     : '===';
 GHOST_NOT_EQUALS : '!==';
 WITH        : 'with';
 OPAQUE      : 'opaque' -> mode(NLSEMI);
+MAYINIT     : 'mayInit' -> mode(NLSEMI);
 REVEAL      : 'reveal';
 BACKEND     : '#backend';
-// NOTE: if you append a new token, do not forget to update InformativeErrorListener.LAST_GOBRA_TOKEN
+FRIENDPKG   : 'friendPkg';
+// NOTE: if you append a new token, do not forget to update InformativeErrorListener.LAST_GOBRA_TOKEN

src/main/antlr4/GobraParser.g4

@@ -31,21 +31,24 @@ maybeAddressableIdentifierList: maybeAddressableIdentifier (COMMA maybeAddressab
 
 maybeAddressableIdentifier: IDENTIFIER ADDR_MOD?;
 
-// Ghost members
+friendPkgDecl: FRIENDPKG importPath assertion;
 
+// Ghost members
 sourceFile:
-  (initPost eos)* packageClause eos (importDecl eos)* (
+  (pkgInvariant eos)* (initPost eos)* packageClause eos (friendPkgDecl eos)* (importDecl eos)* (
     member eos
   )* EOF;
 
 // `preamble` is a second entry point allowing us to parse only the top of a source.
 // That's also why we don not enforce EOF at the end.
-preamble: (initPost eos)* packageClause eos (importDecl eos)*;
+preamble: (pkgInvariant eos)* (initPost eos)* packageClause eos (friendPkgDecl eos)* (importDecl eos)*;
 
 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);
@@ -64,6 +67,7 @@ ghostStatement:
   | fold_stmt=(FOLD | UNFOLD) predicateAccess #foldStatement
   | kind=(ASSUME | ASSERT | REFUTE | INHALE | EXHALE) expression #proofStatement
   | matchStmt #matchStmt_
+  | OPEN_DUP_SINV #pkgInvStatement
   ;
 
 // Auxiliary statements
@@ -172,9 +176,9 @@ sqType: (kind=(SEQ | SET | MSET | OPT) L_BRACKET type_ R_BRACKET)
 
 // Specifications
 
-specification returns[boolean trusted = false, boolean pure = false, boolean opaque = false;]:
+specification returns[boolean trusted = false, boolean pure = false, boolean mayInit = false, boolean opaque = false;]:
   // Non-greedily match PURE to avoid missing eos errors.
-  ((specStatement | OPAQUE {$opaque = true;} | PURE {$pure = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? backendAnnotation?
+  ((specStatement | OPAQUE {$opaque = true;} | PURE {$pure = true;} | MAYINIT {$mayInit = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? backendAnnotation?
   ;
 
 backendAnnotationEntry: ~('('|')'|',')+;

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -53,23 +53,26 @@ case class PPackage(
 
 case class PProgram(
                      packageClause: PPackageClause,
-                     // init postconditions describe the state and resources right
-                     // after this program is initialized
+                     pkgInvariants: Vector[PPkgInvariant],
+                     @deprecated("Init postconditions were deprecated in PR #797 and will soon be completely removed.")
                      initPosts: Vector[PExpression],
                      imports: Vector[PImport],
+                     friends: Vector[PFriendPkgDecl],
                      declarations: Vector[PMember]
                    ) extends PNode with PUnorderedScope // imports are in program scopes
 
 
 case class PPreamble(
                       packageClause: PPackageClause,
-                      // init postconditions describe the state and resources right
-                      // after this program is initialized
+                      pkgInvariants: Vector[PPkgInvariant],
+                      @deprecated("Init postconditions were deprecated in PR #797 and will soon be completely removed.")
                       initPosts: Vector[PExpression],
                       imports: Vector[PImport],
+                      friends: Vector[PFriendPkgDecl],
                       positions: PositionManager,
                     ) extends PNode with PUnorderedScope
 
+case class PPkgInvariant(inv: PExpression, duplicable: Boolean) extends PNode
 
 class PositionManager(val positions: Positions) extends Messaging(positions) {
 
@@ -124,6 +127,8 @@ case class PImplicitQualifiedImport(importPath: String, importPres: Vector[PExpr
 
 case class PUnqualifiedImport(importPath: String, importPres: Vector[PExpression]) extends PImport
 
+case class PFriendPkgDecl(path: String, assertion: PExpression) extends PNode
+
 sealed trait PGhostifiable extends PNode
 
 sealed trait PMember extends PNode
@@ -893,6 +898,7 @@ case class PFunctionSpec(
                           isPure: Boolean = false,
                           isTrusted: Boolean = false,
                           isOpaque: Boolean = false,
+                          mayBeUsedInInit: Boolean = false,
                       ) extends PSpecification
 
 case class PBackendAnnotation(key: String, values: Vector[String]) extends PGhostMisc
@@ -981,6 +987,8 @@ case class PFold(exp: PPredicateAccess) extends PGhostStatement with PDeferrable
 
 case class PUnfold(exp: PPredicateAccess) extends PGhostStatement with PDeferrable
 
+case class POpenDupPkgInv() extends PGhostStatement with PDeferrable
+
 case class PPackageWand(wand: PMagicWand, proofScript: Option[PBlock]) extends PGhostStatement
 
 case class PApplyWand(wand: PMagicWand) extends PGhostStatement

src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala

@@ -50,6 +50,8 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case n: PInterfaceClause => showInterfaceClause(n)
     case n: PBodyParameterInfo => showBodyParameterInfo(n)
     case n: PTerminationMeasure => showTerminationMeasure(n)
+    case n: PPkgInvariant => showPkgInvariant(n)
+    case n: PFriendPkgDecl => showFriend(n)
     case PPos(_) => emptyDoc
   }
 
@@ -61,23 +63,37 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   // program
 
   def showProgram(p: PProgram): Doc = p match {
-    case PProgram(packageClause, progPosts, imports, declarations) =>
-      showPreamble(packageClause, progPosts, imports) <>
+    // initPosts not shown, they are deprecated and will soon be removed
+    case PProgram(packageClause, pkgInvs, _, imports, friends, declarations) =>
+      showPreamble(packageClause, pkgInvs, imports, friends) <>
         ssep(declarations map showMember, line <> line) <> line
   }
 
   // preamble
 
   def showPreamble(p: PPreamble): Doc = p match {
-    case PPreamble(packageClause, progPosts, imports, _) =>
-      showPreamble(packageClause, progPosts, imports)
-  }
-
-  private def showPreamble(packageClause: PPackageClause, progPosts: Vector[PExpression], imports: Vector[PImport]): Doc =
-    vcat(progPosts.map("initEnsures" <+> showExpr(_))) <>
+    // initPosts not shown, they are deprecated and will soon be removed
+    case PPreamble(packageClause, pkgInvs, _, imports, friends, _) =>
+      showPreamble(packageClause, pkgInvs, imports, friends)
+  }
+
+  private def showPreamble(
+                            packageClause: PPackageClause,
+                            pkgInvs: Vector[PPkgInvariant],
+                            imports: Vector[PImport],
+                            friends: Vector[PFriendPkgDecl]
+                          ): Doc =
+    vcat(pkgInvs.map(showPkgInvariant)) <> line <>
       showPackageClause(packageClause) <> line <> line <>
+      ssep(friends map showFriend, line) <> line <>
       ssep(imports map showImport, line) <> line
 
+  private def showPkgInvariant(inv: PPkgInvariant): Doc = {
+    val dup: Doc = if (inv.duplicable) "dup" else emptyDoc
+    val expr = showExpr(inv.inv)
+    dup <+> "pkgInvariant" <+> expr
+  }
+
   // package
 
   def showPackageClause(node: PPackageClause): Doc = "package" <+> showPackageId(node.id)
@@ -99,6 +115,11 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     }
   }
 
+  // friend pkgs
+  def showFriend(decl: PFriendPkgDecl): Doc = {
+    "friendPkg" <+> decl.path <+> showExpr(decl.assertion)
+  }
+
   // members
 
   def showMember(mem: PMember): Doc = mem match {
@@ -130,6 +151,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)
@@ -144,10 +166,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)) <>
@@ -292,6 +315,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       case PFold(exp) => "fold" <+> showExpr(exp)
       case PPackageWand(wand, blockOpt) => "package" <+> showExpr(wand) <+> opt(blockOpt)(showStmt)
       case PApplyWand(wand) => "apply" <+> showExpr(wand)
+      case POpenDupPkgInv() => "openDupPkgInv"
       case PMatchStatement(exp, clauses, _) => "match" <+>
         showExpr(exp) <+> block(ssep(clauses map showMatchClauseStatement, line))
     }

src/main/scala/viper/gobra/ast/internal/Program.scala

@@ -335,6 +335,12 @@ case class MethodBody(
                        postprocessing: Vector[Stmt] = Vector.empty,
                      )(val info: Source.Parser.Info) extends Stmt
 
+object MethodBody {
+  def empty(info: Source.Parser.Info): MethodBody = {
+    MethodBody(Vector.empty, MethodBodySeqn(Vector.empty)(info), Vector.empty)(info)
+  }
+}
+
 /**
   * This node serves as a target of encoding extensions. See [[viper.gobra.translator.encodings.combinators.TypeEncoding.Extension]]
   * Return statements jump exactly to the end of the encoding of this statement.

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

@@ -78,6 +78,7 @@ object ConfigDefaults {
   val DefaultUnsafeWildcardOptimization: Boolean = false
   val DefaultMoreJoins: MoreJoins.Mode = MoreJoins.Disabled
   val DefaultRespectFunctionPrePermAmounts: Boolean = false
+  val DefaultEnableExperimentalFriendClauses: Boolean = false
 }
 
 // More-complete exhale modes
@@ -164,7 +165,6 @@ case class Config(
                    z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode,
                    disableNL: Boolean = ConfigDefaults.DefaultDisableNL,
                    mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode,
-                   enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
                    noVerify: Boolean = ConfigDefaults.DefaultNoVerify,
                    noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors,
                    parseAndTypeCheckMode: TaskManagerMode = ConfigDefaults.DefaultParseAndTypeCheckMode,
@@ -175,6 +175,7 @@ case class Config(
                    unsafeWildcardOptimization: Boolean = ConfigDefaults.DefaultUnsafeWildcardOptimization,
                    moreJoins: MoreJoins.Mode = ConfigDefaults.DefaultMoreJoins,
                    respectFunctionPrePermAmounts: Boolean = ConfigDefaults.DefaultRespectFunctionPrePermAmounts,
+                   enableExperimentalFriendClauses: Boolean = ConfigDefaults.DefaultEnableExperimentalFriendClauses,
 ) {
 
   def merge(other: Config): Config = {
@@ -225,7 +226,6 @@ case class Config(
       z3APIMode = z3APIMode || other.z3APIMode,
       disableNL = disableNL || other.disableNL,
       mceMode = mceMode,
-      enableLazyImports = enableLazyImports || other.enableLazyImports,
       noVerify = noVerify || other.noVerify,
       noStreamErrors = noStreamErrors || other.noStreamErrors,
       parseAndTypeCheckMode = parseAndTypeCheckMode,
@@ -235,6 +235,7 @@ case class Config(
       unsafeWildcardOptimization = unsafeWildcardOptimization && other.unsafeWildcardOptimization,
       moreJoins = MoreJoins.merge(moreJoins, other.moreJoins),
       respectFunctionPrePermAmounts = respectFunctionPrePermAmounts || other.respectFunctionPrePermAmounts,
+      enableExperimentalFriendClauses = enableExperimentalFriendClauses || other.enableExperimentalFriendClauses,
     )
   }
 
@@ -286,7 +287,6 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode,
                       disableNL: Boolean = ConfigDefaults.DefaultDisableNL,
                       mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode,
-                      enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
                       noVerify: Boolean = ConfigDefaults.DefaultNoVerify,
                       noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors,
                       parseAndTypeCheckMode: TaskManagerMode = ConfigDefaults.DefaultParseAndTypeCheckMode,
@@ -296,6 +296,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       unsafeWildcardOptimization: Boolean = ConfigDefaults.DefaultUnsafeWildcardOptimization,
                       moreJoins: MoreJoins.Mode = ConfigDefaults.DefaultMoreJoins,
                       respectFunctionPrePermAmounts: Boolean = ConfigDefaults.DefaultRespectFunctionPrePermAmounts,
+                      enableExperimentalFriendClauses: Boolean = ConfigDefaults.DefaultEnableExperimentalFriendClauses,
                      ) {
   def shouldParse: Boolean = true
   def shouldTypeCheck: Boolean = !shouldParseOnly
@@ -349,7 +350,6 @@ trait RawConfig {
     z3APIMode = baseConfig.z3APIMode,
     disableNL = baseConfig.disableNL,
     mceMode = baseConfig.mceMode,
-    enableLazyImports = baseConfig.enableLazyImports,
     noVerify = baseConfig.noVerify,
     noStreamErrors = baseConfig.noStreamErrors,
     parseAndTypeCheckMode = baseConfig.parseAndTypeCheckMode,
@@ -359,6 +359,7 @@ trait RawConfig {
     unsafeWildcardOptimization = baseConfig.unsafeWildcardOptimization,
     moreJoins = baseConfig.moreJoins,
     respectFunctionPrePermAmounts = baseConfig.respectFunctionPrePermAmounts,
+    enableExperimentalFriendClauses = baseConfig.enableExperimentalFriendClauses,
   )
 }
 
@@ -860,6 +861,13 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     default = Some(ConfigDefaults.DefaultDisableSetAxiomatization),
     noshort = true,
   )
+
+  val enableExperimentalFriendClauses: ScallopOption[Boolean] = opt[Boolean](
+    name = "experimentalFriendClauses",
+    descr = s"Enables the use of 'friendPkg' clauses (experimental).",
+    default = Some(ConfigDefaults.DefaultEnableExperimentalFriendClauses),
+    noshort = true,
+  )
   /**
     * Exception handling
     */
@@ -887,6 +895,15 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     case _ => false
   }
 
+  addValidation {
+    val lazyImportsSet = enableLazyImports.toOption.contains(true)
+    if (lazyImportsSet) {
+      Left(s"The flag ${Config.enableLazyImportOptionPrettyPrinted} was removed in Gobra's PR #797.")
+    } else {
+      Right(())
+    }
+  }
+
   // `parallelizeBranches` requires a backend that supports branch parallelization (i.e., a silicon-based backend)
   addValidation {
     val parallelizeBranchesOn = parallelizeBranches.toOption.contains(true)
@@ -1052,7 +1069,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     z3APIMode = z3APIMode(),
     disableNL = disableNL(),
     mceMode = mceMode(),
-    enableLazyImports = enableLazyImports(),
     noVerify = noVerify(),
     noStreamErrors = noStreamErrors(),
     parseAndTypeCheckMode = parseAndTypeCheckMode(),
@@ -1062,5 +1078,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     unsafeWildcardOptimization = unsafeWildcardOptimization(),
     moreJoins = moreJoins(),
     respectFunctionPrePermAmounts = respectFunctionPrePermAmounts(),
+    enableExperimentalFriendClauses = enableExperimentalFriendClauses(),
   )
 }