backup

src/main/antlr4/GobraLexer.g4

@@ -97,4 +97,5 @@ WITH        : 'with';
 OPAQUE      : 'opaque' -> mode(NLSEMI);
 MAYINIT     : 'mayInit' -> mode(NLSEMI);
 REVEAL      : 'reveal';
-BACKEND     : '#backend';
+BACKEND     : '#backend';
+FRIENDPKG   : 'friendPkg';

src/main/antlr4/GobraParser.g4

@@ -31,15 +31,17 @@ maybeAddressableIdentifierList: maybeAddressableIdentifier (COMMA maybeAddressab
 
 maybeAddressableIdentifier: IDENTIFIER ADDR_MOD?;
 
+friendPkgDecl: FRIENDPKG importPath assertion;
+
 // Ghost members
 sourceFile:
-   (pkgInvariant eos)* (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: (pkgInvariant eos)* (initPost eos)* packageClause eos (importDecl eos)*;
+preamble: (pkgInvariant eos)* (initPost eos)* packageClause eos (friendPkgDecl eos)* (importDecl eos)*;
 
 initPost: INIT_POST expression;
 

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

@@ -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}
 	 *

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

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

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

@@ -59,6 +59,7 @@ case class PProgram(
                      // TODO: doc
                      staticInvs: Vector[PPkgInvariant],
                      imports: Vector[PImport],
+                     friends: Vector[PFriendPkgDecl],
                      declarations: Vector[PMember]
                    ) extends PNode with PUnorderedScope // imports are in program scopes
 
@@ -71,6 +72,7 @@ case class PPreamble(
                       // TODO: doc
                       staticInvs: Vector[PPkgInvariant],
                       imports: Vector[PImport],
+                      friends: Vector[PFriendPkgDecl],
                       positions: PositionManager,
                     ) extends PNode with PUnorderedScope
 
@@ -129,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

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

@@ -51,6 +51,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case n: PBodyParameterInfo => showBodyParameterInfo(n)
     case n: PTerminationMeasure => showTerminationMeasure(n)
     case n: PPkgInvariant => showPkgInvariant(n)
+    case n: PFriendPkgDecl => showFriend(n)
     case PPos(_) => emptyDoc
   }
 
@@ -62,22 +63,29 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   // program
 
   def showProgram(p: PProgram): Doc = p match {
-    case PProgram(packageClause, progPosts, staticInvs, imports, declarations) =>
-      showPreamble(packageClause, progPosts, staticInvs, 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, staticInvs, imports, _) =>
-      showPreamble(packageClause, progPosts, staticInvs, imports)
+    case PPreamble(packageClause, progPosts, staticInvs, imports, friends, _) =>
+      showPreamble(packageClause, progPosts, staticInvs, imports, friends)
   }
 
-  private def showPreamble(packageClause: PPackageClause, progPosts: Vector[PExpression], staticInvs: Vector[PPkgInvariant], 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 = {
@@ -107,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 {

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

@@ -10,7 +10,7 @@ import com.typesafe.scalalogging.LazyLogging
 import viper.gobra.ast.frontend.{PExpression, AstPattern => ap, _}
 import viper.gobra.ast.{internal => in}
 import viper.gobra.frontend.PackageResolver.RegularImport
-import viper.gobra.frontend.Source.TransformableSource
+import viper.gobra.frontend.Source.{TransformableSource, uniquePath}
 import viper.gobra.frontend.info.base.BuiltInMemberTag._
 import viper.gobra.frontend.info.base.Type._
 import viper.gobra.frontend.info.base.{BuiltInMemberTag, Type, SymbolTable => st}
@@ -23,6 +23,7 @@ import viper.gobra.translator.Names
 import viper.gobra.util.Violation.violation
 import viper.gobra.util.{BackendAnnotation, Constants, DesugarWriter, GobraExecutionContext, Violation}
 
+import java.nio.file.Paths
 import java.util.concurrent.atomic.AtomicLong
 import scala.annotation.{tailrec, unused}
 import scala.collection.{Iterable, SortedSet}
@@ -3556,7 +3557,7 @@ object Desugar extends LazyLogging {
       if (generateInitProof) {
         // Check that the initialization code satisfies the contract of every file in the package.
         val fileInitTranslations: Vector[in.Function] = pkg.programs.zip(globalDecls).map {
-          case (p, sortedDecls) => checkProgramInitContract(p)(sortedDecls)
+          case (p, sortedDecls) => checkProgramInitContract(p)(sortedDecls)(config)
         }
         fileInitTranslations.foreach(AdditionalMembers.addMember)
       }
@@ -3698,28 +3699,51 @@ object Desugar extends LazyLogging {
       * @param p
       * @return
       */
-    def checkProgramInitContract(p: PProgram)(sortedGlobVarDecls: Vector[in.GlobalVarDecl]): in.Function = {
+    def checkProgramInitContract(p: PProgram)(sortedGlobVarDecls: Vector[in.GlobalVarDecl])(config: Config): in.Function = {
       // all errors found during init are reported in the package clause of the file
       val src = meta(p.packageClause, info)
       val funcProxy = in.FunctionProxy(nm.programInit(p, info))(src)
       val progPres: Vector[in.Assertion] = p.imports.flatMap(_.importPres).map(specificationD(FunctionContext.empty(), info)(_))
       val progPosts: Vector[in.Assertion] = p.initPosts.map(specificationD(FunctionContext.empty(), info)(_))
-      val pkgInvariants: Vector[in.Assertion] =
-        p.staticInvs.map{i => specificationD(FunctionContext.empty(), info)(i.inv)}
+      val pkgInvariants: Vector[in.Assertion] = p.staticInvs.map{i => specificationD(FunctionContext.empty(), info)(i.inv)}
+      // val friendPkgAssertions: Vector[in.Assertion] = p.friends.map{i => specificationD(FunctionContext.empty(), info)(i.assertion)}
       val pkgInvariantsImportedPackages: Vector[in.Assertion] =
         initSpecs match {
           case Some(initSpecs) => initSpecs.getNonDupInvariantsImportedPkgs()
           case None => Vector.empty
         }
 
+      // TODO: the following is only sound while there is a single init function per-package, otherwise, we might have
+      //  multiple blocks inhaling the "same" resource. The solution to this is to adopt preconditions for init functions
+      //  and introduce a proof obligation that all package invariants of imported packages (together with
+      //  the friendPkg declarations destined at the current package) imply the conjunction of all init preconditions.
+
+      val currPkg = info.tree.originalRoot
+      val uniquePathPkg = currPkg.info.id
+      // val resourcesFromFriendPkgs: Vector[in.Assertion] = Vector.empty
+
+      println(s"unique: ${currPkg.info.id}")
+      val resourcesFromFriendPkgs = info.getDirectlyImportedTypeInfos(false).flatMap { pp =>
+        val pkg = pp.getTypeInfo.tree.originalRoot
+        pkg.programs.flatMap(_.friends).filter{ i: PFriendPkgDecl =>
+          // Check if the import path corresponds to current package
+          val unique = uniquePath(Paths.get(i.path), config.projectRoot)
+          println(s"Unique from friend: $unique")
+          unique == uniquePathPkg
+        }.map(_.assertion).map(specificationD(FunctionContext.empty(), info)(_))
+      }
+
+      println(s"resources: $resourcesFromFriendPkgs")
+
+
       in.Function(
         name = funcProxy,
         args = Vector(),
         results = Vector(),
         // inhales all preconditions in the imports of the current file
         pres = progPres ++ pkgInvariantsImportedPackages, // TODO: doc
         // exhales all package postconditions and pkg invariants from the current file
-        posts = progPosts ++ pkgInvariantsImportedPackages ++ pkgInvariants, // TODO: doc
+        posts = progPosts ++ pkgInvariantsImportedPackages ++ pkgInvariants ++ resourcesFromFriendPkgs, // TODO: doc
         // in our verification approach, the initialization code must be proven to terminate
         terminationMeasures = Vector(in.TupleTerminationMeasure(Vector(), None)(src)),
         backendAnnotations = Vector.empty,

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

@@ -2185,7 +2185,14 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     POpenDupPkgInv().at(ctx)
   }
 
-  /**
+  override def visitFriendPkgDecl(ctx: FriendPkgDeclContext): PFriendPkgDecl = {
+    val path = visitString_(ctx.importPath().string_()).lit
+    val assertion = visitNode[PExpression](ctx.assertion())
+    PFriendPkgDecl(path, assertion).at(ctx)
+  }
+
+
+    /**
     * Visits the production
     * kind=(ASSUME | ASSERT | INHALE | EXHALE) expression
     *     */
@@ -2257,19 +2264,22 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     val initPosts: Vector[PExpression] = visitListNode[PExpression](ctx.initPost())
     val staticInvs: Vector[PPkgInvariant] = visitListNode[PPkgInvariant](ctx.pkgInvariant())
     val importDecls = ctx.importDecl().asScala.toVector.flatMap(visitImportDecl)
+    val friendPkgs: Vector[PFriendPkgDecl] = visitListNode[PFriendPkgDecl](ctx.friendPkgDecl())
+
     // Don't parse functions/methods if the identifier is blank
     val members = visitListNode[PMember](ctx.specMember())
     val ghostMembers = ctx.ghostMember().asScala.flatMap(visitNode[Vector[PGhostMember]])
     val decls = ctx.declaration().asScala.toVector.flatMap(visitDeclaration(_).asInstanceOf[Vector[PDeclaration]])
-    PProgram(packageClause, initPosts, staticInvs, importDecls, members ++ decls ++ ghostMembers).at(ctx)
+    PProgram(packageClause, initPosts, staticInvs, importDecls, friendPkgs, members ++ decls ++ ghostMembers).at(ctx)
   }
 
   override def visitPreamble(ctx: GobraParser.PreambleContext): PPreamble = {
     val packageClause: PPackageClause = visitNode(ctx.packageClause())
     val initPosts: Vector[PExpression] = visitListNode[PExpression](ctx.initPost())
     val staticInvs: Vector[PPkgInvariant] = visitListNode[PPkgInvariant](ctx.pkgInvariant())
     val importDecls = ctx.importDecl().asScala.toVector.flatMap(visitImportDecl)
-    PPreamble(packageClause, initPosts, staticInvs, importDecls, pom).at(ctx)
+    val friendPkgs: Vector[PFriendPkgDecl] = visitListNode[PFriendPkgDecl](ctx.friendPkgDecl())
+    PPreamble(packageClause, initPosts, staticInvs, importDecls, friendPkgs, pom).at(ctx)
   }
 
   /**

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

@@ -461,7 +461,7 @@ object Parser extends LazyLogging {
         // note that the resolveImports strategy could be embedded in e.g. a logfail strategy to report a
         // failed strategy application
         val updatedImports = rewrite(topdown(attempt(resolveImports)))(prog.imports)
-        PProgram(prog.packageClause, prog.initPosts, prog.staticInvs, updatedImports, prog.declarations).at(prog)
+        PProgram(prog.packageClause, prog.initPosts, prog.staticInvs, updatedImports, prog.friends, prog.declarations).at(prog)
       })
       // create a new package node with the updated programs
       val updatedPkg = PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info).at(pkg)
@@ -509,7 +509,7 @@ object Parser extends LazyLogging {
         // apply the replaceTerminationMeasuresForFunctionsAndMethods to declarations until the strategy has succeeded
         // (i.e. has reached PMember nodes) and stop then
         val updatedDecls = rewrite(alltd(replaceTerminationMeasuresForFunctionsAndMethods))(prog.declarations)
-        PProgram(prog.packageClause, prog.initPosts, prog.staticInvs, prog.imports, updatedDecls).at(prog)
+        PProgram(prog.packageClause, prog.initPosts, prog.staticInvs, prog.imports, prog.friends, updatedDecls).at(prog)
       })
       // create a new package node with the updated programs
       Right(PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info).at(pkg))

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 p@PProgram(_, posts, staticInvs, imports, members) =>
+    case p@PProgram(_, posts, staticInvs, imports, _, members) =>
       if (config.enableLazyImports) {
         posts.flatMap(post => message(post, s"Init postconditions are not allowed when executing ${GoVerifier.name} with ${Config.enableLazyImportOptionPrettyPrinted}")) ++
         staticInvs.flatMap(inv => message(inv, s"Package invariants are not allowed when executing ${GoVerifier.name} with ${Config.enableLazyImportOptionPrettyPrinted}"))