Use EBMC language API

regression/verilog/preprocessor/unknown_directive.desc

@@ -2,7 +2,6 @@ CORE
 unknown_directive.v
 --preprocess
 ^file unknown_directive\.v line 1: unknown preprocessor directive "something"$
-^PREPROCESSING FAILED$
 ^EXIT=1$
 ^SIGNAL=0$
 --

src/ebmc/Makefile

@@ -13,6 +13,7 @@ SRC = \
       diatest.cpp \
       dimacs_writer.cpp \
       ebmc_base.cpp \
+      ebmc_language.cpp \
       ebmc_language_file.cpp \
       ebmc_languages.cpp \
       ebmc_parse_options.cpp \

src/ebmc/build_transition_system.cpp

@@ -30,36 +30,29 @@ Author: Daniel Kroening, [email protected]
 #include <fstream>
 #include <iostream>
 
-int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
+void preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
 {
   messaget message(message_handler);
 
   if(cmdline.args.size() != 1)
-  {
-    message.error() << "please give exactly one file to preprocess"
-                    << messaget::eom;
-    return 1;
-  }
+    throw ebmc_errort{}.with_exit_code(1)
+      << "please give exactly one file to preprocess";
 
   const auto &filename = cmdline.args.front();
   std::ifstream infile(widen_if_needed(filename));
 
   if(!infile)
-  {
-    message.error() << "failed to open input file `" << filename << "'"
-                    << messaget::eom;
-    return 1;
-  }
+    throw ebmc_errort{}.with_exit_code(1)
+      << "failed to open input file `" << filename << "'";
 
   auto language = get_language_from_filename(filename);
 
   if(language == nullptr)
   {
     source_locationt location;
     location.set_file(filename);
-    message.error().source_location = location;
-    message.error() << "failed to figure out type of file" << messaget::eom;
-    return 1;
+    throw ebmc_errort{}.with_location(location).with_exit_code(1)
+      << "failed to figure out type of file";
   }
 
   optionst options;
@@ -77,12 +70,7 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
   language->set_language_options(options, message_handler);
 
   if(language->preprocess(infile, filename, std::cout, message_handler))
-  {
-    message.error() << "PREPROCESSING FAILED" << messaget::eom;
-    return 1;
-  }
-
-  return 0;
+    throw ebmc_errort{}.with_exit_code(1);
 }
 
 static bool parse(
@@ -211,9 +199,6 @@ int get_transition_system(
 {
   messaget message(message_handler);
 
-  if(cmdline.isset("preprocess"))
-    return preprocess(cmdline, message_handler);
-
   //
   // parsing
   //
@@ -349,3 +334,40 @@ int show_symbol_table(
   return get_transition_system(
     cmdline, message_handler, dummy_transition_system);
 }
+
+std::optional<transition_systemt> ebmc_languagest::transition_system()
+{
+  if(cmdline.isset("preprocess"))
+  {
+    preprocess(cmdline, message_handler);
+    return {};
+  }
+
+  if(cmdline.isset("show-parse"))
+  {
+    show_parse(cmdline, message_handler);
+    return {};
+  }
+
+  if(
+    cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
+    cmdline.isset("json-modules"))
+  {
+    show_modules(cmdline, message_handler);
+    return {};
+  }
+
+  if(cmdline.isset("show-module-hierarchy"))
+  {
+    show_module_hierarchy(cmdline, message_handler);
+    return {};
+  }
+
+  if(cmdline.isset("show-symbol-table"))
+  {
+    show_symbol_table(cmdline, message_handler);
+    return {};
+  }
+
+  return get_transition_system(cmdline, message_handler);
+}

src/ebmc/build_transition_system.h

@@ -9,16 +9,25 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_EBMC_BUILD_TRANSITION_SYSTEM_H
 #define CPROVER_EBMC_BUILD_TRANSITION_SYSTEM_H
 
-class cmdlinet;
-class message_handlert;
-class transition_systemt;
+#include "ebmc_language.h"
 
 transition_systemt get_transition_system(const cmdlinet &, message_handlert &);
 
-int preprocess(const cmdlinet &, message_handlert &);
+void preprocess(const cmdlinet &, message_handlert &);
 int show_parse(const cmdlinet &, message_handlert &);
 int show_modules(const cmdlinet &, message_handlert &);
 int show_module_hierarchy(const cmdlinet &, message_handlert &);
 int show_symbol_table(const cmdlinet &, message_handlert &);
 
+class ebmc_languagest : public ebmc_languaget
+{
+public:
+  ebmc_languagest(cmdlinet &_cmdline, message_handlert &_message_handler)
+    : ebmc_languaget{_cmdline, _message_handler}
+  {
+  }
+
+  std::optional<transition_systemt> transition_system() override;
+};
+
 #endif // CPROVER_EBMC_BUILD_TRANSITION_SYSTEM_H

src/ebmc/ebmc_language.cpp

@@ -0,0 +1,13 @@
+/*******************************************************************\
+
+Module: Abstract interface to support a modeling language
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "ebmc_language.h"
+
+ebmc_languaget::~ebmc_languaget()
+{
+}

src/ebmc/ebmc_language.h

@@ -0,0 +1,42 @@
+/*******************************************************************\
+
+Module: Abstract interface to support a modeling language
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Abstract interface to support a modeling language
+
+#ifndef EBMC_LANGUAGE_H
+#define EBMC_LANGUAGE_H
+
+#include <iosfwd>
+#include <optional>
+
+class cmdlinet;
+class message_handlert;
+class transition_systemt;
+
+class ebmc_languaget
+{
+public:
+  // constructor / destructor
+  ebmc_languaget(cmdlinet &_cmdline, message_handlert &_message_handler)
+    : cmdline(_cmdline), message_handler(_message_handler)
+  {
+  }
+
+  virtual ~ebmc_languaget();
+
+  /// Produce the transition system, and return it;
+  /// returns {} when diagnostic output was produced instead.
+  virtual std::optional<transition_systemt> transition_system() = 0;
+
+protected:
+  cmdlinet &cmdline;
+  message_handlert &message_handler;
+};
+
+#endif // EBMC_LANGUAGE_H

src/ebmc/ebmc_parse_options.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include "diatest.h"
 #include "ebmc_base.h"
 #include "ebmc_error.h"
+#include "ebmc_language.h"
 #include "ebmc_version.h"
 #include "format_hooks.h"
 #include "instrument_buechi.h"
@@ -108,23 +109,6 @@ int ebmc_parse_optionst::doit()
       return 0;
     }
 
-    if(cmdline.isset("preprocess"))
-      return preprocess(cmdline, ui_message_handler);
-
-    if(cmdline.isset("show-parse"))
-      return show_parse(cmdline, ui_message_handler);
-
-    if(
-      cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
-      cmdline.isset("json-modules"))
-      return show_modules(cmdline, ui_message_handler);
-
-    if(cmdline.isset("show-module-hierarchy"))
-      return show_module_hierarchy(cmdline, ui_message_handler);
-
-    if(cmdline.isset("show-symbol-table"))
-      return show_symbol_table(cmdline, ui_message_handler);
-
     if(cmdline.isset("coverage"))
     {
       throw ebmc_errort() << "This option is currently disabled";
@@ -140,18 +124,6 @@ int ebmc_parse_optionst::doit()
 #endif
     }
 
-    if(cmdline.isset("random-traces"))
-      return random_traces(cmdline, ui_message_handler);
-
-    if(cmdline.isset("random-trace") || cmdline.isset("random-waveform"))
-      return random_trace(cmdline, ui_message_handler);
-
-    if(cmdline.isset("neural-liveness"))
-      return do_neural_liveness(cmdline, ui_message_handler);
-
-    if(cmdline.isset("ranking-function"))
-      return do_ranking_function(cmdline, ui_message_handler);
-
     if(cmdline.isset("interpolation-word"))
     {
       throw ebmc_errort() << "This option is currently disabled";
@@ -208,7 +180,28 @@ int ebmc_parse_optionst::doit()
     }
 
     // get the transition system
-    auto transition_system = get_transition_system(cmdline, ui_message_handler);
+    ebmc_languagest ebmc_languages{cmdline, ui_message_handler};
+
+    auto transition_system_opt = ebmc_languages.transition_system();
+
+    // Did we produce diagnostics instead?
+    if(!transition_system_opt.has_value())
+      return 0;
+
+    auto &transition_system = transition_system_opt.value();
+
+    if(cmdline.isset("random-traces"))
+      return random_traces(transition_system, cmdline, ui_message_handler);
+
+    if(cmdline.isset("random-trace") || cmdline.isset("random-waveform"))
+      return random_trace(transition_system, cmdline, ui_message_handler);
+
+    if(cmdline.isset("neural-liveness"))
+      return do_neural_liveness(transition_system, cmdline, ui_message_handler);
+
+    if(cmdline.isset("ranking-function"))
+      return do_ranking_function(
+        transition_system, cmdline, ui_message_handler);
 
     // get the properties
     auto properties = ebmc_propertiest::from_command_line(

src/ebmc/neural_liveness.cpp

@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
 #include <temporal-logic/temporal_expr.h>
 #include <verilog/sva_expr.h>
 
-#include "build_transition_system.h"
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "live_signal.h"
@@ -42,10 +41,14 @@ Author: Daniel Kroening, [email protected]
 class neural_livenesst
 {
 public:
-  neural_livenesst(const cmdlinet &_cmdline, message_handlert &_message_handler)
+  neural_livenesst(
+    transition_systemt &_transition_system,
+    const cmdlinet &_cmdline,
+    message_handlert &_message_handler)
     : cmdline(_cmdline),
       message(_message_handler),
-      solver_factory(ebmc_solver_factory(_cmdline))
+      solver_factory(ebmc_solver_factory(_cmdline)),
+      transition_system(_transition_system)
   {
   }
 
@@ -55,7 +58,7 @@ class neural_livenesst
   const cmdlinet &cmdline;
   messaget message;
   ebmc_solver_factoryt solver_factory;
-  transition_systemt transition_system;
+  transition_systemt &transition_system;
   ebmc_propertiest properties;
 
   int show_traces();
@@ -75,9 +78,6 @@ int neural_livenesst::operator()()
   if(!cmdline.isset("neural-engine"))
     throw ebmc_errort() << "give a neural engine";
 
-  transition_system =
-    get_transition_system(cmdline, message.get_message_handler());
-
   // Get the properties
   properties = ebmc_propertiest::from_command_line(
     cmdline, transition_system, message.get_message_handler());
@@ -127,9 +127,6 @@ int neural_livenesst::operator()()
 
 int neural_livenesst::show_traces()
 {
-  transition_system =
-    get_transition_system(cmdline, message.get_message_handler());
-
   properties = ebmc_propertiest::from_command_line(
     cmdline, transition_system, message.get_message_handler());
 
@@ -317,8 +314,9 @@ tvt neural_livenesst::verify(
 }
 
 int do_neural_liveness(
+  transition_systemt &transition_system,
   const cmdlinet &cmdline,
-  ui_message_handlert &ui_message_handler)
+  message_handlert &message_handler)
 {
-  return neural_livenesst(cmdline, ui_message_handler)();
+  return neural_livenesst{transition_system, cmdline, message_handler}();
 }

src/ebmc/neural_liveness.h

@@ -9,9 +9,13 @@ Author: Daniel Kroening, [email protected]
 #ifndef EBMC_NEURAL_LIVENESS_H
 #define EBMC_NEURAL_LIVENESS_H
 
-#include <util/cmdline.h>
-#include <util/ui_message.h>
+class cmdlinet;
+class message_handlert;
+class transition_systemt;
 
-int do_neural_liveness(const cmdlinet &, ui_message_handlert &);
+int do_neural_liveness(
+  transition_systemt &,
+  const cmdlinet &,
+  message_handlert &);
 
 #endif // EBMC_NEURAL_LIVENESS_H