Add support for chopping programs before the Termination plugin runs

src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala

@@ -50,9 +50,10 @@ trait ChopperLike { this: ViperGraphs with Cut =>
     * for all returned Viper programs. Members that are not dependencies of important nodes are not contained
     * in any of the returned programs.
     *
-    * The chopper does not support AST nodes introduced by Viper plugins. However, the chopper can be invoked
-    * after the AST nodes are translated through SilverPlugin.beforeVerify. Furthermore, in the input Viper program,
-    * all quantified expressions must have triggers.
+    * The chopper does not support AST nodes introduced by Viper plugins, except for those introduced by the
+    * termination plugin (in which case, `beforeTerminationPlugin` must be true). However, the chopper can be
+    * invoked after the AST nodes are translated through SilverPlugin.beforeVerify. Furthermore, in the
+    * input Viper program, all quantified expressions must have triggers.
     *
     * @param choppee   Targeted program.
     * @param selection Specifies which members of the program should be verified.
@@ -61,6 +62,7 @@ trait ChopperLike { this: ViperGraphs with Cut =>
     *                  If none, then maximum number of programs is returned.
     * @param penalty   Specifies penalty of merging programs. Two default implementations are provided.
     *                  [[Penalty.DefaultWithoutForcedMerge]] defines that the penalty of a merge is always > 0.
+    * @param beforeTerminationPlugin Specifies if the chopper is running before the termination plugin.
     * @return Chopped programs.
     */
   def chop(
@@ -69,8 +71,9 @@ trait ChopperLike { this: ViperGraphs with Cut =>
             selection: Option[ast.Member => Boolean] = None,
             bound: Option[Int] = Some(1),
             penalty: Penalty[Vertices.Vertex] = Penalty.Default,
+            beforeTerminationPlugin: Boolean = false,
           ): Vector[ast.Program] = {
-    chopWithMetrics(choppee)(selection, bound, penalty)._1
+    chopWithMetrics(choppee)(selection, bound, penalty, beforeTerminationPlugin)._1
   }
 
   /**
@@ -83,6 +86,7 @@ trait ChopperLike { this: ViperGraphs with Cut =>
     *                  If none, then maximum number of programs is returned.
     * @param penalty   Specifies penalty of merging programs. Two default implementations are provided.
     *                  [[Penalty.DefaultWithoutForcedMerge]] defines that the penalty of a merge is always > 0.
+    * @param beforeTerminationPlugin Specifies if the chopper is running before the termination plugin.
     * @return Chopped programs and metrics.
     */
   def chopWithMetrics(
@@ -91,9 +95,10 @@ trait ChopperLike { this: ViperGraphs with Cut =>
                        selection: Option[ast.Member => Boolean] = None,
                        bound: Option[Int] = Some(1),
                        penalty: Penalty[Vertices.Vertex] = Penalty.Default,
+                       beforeTerminationPlugin: Boolean = false,
                      ): (Vector[ast.Program], Metrics) = {
 
-    val graph = toGraph(choppee, selection)
+    val graph = toGraph(choppee, selection, beforeTerminationPlugin)
     val (programs, metrics) = boundedCut(graph)(bound, penalty)
     (programs flatMap (list => graph.unapply(list)), metrics)
   }
@@ -611,6 +616,7 @@ trait ViperGraphs { this: Vertices with Edges =>
   def toGraph(
                program: ast.Program,
                select: Option[ast.Member => Boolean] = None,
+               beforeTerminationPlugin: Boolean = false,
              ): ViperGraph = {
 
     var vertexToId = Map.empty[Vertices.Vertex, Int]
@@ -626,7 +632,7 @@ trait ViperGraphs { this: Vertices with Edges =>
     }
 
     val members = program.members.toVector
-    val vertexEdges = members.flatMap(dependencies)
+    val vertexEdges = members.flatMap(dependencies(_, beforeTerminationPlugin))
     val edges = vertexEdges.map { case (l, r) => (id(l), id(r)) }
     val selector: ast.Member => Boolean = select.getOrElse {
       // Per default, the important nodes are all nodes with a proof obligation, i.e. methods, functions, and predicates.
@@ -836,13 +842,14 @@ object Edges {
 
 trait Edges { this: Vertices =>
   import Edges._
+  import viper.silver.plugin.standard.termination.TerminationPlugin.wellFoundedOrderDomainSuffix
 
   /**
     * Returns all dependencies induced by a member.
     * The result is an unsorted sequence of edges.
     * The edges are sorted at a later point, after the translation to int nodes (where it is cheaper).
     * */
-  def dependencies(member: ast.Member): Seq[Edge[Vertices.Vertex]] = {
+  def dependencies(member: ast.Member, beforeTerminationPlugin: Boolean): Seq[Edge[Vertices.Vertex]] = {
     val defVertex = toDefVertex(member)
     val useVertex = toUseVertex(member)
 
@@ -865,6 +872,28 @@ trait Edges { this: Vertices =>
 
       case _: ast.Field => dependenciesToChildren(member, defVertex)
 
+      case d: ast.Domain if d.name.endsWith(wellFoundedOrderDomainSuffix) && beforeTerminationPlugin =>
+        // If we are computing dependencies before the termination plugin has run, then
+        // we conservatively include all domains that define well founded orders for
+        // termination checking, given that, at this point, there is no explicit dependency between
+        // the expressions in the termination measure and the "bounded" and "decreasing" functions defined
+        // in the domains that establish a well-founded order, and these domains end up being removed,
+        // leading to errors.
+        val domainVertex = toDefVertex(d)
+        val axiomDeps = d.axioms.flatMap { ax =>
+          val axVertex = Vertices.DomainAxiom(ax, d)
+          val dependenciesOfAxiom = dependenciesToChildren(ax.exp, axVertex)
+          val dependenciesToAxiom = Seq(domainVertex -> axVertex)
+          dependenciesOfAxiom ++ dependenciesToAxiom
+        }
+        val funcDeps = d.functions.flatMap { f =>
+          val fVertex = Vertices.DomainFunction(f.name)
+          val dependenciesOfFunction = dependenciesToChildren(f, fVertex)
+          val dependenciesToFunction = Seq(domainVertex -> fVertex)
+          dependenciesOfFunction ++ dependenciesToFunction
+
+        }
+        (Vertices.Always -> domainVertex) +: (axiomDeps ++ funcDeps)
       case d: ast.Domain =>
         d.axioms.flatMap { ax =>
 

src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala

@@ -169,7 +169,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
     // Check if the program contains any domains that define decreasing and bounded functions that do *not* have the expected names.
     for (d <- input.domains) {
       val name = d.idndef.name
-      val typeName = if (name.endsWith("WellFoundedOrder"))
+      val typeName = if (name.endsWith(TerminationPlugin.wellFoundedOrderDomainSuffix))
         Some(name.substring(0, name.length - 16))
       else
         None
@@ -411,4 +411,8 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
     case Unfolding(_, exp) => Seq(exp)
     case CurrentPerm(_) => Nil
   })
+}
+
+object TerminationPlugin {
+  val wellFoundedOrderDomainSuffix = "WellFoundedOrder"
 }

src/test/scala/ChopperTests.scala

@@ -235,6 +235,23 @@ class ChopperTests extends AnyFunSuite with Matchers with Inside {
     )
   }
 
+  test("WellFoundedOrders are kept for programs that still have termination measures") {
+    val intVarDecl = ast.LocalVarDecl("i", ast.Int)()
+    val function = ast.Function("functionA", Seq(intVarDecl), ast.Bool, Seq.empty, Seq.empty, None)()
+    val domainName = "IntWellFoundedOrder"
+    val decreasingFn = ast.DomainFunc(
+      "decreasing",
+      Seq(ast.LocalVarDecl("l1", ast.Int)(), ast.LocalVarDecl("l2", ast.Int)()),
+      ast.Bool,
+    )(domainName = domainName)
+    val boundedFn = ast.DomainFunc("bounded", Seq(ast.LocalVarDecl("l", ast.Int)()), ast.Bool)(domainName = domainName)
+    val wfoDomain = ast.Domain(domainName, Seq(decreasingFn, boundedFn), Seq())()
+    val program = ast.Program(Seq(wfoDomain), Seq.empty, Seq(function), Seq.empty, Seq.empty, Seq.empty)()
+    val result = Chopper.chop(program)(bound = Some(5), penalty = Penalty.DefaultWithoutForcedMerge, beforeTerminationPlugin = true)
+    result.length shouldBe 1
+    result.head shouldEqual program
+  }
+
   // SCC tests
 
   test("SCC with singleton graph") {