Merge pull request #1418 from diffblue/ebmc_language_api

ebmc language interface implementation for SMV

Author: tautschnig

src/ebmc/build_transition_system.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #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 <trans-word-level/show_modules.h>
 
@@ -335,39 +336,76 @@ int show_symbol_table(
     cmdline, message_handler, dummy_transition_system);
 }
 
-std::optional<transition_systemt> ebmc_languagest::transition_system()
+static std::set<std::string> file_extensions(const cmdlinet::argst &args)
 {
-  if(cmdline.isset("preprocess"))
-  {
-    preprocess(cmdline, message_handler);
-    return {};
-  }
+  std::set<std::string> result;
 
-  if(cmdline.isset("show-parse"))
+  for(auto &arg : args)
   {
-    show_parse(cmdline, message_handler);
-    return {};
+    std::size_t ext_pos = arg.rfind('.');
+
+    if(ext_pos != std::string::npos)
+    {
+      auto ext = std::string(arg, ext_pos + 1, std::string::npos);
+      result.insert(ext);
+    }
   }
 
-  if(
-    cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
-    cmdline.isset("json-modules"))
+  return result;
+}
+
+std::optional<transition_systemt> ebmc_languagest::transition_system()
+{
+  auto extensions = file_extensions(cmdline.args);
+  auto ext_used = [&extensions](const char *ext)
+  { return extensions.find(ext) != extensions.end(); };
+
+  bool have_smv = ext_used("smv");
+  bool have_verilog = ext_used("v") || ext_used("sv");
+
+  if(have_smv && have_verilog)
   {
-    show_modules(cmdline, message_handler);
-    return {};
+    throw ebmc_errort{} << "no support for mixed-language models";
   }
 
-  if(cmdline.isset("show-module-hierarchy"))
+  if(have_smv)
   {
-    show_module_hierarchy(cmdline, message_handler);
-    return {};
+    return smv_ebmc_languaget{cmdline, message_handler}.transition_system();
   }
-
-  if(cmdline.isset("show-symbol-table"))
+  else
   {
-    show_symbol_table(cmdline, message_handler);
-    return {};
+    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);
   }
-
-  return get_transition_system(cmdline, message_handler);
 }

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,109 @@
+/*******************************************************************\
+
+Module: SMV Language Interface
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \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, [email protected]
+
+\*******************************************************************/
+
+/// \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

src/smvlang/smv_parse_tree.h

@@ -20,6 +20,7 @@ class smv_parse_treet
 {
 public:
   smv_parse_treet() = default;
+  smv_parse_treet(smv_parse_treet &&) = default;
 
   // don't copy, contains pointers
   smv_parse_treet(const smv_parse_treet &) = delete;