backup

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

@@ -50,6 +50,7 @@ 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 PPos(_) => emptyDoc
   }
 

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

@@ -54,13 +54,26 @@ object Desugar extends LazyLogging {
       val mainDesugaringStartMs = System.currentTimeMillis()
       // desugar the main package, i.e. the package on which verification is performed:
       val mainDesugarer = new Desugarer(pkg.positions, info, Some(importsCollector))
+
+      // register non-dup invariants of all direct imports and of the current package
+      info.getDirectlyImportedTypeInfos().foreach { i =>
+        val pkg = i.getTypeInfo.tree.originalRoot
+        val nonDupInvs = pkg.programs
+          .flatMap(_.staticInvs)
+          .filter(!_.duplicable)
+          .map(_.inv)
+          .map(mainDesugarer.specificationD(mainDesugarer.FunctionContext.empty(), i.getTypeInfo)(_))
+        importsCollector.addSelfOrImportedPkgInvariant(pkg, nonDupInvs)
+      }
+
       // registers main package to generate proof obligations for its init code
       mainDesugarer.registerMainPackage(pkg, importsCollector)(config)
       val res = (mainDesugarer, mainDesugarer.packageD(pkg))
       logger.trace {
         val durationS = f"${(System.currentTimeMillis() - mainDesugaringStartMs) / 1000f}%.1f"
         s"desugaring package ${info.pkgInfo.id} done, took ${durationS}s"
       }
+
       res
     }
 
@@ -3478,7 +3491,8 @@ object Desugar extends LazyLogging {
           .map(genCheckAssertionIsDup)
           .foreach(AdditionalMembers.addMember)
 
-        // TODO: add static tokens to main's pre
+        val mainFuncObligations = generateMainFuncObligationsModular(mainPkg, specCollector)
+        mainFuncObligations.foreach(AdditionalMembers.addMember)
       } else {
         // check that the postconditions of every package are enough to satisfy all of their imports' preconditions
         val src = meta(mainPkg, info)
@@ -3487,7 +3501,7 @@ object Desugar extends LazyLogging {
           AdditionalMembers.addMember(checkPkgImports)
         }
         // proof obligations for function main
-        val mainFuncObligations = generateMainFuncObligations(mainPkg, specCollector)
+        val mainFuncObligations = generateMainFuncObligationsNonModular(mainPkg, specCollector)
         mainFuncObligations.foreach(AdditionalMembers.addMember)
       }
     }
@@ -3576,7 +3590,7 @@ object Desugar extends LazyLogging {
         val dDups = dups.map(goA)
         val dNonDups = nonDups.map(goA)
         val _ = dNonDups
-        specCollector.addDupPkgInv(pkg, dDups)
+        specCollector.addDupPkgInvCurrentPkg(dDups)
       }
     }
 
@@ -3616,7 +3630,7 @@ object Desugar extends LazyLogging {
       *                      have been registered in `specCollector` before calling this method
       * @return
       */
-    def generateMainFuncObligations(mainPkg: PPackage, specCollector: PackageInitSpecCollector): Option[in.Function] = {
+    def generateMainFuncObligationsNonModular(mainPkg: PPackage, specCollector: PackageInitSpecCollector): Option[in.Function] = {
       val mainFuncOpt = mainPkg.declarations.collectFirst{
         case f: PFunctionDecl if f.id.name == Constants.MAIN_FUNC_NAME => f
       }
@@ -3641,6 +3655,31 @@ object Desugar extends LazyLogging {
       }
     }
 
+    def generateMainFuncObligationsModular(mainPkg: PPackage, specCollector: PackageInitSpecCollector): Option[in.Function] = {
+      val mainFuncOpt = mainPkg.declarations.collectFirst {
+        case f: PFunctionDecl if f.id.name == Constants.MAIN_FUNC_NAME => f
+      }
+      mainFuncOpt.map { mainFunc =>
+        val src = meta(mainFunc, info)
+        val mainPkgPosts = specCollector.getNonDupInvariants()
+        val mainFuncPre = mainFunc.spec.pres ++ mainFunc.spec.preserves
+        val mainFuncPreD = mainFuncPre.map(specificationD(FunctionContext.empty(), info)).map { a =>
+          a.withInfo(a.info.asInstanceOf[Source.Parser.Single].createAnnotatedInfo(MainPreNotEstablished))
+        }
+        val funcProxy = in.FunctionProxy(nm.mainFuncProofObligation(info))(src)
+        in.Function(
+          name = funcProxy,
+          args = Vector.empty,
+          results = Vector.empty,
+          pres = mainPkgPosts,
+          posts = mainFuncPreD,
+          terminationMeasures = Vector.empty,
+          backendAnnotations = Vector.empty,
+          body = Some(in.MethodBody(Vector.empty, in.MethodBodySeqn(Vector.empty)(src), Vector.empty)(src)),
+        )(src)
+      }
+    }
+
     /**
       * Generates the proof obligation for the init code in `p`. The proof obligations for the init of `p` are
       * encoded as a method that performs the following operations, in order:
@@ -4150,10 +4189,7 @@ object Desugar extends LazyLogging {
           }
         case POpenDupPkgInv() =>
           // open the current package's invariant.
-          val ppkg = info.tree.root
-          // TODO: the following map is unnecessary, we only need to keep track of the invariants in this package,
-          //  maybe simplify code
-          val dupInvs = initSpecs.get.dupPkgInvsOfPackage(ppkg)
+          val dupInvs = initSpecs.get.dupPkgInvsOfCurrentPackage()
           val inhales = dupInvs.map(i => in.Inhale(i)(src))
           val block = in.Block(Vector.empty, inhales)(src)
           unit(block)
@@ -5166,7 +5202,9 @@ object Desugar extends LazyLogging {
     // pairs of a package X and the postconditions of a program of X (one entry in the list per program of X)
     private var packagePostconditions: Vector[(PPackage, Vector[in.Assertion])] = Vector.empty
     // TODO: DOC
-    private var dupPackageInvariants: Vector[(PPackage, Vector[in.Assertion])] = Vector.empty
+    private var dupPackageInvariantsCurrentPackage: Vector[in.Assertion] = Vector.empty
+
+    private var nonDupInvariantsOfSelfOrImportedPackages: Map[PPackage, Vector[in.Assertion]] = Map.empty
 
     def addImportPres(pkg: PPackage, desugaredImportPre: Vector[in.Assertion]): Unit = {
       importPreconditions :+= (pkg, desugaredImportPre)
@@ -5184,12 +5222,21 @@ object Desugar extends LazyLogging {
       packagePostconditions.filter(_._1.info.id == pkg.info.id).flatMap(_._2)
     }
 
-    def addDupPkgInv(pkg: PPackage, desugaredInvs: Vector[in.Assertion]) = {
-      dupPackageInvariants :+= (pkg, desugaredInvs)
+    def addDupPkgInvCurrentPkg(desugaredInvs: Vector[in.Assertion]) = {
+      dupPackageInvariantsCurrentPackage = desugaredInvs
+    }
+
+    def dupPkgInvsOfCurrentPackage(): Vector[in.Assertion] = {
+      dupPackageInvariantsCurrentPackage
+    }
+
+    def addSelfOrImportedPkgInvariant(pkg: PPackage, desugaredInvs: Vector[in.Assertion]) = {
+      val curr = nonDupInvariantsOfSelfOrImportedPackages.getOrElse(pkg, Vector.empty)
+      nonDupInvariantsOfSelfOrImportedPackages = nonDupInvariantsOfSelfOrImportedPackages.updated(pkg, curr ++ desugaredInvs)
     }
 
-    def dupPkgInvsOfPackage(pkg: PPackage): Vector[in.Assertion] = {
-      dupPackageInvariants.filter(_._1.info.id == pkg.info.id).flatMap(_._2)
+    def getNonDupInvariants(): Vector[in.Assertion] = {
+      nonDupInvariantsOfSelfOrImportedPackages.values.flatten.toVector
     }
 
     def registeredPackages(): Vector[PPackage] = {

src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala

@@ -23,6 +23,8 @@ trait ExternalTypeInfo {
   def pkgInfo: PackageInfo
   def dependentTypeInfo: Map[AbstractImport, () => Either[Vector[VerifierError], ExternalTypeInfo]]
 
+  def getDirectlyImportedTypeInfos(includeThis: Boolean = true): Set[ExternalTypeInfo]
+
   /** returns this (unless disabled via parameter) and the type information of directly and transitively dependent packages */
   def getTransitiveTypeInfos(includeThis: Boolean = true): Set[ExternalTypeInfo]
 

src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala

@@ -153,7 +153,18 @@ class TypeInfoImpl(final val tree: Info.GoTree, final val dependentTypeInfo: Map
 
   override def isPureExpression(expr: PExpression): Boolean = isPureExpr(expr).isEmpty
 
-  def getTransitiveTypeInfos(includeThis: Boolean = true): Set[ExternalTypeInfo] = {
+  override def getDirectlyImportedTypeInfos(includeThis: Boolean = true): Set[ExternalTypeInfo] = {
+    val directInfos = dependentTypeInfo
+      .map { case (_, resultFn) => resultFn() }
+      .collect { case Right(info) => info }
+      .toSet
+    if (includeThis)
+      directInfos + this
+    else
+      directInfos
+  }
+
+  override def getTransitiveTypeInfos(includeThis: Boolean = true): Set[ExternalTypeInfo] = {
     val directTypeInfos = dependentTypeInfo
       .map { case (_, resultFn) => resultFn() }
       .collect { case Right(info) => info }