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 
15 
16 #ifdef DEBUG
17 #include <iostream>
18 #include <util/format_expr.h>
19 #endif
20 
21 #include <util/arith_tools.h>
22 #include <util/c_types.h>
23 #include <util/cprover_prefix.h>
24 #include <util/expr_util.h>
25 #include <util/ieee_float.h>
27 #include <util/simplify_expr.h>
28 
29 #include <langapi/language_util.h>
30 
31 #include <algorithm>
32 #include <array>
33 
53  valuest &dest_values,
54  const exprt &lhs,
55  const exprt &rhs,
56  const namespacet &ns,
57  const constant_propagator_ait *cp,
58  bool is_assignment)
59 {
60  if(lhs.id() == ID_dereference)
61  {
62  exprt eval_lhs = lhs;
63  if(partial_evaluate(dest_values, eval_lhs, ns))
64  {
65  if(is_assignment)
66  {
67  const bool have_dirty = (cp != nullptr);
68 
69  if(have_dirty)
70  dest_values.set_dirty_to_top(cp->dirty, ns);
71  else
72  dest_values.set_to_top();
73  }
74  // Otherwise disregard this unknown deref in a read-only context.
75  }
76  else
77  assign_rec(dest_values, eval_lhs, rhs, ns, cp, is_assignment);
78  }
79  else if(lhs.id() == ID_index)
80  {
81  const index_exprt &index_expr = to_index_expr(lhs);
82  with_exprt new_rhs(index_expr.array(), index_expr.index(), rhs);
83  assign_rec(dest_values, index_expr.array(), new_rhs, ns, cp, is_assignment);
84  }
85  else if(lhs.id() == ID_member)
86  {
87  const member_exprt &member_expr = to_member_expr(lhs);
88  with_exprt new_rhs(member_expr.compound(), exprt(ID_member_name), rhs);
89  new_rhs.where().set(ID_component_name, member_expr.get_component_name());
90  assign_rec(
91  dest_values, member_expr.compound(), new_rhs, ns, cp, is_assignment);
92  }
93  else if(lhs.id() == ID_symbol)
94  {
95  if(cp && !cp->should_track_value(lhs, ns))
96  return;
97 
98  const symbol_exprt &s = to_symbol_expr(lhs);
99 
100  exprt tmp = rhs;
101  partial_evaluate(dest_values, tmp, ns);
102 
103  if(dest_values.is_constant(tmp))
104  {
106  ns.lookup(s).type == tmp.type(),
107  "type of constant to be replaced should match");
108  dest_values.set_to(s, tmp);
109  }
110  else
111  {
112  if(is_assignment)
113  dest_values.set_to_top(s);
114  }
115  }
116  else if(is_assignment)
117  {
118  // it's an assignment, but we don't really know what object is being written
119  // to: assume it may write to anything.
120  dest_values.set_to_top();
121  }
122 }
123 
125  const irep_idt &function_from,
126  trace_ptrt trace_from,
127  const irep_idt &function_to,
128  trace_ptrt trace_to,
129  ai_baset &ai,
130  const namespacet &ns)
131 {
132  locationt from{trace_from->current_location()};
133  locationt to{trace_to->current_location()};
134 
135 #ifdef DEBUG
136  std::cout << "Transform from/to:\n";
137  std::cout << from->location_number << " --> "
138  << to->location_number << '\n';
139 #endif
140 
141 #ifdef DEBUG
142  std::cout << "Before:\n";
143  output(std::cout, ai, ns);
144 #endif
145 
146  // When the domain is used with constant_propagator_ait,
147  // information about dirty variables and config flags are
148  // available. Otherwise, the below will be null and we use default
149  // values
150  const constant_propagator_ait *cp=
151  dynamic_cast<constant_propagator_ait *>(&ai);
152  bool have_dirty=(cp!=nullptr);
153 
154  // Transform on a domain that is bottom is possible
155  // if a branch is impossible the target can still wind
156  // up on the work list.
157  if(values.is_bottom)
158  return;
159 
160  if(from->is_decl())
161  {
162  const symbol_exprt &symbol = from->decl_symbol();
163  values.set_to_top(symbol);
164  }
165  else if(from->is_assign())
166  {
167  const exprt &lhs = from->assign_lhs();
168  const exprt &rhs = from->assign_rhs();
169  assign_rec(values, lhs, rhs, ns, cp, true);
170  }
171  else if(from->is_assume())
172  {
173  two_way_propagate_rec(from->get_condition(), ns, cp);
174  }
175  else if(from->is_goto())
176  {
177  exprt g;
178 
179  // Comparing iterators is safe as the target must be within the same list
180  // of instructions because this is a GOTO.
181  if(from->get_target()==to)
182  g = from->get_condition();
183  else
184  g = not_exprt(from->get_condition());
185  partial_evaluate(values, g, ns);
186  if(g.is_false())
188  else
189  two_way_propagate_rec(g, ns, cp);
190  }
191  else if(from->is_dead())
192  {
193  values.set_to_top(from->dead_symbol());
194  }
195  else if(from->is_function_call())
196  {
197  const exprt &function = from->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  from->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  trace_ptrt,
641  trace_ptrt)
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(rounding_mode_identifier()))
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  for(auto &gf_entry : goto_functions.function_map)
742  replace(gf_entry.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  auto const current_domain_ptr =
753  std::dynamic_pointer_cast<const constant_propagator_domaint>(
754  this->abstract_state_before(it));
755  const constant_propagator_domaint &d = *current_domain_ptr;
756 
757  if(d.is_bottom())
758  continue;
759 
760  replace_types_rec(d.values.replace_const, it->code_nonconst());
761 
762  if(it->is_goto() || it->is_assume() || it->is_assert())
763  {
764  exprt c = it->get_condition();
765  replace_types_rec(d.values.replace_const, c);
767  it->set_condition(c);
768  }
769  else if(it->is_assign())
770  {
771  exprt &rhs = it->assign_rhs_nonconst();
772 
774  {
775  if(rhs.id() == ID_constant)
776  rhs.add_source_location() = it->assign_lhs().source_location();
777  }
778  }
779  else if(it->is_function_call())
780  {
782  d.values, it->call_function(), ns);
783 
784  for(auto &arg : it->call_arguments())
786  }
787  else if(it->is_other())
788  {
789  if(it->get_other().get_statement() == ID_expression)
790  {
791  auto c = to_code_expression(it->get_other());
793  d.values, c.expression(), ns))
794  {
795  it->set_other(c);
796  }
797  }
798  }
799  }
800 }
801 
803  const replace_symbolt &replace_const,
804  exprt &expr)
805 {
806  replace_const(expr.type());
807 
808  Forall_operands(it, expr)
809  replace_types_rec(replace_const, *it);
810 }
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
typet c_bool_type()
Definition: c_types.cpp:108
bool replace(exprt &dest) const override
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:74
goto_programt::const_targett locationt
Definition: ai_domain.h:73
exprt & lhs()
Definition: std_expr.h:580
exprt & rhs()
Definition: std_expr.h:590
The Boolean type.
Definition: std_types.h:36
exprt::operandst argumentst
Definition: std_code.h:1222
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:541
const parameterst & parameters() const
Definition: std_types.h:655
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
should_track_valuet should_track_value
void replace(goto_functionst::goto_functiont &, const namespacet &)
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.
virtual bool is_bottom() const final override
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...
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const final override
Simplify the condition given context-sensitive knowledge from the abstract state.
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.
virtual void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_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...
static bool replace_constants_and_simplify(const valuest &known_values, exprt &expr, const namespacet &ns)
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
bool merge(const constant_propagator_domaint &other, trace_ptrt from, trace_ptrt to)
constant_propagator_is_constantt(const replace_symbolt &replace_const)
bool is_constant(const irep_idt &id) const
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition: dirty.h:27
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
source_locationt & add_source_location()
Definition: expr.h:235
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
The Boolean constant false.
Definition: std_expr.h:2811
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:126
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:125
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1344
exprt & index()
Definition: std_expr.h:1354
Unbounded, signed integers (mathematical integers, not bitvectors)
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
const irep_idt & id() const
Definition: irep.h:407
Determine whether an expression is constant.
Definition: expr_util.h:85
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:225
Extract member of struct or union.
Definition: std_expr.h:2613
const exprt & compound() const
Definition: std_expr.h:2654
irep_idt get_component_name() const
Definition: std_expr.h:2627
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Boolean negation.
Definition: std_expr.h:2127
Replace expression or type symbols by an expression or type, respectively.
const expr_mapt & get_expr_map() const
std::unordered_map< irep_idt, exprt > expr_mapt
bool replaces_symbol(const irep_idt &id) const
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Symbol table entry.
Definition: symbol.h:28
bool is_static_lifetime
Definition: symbol.h:65
typet type
Type of symbol.
Definition: symbol.h:31
The Boolean constant true.
Definition: std_expr.h:2802
Semantic type conversion.
Definition: std_expr.h:1866
The type of an expression, extends irept.
Definition: type.h:28
const exprt & op() const
Definition: std_expr.h:293
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
exprt & where()
Definition: std_expr.h:2278
static void replace_typecast_of_bool(exprt &lhs, exprt &rhs, const namespacet &ns)
Constant propagation.
#define CPROVER_PREFIX
bool is_empty(const std::string &s)
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
Deprecated expression utility functions.
static format_containert< T > format(const T &o)
Definition: format.h:37
#define Forall_goto_program_instructions(it, program)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Mathematical types.
bool simplify(exprt &expr, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1874
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1308
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2152
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
bool is_constant(const exprt &expr) const
bool meet(const valuest &src, const namespacet &ns)
meet
void output(std::ostream &out, const namespacet &ns) const
void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns)
address_of_aware_replace_symbolt replace_const
void set_to(const symbol_exprt &lhs, const exprt &rhs)