Map auto-generated impl proofs to their implements clause in dependency analysis

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)))
   }

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)
 }

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

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
 

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

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))
   }