CBMC
goto_rw.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening
6 
7 Date: 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 
25 #include <langapi/language_util.h>
27 
28 #include <memory>
29 
31 {
32 }
33 
34 void range_domaint::output(const namespacet &, std::ostream &out) const
35 {
36  out << "[";
37  for(const_iterator itr=begin();
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 
61 void 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,
85  const range_spect &range_start,
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,
94  const range_spect &range_start,
95  const range_spect &size)
96 {
97  const exprt &op = expr.op();
98 
99  auto subtype_bits =
101  CHECK_RETURN(subtype_bits.has_value());
102 
103  range_spect sub_size = range_spect::to_range_spect(*subtype_bits);
104  CHECK_RETURN(sub_size > range_spect{0});
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,
116  const range_spect &range_start,
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,
134  const dereference_exprt &deref,
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,
147  const range_spect &range_start,
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 
153  auto index = numeric_cast<mp_integer>(simp_offset);
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(),
168  be.id()==ID_byte_extract_little_endian,
169  ns);
170  range_spect offset = range_start;
171  if(*index > 0)
172  {
173  offset += range_spect::to_range_spect(
174  map.map_bit(numeric_cast_v<std::size_t>(*index)));
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,
189  const range_spect &range_start,
190  const range_spect &size)
191 {
192  const exprt simp_distance=simplify_expr(shift.distance(), ns);
193 
194  auto op_bits = pointer_offset_bits(shift.op().type(), ns);
195 
196  range_spect src_size = op_bits.has_value()
197  ? range_spect::to_range_spect(*op_bits)
199 
200  const auto dist = numeric_cast<mp_integer>(simp_distance);
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  {
212  const range_spect dist_r = range_spect::to_range_spect(*dist);
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  {
220  range_spect sh_range_start=range_start;
221  sh_range_start+=dist_r;
222 
223  range_spect sh_size=std::min(size, src_size-sh_range_start);
224 
225  if(sh_range_start >= range_spect{0} && sh_range_start < src_size)
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,
240  const range_spect &range_start,
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)
256 
257  auto offset_bits =
258  member_offset_bits(struct_type, expr.get_component_name(), ns);
259 
261 
262  if(offset_bits.has_value())
263  {
264  offset = range_spect::to_range_spect(*offset_bits);
265  offset += range_start;
266  }
267 
268  get_objects_rec(mode, expr.struct_op(), offset, size);
269 }
270 
272  get_modet mode,
273  const index_exprt &expr,
274  const range_spect &range_start,
275  const range_spect &size)
276 {
277  if(expr.array().id() == ID_null_object)
278  return;
279 
280  range_spect sub_size = range_spect::unknown();
281  const typet &type = expr.array().type();
282 
283  if(type.id()==ID_vector)
284  {
285  const vector_typet &vector_type=to_vector_type(type);
286 
287  auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
288 
289  if(subtype_bits.has_value())
290  sub_size = range_spect::to_range_spect(*subtype_bits);
291  }
292  else if(type.id()==ID_array)
293  {
294  const array_typet &array_type=to_array_type(type);
295 
296  auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
297 
298  if(subtype_bits.has_value())
299  sub_size = range_spect::to_range_spect(*subtype_bits);
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(),
317  range_start + range_spect::to_range_spect(*index) * sub_size,
318  size);
319  }
320 }
321 
323  get_modet mode,
324  const array_exprt &expr,
325  const range_spect &range_start,
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 
340  range_spect sub_size = range_spect::to_range_spect(*subtype_bits);
341 
342  range_spect offset{0};
343  range_spect full_r_s =
344  range_start.is_unknown() ? range_spect{0} : range_start;
345  range_spect full_r_e =
346  size.is_unknown()
347  ? sub_size * range_spect::to_range_spect(expr.operands().size())
348  : full_r_s + size;
349 
350  for(const auto &op : expr.operands())
351  {
352  if(full_r_s<=offset+sub_size && full_r_e>offset)
353  {
354  range_spect cur_r_s =
355  full_r_s <= offset ? range_spect{0} : full_r_s - offset;
356  range_spect cur_r_e=
357  full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
358 
359  get_objects_rec(mode, op, cur_r_s, cur_r_e - cur_r_s);
360  }
361 
362  offset+=sub_size;
363  }
364 }
365 
367  get_modet mode,
368  const struct_exprt &expr,
369  const range_spect &range_start,
370  const range_spect &size)
371 {
372  const struct_typet &struct_type =
373  expr.type().id() == ID_struct
374  ? to_struct_type(expr.type())
376 
377  auto struct_bits = pointer_offset_bits(struct_type, ns);
378 
379  range_spect full_size = struct_bits.has_value()
380  ? range_spect::to_range_spect(*struct_bits)
382 
383  range_spect offset = range_spect{0};
384  range_spect full_r_s =
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()
395  ? range_spect::to_range_spect(*it_bits)
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  {
406  range_spect cur_r_s =
407  full_r_s <= offset ? range_spect{0} : full_r_s - offset;
408 
409  get_objects_rec(mode, op, cur_r_s, range_spect::unknown());
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  {
418  range_spect cur_r_s =
419  full_r_s <= offset ? range_spect{0} : full_r_s - offset;
420 
421  get_objects_rec(mode, op, cur_r_s, sub_size - cur_r_s);
422  }
423 
424  offset+=sub_size;
425  }
426  else if(full_r_s<=offset+sub_size && full_r_e>offset)
427  {
428  range_spect cur_r_s =
429  full_r_s <= offset ? range_spect{0} : full_r_s - offset;
430  range_spect cur_r_e=
431  full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
432 
433  get_objects_rec(mode, op, cur_r_s, cur_r_e - cur_r_s);
434 
435  offset+=sub_size;
436  }
437  }
438 }
439 
441  get_modet mode,
442  const typecast_exprt &tc,
443  const range_spect &range_start,
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()
451  ? range_spect::to_range_spect(*op_bits)
453 
454  if(range_start.is_unknown())
455  new_size = range_spect::unknown();
456  else if(!new_size.is_unknown())
457  {
458  if(new_size<=range_start)
459  return;
460 
461  new_size-=range_start;
462  new_size=std::min(size, new_size);
463  }
464 
465  get_objects_rec(mode, op, range_start, new_size);
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  {
506  const byte_extract_exprt &be=to_byte_extract_expr(object);
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,
523  const range_spect &range_start,
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(
537  {range_start, range_end});
538 }
539 
541  get_modet mode,
542  const exprt &expr,
543  const range_spect &range_start,
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),
556  range_start,
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,
563  to_dereference_expr(expr),
564  range_start,
565  size);
566  else if(expr.id()==ID_byte_extract_little_endian ||
567  expr.id()==ID_byte_extract_big_endian)
569  mode,
570  to_byte_extract_expr(expr),
571  range_start,
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)
578  get_objects_member(mode, to_member_expr(expr), range_start, size);
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)
584  get_objects_struct(mode, to_struct_expr(expr), range_start, size);
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()
593  ? range_spect::to_range_spect(*symbol_bits)
595 
596  if(
597  !full_size.is_unknown() &&
598  (full_size == range_spect{0} ||
599  (full_size > range_spect{0} && !range_start.is_unknown() &&
600  range_start >= full_size)))
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  {
608  range_spect range_end =
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()
647  ? range_spect::to_range_spect(*expr_bits)
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());
660  get_objects_rec(get_modet::READ, array_type.size());
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);
674 }
675 
677  get_modet mode,
678  const dereference_exprt &deref,
679  const range_spect &range_start,
680  const range_spect &size)
681 {
683  mode,
684  deref,
685  range_start,
686  size);
687 
688  exprt object=deref;
689  dereference(function, target, object, ns, value_sets, message_handler);
690 
691  auto type_bits = pointer_offset_bits(object.type(), ns);
692 
693  range_spect new_size = range_spect::unknown();
694 
695  if(type_bits.has_value())
696  {
697  new_size = range_spect::to_range_spect(*type_bits);
698 
699  if(range_start.is_unknown() || new_size <= range_start)
700  new_size = range_spect::unknown();
701  else
702  {
703  new_size -= range_start;
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 << "[";
718  for(const_iterator itr=begin();
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,
735  const range_spect &range_start,
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,
761  const range_spect &range_start,
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(
775  {range_start, {range_end, guard.as_expr()}});
776 }
777 
778 static void goto_rw_assign(
779  const irep_idt &function,
781  const exprt &lhs,
782  const exprt &rhs,
783  rw_range_sett &rw_set)
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 
790 static void goto_rw_other(
791  const irep_idt &function,
793  const codet &code,
794  rw_range_sett &rw_set)
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 
845 static void goto_rw(
846  const irep_idt &function,
848  const exprt &lhs,
849  const exprt &function_expr,
850  const exprt::operandst &arguments,
851  rw_range_sett &rw_set)
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(
858  function, target, rw_range_sett::get_modet::READ, function_expr);
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 
867 void goto_rw(
868  const irep_idt &function,
870  rw_range_sett &rw_set)
871 {
872  switch(target->type())
873  {
874  case NO_INSTRUCTION_TYPE:
875  case INCOMPLETE_GOTO:
876  UNREACHABLE;
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 
935 void goto_rw(
936  const irep_idt &function,
937  const goto_programt &goto_program,
938  rw_range_sett &rw_set)
939 {
940  forall_goto_program_instructions(i_it, goto_program)
941  goto_rw(function, i_it, rw_set);
942 }
943 
944 void goto_rw(const goto_functionst &goto_functions,
945  const irep_idt &function,
946  rw_range_sett &rw_set)
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.
Definition: pointer_expr.h:540
exprt & object()
Definition: pointer_expr.h:549
Array constructor from list of elements.
Definition: std_expr.h:1616
const array_typet & type() const
Definition: std_expr.h:1623
Arrays with given size.
Definition: std_types.h:807
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:827
const exprt & size() const
Definition: std_types.h:840
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.
Definition: std_code_base.h:29
exprt & op1()
Definition: expr.h:136
exprt & op2()
Definition: expr.h:139
exprt & op0()
Definition: expr.h:133
const irep_idt & get_statement() const
Definition: std_code_base.h:65
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:2022
Real part of the expression describing a complex number.
Definition: std_expr.h:1979
Operator to dereference a pointer.
Definition: pointer_expr.h:834
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
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.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:615
void add(const exprt &expr)
Definition: guard_expr.cpp:38
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
iterator end()
Definition: goto_rw.h:441
iterator begin()
Definition: goto_rw.h:437
The trinary if-then-else operator.
Definition: std_expr.h:2370
exprt & true_case()
Definition: std_expr.h:2397
exprt & false_case()
Definition: std_expr.h:2407
exprt & cond()
Definition: std_expr.h:2387
Array index operator.
Definition: std_expr.h:1465
exprt & array()
Definition: std_expr.h:1495
exprt & index()
Definition: std_expr.h:1505
const std::string & id_string() const
Definition: irep.h:391
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
Extract member of struct or union.
Definition: std_expr.h:2844
const exprt & struct_op() const
Definition: std_expr.h:2882
irep_idt get_component_name() const
Definition: std_expr.h:2866
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Boolean negation.
Definition: std_expr.h:2327
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:181
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: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_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size) override
Definition: goto_rw.cpp:732
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
Definition: goto_rw.h:234
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
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
Definition: goto_rw.h:234
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_r_set() const
Definition: goto_rw.h:215
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
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
const objectst & get_w_set() const
Definition: goto_rw.h:220
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()
exprt & op()
Struct constructor from list of elements.
Definition: std_expr.h:1872
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
const typet & subtype() const
Definition: type.h:187
Semantic type conversion.
Definition: std_expr.h:2068
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:1061
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1077
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:193
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:115
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, 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 dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:890
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
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 if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2450
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1660
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2102
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:2005
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1895
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2936
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:2048
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1113
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1155
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
dstringt irep_idt