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 #include "goto_symex_is_constant.h"
14 
15 #include <cstdlib>
16 #include <iostream>
17 
18 #include <util/as_const.h>
19 #include <util/base_exceptions.h>
20 #include <util/byte_operators.h>
21 #include <util/c_types.h>
22 #include <util/exception_utils.h>
23 #include <util/expr_util.h>
24 #include <util/format.h>
25 #include <util/format_expr.h>
26 #include <util/invariant.h>
28 #include <util/prefix.h>
29 #include <util/std_expr.h>
30 
31 #include <analyses/dirty.h>
33 
34 static void get_l1_name(exprt &expr);
35 
37  const symex_targett::sourcet &_source,
38  std::size_t max_field_sensitive_array_size,
39  guard_managert &manager,
40  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
41  : goto_statet(manager),
42  source(_source),
43  guard_manager(manager),
44  symex_target(nullptr),
45  field_sensitivity(max_field_sensitive_array_size),
46  record_events({true}),
47  fresh_l2_name_provider(fresh_l2_name_provider)
48 {
49  threads.emplace_back(guard_manager);
51 }
52 
54 
55 template <>
57 goto_symex_statet::set_indices<L0>(ssa_exprt ssa_expr, const namespacet &ns)
58 {
59  return symex_level0(std::move(ssa_expr), ns, source.thread_nr);
60 }
61 
62 template <>
64 goto_symex_statet::set_indices<L1>(ssa_exprt ssa_expr, const namespacet &ns)
65 {
66  return level1(symex_level0(std::move(ssa_expr), ns, source.thread_nr));
67 }
68 
69 template <>
71 goto_symex_statet::set_indices<L2>(ssa_exprt ssa_expr, const namespacet &ns)
72 {
73  return level2(
74  level1(symex_level0(std::move(ssa_expr), ns, source.thread_nr)));
75 }
76 
78  ssa_exprt lhs, // L0/L1
79  const exprt &rhs, // L2
80  const namespacet &ns,
81  bool rhs_is_simplified,
82  bool record_value,
83  bool allow_pointer_unsoundness)
84 {
85  // identifier should be l0 or l1, make sure it's l1
86  lhs = rename_ssa<L1>(std::move(lhs), ns).get();
87  irep_idt l1_identifier=lhs.get_identifier();
88 
89  // the type might need renaming
90  rename<L2>(lhs.type(), l1_identifier, ns);
91  lhs.update_type();
93  {
94  DATA_INVARIANT(!check_renaming_l1(lhs), "lhs renaming failed on l1");
95  }
96 
97  // do the l2 renaming
99  renamedt<ssa_exprt, L2> l2_lhs = set_indices<L2>(std::move(lhs), ns);
100  lhs = l2_lhs.get();
101 
102  // in case we happen to be multi-threaded, record the memory access
103  bool is_shared=l2_thread_write_encoding(lhs, ns);
104 
106  {
107  DATA_INVARIANT(!check_renaming(lhs), "lhs renaming failed on l2");
108  DATA_INVARIANT(!check_renaming(rhs), "rhs renaming failed on l2");
109  }
110 
111  // see #305 on GitHub for a simple example and possible discussion
112  if(is_shared && lhs.type().id() == ID_pointer && !allow_pointer_unsoundness)
114  "pointer handling for concurrency is unsound");
115 
116  // Update constant propagation map -- the RHS is L2
117  if(!is_shared && record_value && goto_symex_is_constantt()(rhs))
118  {
119  const auto propagation_entry = propagation.find(l1_identifier);
120  if(!propagation_entry.has_value())
121  propagation.insert(l1_identifier, rhs);
122  else if(propagation_entry->get() != rhs)
123  propagation.replace(l1_identifier, rhs);
124  }
125  else
126  propagation.erase_if_exists(l1_identifier);
127 
128  {
129  // update value sets
130  exprt l1_rhs(rhs);
131  get_l1_name(l1_rhs);
132 
133  const ssa_exprt l1_lhs = remove_level_2(lhs);
135  {
136  DATA_INVARIANT(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
137  DATA_INVARIANT(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
138  }
139 
140  value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
141  }
142 
143 #ifdef DEBUG
144  std::cout << "Assigning " << l1_identifier << '\n';
145  value_set.output(std::cout);
146  std::cout << "**********************\n";
147 #endif
148 
149  return l2_lhs;
150 }
151 
152 template <levelt level>
155 {
156  static_assert(
157  level == L0 || level == L1,
158  "rename_ssa can only be used for levels L0 and L1");
159  ssa = set_indices<level>(std::move(ssa), ns).get();
160  rename<level>(ssa.type(), ssa.get_identifier(), ns);
161  ssa.update_type();
162  return renamedt<ssa_exprt, level>{ssa};
163 }
164 
167 goto_symex_statet::rename_ssa<L0>(ssa_exprt ssa, const namespacet &ns);
169 goto_symex_statet::rename_ssa<L1>(ssa_exprt ssa, const namespacet &ns);
170 
171 template <levelt level>
174 {
175  // rename all the symbols with their last known value
176 
177  static_assert(
178  level == L0 || level == L1 || level == L1_WITH_CONSTANT_PROPAGATION ||
179  level == L2,
180  "must handle all renaming levels");
181 
182  if(is_ssa_expr(expr))
183  {
184  exprt original_expr = expr;
185  ssa_exprt &ssa=to_ssa_expr(expr);
186 
187  if(level == L0)
188  {
189  return renamedt<exprt, level>{
190  std::move(rename_ssa<L0>(std::move(ssa), ns).value())};
191  }
192  else if(level == L1)
193  {
194  return renamedt<exprt, level>{
195  std::move(rename_ssa<L1>(std::move(ssa), ns).value())};
196  }
197  else
198  {
199  ssa = set_indices<L1>(std::move(ssa), ns).get();
200  rename<level>(expr.type(), ssa.get_identifier(), ns);
201  ssa.update_type();
202 
203  // renaming taken care of by l2_thread_encoding, or already at L2
204  if(l2_thread_read_encoding(ssa, ns) || !ssa.get_level_2().empty())
205  {
206  if(level == L1_WITH_CONSTANT_PROPAGATION)
207  {
208  // Don't actually rename to L2 -- we just used `ssa` to check whether
209  // constant-propagation was applicable
210  return renamedt<exprt, level>(std::move(original_expr));
211  }
212  else
213  return renamedt<exprt, level>(std::move(ssa));
214  }
215  else
216  {
217  // We also consider propagation if we go up to L2.
218  // L1 identifiers are used for propagation!
219  auto p_it = propagation.find(ssa.get_identifier());
220 
221  if(p_it.has_value())
222  {
223  return renamedt<exprt, level>(*p_it); // already L2
224  }
225  else
226  {
227  if(level == L2)
228  ssa = set_indices<L2>(std::move(ssa), ns).get();
229  return renamedt<exprt, level>(std::move(ssa));
230  }
231  }
232  }
233  }
234  else if(expr.id()==ID_symbol)
235  {
236  const auto &type = as_const(expr).type();
237 
238  // we never rename function symbols
239  if(type.id() == ID_code || type.id() == ID_mathematical_function)
240  {
241  rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
242  return renamedt<exprt, level>{std::move(expr)};
243  }
244  else
245  return rename<level>(ssa_exprt{expr}, ns);
246  }
247  else if(expr.id()==ID_address_of)
248  {
249  auto &address_of_expr = to_address_of_expr(expr);
250  rename_address<level>(address_of_expr.object(), ns);
251  to_pointer_type(expr.type()).subtype() =
252  as_const(address_of_expr).object().type();
253  return renamedt<exprt, level>{std::move(expr)};
254  }
255  else if(expr.is_nil())
256  {
257  return renamedt<exprt, level>{std::move(expr)};
258  }
259  else
260  {
261  rename<level>(expr.type(), irep_idt(), ns);
262 
263  // do this recursively
264  Forall_operands(it, expr)
265  *it = rename<level>(std::move(*it), ns).get();
266 
267  const exprt &c_expr = as_const(expr);
268  INVARIANT(
269  (expr.id() != ID_with ||
270  c_expr.type() == to_with_expr(c_expr).old().type()) &&
271  (expr.id() != ID_if ||
272  (c_expr.type() == to_if_expr(c_expr).true_case().type() &&
273  c_expr.type() == to_if_expr(c_expr).false_case().type())),
274  "Type of renamed expr should be the same as operands for with_exprt and "
275  "if_exprt");
276 
277  if(level == L2)
278  expr = field_sensitivity.apply(ns, *this, std::move(expr), false);
279 
280  return renamedt<exprt, level>{std::move(expr)};
281  }
282 }
283 
284 // Explicitly instantiate the one version of this function without an explicit
285 // caller in this file:
288 
290 {
291  rename(lvalue.type(), irep_idt(), ns);
292 
293  if(lvalue.id() == ID_symbol)
294  {
295  // Nothing to do
296  }
297  else if(is_read_only_object(lvalue))
298  {
299  // Ignore apparent writes to 'NULL-object' and similar read-only objects
300  }
301  else if(lvalue.id() == ID_typecast)
302  {
303  auto &typecast_lvalue = to_typecast_expr(lvalue);
304  typecast_lvalue.op() = l2_rename_rvalues(typecast_lvalue.op(), ns);
305  }
306  else if(lvalue.id() == ID_member)
307  {
308  auto &member_lvalue = to_member_expr(lvalue);
309  member_lvalue.compound() = l2_rename_rvalues(member_lvalue.compound(), ns);
310  }
311  else if(lvalue.id() == ID_index)
312  {
313  // The index is an rvalue:
314  auto &index_lvalue = to_index_expr(lvalue);
315  index_lvalue.array() = l2_rename_rvalues(index_lvalue.array(), ns);
316  index_lvalue.index() = rename(index_lvalue.index(), ns).get();
317  }
318  else if(
319  lvalue.id() == ID_byte_extract_little_endian ||
320  lvalue.id() == ID_byte_extract_big_endian)
321  {
322  // The offset is an rvalue:
323  auto &byte_extract_lvalue = to_byte_extract_expr(lvalue);
324  byte_extract_lvalue.op() = l2_rename_rvalues(byte_extract_lvalue.op(), ns);
325  byte_extract_lvalue.offset() = rename(byte_extract_lvalue.offset(), ns);
326  }
327  else if(lvalue.id() == ID_if)
328  {
329  // The condition is an rvalue:
330  auto &if_lvalue = to_if_expr(lvalue);
331  if_lvalue.cond() = rename(if_lvalue.cond(), ns);
332  if(!if_lvalue.cond().is_false())
333  if_lvalue.true_case() = l2_rename_rvalues(if_lvalue.true_case(), ns);
334  if(!if_lvalue.cond().is_true())
335  if_lvalue.false_case() = l2_rename_rvalues(if_lvalue.false_case(), ns);
336  }
337  else if(lvalue.id() == ID_complex_real)
338  {
339  auto &complex_real_lvalue = to_complex_real_expr(lvalue);
340  complex_real_lvalue.op() = l2_rename_rvalues(complex_real_lvalue.op(), ns);
341  }
342  else if(lvalue.id() == ID_complex_imag)
343  {
344  auto &complex_imag_lvalue = to_complex_imag_expr(lvalue);
345  complex_imag_lvalue.op() = l2_rename_rvalues(complex_imag_lvalue.op(), ns);
346  }
347  else
348  {
350  "l2_rename_rvalues case `" + lvalue.id_string() + "' not handled");
351  }
352 
353  return lvalue;
354 }
355 
356 template renamedt<exprt, L1>
357 goto_symex_statet::rename<L1>(exprt expr, const namespacet &ns);
358 
361  ssa_exprt &expr,
362  const namespacet &ns)
363 {
364  // do we have threads?
365  if(threads.size()<=1)
366  return false;
367 
368  // is it a shared object?
369  PRECONDITION(dirty != nullptr);
370  const irep_idt &obj_identifier=expr.get_object_name();
371  if(
372  obj_identifier == guard_identifier() ||
373  (!ns.lookup(obj_identifier).is_shared() && !(*dirty)(obj_identifier)))
374  {
375  return false;
376  }
377 
378  // only continue if an indivisible object is being accessed
380  return false;
381 
382  const ssa_exprt ssa_l1 = remove_level_2(expr);
383  const irep_idt &l1_identifier=ssa_l1.get_identifier();
384  const exprt guard_as_expr = guard.as_expr();
385 
386  // see whether we are within an atomic section
387  if(atomic_section_id!=0)
388  {
389  guardt write_guard{false_exprt{}, guard_manager};
390 
391  const auto a_s_writes = written_in_atomic_section.find(ssa_l1);
392  if(a_s_writes!=written_in_atomic_section.end())
393  {
394  for(const auto &guard_in_list : a_s_writes->second)
395  {
396  guardt g = guard_in_list;
397  g-=guard;
398  if(g.is_true())
399  // There has already been a write to l1_identifier within this atomic
400  // section under the same guard, or a guard implied by the current
401  // one.
402  return false;
403 
404  write_guard |= guard_in_list;
405  }
406  }
407 
408  not_exprt no_write(write_guard.as_expr());
409 
410  // we cannot determine for sure that there has been a write already
411  // so generate a read even if l1_identifier has been written on
412  // all branches flowing into this read
413  guardt read_guard{false_exprt{}, guard_manager};
414 
415  a_s_r_entryt &a_s_read=read_in_atomic_section[ssa_l1];
416  for(const auto &a_s_read_guard : a_s_read.second)
417  {
418  guardt g = a_s_read_guard; // copy
419  g-=guard;
420  if(g.is_true())
421  // There has already been a read of l1_identifier within this atomic
422  // section under the same guard, or a guard implied by the current one.
423  return false;
424 
425  read_guard |= a_s_read_guard;
426  }
427 
428  guardt cond = read_guard;
429  if(!no_write.op().is_false())
430  cond |= guardt{no_write.op(), guard_manager};
431 
432  // It is safe to perform constant propagation in case we have read or
433  // written this object within the atomic section. We must actually do this,
434  // because goto_state::apply_condition may have placed the latest value in
435  // the propagation map without recording an assignment.
436  auto p_it = propagation.find(ssa_l1.get_identifier());
437  const exprt l2_true_case =
438  p_it.has_value() ? *p_it : set_indices<L2>(ssa_l1, ns).get();
439 
440  if(!cond.is_true())
441  level2.increase_generation(l1_identifier, ssa_l1, fresh_l2_name_provider);
442 
443  if(a_s_read.second.empty())
444  a_s_read.first = level2.latest_index(l1_identifier);
445 
446  const renamedt<ssa_exprt, L2> l2_false_case = set_indices<L2>(ssa_l1, ns);
447 
448  exprt tmp;
449  if(cond.is_false())
450  tmp = l2_false_case.get();
451  else if(cond.is_true())
452  tmp = l2_true_case;
453  else
454  tmp = if_exprt{cond.as_expr(), l2_true_case, l2_false_case.get()};
455 
456  record_events.push(false);
457  ssa_exprt ssa_l2 = assignment(std::move(ssa_l1), tmp, ns, true, true).get();
458  record_events.pop();
459 
461  guard_as_expr,
462  ssa_l2,
463  ssa_l2,
464  ssa_l2.get_original_expr(),
465  tmp,
466  source,
468 
469  INVARIANT(!check_renaming(ssa_l2), "expr should be renamed to L2");
470  expr = std::move(ssa_l2);
471 
472  a_s_read.second.push_back(guard);
473  if(!no_write.op().is_false())
474  a_s_read.second.back().add(no_write);
475 
476  return true;
477  }
478 
479  // No event and no fresh index, but avoid constant propagation
480  if(!record_events.top())
481  {
482  expr = set_indices<L2>(std::move(ssa_l1), ns).get();
483  return true;
484  }
485 
486  // produce a fresh L2 name
487  level2.increase_generation(l1_identifier, ssa_l1, fresh_l2_name_provider);
488  expr = set_indices<L2>(std::move(ssa_l1), ns).get();
489 
490  // and record that
492  symex_target!=nullptr, nullptr_exceptiont, "symex_target is null");
493  symex_target->shared_read(guard_as_expr, expr, atomic_section_id, source);
494 
495  return true;
496 }
497 
499  const ssa_exprt &expr,
500  const namespacet &ns) const
501 {
502  if(!record_events.top())
504 
505  PRECONDITION(dirty != nullptr);
506  const irep_idt &obj_identifier = expr.get_object_name();
507  if(
508  obj_identifier == guard_identifier() ||
509  (!ns.lookup(obj_identifier).is_shared() && !(*dirty)(obj_identifier)))
510  {
512  }
513 
514  // only continue if an indivisible object is being accessed
517 
518  if(atomic_section_id != 0)
520 
522 }
523 
527  const ssa_exprt &expr,
528  const namespacet &ns)
529 {
530  switch(write_is_shared(expr, ns))
531  {
533  return false;
535  {
537  return false;
538  }
540  break;
541  }
542 
543  // record a shared write
545  guard.as_expr(),
546  expr,
548  source);
549 
550  // do we have threads?
551  return threads.size() > 1;
552 }
553 
554 template <levelt level>
556 {
557  if(is_ssa_expr(expr))
558  {
559  ssa_exprt &ssa=to_ssa_expr(expr);
560 
561  // only do L1!
562  ssa = set_indices<L1>(std::move(ssa), ns).get();
563 
564  rename<level>(expr.type(), ssa.get_identifier(), ns);
565  ssa.update_type();
566  }
567  else if(expr.id()==ID_symbol)
568  {
569  expr=ssa_exprt(expr);
570  rename_address<level>(expr, ns);
571  }
572  else
573  {
574  if(expr.id()==ID_index)
575  {
576  index_exprt &index_expr=to_index_expr(expr);
577 
578  rename_address<level>(index_expr.array(), ns);
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  index_expr.index() =
584  rename<level>(std::move(index_expr.index()), ns).get();
585  }
586  else if(expr.id()==ID_if)
587  {
588  // the condition is not an address
589  if_exprt &if_expr=to_if_expr(expr);
590  if_expr.cond() = rename<level>(std::move(if_expr.cond()), ns).get();
591  rename_address<level>(if_expr.true_case(), ns);
592  rename_address<level>(if_expr.false_case(), ns);
593 
594  if_expr.type()=if_expr.true_case().type();
595  }
596  else if(expr.id()==ID_member)
597  {
598  member_exprt &member_expr=to_member_expr(expr);
599 
600  rename_address<level>(member_expr.struct_op(), ns);
601 
602  // type might not have been renamed in case of nesting of
603  // structs and pointers/arrays
604  if(
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<level>(expr.type(), irep_idt(), ns);
617  }
618  else
619  {
620  // this could go wrong, but we would have to re-typecheck ...
621  rename<level>(expr.type(), irep_idt(), ns);
622 
623  // do this recursively; we assume here
624  // that all the operands are addresses
625  Forall_operands(it, expr)
626  rename_address<level>(*it, ns);
627  }
628  }
629 }
630 
634 static bool requires_renaming(const typet &type, const namespacet &ns)
635 {
636  if(type.id() == ID_array)
637  {
638  const auto &array_type = to_array_type(type);
639  return requires_renaming(array_type.subtype(), ns) ||
640  !array_type.size().is_constant();
641  }
642  else if(type.id() == ID_struct || type.id() == ID_union)
643  {
644  const struct_union_typet &s_u_type = to_struct_union_type(type);
645  const struct_union_typet::componentst &components = s_u_type.components();
646 
647  for(auto &component : components)
648  {
649  // be careful, or it might get cyclic
650  if(component.type().id() == ID_array)
651  {
652  if(!to_array_type(component.type()).size().is_constant())
653  return true;
654  }
655  else if(
656  component.type().id() != ID_pointer &&
657  requires_renaming(component.type(), ns))
658  {
659  return true;
660  }
661  }
662 
663  return false;
664  }
665  else if(type.id() == ID_pointer)
666  {
667  return requires_renaming(to_pointer_type(type).subtype(), ns);
668  }
669  else if(type.id() == ID_union_tag)
670  {
671  const symbolt &symbol = ns.lookup(to_union_tag_type(type));
672  return requires_renaming(symbol.type, ns);
673  }
674  else if(type.id() == ID_struct_tag)
675  {
676  const symbolt &symbol = ns.lookup(to_struct_tag_type(type));
677  return requires_renaming(symbol.type, ns);
678  }
679 
680  return false;
681 }
682 
683 template <levelt level>
685  typet &type,
686  const irep_idt &l1_identifier,
687  const namespacet &ns)
688 {
689  // check whether there are symbol expressions in the type; if not, there
690  // is no need to expand the struct/union tags in the type
691  if(!requires_renaming(type, ns))
692  return; // no action
693 
694  // rename all the symbols with their last known value
695  // to the given level
696 
697  std::pair<l1_typest::iterator, bool> l1_type_entry;
698  if(level==L2 &&
699  !l1_identifier.empty())
700  {
701  l1_type_entry=l1_types.insert(std::make_pair(l1_identifier, type));
702 
703  if(!l1_type_entry.second) // was already in map
704  {
705  // do not change a complete array type to an incomplete one
706 
707  const typet &type_prev=l1_type_entry.first->second;
708 
709  if(type.id()!=ID_array ||
710  type_prev.id()!=ID_array ||
711  to_array_type(type).is_incomplete() ||
712  to_array_type(type_prev).is_complete())
713  {
714  type=l1_type_entry.first->second;
715  return;
716  }
717  }
718  }
719 
720  // expand struct and union tag types
721  type = ns.follow(type);
722 
723  if(type.id()==ID_array)
724  {
725  auto &array_type = to_array_type(type);
726  rename<level>(array_type.subtype(), irep_idt(), ns);
727  array_type.size() = rename<level>(std::move(array_type.size()), ns).get();
728  }
729  else if(type.id() == ID_struct || type.id() == ID_union)
730  {
732  struct_union_typet::componentst &components=s_u_type.components();
733 
734  for(auto &component : components)
735  {
736  // be careful, or it might get cyclic
737  if(component.type().id() == ID_array)
738  {
739  auto &array_type = to_array_type(component.type());
740  array_type.size() =
741  rename<level>(std::move(array_type.size()), ns).get();
742  }
743  else if(component.type().id() != ID_pointer)
744  rename<level>(component.type(), irep_idt(), ns);
745  }
746  }
747  else if(type.id()==ID_pointer)
748  {
749  rename<level>(to_pointer_type(type).subtype(), irep_idt(), ns);
750  }
751 
752  if(level==L2 &&
753  !l1_identifier.empty())
754  l1_type_entry.first->second=type;
755 }
756 
757 static void get_l1_name(exprt &expr)
758 {
759  // do not reset the type !
760 
761  if(is_ssa_expr(expr))
762  to_ssa_expr(expr).remove_level_2();
763  else
764  Forall_operands(it, expr)
765  get_l1_name(*it);
766 }
767 
773 void goto_symex_statet::print_backtrace(std::ostream &out) const
774 {
775  if(threads[source.thread_nr].call_stack.empty())
776  {
777  out << "No stack!\n";
778  return;
779  }
780 
781  out << source.function_id << " " << source.pc->location_number << "\n";
782 
783  for(auto stackit = threads[source.thread_nr].call_stack.rbegin(),
784  stackend = threads[source.thread_nr].call_stack.rend();
785  stackit != stackend;
786  ++stackit)
787  {
788  const auto &frame = *stackit;
789  out << frame.calling_location.function_id << " "
790  << frame.calling_location.pc->location_number << "\n";
791  }
792 }
793 
795  const symbol_exprt &expr,
796  std::function<std::size_t(const irep_idt &)> index_generator,
797  const namespacet &ns)
798 {
799  framet &frame = call_stack().top();
800 
801  const renamedt<ssa_exprt, L0> renamed = rename_ssa<L0>(ssa_exprt{expr}, ns);
802  const irep_idt l0_name = renamed.get_identifier();
803  const std::size_t l1_index = index_generator(l0_name);
804 
805  if(const auto old_value = level1.insert_or_replace(renamed, l1_index))
806  {
807  // save old L1 name
808  if(!frame.old_level1.has(renamed))
809  frame.old_level1.insert(renamed, old_value->second);
810  }
811 
812  const ssa_exprt ssa = rename_ssa<L1>(renamed.get(), ns).get();
813  const bool inserted = frame.local_objects.insert(ssa.get_identifier()).second;
814  INVARIANT(inserted, "l1_name expected to be unique by construction");
815 
816  return ssa;
817 }
818 
820 {
821  const irep_idt &l1_identifier = ssa.get_identifier();
822 
823  // rename type to L2
824  rename(ssa.type(), l1_identifier, ns);
825  ssa.update_type();
826 
827  // in case of pointers, put something into the value set
828  if(ssa.type().id() == ID_pointer)
829  {
830  exprt rhs;
831  if(
832  auto failed =
835  else
836  rhs = exprt(ID_invalid);
837 
838  exprt l1_rhs = rename<L1>(std::move(rhs), ns).get();
839  value_set.assign(ssa, l1_rhs, ns, true, false);
840  }
841 
842  // L2 renaming
843  const exprt fields = field_sensitivity.get_fields(ns, *this, ssa);
844  for(const auto &l1_symbol : find_symbols(fields))
845  {
846  const ssa_exprt &field_ssa = to_ssa_expr(l1_symbol);
847  const std::size_t field_generation = level2.increase_generation(
848  l1_symbol.get_identifier(), field_ssa, fresh_l2_name_provider);
849  CHECK_RETURN(field_generation == 1);
850  }
851 
852  record_events.push(false);
853  exprt expr_l2 = rename(std::move(ssa), ns).get();
854  INVARIANT(
855  is_ssa_expr(expr_l2),
856  "symbol to declare should not be replaced by constant propagation");
857  ssa = to_ssa_expr(expr_l2);
858  record_events.pop();
859 
860  return ssa;
861 }
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
guard_exprt
Definition: guard_expr.h:27
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
L2
@ L2
Definition: renamed.h:20
get_failed_symbol
optionalt< symbol_exprt > get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
Definition: add_failed_symbols.cpp:90
goto_symex_statet::print_backtrace
void print_backtrace(std::ostream &) const
Dumps the current state of symex, printing the function name and location number for each stack frame...
Definition: goto_symex_state.cpp:773
typet::subtype
const typet & subtype() const
Definition: type.h:47
goto_symex_statet::a_s_r_entryt
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
Definition: goto_symex_state.h:179
check_renaming_l1
bool check_renaming_l1(const exprt &expr)
Check that expr is correctly renamed to level 1 and return true in case an error is detected.
Definition: renaming_level.cpp:212
dirty.h
Variables whose address is taken.
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
goto_symex_statet::level1
symex_level1t level1
Definition: goto_symex_state.h:75
ssa_exprt::remove_level_2
void remove_level_2()
goto_symex_statet::assignment
NODISCARD renamedt< ssa_exprt, L2 > assignment(ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
Definition: goto_symex_state.cpp:77
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
L1
@ L1
Definition: renamed.h:18
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:208
goto_symex_statet::guard_identifier
static irep_idt guard_identifier()
Definition: goto_symex_state.h:141
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
value_sett::assign
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:1168
typet
The type of an expression, extends irept.
Definition: type.h:28
goto_symex_statet::l2_rename_rvalues
NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
Definition: goto_symex_state.cpp:289
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:43
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
goto_symex_statet::dirty
const incremental_dirtyt * dirty
Definition: goto_symex_state.h:214
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:56
goto_symex_statet::read_in_atomic_section
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
Definition: goto_symex_state.h:181
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
unsupported_operation_exceptiont
Thrown when we encounter an instruction, parameters to an instruction etc.
Definition: exception_utils.h:144
goto_symex_statet::~goto_symex_statet
~goto_symex_statet()
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
pointer_predicates.h
Various predicates over pointers in programs.
goto_symex_statet::fresh_l2_name_provider
std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider
Definition: goto_symex_state.h:260
format.h
goto_symex_statet::guard_manager
guard_managert & guard_manager
Definition: goto_symex_state.h:72
symex_targett::sourcet::thread_nr
unsigned thread_nr
Definition: symex_target.h:39
prefix.h
invariant.h
goto_symex_statet::written_in_atomic_section
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
Definition: goto_symex_state.h:183
exprt
Base class for all expressions.
Definition: expr.h:54
ssa_exprt::get_object_name
irep_idt get_object_name() const
guard_exprt::is_true
bool is_true() const
Definition: guard_expr.h:63
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:64
goto_symex_statet::is_read_only_object
static bool is_read_only_object(const exprt &lvalue)
Returns true if lvalue is a read-only object, such as the null object.
Definition: goto_symex_state.h:249
nullptr_exceptiont
Definition: base_exceptions.h:30
goto_symex_statet::rename_ssa
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
irep_idt
dstringt irep_idt
Definition: irep.h:37
symex_level2t::increase_generation
std::size_t increase_generation(const irep_idt &l1_identifier, const ssa_exprt &lhs, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
Allocates a fresh L2 name for the given L1 identifier, and makes it the latest generation on this pat...
Definition: renaming_level.cpp:135
guardt
guard_exprt guardt
Definition: guard.h:27
symex_level0
renamedt< ssa_exprt, L0 > symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)
Set the level 0 renaming of SSA expressions.
Definition: renaming_level.cpp:21
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
field_sensitivityt::apply
NODISCARD exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
Definition: field_sensitivity.cpp:33
goto_symex_statet::write_is_shared_resultt::SHARED
@ SHARED
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
renamedt::get
const underlyingt & get() const
Definition: renamed.h:34
goto_symex_is_constant.h
GOTO Symex constant propagation.
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2123
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:69
goto_symex_statet::goto_symex_statet
goto_symex_statet(const symex_targett::sourcet &, std::size_t max_field_sensitive_array_size, guard_managert &manager, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
Definition: goto_symex_state.cpp:36
goto_statet::propagation
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:71
is_shared
static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
Definition: race_check.cpp:122
to_complex_real_expr
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1715
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
array_typet::size
const exprt & size() const
Definition: std_types.h:765
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
base_exceptions.h
Generic exception types primarily designed for use with invariants.
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
call_stackt::new_frame
framet & new_frame(symex_targett::sourcet calling_location, const guardt &guard)
Definition: call_stack.h:30
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:141
goto_symex_statet::l2_thread_write_encoding
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)
thread encoding
Definition: goto_symex_state.cpp:526
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
goto_symex_statet::threads
std::vector< threadt > threads
Definition: goto_symex_state.h:198
L0
@ L0
Definition: renamed.h:17
byte_operators.h
Expression classes for byte-level operators.
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
goto_symex_statet::call_stack
call_stackt & call_stack()
Definition: goto_symex_state.h:147
as_const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
ssa_exprt::update_type
void update_type()
Definition: ssa_expr.h:28
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
call_stackt::top
framet & top()
Definition: call_stack.h:17
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
value_sett::output
void output(std::ostream &out, const std::string &indent="") const
Pretty-print this value-set.
Definition: value_set.cpp:136
goto_symex_statet::l2_thread_read_encoding
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
Definition: goto_symex_state.cpp:360
failed
static bool failed(bool error_indicator)
Definition: symtab2gb_parse_options.cpp:36
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:49
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:2557
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
goto_statet::level2
symex_level2t level2
Definition: goto_state.h:38
goto_symex_statet::write_is_shared_resultt
write_is_shared_resultt
Definition: goto_symex_state.h:201
goto_statet::guard
guardt guard
Definition: goto_state.h:58
goto_symex_statet::symex_target
symex_target_equationt * symex_target
Definition: goto_symex_state.h:73
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
index_exprt::index
exprt & index()
Definition: std_expr.h:1268
ssa_exprt::get_level_2
const irep_idt get_level_2() const
Definition: ssa_expr.h:73
index_exprt::array
exprt & array()
Definition: std_expr.h:1258
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
symex_level1t::insert
void insert(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Assume ssa is not already known.
Definition: renaming_level.cpp:46
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:468
dstringt::empty
bool empty() const
Definition: dstring.h:88
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
framet
Stack frames – these are used for function calls and for exceptions.
Definition: frame.h:21
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
framet::old_level1
symex_level1t old_level1
Definition: frame.h:36
find_symbols
void find_symbols(const exprt &src, find_symbols_sett &dest, bool current, bool next)
Add to the set dest the sub-expressions of src with id ID_symbol if current is true,...
Definition: find_symbols.cpp:24
goto_symex_is_constantt
Definition: goto_symex_is_constant.h:19
guard_exprt::is_false
bool is_false() const
Definition: guard_expr.h:68
goto_symex_statet::write_is_shared
write_is_shared_resultt write_is_shared(const ssa_exprt &expr, const namespacet &ns) const
Definition: goto_symex_state.cpp:498
L1_WITH_CONSTANT_PROPAGATION
@ L1_WITH_CONSTANT_PROPAGATION
Definition: renamed.h:19
to_complex_imag_expr
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1760
goto_statet
Container for data that varies per program point, e.g.
Definition: goto_state.h:32
symex_target_equationt::shared_write
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...
Definition: symex_target_equation.cpp:50
goto_symex_statet::field_sensitivity
field_sensitivityt field_sensitivity
Definition: goto_symex_state.h:124
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2234
goto_symex_statet::run_validation_checks
bool run_validation_checks
Should the additional validation checks be run?
Definition: goto_symex_state.h:226
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
struct_union_typet::componentt
Definition: std_types.h:63
expr_util.h
Deprecated expression utility functions.
format_expr.h
symex_targett::assignment_typet::PHI
@ PHI
requires_renaming
static bool requires_renaming(const typet &type, const namespacet &ns)
Return true if, and only if, the type or one of its subtypes requires SSA renaming.
Definition: goto_symex_state.cpp:634
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2113
goto_symex_state.h
Symbolic Execution.
remove_level_2
ssa_exprt remove_level_2(ssa_exprt ssa)
field_sensitivityt::is_divisible
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
Definition: field_sensitivity.cpp:349
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
goto_symex_statet::declare
ssa_exprt declare(ssa_exprt ssa, const namespacet &ns)
Add invalid (or a failed symbol) to the value_set if ssa is a pointer, ensure that level2 index of sy...
Definition: goto_symex_state.cpp:819
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_statet::atomic_section_id
unsigned atomic_section_id
Threads.
Definition: goto_state.h:76
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:53
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2103
check_renaming
bool check_renaming(const typet &type)
Check that type is correctly renamed to level 2 and return true in case an error is detected.
Definition: renaming_level.cpp:196
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
framet::local_objects
std::set< irep_idt > local_objects
Definition: frame.h:38
symex_target_equationt::shared_read
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...
Definition: symex_target_equation.cpp:34
get_l1_name
static void get_l1_name(exprt &expr)
Definition: goto_symex_state.cpp:757
goto_symex_statet::write_is_shared_resultt::NOT_SHARED
@ NOT_SHARED
INVARIANT_STRUCTURED
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:408
goto_symex_statet::write_is_shared_resultt::IN_ATOMIC_SECTION
@ IN_ATOMIC_SECTION
goto_symex_statet::record_events
std::stack< bool > record_events
Definition: goto_symex_state.h:212
symex_level1t::has
bool has(const renamedt< ssa_exprt, L0 > &ssa) const
Definition: renaming_level.cpp:70
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2611
goto_symex_statet::rename
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2541
field_sensitivityt::get_fields
exprt get_fields(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &ssa_expr) const
Compute an expression representing the individual components of a field-sensitive SSA representation ...
Definition: field_sensitivity.cpp:156
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:367
symex_level2t::latest_index
unsigned latest_index(const irep_idt &identifier) const
Counter corresponding to an identifier.
Definition: renaming_level.cpp:129
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38
add_failed_symbols.h
Pointer Dereferencing.
index_exprt
Array index operator.
Definition: std_expr.h:1242
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
symex_targett::sourcet::function_id
irep_idt function_id
Definition: symex_target.h:40
true_exprt
The Boolean constant true.
Definition: std_expr.h:2716
std_expr.h
API to expression classes.
goto_statet::value_set
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:51
goto_symex_statet::add_object
ssa_exprt add_object(const symbol_exprt &expr, std::function< std::size_t(const irep_idt &)> index_generator, const namespacet &ns)
Instantiate the object expr.
Definition: goto_symex_state.cpp:794
c_types.h
goto_symex_statet::rename_address
void rename_address(exprt &expr, const namespacet &ns)
Definition: goto_symex_state.cpp:555
goto_symex_statet::l1_types
l1_typest l1_types
Definition: goto_symex_state.h:137
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:27
as_const.h
symex_level1t::insert_or_replace
optionalt< std::pair< ssa_exprt, std::size_t > > insert_or_replace(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Set the index for ssa to index.
Definition: renaming_level.cpp:54
not_exprt
Boolean negation.
Definition: std_expr.h:2041
symex_target_equationt::assignment
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.
Definition: symex_target_equation.cpp:117