Package invariants

src/main/antlr4/GobraLexer.g4

@@ -85,12 +85,17 @@ 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';
+BACKEND     : '#backend';
+FRIENDPKG   : 'friendPkg';

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)* (
     (specMember | declaration | ghostMember) 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);
@@ -62,6 +65,7 @@ ghostStatement:
   | fold_stmt=(FOLD | UNFOLD) predicateAccess #foldStatement
   | kind=(ASSUME | ASSERT | REFUTE | INHALE | EXHALE) expression #proofStatement
   | matchStmt #matchStmt_
+  | OPEN_DUP_SINV #pkgInvStatement
   ;
 
 // Auxiliary statements
@@ -168,9 +172,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/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;
 
@@ -47,6 +47,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitMaybeAddressableIdentifier(GobraParser.MaybeAddressableIdentifierContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitFriendPkgDecl(GobraParser.FriendPkgDeclContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *
@@ -75,6 +82,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}
 	 *
@@ -124,6 +138,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitMatchStmt_(GobraParser.MatchStmt_Context ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitPkgInvStatement(GobraParser.PkgInvStatementContext 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;
 
@@ -40,6 +40,12 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitMaybeAddressableIdentifier(GobraParser.MaybeAddressableIdentifierContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#friendPkgDecl}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitFriendPkgDecl(GobraParser.FriendPkgDeclContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#sourceFile}.
 	 * @param ctx the parse tree
@@ -64,6 +70,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
@@ -110,6 +122,13 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitMatchStmt_(GobraParser.MatchStmt_Context ctx);
+	/**
+	 * Visit a parse tree produced by the {@code pkgInvStatement}
+	 * labeled alternative in {@link GobraParser#ghostStatement}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitPkgInvStatement(GobraParser.PkgInvStatementContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#auxiliaryStatement}.
 	 * @param ctx the parse tree

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

@@ -56,7 +56,10 @@ case class PProgram(
                      // init postconditions describe the state and resources right
                      // after this program is initialized
                      initPosts: Vector[PExpression],
+                     // TODO: doc
+                     staticInvs: Vector[PPkgInvariant],
                      imports: Vector[PImport],
+                     friends: Vector[PFriendPkgDecl],
                      declarations: Vector[PMember]
                    ) extends PNode with PUnorderedScope // imports are in program scopes
 
@@ -66,10 +69,14 @@ case class PPreamble(
                       // init postconditions describe the state and resources right
                       // after this program is initialized
                       initPosts: Vector[PExpression],
+                      // TODO: doc
+                      staticInvs: Vector[PPkgInvariant],
                       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 +131,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 +902,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
@@ -981,6 +991,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) <>
+    case PProgram(packageClause, progPosts, staticInvs, imports, friends, declarations) =>
+      showPreamble(packageClause, progPosts, staticInvs, 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)
+    case PPreamble(packageClause, progPosts, staticInvs, imports, friends, _) =>
+      showPreamble(packageClause, progPosts, staticInvs, imports, friends)
   }
 
-  private def showPreamble(packageClause: PPackageClause, progPosts: Vector[PExpression], imports: Vector[PImport]): Doc =
+  private def showPreamble(
+                            packageClause: PPackageClause,
+                            progPosts: Vector[PExpression],
+                            staticInvs: Vector[PPkgInvariant],
+                            imports: Vector[PImport],
+                            friends: Vector[PFriendPkgDecl]
+                          ): Doc =
     vcat(progPosts.map("initEnsures" <+> showExpr(_))) <>
+      vcat(staticInvs.map(showPkgInvariant)) <>
       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)) <>

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.