cprover
goto_symex_state.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_symex_state.h"
13 
14 #include <cstdlib>
15 #include <iostream>
16 
17 #include <util/base_exceptions.h>
18 #include <util/exception_utils.h>
19 #include <util/expr_util.h>
20 #include <util/format.h>
21 #include <util/format_expr.h>
22 #include <util/invariant.h>
23 #include <util/prefix.h>
24 #include <util/std_expr.h>
25 
26 #include <analyses/dirty.h>
27 
28 static void get_l1_name(exprt &expr);
29 
31  : depth(0),
32  symex_target(nullptr),
33  atomic_section_id(0),
34  total_vccs(0),
35  remaining_vccs(0),
36  record_events(true),
37  dirty()
38 {
39  threads.resize(1);
40  new_frame();
41 }
42 
44 
46 static bool check_renaming(const exprt &expr);
47 
48 static bool check_renaming(const typet &type)
49 {
50  if(type.id()==ID_array)
51  return check_renaming(to_array_type(type).size());
52  else if(type.id()==ID_struct ||
53  type.id()==ID_union ||
54  type.id()==ID_class)
55  {
56  for(const auto &c : to_struct_union_type(type).components())
57  if(check_renaming(c.type()))
58  return true;
59  }
60  else if(type.has_subtype())
62 
63  return false;
64 }
65 
66 static bool check_renaming_l1(const exprt &expr)
67 {
68  if(check_renaming(expr.type()))
69  return true;
70 
71  if(expr.id()==ID_symbol)
72  {
73  if(!expr.get_bool(ID_C_SSA_symbol))
74  return expr.type().id()!=ID_code;
75  if(!to_ssa_expr(expr).get_level_2().empty())
76  return true;
77  if(to_ssa_expr(expr).get_original_expr().type()!=expr.type())
78  return true;
79  }
80  else
81  {
82  forall_operands(it, expr)
83  if(check_renaming_l1(*it))
84  return true;
85  }
86 
87  return false;
88 }
89 
90 static bool check_renaming(const exprt &expr)
91 {
92  if(check_renaming(expr.type()))
93  return true;
94 
95  if(
96  expr.id() == ID_address_of &&
97  to_address_of_expr(expr).object().id() == ID_symbol)
98  {
99  return check_renaming_l1(to_address_of_expr(expr).object());
100  }
101  else if(
102  expr.id() == ID_address_of &&
103  to_address_of_expr(expr).object().id() == ID_index)
104  {
105  const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
106  return check_renaming_l1(index_expr.array()) ||
107  check_renaming(index_expr.index());
108  }
109  else if(expr.id()==ID_symbol)
110  {
111  if(!expr.get_bool(ID_C_SSA_symbol))
112  return expr.type().id()!=ID_code;
113  if(to_ssa_expr(expr).get_level_2().empty())
114  return true;
115  if(to_ssa_expr(expr).get_original_expr().type()!=expr.type())
116  return true;
117  }
118  else
119  {
120  forall_operands(it, expr)
121  if(check_renaming(*it))
122  return true;
123  }
124 
125  return false;
126 }
127 
129 {
130 protected:
131  bool is_constant(const exprt &expr) const override
132  {
133  if(expr.id() == ID_mult)
134  {
135  // propagate stuff with sizeof in it
136  forall_operands(it, expr)
137  {
138  if(it->find(ID_C_c_sizeof_type).is_not_nil())
139  return true;
140  else if(!is_constant(*it))
141  return false;
142  }
143 
144  return true;
145  }
146  else if(expr.id() == ID_with)
147  {
148  // this is bad
149  /*
150  forall_operands(it, expr)
151  if(!is_constant(expr.op0()))
152  return false;
153 
154  return true;
155  */
156  return false;
157  }
158 
159  return is_constantt::is_constant(expr);
160  }
161 };
162 
164  ssa_exprt &lhs, // L0/L1
165  const exprt &rhs, // L2
166  const namespacet &ns,
167  bool rhs_is_simplified,
168  bool record_value,
169  bool allow_pointer_unsoundness)
170 {
171  // identifier should be l0 or l1, make sure it's l1
172  rename(lhs, ns, L1);
173  irep_idt l1_identifier=lhs.get_identifier();
174 
175  // the type might need renaming
176  rename(lhs.type(), l1_identifier, ns);
177  lhs.update_type();
179  {
180  DATA_INVARIANT(!check_renaming_l1(lhs), "lhs renaming failed on l1");
181  }
182 
183 #if 0
184  PRECONDITION(l1_identifier != get_original_name(l1_identifier)
185  || l1_identifier=="goto_symex::\\guard"
186  || ns.lookup(l1_identifier).is_shared()
187  || has_prefix(id2string(l1_identifier), "symex::invalid_object")
188  || has_prefix(id2string(l1_identifier), "symex_dynamic::dynamic_object"));
189 #endif
190 
191  // do the l2 renaming
192  const auto level2_it =
193  level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0)).first;
195  set_l2_indices(lhs, ns);
196 
197  // in case we happen to be multi-threaded, record the memory access
198  bool is_shared=l2_thread_write_encoding(lhs, ns);
199 
201  {
202  DATA_INVARIANT(!check_renaming(lhs), "lhs renaming failed on l2");
203  DATA_INVARIANT(!check_renaming(rhs), "rhs renaming failed on l2");
204  }
205 
206  // see #305 on GitHub for a simple example and possible discussion
207  if(is_shared && lhs.type().id() == ID_pointer && !allow_pointer_unsoundness)
209  "pointer handling for concurrency is unsound");
210 
211  // for value propagation -- the RHS is L2
212 
213  if(!is_shared && record_value && goto_symex_is_constantt()(rhs))
214  propagation[l1_identifier] = rhs;
215  else
216  propagation.erase(l1_identifier);
217 
218  {
219  // update value sets
220  value_sett::expr_sett rhs_value_set;
221  exprt l1_rhs(rhs);
222  get_l1_name(l1_rhs);
223 
224  ssa_exprt l1_lhs(lhs);
225  l1_lhs.remove_level_2();
226 
228  {
229  DATA_INVARIANT(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
230  DATA_INVARIANT(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
231  }
232 
233  value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
234  }
235 
236  #if 0
237  std::cout << "Assigning " << l1_identifier << '\n';
238  value_set.output(ns, std::cout);
239  std::cout << "**********************\n";
240  #endif
241 }
242 
244  ssa_exprt &ssa_expr,
245  const namespacet &ns)
246 {
247  level0(ssa_expr, ns, source.thread_nr);
248 }
249 
251  ssa_exprt &ssa_expr,
252  const namespacet &ns)
253 {
254  if(!ssa_expr.get_level_2().empty())
255  return;
256  if(!ssa_expr.get_level_1().empty())
257  return;
258  level0(ssa_expr, ns, source.thread_nr);
259  level1(ssa_expr);
260 }
261 
263  ssa_exprt &ssa_expr,
264  const namespacet &ns)
265 {
266  if(!ssa_expr.get_level_2().empty())
267  return;
268  level0(ssa_expr, ns, source.thread_nr);
269  level1(ssa_expr);
270  ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
271 }
272 
274  exprt &expr,
275  const namespacet &ns,
276  levelt level)
277 {
278  // rename all the symbols with their last known value
279 
280  if(expr.id()==ID_symbol &&
281  expr.get_bool(ID_C_SSA_symbol))
282  {
283  ssa_exprt &ssa=to_ssa_expr(expr);
284 
285  if(level == L0)
286  {
287  set_l0_indices(ssa, ns);
288  rename(expr.type(), ssa.get_identifier(), ns, level);
289  ssa.update_type();
290  }
291  else if(level == L1)
292  {
293  set_l1_indices(ssa, ns);
294  rename(expr.type(), ssa.get_identifier(), ns, level);
295  ssa.update_type();
296  }
297  else if(level==L2)
298  {
299  set_l1_indices(ssa, ns);
300  rename(expr.type(), ssa.get_identifier(), ns, level);
301  ssa.update_type();
302 
303  if(l2_thread_read_encoding(ssa, ns))
304  {
305  // renaming taken care of by l2_thread_encoding
306  }
307  else if(!ssa.get_level_2().empty())
308  {
309  // already at L2
310  }
311  else
312  {
313  // We also consider propagation if we go up to L2.
314  // L1 identifiers are used for propagation!
315  auto p_it = propagation.find(ssa.get_identifier());
316 
317  if(p_it != propagation.end())
318  expr=p_it->second; // already L2
319  else
320  set_l2_indices(ssa, ns);
321  }
322  }
323  }
324  else if(expr.id()==ID_symbol)
325  {
326  // we never rename function symbols
327  if(ns.follow(expr.type()).id()==ID_code)
328  {
329  rename(
330  expr.type(),
332  ns,
333  level);
334 
335  return;
336  }
337 
338  expr=ssa_exprt(expr);
339  rename(expr, ns, level);
340  }
341  else if(expr.id()==ID_address_of)
342  {
343  auto &address_of_expr = to_address_of_expr(expr);
344  rename_address(address_of_expr.object(), ns, level);
345  to_pointer_type(expr.type()).subtype() = address_of_expr.object().type();
346  }
347  else
348  {
349  // this could go wrong, but we would have to re-typecheck ...
350  rename(expr.type(), irep_idt(), ns, level);
351 
352  // do this recursively
353  Forall_operands(it, expr)
354  rename(*it, ns, level);
355 
356  // some fixes
357  if(expr.id()==ID_with)
358  expr.type()=to_with_expr(expr).old().type();
359  else if(expr.id()==ID_if)
360  {
362  to_if_expr(expr).true_case().type() ==
363  to_if_expr(expr).false_case().type(),
364  "true case of to_if_expr should be of same type "
365  "as false case");
366  expr.type()=to_if_expr(expr).true_case().type();
367  }
368  }
369 }
370 
373  ssa_exprt &expr,
374  const namespacet &ns)
375 {
376  // do we have threads?
377  if(threads.size()<=1)
378  return false;
379 
380  // is it a shared object?
381  const irep_idt &obj_identifier=expr.get_object_name();
382  if(
383  obj_identifier == "goto_symex::\\guard" ||
384  (!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier)))
385  return false;
386 
387  ssa_exprt ssa_l1=expr;
388  ssa_l1.remove_level_2();
389  const irep_idt &l1_identifier=ssa_l1.get_identifier();
390 
391  // see whether we are within an atomic section
392  if(atomic_section_id!=0)
393  {
394  guardt write_guard;
395  write_guard.add(false_exprt());
396 
397  const auto a_s_writes = written_in_atomic_section.find(ssa_l1);
398  if(a_s_writes!=written_in_atomic_section.end())
399  {
400  for(const auto &guard_in_list : a_s_writes->second)
401  {
402  guardt g = guard_in_list;
403  g-=guard;
404  if(g.is_true())
405  // there has already been a write to l1_identifier within
406  // this atomic section under the same guard, or a guard
407  // that implies the current one
408  return false;
409 
410  write_guard |= guard_in_list;
411  }
412  }
413 
414  not_exprt no_write(write_guard.as_expr());
415 
416  // we cannot determine for sure that there has been a write already
417  // so generate a read even if l1_identifier has been written on
418  // all branches flowing into this read
419  guardt read_guard;
420  read_guard.add(false_exprt());
421 
422  a_s_r_entryt &a_s_read=read_in_atomic_section[ssa_l1];
423  for(std::list<guardt>::const_iterator it=a_s_read.second.begin();
424  it!=a_s_read.second.end();
425  ++it)
426  {
427  guardt g=*it;
428  g-=guard;
429  if(g.is_true())
430  // there has already been a read l1_identifier within
431  // this atomic section under the same guard, or a guard
432  // that implies the current one
433  return false;
434 
435  read_guard|=*it;
436  }
437 
438  exprt cond=read_guard.as_expr();
439  if(!no_write.op().is_false())
440  cond=or_exprt(no_write.op(), cond);
441 
442  if_exprt tmp(cond, ssa_l1, ssa_l1);
444 
445  if(a_s_read.second.empty())
446  {
447  auto level2_it =
448  level2.current_names.emplace(l1_identifier, std::make_pair(ssa_l1, 0))
449  .first;
451  a_s_read.first=level2.current_count(l1_identifier);
452  }
453 
454  to_ssa_expr(tmp.false_case()).set_level_2(a_s_read.first);
455 
456  if(cond.is_false())
457  {
458  exprt t=tmp.false_case();
459  t.swap(tmp);
460  }
461 
462  const bool record_events_bak=record_events;
463  record_events=false;
464  assignment(ssa_l1, tmp, ns, true, true);
465  record_events=record_events_bak;
466 
468  guard.as_expr(),
469  ssa_l1,
470  ssa_l1,
471  ssa_l1.get_original_expr(),
472  tmp,
473  source,
475 
476  set_l2_indices(ssa_l1, ns);
477  expr=ssa_l1;
478 
479  a_s_read.second.push_back(guard);
480  if(!no_write.op().is_false())
481  a_s_read.second.back().add(no_write);
482 
483  return true;
484  }
485 
486  const auto level2_it =
487  level2.current_names.emplace(l1_identifier, std::make_pair(ssa_l1, 0))
488  .first;
489 
490  // No event and no fresh index, but avoid constant propagation
491  if(!record_events)
492  {
493  set_l2_indices(ssa_l1, ns);
494  expr=ssa_l1;
495  return true;
496  }
497 
498  // produce a fresh L2 name
500  set_l2_indices(ssa_l1, ns);
501  expr=ssa_l1;
502 
503  // and record that
505  symex_target!=nullptr, nullptr_exceptiont, "symex_target is null");
507  guard.as_expr(),
508  expr,
510  source);
511 
512  return true;
513 }
514 
517  const ssa_exprt &expr,
518  const namespacet &ns)
519 {
520  if(!record_events)
521  return false;
522 
523  // is it a shared object?
524  const irep_idt &obj_identifier=expr.get_object_name();
525  if(
526  obj_identifier == "goto_symex::\\guard" ||
527  (!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier)))
528  return false; // not shared
529 
530  // see whether we are within an atomic section
531  if(atomic_section_id!=0)
532  {
533  ssa_exprt ssa_l1=expr;
534  ssa_l1.remove_level_2();
535 
536  written_in_atomic_section[ssa_l1].push_back(guard);
537  return false;
538  }
539 
540  // record a shared write
542  guard.as_expr(),
543  expr,
545  source);
546 
547  // do we have threads?
548  return threads.size()>1;
549 }
550 
552  exprt &expr,
553  const namespacet &ns,
554  levelt level)
555 {
556  if(expr.id()==ID_symbol &&
557  expr.get_bool(ID_C_SSA_symbol))
558  {
559  ssa_exprt &ssa=to_ssa_expr(expr);
560 
561  // only do L1!
562  set_l1_indices(ssa, ns);
563 
564  rename(expr.type(), ssa.get_identifier(), ns, level);
565  ssa.update_type();
566  }
567  else if(expr.id()==ID_symbol)
568  {
569  expr=ssa_exprt(expr);
570  rename_address(expr, ns, level);
571  }
572  else
573  {
574  if(expr.id()==ID_index)
575  {
576  index_exprt &index_expr=to_index_expr(expr);
577 
578  rename_address(index_expr.array(), ns, level);
579  PRECONDITION(index_expr.array().type().id() == ID_array);
580  expr.type() = to_array_type(index_expr.array().type()).subtype();
581 
582  // the index is not an address
583  rename(index_expr.index(), ns, level);
584  }
585  else if(expr.id()==ID_if)
586  {
587  // the condition is not an address
588  if_exprt &if_expr=to_if_expr(expr);
589  rename(if_expr.cond(), ns, level);
590  rename_address(if_expr.true_case(), ns, level);
591  rename_address(if_expr.false_case(), ns, level);
592 
593  if_expr.type()=if_expr.true_case().type();
594  }
595  else if(expr.id()==ID_member)
596  {
597  member_exprt &member_expr=to_member_expr(expr);
598 
599  rename_address(member_expr.struct_op(), ns, level);
600 
601  // type might not have been renamed in case of nesting of
602  // structs and pointers/arrays
603  if(
604  member_expr.struct_op().type().id() != ID_symbol_type &&
605  member_expr.struct_op().type().id() != ID_struct_tag &&
606  member_expr.struct_op().type().id() != ID_union_tag)
607  {
608  const struct_union_typet &su_type=
609  to_struct_union_type(member_expr.struct_op().type());
610  const struct_union_typet::componentt &comp=
611  su_type.get_component(member_expr.get_component_name());
612  PRECONDITION(comp.is_not_nil());
613  expr.type()=comp.type();
614  }
615  else
616  rename(expr.type(), irep_idt(), ns, level);
617  }
618  else
619  {
620  // this could go wrong, but we would have to re-typecheck ...
621  rename(expr.type(), irep_idt(), ns, level);
622 
623  // do this recursively; we assume here
624  // that all the operands are addresses
625  Forall_operands(it, expr)
626  rename_address(*it, ns, level);
627  }
628  }
629 }
630 
632  typet &type,
633  const irep_idt &l1_identifier,
634  const namespacet &ns,
635  levelt level)
636 {
637  // rename all the symbols with their last known value
638  // to the given level
639 
640  std::pair<l1_typest::iterator, bool> l1_type_entry;
641  if(level==L2 &&
642  !l1_identifier.empty())
643  {
644  l1_type_entry=l1_types.insert(std::make_pair(l1_identifier, type));
645 
646  if(!l1_type_entry.second) // was already in map
647  {
648  // do not change a complete array type to an incomplete one
649 
650  const typet &type_prev=l1_type_entry.first->second;
651 
652  if(type.id()!=ID_array ||
653  type_prev.id()!=ID_array ||
654  to_array_type(type).is_incomplete() ||
655  to_array_type(type_prev).is_complete())
656  {
657  type=l1_type_entry.first->second;
658  return;
659  }
660  }
661  }
662 
663  if(type.id()==ID_array)
664  {
665  auto &array_type = to_array_type(type);
666  rename(array_type.subtype(), irep_idt(), ns, level);
667  rename(array_type.size(), ns, level);
668  }
669  else if(type.id()==ID_struct ||
670  type.id()==ID_union ||
671  type.id()==ID_class)
672  {
674  struct_union_typet::componentst &components=s_u_type.components();
675 
676  for(struct_union_typet::componentst::iterator
677  it=components.begin();
678  it!=components.end();
679  ++it)
680  // be careful, or it might get cyclic
681  if(it->type().id()==ID_array)
682  rename(to_array_type(it->type()).size(), ns, level);
683  else if(it->type().id()!=ID_pointer)
684  rename(it->type(), irep_idt(), ns, level);
685  }
686  else if(type.id()==ID_pointer)
687  {
688  rename(to_pointer_type(type).subtype(), irep_idt(), ns, level);
689  }
690  else if(type.id() == ID_symbol_type)
691  {
692  const symbolt &symbol = ns.lookup(to_symbol_type(type));
693  type = symbol.type;
694  rename(type, l1_identifier, ns, level);
695  }
696  else if(type.id() == ID_union_tag)
697  {
698  const symbolt &symbol = ns.lookup(to_union_tag_type(type));
699  type = symbol.type;
700  rename(type, l1_identifier, ns, level);
701  }
702  else if(type.id() == ID_struct_tag)
703  {
704  const symbolt &symbol = ns.lookup(to_struct_tag_type(type));
705  type=symbol.type;
706  rename(type, l1_identifier, ns, level);
707  }
708 
709  if(level==L2 &&
710  !l1_identifier.empty())
711  l1_type_entry.first->second=type;
712 }
713 
715 {
716  get_original_name(expr.type());
717 
718  if(expr.id()==ID_symbol &&
719  expr.get_bool(ID_C_SSA_symbol))
720  expr=to_ssa_expr(expr).get_original_expr();
721  else
722  Forall_operands(it, expr)
723  get_original_name(*it);
724 }
725 
727 {
728  // rename all the symbols with their last known value
729 
730  if(type.id()==ID_array)
731  {
732  auto &array_type = to_array_type(type);
733  get_original_name(array_type.subtype());
734  get_original_name(array_type.size());
735  }
736  else if(type.id()==ID_struct ||
737  type.id()==ID_union ||
738  type.id()==ID_class)
739  {
741  struct_union_typet::componentst &components=s_u_type.components();
742 
743  for(struct_union_typet::componentst::iterator
744  it=components.begin();
745  it!=components.end();
746  ++it)
747  get_original_name(it->type());
748  }
749  else if(type.id()==ID_pointer)
750  {
751  get_original_name(to_pointer_type(type).subtype());
752  }
753 }
754 
755 static void get_l1_name(exprt &expr)
756 {
757  // do not reset the type !
758 
759  if(expr.id()==ID_symbol &&
760  expr.get_bool(ID_C_SSA_symbol))
761  to_ssa_expr(expr).remove_level_2();
762  else
763  Forall_operands(it, expr)
764  get_l1_name(*it);
765 }
766 
772 void goto_symex_statet::print_backtrace(std::ostream &out) const
773 {
774  if(threads[source.thread_nr].call_stack.empty())
775  {
776  out << "No stack!\n";
777  return;
778  }
779 
780  out << source.pc->function << " " << source.pc->location_number << "\n";
781 
782  for(auto stackit = threads[source.thread_nr].call_stack.rbegin(),
783  stackend = threads[source.thread_nr].call_stack.rend();
784  stackit != stackend;
785  ++stackit)
786  {
787  const auto &frame = *stackit;
788  if(frame.calling_location.is_set)
789  {
790  out << frame.calling_location.pc->function << " "
791  << frame.calling_location.pc->location_number << "\n";
792  }
793  }
794 }
795 
800 {
801  for(const auto &name_value : propagation)
802  {
803  out << name_value.first << " <- " << format(name_value.second) << "\n";
804  }
805 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
The type of an expression, extends irept.
Definition: type.h:27
exprt as_expr() const
Definition: guard.h:41
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:382
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
Boolean negation.
Definition: std_expr.h:3308
exprt & true_case()
Definition: std_expr.h:3455
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)
thread encoding
static void increase_counter(const current_namest::iterator &it)
Increase the counter corresponding to an identifier.
goto_programt::const_targett pc
Definition: symex_target.h:41
exprt & object()
Definition: std_expr.h:3265
Boolean OR.
Definition: std_expr.h:2531
void print_backtrace(std::ostream &) const
Dumps the current state of symex, printing the function name and location number for each stack frame...
bool has_subtype() const
Definition: type.h:56
Variables whose address is taken.
Determine whether an expression is constant.
Definition: expr_util.h:86
Deprecated expression utility functions.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
bool run_validation_checks
Should the additional validation checks be run?
const irep_idt & get_identifier() const
Definition: std_expr.h:176
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Transforms this value-set by executing executing the assignment lhs := rhs against it.
Definition: value_set.cpp:1151
std::vector< componentt > componentst
Definition: std_types.h:203
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
Definition: std_types.h:98
Thrown when we encounter an instruction, parameters to an instruction etc.
symex_target_equationt * symex_target
const componentst & components() const
Definition: std_types.h:205
Symbolic Execution.
bool is_incomplete() const
Definition: std_types.h:1025
The trinary if-then-else operator.
Definition: std_expr.h:3427
exprt & cond()
Definition: std_expr.h:3445
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
exprt & old()
Definition: std_expr.h:3532
Definition: guard.h:19
typet & type()
Return the type of the expression.
Definition: expr.h:68
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
void set_level_2(unsigned i)
Definition: ssa_expr.h:95
Symbol table entry.
Definition: symbol.h:27
void set_l1_indices(ssa_exprt &expr, const namespacet &ns)
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible b...
std::map< irep_idt, exprt > propagation
void get_original_name(exprt &expr) const
Extract member of struct or union.
Definition: std_expr.h:3890
const irep_idt get_level_1() const
Definition: ssa_expr.h:112
const irep_idt & id() const
Definition: irep.h:259
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:229
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
void set_l0_indices(ssa_exprt &expr, const namespacet &ns)
std::set< exprt > expr_sett
Set of expressions; only used for the get API, not for internal data representation.
Definition: value_set.h:268
void remove_level_2()
Definition: ssa_expr.h:101
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:583
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
static bool check_renaming_l1(const exprt &expr)
API to expression classes.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:156
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
unsigned current_count(const irep_idt &identifier) const
Counter corresponding to an identifier.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
static void get_l1_name(exprt &expr)
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)
Write to a local variable.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
const exprt & size() const
Definition: std_types.h:1010
std::vector< threadt > threads
bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
Definition: race_check.cpp:120
#define forall_operands(it, expr)
Definition: expr.h:20
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
incremental_dirtyt dirty
current_namest current_names
symex_level1t level1
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
void set_l2_indices(ssa_exprt &expr, const namespacet &ns)
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
exprt & false_case()
Definition: std_expr.h:3465
The Boolean constant false.
Definition: std_expr.h:4452
symex_level0t level0
symex_level2t level2
static bool check_renaming(const exprt &expr)
write to a variable
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3569
typet type
Type of symbol.
Definition: symbol.h:31
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Read from a shared variable ssa_object (which is both the left- and the right–hand side of assignment...
Base type for structs and unions.
Definition: std_types.h:114
exprt & index()
Definition: std_expr.h:1631
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
const exprt & struct_op() const
Definition: std_expr.h:3931
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
irep_idt get_object_name() const
Definition: ssa_expr.h:46
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
irep_idt get_component_name() const
Definition: std_expr.h:3915
void update_type()
Definition: ssa_expr.h:36
void output_propagation_map(std::ostream &)
Print the constant propagation map in a human-friendly format.
irept & add(const irep_namet &name)
Definition: irep.cpp:305
void swap(irept &irep)
Definition: irep.h:303
bool is_complete() const
Definition: std_types.h:1020
#define Forall_operands(it, expr)
Definition: expr.h:26
void output(const namespacet &ns, std::ostream &out) const
Pretty-print this value-set.
Definition: value_set.cpp:103
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
dstringt irep_idt
Definition: irep.h:32
const typet & subtype() const
Definition: type.h:38
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
const irep_idt get_level_2() const
Definition: ssa_expr.h:117
Generic exception types primarily designed for use with invariants.
bool empty() const
Definition: dstring.h:75
exprt & array()
Definition: std_expr.h:1621
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
void add(const exprt &expr)
Definition: guard.cpp:43
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
Array index operator.
Definition: std_expr.h:1595
void rename_address(exprt &expr, const namespacet &ns, levelt level)
symex_targett::sourcet source
static format_containert< T > format(const T &o)
Definition: format.h:35