diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index f7b95062134..10653ada420 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -57,29 +57,33 @@ bool ai_domain_baset::ai_simplify_lhs( if(condition.id()==ID_index) { index_exprt ie=to_index_expr(condition); - bool changed=ai_simplify(ie.index(), ns); - if(changed) + bool no_simplification=ai_simplify(ie.index(), ns); + if(!no_simplification) condition=simplify_expr(ie, ns); - return !changed; + return no_simplification; } else if(condition.id()==ID_dereference) { dereference_exprt de=to_dereference_expr(condition); - bool changed=ai_simplify(de.pointer(), ns); - if(changed) + bool no_simplification=ai_simplify(de.pointer(), ns); + if(!no_simplification) condition=simplify_expr(de, ns); // So *(&x) -> x - return !changed; + return no_simplification; } else if(condition.id()==ID_member) { member_exprt me=to_member_expr(condition); - bool changed=ai_simplify_lhs(me.compound(), ns); // <-- lhs! - if(changed) + // Since simplify_ai_lhs is required to return an addressable object + // (so remains a valid left hand side), to simplify + // `(something_simplifiable).b` we require that `something_simplifiable` + // must also be addressable + bool no_simplification=ai_simplify_lhs(me.compound(), ns); + if(!no_simplification) condition=simplify_expr(me, ns); - return !changed; + return no_simplification; } else return true; diff --git a/unit/Makefile b/unit/Makefile index f329e489773..3e5bb48afbe 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -7,6 +7,7 @@ SRC = src/expr/require_expr.cpp \ # Test source files SRC += unit_tests.cpp \ + analyses/ai/ai_simplify_lhs.cpp \ analyses/does_remove_const/does_expr_lose_const.cpp \ analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp new file mode 100644 index 00000000000..2d276fdbbd8 --- /dev/null +++ b/unit/analyses/ai/ai_simplify_lhs.cpp @@ -0,0 +1,168 @@ +/*******************************************************************\ + + Module: Unit tests for ai_domain_baset::ai_simplify_lhs + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Unit tests for ai_domain_baset::ai_simplify_lhs + +#include + +#include + +#include + +#include +#include +#include +#include +#include + +class constant_simplification_mockt:public ai_domain_baset +{ +public: + void transform(locationt, locationt, ai_baset &, const namespacet &) override + {} + void make_bottom() override + {} + void make_top() override + {} + void make_entry() override + {} + + bool ai_simplify(exprt &condition, const namespacet &ns) const override; +}; + +bool constant_simplification_mockt::ai_simplify( + exprt &condition, const namespacet &ns) const +{ + exprt simplified_expr=simplify_expr(condition, ns); + // no simplification + if(simplified_expr==condition) + { + return true; + } + // a simplification has occurred + condition=simplified_expr; + return false; +} + +SCENARIO("ai_domain_baset::ai_simplify_lhs", + "[core][analyses][ai][ai_simplify_lhs]") +{ + ui_message_handlert message_handler; + ansi_c_languaget language; + language.set_message_handler(message_handler); + + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + constant_simplification_mockt mock_ai_domain; + + config.set_arch("none"); + + GIVEN("A index_exprt") + { + // Construct an expression that the simplify_expr can simplify + exprt simplifiable_expression; + bool compile_failed= + language.to_expr("1 + 1", "", simplifiable_expression, ns); + + const unsigned int array_size=5; + array_typet array_type( + signedbv_typet(32), constant_exprt::integer_constant(array_size)); + + // Verify the results of the setup + REQUIRE_FALSE(compile_failed);\ + REQUIRE(simplifiable_expression.id()==ID_plus); + exprt simplified_version=simplify_expr(simplifiable_expression, ns); + REQUIRE(simplified_version.id()==ID_constant); + + WHEN( + "Simplifying an index expression with constant index but variable array") + { + const index_exprt &index_expr= + index_exprt(symbol_exprt("a", array_type), simplifiable_expression); + + THEN("Then only the index of the part of the expression should be " + "simplified") + { + exprt out_expr=index_expr; + bool no_simplification=mock_ai_domain.ai_simplify_lhs(out_expr, ns); + REQUIRE_FALSE(no_simplification); + REQUIRE(index_expr.id()==ID_index); + + index_exprt simplified_index_expr=to_index_expr(out_expr); + REQUIRE(simplified_index_expr.index().id()==ID_constant); + + constant_exprt constant_index= + to_constant_expr(simplified_index_expr.index()); + + mp_integer out_index; + bool failed_to_integer=to_integer(constant_index, out_index); + REQUIRE_FALSE(failed_to_integer); + REQUIRE(out_index==2); + } + } + WHEN("Simplifying an index expression with variable index and array") + { + // a[i] + const index_exprt &index_expr= + index_exprt( + symbol_exprt("a", array_type), symbol_exprt("i", signedbv_typet(32))); + + THEN("Then no simplification should occur") + { + exprt out_expr=index_expr; + bool no_simplification=mock_ai_domain.ai_simplify_lhs(out_expr, ns); + REQUIRE(no_simplification); + REQUIRE(index_expr.id()==ID_index); + + index_exprt simplified_index_expr=to_index_expr(out_expr); + REQUIRE(simplified_index_expr.index().id()==ID_symbol); + } + } + + // This fails since the implementation does do a constant simplification + // on the array part. It isn't clear to me if this is correct +#if 0 + WHEN( + "Simplifying an index expression with constant index in a constant array") + { + array_exprt constant_array=array_exprt(array_type); + for(unsigned int i=0; i