cprover
goto_rw.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening
6
7Date: April 2010
8
9\*******************************************************************/
10
11#include "goto_rw.h"
12
13#include <memory>
14
15#include <util/arith_tools.h>
16#include <util/bitvector_expr.h>
17#include <util/byte_operators.h>
18#include <util/endianness_map.h>
19#include <util/expr_util.h>
20#include <util/make_unique.h>
21#include <util/pointer_expr.h>
23#include <util/simplify_expr.h>
24#include <util/std_code.h>
25
27
29
31
33{
34}
35
36void range_domaint::output(const namespacet &, std::ostream &out) const
37{
38 out << "[";
39 for(const_iterator itr=begin();
40 itr!=end();
41 ++itr)
42 {
43 if(itr!=begin())
44 out << ";";
45 out << itr->first << ":" << itr->second;
46 }
47 out << "]";
48}
49
51{
52 for(rw_range_sett::objectst::iterator it=r_range_set.begin();
53 it!=r_range_set.end();
54 ++it)
55 it->second=nullptr;
56
57 for(rw_range_sett::objectst::iterator it=w_range_set.begin();
58 it!=w_range_set.end();
59 ++it)
60 it->second=nullptr;
61}
62
63void rw_range_sett::output(std::ostream &out) const
64{
65 out << "READ:\n";
66 for(const auto &read_object_entry : get_r_set())
67 {
68 out << " " << read_object_entry.first;
69 read_object_entry.second->output(ns, out);
70 out << '\n';
71 }
72
73 out << '\n';
74
75 out << "WRITE:\n";
76 for(const auto &written_object_entry : get_w_set())
77 {
78 out << " " << written_object_entry.first;
79 written_object_entry.second->output(ns, out);
80 out << '\n';
81 }
82}
83
85 get_modet mode,
86 const complex_real_exprt &expr,
87 const range_spect &range_start,
88 const range_spect &size)
89{
90 get_objects_rec(mode, expr.op(), range_start, size);
91}
92
94 get_modet mode,
95 const complex_imag_exprt &expr,
96 const range_spect &range_start,
97 const range_spect &size)
98{
99 const exprt &op = expr.op();
100
101 auto subtype_bits =
103 CHECK_RETURN(subtype_bits.has_value());
104
105 range_spect sub_size = to_range_spect(*subtype_bits);
106 CHECK_RETURN(sub_size > 0);
107
108 range_spect offset=
109 (range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size;
110
111 get_objects_rec(mode, op, range_start + offset, size);
112}
113
115 get_modet mode,
116 const if_exprt &if_expr,
117 const range_spect &range_start,
118 const range_spect &size)
119{
120 if(if_expr.cond().is_false())
121 get_objects_rec(mode, if_expr.false_case(), range_start, size);
122 else if(if_expr.cond().is_true())
123 get_objects_rec(mode, if_expr.true_case(), range_start, size);
124 else
125 {
127
128 get_objects_rec(mode, if_expr.false_case(), range_start, size);
129 get_objects_rec(mode, if_expr.true_case(), range_start, size);
130 }
131}
132
134 get_modet mode,
135 const dereference_exprt &deref,
136 const range_spect &,
137 const range_spect &)
138{
139 const exprt &pointer=deref.pointer();
141 if(mode!=get_modet::READ)
142 get_objects_rec(mode, pointer);
143}
144
146 get_modet mode,
147 const byte_extract_exprt &be,
148 const range_spect &range_start,
149 const range_spect &size)
150{
151 const exprt simp_offset=simplify_expr(be.offset(), ns);
152
153 auto index = numeric_cast<mp_integer>(simp_offset);
154 if(range_start == -1 || !index.has_value())
155 get_objects_rec(mode, be.op(), -1, size);
156 else
157 {
158 *index *= 8;
159 if(*index >= *pointer_offset_bits(be.op().type(), ns))
160 return;
161
163 be.op().type(),
164 be.id()==ID_byte_extract_little_endian,
165 ns);
166 range_spect offset =
167 range_start + map.map_bit(numeric_cast_v<std::size_t>(*index));
168 get_objects_rec(mode, be.op(), offset, size);
169 }
170}
171
173 get_modet mode,
174 const shift_exprt &shift,
175 const range_spect &range_start,
176 const range_spect &size)
177{
178 const exprt simp_distance=simplify_expr(shift.distance(), ns);
179
180 auto op_bits = pointer_offset_bits(shift.op().type(), ns);
181
182 range_spect src_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;
183
184 const auto dist = numeric_cast<mp_integer>(simp_distance);
185 if(range_start == -1 || size == -1 || src_size == -1 || !dist.has_value())
186 {
187 get_objects_rec(mode, shift.op(), -1, -1);
188 get_objects_rec(mode, shift.distance(), -1, -1);
189 }
190 else
191 {
192 const range_spect dist_r = to_range_spect(*dist);
193
194 // not sure whether to worry about
195 // config.ansi_c.endianness==configt::ansi_ct::IS_LITTLE_ENDIAN
196 // right here maybe?
197
198 if(shift.id()==ID_ashr || shift.id()==ID_lshr)
199 {
200 range_spect sh_range_start=range_start;
201 sh_range_start+=dist_r;
202
203 range_spect sh_size=std::min(size, src_size-sh_range_start);
204
205 if(sh_range_start>=0 && sh_range_start<src_size)
206 get_objects_rec(mode, shift.op(), sh_range_start, sh_size);
207 }
208 else
209 {
210 assert(src_size-dist_r>=0);
211 range_spect sh_size=std::min(size, src_size-dist_r);
212
213 get_objects_rec(mode, shift.op(), range_start, sh_size);
214 }
215 }
216}
217
219 get_modet mode,
220 const member_exprt &expr,
221 const range_spect &range_start,
222 const range_spect &size)
223{
224 const typet &type = expr.struct_op().type();
225
226 if(type.id() == ID_union || type.id() == ID_union_tag || range_start == -1)
227 {
228 get_objects_rec(mode, expr.struct_op(), range_start, size);
229 return;
230 }
231
232 const struct_typet &struct_type = to_struct_type(ns.follow(type));
233
234 auto offset_bits =
235 member_offset_bits(struct_type, expr.get_component_name(), ns);
236
237 range_spect offset;
238
239 if(offset_bits.has_value())
240 {
241 offset = to_range_spect(*offset_bits);
242 offset += range_start;
243 }
244 else
245 offset = -1;
246
247 get_objects_rec(mode, expr.struct_op(), offset, size);
248}
249
251 get_modet mode,
252 const index_exprt &expr,
253 const range_spect &range_start,
254 const range_spect &size)
255{
256 if(expr.array().id() == ID_null_object)
257 return;
258
259 range_spect sub_size=0;
260 const typet &type = expr.array().type();
261
262 if(type.id()==ID_vector)
263 {
264 const vector_typet &vector_type=to_vector_type(type);
265
266 auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
267
268 sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
269 }
270 else if(type.id()==ID_array)
271 {
272 const array_typet &array_type=to_array_type(type);
273
274 auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
275
276 sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
277 }
278 else
279 return;
280
281 const exprt simp_index=simplify_expr(expr.index(), ns);
282
283 const auto index = numeric_cast<mp_integer>(simp_index);
284 if(!index.has_value())
286
287 if(range_start == -1 || sub_size == -1 || !index.has_value())
288 get_objects_rec(mode, expr.array(), -1, size);
289 else
291 mode,
292 expr.array(),
293 range_start + to_range_spect(*index * sub_size),
294 size);
295}
296
298 get_modet mode,
299 const array_exprt &expr,
300 const range_spect &range_start,
301 const range_spect &size)
302{
303 const array_typet &array_type = expr.type();
304
305 auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
306
307 range_spect sub_size;
308
309 if(subtype_bits.has_value())
310 sub_size = to_range_spect(*subtype_bits);
311 else
312 {
313 forall_operands(it, expr)
314 get_objects_rec(mode, *it, 0, -1);
315
316 return;
317 }
318
319 range_spect offset=0;
320 range_spect full_r_s=range_start==-1 ? 0 : range_start;
321 range_spect full_r_e=
322 size==-1 ? sub_size*expr.operands().size() : full_r_s+size;
323
324 forall_operands(it, expr)
325 {
326 if(full_r_s<=offset+sub_size && full_r_e>offset)
327 {
328 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
329 range_spect cur_r_e=
330 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
331
332 get_objects_rec(mode, *it, cur_r_s, cur_r_e-cur_r_s);
333 }
334
335 offset+=sub_size;
336 }
337}
338
340 get_modet mode,
341 const struct_exprt &expr,
342 const range_spect &range_start,
343 const range_spect &size)
344{
345 const struct_typet &struct_type=
346 to_struct_type(ns.follow(expr.type()));
347
348 auto struct_bits = pointer_offset_bits(struct_type, ns);
349
350 range_spect full_size =
351 struct_bits.has_value() ? to_range_spect(*struct_bits) : -1;
352
353 range_spect offset=0;
354 range_spect full_r_s=range_start==-1 ? 0 : range_start;
355 range_spect full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size;
356
357 forall_operands(it, expr)
358 {
359 auto it_bits = pointer_offset_bits(it->type(), ns);
360
361 range_spect sub_size = it_bits.has_value() ? to_range_spect(*it_bits) : -1;
362
363 if(offset==-1)
364 {
365 get_objects_rec(mode, *it, 0, sub_size);
366 }
367 else if(sub_size==-1)
368 {
369 if(full_r_e==-1 || full_r_e>offset)
370 {
371 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
372
373 get_objects_rec(mode, *it, cur_r_s, -1);
374 }
375
376 offset=-1;
377 }
378 else if(full_r_e==-1)
379 {
380 if(full_r_s<=offset+sub_size)
381 {
382 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
383
384 get_objects_rec(mode, *it, cur_r_s, sub_size-cur_r_s);
385 }
386
387 offset+=sub_size;
388 }
389 else if(full_r_s<=offset+sub_size && full_r_e>offset)
390 {
391 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
392 range_spect cur_r_e=
393 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
394
395 get_objects_rec(mode, *it, cur_r_s, cur_r_e-cur_r_s);
396
397 offset+=sub_size;
398 }
399 }
400}
401
403 get_modet mode,
404 const typecast_exprt &tc,
405 const range_spect &range_start,
406 const range_spect &size)
407{
408 const exprt &op=tc.op();
409
410 auto op_bits = pointer_offset_bits(op.type(), ns);
411
412 range_spect new_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;
413
414 if(range_start==-1)
415 new_size=-1;
416 else if(new_size!=-1)
417 {
418 if(new_size<=range_start)
419 return;
420
421 new_size-=range_start;
422 new_size=std::min(size, new_size);
423 }
424
425 get_objects_rec(mode, op, range_start, new_size);
426}
427
429{
430 if(
431 object.id() == ID_string_constant || object.id() == ID_label ||
432 object.id() == ID_array || object.id() == ID_null_object ||
433 object.id() == ID_symbol)
434 {
435 // constant, nothing to do
436 return;
437 }
438 else if(object.id()==ID_dereference)
439 {
441 }
442 else if(object.id()==ID_index)
443 {
444 const index_exprt &index=to_index_expr(object);
445
448 }
449 else if(object.id()==ID_member)
450 {
451 const member_exprt &member=to_member_expr(object);
452
454 }
455 else if(object.id()==ID_if)
456 {
457 const if_exprt &if_expr=to_if_expr(object);
458
462 }
463 else if(object.id()==ID_byte_extract_little_endian ||
464 object.id()==ID_byte_extract_big_endian)
465 {
467
469 }
470 else if(object.id()==ID_typecast)
471 {
472 const typecast_exprt &tc=to_typecast_expr(object);
473
475 }
476 else
477 throw "rw_range_sett: address_of '" + object.id_string() + "' not handled";
478}
479
481 get_modet mode,
482 const irep_idt &identifier,
483 const range_spect &range_start,
484 const range_spect &range_end)
485{
486 objectst::iterator entry=
488 .insert(
489 std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
490 identifier, nullptr))
491 .first;
492
493 if(entry->second==nullptr)
494 entry->second=util_make_unique<range_domaint>();
495
496 static_cast<range_domaint&>(*entry->second).push_back(
497 {range_start, range_end});
498}
499
501 get_modet mode,
502 const exprt &expr,
503 const range_spect &range_start,
504 const range_spect &size)
505{
506 if(expr.id() == ID_complex_real)
508 mode, to_complex_real_expr(expr), range_start, size);
509 else if(expr.id() == ID_complex_imag)
511 mode, to_complex_imag_expr(expr), range_start, size);
512 else if(expr.id()==ID_typecast)
514 mode,
515 to_typecast_expr(expr),
516 range_start,
517 size);
518 else if(expr.id()==ID_if)
519 get_objects_if(mode, to_if_expr(expr), range_start, size);
520 else if(expr.id()==ID_dereference)
522 mode,
524 range_start,
525 size);
526 else if(expr.id()==ID_byte_extract_little_endian ||
527 expr.id()==ID_byte_extract_big_endian)
529 mode,
531 range_start,
532 size);
533 else if(expr.id()==ID_shl ||
534 expr.id()==ID_ashr ||
535 expr.id()==ID_lshr)
536 get_objects_shift(mode, to_shift_expr(expr), range_start, size);
537 else if(expr.id()==ID_member)
538 get_objects_member(mode, to_member_expr(expr), range_start, size);
539 else if(expr.id()==ID_index)
540 get_objects_index(mode, to_index_expr(expr), range_start, size);
541 else if(expr.id()==ID_array)
542 get_objects_array(mode, to_array_expr(expr), range_start, size);
543 else if(expr.id()==ID_struct)
544 get_objects_struct(mode, to_struct_expr(expr), range_start, size);
545 else if(expr.id()==ID_symbol)
546 {
547 const symbol_exprt &symbol=to_symbol_expr(expr);
548 const irep_idt identifier=symbol.get_identifier();
549
550 auto symbol_bits = pointer_offset_bits(symbol.type(), ns);
551
552 range_spect full_size =
553 symbol_bits.has_value() ? to_range_spect(*symbol_bits) : -1;
554
555 if(full_size==0 ||
556 (full_size>0 && range_start>=full_size))
557 {
558 // nothing to do, these are effectively constants (like function
559 // symbols or structs with no members)
560 // OR: invalid memory accesses
561 }
562 else if(range_start>=0)
563 {
564 range_spect range_end=size==-1 ? -1 : range_start+size;
565 if(size!=-1 && full_size!=-1)
566 range_end=std::min(range_end, full_size);
567
568 add(mode, identifier, range_start, range_end);
569 }
570 else
571 add(mode, identifier, 0, -1);
572 }
573 else if(mode==get_modet::READ && expr.id()==ID_address_of)
575 else if(mode==get_modet::READ)
576 {
577 // possibly affects the full object size, even if range_start/size
578 // are only a subset of the bytes (e.g., when using the result of
579 // arithmetic operations)
580 forall_operands(it, expr)
581 get_objects_rec(mode, *it);
582 }
583 else if(expr.id() == ID_null_object ||
584 expr.id() == ID_string_constant)
585 {
586 // dereferencing may yield some weird ones, ignore these
587 }
588 else if(mode==get_modet::LHS_W)
589 {
590 forall_operands(it, expr)
591 get_objects_rec(mode, *it);
592 }
593 else
594 throw "rw_range_sett: assignment to '" + expr.id_string() + "' not handled";
595}
596
598{
599 auto expr_bits = pointer_offset_bits(expr.type(), ns);
600
601 range_spect size = expr_bits.has_value() ? to_range_spect(*expr_bits) : -1;
602
603 get_objects_rec(mode, expr, 0, size);
604}
605
607{
608 // TODO should recurse into various composite types
609 if(type.id()==ID_array)
610 {
611 const auto &array_type = to_array_type(type);
612 get_objects_rec(array_type.element_type());
613 get_objects_rec(get_modet::READ, array_type.size());
614 }
615}
616
618 get_modet mode,
619 const dereference_exprt &deref,
620 const range_spect &range_start,
621 const range_spect &size)
622{
624 mode,
625 deref,
626 range_start,
627 size);
628
629 exprt object=deref;
631
632 auto type_bits = pointer_offset_bits(object.type(), ns);
633
634 range_spect new_size;
635
636 if(type_bits.has_value())
637 {
638 new_size = to_range_spect(*type_bits);
639
640 if(range_start == -1 || new_size <= range_start)
641 new_size = -1;
642 else
643 {
644 new_size -= range_start;
645 new_size = std::min(size, new_size);
646 }
647 }
648 else
649 new_size = -1;
650
651 // value_set_dereferencet::build_reference_to will turn *p into
652 // DYNAMIC_OBJECT(p) ? *p : invalid_objectN
653 if(object.is_not_nil() && !has_subexpr(object, ID_dereference))
654 get_objects_rec(mode, object, range_start, new_size);
655}
656
658 const namespacet &ns, std::ostream &out) const
659{
660 out << "[";
661 for(const_iterator itr=begin();
662 itr!=end();
663 ++itr)
664 {
665 if(itr!=begin())
666 out << ";";
667 out << itr->first << ":" << itr->second.first;
668 // we don't know what mode (language) we are in, so we rely on the default
669 // language to be reasonable for from_expr
670 out << " if " << from_expr(ns, irep_idt(), itr->second.second);
671 }
672 out << "]";
673}
674
676 get_modet mode,
677 const if_exprt &if_expr,
678 const range_spect &range_start,
679 const range_spect &size)
680{
681 if(if_expr.cond().is_false())
682 get_objects_rec(mode, if_expr.false_case(), range_start, size);
683 else if(if_expr.cond().is_true())
684 get_objects_rec(mode, if_expr.true_case(), range_start, size);
685 else
686 {
688
689 guardt copy = guard;
690
691 guard.add(not_exprt(if_expr.cond()));
692 get_objects_rec(mode, if_expr.false_case(), range_start, size);
693 guard = copy;
694
695 guard.add(if_expr.cond());
696 get_objects_rec(mode, if_expr.true_case(), range_start, size);
697 guard = std::move(copy);
698 }
699}
700
702 get_modet mode,
703 const irep_idt &identifier,
704 const range_spect &range_start,
705 const range_spect &range_end)
706{
707 objectst::iterator entry=
709 .insert(
710 std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
711 identifier, nullptr))
712 .first;
713
714 if(entry->second==nullptr)
715 entry->second=util_make_unique<guarded_range_domaint>();
716
717 static_cast<guarded_range_domaint&>(*entry->second).insert(
718 {range_start, {range_end, guard.as_expr()}});
719}
720
721static void goto_rw_assign(
722 const irep_idt &function,
724 const exprt &lhs,
725 const exprt &rhs,
726 rw_range_sett &rw_set)
727{
728 rw_set.get_objects_rec(
729 function, target, rw_range_sett::get_modet::LHS_W, lhs);
730 rw_set.get_objects_rec(function, target, rw_range_sett::get_modet::READ, rhs);
731}
732
733static void goto_rw(
734 const irep_idt &function,
736 const exprt &lhs,
737 const exprt &function_expr,
738 const exprt::operandst &arguments,
739 rw_range_sett &rw_set)
740{
741 if(lhs.is_not_nil())
742 rw_set.get_objects_rec(
743 function, target, rw_range_sett::get_modet::LHS_W, lhs);
744
745 rw_set.get_objects_rec(
746 function, target, rw_range_sett::get_modet::READ, function_expr);
747
748 for(const auto &argument : arguments)
749 {
750 rw_set.get_objects_rec(
751 function, target, rw_range_sett::get_modet::READ, argument);
752 }
753}
754
756 const irep_idt &function,
758 rw_range_sett &rw_set)
759{
760 switch(target->type())
761 {
763 case INCOMPLETE_GOTO:
765 break;
766
767 case GOTO:
768 case ASSUME:
769 case ASSERT:
770 rw_set.get_objects_rec(
771 function,
772 target,
774 target->get_condition());
775 break;
776
777 case SET_RETURN_VALUE:
778 rw_set.get_objects_rec(
779 function, target, rw_range_sett::get_modet::READ, target->return_value());
780 break;
781
782 case OTHER:
783 // if it's printf, mark the operands as read here
784 if(target->get_other().get_statement() == ID_printf)
785 {
786 for(const auto &op : target->get_other().operands())
787 rw_set.get_objects_rec(
788 function, target, rw_range_sett::get_modet::READ, op);
789 }
790 break;
791
792 case SKIP:
793 case START_THREAD:
794 case END_THREAD:
795 case LOCATION:
796 case END_FUNCTION:
797 case ATOMIC_BEGIN:
798 case ATOMIC_END:
799 case THROW:
800 case CATCH:
801 // these don't read or write anything
802 break;
803
804 case ASSIGN:
806 function, target, target->assign_lhs(), target->assign_rhs(), rw_set);
807 break;
808
809 case DEAD:
810 rw_set.get_objects_rec(
811 function, target, rw_range_sett::get_modet::LHS_W, target->dead_symbol());
812 break;
813
814 case DECL:
815 rw_set.get_objects_rec(function, target, target->decl_symbol().type());
816 rw_set.get_objects_rec(
817 function, target, rw_range_sett::get_modet::LHS_W, target->decl_symbol());
818 break;
819
820 case FUNCTION_CALL:
821 goto_rw(
822 function,
823 target,
824 target->call_lhs(),
825 target->call_function(),
826 target->call_arguments(),
827 rw_set);
828 break;
829 }
830}
831
833 const irep_idt &function,
834 const goto_programt &goto_program,
835 rw_range_sett &rw_set)
836{
837 forall_goto_program_instructions(i_it, goto_program)
838 goto_rw(function, i_it, rw_set);
839}
840
841void goto_rw(const goto_functionst &goto_functions,
842 const irep_idt &function,
843 rw_range_sett &rw_set)
844{
845 goto_functionst::function_mapt::const_iterator f_it=
846 goto_functions.function_map.find(function);
847
848 if(f_it!=goto_functions.function_map.end())
849 {
850 const goto_programt &body=f_it->second.body;
851
852 goto_rw(f_it->first, body, rw_set);
853 }
854}
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
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:361
Array constructor from list of elements.
Definition: std_expr.h:1476
const array_typet & type() const
Definition: std_expr.h:1483
Arrays with given size.
Definition: std_types.h:763
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
Expression of type type extracted from some object op starting at position offset (given in number of...
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1874
Real part of the expression describing a complex number.
Definition: std_expr.h:1829
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Maps a big-endian offset to a little-endian offset.
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:593
void add(const exprt &expr)
Definition: guard_expr.cpp:39
exprt as_expr() const
Definition: guard_expr.h:46
virtual void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:657
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:316
iterator end()
Definition: goto_rw.h:322
iterator begin()
Definition: goto_rw.h:318
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
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
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
Boolean negation.
Definition: std_expr.h:2181
virtual ~range_domain_baset()
Definition: goto_rw.cpp:32
void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:36
iterator end()
Definition: goto_rw.h:86
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:80
iterator begin()
Definition: goto_rw.h:82
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
Definition: goto_rw.h:358
void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size) override
Definition: goto_rw.cpp:675
void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) override
Definition: goto_rw.cpp:701
void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size) override
Definition: goto_rw.cpp:617
value_setst & value_sets
Definition: goto_rw.h:292
goto_programt::const_targett target
Definition: goto_rw.h:294
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
Definition: goto_rw.h:268
void output(std::ostream &out) const
Definition: goto_rw.cpp:63
objectst r_range_set
Definition: goto_rw.h:156
virtual void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:133
virtual void get_objects_complex_real(get_modet mode, const complex_real_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:84
virtual ~rw_range_sett()
Definition: goto_rw.cpp:50
const objectst & get_w_set() const
Definition: goto_rw.h:120
virtual void get_objects_shift(get_modet mode, const shift_exprt &shift, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:172
virtual void get_objects_index(get_modet mode, const index_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:250
virtual void get_objects_struct(get_modet mode, const struct_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:339
virtual void get_objects_complex_imag(get_modet mode, const complex_imag_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:93
virtual void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:114
virtual void get_objects_address_of(const exprt &object)
Definition: goto_rw.cpp:428
objectst w_range_set
Definition: goto_rw.h:156
const objectst & get_r_set() const
Definition: goto_rw.h:115
virtual void get_objects_byte_extract(get_modet mode, const byte_extract_exprt &be, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:145
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
Definition: goto_rw.h:134
virtual void get_objects_member(get_modet mode, const member_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:218
const namespacet & ns
Definition: goto_rw.h:154
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: goto_rw.cpp:480
virtual void get_objects_typecast(get_modet mode, const typecast_exprt &tc, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:402
virtual void get_objects_array(get_modet mode, const array_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:297
A base class for shift and rotate operators.
exprt & distance()
exprt & op()
Struct constructor from list of elements.
Definition: std_expr.h:1722
Structure type, corresponds to C style structs.
Definition: std_types.h:231
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const typet & subtype() const
Definition: type.h:156
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
The vector type.
Definition: std_types.h:996
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1006
#define forall_operands(it, expr)
Definition: expr.h:18
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:138
Deprecated expression utility functions.
Goto Programs with Functions.
#define forall_goto_program_instructions(it, program)
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ LOCATION
Definition: goto_program.h:41
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
@ ASSUME
Definition: goto_program.h:35
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
static void goto_rw_assign(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &rhs, rw_range_sett &rw_set)
Definition: goto_rw.cpp:721
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
Definition: goto_rw.cpp:733
int range_spect
Definition: goto_rw.h:57
range_spect to_range_spect(const mp_integer &size)
Definition: goto_rw.h:59
dstringt irep_idt
Definition: irep.h:37
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for Pointers.
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 dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1745
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1506
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 vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1082
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832