CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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/namespace.h>
19#include <util/pointer_expr.h>
21#include <util/simplify_expr.h>
22
24
27
28#include <memory>
29
33
34void range_domaint::output(const namespacet &, std::ostream &out) const
35{
36 out << "[";
38 itr!=end();
39 ++itr)
40 {
41 if(itr!=begin())
42 out << ";";
43 out << itr->first << ":" << itr->second;
44 }
45 out << "]";
46}
47
49{
50 for(rw_range_sett::objectst::iterator it=r_range_set.begin();
51 it!=r_range_set.end();
52 ++it)
53 it->second=nullptr;
54
55 for(rw_range_sett::objectst::iterator it=w_range_set.begin();
56 it!=w_range_set.end();
57 ++it)
58 it->second=nullptr;
59}
60
61void rw_range_sett::output(std::ostream &out) const
62{
63 out << "READ:\n";
64 for(const auto &read_object_entry : get_r_set())
65 {
66 out << " " << read_object_entry.first;
67 read_object_entry.second->output(ns, out);
68 out << '\n';
69 }
70
71 out << '\n';
72
73 out << "WRITE:\n";
74 for(const auto &written_object_entry : get_w_set())
75 {
76 out << " " << written_object_entry.first;
77 written_object_entry.second->output(ns, out);
78 out << '\n';
79 }
80}
81
83 get_modet mode,
84 const complex_real_exprt &expr,
86 const range_spect &size)
87{
88 get_objects_rec(mode, expr.op(), range_start, size);
89}
90
92 get_modet mode,
93 const complex_imag_exprt &expr,
95 const range_spect &size)
96{
97 const exprt &op = expr.op();
98
99 auto subtype_bits =
100 pointer_offset_bits(to_complex_type(op.type()).subtype(), ns);
101 CHECK_RETURN(subtype_bits.has_value());
102
105
106 range_spect offset =
107 (range_start.is_unknown() || expr.id() == ID_complex_real) ? range_spect{0}
108 : sub_size;
109
110 get_objects_rec(mode, op, range_start + offset, size);
111}
112
114 get_modet mode,
115 const if_exprt &if_expr,
117 const range_spect &size)
118{
119 if(if_expr.cond().is_false())
120 get_objects_rec(mode, if_expr.false_case(), range_start, size);
121 else if(if_expr.cond().is_true())
122 get_objects_rec(mode, if_expr.true_case(), range_start, size);
123 else
124 {
126
127 get_objects_rec(mode, if_expr.false_case(), range_start, size);
128 get_objects_rec(mode, if_expr.true_case(), range_start, size);
129 }
130}
131
133 get_modet mode,
135 const range_spect &,
136 const range_spect &)
137{
138 const exprt &pointer=deref.pointer();
140 if(mode!=get_modet::READ)
141 get_objects_rec(mode, pointer);
142}
143
145 get_modet mode,
146 const byte_extract_exprt &be,
148 const range_spect &size)
149{
150 auto object_size_bits_opt = pointer_offset_bits(be.op().type(), ns);
151 const exprt simp_offset=simplify_expr(be.offset(), ns);
152
154 if(
155 range_start.is_unknown() || !index.has_value() ||
156 !object_size_bits_opt.has_value())
157 {
158 get_objects_rec(mode, be.op(), range_spect::unknown(), size);
159 }
160 else
161 {
162 *index *= be.get_bits_per_byte();
163 if(*index >= *object_size_bits_opt)
164 return;
165
166 endianness_mapt map(
167 be.op().type(),
169 ns);
170 range_spect offset = range_start;
171 if(*index > 0)
172 {
175 }
176 else
177 {
178 // outside the bounds of immediate byte-extract operand, might still be in
179 // bounds of a parent object
180 offset += range_spect::to_range_spect(*index);
181 }
182 get_objects_rec(mode, be.op(), offset, size);
183 }
184}
185
187 get_modet mode,
188 const shift_exprt &shift,
190 const range_spect &size)
191{
193
194 auto op_bits = pointer_offset_bits(shift.op().type(), ns);
195
196 range_spect src_size = op_bits.has_value()
199
201 if(
202 range_start.is_unknown() || size.is_unknown() || src_size.is_unknown() ||
203 !dist.has_value())
204 {
206 mode, shift.op(), range_spect::unknown(), range_spect::unknown());
209 }
210 else
211 {
213
214 // not sure whether to worry about
215 // config.ansi_c.endianness==configt::ansi_ct::IS_LITTLE_ENDIAN
216 // right here maybe?
217
218 if(shift.id()==ID_ashr || shift.id()==ID_lshr)
219 {
222
223 range_spect sh_size=std::min(size, src_size-sh_range_start);
224
226 get_objects_rec(mode, shift.op(), sh_range_start, sh_size);
227 }
228 if(src_size >= dist_r)
229 {
230 range_spect sh_size=std::min(size, src_size-dist_r);
231
232 get_objects_rec(mode, shift.op(), range_start, sh_size);
233 }
234 }
235}
236
238 get_modet mode,
239 const member_exprt &expr,
241 const range_spect &size)
242{
243 const typet &type = expr.struct_op().type();
244
245 if(
246 type.id() == ID_union || type.id() == ID_union_tag ||
247 range_start.is_unknown())
248 {
249 get_objects_rec(mode, expr.struct_op(), range_start, size);
250 return;
251 }
252
253 const struct_typet &struct_type = type.id() == ID_struct
254 ? to_struct_type(type)
255 : ns.follow_tag(to_struct_tag_type(type));
256
257 auto offset_bits =
259
261
262 if(offset_bits.has_value())
263 {
265 offset += range_start;
266 }
267
268 get_objects_rec(mode, expr.struct_op(), offset, size);
270
272 get_modet mode,
273 const index_exprt &expr,
275 const range_spect &size)
276{
277 if(expr.array().id() == ID_null_object)
278 return;
279
281 const typet &type = expr.array().type();
282
283 if(type.id()==ID_vector)
284 {
286
287 auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
288
289 if(subtype_bits.has_value())
291 }
292 else if(type.id()==ID_array)
293 {
295
296 auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
297
298 if(subtype_bits.has_value())
300 }
301 else
302 return;
303
304 const exprt simp_index=simplify_expr(expr.index(), ns);
305
306 const auto index = numeric_cast<mp_integer>(simp_index);
307 if(!index.has_value())
309
310 if(range_start.is_unknown() || sub_size.is_unknown() || !index.has_value())
311 get_objects_rec(mode, expr.array(), range_spect::unknown(), size);
312 else
313 {
315 mode,
316 expr.array(),
318 size);
319 }
320}
321
323 get_modet mode,
324 const array_exprt &expr,
326 const range_spect &size)
327{
328 const array_typet &array_type = expr.type();
329
330 auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
331
332 if(!subtype_bits.has_value())
333 {
334 for(const auto &op : expr.operands())
336
337 return;
338 }
339
342 range_spect offset{0};
344 range_start.is_unknown() ? range_spect{0} : range_start;
346 size.is_unknown()
348 : full_r_s + size;
349
350 for(const auto &op : expr.operands())
351 {
353 {
355 full_r_s <= offset ? range_spect{0} : full_r_s - offset;
357 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
358
360 }
361
362 offset+=sub_size;
363 }
364}
365
367 get_modet mode,
368 const struct_exprt &expr,
370 const range_spect &size)
371{
373 expr.type().id() == ID_struct
374 ? to_struct_type(expr.type())
375 : ns.follow_tag(to_struct_tag_type(expr.type()));
376
378
379 range_spect full_size = struct_bits.has_value()
382
383 range_spect offset = range_spect{0};
385 range_start.is_unknown() ? range_spect{0} : range_start;
386 range_spect full_r_e = size.is_unknown() || full_size.is_unknown()
388 : full_r_s + size;
389
390 for(const auto &op : expr.operands())
391 {
392 auto it_bits = pointer_offset_bits(op.type(), ns);
393
394 range_spect sub_size = it_bits.has_value()
397
398 if(offset.is_unknown())
399 {
400 get_objects_rec(mode, op, range_spect{0}, sub_size);
401 }
402 else if(sub_size.is_unknown())
403 {
404 if(full_r_e.is_unknown() || full_r_e > offset)
405 {
407 full_r_s <= offset ? range_spect{0} : full_r_s - offset;
408
410 }
411
412 offset = range_spect::unknown();
413 }
414 else if(full_r_e.is_unknown())
415 {
416 if(full_r_s<=offset+sub_size)
417 {
419 full_r_s <= offset ? range_spect{0} : full_r_s - offset;
420
422 }
423
424 offset+=sub_size;
425 }
427 {
429 full_r_s <= offset ? range_spect{0} : full_r_s - offset;
431 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
432
434
435 offset+=sub_size;
436 }
437 }
438}
439
441 get_modet mode,
442 const typecast_exprt &tc,
444 const range_spect &size)
445{
446 const exprt &op=tc.op();
447
448 auto op_bits = pointer_offset_bits(op.type(), ns);
449
450 range_spect new_size = op_bits.has_value()
453
454 if(range_start.is_unknown())
456 else if(!new_size.is_unknown())
457 {
459 return;
460
462 new_size=std::min(size, new_size);
463 }
464
466}
467
469{
470 if(
471 object.id() == ID_string_constant || object.id() == ID_label ||
472 object.id() == ID_array || object.id() == ID_null_object ||
473 object.id() == ID_symbol)
474 {
475 // constant, nothing to do
476 return;
477 }
478 else if(object.id()==ID_dereference)
479 {
481 }
482 else if(object.id()==ID_index)
483 {
484 const index_exprt &index=to_index_expr(object);
485
488 }
489 else if(object.id()==ID_member)
490 {
491 const member_exprt &member=to_member_expr(object);
492
494 }
495 else if(object.id()==ID_if)
496 {
497 const if_exprt &if_expr=to_if_expr(object);
498
502 }
503 else if(object.id()==ID_byte_extract_little_endian ||
504 object.id()==ID_byte_extract_big_endian)
505 {
507
509 }
510 else if(object.id()==ID_typecast)
511 {
512 const typecast_exprt &tc=to_typecast_expr(object);
513
515 }
516 else
517 throw "rw_range_sett: address_of '" + object.id_string() + "' not handled";
518}
519
521 get_modet mode,
522 const irep_idt &identifier,
524 const range_spect &range_end)
525{
526 objectst::iterator entry=
528 .insert(
529 std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
530 identifier, nullptr))
531 .first;
532
533 if(entry->second==nullptr)
534 entry->second = std::make_unique<range_domaint>();
535
536 static_cast<range_domaint&>(*entry->second).push_back(
538}
539
541 get_modet mode,
542 const exprt &expr,
544 const range_spect &size)
545{
546 if(expr.id() == ID_complex_real)
548 mode, to_complex_real_expr(expr), range_start, size);
549 else if(expr.id() == ID_complex_imag)
551 mode, to_complex_imag_expr(expr), range_start, size);
552 else if(expr.id()==ID_typecast)
554 mode,
555 to_typecast_expr(expr),
557 size);
558 else if(expr.id()==ID_if)
559 get_objects_if(mode, to_if_expr(expr), range_start, size);
560 else if(expr.id()==ID_dereference)
562 mode,
565 size);
566 else if(expr.id()==ID_byte_extract_little_endian ||
569 mode,
572 size);
573 else if(expr.id()==ID_shl ||
574 expr.id()==ID_ashr ||
575 expr.id()==ID_lshr)
576 get_objects_shift(mode, to_shift_expr(expr), range_start, size);
577 else if(expr.id()==ID_member)
579 else if(expr.id()==ID_index)
580 get_objects_index(mode, to_index_expr(expr), range_start, size);
581 else if(expr.id()==ID_array)
582 get_objects_array(mode, to_array_expr(expr), range_start, size);
583 else if(expr.id()==ID_struct)
585 else if(expr.id()==ID_symbol)
586 {
587 const symbol_exprt &symbol=to_symbol_expr(expr);
588 const irep_idt identifier=symbol.get_identifier();
589
590 auto symbol_bits = pointer_offset_bits(symbol.type(), ns);
591
592 range_spect full_size = symbol_bits.has_value()
595
596 if(
597 !full_size.is_unknown() &&
598 (full_size == range_spect{0} ||
599 (full_size > range_spect{0} && !range_start.is_unknown() &&
601 {
602 // nothing to do, these are effectively constants (like function
603 // symbols or structs with no members)
604 // OR: invalid memory accesses
605 }
606 else if(!range_start.is_unknown() && range_start >= range_spect{0})
607 {
609 size.is_unknown() ? range_spect::unknown() : range_start + size;
610 if(!size.is_unknown() && !full_size.is_unknown())
611 range_end=std::min(range_end, full_size);
612
613 add(mode, identifier, range_start, range_end);
614 }
615 else
616 add(mode, identifier, range_spect{0}, range_spect::unknown());
617 }
618 else if(mode==get_modet::READ && expr.id()==ID_address_of)
620 else if(mode==get_modet::READ)
621 {
622 // possibly affects the full object size, even if range_start/size
623 // are only a subset of the bytes (e.g., when using the result of
624 // arithmetic operations)
625 for(const auto &op : expr.operands())
626 get_objects_rec(mode, op);
627 }
628 else if(expr.id() == ID_null_object ||
629 expr.id() == ID_string_constant)
630 {
631 // dereferencing may yield some weird ones, ignore these
632 }
633 else if(mode==get_modet::LHS_W)
634 {
635 for(const auto &op : expr.operands())
636 get_objects_rec(mode, op);
637 }
638 else
639 throw "rw_range_sett: assignment to '" + expr.id_string() + "' not handled";
640}
641
643{
644 auto expr_bits = pointer_offset_bits(expr.type(), ns);
645
646 range_spect size = expr_bits.has_value()
649
650 get_objects_rec(mode, expr, range_spect{0}, size);
651}
652
654{
655 // TODO should recurse into various composite types
656 if(type.id()==ID_array)
657 {
658 const auto &array_type = to_array_type(type);
659 get_objects_rec(array_type.element_type());
661 }
662}
663
665 const irep_idt &,
667 get_modet mode,
668 const exprt &pointer)
669{
671 ode.build(dereference_exprt{skip_typecast(pointer)}, ns);
673 mode, ode.root_object(), range_spect::unknown(), range_spect::unknown());
674}
675
677 get_modet mode,
680 const range_spect &size)
681{
683 mode,
684 deref,
686 size);
687
688 exprt object=deref;
690
691 auto type_bits = pointer_offset_bits(object.type(), ns);
692
694
695 if(type_bits.has_value())
696 {
698
699 if(range_start.is_unknown() || new_size <= range_start)
701 else
702 {
704 new_size = std::min(size, new_size);
705 }
706 }
707
708 // value_set_dereferencet::build_reference_to will turn *p into
709 // DYNAMIC_OBJECT(p) ? *p : invalid_objectN
710 if(object.is_not_nil() && !has_subexpr(object, ID_dereference))
711 get_objects_rec(mode, object, range_start, new_size);
712}
713
715 const namespacet &ns, std::ostream &out) const
716{
717 out << "[";
719 itr!=end();
720 ++itr)
721 {
722 if(itr!=begin())
723 out << ";";
724 out << itr->first << ":" << itr->second.first;
725 // we don't know what mode (language) we are in, so we rely on the default
726 // language to be reasonable for from_expr
727 out << " if " << from_expr(ns, irep_idt(), itr->second.second);
728 }
729 out << "]";
730}
731
733 get_modet mode,
734 const if_exprt &if_expr,
736 const range_spect &size)
737{
738 if(if_expr.cond().is_false())
739 get_objects_rec(mode, if_expr.false_case(), range_start, size);
740 else if(if_expr.cond().is_true())
741 get_objects_rec(mode, if_expr.true_case(), range_start, size);
742 else
743 {
745
746 guardt copy = guard;
747
748 guard.add(not_exprt(if_expr.cond()));
749 get_objects_rec(mode, if_expr.false_case(), range_start, size);
750 guard = copy;
751
752 guard.add(if_expr.cond());
753 get_objects_rec(mode, if_expr.true_case(), range_start, size);
754 guard = std::move(copy);
755 }
756}
757
759 get_modet mode,
760 const irep_idt &identifier,
762 const range_spect &range_end)
763{
764 objectst::iterator entry=
766 .insert(
767 std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
768 identifier, nullptr))
769 .first;
770
771 if(entry->second==nullptr)
772 entry->second = std::make_unique<guarded_range_domaint>();
773
774 static_cast<guarded_range_domaint&>(*entry->second).insert(
776}
777
778static void goto_rw_assign(
779 const irep_idt &function,
781 const exprt &lhs,
782 const exprt &rhs,
784{
785 rw_set.get_objects_rec(
786 function, target, rw_range_sett::get_modet::LHS_W, lhs);
787 rw_set.get_objects_rec(function, target, rw_range_sett::get_modet::READ, rhs);
788}
789
790static void goto_rw_other(
791 const irep_idt &function,
793 const codet &code,
795{
796 const irep_idt &statement = code.get_statement();
797
798 if(statement == ID_printf)
799 {
800 // if it's printf, mark the operands as read here
801 for(const auto &op : code.operands())
802 {
803 rw_set.get_objects_rec(
804 function, target, rw_range_sett::get_modet::READ, op);
805 }
806 }
807 else if(statement == ID_array_equal)
808 {
809 // mark the dereferenced operands as being read
810 PRECONDITION(code.operands().size() == 3);
811 rw_set.get_array_objects(
812 function, target, rw_range_sett::get_modet::READ, code.op0());
813 rw_set.get_array_objects(
814 function, target, rw_range_sett::get_modet::READ, code.op1());
815 // the third operand is the result
816 rw_set.get_objects_rec(
817 function, target, rw_range_sett::get_modet::LHS_W, code.op2());
818 }
819 else if(statement == ID_array_set)
820 {
821 PRECONDITION(code.operands().size() == 2);
822 rw_set.get_array_objects(
823 function, target, rw_range_sett::get_modet::LHS_W, code.op0());
824 rw_set.get_objects_rec(
825 function, target, rw_range_sett::get_modet::READ, code.op1());
826 }
827 else if(statement == ID_array_copy || statement == ID_array_replace)
828 {
829 PRECONDITION(code.operands().size() == 2);
830 rw_set.get_array_objects(
831 function, target, rw_range_sett::get_modet::LHS_W, code.op0());
832 rw_set.get_array_objects(
833 function, target, rw_range_sett::get_modet::READ, code.op1());
834 }
835 else if(statement == ID_havoc_object)
836 {
837 PRECONDITION(code.operands().size() == 1);
838 // re-use get_array_objects as this havoc_object affects whatever is the
839 // object being the pointer that code.op0() is
840 rw_set.get_array_objects(
841 function, target, rw_range_sett::get_modet::LHS_W, code.op0());
842 }
843}
844
845static void goto_rw(
846 const irep_idt &function,
848 const exprt &lhs,
849 const exprt &function_expr,
850 const exprt::operandst &arguments,
852{
853 if(lhs.is_not_nil())
854 rw_set.get_objects_rec(
855 function, target, rw_range_sett::get_modet::LHS_W, lhs);
856
857 rw_set.get_objects_rec(
859
860 for(const auto &argument : arguments)
861 {
862 rw_set.get_objects_rec(
863 function, target, rw_range_sett::get_modet::READ, argument);
864 }
865}
866
868 const irep_idt &function,
871{
872 switch(target->type())
873 {
875 case INCOMPLETE_GOTO:
877 break;
878
879 case GOTO:
880 case ASSUME:
881 case ASSERT:
882 rw_set.get_objects_rec(
883 function, target, rw_range_sett::get_modet::READ, target->condition());
884 break;
885
886 case SET_RETURN_VALUE:
887 rw_set.get_objects_rec(
888 function, target, rw_range_sett::get_modet::READ, target->return_value());
889 break;
890
891 case OTHER:
892 goto_rw_other(function, target, target->get_other(), rw_set);
893 break;
894
895 case SKIP:
896 case START_THREAD:
897 case END_THREAD:
898 case LOCATION:
899 case END_FUNCTION:
900 case ATOMIC_BEGIN:
901 case ATOMIC_END:
902 case THROW:
903 case CATCH:
904 // these don't read or write anything
905 break;
906
907 case ASSIGN:
909 function, target, target->assign_lhs(), target->assign_rhs(), rw_set);
910 break;
911
912 case DEAD:
913 rw_set.get_objects_rec(
914 function, target, rw_range_sett::get_modet::LHS_W, target->dead_symbol());
915 break;
916
917 case DECL:
918 rw_set.get_objects_rec(function, target, target->decl_symbol().type());
919 rw_set.get_objects_rec(
920 function, target, rw_range_sett::get_modet::LHS_W, target->decl_symbol());
921 break;
922
923 case FUNCTION_CALL:
924 goto_rw(
925 function,
926 target,
927 target->call_lhs(),
928 target->call_function(),
929 target->call_arguments(),
930 rw_set);
931 break;
932 }
933}
934
936 const irep_idt &function,
937 const goto_programt &goto_program,
939{
941 goto_rw(function, i_it, rw_set);
942}
943
944void goto_rw(const goto_functionst &goto_functions,
945 const irep_idt &function,
947{
948 goto_functionst::function_mapt::const_iterator f_it=
949 goto_functions.function_map.find(function);
950
951 if(f_it!=goto_functions.function_map.end())
952 {
953 const goto_programt &body=f_it->second.body;
954
955 goto_rw(f_it->first, body, rw_set);
956 }
957}
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.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Array constructor from list of elements.
Definition std_expr.h:1621
const array_typet & type() const
Definition std_expr.h:1628
Arrays with given size.
Definition std_types.h:807
Expression of type type extracted from some object op starting at position offset (given in number of...
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
const irep_idt & get_statement() const
Imaginary part of the expression describing a complex number.
Definition std_expr.h:2027
Real part of the expression describing a complex number.
Definition std_expr.h:1984
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:38
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
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:714
sub_typet::const_iterator const_iterator
Definition goto_rw.h:435
The trinary if-then-else operator.
Definition std_expr.h:2497
Array index operator.
Definition std_expr.h:1470
exprt & index()
Definition std_expr.h:1510
exprt & array()
Definition std_expr.h:1500
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
Extract member of struct or union.
Definition std_expr.h:2971
const exprt & struct_op() const
Definition std_expr.h:3009
irep_idt get_component_name() const
Definition std_expr.h:2993
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:2454
Split an expression into a base object and a (byte) offset.
virtual ~range_domain_baset()
Definition goto_rw.cpp:30
void output(const namespacet &ns, std::ostream &out) const override
Definition goto_rw.cpp:34
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:478
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:732
void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) override
Definition goto_rw.cpp:758
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:676
value_setst & value_sets
Definition goto_rw.h:411
goto_programt::const_targett target
Definition goto_rw.h:413
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
Definition goto_rw.h:375
void output(std::ostream &out) const
Definition goto_rw.cpp:61
objectst r_range_set
Definition goto_rw.h:263
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:132
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:82
message_handlert & message_handler
Definition goto_rw.h:261
virtual ~rw_range_sett()
Definition goto_rw.cpp:48
const objectst & get_w_set() const
Definition goto_rw.h:220
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:186
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:271
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:366
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:91
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:113
virtual void get_objects_address_of(const exprt &object)
Definition goto_rw.cpp:468
objectst w_range_set
Definition goto_rw.h:263
virtual void get_array_objects(const irep_idt &, goto_programt::const_targett, get_modet, const exprt &)
Definition goto_rw.cpp:664
const objectst & get_r_set() const
Definition goto_rw.h:215
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:144
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
Definition goto_rw.h:234
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:237
const namespacet & ns
Definition goto_rw.h:260
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition goto_rw.cpp:520
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:440
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:322
A base class for shift and rotate operators.
exprt & distance()
Struct constructor from list of elements.
Definition std_expr.h:1877
Structure type, corresponds to C style structs.
Definition std_types.h:231
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
Semantic type conversion.
Definition std_expr.h:2073
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:391
The vector type.
Definition std_types.h:1064
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, message_handlert &message_handler)
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:778
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:845
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:790
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.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, 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:1900
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1665
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:2053
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:2010
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1116
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
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 complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1158
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
dstringt irep_idt