Package invariants #810
Package invariants #810
Conversation
| // Check that the initialization code satisfies the contract of every file in the package. | ||
| val globalDecls = sortedGlobalVariableDecls(mainPkg) | ||
| val fileInitTranslations: Vector[in.Function] = mainPkg.programs.zip(globalDecls).map { | ||
| case (p, sortedDecls) => checkProgramInitContract(p)(sortedDecls) | ||
| } | ||
| fileInitTranslations.foreach(AdditionalMembers.addMember) |
There was a problem hiding this comment.
I don't understand this.
- why are the global decls need to be sorted? Or does this return the global decls per file such that they can get zipped on the next line?
- what exactly is checked? That the per-file global vars are sufficient to satisfy the (generated) per-file init precondition and all postconditions of init functions of the package imply the package invariant?
There was a problem hiding this comment.
- in go, globals are initialized according to a dependency order (variables initialize in lexicographic order, when the variables used in the rhs of the declaration are already initialize; cyclic dependencies are disallowed). Right now, we check that variables are declared in dependency order and we need to get them in the order they execute so that the order of effectful operations to match that of the go compiler
- regarding the second question, yes (in addition, we may assume the invariants of other imported packages, as long as they have been reestablished by the end of the initialization)
| * it is ok to check the initialization of a package by separately checking the initialization of each of | ||
| * its programs. | ||
| * @param p | ||
| * @return | ||
| */ | ||
| def checkProgramInitContract(p: PProgram)(sortedGlobVarDecls: Vector[in.GlobalVarDecl]): in.Function = { |
There was a problem hiding this comment.
why is sortedGlobVarDecls a parameter? Couldn't we invoke sortedGlobalVariableDecls on p (instead of PPackage) in here?
There was a problem hiding this comment.
sortedGlobalVariableDecls returns a vector of sorted declarations (containing one element per file in the package). In this function, we pass the list of sorted files for the corresponding file (i.e., a PProgram)
| val pkgInvariantsImportedPackages: Vector[in.Assertion] = | ||
| initSpecs.getNonDupPkgInvariants().filter{ case (k, _) => k != currPkg }.values.flatten.toVector |
There was a problem hiding this comment.
I don't understand this. Doesn't initSpecs collect all package invariants? Why is it sufficient to filter out the invariants of this package? It seems that pkgInvariantsImportedPackages will contain the invariants of transitively imported packages. Is this desirable?
There was a problem hiding this comment.
yes, this collects all package invariants, even of those packages that are transitively imported. This does not impact soundness, but I agree that it is suboptimal. I changed this to filter only by packages that are directly imported
| * @return | ||
| */ | ||
| def generateMainFuncProofObligation(mainPkg: PPackage, initSpecs: PackageInitSpecCollector): Option[in.Function] = { | ||
| val mainFuncOpt = mainPkg.declarations.collectFirst { | ||
| case f: PFunctionDecl if f.id.name == Constants.MAIN_FUNC_NAME => f |
There was a problem hiding this comment.
shouldn't this also that into account that the package name is "main"? Go playground allows to write functions called "main" in non-main packages
| private var nonDupPkgInvs: Map[PPackage, Vector[in.Assertion]] = Map.empty | ||
| private var dupPkgInvs: Map[PPackage, Vector[in.Assertion]] = Map.empty | ||
|
|
||
| // Register the invariants of pkg. Each invariant is accompanied by a bool that | ||
| // is true iff the invariants are meant to be duplicable | ||
| def registerPkgInvariants(pkg: PPackage, dInvs: Vector[(in.Assertion, Boolean)]) = { | ||
| assert(!nonDupPkgInvs.contains(pkg) && !dupPkgInvs.contains(pkg)) | ||
| val (dups, nonDups) = dInvs.partitionMap { inv => | ||
| if (inv._2) Left(inv._1) else Right(inv._1) | ||
| } | ||
| dupPkgInvs += pkg -> dups | ||
| nonDupPkgInvs += pkg -> nonDups | ||
| } | ||
|
|
||
| def getNonDupPkgInvariants(): Map[PPackage, Vector[in.Assertion]] = nonDupPkgInvs | ||
| def getDupPkgInvariants(): Map[PPackage, Vector[in.Assertion]] = dupPkgInvs |
There was a problem hiding this comment.
Wouldn't it be sufficient to simply store PPackages and compute (& if necessary memoize) nonDupPkgInvs and dupPkgInvs? It seems this would result in a much simpler interface and also make clients easier to read by encapsulating more functionality in PackageInitSpecCollector
There was a problem hiding this comment.
I think this question is very related to the first one (if we move registerPkgInitData to the PackageInitSpecCollector class, we end up effectively doing this). Once again, the reason I didn't do this is that I wanted PackageInitSpecCollector to act only as a store of simple metadata, instead of having more complicated desugaring logic here.
Co-authored-by: Linard Arquint <ArquintL@users.noreply.github.com>
Co-authored-by: Linard Arquint <ArquintL@users.noreply.github.com>
Co-authored-by: Linard Arquint <ArquintL@users.noreply.github.com>
Co-authored-by: Linard Arquint <ArquintL@users.noreply.github.com>
Co-authored-by: Linard Arquint <ArquintL@users.noreply.github.com>
Co-authored-by: Linard Arquint <ArquintL@users.noreply.github.com>
|
@ArquintL I have addressed your comments, please take a look at this when you find the time |
Changelog:
openDupPkgInvto open the duplicable invariants of the current package if initialization is guaranteed to be finished, and we introduce all necessary proof obligations for theinitfunctions andmainfunction.mayInit) to make sure we never open invariants that might not hold yet - more details on this sooninitEnsuresclauses to allow for modularly checking a package. We also deprecate the--lazyImportsflag, as it is no longer necessary: If the package under verification does not declare any package invariants norinitRequiresclauses, then nothing is checked for that package. Because our methodology is now modular, we do not have to re-check initialization of all imported packages.same_package/import-fail01/mainfails non-deterministically #762Minor TODOs:
--enableFriendClauses