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/exception_utils.h>
22 #include <util/expr_util.h>
23 #include <util/format.h>
24 #include <util/format_expr.h>
25 #include <util/invariant.h>
27 #include <util/prefix.h>
28 #include <util/std_expr.h>
29 
30 #include <analyses/dirty.h>
32 
33 static void get_l1_name(exprt &expr);
34 
36  const symex_targett::sourcet &_source,
37  std::size_t max_field_sensitive_array_size,
38  guard_managert &manager,
39  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
40  : goto_statet(manager),
41  source(_source),
42  guard_manager(manager),
43  symex_target(nullptr),
44  field_sensitivity(max_field_sensitive_array_size),
45  record_events({true}),
46  fresh_l2_name_provider(fresh_l2_name_provider)
47 {
48  threads.emplace_back(guard_manager);
50 }
51 
53 
54 template <>
56 goto_symex_statet::set_indices<L0>(ssa_exprt ssa_expr, const namespacet &ns)
57 {
58  return symex_level0(std::move(ssa_expr), ns, source.thread_nr);
59 }
60 
61 template <>
63 goto_symex_statet::set_indices<L1>(ssa_exprt ssa_expr, const namespacet &ns)
64 {
65  return level1(symex_level0(std::move(ssa_expr), ns, source.thread_nr));
66 }
67 
68 template <>
70 goto_symex_statet::set_indices<L2>(ssa_exprt ssa_expr, const namespacet &ns)
71 {
72  return level2(
73  level1(symex_level0(std::move(ssa_expr), ns, source.thread_nr)));
74 }
75 
77  ssa_exprt lhs, // L0/L1
78  const exprt &rhs, // L2
79  const namespacet &ns,
80  bool rhs_is_simplified,
81  bool record_value,
82  bool allow_pointer_unsoundness)
83 {
84  // identifier should be l0 or l1, make sure it's l1
85  lhs = rename_ssa<L1>(std::move(lhs), ns).get();
86  irep_idt l1_identifier=lhs.get_identifier();
87 
88  // the type might need renaming
89  rename<L2>(lhs.type(), l1_identifier, ns);
90  lhs.update_type();
92  {
93  DATA_INVARIANT(!check_renaming_l1(lhs), "lhs renaming failed on l1");
94  }
95 
96  // do the l2 renaming
98  renamedt<ssa_exprt, L2> l2_lhs = set_indices<L2>(std::move(lhs), ns);
99  lhs = l2_lhs.get();
100 
101  // in case we happen to be multi-threaded, record the memory access
102  bool is_shared=l2_thread_write_encoding(lhs, ns);
103 
105  {
106  DATA_INVARIANT(!check_renaming(lhs), "lhs renaming failed on l2");
107  DATA_INVARIANT(!check_renaming(rhs), "rhs renaming failed on l2");
108  }
109 
110  // see #305 on GitHub for a simple example and possible discussion
111  if(is_shared && lhs.type().id() == ID_pointer && !allow_pointer_unsoundness)
113  "pointer handling for concurrency is unsound");
114 
115  // Update constant propagation map -- the RHS is L2
116  if(!is_shared && record_value && goto_symex_is_constantt()(rhs))
117  {
118  const auto propagation_entry = propagation.find(l1_identifier);
119  if(!propagation_entry.has_value())
120  propagation.insert(l1_identifier, rhs);
121  else if(propagation_entry->get() != rhs)
122  propagation.replace(l1_identifier, rhs);
123  }
124  else
125  propagation.erase_if_exists(l1_identifier);
126 
127  {
128  // update value sets
129  exprt l1_rhs(rhs);
130  get_l1_name(l1_rhs);
131 
132  const ssa_exprt l1_lhs = remove_level_2(lhs);
134  {
135  DATA_INVARIANT(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
136  DATA_INVARIANT(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
137  }
138 
139  value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
140  }
141 
142 #ifdef DEBUG
143  std::cout << "Assigning " << l1_identifier << '\n';
144  value_set.output(std::cout);
145  std::cout << "**********************\n";
146 #endif
147 
148  return l2_lhs;
149 }
150 
151 template <levelt level>
154 {
155  static_assert(
156  level == L0 || level == L1,
157  "rename_ssa can only be used for levels L0 and L1");
158  ssa = set_indices<level>(std::move(ssa), ns).get();
159  rename<level>(ssa.type(), ssa.get_identifier(), ns);
160  ssa.update_type();
161  return renamedt<ssa_exprt, level>{ssa};
162 }
163 
166 goto_symex_statet::rename_ssa<L0>(ssa_exprt ssa, const namespacet &ns);
168 goto_symex_statet::rename_ssa<L1>(ssa_exprt ssa, const namespacet &ns);
169 
170 template <levelt level>
173 {
174  // rename all the symbols with their last known value
175 
176  static_assert(
177  level == L0 || level == L1 || level == L1_WITH_CONSTANT_PROPAGATION ||
178  level == L2,
179  "must handle all renaming levels");
180 
181  if(expr.id()==ID_symbol &&
182  expr.get_bool(ID_C_SSA_symbol))
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
256  {
257  rename<level>(expr.type(), irep_idt(), ns);
258 
259  // do this recursively
260  Forall_operands(it, expr)
261  *it = rename<level>(std::move(*it), ns).get();
262 
263  const exprt &c_expr = as_const(expr);
264  INVARIANT(
265  (expr.id() != ID_with ||
266  c_expr.type() == to_with_expr(c_expr).old().type()) &&
267  (expr.id() != ID_if ||
268  (c_expr.type() == to_if_expr(c_expr).true_case().type() &&
269  c_expr.type() == to_if_expr(c_expr).false_case().type())),
270  "Type of renamed expr should be the same as operands for with_exprt and "
271  "if_exprt");
272 
273  if(level == L2)
274  expr = field_sensitivity.apply(ns, *this, std::move(expr), false);
275 
276  return renamedt<exprt, level>{std::move(expr)};
277  }
278 }
279 
280 // Explicitly instantiate the one version of this function without an explicit
281 // caller in this file:
284 
286 {
287  rename(lvalue.type(), irep_idt(), ns);
288 
289  if(lvalue.id() == ID_symbol)
290  {
291  // Nothing to do
292  }
293  else if(is_read_only_object(lvalue))
294  {
295  // Ignore apparent writes to 'NULL-object' and similar read-only objects
296  }
297  else if(lvalue.id() == ID_typecast)
298  {
299  auto &typecast_lvalue = to_typecast_expr(lvalue);
300  typecast_lvalue.op() = l2_rename_rvalues(typecast_lvalue.op(), ns);
301  }
302  else if(lvalue.id() == ID_member)
303  {
304  auto &member_lvalue = to_member_expr(lvalue);
305  member_lvalue.compound() = l2_rename_rvalues(member_lvalue.compound(), ns);
306  }
307  else if(lvalue.id() == ID_index)
308  {
309  // The index is an rvalue:
310  auto &index_lvalue = to_index_expr(lvalue);
311  index_lvalue.array() = l2_rename_rvalues(index_lvalue.array(), ns);
312  index_lvalue.index() = rename(index_lvalue.index(), ns).get();
313  }
314  else if(
315  lvalue.id() == ID_byte_extract_little_endian ||
316  lvalue.id() == ID_byte_extract_big_endian)
317  {
318  // The offset is an rvalue:
319  auto &byte_extract_lvalue = to_byte_extract_expr(lvalue);
320  byte_extract_lvalue.op() = l2_rename_rvalues(byte_extract_lvalue.op(), ns);
321  byte_extract_lvalue.offset() = rename(byte_extract_lvalue.offset(), ns);
322  }
323  else if(lvalue.id() == ID_if)
324  {
325  // The condition is an rvalue:
326  auto &if_lvalue = to_if_expr(lvalue);
327  if_lvalue.cond() = rename(if_lvalue.cond(), ns);
328  if(!if_lvalue.cond().is_false())
329  if_lvalue.true_case() = l2_rename_rvalues(if_lvalue.true_case(), ns);
330  if(!if_lvalue.cond().is_true())
331  if_lvalue.false_case() = l2_rename_rvalues(if_lvalue.false_case(), ns);
332  }
333  else if(lvalue.id() == ID_complex_real)
334  {
335  auto &complex_real_lvalue = to_complex_real_expr(lvalue);
336  complex_real_lvalue.op() = l2_rename_rvalues(complex_real_lvalue.op(), ns);
337  }
338  else if(lvalue.id() == ID_complex_imag)
339  {
340  auto &complex_imag_lvalue = to_complex_imag_expr(lvalue);
341  complex_imag_lvalue.op() = l2_rename_rvalues(complex_imag_lvalue.op(), ns);
342  }
343  else
344  {
346  "l2_rename_rvalues case `" + lvalue.id_string() + "' not handled");
347  }
348 
349  return lvalue;
350 }
351 
352 template renamedt<exprt, L1>
353 goto_symex_statet::rename<L1>(exprt expr, const namespacet &ns);
354 
357  ssa_exprt &expr,
358  const namespacet &ns)
359 {
360  // do we have threads?
361  if(threads.size()<=1)
362  return false;
363 
364  // is it a shared object?
365  PRECONDITION(dirty != nullptr);
366  const irep_idt &obj_identifier=expr.get_object_name();
367  if(
368  obj_identifier == guard_identifier() ||
369  (!ns.lookup(obj_identifier).is_shared() && !(*dirty)(obj_identifier)))
370  {
371  return false;
372  }
373 
374  // only continue if an indivisible object is being accessed
376  return false;
377 
378  const ssa_exprt ssa_l1 = remove_level_2(expr);
379  const irep_idt &l1_identifier=ssa_l1.get_identifier();
380  const exprt guard_as_expr = guard.as_expr();
381 
382  // see whether we are within an atomic section
383  if(atomic_section_id!=0)
384  {
385  guardt write_guard{false_exprt{}, guard_manager};
386 
387  const auto a_s_writes = written_in_atomic_section.find(ssa_l1);
388  if(a_s_writes!=written_in_atomic_section.end())
389  {
390  for(const auto &guard_in_list : a_s_writes->second)
391  {
392  guardt g = guard_in_list;
393  g-=guard;
394  if(g.is_true())
395  // there has already been a write to l1_identifier within
396  // this atomic section under the same guard, or a guard
397  // that implies the current one
398  return false;
399 
400  write_guard |= guard_in_list;
401  }
402  }
403 
404  not_exprt no_write(write_guard.as_expr());
405 
406  // we cannot determine for sure that there has been a write already
407  // so generate a read even if l1_identifier has been written on
408  // all branches flowing into this read
409  guardt read_guard{false_exprt{}, guard_manager};
410 
411  a_s_r_entryt &a_s_read=read_in_atomic_section[ssa_l1];
412  for(const auto &a_s_read_guard : a_s_read.second)
413  {
414  guardt g = a_s_read_guard; // copy
415  g-=guard;
416  if(g.is_true())
417  // there has already been a read l1_identifier within
418  // this atomic section under the same guard, or a guard
419  // that implies the current one
420  return false;
421 
422  read_guard |= a_s_read_guard;
423  }
424 
425  guardt cond = read_guard;
426  if(!no_write.op().is_false())
427  cond |= guardt{no_write.op(), guard_manager};
428 
429  const renamedt<ssa_exprt, L2> l2_true_case = set_indices<L2>(ssa_l1, ns);
430 
431  if(a_s_read.second.empty())
432  {
433  level2.increase_generation(l1_identifier, ssa_l1, fresh_l2_name_provider);
434  a_s_read.first = level2.latest_index(l1_identifier);
435  }
436  const renamedt<ssa_exprt, L2> l2_false_case = set_indices<L2>(ssa_l1, ns);
437 
438  exprt tmp;
439  if(cond.is_false())
440  tmp = l2_false_case.get();
441  else
442  tmp = if_exprt{cond.as_expr(), l2_true_case.get(), l2_false_case.get()};
443 
444  record_events.push(false);
445  ssa_exprt ssa_l2 = assignment(std::move(ssa_l1), tmp, ns, true, true).get();
446  record_events.pop();
447 
449  guard_as_expr,
450  ssa_l2,
451  ssa_l2,
452  ssa_l2.get_original_expr(),
453  tmp,
454  source,
456 
457  INVARIANT(!check_renaming(ssa_l2), "expr should be renamed to L2");
458  expr = std::move(ssa_l2);
459 
460  a_s_read.second.push_back(guard);
461  if(!no_write.op().is_false())
462  a_s_read.second.back().add(no_write);
463 
464  return true;
465  }
466 
467  // No event and no fresh index, but avoid constant propagation
468  if(!record_events.top())
469  {
470  expr = set_indices<L2>(std::move(ssa_l1), ns).get();
471  return true;
472  }
473 
474  // produce a fresh L2 name
475  level2.increase_generation(l1_identifier, ssa_l1, fresh_l2_name_provider);
476  expr = set_indices<L2>(std::move(ssa_l1), ns).get();
477 
478  // and record that
480  symex_target!=nullptr, nullptr_exceptiont, "symex_target is null");
481  symex_target->shared_read(guard_as_expr, expr, atomic_section_id, source);
482 
483  return true;
484 }
485 
487  const ssa_exprt &expr,
488  const namespacet &ns) const
489 {
490  if(!record_events.top())
492 
493  PRECONDITION(dirty != nullptr);
494  const irep_idt &obj_identifier = expr.get_object_name();
495  if(
496  obj_identifier == guard_identifier() ||
497  (!ns.lookup(obj_identifier).is_shared() && !(*dirty)(obj_identifier)))
498  {
500  }
501 
502  // only continue if an indivisible object is being accessed
505 
506  if(atomic_section_id != 0)
508 
510 }
511 
515  const ssa_exprt &expr,
516  const namespacet &ns)
517 {
518  switch(write_is_shared(expr, ns))
519  {
521  return false;
523  {
525  return false;
526  }
528  break;
529  }
530 
531  // record a shared write
533  guard.as_expr(),
534  expr,
536  source);
537 
538  // do we have threads?
539  return threads.size() > 1;
540 }
541 
542 template <levelt level>
544 {
545  if(expr.id()==ID_symbol &&
546  expr.get_bool(ID_C_SSA_symbol))
547  {
548  ssa_exprt &ssa=to_ssa_expr(expr);
549 
550  // only do L1!
551  ssa = set_indices<L1>(std::move(ssa), ns).get();
552 
553  rename<level>(expr.type(), ssa.get_identifier(), ns);
554  ssa.update_type();
555  }
556  else if(expr.id()==ID_symbol)
557  {
558  expr=ssa_exprt(expr);
559  rename_address<level>(expr, ns);
560  }
561  else
562  {
563  if(expr.id()==ID_index)
564  {
565  index_exprt &index_expr=to_index_expr(expr);
566 
567  rename_address<level>(index_expr.array(), ns);
568  PRECONDITION(index_expr.array().type().id() == ID_array);
569  expr.type() = to_array_type(index_expr.array().type()).subtype();
570 
571  // the index is not an address
572  index_expr.index() =
573  rename<level>(std::move(index_expr.index()), ns).get();
574  }
575  else if(expr.id()==ID_if)
576  {
577  // the condition is not an address
578  if_exprt &if_expr=to_if_expr(expr);
579  if_expr.cond() = rename<level>(std::move(if_expr.cond()), ns).get();
580  rename_address<level>(if_expr.true_case(), ns);
581  rename_address<level>(if_expr.false_case(), ns);
582 
583  if_expr.type()=if_expr.true_case().type();
584  }
585  else if(expr.id()==ID_member)
586  {
587  member_exprt &member_expr=to_member_expr(expr);
588 
589  rename_address<level>(member_expr.struct_op(), ns);
590 
591  // type might not have been renamed in case of nesting of
592  // structs and pointers/arrays
593  if(
594  member_expr.struct_op().type().id() != ID_struct_tag &&
595  member_expr.struct_op().type().id() != ID_union_tag)
596  {
597  const struct_union_typet &su_type=
598  to_struct_union_type(member_expr.struct_op().type());
599  const struct_union_typet::componentt &comp=
600  su_type.get_component(member_expr.get_component_name());
601  PRECONDITION(comp.is_not_nil());
602  expr.type()=comp.type();
603  }
604  else
605  rename<level>(expr.type(), irep_idt(), ns);
606  }
607  else
608  {
609  // this could go wrong, but we would have to re-typecheck ...
610  rename<level>(expr.type(), irep_idt(), ns);
611 
612  // do this recursively; we assume here
613  // that all the operands are addresses
614  Forall_operands(it, expr)
615  rename_address<level>(*it, ns);
616  }
617  }
618 }
619 
623 static bool requires_renaming(const typet &type, const namespacet &ns)
624 {
625  if(type.id() == ID_array)
626  {
627  const auto &array_type = to_array_type(type);
628  return requires_renaming(array_type.subtype(), ns) ||
629  !array_type.size().is_constant();
630  }
631  else if(type.id() == ID_struct || type.id() == ID_union)
632  {
633  const struct_union_typet &s_u_type = to_struct_union_type(type);
634  const struct_union_typet::componentst &components = s_u_type.components();
635 
636  for(auto &component : components)
637  {
638  // be careful, or it might get cyclic
639  if(component.type().id() == ID_array)
640  {
641  if(!to_array_type(component.type()).size().is_constant())
642  return true;
643  }
644  else if(
645  component.type().id() != ID_pointer &&
646  requires_renaming(component.type(), ns))
647  {
648  return true;
649  }
650  }
651 
652  return false;
653  }
654  else if(type.id() == ID_pointer)
655  {
656  return requires_renaming(to_pointer_type(type).subtype(), ns);
657  }
658  else if(type.id() == ID_union_tag)
659  {
660  const symbolt &symbol = ns.lookup(to_union_tag_type(type));
661  return requires_renaming(symbol.type, ns);
662  }
663  else if(type.id() == ID_struct_tag)
664  {
665  const symbolt &symbol = ns.lookup(to_struct_tag_type(type));
666  return requires_renaming(symbol.type, ns);
667  }
668 
669  return false;
670 }
671 
672 template <levelt level>
674  typet &type,
675  const irep_idt &l1_identifier,
676  const namespacet &ns)
677 {
678  // check whether there are symbol expressions in the type; if not, there
679  // is no need to expand the struct/union tags in the type
680  if(!requires_renaming(type, ns))
681  return; // no action
682 
683  // rename all the symbols with their last known value
684  // to the given level
685 
686  std::pair<l1_typest::iterator, bool> l1_type_entry;
687  if(level==L2 &&
688  !l1_identifier.empty())
689  {
690  l1_type_entry=l1_types.insert(std::make_pair(l1_identifier, type));
691 
692  if(!l1_type_entry.second) // was already in map
693  {
694  // do not change a complete array type to an incomplete one
695 
696  const typet &type_prev=l1_type_entry.first->second;
697 
698  if(type.id()!=ID_array ||
699  type_prev.id()!=ID_array ||
700  to_array_type(type).is_incomplete() ||
701  to_array_type(type_prev).is_complete())
702  {
703  type=l1_type_entry.first->second;
704  return;
705  }
706  }
707  }
708 
709  // expand struct and union tag types
710  type = ns.follow(type);
711 
712  if(type.id()==ID_array)
713  {
714  auto &array_type = to_array_type(type);
715  rename<level>(array_type.subtype(), irep_idt(), ns);
716  array_type.size() = rename<level>(std::move(array_type.size()), ns).get();
717  }
718  else if(type.id() == ID_struct || type.id() == ID_union)
719  {
721  struct_union_typet::componentst &components=s_u_type.components();
722 
723  for(auto &component : components)
724  {
725  // be careful, or it might get cyclic
726  if(component.type().id() == ID_array)
727  {
728  auto &array_type = to_array_type(component.type());
729  array_type.size() =
730  rename<level>(std::move(array_type.size()), ns).get();
731  }
732  else if(component.type().id() != ID_pointer)
733  rename<level>(component.type(), irep_idt(), ns);
734  }
735  }
736  else if(type.id()==ID_pointer)
737  {
738  rename<level>(to_pointer_type(type).subtype(), irep_idt(), ns);
739  }
740 
741  if(level==L2 &&
742  !l1_identifier.empty())
743  l1_type_entry.first->second=type;
744 }
745 
746 static void get_l1_name(exprt &expr)
747 {
748  // do not reset the type !
749 
750  if(expr.id()==ID_symbol &&
751  expr.get_bool(ID_C_SSA_symbol))
752  to_ssa_expr(expr).remove_level_2();
753  else
754  Forall_operands(it, expr)
755  get_l1_name(*it);
756 }
757 
763 void goto_symex_statet::print_backtrace(std::ostream &out) const
764 {
765  if(threads[source.thread_nr].call_stack.empty())
766  {
767  out << "No stack!\n";
768  return;
769  }
770 
771  out << source.function_id << " " << source.pc->location_number << "\n";
772 
773  for(auto stackit = threads[source.thread_nr].call_stack.rbegin(),
774  stackend = threads[source.thread_nr].call_stack.rend();
775  stackit != stackend;
776  ++stackit)
777  {
778  const auto &frame = *stackit;
779  out << frame.calling_location.function_id << " "
780  << frame.calling_location.pc->location_number << "\n";
781  }
782 }
783 
785  const symbol_exprt &expr,
786  std::function<std::size_t(const irep_idt &)> index_generator,
787  const namespacet &ns)
788 {
789  framet &frame = call_stack().top();
790 
791  const renamedt<ssa_exprt, L0> renamed = rename_ssa<L0>(ssa_exprt{expr}, ns);
792  const irep_idt l0_name = renamed.get_identifier();
793  const auto l1_index = narrow_cast<unsigned>(index_generator(l0_name));
794 
795  if(const auto old_value = level1.insert_or_replace(renamed, l1_index))
796  {
797  // save old L1 name
798  if(!frame.old_level1.has(renamed))
799  frame.old_level1.insert(renamed, old_value->second);
800  }
801 
802  const ssa_exprt ssa = rename_ssa<L1>(renamed.get(), ns).get();
803  const bool inserted = frame.local_objects.insert(ssa.get_identifier()).second;
804  INVARIANT(inserted, "l1_name expected to be unique by construction");
805 
806  return ssa;
807 }
808 
810 {
811  const irep_idt &l1_identifier = ssa.get_identifier();
812 
813  // rename type to L2
814  rename(ssa.type(), l1_identifier, ns);
815  ssa.update_type();
816 
817  // in case of pointers, put something into the value set
818  if(ssa.type().id() == ID_pointer)
819  {
820  exprt rhs;
821  if(
822  auto failed =
825  else
826  rhs = exprt(ID_invalid);
827 
828  exprt l1_rhs = rename<L1>(std::move(rhs), ns).get();
829  value_set.assign(ssa, l1_rhs, ns, true, false);
830  }
831 
832  // L2 renaming
833  const exprt fields = field_sensitivity.get_fields(ns, *this, ssa);
834  for(const auto &l1_symbol : find_symbols(fields))
835  {
836  const ssa_exprt &field_ssa = to_ssa_expr(l1_symbol);
837  const std::size_t field_generation = level2.increase_generation(
838  l1_symbol.get_identifier(), field_ssa, fresh_l2_name_provider);
839  CHECK_RETURN(field_generation == 1);
840  }
841 
842  record_events.push(false);
843  exprt expr_l2 = rename(std::move(ssa), ns).get();
844  INVARIANT(
845  expr_l2.id() == ID_symbol && expr_l2.get_bool(ID_C_SSA_symbol),
846  "symbol to declare should not be replaced by constant propagation");
847  ssa = to_ssa_expr(expr_l2);
848  record_events.pop();
849 
850  return ssa;
851 }
guard_exprt
Definition: guard_expr.h:26
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
exception_utils.h
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:555
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
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:763
array_typet::is_incomplete
bool is_incomplete() const
Definition: std_types.h:988
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:225
dirty.h
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
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:76
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
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:209
goto_symex_statet::guard_identifier
static irep_idt guard_identifier()
Definition: goto_symex_state.h:141
array_typet::is_complete
bool is_complete() const
Definition: std_types.h:983
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:1203
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:285
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:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
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:143
goto_symex_statet::~goto_symex_statet
~goto_symex_statet()
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2963
pointer_predicates.h
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:52
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:135
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:29
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:192
irep_idt
dstringt irep_idt
Definition: irep.h:32
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:148
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:34
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
field_sensitivityt::apply
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:21
goto_symex_statet::write_is_shared_resultt::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
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
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:35
goto_statet::propagation
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:63
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:1766
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:16
array_typet::size
const exprt & size() const
Definition: std_types.h:973
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
base_exceptions.h
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:22
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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:140
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:514
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
goto_symex_statet::threads
std::vector< threadt > threads
Definition: goto_symex_state.h:198
with_exprt::old
exprt & old()
Definition: std_expr.h:3060
L0
Definition: renamed.h:17
byte_operators.h
Expression classes for byte-level operators.
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:148
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
value_sett::output
void output(std::ostream &out, const std::string &indent="") const
Pretty-print this value-set.
Definition: value_set.cpp:144
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:356
failed
static bool failed(bool error_indicator)
Definition: symtab2gb_parse_options.cpp:34
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:3435
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
goto_statet::level2
symex_level2t level2
Definition: goto_state.h:34
goto_symex_statet::write_is_shared_resultt
write_is_shared_resultt
Definition: goto_symex_state.h:200
goto_statet::guard
guardt guard
Definition: goto_state.h:50
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:421
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
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:1309
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:59
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:515
dstringt::empty
bool empty() const
Definition: dstring.h:88
false_exprt
The Boolean constant false.
Definition: std_expr.h:3963
framet
Stack frames – these are used for function calls and for exceptions.
Definition: frame.h:20
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:23
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
goto_symex_is_constantt
Definition: goto_symex_is_constant.h:18
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:486
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:1811
goto_statet
Container for data that varies per program point, e.g.
Definition: goto_state.h:27
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:48
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:3112
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:3404
struct_union_typet::componentt
Definition: std_types.h:63
expr_util.h
Deprecated expression utility functions.
format_expr.h
symex_targett::assignment_typet::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:623
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
goto_symex_state.h
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:341
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
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:809
symbolt
Symbol table entry.
Definition: symbol.h:27
goto_statet::atomic_section_id
unsigned atomic_section_id
Threads.
Definition: goto_state.h:68
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
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:209
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
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:32
get_l1_name
static void get_l1_name(exprt &expr)
Definition: goto_symex_state.cpp:746
goto_symex_statet::write_is_shared_resultt::NOT_SHARED
INVARIANT_STRUCTURED
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:408
goto_symex_statet::write_is_shared_resultt::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:83
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
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:3419
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:147
symex_level2t::latest_index
unsigned latest_index(const irep_idt &identifier) const
Counter corresponding to an identifier.
Definition: renaming_level.cpp:142
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
add_failed_symbols.h
index_exprt
Array index operator.
Definition: std_expr.h:1292
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2785
symex_targett::sourcet::function_id
irep_idt function_id
Definition: symex_target.h:40
true_exprt
The Boolean constant true.
Definition: std_expr.h:3954
std_expr.h
goto_statet::value_set
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:43
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:784
goto_symex_statet::rename_address
void rename_address(exprt &expr, const namespacet &ns)
Definition: goto_symex_state.cpp:543
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:26
as_const.h
validation_modet::INVARIANT
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:67
not_exprt
Boolean negation.
Definition: std_expr.h:2842
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:115