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  auto index = numeric_cast<mp_integer>(simp_offset);
154  if(range_start == -1 || !index.has_value())
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  range_spect offset =
167  range_start + map.map_bit(numeric_cast_v<std::size_t>(*index));
168  get_objects_rec(mode, be.op(), offset, size);
169  }
170 }
171 
173  get_modet mode,
174  const shift_exprt &shift,
175  const range_spect &range_start,
176  const range_spect &size)
177 {
178  const exprt simp_distance=simplify_expr(shift.distance(), ns);
179 
180  auto op_bits = pointer_offset_bits(shift.op().type(), ns);
181 
182  range_spect src_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;
183 
184  const auto dist = numeric_cast<mp_integer>(simp_distance);
185  if(range_start == -1 || size == -1 || src_size == -1 || !dist.has_value())
186  {
187  get_objects_rec(mode, shift.op(), -1, -1);
188  get_objects_rec(mode, shift.distance(), -1, -1);
189  }
190  else
191  {
192  const range_spect dist_r = to_range_spect(*dist);
193 
194  // not sure whether to worry about
195  // config.ansi_c.endianness==configt::ansi_ct::IS_LITTLE_ENDIAN
196  // right here maybe?
197 
198  if(shift.id()==ID_ashr || shift.id()==ID_lshr)
199  {
200  range_spect sh_range_start=range_start;
201  sh_range_start+=dist_r;
202 
203  range_spect sh_size=std::min(size, src_size-sh_range_start);
204 
205  if(sh_range_start>=0 && sh_range_start<src_size)
206  get_objects_rec(mode, shift.op(), sh_range_start, sh_size);
207  }
208  else
209  {
210  assert(src_size-dist_r>=0);
211  range_spect sh_size=std::min(size, src_size-dist_r);
212 
213  get_objects_rec(mode, shift.op(), range_start, sh_size);
214  }
215  }
216 }
217 
219  get_modet mode,
220  const member_exprt &expr,
221  const range_spect &range_start,
222  const range_spect &size)
223 {
224  const typet &type = expr.struct_op().type();
225 
226  if(type.id() == ID_union || type.id() == ID_union_tag || range_start == -1)
227  {
228  get_objects_rec(mode, expr.struct_op(), range_start, size);
229  return;
230  }
231 
232  const struct_typet &struct_type = to_struct_type(ns.follow(type));
233 
234  auto offset_bits =
235  member_offset_bits(struct_type, expr.get_component_name(), ns);
236 
237  range_spect offset;
238 
239  if(offset_bits.has_value())
240  {
241  offset = to_range_spect(*offset_bits);
242  offset += range_start;
243  }
244  else
245  offset = -1;
246 
247  get_objects_rec(mode, expr.struct_op(), offset, size);
248 }
249 
251  get_modet mode,
252  const index_exprt &expr,
253  const range_spect &range_start,
254  const range_spect &size)
255 {
256  if(expr.array().id() == ID_null_object)
257  return;
258 
259  range_spect sub_size=0;
260  const typet &type = expr.array().type();
261 
262  if(type.id()==ID_vector)
263  {
264  const vector_typet &vector_type=to_vector_type(type);
265 
266  auto subtype_bits = pointer_offset_bits(vector_type.subtype(), ns);
267 
268  sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
269  }
270  else if(type.id()==ID_array)
271  {
272  const array_typet &array_type=to_array_type(type);
273 
274  auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);
275 
276  sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
277  }
278  else
279  return;
280 
281  const exprt simp_index=simplify_expr(expr.index(), ns);
282 
283  const auto index = numeric_cast<mp_integer>(simp_index);
284  if(!index.has_value())
286 
287  if(range_start == -1 || sub_size == -1 || !index.has_value())
288  get_objects_rec(mode, expr.array(), -1, size);
289  else
291  mode,
292  expr.array(),
293  range_start + to_range_spect(*index * sub_size),
294  size);
295 }
296 
298  get_modet mode,
299  const array_exprt &expr,
300  const range_spect &range_start,
301  const range_spect &size)
302 {
303  const array_typet &array_type = expr.type();
304 
305  auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);
306 
307  range_spect sub_size;
308 
309  if(subtype_bits.has_value())
310  sub_size = to_range_spect(*subtype_bits);
311  else
312  {
313  forall_operands(it, expr)
314  get_objects_rec(mode, *it, 0, -1);
315 
316  return;
317  }
318 
319  range_spect offset=0;
320  range_spect full_r_s=range_start==-1 ? 0 : range_start;
321  range_spect full_r_e=
322  size==-1 ? sub_size*expr.operands().size() : full_r_s+size;
323 
324  forall_operands(it, expr)
325  {
326  if(full_r_s<=offset+sub_size && full_r_e>offset)
327  {
328  range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
329  range_spect cur_r_e=
330  full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
331 
332  get_objects_rec(mode, *it, cur_r_s, cur_r_e-cur_r_s);
333  }
334 
335  offset+=sub_size;
336  }
337 }
338 
340  get_modet mode,
341  const struct_exprt &expr,
342  const range_spect &range_start,
343  const range_spect &size)
344 {
345  const struct_typet &struct_type=
346  to_struct_type(ns.follow(expr.type()));
347 
348  auto struct_bits = pointer_offset_bits(struct_type, ns);
349 
350  range_spect full_size =
351  struct_bits.has_value() ? to_range_spect(*struct_bits) : -1;
352 
353  range_spect offset=0;
354  range_spect full_r_s=range_start==-1 ? 0 : range_start;
355  range_spect full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size;
356 
357  forall_operands(it, expr)
358  {
359  auto it_bits = pointer_offset_bits(it->type(), ns);
360 
361  range_spect sub_size = it_bits.has_value() ? to_range_spect(*it_bits) : -1;
362 
363  if(offset==-1)
364  {
365  get_objects_rec(mode, *it, 0, sub_size);
366  }
367  else if(sub_size==-1)
368  {
369  if(full_r_e==-1 || full_r_e>offset)
370  {
371  range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
372 
373  get_objects_rec(mode, *it, cur_r_s, -1);
374  }
375 
376  offset=-1;
377  }
378  else if(full_r_e==-1)
379  {
380  if(full_r_s<=offset+sub_size)
381  {
382  range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
383 
384  get_objects_rec(mode, *it, cur_r_s, sub_size-cur_r_s);
385  }
386 
387  offset+=sub_size;
388  }
389  else if(full_r_s<=offset+sub_size && full_r_e>offset)
390  {
391  range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
392  range_spect cur_r_e=
393  full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
394 
395  get_objects_rec(mode, *it, cur_r_s, cur_r_e-cur_r_s);
396 
397  offset+=sub_size;
398  }
399  }
400 }
401 
403  get_modet mode,
404  const typecast_exprt &tc,
405  const range_spect &range_start,
406  const range_spect &size)
407 {
408  const exprt &op=tc.op();
409 
410  auto op_bits = pointer_offset_bits(op.type(), ns);
411 
412  range_spect new_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;
413 
414  if(range_start==-1)
415  new_size=-1;
416  else if(new_size!=-1)
417  {
418  if(new_size<=range_start)
419  return;
420 
421  new_size-=range_start;
422  new_size=std::min(size, new_size);
423  }
424 
425  get_objects_rec(mode, op, range_start, new_size);
426 }
427 
429 {
430  if(object.id() == ID_string_constant ||
431  object.id() == ID_label ||
432  object.id() == ID_array ||
433  object.id() == ID_null_object)
434  {
435  // constant, nothing to do
436  return;
437  }
438  else if(object.id()==ID_symbol)
439  {
441  }
442  else if(object.id()==ID_dereference)
443  {
445  }
446  else if(object.id()==ID_index)
447  {
448  const index_exprt &index=to_index_expr(object);
449 
452  }
453  else if(object.id()==ID_member)
454  {
455  const member_exprt &member=to_member_expr(object);
456 
458  }
459  else if(object.id()==ID_if)
460  {
461  const if_exprt &if_expr=to_if_expr(object);
462 
466  }
467  else if(object.id()==ID_byte_extract_little_endian ||
468  object.id()==ID_byte_extract_big_endian)
469  {
470  const byte_extract_exprt &be=to_byte_extract_expr(object);
471 
473  }
474  else if(object.id()==ID_typecast)
475  {
476  const typecast_exprt &tc=to_typecast_expr(object);
477 
479  }
480  else
481  throw "rw_range_sett: address_of '" + object.id_string() + "' not handled";
482 }
483 
485  get_modet mode,
486  const irep_idt &identifier,
487  const range_spect &range_start,
488  const range_spect &range_end)
489 {
490  objectst::iterator entry=
492  .insert(
493  std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
494  identifier, nullptr))
495  .first;
496 
497  if(entry->second==nullptr)
498  entry->second=util_make_unique<range_domaint>();
499 
500  static_cast<range_domaint&>(*entry->second).push_back(
501  {range_start, range_end});
502 }
503 
505  get_modet mode,
506  const exprt &expr,
507  const range_spect &range_start,
508  const range_spect &size)
509 {
510  if(expr.id() == ID_complex_real)
512  mode, to_complex_real_expr(expr), range_start, size);
513  else if(expr.id() == ID_complex_imag)
515  mode, to_complex_imag_expr(expr), range_start, size);
516  else if(expr.id()==ID_typecast)
518  mode,
519  to_typecast_expr(expr),
520  range_start,
521  size);
522  else if(expr.id()==ID_if)
523  get_objects_if(mode, to_if_expr(expr), range_start, size);
524  else if(expr.id()==ID_dereference)
526  mode,
527  to_dereference_expr(expr),
528  range_start,
529  size);
530  else if(expr.id()==ID_byte_extract_little_endian ||
531  expr.id()==ID_byte_extract_big_endian)
533  mode,
534  to_byte_extract_expr(expr),
535  range_start,
536  size);
537  else if(expr.id()==ID_shl ||
538  expr.id()==ID_ashr ||
539  expr.id()==ID_lshr)
540  get_objects_shift(mode, to_shift_expr(expr), range_start, size);
541  else if(expr.id()==ID_member)
542  get_objects_member(mode, to_member_expr(expr), range_start, size);
543  else if(expr.id()==ID_index)
544  get_objects_index(mode, to_index_expr(expr), range_start, size);
545  else if(expr.id()==ID_array)
546  get_objects_array(mode, to_array_expr(expr), range_start, size);
547  else if(expr.id()==ID_struct)
548  get_objects_struct(mode, to_struct_expr(expr), range_start, size);
549  else if(expr.id()==ID_symbol)
550  {
551  const symbol_exprt &symbol=to_symbol_expr(expr);
552  const irep_idt identifier=symbol.get_identifier();
553 
554  auto symbol_bits = pointer_offset_bits(symbol.type(), ns);
555 
556  range_spect full_size =
557  symbol_bits.has_value() ? to_range_spect(*symbol_bits) : -1;
558 
559  if(full_size==0 ||
560  (full_size>0 && range_start>=full_size))
561  {
562  // nothing to do, these are effectively constants (like function
563  // symbols or structs with no members)
564  // OR: invalid memory accesses
565  }
566  else if(range_start>=0)
567  {
568  range_spect range_end=size==-1 ? -1 : range_start+size;
569  if(size!=-1 && full_size!=-1)
570  range_end=std::min(range_end, full_size);
571 
572  add(mode, identifier, range_start, range_end);
573  }
574  else
575  add(mode, identifier, 0, -1);
576  }
577  else if(mode==get_modet::READ && expr.id()==ID_address_of)
579  else if(mode==get_modet::READ)
580  {
581  // possibly affects the full object size, even if range_start/size
582  // are only a subset of the bytes (e.g., when using the result of
583  // arithmetic operations)
584  forall_operands(it, expr)
585  get_objects_rec(mode, *it);
586  }
587  else if(expr.id() == ID_null_object ||
588  expr.id() == ID_string_constant)
589  {
590  // dereferencing may yield some weird ones, ignore these
591  }
592  else if(mode==get_modet::LHS_W)
593  {
594  forall_operands(it, expr)
595  get_objects_rec(mode, *it);
596  }
597  else
598  throw "rw_range_sett: assignment to '" + expr.id_string() + "' not handled";
599 }
600 
602 {
603  auto expr_bits = pointer_offset_bits(expr.type(), ns);
604 
605  range_spect size = expr_bits.has_value() ? to_range_spect(*expr_bits) : -1;
606 
607  get_objects_rec(mode, expr, 0, size);
608 }
609 
611 {
612  // TODO should recurse into various composite types
613  if(type.id()==ID_array)
614  {
615  const auto &array_type = to_array_type(type);
616  get_objects_rec(array_type.subtype());
617  get_objects_rec(get_modet::READ, array_type.size());
618  }
619 }
620 
622  get_modet mode,
623  const dereference_exprt &deref,
624  const range_spect &range_start,
625  const range_spect &size)
626 {
628  mode,
629  deref,
630  range_start,
631  size);
632 
633  exprt object=deref;
634  dereference(function, target, object, ns, value_sets);
635 
636  auto type_bits = pointer_offset_bits(object.type(), ns);
637 
638  range_spect new_size;
639 
640  if(type_bits.has_value())
641  {
642  new_size = to_range_spect(*type_bits);
643 
644  if(range_start == -1 || new_size <= range_start)
645  new_size = -1;
646  else
647  {
648  new_size -= range_start;
649  new_size = std::min(size, new_size);
650  }
651  }
652  else
653  new_size = -1;
654 
655  // value_set_dereferencet::build_reference_to will turn *p into
656  // DYNAMIC_OBJECT(p) ? *p : invalid_objectN
657  if(object.is_not_nil() && !has_subexpr(object, ID_dereference))
658  get_objects_rec(mode, object, range_start, new_size);
659 }
660 
662  const namespacet &ns, std::ostream &out) const
663 {
664  out << "[";
665  for(const_iterator itr=begin();
666  itr!=end();
667  ++itr)
668  {
669  if(itr!=begin())
670  out << ";";
671  out << itr->first << ":" << itr->second.first;
672  // we don't know what mode (language) we are in, so we rely on the default
673  // language to be reasonable for from_expr
674  out << " if " << from_expr(ns, irep_idt(), itr->second.second);
675  }
676  out << "]";
677 }
678 
680  get_modet mode,
681  const if_exprt &if_expr,
682  const range_spect &range_start,
683  const range_spect &size)
684 {
685  if(if_expr.cond().is_false())
686  get_objects_rec(mode, if_expr.false_case(), range_start, size);
687  else if(if_expr.cond().is_true())
688  get_objects_rec(mode, if_expr.true_case(), range_start, size);
689  else
690  {
692 
693  guardt copy = guard;
694 
695  guard.add(not_exprt(if_expr.cond()));
696  get_objects_rec(mode, if_expr.false_case(), range_start, size);
697  guard = copy;
698 
699  guard.add(if_expr.cond());
700  get_objects_rec(mode, if_expr.true_case(), range_start, size);
701  guard = std::move(copy);
702  }
703 }
704 
706  get_modet mode,
707  const irep_idt &identifier,
708  const range_spect &range_start,
709  const range_spect &range_end)
710 {
711  objectst::iterator entry=
713  .insert(
714  std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
715  identifier, nullptr))
716  .first;
717 
718  if(entry->second==nullptr)
719  entry->second=util_make_unique<guarded_range_domaint>();
720 
721  static_cast<guarded_range_domaint&>(*entry->second).insert(
722  {range_start, {range_end, guard.as_expr()}});
723 }
724 
725 static void goto_rw(
726  const irep_idt &function,
728  const code_assignt &assign,
729  rw_range_sett &rw_set)
730 {
731  rw_set.get_objects_rec(
732  function, target, rw_range_sett::get_modet::LHS_W, assign.lhs());
733  rw_set.get_objects_rec(
734  function, target, rw_range_sett::get_modet::READ, assign.rhs());
735 }
736 
737 static void goto_rw(
738  const irep_idt &function,
740  const code_function_callt &function_call,
741  rw_range_sett &rw_set)
742 {
743  if(function_call.lhs().is_not_nil())
744  rw_set.get_objects_rec(
745  function, target, rw_range_sett::get_modet::LHS_W, function_call.lhs());
746 
747  rw_set.get_objects_rec(
748  function, target, rw_range_sett::get_modet::READ, function_call.function());
749 
750  forall_expr(it, function_call.arguments())
751  rw_set.get_objects_rec(
752  function, target, rw_range_sett::get_modet::READ, *it);
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  {
779  const code_returnt &code_return=
780  to_code_return(target->code);
781  if(code_return.has_return_value())
782  rw_set.get_objects_rec(
783  function,
784  target,
786  code_return.return_value());
787  }
788  break;
789 
790  case OTHER:
791  // if it's printf, mark the operands as read here
792  if(target->get_other().get_statement() == ID_printf)
793  {
794  for(const auto &op : target->get_other().operands())
795  rw_set.get_objects_rec(
796  function, target, rw_range_sett::get_modet::READ, op);
797  }
798  break;
799 
800  case SKIP:
801  case START_THREAD:
802  case END_THREAD:
803  case LOCATION:
804  case END_FUNCTION:
805  case ATOMIC_BEGIN:
806  case ATOMIC_END:
807  case THROW:
808  case CATCH:
809  // these don't read or write anything
810  break;
811 
812  case ASSIGN:
813  goto_rw(function, target, to_code_assign(target->code), rw_set);
814  break;
815 
816  case DEAD:
817  rw_set.get_objects_rec(
818  function,
819  target,
821  to_code_dead(target->code).symbol());
822  break;
823 
824  case DECL:
825  rw_set.get_objects_rec(
826  function, target, to_code_decl(target->code).symbol().type());
827  rw_set.get_objects_rec(
828  function,
829  target,
831  to_code_decl(target->code).symbol());
832  break;
833 
834  case FUNCTION_CALL:
835  goto_rw(function, target, to_code_function_call(target->code), rw_set);
836  break;
837  }
838 }
839 
840 void goto_rw(
841  const irep_idt &function,
842  const goto_programt &goto_program,
843  rw_range_sett &rw_set)
844 {
845  forall_goto_program_instructions(i_it, goto_program)
846  goto_rw(function, i_it, rw_set);
847 }
848 
849 void goto_rw(const goto_functionst &goto_functions,
850  const irep_idt &function,
851  rw_range_sett &rw_set)
852 {
853  goto_functionst::function_mapt::const_iterator f_it=
854  goto_functions.function_map.find(function);
855 
856  if(f_it!=goto_functions.function_map.end())
857  {
858  const goto_programt &body=f_it->second.body;
859 
860  goto_rw(f_it->first, body, rw_set);
861  }
862 }
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_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: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:172
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
guarded_range_domaint::const_iterator
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:329
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:428
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:297
to_array_expr
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1462
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:450
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
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:29
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:133
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:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
rw_guarded_range_set_value_sett::guard
guardt guard
Definition: goto_rw.h:391
guarded_range_domaint::begin
iterator begin()
Definition: goto_rw.h:331
rw_range_sett::get_modet::LHS_W
@ LHS_W
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
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:402
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1740
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:725
exprt
Base class for all expressions.
Definition: expr.h:53
rw_range_sett::~rw_range_sett
virtual ~rw_range_sett()
Definition: goto_rw.cpp:51
irep_idt
dstringt irep_idt
Definition: irep.h:32
vector_typet
The vector type.
Definition: std_types.h:1750
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
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:339
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:82
shift_exprt::op
exprt & op()
Definition: std_expr.h:2505
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
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:147
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:218
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
to_range_spect
range_spect to_range_spect(const mp_integer &size)
Definition: goto_rw.h:67
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
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:1766
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1633
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2543
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:147
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:50
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
array_exprt::type
const array_typet & type() const
Definition: std_expr.h:1439
GOTO
@ GOTO
Definition: goto_program.h:34
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:621
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:147
rw_range_set_value_sett::value_sets
value_setst & value_sets
Definition: goto_rw.h:305
rw_range_sett
Definition: goto_rw.h:113
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:2823
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:3435
guard_exprt::add
void add(const exprt &expr)
Definition: guard_expr.cpp:40
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:519
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:2901
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
endianness_mapt::map_bit
size_t map_bit(size_t bit) const
Definition: endianness_map.h:48
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:705
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:484
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
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
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
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:250
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
range_domain_baset::~range_domain_baset
virtual ~range_domain_baset()
Definition: goto_rw.cpp:33
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
rw_range_set_value_sett::target
goto_programt::const_targett target
Definition: goto_rw.h:307
OTHER
@ OTHER
Definition: goto_program.h:37
code_deadt::symbol
symbol_exprt & symbol()
Definition: std_code.h:473
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1359
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
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:1228
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:1811
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:408
forall_rw_range_set_w_objects
#define forall_rw_range_set_w_objects(it, rw_set)
Definition: goto_rw.h:28
endianness_map.h
simplify_expr.h
RETURN
@ RETURN
Definition: goto_program.h:45
range_spect
int range_spect
Definition: goto_rw.h:65
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:44
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
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:169
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
guarded_range_domaint
Definition: goto_rw.h:319
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
shift_exprt
A base class for shift operators.
Definition: std_expr.h:2496
code_returnt::has_return_value
bool has_return_value() const
Definition: std_code.h:1330
rw_range_sett::ns
const namespacet & ns
Definition: goto_rw.h:167
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
CATCH
@ CATCH
Definition: goto_program.h:51
array_typet
Arrays with given size.
Definition: std_types.h:965
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
DECL
@ DECL
Definition: goto_program.h:47
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
shift_exprt::distance
exprt & distance()
Definition: std_expr.h:2515
guarded_range_domaint::end
iterator end()
Definition: goto_rw.h:335
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:2047
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
goto_program_dereference.h
Value Set.
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1785
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:1011
START_THREAD
@ START_THREAD
Definition: goto_program.h:39
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:32
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:73
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1775
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:3489
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:44
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
DEAD
@ DEAD
Definition: goto_program.h:48
exprt::operands
operandst & operands()
Definition: expr.h:95
guarded_range_domaint::output
virtual void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:661
forall_expr
#define forall_expr(it, expr)
Definition: expr.h:29
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:303
index_exprt
Array index operator.
Definition: std_expr.h:1293
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:43
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1320
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:88
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:679
LOCATION
@ LOCATION
Definition: goto_program.h:41
ASSERT
@ ASSERT
Definition: goto_program.h:36
std_expr.h
API to expression classes.
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1432
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:1218
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
range_domaint::begin
iterator begin()
Definition: goto_rw.h:90
rw_range_sett::get_modet::READ
@ READ
rw_range_sett::get_modet
get_modet
Definition: goto_rw.h:145
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1656
rw_range_sett::r_range_set
objectst r_range_set
Definition: goto_rw.h:169
range_domaint::end
iterator end()
Definition: goto_rw.h:94
range_domaint
Definition: goto_rw.h:78
not_exprt
Boolean negation.
Definition: std_expr.h:2843