From 64b6a6aa511c62ba748719d648ef5e4db82abbd9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Nov 2018 21:14:15 +0000 Subject: [PATCH 01/10] Mark tests using --variable as FUTURE This option is not currently supported, there is no known bug here. --- .../goto-analyzer/sensitivity-function-call-recursive/test.desc | 2 +- .../test.desc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/goto-analyzer/sensitivity-function-call-recursive/test.desc b/regression/goto-analyzer/sensitivity-function-call-recursive/test.desc index 8a270462a0c..6303fef7078 100644 --- a/regression/goto-analyzer/sensitivity-function-call-recursive/test.desc +++ b/regression/goto-analyzer/sensitivity-function-call-recursive/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c --variable --pointers --arrays --structs --verify ^EXIT=0$ diff --git a/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/test.desc b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/test.desc index f0241fbcee8..234895fc2dd 100644 --- a/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/test.desc +++ b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE sensitivity_test_constants_pointer_to_constants_struct.c --variable --pointers --structs --verify ^EXIT=0$ From edcf7b856e66b1bccc8a761eda44963bbe767653 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Nov 2018 21:10:19 +0000 Subject: [PATCH 02/10] Update test results and mark tests as passing Several tests already pass without any code modifications. --- regression/goto-analyzer/constant_propagation_03/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_04/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_05/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_07/test.desc | 6 +++--- regression/goto-analyzer/constant_propagation_12/test.desc | 6 +++--- regression/goto-analyzer/constant_propagation_13/test.desc | 4 ++-- 6 files changed, 14 insertions(+), 14 deletions(-) diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc index ffe6d41d638..6a28820a4b0 100644 --- a/regression/goto-analyzer/constant_propagation_03/test.desc +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -1,9 +1,9 @@ -FUTURE +CORE main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc index ffe6d41d638..6a28820a4b0 100644 --- a/regression/goto-analyzer/constant_propagation_04/test.desc +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -1,9 +1,9 @@ -FUTURE +CORE main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_05/test.desc b/regression/goto-analyzer/constant_propagation_05/test.desc index 039a68bf791..2a351a220f9 100644 --- a/regression/goto-analyzer/constant_propagation_05/test.desc +++ b/regression/goto-analyzer/constant_propagation_05/test.desc @@ -1,8 +1,8 @@ -FUTURE +CORE main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 12 function main, assertion j != 3: FAILURE \(if reachable\)$ +^\[main.assertion.1\] line 11 assertion j != 3: FAILURE \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index c4b03cd8738..291f5339049 100644 --- a/regression/goto-analyzer/constant_propagation_07/test.desc +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -1,9 +1,9 @@ -FUTURE +CORE main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 4, assigns: 10, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 11, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc index 208b235ccd5..df5dd997788 100644 --- a/regression/goto-analyzer/constant_propagation_12/test.desc +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -1,9 +1,9 @@ -FUTURE +CORE main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 4, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 2, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_13/test.desc b/regression/goto-analyzer/constant_propagation_13/test.desc index 9f9186ad98e..91a78a1df7a 100644 --- a/regression/goto-analyzer/constant_propagation_13/test.desc +++ b/regression/goto-analyzer/constant_propagation_13/test.desc @@ -1,8 +1,8 @@ -FUTURE +CORE main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion y == 0: FAILURE \(if reachable\)$ +^\[main.assertion.1\] line 9 assertion y == 0: FAILURE \(if reachable\)$ -- ^warning: ignoring From fe8d1db9579076e5c19a6a1db416e85ce3a03e21 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 10 Nov 2018 13:45:17 +0000 Subject: [PATCH 03/10] Constant propagation: genuinely use the argument passed to assign_rec The "values" parameter shadowed the class member values, which, however, was used by functions called by assign_rec. Thus they possibly operate on two different sets of values. --- src/analyses/constant_propagator.cpp | 51 ++++++++++++++++------------ src/analyses/constant_propagator.h | 19 +++++++---- 2 files changed, 42 insertions(+), 28 deletions(-) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index e976107b19d..c1e3a3b4545 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -29,7 +29,7 @@ Author: Peter Schrammel #include void constant_propagator_domaint::assign_rec( - valuest &values, + valuest &dest_values, const exprt &lhs, const exprt &rhs, const namespacet &ns, @@ -44,17 +44,17 @@ void constant_propagator_domaint::assign_rec( const symbol_exprt &s=to_symbol_expr(lhs); exprt tmp=rhs; - partial_evaluate(tmp, ns); + partial_evaluate(dest_values, tmp, ns); if(tmp.is_constant()) { DATA_INVARIANT( base_type_eq(ns.lookup(s).type, tmp.type(), ns), "type of constant to be replaced should match"); - values.set_to(s, tmp); + dest_values.set_to(s, tmp); } else - values.set_to_top(s); + dest_values.set_to_top(s); } void constant_propagator_domaint::transform( @@ -117,7 +117,7 @@ void constant_propagator_domaint::transform( g = from->guard; else g = not_exprt(from->guard); - partial_evaluate(g, ns); + partial_evaluate(values, g, ns); if(g.is_false()) values.set_to_bottom(); else @@ -289,7 +289,7 @@ bool constant_propagator_domaint::ai_simplify( exprt &condition, const namespacet &ns) const { - return partial_evaluate(condition, ns); + return partial_evaluate(values, condition, ns); } @@ -531,30 +531,36 @@ bool constant_propagator_domaint::merge( /// Attempt to evaluate expression using domain knowledge /// This function changes the expression that is passed into it. +/// \param known_values: The constant values under which to evaluate \p expr /// \param expr The expression to evaluate /// \param ns The namespace for symbols in the expression /// \return True if the expression is unchanged, false otherwise bool constant_propagator_domaint::partial_evaluate( + const valuest &known_values, exprt &expr, - const namespacet &ns) const + const namespacet &ns) { // if the current rounding mode is top we can // still get a non-top result by trying all rounding // modes and checking if the results are all the same - if(!values.is_constant(symbol_exprt(ID_cprover_rounding_mode_str))) + if(!known_values.is_constant(symbol_exprt(ID_cprover_rounding_mode_str))) { - return partial_evaluate_with_all_rounding_modes(expr, ns); + return partial_evaluate_with_all_rounding_modes(known_values, expr, ns); } - return replace_constants_and_simplify(expr, ns); + return replace_constants_and_simplify(known_values, expr, ns); } /// Attempt to evaluate an expression in all rounding modes. /// -/// If the result is the same for all rounding modes, change +/// \param known_values: The constant values under which to evaluate \p expr +/// \param expr The expression to evaluate +/// \param ns The namespace for symbols in the expression +/// \return If the result is the same for all rounding modes, change /// expr to that result and return false. Otherwise, return true. bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes( + const valuest &known_values, exprt &expr, - const namespacet &ns) const + const namespacet &ns) { // NOLINTNEXTLINE (whitespace/braces) auto rounding_modes = std::array{ // NOLINTNEXTLINE (whitespace/braces) @@ -566,12 +572,12 @@ bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes( exprt first_result; for(std::size_t i = 0; i < rounding_modes.size(); ++i) { - constant_propagator_domaint child(*this); - child.values.set_to( + valuest tmp_values = known_values; + tmp_values.set_to( symbol_exprt(ID_cprover_rounding_mode_str, integer_typet()), from_integer(rounding_modes[i], integer_typet())); exprt result = expr; - if(child.replace_constants_and_simplify(result, ns)) + if(replace_constants_and_simplify(tmp_values, result, ns)) { return true; } @@ -589,10 +595,11 @@ bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes( } bool constant_propagator_domaint::replace_constants_and_simplify( + const valuest &known_values, exprt &expr, - const namespacet &ns) const + const namespacet &ns) { - bool did_not_change_anything = values.replace_const.replace(expr); + bool did_not_change_anything = known_values.replace_const.replace(expr); did_not_change_anything &= simplify(expr, ns); return did_not_change_anything; } @@ -623,12 +630,12 @@ void constant_propagator_ait::replace( if(it->is_goto() || it->is_assume() || it->is_assert()) { - d.partial_evaluate(it->guard, ns); + constant_propagator_domaint::partial_evaluate(d.values, it->guard, ns); } else if(it->is_assign()) { exprt &rhs=to_code_assign(it->code).rhs(); - d.partial_evaluate(rhs, ns); + constant_propagator_domaint::partial_evaluate(d.values, rhs, ns); if(rhs.id()==ID_constant) rhs.add_source_location() = @@ -637,21 +644,21 @@ void constant_propagator_ait::replace( else if(it->is_function_call()) { exprt &function = to_code_function_call(it->code).function(); - d.partial_evaluate(function, ns); + constant_propagator_domaint::partial_evaluate(d.values, function, ns); exprt::operandst &args= to_code_function_call(it->code).arguments(); for(auto &arg : args) { - d.partial_evaluate(arg, ns); + constant_propagator_domaint::partial_evaluate(d.values, arg, ns); } } else if(it->is_other()) { if(it->code.get_statement()==ID_expression) { - d.partial_evaluate(it->code, ns); + constant_propagator_domaint::partial_evaluate(d.values, it->code, ns); } } } diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 6edef4a513b..26ba95ff299 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -137,11 +137,14 @@ class constant_propagator_domaint:public ai_domain_baset valuest values; - bool partial_evaluate(exprt &expr, const namespacet &ns) const; + static bool partial_evaluate( + const valuest &known_values, + exprt &expr, + const namespacet &ns); protected: - void assign_rec( - valuest &values, + static void assign_rec( + valuest &dest_values, const exprt &lhs, const exprt &rhs, const namespacet &ns, @@ -152,11 +155,15 @@ class constant_propagator_domaint:public ai_domain_baset const namespacet &ns, const constant_propagator_ait *cp); - bool partial_evaluate_with_all_rounding_modes( + static bool partial_evaluate_with_all_rounding_modes( + const valuest &known_values, exprt &expr, - const namespacet &ns) const; + const namespacet &ns); - bool replace_constants_and_simplify(exprt &expr, const namespacet &ns) const; + static bool replace_constants_and_simplify( + const valuest &known_values, + exprt &expr, + const namespacet &ns); }; class constant_propagator_ait:public ait From 87794c57f0096eb24317443d14bdc4e64fc87399 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 14 Nov 2018 14:31:57 +0000 Subject: [PATCH 04/10] Re-enable two-way constant propagation It has only been disabled on suspicion of being at fault for bugs, but these are quite possibly due to other bugs (cf. soundness fixes later in this series). --- .../constant_propagation_two_way_1/main.c | 11 +++++++++++ .../constant_propagation_two_way_1/test.desc | 8 ++++++++ src/analyses/constant_propagator.cpp | 13 +++---------- 3 files changed, 22 insertions(+), 10 deletions(-) create mode 100644 regression/goto-analyzer/constant_propagation_two_way_1/main.c create mode 100644 regression/goto-analyzer/constant_propagation_two_way_1/test.desc diff --git a/regression/goto-analyzer/constant_propagation_two_way_1/main.c b/regression/goto-analyzer/constant_propagation_two_way_1/main.c new file mode 100644 index 00000000000..f1b83128283 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_two_way_1/main.c @@ -0,0 +1,11 @@ +#include + +int main() +{ + int x; + if(x == 0) + { + assert(!x); + } + return 0; +} diff --git a/regression/goto-analyzer/constant_propagation_two_way_1/test.desc b/regression/goto-analyzer/constant_propagation_two_way_1/test.desc new file mode 100644 index 00000000000..79e9746229d --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_two_way_1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] line 8 assertion !x: SUCCESS$ +-- +^warning: ignoring diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index c1e3a3b4545..65bb482f25d 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -232,19 +232,15 @@ void constant_propagator_domaint::transform( /// handles equalities and conjunctions containing equalities bool constant_propagator_domaint::two_way_propagate_rec( const exprt &expr, - const namespacet &, + const namespacet &ns, const constant_propagator_ait *cp) { #ifdef DEBUG std::cout << "two_way_propagate_rec: " << format(expr) << '\n'; -#else - (void)expr; // unused parameter #endif bool change=false; - // this seems to be buggy at present -#if 0 if(expr.id()==ID_and) { // need a fixed point here to get the most out of it @@ -265,14 +261,11 @@ bool constant_propagator_domaint::two_way_propagate_rec( // two-way propagation valuest copy_values=values; - assign_rec(copy_values, lhs, rhs, ns); + assign_rec(copy_values, lhs, rhs, ns, cp); if(!values.is_constant(rhs) || values.is_constant(lhs)) - assign_rec(values, rhs, lhs, ns); + assign_rec(values, rhs, lhs, ns, cp); change = values.meet(copy_values, ns); } -#else - (void)cp; // unused parameter -#endif #ifdef DEBUG std::cout << "two_way_propagate_rec: " << change << '\n'; From 9e4425ad22f046464bb10c4df8924b4dbdf332ad Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 22 May 2018 12:09:32 +0000 Subject: [PATCH 05/10] address-of-dereference may also permit constant propagation --- src/util/expr_util.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index e20d823a84e..b94d1ae2e8a 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -270,6 +270,12 @@ bool is_constantt::is_constant_address_of(const exprt &expr) const { return is_constant_address_of(to_member_expr(expr).compound()); } + else if(expr.id() == ID_dereference) + { + const dereference_exprt &deref = to_dereference_expr(expr); + + return is_constant(deref.pointer()); + } else if(expr.id() == ID_string_constant) return true; From c23e8eefbf4e5797c684e5bc863d57fec536f02a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 27 Apr 2018 18:24:30 +0000 Subject: [PATCH 06/10] Use central is_constantt to identify constants for propagation --- src/analyses/constant_propagator.cpp | 60 ++++++++++------------------ src/analyses/constant_propagator.h | 2 - 2 files changed, 22 insertions(+), 40 deletions(-) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 65bb482f25d..9d0af5b0665 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -19,6 +19,7 @@ Author: Peter Schrammel #include #include #include +#include #include #include #include @@ -288,48 +289,31 @@ bool constant_propagator_domaint::ai_simplify( bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const { - if(expr.id()==ID_side_effect && - to_side_effect_expr(expr).get_statement()==ID_nondet) - return false; - - if(expr.id()==ID_side_effect && - to_side_effect_expr(expr).get_statement()==ID_allocate) - return false; - - if(expr.id()==ID_symbol) - if(!replace_const.replaces_symbol(to_symbol_expr(expr).get_identifier())) - return false; - - if(expr.id()==ID_index) - return false; - - if(expr.id()==ID_address_of) - return is_constant_address_of(to_address_of_expr(expr).object()); - - forall_operands(it, expr) - if(!is_constant(*it)) - return false; - - return true; -} - -bool constant_propagator_domaint::valuest::is_constant_address_of( - const exprt &expr) const -{ - if(expr.id()==ID_index) - return is_constant_address_of(to_index_expr(expr).array()) && - is_constant(to_index_expr(expr).index()); + class constant_propagator_is_constantt : public is_constantt + { + public: + explicit constant_propagator_is_constantt( + const replace_symbolt &replace_const) + : replace_const(replace_const) + { + } - if(expr.id()==ID_member) - return is_constant_address_of(to_member_expr(expr).struct_op()); + protected: + bool is_constant(const exprt &expr) const override + { + if(expr.id() == ID_symbol) + { + return replace_const.replaces_symbol( + to_symbol_expr(expr).get_identifier()); + } - if(expr.id()==ID_dereference) - return is_constant(to_dereference_expr(expr).pointer()); + return is_constantt::is_constant(expr); + } - if(expr.id()==ID_string_constant) - return true; + const replace_symbolt &replace_const; + }; - return true; + return constant_propagator_is_constantt(replace_const)(expr); } /// Do not call this when iterating over replace_const.expr_map! diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 26ba95ff299..c5bf6c55f1f 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -124,8 +124,6 @@ class constant_propagator_domaint:public ai_domain_baset void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns); bool is_constant(const exprt &expr) const; - bool is_array_constant(const exprt &expr) const; - bool is_constant_address_of(const exprt &expr) const; bool is_empty() const { From 22492886498d806869eff9525dc57941ea8c8748 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 27 Apr 2018 18:25:19 +0000 Subject: [PATCH 07/10] Use extended interpretation of "is constant" --- regression/goto-analyzer/constant_propagation_09/test.desc | 7 +++---- regression/goto-analyzer/constant_propagation_10/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_11/test.desc | 7 +++---- regression/goto-analyzer/constant_propagation_15/test.desc | 4 ++-- src/analyses/constant_propagator.cpp | 2 +- 5 files changed, 11 insertions(+), 13 deletions(-) diff --git a/regression/goto-analyzer/constant_propagation_09/test.desc b/regression/goto-analyzer/constant_propagation_09/test.desc index eebfe27dd49..494af088e03 100644 --- a/regression/goto-analyzer/constant_propagation_09/test.desc +++ b/regression/goto-analyzer/constant_propagation_09/test.desc @@ -1,9 +1,8 @@ -FUTURE +KNOWNBUG main.c ---constants --simplify out.gb +--constants --verify ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +^\[main.assertion.1\] line 9 assertion a\[(\(signed( long)? long int\))?0\] == 0: FAILURE \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_10/test.desc b/regression/goto-analyzer/constant_propagation_10/test.desc index 66b3fce7f71..e34ac581388 100644 --- a/regression/goto-analyzer/constant_propagation_10/test.desc +++ b/regression/goto-analyzer/constant_propagation_10/test.desc @@ -1,8 +1,8 @@ -FUTURE +CORE main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 10 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE$ +^\[main.assertion.1\] line 10 assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc index c3eb2ca93e9..53b1644b3dc 100644 --- a/regression/goto-analyzer/constant_propagation_11/test.desc +++ b/regression/goto-analyzer/constant_propagation_11/test.desc @@ -1,9 +1,8 @@ -FUTURE +KNOWNBUG main.c ---constants --simplify out.gb +--constants --verify ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 0, assigns: 0, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 0, function calls: 0$ +^\[main.assertion.1\] line 9 assertion a\[(\(signed( long)? long int\))?0\] == 1: SUCCESS$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_15/test.desc b/regression/goto-analyzer/constant_propagation_15/test.desc index 39a626cbfe1..bf760877b4a 100644 --- a/regression/goto-analyzer/constant_propagation_15/test.desc +++ b/regression/goto-analyzer/constant_propagation_15/test.desc @@ -1,8 +1,8 @@ -FUTURE +CORE main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE$ +^\[main.assertion.1\] line 9 assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE \(if reachable\)$ -- ^warning: ignoring diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 9d0af5b0665..01c7477b9e1 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -47,7 +47,7 @@ void constant_propagator_domaint::assign_rec( exprt tmp=rhs; partial_evaluate(dest_values, tmp, ns); - if(tmp.is_constant()) + if(dest_values.is_constant(tmp)) { DATA_INVARIANT( base_type_eq(ns.lookup(s).type, tmp.type(), ns), From 11f92da7e9280a874b0bbb6b916847b9830fc4a9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 27 Apr 2018 18:25:40 +0000 Subject: [PATCH 08/10] Expression rewriting may enable further constant propagation The included regression test is an example the requires interleaving of simplification and constant propagation. --- .../constant_propagation_14/test.desc | 6 +++--- .../constant_propagation_18/main.c | 8 +++++++ .../constant_propagation_18/test.desc | 8 +++++++ src/analyses/constant_propagator.cpp | 21 +++++++++++++++++-- 4 files changed, 38 insertions(+), 5 deletions(-) create mode 100644 regression/goto-analyzer/constant_propagation_18/main.c create mode 100644 regression/goto-analyzer/constant_propagation_18/test.desc diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc index 8ba5e9ba7d0..f2801862f9f 100644 --- a/regression/goto-analyzer/constant_propagation_14/test.desc +++ b/regression/goto-analyzer/constant_propagation_14/test.desc @@ -1,9 +1,9 @@ -FUTURE +KNOWNBUG main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 11 function main, assertion tmp_if_expr: SUCCESS$ -^\[main.assertion.2\] file main.c line 12 function main, assertion tmp_if_expr\$1: FAILURE$ +^\[main.assertion.1\] line 11 assertion tmp_if_expr: SUCCESS$ +^\[main.assertion.2\] line 12 assertion tmp_if_expr\$0: FAILURE \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_18/main.c b/regression/goto-analyzer/constant_propagation_18/main.c new file mode 100644 index 00000000000..6a42c1b597f --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_18/main.c @@ -0,0 +1,8 @@ +#include + +int main() +{ + int i = 1; + int *p = &i; + assert(*p == 1); +} diff --git a/regression/goto-analyzer/constant_propagation_18/test.desc b/regression/goto-analyzer/constant_propagation_18/test.desc new file mode 100644 index 00000000000..3594e0cdc8f --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_18/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] line 7 assertion \*p == 1: SUCCESS$ +-- +^warning: ignoring diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 01c7477b9e1..11018777326 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -576,8 +576,25 @@ bool constant_propagator_domaint::replace_constants_and_simplify( exprt &expr, const namespacet &ns) { - bool did_not_change_anything = known_values.replace_const.replace(expr); - did_not_change_anything &= simplify(expr, ns); + bool did_not_change_anything = true; + + // iterate constant propagation and simplification until we cannot + // constant-propagate any further - a prime example is pointer dereferencing, + // where constant propagation may have a value of the pointer, the simplifier + // takes care of evaluating dereferencing, and we might then have the value of + // the resulting symbol known to constant propagation and thus replace the + // dereferenced expression by a constant + while(!known_values.replace_const.replace(expr)) + { + did_not_change_anything = false; + simplify(expr, ns); + } + + // even if we haven't been able to constant-propagate anything, run the + // simplifier on the expression + if(did_not_change_anything) + did_not_change_anything &= simplify(expr, ns); + return did_not_change_anything; } From e367dbccf17fea6eecfea81f93fb6384ef0cb3b3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 14 Nov 2018 17:59:45 +0000 Subject: [PATCH 09/10] Constant propagation: Support non-symbol left-hand sides, soundness 1. Properly handle index, member, or dereference expressions on the left-hand side of assignments. 2. If we find something on the left-hand side that we don't support (maybe byte extracts, if-expressions, type casts, or maybe something else), set the entire value set to top to ensure soundness. --- .../constant_propagation_09/test.desc | 2 +- .../constant_propagation_11/test.desc | 2 +- .../constant_propagation_14/test.desc | 2 +- src/analyses/constant_propagator.cpp | 57 ++++++++++++++----- 4 files changed, 46 insertions(+), 17 deletions(-) diff --git a/regression/goto-analyzer/constant_propagation_09/test.desc b/regression/goto-analyzer/constant_propagation_09/test.desc index 494af088e03..1c0f0d10583 100644 --- a/regression/goto-analyzer/constant_propagation_09/test.desc +++ b/regression/goto-analyzer/constant_propagation_09/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --constants --verify ^EXIT=0$ diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc index 53b1644b3dc..8b5049d2894 100644 --- a/regression/goto-analyzer/constant_propagation_11/test.desc +++ b/regression/goto-analyzer/constant_propagation_11/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --constants --verify ^EXIT=0$ diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc index f2801862f9f..e74316180d5 100644 --- a/regression/goto-analyzer/constant_propagation_14/test.desc +++ b/regression/goto-analyzer/constant_propagation_14/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --constants --verify ^EXIT=0$ diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 11018777326..afb4a63778f 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -36,26 +36,55 @@ void constant_propagator_domaint::assign_rec( const namespacet &ns, const constant_propagator_ait *cp) { - if(lhs.id()!=ID_symbol) - return; + if(lhs.id() == ID_dereference) + { + const bool have_dirty = (cp != nullptr); - if(cp && !cp->should_track_value(lhs, ns)) - return; + if(have_dirty) + dest_values.set_dirty_to_top(cp->dirty, ns); + else + dest_values.set_to_top(); + } + else if(lhs.id() == ID_index) + { + const index_exprt &index_expr = to_index_expr(lhs); + with_exprt new_rhs(index_expr.array(), index_expr.index(), rhs); + assign_rec(dest_values, index_expr.array(), new_rhs, ns, cp); + } + else if(lhs.id() == ID_member) + { + const member_exprt &member_expr = to_member_expr(lhs); + with_exprt new_rhs(member_expr.compound(), exprt(ID_member_name), rhs); + new_rhs.where().set(ID_component_name, member_expr.get_component_name()); + assign_rec(dest_values, member_expr.compound(), new_rhs, ns, cp); + } + else if(lhs.id() == ID_symbol) + { + if(cp && !cp->should_track_value(lhs, ns)) + return; - const symbol_exprt &s=to_symbol_expr(lhs); + const symbol_exprt &s = to_symbol_expr(lhs); - exprt tmp=rhs; - partial_evaluate(dest_values, tmp, ns); + exprt tmp = rhs; + partial_evaluate(dest_values, tmp, ns); - if(dest_values.is_constant(tmp)) - { - DATA_INVARIANT( - base_type_eq(ns.lookup(s).type, tmp.type(), ns), - "type of constant to be replaced should match"); - dest_values.set_to(s, tmp); + if(dest_values.is_constant(tmp)) + { + DATA_INVARIANT( + base_type_eq(ns.lookup(s).type, tmp.type(), ns), + "type of constant to be replaced should match"); + dest_values.set_to(s, tmp); + } + else + dest_values.set_to_top(s); } else - dest_values.set_to_top(s); + { + // it's an assignment, but we don't really know what object is being written + // to on the left-hand side - bail and set all values to top to be on the + // safe side in terms of soundness + dest_values.set_to_top(); + } } void constant_propagator_domaint::transform( From 23596895e341d41fca4068645a8ddf2abf18ccce Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 14 Nov 2018 18:13:21 +0000 Subject: [PATCH 10/10] Use constant propagation to dereference left-hand sides We still fall back to setting values to top if dereferencing fails. --- .../goto-analyzer/constant_propagation_19/main.c | 10 ++++++++++ .../constant_propagation_19/test.desc | 8 ++++++++ src/analyses/constant_propagator.cpp | 14 ++++++++++---- 3 files changed, 28 insertions(+), 4 deletions(-) create mode 100644 regression/goto-analyzer/constant_propagation_19/main.c create mode 100644 regression/goto-analyzer/constant_propagation_19/test.desc diff --git a/regression/goto-analyzer/constant_propagation_19/main.c b/regression/goto-analyzer/constant_propagation_19/main.c new file mode 100644 index 00000000000..10f765f1958 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_19/main.c @@ -0,0 +1,10 @@ +#include + +int main() +{ + int x; + int *p = &x; + *p = 42; + assert(x == 42); + return 0; +} diff --git a/regression/goto-analyzer/constant_propagation_19/test.desc b/regression/goto-analyzer/constant_propagation_19/test.desc new file mode 100644 index 00000000000..a331e26fe28 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_19/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] line 8 assertion x == 42: SUCCESS$ +-- +^warning: ignoring diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index afb4a63778f..f8b469784ae 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -38,12 +38,18 @@ void constant_propagator_domaint::assign_rec( { if(lhs.id() == ID_dereference) { - const bool have_dirty = (cp != nullptr); + exprt eval_lhs = lhs; + if(partial_evaluate(dest_values, eval_lhs, ns)) + { + const bool have_dirty = (cp != nullptr); - if(have_dirty) - dest_values.set_dirty_to_top(cp->dirty, ns); + if(have_dirty) + dest_values.set_dirty_to_top(cp->dirty, ns); + else + dest_values.set_to_top(); + } else - dest_values.set_to_top(); + assign_rec(dest_values, eval_lhs, rhs, ns, cp); } else if(lhs.id() == ID_index) {