Skip to content

Commit

Permalink
backup
Browse files Browse the repository at this point in the history
jcp19 committed Sep 23, 2024
1 parent 5040a93 commit 34d880e
Showing 11 changed files with 189 additions and 50 deletions.
7 changes: 7 additions & 0 deletions src/main/scala/viper/gobra/ast/frontend/Ast.scala
Original file line number Diff line number Diff line change
@@ -56,6 +56,8 @@ 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],
declarations: Vector[PMember]
) extends PNode with PUnorderedScope // imports are in program scopes
@@ -66,10 +68,13 @@ 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],
positions: PositionManager,
) extends PNode with PUnorderedScope

case class PPkgInvariant(inv: PExpression, duplicable: Boolean) extends PNode

class PositionManager(val positions: Positions) extends Messaging(positions) {

@@ -981,6 +986,8 @@ case class PFold(exp: PPredicateAccess) extends PGhostStatement with PDeferrable

case class PUnfold(exp: PPredicateAccess) extends PGhostStatement with PDeferrable

case class POpenDupPkgInv(id: String) extends PGhostStatement with PDeferrable

case class PPackageWand(wand: PMagicWand, proofScript: Option[PBlock]) extends PGhostStatement

case class PApplyWand(wand: PMagicWand) extends PGhostStatement
17 changes: 12 additions & 5 deletions src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala
Original file line number Diff line number Diff line change
@@ -61,23 +61,30 @@ 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, declarations) =>
showPreamble(packageClause, progPosts, staticInvs, imports) <>
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, _) =>
showPreamble(packageClause, progPosts, staticInvs, imports)
}

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]): Doc =
vcat(progPosts.map("initEnsures" <+> showExpr(_))) <>
vcat(staticInvs.map(showPkgInvariant)) <>
showPackageClause(packageClause) <> 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)
6 changes: 6 additions & 0 deletions src/main/scala/viper/gobra/ast/internal/Program.scala
Original file line number Diff line number Diff line change
@@ -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.
2 changes: 1 addition & 1 deletion src/main/scala/viper/gobra/frontend/Config.scala
Original file line number Diff line number Diff line change
@@ -229,7 +229,7 @@ case class Config(
disableCheckTerminationPureFns = disableCheckTerminationPureFns || other.disableCheckTerminationPureFns,
unsafeWildcardOptimization = unsafeWildcardOptimization && other.unsafeWildcardOptimization,
moreJoins = MoreJoins.merge(moreJoins, other.moreJoins),
enableModularInit = enableModularInit && other.enableModularInit,
enableModularInit = enableModularInit || other.enableModularInit,
)
}

147 changes: 117 additions & 30 deletions src/main/scala/viper/gobra/frontend/Desugar.scala
Original file line number Diff line number Diff line change
@@ -8,6 +8,7 @@ package viper.gobra.frontend

import com.typesafe.scalalogging.LazyLogging
import viper.gobra.ast.frontend.{PExpression, AstPattern => ap, _}
import viper.gobra.ast.internal.{MethodBody, MethodBodySeqn}
import viper.gobra.ast.{internal => in}
import viper.gobra.frontend.PackageResolver.RegularImport
import viper.gobra.frontend.Source.TransformableSource
@@ -42,8 +43,8 @@ object Desugar extends LazyLogging {
val importedDesugaringStartMs = System.currentTimeMillis()
val typeInfo = tI.getTypeInfo
val importedPackage = typeInfo.tree.originalRoot
val d = new Desugarer(importedPackage.positions, typeInfo)
// registers a package to generate proof obligations for its init code
val d = new Desugarer(importedPackage.positions, typeInfo, None)
// registers a package to generate proof obligations for its init code.
d.registerPackage(importedPackage, importsCollector)(config)
val res = (d, d.packageD(importedPackage))
importedDesugaringDurationMs.addAndGet(System.currentTimeMillis() - importedDesugaringStartMs)
@@ -53,7 +54,7 @@ object Desugar extends LazyLogging {
val mainPackageFut = Future {
val mainDesugaringStartMs = System.currentTimeMillis()
// desugar the main package, i.e. the package on which verification is performed:
val mainDesugarer = new Desugarer(pkg.positions, info)
val mainDesugarer = new Desugarer(pkg.positions, info, Some(importsCollector))
// registers main package to generate proof obligations for its init code
mainDesugarer.registerMainPackage(pkg, importsCollector)(config)
val res = (mainDesugarer, mainDesugarer.packageD(pkg))
@@ -186,7 +187,7 @@ object Desugar extends LazyLogging {
}
}

private class Desugarer(pom: PositionManager, info: viper.gobra.frontend.info.TypeInfo) {
private class Desugarer(pom: PositionManager, info: viper.gobra.frontend.info.TypeInfo, initSpecs: Option[PackageInitSpecCollector]) {

// TODO: clean initialization

@@ -3457,6 +3458,10 @@ object Desugar extends LazyLogging {
// postconditions in the type checker, which means that we do not have to generate an init proof.
registerPackage(mainPkg, specCollector, generateInitProof = !config.enableLazyImports)(config)

// TODO: register maping from names from paths to PPkg in specCollector:
mainPkg.programs.map(_.imports)


if (config.enableLazyImports) {
// early return to not add any proof obligations because we have made sure in the type checker that
// there aren't any global variables, init blocks, init postconditions, and import preconditions (in the
@@ -3465,16 +3470,44 @@ object Desugar extends LazyLogging {
return
}

// check that the postconditions of every package are enough to satisfy all of their imports' preconditions
val src = meta(mainPkg, info)
specCollector.registeredPackages().foreach{ pkg =>
val checkPkgImports = checkPkgImportObligations(pkg, specCollector)(src)
AdditionalMembers.addMember(checkPkgImports)
if (config.enableModularInit) {
// Check that all duplicable static invariants are actually duplicable.
mainPkg.programs
.flatMap(_.staticInvs)
.filter(_.duplicable)
.map(_.inv)
.map(genCheckAssertionIsDup)
.foreach(AdditionalMembers.addMember)

// TODO: add static tokens to main's pre
} else {
// check that the postconditions of every package are enough to satisfy all of their imports' preconditions
val src = meta(mainPkg, info)
specCollector.registeredPackages().foreach { pkg =>
val checkPkgImports = checkPkgImportObligations(pkg, specCollector)(src)
AdditionalMembers.addMember(checkPkgImports)
}
// proof obligations for function main
val mainFuncObligations = generateMainFuncObligations(mainPkg, specCollector)
mainFuncObligations.foreach(AdditionalMembers.addMember)
}
}

// proof obligations for function main
val mainFuncObligations = generateMainFuncObligations(mainPkg, specCollector)
mainFuncObligations.foreach(AdditionalMembers.addMember)
// TODO: doc
def genCheckAssertionIsDup(e: PExpression): in.Function = {
val src = meta(e, info)
val assertion = specificationD(FunctionContext.empty(), info)(e)
val funcProxy = in.FunctionProxy(nm.dupPkgInv())(src)
in.Function(
name = funcProxy,
args = Vector.empty,
results = Vector.empty,
pres = Vector(assertion),
posts = Vector(assertion, assertion),
terminationMeasures = Vector.empty,
backendAnnotations = Vector.empty,
body = Some(MethodBody.empty(src))
)(src)
}

/**
@@ -3516,22 +3549,36 @@ object Desugar extends LazyLogging {
fileInitTranslations.foreach(AdditionalMembers.addMember)
}

// Collect and register all import-preconditions
pkg.imports.foreach{ imp => {
val importedPackage = RegularImport(imp.importPath)
Violation.violation(info.dependentTypeInfo.contains(importedPackage), s"Desugarer expects to have acess to the type information of all imported packages but could not find $importedPackage")
info.dependentTypeInfo(importedPackage)() match {
case Right(tI) =>
val desugaredPre = imp.importPres.map(specificationD(FunctionContext.empty(), info))
Violation.violation(!config.enableLazyImports || desugaredPre.isEmpty, s"Import precondition found despite running with ${Config.enableLazyImportOptionPrettyPrinted}")
specCollector.addImportPres(tI.getTypeInfo.tree.originalRoot, desugaredPre)
case e => Violation.violation(config.enableLazyImports, s"Unexpected value found $e while importing ${imp.importPath} - type information is assumed to be available for all packages when Gobra is executed with lazy imports disabled")
}
}}
// The following registers all import-preconditions and init-postconditions.
// This only needs to be done if we are using the non-modular encoding for
// static-init. For the modular encoding, all necessary information will be
// obtained from the main package.
if (!config.enableModularInit) {
// Collect and register all import-preconditions
pkg.imports.foreach { imp => {
val importedPackage = RegularImport(imp.importPath)
Violation.violation(info.dependentTypeInfo.contains(importedPackage), s"Desugarer expects to have acess to the type information of all imported packages but could not find $importedPackage")
info.dependentTypeInfo(importedPackage)() match {
case Right(tI) =>
val desugaredPre = imp.importPres.map(specificationD(FunctionContext.empty(), info))
Violation.violation(!config.enableLazyImports || desugaredPre.isEmpty, s"Import precondition found despite running with ${Config.enableLazyImportOptionPrettyPrinted}")
specCollector.addImportPres(tI.getTypeInfo.tree.originalRoot, desugaredPre)
case e => Violation.violation(config.enableLazyImports, s"Unexpected value found $e while importing ${imp.importPath} - type information is assumed to be available for all packages when Gobra is executed with lazy imports disabled")
}
}}

// Collect and register all postconditions of all PPrograms (i.e., files) in pkg
val pkgPost = pkg.programs.flatMap(_.initPosts).map(specificationD(FunctionContext.empty(), info))
specCollector.addPackagePosts(pkg, pkgPost)
// Collect and register all postconditions of all PPrograms (i.e., files) in pkg
val pkgPost = pkg.programs.flatMap(_.initPosts).map(specificationD(FunctionContext.empty(), info))
specCollector.addPackagePosts(pkg, pkgPost)
} else {
val partitionFunc = (inv: PPkgInvariant) => if (inv.duplicable) Left(inv.inv) else Right(inv.inv)
val (dups, nonDups) = pkg.programs.flatMap(_.staticInvs).partitionMap(partitionFunc)
val goA = specificationD(FunctionContext.empty(), info)(_)
val dDups = dups.map(goA)
val dNonDups = nonDups.map(goA)
val _ = dNonDups
specCollector.addDupPkgInv(pkg, dDups)
}
}

/**
@@ -3604,9 +3651,13 @@ object Desugar extends LazyLogging {
* as long as dependency order is respected.
* - execute all inits in the current file in the order they appear
* - exhale all post-conditions of the file
* Notice that these operations enforce non-interference between two different files in the same program. Thus,
* - exhale all package-invariants of the file
* Note 1: these operations enforce non-interference between two different files in the same program. Thus,
* it is ok to check the initialization of a package by separately checking the initialization of each of
* its programs.
* Note 2: if the flag `enableModularInit` is true, there will be no import preconditions and init postconditions.
* If it is false, there will be no package invariants. Thus, this method works for both the modular and
* non-modular termination checks.
* @param p
* @return
*/
@@ -3616,15 +3667,17 @@ object Desugar extends LazyLogging {
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)}

in.Function(
name = funcProxy,
args = Vector(),
results = Vector(),
// inhales all preconditions in the imports of the current file
pres = progPres,
// exhales all package postconditions in the current file
posts = progPosts,
// exhales all package postconditions and pkg invariants from the current file
posts = progPosts ++ pkgInvariants,
// in our verification approach, the initialization code must be proven to terminate
terminationMeasures = Vector(in.TupleTerminationMeasure(Vector(), None)(src)),
backendAnnotations = Vector.empty,
@@ -4096,6 +4149,23 @@ object Desugar extends LazyLogging {
} yield in.PredExprUnfold(predExpInstance.base.asInstanceOf[in.PredicateConstructor], args, access.p)(src)
case _ => for {e <- goA(exp)} yield in.Unfold(e.asInstanceOf[in.Access])(src)
}
case POpenDupPkgInv(pkgId) =>
val currPkgName = info.pkgName.name
val thisPkg = info.tree.root
val ppkg = pkgId match {
case `currPkgName` =>
thisPkg
case _ =>
// TODO: explain this hack - we require the full path, getting the pkg
// from its qualifier is very hard because the desugarer does not know which
// PProgram it is currently looking at
// thisPkg.programs.flatMap(_.imports).filter(_.importPath == pkgId)
???
}
val dupInvs = initSpecs.get.dupPkgInvsOfPackage(ppkg)
val inhales = dupInvs.map(i => in.Inhale(i)(src))
val block = in.Block(Vector.empty, inhales)(src)
unit(block)
case PPackageWand(wand, blockOpt) =>
for {
w <- goA(wand)
@@ -4854,6 +4924,7 @@ object Desugar extends LazyLogging {
private val PROGRAM_INIT_CODE_PREFIX = "$INIT"
private val PACKAGE_IMPORT_OBLIGATIONS_PREFIX = "$IMPORTS"
private val MAIN_FUNC_OBLIGATIONS_PREFIX = "$CHECKMAIN"
private val CHECK_PKG_INV_IS_DUP = "$IS_DUP"
private val INTERFACE_PREFIX = "Y"
private val DOMAIN_PREFIX = "D"
private val ADT_PREFIX = "ADT"
@@ -4880,6 +4951,8 @@ object Desugar extends LazyLogging {
*/
private var scopeMap: Map[PScope, Int] = Map.empty

private var dupInvCounter = 0

private def maybeRegister(s: PScope, ctx: ExternalTypeInfo): Unit = {
if (!(scopeMap contains s)) {
val codeRoot = ctx.codeRoot(s)
@@ -4922,6 +4995,10 @@ object Desugar extends LazyLogging {
val hashedId = Names.hash(p.info.id)
topLevelName(hashedId)(PACKAGE_IMPORT_OBLIGATIONS_PREFIX, context)
}
def dupPkgInv(): String = {
dupInvCounter += 1
s"$CHECK_PKG_INV_IS_DUP$dupInvCounter"
}
def mainFuncProofObligation(context: ExternalTypeInfo): String =
topLevelName(MAIN_FUNC_OBLIGATIONS_PREFIX)(Constants.MAIN_FUNC_NAME, context)
def variable(n: String, s: PScope, context: ExternalTypeInfo): String = name(VARIABLE_PREFIX)(n, s, context)
@@ -5097,6 +5174,8 @@ object Desugar extends LazyLogging {
private var importPreconditions: Vector[(PPackage, Vector[in.Assertion])] = Vector.empty
// 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

def addImportPres(pkg: PPackage, desugaredImportPre: Vector[in.Assertion]): Unit = {
importPreconditions :+= (pkg, desugaredImportPre)
@@ -5114,6 +5193,14 @@ 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 dupPkgInvsOfPackage(pkg: PPackage): Vector[in.Assertion] = {
dupPackageInvariants.filter(_._1.info.id == pkg.info.id).flatMap(_._2)
}

def registeredPackages(): Vector[PPackage] = {
// the domain of package posts should have all registered packages
packagePostconditions.map(_._1).distinct
Loading

0 comments on commit 34d880e

Please sign in to comment.