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