cprover
Loading...
Searching...
No Matches
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 <util/arith_tools.h>
14#include <util/bitvector_expr.h>
15#include <util/byte_operators.h>
16#include <util/endianness_map.h>
17#include <util/expr_util.h>
18#include <util/make_unique.h>
19#include <util/namespace.h>
20#include <util/pointer_expr.h>
22#include <util/simplify_expr.h>
23
25
28
29#include <memory>
30
34
35void range_domaint::output(const namespacet &, std::ostream &out) const
36{
37 out << "[";
38 for(const_iterator itr=begin();
39 itr!=end();
40 ++itr)
41 {
42 if(itr!=begin())
43 out << ";";
44 out << itr->first << ":" << itr->second;
45 }
46 out << "]";
47}
48
50{
51 for(rw_range_sett::objectst::iterator it=r_range_set.begin();
52 it!=r_range_set.end();
53 ++it)
54 it->second=nullptr;
55
56 for(rw_range_sett::objectst::iterator it=w_range_set.begin();
57 it!=w_range_set.end();
58 ++it)
59 it->second=nullptr;
60}
61
62void rw_range_sett::output(std::ostream &out) const
63{
64 out << "READ:\n";
65 for(const auto &read_object_entry : get_r_set())
66 {
67 out << " " << read_object_entry.first;
68 read_object_entry.second->output(ns, out);
69 out << '\n';
70 }
71
72 out << '\n';
73
74 out << "WRITE:\n";
75 for(const auto &written_object_entry : get_w_set())
76 {
77 out << " " << written_object_entry.first;
78 written_object_entry.second->output(ns, out);
79 out << '\n';
80 }
81}
82
84 get_modet mode,
85 const complex_real_exprt &expr,
86 const range_spect &range_start,
87 const range_spect &size)
88{
89 get_objects_rec(mode, expr.op(), range_start, size);
90}
91
93 get_modet mode,
94 const complex_imag_exprt &expr,
95 const range_spect &range_start,
96 const range_spect &size)
97{
98 const exprt &op = expr.op();
99
100 auto subtype_bits =
102 CHECK_RETURN(subtype_bits.has_value());
103
104 range_spect sub_size = range_spect::to_range_spect(*subtype_bits);
105 CHECK_RETURN(sub_size > range_spect{0});
106
107 range_spect offset =
108 (range_start.is_unknown() || expr.id() == ID_complex_real) ? range_spect{0}
109 : 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 auto object_size_bits_opt = pointer_offset_bits(be.op().type(), ns);
152 const exprt simp_offset=simplify_expr(be.offset(), ns);
153
154 auto index = numeric_cast<mp_integer>(simp_offset);
155 if(
156 range_start.is_unknown() || !index.has_value() ||
157 !object_size_bits_opt.has_value())
158 {
159 get_objects_rec(mode, be.op(), range_spect::unknown(), size);
160 }
161 else
162 {
163 *index *= be.get_bits_per_byte();
164 if(*index >= *object_size_bits_opt)
165 return;
166
167 endianness_mapt map(
168 be.op().type(),
169 be.id()==ID_byte_extract_little_endian,
170 ns);
171 range_spect offset = range_start;
172 if(*index > 0)
173 {
176 }
177 else
178 {
179 // outside the bounds of immediate byte-extract operand, might still be in
180 // bounds of a parent object
181 offset += range_spect::to_range_spect(*index);
182 }
183 get_objects_rec(mode, be.op(), offset, size);
184 }
185}
186
188 get_modet mode,
189 const shift_exprt &shift,
190 const range_spect &range_start,
191 const range_spect &size)
192{
193 const exprt simp_distance=simplify_expr(shift.distance(), ns);
194
195 auto op_bits = pointer_offset_bits(shift.op().type(), ns);
196
197 range_spect src_size = op_bits.has_value()
200
201 const auto dist = numeric_cast<mp_integer>(simp_distance);
202 if(
203 range_start.is_unknown() || size.is_unknown() || src_size.is_unknown() ||
204 !dist.has_value())
205 {
207 mode, shift.op(), range_spect::unknown(), range_spect::unknown());
210 }
211 else
212 {
213 const range_spect dist_r = range_spect::to_range_spect(*dist);
214
215 // not sure whether to worry about
216 // config.ansi_c.endianness==configt::ansi_ct::IS_LITTLE_ENDIAN
217 // right here maybe?
218
219 if(shift.id()==ID_ashr || shift.id()==ID_lshr)
220 {
221 range_spect sh_range_start=range_start;
222 sh_range_start+=dist_r;
223
224 range_spect sh_size=std::min(size, src_size-sh_range_start);
225
226 if(sh_range_start >= range_spect{0} && sh_range_start < src_size)
227 get_objects_rec(mode, shift.op(), sh_range_start, sh_size);
228 }
229 if(src_size >= dist_r)
230 {
231 range_spect sh_size=std::min(size, src_size-dist_r);
232
233 get_objects_rec(mode, shift.op(), range_start, sh_size);
234 }
235 }
236}
237
239 get_modet mode,
240 const member_exprt &expr,
241 const range_spect &range_start,
242 const range_spect &size)
243{
244 const typet &type = expr.struct_op().type();
245
246 if(
247 type.id() == ID_union || type.id() == ID_union_tag ||
248 range_start.is_unknown())
249 {
250 get_objects_rec(mode, expr.struct_op(), range_start, size);
251 return;
252 }
253
254 const struct_typet &struct_type = to_struct_type(ns.follow(type));
255
256 auto offset_bits =
257 member_offset_bits(struct_type, expr.get_component_name(), ns);
258
260
261 if(offset_bits.has_value())
262 {
263 offset = range_spect::to_range_spect(*offset_bits);
264 offset += range_start;
265 }
266
267 get_objects_rec(mode, expr.struct_op(), offset, size);
268}
271 get_modet mode,
272 const index_exprt &expr,
273 const range_spect &range_start,
274 const range_spect &size)
275{
276 if(expr.array().id() == ID_null_object)
277 return;
278
280 const typet &type = expr.array().type();
281
282 if(type.id()==ID_vector)
283 {
284 const vector_typet &vector_type=to_vector_type(type);
285
286 auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
287
288 if(subtype_bits.has_value())
289 sub_size = range_spect::to_range_spect(*subtype_bits);
290 }
291 else if(type.id()==ID_array)
292 {
293 const array_typet &array_type=to_array_type(type);
294
295 auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
296
297 if(subtype_bits.has_value())
298 sub_size = range_spect::to_range_spect(*subtype_bits);
299 }
300 else
301 return;
302
303 const exprt simp_index=simplify_expr(expr.index(), ns);
304
305 const auto index = numeric_cast<mp_integer>(simp_index);
306 if(!index.has_value())
308
309 if(range_start.is_unknown() || sub_size.is_unknown() || !index.has_value())
310 get_objects_rec(mode, expr.array(), range_spect::unknown(), size);
311 else
312 {
314 mode,
315 expr.array(),
316 range_start + range_spect::to_range_spect(*index) * sub_size,
317 size);
318 }
319}
320
322 get_modet mode,
323 const array_exprt &expr,
324 const range_spect &range_start,
325 const range_spect &size)
326{
327 const array_typet &array_type = expr.type();
328
329 auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
330
331 if(!subtype_bits.has_value())
332 {
333 for(const auto &op : expr.operands())
335
336 return;
337 }
338
339 range_spect sub_size = range_spect::to_range_spect(*subtype_bits);
340
341 range_spect offset{0};
342 range_spect full_r_s =
343 range_start.is_unknown() ? range_spect{0} : range_start;
344 range_spect full_r_e =
346 ? sub_size * range_spect::to_range_spect(expr.operands().size())
347 : full_r_s + size;
348
349 for(const auto &op : expr.operands())
350 {
351 if(full_r_s<=offset+sub_size && full_r_e>offset)
352 {
353 range_spect cur_r_s =
354 full_r_s <= offset ? range_spect{0} : full_r_s - offset;
355 range_spect cur_r_e=
356 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
357
358 get_objects_rec(mode, op, cur_r_s, cur_r_e - cur_r_s);
359 }
360
361 offset+=sub_size;
362 }
363}
364
366 get_modet mode,
367 const struct_exprt &expr,
368 const range_spect &range_start,
369 const range_spect &size)
370{
371 const struct_typet &struct_type=
372 to_struct_type(ns.follow(expr.type()));
373
374 auto struct_bits = pointer_offset_bits(struct_type, ns);
375
376 range_spect full_size = struct_bits.has_value()
377 ? range_spect::to_range_spect(*struct_bits)
379
380 range_spect offset = range_spect{0};
381 range_spect full_r_s =
382 range_start.is_unknown() ? range_spect{0} : range_start;
383 range_spect full_r_e = size.is_unknown() || full_size.is_unknown()
385 : full_r_s + size;
386
387 for(const auto &op : expr.operands())
388 {
389 auto it_bits = pointer_offset_bits(op.type(), ns);
390
391 range_spect sub_size = it_bits.has_value()
394
395 if(offset.is_unknown())
396 {
397 get_objects_rec(mode, op, range_spect{0}, sub_size);
398 }
399 else if(sub_size.is_unknown())
400 {
401 if(full_r_e.is_unknown() || full_r_e > offset)
402 {
403 range_spect cur_r_s =
404 full_r_s <= offset ? range_spect{0} : full_r_s - offset;
405
406 get_objects_rec(mode, op, cur_r_s, range_spect::unknown());
407 }
408
409 offset = range_spect::unknown();
410 }
411 else if(full_r_e.is_unknown())
412 {
413 if(full_r_s<=offset+sub_size)
414 {
415 range_spect cur_r_s =
416 full_r_s <= offset ? range_spect{0} : full_r_s - offset;
417
418 get_objects_rec(mode, op, cur_r_s, sub_size - cur_r_s);
419 }
420
421 offset+=sub_size;
422 }
423 else if(full_r_s<=offset+sub_size && full_r_e>offset)
424 {
425 range_spect cur_r_s =
426 full_r_s <= offset ? range_spect{0} : full_r_s - offset;
427 range_spect cur_r_e=
428 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
429
430 get_objects_rec(mode, op, cur_r_s, cur_r_e - cur_r_s);
431
432 offset+=sub_size;
433 }
434 }
435}
436
438 get_modet mode,
439 const typecast_exprt &tc,
440 const range_spect &range_start,
441 const range_spect &size)
442{
443 const exprt &op=tc.op();
444
445 auto op_bits = pointer_offset_bits(op.type(), ns);
446
447 range_spect new_size = op_bits.has_value()
450
451 if(range_start.is_unknown())
452 new_size = range_spect::unknown();
453 else if(!new_size.is_unknown())
454 {
455 if(new_size<=range_start)
456 return;
457
458 new_size-=range_start;
459 new_size=std::min(size, new_size);
460 }
461
462 get_objects_rec(mode, op, range_start, new_size);
463}
464
466{
467 if(
468 object.id() == ID_string_constant || object.id() == ID_label ||
469 object.id() == ID_array || object.id() == ID_null_object ||
470 object.id() == ID_symbol)
471 {
472 // constant, nothing to do
473 return;
474 }
475 else if(object.id()==ID_dereference)
476 {
478 }
479 else if(object.id()==ID_index)
480 {
481 const index_exprt &index=to_index_expr(object);
482
485 }
486 else if(object.id()==ID_member)
487 {
488 const member_exprt &member=to_member_expr(object);
489
491 }
492 else if(object.id()==ID_if)
493 {
494 const if_exprt &if_expr=to_if_expr(object);
495
499 }
500 else if(object.id()==ID_byte_extract_little_endian ||
501 object.id()==ID_byte_extract_big_endian)
502 {
504
506 }
507 else if(object.id()==ID_typecast)
508 {
509 const typecast_exprt &tc=to_typecast_expr(object);
510
512 }
513 else
514 throw "rw_range_sett: address_of '" + object.id_string() + "' not handled";
515}
516
518 get_modet mode,
519 const irep_idt &identifier,
520 const range_spect &range_start,
521 const range_spect &range_end)
522{
523 objectst::iterator entry=
525 .insert(
526 std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
527 identifier, nullptr))
528 .first;
529
530 if(entry->second==nullptr)
531 entry->second=util_make_unique<range_domaint>();
532
533 static_cast<range_domaint&>(*entry->second).push_back(
534 {range_start, range_end});
535}
536
538 get_modet mode,
539 const exprt &expr,
540 const range_spect &range_start,
541 const range_spect &size)
542{
543 if(expr.id() == ID_complex_real)
545 mode, to_complex_real_expr(expr), range_start, size);
546 else if(expr.id() == ID_complex_imag)
548 mode, to_complex_imag_expr(expr), range_start, size);
549 else if(expr.id()==ID_typecast)
551 mode,
552 to_typecast_expr(expr),
553 range_start,
554 size);
555 else if(expr.id()==ID_if)
556 get_objects_if(mode, to_if_expr(expr), range_start, size);
557 else if(expr.id()==ID_dereference)
559 mode,
561 range_start,
562 size);
563 else if(expr.id()==ID_byte_extract_little_endian ||
564 expr.id()==ID_byte_extract_big_endian)
566 mode,
568 range_start,
569 size);
570 else if(expr.id()==ID_shl ||
571 expr.id()==ID_ashr ||
572 expr.id()==ID_lshr)
573 get_objects_shift(mode, to_shift_expr(expr), range_start, size);
574 else if(expr.id()==ID_member)
575 get_objects_member(mode, to_member_expr(expr), range_start, size);
576 else if(expr.id()==ID_index)
577 get_objects_index(mode, to_index_expr(expr), range_start, size);
578 else if(expr.id()==ID_array)
579 get_objects_array(mode, to_array_expr(expr), range_start, size);
580 else if(expr.id()==ID_struct)
581 get_objects_struct(mode, to_struct_expr(expr), range_start, size);
582 else if(expr.id()==ID_symbol)
583 {
584 const symbol_exprt &symbol=to_symbol_expr(expr);
585 const irep_idt identifier=symbol.get_identifier();
586
587 auto symbol_bits = pointer_offset_bits(symbol.type(), ns);
588
589 range_spect full_size = symbol_bits.has_value()
590 ? range_spect::to_range_spect(*symbol_bits)
592
593 if(
594 !full_size.is_unknown() &&
595 (full_size == range_spect{0} ||
596 (full_size > range_spect{0} && !range_start.is_unknown() &&
597 range_start >= full_size)))
598 {
599 // nothing to do, these are effectively constants (like function
600 // symbols or structs with no members)
601 // OR: invalid memory accesses
602 }
603 else if(!range_start.is_unknown() && range_start >= range_spect{0})
604 {
605 range_spect range_end =
606 size.is_unknown() ? range_spect::unknown() : range_start + size;
607 if(!size.is_unknown() && !full_size.is_unknown())
608 range_end=std::min(range_end, full_size);
609
610 add(mode, identifier, range_start, range_end);
611 }
612 else
613 add(mode, identifier, range_spect{0}, range_spect::unknown());
614 }
615 else if(mode==get_modet::READ && expr.id()==ID_address_of)
617 else if(mode==get_modet::READ)
618 {
619 // possibly affects the full object size, even if range_start/size
620 // are only a subset of the bytes (e.g., when using the result of
621 // arithmetic operations)
622 for(const auto &op : expr.operands())
623 get_objects_rec(mode, op);
624 }
625 else if(expr.id() == ID_null_object ||
626 expr.id() == ID_string_constant)
627 {
628 // dereferencing may yield some weird ones, ignore these
629 }
630 else if(mode==get_modet::LHS_W)
631 {
632 for(const auto &op : expr.operands())
633 get_objects_rec(mode, op);
634 }
635 else
636 throw "rw_range_sett: assignment to '" + expr.id_string() + "' not handled";
637}
638
640{
641 auto expr_bits = pointer_offset_bits(expr.type(), ns);
642
643 range_spect size = expr_bits.has_value()
644 ? range_spect::to_range_spect(*expr_bits)
646
647 get_objects_rec(mode, expr, range_spect{0}, size);
648}
649
651{
652 // TODO should recurse into various composite types
653 if(type.id()==ID_array)
654 {
655 const auto &array_type = to_array_type(type);
656 get_objects_rec(array_type.element_type());
657 get_objects_rec(get_modet::READ, array_type.size());
658 }
659}
660
672
674 get_modet mode,
675 const dereference_exprt &deref,
676 const range_spect &range_start,
677 const range_spect &size)
678{
680 mode,
681 deref,
682 range_start,
683 size);
684
685 exprt object=deref;
687
688 auto type_bits = pointer_offset_bits(object.type(), ns);
689
691
692 if(type_bits.has_value())
693 {
694 new_size = range_spect::to_range_spect(*type_bits);
695
696 if(range_start.is_unknown() || new_size <= range_start)
697 new_size = range_spect::unknown();
698 else
699 {
700 new_size -= range_start;
701 new_size = std::min(size, new_size);
702 }
703 }
704
705 // value_set_dereferencet::build_reference_to will turn *p into
706 // DYNAMIC_OBJECT(p) ? *p : invalid_objectN
707 if(object.is_not_nil() && !has_subexpr(object, ID_dereference))
708 get_objects_rec(mode, object, range_start, new_size);
709}
710
712 const namespacet &ns, std::ostream &out) const
713{
714 out << "[";
715 for(const_iterator itr=begin();
716 itr!=end();
717 ++itr)
718 {
719 if(itr!=begin())
720 out << ";";
721 out << itr->first << ":" << itr->second.first;
722 // we don't know what mode (language) we are in, so we rely on the default
723 // language to be reasonable for from_expr
724 out << " if " << from_expr(ns, irep_idt(), itr->second.second);
725 }
726 out << "]";
727}
728
730 get_modet mode,
731 const if_exprt &if_expr,
732 const range_spect &range_start,
733 const range_spect &size)
734{
735 if(if_expr.cond().is_false())
736 get_objects_rec(mode, if_expr.false_case(), range_start, size);
737 else if(if_expr.cond().is_true())
738 get_objects_rec(mode, if_expr.true_case(), range_start, size);
739 else
740 {
742
743 guardt copy = guard;
744
745 guard.add(not_exprt(if_expr.cond()));
746 get_objects_rec(mode, if_expr.false_case(), range_start, size);
747 guard = copy;
748
749 guard.add(if_expr.cond());
750 get_objects_rec(mode, if_expr.true_case(), range_start, size);
751 guard = std::move(copy);
752 }
753}
754
756 get_modet mode,
757 const irep_idt &identifier,
758 const range_spect &range_start,
759 const range_spect &range_end)
760{
761 objectst::iterator entry=
763 .insert(
764 std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
765 identifier, nullptr))
766 .first;
767
768 if(entry->second==nullptr)
770
771 static_cast<guarded_range_domaint&>(*entry->second).insert(
772 {range_start, {range_end, guard.as_expr()}});
773}
774
775static void goto_rw_assign(
776 const irep_idt &function,
778 const exprt &lhs,
779 const exprt &rhs,
780 rw_range_sett &rw_set)
781{
782 rw_set.get_objects_rec(
783 function, target, rw_range_sett::get_modet::LHS_W, lhs);
784 rw_set.get_objects_rec(function, target, rw_range_sett::get_modet::READ, rhs);
785}
786
787static void goto_rw_other(
788 const irep_idt &function,
790 const codet &code,
791 rw_range_sett &rw_set)
792{
793 const irep_idt &statement = code.get_statement();
794
795 if(statement == ID_printf)
796 {
797 // if it's printf, mark the operands as read here
798 for(const auto &op : code.operands())
799 {
800 rw_set.get_objects_rec(
801 function, target, rw_range_sett::get_modet::READ, op);
802 }
803 }
804 else if(statement == ID_array_equal)
805 {
806 // mark the dereferenced operands as being read
807 PRECONDITION(code.operands().size() == 3);
808 rw_set.get_array_objects(
809 function, target, rw_range_sett::get_modet::READ, code.op0());
810 rw_set.get_array_objects(
811 function, target, rw_range_sett::get_modet::READ, code.op1());
812 // the third operand is the result
813 rw_set.get_objects_rec(
814 function, target, rw_range_sett::get_modet::LHS_W, code.op2());
815 }
816 else if(statement == ID_array_set)
817 {
818 PRECONDITION(code.operands().size() == 2);
819 rw_set.get_array_objects(
820 function, target, rw_range_sett::get_modet::LHS_W, code.op0());
821 rw_set.get_objects_rec(
822 function, target, rw_range_sett::get_modet::READ, code.op1());
823 }
824 else if(statement == ID_array_copy || statement == ID_array_replace)
825 {
826 PRECONDITION(code.operands().size() == 2);
827 rw_set.get_array_objects(
828 function, target, rw_range_sett::get_modet::LHS_W, code.op0());
829 rw_set.get_array_objects(
830 function, target, rw_range_sett::get_modet::READ, code.op1());
831 }
832 else if(statement == ID_havoc_object)
833 {
834 PRECONDITION(code.operands().size() == 1);
835 // re-use get_array_objects as this havoc_object affects whatever is the
836 // object being the pointer that code.op0() is
837 rw_set.get_array_objects(
838 function, target, rw_range_sett::get_modet::LHS_W, code.op0());
839 }
840}
841
842static void goto_rw(
843 const irep_idt &function,
845 const exprt &lhs,
846 const exprt &function_expr,
847 const exprt::operandst &arguments,
848 rw_range_sett &rw_set)
849{
850 if(lhs.is_not_nil())
851 rw_set.get_objects_rec(
852 function, target, rw_range_sett::get_modet::LHS_W, lhs);
853
854 rw_set.get_objects_rec(
855 function, target, rw_range_sett::get_modet::READ, function_expr);
856
857 for(const auto &argument : arguments)
858 {
859 rw_set.get_objects_rec(
860 function, target, rw_range_sett::get_modet::READ, argument);
861 }
862}
863
865 const irep_idt &function,
867 rw_range_sett &rw_set)
868{
869 switch(target->type())
870 {
872 case INCOMPLETE_GOTO:
874 break;
875
876 case GOTO:
877 case ASSUME:
878 case ASSERT:
879 rw_set.get_objects_rec(
880 function, target, rw_range_sett::get_modet::READ, target->condition());
881 break;
882
883 case SET_RETURN_VALUE:
884 rw_set.get_objects_rec(
885 function, target, rw_range_sett::get_modet::READ, target->return_value());
886 break;
887
888 case OTHER:
889 goto_rw_other(function, target, target->get_other(), rw_set);
890 break;
891
892 case SKIP:
893 case START_THREAD:
894 case END_THREAD:
895 case LOCATION:
896 case END_FUNCTION:
897 case ATOMIC_BEGIN:
898 case ATOMIC_END:
899 case THROW:
900 case CATCH:
901 // these don't read or write anything
902 break;
903
904 case ASSIGN:
906 function, target, target->assign_lhs(), target->assign_rhs(), rw_set);
907 break;
908
909 case DEAD:
910 rw_set.get_objects_rec(
911 function, target, rw_range_sett::get_modet::LHS_W, target->dead_symbol());
912 break;
913
914 case DECL:
915 rw_set.get_objects_rec(function, target, target->decl_symbol().type());
916 rw_set.get_objects_rec(
917 function, target, rw_range_sett::get_modet::LHS_W, target->decl_symbol());
918 break;
919
920 case FUNCTION_CALL:
921 goto_rw(
922 function,
923 target,
924 target->call_lhs(),
925 target->call_function(),
926 target->call_arguments(),
927 rw_set);
928 break;
929 }
930}
931
933 const irep_idt &function,
934 const goto_programt &goto_program,
935 rw_range_sett &rw_set)
936{
937 forall_goto_program_instructions(i_it, goto_program)
938 goto_rw(function, i_it, rw_set);
939}
940
941void goto_rw(const goto_functionst &goto_functions,
942 const irep_idt &function,
943 rw_range_sett &rw_set)
944{
945 goto_functionst::function_mapt::const_iterator f_it=
946 goto_functions.function_map.find(function);
947
948 if(f_it!=goto_functions.function_map.end())
949 {
950 const goto_programt &body=f_it->second.body;
951
952 goto_rw(f_it->first, body, rw_set);
953 }
954}
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
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.
Array constructor from list of elements.
Definition std_expr.h:1563
const array_typet & type() const
Definition std_expr.h:1570
Arrays with given size.
Definition std_types.h:763
const exprt & size() const
Definition std_types.h:796
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:783
Expression of type type extracted from some object op starting at position offset (given in number of...
std::size_t get_bits_per_byte() const
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
exprt & op2()
Definition expr.h:131
const irep_idt & get_statement() const
Imaginary part of the expression describing a complex number.
Definition std_expr.h:1971
Real part of the expression describing a complex number.
Definition std_expr.h:1926
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Maps a big-endian offset to a little-endian offset.
size_t map_bit(size_t bit) const
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
void add(const exprt &expr)
exprt as_expr() const
Definition guard_expr.h:46
virtual void output(const namespacet &ns, std::ostream &out) const override
Definition goto_rw.cpp:711
sub_typet::const_iterator const_iterator
Definition goto_rw.h:439
The trinary if-then-else operator.
Definition std_expr.h:2323
exprt & cond()
Definition std_expr.h:2340
exprt & false_case()
Definition std_expr.h:2360
exprt & true_case()
Definition std_expr.h:2350
Array index operator.
Definition std_expr.h:1410
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
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:2794
const exprt & struct_op() const
Definition std_expr.h:2832
irep_idt get_component_name() const
Definition std_expr.h:2816
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:2278
Split an expression into a base object and a (byte) offset.
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
static const exprt & root_object(const exprt &expr)
virtual ~range_domain_baset()
Definition goto_rw.cpp:31
void output(const namespacet &ns, std::ostream &out) const override
Definition goto_rw.cpp:35
iterator end()
Definition goto_rw.h:191
sub_typet::const_iterator const_iterator
Definition goto_rw.h:185
iterator begin()
Definition goto_rw.h:187
Data type to describe upper and lower bounds of the range of bits that a read or write access may aff...
Definition goto_rw.h:61
static range_spect unknown()
Definition goto_rw.h:69
static range_spect to_range_spect(const mp_integer &size)
Definition goto_rw.h:79
bool is_unknown() const
Definition goto_rw.h:74
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
Definition goto_rw.h:481
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:729
void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) override
Definition goto_rw.cpp:755
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:673
value_setst & value_sets
Definition goto_rw.h:415
goto_programt::const_targett target
Definition goto_rw.h:417
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
Definition goto_rw.h:379
void output(std::ostream &out) const
Definition goto_rw.cpp:62
objectst r_range_set
Definition goto_rw.h:267
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:83
virtual ~rw_range_sett()
Definition goto_rw.cpp:49
const objectst & get_w_set() const
Definition goto_rw.h:225
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:187
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:270
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:365
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:92
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:465
objectst w_range_set
Definition goto_rw.h:267
virtual void get_array_objects(const irep_idt &, goto_programt::const_targett, get_modet, const exprt &)
Definition goto_rw.cpp:661
const objectst & get_r_set() const
Definition goto_rw.h:220
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:239
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:238
const namespacet & ns
Definition goto_rw.h:265
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition goto_rw.cpp:517
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:437
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:321
A base class for shift and rotate operators.
exprt & distance()
Struct constructor from list of elements.
Definition std_expr.h:1819
Structure type, corresponds to C style structs.
Definition std_types.h:231
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
const typet & subtype() const
Definition type.h:154
Semantic type conversion.
Definition std_expr.h:2017
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:326
The vector type.
Definition std_types.h:1008
const typet & element_type() const
The type of the elements of the vector.
Definition std_types.h:1024
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
Goto Programs with Functions.
#define forall_goto_program_instructions(it, program)
@ FUNCTION_CALL
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
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:775
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:842
static void goto_rw_other(const irep_idt &function, goto_programt::const_targett target, const codet &code, rw_range_sett &rw_set)
Definition goto_rw.cpp:787
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
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.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
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:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1842
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1603
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:1997
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:1952
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1060
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:1102
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
dstringt irep_idt