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  trace_ptrt trace_from,
126  const irep_idt &function_to,
127  trace_ptrt trace_to,
128  ai_baset &ai,
129  const namespacet &ns)
130 {
131  locationt from{trace_from->current_location()};
132  locationt to{trace_to->current_location()};
133 
134 #ifdef DEBUG
135  std::cout << "Transform from/to:\n";
136  std::cout << from->location_number << " --> "
137  << to->location_number << '\n';
138 #endif
139 
140 #ifdef DEBUG
141  std::cout << "Before:\n";
142  output(std::cout, ai, ns);
143 #endif
144 
145  // When the domain is used with constant_propagator_ait,
146  // information about dirty variables and config flags are
147  // available. Otherwise, the below will be null and we use default
148  // values
149  const constant_propagator_ait *cp=
150  dynamic_cast<constant_propagator_ait *>(&ai);
151  bool have_dirty=(cp!=nullptr);
152 
153  // Transform on a domain that is bottom is possible
154  // if a branch is impossible the target can still wind
155  // up on the work list.
156  if(values.is_bottom)
157  return;
158 
159  if(from->is_decl())
160  {
161  const symbol_exprt &symbol = from->decl_symbol();
162  values.set_to_top(symbol);
163  }
164  else if(from->is_assign())
165  {
166  const auto &assignment = from->get_assign();
167  const exprt &lhs=assignment.lhs();
168  const exprt &rhs=assignment.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 auto &function_call = from->get_function_call();
198  const exprt &function=function_call.function();
199 
200  if(function.id()==ID_symbol)
201  {
202  // called function identifier
203  const symbol_exprt &symbol_expr=to_symbol_expr(function);
204  const irep_idt id=symbol_expr.get_identifier();
205 
206  // Functions with no body
207  if(function_from == function_to)
208  {
209  if(id==CPROVER_PREFIX "set_must" ||
210  id==CPROVER_PREFIX "get_must" ||
211  id==CPROVER_PREFIX "set_may" ||
212  id==CPROVER_PREFIX "get_may" ||
213  id==CPROVER_PREFIX "cleanup" ||
214  id==CPROVER_PREFIX "clear_may" ||
215  id==CPROVER_PREFIX "clear_must")
216  {
217  // no effect on constants
218  }
219  else
220  {
221  if(have_dirty)
222  values.set_dirty_to_top(cp->dirty, ns);
223  else
224  values.set_to_top();
225  }
226  }
227  else
228  {
229  // we have an actual call
230 
231  // parameters of called function
232  const symbolt &symbol=ns.lookup(id);
233  const code_typet &code_type=to_code_type(symbol.type);
234  const code_typet::parameterst &parameters=code_type.parameters();
235 
236  const code_function_callt::argumentst &arguments=
237  function_call.arguments();
238 
239  code_typet::parameterst::const_iterator p_it=parameters.begin();
240  for(const auto &arg : arguments)
241  {
242  if(p_it==parameters.end())
243  break;
244 
245  const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
246  assign_rec(values, parameter_expr, arg, ns, cp, true);
247 
248  ++p_it;
249  }
250  }
251  }
252  else
253  {
254  // unresolved call
255  INVARIANT(
256  function_from == function_to,
257  "Unresolved call can only be approximated if a skip");
258 
259  if(have_dirty)
260  values.set_dirty_to_top(cp->dirty, ns);
261  else
262  values.set_to_top();
263  }
264  }
265  else if(from->is_end_function())
266  {
267  // erase parameters
268 
269  const irep_idt id = function_from;
270  const symbolt &symbol=ns.lookup(id);
271 
272  const code_typet &type=to_code_type(symbol.type);
273 
274  for(const auto &param : type.parameters())
275  values.set_to_top(symbol_exprt(param.get_identifier(), param.type()));
276  }
277 
278  INVARIANT(from->is_goto() || !values.is_bottom,
279  "Transform only sets bottom by using branch conditions");
280 
281 #ifdef DEBUG
282  std::cout << "After:\n";
283  output(std::cout, ai, ns);
284 #endif
285 }
286 
287 static void
289 {
290  // (int)var xx 0 ==> var xx (_Bool)0 or similar (xx is == or !=)
291  // Note this is restricted to bools because in general turning a widening
292  // into a narrowing typecast is not correct.
293  if(lhs.id() != ID_typecast)
294  return;
295 
296  const exprt &lhs_underlying = to_typecast_expr(lhs).op();
297  if(
298  lhs_underlying.type() == bool_typet() ||
299  lhs_underlying.type() == c_bool_type())
300  {
301  rhs = typecast_exprt(rhs, lhs_underlying.type());
302  simplify(rhs, ns);
303 
304  lhs = lhs_underlying;
305  }
306 }
307 
310  const exprt &expr,
311  const namespacet &ns,
312  const constant_propagator_ait *cp)
313 {
314 #ifdef DEBUG
315  std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
316 #endif
317 
318  bool change=false;
319 
320  if(expr.id()==ID_and)
321  {
322  // need a fixed point here to get the most out of it
323  bool change_this_time;
324  do
325  {
326  change_this_time = false;
327 
328  forall_operands(it, expr)
329  {
330  change_this_time |= two_way_propagate_rec(*it, ns, cp);
331  if(change_this_time)
332  change = true;
333  }
334  } while(change_this_time);
335  }
336  else if(expr.id() == ID_not)
337  {
338  const auto &op = to_not_expr(expr).op();
339 
340  if(op.id() == ID_equal || op.id() == ID_notequal)
341  {
342  exprt subexpr = op;
343  subexpr.id(subexpr.id() == ID_equal ? ID_notequal : ID_equal);
344  change = two_way_propagate_rec(subexpr, ns, cp);
345  }
346  else if(op.id() == ID_symbol && expr.type() == bool_typet())
347  {
348  // Treat `IF !x` like `IF x == FALSE`:
349  change = two_way_propagate_rec(equal_exprt(op, false_exprt()), ns, cp);
350  }
351  }
352  else if(expr.id() == ID_symbol)
353  {
354  if(expr.type() == bool_typet())
355  {
356  // Treat `IF x` like `IF x == TRUE`:
357  change = two_way_propagate_rec(equal_exprt(expr, true_exprt()), ns, cp);
358  }
359  }
360  else if(expr.id() == ID_notequal)
361  {
362  // Treat "symbol != constant" like "symbol == !constant" when the constant
363  // is a boolean.
364  exprt lhs = to_notequal_expr(expr).lhs();
365  exprt rhs = to_notequal_expr(expr).rhs();
366 
367  if(lhs.is_constant() && !rhs.is_constant())
368  std::swap(lhs, rhs);
369 
370  if(lhs.is_constant() || !rhs.is_constant())
371  return false;
372 
373  replace_typecast_of_bool(lhs, rhs, ns);
374 
375  if(lhs.type() != bool_typet() && lhs.type() != c_bool_type())
376  return false;
377 
378  // x != FALSE ==> x == TRUE
379 
380  if(rhs.is_zero() || rhs.is_false())
381  rhs = from_integer(1, rhs.type());
382  else
383  rhs = from_integer(0, rhs.type());
384 
385  change = two_way_propagate_rec(equal_exprt(lhs, rhs), ns, cp);
386  }
387  else if(expr.id() == ID_equal)
388  {
389  exprt lhs = to_equal_expr(expr).lhs();
390  exprt rhs = to_equal_expr(expr).rhs();
391 
392  replace_typecast_of_bool(lhs, rhs, ns);
393 
394  // two-way propagation
395  valuest copy_values=values;
396  assign_rec(copy_values, lhs, rhs, ns, cp, false);
397  if(!values.is_constant(rhs) || values.is_constant(lhs))
398  assign_rec(values, rhs, lhs, ns, cp, false);
399  change = values.meet(copy_values, ns);
400  }
401 
402 #ifdef DEBUG
403  std::cout << "two_way_propagate_rec: " << change << '\n';
404 #endif
405 
406  return change;
407 }
408 
414  exprt &condition,
415  const namespacet &ns) const
416 {
417  return partial_evaluate(values, condition, ns);
418 }
419 
421 {
422 public:
426  {
427  }
428 
429  bool is_constant(const irep_idt &id) const
430  {
431  return replace_const.replaces_symbol(id);
432  }
433 
434 protected:
435  bool is_constant(const exprt &expr) const override
436  {
437  if(expr.id() == ID_symbol)
438  return is_constant(to_symbol_expr(expr).get_identifier());
439 
440  return is_constantt::is_constant(expr);
441  }
442 
444 };
445 
447 {
449 }
450 
452 {
453  return constant_propagator_is_constantt(replace_const).is_constant(id);
454 }
455 
458  const symbol_exprt &symbol_expr)
459 {
460  const auto n_erased = replace_const.erase(symbol_expr.get_identifier());
461 
462  INVARIANT(n_erased==0 || !is_bottom, "bottom should have no elements at all");
463 
464  return n_erased>0;
465 }
466 
467 
469  const dirtyt &dirty,
470  const namespacet &ns)
471 {
473  expr_mapt &expr_map = replace_const.get_expr_map();
474 
475  for(expr_mapt::iterator it=expr_map.begin();
476  it!=expr_map.end();)
477  {
478  const irep_idt id=it->first;
479 
480  const symbolt &symbol=ns.lookup(id);
481 
482  if(
483  (symbol.is_static_lifetime || dirty(id)) &&
484  !symbol.type.get_bool(ID_C_constant))
485  {
486  it = replace_const.erase(it);
487  }
488  else
489  it++;
490  }
491 }
492 
494  std::ostream &out,
495  const namespacet &ns) const
496 {
497  out << "const map:\n";
498 
499  if(is_bottom)
500  {
501  out << " bottom\n";
503  "If the domain is bottom, the map must be empty");
504  return;
505  }
506 
507  INVARIANT(!is_bottom, "Have handled bottom");
508  if(is_empty())
509  {
510  out << "top\n";
511  return;
512  }
513 
514  for(const auto &p : replace_const.get_expr_map())
515  {
516  out << ' ' << p.first << "=" << from_expr(ns, p.first, p.second) << '\n';
517  }
518 }
519 
521  std::ostream &out,
522  const ai_baset &,
523  const namespacet &ns) const
524 {
525  values.output(out, ns);
526 }
527 
531 {
532  // nothing to do
533  if(src.is_bottom)
534  return false;
535 
536  // just copy
537  if(is_bottom)
538  {
539  PRECONDITION(!src.is_bottom);
540  replace_const=src.replace_const; // copy
541  is_bottom=false;
542  return true;
543  }
544 
545  INVARIANT(!is_bottom && !src.is_bottom, "Case handled");
546 
547  bool changed=false;
548 
549  // handle top
550  if(src.is_empty())
551  {
552  // change if it was not top
553  changed = !is_empty();
554 
555  set_to_top();
556 
557  return changed;
558  }
559 
560  replace_symbolt::expr_mapt &expr_map = replace_const.get_expr_map();
561  const replace_symbolt::expr_mapt &src_expr_map =
563 
564  // remove those that are
565  // - different in src
566  // - do not exist in src
567  for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
568  it!=expr_map.end();)
569  {
570  const irep_idt id=it->first;
571  const exprt &expr=it->second;
572 
573  replace_symbolt::expr_mapt::const_iterator s_it;
574  s_it=src_expr_map.find(id);
575 
576  if(s_it!=src_expr_map.end())
577  {
578  // check value
579  const exprt &src_expr=s_it->second;
580 
581  if(expr!=src_expr)
582  {
583  it = replace_const.erase(it);
584  changed=true;
585  }
586  else
587  it++;
588  }
589  else
590  {
591  it = replace_const.erase(it);
592  changed=true;
593  }
594  }
595 
596  return changed;
597 }
598 
602  const valuest &src,
603  const namespacet &ns)
604 {
605  if(src.is_bottom || is_bottom)
606  return false;
607 
608  bool changed=false;
609 
610  for(const auto &m : src.replace_const.get_expr_map())
611  {
612  replace_symbolt::expr_mapt::const_iterator c_it =
613  replace_const.get_expr_map().find(m.first);
614 
615  if(c_it != replace_const.get_expr_map().end())
616  {
617  if(c_it->second!=m.second)
618  {
619  set_to_bottom();
620  changed=true;
621  break;
622  }
623  }
624  else
625  {
626  const typet &m_id_type = ns.lookup(m.first).type;
628  m_id_type == m.second.type(),
629  "type of constant to be stored should match");
630  set_to(symbol_exprt(m.first, m_id_type), m.second);
631  changed=true;
632  }
633  }
634 
635  return changed;
636 }
637 
640  const constant_propagator_domaint &other,
641  locationt,
642  locationt)
643 {
644  return values.merge(other.values);
645 }
646 
654  const valuest &known_values,
655  exprt &expr,
656  const namespacet &ns)
657 {
658  // if the current rounding mode is top we can
659  // still get a non-top result by trying all rounding
660  // modes and checking if the results are all the same
661  if(!known_values.is_constant(ID_cprover_rounding_mode_str))
662  return partial_evaluate_with_all_rounding_modes(known_values, expr, ns);
663 
664  return replace_constants_and_simplify(known_values, expr, ns);
665 }
666 
675  const valuest &known_values,
676  exprt &expr,
677  const namespacet &ns)
678 { // NOLINTNEXTLINE (whitespace/braces)
679  auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
680  // NOLINTNEXTLINE (whitespace/braces)
684  // NOLINTNEXTLINE (whitespace/braces)
686  exprt first_result;
687  for(std::size_t i = 0; i < rounding_modes.size(); ++i)
688  {
689  valuest tmp_values = known_values;
690  tmp_values.set_to(
692  from_integer(rounding_modes[i], integer_typet()));
693  exprt result = expr;
694  if(replace_constants_and_simplify(tmp_values, result, ns))
695  {
696  return true;
697  }
698  else if(i == 0)
699  {
700  first_result = result;
701  }
702  else if(result != first_result)
703  {
704  return true;
705  }
706  }
707  expr = first_result;
708  return false;
709 }
710 
712  const valuest &known_values,
713  exprt &expr,
714  const namespacet &ns)
715 {
716  bool did_not_change_anything = true;
717 
718  // iterate constant propagation and simplification until we cannot
719  // constant-propagate any further - a prime example is pointer dereferencing,
720  // where constant propagation may have a value of the pointer, the simplifier
721  // takes care of evaluating dereferencing, and we might then have the value of
722  // the resulting symbol known to constant propagation and thus replace the
723  // dereferenced expression by a constant
724  while(!known_values.replace_const.replace(expr))
725  {
726  did_not_change_anything = false;
727  simplify(expr, ns);
728  }
729 
730  // even if we haven't been able to constant-propagate anything, run the
731  // simplifier on the expression
732  if(did_not_change_anything)
733  did_not_change_anything &= simplify(expr, ns);
734 
735  return did_not_change_anything;
736 }
737 
739  goto_functionst &goto_functions,
740  const namespacet &ns)
741 {
742  for(auto &gf_entry : goto_functions.function_map)
743  replace(gf_entry.second, ns);
744 }
745 
746 
748  goto_functionst::goto_functiont &goto_function,
749  const namespacet &ns)
750 {
751  Forall_goto_program_instructions(it, goto_function.body)
752  {
753  auto const current_domain_ptr =
754  std::dynamic_pointer_cast<const constant_propagator_domaint>(
755  this->abstract_state_before(it));
756  const constant_propagator_domaint &d = *current_domain_ptr;
757 
758  if(d.is_bottom())
759  continue;
760 
761  replace_types_rec(d.values.replace_const, it->code);
762 
763  if(it->is_goto() || it->is_assume() || it->is_assert())
764  {
765  exprt c = it->get_condition();
766  replace_types_rec(d.values.replace_const, c);
768  it->set_condition(c);
769  }
770  else if(it->is_assign())
771  {
772  auto assign = it->get_assign();
773  exprt &rhs = assign.rhs();
774 
776  {
777  if(rhs.id() == ID_constant)
778  rhs.add_source_location() = assign.lhs().source_location();
779  it->set_assign(assign);
780  }
781  }
782  else if(it->is_function_call())
783  {
784  auto call = it->get_function_call();
785 
786  bool call_changed = false;
787 
789  d.values, call.function(), ns))
790  {
791  call_changed = true;
792  }
793 
794  for(auto &arg : call.arguments())
796  call_changed = true;
797 
798  if(call_changed)
799  it->set_function_call(call);
800  }
801  else if(it->is_other())
802  {
803  if(it->get_other().get_statement() == ID_expression)
804  {
805  auto c = to_code_expression(it->get_other());
807  d.values, c.expression(), ns))
808  {
809  it->set_other(c);
810  }
811  }
812  }
813  }
814 }
815 
817  const replace_symbolt &replace_const,
818  exprt &expr)
819 {
820  replace_const(expr.type());
821 
822  Forall_operands(it, expr)
823  replace_types_rec(replace_const, *it);
824 }
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
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:120
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
goto_programt::const_targett locationt
Definition: ai_domain.h:77
exprt & lhs()
Definition: std_expr.h:581
exprt & rhs()
Definition: std_expr.h:591
The Boolean type.
Definition: std_types.h:37
exprt::operandst argumentst
Definition: std_code.h:1224
Base type of functions.
Definition: std_types.h:744
std::vector< parametert > parameterst
Definition: std_types.h:746
const parameterst & parameters() const
Definition: std_types.h:860
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
bool merge(const constant_propagator_domaint &other, locationt from, locationt to)
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
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:1140
Base class for all expressions.
Definition: expr.h:54
source_locationt & add_source_location()
Definition: expr.h:239
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:78
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:40
The Boolean constant false.
Definition: std_expr.h:2726
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:128
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:127
Array index operator.
Definition: std_expr.h:1243
exprt & array()
Definition: std_expr.h:1259
exprt & index()
Definition: std_expr.h:1269
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:64
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
const irep_idt & id() const
Definition: irep.h:407
Determine whether an expression is constant.
Definition: expr_util.h:87
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:228
Extract member of struct or union.
Definition: std_expr.h:2528
const exprt & compound() const
Definition: std_expr.h:2569
irep_idt get_component_name() const
Definition: std_expr.h:2542
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
Boolean negation.
Definition: std_expr.h:2042
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:81
const irep_idt & get_identifier() const
Definition: std_expr.h:110
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:2717
Semantic type conversion.
Definition: std_expr.h:1781
The type of an expression, extends irept.
Definition: type.h:28
const exprt & op() const
Definition: std_expr.h:294
Operator to update elements in structs and arrays.
Definition: std_expr.h:2173
exprt & where()
Definition: std_expr.h:2193
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)
const char ID_cprover_rounding_mode_str[]
Definition: ieee_float.h:23
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:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1876
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1223
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2067
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1180
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
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)