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..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; @@ -196,17 +198,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, 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..7a6f186ba31 --- /dev/null +++ b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp @@ -0,0 +1,261 @@ +/*******************************************************************\ + +Module: Unit tests for try_evaluate_pointer_comparisons + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#include +#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{}}; + const null_pointer_exprt null_ptr{ptr_type}; + + // 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()); + } + } + + 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 succeeds") + { + REQUIRE(result.get() == true_exprt{}); + } + } + } + + 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` + 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{}); + } + } + } +}