cprover
simplify_expr_class.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
29 class abs_exprt;
30 class address_of_exprt;
31 class array_exprt;
32 class binary_exprt;
35 class bitnot_exprt;
36 class bswap_exprt;
37 class byte_extract_exprt;
38 class byte_update_exprt;
42 class dereference_exprt;
43 class div_exprt;
44 class exprt;
45 class extractbit_exprt;
46 class extractbits_exprt;
50 class if_exprt;
51 class index_exprt;
52 class lambda_exprt;
53 class member_exprt;
54 class minus_exprt;
55 class mod_exprt;
56 class multi_ary_exprt;
57 class mult_exprt;
58 class namespacet;
59 class not_exprt;
60 class plus_exprt;
61 class popcount_exprt;
63 class shift_exprt;
64 class sign_exprt;
65 class typecast_exprt;
66 class unary_exprt;
67 class unary_minus_exprt;
69 class unary_plus_exprt;
70 class update_exprt;
71 class with_exprt;
72 
74 {
75 public:
76  explicit simplify_exprt(const namespacet &_ns):
77  do_simplify_if(true),
78  ns(_ns)
79 #ifdef DEBUG_ON_DEMAND
80  , debug_on(false)
81 #endif
82  {
83 #ifdef DEBUG_ON_DEMAND
84  struct stat f;
85  debug_on=stat("SIMP_DEBUG", &f)==0;
86 #endif
87  }
88 
89  virtual ~simplify_exprt()
90  {
91  }
92 
94 
95  template <typename T = exprt>
96  struct resultt
97  {
98  bool has_changed() const
99  {
100  return expr_changed == CHANGED;
101  }
102 
104  {
106  UNCHANGED
108 
109  T expr;
110 
112  operator T() const
113  {
114  return expr;
115  }
116 
119  // NOLINTNEXTLINE(runtime/explicit)
120  resultt(T _expr) : expr_changed(CHANGED), expr(std::move(_expr))
121  {
122  }
123 
124  resultt(expr_changedt _expr_changed, T _expr)
125  : expr_changed(_expr_changed), expr(std::move(_expr))
126  {
127  }
128  };
129 
131  {
132  return resultt<>(resultt<>::UNCHANGED, std::move(expr));
133  }
134 
136  {
138  return result;
139  }
140 
141  // These below all return 'true' if the simplification wasn't applicable.
142  // If false is returned, the expression has changed.
157  bool simplify_if_preorder(if_exprt &expr);
191 
196 
201 
206 
209 
212 
213  // auxiliary
214  bool simplify_if_implies(
215  exprt &expr, const exprt &cond, bool truth, bool &new_truth);
216  bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth);
217  bool simplify_if_conj(exprt &expr, const exprt &cond);
218  bool simplify_if_disj(exprt &expr, const exprt &cond);
219  bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond);
220  bool simplify_if_cond(exprt &expr);
232 
233  // main recursion
235  bool simplify_node_preorder(exprt &expr);
237 
238  virtual bool simplify(exprt &expr);
239 
240  static bool is_bitvector_type(const typet &type)
241  {
242  return type.id()==ID_unsignedbv ||
243  type.id()==ID_signedbv ||
244  type.id()==ID_bv;
245  }
246 
247 protected:
248  const namespacet &ns;
249 #ifdef DEBUG_ON_DEMAND
250  bool debug_on;
251 #endif
252 #ifdef USE_LOCAL_REPLACE_MAP
253  replace_mapt local_replace_map;
254 #endif
255 
256 };
257 
258 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
simplify_exprt::~simplify_exprt
virtual ~simplify_exprt()
Definition: simplify_expr_class.h:89
simplify_exprt::simplify_rec
resultt simplify_rec(const exprt &)
Definition: simplify_expr.cpp:2564
simplify_exprt::simplify_if_recursive
bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth)
Definition: simplify_expr_if.cpp:74
simplify_exprt::simplify_is_invalid_pointer
resultt simplify_is_invalid_pointer(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:611
simplify_exprt::simplify_isnormal
resultt simplify_isnormal(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:51
simplify_exprt::simplify_if_disj
bool simplify_if_disj(exprt &expr, const exprt &cond)
Definition: simplify_expr_if.cpp:125
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
simplify_exprt::simplify_shifts
resultt simplify_shifts(const shift_exprt &)
Definition: simplify_expr_int.cpp:907
simplify_exprt::simplify_dereference
resultt simplify_dereference(const dereference_exprt &)
Definition: simplify_expr.cpp:1328
simplify_exprt::simplify_concatenation
resultt simplify_concatenation(const concatenation_exprt &)
Definition: simplify_expr_int.cpp:805
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:78
NODISCARD
#define NODISCARD
Definition: nodiscard.h:22
count_trailing_zeros_exprt
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Definition: bitvector_expr.h:924
mp_arith.h
simplify_exprt::simplify_address_of
resultt simplify_address_of(const address_of_exprt &)
Definition: simplify_expr_pointer.cpp:210
resultt
resultt
The result of goto verifying.
Definition: properties.h:45
simplify_exprt::simplify_unary_plus
resultt simplify_unary_plus(const unary_plus_exprt &)
Definition: simplify_expr_int.cpp:1112
simplify_exprt::simplify_bitwise
resultt simplify_bitwise(const multi_ary_exprt &)
Definition: simplify_expr_int.cpp:600
simplify_exprt::simplify_if_preorder
bool simplify_if_preorder(if_exprt &expr)
Definition: simplify_expr_if.cpp:214
simplify_exprt::simplify_bitnot
resultt simplify_bitnot(const bitnot_exprt &)
Definition: simplify_expr_int.cpp:1179
typet
The type of an expression, extends irept.
Definition: type.h:28
simplify_exprt::simplify_overflow_binary
resultt simplify_overflow_binary(const binary_overflow_exprt &)
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
Definition: simplify_expr.cpp:2173
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:628
simplify_exprt::simplify_exprt
simplify_exprt(const namespacet &_ns)
Definition: simplify_expr_class.h:76
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2172
simplify_exprt::simplify_popcount
resultt simplify_popcount(const popcount_exprt &)
Definition: simplify_expr.cpp:125
simplify_exprt::simplify_inequality_address_of
resultt simplify_inequality_address_of(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:410
simplify_exprt::simplify
virtual bool simplify(exprt &expr)
Definition: simplify_expr.cpp:2633
simplify_exprt::simplify_is_dynamic_object
resultt simplify_is_dynamic_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:552
simplify_exprt::simplify_if_conj
bool simplify_if_conj(exprt &expr, const exprt &cond)
Definition: simplify_expr_if.cpp:106
simplify_exprt::simplify_clz
resultt simplify_clz(const count_leading_zeros_exprt &)
Try to simplify count-leading-zeros to a constant expression.
Definition: simplify_expr.cpp:151
nodiscard.h
simplify_exprt::simplify_update
resultt simplify_update(const update_exprt &)
Definition: simplify_expr.cpp:1471
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:914
simplify_exprt::simplify_boolean
resultt simplify_boolean(const exprt &)
Definition: simplify_expr_boolean.cpp:17
simplify_exprt::simplify_overflow_unary
resultt simplify_overflow_unary(const unary_overflow_exprt &)
Try to simplify overflow-unary-.
Definition: simplify_expr.cpp:2236
exprt
Base class for all expressions.
Definition: expr.h:54
simplify_exprt::simplify_if_cond
bool simplify_if_cond(exprt &expr)
Definition: simplify_expr_if.cpp:176
simplify_exprt::simplify_ctz
resultt simplify_ctz(const count_trailing_zeros_exprt &)
Try to simplify count-trailing-zeros to a constant expression.
Definition: simplify_expr.cpp:177
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
simplify_exprt::simplify_extractbit
resultt simplify_extractbit(const extractbit_exprt &)
Definition: simplify_expr_int.cpp:776
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:550
sign_exprt
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:506
concatenation_exprt
Concatenation of bit-vector operands.
Definition: bitvector_expr.h:590
simplify_exprt::simplify_complex
resultt simplify_complex(const unary_exprt &)
Definition: simplify_expr.cpp:2152
simplify_exprt::simplify_pointer_offset
resultt simplify_pointer_offset(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:248
simplify_exprt::resultt::has_changed
bool has_changed() const
Definition: simplify_expr_class.h:98
div_exprt
Division.
Definition: std_expr.h:1064
simplify_exprt::simplify_plus
resultt simplify_plus(const plus_exprt &)
Definition: simplify_expr_int.cpp:402
simplify_exprt::simplify_byte_extract
resultt simplify_byte_extract(const byte_extract_exprt &)
Definition: simplify_expr.cpp:1599
simplify_exprt::simplify_not
resultt simplify_not(const not_exprt &)
Definition: simplify_expr_boolean.cpp:162
simplify_exprt::simplify_inequality_both_constant
resultt simplify_inequality_both_constant(const binary_relation_exprt &)
simplifies inequalities for the case in which both sides of the inequality are constants
Definition: simplify_expr_int.cpp:1306
simplify_exprt::unchanged
static resultt unchanged(exprt expr)
Definition: simplify_expr_class.h:130
simplify_exprt::simplify_node
resultt simplify_node(exprt)
Definition: simplify_expr.cpp:2314
refined_string_exprt
Definition: string_expr.h:109
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
simplify_exprt::resultt::CHANGED
@ CHANGED
Definition: simplify_expr_class.h:105
expr.h
simplify_exprt::simplify_if
resultt simplify_if(const if_exprt &)
Definition: simplify_expr_if.cpp:330
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
simplify_exprt::resultt::UNCHANGED
@ UNCHANGED
Definition: simplify_expr_class.h:106
simplify_exprt::simplify_minus
resultt simplify_minus(const minus_exprt &)
Definition: simplify_expr_int.cpp:558
simplify_exprt::resultt::expr_changedt
expr_changedt
Definition: simplify_expr_class.h:104
simplify_exprt::simplify_power
resultt simplify_power(const binary_exprt &)
Definition: simplify_expr_int.cpp:1015
simplify_exprt::simplify_div
resultt simplify_div(const div_exprt &)
Definition: simplify_expr_int.cpp:271
simplify_exprt::simplify_inequality_no_constant
resultt simplify_inequality_no_constant(const binary_relation_exprt &)
Definition: simplify_expr_int.cpp:1467
simplify_exprt::simplify_typecast
resultt simplify_typecast(const typecast_exprt &)
Definition: simplify_expr.cpp:732
simplify_exprt::simplify_mod
resultt simplify_mod(const mod_exprt &)
Definition: simplify_expr_int.cpp:365
floatbv_typecast_exprt
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
simplify_exprt::simplify_isnan
resultt simplify_isnan(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:37
binary_overflow_exprt
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
Definition: bitvector_expr.h:687
simplify_exprt::changed
static resultt changed(resultt<> result)
Definition: simplify_expr_class.h:135
simplify_exprt::is_bitvector_type
static bool is_bitvector_type(const typet &type)
Definition: simplify_expr_class.h:240
simplify_exprt::simplify_inequality_rhs_is_constant
resultt simplify_inequality_rhs_is_constant(const binary_relation_exprt &)
Definition: simplify_expr_int.cpp:1539
simplify_exprt::simplify_bswap
resultt simplify_bswap(const bswap_exprt &)
Definition: simplify_expr_int.cpp:29
simplify_exprt::simplify_node_preorder
bool simplify_node_preorder(exprt &expr)
Definition: simplify_expr.cpp:2283
simplify_exprt::resultt::expr_changed
enum simplify_exprt::resultt::expr_changedt expr_changed
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:192
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
simplify_exprt::simplify_inequality
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition: simplify_expr_int.cpp:1210
simplify_exprt
Definition: simplify_expr_class.h:74
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:390
simplify_exprt::simplify_good_pointer
resultt simplify_good_pointer(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:692
irept::id
const irep_idt & id() const
Definition: irep.h:407
abs_exprt
Absolute value.
Definition: std_expr.h:346
unary_plus_exprt
The unary plus expression.
Definition: std_expr.h:439
simplify_exprt::simplify_mult
resultt simplify_mult(const mult_exprt &)
Definition: simplify_expr_int.cpp:159
simplify_exprt::simplify_with
resultt simplify_with(const with_exprt &)
Definition: simplify_expr.cpp:1391
simplify_exprt::resultt
Definition: simplify_expr_class.h:97
simplify_exprt::resultt::resultt
resultt(expr_changedt _expr_changed, T _expr)
Definition: simplify_expr_class.h:124
simplify_exprt::simplify_unary_minus
resultt simplify_unary_minus(const unary_minus_exprt &)
Definition: simplify_expr_int.cpp:1119
simplify_exprt::simplify_function_application
resultt simplify_function_application(const function_application_exprt &)
Attempt to simplify mathematical function applications if we have enough information to do so.
Definition: simplify_expr.cpp:675
simplify_exprt::simplify_pointer_object
resultt simplify_pointer_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:520
minus_exprt
Binary minus.
Definition: std_expr.h:973
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2442
simplify_exprt::simplify_if_branch
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
Definition: simplify_expr_if.cpp:144
simplify_exprt::simplify_index
resultt simplify_index(const index_exprt &)
Definition: simplify_expr_array.cpp:19
simplify_exprt::resultt::resultt
resultt(T _expr)
conversion from expression, thus not 'explicit' marks the expression as "CHANGED"
Definition: simplify_expr_class.h:120
bitnot_exprt
Bit-wise negation of bit-vectors.
Definition: bitvector_expr.h:82
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: bitvector_expr.h:363
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2613
simplify_exprt::simplify_member
resultt simplify_member(const member_exprt &)
Definition: simplify_expr_struct.cpp:21
unary_overflow_exprt
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Definition: bitvector_expr.h:766
shift_exprt
A base class for shift and rotate operators.
Definition: bitvector_expr.h:230
simplify_exprt::simplify_object
resultt simplify_object(const exprt &)
Definition: simplify_expr.cpp:1519
simplify_exprt::simplify_inequality_pointer_object
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:475
simplify_exprt::resultt::expr
T expr
Definition: simplify_expr_class.h:109
lambda_exprt
A (mathematical) lambda expression.
Definition: mathematical_expr.h:407
simplify_exprt::simplify_sign
resultt simplify_sign(const sign_exprt &)
Definition: simplify_expr.cpp:99
replace_mapt
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Definition: replace_expr.h:22
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
simplify_exprt::simplify_lambda
resultt simplify_lambda(const lambda_exprt &)
Definition: simplify_expr.cpp:1386
simplify_exprt::simplify_if_implies
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
Definition: simplify_expr_if.cpp:15
simplify_exprt::simplify_extractbits
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
Definition: simplify_expr_int.cpp:1036
ieee_float_op_exprt
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:248
bswap_exprt
The byte swap expression.
Definition: bitvector_expr.h:19
simplify_exprt::do_simplify_if
bool do_simplify_if
Definition: simplify_expr_class.h:93
simplify_exprt::simplify_address_of_arg
resultt simplify_address_of_arg(const exprt &)
Definition: simplify_expr_pointer.cpp:57
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: bitvector_expr.h:430
replace_expr.h
simplify_exprt::simplify_byte_update
resultt simplify_byte_update(const byte_update_exprt &)
Definition: simplify_expr.cpp:1844
index_exprt
Array index operator.
Definition: std_expr.h:1328
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: bitvector_expr.h:633
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
simplify_exprt::simplify_object_size
resultt simplify_object_size(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:644
simplify_exprt::simplify_abs
resultt simplify_abs(const abs_exprt &)
Definition: simplify_expr.cpp:65
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1467
simplify_exprt::simplify_ieee_float_relation
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
Definition: simplify_expr_floatbv.cpp:338
simplify_exprt::simplify_floatbv_typecast
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
Definition: simplify_expr_floatbv.cpp:139
mod_exprt
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
count_leading_zeros_exprt
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
Definition: bitvector_expr.h:831
simplify_exprt::simplify_floatbv_op
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
Definition: simplify_expr_floatbv.cpp:273
not_exprt
Boolean negation.
Definition: std_expr.h:2127
simplify_exprt::simplify_isinf
resultt simplify_isinf(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:23