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;
41 class dereference_exprt;
42 class div_exprt;
43 class exprt;
44 class extractbit_exprt;
45 class extractbits_exprt;
49 class if_exprt;
50 class index_exprt;
51 class lambda_exprt;
52 class member_exprt;
53 class minus_exprt;
54 class mod_exprt;
55 class multi_ary_exprt;
56 class mult_exprt;
57 class namespacet;
58 class not_exprt;
59 class plus_exprt;
60 class popcount_exprt;
62 class shift_exprt;
63 class sign_exprt;
64 class typecast_exprt;
65 class unary_exprt;
66 class unary_minus_exprt;
68 class unary_plus_exprt;
69 class update_exprt;
70 class with_exprt;
71 
73 {
74 public:
75  explicit simplify_exprt(const namespacet &_ns):
76  do_simplify_if(true),
77  ns(_ns)
78 #ifdef DEBUG_ON_DEMAND
79  , debug_on(false)
80 #endif
81  {
82 #ifdef DEBUG_ON_DEMAND
83  struct stat f;
84  debug_on=stat("SIMP_DEBUG", &f)==0;
85 #endif
86  }
87 
88  virtual ~simplify_exprt()
89  {
90  }
91 
93 
94  template <typename T = exprt>
95  struct resultt
96  {
97  bool has_changed() const
98  {
99  return expr_changed == CHANGED;
100  }
101 
103  {
105  UNCHANGED
107 
108  T expr;
109 
111  operator T() const
112  {
113  return expr;
114  }
115 
118  // NOLINTNEXTLINE(runtime/explicit)
119  resultt(T _expr) : expr_changed(CHANGED), expr(std::move(_expr))
120  {
121  }
122 
123  resultt(expr_changedt _expr_changed, T _expr)
124  : expr_changed(_expr_changed), expr(std::move(_expr))
125  {
126  }
127  };
128 
130  {
131  return resultt<>(resultt<>::UNCHANGED, std::move(expr));
132  }
133 
135  {
137  return result;
138  }
139 
140  // These below all return 'true' if the simplification wasn't applicable.
141  // If false is returned, the expression has changed.
156  bool simplify_if_preorder(if_exprt &expr);
190 
195 
200 
205 
208 
209  // auxiliary
210  bool simplify_if_implies(
211  exprt &expr, const exprt &cond, bool truth, bool &new_truth);
212  bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth);
213  bool simplify_if_conj(exprt &expr, const exprt &cond);
214  bool simplify_if_disj(exprt &expr, const exprt &cond);
215  bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond);
216  bool simplify_if_cond(exprt &expr);
228 
229  // main recursion
231  bool simplify_node_preorder(exprt &expr);
233 
234  virtual bool simplify(exprt &expr);
235 
236  static bool is_bitvector_type(const typet &type)
237  {
238  return type.id()==ID_unsignedbv ||
239  type.id()==ID_signedbv ||
240  type.id()==ID_bv;
241  }
242 
243 protected:
244  const namespacet &ns;
245 #ifdef DEBUG_ON_DEMAND
246  bool debug_on;
247 #endif
248 #ifdef USE_LOCAL_REPLACE_MAP
249  replace_mapt local_replace_map;
250 #endif
251 
252 };
253 
254 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2172
simplify_exprt::~simplify_exprt
virtual ~simplify_exprt()
Definition: simplify_expr_class.h:88
simplify_exprt::simplify_rec
resultt simplify_rec(const exprt &)
Definition: simplify_expr.cpp:2462
simplify_exprt::simplify_if_recursive
bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth)
Definition: simplify_expr_if.cpp:75
simplify_exprt::simplify_is_invalid_pointer
resultt simplify_is_invalid_pointer(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:621
simplify_exprt::simplify_isnormal
resultt simplify_isnormal(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:52
simplify_exprt::simplify_if_disj
bool simplify_if_disj(exprt &expr, const exprt &cond)
Definition: simplify_expr_if.cpp:126
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:740
simplify_exprt::simplify_shifts
resultt simplify_shifts(const shift_exprt &)
Definition: simplify_expr_int.cpp:909
simplify_exprt::simplify_dereference
resultt simplify_dereference(const dereference_exprt &)
Definition: simplify_expr.cpp:1302
simplify_exprt::simplify_concatenation
resultt simplify_concatenation(const concatenation_exprt &)
Definition: simplify_expr_int.cpp:807
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:81
NODISCARD
#define NODISCARD
Definition: nodiscard.h:22
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:44
simplify_exprt::simplify_unary_plus
resultt simplify_unary_plus(const unary_plus_exprt &)
Definition: simplify_expr_int.cpp:1114
simplify_exprt::simplify_bitwise
resultt simplify_bitwise(const multi_ary_exprt &)
Definition: simplify_expr_int.cpp:601
simplify_exprt::simplify_if_preorder
bool simplify_if_preorder(if_exprt &expr)
Definition: simplify_expr_if.cpp:215
simplify_exprt::simplify_bitnot
resultt simplify_bitnot(const bitnot_exprt &)
Definition: simplify_expr_int.cpp:1181
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:2075
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:386
simplify_exprt::simplify_exprt
simplify_exprt(const namespacet &_ns)
Definition: simplify_expr_class.h:75
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
simplify_exprt::simplify_popcount
resultt simplify_popcount(const popcount_exprt &)
Definition: simplify_expr.cpp:126
simplify_exprt::simplify_inequality_address_of
resultt simplify_inequality_address_of(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:420
simplify_exprt::simplify
virtual bool simplify(exprt &expr)
Definition: simplify_expr.cpp:2531
simplify_exprt::simplify_is_dynamic_object
resultt simplify_is_dynamic_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:562
simplify_exprt::simplify_if_conj
bool simplify_if_conj(exprt &expr, const exprt &cond)
Definition: simplify_expr_if.cpp:107
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:152
nodiscard.h
simplify_exprt::simplify_update
resultt simplify_update(const update_exprt &)
Definition: simplify_expr.cpp:1445
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
simplify_exprt::simplify_boolean
resultt simplify_boolean(const exprt &)
Definition: simplify_expr_boolean.cpp:20
simplify_exprt::simplify_overflow_unary
resultt simplify_overflow_unary(const unary_overflow_exprt &)
Try to simplify overflow-unary-.
Definition: simplify_expr.cpp:2138
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: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:778
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:2054
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:97
div_exprt
Division.
Definition: std_expr.h:980
simplify_exprt::simplify_plus
resultt simplify_plus(const plus_exprt &)
Definition: simplify_expr_int.cpp:403
simplify_exprt::simplify_byte_extract
resultt simplify_byte_extract(const byte_extract_exprt &)
Definition: simplify_expr.cpp:1573
simplify_exprt::simplify_not
resultt simplify_not(const not_exprt &)
Definition: simplify_expr_boolean.cpp:165
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:1307
simplify_exprt::unchanged
static resultt unchanged(exprt expr)
Definition: simplify_expr_class.h:129
simplify_exprt::simplify_node
resultt simplify_node(exprt)
Definition: simplify_expr.cpp:2216
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:104
expr.h
simplify_exprt::simplify_if
resultt simplify_if(const if_exprt &)
Definition: simplify_expr_if.cpp:331
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
simplify_exprt::resultt::UNCHANGED
@ UNCHANGED
Definition: simplify_expr_class.h:105
simplify_exprt::simplify_minus
resultt simplify_minus(const minus_exprt &)
Definition: simplify_expr_int.cpp:559
simplify_exprt::resultt::expr_changedt
expr_changedt
Definition: simplify_expr_class.h:103
simplify_exprt::simplify_power
resultt simplify_power(const binary_exprt &)
Definition: simplify_expr_int.cpp:1017
simplify_exprt::simplify_div
resultt simplify_div(const div_exprt &)
Definition: simplify_expr_int.cpp:272
simplify_exprt::simplify_inequality_no_constant
resultt simplify_inequality_no_constant(const binary_relation_exprt &)
Definition: simplify_expr_int.cpp:1468
simplify_exprt::simplify_typecast
resultt simplify_typecast(const typecast_exprt &)
Definition: simplify_expr.cpp:707
simplify_exprt::simplify_mod
resultt simplify_mod(const mod_exprt &)
Definition: simplify_expr_int.cpp:366
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:38
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:134
simplify_exprt::is_bitvector_type
static bool is_bitvector_type(const typet &type)
Definition: simplify_expr_class.h:236
simplify_exprt::simplify_inequality_rhs_is_constant
resultt simplify_inequality_rhs_is_constant(const binary_relation_exprt &)
Definition: simplify_expr_int.cpp:1540
simplify_exprt::simplify_bswap
resultt simplify_bswap(const bswap_exprt &)
Definition: simplify_expr_int.cpp:30
simplify_exprt::simplify_node_preorder
bool simplify_node_preorder(exprt &expr)
Definition: simplify_expr.cpp:2185
simplify_exprt::resultt::expr_changed
enum simplify_exprt::resultt::expr_changedt expr_changed
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:194
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:935
simplify_exprt::simplify_inequality
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition: simplify_expr_int.cpp:1212
simplify_exprt
Definition: simplify_expr_class.h:73
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:705
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:160
simplify_exprt::simplify_with
resultt simplify_with(const with_exprt &)
Definition: simplify_expr.cpp:1365
simplify_exprt::resultt
Definition: simplify_expr_class.h:96
simplify_exprt::resultt::resultt
resultt(expr_changedt _expr_changed, T _expr)
Definition: simplify_expr_class.h:123
simplify_exprt::simplify_unary_minus
resultt simplify_unary_minus(const unary_minus_exprt &)
Definition: simplify_expr_int.cpp:1121
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:650
simplify_exprt::simplify_pointer_object
resultt simplify_pointer_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:530
minus_exprt
Binary minus.
Definition: std_expr.h:889
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2356
simplify_exprt::simplify_if_branch
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
Definition: simplify_expr_if.cpp:145
simplify_exprt::simplify_index
resultt simplify_index(const index_exprt &)
Definition: simplify_expr_array.cpp:20
simplify_exprt::resultt::resultt
resultt(T _expr)
conversion from expression, thus not 'explicit' marks the expression as "CHANGED"
Definition: simplify_expr_class.h:119
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:2527
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:1493
simplify_exprt::simplify_inequality_pointer_object
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:485
simplify_exprt::resultt::expr
T expr
Definition: simplify_expr_class.h:108
lambda_exprt
A (mathematical) lambda expression.
Definition: mathematical_expr.h:387
simplify_exprt::simplify_sign
resultt simplify_sign(const sign_exprt &)
Definition: simplify_expr.cpp:100
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:1360
simplify_exprt::simplify_if_implies
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
Definition: simplify_expr_if.cpp:16
simplify_exprt::simplify_extractbits
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
Definition: simplify_expr_int.cpp:1038
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:244
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:92
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:1746
index_exprt
Array index operator.
Definition: std_expr.h:1242
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
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:1780
simplify_exprt::simplify_object_size
resultt simplify_object_size(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:654
simplify_exprt::simplify_abs
resultt simplify_abs(const abs_exprt &)
Definition: simplify_expr.cpp:66
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1381
simplify_exprt::simplify_ieee_float_relation
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
Definition: simplify_expr_floatbv.cpp:339
simplify_exprt::simplify_floatbv_typecast
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
Definition: simplify_expr_floatbv.cpp:140
mod_exprt
Modulo.
Definition: std_expr.h:1049
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:274
not_exprt
Boolean negation.
Definition: std_expr.h:2041
simplify_exprt::simplify_isinf
resultt simplify_isinf(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:24