transition system language API

regression/smv/define/define2.desc

@@ -1,7 +1,7 @@
 CORE
 define2.smv
 
-^file .* line 6: variable `x' already declared.*$
+^file .* line 6: identifier x already used as variable$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/define/define3.desc

@@ -1,7 +1,7 @@
 CORE
 define3.smv
 
-^file .* line 6: variable x already declared, at file .* line 3$
+^file .* line 6: identifier x already used as define$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/enums/name_collision1.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 name_collision1.smv
 
-^EXIT=0$
+^file .* line 6: identifier red already used as enum$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This crashes.

regression/smv/enums/name_collision2.desc

@@ -1,7 +1,7 @@
 CORE
 name_collision2.smv
 
-^file .* line 8: enum red already declared, at file .* line 3$
+^file .* line 8: identifier red already used as variable$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/enums/name_collision3.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 name_collision3.smv
 
-^EXIT=0$
+^file .* line 8: identifier red already used as enum$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This crashes.

regression/smv/modules/parameters2.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 parameters2.smv
 
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This yields a type-checking error.

regression/smv/var/already_declared1.desc

@@ -1,7 +1,7 @@
 CORE
 already_declared1.smv
 
-^file .* line 6: variable x already declared, at file .* line 3$
+^file .* line 6: identifier x already used as variable$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/var/already_declared2.desc

@@ -1,7 +1,7 @@
 CORE
 already_declared2.smv
 
-^file .* line 6: variable x already declared, at file .* line 3$
+^file .* line 6: identifier x already used as define$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/var/already_declared3.desc

@@ -1,7 +1,7 @@
 CORE
 already_declared3.smv
 
-^file .* line 8: variable x already declared, at file .* line 5$
+^file .* line 8: identifier x already used as variable$
 ^EXIT=2$
 ^SIGNAL=0$
 --

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,110 @@
+/*******************************************************************\
+
+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

@@ -24,7 +24,7 @@ class smv_parse_treet
   struct modulet
   {
     irep_idt name, base_name;
-    std::list<irep_idt> parameters;
+    std::vector<irep_idt> parameters;
 
     struct elementt
     {