Minimal STL parser

.gitignore

@@ -84,6 +84,10 @@ src/json/json_lex.yy.cpp
 src/json/json_y.output
 src/json/json_y.tab.cpp
 src/json/json_y.tab.h
+src/statement-list/statement_list_lex.yy.cpp
+src/statement-list/statement_list_y.output
+src/statement-list/statement_list_y.tab.cpp
+src/statement-list/statement_list_y.tab.h
 src/xmllang/xml_lex.yy.cpp
 src/xmllang/xml_y.output
 src/xmllang/xml_y.tab.cpp

CMakeLists.txt

@@ -165,6 +165,7 @@ cprover_default_properties(
     linking
     pointer-analysis
     solvers
+    statement-list
     symtab2gb
     testing-utils
     unit

regression/CMakeLists.txt

@@ -47,6 +47,7 @@ endif()
 add_subdirectory(goto-cc-cbmc)
 add_subdirectory(cbmc-cpp)
 add_subdirectory(goto-cc-goto-analyzer)
+add_subdirectory(statement-list)
 add_subdirectory(systemc)
 add_subdirectory(contracts)
 add_subdirectory(goto-harness)

regression/Makefile

@@ -23,6 +23,7 @@ DIRS = cbmc \
        goto-cc-cbmc \
        cbmc-cpp \
        goto-cc-goto-analyzer \
+       statement-list \
        systemc \
        contracts \
        goto-cc-file-local \

regression/statement-list/Add_Int/main.awl

@@ -0,0 +1,24 @@
+FUNCTION_BLOCK "Add_Int"
+VERSION : 0.1
+   VAR_INPUT 
+      "I0.0" : Int;
+      "I0.1" : Int;
+   END_VAR
+
+   VAR_OUTPUT 
+      "O0.0" : Int;
+   END_VAR
+
+
+BEGIN
+NETWORK
+TITLE = 
+      L #"I0.0";
+      L #"I0.1";
+      +I;
+      T #"O0.0";
+      NOP 0;
+NETWORK
+TITLE = 
+END_FUNCTION_BLOCK
+

regression/statement-list/Add_Int/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.awl
+--show-parse-tree
+^EXIT=0$
+^SIGNAL=0$
+^Name: "Add_Int"$
+^Version: 0[.]1$
+^  \* type: statement_list_int$
+^  \* identifier: "I0[.]0"$
+^  \* identifier: "I0[.]1"$
+^  \* identifier: "O0[.]0"$
+^statement_list_load	"I0[.]0"$
+^statement_list_load	"I0[.]1"$
+^statement_list_accu_int_add$
+^statement_list_transfer	"O0[.]0"$
+^statement_list_nop	0$
+--
+^warning: ignoring

regression/statement-list/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>" -X smt-backend
+)

regression/statement-list/Div_Real/main.awl

@@ -0,0 +1,24 @@
+FUNCTION_BLOCK "Div_Real"
+VERSION : 0.1
+   VAR_INPUT 
+      "I0.0" : Real;
+      "I0.1" : Real;
+   END_VAR
+
+   VAR_OUTPUT 
+      "O0.0" : Real;
+   END_VAR
+
+
+BEGIN
+NETWORK
+TITLE = 
+      L #"I0.0";
+      L #"I0.1";
+      /R;
+      T #"O0.0";
+      NOP 0;
+NETWORK
+TITLE = 
+END_FUNCTION_BLOCK
+

regression/statement-list/Div_Real/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.awl
+--show-parse-tree
+^EXIT=0$
+^SIGNAL=0$
+^Name: "Div_Real"$
+^Version: 0[.]1$
+^  \* type: statement_list_real$
+^  \* identifier: "I0[.]0"$
+^  \* identifier: "I0[.]1"$
+^  \* identifier: "O0[.]0"$
+^statement_list_load	"I0[.]0"$
+^statement_list_load	"I0[.]1"$
+^statement_list_accu_real_div$
+^statement_list_transfer	"O0[.]0"$
+^statement_list_nop	0$
+--
+^warning: ignoring

regression/statement-list/Makefile

@@ -0,0 +1,18 @@
+default: test
+
+test:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc" -X smt-backend
+
+tests.log: ../test.pl test
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.awl" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.smt2' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/statement-list/Mul_DInt/main.awl

@@ -0,0 +1,24 @@
+FUNCTION_BLOCK "Mul_DInt"
+VERSION : 0.1
+   VAR_INPUT 
+      "I0.0" : DInt;
+      "I0.1" : DInt;
+   END_VAR
+
+   VAR_OUTPUT 
+      "O0.0" : DInt;
+   END_VAR
+
+
+BEGIN
+NETWORK
+TITLE = 
+      L #"I0.0";
+      L #"I0.1";
+      *D;
+      T #"O0.0";
+      NOP 0;
+NETWORK
+TITLE = 
+END_FUNCTION_BLOCK
+

regression/statement-list/Mul_DInt/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.awl
+--show-parse-tree
+^EXIT=0$
+^SIGNAL=0$
+^Name: "Mul_DInt"$
+^Version: 0[.]1$
+^  \* type: statement_list_dint$
+^  \* identifier: "I0[.]0"$
+^  \* identifier: "I0[.]1"$
+^  \* identifier: "O0[.]0"$
+^statement_list_load	"I0[.]0"$
+^statement_list_load	"I0[.]1"$
+^statement_list_accu_dint_mul$
+^statement_list_transfer	"O0[.]0"$
+^statement_list_nop	0$
+--
+^warning: ignoring

regression/statement-list/Multiple_Elements/main.awl

@@ -0,0 +1,24 @@
+FUNCTION_BLOCK "Mult_1"
+VERSION : 0.1
+
+BEGIN
+NETWORK
+TITLE = 
+END_FUNCTION_BLOCK
+
+FUNCTION_BLOCK "Mult_2"
+VERSION : 0.1
+
+BEGIN
+NETWORK
+TITLE = 
+END_FUNCTION_BLOCK
+
+FUNCTION "Mult_3" : Void
+VERSION : 0.1
+
+BEGIN
+NETWORK
+TITLE = 
+END_FUNCTION
+

regression/statement-list/Multiple_Elements/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.awl
+--show-parse-tree
+^EXIT=0$
+^SIGNAL=0$
+^Name: "Mult_1"$
+^Name: "Mult_2"$
+^Name: "Mult_3"$
+--
+^warning: ignoring

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)

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
 

src/cbmc/CMakeLists.txt

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

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 ..
 

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 <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);
 

src/cbmc/module_dependencies.txt

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

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)

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)
+

src/statement-list/converters/convert_bool_literal.cpp

@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module: Statement List Language Conversion
+
+Author: Matthias Weiss, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Statement List Language Conversion
+
+#include "convert_bool_literal.h"
+
+#include <algorithm>
+#include <util/std_types.h>
+// Needed for back_inserter in Visual Studio.
+#include <iterator>
+
+constant_exprt convert_bool_literal(const std::string &src)
+{
+  std::string copy;
+  transform(begin(src), end(src), back_inserter(copy), ::tolower);
+
+  bool_typet type;
+  type.set(ID_statement_list_type, ID_statement_list_bool);
+
+  return constant_exprt(copy, type);
+}