From 6adc45e0d2991e2f24c8da6e2336be062f05ca73 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 16 Feb 2021 18:51:43 +0000 Subject: [PATCH 01/11] Implement `format` of initialisation in `code_declt` This was previously unimplemented, which resulted in the part of the statement being missing from the formatted output. --- src/util/format_expr.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index fe6c3eb1689..b69d1bcfc9e 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -357,8 +357,11 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr) else if(statement == ID_decl) { const auto &declaration_symb = to_code_decl(code).symbol(); - return os << "decl " << format(declaration_symb.type()) << " " - << format(declaration_symb) << ";"; + os << "decl " << format(declaration_symb.type()) << " " + << format(declaration_symb); + if(code.operands().size() > 1) + os << " = " << format(code.op1()); + return os << ";"; } else if(statement == ID_function_call) { From 7b6a25da723097848fb00e24eae74117a6d8fa1a Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 17 Feb 2021 14:33:32 +0000 Subject: [PATCH 02/11] Add test of `format` applied to `code_declt` To confirm the functionality added is correct and continues to work when follow up refactorings are applied. --- unit/Makefile | 1 + unit/util/format.cpp | 22 ++++++++++++++++++++++ 2 files changed, 23 insertions(+) create mode 100644 unit/util/format.cpp diff --git a/unit/Makefile b/unit/Makefile index ff37116bb75..0a582855351 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -90,6 +90,7 @@ SRC += analyses/ai/ai.cpp \ util/expr.cpp \ util/expr_iterator.cpp \ util/file_util.cpp \ + util/format.cpp \ util/format_number_range.cpp \ util/get_base_name.cpp \ util/graph.cpp \ diff --git a/unit/util/format.cpp b/unit/util/format.cpp new file mode 100644 index 00000000000..b1c4718f5e9 --- /dev/null +++ b/unit/util/format.cpp @@ -0,0 +1,22 @@ +/*******************************************************************\ + + Module: Unit tests for `format` function. + + Author: DiffBlue Limited. + +\*******************************************************************/ + +#include +#include +#include + +#include + +TEST_CASE("Format a declaration statement.", "[core][util][format]") +{ + const signedbv_typet int_type{32}; + code_declt declaration{symbol_exprt{"foo", int_type}}; + REQUIRE(format_to_string(declaration) == "decl signedbv[32] foo;"); + declaration.add_to_operands(int_type.zero_expr()); + REQUIRE(format_to_string(declaration) == "decl signedbv[32] foo = 0;"); +} From 7ea0e60714e21a10f6d2f33eb6d7541c67c532da Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 17 Feb 2021 17:34:30 +0000 Subject: [PATCH 03/11] Add interface for reading the initialisation from a `code_declt` So that the initial value can be read out of a `code_declt` without directly accessing the operands. --- src/util/std_code.h | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/util/std_code.h b/src/util/std_code.h index f27d3189377..de83675baf9 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -420,6 +420,15 @@ class code_declt:public codet return symbol().get_identifier(); } + /// Returns the initial value to which the declared variable is initialized, + /// or empty in the case where no initialisation is included. + optionalt initial_value() const + { + if(operands().size() < 2) + return {}; + return {op1()}; + } + static void check( const codet &code, const validation_modet vm = validation_modet::INVARIANT) From f593d182e2085e1582eec906584a8e7cd693c75a Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 17 Feb 2021 17:35:09 +0000 Subject: [PATCH 04/11] Use `code_declt::initial_value` in `dump_ct::cleanup_decl` To avoid directly reading from the operands. --- src/goto-instrument/dump_c.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index fdbeead99bc..feb02e45cec 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -650,19 +650,18 @@ void dump_ct::cleanup_decl( std::list &local_static, std::list &local_type_decls) { - exprt value=nil_exprt(); + const optionalt value = decl.initial_value(); - if(decl.operands().size()==2) + if(value) { - value=decl.op1(); decl.operands().resize(1); } goto_programt tmp; tmp.add(goto_programt::make_decl(decl.symbol())); - if(value.is_not_nil()) - tmp.add(goto_programt::make_assignment(decl.symbol(), value)); + if(value) + tmp.add(goto_programt::make_assignment(decl.symbol(), *value)); tmp.add(goto_programt::make_end_function()); From 51887aadc909b668910814630286165778461739 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 17 Feb 2021 17:48:07 +0000 Subject: [PATCH 05/11] Add interface for setting the initialisation in a `code_declt` So that the initial value can be written to a `code_declt` without directly accessing the operands. --- src/util/std_code.h | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/util/std_code.h b/src/util/std_code.h index de83675baf9..4ee41e38583 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -429,6 +429,25 @@ class code_declt:public codet return {op1()}; } + /// Sets the value to which this declaration initializes the declared + /// variable. Empty optional maybe passed to remove existing initialisation. + void set_initial_value(optionalt initial_value) + { + if(!initial_value) + { + operands().resize(1); + } + else if(operands().size() < 2) + { + PRECONDITION(operands().size() == 1); + add_to_operands(std::move(*initial_value)); + } + else + { + op1() = std::move(*initial_value); + } + } + static void check( const codet &code, const validation_modet vm = validation_modet::INVARIANT) From 8a14e670863c86f85d68996ca6afc40851f9a587 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 17 Feb 2021 17:49:09 +0000 Subject: [PATCH 06/11] Use `code_declt::set_initial_value` To avoid directly writing to the operands of a `code_declt`. --- src/goto-instrument/dump_c.cpp | 2 +- src/goto-instrument/goto_program2code.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index feb02e45cec..1e40383acb1 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -654,7 +654,7 @@ void dump_ct::cleanup_decl( if(value) { - decl.operands().resize(1); + decl.set_initial_value({}); } goto_programt tmp; diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index eb37f44ee2d..379414c0bb3 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -477,7 +477,7 @@ goto_programt::const_targett goto_program2codet::convert_decl( { if(next->is_assign()) { - d.copy_to_operands(next->get_assign().rhs()); + d.set_initial_value({next->get_assign().rhs()}); } else { From b5df13b69f53dcef92aeb97ac8344f2036d9b5ed Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 17 Feb 2021 17:53:56 +0000 Subject: [PATCH 07/11] Refactor `dump_ct::cleanup_decl` To avoid repeatedly checking the same condition and so that `value` is only in scope where it is required and non-empty. --- src/goto-instrument/dump_c.cpp | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 1e40383acb1..88241eb3e9c 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -650,19 +650,15 @@ void dump_ct::cleanup_decl( std::list &local_static, std::list &local_type_decls) { - const optionalt value = decl.initial_value(); + goto_programt tmp; + tmp.add(goto_programt::make_decl(decl.symbol())); - if(value) + if(optionalt value = decl.initial_value()) { decl.set_initial_value({}); + tmp.add(goto_programt::make_assignment(decl.symbol(), std::move(*value))); } - goto_programt tmp; - tmp.add(goto_programt::make_decl(decl.symbol())); - - if(value) - tmp.add(goto_programt::make_assignment(decl.symbol(), *value)); - tmp.add(goto_programt::make_end_function()); // goto_program2codet requires valid location numbers: From 541cd8a1cd08d6223f4a3dcbd9a5cc865bca4853 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 17 Feb 2021 18:01:28 +0000 Subject: [PATCH 08/11] Use `set_initial_value` in `format` unit test To avoid directly setting the operands. --- unit/util/format.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/unit/util/format.cpp b/unit/util/format.cpp index b1c4718f5e9..caf2d15139b 100644 --- a/unit/util/format.cpp +++ b/unit/util/format.cpp @@ -17,6 +17,6 @@ TEST_CASE("Format a declaration statement.", "[core][util][format]") const signedbv_typet int_type{32}; code_declt declaration{symbol_exprt{"foo", int_type}}; REQUIRE(format_to_string(declaration) == "decl signedbv[32] foo;"); - declaration.add_to_operands(int_type.zero_expr()); + declaration.set_initial_value({int_type.zero_expr()}); REQUIRE(format_to_string(declaration) == "decl signedbv[32] foo = 0;"); } From 111d05f5f07e600471fa4addf3a6f344f943e00e Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 17 Feb 2021 18:09:15 +0000 Subject: [PATCH 09/11] Refactor formatting of `code_declt` to use `initial_value()` To avoid directly accessing the operands. --- src/util/format_expr.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index b69d1bcfc9e..313eb8b1241 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -354,13 +354,13 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr) { return os << "dead " << format(to_code_dead(code).symbol()) << ";"; } - else if(statement == ID_decl) + else if(const auto decl = expr_try_dynamic_cast(code)) { - const auto &declaration_symb = to_code_decl(code).symbol(); + const auto &declaration_symb = decl->symbol(); os << "decl " << format(declaration_symb.type()) << " " << format(declaration_symb); - if(code.operands().size() > 1) - os << " = " << format(code.op1()); + if(const optionalt initial_value = decl->initial_value()) + os << " = " << format(*initial_value); return os << ";"; } else if(statement == ID_function_call) From 0d0b964c269e2f247b02213be8fe9d9a43b9f9dd Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 18 Feb 2021 15:01:44 +0000 Subject: [PATCH 10/11] Add no initialisation PRECONDITION to `wp_decl` This function does not account for the case where a code_declt contains `initialization`. Given that the test suite passes with this PRECONDITION is in place, such statements must be separated out before this function is reached. Should this condition be violated in future, then the CONDITION can be removed and the handling of this case implemented. --- src/goto-programs/wp.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp index c8ce71ae28b..750100cb7aa 100644 --- a/src/goto-programs/wp.cpp +++ b/src/goto-programs/wp.cpp @@ -226,6 +226,7 @@ exprt wp_decl( const exprt &post, const namespacet &ns) { + PRECONDITION(!code.initial_value()); // Model decl(var) as var = nondet() const exprt &var = code.symbol(); side_effect_expr_nondett nondet(var.type(), source_locationt()); From dae3eca4c5352c8011a32c7d375429cfe205beb2 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 19 Feb 2021 11:41:21 +0000 Subject: [PATCH 11/11] Add INVARIANTs that goto declarations may not initialize Initializations must be sepearated out of `code_declt` into a separate assignment before adding to goto program. This is the case already. These new INVARIANTs check that this continues to be true. --- src/goto-programs/goto_program.h | 10 +++++++++- src/util/std_code.h | 4 ++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index b352abc987e..b461b7f0c6f 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -199,13 +199,21 @@ class goto_programt const code_declt &get_decl() const { PRECONDITION(is_decl()); - return to_code_decl(code); + const auto &decl = expr_checked_cast(code); + INVARIANT( + !decl.initial_value(), + "code_declt in goto program may not contain initialization."); + return decl; } /// Set the declaration for DECL void set_decl(code_declt c) { PRECONDITION(is_decl()); + INVARIANT( + !c.initial_value(), + "Initialization must be separated from code_declt before adding to " + "goto_instructiont."); code = std::move(c); } diff --git a/src/util/std_code.h b/src/util/std_code.h index 4ee41e38583..ffa1c698e15 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -422,6 +422,8 @@ class code_declt:public codet /// Returns the initial value to which the declared variable is initialized, /// or empty in the case where no initialisation is included. + /// \note: Initial values may be present in the front end but they must be + /// separated into a separate assignment when used in a `goto_instructiont`. optionalt initial_value() const { if(operands().size() < 2) @@ -431,6 +433,8 @@ class code_declt:public codet /// Sets the value to which this declaration initializes the declared /// variable. Empty optional maybe passed to remove existing initialisation. + /// \note: Initial values may be present in the front end but they must be + /// separated into a separate assignment when used in a `goto_instructiont`. void set_initial_value(optionalt initial_value) { if(!initial_value)