diff --git a/regression/statement-list/Bool5/main.awl b/regression/statement-list/Bool5/main.awl new file mode 100644 index 00000000000..5dbf7784a1d --- /dev/null +++ b/regression/statement-list/Bool5/main.awl @@ -0,0 +1,24 @@ +FUNCTION_BLOCK "Bool5" +VERSION : 0.1 + VAR_INPUT + in1 : Bool; + END_VAR + + VAR_OUTPUT + out1 : Bool; + END_VAR + + +BEGIN +NETWORK +TITLE = + CLR; + X #in1; + XN #in1; + = #out1; + CALL "__CPROVER_assert" + ( condition := #out1 + ); + +END_FUNCTION_BLOCK + diff --git a/regression/statement-list/Bool5/test.desc b/regression/statement-list/Bool5/test.desc new file mode 100644 index 00000000000..5ac35659259 --- /dev/null +++ b/regression/statement-list/Bool5/test.desc @@ -0,0 +1,9 @@ +CORE +main.awl +--function \"Bool5\" +^EXIT=0$ +^SIGNAL=0$ +^\*\* 0 of 1 failed \(1 iterations\)$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/statement-list/Function_Call/main.awl b/regression/statement-list/Function_Call1/main.awl similarity index 77% rename from regression/statement-list/Function_Call/main.awl rename to regression/statement-list/Function_Call1/main.awl index 0394727cdb5..ef296974493 100644 --- a/regression/statement-list/Function_Call/main.awl +++ b/regression/statement-list/Function_Call1/main.awl @@ -1,4 +1,4 @@ -FUNCTION_BLOCK "Function_Call" +FUNCTION_BLOCK "Function_Call1" VERSION : 0.1 VAR_INPUT In1 : Bool; diff --git a/regression/statement-list/Function_Call/test.desc b/regression/statement-list/Function_Call1/test.desc similarity index 85% rename from regression/statement-list/Function_Call/test.desc rename to regression/statement-list/Function_Call1/test.desc index 7db6bc3447d..05b229262ad 100644 --- a/regression/statement-list/Function_Call/test.desc +++ b/regression/statement-list/Function_Call1/test.desc @@ -3,7 +3,7 @@ main.awl --show-parse-tree ^EXIT=0$ ^SIGNAL=0$ -^Name: "Function_Call"$ +^Name: "Function_Call1"$ ^Version: 0[.]1$ ^statement_list_call "__Function"$ ^ param := In1$ diff --git a/regression/statement-list/Function_Call2/main.awl b/regression/statement-list/Function_Call2/main.awl new file mode 100644 index 00000000000..b12ab8b419f --- /dev/null +++ b/regression/statement-list/Function_Call2/main.awl @@ -0,0 +1,40 @@ +FUNCTION "Called_Function" : Void +VERSION : 0.1 + VAR_INPUT + Input : Bool; + END_VAR + +BEGIN +NETWORK +TITLE = + +END_FUNCTION + + +FUNCTION_BLOCK "Function_Call2" +VERSION : 0.1 + VAR_INPUT + In1 : Bool; + END_VAR + +BEGIN +NETWORK +TITLE = + CALL "__CPROVER_assert" + ( condition := TRUE + ); + + CALL "__CPROVER_assume" + ( condition := #In1 + ); + + CALL "__CPROVER_assert" + ( condition := #In1 + ); + + CALL "Called_Function" + ( Input := #In1 + ); + +END_FUNCTION_BLOCK + diff --git a/regression/statement-list/Function_Call2/test.desc b/regression/statement-list/Function_Call2/test.desc new file mode 100644 index 00000000000..9afe8d2a1a6 --- /dev/null +++ b/regression/statement-list/Function_Call2/test.desc @@ -0,0 +1,8 @@ +CORE +main.awl +--function \"Function_Call2\" +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/statement-list/parser.y b/src/statement-list/parser.y index e1d8438405f..4cecf30438f 100644 --- a/src/statement-list/parser.y +++ b/src/statement-list/parser.y @@ -1080,7 +1080,7 @@ Oom_Param_Assignment: ; Param_Assignment: - Variable_Name TOK_ASSIGNMENT Variable_Access + Variable_Name TOK_ASSIGNMENT IL_Operand { newstack($$); parser_stack($$) = equal_exprt{std::move(parser_stack($1)), diff --git a/src/statement-list/statement_list_parse_tree_io.cpp b/src/statement-list/statement_list_parse_tree_io.cpp index 5d0891500ac..2719720b6a7 100644 --- a/src/statement-list/statement_list_parse_tree_io.cpp +++ b/src/statement-list/statement_list_parse_tree_io.cpp @@ -15,24 +15,40 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include #include +/// String to indicate that there is no value. #define NO_VALUE "(none)" /// Prints a constant to the given output stream. -/// \param [out] out: Stream that should receive the result. +/// \param [out] os: Stream that should receive the result. /// \param constant: Constant that shall be printed. -static void output_constant(std::ostream &out, const constant_exprt &constant) +static void output_constant(std::ostream &os, const constant_exprt &constant) { mp_integer ivalue; if(!to_integer(constant, ivalue)) - out << ivalue; + os << ivalue; else if(can_cast_type(constant.type())) { ieee_floatt real{get_real_type()}; real.from_expr(constant); - out << real.to_float(); + os << real.to_float(); } else - out << constant.get_value(); + os << constant.get_value(); +} + +/// Prints the assignment of a module parameter to the given output stream. +/// \param [out] os: Stream that should receive the result. +/// \param assignment: Assignment that shall be printed. +static void +output_parameter_assignment(std::ostream &os, const equal_exprt &assignment) +{ + os << assignment.lhs().get(ID_identifier) << " := "; + const constant_exprt *const constant = + expr_try_dynamic_cast(assignment.rhs()); + if(constant) + output_constant(os, *constant); + else + os << assignment.rhs().get(ID_identifier); } void output_parse_tree( @@ -65,176 +81,178 @@ void output_parse_tree( } void output_function_block( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::function_blockt &function_block) { - output_tia_module_properties(function_block, out); - output_common_var_declarations(out, function_block); - output_static_var_declarations(out, function_block); - output_network_list(out, function_block.networks); + output_tia_module_properties(function_block, os); + output_common_var_declarations(os, function_block); + output_static_var_declarations(os, function_block); + output_network_list(os, function_block.networks); } void output_function( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::functiont &function) { - output_tia_module_properties(function, out); - output_return_value(function, out); - output_common_var_declarations(out, function); - output_network_list(out, function.networks); + output_tia_module_properties(function, os); + output_return_value(function, os); + output_common_var_declarations(os, function); + output_network_list(os, function.networks); } void output_tia_module_properties( const statement_list_parse_treet::tia_modulet &module, - std::ostream &out) + std::ostream &os) { - out << "Name: " << module.name << '\n'; - out << "Version: " << module.version << "\n\n"; + os << "Name: " << module.name << '\n'; + os << "Version: " << module.version << "\n\n"; } void output_return_value( const statement_list_parse_treet::functiont &function, - std::ostream &out) + std::ostream &os) { - out << "Return type: "; + os << "Return type: "; if(function.return_type.is_nil()) - out << "Void"; + os << "Void"; else - out << function.return_type.id(); - out << "\n\n"; + os << function.return_type.id(); + os << "\n\n"; } void output_common_var_declarations( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::tia_modulet &module) { if(!module.var_input.empty()) { - out << "--------- Input Variables ----------\n\n"; - output_var_declaration_list(out, module.var_input); + os << "--------- Input Variables ----------\n\n"; + output_var_declaration_list(os, module.var_input); } if(!module.var_inout.empty()) { - out << "--------- In/Out Variables ---------\n\n"; - output_var_declaration_list(out, module.var_inout); + os << "--------- In/Out Variables ---------\n\n"; + output_var_declaration_list(os, module.var_inout); } if(!module.var_output.empty()) { - out << "--------- Output Variables ---------\n\n"; - output_var_declaration_list(out, module.var_output); + os << "--------- Output Variables ---------\n\n"; + output_var_declaration_list(os, module.var_output); } if(!module.var_constant.empty()) { - out << "-------- Constant Variables --------\n\n"; - output_var_declaration_list(out, module.var_constant); + os << "-------- Constant Variables --------\n\n"; + output_var_declaration_list(os, module.var_constant); } if(!module.var_temp.empty()) { - out << "---------- Temp Variables ----------\n\n"; - output_var_declaration_list(out, module.var_temp); + os << "---------- Temp Variables ----------\n\n"; + output_var_declaration_list(os, module.var_temp); } } void output_static_var_declarations( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::function_blockt &block) { if(!block.var_static.empty()) { - out << "--------- Static Variables ---------\n\n"; - output_var_declaration_list(out, block.var_static); + os << "--------- Static Variables ---------\n\n"; + output_var_declaration_list(os, block.var_static); } } void output_var_declaration_list( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::var_declarationst &declarations) { for(const auto &declaration : declarations) { - output_var_declaration(out, declaration); - out << "\n\n"; + output_var_declaration(os, declaration); + os << "\n\n"; } } void output_var_declaration( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::var_declarationt &declaration) { - out << declaration.variable.pretty() << '\n'; - out << " * default_value: "; + os << declaration.variable.pretty() << '\n'; + os << " * default_value: "; if(declaration.default_value) { const constant_exprt &constant = to_constant_expr(declaration.default_value.value()); - output_constant(out, constant); + output_constant(os, constant); } else - out << NO_VALUE; + os << NO_VALUE; } void output_network_list( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::networkst &networks) { - out << "-------------- Networks --------------\n\n"; + os << "-------------- Networks --------------\n\n"; for(const auto &network : networks) { - output_network(out, network); - out << '\n'; + output_network(os, network); + os << '\n'; } } void output_network( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::networkt &network) { - out << "Title: " << network.title.value_or(NO_VALUE) << '\n'; - out << "Instructions: "; + os << "Title: " << network.title.value_or(NO_VALUE) << '\n'; + os << "Instructions: "; if(network.instructions.empty()) - out << NO_VALUE; - out << '\n'; + os << NO_VALUE; + os << '\n'; for(const auto &instruction : network.instructions) { - output_instruction(out, instruction); - out << '\n'; + output_instruction(os, instruction); + os << '\n'; } } void output_instruction( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::instructiont &instruction) { for(const codet &token : instruction.tokens) { - out << token.get_statement(); + os << token.get_statement(); for(const auto &expr : token.operands()) { - if(expr.id() == ID_symbol) + const symbol_exprt *const symbol = + expr_try_dynamic_cast(expr); + if(symbol) { - out << '\t' << expr.get(ID_identifier); + os << '\t' << symbol->get_identifier(); continue; } const constant_exprt *const constant = expr_try_dynamic_cast(expr); if(constant) { - out << '\t'; - output_constant(out, *constant); + os << '\t'; + output_constant(os, *constant); continue; } - const equal_exprt *const eq = expr_try_dynamic_cast(expr); - if(eq) + const equal_exprt *const equal = expr_try_dynamic_cast(expr); + if(equal) { - out << "\n\t" << eq->lhs().get(ID_identifier) - << " := " << eq->rhs().get(ID_identifier); + os << "\n\t"; + output_parameter_assignment(os, *equal); + continue; } - else - out << '\t' << expr.id(); + os << '\t' << expr.id(); } } } diff --git a/src/statement-list/statement_list_parse_tree_io.h b/src/statement-list/statement_list_parse_tree_io.h index 58089a75cc2..700a462af0c 100644 --- a/src/statement-list/statement_list_parse_tree_io.h +++ b/src/statement-list/statement_list_parse_tree_io.h @@ -16,97 +16,97 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com /// Prints the given Statement List parse tree in a human-readable form to the /// given output stream. -/// \param out: Stream that should receive the result. +/// \param os: Stream that should receive the result. /// \param tree: Parse Tree whose contents should be printed. void output_parse_tree( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet &tree); /// Prints the given Statement List function block in a human-readable form to /// the given output stream. -/// \param out: Stream that should receive the result. +/// \param os: Stream that should receive the result. /// \param block: Function block whose contents should be printed. void output_function_block( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::function_blockt &block); /// Prints the given Statement List function in a human-readable form to /// the given output stream. -/// \param out: Stream that should receive the result. +/// \param os: Stream that should receive the result. /// \param function: Function whose contents should be printed. void output_function( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::functiont &function); /// Prints the basic information about a TIA module to the given output stream. /// \param module: TIA module whose contents should be printed. -/// \param out: Stream that should receive the result. +/// \param os: Stream that should receive the result. void output_tia_module_properties( const statement_list_parse_treet::tia_modulet &module, - std::ostream &out); + std::ostream &os); /// Prints the return value of a function to the given output stream. /// \param function: Function whose return value should be printed. -/// \param out: Stream that should receive the result. +/// \param os: Stream that should receive the result. void output_return_value( const statement_list_parse_treet::functiont &function, - std::ostream &out); + std::ostream &os); /// Prints all variable declarations functions and function blocks have in /// common to the given output stream. -/// \param out: Stream that should receive the result. +/// \param os: Stream that should receive the result. /// \param module: TIA module whose variable declarations should be printed. void output_common_var_declarations( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::tia_modulet &module); /// Prints the static variable declarations of a function block to the given /// output stream. -/// \param out: Stream that should receive the result. +/// \param os: Stream that should receive the result. /// \param block: Function block whose static variables should be /// printed. void output_static_var_declarations( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::function_blockt &block); /// Prints all variable declarations of the given list to the given output /// stream. -/// \param out: Stream that should receive the result. +/// \param os: Stream that should receive the result. /// \param declarations: List whose contents should be printed. void output_var_declaration_list( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::var_declarationst &declarations); /// Prints the given Statement List variable declaration in a human-readable /// form to the given output stream. -/// \param out: Stream that should receive the result. +/// \param os: Stream that should receive the result. /// \param declaration: Declaration that should be printed. void output_var_declaration( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::var_declarationt &declaration); /// Prints the given network list in a human-readable form to the given output /// stream. -/// \param out: Stream that should receive the result. +/// \param os: Stream that should receive the result. /// \param networks: List whose contents should be printed. void output_network_list( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::networkst &networks); /// Prints the given Statement List network in a human-readable form to the /// given output stream. -/// \param out: Stream that should receive the result. +/// \param os: Stream that should receive the result. /// \param network: Network that should be printed. void output_network( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::networkt &network); /// Prints the given Statement List instruction in a human-readable form to the /// given output stream. -/// \param out: Stream that should receive the result. +/// \param os: Stream that should receive the result. /// \param instruction: Instruction that should be printed. void output_instruction( - std::ostream &out, + std::ostream &os, const statement_list_parse_treet::instructiont &instruction); #endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_PARSE_TREE_IO_H diff --git a/src/statement-list/statement_list_typecheck.cpp b/src/statement-list/statement_list_typecheck.cpp index e90eeee88d4..65366966dac 100644 --- a/src/statement-list/statement_list_typecheck.cpp +++ b/src/statement-list/statement_list_typecheck.cpp @@ -33,6 +33,8 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #define CPROVER_ASSERT "\"" CPROVER_PREFIX "assert\"" /// Name of the CBMC assume function. #define CPROVER_ASSUME "\"" CPROVER_PREFIX "assume\"" +/// Name of the RLO symbol used in some operations. +#define CPROVER_TEMP_RLO CPROVER_PREFIX "temp_rlo" /// Creates the artificial data block parameter with a generic name and the /// specified type. @@ -94,6 +96,8 @@ void statement_list_typecheckt::typecheck() parse_tree.function_blocks) typecheck_function_block_declaration(fb); typecheck_tag_list(); + // Temporary RLO symbol for certain operations. + add_temp_rlo(); // Iterate through all networks to generate the function bodies. for(const statement_list_parse_treet::function_blockt &fb : @@ -197,6 +201,19 @@ void statement_list_typecheckt::typecheck_tag_list() } } +void statement_list_typecheckt::add_temp_rlo() +{ + symbolt temp_rlo; + temp_rlo.is_static_lifetime = true; + temp_rlo.module = module; + temp_rlo.name = CPROVER_TEMP_RLO; + temp_rlo.base_name = temp_rlo.name; + temp_rlo.pretty_name = temp_rlo.name; + temp_rlo.type = get_bool_type(); + temp_rlo.mode = ID_statement_list; + symbol_table.add(temp_rlo); +} + struct_typet statement_list_typecheckt::create_instance_data_block_type( const statement_list_parse_treet::function_blockt &function_block) { @@ -378,6 +395,10 @@ void statement_list_typecheckt::typecheck_statement_list_instruction( typecheck_statement_list_or(op_code, tia_element); else if(ID_statement_list_or_not == statement) typecheck_statement_list_or_not(op_code, tia_element); + else if(ID_statement_list_xor == statement) + typecheck_statement_list_xor(op_code, tia_element); + else if(ID_statement_list_xor_not == statement) + typecheck_statement_list_xor_not(op_code, tia_element); else if(ID_statement_list_and_nested == statement) typecheck_statement_list_nested_and(op_code); else if(ID_statement_list_and_not_nested == statement) @@ -386,6 +407,10 @@ void statement_list_typecheckt::typecheck_statement_list_instruction( typecheck_statement_list_nested_or(op_code); else if(ID_statement_list_or_not_nested == statement) typecheck_statement_list_nested_or_not(op_code); + else if(ID_statement_list_xor_nested == statement) + typecheck_statement_list_nested_xor(op_code); + else if(ID_statement_list_xor_not_nested == statement) + typecheck_statement_list_nested_xor_not(op_code); else if(ID_statement_list_nesting_closed == statement) typecheck_statement_list_nesting_closed(op_code); else if(ID_statement_list_assign == statement) @@ -732,9 +757,8 @@ void statement_list_typecheckt::typecheck_statement_list_and( const codet &op_code, const symbolt &tia_element) { - const symbol_exprt &sym{ - typecheck_instruction_with_non_const_operand(op_code)}; - const exprt op{typecheck_identifier(tia_element, sym.get_identifier())}; + exprt op{ + typecheck_simple_boolean_instruction_operand(op_code, tia_element, false)}; // If inside of a bit string and if the OR bit is not set, create an 'and' // expression with the operand and the current contents of the rlo bit. If @@ -755,24 +779,22 @@ void statement_list_typecheckt::typecheck_statement_list_and_not( const codet &op_code, const symbolt &tia_element) { - const symbol_exprt &sym{ - typecheck_instruction_with_non_const_operand(op_code)}; - const exprt op{typecheck_identifier(tia_element, sym.get_identifier())}; - const not_exprt not_op{op}; + exprt op{ + typecheck_simple_boolean_instruction_operand(op_code, tia_element, true)}; // If inside of a bit string and if the OR bit is not set, create an 'and' // expression with the operand and the current contents of the rlo bit. If // the OR bit is set then this instruction is part of an 'and-before-or' // block and needs to be added to the rlo in a special way. if(or_bit && fc_bit) - add_to_or_rlo_wrapper(not_op); + add_to_or_rlo_wrapper(op); else if(fc_bit) { - const and_exprt unsimplified{rlo_bit, not_op}; + const and_exprt unsimplified{rlo_bit, op}; rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table)); } else - initialize_bit_expression(not_op); + initialize_bit_expression(op); } void statement_list_typecheckt::typecheck_statement_list_or( @@ -821,6 +843,47 @@ void statement_list_typecheckt::typecheck_statement_list_or_not( initialize_bit_expression(not_op); } +void statement_list_typecheckt::typecheck_statement_list_xor( + const codet &op_code, + const symbolt &tia_element) +{ + const symbol_exprt &sym{ + typecheck_instruction_with_non_const_operand(op_code)}; + const exprt op{typecheck_identifier(tia_element, sym.get_identifier())}; + + // If inside of a bit string, create an 'xor' expression with the operand and + // the current contents of the rlo bit. + if(fc_bit) + { + const xor_exprt unsimplified{rlo_bit, op}; + rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table)); + or_bit = false; + } + else + initialize_bit_expression(op); +} + +void statement_list_typecheckt::typecheck_statement_list_xor_not( + const codet &op_code, + const symbolt &tia_element) +{ + const symbol_exprt &sym{ + typecheck_instruction_with_non_const_operand(op_code)}; + const exprt op{typecheck_identifier(tia_element, sym.get_identifier())}; + const not_exprt not_op{op}; + + // If inside of a bit string, create an 'xor not' expression with the + // operand and the current contents of the rlo bit. + if(fc_bit) + { + const xor_exprt unsimplified{rlo_bit, not_op}; + rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table)); + or_bit = false; + } + else + initialize_bit_expression(not_op); +} + void statement_list_typecheckt::typecheck_statement_list_and_before_or() { if(fc_bit) @@ -835,61 +898,49 @@ void statement_list_typecheckt::typecheck_statement_list_and_before_or() void statement_list_typecheckt::typecheck_statement_list_nested_and( const codet &op_code) { - typecheck_instruction_without_operand(op_code); - // If inside of a bit string use the value of the rlo. If this is the first - // expression of a bit string, load the value of the nested operation by - // implicitly setting the rlo to true. - if(!fc_bit) - rlo_bit = true_exprt{}; - const nesting_stack_entryt stack_entry{rlo_bit, or_bit, op_code}; - nesting_stack.push_back(stack_entry); - fc_bit = false; - or_bit = false; + // Set the rlo to true implicitly so that the value of the AND instruction + // is being loaded in case of a new bit string. + typecheck_nested_boolean_instruction(op_code, true_exprt{}); } void statement_list_typecheckt::typecheck_statement_list_nested_and_not( const codet &op_code) { - typecheck_instruction_without_operand(op_code); - // If inside of a bit string use the value of the rlo. If this is the first - // expression of a bit string, load the value of the nested operation by - // implicitly setting the rlo to true. - if(!fc_bit) - rlo_bit = true_exprt{}; - const nesting_stack_entryt stack_entry{rlo_bit, or_bit, op_code}; - nesting_stack.push_back(stack_entry); - fc_bit = false; - or_bit = false; + // Set the rlo to true implicitly so that the value of the AND instruction + // is being loaded in case of a new bit string. + typecheck_nested_boolean_instruction(op_code, true_exprt{}); } void statement_list_typecheckt::typecheck_statement_list_nested_or( const codet &op_code) { - typecheck_instruction_without_operand(op_code); - // If inside of a bit string use the value of the rlo. If this is the first - // expression of a bit string, load the value of the nested operation by - // implicitly setting the rlo to false. - if(!fc_bit) - rlo_bit = false_exprt{}; - const nesting_stack_entryt stack_entry{rlo_bit, or_bit, op_code}; - nesting_stack.push_back(stack_entry); - fc_bit = false; - or_bit = false; + // Set the rlo to false implicitly so that the value of the OR instruction + // is being loaded in case of a new bit string. + typecheck_nested_boolean_instruction(op_code, false_exprt{}); } void statement_list_typecheckt::typecheck_statement_list_nested_or_not( const codet &op_code) { - typecheck_instruction_without_operand(op_code); - // If inside of a bit string use the value of the rlo. If this is the first - // expression of a bit string, load the value of the nested operation by - // implicitly setting the rlo to false. - if(!fc_bit) - rlo_bit = false_exprt{}; - const nesting_stack_entryt stack_entry{rlo_bit, or_bit, op_code}; - nesting_stack.push_back(stack_entry); - fc_bit = false; - or_bit = false; + // Set the rlo to false implicitly so that the value of the OR instruction + // is being loaded in case of a new bit string. + typecheck_nested_boolean_instruction(op_code, false_exprt{}); +} + +void statement_list_typecheckt::typecheck_statement_list_nested_xor( + const codet &op_code) +{ + // Set the rlo to false implicitly so that the value of the XOR instruction + // is being loaded in case of a new bit string. + typecheck_nested_boolean_instruction(op_code, false_exprt{}); +} + +void statement_list_typecheckt::typecheck_statement_list_nested_xor_not( + const codet &op_code) +{ + // Set the rlo to false implicitly so that the value of the XOR instruction + // is being loaded in case of a new bit string. + typecheck_nested_boolean_instruction(op_code, false_exprt{}); } void statement_list_typecheckt::typecheck_statement_list_nesting_closed( @@ -938,6 +989,17 @@ void statement_list_typecheckt::typecheck_statement_list_nesting_closed( or_bit = false; rlo_bit = or_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}}; } + else if(ID_statement_list_xor_nested == statement) + { + or_bit = false; + rlo_bit = xor_exprt{nesting_stack.back().rlo_bit, rlo_bit}; + } + else if(ID_statement_list_xor_not_nested == statement) + { + or_bit = false; + rlo_bit = xor_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}}; + } + nesting_stack.pop_back(); } void statement_list_typecheckt::typecheck_statement_list_assign( @@ -956,6 +1018,9 @@ void statement_list_typecheckt::typecheck_statement_list_assign( tia_element.value.add_to_operands(assignment); fc_bit = false; or_bit = false; + // Set RLO to assigned operand in order to prevent false results if a symbol + // that's implicitly part of the RLO was changed by the assignment. + rlo_bit = lhs; } void statement_list_typecheckt::typecheck_statement_list_set_rlo( @@ -982,6 +1047,9 @@ void statement_list_typecheckt::typecheck_statement_list_set( { const symbol_exprt &op{typecheck_instruction_with_non_const_operand(op_code)}; const irep_idt &identifier{op.get_identifier()}; + + save_rlo_state(tia_element); + const exprt lhs{typecheck_identifier(tia_element, identifier)}; const code_assignt assignment{lhs, true_exprt()}; const code_ifthenelset ifthen{rlo_bit, assignment}; @@ -996,6 +1064,9 @@ void statement_list_typecheckt::typecheck_statement_list_reset( { const symbol_exprt &op{typecheck_instruction_with_non_const_operand(op_code)}; const irep_idt &identifier{op.get_identifier()}; + + save_rlo_state(tia_element); + const exprt lhs{typecheck_identifier(tia_element, identifier)}; const code_assignt assignment{lhs, false_exprt()}; const code_ifthenelset ifthen{rlo_bit, assignment}; @@ -1129,6 +1200,34 @@ void statement_list_typecheckt::typecheck_binary_accumulator_instruction( } } +void statement_list_typecheckt::typecheck_nested_boolean_instruction( + const codet &op_code, + const exprt &rlo_value) +{ + typecheck_instruction_without_operand(op_code); + // If inside of a bit string use the value of the rlo. If this is the first + // expression of a bit string, load the value of the nested operation by + // implicitly setting the rlo to the specified value. + if(!fc_bit) + rlo_bit = rlo_value; + const nesting_stack_entryt stack_entry{rlo_bit, or_bit, op_code}; + nesting_stack.push_back(stack_entry); + fc_bit = false; + or_bit = false; +} + +exprt statement_list_typecheckt::typecheck_simple_boolean_instruction_operand( + const codet &op_code, + const symbolt &tia_element, + bool negate) +{ + const symbol_exprt &sym{ + typecheck_instruction_with_non_const_operand(op_code)}; + const exprt op{typecheck_identifier(tia_element, sym.get_identifier())}; + const not_exprt not_op{op}; + return negate ? not_op : op; +} + exprt statement_list_typecheckt::typecheck_identifier( const symbolt &tia_element, const irep_idt &identifier) @@ -1199,11 +1298,8 @@ void statement_list_typecheckt::typecheck_CPROVER_assert( expr_try_dynamic_cast(op_code.op1()); if(assignment) { - const symbol_exprt &rhs{to_symbol_expr(assignment->rhs())}; - // Check if identifier is present, create assertion and add it to the - // function body. - const exprt op{typecheck_identifier(tia_element, rhs.get_identifier())}; - const code_assertt assertion{op}; + const code_assertt assertion{ + typecheck_function_call_argument_rhs(tia_element, assignment->rhs())}; tia_element.value.add_to_operands(assertion); } else @@ -1221,11 +1317,8 @@ void statement_list_typecheckt::typecheck_CPROVER_assume( expr_try_dynamic_cast(op_code.op1()); if(assignment) { - const symbol_exprt &rhs{to_symbol_expr(assignment->rhs())}; - // Check if identifier is present, create assumption and add it to the - // function body. - const exprt op{typecheck_identifier(tia_element, rhs.get_identifier())}; - const code_assumet assumption{op}; + const code_assumet assumption{ + typecheck_function_call_argument_rhs(tia_element, assignment->rhs())}; tia_element.value.add_to_operands(assumption); } else @@ -1281,18 +1374,12 @@ void statement_list_typecheckt::typecheck_called_function( for(const auto &expr : op_code.operands()) { if(can_cast_expr(expr)) - { - const equal_exprt &assignment{to_equal_expr(expr)}; - assignments.push_back(assignment); - } + assignments.push_back(to_equal_expr(expr)); } for(const code_typet::parametert ¶m : params) - { - const exprt &arg{ - typecheck_function_call_arguments(assignments, param, tia_element)}; - args.push_back(arg); - } + args.emplace_back( + typecheck_function_call_arguments(assignments, param, tia_element)); // Check the return value if present. if(called_type.return_type().is_nil()) @@ -1331,9 +1418,9 @@ exprt statement_list_typecheckt::typecheck_function_call_arguments( const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())}; if(param_name == lhs.get_identifier()) { - const symbol_exprt &rhs{to_symbol_expr(assignment.rhs())}; - const exprt assigned_variable{ - typecheck_identifier(tia_element, rhs.get_identifier())}; + exprt assigned_variable{ + typecheck_function_call_argument_rhs(tia_element, assignment.rhs())}; + if(param_type == assigned_variable.type()) return assigned_variable; else @@ -1350,6 +1437,21 @@ exprt statement_list_typecheckt::typecheck_function_call_arguments( throw TYPECHECK_ERROR; } +exprt statement_list_typecheckt::typecheck_function_call_argument_rhs( + const symbolt &tia_element, + const exprt &rhs) +{ + exprt assigned_operand; + const symbol_exprt *const symbol_rhs = + expr_try_dynamic_cast(rhs); + if(symbol_rhs) + assigned_operand = + typecheck_identifier(tia_element, symbol_rhs->get_identifier()); + else // constant_exprt. + assigned_operand = rhs; + return assigned_operand; +} + exprt statement_list_typecheckt::typecheck_return_value_assignment( const std::vector &assignments, const typet &return_type, @@ -1404,3 +1506,12 @@ void statement_list_typecheckt::initialize_bit_expression(const exprt &op) or_bit = false; rlo_bit = op; } + +void statement_list_typecheckt::save_rlo_state(symbolt &tia_element) +{ + symbol_exprt temp_rlo{ + symbol_table.lookup_ref(CPROVER_TEMP_RLO).symbol_expr()}; + const code_assignt rlo_assignment{temp_rlo, rlo_bit}; + tia_element.value.add_to_operands(rlo_assignment); + rlo_bit = std::move(temp_rlo); +} diff --git a/src/statement-list/statement_list_typecheck.h b/src/statement-list/statement_list_typecheck.h index 0bfc82ec7e7..4a99fdf70be 100644 --- a/src/statement-list/statement_list_typecheck.h +++ b/src/statement-list/statement_list_typecheck.h @@ -129,6 +129,10 @@ class statement_list_typecheckt : public typecheckt /// adds symbols for its contents to the symbol table. void typecheck_tag_list(); + /// Adds a symbol for the RLO to the symbol table. This symbol is used by + /// other operations to save intermediate results of the rlo expression. + void add_temp_rlo(); + /// Creates a data block type for the given function block. /// \param function_block: Function block with an interface that should be /// converted to a data block. @@ -368,15 +372,23 @@ class statement_list_typecheckt : public typecheckt const codet &op_code, const symbolt &tia_element); - /// Performs a typecheck on a STL boolean And Not instruction. Reads and + /// Performs a typecheck on a STL boolean Or instruction. Reads and /// modifies the RLO, OR and FC bit. /// \param op_code: OP code of the instruction. /// \param tia_element: Symbol representation of the TIA element. void typecheck_statement_list_or(const codet &op_code, const symbolt &tia_element); - /// Performs a typecheck on a STL boolean Or instruction. Reads and modifies - /// the RLO, OR and FC bit. + /// Performs a typecheck on a STL boolean XOR instruction. Reads and + /// modifies the RLO, OR and FC bit. + /// \param op_code: OP code of the instruction. + /// \param tia_element: Symbol representation of the TIA element. + void typecheck_statement_list_xor( + const codet &op_code, + const symbolt &tia_element); + + /// Performs a typecheck on a STL boolean And Not instruction. Reads and + /// modifies the RLO, OR and FC bit. /// \param op_code: OP code of the instruction. /// \param tia_element: Symbol representation of the TIA element. void typecheck_statement_list_and_not( @@ -391,6 +403,14 @@ class statement_list_typecheckt : public typecheckt const codet &op_code, const symbolt &tia_element); + /// Performs a typecheck on a STL boolean XOR Not instruction. Reads and + /// modifies the RLO, OR and FC bit. + /// \param op_code: OP code of the instruction. + /// \param tia_element: Symbol representation of the TIA element. + void typecheck_statement_list_xor_not( + const codet &op_code, + const symbolt &tia_element); + /// Performs a typecheck on a STL operand-less Or instruction. Reads and /// modifies the RLO, OR and FC bit. void typecheck_statement_list_and_before_or(); @@ -405,6 +425,11 @@ class statement_list_typecheckt : public typecheckt /// \param op_code: OP code of the instruction. void typecheck_statement_list_nested_or(const codet &op_code); + /// Performs a typecheck on a nested XOR instruction. Pushes the current + /// program state to the nesting stack and cleans the RLO, OR and FC bit. + /// \param op_code: OP code of the instruction. + void typecheck_statement_list_nested_xor(const codet &op_code); + /// Performs a typecheck on a nested And Not instruction. Pushes the current /// program state to the nesting stack and cleans the RLO, OR and FC bit. /// \param op_code: OP code of the instruction. @@ -415,6 +440,11 @@ class statement_list_typecheckt : public typecheckt /// \param op_code: OP code of the instruction. void typecheck_statement_list_nested_or_not(const codet &op_code); + /// Performs a typecheck on a nested XOR Not instruction. Pushes the current + /// program state to the nesting stack and cleans the RLO, OR and FC bit. + /// \param op_code: OP code of the instruction. + void typecheck_statement_list_nested_xor_not(const codet &op_code); + /// Performs a typecheck on a Nesting Closed instruction. Uses the latest /// entry on the nesting stack and modifies the RLO, OR and FC bit according /// to the instruction that started the nesting. @@ -478,7 +508,7 @@ class statement_list_typecheckt : public typecheckt /// Performs a typecheck on a STL instruction with an additional operand that /// should be no constant. /// \param op_code: OP code of the instruction. - /// \return Reference to the operand. + /// \return: Reference to the operand. const symbol_exprt & typecheck_instruction_with_non_const_operand(const codet &op_code); @@ -486,11 +516,32 @@ class statement_list_typecheckt : public typecheckt /// \param op_code: OP code of the instruction. void typecheck_instruction_without_operand(const codet &op_code); - /// Performs a typecheck on an STL instruction that uses two accumulator + /// Performs a typecheck on a STL instruction that uses two accumulator /// entries. /// \param op_code: OP code of the instruction. void typecheck_binary_accumulator_instruction(const codet &op_code); + /// Performs a typecheck on a STL instruction that initializes a new boolean + /// nesting. + /// \param op_code: OP code of the instruction. + /// \param rlo_value: Value of the RLO that is pushed on the nesting stack + /// for the case that this is the first instruction of a new bit string. + void typecheck_nested_boolean_instruction( + const codet &op_code, + const exprt &rlo_value); + + /// Performs a typecheck on the operand of a not nested boolean instruction + /// and returns the result. + /// \param op_code: OP code of the instruction. + /// \param tia_element: Symbol representation of the TIA element. + /// \param negate: Whether the operand should be negated (e.g. for the + /// `AND NOT` expression). + /// \return: Typechecked operand. + exprt typecheck_simple_boolean_instruction_operand( + const codet &op_code, + const symbolt &tia_element, + bool negate); + /// Performs a typecheck on an STL comparison instruction. Modifies the RLO. /// \param comparison: ID of the compare expression that should be pushed to /// the RLO. @@ -545,6 +596,15 @@ class statement_list_typecheckt : public typecheckt const code_typet::parametert ¶m, const symbolt &tia_element); + /// Checks if the given assigned expression is a variable or a constant and + /// returns the typechecked version. + /// \param tia_element: Symbol representation of the TIA element. + /// \param rhs: Expression that the function parameter got assigned to. + /// \return: Expression of either a symbol or a constant. + exprt typecheck_function_call_argument_rhs( + const symbolt &tia_element, + const exprt &rhs); + /// Checks if there is a return value assignment inside of the assignment /// list of a function call and returns the expression of the assigned /// variable. @@ -568,6 +628,11 @@ class statement_list_typecheckt : public typecheckt /// instruction was encontered. /// \param op: Operand of the encountered instruction. void initialize_bit_expression(const exprt &op); + + /// Saves the current RLO bit to a temporary variable to prevent false + /// overrides when modifying boolean variables. + /// \param tia_element: Symbol representation of the TIA element. + void save_rlo_state(symbolt &tia_element); }; #endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H