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/ieee_float.h>
20 #include <util/find_symbols.h>
21 #include <util/arith_tools.h>
22 #include <util/simplify_expr.h>
23 #include <util/cprover_prefix.h>
24 
25 #include <langapi/language_util.h>
26 
27 #include <algorithm>
28 #include <array>
29 
31  valuest &values,
32  const exprt &lhs,
33  const exprt &rhs,
34  const namespacet &ns)
35 {
36  if(lhs.id()!=ID_symbol)
37  return;
38 
39  const symbol_exprt &s=to_symbol_expr(lhs);
40 
41  exprt tmp=rhs;
42  partial_evaluate(tmp, ns);
43 
44  if(tmp.is_constant())
45  values.set_to(s, tmp);
46  else
47  values.set_to_top(s);
48 }
49 
51  locationt from,
52  locationt to,
53  ai_baset &ai,
54  const namespacet &ns)
55 {
56 #ifdef DEBUG
57  std::cout << "Transform from/to:\n";
58  std::cout << from->location_number << " --> "
59  << to->location_number << '\n';
60 #endif
61 
62 #ifdef DEBUG
63  std::cout << "Before:\n";
64  output(std::cout, ai, ns);
65 #endif
66 
67  // When the domain is used with constant_propagator_ait,
68  // information about dirty variables and config flags are
69  // available. Otherwise, the below will be null and we use default
70  // values
71  const constant_propagator_ait *cp=
72  dynamic_cast<constant_propagator_ait *>(&ai);
73  bool have_dirty=(cp!=nullptr);
74 
75  // Transform on a domain that is bottom is possible
76  // if a branch is impossible the target can still wind
77  // up on the work list.
78  if(values.is_bottom)
79  return;
80 
81  if(from->is_decl())
82  {
83  const code_declt &code_decl=to_code_decl(from->code);
84  const symbol_exprt &symbol=to_symbol_expr(code_decl.symbol());
85  values.set_to_top(symbol);
86  }
87  else if(from->is_assign())
88  {
89  const code_assignt &assignment=to_code_assign(from->code);
90  const exprt &lhs=assignment.lhs();
91  const exprt &rhs=assignment.rhs();
92  assign_rec(values, lhs, rhs, ns);
93  }
94  else if(from->is_assume())
95  {
96  two_way_propagate_rec(from->guard, ns);
97  }
98  else if(from->is_goto())
99  {
100  exprt g;
101 
102  // Comparing iterators is safe as the target must be within the same list
103  // of instructions because this is a GOTO.
104  if(from->get_target()==to)
105  g = from->guard;
106  else
107  g = not_exprt(from->guard);
108  partial_evaluate(g, ns);
109  if(g.is_false())
111  else
112  {
113  two_way_propagate_rec(g, ns);
114  // If two way propagate is enabled then it may be possible to detect
115  // that the branch condition is infeasible and thus the domain should
116  // be set to bottom. Without it the domain will only be set to bottom
117  // if the guard expression is trivially (i.e. without context) false.
119  "Without two-way propagation this should be impossible.");
120  }
121  }
122  else if(from->is_dead())
123  {
124  const code_deadt &code_dead=to_code_dead(from->code);
125  values.set_to_top(to_symbol_expr(code_dead.symbol()));
126  }
127  else if(from->is_function_call())
128  {
129  const code_function_callt &function_call=to_code_function_call(from->code);
130  const exprt &function=function_call.function();
131 
132  if(function.id()==ID_symbol)
133  {
134  // called function identifier
135  const symbol_exprt &symbol_expr=to_symbol_expr(function);
136  const irep_idt id=symbol_expr.get_identifier();
137 
138  // Functions with no body
139  if(from->function == to->function)
140  {
141  if(id==CPROVER_PREFIX "set_must" ||
142  id==CPROVER_PREFIX "get_must" ||
143  id==CPROVER_PREFIX "set_may" ||
144  id==CPROVER_PREFIX "get_may" ||
145  id==CPROVER_PREFIX "cleanup" ||
146  id==CPROVER_PREFIX "clear_may" ||
147  id==CPROVER_PREFIX "clear_must")
148  {
149  // no effect on constants
150  }
151  else
152  {
153  if(have_dirty)
154  values.set_dirty_to_top(cp->dirty, ns);
155  else
156  values.set_to_top();
157  }
158  }
159  else
160  {
161  // we have an actual call
162 
163  // parameters of called function
164  const symbolt &symbol=ns.lookup(id);
165  const code_typet &code_type=to_code_type(symbol.type);
166  const code_typet::parameterst &parameters=code_type.parameters();
167 
168  const code_function_callt::argumentst &arguments=
169  function_call.arguments();
170 
171  code_typet::parameterst::const_iterator p_it=parameters.begin();
172  for(const auto &arg : arguments)
173  {
174  if(p_it==parameters.end())
175  break;
176 
177  const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
178  assign_rec(values, parameter_expr, arg, ns);
179 
180  ++p_it;
181  }
182  }
183  }
184  else
185  {
186  // unresolved call
187  INVARIANT(
188  from->function == to->function,
189  "Unresolved call can only be approximated if a skip");
190 
191  if(have_dirty)
192  values.set_dirty_to_top(cp->dirty, ns);
193  else
194  values.set_to_top();
195  }
196  }
197  else if(from->is_end_function())
198  {
199  // erase parameters
200 
201  const irep_idt id=from->function;
202  const symbolt &symbol=ns.lookup(id);
203 
204  const code_typet &type=to_code_type(symbol.type);
205 
206  for(const auto &param : type.parameters())
207  values.set_to_top(param.get_identifier());
208  }
209 
210  INVARIANT(from->is_goto() || !values.is_bottom,
211  "Transform only sets bottom by using branch conditions");
212 
213 #ifdef DEBUG
214  std::cout << "After:\n";
215  output(std::cout, ai, ns);
216 #endif
217 }
218 
219 
222  const exprt &expr,
223  const namespacet &ns)
224 {
225 #ifdef DEBUG
226  std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
227 #endif
228 
229  bool change=false;
230 
231  // this seems to be buggy at present
232 #if 0
233  if(expr.id()==ID_and)
234  {
235  // need a fixed point here to get the most out of it
236  do
237  {
238  change = false;
239 
240  forall_operands(it, expr)
241  if(two_way_propagate_rec(*it, ns))
242  change=true;
243  }
244  while(change);
245  }
246  else if(expr.id()==ID_equal)
247  {
248  const exprt &lhs=expr.op0();
249  const exprt &rhs=expr.op1();
250 
251  // two-way propagation
252  valuest copy_values=values;
253  assign_rec(copy_values, lhs, rhs, ns);
254  if(!values.is_constant(rhs) || values.is_constant(lhs))
255  assign_rec(values, rhs, lhs, ns);
256  change=values.meet(copy_values);
257  }
258 #endif
259 
260 #ifdef DEBUG
261  std::cout << "two_way_propagate_rec: " << change << '\n';
262 #endif
263 
264  return change;
265 }
266 
272  exprt &condition,
273  const namespacet &ns) const
274 {
275  return partial_evaluate(condition, ns);
276 }
277 
278 
280 {
281  if(expr.id()==ID_side_effect &&
282  to_side_effect_expr(expr).get_statement()==ID_nondet)
283  return false;
284 
285  if(expr.id()==ID_side_effect &&
286  to_side_effect_expr(expr).get_statement()==ID_allocate)
287  return false;
288 
289  if(expr.id()==ID_symbol)
290  if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier())==
291  replace_const.expr_map.end())
292  return false;
293 
294  if(expr.id()==ID_index)
295  return false;
296 
297  if(expr.id()==ID_address_of)
299 
300  forall_operands(it, expr)
301  if(!is_constant(*it))
302  return false;
303 
304  return true;
305 }
306 
308  const exprt &expr) const
309 {
310  if(expr.id()==ID_index)
311  return is_constant_address_of(to_index_expr(expr).array()) &&
312  is_constant(to_index_expr(expr).index());
313 
314  if(expr.id()==ID_member)
315  return is_constant_address_of(to_member_expr(expr).struct_op());
316 
317  if(expr.id()==ID_dereference)
318  return is_constant(to_dereference_expr(expr).pointer());
319 
320  if(expr.id()==ID_string_constant)
321  return true;
322 
323  return true;
324 }
325 
328 {
330  replace_const.expr_map.erase(id);
331 
332  INVARIANT(n_erased==0 || !is_bottom, "bottom should have no elements at all");
333 
334  return n_erased>0;
335 }
336 
337 
339  const dirtyt &dirty,
340  const namespacet &ns)
341 {
343  expr_mapt &expr_map=replace_const.expr_map;
344 
345  for(expr_mapt::iterator it=expr_map.begin();
346  it!=expr_map.end();)
347  {
348  const irep_idt id=it->first;
349 
350  const symbolt &symbol=ns.lookup(id);
351 
352  if((!symbol.is_procedure_local() || dirty(id)) &&
353  !symbol.type.get_bool(ID_C_constant))
354  it=expr_map.erase(it);
355  else
356  it++;
357  }
358 }
359 
361  std::ostream &out,
362  const namespacet &ns) const
363 {
364  out << "const map:\n";
365 
366  if(is_bottom)
367  {
368  out << " bottom\n";
369  DATA_INVARIANT(replace_const.expr_map.empty(),
370  "If the domain is bottom, the map must be empty");
371  return;
372  }
373 
374  INVARIANT(!is_bottom, "Have handled bottom");
375  if(replace_const.expr_map.empty())
376  {
377  out << "top\n";
378  return;
379  }
380 
381  for(const auto &p : replace_const.expr_map)
382  {
383  out << ' ' << p.first << "=" << from_expr(ns, p.first, p.second) << '\n';
384  }
385 }
386 
388  std::ostream &out,
389  const ai_baset &ai,
390  const namespacet &ns) const
391 {
392  values.output(out, ns);
393 }
394 
398 {
399  // nothing to do
400  if(src.is_bottom)
401  return false;
402 
403  // just copy
404  if(is_bottom)
405  {
406  PRECONDITION(!src.is_bottom);
407  replace_const=src.replace_const; // copy
408  is_bottom=false;
409  return true;
410  }
411 
412  INVARIANT(!is_bottom && !src.is_bottom, "Case handled");
413 
414  bool changed=false;
415 
416  replace_symbolt::expr_mapt &expr_map=replace_const.expr_map;
417  const replace_symbolt::expr_mapt &src_expr_map=src.replace_const.expr_map;
418 
419  // handle top
420  if(src_expr_map.empty())
421  {
422  // change if it was not top
423  changed=!expr_map.empty();
424 
425  set_to_top();
426 
427  return changed;
428  }
429 
430  // remove those that are
431  // - different in src
432  // - do not exist in src
433  for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
434  it!=expr_map.end();)
435  {
436  const irep_idt id=it->first;
437  const exprt &expr=it->second;
438 
439  replace_symbolt::expr_mapt::const_iterator s_it;
440  s_it=src_expr_map.find(id);
441 
442  if(s_it!=src_expr_map.end())
443  {
444  // check value
445  const exprt &src_expr=s_it->second;
446 
447  if(expr!=src_expr)
448  {
449  it=expr_map.erase(it);
450  changed=true;
451  }
452  else
453  it++;
454  }
455  else
456  {
457  it=expr_map.erase(it);
458  changed=true;
459  }
460  }
461 
462  return changed;
463 }
464 
468 {
469  if(src.is_bottom || is_bottom)
470  return false;
471 
472  bool changed=false;
473 
474  for(const auto &m : src.replace_const.expr_map)
475  {
476  replace_symbolt::expr_mapt::iterator
477  c_it=replace_const.expr_map.find(m.first);
478 
479  if(c_it!=replace_const.expr_map.end())
480  {
481  if(c_it->second!=m.second)
482  {
483  set_to_bottom();
484  changed=true;
485  break;
486  }
487  }
488  else
489  {
490  set_to(m.first, m.second);
491  changed=true;
492  }
493  }
494 
495  return changed;
496 }
497 
500  const constant_propagator_domaint &other,
501  locationt from,
502  locationt to)
503 {
504  return values.merge(other.values);
505 }
506 
513  exprt &expr,
514  const namespacet &ns) const
515 {
516  // if the current rounding mode is top we can
517  // still get a non-top result by trying all rounding
518  // modes and checking if the results are all the same
520  {
522  }
523  return replace_constants_and_simplify(expr, ns);
524 }
525 
531  exprt &expr,
532  const namespacet &ns) const
533 { // NOLINTNEXTLINE (whitespace/braces)
534  auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
535  // NOLINTNEXTLINE (whitespace/braces)
539  // NOLINTNEXTLINE (whitespace/braces)
541  exprt first_result;
542  for(std::size_t i = 0; i < rounding_modes.size(); ++i)
543  {
544  constant_propagator_domaint child(*this);
545  child.values.set_to(
547  from_integer(rounding_modes[i], integer_typet()));
548  exprt result = expr;
549  if(child.replace_constants_and_simplify(result, ns))
550  {
551  return true;
552  }
553  else if(i == 0)
554  {
555  first_result = result;
556  }
557  else if(result != first_result)
558  {
559  return true;
560  }
561  }
562  expr = first_result;
563  return false;
564 }
565 
567  exprt &expr,
568  const namespacet &ns) const
569 {
570  bool did_not_change_anything = values.replace_const.replace(expr);
571  did_not_change_anything &= simplify(expr, ns);
572  return did_not_change_anything;
573 }
574 
576  goto_functionst &goto_functions,
577  const namespacet &ns)
578 {
579  Forall_goto_functions(f_it, goto_functions)
580  replace(f_it->second, ns);
581 }
582 
583 
585  goto_functionst::goto_functiont &goto_function,
586  const namespacet &ns)
587 {
588  Forall_goto_program_instructions(it, goto_function.body)
589  {
590  state_mapt::iterator s_it=state_map.find(it);
591 
592  if(s_it==state_map.end())
593  continue;
594 
595  replace_types_rec(s_it->second.values.replace_const, it->code);
596  replace_types_rec(s_it->second.values.replace_const, it->guard);
597 
598  if(it->is_goto() || it->is_assume() || it->is_assert())
599  {
600  s_it->second.partial_evaluate(it->guard, ns);
601  }
602  else if(it->is_assign())
603  {
604  exprt &rhs=to_code_assign(it->code).rhs();
605  s_it->second.partial_evaluate(rhs, ns);
606  if(rhs.id()==ID_constant)
607  rhs.add_source_location()=it->code.op0().source_location();
608  }
609  else if(it->is_function_call())
610  {
611  exprt &function = to_code_function_call(it->code).function();
612  s_it->second.partial_evaluate(function, ns);
613 
614  exprt::operandst &args=
615  to_code_function_call(it->code).arguments();
616 
617  for(auto &arg : args)
618  {
619  s_it->second.partial_evaluate(arg, ns);
620  }
621  }
622  else if(it->is_other())
623  {
624  if(it->code.get_statement()==ID_expression)
625  {
626  s_it->second.partial_evaluate(it->code, ns);
627  }
628  }
629  }
630 }
631 
633  const replace_symbolt &replace_const,
634  exprt &expr)
635 {
636  replace_const(expr.type());
637 
638  Forall_operands(it, expr)
639  replace_types_rec(replace_const, *it);
640 }
Boolean negation.
Definition: std_expr.h:3230
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:289
Base type of functions.
Definition: std_types.h:764
exprt & object()
Definition: std_expr.h:3180
virtual void transform(locationt from, locationt to, ai_baset &ai_base, const namespacet &ns) final override
bool is_constant_address_of(const exprt &expr) const
exprt & op0()
Definition: expr.h:72
#define CPROVER_PREFIX
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:341
bool replace_constants_and_simplify(exprt &expr, const namespacet &ns) const
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
exprt & symbol()
Definition: std_code.h:266
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
const irep_idt & get_identifier() const
Definition: std_expr.h:128
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool is_false() const
Definition: expr.cpp:131
std::vector< parametert > parameterst
Definition: std_types.h:767
typet & type()
Definition: expr.h:56
exprt::operandst argumentst
Definition: std_code.h:858
unsignedbv_typet size_type()
Definition: c_types.cpp:58
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:3201
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
bool meet(const valuest &src)
meet
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
bool merge(const valuest &src)
join
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3328
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1287
bool is_constant(const exprt &expr) const
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
argumentst & arguments()
Definition: std_code.h:860
A declaration of a local variable.
Definition: std_code.h:253
exprt & rhs()
Definition: std_code.h:213
bool partial_evaluate(exprt &expr, const namespacet &ns) const
Attempt to evaluate expression using domain knowledge This function changes the expression that is pa...
exprt & op1()
Definition: expr.h:75
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const final override
Simplify the condition given context-sensitive knowledge from the abstract state. ...
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
A function call.
Definition: std_code.h:828
#define forall_operands(it, expr)
Definition: expr.h:17
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
exprt & symbol()
Definition: std_code.h:318
bool is_constant() const
Definition: expr.cpp:119
std::vector< exprt > operandst
Definition: expr.h:45
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.
Definition: std_types.h:70
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns)
handles equalities and conjunctions containing equalities
typet type
Type of symbol.
Definition: symbol.h:34
void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns)
virtual bool replace(exprt &dest, const bool replace_with_const=true) const
Replaces a symbol with a constant If you are replacing symbols with constants in an l-value...
exprt & index()
Definition: std_expr.h:1496
const char ID_cprover_rounding_mode_str[]
Definition: ieee_float.h:23
exprt & function()
Definition: std_code.h:848
Definition: ai.h:128
Base class for all expressions.
Definition: expr.h:42
exprt & pointer()
Definition: std_expr.h:3307
const exprt & struct_op() const
Definition: std_expr.h:3911
const parameterst & parameters() const
Definition: std_types.h:905
Constant propagation.
Definition: dirty.h:23
#define Forall_goto_functions(it, functions)
A removal of a local variable.
Definition: std_code.h:305
#define Forall_operands(it, expr)
Definition: expr.h:23
source_locationt & add_source_location()
Definition: expr.h:130
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
goto_programt::const_targett locationt
Definition: ai.h:44
bool is_procedure_local() const
Definition: symbol.h:101
Expression to hold a symbol (variable)
Definition: std_expr.h:90
void set_to(const irep_idt &lhs, const exprt &rhs)
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
expr_mapt expr_map
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
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:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
Assignment.
Definition: std_code.h:195
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:1253
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
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)