cprover
Loading...
Searching...
No Matches
simplify_expr_class.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
11#define CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
12
13// #define DEBUG_ON_DEMAND
14#ifdef DEBUG_ON_DEMAND
15#include <sys/stat.h>
16#endif
17
18#include <set>
19
20#include "expr.h"
21#include "mp_arith.h"
22#include "nodiscard.h"
23#include "type.h"
24// #define USE_LOCAL_REPLACE_MAP
25#ifdef USE_LOCAL_REPLACE_MAP
26#include "replace_expr.h"
27#endif
28
29class abs_exprt;
31class array_exprt;
32class binary_exprt;
35class bitnot_exprt;
37class bswap_exprt;
44class div_exprt;
45class exprt;
52class if_exprt;
53class index_exprt;
54class lambda_exprt;
55class member_exprt;
56class minus_exprt;
57class mod_exprt;
58class multi_ary_exprt;
59class mult_exprt;
60class namespacet;
61class not_exprt;
64class plus_exprt;
67class popcount_exprt;
71class shift_exprt;
72class sign_exprt;
73class typecast_exprt;
74class unary_exprt;
78class update_exprt;
79class with_exprt;
80
82{
83public:
84 explicit simplify_exprt(const namespacet &_ns):
85 do_simplify_if(true),
86 ns(_ns)
87#ifdef DEBUG_ON_DEMAND
88 , debug_on(false)
89#endif
90 {
91#ifdef DEBUG_ON_DEMAND
92 struct stat f;
93 debug_on=stat("SIMP_DEBUG", &f)==0;
94#endif
95 }
96
98 {
99 }
100
102
103 template <typename T = exprt>
104 struct resultt
105 {
106 bool has_changed() const
107 {
108 return expr_changed == CHANGED;
109 }
110
116
118
120 operator T() const
121 {
122 return expr;
123 }
124
127 // NOLINTNEXTLINE(runtime/explicit)
128 resultt(T _expr) : expr_changed(CHANGED), expr(std::move(_expr))
129 {
130 }
131
132 resultt(expr_changedt _expr_changed, T _expr)
133 : expr_changed(_expr_changed), expr(std::move(_expr))
134 {
135 }
136 };
137
139 {
140 return resultt<>(resultt<>::UNCHANGED, std::move(expr));
141 }
142
144 {
146 return result;
147 }
148
149 // These below all return 'true' if the simplification wasn't applicable.
150 // If false is returned, the expression has changed.
166 bool simplify_if_preorder(if_exprt &expr);
199
204
209
215
220
223
226
229
232
236
240
241 // auxiliary
243 exprt &expr, const exprt &cond, bool truth, bool &new_truth);
244 bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth);
245 bool simplify_if_conj(exprt &expr, const exprt &cond);
246 bool simplify_if_disj(exprt &expr, const exprt &cond);
247 bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond);
248 bool simplify_if_cond(exprt &expr);
260
261 // main recursion
263 bool simplify_node_preorder(exprt &expr);
265
266 virtual bool simplify(exprt &expr);
267
268 static bool is_bitvector_type(const typet &type)
269 {
270 return type.id()==ID_unsignedbv ||
271 type.id()==ID_signedbv ||
272 type.id()==ID_bv;
273 }
274
275protected:
277#ifdef DEBUG_ON_DEMAND
278 bool debug_on;
279#endif
280#ifdef USE_LOCAL_REPLACE_MAP
281 replace_mapt local_replace_map;
282#endif
283
284};
285
286#endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
Absolute value.
Definition std_expr.h:379
Operator to return the address of an object.
Array constructor from list of elements.
Definition std_expr.h:1563
A base class for binary expressions.
Definition std_expr.h:583
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.
Definition std_expr.h:707
Bit-wise negation of bit-vectors.
Reverse the order of bits in a bit-vector.
The byte swap expression.
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Concatenation of bit-vector operands.
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Operator to dereference a pointer.
Division.
Definition std_expr.h:1097
Base class for all expressions.
Definition expr.h:56
Extracts a single bit of a bit-vector operand.
Extracts a sub-range of a bit-vector operand.
Returns one plus the index of the least-significant one bit, or zero if the operand is zero.
Semantic type conversion from/to floating-point formats.
Application of (mathematical) function.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
The trinary if-then-else operator.
Definition std_expr.h:2323
Array index operator.
Definition std_expr.h:1410
const irep_idt & id() const
Definition irep.h:396
A (mathematical) lambda expression.
Extract member of struct or union.
Definition std_expr.h:2794
Binary minus.
Definition std_expr.h:1006
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1168
Binary multiplication Associativity is not specified.
Definition std_expr.h:1052
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:857
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Boolean negation.
Definition std_expr.h:2278
Expression for finding the size (in bytes) of the object a pointer points to.
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
The plus expression Associativity is not specified.
Definition std_expr.h:947
A numerical identifier for the object a pointer points to.
The offset (in bytes) of a pointer relative to the object.
The popcount (counting the number of bits set to 1) expression.
pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer r...
A base class for a predicate that indicates that an address range is ok to read or write or both.
A base class for shift and rotate operators.
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:539
static bool is_bitvector_type(const typet &type)
resultt simplify_isnan(const unary_exprt &)
resultt simplify_bitwise(const multi_ary_exprt &)
resultt simplify_power(const binary_exprt &)
const namespacet & ns
resultt simplify_inequality_address_of(const binary_relation_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 &)
bool simplify_if_conj(exprt &expr, const exprt &cond)
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.
bool simplify_if_disj(exprt &expr, const exprt &cond)
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-.
bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth)
resultt simplify_minus(const minus_exprt &)
resultt simplify_extractbit(const extractbit_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_shifts(const shift_exprt &)
bool simplify_if_cond(exprt &expr)
resultt simplify_typecast(const typecast_exprt &)
simplify_exprt(const namespacet &_ns)
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 &)
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
resultt simplify_inequality_rhs_is_constant(const binary_relation_exprt &)
resultt simplify_address_of_arg(const 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 &)
resultt simplify_inequality_pointer_object(const binary_relation_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_inequality_no_constant(const binary_relation_exprt &)
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_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
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_inequality_both_constant(const binary_relation_exprt &)
simplifies inequalities for the case in which both sides of the inequality are constants
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 &)
Semantic type conversion.
Definition std_expr.h:2017
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:314
The unary minus expression.
Definition std_expr.h:423
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
The unary plus expression.
Definition std_expr.h:472
Operator to update elements in structs and arrays.
Definition std_expr.h:2608
Operator to update elements in structs and arrays.
Definition std_expr.h:2424
STL namespace.
#define NODISCARD
Definition nodiscard.h:22
resultt
The result of goto verifying.
Definition properties.h:45
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
resultt(expr_changedt _expr_changed, T _expr)
resultt(T _expr)
conversion from expression, thus not 'explicit' marks the expression as "CHANGED"
enum simplify_exprt::resultt::expr_changedt expr_changed
Defines typet, type_with_subtypet and type_with_subtypest.