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 member_exprt;
50 class minus_exprt;
51 class mod_exprt;
52 class multi_ary_exprt;
53 class mult_exprt;
54 class namespacet;
55 class not_exprt;
56 class plus_exprt;
57 class popcount_exprt;
59 class shift_exprt;
60 class sign_exprt;
61 class tvt;
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 
69 #define forall_value_list(it, value_list) \
70  for(simplify_exprt::value_listt::const_iterator it=(value_list).begin(); \
71  it!=(value_list).end(); ++it)
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);
193 
198 
199  // auxiliary
200  bool simplify_if_implies(
201  exprt &expr, const exprt &cond, bool truth, bool &new_truth);
202  bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth);
203  bool simplify_if_conj(exprt &expr, const exprt &cond);
204  bool simplify_if_disj(exprt &expr, const exprt &cond);
205  bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond);
206  bool simplify_if_cond(exprt &expr);
207  bool eliminate_common_addends(exprt &op0, exprt &op1);
208  static tvt objects_equal(const exprt &a, const exprt &b);
209  static tvt objects_equal_address_of(const exprt &a, const exprt &b);
221 
222  // main recursion
224  bool simplify_node_preorder(exprt &expr);
226 
227  virtual bool simplify(exprt &expr);
228 
229  typedef std::set<mp_integer> value_listt;
230  bool get_values(const exprt &expr, value_listt &value_list);
231 
232  static bool is_bitvector_type(const typet &type)
233  {
234  return type.id()==ID_unsignedbv ||
235  type.id()==ID_signedbv ||
236  type.id()==ID_bv;
237  }
238 
239  // bit-level conversions
241  bits2expr(const std::string &bits, const typet &type, bool little_endian);
242 
243  optionalt<std::string> expr2bits(const exprt &, bool little_endian);
244 
245 protected:
246  const namespacet &ns;
247 #ifdef DEBUG_ON_DEMAND
248  bool debug_on;
249 #endif
250 #ifdef USE_LOCAL_REPLACE_MAP
251  replace_mapt local_replace_map;
252 #endif
253 
254 };
255 
256 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3050
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:2603
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:631
simplify_exprt::simplify_isnormal
resultt simplify_isnormal(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:48
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:791
simplify_exprt::simplify_shifts
resultt simplify_shifts(const shift_exprt &)
Definition: simplify_expr_int.cpp:899
simplify_exprt::simplify_dereference
resultt simplify_dereference(const dereference_exprt &)
Definition: simplify_expr.cpp:1273
simplify_exprt::simplify_concatenation
resultt simplify_concatenation(const concatenation_exprt &)
Definition: simplify_expr_int.cpp:797
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:212
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:1104
simplify_exprt::simplify_bitwise
resultt simplify_bitwise(const multi_ary_exprt &)
Definition: simplify_expr_int.cpp:599
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:1171
typet
The type of an expression, extends irept.
Definition: type.h:29
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
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:2964
simplify_exprt::simplify_popcount
resultt simplify_popcount(const popcount_exprt &)
Definition: simplify_expr.cpp:127
simplify_exprt::simplify_inequality_address_of
resultt simplify_inequality_address_of(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:422
simplify_exprt::simplify
virtual bool simplify(exprt &expr)
Definition: simplify_expr.cpp:2672
simplify_exprt::simplify_is_dynamic_object
resultt simplify_is_dynamic_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:572
simplify_exprt::simplify_if_conj
bool simplify_if_conj(exprt &expr, const exprt &cond)
Definition: simplify_expr_if.cpp:107
simplify_exprt::get_values
bool get_values(const exprt &expr, value_listt &value_list)
Definition: simplify_expr.cpp:1330
simplify_exprt::bits2expr
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian)
Definition: simplify_expr.cpp:1567
nodiscard.h
simplify_exprt::simplify_update
resultt simplify_update(const update_exprt &)
Definition: simplify_expr.cpp:1440
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
simplify_exprt::simplify_boolean
resultt simplify_boolean(const exprt &)
Definition: simplify_expr_boolean.cpp:20
exprt
Base class for all expressions.
Definition: expr.h:53
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:269
simplify_exprt::simplify_extractbit
resultt simplify_extractbit(const extractbit_exprt &)
Definition: simplify_expr_int.cpp:768
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
sign_exprt
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:557
concatenation_exprt
Concatenation of bit-vector operands.
Definition: std_expr.h:4067
simplify_exprt::simplify_complex
resultt simplify_complex(const unary_exprt &)
Definition: simplify_expr.cpp:2320
simplify_exprt::simplify_pointer_offset
resultt simplify_pointer_offset(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:250
simplify_exprt::resultt::has_changed
bool has_changed() const
Definition: simplify_expr_class.h:98
div_exprt
Division.
Definition: std_expr.h:1031
simplify_exprt::simplify_plus
resultt simplify_plus(const plus_exprt &)
Definition: simplify_expr_int.cpp:401
simplify_exprt::simplify_byte_extract
resultt simplify_byte_extract(const byte_extract_exprt &)
Definition: simplify_expr.cpp:1875
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:1302
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:2371
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: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:106
simplify_exprt::simplify_minus
resultt simplify_minus(const minus_exprt &)
Definition: simplify_expr_int.cpp:557
simplify_exprt::simplify_dynamic_size
resultt simplify_dynamic_size(const unary_exprt &)
simplify_exprt::resultt::expr_changedt
expr_changedt
Definition: simplify_expr_class.h:104
simplify_exprt::simplify_same_object
resultt simplify_same_object(const unary_exprt &)
simplify_exprt::simplify_power
resultt simplify_power(const binary_exprt &)
Definition: simplify_expr_int.cpp:1007
simplify_exprt::simplify_div
resultt simplify_div(const div_exprt &)
Definition: simplify_expr_int.cpp:270
simplify_exprt::simplify_inequality_no_constant
resultt simplify_inequality_no_constant(const binary_relation_exprt &)
Definition: simplify_expr_int.cpp:1465
simplify_exprt::simplify_typecast
resultt simplify_typecast(const typecast_exprt &)
Definition: simplify_expr.cpp:678
simplify_exprt::simplify_mod
resultt simplify_mod(const mod_exprt &)
Definition: simplify_expr_int.cpp:364
floatbv_typecast_exprt
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2067
simplify_exprt::simplify_isnan
resultt simplify_isnan(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:36
simplify_exprt::changed
static resultt changed(resultt<> result)
Definition: simplify_expr_class.h:135
simplify_exprt::value_listt
std::set< mp_integer > value_listt
Definition: simplify_expr_class.h:229
simplify_exprt::is_bitvector_type
static bool is_bitvector_type(const typet &type)
Definition: simplify_expr_class.h:232
simplify_exprt::simplify_inequality_rhs_is_constant
resultt simplify_inequality_rhs_is_constant(const binary_relation_exprt &)
Definition: simplify_expr_int.cpp:1587
simplify_exprt::simplify_bswap
resultt simplify_bswap(const bswap_exprt &)
Definition: simplify_expr_int.cpp:28
simplify_exprt::simplify_node_preorder
bool simplify_node_preorder(exprt &expr)
Definition: simplify_expr.cpp:2340
simplify_exprt::resultt::expr_changed
enum simplify_exprt::resultt::expr_changedt expr_changed
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
simplify_exprt::simplify_inequality
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition: simplify_expr_int.cpp:1202
simplify_exprt
Definition: simplify_expr_class.h:74
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:378
simplify_exprt::simplify_good_pointer
resultt simplify_good_pointer(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:765
irept::id
const irep_idt & id() const
Definition: irep.h:418
abs_exprt
Absolute value.
Definition: std_expr.h:334
unary_plus_exprt
The unary plus expression.
Definition: std_expr.h:427
simplify_exprt::simplify_mult
resultt simplify_mult(const mult_exprt &)
Definition: simplify_expr_int.cpp:158
simplify_exprt::simplify_with
resultt simplify_with(const with_exprt &)
Definition: simplify_expr.cpp:1360
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:1111
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
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:627
simplify_exprt::simplify_pointer_object
resultt simplify_pointer_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:540
tvt
Definition: threeval.h:20
minus_exprt
Binary minus.
Definition: std_expr.h:940
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3234
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:120
bitnot_exprt
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2344
simplify_exprt::expr2bits
optionalt< std::string > expr2bits(const exprt &, bool little_endian)
Definition: simplify_expr.cpp:1764
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2629
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
simplify_exprt::simplify_member
resultt simplify_member(const member_exprt &)
Definition: simplify_expr_struct.cpp:19
shift_exprt
A base class for shift operators.
Definition: std_expr.h:2496
simplify_exprt::simplify_object
resultt simplify_object(const exprt &)
Definition: simplify_expr.cpp:1488
simplify_exprt::objects_equal
static tvt objects_equal(const exprt &a, const exprt &b)
Definition: simplify_expr_pointer.cpp:663
simplify_exprt::objects_equal_address_of
static tvt objects_equal_address_of(const exprt &a, const exprt &b)
Definition: simplify_expr_pointer.cpp:689
simplify_exprt::simplify_inequality_pointer_object
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:495
simplify_exprt::resultt::expr
T expr
Definition: simplify_expr_class.h:109
simplify_exprt::simplify_sign
resultt simplify_sign(const sign_exprt &)
Definition: simplify_expr.cpp:101
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:725
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_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:1028
ieee_float_op_exprt
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: std_expr.h:3790
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:246
bswap_exprt
The byte swap expression.
Definition: std_expr.h:471
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:59
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2697
replace_expr.h
simplify_exprt::simplify_byte_update
resultt simplify_byte_update(const byte_update_exprt &)
Definition: simplify_expr.cpp:2045
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4308
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
simplify_exprt::eliminate_common_addends
bool eliminate_common_addends(exprt &op0, exprt &op1)
Definition: simplify_expr_int.cpp:1417
simplify_exprt::simplify_object_size
resultt simplify_object_size(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:714
simplify_exprt::simplify_abs
resultt simplify_abs(const abs_exprt &)
Definition: simplify_expr.cpp:67
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1432
simplify_exprt::simplify_ieee_float_relation
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
Definition: simplify_expr_floatbv.cpp:333
simplify_exprt::simplify_lambda
resultt simplify_lambda(const exprt &)
Definition: simplify_expr.cpp:1355
simplify_exprt::simplify_floatbv_typecast
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
Definition: simplify_expr_floatbv.cpp:134
mod_exprt
Modulo.
Definition: std_expr.h:1100
simplify_exprt::simplify_floatbv_op
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
Definition: simplify_expr_floatbv.cpp:268
not_exprt
Boolean negation.
Definition: std_expr.h:2843
simplify_exprt::simplify_isinf
resultt simplify_isinf(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:21