ebmc language implementation for SMV

This adds an implementation of the ebmc_languaget interface for SMV.

Author: kroening

src/smvlang/Makefile

@@ -1,4 +1,5 @@
-SRC = smv_expr.cpp \
+SRC = smv_ebmc_language.cpp \
+      smv_expr.cpp \
       smv_language.cpp \
       smv_parser.cpp \
       smv_typecheck.cpp \

src/smvlang/smv_ebmc_language.cpp

@@ -0,0 +1,110 @@
+/*******************************************************************\
+
+Module: SMV Language Interface
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// SMV Language Interface
+
+#include "smv_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 "smv_parser.h"
+#include "smv_typecheck.h"
+
+#include <fstream>
+#include <iostream>
+
+std::string smv_file_name(const cmdlinet &cmdline)
+{
+  if(cmdline.args.size() == 0)
+    throw ebmc_errort{} << "no file name given";
+
+  if(cmdline.args.size() >= 2)
+    throw ebmc_errort{}.with_exit_code(1) << "SMV only uses a single file";
+
+  return cmdline.args.front();
+}
+
+smv_parse_treet smv_ebmc_languaget::parse()
+{
+  smv_parsert smv_parser{message_handler};
+
+  auto file_name = smv_file_name(cmdline);
+
+  std::ifstream infile{widen_if_needed(file_name)};
+
+  if(!infile)
+    throw ebmc_errort{}.with_exit_code(1) << "failed to open " << file_name;
+
+  smv_parser.set_file(file_name);
+  smv_parser.in = &infile;
+
+  if(smv_parser.parse())
+    throw ebmc_errort{}.with_exit_code(1);
+
+  return std::move(smv_parser.parse_tree);
+}
+
+std::optional<transition_systemt> smv_ebmc_languaget::transition_system()
+{
+  if(cmdline.isset("preprocess"))
+  {
+    throw ebmc_errort{}.with_exit_code(1) << "SMV does not use preprocessing";
+  }
+
+  auto parse_tree = parse();
+
+  if(cmdline.isset("show-parse"))
+  {
+    parse_tree.show(std::cout);
+    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 {};
+  }
+
+  transition_systemt result;
+
+  if(smv_typecheck(
+       parse_tree, result.symbol_table, "smv::main", message_handler))
+  {
+    messaget message{message_handler};
+    message.error() << "CONVERSION ERROR" << messaget::eom;
+    throw ebmc_errort{}.with_exit_code(2);
+  }
+
+  if(cmdline.isset("show-symbol-table"))
+  {
+    std::cout << result.symbol_table;
+    return {};
+  }
+
+  result.main_symbol =
+    &get_module(result.symbol_table, "main", message_handler);
+
+  result.trans_expr =
+    to_trans_expr(result.main_symbol->value);
+
+  return result;
+}

src/smvlang/smv_ebmc_language.h

@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+Module: SMV Language Interface
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// SMV Language Interface
+
+#ifndef EBMC_SMV_LANGUAGE_H
+#define EBMC_SMV_LANGUAGE_H
+
+#include <ebmc/ebmc_language.h>
+
+class smv_parse_treet;
+
+class smv_ebmc_languaget : public ebmc_languaget
+{
+public:
+  smv_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:
+  smv_parse_treet parse();
+};
+
+#endif // EBMC_SMV_LANGUAGE_H