From 37f60f28310d3a49a2b233b992c1014404dae4ee Mon Sep 17 00:00:00 2001 From: Matthias Weiss Date: Mon, 20 May 2019 15:48:10 +0100 Subject: [PATCH 1/3] Add basic Statement List parser Includes support for simple arithmetic and boolean expressions as well as other Statement List language features, such as networks, functions and function blocks. --- .gitignore | 4 + .../converters/convert_bool_literal.cpp | 28 + .../converters/convert_bool_literal.h | 25 + .../converters/convert_int_literal.cpp | 55 ++ .../converters/convert_int_literal.h | 33 + .../converters/convert_real_literal.cpp | 23 + .../converters/convert_real_literal.h | 25 + .../converters/convert_string_value.cpp | 34 + .../converters/convert_string_value.h | 33 + .../converters/module_dependencies.txt | 3 + src/statement-list/module_dependencies.txt | 5 + src/statement-list/parser.y | 701 ++++++++++++++++++ src/statement-list/scanner.l | 191 +++++ .../statement_list_parse_tree.cpp | 129 ++++ .../statement_list_parse_tree.h | 211 ++++++ src/statement-list/statement_list_parser.cpp | 254 +++++++ src/statement-list/statement_list_parser.h | 159 ++++ src/util/irep_ids.def | 41 + 18 files changed, 1954 insertions(+) create mode 100644 src/statement-list/converters/convert_bool_literal.cpp create mode 100644 src/statement-list/converters/convert_bool_literal.h create mode 100644 src/statement-list/converters/convert_int_literal.cpp create mode 100644 src/statement-list/converters/convert_int_literal.h create mode 100644 src/statement-list/converters/convert_real_literal.cpp create mode 100644 src/statement-list/converters/convert_real_literal.h create mode 100644 src/statement-list/converters/convert_string_value.cpp create mode 100644 src/statement-list/converters/convert_string_value.h create mode 100644 src/statement-list/converters/module_dependencies.txt create mode 100644 src/statement-list/module_dependencies.txt create mode 100644 src/statement-list/parser.y create mode 100644 src/statement-list/scanner.l create mode 100644 src/statement-list/statement_list_parse_tree.cpp create mode 100644 src/statement-list/statement_list_parse_tree.h create mode 100644 src/statement-list/statement_list_parser.cpp create mode 100644 src/statement-list/statement_list_parser.h diff --git a/.gitignore b/.gitignore index 2b49e07380b..869d1f78d06 100644 --- a/.gitignore +++ b/.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 diff --git a/src/statement-list/converters/convert_bool_literal.cpp b/src/statement-list/converters/convert_bool_literal.cpp new file mode 100644 index 00000000000..3b598fe0291 --- /dev/null +++ b/src/statement-list/converters/convert_bool_literal.cpp @@ -0,0 +1,28 @@ +/*******************************************************************\ + +Module: Statement List Language Conversion + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Conversion + +#include "convert_bool_literal.h" + +#include +#include +// Needed for back_inserter in Visual Studio. +#include + +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); +} diff --git a/src/statement-list/converters/convert_bool_literal.h b/src/statement-list/converters/convert_bool_literal.h new file mode 100644 index 00000000000..60d9fb28b5a --- /dev/null +++ b/src/statement-list/converters/convert_bool_literal.h @@ -0,0 +1,25 @@ +/*******************************************************************\ + +Module: Statement List Language Conversion + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Conversion + +#ifndef CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_BOOL_LITERAL_H +#define CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_BOOL_LITERAL_H + +#include + +#include +#include + +/// Converts a string into the corresponding 'Bool' expression. +/// \param src: String returned by the parser. +/// \return Constant expression representing the boolean value. +constant_exprt convert_bool_literal(const std::string &src); + +#endif // CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_INT_LITERAL_H diff --git a/src/statement-list/converters/convert_int_literal.cpp b/src/statement-list/converters/convert_int_literal.cpp new file mode 100644 index 00000000000..56144dbe516 --- /dev/null +++ b/src/statement-list/converters/convert_int_literal.cpp @@ -0,0 +1,55 @@ +/*******************************************************************\ + +Module: Statement List Language Conversion + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Conversion + +#include "convert_int_literal.h" + +#include +#include + +/// Hex literals in STL are preceded by '16#' +#define HEX_PREFIX_LENGTH 3 +/// Binary literals in STL are preceded by '2#' +#define BINARY_PREFIX_LENGTH 2 + +constant_exprt convert_int_dec_literal(const std::string &src) +{ + std::string value(src); + value.erase(std::remove(begin(value), end(value), '+'), end(value)); + + signedbv_typet type{16}; + type.set(ID_statement_list_type, ID_statement_list_int); + + return constant_exprt(value, type); +} + +constant_exprt convert_int_hex_literal(const std::string &src) +{ + const std::string hex_literal( + src.substr(HEX_PREFIX_LENGTH, std::string::npos)); + int value = std::stoi(hex_literal, nullptr, 16); + + signedbv_typet type{16}; + type.set(ID_statement_list_type, ID_statement_list_int); + + return constant_exprt(std::to_string(value), type); +} + +constant_exprt convert_int_bit_literal(const std::string &src) +{ + const std::string bit_literal( + src.substr(BINARY_PREFIX_LENGTH, std::string::npos)); + int value = std::stoi(bit_literal, nullptr, 2); + + signedbv_typet type{16}; + type.set(ID_statement_list_type, ID_statement_list_int); + + return constant_exprt{std::to_string(value), type}; +} diff --git a/src/statement-list/converters/convert_int_literal.h b/src/statement-list/converters/convert_int_literal.h new file mode 100644 index 00000000000..f752e029902 --- /dev/null +++ b/src/statement-list/converters/convert_int_literal.h @@ -0,0 +1,33 @@ +/*******************************************************************\ + +Module: Statement List Language Conversion + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Conversion + +#ifndef CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_INT_LITERAL_H +#define CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_INT_LITERAL_H + +#include +#include + +/// Converts a string into the corresponding 'Int' expression. +/// \param src: String returned by the parser (base 10). +/// \return Constant expression representing the integer value. +constant_exprt convert_int_dec_literal(const std::string &src); + +/// Converts a string into the corresponding 'Int' expression. +/// \param src: String returned by the parser (base 16). +/// \return Constant expression representing the integer value. +constant_exprt convert_int_hex_literal(const std::string &src); + +/// Converts a string into the corresponding 'Int' expression. +/// \param src: String returned by the parser (base 2). +/// \return Constant expression representing the integer value. +constant_exprt convert_int_bit_literal(const std::string &src); + +#endif // CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_INT_LITERAL_H diff --git a/src/statement-list/converters/convert_real_literal.cpp b/src/statement-list/converters/convert_real_literal.cpp new file mode 100644 index 00000000000..61145e0e00b --- /dev/null +++ b/src/statement-list/converters/convert_real_literal.cpp @@ -0,0 +1,23 @@ +/*******************************************************************\ + +Module: Statement List Language Conversion + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Conversion + +#include "convert_real_literal.h" + +#include +#include + +constant_exprt convert_real_literal(const std::string &src) +{ + floatbv_typet type = ieee_float_spect::single_precision().to_type(); + type.set(ID_statement_list_type, ID_statement_list_real); + + return constant_exprt(src, type); +} diff --git a/src/statement-list/converters/convert_real_literal.h b/src/statement-list/converters/convert_real_literal.h new file mode 100644 index 00000000000..2fcb209bfd7 --- /dev/null +++ b/src/statement-list/converters/convert_real_literal.h @@ -0,0 +1,25 @@ +/*******************************************************************\ + +Module: Statement List Language Conversion + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Conversion + +#ifndef CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_REAL_LITERAL_H +#define CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_REAL_LITERAL_H + +#include + +#include +#include + +/// Converts a string into the corresponding 'Real' expression. +/// \param src: String returned by the parser. +/// \return Constant expression representing the real value. +constant_exprt convert_real_literal(const std::string &src); + +#endif // CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_REAL_VALUE_H diff --git a/src/statement-list/converters/convert_string_value.cpp b/src/statement-list/converters/convert_string_value.cpp new file mode 100644 index 00000000000..2f03408eab4 --- /dev/null +++ b/src/statement-list/converters/convert_string_value.cpp @@ -0,0 +1,34 @@ +/*******************************************************************\ + +Module: Statement List Language Conversion + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Conversion + +#include "convert_string_value.h" + +string_constantt convert_identifier(const std::string &src) +{ + string_constantt result{src}; + result.set(ID_statement_list_type, ID_statement_list_identifier); + return result; +} + +string_constantt convert_title(const std::string &src) +{ + string_constantt result{src}; + result.set(ID_statement_list_type, ID_statement_list_title); + return result; +} + +code_labelt convert_label(const std::string &src) +{ + // Cut the trailing colon + std::string value = src.substr(0, src.length() - 1); + + return code_labelt{value, codet(ID_label)}; +} diff --git a/src/statement-list/converters/convert_string_value.h b/src/statement-list/converters/convert_string_value.h new file mode 100644 index 00000000000..770eda247db --- /dev/null +++ b/src/statement-list/converters/convert_string_value.h @@ -0,0 +1,33 @@ +/*******************************************************************\ + +Module: Statement List Language Conversion + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Conversion + +#ifndef CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_STRING_VALUE_H +#define CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_STRING_VALUE_H + +#include +#include + +/// Converts a string into a Statement List identifier. +/// \param src: String returned by the parser. +/// \return Constant string expression representing the identifier. +string_constantt convert_identifier(const std::string &src); + +/// Converts a string into a Statement List title. +/// \param src: String returned by the parser. +/// \return Constant string expression representing the title. +string_constantt convert_title(const std::string &src); + +/// Converts a string into a Statement List label. +/// \param src: String returned by the parser. +/// \return Code label expression representing the label. +code_labelt convert_label(const std::string &src); + +#endif // CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_STRING_VALUE_H diff --git a/src/statement-list/converters/module_dependencies.txt b/src/statement-list/converters/module_dependencies.txt new file mode 100644 index 00000000000..a0b992cc033 --- /dev/null +++ b/src/statement-list/converters/module_dependencies.txt @@ -0,0 +1,3 @@ +statement-list +statement-list/converters +util diff --git a/src/statement-list/module_dependencies.txt b/src/statement-list/module_dependencies.txt new file mode 100644 index 00000000000..2c747dd9b95 --- /dev/null +++ b/src/statement-list/module_dependencies.txt @@ -0,0 +1,5 @@ +converters +langapi +linking +statement-list +util \ No newline at end of file diff --git a/src/statement-list/parser.y b/src/statement-list/parser.y new file mode 100644 index 00000000000..0ebb27a07b2 --- /dev/null +++ b/src/statement-list/parser.y @@ -0,0 +1,701 @@ +%{ + +// This parser is based on the IEC standard 61131-3 which, among other things, +// includes a BNF grammar for the Instruction List (IL) language. The +// Statement List language (STL) by Siemens complies with the standards +// defined by the IEC, although some modifications were made for compatibility +// reasons. As a consequence, the general language structure specified by the +// IEC is similar to the structure of STL, but there are differences between +// their syntax and some language features (In general, Siemens implements more +// language features in STL than described in the standard). + +#ifdef STATEMENT_LIST_DEBUG +#define YYDEBUG 1 +#endif +#define PARSER statement_list_parser + +#include "statement_list_parser.h" +#include "converters/convert_string_value.h" +#include + +int yystatement_listlex(); +extern char *yystatement_listtext; + +#define YYSTYPE unsigned +#define YYSTYPE_IS_TRIVIAL 1 + +#include "statement_list_y.tab.h" + +// Visual Studio +#ifdef _MSC_VER +// Disable warnings for possible loss of data. +#pragma warning(disable:4242) +#pragma warning(disable:4244) +// Disable warning for signed/unsigned mismatch. +#pragma warning(disable:4365) +// Disable warning for switch with default but no case labels. +#pragma warning(disable:4065) +// Disable warning for unreachable code. +#pragma warning(disable:4702) +#endif + +/*** Token declaration *******************************************************/ +%} + +/*** STL file structure keywords *********************************************/ +%token TOK_VERSION "VERSION" +%token TOK_BEGIN "BEGIN" +%token TOK_FUNCTION_BLOCK "FUNCTION_BLOCK" +%token TOK_END_FUNCTION_BLOCK "END_FUNCTION_BLOCK" +%token TOK_FUNCTION "FUNCTION" +%token TOK_END_FUNCTION "END_FUNCTION" +%token TOK_VAR_INPUT "VAR_INPUT" +%token TOK_VAR_OUTPUT "VAR_OUTPUT" +%token TOK_END_VAR "END_VAR" +%token TOK_NETWORK "NETWORK" +%token TOK_TITLE "TITLE" + +/*** Siemens types ***********************************************************/ +%token TOK_INT "Int" +%token TOK_DINT "DInt" +%token TOK_REAL "Real" +%token TOK_BOOL "Bool" +%token TOK_VOID "Void" + +/*** Operators ***************************************************************/ +%token TOK_LOAD "L" +%token TOK_TRANSFER "T" +%token TOK_NOP "NOP" +%token TOK_AND "A" +%token TOK_AND_NOT "AN" +%token TOK_OR "O" +%token TOK_OR_NOT "ON" +%token TOK_XOR "X" +%token TOK_XOR_NOT "XN" +%token TOK_CONST_ADD "+" +%token TOK_ACCU_INT_ADD "+I" +%token TOK_ACCU_INT_SUB "-I" +%token TOK_ACCU_INT_MUL "*I" +%token TOK_ACCU_INT_DIV "/I" +%token TOK_ACCU_REAL_ADD "+R" +%token TOK_ACCU_REAL_SUB "-R" +%token TOK_ACCU_REAL_MUL "*R" +%token TOK_ACCU_REAL_DIV "/R" +%token TOK_ACCU_DINT_ADD "+D" +%token TOK_ACCU_DINT_SUB "-D" +%token TOK_ACCU_DINT_MUL "*D" +%token TOK_ACCU_DINT_DIV "/D" +%token TOK_ASSIGNMENT ":=" + +/*** Value tokens ***/ +%token TOK_INT_LITERAL +%token TOK_BOOL_LITERAL +%token TOK_REAL_LITERAL +%token TOK_IDENTIFIER +%token TOK_TITLE_VALUE +%token TOK_LABEL + +/*** Priority, associativity, etc. definitions *******************************/ + +%start init + +%{ +/*** Grammar rules ***********************************************************/ + +// The follwing abbreviations will be used: +// Zom: "Zero or more", eqivalent to the '*' quantifier +// Opt: "Optional", equivalent to the '?' quantifier +// Oom: "One or more", equivalent to the '+' quantifier +%} +%% + +init: + init FB_Decl + | init Func_Decl + | /* nothing */ + ; + +// Variable and type declarations +Var_Decl_Init: + Variable_List ':' Simple_Spec_Init + { + $$ = $1; + parser_stack($$).add_to_operands(std::move(parser_stack($3))); + } + ; + +Variable_List: + Variable_Name Zom_Separated_Variable_Name + { + $$ = $2; + parser_stack($$).add_to_operands(std::move(parser_stack($1))); + } + ; + +Zom_Separated_Variable_Name: + Zom_Separated_Variable_Name ',' Variable_Name + { + $$ = $1; + parser_stack($$).add_to_operands(std::move(parser_stack($3))); + } + | /* nothing */ + { + newstack($$); + parser_stack($$).id(ID_statement_list_var_entry); + + } + ; + +Variable_Name: + TOK_IDENTIFIER + ; + +Simple_Spec_Init: + Simple_Spec + ; + +Simple_Spec: + Elem_Type_Name + ; + +Elem_Type_Name: + Numeric_Type_Name + ; + +Numeric_Type_Name: + Int_Type_Name + | DInt_Type_Name + | Real_Type_Name + | Bool_Type_Name + ; + +Int_Type_Name: + Sign_Int_Type_Name + ; + +Sign_Int_Type_Name: + TOK_INT + { + $$ = $1; + parser_stack($$).id(ID_statement_list_int); + } + ; + +DInt_Type_Name: + Sign_DInt_Type_Name + ; + +Sign_DInt_Type_Name: + TOK_DINT + { + $$ = $1; + parser_stack($$).id(ID_statement_list_dint); + } + ; + +Real_Type_Name: + TOK_REAL + { + $$ = $1; + parser_stack($$).id(ID_statement_list_real); + } + ; + +Bool_Type_Name: + TOK_BOOL + { + $$ = $1; + parser_stack($$).id(ID_statement_list_bool); + } + +// Function Block declaration +Derived_FB_Name: + TOK_IDENTIFIER + ; + +FB_Decl: + TOK_FUNCTION_BLOCK Derived_FB_Name Version_Label Zom_FB_General_Var_Decls + FB_Body TOK_END_FUNCTION_BLOCK + { + newstack($$); + parser_stack($$).id(ID_statement_list_function_block); + parser_stack($$).add_to_operands(std::move(parser_stack($2)), + std::move(parser_stack($3))); + parser_stack($$).add_to_operands(std::move(parser_stack($4)), + std::move(parser_stack($5))); + PARSER.add_function_block(parser_stack($$)); + } + ; + +Version_Label: + TOK_VERSION ':' TOK_REAL_LITERAL + { + $$ = $3; + parser_stack($$).type().id(ID_statement_list_version); + } + ; + +Zom_FB_General_Var_Decls: + Zom_FB_General_Var_Decls FB_General_Var_Decl + { + $$ = $1; + parser_stack($$).add_to_operands(std::move(parser_stack($2))); + } + | /* nothing */ + { + newstack($$); + parser_stack($$).id(ID_statement_list_var_decls); + } + ; + +FB_General_Var_Decl: + FB_IO_Var_Decls + ; + +FB_IO_Var_Decls: + FB_Input_Decls + | FB_Output_Decls + ; + +FB_Input_Decls: + TOK_VAR_INPUT Zom_FB_Input_Decl TOK_END_VAR + { + $$ = $2; + } + ; + +Zom_FB_Input_Decl: + Zom_FB_Input_Decl FB_Input_Decl ';' + { + $$ = $1; + parser_stack($$).add_to_operands(std::move(parser_stack($2))); + } + | /* nothing */ + { + newstack($$); + parser_stack($$).id(ID_statement_list_var_input); + } + ; + +FB_Input_Decl: + Var_Decl_Init + ; + +FB_Output_Decls: + TOK_VAR_OUTPUT Zom_FB_Output_Decl TOK_END_VAR + { + $$ = $2; + } + ; + +Zom_FB_Output_Decl: + Zom_FB_Output_Decl FB_Output_Decl ';' + { + $$ = $1; + parser_stack($$).add_to_operands(std::move(parser_stack($2))); + } + | /* nothing */ + { + newstack($$); + parser_stack($$).id(ID_statement_list_var_output); + } + ; + +FB_Output_Decl: + Var_Decl_Init + ; + +FB_Body: + TOK_BEGIN Oom_IL_Network + { + $$ = $2; + } + ; + +// Function declaration +Func_Decl: + TOK_FUNCTION Derived_Func_Name ':' Func_Return_Value Version_Label + Zom_Func_General_Var_Decls Func_Body TOK_END_FUNCTION + { + newstack($$); + parser_stack($$).id(ID_statement_list_function); + parser_stack($$).add_to_operands(std::move(parser_stack($2)), + std::move(parser_stack($5))); + parser_stack($$).add_to_operands(std::move(parser_stack($6)), + std::move(parser_stack($7))); + PARSER.add_function(parser_stack($$)); + } + ; + +Derived_Func_Name: + TOK_IDENTIFIER + ; + +Func_Return_Value: + TOK_VOID + ; + +Zom_Func_General_Var_Decls: + Zom_Func_General_Var_Decls Func_General_Var_Decl + { + $$ = $1; + parser_stack($$).add_to_operands(std::move(parser_stack($2))); + } + | /* nothing */ + { + newstack($$); + parser_stack($$).id(ID_statement_list_var_decls); + } + ; + +Func_General_Var_Decl: + IO_Var_Decls + ; + +IO_Var_Decls: + Input_Decls + | Output_Decls + ; + +Input_Decls: + TOK_VAR_INPUT Zom_Input_Decl TOK_END_VAR + { + $$ = $2; + } + ; + +Zom_Input_Decl: + Zom_Input_Decl Input_Decl ';' + { + $$ = $1; + parser_stack($$).add_to_operands(std::move(parser_stack($2))); + } + | /* nothing */ + { + newstack($$); + parser_stack($$).id(ID_statement_list_var_input); + } + ; + +Input_Decl: + Var_Decl_Init + ; + +Output_Decls: + TOK_VAR_OUTPUT Zom_Output_Decl TOK_END_VAR + { + $$ = $2; + } + ; + +Zom_Output_Decl: + Zom_Output_Decl Output_Decl ';' + { + $$ = $1; + parser_stack($$).add_to_operands(std::move(parser_stack($2))); + } + | /* nothing */ + { + newstack($$); + parser_stack($$).id(ID_statement_list_var_output); + } + ; + +Output_Decl: + Var_Decl_Init + ; + +Func_Body: + TOK_BEGIN Oom_IL_Network + { + $$ = $2; + } + ; + +// Network declaration +Oom_IL_Network: + Oom_IL_Network IL_Network + { + $$ = $1; + parser_stack($$).add_to_operands(std::move(parser_stack($2))); + } + | IL_Network + { + newstack($$); + parser_stack($$).id(ID_statement_list_networks); + parser_stack($$).add_to_operands(std::move(parser_stack($1))); + } + ; + +IL_Network: + TOK_NETWORK TOK_TITLE '=' Opt_TITLE_VALUE Opt_Instruction_List + { + newstack($$); + parser_stack($$).id(ID_statement_list_network); + parser_stack($$).add_to_operands(std::move(parser_stack($4)), + std::move(parser_stack($5))); + } + ; + + +Opt_TITLE_VALUE: + TOK_TITLE_VALUE + | /* nothing */ + { + newstack($$); + parser_stack($$) = convert_title(""); + } + ; + +Opt_Instruction_List: + Instruction_List + | + { + newstack($$); + parser_stack($$).id(ID_statement_list_instructions); + } + ; + +// Structured Text grammar +Instruction_List: + Oom_IL_Instruction + ; + +Oom_IL_Instruction: + Oom_IL_Instruction IL_Instruction + { + $$ = $1; + parser_stack($$).add_to_operands(std::move(parser_stack($2))); + } + | IL_Instruction + { + newstack($$); + parser_stack($$).id(ID_statement_list_instructions); + parser_stack($$).add_to_operands(std::move(parser_stack($1))); + } + ; + +IL_Instruction: + Opt_Label Opt_Instruction ';' + { + $$ = $2; + parser_stack($$).add_to_operands(std::move(parser_stack($1))); + } + ; + +Opt_Label: + IL_Label + | /* nothing */ + { + newstack($$); + // ID of expression is nil to indicate that there is no label + } + ; + +IL_Label: + TOK_LABEL + ; + +Opt_Instruction: + IL_Simple_Operation + | IL_Expr + | /* nothing */ + { + newstack($$); + parser_stack($$).id(ID_statement_list_instruction); + } + ; + +IL_Simple_Operation: + IL_Simple_Operator Opt_Operand + { + newstack($$); + parser_stack($$).id(ID_statement_list_instruction); + parser_stack($$).add_to_operands(std::move(parser_stack($1)), + std::move(parser_stack($2))); + } + ; + +Opt_Operand: + IL_Operand + | + { + newstack($$); + // ID of expression is nil to indicate that there is no operand + } + ; + +IL_Expr: + IL_Expr_Operator '(' Opt_Operand Opt_Simple_Inst_List ')' + { + newstack($$); + parser_stack($$).id(ID_statement_list_instruction); + parser_stack($$).add_to_operands(std::move(parser_stack($3)), + std::move(parser_stack($4))); + } + ; + +IL_Simple_Operator: + TOK_LOAD + { + $$ = $1; + parser_stack($$).id(ID_statement_list_load); + } + | TOK_TRANSFER + { + $$ = $1; + parser_stack($$).id(ID_statement_list_transfer); + } + | TOK_NOP + { + $$ = $1; + parser_stack($$).id(ID_statement_list_nop); + } + | TOK_CONST_ADD + { + $$ = $1; + parser_stack($$).id(ID_statement_list_const_add); + } + | TOK_ACCU_INT_ADD + { + $$ = $1; + parser_stack($$).id(ID_statement_list_accu_int_add); + } + | TOK_ACCU_INT_SUB + { + $$ = $1; + parser_stack($$).id(ID_statement_list_accu_int_sub); + } + | TOK_ACCU_INT_MUL + { + $$ = $1; + parser_stack($$).id(ID_statement_list_accu_int_mul); + } + | TOK_ACCU_INT_DIV + { + $$ = $1; + parser_stack($$).id(ID_statement_list_accu_int_div); + } + | TOK_ACCU_REAL_ADD + { + $$ = $1; + parser_stack($$).id(ID_statement_list_accu_real_add); + } + | TOK_ACCU_REAL_SUB + { + $$ = $1; + parser_stack($$).id(ID_statement_list_accu_real_sub); + } + | TOK_ACCU_REAL_MUL + { + $$ = $1; + parser_stack($$).id(ID_statement_list_accu_real_mul); + } + | TOK_ACCU_REAL_DIV + { + $$ = $1; + parser_stack($$).id(ID_statement_list_accu_real_div); + } + | TOK_ACCU_DINT_ADD + { + $$ = $1; + parser_stack($$).id(ID_statement_list_accu_dint_add); + } + | TOK_ACCU_DINT_SUB + { + $$ = $1; + parser_stack($$).id(ID_statement_list_accu_dint_sub); + } + | TOK_ACCU_DINT_MUL + { + $$ = $1; + parser_stack($$).id(ID_statement_list_accu_dint_mul); + } + | TOK_ACCU_DINT_DIV + { + $$ = $1; + parser_stack($$).id(ID_statement_list_accu_dint_div); + } + ; + +IL_Operand: + Constant + | Variable_Access + ; + +Variable_Access: + '#' Variable_Name + { + newstack($$); + parser_stack($$) = + symbol_exprt::typeless(parser_stack($2).get(ID_value)); + } + | Variable_Name + ; + +Constant: + TOK_INT_LITERAL + | TOK_BOOL_LITERAL + ; + +IL_Expr_Operator: + TOK_AND + { + $$ = $1; + parser_stack($$).id(ID_statement_list_and); + } + | TOK_AND_NOT + { + $$ = $1; + parser_stack($$).id(ID_statement_list_and_not); + } + | TOK_OR + { + $$ = $1; + parser_stack($$).id(ID_statement_list_or); + } + | TOK_OR_NOT + { + $$ = $1; + parser_stack($$).id(ID_statement_list_or_not); + } + | TOK_XOR + { + $$ = $1; + parser_stack($$).id(ID_statement_list_xor); + } + | TOK_XOR_NOT + { + $$ = $1; + parser_stack($$).id(ID_statement_list_xor_not); + } + ; + +IL_Simple_Inst_List: + IL_Simple_Inst_List IL_Simple_Instruction + { + $$ = $1; + parser_stack($$).add_to_operands(std::move(parser_stack($2))); + } + | IL_Simple_Instruction + { + newstack($$); + parser_stack($$).id(ID_statement_list_instructions); + parser_stack($$).add_to_operands(std::move(parser_stack($1))); + } + ; + +Opt_Simple_Inst_List: + IL_Simple_Inst_List + | /* nothing */ + { + newstack($$); + parser_stack($$).id(ID_statement_list_instructions); + } + ; + +IL_Simple_Instruction: + IL_Simple_Operation';' + | IL_Expr';' + ; +%% diff --git a/src/statement-list/scanner.l b/src/statement-list/scanner.l new file mode 100644 index 00000000000..1f0a6b67724 --- /dev/null +++ b/src/statement-list/scanner.l @@ -0,0 +1,191 @@ +%{ + +// This scanner is based on the IEC standard 61131-3 which, among other things, +// includes a BNF grammar for the Instruction List (IL) language. The +// Statement List language (STL) by Siemens complies with the standards +// defined by the IEC, although some modifications were made for compatibility +// reasons. As a consequence, the general language structure specified by the +// IEC is similar to the structure of STL, but there are differences between +// their syntax and some language features (In general, Siemens implements more +// language features in STL than described in the standard). + +// Conversion from yytext to expressions. +#include "converters/convert_bool_literal.h" +#include "converters/convert_int_literal.h" +#include "converters/convert_real_literal.h" +#include "converters/convert_string_value.h" + +// Disable warnings for generated file. +#include +#include +#include + +// Visual Studio +#if defined _MSC_VER +// Disable warning for signed/unsigned mismatch. +#pragma warning(disable:4365) +// Disable warning for macro re-definition: Flex conditionally defines +// INT32_MAX et al. and thus they are set before library headers get to define +// them. +#pragma warning(disable:4005) +#endif + +// Conditionally disable unistd header since it does not exist when building on +// Windows. +#ifdef _WIN32 +#define YY_NO_UNISTD_H +static int isatty(int) { return 0; } +#endif + +// Value inside of statement_list_parser.h. +#define PARSER statement_list_parser + +// Sets the type of yystatement_listlval so that it can be used as the stack +// index. +#define YYSTYPE unsigned + +// For access to the stack and the parser itself. +#include "statement_list_parser.h" + + // To get the token types from Bison. +#include "statement_list_y.tab.h" + +// Add an empty expression to the stack, set yystatement_listlval to the +// position of that element and set the source location to the new expression. +#define loc() \ + { newstack(yystatement_listlval); \ + PARSER.set_source_location(parser_stack(yystatement_listlval)); } + +#ifdef STATEMENT_LIST_DEBUG +extern int yystatement_listdebug; +#endif + +void statement_list_scanner_init() +{ +#ifdef STATEMENT_LIST_DEBUG + yystatement_listdebug=1; +#endif + YY_FLUSH_BUFFER; + BEGIN(0); +} +%} +%option noyywrap +%option noinput +%option nounput + + +%% +[\(\):\.,;#=] { loc(); return yytext[0]; } +[\t\r\n ] ; +:= { loc(); return TOK_ASSIGNMENT; } +BEGIN { loc(); return TOK_BEGIN; } +VERSION { loc(); return TOK_VERSION; } +FUNCTION_BLOCK { loc(); return TOK_FUNCTION_BLOCK; } +END_FUNCTION_BLOCK { loc(); return TOK_END_FUNCTION_BLOCK; } +FUNCTION { loc(); return TOK_FUNCTION; } +END_FUNCTION { loc(); return TOK_END_FUNCTION; } +VAR_INPUT { loc(); return TOK_VAR_INPUT; } +VAR_OUTPUT { loc(); return TOK_VAR_OUTPUT; } +END_VAR { loc(); return TOK_END_VAR; } +NETWORK { loc(); return TOK_NETWORK; } +TITLE { loc(); return TOK_TITLE; } +Int { loc(); return TOK_INT; } +DInt { loc(); return TOK_DINT; } +Bool { loc(); return TOK_BOOL; } +Real { loc(); return TOK_REAL; } +Void { loc(); return TOK_VOID; } +L { loc(); return TOK_LOAD; } +T { loc(); return TOK_TRANSFER; } +NOP { loc(); return TOK_NOP; } +A { loc(); return TOK_AND; } +AN { loc(); return TOK_AND_NOT; } +O { loc(); return TOK_OR; } +ON { loc(); return TOK_OR_NOT; } +X { loc(); return TOK_XOR; } +XN { loc(); return TOK_XOR_NOT; } +\+ { loc(); return TOK_CONST_ADD; } +\+I { loc(); return TOK_ACCU_INT_ADD; } +\-I { loc(); return TOK_ACCU_INT_SUB; } +\*I { loc(); return TOK_ACCU_INT_MUL; } +\/I { loc(); return TOK_ACCU_INT_DIV; } +\+R { loc(); return TOK_ACCU_REAL_ADD; } +\-R { loc(); return TOK_ACCU_REAL_SUB; } +\*R { loc(); return TOK_ACCU_REAL_MUL; } +\/R { loc(); return TOK_ACCU_REAL_DIV; } +\+D { loc(); return TOK_ACCU_DINT_ADD; } +\-D { loc(); return TOK_ACCU_DINT_SUB; } +\*D { loc(); return TOK_ACCU_DINT_MUL; } +\/D { loc(); return TOK_ACCU_DINT_DIV; } + +[\+-]?[0-9]+ { + newstack(yystatement_listlval); + parser_stack(yystatement_listlval) = + convert_int_dec_literal(yytext); + PARSER.set_source_location( + parser_stack(yystatement_listlval)); + return TOK_INT_LITERAL; + } + +16#[0-9A-Fa-f]+ { + newstack(yystatement_listlval); + parser_stack(yystatement_listlval) = + convert_int_hex_literal(yytext); + PARSER.set_source_location( + parser_stack(yystatement_listlval)); + return TOK_INT_LITERAL; + } + +2#[0-9A-Fa-f]+ { + newstack(yystatement_listlval); + parser_stack(yystatement_listlval) = + convert_int_bit_literal(yytext); + PARSER.set_source_location( + parser_stack(yystatement_listlval)); + return TOK_INT_LITERAL; + } + +TRUE|FALSE { + newstack(yystatement_listlval); + parser_stack(yystatement_listlval) = + convert_bool_literal(yytext); + PARSER.set_source_location( + parser_stack(yystatement_listlval)); + return TOK_BOOL_LITERAL; + } + +(\+|-)?[0-9]+\.[0-9]+ { + newstack(yystatement_listlval); + parser_stack(yystatement_listlval) = + convert_real_literal(yytext); + PARSER.set_source_location( + parser_stack(yystatement_listlval)); + return TOK_REAL_LITERAL; + } + +\"[a-zA-Z_\.][a-zA-Z0-9_\.]*\" { + newstack(yystatement_listlval); + parser_stack(yystatement_listlval) = + convert_identifier(yytext); + PARSER.set_source_location( + parser_stack(yystatement_listlval)); + return TOK_IDENTIFIER; + } + +[a-zA-Z_\.][a-zA-Z0-9_\.]* { + newstack(yystatement_listlval); + parser_stack(yystatement_listlval) = + convert_title(yytext); + PARSER.set_source_location( + parser_stack(yystatement_listlval)); + return TOK_TITLE_VALUE; + } + +[a-zA-Z_\.][a-zA-Z0-9_\.]*: { + newstack(yystatement_listlval); + parser_stack(yystatement_listlval) = + convert_label(yytext); + PARSER.set_source_location( + parser_stack(yystatement_listlval)); + return TOK_LABEL; + } +%% diff --git a/src/statement-list/statement_list_parse_tree.cpp b/src/statement-list/statement_list_parse_tree.cpp new file mode 100644 index 00000000000..aa41e881934 --- /dev/null +++ b/src/statement-list/statement_list_parse_tree.cpp @@ -0,0 +1,129 @@ +/*******************************************************************\ + +Module: Statement List Language Parse Tree + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Parse Tree + +#include "statement_list_parse_tree.h" + +void statement_list_parse_treet::output(std::ostream &out) const +{ + for(const auto &function_block : function_blocks) + { + out << "============== Function Block ==============\n"; + function_block.output(out); + out << "\n"; + } + + for(const auto &function : functions) + { + out << "================= Function =================\n"; + function.output(out); + out << "\n"; + } +} + +void statement_list_parse_treet::functiont::output(std::ostream &out) const +{ + out << "Name: " << name << "\n"; + out << "Version: " << version << "\n\n"; + + out << "--------- Input Variables ----------\n\n"; + for(const auto &declaration : var_input) + { + declaration.output(out); + out << "\n\n"; + } + + out << "--------- In/Out Variables ---------\n\n"; + for(const auto &declaration : var_inout) + { + declaration.output(out); + out << "\n\n"; + } + + out << "--------- Output Variables ---------\n\n"; + for(const auto &declaration : var_output) + { + declaration.output(out); + out << "\n\n"; + } + + out << "------------- Networks -------------\n\n"; + for(const auto &network : networks) + { + network.output(out); + out << "\n"; + } +} + +void statement_list_parse_treet::function_blockt::output( + std::ostream &out) const +{ + statement_list_parse_treet::functiont::output(out); +} + +void statement_list_parse_treet::var_declarationt::output( + std::ostream &out) const +{ + out << variable.pretty() << "\n"; + out << " * initial_value: (default)"; +} + +void statement_list_parse_treet::networkt::output(std::ostream &out) const +{ + out << "Title: " << title.value_or("(none)") << "\n"; + out << "Instructions: "; + if(instructions.empty()) + out << "(none)"; + out << "\n"; + for(const auto &instruction : instructions) + { + instruction.output(out); + out << "\n"; + } +} + +void statement_list_parse_treet::instructiont::output(std::ostream &out) const +{ + for(const auto &token : tokens) + { + out << token.get_statement(); + for(const auto expr : token.operands()) + { + if(expr.id() == ID_symbol) + out << "\t" << expr.get(ID_identifier); + else if(expr.id() == ID_constant) + out << "\t" << expr.get(ID_value); + else + out << "\t" << expr.id(); + } + } +} + +void statement_list_parse_treet::add_function_block(function_blockt &block) +{ + function_blocks.push_back(std::move(block)); +} + +void statement_list_parse_treet::add_function(functiont &function) +{ + functions.push_back(std::move(function)); +} + +void statement_list_parse_treet::clear() +{ + function_blocks.clear(); + functions.clear(); +} + +void statement_list_parse_treet::swap(statement_list_parse_treet &other) +{ + function_blocks.swap(other.function_blocks); + functions.swap(other.functions); +} diff --git a/src/statement-list/statement_list_parse_tree.h b/src/statement-list/statement_list_parse_tree.h new file mode 100644 index 00000000000..66ddbebe40d --- /dev/null +++ b/src/statement-list/statement_list_parse_tree.h @@ -0,0 +1,211 @@ +/*******************************************************************\ + +Module: Statement List Language Parse Tree + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Parse Tree + +#ifndef CPROVER_STATEMENT_LIST_STATEMENT_LIST_PARSE_TREE_H +#define CPROVER_STATEMENT_LIST_STATEMENT_LIST_PARSE_TREE_H + +#include +#include + +/// Intermediate representation of a parsed Statement List file before +/// converting it into a goto program. Contains all data structures that are +/// necessary for describing Statement List functions and function blocks. +class statement_list_parse_treet +{ +public: + // Disallow copy construction and copy assignment, but allow move construction + // and move assignment. + statement_list_parse_treet(const statement_list_parse_treet &) = delete; + statement_list_parse_treet & + operator=(const statement_list_parse_treet &) = delete; + statement_list_parse_treet(statement_list_parse_treet &&) = default; + statement_list_parse_treet & + operator=(statement_list_parse_treet &&) = default; + statement_list_parse_treet() = default; + + /// Removes all functions and function blocks from the parse tree. + void clear(); + + /// Prints the tree in a human-readable form to the given output stream. + void output(std::ostream &out) const; + + /// Struct for a single variable declaration in Statement List. Includes + /// identifier, type and an optional assignment. + struct var_declarationt + { + symbol_exprt variable; + optionalt assignment; + + explicit var_declarationt(irep_idt &identifier, typet &type) + : variable(symbol_exprt(identifier, type)) + { + } + + /// Prints the declaration in a human-readable form to the given output + /// stream. + void output(std::ostream &out) const; + }; + using var_declarationst = std::list; + + /// Represents a regular Statement List instruction which consists out of + /// one or more codet tokens. + struct instructiont + { + std::vector tokens; + + /// Adds a codet element to the list of all tokens. + void add_token(codet &token) + { + tokens.push_back(token); + } + + /// Prints the instruction in a human-readable form to the given output + /// stream. + void output(std::ostream &out) const; + }; + using instructionst = std::list; + + /// Representation of a network in Siemens TIA. Networks are used to divide + /// multiple Statement List instructions into simpler parts. A function or + /// function block contains one or more networks. A network can have a title + /// and may contain zero or more instructions. + struct networkt + { + optionalt title; + instructionst instructions; + + /// Sets the title of the network to a specific value. + /// \param value: New title. Use an empty string to indicate that there is + /// no title. + void set_title(std::string &value) + { + if(value.empty()) + title.reset(); + else + title = value; + } + + /// Adds an instruction to the network. + void add_instruction(instructiont &inst) + { + instructions.push_back(inst); + } + + /// Create the network with a specific \p title. + explicit networkt(std::string &title) + { + set_title(title); + } + + networkt() + { + } + + /// Prints the network in a human-readable form to the given output stream. + void output(std::ostream &out) const; + }; + using networkst = std::list; + + /// Structure for a simple function in Statement List. Includes fields for + /// its name, version, variable declarations and networks. + struct functiont + { + // Header + irep_idt name; + float version; + + // Variable declarations + var_declarationst var_input; + var_declarationst var_inout; + var_declarationst var_output; + + // Body + networkst networks; + + /// Create the function \p name with a specific \p version. + explicit functiont(const irep_idt &name, const float version) + : name(name), version(version) + { + } + + // Disallow copy construction and copy assignment, but allow move + // construction and move assignment. + functiont(const functiont &) = delete; + functiont &operator=(const functiont &) = delete; + functiont(functiont &&) = default; + functiont &operator=(functiont &&) = default; + + /// Adds a variable declaration to the list of input variables. + void add_var_input_entry(var_declarationt &declaration) + { + var_input.push_back(declaration); + } + + /// Adds a variable declaration to the list of inout variables. + void add_var_inout_entry(var_declarationt &declaration) + { + var_inout.push_back(declaration); + } + + /// Adds a variable declaration to the list of output variables. + void add_var_output_entry(var_declarationt &declaration) + { + var_output.push_back(declaration); + } + + /// Adds a network to the function. + void add_network(networkt &network) + { + networks.push_back(network); + } + + /// Prints the function in a human-readable form to the given output + /// stream. + virtual void output(std::ostream &out) const; + }; + using functionst = std::list; + + /// Structure for a simple function block in Statement List. Includes fields + /// for its name, version, variable declarations and networks. + struct function_blockt : functiont + { + /// Create the function block \p name with a specific \p version. + explicit function_blockt(const irep_idt &name, const float version) + : functiont(name, version) + { + } + + // Disallow copy construction and copy assignment, but allow move + // construction and move assignment. + function_blockt(const function_blockt &) = delete; + function_blockt &operator=(const function_blockt &) = delete; + function_blockt(function_blockt &&) = default; + function_blockt &operator=(function_blockt &&) = default; + + /// Prints the function block in a human-readable form to the given output + /// stream. + void output(std::ostream &out) const override; + }; + using function_blockst = std::list; + + /// Adds a function block to the parse tree. + void add_function_block(function_blockt &block); + /// Adds a function to the parse tree. + void add_function(functiont &function); + /// Swaps the contents of the parse tree with the parameter. + void swap(statement_list_parse_treet &other); + + // Lists of functions and function blocks. + function_blockst function_blocks; + functionst functions; +}; + +#endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_PARSE_TREE_H diff --git a/src/statement-list/statement_list_parser.cpp b/src/statement-list/statement_list_parser.cpp new file mode 100644 index 00000000000..5563f261b00 --- /dev/null +++ b/src/statement-list/statement_list_parser.cpp @@ -0,0 +1,254 @@ +/*******************************************************************\ + +Module: Statement List Language Parser + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Parser + +#include "statement_list_parser.h" + +#include "statement_list_parse_tree.h" +#include +#include +#include + +statement_list_parsert statement_list_parser; + +extern char *yystatement_listtext; + +int yystatement_listerror(const std::string &error) +{ + statement_list_parser.parse_error(error, yystatement_listtext); + return 0; +} + +void statement_list_parsert::add_function_block(exprt &block) +{ + INVARIANT( + block.id() == ID_statement_list_function_block, + "Root expression ID should be ID_statement_list_function_block"); + + // Generate new function block. + statement_list_parse_treet::function_blockt fb{find_name(block), + find_version(block)}; + + // Fill the block with networks and variables. + exprt var_list = find_variable_list(block); + find_variables(fb, var_list); + exprt network_list = find_network_list(block); + find_networks(fb, network_list); + + parse_tree.add_function_block(fb); +} + +void statement_list_parsert::add_function(exprt &function) +{ + INVARIANT( + function.id() == ID_statement_list_function, + "Expression ID should be statement_list_function"); + + // Generate new function. + statement_list_parse_treet::functiont fn{find_name(function), + find_version(function)}; + + // Fill the function with networks and variables. + exprt var_decls = find_variable_list(function); + find_variables(fn, var_decls); + exprt network_list = find_network_list(function); + find_networks(fn, network_list); + + parse_tree.add_function(fn); +} + +void statement_list_parsert::clear() +{ + parsert::clear(); + parse_tree.clear(); +} + +void statement_list_parsert::print_tree(std::ostream &out) const +{ + parse_tree.output(out); +} + +irep_idt statement_list_parsert::find_name(const exprt &root) +{ + for(exprt op : root.operands()) + { + if(op.get(ID_statement_list_type) == ID_statement_list_identifier) + return op.get(ID_value); + } + + UNREACHABLE; // Root expression should always have a name +} + +float statement_list_parsert::find_version(const exprt &root) +{ + for(exprt op : root.operands()) + { + if(op.type().id() == ID_statement_list_version) + return std::stof(op.get(ID_value).c_str()); + } + + UNREACHABLE; // Root expression should always have a version +} + +exprt statement_list_parsert::find_variable_list(const exprt &root) +{ + for(exprt op : root.operands()) + { + if(op.id() == ID_statement_list_var_decls) + return op; + } + UNREACHABLE; // Root expression should always have a variable list +} + +exprt statement_list_parsert::find_network_list(const exprt &root) +{ + for(exprt op : root.operands()) + { + if(op.id() == ID_statement_list_networks) + return op; + } + + UNREACHABLE; // Root expression should always have a network list +} + +void statement_list_parsert::find_variables( + statement_list_parse_treet::functiont &function, + const exprt &var_decls) +{ + for(exprt decls : var_decls.operands()) + { + if(decls.id() == ID_statement_list_var_input) + fill_input_vars(function, decls); + else if(decls.id() == ID_statement_list_var_inout) + fill_output_vars(function, decls); + else if(decls.id() == ID_statement_list_var_output) + fill_output_vars(function, decls); + } +} + +void statement_list_parsert::fill_input_vars( + statement_list_parse_treet::functiont &function, + const exprt &input_vars) +{ + for(exprt entry : input_vars.operands()) + { + irep_idt identifier; + typet type; + for(exprt part : entry.operands()) + { + if(part.get(ID_statement_list_type) == ID_statement_list_identifier) + identifier = part.get(ID_value); + else + type = typet(part.id()); + } + + statement_list_parse_treet::var_declarationt declaration(identifier, type); + function.add_var_input_entry(declaration); + } +} + +void statement_list_parsert::fill_inout_vars( + statement_list_parse_treet::functiont &function, + const exprt &inout_vars) +{ + for(exprt entry : inout_vars.operands()) + { + irep_idt identifier; + typet type; + for(exprt part : entry.operands()) + { + if(part.get(ID_statement_list_type) == ID_statement_list_identifier) + identifier = part.get(ID_value); + else + type = typet(part.id()); + } + + statement_list_parse_treet::var_declarationt declaration(identifier, type); + function.add_var_inout_entry(declaration); + } +} + +void statement_list_parsert::fill_output_vars( + statement_list_parse_treet::functiont &function, + const exprt &output_vars) +{ + for(exprt entry : output_vars.operands()) + { + irep_idt identifier; + typet type; + for(exprt part : entry.operands()) + { + if(part.get(ID_statement_list_type) == ID_statement_list_identifier) + identifier = part.get(ID_value); + else + type = typet(part.id()); + } + + statement_list_parse_treet::var_declarationt declaration(identifier, type); + function.add_var_output_entry(declaration); + } +} + +void statement_list_parsert::find_networks( + statement_list_parse_treet::functiont &function, + const exprt &network_list) +{ + for(exprt expr_network : network_list.operands()) + { + std::string title(find_network_title(expr_network)); + statement_list_parse_treet::networkt network(title); + exprt instructions = find_network_instructions(expr_network); + find_instructions(network, instructions); + function.add_network(network); + } +} + +std::string statement_list_parsert::find_network_title(const exprt &network) +{ + for(exprt network_element : network.operands()) + { + if(network_element.get(ID_statement_list_type) == ID_statement_list_title) + return network_element.get(ID_value).c_str(); + } + UNREACHABLE; // Network expression should always have a title +} + +exprt statement_list_parsert::find_network_instructions(const exprt &network) +{ + for(exprt network_element : network.operands()) + { + if(network_element.id() == ID_statement_list_instructions) + return network_element; + } + UNREACHABLE; // Network expression should always have an instruction list +} + +void statement_list_parsert::find_instructions( + statement_list_parse_treet::networkt &network, + const exprt &instructions) +{ + for(exprt expr_instruction : instructions.operands()) + { + statement_list_parse_treet::instructiont instruction; + codet code_token(expr_instruction.op0().id()); + for(exprt expr : expr_instruction.operands()) + { + if(expr.id() != ID_nil && expr.id() != code_token.get_statement()) + code_token.add_to_operands(expr); + } + instruction.add_token(code_token); + network.add_instruction(instruction); + } +} + +void statement_list_parsert::swap_tree(statement_list_parse_treet &other) +{ + parse_tree.swap(other); +} diff --git a/src/statement-list/statement_list_parser.h b/src/statement-list/statement_list_parser.h new file mode 100644 index 00000000000..2797719547c --- /dev/null +++ b/src/statement-list/statement_list_parser.h @@ -0,0 +1,159 @@ +/*******************************************************************\ + +Module: Statement List Language Parser + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Parser + +#ifndef CPROVER_STATEMENT_LIST_STATEMENT_LIST_PARSER_H +#define CPROVER_STATEMENT_LIST_STATEMENT_LIST_PARSER_H + +#include + +#include "statement_list_parse_tree.h" + +// Defined in statement_list_y.tab.cpp. +int yystatement_listparse(); + +/// Responsible for starting the parse process and to translate the result into +/// a statement_list_parse_treet. This parser works by using the expression +/// stack of its base class. During the parse process, expressions with +/// different IDs and types are put on this stack and may get associated with +/// each other. This way a tree structure with expressions as nodes is created. +/// If the parser encounters a function or function block, it invokes +/// add_function() or add_function_block(). These functions then convert the +/// expression tree structure into a statement_list_parse_treet::functiont or +/// statement_list_parse_treet::function_blockt and add it to the +/// statement_list_parse_treet. See the implementation of scanner.l and +/// parser.y for details about how and when the stack operations are performed. +class statement_list_parsert : public parsert +{ +public: + /// Starts the parsing process and saves the result inside of this instance's + /// parse tree. + /// \return: False if successful. + bool parse() override + { + return yystatement_listparse() != 0; + } + + /// Adds a function block to the parse tree by converting the \p block + /// expression tree. + void add_function_block(exprt &block); + + /// Adds a function to the parse tree by converting the \p function + /// expression tree. + void add_function(exprt &function); + + /// Prints the parse tree of this instance to the given output stream. + void print_tree(std::ostream &out) const; + + /// Swaps the contents of the parse tree of this instance with \p other. + void swap_tree(statement_list_parse_treet &other); + + /// Removes all functions and function blocks from the parse tree and + /// clears the internal state of the parser. + void clear() override; + +private: + statement_list_parse_treet parse_tree; + + /// Searches for the name of the function element inside of its root + /// expression. + /// \param root: Expression that includes the element's name as a + /// direct operand. + /// \return The name of the function element. + static irep_idt find_name(const exprt &root); + + /// Searches for the version of the function element inside of its root + /// expression. + /// \param root: Expression that includes the element's version as a + /// direct operand. + /// \return The version of the function element. + static float find_version(const exprt &root); + + /// Searches for the variable list of the function element inside of its root + /// expression. + /// \param root: Expression that includes the element's variable list as a + /// direct operand. + /// \return The variable list of the function element. + static exprt find_variable_list(const exprt &root); + + /// Adds all valid variable declarations to the given function element. + /// \param function: The function to which the variables belong. + /// \param var_decls: The root expression of a valid variable list. + static void find_variables( + statement_list_parse_treet::functiont &function, + const exprt &var_decls); + + /// Adds all input variable declarations to the given function element. + /// \param function: The function to which the variables belong. + /// \param input_vars: The root expression of a input variable list. + static void fill_input_vars( + statement_list_parse_treet::functiont &function, + const exprt &input_vars); + + /// Adds all input variable declarations to the given function element. + /// \param function: The function to which the variables belong. + /// \param inout_vars: The root expression of a inout variable list. + static void fill_inout_vars( + statement_list_parse_treet::functiont &function, + const exprt &inout_vars); + + /// Adds all input variable declarations to the given function element. + /// \param function: The function to which the variables belong. + /// \param output_vars: The root expression of a output variable list. + static void fill_output_vars( + statement_list_parse_treet::functiont &function, + const exprt &output_vars); + + /// Searches for the network list of the function element inside of its root + /// expression. + /// \param root: Expression that includes the element's network list as a + /// direct operand. + /// \return The network list of the function element. + static exprt find_network_list(const exprt &root); + + /// Adds all valid networks and their instructions to the given function + /// element. + /// \param function: The function to which the networks belong. + /// \param network_list: The root expression of a valid network list. + static void find_networks( + statement_list_parse_treet::functiont &function, + const exprt &network_list); + + /// Searches for the title of a network inside of its root expression. + /// \param network: Expression that includes the network's title as a + /// direct operand. + /// \return The title of the network. + static std::string find_network_title(const exprt &network); + + /// Searches for the instruction list of a network inside of its root + /// expression. + /// \param network: Expression that includes the network's instructions as a + /// direct operand. + /// \return The instruction list expression of the network. + static exprt find_network_instructions(const exprt &network); + + /// Adds all valid instructions to the given network. + /// \param network: The network to which the instructions belong. + /// \param instructions: The root expression of a valid instruction list. + static void find_instructions( + statement_list_parse_treet::networkt &network, + const exprt &instructions); +}; + +extern statement_list_parsert statement_list_parser; + +/// Forwards any errors that are encountered during the parse process. This +/// function gets called by the generated files of flex and bison. +/// \param error: Error message. +/// \return Always 0. +int yystatement_listerror(const std::string &error); +void statement_list_scanner_init(); + +#endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_PARSER_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index b2bfa73fdb7..5b21c8f388d 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -761,6 +761,47 @@ IREP_ID_ONE(__sync_or_and_fetch) IREP_ID_ONE(__sync_sub_and_fetch) IREP_ID_ONE(__sync_val_compare_and_swap) IREP_ID_ONE(__sync_xor_and_fetch) +IREP_ID_ONE(statement_list_type) +IREP_ID_ONE(statement_list_function) +IREP_ID_ONE(statement_list_function_block) +IREP_ID_ONE(statement_list_version) +IREP_ID_ONE(statement_list_var_input) +IREP_ID_ONE(statement_list_var_inout) +IREP_ID_ONE(statement_list_var_output) +IREP_ID_ONE(statement_list_var_entry) +IREP_ID_ONE(statement_list_var_decls) +IREP_ID_ONE(statement_list_network) +IREP_ID_ONE(statement_list_networks) +IREP_ID_ONE(statement_list_title) +IREP_ID_ONE(statement_list_identifier) +IREP_ID_ONE(statement_list_int) +IREP_ID_ONE(statement_list_dint) +IREP_ID_ONE(statement_list_bool) +IREP_ID_ONE(statement_list_real) +IREP_ID_ONE(statement_list_load) +IREP_ID_ONE(statement_list_transfer) +IREP_ID_ONE(statement_list_nop) +IREP_ID_ONE(statement_list_const_add) +IREP_ID_ONE(statement_list_accu_int_add) +IREP_ID_ONE(statement_list_accu_int_sub) +IREP_ID_ONE(statement_list_accu_int_mul) +IREP_ID_ONE(statement_list_accu_int_div) +IREP_ID_ONE(statement_list_accu_real_add) +IREP_ID_ONE(statement_list_accu_real_sub) +IREP_ID_ONE(statement_list_accu_real_mul) +IREP_ID_ONE(statement_list_accu_real_div) +IREP_ID_ONE(statement_list_accu_dint_add) +IREP_ID_ONE(statement_list_accu_dint_sub) +IREP_ID_ONE(statement_list_accu_dint_mul) +IREP_ID_ONE(statement_list_accu_dint_div) +IREP_ID_ONE(statement_list_and) +IREP_ID_ONE(statement_list_and_not) +IREP_ID_ONE(statement_list_or) +IREP_ID_ONE(statement_list_or_not) +IREP_ID_ONE(statement_list_xor) +IREP_ID_ONE(statement_list_xor_not) +IREP_ID_ONE(statement_list_instruction) +IREP_ID_ONE(statement_list_instructions) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree From b900edc73413be567b282ee00394a7c1ddd9c40a Mon Sep 17 00:00:00 2001 From: Matthias Weiss Date: Mon, 20 May 2019 15:52:05 +0100 Subject: [PATCH 2/3] Integrate STL parser into CBMC executable 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. --- CMakeLists.txt | 1 + src/CMakeLists.txt | 1 + src/Makefile | 3 +- src/cbmc/CMakeLists.txt | 1 + src/cbmc/Makefile | 3 +- src/cbmc/cbmc_languages.cpp | 4 +- src/cbmc/module_dependencies.txt | 1 + src/statement-list/CMakeLists.txt | 14 ++ src/statement-list/Makefile | 54 ++++++ .../converters/expr2statement_list.cpp | 35 ++++ .../converters/expr2statement_list.h | 30 ++++ .../statement_list_language.cpp | 158 ++++++++++++++++++ src/statement-list/statement_list_language.h | 116 +++++++++++++ .../statement_list_typecheck.cpp | 116 +++++++++++++ src/statement-list/statement_list_typecheck.h | 71 ++++++++ unit/CMakeLists.txt | 1 + unit/Makefile | 1 + 17 files changed, 607 insertions(+), 3 deletions(-) create mode 100644 src/statement-list/CMakeLists.txt create mode 100644 src/statement-list/Makefile create mode 100644 src/statement-list/converters/expr2statement_list.cpp create mode 100644 src/statement-list/converters/expr2statement_list.h create mode 100644 src/statement-list/statement_list_language.cpp create mode 100644 src/statement-list/statement_list_language.h create mode 100644 src/statement-list/statement_list_typecheck.cpp create mode 100644 src/statement-list/statement_list_typecheck.h diff --git a/CMakeLists.txt b/CMakeLists.txt index 26732212843..f9faec981b1 100644 --- 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 index ecc5aead4c6..b5557658c4c 100644 --- 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 index 9a9eba04d04..ace5c03bda5 100644 --- 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 index 82b6ab9cdc3..6d922df38c2 100644 --- 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 index 45b80870700..f2e80d151a0 100644 --- 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 index 7d336f7defb..cbf142cf017 100644 --- a/src/cbmc/cbmc_languages.cpp +++ b/src/cbmc/cbmc_languages.cpp @@ -16,14 +16,16 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #ifdef HAVE_JSIL -#include +# include #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 index ca9b882227d..9c9fd45de75 100644 --- 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 new file mode 100644 index 00000000000..a2b228af8a6 --- /dev/null +++ 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 new file mode 100644 index 00000000000..e6b58d5e026 --- /dev/null +++ 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 new file mode 100644 index 00000000000..7ecf4cf5ff1 --- /dev/null +++ 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 + +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 new file mode 100644 index 00000000000..3d3bcfa6ba0 --- /dev/null +++ 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 + +/// 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 new file mode 100644 index 00000000000..2341aad626b --- /dev/null +++ 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 +#include +#include + +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 &modules) +{ + modules.insert(get_base_name(parse_path, true)); +} + +std::set statement_list_languaget::extensions() const +{ + return {"awl"}; +} + +std::unique_ptr new_statement_list_language() +{ + return util_make_unique(); +} + +std::unique_ptr statement_list_languaget::new_language() +{ + return util_make_unique(); +} + +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 new file mode 100644 index 00000000000..106afc65213 --- /dev/null +++ b/src/statement-list/statement_list_language.h @@ -0,0 +1,116 @@ +/*******************************************************************\ + +Module: Statement List Language Interface + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Interface + +#ifndef CPROVER_STATEMENT_LIST_STATEMENT_LIST_LANGUAGE_H +#define CPROVER_STATEMENT_LIST_STATEMENT_LIST_LANGUAGE_H + +#include "statement_list_parse_tree.h" +#include +#include + +/// Implements the language interface for the Statement List language. +/// Includes functions for parsing input streams and for converting the +/// resulting parse tree into a symbol table. +class statement_list_languaget : public languaget +{ +public: + /// Sets language specific options. + /// \param options: Options that shall apply during the parse and + /// typecheck process. + void set_language_options(const optionst &options) override; + + /// Parses input given by \p instream and saves this result to this + /// instance's parse tree. + /// \param instream: Input to parse. + /// \param path: Path of the input. + /// \return: False if successful. + bool parse(std::istream &instream, const std::string &path) override; + + /// Currently unused. + bool generate_support_functions(symbol_tablet &symbol_table) override; + + /// Converts the current parse tree into a symbol table. + /// \param [out] symbol_table: Object that shall be filled by this function. + /// If the symbol table is not empty when calling this function, its + /// contents are merged with the new entries. + /// \param module: Name of the file that has been parsed. + /// \param keep_file_local: Set to true if local variables of this module + /// should be included in the table. + /// \return: False if no errors occurred, true otherwise. + bool typecheck( + symbol_tablet &symbol_table, + const std::string &module, + const bool keep_file_local) override; + + bool + typecheck(symbol_tablet &symbol_table, const std::string &module) override; + + bool can_keep_file_local() override; + + /// Prints the parse tree to the given output stream. + void show_parse(std::ostream &out) override; + + // Constructor and destructor. + ~statement_list_languaget() override; + statement_list_languaget(); + + /// Formats the given expression in a language-specific way. + /// \param expr: the expression to format + /// \param code: the formatted expression + /// \param ns: a namespace + /// \return false if conversion succeeds + bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) + override; + + /// Formats the given type in a language-specific way. + /// \param type: the type to format + /// \param code: the formatted type + /// \param ns: a namespace + /// \return false if conversion succeeds + bool from_type(const typet &type, std::string &code, const namespacet &ns) + override; + + /// Encodes the given type in a language-specific way. + /// \param type: the type to encode + /// \param name: the encoded type + /// \param ns: a namespace + /// \return false if the conversion succeeds + bool type_to_name(const typet &type, std::string &name, const namespacet &ns) + override; + + /// Parses the given string into an expression. + /// \param code: the string to parse + /// \param module: prefix to be used for identifiers + /// \param expr: the parsed expression + /// \param ns: a namespace + /// \return false if the conversion succeeds + bool to_expr( + const std::string &code, + const std::string &module, + exprt &expr, + const namespacet &ns) override; + + std::unique_ptr new_language() override; + + // ID, description, extensions, modules. + std::string id() const override; + std::string description() const override; + std::set extensions() const override; + void modules_provided(std::set &modules) override; + +private: + statement_list_parse_treet parse_tree; + std::string parse_path; +}; + +std::unique_ptr new_statement_list_language(); + +#endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_LANGUAGE_H diff --git a/src/statement-list/statement_list_typecheck.cpp b/src/statement-list/statement_list_typecheck.cpp new file mode 100644 index 00000000000..12d1ad01cdd --- /dev/null +++ b/src/statement-list/statement_list_typecheck.cpp @@ -0,0 +1,116 @@ +/*******************************************************************\ + +Module: Statement List Language Type Checking + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Type Checking + +#include "statement_list_typecheck.h" + +#include +#include +#include +#include + +bool statement_list_typecheck( + statement_list_parse_treet &parse_tree, + symbol_tablet &symbol_table, + const std::string &module, + message_handlert &message_handler) +{ + statement_list_typecheckt stl_typecheck( + parse_tree, symbol_table, module, message_handler); + + return stl_typecheck.typecheck_main(); +} + +void statement_list_typecheckt::typecheck() +{ + for(const auto &fn : parse_tree.functions) + { + typecheck_function(fn); + } + + for(const auto &fb : parse_tree.function_blocks) + { + typecheck_function_block(fb); + } +} + +void statement_list_typecheckt::typecheck_function_block( + const statement_list_parse_treet::function_blockt &function_block) +{ + symbolt fb_sym; + fb_sym.module = module; + code_typet::parameterst params = typecheck_fb_params(function_block); + typet return_type(ID_void); + fb_sym.type = code_typet(params, return_type); + symbol_table.add(fb_sym); + typecheck_statement_list_networks(function_block.networks); + // TODO: Expand function. + // The complete function body is missing. +} + +void statement_list_typecheckt::typecheck_function( + const statement_list_parse_treet::functiont &function) +{ + // TODO: Implement. + // This can be done in a similar way as with function blocks. See the Siemens + // documentation for details about the key differences between functions and + // function blocks. + return; +} + +code_typet::parameterst statement_list_typecheckt::typecheck_fb_params( + const statement_list_parse_treet::function_blockt &function_block) +{ + code_typet::parameterst params; + + // Input parameters (read-only, are copied* to the instance data block upon + // calling it) + // *TODO: Implement call by reference for structured data types like strings. + for(const auto &declaration : function_block.var_input) + { + typet converted_type = + typecheck_statement_list_type(declaration.variable.type()); + code_typet::parametert param{converted_type}; + params.push_back(param); + } + + // Inout parameters (read and write) + for(const auto &declaration : function_block.var_output) + { + typet converted_type = + typecheck_statement_list_type(declaration.variable.type()); + code_typet::parametert param{converted_type}; + params.push_back(param); + } + + // Output parameters (write-only, are read by the caller after fb execution) + for(const auto &declaration : function_block.var_output) + { + typet converted_type = + typecheck_statement_list_type(declaration.variable.type()); + code_typet::parametert param{converted_type}; + params.push_back(param); + } + return params; +} + +typet statement_list_typecheckt::typecheck_statement_list_type( + const typet &stl_type) +{ + return std::move(stl_type); +} + +void statement_list_typecheckt::typecheck_statement_list_networks( + const statement_list_parse_treet::networkst &) +{ + // TODO: Implement function. + // This function should typecheck the instructions in every STL network. + return; +} diff --git a/src/statement-list/statement_list_typecheck.h b/src/statement-list/statement_list_typecheck.h new file mode 100644 index 00000000000..d68721fc67e --- /dev/null +++ b/src/statement-list/statement_list_typecheck.h @@ -0,0 +1,71 @@ +/*******************************************************************\ + +Module: Statement List Language Type Checking + +Author: Matthias Weiss, matthias.weiss@diffblue.com + +\*******************************************************************/ + +/// \file +/// Statement List Language Type Checking + +#ifndef CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H +#define CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H + +#include +#include + +#include "statement_list_parse_tree.h" + +/// Create a new statement_list_typecheckt object and perform a type check to +/// fill the symbol table. +/// \param parse_tree: Parse tree generated by parsing a Statement List file. +/// \param [out] symbol_table: Object that shall be filled by this function. +/// If the symbol table is not empty when calling this function, its contents +/// are merged with the new entries. +/// \param module: Name of the file that has been parsed. +/// \param message_handler: Used to provide debug information and error +/// messages. +/// \return: False if no errors occurred, true otherwise. +bool statement_list_typecheck( + statement_list_parse_treet &parse_tree, + symbol_tablet &symbol_table, + const std::string &module, + message_handlert &message_handler); + +/// Class for encapsulating the current state of the type check. +class statement_list_typecheckt : public typecheckt +{ +public: + statement_list_typecheckt( + statement_list_parse_treet &parse_tree, + symbol_tablet &symbol_table, + const std::string &module, + message_handlert &message_handler) + : typecheckt(message_handler), + parse_tree(parse_tree), + symbol_table(symbol_table), + module(module) + { + } + + void typecheck() override; + void + typecheck_function(const statement_list_parse_treet::functiont &function); + void typecheck_function_block( + const statement_list_parse_treet::function_blockt &function_block); + +private: + statement_list_parse_treet &parse_tree; + // std::vector accumulator; + symbol_tablet &symbol_table; + const irep_idt module; + + code_typet::parameterst typecheck_fb_params( + const statement_list_parse_treet::function_blockt &function_block); + typet typecheck_statement_list_type(const typet &standard_text_type); + void typecheck_statement_list_networks( + const statement_list_parse_treet::networkst &networks); +}; + +#endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index 1f69c26cbb6..6a765e74e95 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -57,6 +57,7 @@ target_link_libraries( goto-symex cbmc-lib json-symtab-language + statement-list ) add_test( diff --git a/unit/Makefile b/unit/Makefile index f0c67575899..2ac7e4aad98 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -155,6 +155,7 @@ CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \ ../src/assembler/assembler$(LIBEXT) \ ../src/analyses/analyses$(LIBEXT) \ ../src/solvers/solvers$(LIBEXT) \ + ../src/statement-list/statement-list$(LIBEXT) \ $(BMC_DEPS) # Empty last line From 2ba1361886efb5d6949e453440ee2e8b26c8c4fc Mon Sep 17 00:00:00 2001 From: Matthias Weiss Date: Mon, 20 May 2019 18:01:10 +0100 Subject: [PATCH 3/3] Add Statement List regression tests Includes tests for simple integer additions/multiplications, multiple functions/function blocks and for dividing two floats. --- regression/CMakeLists.txt | 1 + regression/Makefile | 1 + regression/statement-list/Add_Int/main.awl | 24 +++++++++++++++++++ regression/statement-list/Add_Int/test.desc | 18 ++++++++++++++ regression/statement-list/CMakeLists.txt | 3 +++ regression/statement-list/Div_Real/main.awl | 24 +++++++++++++++++++ regression/statement-list/Div_Real/test.desc | 18 ++++++++++++++ regression/statement-list/Makefile | 18 ++++++++++++++ regression/statement-list/Mul_DInt/main.awl | 24 +++++++++++++++++++ regression/statement-list/Mul_DInt/test.desc | 18 ++++++++++++++ .../statement-list/Multiple_Elements/main.awl | 24 +++++++++++++++++++ .../Multiple_Elements/test.desc | 10 ++++++++ 12 files changed, 183 insertions(+) create mode 100644 regression/statement-list/Add_Int/main.awl create mode 100644 regression/statement-list/Add_Int/test.desc create mode 100644 regression/statement-list/CMakeLists.txt create mode 100644 regression/statement-list/Div_Real/main.awl create mode 100644 regression/statement-list/Div_Real/test.desc create mode 100644 regression/statement-list/Makefile create mode 100644 regression/statement-list/Mul_DInt/main.awl create mode 100644 regression/statement-list/Mul_DInt/test.desc create mode 100644 regression/statement-list/Multiple_Elements/main.awl create mode 100644 regression/statement-list/Multiple_Elements/test.desc diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index b47c8e5d6ba..a32af852c52 100644 --- a/regression/CMakeLists.txt +++ b/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) diff --git a/regression/Makefile b/regression/Makefile index 3742ce83e47..e4bb8dde0ca 100644 --- a/regression/Makefile +++ b/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 \ diff --git a/regression/statement-list/Add_Int/main.awl b/regression/statement-list/Add_Int/main.awl new file mode 100644 index 00000000000..b26a912309f --- /dev/null +++ b/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 + diff --git a/regression/statement-list/Add_Int/test.desc b/regression/statement-list/Add_Int/test.desc new file mode 100644 index 00000000000..489da4b584f --- /dev/null +++ b/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 diff --git a/regression/statement-list/CMakeLists.txt b/regression/statement-list/CMakeLists.txt new file mode 100644 index 00000000000..1785e0f124b --- /dev/null +++ b/regression/statement-list/CMakeLists.txt @@ -0,0 +1,3 @@ +add_test_pl_tests( + "$" -X smt-backend +) diff --git a/regression/statement-list/Div_Real/main.awl b/regression/statement-list/Div_Real/main.awl new file mode 100644 index 00000000000..98304d04989 --- /dev/null +++ b/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 + diff --git a/regression/statement-list/Div_Real/test.desc b/regression/statement-list/Div_Real/test.desc new file mode 100644 index 00000000000..d7a16022173 --- /dev/null +++ b/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 diff --git a/regression/statement-list/Makefile b/regression/statement-list/Makefile new file mode 100644 index 00000000000..97e365e8263 --- /dev/null +++ b/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 diff --git a/regression/statement-list/Mul_DInt/main.awl b/regression/statement-list/Mul_DInt/main.awl new file mode 100644 index 00000000000..a11e76be509 --- /dev/null +++ b/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 + diff --git a/regression/statement-list/Mul_DInt/test.desc b/regression/statement-list/Mul_DInt/test.desc new file mode 100644 index 00000000000..60957317bc5 --- /dev/null +++ b/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 diff --git a/regression/statement-list/Multiple_Elements/main.awl b/regression/statement-list/Multiple_Elements/main.awl new file mode 100644 index 00000000000..5d70c967185 --- /dev/null +++ b/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 + diff --git a/regression/statement-list/Multiple_Elements/test.desc b/regression/statement-list/Multiple_Elements/test.desc new file mode 100644 index 00000000000..de72c04c521 --- /dev/null +++ b/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