ebmc language interface implementation for Verilog

This adds an implementation of the ebmc_languaget interface for Verilog.

Author: kroening

src/ebmc/build_transition_system.cpp

@@ -9,339 +9,16 @@ Author: Daniel Kroening, [email protected]
 #include "build_transition_system.h"
 
 #include <util/cmdline.h>
-#include <util/get_module.h>
 #include <util/message.h>
-#include <util/namespace.h>
-#include <util/options.h>
-#include <util/unicode.h>
 
-#include <langapi/language.h>
-#include <langapi/language_util.h>
-#include <langapi/mode.h>
 #include <smvlang/smv_ebmc_language.h>
-#include <trans-word-level/show_module_hierarchy.h>
+#include <verilog/verilog_ebmc_language.h>
 
 #include "ebmc_error.h"
-#include "ebmc_language_file.h"
-#include "ebmc_version.h"
-#include "output_file.h"
-#include "show_modules.h"
 #include "transition_system.h"
 
 #include <fstream>
-#include <iostream>
-
-void preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
-{
-  messaget message(message_handler);
-
-  if(cmdline.args.size() != 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)
-    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);
-    throw ebmc_errort{}.with_location(location).with_exit_code(1)
-      << "failed to figure out type of file";
-  }
-
-  optionst options;
-
-  // do -I
-  if(cmdline.isset('I'))
-    options.set_option("I", cmdline.get_values('I'));
-
-  options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
-
-  // do -D
-  if(cmdline.isset('D'))
-    options.set_option("defines", cmdline.get_values('D'));
-
-  language->set_language_options(options, message_handler);
-
-  if(language->preprocess(infile, filename, std::cout, message_handler))
-    throw ebmc_errort{}.with_exit_code(1);
-}
-
-static bool parse(
-  const cmdlinet &cmdline,
-  const std::string &filename,
-  ebmc_language_filest &language_files,
-  message_handlert &message_handler)
-{
-  messaget message(message_handler);
-
-  std::ifstream infile(widen_if_needed(filename));
-
-  if(!infile)
-  {
-    message.error() << "failed to open input file `" << filename << "'"
-                    << messaget::eom;
-    return true;
-  }
-
-  auto &lf = language_files.add_file(filename);
-  lf.filename = filename;
-  lf.language = get_language_from_filename(filename);
-
-  if(lf.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 true;
-  }
-
-  languaget &language = *lf.language;
-
-  optionst options;
-
-  // do -I
-  if(cmdline.isset('I'))
-    options.set_option("I", cmdline.get_values('I'));
-
-  options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
-  options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions"));
-  options.set_option("warn-implicit-nets", cmdline.isset("warn-implicit-nets"));
-
-  // do -D
-  if(cmdline.isset('D'))
-    options.set_option("defines", cmdline.get_values('D'));
-
-  // do --ignore-initial
-  if(cmdline.isset("ignore-initial"))
-    options.set_option("ignore-initial", true);
-
-  // do --initial-zero
-  if(cmdline.isset("initial-zero"))
-    options.set_option("initial-zero", true);
-
-  language.set_language_options(options, message_handler);
-
-  message.status() << "Parsing " << filename << messaget::eom;
-
-  if(language.parse(infile, filename, message_handler))
-  {
-    message.error() << "PARSING ERROR\n";
-    return true;
-  }
-
-  lf.get_modules();
-
-  return false;
-}
-
-bool parse(
-  const cmdlinet &cmdline,
-  ebmc_language_filest &language_files,
-  message_handlert &message_handler)
-{
-  for(unsigned i = 0; i < cmdline.args.size(); i++)
-  {
-    if(parse(cmdline, cmdline.args[i], language_files, message_handler))
-      return true;
-  }
-  return false;
-}
-
-bool get_main(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler,
-  transition_systemt &transition_system)
-{
-  std::string top_module;
-
-  if(cmdline.isset("module"))
-    top_module = cmdline.get_value("module");
-  else if(cmdline.isset("top"))
-    top_module = cmdline.get_value("top");
-
-  try
-  {
-    transition_system.main_symbol =
-      &get_module(transition_system.symbol_table, top_module, message_handler);
-    transition_system.trans_expr =
-      to_trans_expr(transition_system.main_symbol->value);
-  }
-
-  catch(int e)
-  {
-    return true;
-  }
-
-  return false;
-}
-
-void make_next_state(exprt &expr)
-{
-  for(auto &sub_expression : expr.operands())
-    make_next_state(sub_expression);
-
-  if(expr.id() == ID_symbol)
-    expr.id(ID_next_symbol);
-}
-
-int get_transition_system(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler,
-  transition_systemt &transition_system)
-{
-  messaget message(message_handler);
-
-  //
-  // parsing
-  //
-  ebmc_language_filest language_files;
-
-  if(parse(cmdline, language_files, message_handler))
-    return 1;
-
-  if(cmdline.isset("show-parse"))
-  {
-    language_files.show_parse(std::cout, message_handler);
-    return 0;
-  }
-
-  //
-  // type checking
-  //
-
-  message.status() << "Converting" << messaget::eom;
-
-  if(language_files.typecheck(transition_system.symbol_table, message_handler))
-  {
-    message.error() << "CONVERSION ERROR" << messaget::eom;
-    return 2;
-  }
-
-  if(cmdline.isset("show-modules"))
-  {
-    show_modulest::from_symbol_table(transition_system.symbol_table)
-      .plain_text(std::cout);
-    return 0;
-  }
-
-  if(cmdline.isset("modules-xml"))
-  {
-    auto filename = cmdline.get_value("modules-xml");
-    auto out_file = output_filet{filename};
-    show_modulest::from_symbol_table(transition_system.symbol_table)
-      .xml(out_file.stream());
-    return 0;
-  }
-
-  if(cmdline.isset("json-modules"))
-  {
-    auto out_file = output_filet{cmdline.get_value("json-modules")};
-    show_modulest::from_symbol_table(transition_system.symbol_table)
-      .json(out_file.stream());
-    return 0;
-  }
-
-  if(cmdline.isset("show-symbol-table"))
-  {
-    std::cout << transition_system.symbol_table;
-    return 0;
-  }
-
-  // get module name
-
-  if(get_main(cmdline, message_handler, transition_system))
-    return 1;
-
-  if(cmdline.isset("show-module-hierarchy"))
-  {
-    DATA_INVARIANT(
-      transition_system.main_symbol != nullptr, "must have main_symbol");
-    show_module_hierarchy(
-      transition_system.symbol_table,
-      *transition_system.main_symbol,
-      std::cout);
-    return 0;
-  }
-
-  // --reset given?
-  if(cmdline.isset("reset"))
-  {
-    namespacet ns(transition_system.symbol_table);
-    exprt reset_constraint = to_expr(
-      ns, transition_system.main_symbol->name, cmdline.get_value("reset"));
-
-    // we want the constraint to be boolean
-    reset_constraint =
-      typecast_exprt::conditional_cast(reset_constraint, bool_typet{});
-
-    // true in initial state
-    transt new_trans_expr = transition_system.trans_expr;
-    new_trans_expr.init() = and_exprt(new_trans_expr.init(), reset_constraint);
-
-    // and not anymore afterwards
-    exprt reset_next_state = reset_constraint;
-    make_next_state(reset_next_state);
-
-    new_trans_expr.trans() =
-      and_exprt(new_trans_expr.trans(), not_exprt(reset_next_state));
-    transition_system.trans_expr = new_trans_expr;
-  }
-
-  return -1; // done with the transition system
-}
-
-transition_systemt get_transition_system(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler)
-{
-  transition_systemt transition_system;
-  auto exit_code =
-    get_transition_system(cmdline, message_handler, transition_system);
-  if(exit_code != -1)
-    throw ebmc_errort().with_exit_code(exit_code);
-  return transition_system;
-}
-
-int show_parse(const cmdlinet &cmdline, message_handlert &message_handler)
-{
-  transition_systemt dummy_transition_system;
-  return get_transition_system(
-    cmdline, message_handler, dummy_transition_system);
-}
-
-int show_modules(const cmdlinet &cmdline, message_handlert &message_handler)
-{
-  transition_systemt dummy_transition_system;
-  return get_transition_system(
-    cmdline, message_handler, dummy_transition_system);
-}
-
-int show_module_hierarchy(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler)
-{
-  transition_systemt dummy_transition_system;
-  return get_transition_system(
-    cmdline, message_handler, dummy_transition_system);
-}
-
-int show_symbol_table(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler)
-{
-  transition_systemt dummy_transition_system;
-  return get_transition_system(
-    cmdline, message_handler, dummy_transition_system);
-}
+#include <set>
 
 static std::set<std::string> file_extensions(const cmdlinet::argst &args)
 {
@@ -379,40 +56,12 @@ std::optional<transition_systemt> ebmc_languagest::transition_system()
   {
     return smv_ebmc_languaget{cmdline, message_handler}.transition_system();
   }
+  else if(have_verilog)
+  {
+    return verilog_ebmc_languaget{cmdline, message_handler}.transition_system();
+  }
   else
   {
-    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);
+    throw ebmc_errort{} << "no support for given input file extensions";
   }
 }

src/verilog/Makefile

@@ -4,6 +4,7 @@ SRC = aval_bval_encoding.cpp \
       sva_expr.cpp \
       typename.cpp \
       verilog_bits.cpp \
+      verilog_ebmc_language.cpp \
       verilog_elaborate.cpp \
       verilog_elaborate_type.cpp \
       verilog_expr.cpp \