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 // #define USE_LOCAL_REPLACE_MAP
23 #ifdef USE_LOCAL_REPLACE_MAP
24 #include "replace_expr.h"
25 #endif
26 
27 class bswap_exprt;
28 class byte_extract_exprt;
29 class byte_update_exprt;
30 class exprt;
31 class extractbits_exprt;
32 class if_exprt;
33 class index_exprt;
34 class member_exprt;
35 class namespacet;
36 class popcount_exprt;
37 class tvt;
38 
39 #define forall_value_list(it, value_list) \
40  for(simplify_exprt::value_listt::const_iterator it=(value_list).begin(); \
41  it!=(value_list).end(); ++it)
42 
44 {
45 public:
46  explicit simplify_exprt(const namespacet &_ns):
47  do_simplify_if(true),
48  ns(_ns)
49 #ifdef DEBUG_ON_DEMAND
50  , debug_on(false)
51 #endif
52  {
53 #ifdef DEBUG_ON_DEMAND
54  struct stat f;
55  debug_on=stat("SIMP_DEBUG", &f)==0;
56 #endif
57  }
58 
59  virtual ~simplify_exprt()
60  {
61  }
62 
64 
65  // These below all return 'true' if the simplification wasn't applicable.
66  // If false is returned, the expression has changed.
67 
68  bool simplify_typecast(exprt &expr);
69  bool simplify_extractbit(exprt &expr);
71  bool simplify_concatenation(exprt &expr);
72  bool simplify_mult(exprt &expr);
73  bool simplify_div(exprt &expr);
74  bool simplify_mod(exprt &expr);
75  bool simplify_plus(exprt &expr);
76  bool simplify_minus(exprt &expr);
77  bool simplify_floatbv_op(exprt &expr);
78  bool simplify_floatbv_typecast(exprt &expr);
79  bool simplify_shifts(exprt &expr);
80  bool simplify_power(exprt &expr);
81  bool simplify_bitwise(exprt &expr);
82  bool simplify_if_preorder(if_exprt &expr);
83  bool simplify_if(if_exprt &expr);
84  bool simplify_bitnot(exprt &expr);
85  bool simplify_not(exprt &expr);
86  bool simplify_boolean(exprt &expr);
87  bool simplify_inequality(exprt &expr);
89  bool simplify_lambda(exprt &expr);
90  bool simplify_with(exprt &expr);
91  bool simplify_update(exprt &expr);
92  bool simplify_index(exprt &expr);
93  bool simplify_member(exprt &expr);
96  bool simplify_pointer_object(exprt &expr);
97  bool simplify_object_size(exprt &expr);
98  bool simplify_dynamic_size(exprt &expr);
99  bool simplify_dynamic_object(exprt &expr);
100  bool simplify_invalid_pointer(exprt &expr);
101  bool simplify_same_object(exprt &expr);
102  bool simplify_good_pointer(exprt &expr);
103  bool simplify_object(exprt &expr);
104  bool simplify_unary_minus(exprt &expr);
105  bool simplify_unary_plus(exprt &expr);
106  bool simplify_dereference(exprt &expr);
107  bool simplify_address_of(exprt &expr);
108  bool simplify_pointer_offset(exprt &expr);
109  bool simplify_bswap(bswap_exprt &expr);
110  bool simplify_isinf(exprt &expr);
111  bool simplify_isnan(exprt &expr);
112  bool simplify_isnormal(exprt &expr);
113  bool simplify_abs(exprt &expr);
114  bool simplify_sign(exprt &expr);
115  bool simplify_popcount(popcount_exprt &expr);
116 
117  // auxiliary
118  bool simplify_if_implies(
119  exprt &expr, const exprt &cond, bool truth, bool &new_truth);
120  bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth);
121  bool simplify_if_conj(exprt &expr, const exprt &cond);
122  bool simplify_if_disj(exprt &expr, const exprt &cond);
123  bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond);
124  bool simplify_if_cond(exprt &expr);
125  bool eliminate_common_addends(exprt &op0, exprt &op1);
126  static tvt objects_equal(const exprt &a, const exprt &b);
127  static tvt objects_equal_address_of(const exprt &a, const exprt &b);
128  bool simplify_address_of_arg(exprt &expr);
133 
134  // main recursion
135  bool simplify_node(exprt &expr);
136  bool simplify_node_preorder(exprt &expr);
137  bool simplify_rec(exprt &expr);
138 
139  virtual bool simplify(exprt &expr);
140 
141  typedef std::set<mp_integer> value_listt;
142  bool get_values(const exprt &expr, value_listt &value_list);
143 
144  static bool is_bitvector_type(const typet &type)
145  {
146  return type.id()==ID_unsignedbv ||
147  type.id()==ID_signedbv ||
148  type.id()==ID_bv;
149  }
150 
151  // bit-level conversions
153  const std::string &bits, const typet &type, bool little_endian);
154  std::string expr2bits(const exprt &expr, bool little_endian);
155 
156 protected:
157  const namespacet &ns;
158 #ifdef DEBUG_ON_DEMAND
159  bool debug_on;
160 #endif
161 #ifdef USE_LOCAL_REPLACE_MAP
162  replace_mapt local_replace_map;
163 #endif
164 };
165 
166 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
The type of an expression.
Definition: type.h:22
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_popcount(popcount_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:3361
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:3871
bool simplify_bswap(bswap_exprt &expr)
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)
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:3072
bool simplify_pointer_offset(exprt &expr)
bool simplify_isinf(exprt &expr)
Definition: threeval.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
bool simplify_byte_extract(byte_extract_exprt &expr)
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_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)
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4890
bool simplify_unary_minus(exprt &expr)
Base class for all expressions.
Definition: expr.h:42
bool simplify_power(exprt &expr)
bool simplify_bitwise(exprt &expr)
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:22
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)
The byte swap expression.
Definition: std_expr.h:506
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)
bool simplify_extractbits(extractbits_exprt &expr)
Simplifies extracting of bits from a constant.
array index operator
Definition: std_expr.h:1462