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(is_ssa_expr(expr))
182  {
183  exprt original_expr = expr;
184  ssa_exprt &ssa=to_ssa_expr(expr);
185 
186  if(level == L0)
187  {
188  return renamedt<exprt, level>{
189  std::move(rename_ssa<L0>(std::move(ssa), ns).value())};
190  }
191  else if(level == L1)
192  {
193  return renamedt<exprt, level>{
194  std::move(rename_ssa<L1>(std::move(ssa), ns).value())};
195  }
196  else
197  {
198  ssa = set_indices<L1>(std::move(ssa), ns).get();
199  rename<level>(expr.type(), ssa.get_identifier(), ns);
200  ssa.update_type();
201 
202  // renaming taken care of by l2_thread_encoding, or already at L2
203  if(l2_thread_read_encoding(ssa, ns) || !ssa.get_level_2().empty())
204  {
205  if(level == L1_WITH_CONSTANT_PROPAGATION)
206  {
207  // Don't actually rename to L2 -- we just used `ssa` to check whether
208  // constant-propagation was applicable
209  return renamedt<exprt, level>(std::move(original_expr));
210  }
211  else
212  return renamedt<exprt, level>(std::move(ssa));
213  }
214  else
215  {
216  // We also consider propagation if we go up to L2.
217  // L1 identifiers are used for propagation!
218  auto p_it = propagation.find(ssa.get_identifier());
219 
220  if(p_it.has_value())
221  {
222  return renamedt<exprt, level>(*p_it); // already L2
223  }
224  else
225  {
226  if(level == L2)
227  ssa = set_indices<L2>(std::move(ssa), ns).get();
228  return renamedt<exprt, level>(std::move(ssa));
229  }
230  }
231  }
232  }
233  else if(expr.id()==ID_symbol)
234  {
235  const auto &type = as_const(expr).type();
236 
237  // we never rename function symbols
238  if(type.id() == ID_code || type.id() == ID_mathematical_function)
239  {
240  rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
241  return renamedt<exprt, level>{std::move(expr)};
242  }
243  else
244  return rename<level>(ssa_exprt{expr}, ns);
245  }
246  else if(expr.id()==ID_address_of)
247  {
248  auto &address_of_expr = to_address_of_expr(expr);
249  rename_address<level>(address_of_expr.object(), ns);
250  to_pointer_type(expr.type()).subtype() =
251  as_const(address_of_expr).object().type();
252  return renamedt<exprt, level>{std::move(expr)};
253  }
254  else if(expr.is_nil())
255  {
256  return renamedt<exprt, level>{std::move(expr)};
257  }
258  else
259  {
260  rename<level>(expr.type(), irep_idt(), ns);
261 
262  // do this recursively
263  Forall_operands(it, expr)
264  *it = rename<level>(std::move(*it), ns).get();
265 
266  const exprt &c_expr = as_const(expr);
267  INVARIANT(
268  (expr.id() != ID_with ||
269  c_expr.type() == to_with_expr(c_expr).old().type()) &&
270  (expr.id() != ID_if ||
271  (c_expr.type() == to_if_expr(c_expr).true_case().type() &&
272  c_expr.type() == to_if_expr(c_expr).false_case().type())),
273  "Type of renamed expr should be the same as operands for with_exprt and "
274  "if_exprt");
275 
276  if(level == L2)
277  expr = field_sensitivity.apply(ns, *this, std::move(expr), false);
278 
279  return renamedt<exprt, level>{std::move(expr)};
280  }
281 }
282 
283 // Explicitly instantiate the one version of this function without an explicit
284 // caller in this file:
287 
289 {
290  rename(lvalue.type(), irep_idt(), ns);
291 
292  if(lvalue.id() == ID_symbol)
293  {
294  // Nothing to do
295  }
296  else if(is_read_only_object(lvalue))
297  {
298  // Ignore apparent writes to 'NULL-object' and similar read-only objects
299  }
300  else if(lvalue.id() == ID_typecast)
301  {
302  auto &typecast_lvalue = to_typecast_expr(lvalue);
303  typecast_lvalue.op() = l2_rename_rvalues(typecast_lvalue.op(), ns);
304  }
305  else if(lvalue.id() == ID_member)
306  {
307  auto &member_lvalue = to_member_expr(lvalue);
308  member_lvalue.compound() = l2_rename_rvalues(member_lvalue.compound(), ns);
309  }
310  else if(lvalue.id() == ID_index)
311  {
312  // The index is an rvalue:
313  auto &index_lvalue = to_index_expr(lvalue);
314  index_lvalue.array() = l2_rename_rvalues(index_lvalue.array(), ns);
315  index_lvalue.index() = rename(index_lvalue.index(), ns).get();
316  }
317  else if(
318  lvalue.id() == ID_byte_extract_little_endian ||
319  lvalue.id() == ID_byte_extract_big_endian)
320  {
321  // The offset is an rvalue:
322  auto &byte_extract_lvalue = to_byte_extract_expr(lvalue);
323  byte_extract_lvalue.op() = l2_rename_rvalues(byte_extract_lvalue.op(), ns);
324  byte_extract_lvalue.offset() = rename(byte_extract_lvalue.offset(), ns);
325  }
326  else if(lvalue.id() == ID_if)
327  {
328  // The condition is an rvalue:
329  auto &if_lvalue = to_if_expr(lvalue);
330  if_lvalue.cond() = rename(if_lvalue.cond(), ns);
331  if(!if_lvalue.cond().is_false())
332  if_lvalue.true_case() = l2_rename_rvalues(if_lvalue.true_case(), ns);
333  if(!if_lvalue.cond().is_true())
334  if_lvalue.false_case() = l2_rename_rvalues(if_lvalue.false_case(), ns);
335  }
336  else if(lvalue.id() == ID_complex_real)
337  {
338  auto &complex_real_lvalue = to_complex_real_expr(lvalue);
339  complex_real_lvalue.op() = l2_rename_rvalues(complex_real_lvalue.op(), ns);
340  }
341  else if(lvalue.id() == ID_complex_imag)
342  {
343  auto &complex_imag_lvalue = to_complex_imag_expr(lvalue);
344  complex_imag_lvalue.op() = l2_rename_rvalues(complex_imag_lvalue.op(), ns);
345  }
346  else
347  {
349  "l2_rename_rvalues case `" + lvalue.id_string() + "' not handled");
350  }
351 
352  return lvalue;
353 }
354 
355 template renamedt<exprt, L1>
356 goto_symex_statet::rename<L1>(exprt expr, const namespacet &ns);
357 
360  ssa_exprt &expr,
361  const namespacet &ns)
362 {
363  // do we have threads?
364  if(threads.size()<=1)
365  return false;
366 
367  // is it a shared object?
368  PRECONDITION(dirty != nullptr);
369  const irep_idt &obj_identifier=expr.get_object_name();
370  if(
371  obj_identifier == guard_identifier() ||
372  (!ns.lookup(obj_identifier).is_shared() && !(*dirty)(obj_identifier)))
373  {
374  return false;
375  }
376 
377  // only continue if an indivisible object is being accessed
379  return false;
380 
381  const ssa_exprt ssa_l1 = remove_level_2(expr);
382  const irep_idt &l1_identifier=ssa_l1.get_identifier();
383  const exprt guard_as_expr = guard.as_expr();
384 
385  // see whether we are within an atomic section
386  if(atomic_section_id!=0)
387  {
388  guardt write_guard{false_exprt{}, guard_manager};
389 
390  const auto a_s_writes = written_in_atomic_section.find(ssa_l1);
391  if(a_s_writes!=written_in_atomic_section.end())
392  {
393  for(const auto &guard_in_list : a_s_writes->second)
394  {
395  guardt g = guard_in_list;
396  g-=guard;
397  if(g.is_true())
398  // There has already been a write to l1_identifier within this atomic
399  // section under the same guard, or a guard implied by the current
400  // one.
401  return false;
402 
403  write_guard |= guard_in_list;
404  }
405  }
406 
407  not_exprt no_write(write_guard.as_expr());
408 
409  // we cannot determine for sure that there has been a write already
410  // so generate a read even if l1_identifier has been written on
411  // all branches flowing into this read
412  guardt read_guard{false_exprt{}, guard_manager};
413 
414  a_s_r_entryt &a_s_read=read_in_atomic_section[ssa_l1];
415  for(const auto &a_s_read_guard : a_s_read.second)
416  {
417  guardt g = a_s_read_guard; // copy
418  g-=guard;
419  if(g.is_true())
420  // There has already been a read of l1_identifier within this atomic
421  // section under the same guard, or a guard implied by the current one.
422  return false;
423 
424  read_guard |= a_s_read_guard;
425  }
426 
427  guardt cond = read_guard;
428  if(!no_write.op().is_false())
429  cond |= guardt{no_write.op(), guard_manager};
430 
431  // It is safe to perform constant propagation in case we have read or
432  // written this object within the atomic section. We must actually do this,
433  // because goto_state::apply_condition may have placed the latest value in
434  // the propagation map without recording an assignment.
435  auto p_it = propagation.find(ssa_l1.get_identifier());
436  const exprt l2_true_case =
437  p_it.has_value() ? *p_it : set_indices<L2>(ssa_l1, ns).get();
438 
439  if(!cond.is_true())
440  level2.increase_generation(l1_identifier, ssa_l1, fresh_l2_name_provider);
441 
442  if(a_s_read.second.empty())
443  a_s_read.first = level2.latest_index(l1_identifier);
444 
445  const renamedt<ssa_exprt, L2> l2_false_case = set_indices<L2>(ssa_l1, ns);
446 
447  exprt tmp;
448  if(cond.is_false())
449  tmp = l2_false_case.get();
450  else if(cond.is_true())
451  tmp = l2_true_case;
452  else
453  tmp = if_exprt{cond.as_expr(), l2_true_case, l2_false_case.get()};
454 
455  record_events.push(false);
456  ssa_exprt ssa_l2 = assignment(std::move(ssa_l1), tmp, ns, true, true).get();
457  record_events.pop();
458 
460  guard_as_expr,
461  ssa_l2,
462  ssa_l2,
463  ssa_l2.get_original_expr(),
464  tmp,
465  source,
467 
468  INVARIANT(!check_renaming(ssa_l2), "expr should be renamed to L2");
469  expr = std::move(ssa_l2);
470 
471  a_s_read.second.push_back(guard);
472  if(!no_write.op().is_false())
473  a_s_read.second.back().add(no_write);
474 
475  return true;
476  }
477 
478  // No event and no fresh index, but avoid constant propagation
479  if(!record_events.top())
480  {
481  expr = set_indices<L2>(std::move(ssa_l1), ns).get();
482  return true;
483  }
484 
485  // produce a fresh L2 name
486  level2.increase_generation(l1_identifier, ssa_l1, fresh_l2_name_provider);
487  expr = set_indices<L2>(std::move(ssa_l1), ns).get();
488 
489  // and record that
491  symex_target!=nullptr, nullptr_exceptiont, "symex_target is null");
492  symex_target->shared_read(guard_as_expr, expr, atomic_section_id, source);
493 
494  return true;
495 }
496 
498  const ssa_exprt &expr,
499  const namespacet &ns) const
500 {
501  if(!record_events.top())
503 
504  PRECONDITION(dirty != nullptr);
505  const irep_idt &obj_identifier = expr.get_object_name();
506  if(
507  obj_identifier == guard_identifier() ||
508  (!ns.lookup(obj_identifier).is_shared() && !(*dirty)(obj_identifier)))
509  {
511  }
512 
513  // only continue if an indivisible object is being accessed
516 
517  if(atomic_section_id != 0)
519 
521 }
522 
526  const ssa_exprt &expr,
527  const namespacet &ns)
528 {
529  switch(write_is_shared(expr, ns))
530  {
532  return false;
534  {
536  return false;
537  }
539  break;
540  }
541 
542  // record a shared write
544  guard.as_expr(),
545  expr,
547  source);
548 
549  // do we have threads?
550  return threads.size() > 1;
551 }
552 
553 template <levelt level>
555 {
556  if(is_ssa_expr(expr))
557  {
558  ssa_exprt &ssa=to_ssa_expr(expr);
559 
560  // only do L1!
561  ssa = set_indices<L1>(std::move(ssa), ns).get();
562 
563  rename<level>(expr.type(), ssa.get_identifier(), ns);
564  ssa.update_type();
565  }
566  else if(expr.id()==ID_symbol)
567  {
568  expr=ssa_exprt(expr);
569  rename_address<level>(expr, ns);
570  }
571  else
572  {
573  if(expr.id()==ID_index)
574  {
575  index_exprt &index_expr=to_index_expr(expr);
576 
577  rename_address<level>(index_expr.array(), ns);
578  PRECONDITION(index_expr.array().type().id() == ID_array);
579  expr.type() = to_array_type(index_expr.array().type()).subtype();
580 
581  // the index is not an address
582  index_expr.index() =
583  rename<level>(std::move(index_expr.index()), ns).get();
584  }
585  else if(expr.id()==ID_if)
586  {
587  // the condition is not an address
588  if_exprt &if_expr=to_if_expr(expr);
589  if_expr.cond() = rename<level>(std::move(if_expr.cond()), ns).get();
590  rename_address<level>(if_expr.true_case(), ns);
591  rename_address<level>(if_expr.false_case(), ns);
592 
593  if_expr.type()=if_expr.true_case().type();
594  }
595  else if(expr.id()==ID_member)
596  {
597  member_exprt &member_expr=to_member_expr(expr);
598 
599  rename_address<level>(member_expr.struct_op(), ns);
600 
601  // type might not have been renamed in case of nesting of
602  // structs and pointers/arrays
603  if(
604  member_expr.struct_op().type().id() != ID_struct_tag &&
605  member_expr.struct_op().type().id() != ID_union_tag)
606  {
607  const struct_union_typet &su_type=
608  to_struct_union_type(member_expr.struct_op().type());
609  const struct_union_typet::componentt &comp=
610  su_type.get_component(member_expr.get_component_name());
611  PRECONDITION(comp.is_not_nil());
612  expr.type()=comp.type();
613  }
614  else
615  rename<level>(expr.type(), irep_idt(), ns);
616  }
617  else
618  {
619  // this could go wrong, but we would have to re-typecheck ...
620  rename<level>(expr.type(), irep_idt(), ns);
621 
622  // do this recursively; we assume here
623  // that all the operands are addresses
624  Forall_operands(it, expr)
625  rename_address<level>(*it, ns);
626  }
627  }
628 }
629 
633 static bool requires_renaming(const typet &type, const namespacet &ns)
634 {
635  if(type.id() == ID_array)
636  {
637  const auto &array_type = to_array_type(type);
638  return requires_renaming(array_type.subtype(), ns) ||
639  !array_type.size().is_constant();
640  }
641  else if(type.id() == ID_struct || type.id() == ID_union)
642  {
643  const struct_union_typet &s_u_type = to_struct_union_type(type);
644  const struct_union_typet::componentst &components = s_u_type.components();
645 
646  for(auto &component : components)
647  {
648  // be careful, or it might get cyclic
649  if(component.type().id() == ID_array)
650  {
651  if(!to_array_type(component.type()).size().is_constant())
652  return true;
653  }
654  else if(
655  component.type().id() != ID_pointer &&
656  requires_renaming(component.type(), ns))
657  {
658  return true;
659  }
660  }
661 
662  return false;
663  }
664  else if(type.id() == ID_pointer)
665  {
666  return requires_renaming(to_pointer_type(type).subtype(), ns);
667  }
668  else if(type.id() == ID_union_tag)
669  {
670  const symbolt &symbol = ns.lookup(to_union_tag_type(type));
671  return requires_renaming(symbol.type, ns);
672  }
673  else if(type.id() == ID_struct_tag)
674  {
675  const symbolt &symbol = ns.lookup(to_struct_tag_type(type));
676  return requires_renaming(symbol.type, ns);
677  }
678 
679  return false;
680 }
681 
682 template <levelt level>
684  typet &type,
685  const irep_idt &l1_identifier,
686  const namespacet &ns)
687 {
688  // check whether there are symbol expressions in the type; if not, there
689  // is no need to expand the struct/union tags in the type
690  if(!requires_renaming(type, ns))
691  return; // no action
692 
693  // rename all the symbols with their last known value
694  // to the given level
695 
696  std::pair<l1_typest::iterator, bool> l1_type_entry;
697  if(level==L2 &&
698  !l1_identifier.empty())
699  {
700  l1_type_entry=l1_types.insert(std::make_pair(l1_identifier, type));
701 
702  if(!l1_type_entry.second) // was already in map
703  {
704  // do not change a complete array type to an incomplete one
705 
706  const typet &type_prev=l1_type_entry.first->second;
707 
708  if(type.id()!=ID_array ||
709  type_prev.id()!=ID_array ||
710  to_array_type(type).is_incomplete() ||
711  to_array_type(type_prev).is_complete())
712  {
713  type=l1_type_entry.first->second;
714  return;
715  }
716  }
717  }
718 
719  // expand struct and union tag types
720  type = ns.follow(type);
721 
722  if(type.id()==ID_array)
723  {
724  auto &array_type = to_array_type(type);
725  rename<level>(array_type.subtype(), irep_idt(), ns);
726  array_type.size() = rename<level>(std::move(array_type.size()), ns).get();
727  }
728  else if(type.id() == ID_struct || type.id() == ID_union)
729  {
731  struct_union_typet::componentst &components=s_u_type.components();
732 
733  for(auto &component : components)
734  {
735  // be careful, or it might get cyclic
736  if(component.type().id() == ID_array)
737  {
738  auto &array_type = to_array_type(component.type());
739  array_type.size() =
740  rename<level>(std::move(array_type.size()), ns).get();
741  }
742  else if(component.type().id() != ID_pointer)
743  rename<level>(component.type(), irep_idt(), ns);
744  }
745  }
746  else if(type.id()==ID_pointer)
747  {
748  rename<level>(to_pointer_type(type).subtype(), irep_idt(), ns);
749  }
750 
751  if(level==L2 &&
752  !l1_identifier.empty())
753  l1_type_entry.first->second=type;
754 }
755 
756 static void get_l1_name(exprt &expr)
757 {
758  // do not reset the type !
759 
760  if(is_ssa_expr(expr))
761  to_ssa_expr(expr).remove_level_2();
762  else
763  Forall_operands(it, expr)
764  get_l1_name(*it);
765 }
766 
772 void goto_symex_statet::print_backtrace(std::ostream &out) const
773 {
774  if(threads[source.thread_nr].call_stack.empty())
775  {
776  out << "No stack!\n";
777  return;
778  }
779 
780  out << source.function_id << " " << source.pc->location_number << "\n";
781 
782  for(auto stackit = threads[source.thread_nr].call_stack.rbegin(),
783  stackend = threads[source.thread_nr].call_stack.rend();
784  stackit != stackend;
785  ++stackit)
786  {
787  const auto &frame = *stackit;
788  out << frame.calling_location.function_id << " "
789  << frame.calling_location.pc->location_number << "\n";
790  }
791 }
792 
794  const symbol_exprt &expr,
795  std::function<std::size_t(const irep_idt &)> index_generator,
796  const namespacet &ns)
797 {
798  framet &frame = call_stack().top();
799 
800  const renamedt<ssa_exprt, L0> renamed = rename_ssa<L0>(ssa_exprt{expr}, ns);
801  const irep_idt l0_name = renamed.get_identifier();
802  const auto l1_index = narrow_cast<unsigned>(index_generator(l0_name));
803 
804  if(const auto old_value = level1.insert_or_replace(renamed, l1_index))
805  {
806  // save old L1 name
807  if(!frame.old_level1.has(renamed))
808  frame.old_level1.insert(renamed, old_value->second);
809  }
810 
811  const ssa_exprt ssa = rename_ssa<L1>(renamed.get(), ns).get();
812  const bool inserted = frame.local_objects.insert(ssa.get_identifier()).second;
813  INVARIANT(inserted, "l1_name expected to be unique by construction");
814 
815  return ssa;
816 }
817 
819 {
820  const irep_idt &l1_identifier = ssa.get_identifier();
821 
822  // rename type to L2
823  rename(ssa.type(), l1_identifier, ns);
824  ssa.update_type();
825 
826  // in case of pointers, put something into the value set
827  if(ssa.type().id() == ID_pointer)
828  {
829  exprt rhs;
830  if(
831  auto failed =
834  else
835  rhs = exprt(ID_invalid);
836 
837  exprt l1_rhs = rename<L1>(std::move(rhs), ns).get();
838  value_set.assign(ssa, l1_rhs, ns, true, false);
839  }
840 
841  // L2 renaming
842  const exprt fields = field_sensitivity.get_fields(ns, *this, ssa);
843  for(const auto &l1_symbol : find_symbols(fields))
844  {
845  const ssa_exprt &field_ssa = to_ssa_expr(l1_symbol);
846  const std::size_t field_generation = level2.increase_generation(
847  l1_symbol.get_identifier(), field_ssa, fresh_l2_name_provider);
848  CHECK_RETURN(field_generation == 1);
849  }
850 
851  record_events.push(false);
852  exprt expr_l2 = rename(std::move(ssa), ns).get();
853  INVARIANT(
854  is_ssa_expr(expr_l2),
855  "symbol to declare should not be replaced by constant propagation");
856  ssa = to_ssa_expr(expr_l2);
857  record_events.pop();
858 
859  return ssa;
860 }
optionalt< symbol_exprt > get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
Pointer Dereferencing.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
Generic exception types primarily designed for use with invariants.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Operator to return the address of an object.
Definition: pointer_expr.h:200
const exprt & size() const
Definition: std_types.h:976
framet & new_frame(symex_targett::sourcet calling_location, const guardt &guard)
Definition: call_stack.h:30
framet & top()
Definition: call_stack.h:17
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
The Boolean constant false.
Definition: std_expr.h:2726
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
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 ...
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.
Container for data that varies per program point, e.g.
Definition: goto_state.h:32
symex_level2t level2
Definition: goto_state.h:38
guardt guard
Definition: goto_state.h:54
unsigned atomic_section_id
Threads.
Definition: goto_state.h:72
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:67
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:47
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...
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.
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
std::stack< bool > record_events
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)
thread encoding
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...
NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
static irep_idt guard_identifier()
call_stackt & call_stack()
const incremental_dirtyt * dirty
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)
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
symex_level1t level1
void rename_address(exprt &expr, const namespacet &ns)
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)
guard_managert & guard_manager
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
void print_backtrace(std::ostream &) const
Dumps the current state of symex, printing the function name and location number for each stack frame...
symex_target_equationt * symex_target
static bool is_read_only_object(const exprt &lvalue)
Returns true if lvalue is a read-only object, such as the null object.
field_sensitivityt field_sensitivity
write_is_shared_resultt write_is_shared(const ssa_exprt &expr, const namespacet &ns) const
symex_targett::sourcet source
bool run_validation_checks
Should the additional validation checks be run?
std::vector< threadt > threads
std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider
bool is_true() const
Definition: guard_expr.h:63
exprt as_expr() const
Definition: guard_expr.h:49
bool is_false() const
Definition: guard_expr.h:68
The trinary if-then-else operator.
Definition: std_expr.h:2087
exprt & true_case()
Definition: std_expr.h:2114
exprt & false_case()
Definition: std_expr.h:2124
exprt & cond()
Definition: std_expr.h:2104
Array index operator.
Definition: std_expr.h:1243
exprt & array()
Definition: std_expr.h:1259
exprt & index()
Definition: std_expr.h:1269
const std::string & id_string() const
Definition: irep.h:410
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
bool is_nil() const
Definition: irep.h:387
Extract member of struct or union.
Definition: std_expr.h:2528
const exprt & struct_op() const
Definition: std_expr.h:2558
irep_idt get_component_name() const
Definition: std_expr.h:2542
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
Boolean negation.
Definition: std_expr.h:2042
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:27
const underlyingt & get() const
Definition: renamed.h:34
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
void remove_level_2()
void update_type()
Definition: ssa_expr.h:28
const irep_idt get_level_2() const
Definition: ssa_expr.h:73
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
irep_idt get_object_name() const
Base type for structs and unions.
Definition: std_types.h:57
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:67
const componentst & components() const
Definition: std_types.h:142
std::vector< componentt > componentst
Definition: std_types.h:135
Expression to hold a symbol (variable)
Definition: std_expr.h:81
const irep_idt & get_identifier() const
Definition: std_expr.h:110
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Read from a shared variable ssa_object (which is both the left- and the right–hand side of assignment...
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...
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.
The Boolean constant true.
Definition: std_expr.h:2717
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
const exprt & op() const
Definition: std_expr.h:294
Thrown when we encounter an instruction, parameters to an instruction etc.
void output(std::ostream &out, const std::string &indent="") const
Pretty-print this value-set.
Definition: value_set.cpp:136
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
Variables whose address is taken.
#define Forall_operands(it, expr)
Definition: expr.h:25
Deprecated expression utility functions.
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,...
GOTO Symex constant propagation.
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.
static void get_l1_name(exprt &expr)
Symbolic Execution.
guard_exprt guardt
Definition: guard.h:27
dstringt irep_idt
Definition: irep.h:37
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
Various predicates over pointers in programs.
static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
Definition: race_check.cpp:122
@ L2
Definition: renamed.h:20
@ L0
Definition: renamed.h:17
@ L1_WITH_CONSTANT_PROPAGATION
Definition: renamed.h:19
@ L1
Definition: renamed.h:18
bool check_renaming(const typet &type)
Check that type is correctly renamed to level 2 and return true in case an error is detected.
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.
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.
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:408
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
ssa_exprt remove_level_2(ssa_exprt ssa)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1716
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2235
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1761
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:563
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:523
Stack frames – these are used for function calls and for exceptions.
Definition: frame.h:21
symex_level1t old_level1
Definition: frame.h:36
std::set< irep_idt > local_objects
Definition: frame.h:38
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
bool has(const renamedt< ssa_exprt, L0 > &ssa) const
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.
void insert(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Assume ssa is not already known.
unsigned latest_index(const irep_idt &identifier) const
Counter corresponding to an identifier.
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...
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38
goto_programt::const_targett pc
Definition: symex_target.h:43
static bool failed(bool error_indicator)