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 
155  optionalt<std::string> expr2bits(const exprt &, bool little_endian);
156 
157 protected:
158  const namespacet &ns;
159 #ifdef DEBUG_ON_DEMAND
160  bool debug_on;
161 #endif
162 #ifdef USE_LOCAL_REPLACE_MAP
163  replace_mapt local_replace_map;
164 #endif
165 };
166 
167 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
simplify_exprt::simplify_node
bool simplify_node(exprt &expr)
Definition: simplify_expr.cpp:2113
simplify_exprt::~simplify_exprt
virtual ~simplify_exprt()
Definition: simplify_expr_class.h:59
simplify_exprt::simplify_if_recursive
bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth)
Definition: simplify_expr.cpp:851
simplify_exprt::simplify_if_disj
bool simplify_if_disj(exprt &expr, const exprt &cond)
Definition: simplify_expr.cpp:904
simplify_exprt::simplify_pointer_object
bool simplify_pointer_object(exprt &expr)
Definition: simplify_expr_pointer.cpp:487
simplify_exprt::simplify_extractbit
bool simplify_extractbit(exprt &expr)
Definition: simplify_expr_int.cpp:835
simplify_exprt::simplify_index
bool simplify_index(exprt &expr)
Definition: simplify_expr_array.cpp:17
simplify_exprt::simplify_minus
bool simplify_minus(exprt &expr)
Definition: simplify_expr_int.cpp:592
simplify_exprt::simplify_mult
bool simplify_mult(exprt &expr)
Definition: simplify_expr_int.cpp:160
simplify_exprt::simplify_inequality
bool simplify_inequality(exprt &expr)
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition: simplify_expr_int.cpp:1305
simplify_exprt::simplify_inequality_pointer_object
bool simplify_inequality_pointer_object(exprt &expr)
Definition: simplify_expr_pointer.cpp:454
byte_update_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:70
mp_arith.h
simplify_exprt::simplify_dynamic_size
bool simplify_dynamic_size(exprt &expr)
simplify_exprt::simplify_isnormal
bool simplify_isnormal(exprt &expr)
Definition: simplify_expr_floatbv.cpp:52
simplify_exprt::simplify_if_preorder
bool simplify_if_preorder(if_exprt &expr)
Definition: simplify_expr.cpp:993
typet
The type of an expression, extends irept.
Definition: type.h:27
simplify_exprt::simplify_exprt
simplify_exprt(const namespacet &_ns)
Definition: simplify_expr_class.h:46
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
simplify_exprt::simplify
virtual bool simplify(exprt &expr)
Definition: simplify_expr.cpp:2306
simplify_exprt::simplify_if_conj
bool simplify_if_conj(exprt &expr, const exprt &cond)
Definition: simplify_expr.cpp:883
simplify_exprt::get_values
bool get_values(const exprt &expr, value_listt &value_list)
Definition: simplify_expr.cpp:1182
exprt
Base class for all expressions.
Definition: expr.h:54
simplify_exprt::simplify_if_cond
bool simplify_if_cond(exprt &expr)
Definition: simplify_expr.cpp:957
simplify_exprt::simplify_bitwise
bool simplify_bitwise(exprt &expr)
Definition: simplify_expr_int.cpp:649
simplify_exprt::simplify_inequality_not_constant
bool simplify_inequality_not_constant(exprt &expr)
Definition: simplify_expr_int.cpp:1540
simplify_exprt::simplify_lambda
bool simplify_lambda(exprt &expr)
Definition: simplify_expr.cpp:1208
simplify_exprt::simplify_boolean
bool simplify_boolean(exprt &expr)
Definition: simplify_expr_boolean.cpp:19
simplify_exprt::simplify_popcount
bool simplify_popcount(popcount_exprt &expr)
Definition: simplify_expr.cpp:132
simplify_exprt::simplify_abs
bool simplify_abs(exprt &expr)
Definition: simplify_expr.cpp:62
simplify_exprt::simplify_dynamic_object
bool simplify_dynamic_object(exprt &expr)
Definition: simplify_expr_pointer.cpp:515
simplify_exprt::simplify_typecast
bool simplify_typecast(exprt &expr)
Definition: simplify_expr.cpp:160
simplify_exprt::simplify_member
bool simplify_member(exprt &expr)
Definition: simplify_expr_struct.cpp:19
simplify_exprt::simplify_good_pointer
bool simplify_good_pointer(exprt &expr)
Definition: simplify_expr_pointer.cpp:694
type.h
simplify_exprt::simplify_concatenation
bool simplify_concatenation(exprt &expr)
Definition: simplify_expr_int.cpp:869
simplify_exprt::bits2expr
exprt bits2expr(const std::string &bits, const typet &type, bool little_endian)
Definition: simplify_expr.cpp:1431
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
simplify_exprt::simplify_inequality_address_of
bool simplify_inequality_address_of(exprt &expr)
Definition: simplify_expr_pointer.cpp:413
simplify_exprt::simplify_shifts
bool simplify_shifts(exprt &expr)
Definition: simplify_expr_int.cpp:967
simplify_exprt::simplify_not
bool simplify_not(exprt &expr)
Definition: simplify_expr_boolean.cpp:159
simplify_exprt::simplify_update
bool simplify_update(exprt &expr)
Definition: simplify_expr.cpp:1288
simplify_exprt::value_listt
std::set< mp_integer > value_listt
Definition: simplify_expr_class.h:141
simplify_exprt::is_bitvector_type
static bool is_bitvector_type(const typet &type)
Definition: simplify_expr_class.h:144
simplify_exprt::simplify_unary_minus
bool simplify_unary_minus(exprt &expr)
Definition: simplify_expr_int.cpp:1189
simplify_exprt::simplify_invalid_pointer
bool simplify_invalid_pointer(exprt &expr)
Definition: simplify_expr_pointer.cpp:571
simplify_exprt::simplify_node_preorder
bool simplify_node_preorder(exprt &expr)
Definition: simplify_expr.cpp:2088
simplify_exprt::simplify_object_size
bool simplify_object_size(exprt &expr)
Definition: simplify_expr_pointer.cpp:648
simplify_exprt::simplify_bswap
bool simplify_bswap(bswap_exprt &expr)
Definition: simplify_expr_int.cpp:29
simplify_exprt::simplify_sign
bool simplify_sign(exprt &expr)
Definition: simplify_expr.cpp:102
simplify_exprt
Definition: simplify_expr_class.h:43
simplify_exprt::simplify_bitnot
bool simplify_bitnot(exprt &expr)
Definition: simplify_expr_int.cpp:1266
simplify_exprt::simplify_same_object
bool simplify_same_object(exprt &expr)
irept::id
const irep_idt & id() const
Definition: irep.h:259
simplify_exprt::simplify_unary_plus
bool simplify_unary_plus(exprt &expr)
Definition: simplify_expr_int.cpp:1179
simplify_exprt::simplify_pointer_offset
bool simplify_pointer_offset(exprt &expr)
Definition: simplify_expr_pointer.cpp:211
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
simplify_exprt::simplify_floatbv_op
bool simplify_floatbv_op(exprt &expr)
Definition: simplify_expr_floatbv.cpp:283
tvt
Definition: threeval.h:19
simplify_exprt::simplify_if_branch
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
Definition: simplify_expr.cpp:925
simplify_exprt::expr2bits
optionalt< std::string > expr2bits(const exprt &, bool little_endian)
Definition: simplify_expr.cpp:1547
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
simplify_exprt::simplify_power
bool simplify_power(exprt &expr)
Definition: simplify_expr_int.cpp:1079
simplify_exprt::simplify_ieee_float_relation
bool simplify_ieee_float_relation(exprt &expr)
Definition: simplify_expr_floatbv.cpp:354
simplify_exprt::objects_equal
static tvt objects_equal(const exprt &a, const exprt &b)
Definition: simplify_expr_pointer.cpp:600
simplify_exprt::objects_equal_address_of
static tvt objects_equal_address_of(const exprt &a, const exprt &b)
Definition: simplify_expr_pointer.cpp:624
simplify_exprt::simplify_isinf
bool simplify_isinf(exprt &expr)
Definition: simplify_expr_floatbv.cpp:19
simplify_exprt::simplify_byte_update
bool simplify_byte_update(byte_update_exprt &expr)
Definition: simplify_expr.cpp:1795
simplify_exprt::simplify_address_of
bool simplify_address_of(exprt &expr)
Definition: simplify_expr_pointer.cpp:173
simplify_exprt::simplify_rec
bool simplify_rec(exprt &expr)
Definition: simplify_expr.cpp:2245
replace_mapt
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Definition: replace_expr.h:22
simplify_exprt::simplify_isnan
bool simplify_isnan(exprt &expr)
Definition: simplify_expr_floatbv.cpp:37
byte_extract_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:25
simplify_exprt::simplify_object
bool simplify_object(exprt &expr)
Definition: simplify_expr.cpp:1341
simplify_exprt::simplify_mod
bool simplify_mod(exprt &expr)
Definition: simplify_expr_int.cpp:388
simplify_exprt::simplify_if_implies
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
Definition: simplify_expr.cpp:795
simplify_exprt::simplify_inequality_constant
bool simplify_inequality_constant(exprt &expr)
Definition: simplify_expr_int.cpp:1669
simplify_exprt::simplify_if
bool simplify_if(if_exprt &expr)
Definition: simplify_expr.cpp:1078
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:158
bswap_exprt
The byte swap expression.
Definition: std_expr.h:568
simplify_exprt::do_simplify_if
bool do_simplify_if
Definition: simplify_expr_class.h:63
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:3157
replace_expr.h
simplify_exprt::simplify_plus
bool simplify_plus(exprt &expr)
Definition: simplify_expr_int.cpp:437
index_exprt
Array index operator.
Definition: std_expr.h:1595
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4815
simplify_exprt::simplify_address_of_arg
bool simplify_address_of_arg(exprt &expr)
Definition: simplify_expr_pointer.cpp:52
simplify_exprt::eliminate_common_addends
bool eliminate_common_addends(exprt &op0, exprt &op1)
Definition: simplify_expr_int.cpp:1492
simplify_exprt::simplify_with
bool simplify_with(exprt &expr)
Definition: simplify_expr.cpp:1215
simplify_exprt::simplify_extractbits
bool simplify_extractbits(extractbits_exprt &expr)
Simplifies extracting of bits from a constant.
Definition: simplify_expr_int.cpp:1102
simplify_exprt::simplify_dereference
bool simplify_dereference(exprt &expr)
Definition: simplify_expr.cpp:737
simplify_exprt::simplify_byte_extract
bool simplify_byte_extract(byte_extract_exprt &expr)
Definition: simplify_expr.cpp:1619
simplify_exprt::simplify_div
bool simplify_div(exprt &expr)
Definition: simplify_expr_int.cpp:268
simplify_exprt::simplify_floatbv_typecast
bool simplify_floatbv_typecast(exprt &expr)
Definition: simplify_expr_floatbv.cpp:141