Add necessary framework to enable selective verification of methods in viper

src/main/scala/viper/silver/ast/Position.scala

@@ -34,6 +34,12 @@ trait HasLineColumn extends Position {
     else column <= other.column
   }
 
+  def >=(other: HasLineColumn): Boolean = {
+    if (line > other.line) true
+    else if (line < other.line) false
+    else column >= other.column
+  }
+
   def deltaColumn(delta: Int): HasLineColumn
   override def toString = s"$line.$column"
 }

src/main/scala/viper/silver/reporter/Message.scala

@@ -8,7 +8,7 @@ package viper.silver.reporter
 
 import viper.silver.reporter.BackendSubProcessStages.BackendSubProcessStage
 import viper.silver.verifier._
-import viper.silver.ast.{QuantifiedExp, Trigger}
+import viper.silver.ast.{QuantifiedExp, SourcePosition, Trigger}
 import viper.silver.parser.PProgram
 
 /**
@@ -180,6 +180,12 @@ case class StatisticsReport(nOfMethods: Int, nOfFunctions: Int, nOfPredicates: I
   override val name = "statistics"
 }
 
+case class TargetSelectionReport(target: SourcePosition) extends Message {
+
+  override lazy val toString: String = s"target_selection_report(target=${target})"
+  override val name: String = "target_selection"
+}
+
 case class ProgramOutlineReport(members: List[Entity]) extends Message {
 
   override lazy val toString: String = s"program_outline_report(members=${members.map(print)})"

src/main/scala/viper/silver/reporter/Reporter.scala

@@ -81,6 +81,9 @@ case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv
         warnings.foreach(report => {
           csv_file.write(s"WarningsDuringParsing,${report}\n")
         })
+      case TargetSelectionReport(ts) => {
+        csv_file.write(s"TargetSelection,${ts}\n")
+      }
       case WarningsDuringTypechecking(warnings) =>
         warnings.foreach(report => {
           csv_file.write(s"WarningsDuringTypechecking,${report}\n")
@@ -186,6 +189,9 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t
       case AnnotationWarning(text) =>
         println(s"Annotation warning: ${text}")
 
+      case TargetSelectionReport(rep) =>
+        println(s"Target selection: ${rep}")
+
       case InvalidArgumentsReport(_, errors) =>
         errors.foreach(e => println(s"  ${e.readableMessage}"))
         println( s"Run with just --help for usage and options" )

src/main/scala/viper/silver/utility/Caching.scala

@@ -19,6 +19,20 @@ trait DependencyAware {
 
   val dependencyHashMap: Map[Method, String]
 
+  private def handleFunction(p: Program, marker: mutable.Set[Hashable], func: Function): Seq[Hashable] = {
+    if (!marker.contains(func)) {
+      markSubAST(func, marker)
+      Seq(func) ++ getDependenciesRec(p, func.pres ++ func.posts ++ extractOptionalNode(func.body), marker)
+    } else Nil
+  }
+
+  private def handlePredicate(p: Program, marker: mutable.Set[Hashable], pred: Predicate): Seq[Hashable] = {
+    if (!marker.contains(pred)) {
+      markSubAST(pred, marker)
+      Seq(pred) ++ getDependenciesRec(p, extractOptionalNode(pred.body), marker)
+    } else Nil
+  }
+
   /**
     * Get the (irreflexive) transitive closure of dependencies of nodes from a list.
     *
@@ -37,20 +51,35 @@ trait DependencyAware {
         n.deepCollect {
           case func_app: FuncApp =>
             val func = p.findFunction(func_app.funcname)
-            if (!marker.contains(func)) {
-              markSubAST(func, marker)
-              Seq(func) ++ getDependenciesRec(p, func.pres ++ func.posts ++ extractOptionalNode(func.body), marker)
-            } else Nil
+            handleFunction(p, marker, func)
           case pred_access: PredicateAccess =>
             val pred = p.findPredicate(pred_access.predicateName)
-            if (!marker.contains(pred)) {
-              markSubAST(pred, marker)
-              Seq(pred) ++ getDependenciesRec(p, extractOptionalNode(pred.body), marker)
-            } else Nil
+            handlePredicate(p, marker, pred)
         } flatten
     } toList
   }
 
+  private def getDependenciesInner(p: Program, m: Method, includeMethods: Boolean): List[Hashable] = {
+    val marker: mutable.Set[Hashable] = mutable.Set.empty
+    markSubAST(m, marker)
+    Seq(m) ++ p.domains ++ p.fields ++
+      (m.pres ++ m.posts ++ m.body.toSeq).flatMap {
+        n => n.deepCollect {
+          case method_call: MethodCall =>
+            val method = p.findMethod(method_call.methodName)
+            if (!marker.contains(method)) {
+              (if(includeMethods) {getDependenciesInner(p, method, includeMethods)} else {Seq()}) ++ method.formalArgs ++ method.formalReturns ++
+                method.pres ++ method.posts ++
+                getDependenciesRec(p, method.formalArgs ++ method.formalReturns ++ method.pres ++ method.posts, marker)
+            } else Nil
+          case func_app: FuncApp =>
+            getDependenciesRec(p, Seq(func_app), marker)
+          case pred_access: PredicateAccess =>
+            getDependenciesRec(p, Seq(pred_access), marker)
+        } flatten
+      } toList
+  }
+
   /**
     * Find all (irreflexive) dependencies of the current method.
     *
@@ -70,24 +99,25 @@ trait DependencyAware {
     *          List of dependency [[Hashable]]s.
     */
   def getDependencies(p: Program, m: Method): List[Hashable] = {
+    getDependenciesInner(p, m, false)
+  }
+
+  /**
+   * Same as `getDependencies`, but instead also collects all methods that are used transitively.
+   * `getDependencies` is used for caching, which does not include transitively called
+   * methods (only their pres, posts, etc.).
+   *
+   * `getDependenciesWithMethods` is instead used for the IDE functionality that allows to verify
+   * a method or function at a specific source code location. In this case, we do want to also include
+   * methods, so that we can form the transitive closure.
+   */
+  def getMethodDependenciesWithMethods(p: Program, m: Method): List[Hashable] = {
+    getDependenciesInner(p, m, true)
+  }
+
+  def getFunctionDependencies(p: Program, f: Function): List[Hashable] = {
     val marker: mutable.Set[Hashable] = mutable.Set.empty
-    markSubAST(m, marker)
-    Seq(m) ++ p.domains ++ p.fields ++
-      (m.pres ++ m.posts ++ m.body.toSeq).flatMap {
-        n => n.deepCollect {
-          case method_call: MethodCall =>
-            val method = p.findMethod(method_call.methodName)
-            if (!marker.contains(method)) {
-              method.formalArgs ++ method.formalReturns ++
-                method.pres ++ method.posts ++
-                getDependenciesRec(p, method.formalArgs ++ method.formalReturns ++ method.pres ++ method.posts, marker)
-            } else Nil
-          case func_app: FuncApp =>
-            getDependenciesRec(p, Seq(func_app), marker)
-          case pred_access: PredicateAccess =>
-            getDependenciesRec(p, Seq(pred_access), marker)
-        } flatten
-      } toList
+    handleFunction(p, marker, f) toList
   }
 
   private def markSubAST(node: Node, marker: mutable.Set[Hashable]): Unit = node.deepCollect {

src/test/scala/MethodDependencyTests.scala

@@ -135,6 +135,11 @@ class MethodDependencyTests extends AnyFunSuite with Matchers {
 
   val computed_deps: List[Hashable] = p.getDependencies(p, test)
 
+  // These are for testing the method that also fetches transitive method depdendencies.
+  val must_be_deps_with_methods: List[Hashable] = List(test) ++ global_deps ++ via_pre_deps ++ via_post_deps ++ via_body_deps ++ transitive_deps ++ List(m0) ++ List(m1)
+  val must_not_be_deps_with_methods: List[Hashable] = List(fun3, p3)
+
+  val computed_deps_with_methods: List[Hashable] = p.getMethodDependenciesWithMethods(p, test)
 
   val test_prefix = s"Test Dependency Analysis"
 
@@ -195,6 +200,14 @@ class MethodDependencyTests extends AnyFunSuite with Matchers {
     }
   }
 
+  test(s"$test_prefix: do we fetch method dependencies for `getMethodDependenciesWithMethods`?") {
+    computed_deps_with_methods.foreach {
+      n =>
+        if ( !must_be_deps_with_methods.contains(n) || must_not_be_deps_with_methods.contains(n) )
+          fail(s"AST node ```$n``` is not expected to be a dependency of ```$test```, but is present in the result of `getDependenciesWithMethods`.")
+    }
+  }
+
   test(s"$test_prefix: are there duplicated dependencies?") {
     computed_deps.size should be (computed_deps.distinct.size)
   }