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