|
| 1 | +/*******************************************************************\ |
| 2 | +
|
| 3 | +Module: Variant of simplify_exprt that uses a value_sett |
| 4 | +
|
| 5 | +Author: Michael Tautschnig |
| 6 | +
|
| 7 | +\*******************************************************************/ |
| 8 | + |
| 9 | +#include "simplify_expr_with_value_set.h" |
| 10 | + |
| 11 | +#include <util/expr_util.h> |
| 12 | +#include <util/pointer_expr.h> |
| 13 | +#include <util/simplify_expr.h> |
| 14 | +#include <util/ssa_expr.h> |
| 15 | + |
| 16 | +#include <pointer-analysis/add_failed_symbols.h> |
| 17 | +#include <pointer-analysis/value_set.h> |
| 18 | +#include <pointer-analysis/value_set_dereference.h> |
| 19 | + |
| 20 | +#include "goto_symex_can_forward_propagate.h" |
| 21 | + |
| 22 | +/// Try to evaluate a simple pointer comparison. |
| 23 | +/// \param operation: ID_equal or ID_not_equal |
| 24 | +/// \param symbol_expr: The symbol expression in the condition |
| 25 | +/// \param other_operand: The other expression in the condition; we only support |
| 26 | +/// an address of expression, a typecast of an address of expression or a |
| 27 | +/// null pointer, and return an empty std::optional in all other cases |
| 28 | +/// \param value_set: The value-set for looking up what the symbol can point to |
| 29 | +/// \param language_mode: The language mode |
| 30 | +/// \param ns: A namespace |
| 31 | +/// \return If we were able to evaluate the condition as true or false then we |
| 32 | +/// return that, otherwise we return an empty std::optional |
| 33 | +static std::optional<exprt> try_evaluate_pointer_comparison( |
| 34 | + const irep_idt &operation, |
| 35 | + const symbol_exprt &symbol_expr, |
| 36 | + const exprt &other_operand, |
| 37 | + const value_sett &value_set, |
| 38 | + const irep_idt language_mode, |
| 39 | + const namespacet &ns) |
| 40 | +{ |
| 41 | + const constant_exprt *constant_expr = |
| 42 | + expr_try_dynamic_cast<constant_exprt>(other_operand); |
| 43 | + |
| 44 | + if( |
| 45 | + skip_typecast(other_operand).id() != ID_address_of && |
| 46 | + (!constant_expr || !constant_expr->is_null_pointer())) |
| 47 | + { |
| 48 | + return {}; |
| 49 | + } |
| 50 | + |
| 51 | + const ssa_exprt *ssa_symbol_expr = |
| 52 | + expr_try_dynamic_cast<ssa_exprt>(symbol_expr); |
| 53 | + |
| 54 | + ssa_exprt l1_expr{*ssa_symbol_expr}; |
| 55 | + l1_expr.remove_level_2(); |
| 56 | + const std::vector<exprt> value_set_elements = |
| 57 | + value_set.get_value_set(l1_expr, ns); |
| 58 | + |
| 59 | + bool constant_found = false; |
| 60 | + |
| 61 | + for(const auto &value_set_element : value_set_elements) |
| 62 | + { |
| 63 | + if( |
| 64 | + value_set_element.id() == ID_unknown || |
| 65 | + value_set_element.id() == ID_invalid || |
| 66 | + is_failed_symbol( |
| 67 | + to_object_descriptor_expr(value_set_element).root_object()) || |
| 68 | + to_object_descriptor_expr(value_set_element).offset().id() == ID_unknown) |
| 69 | + { |
| 70 | + // We can't conclude anything about the value-set |
| 71 | + return {}; |
| 72 | + } |
| 73 | + |
| 74 | + if(!constant_found) |
| 75 | + { |
| 76 | + if(value_set_dereferencet::should_ignore_value( |
| 77 | + value_set_element, false, language_mode)) |
| 78 | + { |
| 79 | + continue; |
| 80 | + } |
| 81 | + |
| 82 | + value_set_dereferencet::valuet value = |
| 83 | + value_set_dereferencet::build_reference_to( |
| 84 | + value_set_element, symbol_expr, ns); |
| 85 | + |
| 86 | + // use the simplifier to test equality as we need to skip over typecasts |
| 87 | + // and cannot rely on canonical representations, which would permit a |
| 88 | + // simple syntactic equality test |
| 89 | + exprt test_equal = simplify_expr( |
| 90 | + equal_exprt{ |
| 91 | + typecast_exprt::conditional_cast(value.pointer, other_operand.type()), |
| 92 | + other_operand}, |
| 93 | + ns); |
| 94 | + if(test_equal.is_true()) |
| 95 | + { |
| 96 | + constant_found = true; |
| 97 | + // We can't break because we have to make sure we find any instances of |
| 98 | + // ID_unknown or ID_invalid |
| 99 | + } |
| 100 | + else if(!test_equal.is_false()) |
| 101 | + { |
| 102 | + // We can't conclude anything about the value-set |
| 103 | + return {}; |
| 104 | + } |
| 105 | + } |
| 106 | + } |
| 107 | + |
| 108 | + if(!constant_found) |
| 109 | + { |
| 110 | + // The symbol cannot possibly have the value \p other_operand because it |
| 111 | + // isn't in the symbol's value-set |
| 112 | + return operation == ID_equal ? static_cast<exprt>(false_exprt{}) |
| 113 | + : static_cast<exprt>(true_exprt{}); |
| 114 | + } |
| 115 | + else if(value_set_elements.size() == 1) |
| 116 | + { |
| 117 | + // The symbol must have the value \p other_operand because it is the only |
| 118 | + // thing in the symbol's value-set |
| 119 | + return operation == ID_equal ? static_cast<exprt>(true_exprt{}) |
| 120 | + : static_cast<exprt>(false_exprt{}); |
| 121 | + } |
| 122 | + else |
| 123 | + { |
| 124 | + return {}; |
| 125 | + } |
| 126 | +} |
| 127 | + |
| 128 | +simplify_exprt::resultt<> simplify_expr_with_value_sett::simplify_inequality( |
| 129 | + const binary_relation_exprt &expr) |
| 130 | +{ |
| 131 | + if(expr.id() != ID_equal && expr.id() != ID_notequal) |
| 132 | + return simplify_exprt::simplify_inequality(expr); |
| 133 | + |
| 134 | + if(!can_cast_type<pointer_typet>( to_binary_expr(expr). op0(). type())) |
| 135 | + return simplify_exprt::simplify_inequality(expr); |
| 136 | + |
| 137 | + exprt lhs = to_binary_expr(expr).op0(), rhs = to_binary_expr(expr).op1(); |
| 138 | + if(can_cast_expr<symbol_exprt>(rhs)) |
| 139 | + std::swap(lhs, rhs); |
| 140 | + |
| 141 | + const symbol_exprt *symbol_expr_lhs = |
| 142 | + expr_try_dynamic_cast<symbol_exprt>(lhs); |
| 143 | + |
| 144 | + if(!symbol_expr_lhs) |
| 145 | + return simplify_exprt::simplify_inequality(expr); |
| 146 | + |
| 147 | + if(!goto_symex_can_forward_propagatet(ns)(rhs)) |
| 148 | + return simplify_exprt::simplify_inequality(expr); |
| 149 | + |
| 150 | + auto maybe_constant = try_evaluate_pointer_comparison( |
| 151 | + expr.id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns); |
| 152 | + if(maybe_constant.has_value()) |
| 153 | + return changed(*maybe_constant); |
| 154 | + else |
| 155 | + return unchanged(expr); |
| 156 | +} |
0 commit comments