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/c_types.h>
21 #include <util/cprover_prefix.h>
22 #include <util/expr_util.h>
23 #include <util/find_symbols.h>
24 #include <util/ieee_float.h>
26 #include <util/simplify_expr.h>
27 
28 #include <langapi/language_util.h>
29 
30 #include <algorithm>
31 #include <array>
32 
52  valuest &dest_values,
53  const exprt &lhs,
54  const exprt &rhs,
55  const namespacet &ns,
56  const constant_propagator_ait *cp,
57  bool is_assignment)
58 {
59  if(lhs.id() == ID_dereference)
60  {
61  exprt eval_lhs = lhs;
62  if(partial_evaluate(dest_values, eval_lhs, ns))
63  {
64  if(is_assignment)
65  {
66  const bool have_dirty = (cp != nullptr);
67 
68  if(have_dirty)
69  dest_values.set_dirty_to_top(cp->dirty, ns);
70  else
71  dest_values.set_to_top();
72  }
73  // Otherwise disregard this unknown deref in a read-only context.
74  }
75  else
76  assign_rec(dest_values, eval_lhs, rhs, ns, cp, is_assignment);
77  }
78  else if(lhs.id() == ID_index)
79  {
80  const index_exprt &index_expr = to_index_expr(lhs);
81  with_exprt new_rhs(index_expr.array(), index_expr.index(), rhs);
82  assign_rec(dest_values, index_expr.array(), new_rhs, ns, cp, is_assignment);
83  }
84  else if(lhs.id() == ID_member)
85  {
86  const member_exprt &member_expr = to_member_expr(lhs);
87  with_exprt new_rhs(member_expr.compound(), exprt(ID_member_name), rhs);
88  new_rhs.where().set(ID_component_name, member_expr.get_component_name());
89  assign_rec(
90  dest_values, member_expr.compound(), new_rhs, ns, cp, is_assignment);
91  }
92  else if(lhs.id() == ID_symbol)
93  {
94  if(cp && !cp->should_track_value(lhs, ns))
95  return;
96 
97  const symbol_exprt &s = to_symbol_expr(lhs);
98 
99  exprt tmp = rhs;
100  partial_evaluate(dest_values, tmp, ns);
101 
102  if(dest_values.is_constant(tmp))
103  {
105  ns.lookup(s).type == tmp.type(),
106  "type of constant to be replaced should match");
107  dest_values.set_to(s, tmp);
108  }
109  else
110  {
111  if(is_assignment)
112  dest_values.set_to_top(s);
113  }
114  }
115  else if(is_assignment)
116  {
117  // it's an assignment, but we don't really know what object is being written
118  // to: assume it may write to anything.
119  dest_values.set_to_top();
120  }
121 }
122 
124  const irep_idt &function_from,
125  locationt from,
126  const irep_idt &function_to,
127  locationt to,
128  ai_baset &ai,
129  const namespacet &ns)
130 {
131 #ifdef DEBUG
132  std::cout << "Transform from/to:\n";
133  std::cout << from->location_number << " --> "
134  << to->location_number << '\n';
135 #endif
136 
137 #ifdef DEBUG
138  std::cout << "Before:\n";
139  output(std::cout, ai, ns);
140 #endif
141 
142  // When the domain is used with constant_propagator_ait,
143  // information about dirty variables and config flags are
144  // available. Otherwise, the below will be null and we use default
145  // values
146  const constant_propagator_ait *cp=
147  dynamic_cast<constant_propagator_ait *>(&ai);
148  bool have_dirty=(cp!=nullptr);
149 
150  // Transform on a domain that is bottom is possible
151  // if a branch is impossible the target can still wind
152  // up on the work list.
153  if(values.is_bottom)
154  return;
155 
156  if(from->is_decl())
157  {
158  const auto &code_decl = from->get_decl();
159  const symbol_exprt &symbol = code_decl.symbol();
160  values.set_to_top(symbol);
161  }
162  else if(from->is_assign())
163  {
164  const auto &assignment = from->get_assign();
165  const exprt &lhs=assignment.lhs();
166  const exprt &rhs=assignment.rhs();
167  assign_rec(values, lhs, rhs, ns, cp, true);
168  }
169  else if(from->is_assume())
170  {
171  two_way_propagate_rec(from->get_condition(), ns, cp);
172  }
173  else if(from->is_goto())
174  {
175  exprt g;
176 
177  // Comparing iterators is safe as the target must be within the same list
178  // of instructions because this is a GOTO.
179  if(from->get_target()==to)
180  g = from->get_condition();
181  else
182  g = not_exprt(from->get_condition());
183  partial_evaluate(values, g, ns);
184  if(g.is_false())
186  else
187  two_way_propagate_rec(g, ns, cp);
188  }
189  else if(from->is_dead())
190  {
191  const auto &code_dead = from->get_dead();
192  values.set_to_top(code_dead.symbol());
193  }
194  else if(from->is_function_call())
195  {
196  const auto &function_call = from->get_function_call();
197  const exprt &function=function_call.function();
198 
199  if(function.id()==ID_symbol)
200  {
201  // called function identifier
202  const symbol_exprt &symbol_expr=to_symbol_expr(function);
203  const irep_idt id=symbol_expr.get_identifier();
204 
205  // Functions with no body
206  if(function_from == function_to)
207  {
208  if(id==CPROVER_PREFIX "set_must" ||
209  id==CPROVER_PREFIX "get_must" ||
210  id==CPROVER_PREFIX "set_may" ||
211  id==CPROVER_PREFIX "get_may" ||
212  id==CPROVER_PREFIX "cleanup" ||
213  id==CPROVER_PREFIX "clear_may" ||
214  id==CPROVER_PREFIX "clear_must")
215  {
216  // no effect on constants
217  }
218  else
219  {
220  if(have_dirty)
221  values.set_dirty_to_top(cp->dirty, ns);
222  else
223  values.set_to_top();
224  }
225  }
226  else
227  {
228  // we have an actual call
229 
230  // parameters of called function
231  const symbolt &symbol=ns.lookup(id);
232  const code_typet &code_type=to_code_type(symbol.type);
233  const code_typet::parameterst &parameters=code_type.parameters();
234 
235  const code_function_callt::argumentst &arguments=
236  function_call.arguments();
237 
238  code_typet::parameterst::const_iterator p_it=parameters.begin();
239  for(const auto &arg : arguments)
240  {
241  if(p_it==parameters.end())
242  break;
243 
244  const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
245  assign_rec(values, parameter_expr, arg, ns, cp, true);
246 
247  ++p_it;
248  }
249  }
250  }
251  else
252  {
253  // unresolved call
254  INVARIANT(
255  function_from == function_to,
256  "Unresolved call can only be approximated if a skip");
257 
258  if(have_dirty)
259  values.set_dirty_to_top(cp->dirty, ns);
260  else
261  values.set_to_top();
262  }
263  }
264  else if(from->is_end_function())
265  {
266  // erase parameters
267 
268  const irep_idt id = function_from;
269  const symbolt &symbol=ns.lookup(id);
270 
271  const code_typet &type=to_code_type(symbol.type);
272 
273  for(const auto &param : type.parameters())
274  values.set_to_top(symbol_exprt(param.get_identifier(), param.type()));
275  }
276 
277  INVARIANT(from->is_goto() || !values.is_bottom,
278  "Transform only sets bottom by using branch conditions");
279 
280 #ifdef DEBUG
281  std::cout << "After:\n";
282  output(std::cout, ai, ns);
283 #endif
284 }
285 
286 static void
288 {
289  // (int)var xx 0 ==> var xx (_Bool)0 or similar (xx is == or !=)
290  // Note this is restricted to bools because in general turning a widening
291  // into a narrowing typecast is not correct.
292  if(lhs.id() != ID_typecast)
293  return;
294 
295  const exprt &lhs_underlying = to_typecast_expr(lhs).op();
296  if(
297  lhs_underlying.type() == bool_typet() ||
298  lhs_underlying.type() == c_bool_type())
299  {
300  rhs = typecast_exprt(rhs, lhs_underlying.type());
301  simplify(rhs, ns);
302 
303  lhs = lhs_underlying;
304  }
305 }
306 
309  const exprt &expr,
310  const namespacet &ns,
311  const constant_propagator_ait *cp)
312 {
313 #ifdef DEBUG
314  std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
315 #endif
316 
317  bool change=false;
318 
319  if(expr.id()==ID_and)
320  {
321  // need a fixed point here to get the most out of it
322  bool change_this_time;
323  do
324  {
325  change_this_time = false;
326 
327  forall_operands(it, expr)
328  {
329  change_this_time |= two_way_propagate_rec(*it, ns, cp);
330  if(change_this_time)
331  change = true;
332  }
333  } while(change_this_time);
334  }
335  else if(expr.id() == ID_not)
336  {
337  const auto &op = to_not_expr(expr).op();
338 
339  if(op.id() == ID_equal || op.id() == ID_notequal)
340  {
341  exprt subexpr = op;
342  subexpr.id(subexpr.id() == ID_equal ? ID_notequal : ID_equal);
343  change = two_way_propagate_rec(subexpr, ns, cp);
344  }
345  else if(op.id() == ID_symbol && expr.type() == bool_typet())
346  {
347  // Treat `IF !x` like `IF x == FALSE`:
348  change = two_way_propagate_rec(equal_exprt(op, false_exprt()), ns, cp);
349  }
350  }
351  else if(expr.id() == ID_symbol)
352  {
353  if(expr.type() == bool_typet())
354  {
355  // Treat `IF x` like `IF x == TRUE`:
356  change = two_way_propagate_rec(equal_exprt(expr, true_exprt()), ns, cp);
357  }
358  }
359  else if(expr.id() == ID_notequal)
360  {
361  // Treat "symbol != constant" like "symbol == !constant" when the constant
362  // is a boolean.
363  exprt lhs = to_notequal_expr(expr).lhs();
364  exprt rhs = to_notequal_expr(expr).rhs();
365 
366  if(lhs.is_constant() && !rhs.is_constant())
367  std::swap(lhs, rhs);
368 
369  if(lhs.is_constant() || !rhs.is_constant())
370  return false;
371 
372  replace_typecast_of_bool(lhs, rhs, ns);
373 
374  if(lhs.type() != bool_typet() && lhs.type() != c_bool_type())
375  return false;
376 
377  // x != FALSE ==> x == TRUE
378 
379  if(rhs.is_zero() || rhs.is_false())
380  rhs = from_integer(1, rhs.type());
381  else
382  rhs = from_integer(0, rhs.type());
383 
384  change = two_way_propagate_rec(equal_exprt(lhs, rhs), ns, cp);
385  }
386  else if(expr.id() == ID_equal)
387  {
388  exprt lhs = to_equal_expr(expr).lhs();
389  exprt rhs = to_equal_expr(expr).rhs();
390 
391  replace_typecast_of_bool(lhs, rhs, ns);
392 
393  // two-way propagation
394  valuest copy_values=values;
395  assign_rec(copy_values, lhs, rhs, ns, cp, false);
396  if(!values.is_constant(rhs) || values.is_constant(lhs))
397  assign_rec(values, rhs, lhs, ns, cp, false);
398  change = values.meet(copy_values, ns);
399  }
400 
401 #ifdef DEBUG
402  std::cout << "two_way_propagate_rec: " << change << '\n';
403 #endif
404 
405  return change;
406 }
407 
413  exprt &condition,
414  const namespacet &ns) const
415 {
416  return partial_evaluate(values, condition, ns);
417 }
418 
420 {
421 public:
425  {
426  }
427 
428  bool is_constant(const irep_idt &id) const
429  {
430  return replace_const.replaces_symbol(id);
431  }
432 
433 protected:
434  bool is_constant(const exprt &expr) const override
435  {
436  if(expr.id() == ID_symbol)
437  return is_constant(to_symbol_expr(expr).get_identifier());
438 
439  return is_constantt::is_constant(expr);
440  }
441 
443 };
444 
446 {
448 }
449 
451 {
452  return constant_propagator_is_constantt(replace_const).is_constant(id);
453 }
454 
457  const symbol_exprt &symbol_expr)
458 {
459  const auto n_erased = replace_const.erase(symbol_expr.get_identifier());
460 
461  INVARIANT(n_erased==0 || !is_bottom, "bottom should have no elements at all");
462 
463  return n_erased>0;
464 }
465 
466 
468  const dirtyt &dirty,
469  const namespacet &ns)
470 {
472  expr_mapt &expr_map = replace_const.get_expr_map();
473 
474  for(expr_mapt::iterator it=expr_map.begin();
475  it!=expr_map.end();)
476  {
477  const irep_idt id=it->first;
478 
479  const symbolt &symbol=ns.lookup(id);
480 
481  if(
482  (symbol.is_static_lifetime || dirty(id)) &&
483  !symbol.type.get_bool(ID_C_constant))
484  {
485  it = replace_const.erase(it);
486  }
487  else
488  it++;
489  }
490 }
491 
493  std::ostream &out,
494  const namespacet &ns) const
495 {
496  out << "const map:\n";
497 
498  if(is_bottom)
499  {
500  out << " bottom\n";
502  "If the domain is bottom, the map must be empty");
503  return;
504  }
505 
506  INVARIANT(!is_bottom, "Have handled bottom");
507  if(is_empty())
508  {
509  out << "top\n";
510  return;
511  }
512 
513  for(const auto &p : replace_const.get_expr_map())
514  {
515  out << ' ' << p.first << "=" << from_expr(ns, p.first, p.second) << '\n';
516  }
517 }
518 
520  std::ostream &out,
521  const ai_baset &,
522  const namespacet &ns) const
523 {
524  values.output(out, ns);
525 }
526 
530 {
531  // nothing to do
532  if(src.is_bottom)
533  return false;
534 
535  // just copy
536  if(is_bottom)
537  {
538  PRECONDITION(!src.is_bottom);
539  replace_const=src.replace_const; // copy
540  is_bottom=false;
541  return true;
542  }
543 
544  INVARIANT(!is_bottom && !src.is_bottom, "Case handled");
545 
546  bool changed=false;
547 
548  // handle top
549  if(src.is_empty())
550  {
551  // change if it was not top
552  changed = !is_empty();
553 
554  set_to_top();
555 
556  return changed;
557  }
558 
559  replace_symbolt::expr_mapt &expr_map = replace_const.get_expr_map();
560  const replace_symbolt::expr_mapt &src_expr_map =
562 
563  // remove those that are
564  // - different in src
565  // - do not exist in src
566  for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
567  it!=expr_map.end();)
568  {
569  const irep_idt id=it->first;
570  const exprt &expr=it->second;
571 
572  replace_symbolt::expr_mapt::const_iterator s_it;
573  s_it=src_expr_map.find(id);
574 
575  if(s_it!=src_expr_map.end())
576  {
577  // check value
578  const exprt &src_expr=s_it->second;
579 
580  if(expr!=src_expr)
581  {
582  it = replace_const.erase(it);
583  changed=true;
584  }
585  else
586  it++;
587  }
588  else
589  {
590  it = replace_const.erase(it);
591  changed=true;
592  }
593  }
594 
595  return changed;
596 }
597 
601  const valuest &src,
602  const namespacet &ns)
603 {
604  if(src.is_bottom || is_bottom)
605  return false;
606 
607  bool changed=false;
608 
609  for(const auto &m : src.replace_const.get_expr_map())
610  {
611  replace_symbolt::expr_mapt::const_iterator c_it =
612  replace_const.get_expr_map().find(m.first);
613 
614  if(c_it != replace_const.get_expr_map().end())
615  {
616  if(c_it->second!=m.second)
617  {
618  set_to_bottom();
619  changed=true;
620  break;
621  }
622  }
623  else
624  {
625  const typet &m_id_type = ns.lookup(m.first).type;
627  m_id_type == m.second.type(),
628  "type of constant to be stored should match");
629  set_to(symbol_exprt(m.first, m_id_type), m.second);
630  changed=true;
631  }
632  }
633 
634  return changed;
635 }
636 
639  const constant_propagator_domaint &other,
640  locationt,
641  locationt)
642 {
643  return values.merge(other.values);
644 }
645 
653  const valuest &known_values,
654  exprt &expr,
655  const namespacet &ns)
656 {
657  // if the current rounding mode is top we can
658  // still get a non-top result by trying all rounding
659  // modes and checking if the results are all the same
660  if(!known_values.is_constant(ID_cprover_rounding_mode_str))
661  return partial_evaluate_with_all_rounding_modes(known_values, expr, ns);
662 
663  return replace_constants_and_simplify(known_values, expr, ns);
664 }
665 
674  const valuest &known_values,
675  exprt &expr,
676  const namespacet &ns)
677 { // NOLINTNEXTLINE (whitespace/braces)
678  auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
679  // NOLINTNEXTLINE (whitespace/braces)
683  // NOLINTNEXTLINE (whitespace/braces)
685  exprt first_result;
686  for(std::size_t i = 0; i < rounding_modes.size(); ++i)
687  {
688  valuest tmp_values = known_values;
689  tmp_values.set_to(
691  from_integer(rounding_modes[i], integer_typet()));
692  exprt result = expr;
693  if(replace_constants_and_simplify(tmp_values, result, ns))
694  {
695  return true;
696  }
697  else if(i == 0)
698  {
699  first_result = result;
700  }
701  else if(result != first_result)
702  {
703  return true;
704  }
705  }
706  expr = first_result;
707  return false;
708 }
709 
711  const valuest &known_values,
712  exprt &expr,
713  const namespacet &ns)
714 {
715  bool did_not_change_anything = true;
716 
717  // iterate constant propagation and simplification until we cannot
718  // constant-propagate any further - a prime example is pointer dereferencing,
719  // where constant propagation may have a value of the pointer, the simplifier
720  // takes care of evaluating dereferencing, and we might then have the value of
721  // the resulting symbol known to constant propagation and thus replace the
722  // dereferenced expression by a constant
723  while(!known_values.replace_const.replace(expr))
724  {
725  did_not_change_anything = false;
726  simplify(expr, ns);
727  }
728 
729  // even if we haven't been able to constant-propagate anything, run the
730  // simplifier on the expression
731  if(did_not_change_anything)
732  did_not_change_anything &= simplify(expr, ns);
733 
734  return did_not_change_anything;
735 }
736 
738  goto_functionst &goto_functions,
739  const namespacet &ns)
740 {
741  Forall_goto_functions(f_it, goto_functions)
742  replace(f_it->second, ns);
743 }
744 
745 
747  goto_functionst::goto_functiont &goto_function,
748  const namespacet &ns)
749 {
750  Forall_goto_program_instructions(it, goto_function.body)
751  {
752  // Works because this is a location (but not history) sensitive domain
753  const constant_propagator_domaint &d = (*this)[it];
754 
755  if(d.is_bottom())
756  continue;
757 
758  replace_types_rec(d.values.replace_const, it->code);
759 
760  if(it->is_goto() || it->is_assume() || it->is_assert())
761  {
762  exprt c = it->get_condition();
763  replace_types_rec(d.values.replace_const, c);
765  it->set_condition(c);
766  }
767  else if(it->is_assign())
768  {
769  auto assign = it->get_assign();
770  exprt &rhs = assign.rhs();
771 
773  {
774  if(rhs.id() == ID_constant)
775  rhs.add_source_location() = assign.lhs().source_location();
776  it->set_assign(assign);
777  }
778  }
779  else if(it->is_function_call())
780  {
781  auto call = it->get_function_call();
782 
783  bool call_changed = false;
784 
786  d.values, call.function(), ns))
787  {
788  call_changed = true;
789  }
790 
791  for(auto &arg : call.arguments())
793  call_changed = true;
794 
795  if(call_changed)
796  it->set_function_call(call);
797  }
798  else if(it->is_other())
799  {
800  if(it->get_other().get_statement() == ID_expression)
801  {
802  auto c = to_code_expression(it->get_other());
804  d.values, c.expression(), ns))
805  {
806  it->set_other(c);
807  }
808  }
809  }
810  }
811 }
812 
814  const replace_symbolt &replace_const,
815  exprt &expr)
816 {
817  replace_const(expr.type());
818 
819  Forall_operands(it, expr)
820  replace_types_rec(replace_const, *it);
821 }
is_constantt
Determine whether an expression is constant.
Definition: expr_util.h:87
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3050
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
ID_cprover_rounding_mode_str
const char ID_cprover_rounding_mode_str[]
Definition: ieee_float.h:23
format
static format_containert< T > format(const T &o)
Definition: format.h:35
to_code_expression
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1844
constant_propagator_domaint::valuest::replace_const
address_of_aware_replace_symbolt replace_const
Definition: constant_propagator.h:86
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:641
replace_symbolt::replaces_symbol
bool replaces_symbol(const irep_idt &id) const
Definition: replace_symbol.h:71
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
arith_tools.h
constant_propagator_ait::should_track_value
should_track_valuet should_track_value
Definition: constant_propagator.h:236
constant_propagator_domaint::valuest::is_constant
bool is_constant(const exprt &expr) const
Definition: constant_propagator.cpp:445
constant_propagator_domaint
Definition: constant_propagator.h:34
dirtyt
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition: dirty.h:27
constant_propagator_domaint::two_way_propagate_rec
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
Definition: constant_propagator.cpp:308
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
constant_propagator_is_constantt::is_constant
bool is_constant(const irep_idt &id) const
Definition: constant_propagator.cpp:428
constant_propagator_domaint::partial_evaluate
static bool partial_evaluate(const valuest &known_values, exprt &expr, const namespacet &ns)
Attempt to evaluate expression using domain knowledge This function changes the expression that is pa...
Definition: constant_propagator.cpp:652
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
constant_propagator_domaint::assign_rec
static void assign_rec(valuest &dest_values, const exprt &lhs, const exprt &rhs, const namespacet &ns, const constant_propagator_ait *cp, bool is_assignment)
Assign value rhs to lhs, recording any newly-known constants in dest_values.
Definition: constant_propagator.cpp:51
c_bool_type
typet c_bool_type()
Definition: c_types.cpp:108
constant_propagator_domaint::valuest::set_dirty_to_top
void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns)
Definition: constant_propagator.cpp:467
replace_symbolt::expr_mapt
std::unordered_map< irep_idt, exprt > expr_mapt
Definition: replace_symbol.h:27
replace_symbolt::get_expr_map
const expr_mapt & get_expr_map() const
Definition: replace_symbol.h:79
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
constant_propagator.h
Constant propagation.
integer_typet
Unbounded, signed integers (mathematical integers, not bitvectors)
Definition: mathematical_types.h:22
exprt
Base class for all expressions.
Definition: expr.h:53
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:631
bool_typet
The Boolean type.
Definition: std_types.h:37
constant_propagator_domaint::output
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
Definition: constant_propagator.cpp:519
constant_propagator_domaint::values
valuest values
Definition: constant_propagator.h:138
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
equal_exprt
Equality.
Definition: std_expr.h:1190
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
constant_propagator_ait::dirty
dirtyt dirty
Definition: constant_propagator.h:219
constant_propagator_domaint::replace_constants_and_simplify
static bool replace_constants_and_simplify(const valuest &known_values, exprt &expr, const namespacet &ns)
Definition: constant_propagator.cpp:710
mathematical_types.h
Mathematical types.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
constant_propagator_domaint::valuest::is_bottom
bool is_bottom
Definition: constant_propagator.h:87
constant_propagator_domaint::valuest::set_to_bottom
void set_to_bottom()
Definition: constant_propagator.h:94
is_constantt::is_constant
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:227
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
is_empty
bool is_empty(const std::string &s)
Definition: document_properties.cpp:140
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
find_symbols.h
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:3446
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
language_util.h
constant_propagator_domaint::merge
bool merge(const constant_propagator_domaint &other, locationt from, locationt to)
Definition: constant_propagator.cpp:638
constant_propagator_domaint::valuest::output
void output(std::ostream &out, const namespacet &ns) const
Definition: constant_propagator.cpp:492
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
constant_propagator_domaint::valuest::set_to_top
void set_to_top()
Definition: constant_propagator.h:100
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
address_of_aware_replace_symbolt::replace
bool replace(exprt &dest) const override
Definition: replace_symbol.cpp:263
constant_propagator_is_constantt::is_constant
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
Definition: constant_propagator.cpp:434
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
to_notequal_expr
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1273
constant_propagator_domaint::valuest::merge
bool merge(const valuest &src)
join
Definition: constant_propagator.cpp:529
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
constant_propagator_domaint::is_bottom
virtual bool is_bottom() const final override
Definition: constant_propagator.h:73
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
irept::id
const irep_idt & id() const
Definition: irep.h:418
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1192
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
cprover_prefix.h
constant_propagator_is_constantt::constant_propagator_is_constantt
constant_propagator_is_constantt(const replace_symbolt &replace_const)
Definition: constant_propagator.cpp:422
constant_propagator_ait::replace_types_rec
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
Definition: constant_propagator.cpp:813
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
simplify_expr.h
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:132
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
constant_propagator_domaint::transform
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
Definition: constant_propagator.cpp:123
expr_util.h
Deprecated expression utility functions.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
format_expr.h
ieee_floatt::ROUND_TO_PLUS_INF
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:128
ieee_floatt::ROUND_TO_EVEN
@ ROUND_TO_EVEN
Definition: ieee_float.h:127
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2868
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
constant_propagator_domaint::ai_simplify
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const final override
Simplify the condition given context-sensitive knowledge from the abstract state.
Definition: constant_propagator.cpp:412
constant_propagator_domaint::partial_evaluate_with_all_rounding_modes
static bool partial_evaluate_with_all_rounding_modes(const valuest &known_values, exprt &expr, const namespacet &ns)
Attempt to evaluate an expression in all rounding modes.
Definition: constant_propagator.cpp:673
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
ieee_float.h
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:85
constant_propagator_ait
Definition: constant_propagator.h:171
constant_propagator_domaint::valuest::set_to
void set_to(const symbol_exprt &lhs, const exprt &rhs)
Definition: constant_propagator.h:116
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
constant_propagator_domaint::valuest::meet
bool meet(const valuest &src, const namespacet &ns)
meet
Definition: constant_propagator.cpp:600
constant_propagator_is_constantt::replace_const
const replace_symbolt & replace_const
Definition: constant_propagator.cpp:442
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1230
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
constant_propagator_ait::replace
void replace(goto_functionst::goto_functiont &, const namespacet &)
Definition: constant_propagator.cpp:746
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
replace_typecast_of_bool
static void replace_typecast_of_bool(exprt &lhs, exprt &rhs, const namespacet &ns)
Definition: constant_propagator.cpp:287
constant_propagator_domaint::valuest
Definition: constant_propagator.h:84
index_exprt
Array index operator.
Definition: std_expr.h:1293
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
expr_mapt
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
Definition: acceleration_utils.h:33
with_exprt::where
exprt & where()
Definition: std_expr.h:3070
constant_propagator_domaint::valuest::is_empty
bool is_empty() const
Definition: constant_propagator.h:130
c_types.h
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
ieee_floatt::ROUND_TO_MINUS_INF
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:127
ieee_floatt::ROUND_TO_ZERO
@ ROUND_TO_ZERO
Definition: ieee_float.h:128
constant_propagator_is_constantt
Definition: constant_propagator.cpp:420
validation_modet::INVARIANT
@ INVARIANT
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25
not_exprt
Boolean negation.
Definition: std_expr.h:2843