From c1a1a4d1a05f3ff21e6f088572ba499ac87772f3 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 14 Aug 2023 12:49:24 +0200 Subject: [PATCH 1/4] WIP --- .../silver/frontend/SilFrontEndConfig.scala | 7 ++++ .../viper/silver/frontend/SilFrontend.scala | 15 ++++++++ .../silver/frontend/ViperFrontendAPI.scala | 38 +++++++++++++++++++ 3 files changed, 60 insertions(+) create mode 100644 src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala diff --git a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala index 62fa07f4f..cff594043 100644 --- a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala +++ b/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.", diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala index f1e336091..8bac404cf 100644 --- a/src/main/scala/viper/silver/frontend/SilFrontend.scala +++ b/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 diff --git a/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala b/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala new file mode 100644 index 000000000..03c9a1447 --- /dev/null +++ b/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala @@ -0,0 +1,38 @@ +package viper.silver.frontend + +import viper.silver.ast.Program +import viper.silver.verifier.VerificationResult + +import java.nio.file.Paths + +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) + println("Not initialized") + setStartingState() + _program = Some(p) + runAllPhases() + result + } + +} From d78442093c12416190dd13cf91573d7b8a111ebb Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 14 Aug 2023 14:07:11 +0200 Subject: [PATCH 2/4] Some comments --- .../silver/frontend/ViperFrontendAPI.scala | 25 ++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala b/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala index 03c9a1447..cb4585d76 100644 --- a/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala +++ b/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala @@ -5,6 +5,18 @@ import viper.silver.verifier.VerificationResult import java.nio.file.Paths +/** + * 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 + * Plugin usage must be managed via command line arguments. + * Existing implementations are SiliconFrontendAPI and CarbonFrontendAPI + */ trait ViperFrontendAPI extends SilFrontend { private var initialized = false @@ -28,7 +40,7 @@ trait ViperFrontendAPI extends SilFrontend { def verify(p: Program): VerificationResult = { if (!initialized) - println("Not initialized") + throw new IllegalStateException("Not initialized") setStartingState() _program = Some(p) runAllPhases() @@ -36,3 +48,14 @@ trait ViperFrontendAPI extends SilFrontend { } } + +/** + * 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 + } +} From afaf4523a8429873c4f160713a22764162b12b21 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 15 Aug 2023 00:31:17 +0200 Subject: [PATCH 3/4] Removed duplicated code --- src/main/scala/viper/silver/frontend/SilFrontend.scala | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala index 8bac404cf..a2ee386f0 100644 --- a/src/main/scala/viper/silver/frontend/SilFrontend.scala +++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala @@ -199,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() } } From d52e42faec49614fc5e280d7960b15f8924da1de Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 16 Aug 2023 21:52:10 +0200 Subject: [PATCH 4/4] Added stop method to API, fixed random CE extraction issue --- .../scala/viper/silver/frontend/ViperFrontendAPI.scala | 8 +++++++- .../scala/viper/silver/verifier/VerificationError.scala | 2 +- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala b/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala index cb4585d76..2e2517364 100644 --- a/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala +++ b/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala @@ -3,7 +3,6 @@ package viper.silver.frontend import viper.silver.ast.Program import viper.silver.verifier.VerificationResult -import java.nio.file.Paths /** * Trait that can be mixed into SilFrontends to make them easily usable by actual Viper frontends that do not use @@ -14,6 +13,7 @@ import java.nio.file.Paths * - 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 */ @@ -47,6 +47,12 @@ trait ViperFrontendAPI extends SilFrontend { result } + def stop(): Unit = { + if (!initialized) + throw new IllegalStateException("Not initialized") + _verifier.foreach(_.stop()) + } + } /** diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala index 16180457f..67c0c66e0 100644 --- a/src/main/scala/viper/silver/verifier/VerificationError.scala +++ b/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))