cprover
goto_symex_state.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "goto_symex_state.h"
14
15#include <iostream>
16
17#include <util/as_const.h>
19#include <util/byte_operators.h>
20#include <util/c_types.h>
22#include <util/expr_util.h>
23#include <util/find_symbols.h>
24#include <util/invariant.h>
25#include <util/std_expr.h>
26
27#include <analyses/dirty.h>
29
30static void get_l1_name(exprt &expr);
31
33 const symex_targett::sourcet &_source,
34 std::size_t max_field_sensitive_array_size,
35 guard_managert &manager,
36 std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
37 : goto_statet(manager),
38 source(_source),
39 guard_manager(manager),
40 symex_target(nullptr),
41 field_sensitivity(max_field_sensitive_array_size),
42 record_events({true}),
43 fresh_l2_name_provider(fresh_l2_name_provider)
44{
45 threads.emplace_back(guard_manager);
47}
48
50
51template <>
53goto_symex_statet::set_indices<L0>(ssa_exprt ssa_expr, const namespacet &ns)
54{
55 return symex_level0(std::move(ssa_expr), ns, source.thread_nr);
56}
57
58template <>
60goto_symex_statet::set_indices<L1>(ssa_exprt ssa_expr, const namespacet &ns)
61{
62 return level1(symex_level0(std::move(ssa_expr), ns, source.thread_nr));
63}
64
65template <>
67goto_symex_statet::set_indices<L2>(ssa_exprt ssa_expr, const namespacet &ns)
68{
69 return level2(
70 level1(symex_level0(std::move(ssa_expr), ns, source.thread_nr)));
71}
72
74 ssa_exprt lhs, // L0/L1
75 const exprt &rhs, // L2
76 const namespacet &ns,
77 bool rhs_is_simplified,
78 bool record_value,
79 bool allow_pointer_unsoundness)
80{
81 // identifier should be l0 or l1, make sure it's l1
82 lhs = rename_ssa<L1>(std::move(lhs), ns).get();
83 irep_idt l1_identifier=lhs.get_identifier();
84
85 // the type might need renaming
86 rename<L2>(lhs.type(), l1_identifier, ns);
87 lhs.update_type();
89 {
90 DATA_INVARIANT(!check_renaming_l1(lhs), "lhs renaming failed on l1");
91 }
92
93 // do the l2 renaming
95 renamedt<ssa_exprt, L2> l2_lhs = set_indices<L2>(std::move(lhs), ns);
96 lhs = l2_lhs.get();
97
98 // in case we happen to be multi-threaded, record the memory access
100
102 {
103 DATA_INVARIANT(!check_renaming(lhs), "lhs renaming failed on l2");
104 DATA_INVARIANT(!check_renaming(rhs), "rhs renaming failed on l2");
105 }
106
107 // see #305 on GitHub for a simple example and possible discussion
108 if(is_shared && lhs.type().id() == ID_pointer && !allow_pointer_unsoundness)
110 "pointer handling for concurrency is unsound");
111
112 // Update constant propagation map -- the RHS is L2
113 if(!is_shared && record_value && goto_symex_is_constantt()(rhs))
114 {
115 const auto propagation_entry = propagation.find(l1_identifier);
116 if(!propagation_entry.has_value())
117 propagation.insert(l1_identifier, rhs);
118 else if(propagation_entry->get() != rhs)
119 propagation.replace(l1_identifier, rhs);
120 }
121 else
122 propagation.erase_if_exists(l1_identifier);
123
124 {
125 // update value sets
126 exprt l1_rhs(rhs);
127 get_l1_name(l1_rhs);
128
129 const ssa_exprt l1_lhs = remove_level_2(lhs);
131 {
132 DATA_INVARIANT(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
133 DATA_INVARIANT(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
134 }
135
136 value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
137 }
138
139#ifdef DEBUG
140 std::cout << "Assigning " << l1_identifier << '\n';
141 value_set.output(std::cout);
142 std::cout << "**********************\n";
143#endif
144
145 return l2_lhs;
146}
147
148template <levelt level>
151{
152 static_assert(
153 level == L0 || level == L1,
154 "rename_ssa can only be used for levels L0 and L1");
155 ssa = set_indices<level>(std::move(ssa), ns).get();
156 rename<level>(ssa.type(), ssa.get_identifier(), ns);
157 ssa.update_type();
158 return renamedt<ssa_exprt, level>{ssa};
159}
160
163goto_symex_statet::rename_ssa<L0>(ssa_exprt ssa, const namespacet &ns);
165goto_symex_statet::rename_ssa<L1>(ssa_exprt ssa, const namespacet &ns);
166
167template <levelt level>
170{
171 // rename all the symbols with their last known value
172
173 static_assert(
174 level == L0 || level == L1 || level == L1_WITH_CONSTANT_PROPAGATION ||
175 level == L2,
176 "must handle all renaming levels");
177
178 if(is_ssa_expr(expr))
179 {
180 exprt original_expr = expr;
181 ssa_exprt &ssa=to_ssa_expr(expr);
182
183 if(level == L0)
184 {
186 std::move(rename_ssa<L0>(std::move(ssa), ns).value())};
187 }
188 else if(level == L1)
189 {
191 std::move(rename_ssa<L1>(std::move(ssa), ns).value())};
192 }
193 else
194 {
195 ssa = set_indices<L1>(std::move(ssa), ns).get();
196 rename<level>(expr.type(), ssa.get_identifier(), ns);
197 ssa.update_type();
198
199 // renaming taken care of by l2_thread_encoding, or already at L2
200 if(l2_thread_read_encoding(ssa, ns) || !ssa.get_level_2().empty())
201 {
203 {
204 // Don't actually rename to L2 -- we just used `ssa` to check whether
205 // constant-propagation was applicable
206 return renamedt<exprt, level>(std::move(original_expr));
207 }
208 else
209 return renamedt<exprt, level>(std::move(ssa));
210 }
211 else
212 {
213 // We also consider propagation if we go up to L2.
214 // L1 identifiers are used for propagation!
215 auto p_it = propagation.find(ssa.get_identifier());
216
217 if(p_it.has_value())
218 {
219 return renamedt<exprt, level>(*p_it); // already L2
220 }
221 else
222 {
223 if(level == L2)
224 ssa = set_indices<L2>(std::move(ssa), ns).get();
225 return renamedt<exprt, level>(std::move(ssa));
226 }
227 }
228 }
229 }
230 else if(expr.id()==ID_symbol)
231 {
232 const auto &type = as_const(expr).type();
233
234 // we never rename function symbols
235 if(type.id() == ID_code || type.id() == ID_mathematical_function)
236 {
237 rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
238 return renamedt<exprt, level>{std::move(expr)};
239 }
240 else
241 return rename<level>(ssa_exprt{expr}, ns);
242 }
243 else if(expr.id()==ID_address_of)
244 {
245 auto &address_of_expr = to_address_of_expr(expr);
246 rename_address<level>(address_of_expr.object(), ns);
247 to_pointer_type(expr.type()).base_type() =
248 as_const(address_of_expr).object().type();
249 return renamedt<exprt, level>{std::move(expr)};
250 }
251 else if(expr.is_nil())
252 {
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
352template renamedt<exprt, L1>
353goto_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 this atomic
396 // section under the same guard, or a guard implied by the current
397 // 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 of l1_identifier within this atomic
418 // section under the same guard, or a guard implied by the current one.
419 return false;
420
421 read_guard |= a_s_read_guard;
422 }
423
424 guardt cond = read_guard;
425 if(!no_write.op().is_false())
426 cond |= guardt{no_write.op(), guard_manager};
427
428 // It is safe to perform constant propagation in case we have read or
429 // written this object within the atomic section. We must actually do this,
430 // because goto_state::apply_condition may have placed the latest value in
431 // the propagation map without recording an assignment.
432 auto p_it = propagation.find(ssa_l1.get_identifier());
433 const exprt l2_true_case =
434 p_it.has_value() ? *p_it : set_indices<L2>(ssa_l1, ns).get();
435
436 if(!cond.is_true())
437 level2.increase_generation(l1_identifier, ssa_l1, fresh_l2_name_provider);
438
439 if(a_s_read.second.empty())
440 a_s_read.first = level2.latest_index(l1_identifier);
441
442 const renamedt<ssa_exprt, L2> l2_false_case = set_indices<L2>(ssa_l1, ns);
443
444 exprt tmp;
445 if(cond.is_false())
446 tmp = l2_false_case.get();
447 else if(cond.is_true())
448 tmp = l2_true_case;
449 else
450 tmp = if_exprt{cond.as_expr(), l2_true_case, l2_false_case.get()};
451
452 record_events.push(false);
453 ssa_exprt ssa_l2 = assignment(std::move(ssa_l1), tmp, ns, true, true).get();
454 record_events.pop();
455
457 guard_as_expr,
458 ssa_l2,
459 ssa_l2,
460 ssa_l2.get_original_expr(),
461 tmp,
462 source,
464
465 INVARIANT(!check_renaming(ssa_l2), "expr should be renamed to L2");
466 expr = std::move(ssa_l2);
467
468 a_s_read.second.push_back(guard);
469 if(!no_write.op().is_false())
470 a_s_read.second.back().add(no_write);
471
472 return true;
473 }
474
475 // No event and no fresh index, but avoid constant propagation
476 if(!record_events.top())
477 {
478 expr = set_indices<L2>(std::move(ssa_l1), ns).get();
479 return true;
480 }
481
482 // produce a fresh L2 name
483 level2.increase_generation(l1_identifier, ssa_l1, fresh_l2_name_provider);
484 expr = set_indices<L2>(std::move(ssa_l1), ns).get();
485
486 // and record that
488 symex_target!=nullptr, nullptr_exceptiont, "symex_target is null");
489 symex_target->shared_read(guard_as_expr, expr, atomic_section_id, source);
490
491 return true;
492}
493
495 const ssa_exprt &expr,
496 const namespacet &ns) const
497{
498 if(!record_events.top())
500
501 PRECONDITION(dirty != nullptr);
502 const irep_idt &obj_identifier = expr.get_object_name();
503 if(
504 obj_identifier == guard_identifier() ||
505 (!ns.lookup(obj_identifier).is_shared() && !(*dirty)(obj_identifier)))
506 {
508 }
509
510 // only continue if an indivisible object is being accessed
513
514 if(atomic_section_id != 0)
516
518}
519
523 const ssa_exprt &expr,
524 const namespacet &ns)
525{
526 switch(write_is_shared(expr, ns))
527 {
529 return false;
531 {
533 return false;
534 }
536 break;
537 }
538
539 // record a shared write
541 guard.as_expr(),
542 expr,
544 source);
545
546 // do we have threads?
547 return threads.size() > 1;
548}
549
550template <levelt level>
552{
553 if(is_ssa_expr(expr))
554 {
555 ssa_exprt &ssa=to_ssa_expr(expr);
556
557 // only do L1!
558 ssa = set_indices<L1>(std::move(ssa), ns).get();
559
560 rename<level>(expr.type(), ssa.get_identifier(), ns);
561 ssa.update_type();
562 }
563 else if(expr.id()==ID_symbol)
564 {
565 expr=ssa_exprt(expr);
566 rename_address<level>(expr, ns);
567 }
568 else
569 {
570 if(expr.id()==ID_index)
571 {
572 index_exprt &index_expr=to_index_expr(expr);
573
574 rename_address<level>(index_expr.array(), ns);
575 PRECONDITION(index_expr.array().type().id() == ID_array);
576 expr.type() = to_array_type(index_expr.array().type()).element_type();
577
578 // the index is not an address
579 index_expr.index() =
580 rename<level>(std::move(index_expr.index()), ns).get();
581 }
582 else if(expr.id()==ID_if)
583 {
584 // the condition is not an address
585 if_exprt &if_expr=to_if_expr(expr);
586 if_expr.cond() = rename<level>(std::move(if_expr.cond()), ns).get();
587 rename_address<level>(if_expr.true_case(), ns);
588 rename_address<level>(if_expr.false_case(), ns);
589
590 if_expr.type()=if_expr.true_case().type();
591 }
592 else if(expr.id()==ID_member)
593 {
594 member_exprt &member_expr=to_member_expr(expr);
595
596 rename_address<level>(member_expr.struct_op(), ns);
597
598 // type might not have been renamed in case of nesting of
599 // structs and pointers/arrays
600 if(
601 member_expr.struct_op().type().id() != ID_struct_tag &&
602 member_expr.struct_op().type().id() != ID_union_tag)
603 {
604 const struct_union_typet &su_type=
605 to_struct_union_type(member_expr.struct_op().type());
607 su_type.get_component(member_expr.get_component_name());
608 PRECONDITION(comp.is_not_nil());
609 expr.type()=comp.type();
610 }
611 else
612 rename<level>(expr.type(), irep_idt(), ns);
613 }
614 else
615 {
616 // this could go wrong, but we would have to re-typecheck ...
617 rename<level>(expr.type(), irep_idt(), ns);
618
619 // do this recursively; we assume here
620 // that all the operands are addresses
621 Forall_operands(it, expr)
622 rename_address<level>(*it, ns);
623 }
624 }
625}
626
630static bool requires_renaming(const typet &type, const namespacet &ns)
631{
632 if(type.id() == ID_array)
633 {
634 const auto &array_type = to_array_type(type);
635 return requires_renaming(array_type.element_type(), ns) ||
636 !array_type.size().is_constant();
637 }
638 else if(type.id() == ID_struct || type.id() == ID_union)
639 {
640 const struct_union_typet &s_u_type = to_struct_union_type(type);
641 const struct_union_typet::componentst &components = s_u_type.components();
642
643 for(auto &component : components)
644 {
645 // be careful, or it might get cyclic
646 if(component.type().id() == ID_array)
647 {
648 if(!to_array_type(component.type()).size().is_constant())
649 return true;
650 }
651 else if(
652 component.type().id() != ID_pointer &&
653 requires_renaming(component.type(), ns))
654 {
655 return true;
656 }
657 }
658
659 return false;
660 }
661 else if(type.id() == ID_pointer)
662 {
663 return requires_renaming(to_pointer_type(type).base_type(), ns);
664 }
665 else if(type.id() == ID_union_tag)
666 {
667 const symbolt &symbol = ns.lookup(to_union_tag_type(type));
668 return requires_renaming(symbol.type, ns);
669 }
670 else if(type.id() == ID_struct_tag)
671 {
672 const symbolt &symbol = ns.lookup(to_struct_tag_type(type));
673 return requires_renaming(symbol.type, ns);
674 }
675
676 return false;
677}
678
679template <levelt level>
681 typet &type,
682 const irep_idt &l1_identifier,
683 const namespacet &ns)
684{
685 // check whether there are symbol expressions in the type; if not, there
686 // is no need to expand the struct/union tags in the type
687 if(!requires_renaming(type, ns))
688 return; // no action
689
690 // rename all the symbols with their last known value
691 // to the given level
692
693 std::pair<l1_typest::iterator, bool> l1_type_entry;
694 if(level==L2 &&
695 !l1_identifier.empty())
696 {
697 l1_type_entry=l1_types.insert(std::make_pair(l1_identifier, type));
698
699 if(!l1_type_entry.second) // was already in map
700 {
701 // do not change a complete array type to an incomplete one
702
703 const typet &type_prev=l1_type_entry.first->second;
704
705 if(type.id()!=ID_array ||
706 type_prev.id()!=ID_array ||
707 to_array_type(type).is_incomplete() ||
708 to_array_type(type_prev).is_complete())
709 {
710 type=l1_type_entry.first->second;
711 return;
712 }
713 }
714 }
715
716 // expand struct and union tag types
717 type = ns.follow(type);
718
719 if(type.id()==ID_array)
720 {
721 auto &array_type = to_array_type(type);
722 rename<level>(array_type.element_type(), irep_idt(), ns);
723 array_type.size() = rename<level>(std::move(array_type.size()), ns).get();
724 }
725 else if(type.id() == ID_struct || type.id() == ID_union)
726 {
728 struct_union_typet::componentst &components=s_u_type.components();
729
730 for(auto &component : components)
731 {
732 // be careful, or it might get cyclic
733 if(component.type().id() == ID_array)
734 {
735 auto &array_type = to_array_type(component.type());
736 array_type.size() =
737 rename<level>(std::move(array_type.size()), ns).get();
738 }
739 else if(component.type().id() != ID_pointer)
740 rename<level>(component.type(), irep_idt(), ns);
741 }
742 }
743 else if(type.id()==ID_pointer)
744 {
745 rename<level>(to_pointer_type(type).base_type(), irep_idt(), ns);
746 }
747
748 if(level==L2 &&
749 !l1_identifier.empty())
750 l1_type_entry.first->second=type;
751}
752
753static void get_l1_name(exprt &expr)
754{
755 // do not reset the type !
756
757 if(is_ssa_expr(expr))
759 else
760 Forall_operands(it, expr)
761 get_l1_name(*it);
762}
763
769void goto_symex_statet::print_backtrace(std::ostream &out) const
770{
771 if(threads[source.thread_nr].call_stack.empty())
772 {
773 out << "No stack!\n";
774 return;
775 }
776
777 out << source.function_id << " " << source.pc->location_number << "\n";
778
779 for(auto stackit = threads[source.thread_nr].call_stack.rbegin(),
780 stackend = threads[source.thread_nr].call_stack.rend();
781 stackit != stackend;
782 ++stackit)
783 {
784 const auto &frame = *stackit;
785 out << frame.calling_location.function_id << " "
786 << frame.calling_location.pc->location_number << "\n";
787 }
788}
789
791 const symbol_exprt &expr,
792 std::function<std::size_t(const irep_idt &)> index_generator,
793 const namespacet &ns)
794{
795 framet &frame = call_stack().top();
796
797 const renamedt<ssa_exprt, L0> renamed = rename_ssa<L0>(ssa_exprt{expr}, ns);
798 const irep_idt l0_name = renamed.get_identifier();
799 const std::size_t l1_index = index_generator(l0_name);
800
801 if(const auto old_value = level1.insert_or_replace(renamed, l1_index))
802 {
803 // save old L1 name
804 if(!frame.old_level1.has(renamed))
805 frame.old_level1.insert(renamed, old_value->second);
806 }
807
808 const ssa_exprt ssa = rename_ssa<L1>(renamed.get(), ns).get();
809 const bool inserted = frame.local_objects.insert(ssa.get_identifier()).second;
810 INVARIANT(inserted, "l1_name expected to be unique by construction");
811
812 return ssa;
813}
814
816{
817 const irep_idt &l1_identifier = ssa.get_identifier();
818
819 // rename type to L2
820 rename(ssa.type(), l1_identifier, ns);
821 ssa.update_type();
822
823 // in case of pointers, put something into the value set
824 if(ssa.type().id() == ID_pointer)
825 {
826 exprt rhs;
827 if(
828 auto failed =
831 else
832 rhs = exprt(ID_invalid);
833
834 exprt l1_rhs = rename<L1>(std::move(rhs), ns).get();
835 value_set.assign(ssa, l1_rhs, ns, true, false);
836 }
837
838 // L2 renaming
839 const exprt fields = field_sensitivity.get_fields(ns, *this, ssa);
840 for(const auto &l1_symbol : find_symbols(fields))
841 {
842 const ssa_exprt &field_ssa = to_ssa_expr(l1_symbol);
843 const std::size_t field_generation = level2.increase_generation(
844 l1_symbol.get_identifier(), field_ssa, fresh_l2_name_provider);
845 CHECK_RETURN(field_generation == 1);
846 }
847
848 record_events.push(false);
849 exprt expr_l2 = rename(std::move(ssa), ns).get();
850 INVARIANT(
851 is_ssa_expr(expr_l2),
852 "symbol to declare should not be replaced by constant propagation");
853 ssa = to_ssa_expr(expr_l2);
854 record_events.pop();
855
856 return ssa;
857}
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.
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
Operator to return the address of an object.
Definition: pointer_expr.h:361
const exprt & size() const
Definition: std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
framet & top()
Definition: call_stack.h:17
framet & new_frame(symex_targett::sourcet calling_location, const guardt &guard)
Definition: call_stack.h:30
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:42
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2865
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:58
unsigned atomic_section_id
Threads.
Definition: goto_state.h:76
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:71
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:51
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.
call_stackt & call_stack()
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
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...
std::stack< bool > record_events
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)
thread encoding
NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
static irep_idt guard_identifier()
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
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
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
bool is_true() const
Definition: guard_expr.h:60
exprt as_expr() const
Definition: guard_expr.h:46
bool is_false() const
Definition: guard_expr.h:65
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & cond()
Definition: std_expr.h:2243
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
bool is_not_nil() const
Definition: irep.h:380
const std::string & id_string() const
Definition: irep.h:399
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & struct_op() const
Definition: std_expr.h:2697
irep_idt get_component_name() const
Definition: std_expr.h:2681
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Boolean negation.
Definition: std_expr.h:2181
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:33
const underlyingt & get() const
Definition: renamed.h:40
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
void remove_level_2()
Definition: ssa_expr.cpp:198
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
Definition: ssa_expr.cpp:144
Base type for structs and unions.
Definition: std_types.h:62
const componentst & components() const
Definition: std_types.h:147
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:57
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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:2856
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
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:138
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:1233
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:398
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
Definition: race_check.cpp:122
@ L2
Definition: renamed.h:26
@ L0
Definition: renamed.h:23
@ L1_WITH_CONSTANT_PROPAGATION
Definition: renamed.h:25
@ L1
Definition: renamed.h:24
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.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:407
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
ssa_exprt remove_level_2(ssa_exprt ssa)
Definition: ssa_expr.cpp:218
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1900
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1855
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2374
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
Stack frames – these are used for function calls and for exceptions.
Definition: frame.h:22
symex_level1t old_level1
Definition: frame.h:38
std::set< irep_idt > local_objects
Definition: frame.h:40
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
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:37
goto_programt::const_targett pc
Definition: symex_target.h:42
static bool failed(bool error_indicator)