From dcc9d799a105010c40ec0676999283e754d64ad8 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 10 Jun 2019 11:09:42 +0100 Subject: [PATCH 1/7] Declare try_evaluate_pointer_comparisons in header This is so that we can unit-test this function. --- src/goto-symex/goto_symex.h | 16 ++++++++++++++++ src/goto-symex/symex_goto.cpp | 12 +----------- 2 files changed, 17 insertions(+), 11 deletions(-) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 12be632efb2..d5b6075f34b 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -726,4 +726,20 @@ void symex_transition( goto_programt::const_targett to, bool is_backwards_goto); +/// Try to evaluate pointer comparisons where they can be trivially determined +/// using the value-set. This is optional as all it does is allow symex to +/// resolve some comparisons itself and therefore create a simpler formula for +/// the SAT solver. +/// \param [in,out] condition: An L2-renamed expression with boolean type +/// \param value_set: The value-set for determining what pointer-typed symbols +/// might possibly point to +/// \param language_mode: The language mode +/// \param ns: A namespace +/// \return The possibly modified condition +renamedt try_evaluate_pointer_comparisons( + renamedt condition, + const value_sett &value_set, + const irep_idt &language_mode, + const namespacet &ns); + #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index de4640cc563..a78b59decf3 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -196,17 +196,7 @@ static optionalt> try_evaluate_pointer_comparison( expr.id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns); } -/// Try to evaluate pointer comparisons where they can be trivially determined -/// using the value-set. This is optional as all it does is allow symex to -/// resolve some comparisons itself and therefore create a simpler formula for -/// the SAT solver. -/// \param [in,out] condition: An L2-renamed expression with boolean type -/// \param value_set: The value-set for determining what pointer-typed symbols -/// might possibly point to -/// \param language_mode: The language mode -/// \param ns: A namespace -/// \return The possibly modified condition -static renamedt try_evaluate_pointer_comparisons( +renamedt try_evaluate_pointer_comparisons( renamedt condition, const value_sett &value_set, const irep_idt &language_mode, From 1c01ee77d2ea6bcc94fbcf1e3722440078a7ee83 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 10 Jun 2019 11:42:09 +0100 Subject: [PATCH 2/7] Unit test for try_evaluate_pointer_comparisions --- unit/Makefile | 1 + .../try_evaluate_pointer_comparisons.cpp | 130 ++++++++++++++++++ 2 files changed, 131 insertions(+) create mode 100644 unit/goto-symex/try_evaluate_pointer_comparisons.cpp diff --git a/unit/Makefile b/unit/Makefile index c0e7f71a2ae..a38aa67ced4 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -35,6 +35,7 @@ SRC += analyses/ai/ai.cpp \ goto-symex/is_constant.cpp \ goto-symex/symex_level0.cpp \ goto-symex/symex_level1.cpp \ + goto-symex/try_evaluate_pointer_comparisons.cpp \ interpreter/interpreter.cpp \ json/json_parser.cpp \ json_symbol_table.cpp \ diff --git a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp new file mode 100644 index 00000000000..d2d66dfc770 --- /dev/null +++ b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp @@ -0,0 +1,130 @@ +/*******************************************************************\ + +Module: Unit tests for try_evaluate_pointer_comparisons + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#include +#include + +#include +#include + +static void add_to_symbol_table( + symbol_tablet &symbol_table, + const symbol_exprt &symbol_expr) +{ + symbolt symbol; + symbol.name = symbol_expr.get_identifier(); + symbol.type = symbol_expr.type(); + symbol.value = symbol_expr; + symbol.is_thread_local = true; + symbol_table.insert(symbol); +} + +SCENARIO( + "Try to evaluate pointer comparisons", + "[core][goto-symex][try_evaluate_pointer_comparisons]") +{ + const unsignedbv_typet int_type{32}; + const pointer_typet ptr_type = pointer_type(int_type); + const symbol_exprt ptr1{"ptr1", ptr_type}; + const symbol_exprt ptr2{"ptr2", ptr_type}; + const symbol_exprt value1{"value1", int_type}; + const address_of_exprt address1{value1}; + const symbol_exprt value2{"value2", int_type}; + const address_of_exprt address2{value2}; + const symbol_exprt b{"b", bool_typet{}}; + + // Add symbols to symbol table + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + add_to_symbol_table(symbol_table, ptr1); + add_to_symbol_table(symbol_table, ptr2); + add_to_symbol_table(symbol_table, value1); + add_to_symbol_table(symbol_table, value2); + add_to_symbol_table(symbol_table, b); + + // Initialize goto state + std::list target; + symex_targett::sourcet source{"fun", target.begin()}; + guard_managert guard_manager; + std::size_t count = 0; + auto fresh_name = [&count](const irep_idt &) { return count++; }; + goto_symex_statet state{source, guard_manager, fresh_name}; + + GIVEN("A value set in which pointer symbol `ptr1` only points to `&value1`") + { + value_sett value_set; + const renamedt ptr1_l1 = state.rename(ptr1, ns); + const renamedt address1_l1 = state.rename(address1, ns); + // ptr1 <- &value1 + value_set.assign(ptr1_l1.get(), address1_l1.get(), ns, false, false); + + WHEN("Evaluating ptr1 == &value1") + { + const equal_exprt comparison{ptr1, address1}; + const renamedt renamed_comparison = + state.rename(comparison, ns); + auto result = try_evaluate_pointer_comparisons( + renamed_comparison, value_set, ID_java, ns); + THEN("Evaluation succeeds") + { + REQUIRE(result.get() == true_exprt{}); + } + } + + WHEN("Evaluating ptr1 != &value1") + { + const notequal_exprt comparison{ptr1, address1}; + const renamedt renamed_comparison = + state.rename(comparison, ns); + auto result = try_evaluate_pointer_comparisons( + renamed_comparison, value_set, ID_java, ns); + THEN("Evaluation succeeds") + { + REQUIRE(result.get() == false_exprt{}); + } + } + + WHEN("Evaluating ptr1 == ptr2") + { + const equal_exprt comparison{ptr1, ptr2}; + const renamedt renamed_comparison = + state.rename(comparison, ns); + auto result = try_evaluate_pointer_comparisons( + renamed_comparison, value_set, ID_java, ns); + THEN("Evaluation leaves the expression unchanged") + { + REQUIRE(result.get() == renamed_comparison.get()); + } + } + } + + GIVEN( + "A value set in which pointer symbol `ptr1` can point to `&value1` or " + "`&value2`") + { + value_sett value_set; + const if_exprt if_expr{b, address1, address2}; + const renamedt ptr1_l1 = state.rename(ptr1, ns); + const renamedt if_expr_l1 = state.rename(if_expr, ns); + // ptr1 <- b ? &value1 : &value2 + value_set.assign(ptr1_l1.get(), if_expr_l1.get(), ns, false, false); + + WHEN("Evaluating ptr1 == &value1") + { + const equal_exprt comparison{ptr1, address1}; + const renamedt renamed_comparison = + state.rename(comparison, ns); + auto result = try_evaluate_pointer_comparisons( + renamed_comparison, value_set, ID_java, ns); + THEN("Evaluation leaves the expression unchanged") + { + REQUIRE(result.get() == renamed_comparison.get()); + } + } + } +} From 2c3488649c6799be359a42abefeb363c763bdd86 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 10 Jun 2019 09:13:04 +0100 Subject: [PATCH 3/7] Replace use of get_l1_object by remove_level_2 get_l1_object suggests we are comparing the address of the object, but the actually should interpret the symbol itself as a pointer. A unit test for the case of the issue that is fixed will be added in a following commit. --- src/goto-symex/symex_goto.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index a78b59decf3..bbc5ff6e427 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -100,8 +100,10 @@ static optionalt> try_evaluate_pointer_comparison( const ssa_exprt *ssa_symbol_expr = expr_try_dynamic_cast(symbol_expr); + ssa_exprt l1_expr{*ssa_symbol_expr}; + l1_expr.remove_level_2(); const std::vector value_set_elements = - value_set.get_value_set(ssa_symbol_expr->get_l1_object(), ns); + value_set.get_value_set(l1_expr, ns); bool constant_found = false; From e26f4cd523f751cb6c3f5f6614343a28f0a8d983 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 11 Jun 2019 08:21:22 +0100 Subject: [PATCH 4/7] Check pointer evaluation in the member case Field sensitivity the value set to keep track of pointers in individal fields, making it possible to evaluate equalities such as the one in the example. This is a case which would not work if try_evaluate_pointer_comparisons was using get_l1_object_identifier instead of getting the identifier of the whole l1 expression (not the underlying object). fixup! Check pointer evaluation in the array case --- .../try_evaluate_pointer_comparisons.cpp | 52 +++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp index d2d66dfc770..67172446201 100644 --- a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp +++ b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp @@ -10,6 +10,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include +#include #include static void add_to_symbol_table( @@ -127,4 +128,55 @@ SCENARIO( } } } + + GIVEN("A struct whose first element can only point to `&value1`") + { + // member is `struct_symbol.pointer_field` + const member_exprt member = [&]() { + std::vector components; + components.emplace_back("pointer_field", ptr_type); + const struct_typet struct_type{components}; + const symbol_exprt struct_symbol{"struct_symbol", struct_type}; + add_to_symbol_table(symbol_table, struct_symbol); + return member_exprt{struct_symbol, components.back()}; + }(); + + value_sett value_set; + const renamedt member_l1 = state.rename(member, ns); + const renamedt address1_l1 = state.rename(address1, ns); + + // struct_symbol..pointer_field <- &value1 + { + field_sensitivityt field_sensitivity; + const exprt index_fs = + field_sensitivity.apply(ns, state, member_l1.get(), true); + value_set.assign(index_fs, address1_l1.get(), ns, false, false); + } + + WHEN("Evaluating struct_symbol.pointer_field == &value1") + { + const equal_exprt comparison{member, address1}; + const renamedt renamed_comparison = + state.rename(comparison, ns); + auto result = try_evaluate_pointer_comparisons( + renamed_comparison, value_set, ID_java, ns); + THEN("Evaluation succeeds") + { + REQUIRE(result.get() == true_exprt{}); + } + } + + WHEN("Evaluating struct_symbol.pointer_field == &value2") + { + const equal_exprt comparison{member, address2}; + const renamedt renamed_comparison = + state.rename(comparison, ns); + auto result = try_evaluate_pointer_comparisons( + renamed_comparison, value_set, ID_java, ns); + THEN("Evaluation succeeds") + { + REQUIRE(result.get() == false_exprt{}); + } + } + } } From 7272dfb7815ac3c82a03bb66a7c8da61ab20e7a2 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 11 Jun 2019 16:24:21 +0100 Subject: [PATCH 5/7] Add case to try_evaluate_pointer_comparisons test This test the case where ptr1 can point to value1 or value2 and we evaluate `ptr1 != &value1` --- .../goto-symex/try_evaluate_pointer_comparisons.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp index 67172446201..ee6a778515e 100644 --- a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp +++ b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp @@ -127,6 +127,19 @@ SCENARIO( REQUIRE(result.get() == renamed_comparison.get()); } } + + WHEN("Evaluating ptr1 != &value1") + { + const notequal_exprt comparison{ptr1, address1}; + const renamedt renamed_comparison = + state.rename(comparison, ns); + auto result = try_evaluate_pointer_comparisons( + renamed_comparison, value_set, ID_java, ns); + THEN("Evaluation leaves the expression unchanged") + { + REQUIRE(result.get() == renamed_comparison.get()); + } + } } GIVEN("A struct whose first element can only point to `&value1`") From c024823a006df36d2e5ea8e6c64649ba0115ee37 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 11 Jun 2019 16:28:03 +0100 Subject: [PATCH 6/7] Add case for evaluate pointer comparison with null This check the case where ptr1 is either &value1 or &value2 and we compare it to null. --- .../try_evaluate_pointer_comparisons.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp index ee6a778515e..4ca7bdee24f 100644 --- a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp +++ b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp @@ -38,6 +38,7 @@ SCENARIO( const symbol_exprt value2{"value2", int_type}; const address_of_exprt address2{value2}; const symbol_exprt b{"b", bool_typet{}}; + const null_pointer_exprt null_ptr{ptr_type}; // Add symbols to symbol table symbol_tablet symbol_table; @@ -140,6 +141,19 @@ SCENARIO( REQUIRE(result.get() == renamed_comparison.get()); } } + + WHEN("Evaluating ptr1 != nullptr") + { + const notequal_exprt comparison{ptr1, null_ptr}; + const renamedt renamed_comparison = + state.rename(comparison, ns); + auto result = try_evaluate_pointer_comparisons( + renamed_comparison, value_set, ID_java, ns); + THEN("Evaluation succeeds") + { + REQUIRE(result.get() == true_exprt{}); + } + } } GIVEN("A struct whose first element can only point to `&value1`") From 767d8f09ff7d519fc64c2f11b5e912050d5d3e40 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 11 Jun 2019 16:32:03 +0100 Subject: [PATCH 7/7] Test try_evaluate_pointer_comparisons unknown case This adds a unit test for the case where the value set contains unknown. In that case no comparison can be decided. --- .../try_evaluate_pointer_comparisons.cpp | 52 +++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp index 4ca7bdee24f..7a6f186ba31 100644 --- a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp +++ b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp @@ -156,6 +156,58 @@ SCENARIO( } } + GIVEN( + "A value set in which pointer symbol `ptr1` can point to `&value1` or " + "`unknown`") + { + value_sett value_set; + const exprt unknown_expr{ID_unknown, ptr_type}; + const if_exprt if_expr{b, address1, unknown_expr}; + const renamedt ptr1_l1 = state.rename(ptr1, ns); + const renamedt if_expr_l1 = state.rename(if_expr, ns); + // ptr1 <- b ? &value1 : unknown + value_set.assign(ptr1_l1.get(), if_expr_l1.get(), ns, false, false); + + WHEN("Evaluating ptr1 == &value1") + { + const equal_exprt comparison{ptr1, address1}; + const renamedt renamed_comparison = + state.rename(comparison, ns); + auto result = try_evaluate_pointer_comparisons( + renamed_comparison, value_set, ID_java, ns); + THEN("Evaluation leaves the expression unchanged") + { + REQUIRE(result.get() == renamed_comparison.get()); + } + } + + WHEN("Evaluating ptr1 != &value1") + { + const notequal_exprt comparison{ptr1, address1}; + const renamedt renamed_comparison = + state.rename(comparison, ns); + auto result = try_evaluate_pointer_comparisons( + renamed_comparison, value_set, ID_java, ns); + THEN("Evaluation leaves the expression unchanged") + { + REQUIRE(result.get() == renamed_comparison.get()); + } + } + + WHEN("Evaluating ptr1 != nullptr") + { + const notequal_exprt comparison{ptr1, null_ptr}; + const renamedt renamed_comparison = + state.rename(comparison, ns); + auto result = try_evaluate_pointer_comparisons( + renamed_comparison, value_set, ID_java, ns); + THEN("Evaluation leaves the expression unchanged") + { + REQUIRE(result.get() == renamed_comparison.get()); + } + } + } + GIVEN("A struct whose first element can only point to `&value1`") { // member is `struct_symbol.pointer_field`