Merge pull request #732 from viperproject/meilers_term_plugin_deactive_flag

SilFrontend API for Viper frontend usage

Author: marcoeilers

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

@@ -82,6 +82,13 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     hidden = true
   )
 
+  val disableDefaultPlugins = opt[Boolean]("disableDefaultPlugins",
+    descr = "Deactivate all default plugins.",
+    default = Some(false),
+    noshort = true,
+    hidden = true
+  )
+
   val plugin = opt[String]("plugin",
     descr = "Load plugin(s) with given class name(s). Several plugins can be separated by ':'. " +
       "The fully qualified class name of the plugin should be specified.",

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

@@ -52,6 +52,21 @@ trait SilFrontend extends DefaultFrontend {
     }
   }
 
+  def resetPlugins(): Unit = {
+    val pluginsArg: Option[String] = if (_config != null) {
+      // concat defined plugins and default plugins
+      val list = _config.plugin.toOption ++ (if (_config.disableDefaultPlugins()) Seq() else defaultPlugins)
+      if (list.isEmpty) {
+        None
+      } else {
+        Some(list.mkString(":"))
+      }
+    } else {
+      None
+    }
+    _plugins = SilverPluginManager(pluginsArg)(reporter, logger, _config, fp)
+  }
+
   /**
    * Create the verifier. The full command is parsed for debugging purposes only,
    * since the command line arguments will be passed later on via
@@ -184,13 +199,7 @@ trait SilFrontend extends DefaultFrontend {
     super.reset(input)
 
     if(_config != null) {
-
-      // concat defined plugins and default plugins
-      val pluginsArg: Option[String] = {
-        val list = _config.plugin.toOption ++ defaultPlugins
-        if (list.isEmpty) { None } else { Some(list.mkString(":")) }
-      }
-      _plugins = SilverPluginManager(pluginsArg)(reporter, logger, _config, fp)
+      resetPlugins()
     }
   }
 

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

@@ -0,0 +1,67 @@
+package viper.silver.frontend
+
+import viper.silver.ast.Program
+import viper.silver.verifier.VerificationResult
+
+
+/**
+  * Trait that can be mixed into SilFrontends to make them easily usable by actual Viper frontends that do not use
+  * Viper's parser, type checker, etc., but instead directly consistency-check and verify a Viper AST.
+  * Compared to working directly with an instance of [[viper.silver.verifier.Verifier]], SilFrontend manages plugins
+  * automatically.
+  * To use it:
+  * - create an instance f of a specific SilFrontend with ViperFrontendAPI mixed in
+  * - call f.initialize(args), where args are the command line arguments without any file name.
+  * - (potentially repeatedly) call f.verify(p), where p is the program to verify
+  * - call f.stop() when done
+  * Plugin usage must be managed via command line arguments.
+  * Existing implementations are SiliconFrontendAPI and CarbonFrontendAPI
+  */
+trait ViperFrontendAPI extends SilFrontend {
+
+  private var initialized = false
+  override val phases: Seq[Phase] = Seq(ConsistencyCheck, Verification)
+  val dummyInputFilename = "dummy-file-to-prevent-cli-parser-from-complaining-about-missing-file-name.silver"
+
+  def initialize(args: Seq[String]): Unit = {
+    // create verifier
+    // parse args on frontend, set on verifier
+    val v = createVerifier(args.mkString(" "))
+    setVerifier(v)
+    _verifier = Some(v)
+    parseCommandLine(args :+ "--ignoreFile" :+ dummyInputFilename)
+    resetPlugins()
+    initialized = true
+  }
+
+  protected def setStartingState() = {
+    _state = DefaultStates.ConsistencyCheck
+  }
+
+  def verify(p: Program): VerificationResult = {
+    if (!initialized)
+      throw new IllegalStateException("Not initialized")
+    setStartingState()
+    _program = Some(p)
+    runAllPhases()
+    result
+  }
+
+  def stop(): Unit = {
+    if (!initialized)
+      throw new IllegalStateException("Not initialized")
+    _verifier.foreach(_.stop())
+  }
+
+}
+
+/**
+  * Version of ViperFrontendAPI that skips the consistency check phase.
+  */
+trait MinimalViperFrontendAPI extends ViperFrontendAPI {
+  override val phases: Seq[Phase] = Seq(Verification)
+
+  override protected def setStartingState() = {
+    _state = DefaultStates.ConsistencyCheck
+  }
+}

src/main/scala/viper/silver/verifier/VerificationError.scala

@@ -93,7 +93,7 @@ case class MapEntry(options: Map[Seq[ValueEntry], ValueEntry], default: ValueEnt
         val indices = args.map(_.get._1)
         // We expect the arguments in the order 0, 1, ..., n-1; if we get something else, reject.
         // TODO: Find out if this order is always guaranteed,
-        if (indices != (0 until indices.size))
+        if (indices != (0 until indices.size).map(_.toString))
           None
         else
           Some(args.map(_.get._2))