cprover
Loading...
Searching...
No Matches
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"
13
14#include <util/as_const.h>
15#include <util/base_exceptions.h> // IWYU pragma: keep
16#include <util/byte_operators.h>
17#include <util/c_types.h>
19#include <util/expr_util.h>
20#include <util/invariant.h>
21#include <util/std_expr.h>
22
23#include <analyses/dirty.h>
25
28
29static void get_l1_name(exprt &expr);
30
32 const symex_targett::sourcet &_source,
33 std::size_t max_field_sensitive_array_size,
34 bool should_simplify,
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, should_simplify),
42 record_events({true}),
43 fresh_l2_name_provider(fresh_l2_name_provider)
44{
45 threads.emplace_back(guard_manager);
46 call_stack().new_frame(source, guardt(true_exprt(), manager));
47}
48
50
51template <>
54{
55 return symex_level0(std::move(ssa_expr), ns, source.thread_nr);
56}
57
58template <>
61{
62 return level1(symex_level0(std::move(ssa_expr), ns, source.thread_nr));
63}
64
65template <>
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 if(rhs_is_simplified)
88 simplify(lhs, ns);
89 lhs.update_type();
91 {
92 DATA_INVARIANT(!check_renaming_l1(lhs), "lhs renaming failed on l1");
93 }
94
95 // do the l2 renaming
97 renamedt<ssa_exprt, L2> l2_lhs = set_indices<L2>(std::move(lhs), ns);
98 lhs = l2_lhs.get();
99
100 // in case we happen to be multi-threaded, record the memory access
102
104 {
105 DATA_INVARIANT(!check_renaming(lhs), "lhs renaming failed on l2");
106 DATA_INVARIANT(!check_renaming(rhs), "rhs renaming failed on l2");
107 }
108
109 // see #305 on GitHub for a simple example and possible discussion
110 if(is_shared && lhs.type().id() == ID_pointer && !allow_pointer_unsoundness)
112 "pointer handling for concurrency is unsound");
113
114 // Update constant propagation map -- the RHS is L2
115 if(!is_shared && record_value && goto_symex_can_forward_propagatet(ns)(rhs))
116 {
117 const auto propagation_entry = propagation.find(l1_identifier);
118 if(!propagation_entry.has_value())
119 propagation.insert(l1_identifier, rhs);
120 else if(propagation_entry->get() != rhs)
121 propagation.replace(l1_identifier, rhs);
122 }
123 else
124 propagation.erase_if_exists(l1_identifier);
125
126 {
127 // update value sets
128 exprt l1_rhs(rhs);
129 get_l1_name(l1_rhs);
130
131 const ssa_exprt l1_lhs = remove_level_2(lhs);
133 {
134 DATA_INVARIANT(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
135 DATA_INVARIANT(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
136 }
137
138 value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
139 }
140
141#ifdef DEBUG
142 std::cout << "Assigning " << l1_identifier << '\n';
143 value_set.output(std::cout);
144 std::cout << "**********************\n";
145#endif
146
147 return l2_lhs;
148}
149
150template <levelt level>
153{
154 static_assert(
155 level == L0 || level == L1,
156 "rename_ssa can only be used for levels L0 and L1");
157 ssa = set_indices<level>(std::move(ssa), ns).get();
158 rename<level>(ssa.type(), ssa.get_identifier(), ns);
159 ssa.update_type();
160 return renamedt<ssa_exprt, level>{ssa};
161}
162
168
169template <levelt level>
172{
173 // rename all the symbols with their last known value
174
175 static_assert(
176 level == L0 || level == L1 || level == L1_WITH_CONSTANT_PROPAGATION ||
177 level == L2,
178 "must handle all renaming levels");
179
180 if(is_ssa_expr(expr))
181 {
182 exprt original_expr = expr;
183 ssa_exprt &ssa=to_ssa_expr(expr);
184
185 if(level == L0)
186 {
188 std::move(rename_ssa<L0>(std::move(ssa), ns).value())};
189 }
190 else if(level == L1)
191 {
193 std::move(rename_ssa<L1>(std::move(ssa), ns).value())};
194 }
195 else
196 {
197 ssa = set_indices<L1>(std::move(ssa), ns).get();
198 rename<level>(expr.type(), ssa.get_identifier(), ns);
199 ssa.update_type();
200
201 // renaming taken care of by l2_thread_encoding, or already at L2
202 if(l2_thread_read_encoding(ssa, ns) || !ssa.get_level_2().empty())
203 {
205 {
206 // Don't actually rename to L2 -- we just used `ssa` to check whether
207 // constant-propagation was applicable
208 return renamedt<exprt, level>(std::move(original_expr));
209 }
210 else
211 return renamedt<exprt, level>(std::move(ssa));
212 }
213 else
214 {
215 // We also consider propagation if we go up to L2.
216 // L1 identifiers are used for propagation!
217 auto p_it = propagation.find(ssa.get_identifier());
218
219 if(p_it.has_value())
220 {
221 return renamedt<exprt, level>(*p_it); // already L2
222 }
223 else
224 {
225 if(level == L2)
226 ssa = set_indices<L2>(std::move(ssa), ns).get();
227 return renamedt<exprt, level>(std::move(ssa));
228 }
229 }
230 }
231 }
232 else if(expr.id()==ID_symbol)
233 {
234 const auto &type = as_const(expr).type();
235
236 // we never rename function symbols
237 if(type.id() == ID_code || type.id() == ID_mathematical_function)
238 {
239 rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
240 return renamedt<exprt, level>{std::move(expr)};
241 }
242 else
243 return rename<level>(ssa_exprt{expr}, ns);
244 }
245 else if(expr.id()==ID_address_of)
246 {
247 auto &address_of_expr = to_address_of_expr(expr);
248 rename_address<level>(address_of_expr.object(), ns);
249 to_pointer_type(expr.type()).base_type() =
250 as_const(address_of_expr).object().type();
251 return renamedt<exprt, level>{std::move(expr)};
252 }
253 else if(expr.is_nil())
254 {
255 return renamedt<exprt, level>{std::move(expr)};
256 }
257 else
258 {
259 rename<level>(expr.type(), irep_idt(), ns);
260
261 // do this recursively
262 Forall_operands(it, expr)
263 *it = rename<level>(std::move(*it), ns).get();
264
265 const exprt &c_expr = as_const(expr);
266
267 // It may happen that the `old` subexpression of a `with_exprt` expression
268 // is propagated with a value that has an array type with a size that is a
269 // symbol with an L2 index that is different. In this case the type of the
270 // `with_exprt` will not match with the type of the `old` subexpression
271 // anymore.
272 // To address this issue we re-canonicalize the `with_exprt` by propagating
273 // the type of the `old` subexpression to the type of the `with_exprt`.
274 const auto *c_with_expr = expr_try_dynamic_cast<with_exprt>(c_expr);
275 if(
276 c_with_expr && can_cast_type<array_typet>(c_with_expr->type()) &&
277 can_cast_type<array_typet>(c_with_expr->old().type()) &&
278 c_with_expr->type() != c_with_expr->old().type())
279 {
280 expr.type() = to_with_expr(expr).old().type();
281 }
283 expr.id() != ID_with ||
284 c_expr.type() == to_with_expr(c_expr).old().type(),
285 "Type of renamed expr should be the same as operands for with_exprt",
286 c_expr.type().pretty(),
287 to_with_expr(c_expr).old().type().pretty());
289 expr.id() != ID_if ||
290 c_expr.type() == to_if_expr(c_expr).true_case().type(),
291 "Type of renamed expr should be the same as operands for if_exprt",
292 c_expr.type().pretty(),
293 to_if_expr(c_expr).true_case().type().pretty());
295 expr.id() != ID_if ||
296 c_expr.type() == to_if_expr(c_expr).false_case().type(),
297 "Type of renamed expr should be the same as operands for if_exprt",
298 c_expr.type().pretty(),
299 to_if_expr(c_expr).false_case().type().pretty());
300
301 if(level == L2)
302 expr = field_sensitivity.apply(ns, *this, std::move(expr), false);
303
304 return renamedt<exprt, level>{std::move(expr)};
305 }
306}
307
308// Explicitly instantiate the one version of this function without an explicit
309// caller in this file:
312
314{
315 rename(lvalue.type(), irep_idt(), ns);
316
317 if(lvalue.id() == ID_symbol)
318 {
319 // Nothing to do
320 }
321 else if(is_read_only_object(lvalue))
322 {
323 // Ignore apparent writes to 'NULL-object' and similar read-only objects
324 }
325 else if(lvalue.id() == ID_typecast)
326 {
327 auto &typecast_lvalue = to_typecast_expr(lvalue);
328 typecast_lvalue.op() = l2_rename_rvalues(typecast_lvalue.op(), ns);
329 }
330 else if(lvalue.id() == ID_member)
331 {
332 auto &member_lvalue = to_member_expr(lvalue);
333 member_lvalue.compound() = l2_rename_rvalues(member_lvalue.compound(), ns);
334 }
335 else if(lvalue.id() == ID_index)
336 {
337 // The index is an rvalue:
338 auto &index_lvalue = to_index_expr(lvalue);
339 index_lvalue.array() = l2_rename_rvalues(index_lvalue.array(), ns);
340 index_lvalue.index() = rename(index_lvalue.index(), ns).get();
341 }
342 else if(
343 lvalue.id() == ID_byte_extract_little_endian ||
344 lvalue.id() == ID_byte_extract_big_endian)
345 {
346 // The offset is an rvalue:
347 auto &byte_extract_lvalue = to_byte_extract_expr(lvalue);
348 byte_extract_lvalue.op() = l2_rename_rvalues(byte_extract_lvalue.op(), ns);
349 byte_extract_lvalue.offset() = rename(byte_extract_lvalue.offset(), ns);
350 }
351 else if(lvalue.id() == ID_if)
352 {
353 // The condition is an rvalue:
354 auto &if_lvalue = to_if_expr(lvalue);
355 if_lvalue.cond() = rename(if_lvalue.cond(), ns);
356 if(!if_lvalue.cond().is_false())
357 if_lvalue.true_case() = l2_rename_rvalues(if_lvalue.true_case(), ns);
358 if(!if_lvalue.cond().is_true())
359 if_lvalue.false_case() = l2_rename_rvalues(if_lvalue.false_case(), ns);
360 }
361 else if(lvalue.id() == ID_complex_real)
362 {
363 auto &complex_real_lvalue = to_complex_real_expr(lvalue);
364 complex_real_lvalue.op() = l2_rename_rvalues(complex_real_lvalue.op(), ns);
365 }
366 else if(lvalue.id() == ID_complex_imag)
367 {
368 auto &complex_imag_lvalue = to_complex_imag_expr(lvalue);
369 complex_imag_lvalue.op() = l2_rename_rvalues(complex_imag_lvalue.op(), ns);
370 }
371 else
372 {
374 "l2_rename_rvalues case `" + lvalue.id_string() + "' not handled");
375 }
376
377 return lvalue;
378}
379
380template renamedt<exprt, L1>
382
385 ssa_exprt &expr,
386 const namespacet &ns)
387{
388 // do we have threads?
389 if(threads.size()<=1)
390 return false;
391
392 // is it a shared object?
393 PRECONDITION(dirty != nullptr);
394 const irep_idt &obj_identifier=expr.get_object_name();
395 if(
396 obj_identifier == guard_identifier() ||
397 (!ns.lookup(obj_identifier).is_shared() && !(*dirty)(obj_identifier)))
398 {
399 return false;
400 }
401
402 // only continue if an indivisible object is being accessed
403 if(field_sensitivity.is_divisible(expr, true))
404 return false;
405
406 const ssa_exprt ssa_l1 = remove_level_2(expr);
407 const irep_idt &l1_identifier=ssa_l1.get_identifier();
408 const exprt guard_as_expr = guard.as_expr();
409
410 // see whether we are within an atomic section
411 if(atomic_section_id!=0)
412 {
413 guardt write_guard{false_exprt{}, guard_manager};
414
415 const auto a_s_writes = written_in_atomic_section.find(ssa_l1);
416 if(a_s_writes!=written_in_atomic_section.end())
417 {
418 for(const auto &guard_in_list : a_s_writes->second)
419 {
420 guardt g = guard_in_list;
421 g-=guard;
422 if(g.is_true())
423 // There has already been a write to l1_identifier within this atomic
424 // section under the same guard, or a guard implied by the current
425 // one.
426 return false;
427
428 write_guard |= guard_in_list;
429 }
430 }
431
432 not_exprt no_write(write_guard.as_expr());
433
434 // we cannot determine for sure that there has been a write already
435 // so generate a read even if l1_identifier has been written on
436 // all branches flowing into this read
437 guardt read_guard{false_exprt{}, guard_manager};
438
439 a_s_r_entryt &a_s_read=read_in_atomic_section[ssa_l1];
440 for(const auto &a_s_read_guard : a_s_read.second)
441 {
442 guardt g = a_s_read_guard; // copy
443 g-=guard;
444 if(g.is_true())
445 // There has already been a read of l1_identifier within this atomic
446 // section under the same guard, or a guard implied by the current one.
447 return false;
448
449 read_guard |= a_s_read_guard;
450 }
451
452 guardt cond = read_guard;
453 if(!no_write.op().is_false())
454 cond |= guardt{no_write.op(), guard_manager};
455
456 // It is safe to perform constant propagation in case we have read or
457 // written this object within the atomic section. We must actually do this,
458 // because goto_state::apply_condition may have placed the latest value in
459 // the propagation map without recording an assignment.
460 auto p_it = propagation.find(ssa_l1.get_identifier());
461 const exprt l2_true_case =
462 p_it.has_value() ? *p_it : set_indices<L2>(ssa_l1, ns).get();
463
464 if(!cond.is_true())
465 level2.increase_generation(l1_identifier, ssa_l1, fresh_l2_name_provider);
466
467 if(a_s_read.second.empty())
468 a_s_read.first = level2.latest_index(l1_identifier);
469
470 const renamedt<ssa_exprt, L2> l2_false_case = set_indices<L2>(ssa_l1, ns);
471
472 exprt tmp;
473 if(cond.is_false())
474 tmp = l2_false_case.get();
475 else if(cond.is_true())
476 tmp = l2_true_case;
477 else
478 tmp = if_exprt{cond.as_expr(), l2_true_case, l2_false_case.get()};
479
480 record_events.push(false);
481 ssa_exprt ssa_l2 = assignment(std::move(ssa_l1), tmp, ns, true, true).get();
482 record_events.pop();
483
485 guard_as_expr,
486 ssa_l2,
487 ssa_l2,
488 ssa_l2.get_original_expr(),
489 tmp,
490 source,
492
493 INVARIANT(!check_renaming(ssa_l2), "expr should be renamed to L2");
494 expr = std::move(ssa_l2);
495
496 a_s_read.second.push_back(guard);
497 if(!no_write.op().is_false())
498 a_s_read.second.back().add(no_write);
499
500 return true;
501 }
502
503 // No event and no fresh index, but avoid constant propagation
504 if(!record_events.top())
505 {
506 expr = set_indices<L2>(std::move(ssa_l1), ns).get();
507 return true;
508 }
509
510 // produce a fresh L2 name
511 level2.increase_generation(l1_identifier, ssa_l1, fresh_l2_name_provider);
512 expr = set_indices<L2>(std::move(ssa_l1), ns).get();
513
514 // and record that
516 symex_target!=nullptr, nullptr_exceptiont, "symex_target is null");
517 symex_target->shared_read(guard_as_expr, expr, atomic_section_id, source);
518
519 return true;
520}
521
523 const ssa_exprt &expr,
524 const namespacet &ns) const
525{
526 if(!record_events.top())
528
529 PRECONDITION(dirty != nullptr);
530 const irep_idt &obj_identifier = expr.get_object_name();
531 if(
532 obj_identifier == guard_identifier() ||
533 (!ns.lookup(obj_identifier).is_shared() && !(*dirty)(obj_identifier)))
534 {
536 }
537
538 // only continue if an indivisible object is being accessed
539 if(field_sensitivity.is_divisible(expr, true))
541
542 if(atomic_section_id != 0)
544
546}
547
551 const ssa_exprt &expr,
552 const namespacet &ns)
553{
554 switch(write_is_shared(expr, ns))
555 {
557 return false;
559 {
561 return false;
562 }
564 break;
565 }
566
567 // record a shared write
569 guard.as_expr(),
570 expr,
572 source);
573
574 // do we have threads?
575 return threads.size() > 1;
576}
577
578template <levelt level>
580{
581 if(is_ssa_expr(expr))
582 {
583 ssa_exprt &ssa=to_ssa_expr(expr);
584
585 // only do L1!
586 ssa = set_indices<L1>(std::move(ssa), ns).get();
587
588 rename<level>(expr.type(), ssa.get_identifier(), ns);
589 ssa.update_type();
590 }
591 else if(expr.id()==ID_symbol)
592 {
593 expr=ssa_exprt(expr);
594 rename_address<level>(expr, ns);
595 }
596 else
597 {
598 if(expr.id()==ID_index)
599 {
600 index_exprt &index_expr=to_index_expr(expr);
601
602 rename_address<level>(index_expr.array(), ns);
603 PRECONDITION(index_expr.array().type().id() == ID_array);
604 expr.type() = to_array_type(index_expr.array().type()).element_type();
605
606 // the index is not an address
607 index_expr.index() =
608 rename<level>(std::move(index_expr.index()), ns).get();
609 }
610 else if(expr.id()==ID_if)
611 {
612 // the condition is not an address
613 if_exprt &if_expr=to_if_expr(expr);
614 if_expr.cond() = rename<level>(std::move(if_expr.cond()), ns).get();
615 rename_address<level>(if_expr.true_case(), ns);
616 rename_address<level>(if_expr.false_case(), ns);
617
618 if_expr.type()=if_expr.true_case().type();
619 }
620 else if(expr.id()==ID_member)
621 {
622 member_exprt &member_expr=to_member_expr(expr);
623
624 rename_address<level>(member_expr.struct_op(), ns);
625
626 // type might not have been renamed in case of nesting of
627 // structs and pointers/arrays
628 if(
629 member_expr.struct_op().type().id() != ID_struct_tag &&
630 member_expr.struct_op().type().id() != ID_union_tag)
631 {
632 const struct_union_typet &su_type=
633 to_struct_union_type(member_expr.struct_op().type());
635 su_type.get_component(member_expr.get_component_name());
636 PRECONDITION(comp.is_not_nil());
637 expr.type()=comp.type();
638 }
639 else
640 rename<level>(expr.type(), irep_idt(), ns);
641 }
642 else
643 {
644 // this could go wrong, but we would have to re-typecheck ...
645 rename<level>(expr.type(), irep_idt(), ns);
646
647 // do this recursively; we assume here
648 // that all the operands are addresses
649 Forall_operands(it, expr)
650 rename_address<level>(*it, ns);
651 }
652 }
653}
654
658static bool requires_renaming(const typet &type, const namespacet &ns)
659{
660 if(type.id() == ID_array)
661 {
662 const auto &array_type = to_array_type(type);
663 return requires_renaming(array_type.element_type(), ns) ||
664 !array_type.size().is_constant();
665 }
666 else if(type.id() == ID_struct || type.id() == ID_union)
667 {
668 const struct_union_typet &s_u_type = to_struct_union_type(type);
669 const struct_union_typet::componentst &components = s_u_type.components();
670
671 for(auto &component : components)
672 {
673 // be careful, or it might get cyclic
674 if(component.type().id() == ID_array)
675 {
676 if(!to_array_type(component.type()).size().is_constant())
677 return true;
678 }
679 else if(
680 component.type().id() != ID_pointer &&
681 requires_renaming(component.type(), ns))
682 {
683 return true;
684 }
685 }
686
687 return false;
688 }
689 else if(type.id() == ID_pointer)
690 {
691 return requires_renaming(to_pointer_type(type).base_type(), ns);
692 }
693 else if(type.id() == ID_union_tag)
694 {
695 const symbolt &symbol = ns.lookup(to_union_tag_type(type));
696 return requires_renaming(symbol.type, ns);
697 }
698 else if(type.id() == ID_struct_tag)
699 {
700 const symbolt &symbol = ns.lookup(to_struct_tag_type(type));
701 return requires_renaming(symbol.type, ns);
702 }
703
704 return false;
705}
706
707template <levelt level>
709 typet &type,
710 const irep_idt &l1_identifier,
711 const namespacet &ns)
712{
713 // check whether there are symbol expressions in the type; if not, there
714 // is no need to expand the struct/union tags in the type
715 if(!requires_renaming(type, ns))
716 return; // no action
717
718 // rename all the symbols with their last known value
719 // to the given level
720
721 std::pair<l1_typest::iterator, bool> l1_type_entry;
722 if(level==L2 &&
723 !l1_identifier.empty())
724 {
725 l1_type_entry=l1_types.insert(std::make_pair(l1_identifier, type));
726
727 if(!l1_type_entry.second) // was already in map
728 {
729 // do not change a complete array type to an incomplete one
730
731 const typet &type_prev=l1_type_entry.first->second;
732
733 if(type.id()!=ID_array ||
734 type_prev.id()!=ID_array ||
735 to_array_type(type).is_incomplete() ||
736 to_array_type(type_prev).is_complete())
737 {
738 type=l1_type_entry.first->second;
739 return;
740 }
741 }
742 }
743
744 if(type.id()==ID_array)
745 {
746 auto &array_type = to_array_type(type);
747 rename<level>(array_type.element_type(), irep_idt(), ns);
748 array_type.size() = rename<level>(std::move(array_type.size()), ns).get();
749 }
750 else if(
751 type.id() == ID_struct || type.id() == ID_union ||
752 type.id() == ID_struct_tag || type.id() == ID_union_tag)
753 {
754 // expand struct and union tag types
755 if(type.id() == ID_struct_tag)
756 type = ns.follow_tag(to_struct_tag_type(type));
757 else if(type.id() == ID_union_tag)
758 type = ns.follow_tag(to_union_tag_type(type));
759
761 struct_union_typet::componentst &components=s_u_type.components();
762
763 for(auto &component : components)
764 {
765 // be careful, or it might get cyclic
766 if(component.type().id() == ID_array)
767 {
768 auto &array_type = to_array_type(component.type());
769 array_type.size() =
770 rename<level>(std::move(array_type.size()), ns).get();
771 }
772 else if(component.type().id() != ID_pointer)
773 rename<level>(component.type(), irep_idt(), ns);
774 }
775 }
776 else if(type.id()==ID_pointer)
777 {
778 rename<level>(to_pointer_type(type).base_type(), irep_idt(), ns);
779 }
780
781 if(level==L2 &&
782 !l1_identifier.empty())
783 l1_type_entry.first->second=type;
784}
785
786static void get_l1_name(exprt &expr)
787{
788 // do not reset the type !
789
790 if(is_ssa_expr(expr))
792 else
793 Forall_operands(it, expr)
794 get_l1_name(*it);
795}
796
802void goto_symex_statet::print_backtrace(std::ostream &out) const
803{
804 if(threads[source.thread_nr].call_stack.empty())
805 {
806 out << "No stack!\n";
807 return;
808 }
809
810 out << source.function_id << " " << source.pc->location_number << "\n";
811
812 for(auto stackit = threads[source.thread_nr].call_stack.rbegin(),
813 stackend = threads[source.thread_nr].call_stack.rend();
814 stackit != stackend;
815 ++stackit)
816 {
817 const auto &frame = *stackit;
818 out << frame.calling_location.function_id << " "
819 << frame.calling_location.pc->location_number << "\n";
820 }
821}
822
824 const symbol_exprt &expr,
825 std::function<std::size_t(const irep_idt &)> index_generator,
826 const namespacet &ns)
827{
828 framet &frame = call_stack().top();
829
830 const renamedt<ssa_exprt, L0> renamed = rename_ssa<L0>(ssa_exprt{expr}, ns);
831 const irep_idt l0_name = renamed.get_identifier();
832 const std::size_t l1_index = index_generator(l0_name);
833
834 if(const auto old_value = level1.insert_or_replace(renamed, l1_index))
835 {
836 // save old L1 name
837 if(!frame.old_level1.has(renamed))
838 frame.old_level1.insert(renamed, old_value->second);
839 }
840
841 const ssa_exprt ssa = rename_ssa<L1>(renamed.get(), ns).get();
842 const bool inserted = frame.local_objects.insert(ssa.get_identifier()).second;
843 INVARIANT(inserted, "l1_name expected to be unique by construction");
844
845 return ssa;
846}
847
849{
850 const irep_idt &l1_identifier = ssa.get_identifier();
851
852 // rename type to L2
853 rename(ssa.type(), l1_identifier, ns);
854 ssa.update_type();
855
856 // in case of pointers, put something into the value set
857 if(ssa.type().id() == ID_pointer)
858 {
859 exprt rhs;
860 if(
861 auto failed =
864 else
865 rhs = exprt(ID_invalid);
866
867 exprt l1_rhs = rename<L1>(std::move(rhs), ns).get();
868 value_set.assign(ssa, l1_rhs, ns, true, false);
869 }
870
871 // L2 renaming
872 exprt fields = field_sensitivity.get_fields(ns, *this, ssa, false);
873 fields.visit_pre([this](const exprt &e) {
874 if(auto l1_symbol = expr_try_dynamic_cast<symbol_exprt>(e))
875 {
876 const ssa_exprt &field_ssa = to_ssa_expr(*l1_symbol);
877 const std::size_t field_generation = level2.increase_generation(
878 l1_symbol->get_identifier(), field_ssa, fresh_l2_name_provider);
879 CHECK_RETURN(field_generation == 1);
880 }
882 {
883 const ssa_exprt &ssa = fs_ssa->get_object_ssa();
884 const std::size_t field_generation = level2.increase_generation(
886 CHECK_RETURN(field_generation == 1);
887 }
888 });
889
890 record_events.push(false);
891 exprt expr_l2 = rename(std::move(ssa), ns).get();
892 INVARIANT(
893 is_ssa_expr(expr_l2),
894 "symbol to declare should not be replaced by constant propagation");
895 ssa = to_ssa_expr(expr_l2);
896 record_events.pop();
897
898 return ssa;
899}
std::optional< 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)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
Operator to return the address of an object.
const exprt & size() const
Definition std_types.h:840
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:827
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:38
bool empty() const
Definition dstring.h:89
Base class for all expressions.
Definition expr.h:56
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:227
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3064
exprt get_fields(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &ssa_expr, bool disjoined_fields_only) const
Compute an expression representing the individual components of a field-sensitive SSA representation ...
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
bool is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
Stack frames – these are used for function calls and for exceptions.
symex_level1t old_level1
Definition frame.h:42
std::set< irep_idt > local_objects
Definition frame.h:44
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::stack< bool > record_events
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)
thread encoding
exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
static irep_idt guard_identifier()
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
const incremental_dirtyt * dirty
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)
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...
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...
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
renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
renamedt< ssa_exprt, level > set_indices(ssa_exprt expr, const namespacet &ns)
Update values up to level.
goto_symex_statet(const symex_targett::sourcet &, std::size_t max_field_sensitive_array_size, bool should_simplify, guard_managert &manager, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
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: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:2370
exprt & cond()
Definition std_expr.h:2387
exprt & false_case()
Definition std_expr.h:2407
exprt & true_case()
Definition std_expr.h:2397
Array index operator.
Definition std_expr.h:1465
exprt & index()
Definition std_expr.h:1505
exprt & array()
Definition std_expr.h:1495
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
bool is_not_nil() const
Definition irep.h:372
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
Extract member of struct or union.
Definition std_expr.h:2841
const exprt & struct_op() const
Definition std_expr.h:2879
irep_idt get_component_name() const
Definition std_expr.h:2863
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Boolean negation.
Definition std_expr.h:2327
const typet & base_type() const
The type of the data what we point to.
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:199
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:145
Base type for structs and unions.
Definition std_types.h:62
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition std_types.cpp:63
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
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:3055
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:391
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.
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.
exprt & old()
Definition std_expr.h:2481
Variables whose address is taken.
#define Forall_operands(it, expr)
Definition expr.h:27
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
Deprecated expression utility functions.
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:29
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
@ 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.
bool simplify(exprt &expr, const namespacet &ns)
#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:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition invariant.h:437
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
ssa_exprt remove_level_2(ssa_exprt ssa)
Definition ssa_expr.cpp:219
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:80
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1533
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2102
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2450
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2933
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:2048
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:2005
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2533
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
Definition std_types.h:875
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition guard_expr.h:20
std::optional< 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.
bool has(const renamedt< ssa_exprt, L0 > &ssa) const
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.
goto_programt::const_targett pc
Generate Equation using Symbolic Execution.
static bool failed(bool error_indicator)
dstringt irep_idt