From 6bea45a51509a18b9e5d056bca5a4f48cf9872e4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 23 Sep 2024 22:06:50 +0200 Subject: [PATCH] backup --- .../gobra/ast/frontend/PrettyPrinter.scala | 1 + .../scala/viper/gobra/frontend/Desugar.scala | 73 +++++++++++++++---- .../frontend/info/ExternalTypeInfo.scala | 2 + .../info/implementation/TypeInfoImpl.scala | 13 +++- 4 files changed, 75 insertions(+), 14 deletions(-) diff --git a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala index 93045ebb0..7e73be38a 100644 --- a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala +++ b/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 } diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index 0c81968b1..14f155424 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/src/main/scala/viper/gobra/frontend/Desugar.scala @@ -54,6 +54,18 @@ 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)) @@ -61,6 +73,7 @@ object Desugar extends LazyLogging { 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] = { diff --git a/src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala b/src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala index 58cabc5a9..4f2b44c58 100644 --- a/src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala +++ b/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] diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala b/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala index 85749a0a4..c81e3a908 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala +++ b/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 }