diff --git a/.gitignore b/.gitignore index a61e52403..cc42e26ab 100644 --- a/.gitignore +++ b/.gitignore @@ -5,6 +5,7 @@ project/target/ target/ tmp/ sync/ +gobra_tmp/ logger.log .DS_Store diff --git a/src/main/antlr4/GobraLexer.g4 b/src/main/antlr4/GobraLexer.g4 index b5e92eb5f..9e4cae32a 100644 --- a/src/main/antlr4/GobraLexer.g4 +++ b/src/main/antlr4/GobraLexer.g4 @@ -85,6 +85,9 @@ WRITEPERM : 'writePerm' -> mode(NLSEMI); NOPERM : 'noPerm' -> mode(NLSEMI); TRUSTED : 'trusted' -> mode(NLSEMI); OUTLINE : 'outline'; +DUPLICABLE : 'dup'; +PKG_INV : 'pkgInvariant'; +OPEN_DUP_SINV : 'openDupPkgInv' -> mode(NLSEMI); INIT_POST : 'initEnsures'; IMPORT_PRE : 'importRequires'; PROOF : 'proof'; @@ -92,5 +95,7 @@ GHOST_EQUALS : '==='; GHOST_NOT_EQUALS : '!=='; WITH : 'with'; OPAQUE : 'opaque' -> mode(NLSEMI); +MAYINIT : 'mayInit' -> mode(NLSEMI); REVEAL : 'reveal'; -BACKEND : '#backend'; \ No newline at end of file +BACKEND : '#backend'; +FRIENDPKG : 'friendPkg'; \ No newline at end of file diff --git a/src/main/antlr4/GobraParser.g4 b/src/main/antlr4/GobraParser.g4 index df2b51739..ebfa6dacb 100644 --- a/src/main/antlr4/GobraParser.g4 +++ b/src/main/antlr4/GobraParser.g4 @@ -31,21 +31,24 @@ maybeAddressableIdentifierList: maybeAddressableIdentifier (COMMA maybeAddressab maybeAddressableIdentifier: IDENTIFIER ADDR_MOD?; -// Ghost members +friendPkgDecl: FRIENDPKG importPath assertion; +// Ghost members sourceFile: - (initPost eos)* packageClause eos (importDecl eos)* ( + (pkgInvariant eos)* (initPost eos)* packageClause eos (friendPkgDecl eos)* (importDecl eos)* ( member 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: (initPost eos)* packageClause eos (importDecl eos)*; +preamble: (pkgInvariant eos)* (initPost eos)* packageClause eos (friendPkgDecl eos)* (importDecl eos)*; initPost: INIT_POST expression; importPre: IMPORT_PRE expression; +pkgInvariant: DUPLICABLE? PKG_INV assertion; + importSpec: (importPre eos)* alias = (DOT | IDENTIFIER)? importPath; importDecl: (importPre eos)* (IMPORT importSpec | IMPORT L_PAREN (importSpec eos)* R_PAREN); @@ -64,6 +67,7 @@ ghostStatement: | fold_stmt=(FOLD | UNFOLD) predicateAccess #foldStatement | kind=(ASSUME | ASSERT | REFUTE | INHALE | EXHALE) expression #proofStatement | matchStmt #matchStmt_ + | OPEN_DUP_SINV #pkgInvStatement ; // Auxiliary statements @@ -172,9 +176,9 @@ sqType: (kind=(SEQ | SET | MSET | OPT) L_BRACKET type_ R_BRACKET) // Specifications -specification returns[boolean trusted = false, boolean pure = false, boolean opaque = false;]: +specification returns[boolean trusted = false, boolean pure = false, boolean mayInit = false, boolean opaque = false;]: // Non-greedily match PURE to avoid missing eos errors. - ((specStatement | OPAQUE {$opaque = true;} | PURE {$pure = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? backendAnnotation? + ((specStatement | OPAQUE {$opaque = true;} | PURE {$pure = true;} | MAYINIT {$mayInit = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? backendAnnotation? ; backendAnnotationEntry: ~('('|')'|',')+; diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala index 1e83156a9..6f4ad7114 100644 --- a/src/main/scala/viper/gobra/ast/frontend/Ast.scala +++ b/src/main/scala/viper/gobra/ast/frontend/Ast.scala @@ -53,23 +53,22 @@ case class PPackage( case class PProgram( packageClause: PPackageClause, - // init postconditions describe the state and resources right - // after this program is initialized - initPosts: Vector[PExpression], + pkgInvariants: Vector[PPkgInvariant], imports: Vector[PImport], + friends: Vector[PFriendPkgDecl], declarations: Vector[PMember] ) extends PNode with PUnorderedScope // imports are in program scopes case class PPreamble( packageClause: PPackageClause, - // init postconditions describe the state and resources right - // after this program is initialized - initPosts: Vector[PExpression], + pkgInvariants: Vector[PPkgInvariant], imports: Vector[PImport], + friends: Vector[PFriendPkgDecl], positions: PositionManager, ) extends PNode with PUnorderedScope +case class PPkgInvariant(inv: PExpression, duplicable: Boolean) extends PNode class PositionManager(val positions: Positions) extends Messaging(positions) { @@ -124,6 +123,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 @@ -893,6 +894,7 @@ case class PFunctionSpec( isPure: Boolean = false, isTrusted: Boolean = false, isOpaque: Boolean = false, + mayBeUsedInInit: Boolean = false, ) extends PSpecification case class PBackendAnnotation(key: String, values: Vector[String]) extends PGhostMisc @@ -981,6 +983,8 @@ case class PFold(exp: PPredicateAccess) extends PGhostStatement with PDeferrable case class PUnfold(exp: PPredicateAccess) extends PGhostStatement with PDeferrable +case class POpenDupPkgInv() extends PGhostStatement with PDeferrable + case class PPackageWand(wand: PMagicWand, proofScript: Option[PBlock]) extends PGhostStatement case class PApplyWand(wand: PMagicWand) extends PGhostStatement diff --git a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala index 7ceebfc79..e1aab27ed 100644 --- a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala +++ b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala @@ -50,6 +50,8 @@ 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 n: PFriendPkgDecl => showFriend(n) case PPos(_) => emptyDoc } @@ -61,23 +63,35 @@ 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, pkgInvs, imports, friends, declarations) => + showPreamble(packageClause, pkgInvs, imports, friends) <> 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, pkgInvs, imports, friends, _) => + showPreamble(packageClause, pkgInvs, imports, friends) } - private def showPreamble(packageClause: PPackageClause, progPosts: Vector[PExpression], imports: Vector[PImport]): Doc = - vcat(progPosts.map("initEnsures" <+> showExpr(_))) <> + private def showPreamble( + packageClause: PPackageClause, + pkgInvs: Vector[PPkgInvariant], + imports: Vector[PImport], + friends: Vector[PFriendPkgDecl] + ): Doc = + vcat(pkgInvs.map(showPkgInvariant)) <> showPackageClause(packageClause) <> line <> line <> + ssep(friends map showFriend, 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) @@ -99,6 +113,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 { @@ -130,6 +149,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter def showPure: Doc = "pure" <> line def showOpaque: Doc = "opaque" <> line def showTrusted: Doc = "trusted" <> line + def showMayInit: Doc = "mayInit" <> line def showPre(pre: PExpression): Doc = "requires" <+> showExpr(pre) def showPreserves(preserves: PExpression): Doc = "preserves" <+> showExpr(preserves) def showPost(post: PExpression): Doc = "ensures" <+> showExpr(post) @@ -144,10 +164,11 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter } def showSpec(spec: PSpecification): Doc = spec match { - case PFunctionSpec(pres, preserves, posts, measures, backendAnnotations, isPure, isTrusted, isOpaque) => + case PFunctionSpec(pres, preserves, posts, measures, backendAnnotations, isPure, isTrusted, isOpaque, mayInit) => (if (isPure) showPure else emptyDoc) <> (if (isOpaque) showOpaque else emptyDoc) <> (if (isTrusted) showTrusted else emptyDoc) <> + (if (mayInit) showMayInit else emptyDoc) <> hcat(pres map (showPre(_) <> line)) <> hcat(preserves map (showPreserves(_) <> line)) <> hcat(posts map (showPost(_) <> line)) <> @@ -292,6 +313,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter case PFold(exp) => "fold" <+> showExpr(exp) case PPackageWand(wand, blockOpt) => "package" <+> showExpr(wand) <+> opt(blockOpt)(showStmt) case PApplyWand(wand) => "apply" <+> showExpr(wand) + case POpenDupPkgInv() => "openDupPkgInv" case PMatchStatement(exp, clauses, _) => "match" <+> showExpr(exp) <+> block(ssep(clauses map showMatchClauseStatement, line)) } diff --git a/src/main/scala/viper/gobra/ast/internal/Program.scala b/src/main/scala/viper/gobra/ast/internal/Program.scala index 6ff413f24..b7f22068c 100644 --- a/src/main/scala/viper/gobra/ast/internal/Program.scala +++ b/src/main/scala/viper/gobra/ast/internal/Program.scala @@ -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. diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index a0171b307..58445e0f1 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -14,6 +14,7 @@ import org.bitbucket.inkytonik.kiama.util.{FileSource, Source} import org.rogach.scallop.{ScallopConf, ScallopOption, singleArgConverter} import viper.gobra.backend.{ViperBackend, ViperBackends} import viper.gobra.GoVerifier +import viper.gobra.frontend.Config.enableLazyImportOptionPrettyPrinted import viper.gobra.frontend.PackageResolver.FileResource import viper.gobra.frontend.Source.getPackageInfo import viper.gobra.util.TaskManagerMode.{Lazy, Parallel, Sequential, TaskManagerMode} @@ -164,7 +165,6 @@ case class Config( z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode, disableNL: Boolean = ConfigDefaults.DefaultDisableNL, mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode, - enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors, parseAndTypeCheckMode: TaskManagerMode = ConfigDefaults.DefaultParseAndTypeCheckMode, @@ -225,7 +225,6 @@ case class Config( z3APIMode = z3APIMode || other.z3APIMode, disableNL = disableNL || other.disableNL, mceMode = mceMode, - enableLazyImports = enableLazyImports || other.enableLazyImports, noVerify = noVerify || other.noVerify, noStreamErrors = noStreamErrors || other.noStreamErrors, parseAndTypeCheckMode = parseAndTypeCheckMode, @@ -286,7 +285,6 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode, disableNL: Boolean = ConfigDefaults.DefaultDisableNL, mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode, - enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors, parseAndTypeCheckMode: TaskManagerMode = ConfigDefaults.DefaultParseAndTypeCheckMode, @@ -349,7 +347,6 @@ trait RawConfig { z3APIMode = baseConfig.z3APIMode, disableNL = baseConfig.disableNL, mceMode = baseConfig.mceMode, - enableLazyImports = baseConfig.enableLazyImports, noVerify = baseConfig.noVerify, noStreamErrors = baseConfig.noStreamErrors, parseAndTypeCheckMode = baseConfig.parseAndTypeCheckMode, @@ -887,6 +884,15 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals case _ => false } + addValidation { + val lazyImportsSet = enableLazyImports.toOption.nonEmpty + if (lazyImportsSet) { + Left(s"The flag $enableLazyImportOptionPrettyPrinted was removed in Gobra's PR #797.") + } else { + Right(()) + } + } + // `parallelizeBranches` requires a backend that supports branch parallelization (i.e., a silicon-based backend) addValidation { val parallelizeBranchesOn = parallelizeBranches.toOption.contains(true) @@ -1052,7 +1058,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals z3APIMode = z3APIMode(), disableNL = disableNL(), mceMode = mceMode(), - enableLazyImports = enableLazyImports(), noVerify = noVerify(), noStreamErrors = noStreamErrors(), parseAndTypeCheckMode = parseAndTypeCheckMode(), diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index 02bf27df1..d5cbb7a29 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/src/main/scala/viper/gobra/frontend/Desugar.scala @@ -21,42 +21,40 @@ import viper.gobra.reporting.{DesugaredMessage, Source} import viper.gobra.theory.Addressability import viper.gobra.translator.Names import viper.gobra.util.Violation.violation -import viper.gobra.util.{BackendAnnotation, Constants, DesugarWriter, GobraExecutionContext, Violation} +import viper.gobra.util.{BackendAnnotation, Computation, 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} -import scala.concurrent.duration.Duration -import scala.concurrent.{Await, Future} import scala.reflect.ClassTag + // `LazyLogging` provides us with access to `logger` to emit log messages object Desugar extends LazyLogging { + // We currently desugar packages sequentially. We may make it parallel again in the future (if that is beneficial), + // but care must be taken to guarantee that updates to the init specs collector are synchronized. def desugar(config: Config, info: viper.gobra.frontend.info.TypeInfo)(implicit executionContext: GobraExecutionContext): in.Program = { val pkg = info.tree.root - val importsCollector = new PackageInitSpecCollector + val packageInitCollector = new PackageInitSpecCollector val importedDesugaringDurationMs = new AtomicLong(0) - val importedProgramsFuts = info.getTransitiveTypeInfos(includeThis = false).toSeq.map { tI => Future { + val importedPrograms = info.getTransitiveTypeInfos(includeThis = false).toSeq.map { tI => 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 - d.registerPackage(importedPackage, importsCollector)(config) - val res = (d, d.packageD(importedPackage)) + val d = new Desugarer(importedPackage.positions, typeInfo, packageInitCollector) + val res = (d, d.packageD(importedPackage, isImportedPkg = true)) importedDesugaringDurationMs.addAndGet(System.currentTimeMillis() - importedDesugaringStartMs) res - }} + } - val mainPackageFut = Future { + val mainPackage = { val mainDesugaringStartMs = System.currentTimeMillis() // desugar the main package, i.e. the package on which verification is performed: - val mainDesugarer = new Desugarer(pkg.positions, info) - // registers main package to generate proof obligations for its init code - mainDesugarer.registerMainPackage(pkg, importsCollector)(config) - val res = (mainDesugarer, mainDesugarer.packageD(pkg)) + val mainDesugarer = new Desugarer(pkg.positions, info, packageInitCollector) + val res = (mainDesugarer, mainDesugarer.packageD(pkg, isImportedPkg = false)) logger.trace { val durationS = f"${(System.currentTimeMillis() - mainDesugaringStartMs) / 1000f}%.1f" s"desugaring package ${info.pkgInfo.id} done, took ${durationS}s" @@ -64,11 +62,7 @@ object Desugar extends LazyLogging { res } - // we place `mainPackageFut` at index 0 - val allPackagesFut = Future.sequence(mainPackageFut +: importedProgramsFuts) - val futResults = Await.result(allPackagesFut, Duration.Inf) - val (mainDesugarer, mainProgram) = futResults.head - val importedPrograms = futResults.tail + val (mainDesugarer, mainProgram) = mainPackage logger.trace { val importedDurationS = f"${importedDesugaringDurationMs.get() / 1000f}%.1f" s"desugaring imported packages done, took ${importedDurationS}s" @@ -186,9 +180,7 @@ object Desugar extends LazyLogging { } } - private class Desugarer(pom: PositionManager, info: viper.gobra.frontend.info.TypeInfo) { - - // TODO: clean initialization + private class Desugarer(pom: PositionManager, info: viper.gobra.frontend.info.TypeInfo, initSpecs: PackageInitSpecCollector) { type Meta = Source.Parser.Info @@ -198,8 +190,6 @@ object Desugar extends LazyLogging { import desugarWriter._ type Writer[+R] = desugarWriter.Writer[R] -// def complete[X <: in.Stmt](w: Agg[X]): in.Stmt = {val (xs, x) = w.run; in.Seqn(xs :+ x)(x.info)} - private val nm = new NameManager @@ -414,7 +404,11 @@ object Desugar extends LazyLogging { * Desugars a package with an optional `shouldDesugar` function indicating whether a particular member should be * desugared or skipped */ - def packageD(p: PPackage, shouldDesugar: PMember => Boolean = _ => true): in.Program = { + def packageD(p: PPackage, isImportedPkg: Boolean, shouldDesugar: PMember => Boolean = _ => true): in.Program = { + // registers a package to generate proof obligations for its init code. + registerPkgInitData(p, initSpecs, isImportedPkg) + if (!isImportedPkg) { generatePkgInitProofObligations(p, initSpecs) } + val consideredDecls = p.declarations.collect { case m@NoGhost(x: PMember) if shouldDesugar(x) => m } val dMembers = consideredDecls.flatMap{ case NoGhost(_: PVarDecl) => @@ -3019,7 +3013,7 @@ object Desugar extends LazyLogging { // Both will have type Pointer(typeOf(v)) val src: Meta = meta(v, info) val refAlias = nm.refAlias(idName(v, info), info.scope(v), info) - // If `v` is a ghost variable, we consider `param` a ghost pointer. + // If `v` is a ghost variable, we consider `param` a ghost pointer. // However, we can use ActualPointer here since there is a single internal pointer type only. val param = in.Parameter.In(refAlias, typeD(ActualPointerT(info.typ(v)), Addressability.inParameter)(src))(src) val localVar = in.LocalVar(nm.alias(refAlias, info.scope(v), info), param.typ)(src) @@ -3443,142 +3437,206 @@ object Desugar extends LazyLogging { var implementationProofPredicateAliases: Map[(in.Type, in.InterfaceT, String), in.FPredicateProxy] = Map.empty /** - * Generates proof obligations for the initialization of the package under verification. + * Generates proof obligations for the initialization code of the package under verification. + * Following Gobra's methodology, we do not check that the initialization code for imported packages + * establishes their package invariants. Analogously to imported functions, we prove that these package + * invariants are established when verifying the imported packages. Thus, we can assume them here. + * * @param mainPkg package under verification - * @param specCollector info about the init specifications of imported packages. All imported packages should - * have been registered in `specCollector` before calling this method - * @param config + * @param initSpecs info about the init specifications of imported packages. All imported packages should + * have been registered in `initSpecs` before calling this method */ - def registerMainPackage(mainPkg: PPackage, specCollector: PackageInitSpecCollector)(config: Config): Unit = { - // As for imported methods, imported packages are not checked to satisfy their specification. In particular, - // Gobra does not check that the package postconditions are established by the initialization code. Instead, - // this is assumed. We only generate the proof obligations for the initialization code in the main package. - // Note that `config.enableLazyImports` disables init blocks, global variables, import preconditions, and init - // postconditions in the type checker, which means that we do not have to generate an init proof. - registerPackage(mainPkg, specCollector, generateInitProof = !config.enableLazyImports)(config) - - 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 - // packages that have been parsed). Note that packages that have been skipped because of the laziness might - // still contain such features. - 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) - } - - // proof obligations for function main - val mainFuncObligations = generateMainFuncObligations(mainPkg, specCollector) + def generatePkgInitProofObligations(mainPkg: PPackage, initSpecs: PackageInitSpecCollector): Unit = { + mainPkg.programs.map(_.imports) + + // Check that all duplicable static invariants are actually duplicable. + mainPkg.programs + .flatMap(_.pkgInvariants) + .filter(_.duplicable) + .map(_.inv) + .map(genCheckAssertionIsDup) + .foreach(AdditionalMembers.addMember) + + // 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) + + // Check that all import preconditions of imported packages are implied by those packages' + // friend clauses. + val resourcesToPkg = initSpecs.getImportsFromMainPkg() + resourcesToPkg.foreach{ case (pkg, resources) => + val src = meta(mainPkg, info) + val annotatedSrc = src.createAnnotatedInfo(ImportPreNotEstablished) + val importObligationsOpt = checkPkgImportObligations(mainPkg, pkg, resources, initSpecs)(annotatedSrc) + importObligationsOpt.foreach(AdditionalMembers.addMember) + } + + // if the main function is present, check its proof obligations + val mainFuncObligations = generateMainFuncProofObligation(mainPkg, initSpecs) mainFuncObligations.foreach(AdditionalMembers.addMember) } - /** - * Generates the members that correspond to the global variables declared in `pkg` and registers info in - * `specCollector` about all import preconditions and all package postconditions in all files of `pkg`. - * @param pkg - * @param specCollector - * @param generateInitProof true if the proof obligations for the package's initialization code - * should be generated - * @param config - */ - def registerPackage(pkg: PPackage, specCollector: PackageInitSpecCollector, generateInitProof: Boolean = false) - (config: Config): Unit = { - // Desugar all declarations of globals in `pkg` to generate the members that correspond to the global variables. - // Each entry in `pGlobalDecls` contains the declarations of a file in `pkg` sorted by the order in which they - // appear in the program. - val pGlobalDecls: Vector[Vector[PVarDecl]] = pkg.programs.map{ p => - val unsortedDecls = p.declarations.collect{ case d: PVarDecl => d } - // TODO: this is currently fine, given that we currently require global variable declarations to come after - // the declarations of all of the dependencies of the declared variables. This should be changed when - // we lift this restriction. - unsortedDecls.sortBy{ decl => - pom.positions.getStart(decl) match { - case Some(pos) => (pos.line, pos.column) - case None => violation(s"Could not find the position information of node $decl.") + // Check whether an expression e is self-framming and duplicable + 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) + /** + * [ e ] -> + * requires e + * ensures e + * ensures e + * func dupPkgInv() {} + */ + 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(in.MethodBody.empty(src)) + )(src) + } + + // Desugar all declarations of globals in `pkg` to generate the members that correspond to the global variables. + // Each entry in `pGlobalDecls` contains the declarations of a file in `pkg` sorted by the order in which they + // appear in the program. + private val sortedGlobalVariableDecls: PPackage => Vector[Vector[in.GlobalVarDecl]] = + Computation.cachedComputation { pkg => + // the following may only be called once per package, otherwise wildcard identifiers may be desugared multiple + // times, leading to different names being generated on different occasions. + val pGlobalDecls: Vector[Vector[PVarDecl]] = pkg.programs.map { p => + val unsortedDecls = p.declarations.collect { case d: PVarDecl => d; case PExplicitGhostMember(d: PVarDecl) => d } + // TODO: this is currently fine, given that we currently require global variable declarations to come after + // the declarations of all of the dependencies of the declared variables. This should be changed when + // we lift this restriction. + unsortedDecls.sortBy { decl => + pom.positions.getStart(decl) match { + case Some(pos) => (pos.line, pos.column) + case None => violation(s"Could not find the position information of node $decl.") + } } } + // sorted desugared declarations + pGlobalDecls.map(_.map(globalVarDeclD)) } - // sorted desugared declarations - val globalDecls: Vector[Vector[in.GlobalVarDecl]] = pGlobalDecls.map(_.map(globalVarDeclD)) + + /** + * Collects all necessary information necessary to generate the proof obligations related to the initialization + * code of the package under initialization. This should be called by all packages that the main package imports. + * @param pkg Package to register + * @param initSpecs Collector of all necessary meta-data + * @param isImportedPkg true iff the proof obligations for the package's initialization code should be generated + * @param config + */ + def registerPkgInitData(pkg: PPackage, initSpecs: PackageInitSpecCollector, isImportedPkg: Boolean): Unit = { // register all global variable declarations + val globalDecls = sortedGlobalVariableDecls(pkg) globalDecls.flatten.foreach(AdditionalMembers.addMember) - 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) + // Register import preconditions of the package under verification. We don't store this info for imported + // packages because we do not check the init proof obligations for imported packages. + if (!isImportedPkg) { + pkg.imports.foreach { imp => + val importedPackage = RegularImport(imp.importPath) + val tI = info.dependentTypeInfo(importedPackage) + val importedPkg = tI.getTypeInfo.tree.originalRoot + val desugaredPre = imp.importPres.map(specificationD(FunctionContext.empty(), info)) + initSpecs.registerImportPresFromMainPkg(importedPkg, desugaredPre) } - 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") - val tI = info.dependentTypeInfo(importedPackage) - 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) - }} + // collect package invariants + val goA = specificationD(FunctionContext.empty(), info)(_) + val pkgInvs = pkg.programs.flatMap(_.pkgInvariants).map { inv => + val dExpr = goA(inv.inv) + (dExpr, inv.duplicable) + } + initSpecs.registerPkgInvariants(pkg, pkgInvs) + + val fullPathOfPkg = pkg.info.uniquePath - // 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 friend package clauses + pkg.programs.flatMap(_.friends).map{ i => + val fullPathFriend = Paths.get(fullPathOfPkg).resolve(i.path).normalize() + val assertion = specificationD(FunctionContext.empty(), info)(i.assertion) + (fullPathFriend, assertion) + }.foreach { case (absPkg, resource) => + initSpecs.registerResourcesForFriends(pkg, absPkg.toString, resource) + } } /** - * Checks that the postconditions of package `pkg` imply the conjunction of all imports' preconditions (that import - * package `pkg`) - * @param pkg - * @param specCollector + * Checks that the friend clauses of package `importedPackage` imply the conjunction of all imports' preconditions + * of this package in the package under verification, namely `mainPkg`. + * @param mainPkg package under verification + * @param importedPackage package containing friend clauses + * @param importPresOfImportedPackage init preconditions to the package `importedPackage` from the `mainPkg` + * @param initSpecs collector of init specs * @param src * @return */ - def checkPkgImportObligations(pkg: PPackage, specCollector: PackageInitSpecCollector) - (src: Source.Parser.Single): in.Function = { - val funcProxy = in.FunctionProxy(nm.packageImports(pkg, info))(src) - in.Function( - name = funcProxy, - args = Vector.empty, - results = Vector.empty, - pres = specCollector.postsOfPackage(pkg), - posts = specCollector.presImportsOfPackage(pkg).map{ a => - a.withInfo(a.info.asInstanceOf[Source.Parser.Single].createAnnotatedInfo(ImportPreNotEstablished)) - }, - terminationMeasures = Vector.empty, - backendAnnotations = Vector.empty, - body = Some(in.MethodBody(Vector.empty, in.MethodBodySeqn(Vector.empty)(src), Vector.empty)(src)), - )(src) + def checkPkgImportObligations(mainPkg: PPackage, + importedPackage: PPackage, + importPresOfImportedPackage: Vector[in.Assertion], + initSpecs: PackageInitSpecCollector) + (src: Source.Parser.Single): Option[in.Function] = { + val currPkgUniqId = mainPkg.info.uniquePath + val pres = initSpecs.getFriendResourcesFromSrc(importedPackage).filter { + case (path, _) => path == currPkgUniqId + }.map(_._2) + val posts = importPresOfImportedPackage + if (pres.nonEmpty || posts.nonEmpty) { + // as an optimization, only generate methods for imports that introduce + // proof obligations + val checkFn = in.Function( + name = in.FunctionProxy(nm.packageImports(importedPackage, info))(src), + args = Vector.empty, + results = Vector.empty, + pres = pres, + posts = posts.map(_.withInfo(src)), + terminationMeasures = Vector.empty, + backendAnnotations = Vector.empty, + body = Some(in.MethodBody.empty(src)) + )(src) + Some(checkFn) + } else { + None + } } /** - * Generate proof obligations for the main function, if it exists in `mainPkg`. - * To that end, we just check that the init post-conditions of the current package imply the main function's - * precondition. A more complete approach would be to iterate through all packages, - * following the order of the dependencies, and exhale its import-preconditions and then inhale its - * package postconditions, until we reach the main package. Afterward, we could exhale main's precondition. - * @param mainPkg package under verification - * @param specCollector info about the init specifications of imported packages. All imported packages should - * have been registered in `specCollector` before calling this method - * @return - */ - def generateMainFuncObligations(mainPkg: PPackage, specCollector: PackageInitSpecCollector): Option[in.Function] = { - val mainFuncOpt = mainPkg.declarations.collectFirst{ + * Generates proof obligations for the main function, if it exists in the `mainPkg`. + * To that end, we check that the package invariants of the current package and all imported packages + * imply the main function's precondition. + * + * @param mainPkg package under verification + * @param initSpecs info about the init specifications of imported packages. All imported packages should + * have been registered in `specCollector` before calling this method + * @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 } - mainFuncOpt.map{ mainFunc => + mainFuncOpt.map { mainFunc => val src = meta(mainFunc, info) - val mainPkgPosts = specCollector.postsOfPackage(mainPkg) - val mainFuncPre = mainFunc.spec.pres ++ mainFunc.spec.preserves - val mainFuncPreD = mainFuncPre.map(specificationD(FunctionContext.empty(), info)).map{ a => + val mainPkgPosts = initSpecs.getNonDupPkgInvariants().values.flatten.toVector + 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) + /** + * requires mainPkgPosts // postconditions established by initialization + * ensures mainFuncPreD // desugarer preconditions of the main function + * func mainFuncProofObligation() {} + */ in.Function( name = funcProxy, args = Vector.empty, @@ -3597,31 +3655,37 @@ object Desugar extends LazyLogging { * encoded as a method that performs the following operations, in order: * - inhale all preconditions of the imports in the file * - initialize all global variables - * - execute the operations on the LHS of the declarations by declaration order, + * - execute the operations on the RHS of the declarations by declaration order, * 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, - * it is ok to check the initialization of a package by separately checking the initialization of each of - * its programs. - * @param p - * @return + * - exhale all package-invariants of the file + * - exhale all friend clauses + * Note: these operations enforce non-interference between two files belonging to the same package. + * Thus, it is ok to check the initialization of a package by separately checking the initialization of each of + * its files. */ def checkProgramInitContract(p: PProgram)(sortedGlobVarDecls: Vector[in.GlobalVarDecl]): 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.pkgInvariants.map{ i => specificationD(FunctionContext.empty(), info)(i.inv)} + val resourcesForFriends: Vector[in.Assertion] = p.friends.map{i => specificationD(FunctionContext.empty(), info)(i.assertion)} + val currPkg = info.tree.originalRoot + val pkgInvariantsImportedPackages: Vector[in.Assertion] = + initSpecs.getNonDupPkgInvariants().filter{ case (k, _) => k != currPkg }.values.flatten.toVector + + val uniquePathPkg = currPkg.info.uniquePath + val resourcesFromFriendPkgs = initSpecs.getFriendResourcesForDst(uniquePathPkg).map(_._2) 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, + // inhales all import preconditions of the current file all invariants of imported packages + pres = progPres ++ pkgInvariantsImportedPackages ++ resourcesFromFriendPkgs, + // exhales all package invariants from the current file and all resources for friends + posts = pkgInvariantsImportedPackages ++ pkgInvariants ++ resourcesForFriends, // in our verification approach, the initialization code must be proven to terminate terminationMeasures = Vector(in.TupleTerminationMeasure(Vector(), None)(src)), backendAnnotations = Vector.empty, @@ -3654,17 +3718,24 @@ object Desugar extends LazyLogging { * var B = 2 */ val declarationsInOrder: Vector[in.Stmt] = sortedGlobVarDecls.flatMap{ _.declStmts } + // execute all inits in the order they occur // TODO: at the moment, there exists at most one init, but this should change in the future val initBlocks = p.declarations.collect{ case x: PFunctionDecl if x.id.name == Constants.INIT_FUNC_NAME => x } violation(initBlocks.length <= 1, "at most one init block is supported right now") + + // This must be done after the variable declarations, as at this point other files may run their own + // variable declarations that may assume the invariants of imported packages. + val exhaleInhaleImportedPkgsInvs = pkgInvariantsImportedPackages.map(in.Exhale(_)(src)) ++ + pkgInvariantsImportedPackages.map(in.Inhale(_)(src)) + val initCode: Vector[in.Stmt] = initBlocks.flatMap(b => b.body.toVector.map(_._2).map(blockD(FunctionContext.empty(), info))) // body of the generated method - initDeclaredGlobs ++ declarationsInOrder ++ initCode + initDeclaredGlobs ++ declarationsInOrder ++ exhaleInhaleImportedPkgsInvs ++ initCode }(src) )(src) ) @@ -3683,7 +3754,7 @@ object Desugar extends LazyLogging { /** * In Go, functions named init are executed during a package initialization, * and can never be called by any other function. In Gobra, the proof obligations - * associated with init functions are generated in method [[registerPackage]]. + * associated with init functions are generated in method [[generatePkgInitProofObligations]]. * As such, these functions are ignored by [[registerFunction]]. */ None @@ -4093,6 +4164,13 @@ 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() => + // open the current package's invariant. + val currPkg = info.tree.originalRoot + val dupInvs = initSpecs.getDupPkgInvariants().get(currPkg).get + 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) @@ -4855,8 +4933,9 @@ object Desugar extends LazyLogging { private val METHOD_PREFIX = "M" private val TYPE_PREFIX = "T" private val PROGRAM_INIT_CODE_PREFIX = "$INIT" - private val PACKAGE_IMPORT_OBLIGATIONS_PREFIX = "$IMPORTS" + private val PACKAGE_IMPORT_OBLIGATIONS_PREFIX = "$IMPORTS_FROM_FRIENDS" 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" @@ -4883,6 +4962,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) @@ -4925,6 +5006,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) @@ -5092,34 +5177,62 @@ object Desugar extends LazyLogging { /** * Capabilities to store specification relevant to package initialization across * multiple desugarers. In particular, it provides functionality to store and retrieve - * preconditions for all imports of a package and the postconditions of all programs of - * a package. + * preconditions for all imports of a package, the package invariants of all packages, + * and the friend clauses. */ private class PackageInitSpecCollector { + 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 + // pairs of package X and the preconditions on an import of X (one entry in the list per import of X) 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 - def addImportPres(pkg: PPackage, desugaredImportPre: Vector[in.Assertion]): Unit = { - importPreconditions :+= (pkg, desugaredImportPre) + // Register that the package under verification imports package pkg with import preconditions desugaredImportPres. + def registerImportPresFromMainPkg(pkg: PPackage, desugaredImportPres: Vector[in.Assertion]): Unit = { + importPreconditions :+= (pkg, desugaredImportPres) } - def presImportsOfPackage(pkg: PPackage): Vector[in.Assertion] = { - importPreconditions.filter(_._1.info.id == pkg.info.id).flatMap(_._2) + // Get all imports from the package under verification and its import preconditions + def getImportsFromMainPkg(): Map[PPackage, Vector[in.Assertion]] = { + val l = importPreconditions.groupMap(_._1)(_._2) + l.map{ case (k,v) => (k, v.flatten)} } - def addPackagePosts(pkg: PPackage, desugaredPosts: Vector[in.Assertion]): Unit = { - packagePostconditions :+= (pkg, desugaredPosts) + type FullPathFromRootToPkg = String + + // vector of triples (src, dst, resources) + private var friendClauses: Vector[(PPackage, FullPathFromRootToPkg, in.Assertion)] = Vector.empty + + // Register that package src registered the path `dst` as a friend with resource res. + def registerResourcesForFriends(src: PPackage, dst: FullPathFromRootToPkg, res: in.Assertion) = { + friendClauses :+= (src, dst, res) } - def postsOfPackage(pkg: PPackage): Vector[in.Assertion] = { - packagePostconditions.filter(_._1.info.id == pkg.info.id).flatMap(_._2) + // Get all friend clauses registered in package pkg. + def getFriendResourcesFromSrc(pkg: PPackage): Vector[(FullPathFromRootToPkg, in.Assertion)] = { + friendClauses.filter(_._1 == pkg).map(e => (e._2, e._3)) } - def registeredPackages(): Vector[PPackage] = { - // the domain of package posts should have all registered packages - packagePostconditions.map(_._1).distinct + // Get all resources from friends destined to path `uniquePkgPath `. + def getFriendResourcesForDst(uniquePkgPath: String): Vector[(PPackage, in.Assertion)] = { + friendClauses.filter { + case (_, pathFriend, _) => uniquePkgPath == pathFriend + case _ => false + }.map(e => (e._1, e._3)) } } } diff --git a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala index f38cd8aef..92d78f8a3 100644 --- a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala +++ b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala @@ -925,7 +925,8 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole annotations, isPure = ctx.pure, isTrusted = ctx.trusted, - isOpaque = ctx.opaque + isOpaque = ctx.opaque, + mayBeUsedInInit = ctx.mayInit, ) } @@ -2206,7 +2207,18 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole case Vector("unfold", predAcc : PPredicateAccess) => PUnfold(predAcc) } - /** + override def visitPkgInvStatement(ctx: PkgInvStatementContext): POpenDupPkgInv = { + 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 * */ @@ -2276,16 +2288,26 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole override def visitSourceFile(ctx: GobraParser.SourceFileContext): PProgram = { val packageClause: PPackageClause = visitNode(ctx.packageClause()) val initPosts: Vector[PExpression] = visitListNode[PExpression](ctx.initPost()) + if (initPosts.nonEmpty) { + violation(s"initEnsures clauses are no longer supported after Gobra PR #797.") + } + val pkgInvs: Vector[PPkgInvariant] = visitListNode[PPkgInvariant](ctx.pkgInvariant()) val importDecls = ctx.importDecl().asScala.toVector.flatMap(visitImportDecl) + val friendPkgs: Vector[PFriendPkgDecl] = visitListNode[PFriendPkgDecl](ctx.friendPkgDecl()) val members = ctx.member().asScala.toVector.flatMap(visitMember) - PProgram(packageClause, initPosts, importDecls, members).at(ctx) + PProgram(packageClause, pkgInvs, importDecls, friendPkgs, members).at(ctx) } override def visitPreamble(ctx: GobraParser.PreambleContext): PPreamble = { val packageClause: PPackageClause = visitNode(ctx.packageClause()) val initPosts: Vector[PExpression] = visitListNode[PExpression](ctx.initPost()) + if (initPosts.nonEmpty) { + violation(s"initEnsures clauses are no longer supported after Gobra PR #797.") + } + val pkgInvs: Vector[PPkgInvariant] = visitListNode[PPkgInvariant](ctx.pkgInvariant()) val importDecls = ctx.importDecl().asScala.toVector.flatMap(visitImportDecl) - PPreamble(packageClause, initPosts, importDecls, pom).at(ctx) + val friendPkgs: Vector[PFriendPkgDecl] = visitListNode[PFriendPkgDecl](ctx.friendPkgDecl()) + PPreamble(packageClause, pkgInvs, importDecls, friendPkgs, pom).at(ctx) } /** @@ -2295,6 +2317,18 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole */ override def visitInitPost(ctx: InitPostContext): PExpression = visitNode[PExpression](ctx.expression()) + /** + * Visits a pkgInvariant + * + * @param ctx the parse tree + * @return the positioned PPkgInvariant + */ + override def visitPkgInvariant(ctx: PkgInvariantContext): PPkgInvariant = { + val dup = ctx.DUPLICABLE() != null + val inv = visitNode[PExpression](ctx.assertion()) + PPkgInvariant(inv, dup).at(ctx) + } + /** * Visists an import precondition * @param ctx the parse tree diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala index 377ec45ee..26efdf048 100644 --- a/src/main/scala/viper/gobra/frontend/Parser.scala +++ b/src/main/scala/viper/gobra/frontend/Parser.scala @@ -460,7 +460,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, updatedImports, prog.declarations).at(prog) + PProgram(prog.packageClause, prog.pkgInvariants, 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) @@ -492,7 +492,7 @@ object Parser extends LazyLogging { case n@PTupleTerminationMeasure(_, cond) => PWildcardMeasure(cond).at(n) case t => t } - PFunctionSpec(spec.pres, spec.preserves, spec.posts, replacedMeasures, spec.backendAnnotations, spec.isPure, spec.isTrusted) + PFunctionSpec(spec.pres, spec.preserves, spec.posts, replacedMeasures, spec.backendAnnotations, spec.isPure, spec.isTrusted, mayBeUsedInInit = spec.mayBeUsedInInit) } val replaceTerminationMeasuresForFunctionsAndMethods: Strategy = @@ -508,7 +508,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.imports, updatedDecls).at(prog) + PProgram(prog.packageClause, prog.pkgInvariants, 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)) diff --git a/src/main/scala/viper/gobra/frontend/Source.scala b/src/main/scala/viper/gobra/frontend/Source.scala index c6945eebb..a1f8bb7df 100644 --- a/src/main/scala/viper/gobra/frontend/Source.scala +++ b/src/main/scala/viper/gobra/frontend/Source.scala @@ -27,7 +27,17 @@ import scala.io.BufferedSource * @param name the name of the package, does not have to be unique * @param isBuiltIn a flag indicating, if the package comes from within Gobra */ -class PackageInfo(val id: String, val name: String, val isBuiltIn: Boolean) { +class PackageInfo(val uniquePath: String, val name: String, val isBuiltIn: Boolean) { + val id: String = { + if (uniquePath.nonEmpty) { + // The - is enough to unambiguously separate the prefix from the package name, since it can't occur in the package name + // per Go's spec (https://go.dev/ref/spec#Package_clause) + uniquePath + " - " + name + } else { + // Fallback case if the prefix is empty, for example if the directory of a FileSource is in the current directory + name + } + } /** * Unique id of the package to use in Viper member names. @@ -63,18 +73,8 @@ object Source { for { packageName <- packageNameOrError /** A unique identifier for packages */ - packageId = { - val prefix = uniquePath(TransformableSource(src).toPath.toAbsolutePath.getParent, projectRoot).toString - if(prefix.nonEmpty) { - // The - is enough to unambiguously separate the prefix from the package name, since it can't occur in the package name - // per Go's spec (https://go.dev/ref/spec#Package_clause) - prefix + " - " + packageName - } else { - // Fallback case if the prefix is empty, for example if the directory of a FileSource is in the current directory - packageName - } - } - } yield new PackageInfo(packageId, packageName, isBuiltIn) + prefix = uniquePath(TransformableSource(src).toPath.toAbsolutePath.getParent, projectRoot).toString + } yield new PackageInfo(prefix, packageName, isBuiltIn) } /** diff --git a/src/main/scala/viper/gobra/frontend/info/Info.scala b/src/main/scala/viper/gobra/frontend/info/Info.scala index 827dba058..5b738cf2d 100644 --- a/src/main/scala/viper/gobra/frontend/info/Info.scala +++ b/src/main/scala/viper/gobra/frontend/info/Info.scala @@ -235,8 +235,7 @@ object Info extends LazyLogging { .mkString("") val isMainContextKey = if (isMainContext) "1" else "0" val configKey = config.typeBounds.hashCode().toString ++ - (if (config.int32bit) "1" else "0") ++ - (if (config.enableLazyImports) "1" else "0") + (if (config.int32bit) "1" else "0") val key = pkgKey ++ dependentTypeInfoKey ++ 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 705262b65..91c104668 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala @@ -152,7 +152,7 @@ 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 getTransitiveTypeInfos(includeThis: Boolean = true): Set[ExternalTypeInfo] = { val directTypeInfos = dependentTypeInfo.values.toSet // note that we call `getTransitiveTypeInfos` recursively with including the parameter in the results (which // corresponds to the parameter's default value) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala index 1175fe801..be6eba9e2 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala @@ -14,66 +14,98 @@ import viper.gobra.util.TypeBounds.BoundedIntegerKind import viper.gobra.util.Violation.violation trait Assignability extends BaseProperty { this: TypeInfoImpl => - - lazy val declarableTo: Property[(Vector[Type], Option[Type], Vector[Type])] = - createProperty[(Vector[Type], Option[Type], Vector[Type])] { - case (right, None, left) => multiAssignableTo.result(right, left) - case (right, Some(t), _) => propForall(right, assignableTo.before((l: Type) => (l, t))) + lazy val declarableTo: Property[(Vector[Type], Option[Type], Vector[Type], Boolean)] = + createProperty[(Vector[Type], Option[Type], Vector[Type], Boolean)] { + case (right, None, left, mayInit) => multiAssignableTo.result(right, left, mayInit) + case (right, Some(t), _, mayInit) => + propForall(right, assignableTo.before((l: Type) => (l, t, mayInit))) } - lazy val multiAssignableTo: Property[(Vector[Type], Vector[Type])] = createProperty[(Vector[Type], Vector[Type])] { - case (right, left) => + def isImportedContextualType(t: Type): Boolean = t match { + case t: PointerT => isImportedContextualType(t.elem) + case t: ContextualType => t.context != this + case _ => false + } + + def isLocallyDefinedContextualType(t: Type): Boolean = t match { + case t: PointerT => isLocallyDefinedContextualType(t.elem) + case t: ContextualType => t.context == this + case _ => false + } + + // To guarantee that no dynamically dispatched methods that may depend on invariants of the package + // under initialization are called, we disallow assigning a value of a type defined in the current + // package to a variable of an interface type defined in an exported package. This allows us to call, + // without restriction, any interface methods with receiver types defined in imported packages during + // initialization of a package. + private lazy val assignableToIfInit: Property[(Type, Type)] = createProperty[(Type, Type)] { + case (targetType, srcType) => + if (isLocallyDefinedContextualType(targetType) && isImportedContextualType(srcType)) { + failedProp("Assigning values of types defined in the current package to locations " + + "of an interface type that is defined in imported packages is disallowed in code that may run during package initialization.") + } else { + successProp + } + } + + lazy val multiAssignableTo: Property[(Vector[Type], Vector[Type], Boolean)] = createProperty[(Vector[Type], Vector[Type], Boolean)] { + case (right, left, mayInit) => StrictAssignMode(left.size, right.size) match { case AssignMode.Single => right match { // To support Go's function chaining when a tuple with the results of a function call are passed to the // only variadic argument of another function case Vector(InternalTupleT(t)) if left.lastOption.exists(_.isInstanceOf[VariadicT]) => - multiAssignableTo.result(t, left) - case _ => propForall(right.zip(left), assignableTo) + multiAssignableTo.result(t, left, mayInit) + case _ => + propForall( + right.zip(left), + createProperty[(Type, Type)]{ case (l: Type, r: Type) => assignableTo.result(l, r, mayInit) } + ) } case AssignMode.Multi => right.head match { - case Assign(InternalTupleT(ts)) => multiAssignableTo.result(ts, left) + case Assign(InternalTupleT(ts)) => multiAssignableTo.result(ts, left, mayInit) case t => if (left.length == right.length + 1 && left.last.isInstanceOf[VariadicT]) { // this handles the case when all parameters but the last are passed in a function call and the last parameter // is variadic - multiAssignableTo.result(right, left.init) + multiAssignableTo.result(right, left.init, mayInit) } else { failedProp(s"got $t but expected tuple type of size ${left.size}") } } - case AssignMode.Variadic => variadicAssignableTo.result(right, left) + case AssignMode.Variadic => variadicAssignableTo.result(right, left, mayInit) case AssignMode.Error => failedProp(s"cannot assign ${right.size} to ${left.size} elements") } } - lazy val variadicAssignableTo: Property[(Vector[Type], Vector[Type])] = createProperty[(Vector[Type], Vector[Type])] { - case (right, left) => + lazy val variadicAssignableTo: Property[(Vector[Type], Vector[Type], Boolean)] = createProperty[(Vector[Type], Vector[Type], Boolean)] { + case (right, left, mayInit) => StrictAssignMode(left.size, right.size) match { case AssignMode.Variadic => left.lastOption match { case Some(VariadicT(elem)) => val dummyFill = UnknownType // left.init corresponds to the parameter list on the left except for the variadic type - propForall(right.zipAll(left.init, dummyFill, elem), assignableTo) + propForall( + right.zipAll(left.init, dummyFill, elem), + createProperty[(Type, Type)]{ case (l: Type, r: Type) => assignableTo.result(l, r, mayInit) } + ) case _ => failedProp(s"expected the last element of $left to be a variadic type") } case _ => failedProp(s"cannot assign $right to $left") } } - lazy val parameterAssignableTo: Property[(Type, Type)] = createProperty[(Type, Type)] { - case (Argument(InternalTupleT(rs)), Argument(InternalTupleT(ls))) if rs.size == ls.size => - propForall(rs zip ls, assignableTo) - - case (r, l) => assignableTo.result(r, l) - } - - lazy val assignableTo: Property[(Type, Type)] = createFlatPropertyWithReason[(Type, Type)] { - case (right, left) => s"$right is not assignable to $left" + // The notion of assignability depends on the context where the assignments are performed. + // In particular, in code that may execute during package initialization, some assignments + // to interface types are disallowed to guarantee that interface methods that assume the invariant + // of the package under initialization are never called. + lazy val assignableTo: Property[(Type, Type, Boolean)] = createFlatPropertyWithReason[(Type, Type, Boolean)] { + case (right, left, _) => s"$right is not assignable to $left" } { - case (Single(lst), Single(rst)) => (lst, rst) match { + case (Single(lst), Single(rst), mayInit) => (lst, rst) match { + case _ if mayInit && !assignableToIfInit(lst, rst) => assignableToIfInit.result(lst, rst) // for go's types according to go's specification (mostly) case (UNTYPED_INT_CONST, r) if underlyingType(r).isInstanceOf[IntT] => successProp // not part of Go spec, but necessary for the definition of comparability @@ -87,16 +119,16 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl => case (l, r) if underlyingType(r).isInstanceOf[InterfaceT] => implements(l, r) case (ChannelT(le, ChannelModus.Bi), ChannelT(re, _)) if identicalTypes(le, re) => successProp case (NilType, r) if isPointerType(r) => successProp - case (VariadicT(t1), VariadicT(t2)) => assignableTo.result(t1, t2) - case (t1, VariadicT(t2)) => assignableTo.result(t1, t2) + case (VariadicT(t1), VariadicT(t2)) => assignableTo.result(t1, t2, mayInit) + case (t1, VariadicT(t2)) => assignableTo.result(t1, t2, mayInit) case (VariadicT(t1), SliceT(t2)) if identicalTypes(t1, t2) => successProp // for ghost types case (BooleanT, AssertionT) => successProp - case (SequenceT(l), SequenceT(r)) => assignableTo.result(l,r) // implies that Sequences are covariant - case (SetT(l), SetT(r)) => assignableTo.result(l,r) - case (MultisetT(l), MultisetT(r)) => assignableTo.result(l,r) - case (OptionT(l), OptionT(r)) => assignableTo.result(l, r) + case (SequenceT(l), SequenceT(r)) => assignableTo.result(l, r, mayInit) // implies that Sequences are covariant + case (SetT(l), SetT(r)) => assignableTo.result(l, r, mayInit) + case (MultisetT(l), MultisetT(r)) => assignableTo.result(l, r, mayInit) + case (OptionT(l), OptionT(r)) => assignableTo.result(l, r, mayInit) case (IntT(_), PermissionT) => successProp // conservative choice @@ -130,18 +162,18 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl => case _ => false } - lazy val compositeKeyAssignableTo: Property[(PCompositeKey, Type)] = createProperty[(PCompositeKey, Type)] { - case (PIdentifierKey(id), t) => assignableTo.result(idType(id), t) - case (k: PCompositeVal, t) => compositeValAssignableTo.result(k, t) + lazy val compositeKeyAssignableTo: Property[(PCompositeKey, Type, Boolean)] = createProperty[(PCompositeKey, Type, Boolean)] { + case (PIdentifierKey(id), t, mayInit) => assignableTo.result(idType(id), t, mayInit) + case (k: PCompositeVal, t, mayInit) => compositeValAssignableTo.result(k, t, mayInit) } - lazy val compositeValAssignableTo: Property[(PCompositeVal, Type)] = createProperty[(PCompositeVal, Type)] { - case (PExpCompositeVal(exp), t) => assignableTo.result(exprType(exp), t) - case (PLitCompositeVal(lit), t) => literalAssignableTo.result(lit, t) + lazy val compositeValAssignableTo: Property[(PCompositeVal, Type, Boolean)] = createProperty[(PCompositeVal, Type, Boolean)] { + case (PExpCompositeVal(exp), t, mayInit) => assignableTo.result(exprType(exp), t, mayInit) + case (PLitCompositeVal(lit), t, mayInit) => literalAssignableTo.result(lit, t, mayInit) } - lazy val literalAssignableTo: Property[(PLiteralValue, Type)] = createProperty[(PLiteralValue, Type)] { - case (PLiteralValue(elems), Single(typ)) => + lazy val literalAssignableTo: Property[(PLiteralValue, Type, Boolean)] = createProperty[(PLiteralValue, Type, Boolean)] { + case (PLiteralValue(elems), Single(typ), mayInit) => underlyingType(typ) match { case s: StructT => if (elems.isEmpty) { @@ -154,7 +186,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl => propForall(elems, createProperty[PKeyedElement] { e => e.key.map { case PIdentifierKey(id) if tmap.contains(id.name) => - compositeValAssignableTo.result(e.exp, tmap(id.name)) + compositeValAssignableTo.result(e.exp, tmap(id.name), mayInit) case v => failedProp(s"got $v but expected field name") }.getOrElse(successProp) @@ -162,7 +194,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl => } else if (elems.size == s.embedded.size + s.fields.size) { propForall( elems.map(_.exp).zip(s.fieldsAndEmbedded.values), - compositeValAssignableTo + createProperty[(PCompositeVal, Type)]{ case (l: PCompositeVal, r: Type) => compositeValAssignableTo.result(l, r, mayInit) } ) } else { failedProp("number of arguments does not match structure") @@ -179,7 +211,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl => propForall(elems, createProperty[PKeyedElement] { e => e.key.map { case PIdentifierKey(id) if tmap.contains(id.name) => - compositeValAssignableTo.result(e.exp, tmap(id.name)) + compositeValAssignableTo.result(e.exp, tmap(id.name), mayInit) case v => failedProp(s"got $v but expected field name") }.getOrElse(successProp) @@ -187,7 +219,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl => } else if (elems.size == a.fields.size) { propForall( elems.map(_.exp).zip(a.fields.map(_._2)), - compositeValAssignableTo + createProperty[(PCompositeVal, Type)]{ case (l: PCompositeVal, r: Type) => compositeValAssignableTo.result(l, r, mayInit) } ) } else { failedProp("number of arguments does not match adt constructor") @@ -198,49 +230,49 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl => areAllKeysDisjoint(elems) and areAllKeysNonNegative(elems) and areAllKeysWithinBounds(elems, len) and - areAllElementsAssignable(elems, t) + areAllElementsAssignable(elems, t, mayInit) case SliceT(t) => areAllKeysConstant(elems) and areAllKeysDisjoint(elems) and areAllKeysNonNegative(elems) and - areAllElementsAssignable(elems, t) + areAllElementsAssignable(elems, t, mayInit) case GhostSliceT(t) => areAllKeysConstant(elems) and areAllKeysDisjoint(elems) and areAllKeysNonNegative(elems) and - areAllElementsAssignable(elems, t) + areAllElementsAssignable(elems, t, mayInit) case MapT(key, t) => areAllElementsKeyed(elems) and - areAllKeysAssignable(elems, key) and - areAllElementsAssignable(elems, t) and + areAllKeysAssignable(elems, key, mayInit) and + areAllElementsAssignable(elems, t, mayInit) and areAllConstantKeysDifferent(elems, key) case SequenceT(t) => areAllKeysConstant(elems) and areAllKeysDisjoint(elems) and areAllKeysNonNegative(elems) and - areAllElementsAssignable(elems, t) + areAllElementsAssignable(elems, t, mayInit) case SetT(t) => areNoElementsKeyed(elems) and - areAllElementsAssignable(elems, t) + areAllElementsAssignable(elems, t, mayInit) case MultisetT(t) => areNoElementsKeyed(elems) and - areAllElementsAssignable(elems, t) + areAllElementsAssignable(elems, t, mayInit) case MathMapT(keys, values) => areAllElementsKeyed(elems) and - areAllKeysAssignable(elems, keys) and - areAllElementsAssignable(elems, values) and + areAllKeysAssignable(elems, keys, mayInit) and + areAllElementsAssignable(elems, values, mayInit) and areAllConstantKeysDifferent(elems, keys) case t => failedProp(s"cannot assign literal to $t") } - case (l, t) => failedProp(s"cannot assign literal $l to $t") + case (l, t, _) => failedProp(s"cannot assign literal $l to $t") } def assignableWithinBounds: Property[(Type, PExpression)] = createFlatProperty[(Type, PExpression)] { @@ -287,11 +319,11 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl => private def areAllKeysWithinBounds(elems : Vector[PKeyedElement], length : BigInt) : PropertyResult = failedProp("found out-of-bound keys", keyElementIndices(elems).exists(length <= _)) - private def areAllKeysAssignable(elems : Vector[PKeyedElement], typ : Type) = - propForall(elems.flatMap(_.key), compositeKeyAssignableTo.before((c: PCompositeKey) => (c, typ))) + private def areAllKeysAssignable(elems : Vector[PKeyedElement], typ : Type, mayInit: Boolean) = + propForall(elems.flatMap(_.key), compositeKeyAssignableTo.before((c: PCompositeKey) => (c, typ, mayInit))) - private def areAllElementsAssignable(elems : Vector[PKeyedElement], typ : Type) = - propForall(elems.map(_.exp), compositeValAssignableTo.before((c: PCompositeVal) => (c, typ))) + private def areAllElementsAssignable(elems : Vector[PKeyedElement], typ : Type, mayInit: Boolean) = + propForall(elems.map(_.exp), compositeValAssignableTo.before((c: PCompositeVal) => (c, typ, mayInit))) private def areAllConstantKeysDifferent(elems: Vector[PKeyedElement], typ: Type) = { def constVal[T](eval: PExpression => Option[T])(keyed: PKeyedElement) : Option[T] = keyed.key match { diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/Comparability.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/Comparability.scala index 40b133100..d1911223d 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/property/Comparability.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/Comparability.scala @@ -16,7 +16,7 @@ trait Comparability extends BaseProperty { this: TypeInfoImpl => case (left, right) => s"$left is not comparable with $right" } { case (Single(left), Single(right)) => - (assignableTo(left, right) || assignableTo(right, left)) && ((left, right) match { + (assignableTo(left, right, false) || assignableTo(right, left, false)) && ((left, right) match { case (l, r) if comparableType(l) && comparableType(r) => true case (NilType, r) if isPointerType(r) => true case (l, NilType) if isPointerType(l) => true @@ -28,7 +28,7 @@ trait Comparability extends BaseProperty { this: TypeInfoImpl => lazy val ghostComparableTypes: Property[(Type, Type)] = createFlatProperty[(Type, Type)] { case (left, right) => s"$left is not comparable in ghost with $right" } { - case (Single(left), Single(right)) => assignableTo(left, right) || assignableTo(right, left) + case (Single(left), Single(right)) => assignableTo(left, right, false) || assignableTo(right, left, false) case _ => false } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala index 4d2704ca9..3a388b58c 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala @@ -13,29 +13,34 @@ trait Convertibility extends BaseProperty { this: TypeInfoImpl => // TODO: check where convertibility and where assignability is required. - lazy val convertibleTo: Property[(Type, Type)] = createFlatProperty[(Type, Type)] { - case (left, right) => s"$left is not convertible to $right" + lazy val convertibleTo: Property[(Type, Type, Boolean)] = createFlatPropertyWithReason[(Type, Type, Boolean)] { + case (left, right, _) => s"$left is not convertible to $right" } { - case (Single(lst), Single(rst)) => (lst, rst) match { - case (left, right) if assignableTo(left, right) => true - case (IntT(_), Float32T) => true - case (IntT(_), Float64T) => true - case (Float32T, IntT(_)) => true - case (Float64T, IntT(_)) => true - case (IntT(_), IntT(_)) => true - case (SliceT(IntT(config.typeBounds.Byte)), StringT) => true - case (StringT, SliceT(IntT(config.typeBounds.Byte))) => true - case (IntT(_), PermissionT) => true + case (Single(lst), Single(rst), mayInit) => (lst, rst) match { + case (left, right) if assignableTo(left, right, mayInit) => successProp + case (left, right) if mayInit && assignableTo(left, right, false) => + // this branch is only for providing better error messages, + // as it is logically unnecessary + failedProp(s"Type $right may not be converted to type $left in code that may run during the initialization " + + s"of this current package.") + case (IntT(_), Float32T) => successProp + case (IntT(_), Float64T) => successProp + case (Float32T, IntT(_)) => successProp + case (Float64T, IntT(_)) => successProp + case (IntT(_), IntT(_)) => successProp + case (SliceT(IntT(config.typeBounds.Byte)), StringT) => successProp + case (StringT, SliceT(IntT(config.typeBounds.Byte))) => successProp + case (IntT(_), PermissionT) => successProp case (left, right) => (underlyingType(left), underlyingType(right)) match { - case (l, r) if identicalTypes(l, r) => true - case (IntT(_), IntT(_)) => true + case (l, r) if identicalTypes(l, r) => successProp + case (IntT(_), IntT(_)) => successProp case (ActualPointerT(l), ActualPointerT(r)) if identicalTypes(underlyingType(l), underlyingType(r)) && - !(left.isInstanceOf[DeclaredT] && right.isInstanceOf[DeclaredT]) => true + !(left.isInstanceOf[DeclaredT] && right.isInstanceOf[DeclaredT]) => successProp case (GhostPointerT(l), GhostPointerT(r)) if identicalTypes(underlyingType(l), underlyingType(r)) && - !(left.isInstanceOf[DeclaredT] && right.isInstanceOf[DeclaredT]) => true - case _ => false + !(left.isInstanceOf[DeclaredT] && right.isInstanceOf[DeclaredT]) => successProp + case _ => errorProp() } } - case _ => false + case _ => errorProp() } } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala index c25c4c9a3..fa86dc551 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala @@ -84,21 +84,33 @@ trait Enclosing { this: TypeInfoImpl => lazy val tryEnclosingOutline: PNode => Option[POutline] = down[Option[POutline]](None) { case x: POutline => Some(x) } - lazy val isEnclosingExplicitGhost: PNode => Boolean = - down(false){ case _: PGhostifier[_] => true } + lazy val tryEnclosingGlobalVarDeclaration: PNode => Option[PVarDecl] = + down[Option[PVarDecl]](None) { + case x: PVarDecl if isGlobalVarDeclaration(x) => Some(x) + case x: PVarDecl => + val parent = tree.parent(x).head + tryEnclosingGlobalVarDeclaration(parent) + } lazy val isEnclosingGhost: PNode => Boolean = down(false){ case _: PGhostifier[_] | _: PGhostNode => true } - lazy val isEnclosingDomain: PNode => Boolean = - down(false){ case _: PDomainType => true } + def isEnclosingMayInit(n: PNode): Boolean = { + val cond1 = tryEnclosingFunctionOrMethod(n) match { + case Some(f: PFunctionDecl) => f.id.name == "init" || f.spec.mayBeUsedInInit + case Some(m: PMethodDecl) => m.spec.mayBeUsedInInit + case _ => false + } + val cond2 = tryEnclosingGlobalVarDeclaration(n) match { + case Some(_) => true + case _ => false + } + cond1 || cond2 + } def isGlobalVarDeclaration(n: PVarDecl): Boolean = enclosingCodeRoot(n).isInstanceOf[PPackage] - lazy val enclosingInterface: PNode => PInterfaceType = - down((_: PNode) => violation("Node does not root in an interface definition")) { case x: PInterfaceType => x } - lazy val tryEnclosingFunctionLit: PNode => Option[PFunctionLit] = down[Option[PFunctionLit]](None) { case x: PFunctionLit => Some(x) } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/BuiltInMemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/BuiltInMemberTyping.scala index f02d1cb32..ab159b3fb 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/BuiltInMemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/BuiltInMemberTyping.scala @@ -34,25 +34,32 @@ trait BuiltInMemberTyping extends BaseTyping { this: TypeInfoImpl => AbstractType( { - case (n, ts@PermissionT +: s +: v) => underlyingType(s) match { - case t: SliceT => v match { - case Vector(v: VariadicT) if assignableTo(v.elem, t.elem) => noMessages - case tail if tail.forall(assignableTo(_, t.elem)) => noMessages + case (n, ts@PermissionT +: s +: v) => + val mayInit = isEnclosingMayInit(n) + underlyingType(s) match { + case t: SliceT => v match { + case Vector(v: VariadicT) if assignableTo(v.elem, t.elem, mayInit) => noMessages + case tail if tail.forall(assignableTo(_, t.elem, mayInit)) => noMessages + case _ => appendTypeError(n, ts) + } case _ => appendTypeError(n, ts) } - case _ => appendTypeError(n, ts) - } case (n, ts) => appendTypeError(n, ts) }, { - case ts@PermissionT +: s +: v => underlyingType(s) match { - case t: SliceT => v match { - case Vector(v: VariadicT) if assignableTo(v.elem, t.elem) => FunctionT(ts, s) - case tail if tail.forall(assignableTo(_, t.elem)) => FunctionT(Vector(PermissionT, s, VariadicT(t.elem)), s) - case _ => Violation.violation(s"Unexpected pattern found for v: $v") + case ts@PermissionT +: s +: v => + underlyingType(s) match { + case t: SliceT => v match { + // we use the most permissive `mayInit` parameter here, as we cannot recover precise information + // about whether it is in "mayInit" regions of the code. + case Vector(v: VariadicT) if assignableTo(v.elem, t.elem, false) => + FunctionT(ts, s) + case tail if tail.forall(assignableTo(_, t.elem, false)) => + FunctionT(Vector(PermissionT, s, VariadicT(t.elem)), s) + case _ => Violation.violation(s"Unexpected pattern found for v: $v") + } + case t => Violation.violation(s"expected $s to have a slice type as underlying type, got $t instead") } - case t => Violation.violation(s"expected $s to have a slice type as underlying type, got $t instead") - } }) } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala index cc6e638f3..da745b6ab 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala @@ -225,11 +225,12 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case _: PFloatLit => ??? case n@PCompositeLit(t, lit) => + val mayInit = isEnclosingMayInit(n) val simplifiedT = t match { case PImplicitSizeArrayType(elem) => ArrayT(lit.elems.size, typeSymbType(elem)) case t: PType => typeSymbType(t) } - literalAssignableTo.errors(lit, simplifiedT)(n) + literalAssignableTo.errors(lit, simplifiedT, mayInit)(n) case f: PFunctionLit => capturedLocalVariables(f.decl).flatMap(v => addressable.errors(enclosingExpr(v).get)(v)) ++ @@ -237,7 +238,8 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => f.id.fold(noMessages)(id => wellDefID(id).out) ++ error(f, "Opaque function literals are not yet supported.", f.spec.isOpaque) - case n: PInvoke => { + case n: PInvoke => + val mayInit = isEnclosingMayInit(n) val (l, r) = (exprOrType(n.base), resolve(n)) (l,r) match { case (Right(_), Some(p: ap.Conversion)) => @@ -247,18 +249,32 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case _ => noMessages } error(n, "Only calls to pure functions and pure methods can be revealed: Cannot reveal a conversion.", n.reveal) ++ - convertibleTo.errors(exprType(p.arg), typ)(n) ++ + convertibleTo.errors(exprType(p.arg), typ, mayInit)(n) ++ isExpr(p.arg).out ++ argWithinBounds case (Left(callee), Some(c: ap.FunctionCall)) => - val isOpaque = c.callee match { + val (isOpaque, isMayInit, isImported, isPure) = c.callee match { case base: ap.Symbolic => base.symb match { - case f: st.Function => f.isOpaque - case m: st.MethodImpl => m.isOpaque - case _ => false + case f: st.Function => (f.isOpaque, f.decl.spec.mayBeUsedInInit, f.context != this, f.isPure) + case m: st.MethodImpl => + (m.isOpaque, m.decl.spec.mayBeUsedInInit, m.context != this, m.isPure) + case _ => (false, true, false, false) } } + // We disallow calling interface methods whose receiver type is an interface declared in the current package + // in initialization code, as it may be dispatched to a method that assumes the current package's invariant. + val cannotCallItfIfInit = c.callee match { + case base: ap.ReceivedMethod => + val typeRecv = typ(base.recv) + val isLocallyDefinedItfType = isLocallyDefinedContextualType(typeRecv) && isInterfaceType(typeRecv) + if (isLocallyDefinedItfType && mayInit) + error(n, "Call to interface method whose receiver is of an interface type defined in this package is disallowed within code that may run during the initialization of this package.") + else + noMessages + case _ => + noMessages + } val onlyRevealOpaqueFunc = error(n, "Cannot reveal call to non-opaque function.", n.reveal && !isOpaque) val isCallToInit = @@ -269,14 +285,17 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case FunctionT(args, _) => // TODO: add special assignment if (n.spec.nonEmpty) wellDefCallWithSpec(n) else if (n.args.isEmpty && args.isEmpty) noMessages - else multiAssignableTo.errors(n.args map exprType, args)(n) ++ n.args.flatMap(isExpr(_).out) + else multiAssignableTo.errors(n.args map exprType, args, mayInit)(n) ++ n.args.flatMap(isExpr(_).out) case t: AbstractType => t.messages(n, n.args map exprType) case t => error(n.base, s"type error: got $t but expected function type or AbstractType") } - onlyRevealOpaqueFunc ++ isCallToInit ++ wellTypedArgs + val mayInitSeparation = error(n, "Function called from 'mayInit' context is not 'mayInit'.", !isImported && (isEnclosingMayInit(n) && !(isMayInit || isPure))) + cannotCallItfIfInit ++ onlyRevealOpaqueFunc ++ isCallToInit ++ wellTypedArgs ++ mayInitSeparation case (Left(_), Some(_: ap.ClosureCall)) => - error(n, "Only calls to pure functions and pure methods can be revealed: Cannot reveal a closure call.", n.reveal) ++ wellDefCallWithSpec(n) + error(n, "Only calls to pure functions and pure methods can be revealed: Cannot reveal a closure call.", n.reveal) ++ + wellDefCallWithSpec(n) ++ + error(n, "Closures may not be called from code that may be executed during initialization", mayInit) case (Left(callee), Some(p: ap.PredicateCall)) => // TODO: Maybe move case to other file val pureReceiverMsgs = p.predicate match { @@ -293,7 +312,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => val argAssignMsgs = exprType(callee) match { case FunctionT(args, _) => // TODO: add special assignment if (n.args.isEmpty && args.isEmpty) noMessages - else multiAssignableTo.errors(n.args map exprType, args)(n) ++ n.args.flatMap(isExpr(_).out) + else multiAssignableTo.errors(n.args map exprType, args, mayInit)(n) ++ n.args.flatMap(isExpr(_).out) case t: AbstractType => t.messages(n, n.args map exprType) case t => error(n.base, s"type error: got $t but expected function type or AbstractType") } @@ -303,18 +322,20 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => val wellTypedArguments = exprType(callee) match { case PredT(args) => if (n.args.isEmpty && args.isEmpty) noMessages - else multiAssignableTo.errors(n.args map exprType, args)(n) ++ n.args.flatMap(isExpr(_).out) + else multiAssignableTo.errors(n.args map exprType, args, mayInit)(n) ++ n.args.flatMap(isExpr(_).out) case c => Violation.violation(s"This case should be unreachable, but got $c") } error(n, "Only calls to pure functions and pure methods can be revealed: Cannot reveal a predicate expression instance.", n.reveal) ++ wellTypedArguments case _ => error(n, s"expected a call to a conversion, function, or predicate, but got $n") } - } - case PBitNegation(op) => isExpr(op).out ++ assignableTo.errors(typ(op), UNTYPED_INT_CONST)(op) + case n@PBitNegation(op) => + val mayInit = isEnclosingMayInit(n) + isExpr(op).out ++ assignableTo.errors(typ(op), UNTYPED_INT_CONST, mayInit)(op) case n@PIndexedExp(base, index) => + val mayInit = isEnclosingMayInit(n) isExpr(base).out ++ isExpr(index).out ++ { val baseType = exprType(base) val idxType = exprType(index) @@ -345,9 +366,9 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => // between two types, which is less precise. Because of this limitation, and with the goal of handling // untyped literals, we introduce an extra condition here. This makes the type checker of Gobra accept Go // expressions that are not accepted by the compiler. - val assignableToIdxType = error(index, s"$idxType is not assignable to map key of $key", !assignableTo(idxType, key)) + val assignableToIdxType = error(index, s"$idxType is not assignable to map key of $key", !assignableTo(idxType, key, mayInit)) if (assignableToIdxType.nonEmpty) { - error(index, s"$underlyingIdxType is not assignable to map key of $key", !assignableTo(underlyingIdxType, key)) + error(index, s"$underlyingIdxType is not assignable to map key of $key", !assignableTo(underlyingIdxType, key, mayInit)) } else { assignableToIdxType } @@ -357,9 +378,9 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => // between two types, which is less precise. Because of this limitation, and with the goal of handling // untyped literals, we introduce an extra condition here. This makes the type checker of Gobra accept Go // expressions that are not accepted by the compiler. - val assignableToIdxType = error(index, s"$idxType is not assignable to map key of $key", !assignableTo(idxType, key)) + val assignableToIdxType = error(index, s"$idxType is not assignable to map key of $key", !assignableTo(idxType, key, mayInit)) if (assignableToIdxType.nonEmpty) { - error(index, s"$underlyingIdxType is not assignable to map key of $key", !assignableTo(underlyingIdxType, key)) + error(index, s"$underlyingIdxType is not assignable to map key of $key", !assignableTo(underlyingIdxType, key, mayInit)) } else { assignableToIdxType } @@ -420,7 +441,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case (bt, lt, ht, ct) => error(n, s"invalid slice with base $bt and indexes $lt, $ht, and $ct") }) - case n@PTypeAssertion(base, typ) => + case PTypeAssertion(base, typ) => isExpr(base).out ++ isType(typ).out ++ { val baseT = exprType(base) underlyingType(baseT) match { @@ -431,36 +452,43 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => } } - case n@PReceive(e) => isExpr(e).out ++ (exprType(e) match { + case PReceive(e) => isExpr(e).out ++ (exprType(e) match { case ChannelT(_, ChannelModus.Bi | ChannelModus.Recv) => noMessages case t => error(e, s"expected receive-permitting channel but got $t") }) - case n@PReference(e) => isExpr(e).out ++ effAddressable.errors(e)(e) + case PReference(e) => isExpr(e).out ++ effAddressable.errors(e)(e) - case n@PNegation(e) => isExpr(e).out ++ assignableTo.errors(exprType(e), BooleanT)(e) + case n@PNegation(e) => + val mayInit = isEnclosingMayInit(n) + isExpr(e).out ++ assignableTo.errors(exprType(e), BooleanT, mayInit)(e) case n: PBinaryExp[_,_] => + val mayInit = isEnclosingMayInit(n) (n, exprOrTypeType(n.left), exprOrTypeType(n.right)) match { case (_: PEquals | _: PUnequals, l, r) => comparableTypes.errors(l, r)(n) - case (_: PAnd | _: POr, l, r) => assignableTo.errors(l, AssertionT)(n.left) ++ assignableTo.errors(r, AssertionT)(n.right) + case (_: PAnd | _: POr, l, r) => assignableTo.errors(l, AssertionT, mayInit)(n.left) ++ + assignableTo.errors(r, AssertionT, mayInit)(n.right) case (_: PLess | _: PAtMost | _: PGreater | _: PAtLeast, l, r) => (l,r) match { case (StringT, StringT) => noMessages case (Float32T, Float32T) => noMessages case (Float64T, Float64T) => noMessages case _ if l == PermissionT || r == PermissionT => - assignableTo.errors(l, PermissionT)(n.left) ++ assignableTo.errors(r, PermissionT)(n.right) - case _ => assignableTo.errors(l, UNTYPED_INT_CONST)(n.left) ++ assignableTo.errors(r, UNTYPED_INT_CONST)(n.right) + assignableTo.errors(l, PermissionT, mayInit)(n.left) ++ + assignableTo.errors(r, PermissionT, mayInit)(n.right) + case _ => + assignableTo.errors(l, UNTYPED_INT_CONST, mayInit)(n.left) ++ + assignableTo.errors(r, UNTYPED_INT_CONST, mayInit)(n.right) } case (_: PAdd, StringT, StringT) => noMessages case (_: PAdd | _: PSub | _: PMul | _: PDiv, l, r) if Set(l, r).intersect(Set(Float32T, Float64T)).nonEmpty => mergeableTypes.errors(l, r)(n) case (_: PAdd | _: PSub | _: PMul | _: PMod | _: PDiv, l, r) if l == PermissionT || r == PermissionT || getTypeFromCtxt(n).contains(PermissionT) => - assignableTo.errors(l, PermissionT)(n.left) ++ assignableTo.errors(r, PermissionT)(n.right) + assignableTo.errors(l, PermissionT, mayInit)(n.left) ++ assignableTo.errors(r, PermissionT, mayInit)(n.right) case (_: PAdd | _: PSub | _: PMul | _: PMod | _: PDiv | _: PBitAnd | _: PBitOr | _: PBitXor | _: PBitClear, l, r) => - val lIsInteger = assignableTo.errors(l, UNTYPED_INT_CONST)(n.left) - val rIsInteger = assignableTo.errors(r, UNTYPED_INT_CONST)(n.right) + val lIsInteger = assignableTo.errors(l, UNTYPED_INT_CONST, mayInit)(n.left) + val rIsInteger = assignableTo.errors(r, UNTYPED_INT_CONST, mayInit)(n.right) val typesAreMergeable = mergeableTypes.errors(l, r)(n) val exprWithinBounds = { if(typesAreMergeable.isEmpty) { @@ -480,7 +508,8 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => } lIsInteger ++ rIsInteger ++ typesAreMergeable ++ exprWithinBounds case (_: PShiftLeft, l, r) => - val integerOperands = assignableTo.errors(l, UNTYPED_INT_CONST)(n.left) ++ assignableTo.errors(r, UNTYPED_INT_CONST)(n.right) + val integerOperands = assignableTo.errors(l, UNTYPED_INT_CONST, mayInit)(n.left) ++ + assignableTo.errors(r, UNTYPED_INT_CONST, mayInit)(n.right) if (integerOperands.isEmpty) { intConstantEval(n.right.asInstanceOf[PExpression]) match { case Some(v) => @@ -499,7 +528,8 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => } } else integerOperands case (_: PShiftRight, l, r) => - val integerOperands = assignableTo.errors(l, UNTYPED_INT_CONST)(n.left) ++ assignableTo.errors(r, UNTYPED_INT_CONST)(n.right) + val integerOperands = assignableTo.errors(l, UNTYPED_INT_CONST, mayInit)(n.left) ++ + assignableTo.errors(r, UNTYPED_INT_CONST, mayInit)(n.right) if (integerOperands.isEmpty) { (intConstantEval(n.right.asInstanceOf[PExpression]) match { case Some(v) => @@ -536,8 +566,9 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case _: PNew => noMessages case m@PMake(typ, args) => + val mayInit = isEnclosingMayInit(m) args.flatMap { arg => - assignableTo.errors(exprType(arg), INT_TYPE)(arg) ++ + assignableTo.errors(exprType(arg), INT_TYPE, mayInit)(arg) ++ error(arg, s"arguments to make must be non-negative", intConstantEval(arg).exists(_ < 0)) } ++ (underlyingTypeP(typ) match { case None => violation(s"unexpected case reached: underlyingTypeP($typ) returned None") @@ -581,6 +612,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => } case p@PPredConstructor(base, _) => { + val mayInit = isEnclosingMayInit(p) def wellTypedApp(base: PPredConstructorBase): Messages = miscType(base) match { case FunctionT(args, AssertionT) => val unappliedPositions = p.args.zipWithIndex.filter(_._1.isEmpty).map(_._2) @@ -589,7 +621,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => if (givenArgs.isEmpty && expectedArgs.isEmpty) { noMessages } else { - multiAssignableTo.errors(givenArgs map exprType, expectedArgs)(p) ++ + multiAssignableTo.errors(givenArgs map exprType, expectedArgs, mayInit)(p) ++ p.args.flatMap(x => x.map(isExpr(_).out).getOrElse(noMessages)) } @@ -611,7 +643,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => if (givenArgs.isEmpty && args.isEmpty) { noMessages } else { - multiAssignableTo.errors(givenArgs map exprType, args)(p) ++ + multiAssignableTo.errors(givenArgs map exprType, args, mayInit)(p) ++ p.args.flatMap(x => x.map(isExpr(_).out).getOrElse(noMessages)) } case t => error(p, s"expected function type for resolved AbstractType but got $t") @@ -683,7 +715,8 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case p => violation(s"expected conversion, function call, predicate call, or predicate expression instance, but got $p") } - case PIndexedExp(base, index) => + case i@PIndexedExp(base, index) => + val mayInit = isEnclosingMayInit(i) val baseType = exprType(base) val idxType = exprType(index) (underlyingType(baseType), underlyingType(idxType)) match { @@ -694,9 +727,9 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case (SliceT(elem), IntT(_)) => elem case (GhostSliceT(elem), IntT(_)) => elem case (VariadicT(elem), IntT(_)) => elem - case (MapT(key, elem), underlyingIdxType) if assignableTo(idxType, key) || assignableTo(underlyingIdxType, key) => + case (MapT(key, elem), underlyingIdxType) if assignableTo(idxType, key, mayInit) || assignableTo(underlyingIdxType, key, mayInit) => InternalSingleMulti(elem, InternalTupleT(Vector(elem, BooleanT))) - case (MathMapT(key, elem), underlyingIdxType) if assignableTo(idxType, key) || assignableTo(underlyingIdxType, key) => + case (MathMapT(key, elem), underlyingIdxType) if assignableTo(idxType, key, mayInit) || assignableTo(underlyingIdxType, key, mayInit) => InternalSingleMulti(elem, InternalTupleT(Vector(elem, BooleanT))) case (bt, it) => violation(s"$it is not a valid index for the the base $bt") } @@ -730,9 +763,10 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => if (isGhostLocation(exp)) GhostPointerT(exprType(exp)) else ActualPointerT(exprType(exp)) case n: PAnd => // is boolean if left and right argument are boolean, otherwise is an assertion + val mayInit = isEnclosingMayInit(n) val lt = exprType(n.left) val rt = exprType(n.right) - if (assignableTo(lt, BooleanT) && assignableTo(rt, BooleanT)) BooleanT else AssertionT + if (assignableTo(lt, BooleanT, mayInit) && assignableTo(rt, BooleanT, mayInit)) BooleanT else AssertionT case _: PNegation | _: PEquals | _: PUnequals | _: POr | _: PLess | _: PAtMost | _: PGreater | _: PAtLeast => @@ -1058,12 +1092,13 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => } private[typing] def wellDefCallWithSpec(n: PInvoke): Messages = { + val mayInit = isEnclosingMayInit(n) val base = n.base.asInstanceOf[PExpression] val closureMatchesSpec = wellDefIfClosureMatchesSpec(base, n.spec.get) val assignableArgs = (exprType(base), miscType(n.spec.get)) match { case (tC: FunctionT, _: FunctionT) => n.args.flatMap(isExpr(_).out) ++ ( if (n.args.isEmpty && tC.args.isEmpty) noMessages - else multiAssignableTo.errors(n.args map exprType, tC.args)(base)) + else multiAssignableTo.errors(n.args map exprType, tC.args, mayInit)(base)) case (tC, _) => error(base, s"expected function type, but got $tC") } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ImportTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ImportTyping.scala index fcc2ccab4..34464a082 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ImportTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ImportTyping.scala @@ -7,23 +7,19 @@ package viper.gobra.frontend.info.implementation.typing import org.bitbucket.inkytonik.kiama.util.Messaging.{message, noMessages} -import viper.gobra.GoVerifier -import viper.gobra.ast.frontend.{PExplicitQualifiedImport, PImplicitQualifiedImport, PImport, PUnqualifiedImport} -import viper.gobra.frontend.Config +import viper.gobra.ast.frontend._ import viper.gobra.frontend.info.implementation.TypeInfoImpl trait ImportTyping extends BaseTyping { this: TypeInfoImpl => lazy val wellDefImport: WellDefinedness[PImport] = createWellDef { imp => - (if (config.enableLazyImports) { - imp.importPres.flatMap(importPre => message(importPre, s"Import preconditions are not allowed when executing ${GoVerifier.name} with ${Config.enableLazyImportOptionPrettyPrinted}")) - } else { - noMessages - }) ++ (imp match { + val qualifierMsgs = imp match { case _: PExplicitQualifiedImport => noMessages case _: PUnqualifiedImport => noMessages // this case should never occur as these nodes should get converted in the parse postprocessing step case n: PImplicitQualifiedImport => message(n, s"Explicit qualifier could not be derived") - }) + } + val preHasOldExps = hasOldExpression(imp.importPres) + qualifierMsgs ++ preHasOldExps } } \ No newline at end of file diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala index d7c03e0f6..68cf82a15 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala @@ -7,11 +7,10 @@ package viper.gobra.frontend.info.implementation.typing import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages} -import viper.gobra.GoVerifier import viper.gobra.ast.frontend._ -import viper.gobra.frontend.Config import viper.gobra.frontend.info.base.SymbolTable.MPredicateSpec import viper.gobra.frontend.info.implementation.TypeInfoImpl +import viper.gobra.frontend.info.implementation.property.{AssignMode, StrictAssignMode} import viper.gobra.util.Constants trait MemberTyping extends BaseTyping { this: TypeInfoImpl => @@ -36,23 +35,25 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl => case b: PConstDecl => b.specs.flatMap(wellDefConstSpec) case g: PVarDecl if isGlobalVarDeclaration(g) => - if (config.enableLazyImports) { - error(g, s"Global variables are not allowed when executing ${GoVerifier.name} with ${Config.enableLazyImportOptionPrettyPrinted}") + // HACK: without this explicit check, Gobra does not find repeated declarations + // of global variables. This has to do with the changes introduced in PR #186. + // We need this check nonetheless because the checks performed in the "true" branch + // assume that the ids are well-defined. + val idsOkMsgs = g.left.flatMap(l => wellDefID(l).out) + // A common pattern that appears in some codebases is to have global assignments like the following + // var _ pkg.I = T{} + // or similar. The purpose is to assert, at compile time, that T is a subtype of pkg.I. To allow for + // these patterns, we introduce a special case when the lhs contains only wildcards. This is fine, + // because we will not be able to use the expression on the rhs as a receiver to a method call. + val mayBeSpecialCase = g.left.forall(_.isInstanceOf[PWildcard]) && + StrictAssignMode(left = g.left.size, right = g.right.size) == AssignMode.Single && + g.typ.nonEmpty + if (idsOkMsgs.isEmpty) { + g.right.flatMap(isExpr(_).out) ++ + declarableTo.errors(g.right map exprType, g.typ map typeSymbType, g.left map idType, !mayBeSpecialCase)(g) ++ + acyclicGlobalDeclaration.errors(g)(g) } else { - // HACK: without this explicit check, Gobra does not find repeated declarations - // of global variables. This has to do with the changes introduced in PR #186. - // We need this check nonetheless because the checks performed in the "true" branch - // assume that the ids are well-defined. - val idsOkMsgs = g.left.flatMap(l => wellDefID(l).out) - if (idsOkMsgs.isEmpty) { - val isGhost = isEnclosingGhost(g) - g.right.flatMap(isExpr(_).out) ++ - declarableTo.errors(g.right map exprType, g.typ map typeSymbType, g.left map idType)(g) ++ - error(g, s"Currently, global variables cannot be made ghost", isGhost) ++ - acyclicGlobalDeclaration.errors(g)(g) - } else { - idsOkMsgs - } + idsOkMsgs } case s: PActualStatement => wellDefStmt(s).out @@ -91,6 +92,7 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl => private def wellDefConstSpec(spec: PConstSpec): Messages = { val hasInitExpr = error(spec, s"missing init expr for ${spec.left}", spec.right.isEmpty) + val mayInit = isEnclosingMayInit(spec) lazy val canAssignInitExpr = error( spec, s"${spec.right} cannot be assigned to ${spec.left}", @@ -98,8 +100,8 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl => // between two types, which is less precise. Because of this limitation, and with the goal of handling // untyped literals, we introduce an extra condition here. This makes the type checker of Gobra accept Go // expressions that are not accepted by the compiler. - !(multiAssignableTo(spec.left.map(typ), spec.right.map(typ)) || - multiAssignableTo(spec.left.map(n => underlyingType(typ(n))), spec.right.map(typ))) + !(multiAssignableTo(spec.left.map(typ), spec.right.map(typ), mayInit) || + multiAssignableTo(spec.left.map(n => underlyingType(typ(n))), spec.right.map(typ), mayInit)) ) lazy val constExprMsgs = spec.right.flatMap(wellDefIfConstExpr) // helps producing less redundant error messages @@ -113,9 +115,7 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl => private def wellDefIfInitBlock(n: PFunctionDecl): Messages = { val isInitFunc = n.id.name == Constants.INIT_FUNC_NAME - if (isInitFunc && config.enableLazyImports) { - error(n, s"Init functions are not supported when executing ${GoVerifier.name} with ${Config.enableLazyImportOptionPrettyPrinted}") - } else if (isInitFunc) { + if (isInitFunc) { val errorMsgEmptySpec = s"Currently, ${Constants.INIT_FUNC_NAME} blocks cannot have specification. Instead, use package postconditions and import preconditions." val errorMsgNoInOut = s"func ${Constants.INIT_FUNC_NAME} must have no arguments and no return values" diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ProgramTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ProgramTyping.scala index f0641c73e..854846ab8 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ProgramTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ProgramTyping.scala @@ -7,10 +7,8 @@ package viper.gobra.frontend.info.implementation.typing import org.bitbucket.inkytonik.kiama.util.Entity -import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, message} -import viper.gobra.GoVerifier -import viper.gobra.ast.frontend.{PExpression, POld, PPackage, PProgram, PVarDecl} -import viper.gobra.frontend.Config +import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error} +import viper.gobra.ast.frontend._ import viper.gobra.frontend.info.base.{SymbolTable => st} import viper.gobra.frontend.info.implementation.TypeInfoImpl import viper.gobra.frontend.info.implementation.property.{AssignMode, StrictAssignMode} @@ -19,35 +17,33 @@ import viper.gobra.util.Violation trait ProgramTyping extends BaseTyping { this: TypeInfoImpl => lazy val wellDefProgram: WellDefinedness[PProgram] = createWellDef { - case PProgram(_, posts, imports, members) => - if (config.enableLazyImports) { - posts.flatMap(post => message(post, s"Init postconditions are not allowed when executing ${GoVerifier.name} with ${Config.enableLazyImportOptionPrettyPrinted}")) - } else { - // Obtains global variable declarations sorted by the order in which they appear in the file - val sortedByPosDecls: Vector[PVarDecl] = { - val unsortedDecls: Vector[PVarDecl] = members.collect{ case d: PVarDecl => d } - // we require a package to be able to obtain position information - val pkgOpt: Option[PPackage] = unsortedDecls.headOption.flatMap(tryEnclosingPackage) - // sort declarations by the order in which they appear in the program - unsortedDecls.sortBy{ decl => - pkgOpt.get.positions.positions.getStart(decl) match { - case Some(pos) => (pos.line, pos.column) - case _ => Violation.violation(s"Could not find position information of $decl.") - } + case PProgram(_, pkgInvs, _, friends, members) => + // Obtains global variable declarations sorted by the order in which they appear in the file + val sortedByPosDecls: Vector[PVarDecl] = { + val unsortedDecls: Vector[PVarDecl] = members.collect{ case d: PVarDecl => d; case PExplicitGhostMember(d: PVarDecl) => d } + // we require a package to be able to obtain position information + val pkgOpt: Option[PPackage] = unsortedDecls.headOption.flatMap(tryEnclosingPackage) + // sort declarations by the order in which they appear in the program + unsortedDecls.sortBy{ decl => + pkgOpt.get.positions.positions.getStart(decl) match { + case Some(pos) => (pos.line, pos.column) + case _ => Violation.violation(s"Could not find position information of $decl.") } } - // HACK: without this explicit check, Gobra does not find repeated declarations - // of global variables. This has to do with the changes introduced in PR #186. - // We need this check nonetheless because the checks performed in the "true" branch - // assume that the ids are well-defined. - val idsOkMsgs = sortedByPosDecls.flatMap(d => d.left).flatMap(l => wellDefID(l).out) - if (idsOkMsgs.isEmpty) { - globalDeclSatisfiesDepOrder(sortedByPosDecls) ++ - hasOldExpression(posts) ++ - hasOldExpression(imports.flatMap(_.importPres)) - } else { - idsOkMsgs - } + } + // HACK: without this explicit check, Gobra does not find repeated declarations + // of global variables. This has to do with the changes introduced in PR #186. + // We need this check nonetheless because the checks performed in the "true" branch + // assume that the ids are well-defined. + val idsOkMsgs = sortedByPosDecls.flatMap(d => d.left).flatMap(l => wellDefID(l).out) + if (idsOkMsgs.isEmpty) { + val globalDeclsInRightOrder = globalDeclSatisfiesDepOrder(sortedByPosDecls) + val noOldExprs = + hasOldExpression(pkgInvs.map(_.inv)) ++ + hasOldExpression(friends.map(_.assertion)) + globalDeclsInRightOrder ++ noOldExprs + } else { + idsOkMsgs } } @@ -94,10 +90,10 @@ trait ProgramTyping extends BaseTyping { this: TypeInfoImpl => } } - private def hasOldExpression(posts: Vector[PExpression]): Messages = { + private[typing] def hasOldExpression(posts: Vector[PExpression]): Messages = { posts.flatMap{n => val hasOld = allChildren(n).exists(_.isInstanceOf[POld]) - error(n, "'old' expressions cannot occur in init-postconditions and import-preconditions", hasOld) + error(n, "'old' expressions cannot occur in import-preconditions, friend clause assertions, and package invariants", hasOld) } } } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala index 66acbe12e..6b1e1dc08 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala @@ -29,13 +29,20 @@ trait StmtTyping extends BaseTyping { this: TypeInfoImpl => case PConstDecl(decls) => decls flatMap { case n@PConstSpec(typ, right, left) => + val mayInit = isEnclosingMayInit(n) right.flatMap(isExpr(_).out) ++ - declarableTo.errors(right map exprType, typ map typeSymbType, left map idType)(n) + declarableTo.errors(right map exprType, typ map typeSymbType, left map idType, mayInit)(n) } case n@PVarDecl(typ, right, left, _) => - right.flatMap(isExpr(_).out) ++ - declarableTo.errors(right map exprType, typ map typeSymbType, left map idType)(n) + if (isGlobalVarDeclaration(n)) { + // in this case, the checks occur in MemberTyping + noMessages + } else { + val mayInit = isEnclosingMayInit(n) + right.flatMap(isExpr(_).out) ++ + declarableTo.errors(right map exprType, typ map typeSymbType, left map idType, mayInit)(n) + } case n: PTypeDecl => isType(n.right).out ++ (n.right match { case s: PStructType => @@ -49,31 +56,37 @@ trait StmtTyping extends BaseTyping { this: TypeInfoImpl => case n@PExpressionStmt(exp) => isExpr(exp).out ++ isExecutable.errors(exp)(n) case n@PSendStmt(chn, msg) => + val mayInit = isEnclosingMayInit(n) isExpr(chn).out ++ isExpr(msg).out ++ ((exprType(chn), exprType(msg)) match { - case (ChannelT(elem, ChannelModus.Bi | ChannelModus.Send), t) => assignableTo.errors(t, elem)(n) + case (ChannelT(elem, ChannelModus.Bi | ChannelModus.Send), t) => assignableTo.errors(t, elem, mayInit)(n) case (chnt, _) => error(n, s"type error: got $chnt but expected send-permitting channel") }) case n@PAssignment(rights, lefts) => + val mayInit = isEnclosingMayInit(n) rights.flatMap(isExpr(_).out) ++ lefts.flatMap(isExpr(_).out) ++ - lefts.flatMap(a => assignable.errors(a)(a)) ++ multiAssignableTo.errors(rights map exprType, lefts map exprType)(n) + lefts.flatMap(a => assignable.errors(a)(a)) ++ + multiAssignableTo.errors(rights map exprType, lefts map exprType, mayInit)(n) case n@PAssignmentWithOp(right, op@(_: PShiftLeftOp | _: PShiftRightOp), left) => + val mayInit = isEnclosingMayInit(n) isExpr(right).out ++ isExpr(left).out ++ assignable.errors(left)(n) ++ compatibleWithAssOp.errors(exprType(left), op)(n) ++ - assignableTo.errors(exprType(right), UNTYPED_INT_CONST)(n) + assignableTo.errors(exprType(right), UNTYPED_INT_CONST, mayInit)(n) case n@PAssignmentWithOp(right, op, left) => + val mayInit = isEnclosingMayInit(n) isExpr(right).out ++ isExpr(left).out ++ assignable.errors(left)(n) ++ compatibleWithAssOp.errors(exprType(left), op)(n) ++ - assignableTo.errors(exprType(right), exprType(left))(n) + assignableTo.errors(exprType(right), exprType(left), mayInit)(n) case n@PShortVarDecl(rights, lefts, _) => + val mayInit = isEnclosingMayInit(n) // TODO: check that at least one of the variables is new if (lefts.forall(pointsToData)) rights.flatMap(isExpr(_).out) ++ - multiAssignableTo.errors(rights map exprType, lefts map idType)(n) + multiAssignableTo.errors(rights map exprType, lefts map idType, mayInit)(n) else error(n, s"at least one assignee in $lefts points to a type") case _: PLabeledStmt => noMessages @@ -112,37 +125,41 @@ trait StmtTyping extends BaseTyping { this: TypeInfoImpl => comparableTypes.errors(exprType(cond), BooleanT)(n) ++ error(n, noTerminationMeasureMsg, isGhost && spec.terminationMeasure.isEmpty) - case PShortForRange(range, shorts, _, _, _) => + case r@PShortForRange(range, shorts, _, _, _) => + val mayInit = isEnclosingMayInit(r) underlyingType(exprType(range.exp)) match { case _ : ArrayT | _ : SliceT => - multiAssignableTo.errors(Vector(miscType(range)), shorts map idType)(range) ++ - assignableTo.errors(miscType(range), idType(range.enumerated))(range) - case MapT(key, _) => multiAssignableTo.errors(Vector(miscType(range)), shorts map idType)(range) ++ - assignableTo.errors((SetT(key), idType(range.enumerated)))(range) + multiAssignableTo.errors(Vector(miscType(range)), shorts map idType, mayInit)(range) ++ + assignableTo.errors(miscType(range), idType(range.enumerated), mayInit)(range) + case MapT(key, _) => multiAssignableTo.errors(Vector(miscType(range)), shorts map idType, mayInit)(range) ++ + assignableTo.errors((SetT(key), idType(range.enumerated), mayInit))(range) case t => error(range, s"range not supported for type $t") } - case PAssForRange(range, ass, _, _) => + case a@PAssForRange(range, ass, _, _) => + val mayInit = isEnclosingMayInit(a) underlyingType(exprType(range.exp)) match { case _ : ArrayT | _ : SliceT | _ : MapT => - multiAssignableTo.errors(Vector(miscType(range)), ass map exprType)(range) + multiAssignableTo.errors(Vector(miscType(range)), ass map exprType, mayInit)(range) case t => error(range, s"range not supported for type $t") } case n@PGoStmt(exp) => isExpr(exp).out ++ isExecutable.errors(exp)(n) case n: PSelectStmt => + val mayInit = isEnclosingMayInit(n) n.aRec.flatMap(rec => rec.ass.flatMap(isExpr(_).out) ++ - multiAssignableTo.errors(Vector(exprType(rec.recv)), rec.ass.map(exprType))(rec) ++ + multiAssignableTo.errors(Vector(exprType(rec.recv)), rec.ass.map(exprType), mayInit)(rec) ++ rec.ass.flatMap(a => assignable.errors(a)(a)) ) ++ n.sRec.flatMap(rec => if (rec.shorts.forall(pointsToData)) - multiAssignableTo.errors(Vector(exprType(rec.recv)), rec.shorts map idType)(rec) + multiAssignableTo.errors(Vector(exprType(rec.recv)), rec.shorts map idType, mayInit)(rec) else error(n, s"at least one assignee in ${rec.shorts} points to a type") ) case n@PReturn(exps) => + val mayInit = isEnclosingMayInit(n) exps.flatMap(isExpr(_).out) ++ { if (exps.nonEmpty) { val closureImplProof = tryEnclosingClosureImplementationProof(n) @@ -151,7 +168,7 @@ trait StmtTyping extends BaseTyping { this: TypeInfoImpl => if (res.isEmpty) return error(n, s"Statement does not root in a CodeRoot") if (!(res.get.result.outs forall wellDefMisc.valid)) return error(n, s"return cannot be checked because the enclosing signature is incorrect") } - multiAssignableTo.errors(exps map exprType, returnParamsAndTypes(n).map(_._1))(n) + multiAssignableTo.errors(exps map exprType, returnParamsAndTypes(n).map(_._1), mayInit)(n) } else noMessages // a return without arguments is always well-defined } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala index 50631f6f9..0d312a44c 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala @@ -7,15 +7,15 @@ package viper.gobra.frontend.info.implementation.typing import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages} - -import scala.collection.immutable.ListMap -import viper.gobra.ast.frontend._ -import viper.gobra.ast.frontend.{AstPattern => ap} +import viper.gobra.ast.frontend.{AstPattern => ap, _} +import viper.gobra.frontend.info.base.SymbolTable import viper.gobra.frontend.info.base.SymbolTable.{Embbed, Field} -import viper.gobra.frontend.info.base.Type.{StructT, _} +import viper.gobra.frontend.info.base.Type._ import viper.gobra.frontend.info.implementation.TypeInfoImpl import viper.gobra.frontend.info.implementation.property.UnderlyingType +import scala.collection.immutable.ListMap + trait TypeTyping extends BaseTyping { this: TypeInfoImpl => import viper.gobra.util.Violation._ @@ -66,7 +66,17 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => case t: PInterfaceType => val isRecursiveInterface = error(t, "invalid recursive interface", cyclicInterfaceDef(t)) if (isRecursiveInterface.isEmpty) { - addressableMethodSet(InterfaceT(t, this)).errors(t) ++ + val methodSet = addressableMethodSet(InterfaceT(t, this)) + val methodsContainMayInit = methodSet.exists { + case (_, (m, _)) => m match { + case m: SymbolTable.MethodSpec => + m.spec.spec.mayBeUsedInInit + case _ => false + } + } + + methodSet.errors(t) ++ + error(t, "Interface declaration contains methods annotated with 'mayInit'.", methodsContainMayInit) ++ containsRedeclarations(t) // temporary check } else { isRecursiveInterface diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala index 0c5877e96..5f38d0130 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala @@ -38,11 +38,12 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl => isExpr(n).out ++ isPureExpr(n) ++ error(n, "before expressions can only be used inside outline statements.", tryEnclosingOutline(n).isEmpty) - case PConditional(cond, thn, els) => + case n@PConditional(cond, thn, els) => + val mayInit = isEnclosingMayInit(n) // check whether all operands are actually expressions indeed isExpr(cond).out ++ isExpr(thn).out ++ isExpr(els).out ++ // check that `cond` is of type bool - assignableTo.errors(exprType(cond), BooleanT)(expr) ++ + assignableTo.errors(exprType(cond), BooleanT, mayInit)(expr) ++ // check that `thn` and `els` have a common type mergeableTypes.errors(exprType(thn), exprType(els))(expr) ++ // check that all subexpressions are pure. @@ -57,17 +58,19 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl => error(n, "found a quantifier without triggers.", config.requireTriggers && triggers.isEmpty) case n@PExists(vars, triggers, body) => + val mayInit = isEnclosingMayInit(n) // check whether all triggers are valid and consistent validTriggers(vars, triggers) ++ // check that the quantifier `body` is Boolean - assignableToSpec(body) ++ assignableTo.errors(exprType(body), BooleanT)(expr) ++ + assignableToSpec(body) ++ assignableTo.errors(exprType(body), BooleanT, mayInit)(expr) ++ // check that the user provided triggers when running with --requireTriggers error(n, "found a quantifier without triggers.", config.requireTriggers && triggers.isEmpty) case n: PImplication => + val mayInit = isEnclosingMayInit(n) isExpr(n.left).out ++ isExpr(n.right).out ++ // check whether the left operand is a Boolean expression - assignableTo.errors(exprType(n.left), BooleanT)(expr) ++ + assignableTo.errors(exprType(n.left), BooleanT, mayInit)(expr) ++ // check whether the right operand is either Boolean or an assertion assignableToSpec(n.right) @@ -84,8 +87,9 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl => n.ass.right.foldLeft(noMessages)((a, b) => a ++ isPureExpr(b)) case n: PAccess => + val mayInit = isEnclosingMayInit(n) val permWellDef = error(n.perm, s"expected perm or integer division expression, but got ${n.perm}", - !assignableTo(typ(n.perm), PermissionT)) + !assignableTo(typ(n.perm), PermissionT, mayInit)) val expWellDef = resolve(n.exp) match { case Some(_: ap.PredicateCall) => noMessages case Some(_: ap.PredExprInstance) => noMessages @@ -139,9 +143,10 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl => } case m@PMatchExp(exp, clauses) => + val mayInit = isEnclosingMayInit(m) val sameTypeE = allMergeableTypes.errors(clauses map { c => exprType(c.exp) })(exp) val patternE = m.caseClauses.flatMap(c => c.pattern match { - case p: PMatchAdt => assignableTo.errors(miscType(p), exprType(exp))(c) + case p: PMatchAdt => assignableTo.errors(miscType(p), exprType(exp), mayInit)(c) case _ => comparableTypes.errors((miscType(c.pattern), exprType(exp)))(c) }) val pureExpE = error(exp, "Expression has to be pure", !isPure(exp)(strong = false)) @@ -166,11 +171,13 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl => } } - case PGhostCollectionUpdate(seq, clauses) => isExpr(seq).out ++ (underlyingType(exprType(seq)) match { - case SequenceT(t) => clauses.flatMap(wellDefSeqUpdClause(t, _)) - case MathMapT(k, v) => clauses.flatMap(wellDefMapUpdClause(k, v, _)) - case t => error(seq, s"expected a sequence or mathematical map, but got $t") - }) + case n@PGhostCollectionUpdate(seq, clauses) => + val mayInit = isEnclosingMayInit(n) + isExpr(seq).out ++ (underlyingType(exprType(seq)) match { + case SequenceT(t) => clauses.flatMap(wellDefSeqUpdClause(t, _, mayInit)) + case MathMapT(k, v) => clauses.flatMap(wellDefMapUpdClause(k, v, _, mayInit)) + case t => error(seq, s"expected a sequence or mathematical map, but got $t") + }) case expr : PSequenceExp => expr match { case PRangeSequence(low, high) => isExpr(low).out ++ isExpr(high).out ++ { @@ -232,17 +239,18 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl => } } - private[typing] def wellDefMapUpdClause(keys: Type, values : Type, clause : PGhostCollectionUpdateClause) : Messages = { + private[typing] def wellDefMapUpdClause(keys: Type, values : Type, clause : PGhostCollectionUpdateClause, mayInit: Boolean) : Messages = { isExpr(clause.left).out ++ isExpr(clause.right).out ++ - assignableTo.errors(exprType(clause.left), keys)(clause.left) ++ - assignableTo.errors(exprType(clause.right), values)(clause.right) + assignableTo.errors(exprType(clause.left), keys, mayInit)(clause.left) ++ + assignableTo.errors(exprType(clause.right), values, mayInit)(clause.right) } - private[typing] def wellDefSeqUpdClause(seqTyp : Type, clause : PGhostCollectionUpdateClause) : Messages = exprType(clause.left) match { - case IntT(_) => isExpr(clause.left).out ++ isExpr(clause.right).out ++ - assignableTo.errors(exprType(clause.right), seqTyp)(clause.right) - case t => error(clause.left, s"expected an integer type but got $t") - } + private[typing] def wellDefSeqUpdClause(seqTyp : Type, clause : PGhostCollectionUpdateClause, mayInit: Boolean) : Messages = + exprType(clause.left) match { + case IntT(_) => isExpr(clause.left).out ++ isExpr(clause.right).out ++ + assignableTo.errors(exprType(clause.right), seqTyp, mayInit)(clause.right) + case t => error(clause.left, s"expected an integer type but got $t") + } private[typing] def ghostExprType(expr: PGhostExpression): Type = expr match { case POld(op) => exprType(op) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala index d25b98706..6cdf9bf74 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala @@ -44,12 +44,16 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => needsMeasureError } + private def pureFunctionsDoNotNeedMayInitMsg = "Pure functions and methods cannot open package invariants," + + "and thus, they must not be annotated with 'mayInit'." + private[typing] def wellDefIfPureMethod(member: PMethodDecl): Messages = { if (member.spec.isPure) { isSingleResultArg(member) ++ isSinglePureReturnExpr(member) ++ isPurePostcondition(member.spec) ++ - nonVariadicArguments(member.args) + nonVariadicArguments(member.args) ++ + error(member, pureFunctionsDoNotNeedMayInitMsg, member.spec.mayBeUsedInInit) } else noMessages } @@ -64,7 +68,8 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => isSingleResultArg(member) ++ isSinglePureReturnExpr(member) ++ isPurePostcondition(member.spec) ++ - nonVariadicArguments(member.args) + nonVariadicArguments(member.args) ++ + error(member, pureFunctionsDoNotNeedMayInitMsg, member.spec.mayBeUsedInInit) } else noMessages } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala index 198ce6433..227075fb3 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala @@ -43,7 +43,7 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => } case ax: PDomainAxiom => - assignableTo.errors(exprType(ax.exp), BooleanT)(ax) ++ isPureExpr(ax.exp) + assignableTo.errors(exprType(ax.exp), BooleanT, false)(ax) ++ isPureExpr(ax.exp) case f: PDomainFunction => error(f, s"Uninterpreted functions must have exactly one return argument", f.result.outs.size != 1) ++ @@ -56,8 +56,9 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => case t: AdtClauseT => val fieldTypes = fields.map(typ) val clauseFieldTypes = t.fields.map(_._2) + val mayInit = isEnclosingMayInit(m) error(m, s"Expected ${clauseFieldTypes.size} patterns, but got ${fieldTypes.size}", clauseFieldTypes.size != fieldTypes.size) ++ - fieldTypes.zip(clauseFieldTypes).flatMap(a => assignableTo.errors(a)(m)) + fieldTypes.zip(clauseFieldTypes).flatMap{case (a, b) => assignableTo.errors(a, b, mayInit)(m)} case _ => violation("Pattern matching only works on ADT Literals") } case PMatchValue(lit) => isPureExpr(lit) @@ -150,7 +151,7 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => } implicit lazy val wellDefSpec: WellDefinedness[PSpecification] = createWellDef { - case n@ PFunctionSpec(pres, preserves, posts, terminationMeasures, _, isPure, _, isOpaque) => + case n@ PFunctionSpec(pres, preserves, posts, terminationMeasures, _, isPure, _, isOpaque, _) => pres.flatMap(assignableToSpec) ++ preserves.flatMap(assignableToSpec) ++ posts.flatMap(assignableToSpec) ++ preserves.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++ pres.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++ @@ -179,7 +180,7 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => case PClosureSpecInstance(fName, ps) if ps.size > fArgs.size => error(c, s"spec instance $c has too many parameters (more than the arguments of function $fName)") case spec: PClosureSpecInstance if spec.paramKeys.isEmpty => - (spec.paramExprs zip fArgs) flatMap { case (exp, a) => assignableTo.errors((exprType(exp), a._2))(exp) } + (spec.paramExprs zip fArgs) flatMap { case (exp, a) => assignableTo.errors((exprType(exp), a._2, false))(exp) } case spec@PClosureSpecInstance(fName, ps) if spec.paramKeys.size == ps.size => val argsTypeMap = fArgs.collect { case (PNamedParameter(id, _), t) => id.name -> t @@ -190,7 +191,7 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => }._2 val wellDefIfCanAssignParams = (spec.paramKeys zip spec.paramExprs zip ps) flatMap { case ((k, exp), p) => argsTypeMap.get(k) match { - case Some(t: Type) => assignableTo.errors((exprType(exp), t))(exp) + case Some(t: Type) => assignableTo.errors((exprType(exp), t, false))(exp) case _ => error(p.key.get, s"could not find argument $k in the function $fName") }} wellDefIfNoDuplicateParams ++ wellDefIfCanAssignParams ++ c.paramExprs.flatMap(exp => isPureExpr(exp)) @@ -210,7 +211,8 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => } def assignableToSpec(e: PExpression): Messages = { - isExpr(e).out ++ assignableTo.errors(exprType(e), AssertionT)(e) ++ isWeaklyPureExpr(e) + val mayInit = isEnclosingMayInit(e) + isExpr(e).out ++ assignableTo.errors(exprType(e), AssertionT, mayInit)(e) ++ isWeaklyPureExpr(e) } private def illegalPreconditionNode(n: PNode): Messages = { diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala index 922729f74..bc6ec0fab 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala @@ -6,7 +6,7 @@ package viper.gobra.frontend.info.implementation.typing.ghost -import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error} +import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages} import viper.gobra.ast.frontend.{PClosureImplProof, AstPattern => ap, _} import viper.gobra.frontend.info.base.{SymbolTable => st} import viper.gobra.frontend.info.implementation.TypeInfoImpl @@ -23,13 +23,26 @@ trait GhostStmtTyping extends BaseTyping { this: TypeInfoImpl => case PInhale(exp) => assignableToSpec(exp) case PFold(acc) => wellDefFoldable(acc) case PUnfold(acc) => wellDefFoldable(acc) + case POpenDupPkgInv() => + tryEnclosingFunctionOrMethod(stmt) match { + case Some(m) => + val occursInInitMember = m match { + case f: PFunctionDecl if f.id.name == "init" || f.spec.mayBeUsedInInit => true + case m: PMethodDecl if m.spec.mayBeUsedInInit => true + case _ => false + } + error(stmt, "Trying to open the package invariant in a function that may execute during initialization is not allowed.", occursInInitMember) + case _ => noMessages + } case n@PPackageWand(wand, optBlock) => assignableToSpec(wand) ++ error(n, "ghost error: expected ghostifiable statement", !optBlock.forall(_.isInstanceOf[PGhostifiableStatement])) case PApplyWand(wand) => assignableToSpec(wand) - case PMatchStatement(exp, clauses, _) => clauses.flatMap(c => c.pattern match { - case p: PMatchAdt => assignableTo.errors(miscType(p), exprType(exp))(c) - case _ => comparableTypes.errors((miscType(c.pattern), exprType(exp)))(c) - }) ++ isPureExpr(exp) + case n@PMatchStatement(exp, clauses, _) => + val mayInit = isEnclosingMayInit(n) + clauses.flatMap(c => c.pattern match { + case p: PMatchAdt => assignableTo.errors(miscType(p), exprType(exp), mayInit)(c) + case _ => comparableTypes.errors((miscType(c.pattern), exprType(exp)))(c) + }) ++ isPureExpr(exp) } private[typing] def wellDefFoldable(acc: PPredicateAccess): Messages = { diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostLessPrinter.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostLessPrinter.scala index 8670e27d9..79ac2a072 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostLessPrinter.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostLessPrinter.scala @@ -21,7 +21,7 @@ class GhostLessPrinter(classifier: GhostClassifier) extends DefaultPrettyPrinter rec, filterParamList(args), filterResult(res), - PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty), + PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty, mayBeUsedInInit = false), // TODO: delete body.map( b => (PBodyParameterInfo(Vector.empty), b._2) ) ) ) @@ -32,7 +32,7 @@ class GhostLessPrinter(classifier: GhostClassifier) extends DefaultPrettyPrinter id, filterParamList(args), filterResult(res), - PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty), + PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty, mayBeUsedInInit = false), // TODO: delete body.map( b => (PBodyParameterInfo(Vector.empty), b._2) ) ) ) @@ -171,7 +171,7 @@ class GhostLessPrinter(classifier: GhostClassifier) extends DefaultPrettyPrinter case PFunctionLit(_, PClosureDecl(args, result, _, body)) => super.showMisc(PClosureDecl( filterParamList(args), filterResult(result), - PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty), + PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty, mayBeUsedInInit = false), // TODO: delete body.map( b => (PBodyParameterInfo(Vector.empty), b._2) ) )) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala index 8ec804f85..5fd361b5e 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala @@ -77,10 +77,11 @@ class GoifyingPrinter(info: TypeInfoImpl) extends DefaultPrettyPrinter { * Shows the Goified version of the function / method specification */ override def showSpec(spec: PSpecification): Doc = spec match { - case PFunctionSpec(pres, preserves, posts, measures, backendAnnotations, isPure, isTrusted, isOpaque) => + case PFunctionSpec(pres, preserves, posts, measures, backendAnnotations, isPure, isTrusted, isOpaque, mayInit) => (if (isPure) specComment <+> showPure else emptyDoc) <> (if (isOpaque) specComment <+> showOpaque else emptyDoc) <> (if (isTrusted) specComment <+> showTrusted else emptyDoc) <> + (if (mayInit) specComment <+> showMayInit else emptyDoc) <> hcat(pres map (p => specComment <+> showPre(p) <> line)) <> hcat(preserves map (p => specComment <+> showPreserves(p) <> line)) <> hcat(posts map (p => specComment <+> showPost(p) <> line)) <> @@ -126,7 +127,7 @@ class GoifyingPrinter(info: TypeInfoImpl) extends DefaultPrettyPrinter { rec, getActualParams(args), getActualResult(res), - PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty), + PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty, mayBeUsedInInit = false), // TODO: delete body ) ) @@ -138,7 +139,7 @@ class GoifyingPrinter(info: TypeInfoImpl) extends DefaultPrettyPrinter { id, getActualParams(args), getActualResult(res), - PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty), + PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty, mayBeUsedInInit = false), // TODO: delete body ) ) diff --git a/src/main/scala/viper/gobra/translator/transformers/TerminationDomainTransformer.scala b/src/main/scala/viper/gobra/translator/transformers/TerminationDomainTransformer.scala index 0fe766191..17dffd5e8 100644 --- a/src/main/scala/viper/gobra/translator/transformers/TerminationDomainTransformer.scala +++ b/src/main/scala/viper/gobra/translator/transformers/TerminationDomainTransformer.scala @@ -5,16 +5,17 @@ // Copyright (c) 2011-2021 ETH Zurich. package viper.gobra.translator.transformers -import java.nio.file.Path import viper.gobra.backend.BackendVerifier import viper.silicon.Silicon import viper.silver.ast.utility.FileLoader -import viper.silver.{ast => vpr} import viper.silver.frontend.{DefaultStates, ViperAstProvider} import viper.silver.plugin.standard.predicateinstance.PredicateInstance.PredicateInstanceDomainName import viper.silver.plugin.standard.termination.DecreasesTuple import viper.silver.reporter.{NoopReporter, Reporter} import viper.silver.verifier.AbstractError +import viper.silver.{ast => vpr} + +import java.nio.file.Path // This class should be removed in the future because Viper already implements inference of // imports for termination domains. However, at the moment, Viper performs the inference in diff --git a/src/test/resources/regressions/features/globals/globals-disabled-fail01.gobra b/src/test/resources/regressions/features/globals/globals-disabled-fail01.gobra deleted file mode 100644 index 109b84b02..000000000 --- a/src/test/resources/regressions/features/globals/globals-disabled-fail01.gobra +++ /dev/null @@ -1,58 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -// this is the same file as `globals-simple01.gobra` but additionally provides the `--disableGlobalVars` flag to Gobra. -// ##(--enableLazyImport) - -//:: ExpectedOutput(type_error) -initEnsures acc(&A) && acc(&B) && acc(&C, 1/2) -package pkg - -//:: ExpectedOutput(type_error) -importRequires true -import "fmt" - -import ( - //:: ExpectedOutput(type_error) - importRequires true - //:: ExpectedOutput(type_error) - importRequires true - "bytes" - //:: ExpectedOutput(type_error) - importRequires true - "sync" -) - - -//:: ExpectedOutput(type_error) -var A@ int = 0 -//:: ExpectedOutput(type_error) -var B@, C@ = f() -//:: ExpectedOutput(type_error) -var _ = g() -//:: ExpectedOutput(type_error) -var D@ struct{} - -decreases -func f() (int, bool) - -decreases -func g() interface{} - -requires acc(&A, 1/2) && A == 1 -ensures acc(&A, 1/2) -func testRead() { - var v1 int = A - assert v1 == 1 -} - -requires acc(&C) && C -func testWrite() { - C = false -} - -// Variable hiding works correctly, as in Go -func tesVarHiding() { - var A int = 0 - assert A == 0 -} diff --git a/src/test/resources/regressions/features/globals/globals-exclusive-simple01.gobra b/src/test/resources/regressions/features/globals/globals-exclusive-simple01.gobra index 74ae352ec..bcf6cc85c 100644 --- a/src/test/resources/regressions/features/globals/globals-exclusive-simple01.gobra +++ b/src/test/resources/regressions/features/globals/globals-exclusive-simple01.gobra @@ -12,6 +12,7 @@ func init() { assert false } +mayInit ensures res == 1 decreases func test() (res int) { diff --git a/src/test/resources/regressions/features/globals/globals-fail01.gobra b/src/test/resources/regressions/features/globals/globals-fail01.gobra index 77300045b..a1a510cc5 100644 --- a/src/test/resources/regressions/features/globals/globals-fail01.gobra +++ b/src/test/resources/regressions/features/globals/globals-fail01.gobra @@ -10,6 +10,7 @@ var A@ = 1 //:: ExpectedOutput(function_termination_error) var _, B@ = f() +mayInit func f() (int, bool) func testRead() { diff --git a/src/test/resources/regressions/features/globals/globals-simple01.gobra b/src/test/resources/regressions/features/globals/globals-simple01.gobra index bf84ca8f3..b2a4039e6 100644 --- a/src/test/resources/regressions/features/globals/globals-simple01.gobra +++ b/src/test/resources/regressions/features/globals/globals-simple01.gobra @@ -1,7 +1,7 @@ // Any copyright is dedicated to the Public Domain. // http://creativecommons.org/publicdomain/zero/1.0/ -initEnsures acc(&A) && acc(&B) && acc(&C, 1/2) +pkgInvariant acc(&A) && acc(&B) && acc(&C, 1/2) package pkg importRequires true @@ -20,9 +20,11 @@ var B@, C@ = f() var _ = g() var D@ struct{} +mayInit decreases func f() (int, bool) +mayInit decreases func g() interface{} diff --git a/src/test/resources/regressions/features/globals/globals-type-fail01.gobra b/src/test/resources/regressions/features/globals/globals-type-fail01.gobra index 36532691a..79ef3cce8 100644 --- a/src/test/resources/regressions/features/globals/globals-type-fail01.gobra +++ b/src/test/resources/regressions/features/globals/globals-type-fail01.gobra @@ -1,12 +1,13 @@ // Any copyright is dedicated to the Public Domain. // http://creativecommons.org/publicdomain/zero/1.0/ -initEnsures true +pkgInvariant true package pkg //:: ExpectedOutput(type_error) var B, C, _ = f() +mayInit func f() (int, bool) type T struct { diff --git a/src/test/resources/regressions/features/globals/globals-type-fail04.gobra b/src/test/resources/regressions/features/globals/globals-type-fail04.gobra index ad18d8d11..37f0227ad 100644 --- a/src/test/resources/regressions/features/globals/globals-type-fail04.gobra +++ b/src/test/resources/regressions/features/globals/globals-type-fail04.gobra @@ -13,6 +13,7 @@ type T interface { f() int } +mayInit func newT() T // calls to dynamically-bound methods are not allowed @@ -25,5 +26,4 @@ ghost //:: ExpectedOutput(type_error) func init() {} -//:: ExpectedOutput(type_error) ghost var C int \ No newline at end of file diff --git a/src/test/resources/regressions/features/globals/globals-type-fail05.gobra b/src/test/resources/regressions/features/globals/globals-type-fail05.gobra index 619b52c45..e1234aa56 100644 --- a/src/test/resources/regressions/features/globals/globals-type-fail05.gobra +++ b/src/test/resources/regressions/features/globals/globals-type-fail05.gobra @@ -2,11 +2,5 @@ // http://creativecommons.org/publicdomain/zero/1.0/ //:: ExpectedOutput(type_error) -initEnsures old(1) == 1 +pkgInvariant old(1) == 1 package pkg - -// ##(-I ./imports) - -//:: ExpectedOutput(type_error) -importRequires old(1) == 1 -import _ "path" \ No newline at end of file diff --git a/src/test/resources/regressions/features/globals/imports/empty/empty.go b/src/test/resources/regressions/features/globals/imports/empty/empty.go deleted file mode 100644 index 650689925..000000000 --- a/src/test/resources/regressions/features/globals/imports/empty/empty.go +++ /dev/null @@ -1,29 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -package empty - -// ##(-I ..) - -// The import precondition defaults to true. -// No ownership of any resource is transferred from the `path` -// package to the current package. -import "path" - -const PathType path.Type = 0 - -type Path struct{} - -//@ requires path.PackageMem() -//@ requires !path.Registered(PathType) -//@ ensures path.PackageMem() -//@ ensures path.Registered(PathType) -//@ ensures forall t path.Type :: 0 <= t && t < path.MaxType ==> -//@ t != PathType ==> old(path.Registered(t)) == path.Registered(t) -//@ decreases -func RegisterPath() { - path.RegisterPath(path.Metadata{ - Typ: PathType, - Desc: "Empty", - }) -} diff --git a/src/test/resources/regressions/features/globals/imports/layers/layers.go b/src/test/resources/regressions/features/globals/imports/layers/layers.go deleted file mode 100644 index 57edcde43..000000000 --- a/src/test/resources/regressions/features/globals/imports/layers/layers.go +++ /dev/null @@ -1,39 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -//@ initEnsures path.PackageMem() -//@ initEnsures path.Registered(empty.PathType) -package layers - -// ##(-I ..) - -import ( - // no import precondition, defaults to true - "empty" - - // Care must be taken when using ghost imports, given that having a ghost - // import may allow the user to prove stronger init postconditions then what - // they would have been able to prove (likewise for the main-precondition). - // Unfortunately, Gobra does not yet make a distinction between ghost imports - // and non-ghost imports. This should be addressed in a future PR. - - // This import is required to allow us to use the qualifier 'path' in ghost code. - //@ importRequires path.PackageMem() && !path.Registered(empty.PathType) - //@ "path" - - // This import is the non-ghost import of 'path' to "legitimate" the stronger - // initPostconditions that one may learn from importing it. Unfortunately, gofmt - // automatically removes the import if we remove the wildcard because there is no - // non-ghost usage of the qualifier 'path' - _ "path" -) - -func init() { - //@ assert path.PackageMem() - //@ assert !path.Registered(empty.PathType) - empty.RegisterPath() - //@ assert path.PackageMem() - //@ assert path.Registered(empty.PathType) -} - -type Layer struct{} diff --git a/src/test/resources/regressions/features/globals/imports/path/path.go b/src/test/resources/regressions/features/globals/imports/path/path.go deleted file mode 100644 index fefae5a70..000000000 --- a/src/test/resources/regressions/features/globals/imports/path/path.go +++ /dev/null @@ -1,79 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -// @ initEnsures PackageMem() -// @ initEnsures forall t Type :: 0 <= t && t < MaxType ==> !Registered(t) -package path - -/*@ -ghost const MaxType = 256 -@*/ - -var ( - // the original code uses an array of length 256, - // but arrays of custom types are not yet supported - registeredPaths/*@@@*/ []Metadata - strictDecoding/*@@@*/ bool = true -) - -type Type uint8 - -type Metadata struct { - Desc string - InUse bool - Typ Type -} - -/*@ -pred PackageMem() { - acc(®isteredPaths) && - len(registeredPaths) == MaxType && - (forall i int :: 0 <= i && i < len(registeredPaths) ==> acc(®isteredPaths[i])) && - acc(&strictDecoding) -} -@*/ - -/*@ -ghost -requires 0 <= t && t < MaxType -requires acc(PackageMem(), _) -ensures res == unfolding acc(PackageMem(), _) in registeredPaths[t].InUse -pure func Registered(t Type) (res bool) { - return unfolding acc(PackageMem(), _) in registeredPaths[t].InUse -} -@*/ - -/*@ -ghost -requires 0 <= t && t < MaxType -requires acc(PackageMem(), _) -pure func GetType(t Type) (res Metadata) { - return unfolding acc(PackageMem(), _) in registeredPaths[t] -} -@*/ - -func init() { - //@ assume len(registeredPaths) == MaxType - //@ fold PackageMem() -} - -// RegisterPath registers a new path type globally. -// The type passed in must be unique, or a runtime panic will occur. -// @ requires 0 <= pathMeta.Typ && pathMeta.Typ < MaxType -// @ requires PackageMem() -// @ requires !Registered(pathMeta.Typ) -// @ ensures PackageMem() -// @ ensures forall t Type :: 0 <= t && t < MaxType ==> -// @ t != pathMeta.Typ ==> old(Registered(t)) == Registered(t) -// @ ensures Registered(pathMeta.Typ) -// @ decreases -func RegisterPath(pathMeta Metadata) { - //@ unfold PackageMem() - pm := registeredPaths[pathMeta.Typ] - if pm.InUse { - panic("path type already registered") - } - registeredPaths[pathMeta.Typ] = pathMeta - registeredPaths[pathMeta.Typ].InUse = true - //@ fold PackageMem() -} diff --git a/src/test/resources/same_package/import-success/importer2.gobra b/src/test/resources/regressions/features/globals/itfAssign/defs/defs.gobra similarity index 55% rename from src/test/resources/same_package/import-success/importer2.gobra rename to src/test/resources/regressions/features/globals/itfAssign/defs/defs.gobra index 42cfd2385..94f7e0d79 100644 --- a/src/test/resources/same_package/import-success/importer2.gobra +++ b/src/test/resources/regressions/features/globals/itfAssign/defs/defs.gobra @@ -1,8 +1,13 @@ // Any copyright is dedicated to the Public Domain. // http://creativecommons.org/publicdomain/zero/1.0/ -package main +package defs -// ##(-I ./) -importRequires acc(&bar.B, 1/2) && acc(&bar.C) -import "bar" \ No newline at end of file +type I interface { + decreases + F() +} + +type T interface { + I +} \ No newline at end of file diff --git a/src/test/resources/regressions/features/globals/itfAssign/main.gobra b/src/test/resources/regressions/features/globals/itfAssign/main.gobra new file mode 100644 index 000000000..ac73f2f55 --- /dev/null +++ b/src/test/resources/regressions/features/globals/itfAssign/main.gobra @@ -0,0 +1,75 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package main + +// ##(-I ./) + +//:: ExpectedOutput(type_error) +importRequires old(1) == 1 +import "defs" + +type T struct{} + +decreases +func (t T) F() { + openDupPkgInv +} + +decreases +func (t T) Error() string + +// The following is allowed, as this pattern is often used in practice to check +// if the type of the value on the rhs is a subtype of the type of the LHS +var _ defs.I = (*T)(nil) + +// The following is disallowed, as we may use this to get access to a variable of type +// defs.I and, through a call, assume an invariant that does not hold yet +//:: ExpectedOutput(type_error) +var A defs.I = (*T)(nil) +//:: ExpectedOutput(type_error) +var B = defs.I((*T)(nil)) + +type ItfPkg interface { + decreases + F() +} + +mayInit +decreases +func initFun1() { + // this assignment is disallowed, otherwise + // one may use it to open an invariant that + // does not yet hold. + //:: ExpectedOutput(type_error) + var i defs.I = T{} +} + +mayInit +ensures false +decreases +func initFun2() { + // this assignment is disallowed, otherwise + // one may use it to open an invariant that + // does not yet hold. + //:: ExpectedOutput(type_error) + var i = defs.I(T{}) +} + +mayInit +decreases +func initFun3() { + var i ItfPkg = T{} + // This call is disallowed, otherwise we may call an interface method + // that depends on the invariants established upon initialization. + //:: ExpectedOutput(type_error) + i.F() +} + +mayInit +decreases +func initFun4() { + // May not open package invariants on a function that may be called during init + //:: ExpectedOutput(type_error) + openDupPkgInv +} \ No newline at end of file diff --git a/src/test/resources/regressions/features/globals/scion-like01.go b/src/test/resources/regressions/features/globals/scion-like01.go deleted file mode 100644 index 715f1b77f..000000000 --- a/src/test/resources/regressions/features/globals/scion-like01.go +++ /dev/null @@ -1,24 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -//@ initEnsures path.PackageMem() -//@ initEnsures path.Registered(empty.PathType) -package main - -// ##(-I ./imports) - -import ( - //@ importRequires path.PackageMem() - //@ importRequires path.Registered(empty.PathType) - "layers" - //@ "empty" - _ "empty" - //@ "path" - _ "path" -) - -//@ requires path.PackageMem() && path.Registered(empty.PathType) -func main() { - var l layers.Layer = layers.Layer{} - _ = l -} diff --git a/src/test/resources/regressions/features/globals/scion-like02.go b/src/test/resources/regressions/features/globals/scion-like02.go deleted file mode 100644 index 9354161f4..000000000 --- a/src/test/resources/regressions/features/globals/scion-like02.go +++ /dev/null @@ -1,24 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -//@ initEnsures path.PackageMem() -//@ initEnsures path.Registered(empty.PathType) -package main - -// ##(-I ./imports) - -import ( - //@ importRequires path.PackageMem() && path.Registered(empty.PathType) - "layers" - //@ "empty" - _ "empty" - //@ "path" - _ "path" -) - -//:: ExpectedOutput(main_pre_error) -//@ requires path.PackageMem() && path.Registered(10) -func main() { - var l layers.Layer = layers.Layer{} - _ = l -} diff --git a/src/test/resources/regressions/features/globals/scion-like03.go b/src/test/resources/regressions/features/globals/scion-like03.go deleted file mode 100644 index 59707f5dc..000000000 --- a/src/test/resources/regressions/features/globals/scion-like03.go +++ /dev/null @@ -1,28 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -//@ initEnsures path.PackageMem() -// Verifying the the init postcondition here fails, because this property is -// not established by the init code of this package. -//:: ExpectedOutput(postcondition_error) -//@ initEnsures path.Registered(10) -package main - -// ##(-I ./imports) - -import ( - //@ importRequires path.PackageMem() && path.Registered(empty.PathType) - "layers" - //@ "empty" - _ "empty" - //@ "path" - _ "path" -) - -// However, the main function is verified successfully, given that -// the init postconditions of this file imply the preconditions of main. -//@ requires path.PackageMem() && path.Registered(10) -func main() { - var l layers.Layer = layers.Layer{} - _ = l -} diff --git a/src/test/resources/regressions/features/globals/scion/monotonicset/bounded.gobra b/src/test/resources/regressions/features/globals/scion/monotonicset/bounded.gobra new file mode 100644 index 000000000..7d7fa8a2b --- /dev/null +++ b/src/test/resources/regressions/features/globals/scion/monotonicset/bounded.gobra @@ -0,0 +1,243 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package monotonicset + +type BoundedMonotonicSet struct { + ghost valuesMap dict[uint16](gpointer[bool]) +} + +pred (b BoundedMonotonicSet) Inv() { + forall i uint16 :: 0 <= i && i < 256 ==> + (i in domain(b.valuesMap) && acc(b.valuesMap[i], 1/2)) +} + +ghost +requires acc(b.Inv(), _) +requires 0 <= i && i < 256 +decreases +pure func (b BoundedMonotonicSet) FContains(i uint16) bool { + // extra indirection avoids a type-checking bug of Gobra. + return unfolding acc(b.Inv(), _) in + b.fcontainshelper(i) +} + +ghost +requires forall i uint16 :: 0 <= i && i < 256 ==> + (i in domain(b.valuesMap) && acc(b.valuesMap[i], _)) +requires 0 <= i && i < 256 +decreases +pure func (b BoundedMonotonicSet) fcontainshelper(i uint16) bool { + return *b.valuesMap[i] +} + + +pred (b BoundedMonotonicSet) Contains(i uint16) { + 0 <= i && i < 256 && + i in domain(b.valuesMap) && + acc(b.valuesMap[i], _) && + *b.valuesMap[i] +} + +ghost +requires b.Contains(i) +ensures b.Contains(i) && b.Contains(i) +decreases +func (b BoundedMonotonicSet) ContainsIsDup(i uint16) { + unfold b.Contains(i) + fold b.Contains(i) + fold b.Contains(i) +} + +pred (b BoundedMonotonicSet) DoesNotContain(i uint16) { + 0 <= i && i < 256 && + i in domain(b.valuesMap) && + acc(b.valuesMap[i], 1/2) && + !(*b.valuesMap[i]) +} + +ghost +preserves acc(b.Inv(), 1/4) +preserves acc(b.DoesNotContain(i), 1/4) +ensures 0 <= i && i < 256 +ensures !b.FContains(i) +decreases +func (b BoundedMonotonicSet) DoesNotContainImpliesNotFContains(i uint16) { + assert unfolding acc(b.Inv(), _) in + unfolding acc(b.DoesNotContain(i), _) in + !b.fcontainshelper(i) +} + +ghost +preserves acc(b.Inv(), 1/4) +preserves b.Contains(i) +ensures 0 <= i && i < 256 +ensures b.FContains(i) +decreases +func (b BoundedMonotonicSet) ContainsImpliesFContains(i uint16) { + assert unfolding acc(b.Inv(), _) in + unfolding acc(b.Contains(i), _) in + b.fcontainshelper(i) +} + +ghost +ensures res.Inv() +ensures forall i uint16 :: 0 <= i && i < 256 ==> + res.DoesNotContain(i) +// The following is technically redundant, but very useful. +ensures forall i uint16 :: 0 <= i && i < 256 ==> + !res.FContains(i) +decreases +func Alloc() (res BoundedMonotonicSet) { + b := BoundedMonotonicSet{} + var i uint16 + invariant 0 <= i && i <= 256 + invariant forall j uint16 :: 0 <= j && j < i ==> + j in domain(b.valuesMap) + // injectivity requirement + invariant forall j1, j2 uint16 :: 0 <= j1 && j1 < j2 && j2 < i ==> + b.valuesMap[j1] != b.valuesMap[j2] + invariant forall j uint16 :: 0 <= j && j < i ==> + acc(b.valuesMap[j]) + invariant forall j uint16 :: 0 <= j && j < i ==> + !(*b.valuesMap[j]) + decreases 256 - i + for i = 0; i < 256; i +=1 { + b.valuesMap[i] = new(bool) + } + + invariant 0 <= i && i <= 256 + invariant forall j uint16 :: 0 <= j && j < i ==> + j in domain(b.valuesMap) + // injectivity requirement + invariant forall j1, j2 uint16 :: 0 <= j1 && j1 < j2 && j2 < i ==> + b.valuesMap[j1] != b.valuesMap[j2] + invariant forall j uint16 :: i <= j && j < 256 ==> + acc(b.valuesMap[j]) && !(*b.valuesMap[j]) + invariant forall j uint16 :: 0 <= j && j < i ==> + acc(b.valuesMap[j], 1/2) + invariant forall j uint16 :: 0 <= j && j < i ==> + b.DoesNotContain(j) + invariant forall j uint16 :: 0 <= j && j < i ==> + !b.fcontainshelper(j) + decreases 256 - i + for i = 0; i < 256; i +=1 { + fold b.DoesNotContain(i) + } + fold b.Inv() + return b +} + +ghost +opaque // make this closed when that is supported +requires acc(b.Inv(), _) +decreases +pure func (b BoundedMonotonicSet) ToSet() set[uint16] { + return b.toSetAux(0) +} + +ghost +requires acc(b.Inv(), _) +requires 0 <= start && start < 256 +decreases 256 - start +pure func (b BoundedMonotonicSet) toSetAux(start uint16) set[uint16] { + return unfolding acc(b.Inv(), _) in ((*b.valuesMap[start] ? set[uint16]{start} : set[uint16]{}) union (start < 255 ? b.toSetAux(start+1) : set[uint16]{})) +} + +ghost +requires 0 < p +requires acc(b.Inv(), p) +requires b.Contains(v) +ensures acc(b.Inv(), p) +ensures v in b.ToSet() +decreases +func (b BoundedMonotonicSet) ContainsImpliesAbstractContains(v uint16, p perm) { + found := false + i := uint16(0) + part1 := set[uint16]{} + part2 := reveal b.ToSet() + + assert unfolding b.Contains(v) in 0 <= v && v < 256 + + invariant acc(b.Inv(), p/2) + invariant b.Contains(v) + invariant 0 <= i && i <= 256 + invariant v < i ==> found + invariant found ==> v in b.ToSet() + invariant part1 union part2 == b.ToSet() + invariant i < 256 ==> + part2 == unfolding acc(b.Inv(), _) in ((*b.valuesMap[i] ? set[uint16]{i} : set[uint16]{}) union (i < 255 ? b.toSetAux(i+1) : set[uint16]{})) + decreases 256 - i + for i = 0; i < 256; i += 1 { + newpart1 := part1 union unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[uint16]{i} : set[uint16]{}) + newpart2 := i < 255 ? b.toSetAux(i+1) : set[uint16]{} + if i == v { + unfold b.Contains(v) + found = true + assert *b.valuesMap[i] + assert newpart1 union newpart2 == b.ToSet() + assert v in (unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[uint16]{i} : set[uint16]{})) + assert v in newpart1 + fold b.Contains(v) + } + part1 = newpart1 + part2 = newpart2 + } +} + +ghost +requires 0 < p +preserves acc(b.Inv(), p) +preserves b.DoesNotContain(v) +ensures !(v in b.ToSet()) +decreases +func (b BoundedMonotonicSet) DoesNotContainsImpliesAbstractDoesNotContain(v uint16, p perm) { + found := false + i := uint16(0) + part1 := set[uint16]{} + part2 := reveal b.ToSet() + + assert unfolding b.DoesNotContain(v) in 0 <= v && v < 256 + + invariant acc(b.Inv(), p/2) + invariant b.DoesNotContain(v) + invariant 0 <= i && i <= 256 + invariant !found + invariant found == v in part1 + invariant part1 union part2 == b.ToSet() + invariant i < 256 ==> + part2 == unfolding acc(b.Inv(), _) in ((*b.valuesMap[i] ? set[uint16]{i} : set[uint16]{}) union (i < 255 ? b.toSetAux(i+1) : set[uint16]{})) + invariant i == 256 ==> + part2 == set[uint16]{} + decreases 256 - i + for i = 0; i < 256; i += 1 { + newpart1 := part1 union unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[uint16]{i} : set[uint16]{}) + newpart2 := i < 255 ? b.toSetAux(i+1) : set[uint16]{} + if i == v { + unfold b.DoesNotContain(v) + assert !(*b.valuesMap[i]) + assert newpart1 union newpart2 == b.ToSet() + assert !(v in (unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[uint16]{i} : set[uint16]{}))) + assert !(v in newpart1) + fold b.DoesNotContain(v) + } + part1 = newpart1 + part2 = newpart2 + } +} + +ghost +requires b.DoesNotContain(v) +preserves b.Inv() +ensures b.Contains(v) +ensures forall i uint16 :: 0 <= i && i < 256 && i != v ==> + b.FContains(i) == old(b.FContains(i)) +decreases +func (b BoundedMonotonicSet) Add(v uint16) { + unfold b.Inv() + unfold b.DoesNotContain(v) + ghost var ptr gpointer[bool] = b.valuesMap[v] + *ptr = true + fold b.Inv() + fold b.Contains(v) +} \ No newline at end of file diff --git a/src/test/resources/regressions/features/globals/scion/path/onehop/onehop.go b/src/test/resources/regressions/features/globals/scion/path/onehop/onehop.go new file mode 100644 index 000000000..5fcdfe4c7 --- /dev/null +++ b/src/test/resources/regressions/features/globals/scion/path/onehop/onehop.go @@ -0,0 +1,22 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package onehop + +// ##(-I ../../) + +import "path" + +const PathType path.Type = 2 + +// @ requires path.RegisteredTypes().DoesNotContain(uint16(PathType)) +// @ preserves path.PkgInv() +// @ ensures path.RegisteredTypes().Contains(uint16(PathType)) +// @ decreases +func RegisterPath() { + tmp := path.Metadata{ + Type: PathType, + Desc: "OneHop", + } + path.RegisterPath(tmp) +} diff --git a/src/test/resources/regressions/features/globals/scion/path/path.go b/src/test/resources/regressions/features/globals/scion/path/path.go new file mode 100644 index 000000000..38f1b7991 --- /dev/null +++ b/src/test/resources/regressions/features/globals/scion/path/path.go @@ -0,0 +1,96 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package path + +// ##(-I ../) + +// This approach is sound, assuming that the paths below are unique per a package. +// This assumption is not problematic, and is similar to the assumption we make for +// imports. +// @ friendPkg "../" PkgInv() +// @ friendPkg "../" RegisteredTypes().DoesNotContain(1) && +// @ RegisteredTypes().DoesNotContain(2) + +// @ import "monotonicset" + +/*@ + +pred PkgInv() { + acc(®isteredPaths) && + registeredKeys.Inv() && + (forall i uint16 :: 0 <= i && i < maxPathType ==> + registeredPaths[i].inUse == registeredKeys.FContains(i)) +} + +ghost +decreases +pure func RegisteredTypes() monotonicset.BoundedMonotonicSet { + return registeredKeys +} + +@*/ + +const maxPathType = 256 + +var registeredPaths /*@@@*/ [maxPathType]metadata + +// @ ghost var registeredKeys = monotonicset.Alloc() + +// Type indicates the type of the path contained in the SCION header. +type Type uint8 + +type metadata struct { + inUse bool + Metadata +} + +func init() { + // @ fold PkgInv() +} + +// Metadata defines a new SCION path type, used for dynamic SICON path type +// registration. The original definition contains an extra field named 'New' +// which stores a closure that allocates a new instance of the corresponding +// path type. To avoid complications with closures here, we ignore it. +type Metadata struct { + // Type is a unique value for the path. + Type Type + // Desc is the description/name of the path. + Desc string +} + +// @ requires 0 <= pathMeta.Type && pathMeta.Type < 256 +// @ requires RegisteredTypes().DoesNotContain(uint16(pathMeta.Type)) +// @ preserves PkgInv() +// @ ensures RegisteredTypes().Contains(uint16(pathMeta.Type)) +// @ decreases +func RegisterPath(pathMeta Metadata) { + // @ unfold acc(PkgInv(), 1/2) + // @ RegisteredTypes().DoesNotContainsImpliesAbstractDoesNotContain(uint16(pathMeta.Type), 1/4) + // @ RegisteredTypes().DoesNotContainImpliesNotFContains(uint16(pathMeta.Type)) + // @ unfold acc(PkgInv(), 1/2) + // @ defer fold PkgInv() + pm := registeredPaths[pathMeta.Type] + if pm.inUse { + // @ assert false + panic("path type already registered") + } + // @ RegisteredTypes().Add(uint16(pathMeta.Type)) + // @ RegisteredTypes().ContainsImpliesFContains(uint16(pathMeta.Type)) + registeredPaths[pathMeta.Type].inUse = true + registeredPaths[pathMeta.Type].Metadata = pathMeta +} + +// @ requires 0 <= t && t < maxPathType +// @ preserves acc(PkgInv(), 1/512) +// @ decreases +func (t Type) String() string { + // @ unfold acc(PkgInv(), 1/512) + // @ defer fold acc(PkgInv(), 1/512) + pm := registeredPaths[t] + if !pm.inUse { + return "UNKNOWN" + } + return pm.Desc +} diff --git a/src/test/resources/regressions/features/globals/scion/path/scion/base.go b/src/test/resources/regressions/features/globals/scion/path/scion/base.go new file mode 100644 index 000000000..bb7222bc5 --- /dev/null +++ b/src/test/resources/regressions/features/globals/scion/path/scion/base.go @@ -0,0 +1,22 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package scion + +// ##(-I ../../) + +import "path" + +const PathType path.Type = 1 + +// @ requires path.RegisteredTypes().DoesNotContain(uint16(PathType)) +// @ preserves path.PkgInv() +// @ ensures path.RegisteredTypes().Contains(uint16(PathType)) +// @ decreases +func RegisterPath() { + tmp := path.Metadata{ + Type: PathType, + Desc: "SCION", + } + path.RegisterPath(tmp) +} diff --git a/src/test/resources/regressions/features/globals/scion/scion.go b/src/test/resources/regressions/features/globals/scion/scion.go new file mode 100644 index 000000000..fd0f7f3b6 --- /dev/null +++ b/src/test/resources/regressions/features/globals/scion/scion.go @@ -0,0 +1,37 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +//:: IgnoreFile(/gobra/issue/830/) + +// @ pkgInvariant path.PkgInv() +// @ dup pkgInvariant acc(path.RegisteredTypes().Contains(1), _) && +// @ acc(path.RegisteredTypes().Contains(2), _) + +package scion + +// ##(-I .) + +// Example inspired by how PathTypes are registered in the SCION border router. +// Based on https://github.com/viperproject/VerifiedSCION/tree/master/pkg/slayers/scion.go + +// We should have a system of checking ghost imports to make sure they do not introduce +// side effects that would not happen otherwise. +import ( + // @ "monotonicset" + // @ importRequires path.PkgInv() + // @ importRequires path.RegisteredTypes().DoesNotContain(1) && + // @ path.RegisteredTypes().DoesNotContain(2) + // @ "path" + "path/onehop" + "path/scion" +) + +// We should introduce preconditions and postconditions to this function to guarantee that +// all init functions in parallel imply the initialization obligations. The current +// solution is sound only if we have at most one init function (otherwise, resources from +// friend packages may be acquired multiple times). At the moment, only one init function +// per package is supported, so this is not currently a problem. +func init() { + scion.RegisterPath() + onehop.RegisterPath() +} diff --git a/src/test/resources/same_package/import-fail01/importer2.gobra b/src/test/resources/same_package/import-fail01/importer2.gobra deleted file mode 100644 index 9fcb6d7cd..000000000 --- a/src/test/resources/same_package/import-fail01/importer2.gobra +++ /dev/null @@ -1,9 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -package main - -// ##(-I ./) -//:: ExpectedOutput(import_pre_error) -importRequires acc(&bar.B) && acc(&bar.C) -import "bar" \ No newline at end of file diff --git a/src/test/resources/same_package/pkg_init/byte/byte.go b/src/test/resources/same_package/pkg_init/byte/byte.go new file mode 100644 index 000000000..7866c5411 --- /dev/null +++ b/src/test/resources/same_package/pkg_init/byte/byte.go @@ -0,0 +1,53 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +// @ dup pkgInvariant acc(StaticInv(), _) + +package byte + +type Byte struct { + value byte +} + +var byteCache /*@@@*/ [256]*Byte + +func init() { + // @ invariant 0 <= i && i <= 256 && acc(&byteCache) + // @ invariant (forall j, k uint16 :: 0 <= j && j < k && k < i ==> + // @ byteCache[j] != byteCache[k]) + // @ invariant (forall j uint16 :: 0 <= j && j < i ==> + // @ acc(byteCache[j]) && byteCache[j].value == byte(j) - 128) + // @ decreases 256 - i + for i := 0; i < 256; i++ { + byteCache[i] = alloc(byte(i) - 128) + } + // @ fold StaticInv() +} + +// @ ensures acc(&res.value) && res.value == val +// @ decreases +// @ mayInit +func alloc(val byte) (res *Byte) { + res = new(Byte) + res.value = val + return res +} + +// @ pure +// @ requires acc(b.Mem(), _) +// @ decreases +func (b *Byte) ByteValue() byte { + return /*@ unfolding acc(b.Mem(), _) in @*/ b.value +} + +// @ ensures acc(res.Mem(), _) +// @ ensures res.ByteValue() == val +// @ decreases +func ToVal(val byte) (res *Byte) { + // @ assume -128 <= val && val <= 127 + // @ openDupPkgInv + // @ unfold acc(StaticInv(), _) + res = byteCache[val+128] + // @ fold acc(res.Mem(), _) + return res +} diff --git a/src/test/resources/same_package/pkg_init/byte/byte_spec.gobra b/src/test/resources/same_package/pkg_init/byte/byte_spec.gobra new file mode 100644 index 000000000..94a417bf0 --- /dev/null +++ b/src/test/resources/same_package/pkg_init/byte/byte_spec.gobra @@ -0,0 +1,17 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package byte + +pred StaticInv() { + acc(&byteCache, _) && + // for injectivity checks: + (forall j, k uint16 :: 0 <= j && j < k && k < 256 ==> + byteCache[j] != byteCache[k]) && + (forall i uint16 :: 0 <= i && i < 256 ==> + acc(byteCache[i], _) && byteCache[i].value == (byte)(i-128)) +} + +pred (b *Byte) Mem() { + acc(b, _) +} diff --git a/src/test/resources/same_package/pkg_init/concfib/fib.go b/src/test/resources/same_package/pkg_init/concfib/fib.go new file mode 100644 index 000000000..fd3e9b70b --- /dev/null +++ b/src/test/resources/same_package/pkg_init/concfib/fib.go @@ -0,0 +1,72 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +// @ dup pkgInvariant acc(StaticInv(), _) + +package concfib + +import "sync" + +var cache /*@@@*/ map[int]int = make(map[int]int) +var lock *sync.Mutex = &sync.Mutex{} + +func init() { + cache[0] = 1 + cache[1] = 1 + // @ fold lockInv!() + // @ lock.SetInv(lockInv!) + // @ fold acc(StaticInv(), _) +} + +// @ requires 0 <= n +// @ ensures res == FibSpec(n) +// termination cannot be proven due to calls to Lock() +func FibV1(n int) (res int) { + // @ openDupPkgInv + // @ unfold acc(StaticInv(), _) + lock.Lock() + // @ unfold lockInv!() + if v, ok := cache[n]; ok { + // @ fold lockInv!() + lock.Unlock() + return v + } + // @ fold lockInv!() + lock.Unlock() + v := FibV1(n-1) + FibV1(n-2) + lock.Lock() + // @ unfold lockInv!() + cache[n] = v + // @ fold lockInv!() + lock.Unlock() + return v +} + +// @ requires 0 <= n +// @ ensures res == FibSpec(n) +// termination cannot be proven due to calls to Lock() +func FibV2(n int) (res int) { + // @ openDupPkgInv + // @ unfold acc(StaticInv(), _) + lock.Lock() + v := fibImpl(n) + lock.Unlock() + return v +} + +// @ requires 0 <= n +// @ preserves lockInv!() +// @ ensures res == FibSpec(n) +// @ decreases n +func fibImpl(n int) (res int) { + // @ unfold lockInv!() + // @ defer fold lockInv!() + if v, ok := cache[n]; ok { + return v + } + // @ fold lockInv!() + v := fibImpl(n-1) + fibImpl(n-2) + // @ unfold lockInv!() + cache[n] = v + return v +} diff --git a/src/test/resources/same_package/pkg_init/concfib/fib_spec.gobra b/src/test/resources/same_package/pkg_init/concfib/fib_spec.gobra new file mode 100644 index 000000000..eed544616 --- /dev/null +++ b/src/test/resources/same_package/pkg_init/concfib/fib_spec.gobra @@ -0,0 +1,37 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package concfib + +ghost +pure +requires 0 <= n +decreases n +func FibSpec(n int) int { + return n <= 1 ? 1 : FibSpec(n-1) + FibSpec(n-2) +} + +pred lockInv() { + acc(&cache, _) && + acc(cache) && + 0 in domain(cache) && + 1 in domain(cache) && + forall i int :: { cache[i] }{ FibSpec(i) }{ i in domain(cache) } i in domain(cache) ==> + 0 <= i && cache[i] == FibSpec(i) +} + +pred StaticInv() { + acc(lock.LockP(), _) && + lock.LockInv() == lockInv! +} + +// Given that we can always implement a ghost method like the one below to gain +// access to the duplicable static invariants of a package, it is unecessary +// to pass an import path or a package identifier to `openDupPkgInv`. Instead, we +// can just define a method like this in every package and call it. +ghost +ensures acc(StaticInv(), _) +decreases +func AcquireDupPkgInv() { + openDupPkgInv +} \ No newline at end of file diff --git a/src/test/resources/same_package/pkg_init/fib/fib.go b/src/test/resources/same_package/pkg_init/fib/fib.go new file mode 100644 index 000000000..93111550f --- /dev/null +++ b/src/test/resources/same_package/pkg_init/fib/fib.go @@ -0,0 +1,31 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +// @ pkgInvariant StaticInv() + +package fib + +var cache /*@@@*/ map[int]int = make(map[int]int) + +func init() { + cache[0] = 1 + cache[1] = 1 + // @ fold StaticInv() +} + +// @ requires 0 <= n +// @ preserves StaticInv() +// @ ensures res == FibSpec(n) +// @ decreases n +func Fib(n int) (res int) { + // @ unfold StaticInv() + // @ defer fold StaticInv() + if v, ok := cache[n]; ok { + return v + } + // @ fold StaticInv() + v := Fib(n-1) + Fib(n-2) + // @ unfold StaticInv() + cache[n] = v + return v +} diff --git a/src/test/resources/same_package/pkg_init/fib/fib_spec.gobra b/src/test/resources/same_package/pkg_init/fib/fib_spec.gobra new file mode 100644 index 000000000..759b5aadc --- /dev/null +++ b/src/test/resources/same_package/pkg_init/fib/fib_spec.gobra @@ -0,0 +1,21 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package fib + +ghost +pure +requires 0 <= n +decreases n +func FibSpec(n int) int { + return n <= 1 ? 1 : FibSpec(n-1) + FibSpec(n-2) +} + +pred StaticInv() { + acc(&cache, _) && + acc(cache) && + 0 in domain(cache) && + 1 in domain(cache) && + forall i int :: { cache[i] }{ FibSpec(i) }{ i in domain(cache) } i in domain(cache) ==> + 0 <= i && cache[i] == FibSpec(i) +} \ No newline at end of file diff --git a/src/test/resources/same_package/pkg_init/import/main.go b/src/test/resources/same_package/pkg_init/import/main.go new file mode 100644 index 000000000..e104dab8b --- /dev/null +++ b/src/test/resources/same_package/pkg_init/import/main.go @@ -0,0 +1,97 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +// @ dup pkgInvariant acc(DupPkgInv(), _) +package main + +// ##(-I ../) + +import ( + "concfib" + "fib" +) + +// @ pred DupPkgInv() { acc(&x) && x == 10 } + +var x /*@@@*/ int = valX() + +// I am not super happy with having implicit free preconditions (which are sound) for +// this function (it is incosistent with the design of main, where we +// must provide the preconditions for main). Nonetheless, having to provide +// a spec (including termination measures) for this function is a bit excessive. +// An alternative would be to change the encoding for main. +func init() { + // this function is checked to be mayInit + foo() + + // this one is not checked for mayInit, it is imported. + y := fib.Fib(3) + // also, the call above requires fib.StaticInv(). We can actually + // perform this call because the runtime guarantes that the main thread of + // different static initializers does not interleave. Gobra checks that the + // invariant of all imported packages is preserved. + + // @ assert fib.FibSpec(0) == 1 + // @ assert fib.FibSpec(1) == 1 + // @ assert fib.FibSpec(2) == 2 + // @ assert fib.FibSpec(3) == 3 + // @ assert y == 3 + _ = y + + // @ fold DupPkgInv() +} + +func Test() { + x := concfib.FibV1(3) + // @ assert concfib.FibSpec(0) == 1 + // @ assert concfib.FibSpec(1) == 1 + // @ assert concfib.FibSpec(2) == 2 + // @ assert concfib.FibSpec(3) == 3 + // @ assert x == 3 + _ = x +} + +func TestOpenDupInv() { + // @ concfib.AcquireDupPkgInv() + // @ assert acc(concfib.StaticInv(), _) +} + +// Must be marked with `mayInit`, otherwise Gobra throws an error in the declaration +// of `x`. `mayInit` signals that a method might be called from the static initializer +// of the package in which it is declared, and thus, it is not allowed to assume any +// of its invariants. Notice that this is an implementation detail! This fact is not +// considered part of the public interface of the function (if there is one). However, +// we provide this detail with the function spec because we currently do not have any +// systematic way of adding annotations regarding implementation details to Gobra. +// @ mayInit +// @ ensures r == 10 +// @ decreases +func valX() (r int) { + return 10 +} + +// termination is necessary, otherwise `foo` cannot be +// called from the static initializer. +// @ mayInit +// @ decreases +func foo() {} + +// We check that no interface methods are annotated with mayInit. +type I interface { + // @ decreases + m() +} + +// the following precondition is checked to follow from all the non-duplicable +// package invariants of all direct imports: +// @ requires fib.StaticInv() +// @ decreases +func main() { + x := fib.Fib(3) + // @ assert fib.FibSpec(0) == 1 + // @ assert fib.FibSpec(1) == 1 + // @ assert fib.FibSpec(2) == 2 + // @ assert fib.FibSpec(3) == 3 + // @ assert x == 3 + _ = x +} diff --git a/src/test/resources/same_package/import-success/bar/bar.gobra b/src/test/resources/same_package/pkg_init/import1/bar/bar.gobra similarity index 70% rename from src/test/resources/same_package/import-success/bar/bar.gobra rename to src/test/resources/same_package/pkg_init/import1/bar/bar.gobra index 52da3e684..8d5eaf0b8 100644 --- a/src/test/resources/same_package/import-success/bar/bar.gobra +++ b/src/test/resources/same_package/pkg_init/import1/bar/bar.gobra @@ -1,9 +1,12 @@ // Any copyright is dedicated to the Public Domain. // http://creativecommons.org/publicdomain/zero/1.0/ -initEnsures acc(&A) && acc(&B) && acc(&C) package bar +// ##(-I ../) + +friendPkg "../../pkg" acc(&A) && acc(&B) && acc(&C) + var A@ int = 1 var B@ int = 2 var C@ int = 3 diff --git a/src/test/resources/same_package/import-fail01/importer1.gobra b/src/test/resources/same_package/pkg_init/import1/pkg/importer.gobra similarity index 72% rename from src/test/resources/same_package/import-fail01/importer1.gobra rename to src/test/resources/same_package/pkg_init/import1/pkg/importer.gobra index 38bbf4549..55bbad3e2 100644 --- a/src/test/resources/same_package/import-fail01/importer1.gobra +++ b/src/test/resources/same_package/pkg_init/import1/pkg/importer.gobra @@ -1,8 +1,11 @@ // Any copyright is dedicated to the Public Domain. // http://creativecommons.org/publicdomain/zero/1.0/ -package main +//:: IgnoreFile(/gobra/issue/830/) + +package pkg + +// ##(-I ../) -// ##(-I ./) importRequires acc(&bar.A) && acc(&bar.B) import "bar" diff --git a/src/test/resources/same_package/import-fail01/bar/bar.gobra b/src/test/resources/same_package/pkg_init/import2/bar/bar.gobra similarity index 72% rename from src/test/resources/same_package/import-fail01/bar/bar.gobra rename to src/test/resources/same_package/pkg_init/import2/bar/bar.gobra index 52da3e684..9daaab2d6 100644 --- a/src/test/resources/same_package/import-fail01/bar/bar.gobra +++ b/src/test/resources/same_package/pkg_init/import2/bar/bar.gobra @@ -1,9 +1,12 @@ // Any copyright is dedicated to the Public Domain. // http://creativecommons.org/publicdomain/zero/1.0/ -initEnsures acc(&A) && acc(&B) && acc(&C) package bar +// ##(-I ../) + +friendPkg "pkg" acc(&A) && acc(&B) && acc(&C) + var A@ int = 1 var B@ int = 2 var C@ int = 3 diff --git a/src/test/resources/same_package/import-success/importer1.gobra b/src/test/resources/same_package/pkg_init/import2/pkg/importer.gobra similarity index 58% rename from src/test/resources/same_package/import-success/importer1.gobra rename to src/test/resources/same_package/pkg_init/import2/pkg/importer.gobra index f69533138..04a7fe51f 100644 --- a/src/test/resources/same_package/import-success/importer1.gobra +++ b/src/test/resources/same_package/pkg_init/import2/pkg/importer.gobra @@ -1,8 +1,11 @@ // Any copyright is dedicated to the Public Domain. // http://creativecommons.org/publicdomain/zero/1.0/ -package main +//:: IgnoreFile(/gobra/issue/830/) -// ##(-I ./) -importRequires acc(&bar.A) && acc(&bar.B, 1/2) +package pkg + +// ##(-I ../) + +importRequires false import "bar" diff --git a/src/test/resources/same_package/pkg_init/invallinstances/client.go b/src/test/resources/same_package/pkg_init/invallinstances/client.go new file mode 100644 index 000000000..ca8ecafbe --- /dev/null +++ b/src/test/resources/same_package/pkg_init/invallinstances/client.go @@ -0,0 +1,42 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +// @ pkgInvariant PkgInv() + +package invallinstances + +// This example demonstrates the ability to have static invariants over all +// allocated instances of a type (using the New function), as originally demoed +// in Peter's paper (https://link.springer.com/chapter/10.1007/11526841_4) +// with the Client class. Interestingly, the proof annotations for the allocator +// (New) in this version and in the version from Peter are very similar even +// though one is based in ownership types and the other is based in SL/IDF. + +var ids /*@@@*/ int + +// @ ghost var allocs@ set[*Client] + +func init() { + // @ fold PkgInv() +} + +type Client struct { + id int + name string +} + +// @ preserves PkgInv() +// @ ensures res.Inv() +// @ ensures res.Allocated() +// @ decreases +func New(name string) (res *Client) { + // @ unfold PkgInv() + // @ defer fold PkgInv() + res = new(Client) + res.name = name + res.id = ids + ids += 1 + // @ allocs = allocs union set[*Client]{res} + // @ fold res.Inv() + return res +} diff --git a/src/test/resources/same_package/pkg_init/invallinstances/client_spec.gobra b/src/test/resources/same_package/pkg_init/invallinstances/client_spec.gobra new file mode 100644 index 000000000..9945a06ae --- /dev/null +++ b/src/test/resources/same_package/pkg_init/invallinstances/client_spec.gobra @@ -0,0 +1,50 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package invallinstances + +pred PkgInv() { + acc(&ids) && + acc(&allocs) && + (forall c *Client :: { c in allocs } c in allocs ==> + acc(&c.id, 1/2)) && + (forall c *Client :: { c in allocs } c in allocs ==> + c.id < ids) && + (forall c1, c2 *Client :: { c1 in allocs, c2 in allocs } c1 in allocs && c2 in allocs && c1 != c2 ==> + c1.id != c2.id) +} + +ghost +requires acc(PkgInv(), _) +decreases +pure func (c *Client) Allocated() bool { + return unfolding acc(PkgInv(), _) in + c in allocs +} + +pred (c *Client) Inv() { + acc(&c.id, 1/2) && + acc(&c.name) +} + +ghost +requires acc(c.Inv(), _) +decreases +pure func (c *Client) Id() int { + return unfolding acc(c.Inv(), _) in + c.id +} + + +ghost +preserves acc(PkgInv(), 1/4) +preserves c1.Inv() && c2.Inv() +preserves c1.Allocated() && c2.Allocated() +ensures c1.Id() != c2.Id() +decreases +func TwoDiffInstancesHaveDiffIds(c1 *Client, c2 *Client) { + assert unfolding acc(PkgInv(), 1/4) in + unfolding c1.Inv() in + unfolding c2.Inv() in + c1.id != c2.id +} \ No newline at end of file diff --git a/src/test/resources/same_package/pkg_init/names_sequential/names/name/name.go b/src/test/resources/same_package/pkg_init/names_sequential/names/name/name.go new file mode 100644 index 000000000..10f07754f --- /dev/null +++ b/src/test/resources/same_package/pkg_init/names_sequential/names/name/name.go @@ -0,0 +1,45 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +// Contributed by Patricia Firlejczyk based on one of the examples +// not suitable for initialization-time irrelevance reported in +// https://dl.acm.org/doi/10.1145/3622844 + +// @ pkgInvariant NameInv() + +package name + +// ##(-I ../..) + +type Name struct { + _start int + _length int +} + +func init() { + // @ fold NameInv() +} + +// @ ensures acc(&res._length) && acc(&res._start) +// @ ensures res._length == length && res._start == start +// @ decreases +func New(start int, length int) (res *Name) { + res = new(Name) + res._start = start + res._length = length + return res +} + +// @ pure +// @ requires acc(&n._start, _) +// @ decreases +func (n *Name) start() int { + return n._start +} + +// @ pure +// @ requires acc(&n._length, _) +// @ decreases +func (n *Name) length() int { + return n._length +} diff --git a/src/test/resources/same_package/pkg_init/names_sequential/names/name/name_spec.gobra b/src/test/resources/same_package/pkg_init/names_sequential/names/name/name_spec.gobra new file mode 100644 index 000000000..38fedb4aa --- /dev/null +++ b/src/test/resources/same_package/pkg_init/names_sequential/names/name/name_spec.gobra @@ -0,0 +1,13 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +// Contributed by Patricia Firlejczyk based on one of the examples +// not suitable for initialization-time irrelevance reported in +// https://dl.acm.org/doi/10.1145/3622844 + +package name + +// ##(-I ../..) + +pred NameInv() { true } + diff --git a/src/test/resources/same_package/pkg_init/names_sequential/names/names.go b/src/test/resources/same_package/pkg_init/names_sequential/names/names.go new file mode 100644 index 000000000..54a51be95 --- /dev/null +++ b/src/test/resources/same_package/pkg_init/names_sequential/names/names.go @@ -0,0 +1,33 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +// Contributed by Patricia Firlejczyk based on one of the examples +// not suitable for initialization-time irrelevance reported in +// https://dl.acm.org/doi/10.1145/3622844 + +// @ pkgInvariant NamesInv() + +package names + +// ##(-I ..) + +import ( + "names/name" +) + +var chrs /*@@@*/ [131072]string + +func init() { + // @ fold NamesInv() +} + +// @ preserves NamesInv() +// @ ensures acc(&res._start) && acc(&res._length) && res._start == 0 +// @ decreases +func Name(s string) (res *name.Name) { + // @ unfold NamesInv() + res = name.New(0, len(chrs)) + chrs[0] = "a" + // @ fold NamesInv() + return res +} diff --git a/src/test/resources/same_package/pkg_init/names_sequential/names/names_spec.gobra b/src/test/resources/same_package/pkg_init/names_sequential/names/names_spec.gobra new file mode 100644 index 000000000..fb9a36fe9 --- /dev/null +++ b/src/test/resources/same_package/pkg_init/names_sequential/names/names_spec.gobra @@ -0,0 +1,14 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +// Contributed by Patricia Firlejczyk based on one of the examples +// not suitable for initialization-time irrelevance reported in +// https://dl.acm.org/doi/10.1145/3622844 + +package names + +// ##(-I ..) + +pred NamesInv() { + acc(&chrs) && len(chrs) == 131072 +} diff --git a/src/test/resources/same_package/pkg_init/names_sequential/stdNamesAlt/stdNamesAlt.go b/src/test/resources/same_package/pkg_init/names_sequential/stdNamesAlt/stdNamesAlt.go new file mode 100644 index 000000000..f376b3999 --- /dev/null +++ b/src/test/resources/same_package/pkg_init/names_sequential/stdNamesAlt/stdNamesAlt.go @@ -0,0 +1,25 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +// Contributed by Patricia Firlejczyk based on one of the examples +// not suitable for initialization-time irrelevance reported in +// https://dl.acm.org/doi/10.1145/3622844 + +// @ pkgInvariant StdNamesAltInv() + +package stdNamesAlt + +// ##(-I ..) + +import ( + "names" + "names/name" +) + +var anyRef *name.Name = names.Name("anyRef") +var array *name.Name = names.Name("array") +var list *name.Name = names.Name("list") + +func init() { + // @ fold StdNamesAltInv() +} diff --git a/src/test/resources/same_package/pkg_init/names_sequential/stdNamesAlt/stdNamesAlt_spec.gobra b/src/test/resources/same_package/pkg_init/names_sequential/stdNamesAlt/stdNamesAlt_spec.gobra new file mode 100644 index 000000000..790752799 --- /dev/null +++ b/src/test/resources/same_package/pkg_init/names_sequential/stdNamesAlt/stdNamesAlt_spec.gobra @@ -0,0 +1,16 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +// Contributed by Patricia Firlejczyk based on one of the examples +// not suitable for initialization-time irrelevance reported in +// https://dl.acm.org/doi/10.1145/3622844 + +package stdNamesAlt + +// ##(-I ..) + +pred StdNamesAltInv() { + acc(&anyRef._start, _) && acc(&anyRef._length, _) && anyRef._start == 0 && + acc(&array._start, _) && acc(&array._length, _) && array._start == 0 && + acc(&list._start, _) && acc(&list._length, _) && list._start == 0 +} diff --git a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala b/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala index 8f00dcb46..71064d30a 100644 --- a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala +++ b/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala @@ -345,13 +345,14 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside { def stubProgram(inArgs: Vector[(PParameter, Boolean)], body : PStatement) : PProgram = PProgram( PPackageClause(PPkgDef("pkg")), - Vector(), - Vector(), + Vector.empty, + Vector.empty, + Vector.empty, Vector(PFunctionDecl( PIdnDef("foo"), inArgs.map(_._1), PResult(Vector()), - PFunctionSpec(Vector(), Vector(), Vector(), Vector.empty, Vector.empty), + PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty), Some(PBodyParameterInfo(inArgs.collect{ case (n: PNamedParameter, true) => PIdnUse(n.id.name) }), PBlock(Vector(body))) )) ) @@ -385,7 +386,7 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside { val program = stubProgram(inArgs, stmt) val ghostLess = ghostLessProg(program) val block = ghostLess match { - case PProgram(_, _, _, Vector(PFunctionDecl(PIdnDef("foo"), _, _, _, Some((_, b))))) => b + case PProgram(_, _, _, _, Vector(PFunctionDecl(PIdnDef("foo"), _, _, _, Some((_, b))))) => b case p => fail(s"Parsing succeeded but with an unexpected program $p") } normalize(block.stmts) match { diff --git a/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala b/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala index 5f9992921..f989fd3ee 100644 --- a/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala +++ b/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala @@ -120,13 +120,13 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { test("Parser: spec only function") { frontend.parseMemberOrFail("func foo() { b.bar() }", specOnly = true) should matchPattern { - case Vector(PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false), None)) => + case Vector(PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false, false), None)) => } } test("Parser: spec only function with nested blocks") { frontend.parseMemberOrFail("func foo() { if(true) { b.bar() } else { foo() } }", specOnly = true) should matchPattern { - case Vector(PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false), None)) => + case Vector(PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false, false), None)) => } } @@ -159,7 +159,7 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { val modes: Set[Boolean] = Set(false, true) modes.foreach(specOnly => { frontend.parseMemberOrFail("func bar()", specOnly) should matchPattern { - case Vector(PFunctionDecl(PIdnDef("bar"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false), None)) => + case Vector(PFunctionDecl(PIdnDef("bar"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false, false), None)) => } }) } @@ -2643,19 +2643,19 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { test("Parser: should be able to parse normal termination measure") { frontend.parseMemberOrFail("decreases n; func factorial (n int) int") should matchPattern { - case Vector(PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), None)), Vector(), false, false, false), None)) => + case Vector(PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), None)), Vector(), false, false, false, false), None)) => } } test("Parser: should be able to parse underscore termination measure") { frontend.parseMemberOrFail("decreases _; func factorial (n int) int") should matchPattern { - case Vector(PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PWildcardMeasure(None)), Vector(), false, false, false), None)) => + case Vector(PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PWildcardMeasure(None)), Vector(), false, false, false, false), None)) => } } test("Parser: should be able to parse conditional termination measure" ) { frontend.parseMemberOrFail("decreases n if n>1; decreases _ if n<2; func factorial (n int) int") should matchPattern { - case Vector(PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), Some(PGreater(PNamedOperand(PIdnUse("n")), PIntLit(one, Decimal)))), PWildcardMeasure(Some(PLess(PNamedOperand(PIdnUse("n")), PIntLit(two, Decimal))))), Vector(), false, false, false), None)) if one == 1 && two == 2 => + case Vector(PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), Some(PGreater(PNamedOperand(PIdnUse("n")), PIntLit(one, Decimal)))), PWildcardMeasure(Some(PLess(PNamedOperand(PIdnUse("n")), PIntLit(two, Decimal))))), Vector(), false, false, false, false), None)) if one == 1 && two == 2 => } } diff --git a/src/test/scala/viper/gobra/typing/ExprTypingUnitTests.scala b/src/test/scala/viper/gobra/typing/ExprTypingUnitTests.scala index 7dfbcf8d9..98cdbe196 100644 --- a/src/test/scala/viper/gobra/typing/ExprTypingUnitTests.scala +++ b/src/test/scala/viper/gobra/typing/ExprTypingUnitTests.scala @@ -3366,6 +3366,7 @@ class ExprTypingUnitTests extends AnyFunSuite with Matchers with Inside { PPackageClause(PPkgDef("pkg")), Vector(), Vector(), + Vector(), Vector(PMethodDecl( PIdnDef("foo"), PUnnamedReceiver(PMethodReceiveName(PNamedOperand(PIdnUse("self")))), diff --git a/src/test/scala/viper/gobra/typing/MemberTypingUnitTests.scala b/src/test/scala/viper/gobra/typing/MemberTypingUnitTests.scala index aca8e4272..afe9aa164 100644 --- a/src/test/scala/viper/gobra/typing/MemberTypingUnitTests.scala +++ b/src/test/scala/viper/gobra/typing/MemberTypingUnitTests.scala @@ -84,6 +84,7 @@ class MemberTypingUnitTests extends AnyFunSuite with Matchers with Inside { PPackageClause(PPkgDef("pkg")), Vector(), Vector(), + Vector(), members ) (prog, idnUse.map(_ => idnDefX)) diff --git a/src/test/scala/viper/gobra/typing/StmtTypingUnitTests.scala b/src/test/scala/viper/gobra/typing/StmtTypingUnitTests.scala index 34e51a27d..20e5205c3 100644 --- a/src/test/scala/viper/gobra/typing/StmtTypingUnitTests.scala +++ b/src/test/scala/viper/gobra/typing/StmtTypingUnitTests.scala @@ -62,6 +62,7 @@ class StmtTypingUnitTests extends AnyFunSuite with Matchers with Inside { PPackageClause(PPkgDef("pkg")), Vector(), Vector(), + Vector(), Vector(PFunctionDecl( PIdnDef("foo"), inArgs.map(_._1), diff --git a/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala b/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala index 383924a5a..12e27bfa3 100644 --- a/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala +++ b/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala @@ -358,6 +358,7 @@ class TypeTypingUnitTests extends AnyFunSuite with Matchers with Inside { PPackageClause(PPkgDef("pkg")), Vector(), Vector(), + Vector(), Vector(PMethodDecl( PIdnDef("foo"), PUnnamedReceiver(PMethodReceiveName(PNamedOperand(PIdnUse("self")))),