Integrate ST parser into CBMC executable

Includes a basic ST language interface (although without any typechecking yet) as well as modifications to some Makefiles and cbmc_languages.cpp. Use the --show-parse-tree option when parsing a .awl file to see the project's output.

Author: MatWise

src/Makefile

@@ -20,6 +20,7 @@ DIRS = analyses \
        memory-analyzer \
        pointer-analysis \
        solvers \
+       structured-text \
        symtab2gb \
        util \
        xmllang \
@@ -60,7 +61,7 @@ cpp.dir: ansi-c.dir linking.dir
 
 languages: util.dir langapi.dir \
            cpp.dir ansi-c.dir xmllang.dir assembler.dir \
-           jsil.dir json.dir json-symtab-language.dir
+           jsil.dir json.dir json-symtab-language.dir structured-text.dir
 
 solvers.dir: util.dir
 

src/cbmc/Makefile

@@ -41,6 +41,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../solvers/solvers$(LIBEXT) \
+      ../structured-text/structured-text$(LIBEXT) \
       ../util/util$(LIBEXT) \
       ../json/json$(LIBEXT)
 

src/cbmc/cbmc_languages.cpp

@@ -16,14 +16,16 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
 #include <json-symtab-language/json_symtab_language.h>
+#include <structured-text/structured_text_language.h>
 
 #ifdef HAVE_JSIL
-#include <jsil/jsil_language.h>
+#  include <jsil/jsil_language.h>
 #endif
 
 void cbmc_parse_optionst::register_languages()
 {
   register_language(new_ansi_c_language);
+  register_language(new_structured_text_language);
   register_language(new_cpp_language);
   register_language(new_json_symtab_language);
 

src/cbmc/module_dependencies.txt

@@ -13,5 +13,6 @@ langapi # should go away
 linking
 pointer-analysis
 solvers
+structured-text
 xmllang
 util

src/structured-text/Makefile

@@ -0,0 +1,53 @@
+SRC = converters/convert_int_value.cpp \
+      converters/convert_real_value.cpp \
+      converters/convert_string_value.cpp \
+      converters/expr2structured_text.cpp \
+      structured_text_language.cpp \
+      structured_text_lex.yy.cpp \
+      structured_text_parse_tree.cpp \
+      structured_text_parser.cpp \
+      structured_text_typecheck.cpp \
+      structured_text_y.tab.cpp \
+      # Empty last line
+
+INCLUDES= -I ..
+
+include ../config.inc
+include ../common
+
+CLEANFILES = stl$(LIBEXT) \
+  structured_text_y.tab.h structured_text_y.tab.cpp \
+  structured_text_lex.yy.cpp structured_text_y.tab.cpp.output \
+  structured_text_y.output
+
+all: structured-text$(LIBEXT)
+
+###############################################################################
+
+structured_text_y.tab.cpp: parser.y
+	$(YACC) $(YFLAGS) $$flags -pyystructured_text -d parser.y -o $@
+
+structured_text_y.tab.h: structured_text_y.tab.cpp
+	if [ -e structured_text_y.tab.hpp ] ; then mv structured_text_y.tab.hpp \
+	structured_text_y.tab.h ; else mv structured_text_y.tab.cpp.h \
+	structured_text_y.tab.h ; fi
+
+structured_text_lex.yy.cpp: scanner.l
+	$(LEX) -Pyystructured_text -o$@ scanner.l
+
+# extra dependencies
+structured_text_y.tab$(OBJEXT): structured_text_y.tab.cpp \
+  structured_text_y.tab.h
+structured_text_lex.yy$(OBJEXT): structured_text_y.tab.cpp \
+  structured_text_lex.yy.cpp structured_text_y.tab.h
+
+###############################################################################
+
+generated_files: structured_text_y.tab.cpp structured_text_lex.yy.cpp \
+  structured_text_y.tab.h
+
+###############################################################################
+
+structured-text$(LIBEXT): $(OBJ)
+	$(LINKLIB)
+

src/structured-text/converters/expr2structured_text.cpp

@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module: Conversion from Expression or Type to Structured Text
+
+Author: Matthias Weiss, [email protected]
+
+\*******************************************************************/
+
+#include "expr2structured_text.h"
+#include <util/symbol.h>
+
+std::string expr2stl(const exprt &expr)
+{
+  // TODO: Implement.
+  return "";
+}
+
+std::string type2stl(const typet &type)
+{
+  // TODO: Implement.
+  return "";
+}
+
+std::string type2stl(const typet &type, const std::string &identifier)
+{
+  // TODO: Implement.
+  return "";
+}

src/structured-text/converters/expr2structured_text.h

@@ -0,0 +1,24 @@
+/*******************************************************************\
+
+Module: Conversion from Expression or Type to Structured Text
+
+Author: Matthias Weiss, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_STRUCTURED_TEXT_CONVERTERS_EXPR2STRUCTURED_TEXT_H
+#define CPROVER_STRUCTURED_TEXT_CONVERTERS_EXPR2STRUCTURED_TEXT_H
+
+#include <string>
+
+class exprt;
+class namespacet;
+class typet;
+
+std::string expr2stl(const exprt &expr);
+
+std::string type2stl(const typet &type);
+
+std::string type2stl(const typet &type, const std::string &identifier);
+
+#endif // CPROVER_STRUCTURED_TEXT_CONVERTERS_EXPR2STRUCTURED_TEXT_H

src/structured-text/structured_text_language.cpp

@@ -0,0 +1,131 @@
+/*******************************************************************\
+
+Module: Structured Text Language Interface
+
+Author: Matthias Weiss, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Structured Text Language Interface
+
+#include "structured_text_language.h"
+#include "converters/expr2structured_text.h"
+#include "structured_text_parser.h"
+#include "structured_text_typecheck.h"
+
+#include <linking/linking.h>
+#include <linking/remove_internal_symbols.h>
+#include <util/get_base_name.h>
+
+bool structured_text_languaget::generate_support_functions(
+  symbol_tablet &symbol_table)
+{
+  return false;
+}
+
+bool structured_text_languaget::typecheck(
+  symbol_tablet &symbol_table,
+  const std::string &module,
+  const bool keep_file_local)
+{
+  symbol_tablet new_symbol_table;
+
+  if(structured_text_typecheck(
+       parse_tree, new_symbol_table, module, get_message_handler()))
+  {
+    return true;
+  }
+
+  remove_internal_symbols(
+    new_symbol_table, this->get_message_handler(), keep_file_local);
+
+  if(linking(symbol_table, new_symbol_table, get_message_handler()))
+    return true;
+
+  return false;
+}
+
+bool structured_text_languaget::parse(
+  std::istream &instream,
+  const std::string &path)
+{
+  structured_text_parser.clear();
+  parse_path = path;
+  structured_text_parser.set_line_no(0);
+  structured_text_parser.set_file(path);
+  structured_text_parser.in = &instream;
+  structured_text_scanner_init();
+  bool result = structured_text_parser.parse();
+
+  // store result
+  structured_text_parser.swap_tree(parse_tree);
+
+  return result;
+}
+
+void structured_text_languaget::show_parse(std::ostream &out)
+{
+  parse_tree.output(out);
+}
+
+bool structured_text_languaget::from_expr(
+  const exprt &expr,
+  std::string &code,
+  const namespacet &ns)
+{
+  code = expr2stl(expr);
+  return false;
+}
+
+bool structured_text_languaget::from_type(
+  const typet &type,
+  std::string &code,
+  const namespacet &ns)
+{
+  code = type2stl(type);
+  return false;
+}
+
+bool structured_text_languaget::type_to_name(
+  const typet &type,
+  std::string &name,
+  const namespacet &ns)
+{
+  return from_type(type, name, ns);
+}
+
+bool structured_text_languaget::to_expr(
+  const std::string &code,
+  const std::string &module,
+  exprt &expr,
+  const namespacet &ns)
+{
+  // unused parameters
+  (void)code;
+  (void)module;
+  (void)expr;
+  (void)ns;
+
+  return true;
+}
+
+structured_text_languaget::~structured_text_languaget()
+{
+  parse_tree.clear();
+}
+
+void structured_text_languaget::modules_provided(std::set<std::string> &modules)
+{
+  modules.insert(get_base_name(parse_path, true));
+}
+
+std::set<std::string> structured_text_languaget::extensions() const
+{
+  return {"awl"};
+}
+
+std::unique_ptr<languaget> new_structured_text_language()
+{
+  return util_make_unique<structured_text_languaget>();
+}