diff --git a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala index 9999512d6..e6e288b0d 100644 --- a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala +++ b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala @@ -170,13 +170,13 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter } def showMethodSubtypeProof(m: MethodSubtypeProof): Doc = m match { - case MethodSubtypeProof(subProxy, superT, _, receiver, args, results, body) => + case MethodSubtypeProof(subProxy, superT, _, receiver, args, results, body, _) => "proof" <+> parens(showType(superT)) <+> parens(showVarDecl(receiver)) <+> subProxy.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <> opt(body)(b => block(showStmt(b))) } def showPureMethodSubtypeProof(m: PureMethodSubtypeProof): Doc = m match { - case PureMethodSubtypeProof(subProxy, superT, _, receiver, args, results, body) => + case PureMethodSubtypeProof(subProxy, superT, _, receiver, args, results, body, _) => "proof" <+> parens(showType(superT)) <+> "pure" <+> parens(showVarDecl(receiver)) <+> subProxy.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <> opt(body)(b => block("return" <+> showExpr(b))) } diff --git a/src/main/scala/viper/gobra/ast/internal/Program.scala b/src/main/scala/viper/gobra/ast/internal/Program.scala index b69047323..c69023310 100644 --- a/src/main/scala/viper/gobra/ast/internal/Program.scala +++ b/src/main/scala/viper/gobra/ast/internal/Program.scala @@ -223,7 +223,11 @@ case class MethodSubtypeProof( receiver: Parameter.In, args: Vector[Parameter.In], results: Vector[Parameter.Out], - body: Option[Block] // empty if it is generated + body: Option[Block], // empty if it is generated + // for a generated proof, the source of the `implements` clause that demanded it (if any). + // used exclusively by the dependency analysis to present all Viper nodes of the generated + // proof as a single dependency node; it does not affect verification or error positions. + implementsClauseSrc: Option[Parser.Info] = None )(val info: Source.Parser.Info) extends Member case class PureMethodSubtypeProof( @@ -233,7 +237,9 @@ case class PureMethodSubtypeProof( receiver: Parameter.In, args: Vector[Parameter.In], results: Vector[Parameter.Out], - body: Option[Expr] // empty if it is generated + body: Option[Expr], // empty if it is generated + // see MethodSubtypeProof.implementsClauseSrc + implementsClauseSrc: Option[Parser.Info] = None )(val info: Source.Parser.Info) extends Member { require(results.size <= 1) } diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index 004d3f858..4bc6db8bf 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/src/main/scala/viper/gobra/frontend/Desugar.scala @@ -3438,9 +3438,15 @@ object Desugar extends LazyLogging { val args = implSymb.args.zipWithIndex.map{ case (arg, idx) => inParameterD(arg, idx, implSymb.context.getTypeInfo)._1 } val results = implSymb.result.outs.zipWithIndex.map{ case (res, idx) => outParameterD(res, idx, implSymb.context.getTypeInfo)._1 } + // If the user wrote an `implements` clause (possibly without a proof body), remember its source so that + // the dependency analysis can present all Viper nodes of this generated proof as the single clause node. + // This does not influence verification or the position of verification errors (which stay on `src`). + val clauseSrc: Option[Source.Parser.Info] = + info.localImplementationProofNode(implT, itfT).map(clause => meta(clause, info)) + val src = meta(implSymb.decl, implSymb.context.getTypeInfo).createAnnotatedInfo(AutoImplProofAnnotation(implT.toString, itfT.toString)) - if (itfSymb.isPure) in.PureMethodSubtypeProof(subProxy, superT, superProxy, receiver, args, results, None)(src) - else in.MethodSubtypeProof(subProxy, superT, superProxy, receiver, args, results, None)(src) + if (itfSymb.isPure) in.PureMethodSubtypeProof(subProxy, superT, superProxy, receiver, args, results, None, clauseSrc)(src) + else in.MethodSubtypeProof(subProxy, superT, superProxy, receiver, args, results, None, clauseSrc)(src) } } var implementationProofPredicateAliases: Map[(in.Type, in.InterfaceT, String), in.FPredicateProxy] = Map.empty diff --git a/src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala b/src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala index 2d148364d..07077ed18 100644 --- a/src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala +++ b/src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala @@ -6,7 +6,7 @@ package viper.gobra.frontend.info -import viper.gobra.ast.frontend.{PCodeRoot, PEmbeddedDecl, PExpression, PFieldDecl, PFunctionDecl, PFunctionOrMethodDecl, PGeneralForStmt, PIdnNode, PIdnUse, PKeyedElement, PLabelUse, PMPredicateDecl, PMPredicateSig, PMember, PMethodDecl, PMethodSig, PMisc, PNode, PParameter, PPkgDef, PScope, PType} +import viper.gobra.ast.frontend.{PCodeRoot, PEmbeddedDecl, PExpression, PFieldDecl, PFunctionDecl, PFunctionOrMethodDecl, PGeneralForStmt, PIdnNode, PIdnUse, PImplementationProof, PKeyedElement, PLabelUse, PMPredicateDecl, PMPredicateSig, PMember, PMethodDecl, PMethodSig, PMisc, PNode, PParameter, PPkgDef, PScope, PType} import viper.gobra.frontend.PackageInfo import viper.gobra.frontend.PackageResolver.AbstractImport import viper.gobra.frontend.info.base.BuiltInMemberTag.BuiltInMemberTag @@ -103,6 +103,9 @@ trait ExternalTypeInfo { /** returns all implementation proofs found in the current package */ def localImplementationProofs: Vector[(Type, InterfaceT, Vector[String], Vector[String])] + /** returns the `implements` clause node declared in the current package for the given subtype/supertype pair, if any */ + def localImplementationProofNode(subT: Type, superT: InterfaceT): Option[PImplementationProof] + /** returns the code root for a given node; can only be called on nodes that are enclosed in a code root */ def codeRoot(n: PNode): PCodeRoot with PScope 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 28889d347..e63d95862 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 @@ -134,6 +134,16 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => } } + override def localImplementationProofNode(subT: Type, superT: InterfaceT): Option[PImplementationProof] = { + val implementationProofs = tree.root.programs.flatMap(_.declarations.collect{ case m: PImplementationProof => m}) + implementationProofs.find { ip => + (symbType(ip.subT), underlyingType(symbType(ip.superT))) match { + case (`subT`, `superT`) => true + case _ => false + } + } + } + /** * Depends on which packages are loaded. Only call at the end of type checking. * Either returns a set of errors caused by invalid or missing implementation proofs diff --git a/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala index 0b3a05655..8c93dcc05 100644 --- a/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala @@ -9,7 +9,7 @@ package viper.gobra.translator.encodings.interfaces import org.bitbucket.inkytonik.kiama.==> import viper.gobra.ast.internal.theory.{Comparability, TypeHead} import viper.gobra.ast.{internal => in} -import viper.gobra.dependencyAnalysis.ImplProofDependencyAnalysisSourceInfo +import viper.gobra.dependencyAnalysis.{GobraDependencyAnalysisSourceInfo, ImplProofDependencyAnalysisSourceInfo} import viper.gobra.reporting._ import viper.gobra.theory.Addressability import viper.gobra.theory.Addressability.{Exclusive, Shared} @@ -20,7 +20,8 @@ import viper.gobra.translator.util.FunctionGenerator import viper.gobra.translator.util.ViperWriter.CodeWriter import viper.gobra.util.{Algorithms, Violation} import viper.silver.ast.MakeInfoPair -import viper.silver.dependencyAnalysis.{AdditionalAssertionNode, EdgeType, JoinType, SimpleDependencyAnalysisJoin} +import viper.silver.ast.utility.ViperStrategy +import viper.silver.dependencyAnalysis.{AdditionalAssertionNode, AssumptionType, DependencyAnalysisSourceInfo, DependencyTypeInfo, EdgeType, JoinType, SimpleDependencyAnalysisJoin, StringDependencyAnalysisSourceInfo} import viper.silver.plugin.standard.termination import viper.silver.verifier.ErrorReason import viper.silver.{ast => vpr} @@ -735,6 +736,57 @@ class InterfaceEncoding extends LeafTypeEncoding { } yield func } + /** True iff `info` originates from a proof that Gobra generated itself (see Desugar.missingImplProofs). */ + private def isAutoGeneratedProof(info: Source.Parser.Info): Boolean = { + def hasAnnotation(o: Source.AbstractOrigin): Boolean = o match { + case Source.AnnotatedOrigin(_, _: Source.AutoImplProofAnnotation) => true + case Source.AnnotatedOrigin(inner, _) => hasAnnotation(inner) + case _ => false + } + info.origin.exists(hasAnnotation) + } + + /** + * Gives every Viper node of a *generated* implementation proof a single dependency-analysis source info, so that + * the dependency analysis presents all of them as one node instead of scattering them across the interface's and + * the concrete method's pre-/postconditions: + * - if the user wrote an `implements` clause, that clause becomes the presented node; + * - otherwise (the proof was demanded e.g. only by an upcast) the nodes get a single internal node that is + * hidden from the user-level graph (marked with an internal dependency type); the `SimpleDependencyAnalysisJoin` + * tags emitted elsewhere still link it to the corresponding upcasts. + * + * This only influences the dependency analysis: each node's Verifier.Info, position and error transformer are + * preserved (so the position of verification errors is unchanged), and nodes that already carry a source info are + * left untouched. User-provided proofs (which are not auto-generated) are left exactly as before. + */ + private def withGeneratedProofDependencySource[N <: vpr.Node](node: N, info: Source.Parser.Info, clauseSrc: Option[Source.Parser.Info], subT: in.Type, superT: in.InterfaceT): N = { + val depInfo: Option[(DependencyAnalysisSourceInfo, Option[DependencyTypeInfo])] = clauseSrc match { + // a clause source is only ever attached to generated proofs, so no extra generated-check is needed here + case Some(s: Source.Parser.Single) => + Some((GobraDependencyAnalysisSourceInfo(s.pnode, vpr.TranslatedPosition(s.src.pos)), None)) + case _ if isAutoGeneratedProof(info) => + val internalSource = StringDependencyAnalysisSourceInfo(s"generated implementation proof: $subT implements $superT") + Some((internalSource, Some(DependencyTypeInfo(AssumptionType.Internal.asDepType())))) + case _ => None + } + depInfo match { + case Some((source, depTypeOpt)) => + def enrich(i: vpr.Info): vpr.Info = { + val withSource = if (i.getUniqueInfo[DependencyAnalysisSourceInfo].isDefined) i else MakeInfoPair(i, source) + depTypeOpt match { + case Some(depType) if withSource.getUniqueInfo[DependencyTypeInfo].isEmpty => MakeInfoPair(withSource, depType) + case _ => withSource + } + } + ViperStrategy.Slim({ + case n: vpr.Member => n.withMeta((n.meta._1, enrich(n.meta._2), n.meta._3)) + case n: vpr.Stmt => n.withMeta((n.meta._1, enrich(n.meta._2), n.meta._3)) + case n: vpr.Exp => n.withMeta((n.meta._1, enrich(n.meta._2), n.meta._3)) + }).forceCopy().execute[N](node) + case None => node + } + } + /** * function proof_T_I_F(x: T, args) * requires PRE where PRE = [I_F.PRE][ this -> tuple2(this, Type(this)); tuple2(this, Type(this)).I_F -> this.proof_T_implements_I_F ] @@ -776,7 +828,9 @@ class InterfaceEncoding extends LeafTypeEncoding { val depAnJoinInfo = SimpleDependencyAnalysisJoin(ImplProofDependencyAnalysisSourceInfo(p.receiver.typ, p.superT), JoinType.Source, EdgeType.Down) // TODO ake: should every proof obligation in the impl proof be a dependency of every upcast? - pureMethodDummy.map(res => res.copy(pres = pres, posts = posts.flatMap(_.topLevelConjuncts).map(p => p.withMeta(p.pos, MakeInfoPair(depAnJoinInfo, p.info), p.errT)))(pos, MakeInfoPair(depAnJoinInfo, info), errT)) + pureMethodDummy.map(res => withGeneratedProofDependencySource( + res.copy(pres = pres, posts = posts.flatMap(_.topLevelConjuncts).map(p => p.withMeta(p.pos, MakeInfoPair(depAnJoinInfo, p.info), p.errT)))(pos, MakeInfoPair(depAnJoinInfo, info), errT), + p.info, p.implementsClauseSrc, p.receiver.typ, p.superT)) } /** @@ -827,7 +881,9 @@ class InterfaceEncoding extends LeafTypeEncoding { val depAnJoinInfo = SimpleDependencyAnalysisJoin(ImplProofDependencyAnalysisSourceInfo(p.receiver.typ, p.superT), JoinType.Source, EdgeType.Down) // TODO ake: should every proof obligation in the impl proof be a dependency of every upcast? - methodDummy.map(res => res.copy(pres = pres, posts = posts.flatMap(_.topLevelConjuncts).map(p => p.withMeta(p.pos, MakeInfoPair(depAnJoinInfo, p.info), p.errT)))(pos, MakeInfoPair(depAnJoinInfo, info), errT)) + methodDummy.map(res => withGeneratedProofDependencySource( + res.copy(pres = pres, posts = posts.flatMap(_.topLevelConjuncts).map(p => p.withMeta(p.pos, MakeInfoPair(depAnJoinInfo, p.info), p.errT)))(pos, MakeInfoPair(depAnJoinInfo, info), errT), + p.info, p.implementsClauseSrc, p.receiver.typ, p.superT)) }