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 #include <util/format_expr.h>
17 #endif
18 
19 #include <util/arith_tools.h>
20 #include <util/base_type.h>
21 #include <util/cprover_prefix.h>
22 #include <util/find_symbols.h>
23 #include <util/ieee_float.h>
24 #include <util/simplify_expr.h>
25 
26 #include <langapi/language_util.h>
27 
28 #include <algorithm>
29 #include <array>
30 
32  valuest &values,
33  const exprt &lhs,
34  const exprt &rhs,
35  const namespacet &ns,
36  const constant_propagator_ait *cp)
37 {
38  if(lhs.id()!=ID_symbol)
39  return;
40 
41  if(cp && !cp->should_track_value(lhs, ns))
42  return;
43 
44  const symbol_exprt &s=to_symbol_expr(lhs);
45 
46  exprt tmp=rhs;
47  partial_evaluate(tmp, ns);
48 
49  if(tmp.is_constant())
50  {
52  base_type_eq(ns.lookup(s).type, tmp.type(), ns),
53  "type of constant to be replaced should match");
54  values.set_to(s, tmp);
55  }
56  else
57  values.set_to_top(s);
58 }
59 
61  const irep_idt &function_from,
62  locationt from,
63  const irep_idt &function_to,
64  locationt to,
65  ai_baset &ai,
66  const namespacet &ns)
67 {
68 #ifdef DEBUG
69  std::cout << "Transform from/to:\n";
70  std::cout << from->location_number << " --> "
71  << to->location_number << '\n';
72 #endif
73 
74 #ifdef DEBUG
75  std::cout << "Before:\n";
76  output(std::cout, ai, ns);
77 #endif
78 
79  // When the domain is used with constant_propagator_ait,
80  // information about dirty variables and config flags are
81  // available. Otherwise, the below will be null and we use default
82  // values
83  const constant_propagator_ait *cp=
84  dynamic_cast<constant_propagator_ait *>(&ai);
85  bool have_dirty=(cp!=nullptr);
86 
87  // Transform on a domain that is bottom is possible
88  // if a branch is impossible the target can still wind
89  // up on the work list.
90  if(values.is_bottom)
91  return;
92 
93  if(from->is_decl())
94  {
95  const code_declt &code_decl=to_code_decl(from->code);
96  const symbol_exprt &symbol = code_decl.symbol();
97  values.set_to_top(symbol);
98  }
99  else if(from->is_assign())
100  {
101  const code_assignt &assignment=to_code_assign(from->code);
102  const exprt &lhs=assignment.lhs();
103  const exprt &rhs=assignment.rhs();
104  assign_rec(values, lhs, rhs, ns, cp);
105  }
106  else if(from->is_assume())
107  {
108  two_way_propagate_rec(from->guard, ns, cp);
109  }
110  else if(from->is_goto())
111  {
112  exprt g;
113 
114  // Comparing iterators is safe as the target must be within the same list
115  // of instructions because this is a GOTO.
116  if(from->get_target()==to)
117  g = from->guard;
118  else
119  g = not_exprt(from->guard);
120  partial_evaluate(g, ns);
121  if(g.is_false())
123  else
124  {
125  two_way_propagate_rec(g, ns, cp);
126  // If two way propagate is enabled then it may be possible to detect
127  // that the branch condition is infeasible and thus the domain should
128  // be set to bottom. Without it the domain will only be set to bottom
129  // if the guard expression is trivially (i.e. without context) false.
131  "Without two-way propagation this should be impossible.");
132  }
133  }
134  else if(from->is_dead())
135  {
136  const code_deadt &code_dead=to_code_dead(from->code);
137  values.set_to_top(code_dead.symbol());
138  }
139  else if(from->is_function_call())
140  {
141  const code_function_callt &function_call=to_code_function_call(from->code);
142  const exprt &function=function_call.function();
143 
144  if(function.id()==ID_symbol)
145  {
146  // called function identifier
147  const symbol_exprt &symbol_expr=to_symbol_expr(function);
148  const irep_idt id=symbol_expr.get_identifier();
149 
150  // Functions with no body
151  if(function_from == function_to)
152  {
153  if(id==CPROVER_PREFIX "set_must" ||
154  id==CPROVER_PREFIX "get_must" ||
155  id==CPROVER_PREFIX "set_may" ||
156  id==CPROVER_PREFIX "get_may" ||
157  id==CPROVER_PREFIX "cleanup" ||
158  id==CPROVER_PREFIX "clear_may" ||
159  id==CPROVER_PREFIX "clear_must")
160  {
161  // no effect on constants
162  }
163  else
164  {
165  if(have_dirty)
166  values.set_dirty_to_top(cp->dirty, ns);
167  else
168  values.set_to_top();
169  }
170  }
171  else
172  {
173  // we have an actual call
174 
175  // parameters of called function
176  const symbolt &symbol=ns.lookup(id);
177  const code_typet &code_type=to_code_type(symbol.type);
178  const code_typet::parameterst &parameters=code_type.parameters();
179 
180  const code_function_callt::argumentst &arguments=
181  function_call.arguments();
182 
183  code_typet::parameterst::const_iterator p_it=parameters.begin();
184  for(const auto &arg : arguments)
185  {
186  if(p_it==parameters.end())
187  break;
188 
189  const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
190  assign_rec(values, parameter_expr, arg, ns, cp);
191 
192  ++p_it;
193  }
194  }
195  }
196  else
197  {
198  // unresolved call
199  INVARIANT(
200  function_from == function_to,
201  "Unresolved call can only be approximated if a skip");
202 
203  if(have_dirty)
204  values.set_dirty_to_top(cp->dirty, ns);
205  else
206  values.set_to_top();
207  }
208  }
209  else if(from->is_end_function())
210  {
211  // erase parameters
212 
213  const irep_idt id = function_from;
214  const symbolt &symbol=ns.lookup(id);
215 
216  const code_typet &type=to_code_type(symbol.type);
217 
218  for(const auto &param : type.parameters())
219  values.set_to_top(symbol_exprt(param.get_identifier(), param.type()));
220  }
221 
222  INVARIANT(from->is_goto() || !values.is_bottom,
223  "Transform only sets bottom by using branch conditions");
224 
225 #ifdef DEBUG
226  std::cout << "After:\n";
227  output(std::cout, ai, ns);
228 #endif
229 }
230 
231 
234  const exprt &expr,
235  const namespacet &,
236  const constant_propagator_ait *cp)
237 {
238 #ifdef DEBUG
239  std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
240 #else
241  (void)expr; // unused parameter
242 #endif
243 
244  bool change=false;
245 
246  // this seems to be buggy at present
247 #if 0
248  if(expr.id()==ID_and)
249  {
250  // need a fixed point here to get the most out of it
251  do
252  {
253  change = false;
254 
255  forall_operands(it, expr)
256  if(two_way_propagate_rec(*it, ns, cp))
257  change=true;
258  }
259  while(change);
260  }
261  else if(expr.id()==ID_equal)
262  {
263  const exprt &lhs=expr.op0();
264  const exprt &rhs=expr.op1();
265 
266  // two-way propagation
267  valuest copy_values=values;
268  assign_rec(copy_values, lhs, rhs, ns);
269  if(!values.is_constant(rhs) || values.is_constant(lhs))
270  assign_rec(values, rhs, lhs, ns);
271  change = values.meet(copy_values, ns);
272  }
273 #else
274  (void)cp; // unused parameter
275 #endif
276 
277 #ifdef DEBUG
278  std::cout << "two_way_propagate_rec: " << change << '\n';
279 #endif
280 
281  return change;
282 }
283 
289  exprt &condition,
290  const namespacet &ns) const
291 {
292  return partial_evaluate(condition, ns);
293 }
294 
295 
297 {
298  if(expr.id()==ID_side_effect &&
299  to_side_effect_expr(expr).get_statement()==ID_nondet)
300  return false;
301 
302  if(expr.id()==ID_side_effect &&
303  to_side_effect_expr(expr).get_statement()==ID_allocate)
304  return false;
305 
306  if(expr.id()==ID_symbol)
307  if(!replace_const.replaces_symbol(to_symbol_expr(expr).get_identifier()))
308  return false;
309 
310  if(expr.id()==ID_index)
311  return false;
312 
313  if(expr.id()==ID_address_of)
315 
316  forall_operands(it, expr)
317  if(!is_constant(*it))
318  return false;
319 
320  return true;
321 }
322 
324  const exprt &expr) const
325 {
326  if(expr.id()==ID_index)
327  return is_constant_address_of(to_index_expr(expr).array()) &&
328  is_constant(to_index_expr(expr).index());
329 
330  if(expr.id()==ID_member)
331  return is_constant_address_of(to_member_expr(expr).struct_op());
332 
333  if(expr.id()==ID_dereference)
334  return is_constant(to_dereference_expr(expr).pointer());
335 
336  if(expr.id()==ID_string_constant)
337  return true;
338 
339  return true;
340 }
341 
344  const symbol_exprt &symbol_expr)
345 {
346  const auto n_erased = replace_const.erase(symbol_expr.get_identifier());
347 
348  INVARIANT(n_erased==0 || !is_bottom, "bottom should have no elements at all");
349 
350  return n_erased>0;
351 }
352 
353 
355  const dirtyt &dirty,
356  const namespacet &ns)
357 {
359  expr_mapt &expr_map = replace_const.get_expr_map();
360 
361  for(expr_mapt::iterator it=expr_map.begin();
362  it!=expr_map.end();)
363  {
364  const irep_idt id=it->first;
365 
366  const symbolt &symbol=ns.lookup(id);
367 
368  if((!symbol.is_procedure_local() || dirty(id)) &&
369  !symbol.type.get_bool(ID_C_constant))
370  {
371  it = replace_const.erase(it);
372  }
373  else
374  it++;
375  }
376 }
377 
379  std::ostream &out,
380  const namespacet &ns) const
381 {
382  out << "const map:\n";
383 
384  if(is_bottom)
385  {
386  out << " bottom\n";
388  "If the domain is bottom, the map must be empty");
389  return;
390  }
391 
392  INVARIANT(!is_bottom, "Have handled bottom");
393  if(is_empty())
394  {
395  out << "top\n";
396  return;
397  }
398 
399  for(const auto &p : replace_const.get_expr_map())
400  {
401  out << ' ' << p.first << "=" << from_expr(ns, p.first, p.second) << '\n';
402  }
403 }
404 
406  std::ostream &out,
407  const ai_baset &,
408  const namespacet &ns) const
409 {
410  values.output(out, ns);
411 }
412 
416 {
417  // nothing to do
418  if(src.is_bottom)
419  return false;
420 
421  // just copy
422  if(is_bottom)
423  {
424  PRECONDITION(!src.is_bottom);
425  replace_const=src.replace_const; // copy
426  is_bottom=false;
427  return true;
428  }
429 
430  INVARIANT(!is_bottom && !src.is_bottom, "Case handled");
431 
432  bool changed=false;
433 
434  // handle top
435  if(src.is_empty())
436  {
437  // change if it was not top
438  changed = !is_empty();
439 
440  set_to_top();
441 
442  return changed;
443  }
444 
445  replace_symbolt::expr_mapt &expr_map = replace_const.get_expr_map();
446  const replace_symbolt::expr_mapt &src_expr_map =
448 
449  // remove those that are
450  // - different in src
451  // - do not exist in src
452  for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
453  it!=expr_map.end();)
454  {
455  const irep_idt id=it->first;
456  const exprt &expr=it->second;
457 
458  replace_symbolt::expr_mapt::const_iterator s_it;
459  s_it=src_expr_map.find(id);
460 
461  if(s_it!=src_expr_map.end())
462  {
463  // check value
464  const exprt &src_expr=s_it->second;
465 
466  if(expr!=src_expr)
467  {
468  it = replace_const.erase(it);
469  changed=true;
470  }
471  else
472  it++;
473  }
474  else
475  {
476  it = replace_const.erase(it);
477  changed=true;
478  }
479  }
480 
481  return changed;
482 }
483 
487  const valuest &src,
488  const namespacet &ns)
489 {
490  if(src.is_bottom || is_bottom)
491  return false;
492 
493  bool changed=false;
494 
495  for(const auto &m : src.replace_const.get_expr_map())
496  {
497  replace_symbolt::expr_mapt::const_iterator c_it =
498  replace_const.get_expr_map().find(m.first);
499 
500  if(c_it != replace_const.get_expr_map().end())
501  {
502  if(c_it->second!=m.second)
503  {
504  set_to_bottom();
505  changed=true;
506  break;
507  }
508  }
509  else
510  {
511  const typet &m_id_type = ns.lookup(m.first).type;
513  base_type_eq(m_id_type, m.second.type(), ns),
514  "type of constant to be stored should match");
515  set_to(symbol_exprt(m.first, m_id_type), m.second);
516  changed=true;
517  }
518  }
519 
520  return changed;
521 }
522 
525  const constant_propagator_domaint &other,
526  locationt,
527  locationt)
528 {
529  return values.merge(other.values);
530 }
531 
538  exprt &expr,
539  const namespacet &ns) const
540 {
541  // if the current rounding mode is top we can
542  // still get a non-top result by trying all rounding
543  // modes and checking if the results are all the same
545  {
547  }
548  return replace_constants_and_simplify(expr, ns);
549 }
550 
556  exprt &expr,
557  const namespacet &ns) const
558 { // NOLINTNEXTLINE (whitespace/braces)
559  auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
560  // NOLINTNEXTLINE (whitespace/braces)
564  // NOLINTNEXTLINE (whitespace/braces)
566  exprt first_result;
567  for(std::size_t i = 0; i < rounding_modes.size(); ++i)
568  {
569  constant_propagator_domaint child(*this);
570  child.values.set_to(
572  from_integer(rounding_modes[i], integer_typet()));
573  exprt result = expr;
574  if(child.replace_constants_and_simplify(result, ns))
575  {
576  return true;
577  }
578  else if(i == 0)
579  {
580  first_result = result;
581  }
582  else if(result != first_result)
583  {
584  return true;
585  }
586  }
587  expr = first_result;
588  return false;
589 }
590 
592  exprt &expr,
593  const namespacet &ns) const
594 {
595  bool did_not_change_anything = values.replace_const.replace(expr);
596  did_not_change_anything &= simplify(expr, ns);
597  return did_not_change_anything;
598 }
599 
601  goto_functionst &goto_functions,
602  const namespacet &ns)
603 {
604  Forall_goto_functions(f_it, goto_functions)
605  replace(f_it->second, ns);
606 }
607 
608 
610  goto_functionst::goto_functiont &goto_function,
611  const namespacet &ns)
612 {
613  Forall_goto_program_instructions(it, goto_function.body)
614  {
615  // Works because this is a location (but not history) sensitive domain
616  const constant_propagator_domaint &d = (*this)[it];
617 
618  if(d.is_bottom())
619  continue;
620 
621  replace_types_rec(d.values.replace_const, it->code);
622  replace_types_rec(d.values.replace_const, it->guard);
623 
624  if(it->is_goto() || it->is_assume() || it->is_assert())
625  {
626  d.partial_evaluate(it->guard, ns);
627  }
628  else if(it->is_assign())
629  {
630  exprt &rhs=to_code_assign(it->code).rhs();
631  d.partial_evaluate(rhs, ns);
632 
633  if(rhs.id()==ID_constant)
634  rhs.add_source_location() =
635  to_code_assign(it->code).lhs().source_location();
636  }
637  else if(it->is_function_call())
638  {
639  exprt &function = to_code_function_call(it->code).function();
640  d.partial_evaluate(function, ns);
641 
642  exprt::operandst &args=
643  to_code_function_call(it->code).arguments();
644 
645  for(auto &arg : args)
646  {
647  d.partial_evaluate(arg, ns);
648  }
649  }
650  else if(it->is_other())
651  {
652  if(it->code.get_statement()==ID_expression)
653  {
654  d.partial_evaluate(it->code, ns);
655  }
656  }
657  }
658 }
659 
661  const replace_symbolt &replace_const,
662  exprt &expr)
663 {
664  replace_const(expr.type());
665 
666  Forall_operands(it, expr)
667  replace_types_rec(replace_const, *it);
668 }
The type of an expression, extends irept.
Definition: type.h:27
Boolean negation.
Definition: std_expr.h:3308
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:399
Base type of functions.
Definition: std_types.h:751
exprt & object()
Definition: std_expr.h:3265
void assign_rec(valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns, const constant_propagator_ait *cp)
bool is_constant_address_of(const exprt &expr) const
exprt & op0()
Definition: expr.h:84
#define CPROVER_PREFIX
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:473
bool replace_constants_and_simplify(exprt &expr, const namespacet &ns) const
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
const irep_idt & get_identifier() const
Definition: std_expr.h:176
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void set_to(const symbol_exprt &lhs, const exprt &rhs)
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
std::vector< parametert > parameterst
Definition: std_types.h:754
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
typet & type()
Return the type of the expression.
Definition: expr.h:68
exprt::operandst argumentst
Definition: std_code.h:1055
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
Symbol table entry.
Definition: symbol.h:27
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
bool merge(const valuest &src)
join
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3397
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1620
bool is_constant(const exprt &expr) const
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:269
argumentst & arguments()
Definition: std_code.h:1109
Replace expression or type symbols by an expression or type, respectively.
A codet representing the declaration of a local variable.
Definition: std_code.h:352
exprt & rhs()
Definition: std_code.h:274
bool partial_evaluate(exprt &expr, const namespacet &ns) const
Attempt to evaluate expression using domain knowledge This function changes the expression that is pa...
should_track_valuet should_track_value
exprt & op1()
Definition: expr.h:87
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const final override
Simplify the condition given context-sensitive knowledge from the abstract state. ...
virtual void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai_base, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
codet representation of a function call statement.
Definition: std_code.h:1036
#define forall_operands(it, expr)
Definition: expr.h:20
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
std::vector< exprt > operandst
Definition: expr.h:57
std::unordered_map< irep_idt, exprt > expr_mapt
virtual bool is_bottom() const final override
bool partial_evaluate_with_all_rounding_modes(exprt &expr, const namespacet &ns) const
Attempt to evaluate an expression in all rounding modes.
Unbounded, signed integers (mathematical integers, not bitvectors)
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
typet type
Type of symbol.
Definition: symbol.h:31
symbol_exprt & symbol()
Definition: std_code.h:432
void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns)
address_of_aware_replace_symbolt replace_const
bool replaces_symbol(const irep_idt &id) const
exprt & index()
Definition: std_expr.h:1631
symbol_exprt & symbol()
Definition: std_code.h:360
const char ID_cprover_rounding_mode_str[]
Definition: ieee_float.h:23
exprt & function()
Definition: std_code.h:1099
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:54
exprt & pointer()
Definition: std_expr.h:3380
const exprt & struct_op() const
Definition: std_expr.h:3931
const parameterst & parameters() const
Definition: std_types.h:893
Constant propagation.
Definition: dirty.h:23
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:228
bool is_empty(const std::string &s)
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:424
#define Forall_operands(it, expr)
Definition: expr.h:26
source_locationt & add_source_location()
Definition: expr.h:233
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
const expr_mapt & get_expr_map() const
goto_programt::const_targett locationt
Definition: ai_domain.h:40
bool is_procedure_local() const
Definition: symbol.h:100
Expression to hold a symbol (variable)
Definition: std_expr.h:143
Base Type Computation.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void replace(goto_functionst::goto_functiont &, const namespacet &)
bool replace(exprt &dest) const override
exprt & array()
Definition: std_expr.h:1621
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
A codet representing an assignment in the program.
Definition: std_code.h:256
void output(std::ostream &out, const namespacet &ns) const
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
const irep_idt & get_statement() const
Definition: std_code.h:1586
bool meet(const valuest &src, const namespacet &ns)
meet
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
bool simplify(exprt &expr, const namespacet &ns)
static format_containert< T > format(const T &o)
Definition: format.h:35
bool merge(const constant_propagator_domaint &other, locationt from, locationt to)