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  locationt from,
62  locationt to,
63  ai_baset &ai,
64  const namespacet &ns)
65 {
66 #ifdef DEBUG
67  std::cout << "Transform from/to:\n";
68  std::cout << from->location_number << " --> "
69  << to->location_number << '\n';
70 #endif
71 
72 #ifdef DEBUG
73  std::cout << "Before:\n";
74  output(std::cout, ai, ns);
75 #endif
76 
77  // When the domain is used with constant_propagator_ait,
78  // information about dirty variables and config flags are
79  // available. Otherwise, the below will be null and we use default
80  // values
81  const constant_propagator_ait *cp=
82  dynamic_cast<constant_propagator_ait *>(&ai);
83  bool have_dirty=(cp!=nullptr);
84 
85  // Transform on a domain that is bottom is possible
86  // if a branch is impossible the target can still wind
87  // up on the work list.
88  if(values.is_bottom)
89  return;
90 
91  if(from->is_decl())
92  {
93  const code_declt &code_decl=to_code_decl(from->code);
94  const symbol_exprt &symbol=to_symbol_expr(code_decl.symbol());
95  values.set_to_top(symbol);
96  }
97  else if(from->is_assign())
98  {
99  const code_assignt &assignment=to_code_assign(from->code);
100  const exprt &lhs=assignment.lhs();
101  const exprt &rhs=assignment.rhs();
102  assign_rec(values, lhs, rhs, ns, cp);
103  }
104  else if(from->is_assume())
105  {
106  two_way_propagate_rec(from->guard, ns, cp);
107  }
108  else if(from->is_goto())
109  {
110  exprt g;
111 
112  // Comparing iterators is safe as the target must be within the same list
113  // of instructions because this is a GOTO.
114  if(from->get_target()==to)
115  g = from->guard;
116  else
117  g = not_exprt(from->guard);
118  partial_evaluate(g, ns);
119  if(g.is_false())
121  else
122  {
123  two_way_propagate_rec(g, ns, cp);
124  // If two way propagate is enabled then it may be possible to detect
125  // that the branch condition is infeasible and thus the domain should
126  // be set to bottom. Without it the domain will only be set to bottom
127  // if the guard expression is trivially (i.e. without context) false.
129  "Without two-way propagation this should be impossible.");
130  }
131  }
132  else if(from->is_dead())
133  {
134  const code_deadt &code_dead=to_code_dead(from->code);
135  values.set_to_top(to_symbol_expr(code_dead.symbol()));
136  }
137  else if(from->is_function_call())
138  {
139  const code_function_callt &function_call=to_code_function_call(from->code);
140  const exprt &function=function_call.function();
141 
142  if(function.id()==ID_symbol)
143  {
144  // called function identifier
145  const symbol_exprt &symbol_expr=to_symbol_expr(function);
146  const irep_idt id=symbol_expr.get_identifier();
147 
148  // Functions with no body
149  if(from->function == to->function)
150  {
151  if(id==CPROVER_PREFIX "set_must" ||
152  id==CPROVER_PREFIX "get_must" ||
153  id==CPROVER_PREFIX "set_may" ||
154  id==CPROVER_PREFIX "get_may" ||
155  id==CPROVER_PREFIX "cleanup" ||
156  id==CPROVER_PREFIX "clear_may" ||
157  id==CPROVER_PREFIX "clear_must")
158  {
159  // no effect on constants
160  }
161  else
162  {
163  if(have_dirty)
164  values.set_dirty_to_top(cp->dirty, ns);
165  else
166  values.set_to_top();
167  }
168  }
169  else
170  {
171  // we have an actual call
172 
173  // parameters of called function
174  const symbolt &symbol=ns.lookup(id);
175  const code_typet &code_type=to_code_type(symbol.type);
176  const code_typet::parameterst &parameters=code_type.parameters();
177 
178  const code_function_callt::argumentst &arguments=
179  function_call.arguments();
180 
181  code_typet::parameterst::const_iterator p_it=parameters.begin();
182  for(const auto &arg : arguments)
183  {
184  if(p_it==parameters.end())
185  break;
186 
187  const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
188  assign_rec(values, parameter_expr, arg, ns, cp);
189 
190  ++p_it;
191  }
192  }
193  }
194  else
195  {
196  // unresolved call
197  INVARIANT(
198  from->function == to->function,
199  "Unresolved call can only be approximated if a skip");
200 
201  if(have_dirty)
202  values.set_dirty_to_top(cp->dirty, ns);
203  else
204  values.set_to_top();
205  }
206  }
207  else if(from->is_end_function())
208  {
209  // erase parameters
210 
211  const irep_idt id=from->function;
212  const symbolt &symbol=ns.lookup(id);
213 
214  const code_typet &type=to_code_type(symbol.type);
215 
216  for(const auto &param : type.parameters())
217  values.set_to_top(param.get_identifier());
218  }
219 
220  INVARIANT(from->is_goto() || !values.is_bottom,
221  "Transform only sets bottom by using branch conditions");
222 
223 #ifdef DEBUG
224  std::cout << "After:\n";
225  output(std::cout, ai, ns);
226 #endif
227 }
228 
229 
232  const exprt &expr,
233  const namespacet &,
234  const constant_propagator_ait *cp)
235 {
236 #ifdef DEBUG
237  std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
238 #endif
239 
240  bool change=false;
241 
242  // this seems to be buggy at present
243 #if 0
244  if(expr.id()==ID_and)
245  {
246  // need a fixed point here to get the most out of it
247  do
248  {
249  change = false;
250 
251  forall_operands(it, expr)
252  if(two_way_propagate_rec(*it, ns, cp))
253  change=true;
254  }
255  while(change);
256  }
257  else if(expr.id()==ID_equal)
258  {
259  const exprt &lhs=expr.op0();
260  const exprt &rhs=expr.op1();
261 
262  // two-way propagation
263  valuest copy_values=values;
264  assign_rec(copy_values, lhs, rhs, ns);
265  if(!values.is_constant(rhs) || values.is_constant(lhs))
266  assign_rec(values, rhs, lhs, ns);
267  change = values.meet(copy_values, ns);
268  }
269 #endif
270 
271 #ifdef DEBUG
272  std::cout << "two_way_propagate_rec: " << change << '\n';
273 #endif
274 
275  return change;
276 }
277 
283  exprt &condition,
284  const namespacet &ns) const
285 {
286  return partial_evaluate(condition, ns);
287 }
288 
289 
291 {
292  if(expr.id()==ID_side_effect &&
293  to_side_effect_expr(expr).get_statement()==ID_nondet)
294  return false;
295 
296  if(expr.id()==ID_side_effect &&
297  to_side_effect_expr(expr).get_statement()==ID_allocate)
298  return false;
299 
300  if(expr.id()==ID_symbol)
301  if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier())==
302  replace_const.expr_map.end())
303  return false;
304 
305  if(expr.id()==ID_index)
306  return false;
307 
308  if(expr.id()==ID_address_of)
310 
311  forall_operands(it, expr)
312  if(!is_constant(*it))
313  return false;
314 
315  return true;
316 }
317 
319  const exprt &expr) const
320 {
321  if(expr.id()==ID_index)
322  return is_constant_address_of(to_index_expr(expr).array()) &&
323  is_constant(to_index_expr(expr).index());
324 
325  if(expr.id()==ID_member)
326  return is_constant_address_of(to_member_expr(expr).struct_op());
327 
328  if(expr.id()==ID_dereference)
329  return is_constant(to_dereference_expr(expr).pointer());
330 
331  if(expr.id()==ID_string_constant)
332  return true;
333 
334  return true;
335 }
336 
339 {
341  replace_const.expr_map.erase(id);
342 
343  INVARIANT(n_erased==0 || !is_bottom, "bottom should have no elements at all");
344 
345  return n_erased>0;
346 }
347 
348 
350  const dirtyt &dirty,
351  const namespacet &ns)
352 {
354  expr_mapt &expr_map=replace_const.expr_map;
355 
356  for(expr_mapt::iterator it=expr_map.begin();
357  it!=expr_map.end();)
358  {
359  const irep_idt id=it->first;
360 
361  const symbolt &symbol=ns.lookup(id);
362 
363  if((!symbol.is_procedure_local() || dirty(id)) &&
364  !symbol.type.get_bool(ID_C_constant))
365  it=expr_map.erase(it);
366  else
367  it++;
368  }
369 }
370 
372  std::ostream &out,
373  const namespacet &ns) const
374 {
375  out << "const map:\n";
376 
377  if(is_bottom)
378  {
379  out << " bottom\n";
380  DATA_INVARIANT(replace_const.expr_map.empty(),
381  "If the domain is bottom, the map must be empty");
382  return;
383  }
384 
385  INVARIANT(!is_bottom, "Have handled bottom");
386  if(replace_const.expr_map.empty())
387  {
388  out << "top\n";
389  return;
390  }
391 
392  for(const auto &p : replace_const.expr_map)
393  {
394  out << ' ' << p.first << "=" << from_expr(ns, p.first, p.second) << '\n';
395  }
396 }
397 
399  std::ostream &out,
400  const ai_baset &,
401  const namespacet &ns) const
402 {
403  values.output(out, ns);
404 }
405 
409 {
410  // nothing to do
411  if(src.is_bottom)
412  return false;
413 
414  // just copy
415  if(is_bottom)
416  {
417  PRECONDITION(!src.is_bottom);
418  replace_const=src.replace_const; // copy
419  is_bottom=false;
420  return true;
421  }
422 
423  INVARIANT(!is_bottom && !src.is_bottom, "Case handled");
424 
425  bool changed=false;
426 
427  replace_symbolt::expr_mapt &expr_map=replace_const.expr_map;
428  const replace_symbolt::expr_mapt &src_expr_map=src.replace_const.expr_map;
429 
430  // handle top
431  if(src_expr_map.empty())
432  {
433  // change if it was not top
434  changed=!expr_map.empty();
435 
436  set_to_top();
437 
438  return changed;
439  }
440 
441  // remove those that are
442  // - different in src
443  // - do not exist in src
444  for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
445  it!=expr_map.end();)
446  {
447  const irep_idt id=it->first;
448  const exprt &expr=it->second;
449 
450  replace_symbolt::expr_mapt::const_iterator s_it;
451  s_it=src_expr_map.find(id);
452 
453  if(s_it!=src_expr_map.end())
454  {
455  // check value
456  const exprt &src_expr=s_it->second;
457 
458  if(expr!=src_expr)
459  {
460  it=expr_map.erase(it);
461  changed=true;
462  }
463  else
464  it++;
465  }
466  else
467  {
468  it=expr_map.erase(it);
469  changed=true;
470  }
471  }
472 
473  return changed;
474 }
475 
479  const valuest &src,
480  const namespacet &ns)
481 {
482  if(src.is_bottom || is_bottom)
483  return false;
484 
485  bool changed=false;
486 
487  for(const auto &m : src.replace_const.expr_map)
488  {
489  replace_symbolt::expr_mapt::iterator
490  c_it=replace_const.expr_map.find(m.first);
491 
492  if(c_it!=replace_const.expr_map.end())
493  {
494  if(c_it->second!=m.second)
495  {
496  set_to_bottom();
497  changed=true;
498  break;
499  }
500  }
501  else
502  {
504  base_type_eq(ns.lookup(m.first).type, m.second.type(), ns),
505  "type of constant to be stored should match");
506  set_to(m.first, m.second);
507  changed=true;
508  }
509  }
510 
511  return changed;
512 }
513 
516  const constant_propagator_domaint &other,
517  locationt,
518  locationt)
519 {
520  return values.merge(other.values);
521 }
522 
529  exprt &expr,
530  const namespacet &ns) const
531 {
532  // if the current rounding mode is top we can
533  // still get a non-top result by trying all rounding
534  // modes and checking if the results are all the same
536  {
538  }
539  return replace_constants_and_simplify(expr, ns);
540 }
541 
547  exprt &expr,
548  const namespacet &ns) const
549 { // NOLINTNEXTLINE (whitespace/braces)
550  auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
551  // NOLINTNEXTLINE (whitespace/braces)
555  // NOLINTNEXTLINE (whitespace/braces)
557  exprt first_result;
558  for(std::size_t i = 0; i < rounding_modes.size(); ++i)
559  {
560  constant_propagator_domaint child(*this);
561  child.values.set_to(
563  from_integer(rounding_modes[i], integer_typet()));
564  exprt result = expr;
565  if(child.replace_constants_and_simplify(result, ns))
566  {
567  return true;
568  }
569  else if(i == 0)
570  {
571  first_result = result;
572  }
573  else if(result != first_result)
574  {
575  return true;
576  }
577  }
578  expr = first_result;
579  return false;
580 }
581 
583  exprt &expr,
584  const namespacet &ns) const
585 {
586  bool did_not_change_anything = values.replace_const.replace(expr);
587  did_not_change_anything &= simplify(expr, ns);
588  return did_not_change_anything;
589 }
590 
592  goto_functionst &goto_functions,
593  const namespacet &ns)
594 {
595  Forall_goto_functions(f_it, goto_functions)
596  replace(f_it->second, ns);
597 }
598 
599 
601  goto_functionst::goto_functiont &goto_function,
602  const namespacet &ns)
603 {
604  Forall_goto_program_instructions(it, goto_function.body)
605  {
606  // Works because this is a location (but not history) sensitive domain
607  const constant_propagator_domaint &d = (*this)[it];
608 
609  if(d.is_bottom())
610  continue;
611 
612  replace_types_rec(d.values.replace_const, it->code);
613  replace_types_rec(d.values.replace_const, it->guard);
614 
615  if(it->is_goto() || it->is_assume() || it->is_assert())
616  {
617  d.partial_evaluate(it->guard, ns);
618  }
619  else if(it->is_assign())
620  {
621  exprt &rhs=to_code_assign(it->code).rhs();
622  d.partial_evaluate(rhs, ns);
623 
624  if(rhs.id()==ID_constant)
625  rhs.add_source_location()=it->code.op0().source_location();
626  }
627  else if(it->is_function_call())
628  {
629  exprt &function = to_code_function_call(it->code).function();
630  d.partial_evaluate(function, ns);
631 
632  exprt::operandst &args=
633  to_code_function_call(it->code).arguments();
634 
635  for(auto &arg : args)
636  {
637  d.partial_evaluate(arg, ns);
638  }
639  }
640  else if(it->is_other())
641  {
642  if(it->code.get_statement()==ID_expression)
643  {
644  d.partial_evaluate(it->code, ns);
645  }
646  }
647  }
648 }
649 
651  const replace_symbolt &replace_const,
652  exprt &expr)
653 {
654  replace_const(expr.type());
655 
656  Forall_operands(it, expr)
657  replace_types_rec(replace_const, *it);
658 }
Boolean negation.
Definition: std_expr.h:3228
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:291
Base type of functions.
Definition: std_types.h:764
exprt & object()
Definition: std_expr.h:3178
virtual void transform(locationt from, 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...
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:72
#define CPROVER_PREFIX
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:344
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:268
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
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:888
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:3199
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
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:204
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3326
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1326
bool is_constant(const exprt &expr) const
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:209
argumentst & arguments()
Definition: std_code.h:890
A declaration of a local variable.
Definition: std_code.h:254
exprt & rhs()
Definition: std_code.h:214
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: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:242
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
A function call.
Definition: std_code.h:858
#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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
exprt & symbol()
Definition: std_code.h:321
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
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
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:878
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:42
exprt & pointer()
Definition: std_expr.h:3305
const exprt & struct_op() const
Definition: std_expr.h:3909
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:307
#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_domain.h:40
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)
Base Type Computation.
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
expr_mapt expr_map
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void replace(goto_functionst::goto_functiont &, const namespacet &)
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:136
Assignment.
Definition: std_code.h:196
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:1292
bool meet(const valuest &src, const namespacet &ns)
meet
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909
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)