Skip to content

Commit 6c39035

Browse files
pkesselipkesseli
authored
Merge pull request #4657 from MatWise/feature/minimal-stl-parser
Minimal STL parser
2 parents 3f9e1b0 + 2ba1361 commit 6c39035

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

47 files changed

+2744
-3
lines changed

‎.gitignore

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,10 @@ src/json/json_lex.yy.cpp
8484
src/json/json_y.output
8585
src/json/json_y.tab.cpp
8686
src/json/json_y.tab.h
87+
src/statement-list/statement_list_lex.yy.cpp
88+
src/statement-list/statement_list_y.output
89+
src/statement-list/statement_list_y.tab.cpp
90+
src/statement-list/statement_list_y.tab.h
8791
src/xmllang/xml_lex.yy.cpp
8892
src/xmllang/xml_y.output
8993
src/xmllang/xml_y.tab.cpp

‎CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -165,6 +165,7 @@ cprover_default_properties(
165165
linking
166166
pointer-analysis
167167
solvers
168+
statement-list
168169
symtab2gb
169170
testing-utils
170171
unit

‎regression/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,7 @@ endif()
4747
add_subdirectory(goto-cc-cbmc)
4848
add_subdirectory(cbmc-cpp)
4949
add_subdirectory(goto-cc-goto-analyzer)
50+
add_subdirectory(statement-list)
5051
add_subdirectory(systemc)
5152
add_subdirectory(contracts)
5253
add_subdirectory(goto-harness)

‎regression/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ DIRS = cbmc \
2323
goto-cc-cbmc \
2424
cbmc-cpp \
2525
goto-cc-goto-analyzer \
26+
statement-list \
2627
systemc \
2728
contracts \
2829
goto-cc-file-local \

‎regression/statement-list/Add_Int/main.awl

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
FUNCTION_BLOCK "Add_Int"
2+
VERSION : 0.1
3+
VAR_INPUT
4+
"I0.0" : Int;
5+
"I0.1" : Int;
6+
END_VAR
7+
8+
VAR_OUTPUT
9+
"O0.0" : Int;
10+
END_VAR
11+
12+
13+
BEGIN
14+
NETWORK
15+
TITLE =
16+
L #"I0.0";
17+
L #"I0.1";
18+
+I;
19+
T #"O0.0";
20+
NOP 0;
21+
NETWORK
22+
TITLE =
23+
END_FUNCTION_BLOCK
24+

‎regression/statement-list/Add_Int/test.desc

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
main.awl
3+
--show-parse-tree
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^Name: "Add_Int"$
7+
^Version: 0[.]1$
8+
^ \* type: statement_list_int$
9+
^ \* identifier: "I0[.]0"$
10+
^ \* identifier: "I0[.]1"$
11+
^ \* identifier: "O0[.]0"$
12+
^statement_list_load "I0[.]0"$
13+
^statement_list_load "I0[.]1"$
14+
^statement_list_accu_int_add$
15+
^statement_list_transfer "O0[.]0"$
16+
^statement_list_nop 0$
17+
--
18+
^warning: ignoring

‎regression/statement-list/CMakeLists.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
add_test_pl_tests(
2+
"$<TARGET_FILE:cbmc>" -X smt-backend
3+
)

‎regression/statement-list/Div_Real/main.awl

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
FUNCTION_BLOCK "Div_Real"
2+
VERSION : 0.1
3+
VAR_INPUT
4+
"I0.0" : Real;
5+
"I0.1" : Real;
6+
END_VAR
7+
8+
VAR_OUTPUT
9+
"O0.0" : Real;
10+
END_VAR
11+
12+
13+
BEGIN
14+
NETWORK
15+
TITLE =
16+
L #"I0.0";
17+
L #"I0.1";
18+
/R;
19+
T #"O0.0";
20+
NOP 0;
21+
NETWORK
22+
TITLE =
23+
END_FUNCTION_BLOCK
24+

‎regression/statement-list/Div_Real/test.desc

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
main.awl
3+
--show-parse-tree
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^Name: "Div_Real"$
7+
^Version: 0[.]1$
8+
^ \* type: statement_list_real$
9+
^ \* identifier: "I0[.]0"$
10+
^ \* identifier: "I0[.]1"$
11+
^ \* identifier: "O0[.]0"$
12+
^statement_list_load "I0[.]0"$
13+
^statement_list_load "I0[.]1"$
14+
^statement_list_accu_real_div$
15+
^statement_list_transfer "O0[.]0"$
16+
^statement_list_nop 0$
17+
--
18+
^warning: ignoring

‎regression/statement-list/Makefile

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
default: test
2+
3+
test:
4+
@../test.pl -e -p -c "../../../src/cbmc/cbmc" -X smt-backend
5+
6+
tests.log: ../test.pl test
7+
8+
show:
9+
@for dir in *; do \
10+
if [ -d "$$dir" ]; then \
11+
vim -o "$$dir/*.awl" "$$dir/*.out"; \
12+
fi; \
13+
done;
14+
15+
clean:
16+
find -name '*.out' -execdir $(RM) '{}' \;
17+
find -name '*.smt2' -execdir $(RM) '{}' \;
18+
$(RM) tests.log

‎regression/statement-list/Mul_DInt/main.awl

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
FUNCTION_BLOCK "Mul_DInt"
2+
VERSION : 0.1
3+
VAR_INPUT
4+
"I0.0" : DInt;
5+
"I0.1" : DInt;
6+
END_VAR
7+
8+
VAR_OUTPUT
9+
"O0.0" : DInt;
10+
END_VAR
11+
12+
13+
BEGIN
14+
NETWORK
15+
TITLE =
16+
L #"I0.0";
17+
L #"I0.1";
18+
*D;
19+
T #"O0.0";
20+
NOP 0;
21+
NETWORK
22+
TITLE =
23+
END_FUNCTION_BLOCK
24+

‎regression/statement-list/Mul_DInt/test.desc

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
main.awl
3+
--show-parse-tree
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^Name: "Mul_DInt"$
7+
^Version: 0[.]1$
8+
^ \* type: statement_list_dint$
9+
^ \* identifier: "I0[.]0"$
10+
^ \* identifier: "I0[.]1"$
11+
^ \* identifier: "O0[.]0"$
12+
^statement_list_load "I0[.]0"$
13+
^statement_list_load "I0[.]1"$
14+
^statement_list_accu_dint_mul$
15+
^statement_list_transfer "O0[.]0"$
16+
^statement_list_nop 0$
17+
--
18+
^warning: ignoring

‎regression/statement-list/Multiple_Elements/main.awl

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
FUNCTION_BLOCK "Mult_1"
2+
VERSION : 0.1
3+
4+
BEGIN
5+
NETWORK
6+
TITLE =
7+
END_FUNCTION_BLOCK
8+
9+
FUNCTION_BLOCK "Mult_2"
10+
VERSION : 0.1
11+
12+
BEGIN
13+
NETWORK
14+
TITLE =
15+
END_FUNCTION_BLOCK
16+
17+
FUNCTION "Mult_3" : Void
18+
VERSION : 0.1
19+
20+
BEGIN
21+
NETWORK
22+
TITLE =
23+
END_FUNCTION
24+

‎regression/statement-list/Multiple_Elements/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.awl
3+
--show-parse-tree
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^Name: "Mult_1"$
7+
^Name: "Mult_2"$
8+
^Name: "Mult_3"$
9+
--
10+
^warning: ignoring

‎src/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,7 @@ add_subdirectory(langapi)
9696
add_subdirectory(linking)
9797
add_subdirectory(pointer-analysis)
9898
add_subdirectory(solvers)
99+
add_subdirectory(statement-list)
99100
add_subdirectory(util)
100101

101102
add_subdirectory(cbmc)

‎src/Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ DIRS = analyses \
2020
memory-analyzer \
2121
pointer-analysis \
2222
solvers \
23+
statement-list \
2324
symtab2gb \
2425
util \
2526
xmllang \
@@ -60,7 +61,7 @@ cpp.dir: ansi-c.dir linking.dir
6061

6162
languages: util.dir langapi.dir \
6263
cpp.dir ansi-c.dir xmllang.dir assembler.dir \
63-
jsil.dir json.dir json-symtab-language.dir
64+
jsil.dir json.dir json-symtab-language.dir statement-list.dir
6465

6566
solvers.dir: util.dir
6667

‎src/cbmc/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ target_link_libraries(cbmc-lib
2323
linking
2424
pointer-analysis
2525
solvers
26+
statement-list
2627
util
2728
xml
2829
)

‎src/cbmc/Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
88
../cpp/cpp$(LIBEXT) \
99
../json/json$(LIBEXT) \
1010
../json-symtab-language/json-symtab-language$(LIBEXT) \
11+
../statement-list/statement-list$(LIBEXT) \
1112
../linking/linking$(LIBEXT) \
1213
../big-int/big-int$(LIBEXT) \
1314
../goto-checker/goto-checker$(LIBEXT) \
@@ -41,7 +42,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
4142
../xmllang/xmllang$(LIBEXT) \
4243
../assembler/assembler$(LIBEXT) \
4344
../solvers/solvers$(LIBEXT) \
44-
../util/util$(LIBEXT)
45+
../util/util$(LIBEXT) \
4546

4647
INCLUDES= -I ..
4748

‎src/cbmc/cbmc_languages.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,14 +16,16 @@ Author: Daniel Kroening, [email protected]
1616
#include <ansi-c/ansi_c_language.h>
1717
#include <cpp/cpp_language.h>
1818
#include <json-symtab-language/json_symtab_language.h>
19+
#include <statement-list/statement_list_language.h>
1920

2021
#ifdef HAVE_JSIL
21-
#include <jsil/jsil_language.h>
22+
# include <jsil/jsil_language.h>
2223
#endif
2324

2425
void cbmc_parse_optionst::register_languages()
2526
{
2627
register_language(new_ansi_c_language);
28+
register_language(new_statement_list_language);
2729
register_language(new_cpp_language);
2830
register_language(new_json_symtab_language);
2931

‎src/cbmc/module_dependencies.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,5 +13,6 @@ langapi # should go away
1313
linking
1414
pointer-analysis
1515
solvers
16+
statement-list
1617
xmllang
1718
util

‎src/statement-list/CMakeLists.txt

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
generic_bison(statement_list)
2+
generic_flex(statement_list)
3+
4+
file(GLOB_RECURSE sources "*.cpp" "*.h")
5+
6+
add_library(statement-list
7+
${sources}
8+
${BISON_parser_OUTPUTS}
9+
${FLEX_scanner_OUTPUTS}
10+
)
11+
12+
generic_includes(statement-list)
13+
14+
target_link_libraries(statement-list util)

‎src/statement-list/Makefile

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
SRC = converters/convert_bool_literal.cpp \
2+
converters/convert_int_literal.cpp \
3+
converters/convert_real_literal.cpp \
4+
converters/convert_string_value.cpp \
5+
converters/expr2statement_list.cpp \
6+
statement_list_language.cpp \
7+
statement_list_lex.yy.cpp \
8+
statement_list_parse_tree.cpp \
9+
statement_list_parser.cpp \
10+
statement_list_typecheck.cpp \
11+
statement_list_y.tab.cpp \
12+
# Empty last line
13+
14+
INCLUDES= -I ..
15+
16+
include ../config.inc
17+
include ../common
18+
19+
CLEANFILES = stl$(LIBEXT) \
20+
statement_list_y.tab.h statement_list_y.tab.cpp \
21+
statement_list_lex.yy.cpp statement_list_y.tab.cpp.output \
22+
statement_list_y.output
23+
24+
all: statement-list$(LIBEXT)
25+
26+
###############################################################################
27+
28+
statement_list_y.tab.cpp: parser.y
29+
$(YACC) $(YFLAGS) $$flags -pyystatement_list -d parser.y -o $@
30+
31+
statement_list_y.tab.h: statement_list_y.tab.cpp
32+
if [ -e statement_list_y.tab.hpp ] ; then mv statement_list_y.tab.hpp \
33+
statement_list_y.tab.h ; else mv statement_list_y.tab.cpp.h \
34+
statement_list_y.tab.h ; fi
35+
36+
statement_list_lex.yy.cpp: scanner.l
37+
$(LEX) -Pyystatement_list -o$@ scanner.l
38+
39+
# extra dependencies
40+
statement_list_y.tab$(OBJEXT): statement_list_y.tab.cpp \
41+
statement_list_y.tab.h
42+
statement_list_lex.yy$(OBJEXT): statement_list_y.tab.cpp \
43+
statement_list_lex.yy.cpp statement_list_y.tab.h
44+
45+
###############################################################################
46+
47+
generated_files: statement_list_y.tab.cpp statement_list_lex.yy.cpp \
48+
statement_list_y.tab.h
49+
50+
###############################################################################
51+
52+
statement-list$(LIBEXT): $(OBJ)
53+
$(LINKLIB)
54+

‎src/statement-list/converters/convert_bool_literal.cpp

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
/*******************************************************************\
2+
3+
Module: Statement List Language Conversion
4+
5+
Author: Matthias Weiss, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Statement List Language Conversion
11+
12+
#include "convert_bool_literal.h"
13+
14+
#include <algorithm>
15+
#include <util/std_types.h>
16+
// Needed for back_inserter in Visual Studio.
17+
#include <iterator>
18+
19+
constant_exprt convert_bool_literal(const std::string &src)
20+
{
21+
std::string copy;
22+
transform(begin(src), end(src), back_inserter(copy), ::tolower);
23+
24+
bool_typet type;
25+
type.set(ID_statement_list_type, ID_statement_list_bool);
26+
27+
return constant_exprt(copy, type);
28+
}

0 commit comments

Comments
 (0)