cprover
constant_propagator.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Constant Propagation
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "constant_propagator.h"
13 
14 #ifdef DEBUG
15 #include <iostream>
16 #endif
17 
18 #include <util/find_symbols.h>
19 #include <util/arith_tools.h>
20 #include <util/simplify_expr.h>
21 
23  const exprt &array, const exprt &index,
24  const typet &type)
25 {
26  std::string a, idx, identifier;
27  a = array.get_string(ID_identifier);
28 
29  if (index.id()==ID_typecast)
30  idx = index.op0().get_string(ID_value);
31  else
32  idx = index.get_string(ID_value);
33 
35  identifier=a+"["+integer2string(i)+"]";
36  symbol_exprt new_expr(identifier, type);
37 
38  return new_expr;
39 }
40 
42  const exprt &array, const mp_integer &index,
43  const typet &type)
44 {
45  std::string a, identifier;
46  a = array.get_string(ID_identifier);
47  identifier=a+"["+integer2string(index)+"]";
48  symbol_exprt new_expr(identifier, type);
49 
50  return new_expr;
51 }
52 
54  valuest &values,
55  const exprt &lhs, const exprt &rhs,
56  const namespacet &ns)
57 {
58  const typet & lhs_type = ns.follow(lhs.type());
59  const typet & rhs_type = ns.follow(rhs.type());
60 
61 #ifdef DEBUG
62  std::cout << "assign: " << from_expr(ns, "", lhs)
63  << " := " << from_type(ns, "", rhs_type) << '\n';
64 #endif
65 
66  if(lhs.id()==ID_symbol && rhs.id()==ID_if)
67  {
68  exprt cond=rhs.op0();
69  assert(cond.operands().size()==2);
70  if(values.is_constant(cond.op0())
71  && values.is_constant(cond.op1()))
72  {
73  if(cond.op0().id()==ID_index)
74  {
75  exprt index=cond.op0();
76  exprt new_expr=concatenate_array_id(index.op0(), index.op1(), index.type());
77  values.replace_const(new_expr);
78  cond.op0()=new_expr;
79  cond = simplify_expr(cond,ns);
80  }
81  else
82  assert(0);
83 
84  assign(values, to_symbol_expr(lhs), cond, ns);
85  }
86  }
87  else if(lhs.id()==ID_symbol && rhs_type.id()!=ID_array
88  && rhs_type.id()!=ID_struct
89  && rhs_type.id()!=ID_union)
90  {
91  if(values.is_constant(rhs))
92  assign(values, to_symbol_expr(lhs), rhs, ns);
93  else
95  }
96  else if(lhs.id()==ID_symbol && lhs_type.id()==ID_array
97  && rhs_type.id()==ID_array)
98  {
99  exprt new_expr;
100  mp_integer idx=0;
101  forall_operands(it, rhs)
102  {
103  new_expr=concatenate_array_id(lhs, idx, it->type());
104  assign(values, to_symbol_expr(new_expr), *it, ns);
105  idx = idx +1;
106  }
107  }
108  else if (lhs.id()==ID_index)
109  {
110  if (values.is_constant(lhs.op1())
111  && values.is_constant(rhs))
112  {
113  exprt new_expr=concatenate_array_id(lhs.op0(), lhs.op1(), rhs.type());
114  assign(values, to_symbol_expr(new_expr), rhs, ns);
115  }
116  }
117 #if 0
118  else // TODO: could make field or array element-sensitive
119  {
120  }
121 #endif
122 }
123 
125  locationt from,
126  locationt to,
127  ai_baset &ai,
128  const namespacet &ns)
129 {
130  #ifdef DEBUG
131  std::cout << from->location_number << " --> "
132  << to->location_number << '\n';
133  #endif
134 
135 #ifdef DEBUG
136  std::cout << "before:\n";
137  output(std::cout, ai, ns);
138 #endif
139 
140  if(from->is_decl())
141  {
142  const code_declt &code_decl=to_code_decl(from->code);
143  const symbol_exprt &symbol=to_symbol_expr(code_decl.symbol());
144  values.set_to_top(symbol);
145  }
146  else if(from->is_assign())
147  {
148  const code_assignt &assignment=to_code_assign(from->code);
149  const exprt &lhs = assignment.lhs();
150  const exprt &rhs = assignment.rhs();
151  assign_rec(values, lhs, rhs, ns);
152  }
153  else if(from->is_assume())
154  {
155  two_way_propagate_rec(from->guard, ns);
156  }
157  else if(from->is_goto())
158  {
159  exprt g;
160 
161  if(from->get_target()==to)
162  g = simplify_expr(from->guard, ns);
163  else
164  g = simplify_expr(not_exprt(from->guard), ns);
165 
166  if (g.is_false())
168  else
169  {
170  //TODO: we need to support widening!
171  if (g.is_constant())
172  values.set_to_top();
173  else
174  two_way_propagate_rec(g, ns);
175  }
176  }
177  else if(from->is_dead())
178  {
179  const code_deadt &code_dead=to_code_dead(from->code);
180  values.set_to_top(to_symbol_expr(code_dead.symbol()));
181  }
182  else if(from->is_function_call())
183  {
184  const exprt &function=to_code_function_call(from->code).function();
185 
186  if(function.id()==ID_symbol)
187  {
188  const irep_idt &identifier=to_symbol_expr(function).get_identifier();
189 
190  if(identifier=="__CPROVER_set_must" ||
191  identifier=="__CPROVER_get_must" ||
192  identifier=="__CPROVER_set_may" ||
193  identifier=="__CPROVER_get_may" ||
194  identifier=="__CPROVER_cleanup" ||
195  identifier=="__CPROVER_clear_may" ||
196  identifier=="__CPROVER_clear_must")
197  {
198  }
199  else
200  values.set_to_top();
201  }
202  else
203  values.set_to_top();
204  }
205 
206 #ifdef DEBUG
207  std::cout << "after:\n";
208  output(std::cout, ai, ns);
209 #endif
210 }
211 
212 
215  const exprt &expr,
216  const namespacet &ns)
217 {
218 #ifdef DEBUG
219  std::cout << "two_way_propagate_rec: " << from_expr(ns, "", expr) << '\n';
220 #endif
221  bool change = false;
222 
223  if(expr.id()==ID_and)
224  {
225  // need a fixed point here to get the most out of it
226  do
227  {
228  change = false;
229 
230  forall_operands(it, expr)
231  if(two_way_propagate_rec(*it, ns))
232  change = true;
233  }
234  while(change);
235  }
236  else if(expr.id()==ID_equal)
237  {
238  const exprt &lhs = expr.op0();
239  const exprt &rhs = expr.op1();
240 
241  // two-way propagation
242  valuest copy_values = values;
243  assign_rec(copy_values, lhs, rhs, ns);
244  if(!values.is_constant(rhs) || values.is_constant(lhs))
245  assign_rec(values, rhs, lhs, ns);
246  change = values.meet(copy_values);
247  }
248 
249 #ifdef DEBUG
250  std::cout << "two_way_propagate_rec: " << change << '\n';
251 #endif
252  return change;
253 }
254 
256  valuest &dest,
257  const symbol_exprt &lhs,
258  exprt rhs,
259  const namespacet &ns) const
260 {
261  values.replace_const(rhs);
262  rhs = simplify_expr(rhs, ns);
263  dest.set_to(lhs, rhs);
264 }
265 
271  exprt &condition,
272  const namespacet &ns) const
273 {
274  bool b=values.replace_const.replace(condition);
275  b&=simplify(condition, ns);
276 
277  return b;
278 }
279 
281 {
282  exprt new_expr = concatenate_array_id(expr.op0(),
283  expr.op1(), expr.type());
284 
285  if (replace_const.expr_map.find(to_symbol_expr(new_expr).get_identifier()) ==
286  replace_const.expr_map.end())
287  return false;
288 
289  return true;
290 }
291 
293 {
294  if(expr.id()==ID_side_effect &&
295  to_side_effect_expr(expr).get_statement()==ID_nondet)
296  return false;
297 
298  if(expr.id()==ID_side_effect &&
299  to_side_effect_expr(expr).get_statement()==ID_malloc)
300  return false;
301 
302  if(expr.id()==ID_symbol)
303  if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier()) ==
304  replace_const.expr_map.end())
305  return false;
306 
307  if (expr.id()==ID_index)
308  return is_array_constant(expr);
309 
310  if(expr.id()==ID_address_of)
311  return is_constant_address_of(to_address_of_expr(expr).object());
312 
313  forall_operands(it, expr)
314  if(!is_constant(*it))
315  return false;
316 
317  return true;
318 }
319 
321  const exprt &expr) const
322 {
323  if(expr.id()==ID_index)
324  return is_constant_address_of(to_index_expr(expr).array()) &&
325  is_constant(to_index_expr(expr).index());
326 
327  if(expr.id()==ID_member)
328  return is_constant_address_of(to_member_expr(expr).struct_op());
329 
330  if(expr.id()==ID_dereference)
331  return is_constant(to_dereference_expr(expr).pointer());
332 
333  if(expr.id()==ID_string_constant)
334  return true;
335 
336  return true;
337 }
338 
341 {
342  bool result = false;
343 
344  replace_symbolt::expr_mapt::iterator r_it =
345  replace_const.expr_map.find(id);
346 
347  if(r_it != replace_const.expr_map.end())
348  {
349  assert(!is_bottom);
350  replace_const.expr_map.erase(r_it);
351  result = true;
352  }
353 
354  return result;
355 }
356 
358  std::ostream &out,
359  const namespacet &ns) const
360 {
361  out << "const map:\n";
362 
363  if(is_bottom)
364  out << " bottom\n";
365 
366  for(const auto &replace_pair : replace_const.expr_map)
367  out << ' ' << replace_pair.first << "="
368  << from_expr(ns, "", replace_pair.second) << '\n';
369 }
370 
372  std::ostream &out,
373  const ai_baset &ai,
374  const namespacet &ns) const
375 {
376  values.output(out, ns);
377 }
378 
382 {
383  // nothing to do
384  if(src.is_bottom)
385  return false;
386 
387  // just copy
388  if(is_bottom)
389  {
390  replace_const = src.replace_const;
391  is_bottom = src.is_bottom;
392  return true;
393  }
394 
395  bool changed = false;
396 
397  // set everything to top that is not in src
398  for(replace_symbolt::expr_mapt::const_iterator
399  it=replace_const.expr_map.begin();
400  it!=replace_const.expr_map.end();
401  ) // no it++
402  {
403  const replace_symbolt::expr_mapt::const_iterator
404  b_it=src.replace_const.expr_map.find(it->first);
405 
406  if(b_it==src.replace_const.expr_map.end())
407  {
408  //cannot use set_to_top here
409  replace_const.expr_map.erase(it);
410  changed = true;
411  break;
412  }
413  else
414  {
415  const exprt previous=it->second;
416  replace_const.expr_map[b_it->first]=b_it->second;
417  if (it->second != previous) changed = true;
418 
419  it++;
420  }
421  }
422  return changed;
423 }
424 
428 {
429  if(src.is_bottom || is_bottom)
430  return false;
431 
432  bool changed = false;
433 
434  for(const auto &src_replace_pair : src.replace_const.expr_map)
435  {
436  replace_symbolt::expr_mapt::iterator c_it=
437  replace_const.expr_map.find(src_replace_pair.first);
438 
439  if(c_it!=replace_const.expr_map.end())
440  {
441  if(c_it->second!=src_replace_pair.second)
442  {
443  set_to_bottom();
444  changed=true;
445  break;
446  }
447  }
448  else
449  {
450  set_to(src_replace_pair.first, src_replace_pair.second);
451  changed=true;
452  }
453  }
454 
455  return changed;
456 }
457 
460  const constant_propagator_domaint &other,
461  locationt from,
462  locationt to)
463 {
464  return values.merge(other.values);
465 }
466 
468  goto_functionst &goto_functions,
469  const namespacet &ns)
470 {
471  Forall_goto_functions(f_it, goto_functions)
472  replace(f_it->second, ns);
473 }
474 
476 {
477  if (expr.id()==ID_index)
478  expr = concatenate_array_id(expr.op0(),
479  expr.op1(), expr.type());
480 
481  Forall_operands(it, expr)
482  {
483  if (it->id()==ID_equal)
484  replace_array_symbol(it->op0());
485  else if (it->id()==ID_index)
486  replace_array_symbol(expr.op0());
487  }
488 
489 }
490 
492  goto_functionst::goto_functiont &goto_function,
493  const namespacet &ns)
494 {
495  Forall_goto_program_instructions(it, goto_function.body)
496  {
497  state_mapt::iterator s_it = state_map.find(it);
498 
499  if(s_it == state_map.end())
500  continue;
501 
502  replace_types_rec(s_it->second.values.replace_const, it->code);
503  replace_types_rec(s_it->second.values.replace_const, it->guard);
504 
505  if(it->is_goto() || it->is_assume() || it->is_assert())
506  {
507  replace_array_symbol(it->guard);
508  s_it->second.values.replace_const(it->guard);
509  it->guard = simplify_expr(it->guard, ns);
510  }
511  else if(it->is_assign())
512  {
513  exprt &rhs = to_code_assign(it->code).rhs();
514  s_it->second.values.replace_const(rhs);
515  rhs = simplify_expr(rhs, ns);
516  if (rhs.id()==ID_constant)
517  rhs.add_source_location()=it->code.op0().source_location();
518  }
519  else if(it->is_function_call())
520  {
521  s_it->second.values.replace_const(
522  to_code_function_call(it->code).function());
524 
525  exprt::operandst &args =
526  to_code_function_call(it->code).arguments();
527 
528  for(exprt::operandst::iterator o_it = args.begin();
529  o_it != args.end(); ++o_it)
530  {
531  s_it->second.values.replace_const(*o_it);
532  *o_it = simplify_expr(*o_it, ns);
533  }
534  }
535  else if(it->is_other())
536  {
537  if(it->code.get_statement()==ID_expression)
538  s_it->second.values.replace_const(it->code);
539  }
540  }
541 }
542 
544  const replace_symbolt &replace_const,
545  exprt &expr)
546 {
547  replace_const(expr.type());
548 
549  Forall_operands(it, expr)
550  replace_types_rec(replace_const, *it);
551 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
Boolean negation.
Definition: std_expr.h:2648
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
void assign(valuest &dest, const symbol_exprt &lhs, exprt rhs, const namespacet &ns) const
BigInt mp_integer
Definition: mp_arith.h:19
bool is_array_constant(const exprt &expr) const
exprt & object()
Definition: std_expr.h:2608
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:53
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Simplify the condition given context-sensitive knowledge from the abstract state. ...
bool is_constant_address_of(const exprt &expr) const
exprt & op0()
Definition: expr.h:84
exprt simplify_expr(const exprt &src, const namespacet &ns)
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:260
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
exprt & symbol()
Definition: std_code.h:205
void transform(locationt, locationt, ai_baset &, const namespacet &) final
virtual bool replace(exprt &dest) const
does not replace object in address_of expressions
const irep_idt & get_identifier() const
Definition: std_expr.h:120
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
bool is_false() const
Definition: expr.cpp:140
typet & type()
Definition: expr.h:60
bool meet(const valuest &src)
meet
bool merge(const valuest &src)
join
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1023
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:2748
bool is_constant(const exprt &expr) const
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:2629
argumentst & arguments()
Definition: std_code.h:689
A declaration of a local variable.
Definition: std_code.h:192
exprt & rhs()
Definition: std_code.h:162
exprt & op1()
Definition: expr.h:87
TO_BE_DOCUMENTED.
Definition: namespace.h:62
#define forall_operands(it, expr)
Definition: expr.h:17
goto_function_templatet< goto_programt > goto_functiont
exprt & symbol()
Definition: std_code.h:247
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
bool is_constant() const
Definition: expr.cpp:128
std::vector< exprt > operandst
Definition: expr.h:49
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns)
handles equalities and conjunctions containing equalities
exprt & index()
Definition: std_expr.h:1208
exprt & function()
Definition: std_code.h:677
bool set_to_top(const irep_idt &id)
Do not call this when iterating over replace_const.expr_map!
Definition: ai.h:108
Base class for all expressions.
Definition: expr.h:46
exprt & pointer()
Definition: std_expr.h:2727
const exprt & struct_op() const
Definition: std_expr.h:3270
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
Constant propagation.
void output(std::ostream &, const namespacet &) const
#define Forall_goto_functions(it, functions)
void set_to(const irep_idt &lhs_id, const exprt &rhs_val)
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
A removal of a local variable.
Definition: std_code.h:234
#define Forall_operands(it, expr)
Definition: expr.h:23
source_locationt & add_source_location()
Definition: expr.h:147
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
goto_programt::const_targett locationt
Definition: ai.h:42
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt concatenate_array_id(const exprt &array, const exprt &index, const typet &type)
expr_mapt expr_map
bool merge(const constant_propagator_domaint &, locationt, locationt)
void replace_array_symbol(exprt &expr)
operandst & operands()
Definition: expr.h:70
void replace(goto_functionst::goto_functiont &, const namespacet &)
void assign_rec(valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns)
exprt & array()
Definition: std_expr.h:1198
void output(std::ostream &, const ai_baset &, const namespacet &) const final
Assignment.
Definition: std_code.h:144
const irep_idt & get_statement() const
Definition: std_code.h:1012
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
bool simplify(exprt &expr, const namespacet &ns)