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 <cassert>
16 #include <iostream>
17 
18 #include <util/base_exceptions.h>
19 #include <util/std_expr.h>
20 #include <util/prefix.h>
21 
22 #include <analyses/dirty.h>
23 
25  depth(0),
26  symex_target(nullptr),
27  atomic_section_id(0),
28  record_events(true),
29  dirty(nullptr)
30 {
31  threads.resize(1);
32  new_frame();
33 }
34 
36 {
37  goto_functionst::function_mapt::const_iterator it=
38  goto_functions.function_map.find(goto_functionst::entry_point());
39 
40  if(it==goto_functions.function_map.end())
41  throw "program has no entry point";
42 
43  const goto_programt &body=it->second.body;
44 
46  top().end_of_function=--body.instructions.end();
48 }
49 
51  ssa_exprt &ssa_expr,
52  const namespacet &ns,
53  unsigned thread_nr)
54 {
55  // already renamed?
56  if(!ssa_expr.get_level_0().empty())
57  return;
58 
59  const irep_idt &obj_identifier=ssa_expr.get_object_name();
60 
61  // guards are not L0-renamed
62  if(obj_identifier=="goto_symex::\\guard")
63  return;
64 
65  const symbolt *s;
66 
67  if(ns.lookup(obj_identifier, s))
68  {
69  std::cerr << "level0: failed to find " << obj_identifier << '\n';
70  abort();
71  }
72 
73  // don't rename shared variables or functions
74  if(s->type.id()==ID_code ||
75  s->is_shared())
76  return;
77 
78  // rename!
79  ssa_expr.set_level_0(thread_nr);
80 }
81 
83 {
84  // already renamed?
85  if(!ssa_expr.get_level_1().empty())
86  return;
87 
88  const irep_idt l0_name=ssa_expr.get_l1_object_identifier();
89 
90  current_namest::const_iterator it=current_names.find(l0_name);
91  if(it==current_names.end())
92  return;
93 
94  // rename!
95  ssa_expr.set_level_1(it->second.second);
96 }
97 
101 {
102  if(expr.is_constant())
103  return true;
104 
105  if(expr.id()==ID_address_of)
106  {
107  const address_of_exprt &address_of_expr=to_address_of_expr(expr);
108 
109  return constant_propagation_reference(address_of_expr.object());
110  }
111  else if(expr.id()==ID_typecast)
112  {
113  const typecast_exprt &typecast_expr=to_typecast_expr(expr);
114 
115  return constant_propagation(typecast_expr.op());
116  }
117  else if(expr.id()==ID_plus)
118  {
119  forall_operands(it, expr)
120  if(!constant_propagation(*it))
121  return false;
122 
123  return true;
124  }
125  else if(expr.id()==ID_mult)
126  {
127  // propagate stuff with sizeof in it
128  forall_operands(it, expr)
129  {
130  if(it->find(ID_C_c_sizeof_type).is_not_nil())
131  return true;
132  else if(!constant_propagation(*it))
133  return false;
134  }
135 
136  return true;
137  }
138  else if(expr.id()==ID_array)
139  {
140  forall_operands(it, expr)
141  if(!constant_propagation(*it))
142  return false;
143 
144  return true;
145  }
146  else if(expr.id()==ID_array_of)
147  {
148  return constant_propagation(expr.op0());
149  }
150  else if(expr.id()==ID_with)
151  {
152  // this is bad
153  /*
154  forall_operands(it, expr)
155  if(!constant_propagation(expr.op0()))
156  return false;
157 
158  return true;
159  */
160  return false;
161  }
162  else if(expr.id()==ID_struct)
163  {
164  forall_operands(it, expr)
165  if(!constant_propagation(*it))
166  return false;
167 
168  return true;
169  }
170  else if(expr.id()==ID_union)
171  {
172  forall_operands(it, expr)
173  if(!constant_propagation(*it))
174  return false;
175 
176  return true;
177  }
178  // byte_update works, byte_extract may be out-of-bounds
179  else if(expr.id()==ID_byte_update_big_endian ||
180  expr.id()==ID_byte_update_little_endian)
181  {
182  forall_operands(it, expr)
183  if(!constant_propagation(*it))
184  return false;
185 
186  return true;
187  }
188 
189  return false;
190 }
191 
194 {
195  if(expr.id()==ID_symbol)
196  return true;
197  else if(expr.id()==ID_index)
198  {
199  const index_exprt &index_expr=to_index_expr(expr);
200 
201  return constant_propagation_reference(index_expr.array()) &&
202  constant_propagation(index_expr.index());
203  }
204  else if(expr.id()==ID_member)
205  {
206  if(expr.operands().size()!=1)
207  throw "member expects one operand";
208 
209  return constant_propagation_reference(expr.op0());
210  }
211  else if(expr.id()==ID_string_constant)
212  return true;
213 
214  return false;
215 }
216 
218 static bool check_renaming(const exprt &expr);
219 
220 static bool check_renaming(const typet &type)
221 {
222  if(type.id()==ID_array)
223  return check_renaming(to_array_type(type).size());
224  else if(type.id()==ID_struct ||
225  type.id()==ID_union ||
226  type.id()==ID_class)
227  {
228  const struct_union_typet &s_u_type=to_struct_union_type(type);
229  const struct_union_typet::componentst &components=s_u_type.components();
230 
231  for(struct_union_typet::componentst::const_iterator
232  it=components.begin();
233  it!=components.end();
234  ++it)
235  if(check_renaming(it->type()))
236  return true;
237  }
238  else if(type.has_subtype())
239  return check_renaming(type.subtype());
240 
241  return false;
242 }
243 
244 static bool check_renaming_l1(const exprt &expr)
245 {
246  if(check_renaming(expr.type()))
247  return true;
248 
249  if(expr.id()==ID_symbol)
250  {
251  if(!expr.get_bool(ID_C_SSA_symbol))
252  return expr.type().id()!=ID_code;
253  if(!to_ssa_expr(expr).get_level_2().empty())
254  return true;
255  if(to_ssa_expr(expr).get_original_expr().type()!=expr.type())
256  return true;
257  }
258  else
259  {
260  forall_operands(it, expr)
261  if(check_renaming_l1(*it))
262  return true;
263  }
264 
265  return false;
266 }
267 
268 static bool check_renaming(const exprt &expr)
269 {
270  if(check_renaming(expr.type()))
271  return true;
272 
273  if(expr.id()==ID_address_of &&
274  expr.op0().id()==ID_symbol)
275  return check_renaming_l1(expr.op0());
276  else if(expr.id()==ID_address_of &&
277  expr.op0().id()==ID_index)
278  return check_renaming_l1(expr.op0().op0()) ||
279  check_renaming(expr.op0().op1());
280  else if(expr.id()==ID_symbol)
281  {
282  if(!expr.get_bool(ID_C_SSA_symbol))
283  return expr.type().id()!=ID_code;
284  if(to_ssa_expr(expr).get_level_2().empty())
285  return true;
286  if(to_ssa_expr(expr).get_original_expr().type()!=expr.type())
287  return true;
288  }
289  else
290  {
291  forall_operands(it, expr)
292  if(check_renaming(*it))
293  return true;
294  }
295 
296  return false;
297 }
298 
299 static void assert_l1_renaming(const exprt &expr)
300 {
301  #if 1
302  if(check_renaming_l1(expr))
303  {
304  std::cerr << expr.pretty() << '\n';
305  assert(false);
306  }
307  #else
308  (void)expr;
309  #endif
310 }
311 
312 static void assert_l2_renaming(const exprt &expr)
313 {
314  #if 1
315  if(check_renaming(expr))
316  {
317  std::cerr << expr.pretty() << '\n';
318  assert(false);
319  }
320  #else
321  (void)expr;
322  #endif
323 }
324 
326  ssa_exprt &lhs, // L0/L1
327  const exprt &rhs, // L2
328  const namespacet &ns,
329  bool rhs_is_simplified,
330  bool record_value)
331 {
332  // identifier should be l0 or l1, make sure it's l1
333  rename(lhs, ns, L1);
334  irep_idt l1_identifier=lhs.get_identifier();
335 
336  // the type might need renaming
337  rename(lhs.type(), l1_identifier, ns);
338  lhs.update_type();
339  assert_l1_renaming(lhs);
340 
341  #if 0
342  assert(l1_identifier != get_original_name(l1_identifier)
343  || l1_identifier=="goto_symex::\\guard"
344  || ns.lookup(l1_identifier).is_shared()
345  || has_prefix(id2string(l1_identifier), "symex::invalid_object")
346  || has_prefix(id2string(l1_identifier), "symex_dynamic::dynamic_object"));
347  #endif
348 
349  // do the l2 renaming
350  if(level2.current_names.find(l1_identifier)==level2.current_names.end())
351  level2.current_names[l1_identifier]=std::make_pair(lhs, 0);
352  level2.increase_counter(l1_identifier);
353  set_ssa_indices(lhs, ns, L2);
354 
355  // in case we happen to be multi-threaded, record the memory access
356  bool is_shared=l2_thread_write_encoding(lhs, ns);
357 
358  assert_l2_renaming(lhs);
359  assert_l2_renaming(rhs);
360 
361  // for value propagation -- the RHS is L2
362 
363  if(!is_shared && record_value && constant_propagation(rhs))
364  propagation.values[l1_identifier]=rhs;
365  else
366  propagation.remove(l1_identifier);
367 
368  {
369  // update value sets
370  value_sett::expr_sett rhs_value_set;
371  exprt l1_rhs(rhs);
372  get_l1_name(l1_rhs);
373 
374  ssa_exprt l1_lhs(lhs);
375  get_l1_name(l1_lhs);
376 
377  assert_l1_renaming(l1_lhs);
378  assert_l1_renaming(l1_rhs);
379 
380  value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
381  }
382 
383  #if 0
384  std::cout << "Assigning " << l1_identifier << '\n';
385  value_set.output(ns, std::cout);
386  std::cout << "**********************\n";
387  #endif
388 }
389 
391 {
392  if(expr.id()==ID_symbol)
393  {
394  valuest::const_iterator it=
395  values.find(expr.get(ID_identifier));
396  if(it!=values.end())
397  expr=it->second;
398  }
399  else if(expr.id()==ID_address_of)
400  {
401  // ignore
402  }
403  else
404  {
405  // do this recursively
406  Forall_operands(it, expr)
407  operator()(*it);
408  }
409 }
410 
412  ssa_exprt &ssa_expr,
413  const namespacet &ns,
414  levelt level)
415 {
416  switch(level)
417  {
418  case L0:
419  level0(ssa_expr, ns, source.thread_nr);
420  break;
421 
422  case L1:
423  if(!ssa_expr.get_level_2().empty())
424  return;
425  if(!ssa_expr.get_level_1().empty())
426  return;
427  level0(ssa_expr, ns, source.thread_nr);
428  level1(ssa_expr);
429  break;
430 
431  case L2:
432  if(!ssa_expr.get_level_2().empty())
433  return;
434  level0(ssa_expr, ns, source.thread_nr);
435  level1(ssa_expr);
436  ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
437  break;
438 
439  default:
440  assert(false);
441  }
442 }
443 
445  exprt &expr,
446  const namespacet &ns,
447  levelt level)
448 {
449  // rename all the symbols with their last known value
450 
451  if(expr.id()==ID_symbol &&
452  expr.get_bool(ID_C_SSA_symbol))
453  {
454  ssa_exprt &ssa=to_ssa_expr(expr);
455 
456  if(level==L0 || level==L1)
457  {
458  set_ssa_indices(ssa, ns, level);
459  rename(expr.type(), ssa.get_identifier(), ns, level);
460  ssa.update_type();
461  }
462  else if(level==L2)
463  {
464  set_ssa_indices(ssa, ns, L1);
465  rename(expr.type(), ssa.get_identifier(), ns, level);
466  ssa.update_type();
467 
468  if(l2_thread_read_encoding(ssa, ns))
469  {
470  // renaming taken care of by l2_thread_encoding
471  }
472  else if(!ssa.get_level_2().empty())
473  {
474  // already at L2
475  }
476  else
477  {
478  // We also consider propagation if we go up to L2.
479  // L1 identifiers are used for propagation!
480  propagationt::valuest::const_iterator p_it=
481  propagation.values.find(ssa.get_identifier());
482 
483  if(p_it!=propagation.values.end())
484  expr=p_it->second; // already L2
485  else
486  set_ssa_indices(ssa, ns, L2);
487  }
488  }
489  }
490  else if(expr.id()==ID_symbol)
491  {
492  // we never rename function symbols
493  if(ns.follow(expr.type()).id()==ID_code)
494  {
495  rename(
496  expr.type(),
498  ns,
499  level);
500 
501  return;
502  }
503 
504  expr=ssa_exprt(expr);
505  rename(expr, ns, level);
506  }
507  else if(expr.id()==ID_address_of)
508  {
509  assert(expr.operands().size()==1);
510  rename_address(expr.op0(), ns, level);
511  assert(expr.type().id()==ID_pointer);
512  expr.type().subtype()=expr.op0().type();
513  }
514  else
515  {
516  // this could go wrong, but we would have to re-typecheck ...
517  rename(expr.type(), irep_idt(), ns, level);
518 
519  // do this recursively
520  Forall_operands(it, expr)
521  rename(*it, ns, level);
522 
523  // some fixes
524  if(expr.id()==ID_with)
525  expr.type()=to_with_expr(expr).old().type();
526  else if(expr.id()==ID_if)
527  {
528  assert(to_if_expr(expr).true_case().type()==
529  to_if_expr(expr).false_case().type());
530  expr.type()=to_if_expr(expr).true_case().type();
531  }
532  }
533 }
534 
537  ssa_exprt &expr,
538  const namespacet &ns)
539 {
540  // do we have threads?
541  if(threads.size()<=1)
542  return false;
543 
544  // is it a shared object?
545  INVARIANT_STRUCTURED(dirty!=nullptr, nullptr_exceptiont, "dirty is null");
546  const irep_idt &obj_identifier=expr.get_object_name();
547  if(obj_identifier=="goto_symex::\\guard" ||
548  (!ns.lookup(obj_identifier).is_shared() &&
549  !(*dirty)(obj_identifier)))
550  return false;
551 
552  ssa_exprt ssa_l1=expr;
553  ssa_l1.remove_level_2();
554  const irep_idt &l1_identifier=ssa_l1.get_identifier();
555 
556  // see whether we are within an atomic section
557  if(atomic_section_id!=0)
558  {
559  guardt write_guard;
560  write_guard.add(false_exprt());
561 
562  written_in_atomic_sectiont::const_iterator a_s_writes=
563  written_in_atomic_section.find(ssa_l1);
564  if(a_s_writes!=written_in_atomic_section.end())
565  {
566  for(a_s_w_entryt::const_iterator it=a_s_writes->second.begin();
567  it!=a_s_writes->second.end();
568  ++it)
569  {
570  guardt g=*it;
571  g-=guard;
572  if(g.is_true())
573  // there has already been a write to l1_identifier within
574  // this atomic section under the same guard, or a guard
575  // that implies the current one
576  return false;
577 
578  write_guard|=*it;
579  }
580  }
581 
582  not_exprt no_write(write_guard.as_expr());
583 
584  // we cannot determine for sure that there has been a write already
585  // so generate a read even if l1_identifier has been written on
586  // all branches flowing into this read
587  guardt read_guard;
588  read_guard.add(false_exprt());
589 
590  a_s_r_entryt &a_s_read=read_in_atomic_section[ssa_l1];
591  for(std::list<guardt>::const_iterator it=a_s_read.second.begin();
592  it!=a_s_read.second.end();
593  ++it)
594  {
595  guardt g=*it;
596  g-=guard;
597  if(g.is_true())
598  // there has already been a read l1_identifier within
599  // this atomic section under the same guard, or a guard
600  // that implies the current one
601  return false;
602 
603  read_guard|=*it;
604  }
605 
606  exprt cond=read_guard.as_expr();
607  if(!no_write.op().is_false())
608  cond=or_exprt(no_write.op(), cond);
609 
610  if_exprt tmp(cond, ssa_l1, ssa_l1);
612 
613  if(a_s_read.second.empty())
614  {
615  if(level2.current_names.find(l1_identifier)==level2.current_names.end())
616  level2.current_names[l1_identifier]=std::make_pair(ssa_l1, 0);
617  level2.increase_counter(l1_identifier);
618  a_s_read.first=level2.current_count(l1_identifier);
619  }
620 
621  to_ssa_expr(tmp.false_case()).set_level_2(a_s_read.first);
622 
623  if(cond.is_false())
624  {
625  exprt t=tmp.false_case();
626  t.swap(tmp);
627  }
628 
629  const bool record_events_bak=record_events;
630  record_events=false;
631  assignment(ssa_l1, tmp, ns, true, true);
632  record_events=record_events_bak;
633 
635  guard.as_expr(),
636  ssa_l1,
637  ssa_l1,
638  ssa_l1.get_original_expr(),
639  tmp,
640  source,
642 
643  set_ssa_indices(ssa_l1, ns, L2);
644  expr=ssa_l1;
645 
646  a_s_read.second.push_back(guard);
647  if(!no_write.op().is_false())
648  a_s_read.second.back().add(no_write);
649 
650  return true;
651  }
652 
653  if(level2.current_names.find(l1_identifier)==level2.current_names.end())
654  level2.current_names[l1_identifier]=std::make_pair(ssa_l1, 0);
655 
656  // No event and no fresh index, but avoid constant propagation
657  if(!record_events)
658  {
659  set_ssa_indices(ssa_l1, ns, L2);
660  expr=ssa_l1;
661  return true;
662  }
663 
664  // produce a fresh L2 name
665  level2.increase_counter(l1_identifier);
666  set_ssa_indices(ssa_l1, ns, L2);
667  expr=ssa_l1;
668 
669  // and record that
671  symex_target!=nullptr, nullptr_exceptiont, "symex_target is null");
673  guard.as_expr(),
674  expr,
676  source);
677 
678  return true;
679 }
680 
683  const ssa_exprt &expr,
684  const namespacet &ns)
685 {
686  if(!record_events)
687  return false;
688 
689  // is it a shared object?
690  INVARIANT_STRUCTURED(dirty!=nullptr, nullptr_exceptiont, "dirty is null");
691  const irep_idt &obj_identifier=expr.get_object_name();
692  if(obj_identifier=="goto_symex::\\guard" ||
693  (!ns.lookup(obj_identifier).is_shared() &&
694  !(*dirty)(obj_identifier)))
695  return false; // not shared
696 
697  // see whether we are within an atomic section
698  if(atomic_section_id!=0)
699  {
700  ssa_exprt ssa_l1=expr;
701  ssa_l1.remove_level_2();
702 
703  written_in_atomic_section[ssa_l1].push_back(guard);
704  return false;
705  }
706 
707  // record a shared write
709  guard.as_expr(),
710  expr,
712  source);
713 
714  // do we have threads?
715  return threads.size()>1;
716 }
717 
719  exprt &expr,
720  const namespacet &ns,
721  levelt level)
722 {
723  if(expr.id()==ID_symbol &&
724  expr.get_bool(ID_C_SSA_symbol))
725  {
726  ssa_exprt &ssa=to_ssa_expr(expr);
727 
728  // only do L1!
729  set_ssa_indices(ssa, ns, L1);
730 
731  rename(expr.type(), ssa.get_identifier(), ns, level);
732  ssa.update_type();
733  }
734  else if(expr.id()==ID_symbol)
735  {
736  expr=ssa_exprt(expr);
737  rename_address(expr, ns, level);
738  }
739  else
740  {
741  if(expr.id()==ID_index)
742  {
743  index_exprt &index_expr=to_index_expr(expr);
744 
745  rename_address(index_expr.array(), ns, level);
746  assert(index_expr.array().type().id()==ID_array);
747  expr.type()=index_expr.array().type().subtype();
748 
749  // the index is not an address
750  rename(index_expr.index(), ns, level);
751  }
752  else if(expr.id()==ID_if)
753  {
754  // the condition is not an address
755  if_exprt &if_expr=to_if_expr(expr);
756  rename(if_expr.cond(), ns, level);
757  rename_address(if_expr.true_case(), ns, level);
758  rename_address(if_expr.false_case(), ns, level);
759 
760  if_expr.type()=if_expr.true_case().type();
761  }
762  else if(expr.id()==ID_member)
763  {
764  member_exprt &member_expr=to_member_expr(expr);
765 
766  rename_address(member_expr.struct_op(), ns, level);
767 
768  // type might not have been renamed in case of nesting of
769  // structs and pointers/arrays
770  if(member_expr.struct_op().type().id()!=ID_symbol)
771  {
772  const struct_union_typet &su_type=
773  to_struct_union_type(member_expr.struct_op().type());
774  const struct_union_typet::componentt &comp=
775  su_type.get_component(member_expr.get_component_name());
776  assert(comp.is_not_nil());
777  expr.type()=comp.type();
778  }
779  else
780  rename(expr.type(), irep_idt(), ns, level);
781  }
782  else
783  {
784  // this could go wrong, but we would have to re-typecheck ...
785  rename(expr.type(), irep_idt(), ns, level);
786 
787  // do this recursively; we assume here
788  // that all the operands are addresses
789  Forall_operands(it, expr)
790  rename_address(*it, ns, level);
791  }
792  }
793 }
794 
796  typet &type,
797  const irep_idt &l1_identifier,
798  const namespacet &ns,
799  levelt level)
800 {
801  // rename all the symbols with their last known value
802  // to the given level
803 
804  std::pair<l1_typest::iterator, bool> l1_type_entry;
805  if(level==L2 &&
806  !l1_identifier.empty())
807  {
808  l1_type_entry=l1_types.insert(std::make_pair(l1_identifier, type));
809 
810  if(!l1_type_entry.second) // was already in map
811  {
812  // do not change a complete array type to an incomplete one
813 
814  const typet &type_prev=l1_type_entry.first->second;
815 
816  if(type.id()!=ID_array ||
817  type_prev.id()!=ID_array ||
818  to_array_type(type).is_incomplete() ||
819  to_array_type(type_prev).is_complete())
820  {
821  type=l1_type_entry.first->second;
822  return;
823  }
824  }
825  }
826 
827  if(type.id()==ID_array)
828  {
829  rename(type.subtype(), irep_idt(), ns, level);
830  rename(to_array_type(type).size(), ns, level);
831  }
832  else if(type.id()==ID_struct ||
833  type.id()==ID_union ||
834  type.id()==ID_class)
835  {
837  struct_union_typet::componentst &components=s_u_type.components();
838 
839  for(struct_union_typet::componentst::iterator
840  it=components.begin();
841  it!=components.end();
842  ++it)
843  // be careful, or it might get cyclic
844  if(it->type().id()==ID_array)
845  rename(to_array_type(it->type()).size(), ns, level);
846  else if(it->type().id()!=ID_pointer)
847  rename(it->type(), irep_idt(), ns, level);
848  }
849  else if(type.id()==ID_pointer)
850  {
851  rename(type.subtype(), irep_idt(), ns, level);
852  }
853  else if(type.id()==ID_symbol)
854  {
855  const symbolt &symbol=
856  ns.lookup(to_symbol_type(type).get_identifier());
857  type=symbol.type;
858  rename(type, l1_identifier, ns, level);
859  }
860 
861  if(level==L2 &&
862  !l1_identifier.empty())
863  l1_type_entry.first->second=type;
864 }
865 
867 {
868  get_original_name(expr.type());
869 
870  if(expr.id()==ID_symbol &&
871  expr.get_bool(ID_C_SSA_symbol))
872  expr=to_ssa_expr(expr).get_original_expr();
873  else
874  Forall_operands(it, expr)
875  get_original_name(*it);
876 }
877 
879 {
880  // rename all the symbols with their last known value
881 
882  if(type.id()==ID_array)
883  {
884  get_original_name(type.subtype());
885  get_original_name(to_array_type(type).size());
886  }
887  else if(type.id()==ID_struct ||
888  type.id()==ID_union ||
889  type.id()==ID_class)
890  {
892  struct_union_typet::componentst &components=s_u_type.components();
893 
894  for(struct_union_typet::componentst::iterator
895  it=components.begin();
896  it!=components.end();
897  ++it)
898  get_original_name(it->type());
899  }
900  else if(type.id()==ID_pointer)
901  {
902  get_original_name(type.subtype());
903  }
904 }
905 
907 {
908  // do not reset the type !
909 
910  if(expr.id()==ID_symbol &&
911  expr.get_bool(ID_C_SSA_symbol))
912  to_ssa_expr(expr).remove_level_2();
913  else
914  Forall_operands(it, expr)
915  get_l1_name(*it);
916 }
917 
919 {
920  assert(source.thread_nr<threads.size());
921  assert(t<threads.size());
922 
923  // save PC
925  threads[source.thread_nr].atomic_section_id=atomic_section_id;
926 
927  // get new PC
928  source.thread_nr=t;
929  source.pc=threads[t].pc;
930 
931  guard=threads[t].guard;
932 }
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
Definition: std_expr.h:2919
The type of an expression.
Definition: type.h:20
exprt as_expr() const
Definition: guard.h:43
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:209
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
Boolean negation.
Definition: std_expr.h:2648
exprt & true_case()
Definition: std_expr.h:2805
semantic type conversion
Definition: std_expr.h:1725
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
bool is_shared() const
Definition: symbol.h:103
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 assert_l2_renaming(const exprt &expr)
goto_programt::const_targett pc
Definition: symex_target.h:32
exprt & object()
Definition: std_expr.h:2608
class goto_symex_statet::propagationt propagation
boolean OR
Definition: std_expr.h:1968
exprt & op0()
Definition: expr.h:84
read_in_atomic_sectiont read_in_atomic_section
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
bool has_subtype() const
Definition: type.h:77
Variables whose address is taken.
void set_level_1(unsigned i)
Definition: ssa_expr.h:89
instructionst instructions
The list of instructions in the goto program.
void remove(const irep_idt &identifier)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
const irep_idt & get_identifier() const
Definition: std_expr.h:120
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Definition: value_set.cpp:1089
std::vector< componentt > componentst
Definition: std_types.h:240
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
goto_symex_statet::level0t level0
bool is_false() const
Definition: expr.cpp:140
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
void increase_counter(const irep_idt &identifier)
void set_ssa_indices(ssa_exprt &expr, const namespacet &ns, levelt level=L2)
const componentst & components() const
Definition: std_types.h:242
Symbolic Execution.
bool is_incomplete() const
Definition: std_types.h:930
symex_targett * symex_target
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
written_in_atomic_sectiont written_in_atomic_section
bool is_true() const
Definition: expr.cpp:133
exprt & old()
Definition: std_expr.h:2878
Definition: guard.h:19
typet & type()
Definition: expr.h:60
void set_level_2(unsigned i)
Definition: ssa_expr.h:95
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
const irep_idt get_l1_object_identifier() const
Definition: ssa_expr.h:66
exprt & op()
Definition: std_expr.h:1739
void switch_to_thread(unsigned t)
void get_original_name(exprt &expr) const
Extract member of struct or union.
Definition: std_expr.h:3214
bool constant_propagation(const exprt &expr) const
This function determines what expressions are to be propagated as "constants".
const irep_idt get_level_1() const
Definition: ssa_expr.h:112
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
goto_symex_statet::level2t level2
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
void initialize(const goto_functionst &goto_functions)
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
bool constant_propagation_reference(const exprt &expr) const
this function determines which reference-typed expressions are constant
void set_level_0(unsigned i)
Definition: ssa_expr.h:83
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:2629
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:150
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
std::set< exprt > expr_sett
Definition: value_set.h:119
void remove_level_2()
Definition: ssa_expr.h:101
static bool check_renaming_l1(const exprt &expr)
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:62
goto_symex_statet::level1t level1
const exprt & size() const
Definition: std_types.h:915
bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
Definition: race_check.cpp:128
#define forall_operands(it, expr)
Definition: expr.h:17
const irep_idt get_level_0() const
Definition: ssa_expr.h:107
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
Operator to return the address of an object.
Definition: std_expr.h:2593
exprt & false_case()
Definition: std_expr.h:2815
The boolean constant false.
Definition: std_expr.h:3753
bool is_constant() const
Definition: expr.cpp:128
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
static bool check_renaming(const exprt &expr)
write to a variable
const dirtyt * dirty
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
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)=0
typet type
Type of symbol.
Definition: symbol.h:37
void get_l1_name(exprt &expr) const
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:159
void operator()(ssa_exprt &ssa_expr)
exprt & index()
Definition: std_expr.h:1208
unsigned current_count(const irep_idt &identifier) const
static void assert_l1_renaming(const exprt &expr)
Base class for all expressions.
Definition: expr.h:46
const exprt & struct_op() const
Definition: std_expr.h:3270
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value)
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:3249
void update_type()
Definition: ssa_expr.h:36
irept & add(const irep_namet &name)
Definition: irep.cpp:306
void swap(irept &irep)
Definition: irep.h:231
bool is_complete() const
Definition: std_types.h:925
#define Forall_operands(it, expr)
Definition: expr.h:23
symex_targett::sourcet calling_location
void output(const namespacet &ns, std::ostream &out) const
Definition: value_set.cpp:97
void operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
dstringt irep_idt
Definition: irep.h:32
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
const irep_idt get_level_2() const
Definition: ssa_expr.h:117
Generic exception types primarily designed for use with invariants.
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0
bool empty() const
Definition: dstring.h:61
exprt & array()
Definition: std_expr.h:1198
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
goto_programt::const_targett end_of_function
void add(const exprt &expr)
Definition: guard.cpp:64
const componentt & get_component(const irep_idt &component_name) const
Definition: std_types.cpp:51
array index operator
Definition: std_expr.h:1170
void rename_address(exprt &expr, const namespacet &ns, levelt level)
symex_targett::sourcet source