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 "type.h"
21 #include "mp_arith.h"
22 #include "replace_expr.h"
23 
24 class byte_extract_exprt;
25 class byte_update_exprt;
26 class exprt;
27 class if_exprt;
28 class index_exprt;
29 class member_exprt;
30 class namespacet;
31 class tvt;
32 
33 #define forall_value_list(it, value_list) \
34  for(simplify_exprt::value_listt::const_iterator it=(value_list).begin(); \
35  it!=(value_list).end(); ++it)
36 
38 {
39 public:
40  explicit simplify_exprt(const namespacet &_ns):
41  do_simplify_if(true),
42  ns(_ns)
43 #ifdef DEBUG_ON_DEMAND
44  , debug_on(false)
45 #endif
46  {
47 #ifdef DEBUG_ON_DEMAND
48  struct stat f;
49  debug_on=stat("SIMP_DEBUG", &f)==0;
50 #endif
51  }
52 
53  virtual ~simplify_exprt()
54  {
55  }
56 
58 
59  // These below all return 'true' if the simplification wasn't applicable.
60  // If false is returned, the expression has changed.
61 
62  bool simplify_typecast(exprt &expr);
63  bool simplify_extractbit(exprt &expr);
64  bool simplify_extractbits(exprt &expr);
65  bool simplify_concatenation(exprt &expr);
66  bool simplify_mult(exprt &expr);
67  bool simplify_div(exprt &expr);
68  bool simplify_mod(exprt &expr);
69  bool simplify_plus(exprt &expr);
70  bool simplify_minus(exprt &expr);
71  bool simplify_floatbv_op(exprt &expr);
72  bool simplify_floatbv_typecast(exprt &expr);
73  bool simplify_shifts(exprt &expr);
74  bool simplify_power(exprt &expr);
75  bool simplify_bitwise(exprt &expr);
76  bool simplify_if_preorder(if_exprt &expr);
77  bool simplify_if(if_exprt &expr);
78  bool simplify_bitnot(exprt &expr);
79  bool simplify_not(exprt &expr);
80  bool simplify_boolean(exprt &expr);
81  bool simplify_inequality(exprt &expr);
83  bool simplify_lambda(exprt &expr);
84  bool simplify_with(exprt &expr);
85  bool simplify_update(exprt &expr);
86  bool simplify_index(exprt &expr);
87  bool simplify_member(exprt &expr);
90  bool simplify_pointer_object(exprt &expr);
91  bool simplify_object_size(exprt &expr);
92  bool simplify_dynamic_size(exprt &expr);
93  bool simplify_dynamic_object(exprt &expr);
94  bool simplify_invalid_pointer(exprt &expr);
95  bool simplify_same_object(exprt &expr);
96  bool simplify_good_pointer(exprt &expr);
97  bool simplify_object(exprt &expr);
98  bool simplify_unary_minus(exprt &expr);
99  bool simplify_unary_plus(exprt &expr);
100  bool simplify_dereference(exprt &expr);
101  bool simplify_address_of(exprt &expr);
102  bool simplify_pointer_offset(exprt &expr);
103  bool simplify_bswap(exprt &expr);
104  bool simplify_isinf(exprt &expr);
105  bool simplify_isnan(exprt &expr);
106  bool simplify_isnormal(exprt &expr);
107  bool simplify_abs(exprt &expr);
108  bool simplify_sign(exprt &expr);
109  bool simplify_popcount(exprt &expr);
110 
111  // auxiliary
112  bool simplify_if_implies(
113  exprt &expr, const exprt &cond, bool truth, bool &new_truth);
114  bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth);
115  bool simplify_if_conj(exprt &expr, const exprt &cond);
116  bool simplify_if_disj(exprt &expr, const exprt &cond);
117  bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond);
118  bool simplify_if_cond(exprt &expr);
119  bool eliminate_common_addends(exprt &op0, exprt &op1);
120  static tvt objects_equal(const exprt &a, const exprt &b);
121  static tvt objects_equal_address_of(const exprt &a, const exprt &b);
122  bool simplify_address_of_arg(exprt &expr);
127 
128  // main recursion
129  bool simplify_node(exprt &expr);
130  bool simplify_node_preorder(exprt &expr);
131  bool simplify_rec(exprt &expr);
132 
133  virtual bool simplify(exprt &expr);
134 
135  typedef std::set<mp_integer> value_listt;
136  bool get_values(const exprt &expr, value_listt &value_list);
137 
138  static bool is_bitvector_type(const typet &type)
139  {
140  return type.id()==ID_unsignedbv ||
141  type.id()==ID_signedbv ||
142  type.id()==ID_bv;
143  }
144 
145  // bit-level conversions
147  const std::string &bits, const typet &type, bool little_endian);
148  std::string expr2bits(const exprt &expr, bool little_endian);
149 
150 protected:
151  const namespacet &ns;
152 #ifdef DEBUG_ON_DEMAND
153  bool debug_on;
154 #endif
156 };
157 
158 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
The type of an expression.
Definition: type.h:20
bool simplify_abs(exprt &expr)
bool simplify_member(exprt &expr)
bool simplify_same_object(exprt &expr)
bool simplify_sign(exprt &expr)
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
bool simplify_pointer_object(exprt &expr)
bool simplify_node(exprt &expr)
bool simplify_if_cond(exprt &expr)
static tvt objects_equal_address_of(const exprt &a, const exprt &b)
bool simplify_shifts(exprt &expr)
bool simplify_index(exprt &expr)
bool simplify_concatenation(exprt &expr)
bool simplify_dynamic_object(exprt &expr)
std::string expr2bits(const exprt &expr, bool little_endian)
bool simplify_lambda(exprt &expr)
bool simplify_inequality_pointer_object(exprt &expr)
The trinary if-then-else operator.
Definition: std_expr.h:2771
bool simplify_mult(exprt &expr)
bool simplify_address_of_arg(exprt &expr)
bool simplify_mod(exprt &expr)
bool simplify_with(exprt &expr)
bool simplify_if_conj(exprt &expr, const exprt &cond)
bool simplify_node_preorder(exprt &expr)
Extract member of struct or union.
Definition: std_expr.h:3214
virtual ~simplify_exprt()
bool simplify_if(if_exprt &expr)
bool simplify_inequality_constant(exprt &expr)
simplify_exprt(const namespacet &_ns)
const irep_idt & id() const
Definition: irep.h:189
bool simplify_good_pointer(exprt &expr)
bool simplify_object(exprt &expr)
bool simplify_floatbv_op(exprt &expr)
bool simplify_div(exprt &expr)
bool simplify_boolean(exprt &expr)
bool simplify_if_disj(exprt &expr, const exprt &cond)
bool simplify_address_of(exprt &expr)
bool simplify_pointer_offset(exprt &expr)
bool simplify_isinf(exprt &expr)
Definition: threeval.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bool simplify_byte_extract(byte_extract_exprt &expr)
bool simplify_extractbits(exprt &expr)
Simplifies extracting of bits from a constant.
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
exprt bits2expr(const std::string &bits, const typet &type, bool little_endian)
bool simplify_dynamic_size(exprt &expr)
bool simplify_unary_plus(exprt &expr)
bool get_values(const exprt &expr, value_listt &value_list)
bool simplify_bswap(exprt &expr)
bool simplify_popcount(exprt &expr)
bool simplify_floatbv_typecast(exprt &expr)
static tvt objects_equal(const exprt &a, const exprt &b)
bool simplify_if_preorder(if_exprt &expr)
bool simplify_typecast(exprt &expr)
bool simplify_rec(exprt &expr)
bool eliminate_common_addends(exprt &op0, exprt &op1)
bool simplify_unary_minus(exprt &expr)
Base class for all expressions.
Definition: expr.h:46
bool simplify_power(exprt &expr)
bool simplify_bitwise(exprt &expr)
replace_mapt local_replace_map
bool simplify_ieee_float_relation(exprt &expr)
const namespacet & ns
bool simplify_update(exprt &expr)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Definition: replace_expr.h:20
virtual bool simplify(exprt &expr)
TO_BE_DOCUMENTED.
bool simplify_inequality_not_constant(exprt &expr)
bool simplify_dereference(exprt &expr)
bool simplify_not(exprt &expr)
bool simplify_inequality_address_of(exprt &expr)
bool simplify_extractbit(exprt &expr)
bool simplify_minus(exprt &expr)
std::set< mp_integer > value_listt
bool simplify_invalid_pointer(exprt &expr)
TO_BE_DOCUMENTED.
bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth)
bool simplify_isnormal(exprt &expr)
bool simplify_object_size(exprt &expr)
bool simplify_plus(exprt &expr)
bool simplify_inequality(exprt &expr)
simplifies inequalities !=, <=, <, >=, >, and also ==
static bool is_bitvector_type(const typet &type)
bool simplify_byte_update(byte_update_exprt &expr)
bool simplify_bitnot(exprt &expr)
bool simplify_isnan(exprt &expr)
array index operator
Definition: std_expr.h:1170