48 typedef std::unordered_map<
51 typedef std::unordered_map<exprt, exprt, irep_hash>
containert;
67 if(expr.
op().is_constant())
101 if(expr.
op().is_constant())
103 const typet &type = expr.
op().type();
114 if(value.has_value())
137 std::size_t result = 0;
139 for(std::size_t i = 0; i < width; i++)
288 const bool includes =
311 if(!s.
length().is_constant())
451 auto it = std::find_end(
458 std::distance(
s1_data.operands().begin(), it), expr.
type());
462 auto it = std::search(
468 if(it !=
s1_data.operands().end())
470 std::distance(
s1_data.operands().begin(), it), expr.
type());
473 else if(expr.
arguments().at(1).is_constant())
488 auto it = std::find_if(
492 if(it !=
s1_data.operands().rend())
494 std::distance(
s1_data.operands().begin(), it.base() - 1),
499 auto it = std::find_if(
503 if(it !=
s1_data.operands().end())
505 std::distance(
s1_data.operands().begin(), it), expr.
type());
525 if(!expr.
arguments().at(1).is_constant())
552 if(
c.type() != expr.
type())
668 if(!offset.is_constant())
679 exprt::operandst::const_iterator
second_it =
768 return std::move(
tmp);
797 if(expr.
type() == expr.
op().type())
842 return typecast.op();
867 return std::move(
tmp);
902 expr.
op().operands().size() == 2)
991 if(step.has_value() && *step != 0)
998 for(
auto &op :
new_expr.op().operands())
1001 if(op.type().id() !=
ID_pointer && *step > 1)
1054 return std::move(
tmp);
1092 return std::move(
tmp);
1145 return std::move(result);
1155 return std::move(
tmp);
1263 return std::move(result);
1285 const typet &base_type =
1362 if(
r_it.has_changed())
1462 std::size_t number =
1465 if(number >=
with_expr.old().operands().size())
1525 for(
const auto &e : designator)
1663 if(expr.
op().
id()==expr.
id())
1709 if(!offset.has_value() || *offset < 0)
1732 tmp.op() =
bu->op();
1744 tmp.op() =
bu->op();
1754 tmp.op() =
bu->value();
1826 std::string
el_bits = std::string(
1835 return std::move(*
tmp);
1863 [&](
const typet &type) {
1864 if(type.id() != ID_struct && type.id() != ID_struct_tag)
1867 const struct_typet &st = to_struct_type(ns.follow(type));
1868 const auto &comps = st.components();
1869 if(comps.empty() || comps.back().type().id() != ID_array)
1872 if(comps.back().type().get_bool(ID_C_flexible_array_member))
1876 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1877 return !size.has_value() || *size <= 1;
1882 std::string
bits_cut = std::string(
1891 return std::move(*
tmp);
1908 for(
const auto &
comp : components)
1973 slice.operands().erase(
1974 slice.operands().begin(),
1975 slice.operands().begin() +
1977 slice.type().size() =
1992 slice.type().size() =
2020 expr.
id() == expr.
op().id() &&
2026 return std::move(
tmp);
2029 const exprt &root = expr.
op();
2083 return std::move(*
tmp);
2107 if(!(root==extract.
op()))
2109 if(!(offset==extract.
offset()))
2135 tmp.set_value(std::move(new_value));
2160 tmp.set_value(std::move(new_value));
2330 return std::move(result);
2402 if(!op0_value.has_value() || !op1_value.has_value())
2433 if(expr.
op().is_zero())
2452 if(!expr.
op().is_constant())
2649 const std::size_t width =
2674 for(
const auto &op : expr.
operands())
2687 if(!op0_value.has_value() || !op1_value.has_value())
2745 if(
r_it.has_changed())
3035 std::cout <<
"===== " << node.
id() <<
": " <<
format(node) <<
'\n'
3036 <<
" ---> " <<
format(
r.expr) <<
'\n';
3048 std::pair<simplify_expr_cachet::containert::iterator, bool>
3050 insert(std::pair<exprt, exprt>(expr,
exprt()));
3076#ifdef USE_LOCAL_REPLACE_MAP
3111 return std::move(
tmp);
3118#ifdef DEBUG_ON_DEMAND
3120 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
3123#ifdef DEBUG_ON_DEMAND
3125 std::cout <<
"FULLSIMP " <<
format(result.expr) <<
"\n";
3127 if(result.has_changed())
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
Rewrite a byte extract expression to more fundamental operations.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Array constructor from list of elements.
A base class for binary expressions.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for relations, i.e., binary predicates whose two operands have the same type.
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & offset() const
std::size_t get_bits_per_byte() const
const exprt & value() const
C enum tag type, i.e., c_enum_typet with an identifier.
Determine whether an expression is constant.
struct configt::ansi_ct ansi_c
A constant literal expression.
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
bool zero_permitted() const
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
bool zero_permitted() const
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Union constructor to support unions without any member (a GCC/Clang feature).
Base class for all expressions.
std::vector< exprt > operandst
bool is_one() const
Return whether the expression is a constant representing 1.
bool has_operands() const
Return true if there is at least one operand.
bool is_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The Boolean constant false.
Returns one plus the index of the least-significant one bit, or zero if the operand is zero.
Fixed-width bit-vector with signed fixed-point interpretation.
void from_integer(const mp_integer &i)
mp_integer to_integer() const
void round(const fixedbv_spect &dest_spec)
constant_exprt to_expr() const
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
mp_integer to_integer() const
constant_exprt to_expr() const
void set_sign(bool _sign)
void from_integer(const mp_integer &i)
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
Fixed-width bit-vector representing a signed or unsigned integer.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & id() const
A (mathematical) lambda expression.
Extract member of struct or union.
Binary multiplication Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
The plus expression Associativity is not specified.
The offset (in bytes) of a pointer relative to the object.
The popcount (counting the number of bits set to 1) expression.
const exprt & length() const
const exprt & content() const
Sign of an expression Predicate is true if _op is negative, false otherwise.
Fixed-width bit-vector with two's complement interpretation.
resultt simplify_isnan(const unary_exprt &)
resultt simplify_bitwise(const multi_ary_exprt &)
resultt simplify_power(const binary_exprt &)
resultt simplify_div(const div_exprt &)
resultt simplify_byte_extract(const byte_extract_exprt &)
resultt simplify_bitreverse(const bitreverse_exprt &)
Try to simplify bit-reversing to a constant expression.
resultt simplify_abs(const abs_exprt &)
resultt simplify_isnormal(const unary_exprt &)
resultt simplify_dereference(const dereference_exprt &)
resultt simplify_bitnot(const bitnot_exprt &)
resultt simplify_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &)
Try to simplify prophecy_{r,w,rw}_ok to a constant expression.
resultt simplify_popcount(const popcount_exprt &)
static resultt changed(resultt<> result)
bool simplify_if_preorder(if_exprt &expr)
resultt simplify_address_of(const address_of_exprt &)
resultt simplify_if(const if_exprt &)
resultt simplify_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &)
Try to simplify prophecy_pointer_in_range to a constant expression.
resultt simplify_overflow_unary(const unary_overflow_exprt &)
Try to simplify overflow-unary-.
resultt simplify_minus(const minus_exprt &)
resultt simplify_extractbit(const extractbit_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_shifts(const shift_exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_pointer_object(const pointer_object_exprt &)
resultt simplify_boolean(const exprt &)
resultt simplify_object(const exprt &)
resultt simplify_mult(const mult_exprt &)
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
resultt simplify_with(const with_exprt &)
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_not(const not_exprt &)
resultt simplify_isinf(const unary_exprt &)
resultt simplify_overflow_binary(const binary_overflow_exprt &)
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
resultt simplify_function_application(const function_application_exprt &)
Attempt to simplify mathematical function applications if we have enough information to do so.
resultt simplify_index(const index_exprt &)
resultt simplify_bswap(const bswap_exprt &)
resultt simplify_member(const member_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_byte_update(const byte_update_exprt &)
bool simplify_node_preorder(exprt &expr)
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
resultt simplify_update(const update_exprt &)
resultt simplify_is_invalid_pointer(const unary_exprt &)
resultt simplify_mod(const mod_exprt &)
resultt simplify_complex(const unary_exprt &)
resultt simplify_pointer_offset(const pointer_offset_exprt &)
resultt simplify_plus(const plus_exprt &)
virtual bool simplify(exprt &expr)
resultt simplify_unary_plus(const unary_plus_exprt &)
resultt simplify_overflow_result(const overflow_result_exprt &)
Try to simplify overflow_result-+, overflow_result-*, overflow_result–, overflow_result-shl,...
resultt simplify_ffs(const find_first_set_exprt &)
Try to simplify find-first-set to a constant expression.
resultt simplify_is_dynamic_object(const unary_exprt &)
resultt simplify_node(exprt)
bool simplify_typecast_preorder(typecast_exprt &)
resultt simplify_object_size(const object_size_exprt &)
resultt simplify_lambda(const lambda_exprt &)
resultt simplify_concatenation(const concatenation_exprt &)
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
resultt simplify_ctz(const count_trailing_zeros_exprt &)
Try to simplify count-trailing-zeros to a constant expression.
resultt simplify_clz(const count_leading_zeros_exprt &)
Try to simplify count-leading-zeros to a constant expression.
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
resultt simplify_sign(const sign_exprt &)
resultt simplify_unary_minus(const unary_minus_exprt &)
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
std::vector< componentt > componentst
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Generic base class for unary expressions.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Union constructor from single element.
Fixed-width bit-vector with unsigned binary interpretation.
Operator to update elements in structs and arrays.
exprt::operandst & designator()
Operator to update elements in structs and arrays.
#define Forall_operands(it, expr)
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
exprt pointer_offset_sum(const exprt &a, const exprt &b)
exprt object_size(const exprt &pointer)
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
bool simplify(exprt &expr, const namespacet &ns)
static simplify_exprt::resultt simplify_string_compare_to(const function_application_exprt &expr, const namespacet &ns)
Simplify String.compareTo function when arguments are constant.
static simplify_exprt::resultt simplify_string_contains(const function_application_exprt &expr, const namespacet &ns)
Simplify String.contains function when arguments are constant.
static simplify_exprt::resultt simplify_string_endswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.endsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_char_at(const function_application_exprt &expr, const namespacet &ns)
Simplify String.charAt function when arguments are constant.
static simplify_exprt::resultt simplify_string_startswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.startsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_is_empty(const function_application_exprt &expr, const namespacet &ns)
Simplify String.isEmpty function when arguments are constant.
static bool lower_case_string_expression(array_exprt &string_data)
Take the passed-in constant string array and lower-case every character.
static simplify_exprt::resultt simplify_string_index_of(const function_application_exprt &expr, const namespacet &ns, const bool search_from_end)
Simplify String.indexOf function when arguments are constant.
static simplify_exprt::resultt simplify_string_equals_ignore_case(const function_application_exprt &expr, const namespacet &ns)
Simplify String.equalsIgnorecase function when arguments are constant.
exprt simplify_expr(exprt src, const namespacet &ns)
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
optionalt< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
bool join_operands(exprt &expr)
optionalt< std::reference_wrapper< const array_exprt > > try_get_string_data_array(const exprt &content, const namespacet &ns)
Get char sequence from content field of a refined string expression.
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define POSTCONDITION_WITH_DIAGNOSTICS(CONDITION,...)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
String expressions for the string solver.
refined_string_exprt & to_string_expr(exprt &expr)
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)