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