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/CMakeLists.txt

@@ -95,6 +95,7 @@ add_subdirectory(langapi)
 add_subdirectory(linking)
 add_subdirectory(pointer-analysis)
 add_subdirectory(solvers)
+add_subdirectory(structured-text)
 add_subdirectory(util)
 add_subdirectory(xmllang)
 

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/CMakeLists.txt

@@ -23,6 +23,7 @@ target_link_libraries(cbmc-lib
     linking
     pointer-analysis
     solvers
+    structured-text
     util
     xml
 )

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/CMakeLists.txt

@@ -0,0 +1,23 @@
+generic_bison(structured_text)
+generic_flex(structured_text)
+
+################################################################################
+
+
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+
+add_library(structured-text
+    ${sources}
+    ${BISON_parser_OUTPUTS}
+    ${FLEX_scanner_OUTPUTS}
+)
+
+set_source_files_properties(
+    ${sources}
+    PROPERTIES
+    OBJECT_DEPENDS "${extra_dependencies}"
+)
+
+generic_includes(structured-text)
+
+target_link_libraries(structured-text util langapi linking)

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,31 @@
+/*******************************************************************\
+
+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>
+
+/// Converts a given expression to human-readable STL code.
+/// \param expr: Expression to be converted.
+/// \param identifier: Identifier to be converted.
+/// \result String with the STL representation of the given parameters.
+std::string expr2stl(const class exprt &expr);
+
+/// Converts a given type to human-readable STL code.
+/// \param type: Type to be converted.
+/// \result String with the STL representation of the given type.
+std::string type2stl(const class typet &type);
+
+/// Converts a given type and identifier to human-readable STL code.
+/// \param type: Type to be converted.
+/// \param identifier: Identifier to be converted.
+/// \result String with the STL representation of the given parameters.
+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,168 @@
+/*******************************************************************\
+
+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>
+
+void structured_text_languaget::set_language_options(const optionst &options)
+{
+  (void)options;
+  return;
+}
+
+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::can_keep_file_local()
+{
+  return true;
+}
+
+bool structured_text_languaget::typecheck(
+  symbol_tablet &symbol_table,
+  const std::string &module)
+{
+  return typecheck(symbol_table, module, true);
+}
+
+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()
+{
+}
+
+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>();
+}
+
+std::unique_ptr<languaget> structured_text_languaget::new_language()
+{
+  return util_make_unique<structured_text_languaget>();
+}
+
+std::string structured_text_languaget::id() const
+{
+  return "Structured Text";
+}
+
+std::string structured_text_languaget::description() const
+{
+  return "Structured Text Language by Siemens";
+}