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
Absolute value.
Definition: std_expr.h:347
Operator to return the address of an object.
Definition: pointer_expr.h:200
Array constructor from list of elements.
Definition: std_expr.h:1382
A base class for binary expressions.
Definition: std_expr.h:551
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:675
Bit-wise negation of bit-vectors.
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.
Operator to dereference a pointer.
Definition: pointer_expr.h:256
Division.
Definition: std_expr.h:981
Base class for all expressions.
Definition: expr.h:54
Extracts a single bit of a bit-vector operand.
Extracts a sub-range of a bit-vector operand.
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
Application of (mathematical) function.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
The trinary if-then-else operator.
Definition: std_expr.h:2087
Array index operator.
Definition: std_expr.h:1243
const irep_idt & id() const
Definition: irep.h:407
A (mathematical) lambda expression.
Extract member of struct or union.
Definition: std_expr.h:2528
Binary minus.
Definition: std_expr.h:890
Modulo.
Definition: std_expr.h:1050
Binary multiplication Associativity is not specified.
Definition: std_expr.h:936
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:741
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Boolean negation.
Definition: std_expr.h:2042
The plus expression Associativity is not specified.
Definition: std_expr.h:831
The popcount (counting the number of bits set to 1) expression.
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:507
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_overflow_unary(const unary_exprt &)
Try to simplify overflow-unary-.
resultt simplify_byte_extract(const byte_extract_exprt &)
resultt simplify_abs(const abs_exprt &)
resultt simplify_overflow_binary(const binary_exprt &)
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
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_good_pointer(const unary_exprt &)
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 &)
bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth)
resultt simplify_pointer_offset(const unary_exprt &)
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_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 &)
virtual ~simplify_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_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_object_size(const unary_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_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_is_dynamic_object(const unary_exprt &)
resultt simplify_node(exprt)
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
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_ieee_float_relation(const binary_relation_exprt &)
resultt simplify_pointer_object(const unary_exprt &)
resultt simplify_sign(const sign_exprt &)
resultt simplify_unary_minus(const unary_minus_exprt &)
Semantic type conversion.
Definition: std_expr.h:1781
The type of an expression, extends irept.
Definition: type.h:28
Generic base class for unary expressions.
Definition: std_expr.h:282
The unary minus expression.
Definition: std_expr.h:391
The unary plus expression.
Definition: std_expr.h:440
Operator to update elements in structs and arrays.
Definition: std_expr.h:2357
Operator to update elements in structs and arrays.
Definition: std_expr.h:2173
#define NODISCARD
Definition: nodiscard.h:22
resultt
The result of goto verifying.
Definition: properties.h:44
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Definition: replace_expr.h:22
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.