ebmc language interface implementation for Verilog

This adds an implementation of the ebmc_languaget interface for Verilog.

Author: kroening

src/verilog/verilog_ebmc_language.cpp

@@ -0,0 +1,64 @@
+/*******************************************************************\
+
+Module: Verilog Language Interface
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// Verilog Language Interface
+
+#include "verilog_ebmc_language.h"
+
+#include <util/cmdline.h>
+#include <util/get_module.h>
+#include <util/unicode.h>
+
+#include <ebmc/ebmc_error.h>
+#include <ebmc/transition_system.h>
+
+#include "verilog_parser.h"
+#include "verilog_typecheck.h"
+
+#include <fstream>
+
+verilog_parse_treet verilog_ebmc_languaget::parse()
+{
+  verilog_standardt standard;
+
+  verilog_parsert verilog_parser{standard, message_handler};
+
+  auto file_name = verilog_file_name(cmdline);
+
+  std::ifstream infile{widen_if_needed(file_name)};
+
+  if(!infile)
+    throw ebmc_errort{} << "failed to open " << file_name;
+
+  verilog_parser.set_file(file_name);
+  verilog_parser.in = &infile;
+
+  if(verilog_parser.parse())
+    throw ebmc_errort{} << "parsing has failed";
+
+  return std::move(verilog_parser.parse_tree);
+}
+
+std::optional<transition_systemt> verilog_ebmc_languaget::transition_system()
+{
+  auto parse_tree = parse();
+
+  transition_systemt result;
+
+  if(verilog_typecheck(parse_tree, result.symbol_table, "main", message_handler))
+    throw ebmc_errort{} << "typechecking has failed";
+
+  result.main_symbol =
+    &get_module(result.symbol_table, "main", message_handler);
+
+  result.trans_expr =
+    to_trans_expr(result.main_symbol->value);
+
+  return result;
+}

src/verilog/verilog_ebmc_language.h

@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+Module: Verilog Language Interface
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// SMV Language Interface
+
+#ifndef EBMC_VERILOG_LANGUAGE_H
+#define EBMC_VERILOG_LANGUAGE_H
+
+#include <ebmc/ebmc_language.h>
+
+class verilog_parse_treet;
+
+class verilog_ebmc_languaget : public ebmc_languaget
+{
+public:
+  verilog_ebmc_languaget(cmdlinet &_cmdline, message_handlert &_message_handler)
+    : ebmc_languaget(_cmdline, _message_handler)
+  {
+  }
+
+  // produce the transition system, and return it
+  std::optional<transition_systemt> transition_system() override;
+
+protected:
+  verilog_parse_treet parse();
+};
+
+#endif // EBMC_VERILOG_LANGUAGE_H