From 25d519f3635069889baa6dc787571bd6121119ef Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 16 Jul 2026 17:43:13 +0000 Subject: [PATCH 1/2] Map auto-generated impl proofs to their `implements` clause in dependency analysis For an implementation proof that Gobra generates itself (the user wrote an `implements` clause but no proof body, or only a partial one), the Viper nodes of the generated proof previously inherited their dependency-analysis source from wherever they were built: the interface method's pre-/postconditions, the concrete method declaration, and its implicit pre-/postconditions. As a result the dependency analysis reported the proof's obligations as several unrelated Gobra nodes instead of one, and duplicated interface-spec nodes (issue #1042). This attaches the `implements` clause as the dependency-analysis source info of every Viper node of the generated proof, so the analysis presents them as a single dependency node (the clause). The change is confined to the dependency analysis: each node's Verifier.Info, position and error transformer are left untouched, so the position of verification errors is unchanged. Proofs without an `implements` clause and user-provided proof bodies are left exactly as before. - MethodSubtypeProof / PureMethodSubtypeProof carry the optional clause source. - Desugar looks up the clause via a new TypeInfo.localImplementationProofNode. - InterfaceEncoding stamps the clause source over the generated proof subtree. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_017ooFpeAJHUgFCaStKfdUTy --- .../gobra/ast/internal/PrettyPrinter.scala | 4 +- .../viper/gobra/ast/internal/Program.scala | 10 ++++- .../scala/viper/gobra/frontend/Desugar.scala | 10 ++++- .../frontend/info/ExternalTypeInfo.scala | 5 ++- .../typing/ghost/GhostMemberTyping.scala | 10 +++++ .../interfaces/InterfaceEncoding.scala | 39 +++++++++++++++++-- 6 files changed, 67 insertions(+), 11 deletions(-) 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..78fe6da78 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, DependencyAnalysisSourceInfo, EdgeType, JoinType, SimpleDependencyAnalysisJoin} import viper.silver.plugin.standard.termination import viper.silver.verifier.ErrorReason import viper.silver.{ast => vpr} @@ -735,6 +736,32 @@ class InterfaceEncoding extends LeafTypeEncoding { } yield func } + /** + * If the user wrote an `implements` clause for this generated implementation proof, attaches the clause as the + * dependency-analysis source info of every sub-node of the proof. As a result, the dependency analysis presents + * all Viper nodes of the generated proof as a single dependency node (the clause) instead of scattering them + * across the interface's and the concrete method's pre-/postconditions. + * + * 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 + * (e.g. because they stem from a user-provided proof body) are left untouched. If there is no `implements` + * clause, the proof is left exactly as before. + */ + private def withGeneratedProofDependencySource[N <: vpr.Node](node: N, clauseSrc: Option[Source.Parser.Info]): N = { + clauseSrc match { + case Some(s: Source.Parser.Single) => + val source: DependencyAnalysisSourceInfo = GobraDependencyAnalysisSourceInfo(s.pnode, vpr.TranslatedPosition(s.src.pos)) + def enrich(i: vpr.Info): vpr.Info = + if (i.getUniqueInfo[DependencyAnalysisSourceInfo].isDefined) i else MakeInfoPair(i, source) + 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 _ => 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 +803,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.implementsClauseSrc)) } /** @@ -827,7 +856,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.implementsClauseSrc)) } From 3fef134a6f9bc9e4f10b12c1117326dc3b50ba6e Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 17 Jul 2026 09:37:56 +0000 Subject: [PATCH 2/2] Handle no-clause generated impl proofs with a hidden internal dependency node Extends the previous change so that generated implementation proofs are handled in both cases the dependency analysis cares about: - With an `implements` clause: all Viper nodes of the generated proof are presented as the single clause node (as before). - Without a clause (the proof is demanded e.g. only by an upcast): all its Viper nodes are grouped into one node marked internal via DependencyType Internal, so it stays in the lower-level graph and is hidden from the user, while the existing SimpleDependencyAnalysisJoin tags keep it connected to the corresponding upcasts. An auto-generated check on the AutoImplProofAnnotation distinguishes generated proofs from user-provided ones (both carry no clause source), so user-provided proofs remain untouched. Verifier.Info, positions and error transformers are preserved throughout, so verification error positions are unchanged. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_017ooFpeAJHUgFCaStKfdUTy --- .../interfaces/InterfaceEncoding.scala | 57 +++++++++++++------ 1 file changed, 41 insertions(+), 16 deletions(-) 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 78fe6da78..8c93dcc05 100644 --- a/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala @@ -21,7 +21,7 @@ import viper.gobra.translator.util.ViperWriter.CodeWriter import viper.gobra.util.{Algorithms, Violation} import viper.silver.ast.MakeInfoPair import viper.silver.ast.utility.ViperStrategy -import viper.silver.dependencyAnalysis.{AdditionalAssertionNode, DependencyAnalysisSourceInfo, EdgeType, JoinType, SimpleDependencyAnalysisJoin} +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} @@ -736,29 +736,54 @@ 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) + } + /** - * If the user wrote an `implements` clause for this generated implementation proof, attaches the clause as the - * dependency-analysis source info of every sub-node of the proof. As a result, the dependency analysis presents - * all Viper nodes of the generated proof as a single dependency node (the clause) instead of scattering them - * across the interface's and the concrete method's pre-/postconditions. + * 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 - * (e.g. because they stem from a user-provided proof body) are left untouched. If there is no `implements` - * clause, the proof is left exactly as before. + * 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, clauseSrc: Option[Source.Parser.Info]): N = { - clauseSrc match { + 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) => - val source: DependencyAnalysisSourceInfo = GobraDependencyAnalysisSourceInfo(s.pnode, vpr.TranslatedPosition(s.src.pos)) - def enrich(i: vpr.Info): vpr.Info = - if (i.getUniqueInfo[DependencyAnalysisSourceInfo].isDefined) i else MakeInfoPair(i, source) + 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 _ => node + case None => node } } @@ -805,7 +830,7 @@ class InterfaceEncoding extends LeafTypeEncoding { // TODO ake: should every proof obligation in the impl proof be a dependency of every upcast? 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.implementsClauseSrc)) + p.info, p.implementsClauseSrc, p.receiver.typ, p.superT)) } /** @@ -858,7 +883,7 @@ class InterfaceEncoding extends LeafTypeEncoding { // TODO ake: should every proof obligation in the impl proof be a dependency of every upcast? 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.implementsClauseSrc)) + p.info, p.implementsClauseSrc, p.receiver.typ, p.superT)) }