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;
34 class bitnot_exprt;
35 class bswap_exprt;
36 class byte_extract_exprt;
37 class byte_update_exprt;
39 class dereference_exprt;
40 class div_exprt;
41 class exprt;
42 class extractbit_exprt;
43 class extractbits_exprt;
47 class if_exprt;
48 class index_exprt;
49 class lambda_exprt;
50 class member_exprt;
51 class minus_exprt;
52 class mod_exprt;
53 class multi_ary_exprt;
54 class mult_exprt;
55 class namespacet;
56 class not_exprt;
57 class plus_exprt;
58 class popcount_exprt;
60 class shift_exprt;
61 class sign_exprt;
62 class typecast_exprt;
63 class unary_exprt;
64 class unary_minus_exprt;
65 class unary_plus_exprt;
66 class update_exprt;
67 class with_exprt;
68 
70 {
71 public:
72  explicit simplify_exprt(const namespacet &_ns):
73  do_simplify_if(true),
74  ns(_ns)
75 #ifdef DEBUG_ON_DEMAND
76  , debug_on(false)
77 #endif
78  {
79 #ifdef DEBUG_ON_DEMAND
80  struct stat f;
81  debug_on=stat("SIMP_DEBUG", &f)==0;
82 #endif
83  }
84 
85  virtual ~simplify_exprt()
86  {
87  }
88 
90 
91  template <typename T = exprt>
92  struct resultt
93  {
94  bool has_changed() const
95  {
96  return expr_changed == CHANGED;
97  }
98 
100  {
102  UNCHANGED
104 
105  T expr;
106 
108  operator T() const
109  {
110  return expr;
111  }
112 
115  // NOLINTNEXTLINE(runtime/explicit)
116  resultt(T _expr) : expr_changed(CHANGED), expr(std::move(_expr))
117  {
118  }
119 
120  resultt(expr_changedt _expr_changed, T _expr)
121  : expr_changed(_expr_changed), expr(std::move(_expr))
122  {
123  }
124  };
125 
127  {
128  return resultt<>(resultt<>::UNCHANGED, std::move(expr));
129  }
130 
132  {
134  return result;
135  }
136 
137  // These below all return 'true' if the simplification wasn't applicable.
138  // If false is returned, the expression has changed.
153  bool simplify_if_preorder(if_exprt &expr);
187 
192 
197 
202 
203  // auxiliary
204  bool simplify_if_implies(
205  exprt &expr, const exprt &cond, bool truth, bool &new_truth);
206  bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth);
207  bool simplify_if_conj(exprt &expr, const exprt &cond);
208  bool simplify_if_disj(exprt &expr, const exprt &cond);
209  bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond);
210  bool simplify_if_cond(exprt &expr);
222 
223  // main recursion
225  bool simplify_node_preorder(exprt &expr);
227 
228  virtual bool simplify(exprt &expr);
229 
230  static bool is_bitvector_type(const typet &type)
231  {
232  return type.id()==ID_unsignedbv ||
233  type.id()==ID_signedbv ||
234  type.id()==ID_bv;
235  }
236 
237 protected:
238  const namespacet &ns;
239 #ifdef DEBUG_ON_DEMAND
240  bool debug_on;
241 #endif
242 #ifdef USE_LOCAL_REPLACE_MAP
243  replace_mapt local_replace_map;
244 #endif
245 
246 };
247 
248 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2173
simplify_exprt::~simplify_exprt
virtual ~simplify_exprt()
Definition: simplify_expr_class.h:85
simplify_exprt::simplify_rec
resultt simplify_rec(const exprt &)
Definition: simplify_expr.cpp:2434
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:629
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:126
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:741
simplify_exprt::simplify_shifts
resultt simplify_shifts(const shift_exprt &)
Definition: simplify_expr_int.cpp:900
simplify_exprt::simplify_dereference
resultt simplify_dereference(const dereference_exprt &)
Definition: simplify_expr.cpp:1278
simplify_exprt::simplify_concatenation
resultt simplify_concatenation(const concatenation_exprt &)
Definition: simplify_expr_int.cpp:798
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:1105
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:215
simplify_exprt::simplify_bitnot
resultt simplify_bitnot(const bitnot_exprt &)
Definition: simplify_expr_int.cpp:1172
typet
The type of an expression, extends irept.
Definition: type.h:28
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:256
simplify_exprt::simplify_exprt
simplify_exprt(const namespacet &_ns)
Definition: simplify_expr_class.h:72
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2087
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:2503
simplify_exprt::simplify_is_dynamic_object
resultt simplify_is_dynamic_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:570
simplify_exprt::simplify_if_conj
bool simplify_if_conj(exprt &expr, const exprt &cond)
Definition: simplify_expr_if.cpp:107
nodiscard.h
simplify_exprt::simplify_update
resultt simplify_update(const update_exprt &)
Definition: simplify_expr.cpp:1421
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:831
simplify_exprt::simplify_boolean
resultt simplify_boolean(const exprt &)
Definition: simplify_expr_boolean.cpp:20
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:282
simplify_exprt::simplify_extractbit
resultt simplify_extractbit(const extractbit_exprt &)
Definition: simplify_expr_int.cpp:769
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:551
simplify_exprt::simplify_overflow_binary
resultt simplify_overflow_binary(const binary_exprt &)
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
Definition: simplify_expr.cpp:2051
sign_exprt
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:507
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:2030
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:94
div_exprt
Division.
Definition: std_expr.h:981
simplify_exprt::simplify_plus
resultt simplify_plus(const plus_exprt &)
Definition: simplify_expr_int.cpp:402
simplify_exprt::simplify_overflow_unary
resultt simplify_overflow_unary(const unary_exprt &)
Try to simplify overflow-unary-.
Definition: simplify_expr.cpp:2114
simplify_exprt::simplify_byte_extract
resultt simplify_byte_extract(const byte_extract_exprt &)
Definition: simplify_expr.cpp:1549
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:1303
simplify_exprt::unchanged
static resultt unchanged(exprt expr)
Definition: simplify_expr_class.h:126
simplify_exprt::simplify_node
resultt simplify_node(exprt)
Definition: simplify_expr.cpp:2192
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:101
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:102
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:100
simplify_exprt::simplify_power
resultt simplify_power(const binary_exprt &)
Definition: simplify_expr_int.cpp:1008
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:1464
simplify_exprt::simplify_typecast
resultt simplify_typecast(const typecast_exprt &)
Definition: simplify_expr.cpp:683
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
simplify_exprt::changed
static resultt changed(resultt<> result)
Definition: simplify_expr_class.h:131
simplify_exprt::is_bitvector_type
static bool is_bitvector_type(const typet &type)
Definition: simplify_expr_class.h:230
simplify_exprt::simplify_inequality_rhs_is_constant
resultt simplify_inequality_rhs_is_constant(const binary_relation_exprt &)
Definition: simplify_expr_int.cpp:1536
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:2161
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:936
simplify_exprt::simplify_inequality
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition: simplify_expr_int.cpp:1203
simplify_exprt
Definition: simplify_expr_class.h:70
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:391
simplify_exprt::simplify_good_pointer
resultt simplify_good_pointer(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:713
irept::id
const irep_idt & id() const
Definition: irep.h:407
abs_exprt
Absolute value.
Definition: std_expr.h:347
unary_plus_exprt
The unary plus expression.
Definition: std_expr.h:440
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:1341
simplify_exprt::resultt
Definition: simplify_expr_class.h:93
simplify_exprt::resultt::resultt
resultt(expr_changedt _expr_changed, T _expr)
Definition: simplify_expr_class.h:120
simplify_exprt::simplify_unary_minus
resultt simplify_unary_minus(const unary_minus_exprt &)
Definition: simplify_expr_int.cpp:1112
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:626
simplify_exprt::simplify_pointer_object
resultt simplify_pointer_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:538
minus_exprt
Binary minus.
Definition: std_expr.h:890
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2357
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:116
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:2528
simplify_exprt::simplify_member
resultt simplify_member(const member_exprt &)
Definition: simplify_expr_struct.cpp:20
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:1469
simplify_exprt::simplify_inequality_pointer_object
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:493
simplify_exprt::resultt::expr
T expr
Definition: simplify_expr_class.h:105
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:675
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:1336
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:1029
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:238
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:89
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:1722
index_exprt
Array index operator.
Definition: std_expr.h:1243
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:200
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:1781
simplify_exprt::simplify_object_size
resultt simplify_object_size(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:662
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:1382
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.
Definition: std_expr.h:1050
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:2042
simplify_exprt::simplify_isinf
resultt simplify_isinf(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:23