Making chopper available via command line

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

@@ -9,6 +9,7 @@ package viper.silver.ast.utility.chopper
 import viper.silver.ast
 import viper.silver.ast.AnnotationInfo
 import viper.silver.ast.utility.{Nodes, Visitor}
+import viper.silver.plugin.standard.termination.TerminationPluginConstants
 
 import scala.annotation.tailrec
 import scala.collection.{immutable, mutable}
@@ -50,9 +51,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. 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.
+    * A version of the chopper that is compatible with the termination plugin is defined below.
     *
     * @param choppee   Targeted program.
     * @param selection Specifies which members of the program should be verified.
@@ -1174,3 +1176,57 @@ trait SCC {
   }
 
 }
+
+/**
+  * Chopper with support for plugins used by Gobra, in particular Viper's termination plugin.
+  */
+object PluginAwareChopper extends ChopperLike with ViperGraphs with PluginAwareEdges with Vertices with Cut with SCC
+
+/**
+  * Extends the chopper's dependency computation to add artificial dependencies for domains ending in 'WellFoundedOrder',
+  * their axioms, and subexpressions.
+  * These artificial dependencies ensure that these axioms are retained by the chopper, which is necessary
+  * to ensure successful verification of the chopped program because these axioms define well-founded orders
+  * via "bounded" and "decreasing" functions. Without these artificial dependencies, the chopper would remove
+  * these axioms as the decreases measures do not explicitly depend on, i.e., call these domain functions.
+  */
+trait PluginAwareEdges extends Edges {
+  this: Vertices =>
+
+  import viper.silver.ast
+  import viper.silver.ast.utility.chopper.Edges.Edge
+
+  override def dependencies(member: ast.Member): Seq[Edge[Vertices.Vertex]] = member match {
+    case d: ast.Domain if d.name.endsWith(TerminationPluginConstants.WellFoundedOrderDomainName) =>
+      val defVertex = toDefVertex(member)
+      val useVertex = toUseVertex(member)
+
+      val usageDependencies = {
+        // 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)
+      }
+      // to ensure that nodes that depend on Vertex.Always are indeed always included
+      val alwaysDependencies = Seq(defVertex -> Vertices.Always, useVertex -> Vertices.Always)
+      usageDependencies ++ alwaysDependencies
+    case _ => super.dependencies(member)
+  }
+}

src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala

@@ -52,9 +52,11 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     hidden = true
   )
 
-  val methods = opt[String]("methods",
-    descr = "The Viper methods that should be verified. :all means all methods.",
-    default = Some(":all"),
+  val select = opt[String]("select",
+    descr = "Selects specific Viper methods, functions and predicates to be be verified along with the necessary " +
+      "dependencies. All other parts of the given Viper program will be ignored. " +
+      "The expected format is a list of method/function/predicate names separated by commas, e.g., name1,name2,name3.",
+    default = None,
     noshort = true,
     hidden = true
   )

src/main/scala/viper/silver/frontend/SilFrontend.scala

@@ -13,8 +13,10 @@ import viper.silver.plugin.SilverPluginManager
 import viper.silver.plugin.SilverPluginManager.PluginException
 import viper.silver.reporter._
 import viper.silver.verifier._
+
 import java.nio.file.{Path, Paths}
 import viper.silver.FastMessaging
+import viper.silver.ast.utility.chopper.PluginAwareChopper
 
 /**
  * Common functionality to implement a command-line verifier for Viper.  This trait
@@ -264,13 +266,21 @@ trait SilFrontend extends DefaultFrontend {
     def filter(input: Program): Result[Program] = {
       plugins.beforeMethodFilter(input) match {
         case Some(inputPlugin) =>
-          // Filter methods according to command-line arguments.
-          val verifyMethods =
-            if (config != null && config.methods() != ":all") Seq("methods", config.methods())
-            else inputPlugin.methods map (_.name)
-
-          val methods = inputPlugin.methods filter (m => verifyMethods.contains(m.name))
-          val program = Program(inputPlugin.domains, inputPlugin.fields, inputPlugin.functions, inputPlugin.predicates, methods, inputPlugin.extensions)(inputPlugin.pos, inputPlugin.info, inputPlugin.errT)
+          val program = config.select.toOption match {
+            case Some(names) =>
+              val namesSet = names.split(",").toSet
+              val chopped = PluginAwareChopper.chop(inputPlugin)(Some {
+                case m if namesSet.contains(m.name) => true
+                case _ => false
+              }, Some(1))
+              if (chopped.isEmpty) {
+                reporter report WarningsDuringTypechecking(Seq(TypecheckerWarning("No members were selected.", inputPlugin.pos)))
+                Program(Seq(), Seq(), Seq(), Seq(), Seq(), Seq())(inputPlugin.pos, inputPlugin.info, inputPlugin.errT)
+              } else {
+                chopped.head
+              }
+            case _ => inputPlugin
+          }
 
           plugins.beforeVerify(program) match {
             case Some(programPlugin) => Succ(programPlugin)

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

@@ -19,6 +19,7 @@ import fastparse._
 import viper.silver.frontend.{DefaultStates, ViperPAstProvider}
 import viper.silver.logger.SilentLogger
 import viper.silver.parser.FastParserCompanion.whitespace
+import viper.silver.plugin.standard.termination.TerminationPluginConstants.WellFoundedOrderDomainName
 import viper.silver.reporter.{Entity, NoopReporter, WarningsDuringTypechecking}
 
 import scala.annotation.unused
@@ -118,7 +119,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
       if (!(c.idnref.name == "decreases" || c.idnref.name == "bounded"))
         return false
       c.funcDecl match {
-        case Some(df: PDomainFunction) => df.domain.idndef.name == "WellFoundedOrder"
+        case Some(df: PDomainFunction) => df.domain.idndef.name == WellFoundedOrderDomainName
         case _ => false
       }
     }
@@ -169,31 +170,31 @@ 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(WellFoundedOrderDomainName))
         Some(name.substring(0, name.length - 16))
       else
         None
       val wronglyConstrainedTypes = d.axioms.flatMap(a => constrainsWellfoundednessUnexpectedly(a, typeName))
       reporter.report(WarningsDuringTypechecking(wronglyConstrainedTypes.map(t =>
-        TypecheckerWarning(s"Domain ${d.idndef.name} constrains well-foundedness functions for type ${t} and should be named <Type>WellFoundedOrder instead.", d.pos._1))))
+        TypecheckerWarning(s"Domain ${d.idndef.name} constrains well-foundedness functions for type ${t} and should be named <Type>${WellFoundedOrderDomainName} instead.", d.pos._1))))
     }
 
-    val predImport = if (usesPredicate && !presentDomains.contains("PredicateInstancesWellFoundedOrder")) Some("import <decreases/predicate_instance.vpr>") else None
+    val predImport = if (usesPredicate && !presentDomains.contains(s"PredicateInstances${WellFoundedOrderDomainName}")) Some("import <decreases/predicate_instance.vpr>") else None
     val importStmts = (allClauseTypes flatMap {
-      case TypeHelper.Int if !presentDomains.contains("IntWellFoundedOrder") => Some("import <decreases/int.vpr>")
-      case TypeHelper.Ref if !presentDomains.contains("RefWellFoundedOrder") => Some("import <decreases/ref.vpr>")
-      case TypeHelper.Bool if !presentDomains.contains("BoolWellFoundedOrder") => Some("import <decreases/bool.vpr>")
-      case TypeHelper.Perm if !presentDomains.contains("RationalWellFoundedOrder") && !presentDomains.contains("PermWellFoundedOrder") => Some("import <decreases/perm.vpr>")
-      case _: PMultisetType if !presentDomains.contains("MultiSetWellFoundedOrder") => Some("import <decreases/multiset.vpr>")
-      case _: PSeqType if !presentDomains.contains("SeqWellFoundedOrder") => Some("import <decreases/seq.vpr>")
-      case _: PSetType if !presentDomains.contains("SetWellFoundedOrder") => Some("import <decreases/set.vpr>")
-      case _ if !presentDomains.contains("WellFoundedOrder") => Some("import <decreases/declaration.vpr>")
+      case TypeHelper.Int if !presentDomains.contains(s"Int${WellFoundedOrderDomainName}") => Some("import <decreases/int.vpr>")
+      case TypeHelper.Ref if !presentDomains.contains(s"Ref${WellFoundedOrderDomainName}") => Some("import <decreases/ref.vpr>")
+      case TypeHelper.Bool if !presentDomains.contains(s"Bool${WellFoundedOrderDomainName}") => Some("import <decreases/bool.vpr>")
+      case TypeHelper.Perm if !presentDomains.contains(s"Rational${WellFoundedOrderDomainName}") && !presentDomains.contains(s"Perm${WellFoundedOrderDomainName}") => Some("import <decreases/perm.vpr>")
+      case _: PMultisetType if !presentDomains.contains(s"MultiSet${WellFoundedOrderDomainName}") => Some("import <decreases/multiset.vpr>")
+      case _: PSeqType if !presentDomains.contains(s"Seq${WellFoundedOrderDomainName}") => Some("import <decreases/seq.vpr>")
+      case _: PSetType if !presentDomains.contains(s"Set${WellFoundedOrderDomainName}") => Some("import <decreases/set.vpr>")
+      case _ if !presentDomains.contains(WellFoundedOrderDomainName) => Some("import <decreases/declaration.vpr>")
       case _ => None
     }) ++ predImport.toSet
     if (importStmts.nonEmpty) {
       val importOnlyProgram = importStmts.mkString("\n")
       val importPProgram = PAstProvider.generateViperPAst(importOnlyProgram).get.filterMembers(_.isInstanceOf[PDomain])
-      val inputFiltered = input.filterMembers(m => !(m.isInstanceOf[PDomain] && m.asInstanceOf[PDomain].idndef.name == "WellFoundedOrder"))
+      val inputFiltered = input.filterMembers(m => !(m.isInstanceOf[PDomain] && m.asInstanceOf[PDomain].idndef.name == WellFoundedOrderDomainName))
       val mergedProgram = PProgram(inputFiltered.imported :+ importPProgram, inputFiltered.members)(input.pos, input.localErrors, input.offsets, input.rawProgram)
       super.beforeTranslate(mergedProgram)
     } else {
@@ -411,4 +412,8 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
     case Unfolding(_, exp) => Seq(exp)
     case CurrentPerm(_) => Nil
   })
+}
+
+object TerminationPluginConstants {
+  val WellFoundedOrderDomainName = "WellFoundedOrder"
 }