diff --git a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala index e0647ef2d..0516714eb 100644 --- a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala +++ b/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 => diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala index 1aa3261f9..66d939f5d 100644 --- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala +++ b/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" } \ No newline at end of file diff --git a/src/test/scala/ChopperTests.scala b/src/test/scala/ChopperTests.scala index a20742ae8..2b319e6aa 100644 --- a/src/test/scala/ChopperTests.scala +++ b/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") {