Integrate STL parser into CBMC executable

MatWise · MatWise · commit b900edc73413 · 2019-05-31T16:40:00.000+01:00
Includes a basic Statement List 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.
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -165,6 +165,7 @@ cprover_default_properties(
     linking
     pointer-analysis
     solvers
+    statement-list
     symtab2gb
     testing-utils
     unit
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -96,6 +96,7 @@ add_subdirectory(langapi)
 add_subdirectory(linking)
 add_subdirectory(pointer-analysis)
 add_subdirectory(solvers)
+add_subdirectory(statement-list)
 add_subdirectory(util)
 
 add_subdirectory(cbmc)
diff --git a/src/Makefile b/src/Makefile
@@ -20,6 +20,7 @@ DIRS = analyses \
        memory-analyzer \
        pointer-analysis \
        solvers \
+       statement-list \
        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 statement-list.dir
 
 solvers.dir: util.dir
 
diff --git a/src/cbmc/CMakeLists.txt b/src/cbmc/CMakeLists.txt
@@ -23,6 +23,7 @@ target_link_libraries(cbmc-lib
     linking
     pointer-analysis
     solvers
+    statement-list
     util
     xml
 )
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
@@ -8,6 +8,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
       ../json/json$(LIBEXT) \
       ../json-symtab-language/json-symtab-language$(LIBEXT) \
+      ../statement-list/statement-list$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
       ../goto-checker/goto-checker$(LIBEXT) \
@@ -41,7 +42,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../solvers/solvers$(LIBEXT) \
-      ../util/util$(LIBEXT)
+      ../util/util$(LIBEXT) \
 
 INCLUDES= -I ..
 
diff --git a/src/cbmc/cbmc_languages.cpp b/src/cbmc/cbmc_languages.cpp
@@ -16,14 +16,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
 #include <json-symtab-language/json_symtab_language.h>
+#include <statement-list/statement_list_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_statement_list_language);
   register_language(new_cpp_language);
   register_language(new_json_symtab_language);
 
diff --git a/src/cbmc/module_dependencies.txt b/src/cbmc/module_dependencies.txt
@@ -13,5 +13,6 @@ langapi # should go away
 linking
 pointer-analysis
 solvers
+statement-list
 xmllang
 util
diff --git a/src/statement-list/CMakeLists.txt b/src/statement-list/CMakeLists.txt
@@ -0,0 +1,14 @@
+generic_bison(statement_list)
+generic_flex(statement_list)
+
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+
+add_library(statement-list
+    ${sources}
+    ${BISON_parser_OUTPUTS}
+    ${FLEX_scanner_OUTPUTS}
+)
+
+generic_includes(statement-list)
+
+target_link_libraries(statement-list util)
diff --git a/src/statement-list/Makefile b/src/statement-list/Makefile
@@ -0,0 +1,54 @@
+SRC = converters/convert_bool_literal.cpp \
+      converters/convert_int_literal.cpp \
+      converters/convert_real_literal.cpp \
+      converters/convert_string_value.cpp \
+      converters/expr2statement_list.cpp \
+      statement_list_language.cpp \
+      statement_list_lex.yy.cpp \
+      statement_list_parse_tree.cpp \
+      statement_list_parser.cpp \
+      statement_list_typecheck.cpp \
+      statement_list_y.tab.cpp \
+      # Empty last line
+
+INCLUDES= -I ..
+
+include ../config.inc
+include ../common
+
+CLEANFILES = stl$(LIBEXT) \
+  statement_list_y.tab.h statement_list_y.tab.cpp \
+  statement_list_lex.yy.cpp statement_list_y.tab.cpp.output \
+  statement_list_y.output
+
+all: statement-list$(LIBEXT)
+
+###############################################################################
+
+statement_list_y.tab.cpp: parser.y
+	$(YACC) $(YFLAGS) $$flags -pyystatement_list -d parser.y -o $@
+
+statement_list_y.tab.h: statement_list_y.tab.cpp
+	if [ -e statement_list_y.tab.hpp ] ; then mv statement_list_y.tab.hpp \
+	statement_list_y.tab.h ; else mv statement_list_y.tab.cpp.h \
+	statement_list_y.tab.h ; fi
+
+statement_list_lex.yy.cpp: scanner.l
+	$(LEX) -Pyystatement_list -o$@ scanner.l
+
+# extra dependencies
+statement_list_y.tab$(OBJEXT): statement_list_y.tab.cpp \
+  statement_list_y.tab.h
+statement_list_lex.yy$(OBJEXT): statement_list_y.tab.cpp \
+  statement_list_lex.yy.cpp statement_list_y.tab.h
+
+###############################################################################
+
+generated_files: statement_list_y.tab.cpp statement_list_lex.yy.cpp \
+  statement_list_y.tab.h
+
+###############################################################################
+
+statement-list$(LIBEXT): $(OBJ)
+	$(LINKLIB)
+
diff --git a/src/statement-list/converters/expr2statement_list.cpp b/src/statement-list/converters/expr2statement_list.cpp
@@ -0,0 +1,35 @@
+/*******************************************************************\
+
+Module: Conversion from Expression or Type to Statement List
+
+Author: Matthias Weiss, matthias.weiss@diffblue.com
+
+\*******************************************************************/
+
+#include "expr2statement_list.h"
+
+#include <util/symbol.h>
+
+std::string expr2stl(const exprt &expr)
+{
+  // TODO: Implement expr2stl.
+  // Expand this section so that it is able to properly convert from
+  // CBMC expressions to STL code.
+  return expr.pretty();
+}
+
+std::string type2stl(const typet &type)
+{
+  // TODO: Implement type2stl.
+  // Expand this section so that it is able to properly convert from
+  // CBMC types to STL code.
+  return type.pretty();
+}
+
+std::string type2stl(const typet &type, const std::string &identifier)
+{
+  // TODO: Implement type2stl.
+  // Expand this section so that it is able to properly convert from
+  // CBMC types to STL code.
+  return type.pretty();
+}
diff --git a/src/statement-list/converters/expr2statement_list.h b/src/statement-list/converters/expr2statement_list.h
@@ -0,0 +1,30 @@
+/*******************************************************************\
+
+Module: Conversion from Expression or Type to Statement List Language
+
+Author: Matthias Weiss, matthias.weiss@diffblue.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
+#define CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
+
+#include <string>
+
+/// Converts a given expression to human-readable STL code.
+/// \param expr: Expression 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 class typet &type, const std::string &identifier);
+
+#endif // CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
diff --git a/src/statement-list/statement_list_language.cpp b/src/statement-list/statement_list_language.cpp
@@ -0,0 +1,158 @@
+/*******************************************************************\
+
+Module: Statement List Language Interface
+
+Author: Matthias Weiss, matthias.weiss@diffblue.com
+
+\*******************************************************************/
+
+/// \file
+/// Statement List Language Interface
+
+#include "statement_list_language.h"
+#include "converters/expr2statement_list.h"
+#include "statement_list_parser.h"
+#include "statement_list_typecheck.h"
+
+#include <linking/linking.h>
+#include <linking/remove_internal_symbols.h>
+#include <util/get_base_name.h>
+
+void statement_list_languaget::set_language_options(const optionst &)
+{
+  return;
+}
+
+bool statement_list_languaget::generate_support_functions(symbol_tablet &)
+{
+  return false;
+}
+
+bool statement_list_languaget::typecheck(
+  symbol_tablet &symbol_table,
+  const std::string &module,
+  const bool keep_file_local)
+{
+  symbol_tablet new_symbol_table;
+
+  if(statement_list_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 statement_list_languaget::parse(
+  std::istream &instream,
+  const std::string &path)
+{
+  statement_list_parser.clear();
+  parse_path = path;
+  statement_list_parser.set_line_no(0);
+  statement_list_parser.set_file(path);
+  statement_list_parser.in = &instream;
+  statement_list_scanner_init();
+  bool result = statement_list_parser.parse();
+
+  // store result
+  statement_list_parser.swap_tree(parse_tree);
+
+  return result;
+}
+
+void statement_list_languaget::show_parse(std::ostream &out)
+{
+  parse_tree.output(out);
+}
+
+bool statement_list_languaget::can_keep_file_local()
+{
+  return true;
+}
+
+bool statement_list_languaget::typecheck(
+  symbol_tablet &symbol_table,
+  const std::string &module)
+{
+  return typecheck(symbol_table, module, true);
+}
+
+bool statement_list_languaget::from_expr(
+  const exprt &expr,
+  std::string &code,
+  const namespacet &)
+{
+  code = expr2stl(expr);
+  return false;
+}
+
+bool statement_list_languaget::from_type(
+  const typet &type,
+  std::string &code,
+  const namespacet &)
+{
+  code = type2stl(type);
+  return false;
+}
+
+bool statement_list_languaget::type_to_name(
+  const typet &type,
+  std::string &name,
+  const namespacet &ns)
+{
+  return from_type(type, name, ns);
+}
+
+bool statement_list_languaget::to_expr(
+  const std::string &,
+  const std::string &,
+  exprt &,
+  const namespacet &)
+{
+  return true;
+}
+
+statement_list_languaget::statement_list_languaget()
+{
+}
+
+statement_list_languaget::~statement_list_languaget()
+{
+  parse_tree.clear();
+}
+
+void statement_list_languaget::modules_provided(std::set<std::string> &modules)
+{
+  modules.insert(get_base_name(parse_path, true));
+}
+
+std::set<std::string> statement_list_languaget::extensions() const
+{
+  return {"awl"};
+}
+
+std::unique_ptr<languaget> new_statement_list_language()
+{
+  return util_make_unique<statement_list_languaget>();
+}
+
+std::unique_ptr<languaget> statement_list_languaget::new_language()
+{
+  return util_make_unique<statement_list_languaget>();
+}
+
+std::string statement_list_languaget::id() const
+{
+  return "Statement List";
+}
+
+std::string statement_list_languaget::description() const
+{
+  return "Statement List Language by Siemens";
+}
diff --git a/src/statement-list/statement_list_language.h b/src/statement-list/statement_list_language.h
diff --git a/src/statement-list/statement_list_typecheck.cpp b/src/statement-list/statement_list_typecheck.cpp
diff --git a/src/statement-list/statement_list_typecheck.h b/src/statement-list/statement_list_typecheck.h
diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt
diff --git a/unit/Makefile b/unit/Makefile

Original file line number	Diff line number	Diff line change
`@@ -23,6 +23,7 @@ target_link_libraries(cbmc-lib`
`23`	`23`	`linking`
`24`	`24`	`pointer-analysis`
`25`	`25`	`solvers`
	`26`	`+ statement-list`
`26`	`27`	`util`
`27`	`28`	`xml`
`28`	`29`	`)`