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