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 =
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 
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.element_type(), 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.element_type(), 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.element_type(), 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(
431  object.id() == ID_string_constant || object.id() == ID_label ||
432  object.id() == ID_array || object.id() == ID_null_object ||
433  object.id() == ID_symbol)
434  {
435  // constant, nothing to do
436  return;
437  }
438  else if(object.id()==ID_dereference)
439  {
441  }
442  else if(object.id()==ID_index)
443  {
444  const index_exprt &index=to_index_expr(object);
445 
448  }
449  else if(object.id()==ID_member)
450  {
451  const member_exprt &member=to_member_expr(object);
452 
454  }
455  else if(object.id()==ID_if)
456  {
457  const if_exprt &if_expr=to_if_expr(object);
458 
462  }
463  else if(object.id()==ID_byte_extract_little_endian ||
464  object.id()==ID_byte_extract_big_endian)
465  {
466  const byte_extract_exprt &be=to_byte_extract_expr(object);
467 
469  }
470  else if(object.id()==ID_typecast)
471  {
472  const typecast_exprt &tc=to_typecast_expr(object);
473 
475  }
476  else
477  throw "rw_range_sett: address_of '" + object.id_string() + "' not handled";
478 }
479 
481  get_modet mode,
482  const irep_idt &identifier,
483  const range_spect &range_start,
484  const range_spect &range_end)
485 {
486  objectst::iterator entry=
488  .insert(
489  std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
490  identifier, nullptr))
491  .first;
492 
493  if(entry->second==nullptr)
494  entry->second=util_make_unique<range_domaint>();
495 
496  static_cast<range_domaint&>(*entry->second).push_back(
497  {range_start, range_end});
498 }
499 
501  get_modet mode,
502  const exprt &expr,
503  const range_spect &range_start,
504  const range_spect &size)
505 {
506  if(expr.id() == ID_complex_real)
508  mode, to_complex_real_expr(expr), range_start, size);
509  else if(expr.id() == ID_complex_imag)
511  mode, to_complex_imag_expr(expr), range_start, size);
512  else if(expr.id()==ID_typecast)
514  mode,
515  to_typecast_expr(expr),
516  range_start,
517  size);
518  else if(expr.id()==ID_if)
519  get_objects_if(mode, to_if_expr(expr), range_start, size);
520  else if(expr.id()==ID_dereference)
522  mode,
523  to_dereference_expr(expr),
524  range_start,
525  size);
526  else if(expr.id()==ID_byte_extract_little_endian ||
527  expr.id()==ID_byte_extract_big_endian)
529  mode,
530  to_byte_extract_expr(expr),
531  range_start,
532  size);
533  else if(expr.id()==ID_shl ||
534  expr.id()==ID_ashr ||
535  expr.id()==ID_lshr)
536  get_objects_shift(mode, to_shift_expr(expr), range_start, size);
537  else if(expr.id()==ID_member)
538  get_objects_member(mode, to_member_expr(expr), range_start, size);
539  else if(expr.id()==ID_index)
540  get_objects_index(mode, to_index_expr(expr), range_start, size);
541  else if(expr.id()==ID_array)
542  get_objects_array(mode, to_array_expr(expr), range_start, size);
543  else if(expr.id()==ID_struct)
544  get_objects_struct(mode, to_struct_expr(expr), range_start, size);
545  else if(expr.id()==ID_symbol)
546  {
547  const symbol_exprt &symbol=to_symbol_expr(expr);
548  const irep_idt identifier=symbol.get_identifier();
549 
550  auto symbol_bits = pointer_offset_bits(symbol.type(), ns);
551 
552  range_spect full_size =
553  symbol_bits.has_value() ? to_range_spect(*symbol_bits) : -1;
554 
555  if(full_size==0 ||
556  (full_size>0 && range_start>=full_size))
557  {
558  // nothing to do, these are effectively constants (like function
559  // symbols or structs with no members)
560  // OR: invalid memory accesses
561  }
562  else if(range_start>=0)
563  {
564  range_spect range_end=size==-1 ? -1 : range_start+size;
565  if(size!=-1 && full_size!=-1)
566  range_end=std::min(range_end, full_size);
567 
568  add(mode, identifier, range_start, range_end);
569  }
570  else
571  add(mode, identifier, 0, -1);
572  }
573  else if(mode==get_modet::READ && expr.id()==ID_address_of)
575  else if(mode==get_modet::READ)
576  {
577  // possibly affects the full object size, even if range_start/size
578  // are only a subset of the bytes (e.g., when using the result of
579  // arithmetic operations)
580  forall_operands(it, expr)
581  get_objects_rec(mode, *it);
582  }
583  else if(expr.id() == ID_null_object ||
584  expr.id() == ID_string_constant)
585  {
586  // dereferencing may yield some weird ones, ignore these
587  }
588  else if(mode==get_modet::LHS_W)
589  {
590  forall_operands(it, expr)
591  get_objects_rec(mode, *it);
592  }
593  else
594  throw "rw_range_sett: assignment to '" + expr.id_string() + "' not handled";
595 }
596 
598 {
599  auto expr_bits = pointer_offset_bits(expr.type(), ns);
600 
601  range_spect size = expr_bits.has_value() ? to_range_spect(*expr_bits) : -1;
602 
603  get_objects_rec(mode, expr, 0, size);
604 }
605 
607 {
608  // TODO should recurse into various composite types
609  if(type.id()==ID_array)
610  {
611  const auto &array_type = to_array_type(type);
612  get_objects_rec(array_type.element_type());
613  get_objects_rec(get_modet::READ, array_type.size());
614  }
615 }
616 
618  get_modet mode,
619  const dereference_exprt &deref,
620  const range_spect &range_start,
621  const range_spect &size)
622 {
624  mode,
625  deref,
626  range_start,
627  size);
628 
629  exprt object=deref;
630  dereference(function, target, object, ns, value_sets);
631 
632  auto type_bits = pointer_offset_bits(object.type(), ns);
633 
634  range_spect new_size;
635 
636  if(type_bits.has_value())
637  {
638  new_size = to_range_spect(*type_bits);
639 
640  if(range_start == -1 || new_size <= range_start)
641  new_size = -1;
642  else
643  {
644  new_size -= range_start;
645  new_size = std::min(size, new_size);
646  }
647  }
648  else
649  new_size = -1;
650 
651  // value_set_dereferencet::build_reference_to will turn *p into
652  // DYNAMIC_OBJECT(p) ? *p : invalid_objectN
653  if(object.is_not_nil() && !has_subexpr(object, ID_dereference))
654  get_objects_rec(mode, object, range_start, new_size);
655 }
656 
658  const namespacet &ns, std::ostream &out) const
659 {
660  out << "[";
661  for(const_iterator itr=begin();
662  itr!=end();
663  ++itr)
664  {
665  if(itr!=begin())
666  out << ";";
667  out << itr->first << ":" << itr->second.first;
668  // we don't know what mode (language) we are in, so we rely on the default
669  // language to be reasonable for from_expr
670  out << " if " << from_expr(ns, irep_idt(), itr->second.second);
671  }
672  out << "]";
673 }
674 
676  get_modet mode,
677  const if_exprt &if_expr,
678  const range_spect &range_start,
679  const range_spect &size)
680 {
681  if(if_expr.cond().is_false())
682  get_objects_rec(mode, if_expr.false_case(), range_start, size);
683  else if(if_expr.cond().is_true())
684  get_objects_rec(mode, if_expr.true_case(), range_start, size);
685  else
686  {
688 
689  guardt copy = guard;
690 
691  guard.add(not_exprt(if_expr.cond()));
692  get_objects_rec(mode, if_expr.false_case(), range_start, size);
693  guard = copy;
694 
695  guard.add(if_expr.cond());
696  get_objects_rec(mode, if_expr.true_case(), range_start, size);
697  guard = std::move(copy);
698  }
699 }
700 
702  get_modet mode,
703  const irep_idt &identifier,
704  const range_spect &range_start,
705  const range_spect &range_end)
706 {
707  objectst::iterator entry=
709  .insert(
710  std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
711  identifier, nullptr))
712  .first;
713 
714  if(entry->second==nullptr)
715  entry->second=util_make_unique<guarded_range_domaint>();
716 
717  static_cast<guarded_range_domaint&>(*entry->second).insert(
718  {range_start, {range_end, guard.as_expr()}});
719 }
720 
721 static void goto_rw_assign(
722  const irep_idt &function,
724  const exprt &lhs,
725  const exprt &rhs,
726  rw_range_sett &rw_set)
727 {
728  rw_set.get_objects_rec(
729  function, target, rw_range_sett::get_modet::LHS_W, lhs);
730  rw_set.get_objects_rec(function, target, rw_range_sett::get_modet::READ, rhs);
731 }
732 
733 static void goto_rw(
734  const irep_idt &function,
736  const exprt &lhs,
737  const exprt &function_expr,
738  const exprt::operandst &arguments,
739  rw_range_sett &rw_set)
740 {
741  if(lhs.is_not_nil())
742  rw_set.get_objects_rec(
743  function, target, rw_range_sett::get_modet::LHS_W, lhs);
744 
745  rw_set.get_objects_rec(
746  function, target, rw_range_sett::get_modet::READ, function_expr);
747 
748  for(const auto &argument : arguments)
749  {
750  rw_set.get_objects_rec(
751  function, target, rw_range_sett::get_modet::READ, argument);
752  }
753 }
754 
755 void goto_rw(
756  const irep_idt &function,
758  rw_range_sett &rw_set)
759 {
760  switch(target->type())
761  {
762  case NO_INSTRUCTION_TYPE:
763  case INCOMPLETE_GOTO:
764  UNREACHABLE;
765  break;
766 
767  case GOTO:
768  case ASSUME:
769  case ASSERT:
770  rw_set.get_objects_rec(
771  function,
772  target,
774  target->get_condition());
775  break;
776 
777  case SET_RETURN_VALUE:
778  rw_set.get_objects_rec(
779  function, target, rw_range_sett::get_modet::READ, target->return_value());
780  break;
781 
782  case OTHER:
783  // if it's printf, mark the operands as read here
784  if(target->get_other().get_statement() == ID_printf)
785  {
786  for(const auto &op : target->get_other().operands())
787  rw_set.get_objects_rec(
788  function, target, rw_range_sett::get_modet::READ, op);
789  }
790  break;
791 
792  case SKIP:
793  case START_THREAD:
794  case END_THREAD:
795  case LOCATION:
796  case END_FUNCTION:
797  case ATOMIC_BEGIN:
798  case ATOMIC_END:
799  case THROW:
800  case CATCH:
801  // these don't read or write anything
802  break;
803 
804  case ASSIGN:
806  function, target, target->assign_lhs(), target->assign_rhs(), rw_set);
807  break;
808 
809  case DEAD:
810  rw_set.get_objects_rec(
811  function, target, rw_range_sett::get_modet::LHS_W, target->dead_symbol());
812  break;
813 
814  case DECL:
815  rw_set.get_objects_rec(function, target, target->decl_symbol().type());
816  rw_set.get_objects_rec(
817  function, target, rw_range_sett::get_modet::LHS_W, target->decl_symbol());
818  break;
819 
820  case FUNCTION_CALL:
821  goto_rw(
822  function,
823  target,
824  target->call_lhs(),
825  target->call_function(),
826  target->call_arguments(),
827  rw_set);
828  break;
829  }
830 }
831 
832 void goto_rw(
833  const irep_idt &function,
834  const goto_programt &goto_program,
835  rw_range_sett &rw_set)
836 {
837  forall_goto_program_instructions(i_it, goto_program)
838  goto_rw(function, i_it, rw_set);
839 }
840 
841 void goto_rw(const goto_functionst &goto_functions,
842  const irep_idt &function,
843  rw_range_sett &rw_set)
844 {
845  goto_functionst::function_mapt::const_iterator f_it=
846  goto_functions.function_map.find(function);
847 
848  if(f_it!=goto_functions.function_map.end())
849  {
850  const goto_programt &body=f_it->second.body;
851 
852  goto_rw(f_it->first, body, rw_set);
853  }
854 }
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:361
Array constructor from list of elements.
Definition: std_expr.h:1476
const array_typet & type() const
Definition: std_expr.h:1483
Arrays with given size.
Definition: std_types.h:763
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
Expression of type type extracted from some object op starting at position offset (given in number of...
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1874
Real part of the expression describing a complex number.
Definition: std_expr.h:1829
Operator to dereference a pointer.
Definition: pointer_expr.h:648
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:73
instructionst::const_iterator const_targett
Definition: goto_program.h:593
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:657
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:2226
exprt & true_case()
Definition: std_expr.h:2253
exprt & false_case()
Definition: std_expr.h:2263
exprt & cond()
Definition: std_expr.h:2243
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1353
exprt & index()
Definition: std_expr.h:1363
const std::string & id_string() const
Definition: irep.h:399
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & struct_op() const
Definition: std_expr.h:2697
irep_idt get_component_name() const
Definition: std_expr.h:2681
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:2181
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:675
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:701
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:617
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:133
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:172
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
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
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:114
virtual void get_objects_address_of(const exprt &object)
Definition: goto_rw.cpp:428
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:145
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:218
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:480
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
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
A base class for shift and rotate operators.
exprt & distance()
exprt & op()
Struct constructor from list of elements.
Definition: std_expr.h:1722
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
const typet & subtype() const
Definition: type.h:156
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
The vector type.
Definition: std_types.h:996
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1006
#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:138
Deprecated expression utility functions.
Goto Programs with Functions.
#define forall_goto_program_instructions(it, program)
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ LOCATION
Definition: goto_program.h:41
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
@ ASSUME
Definition: goto_program.h:35
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
static void goto_rw_assign(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &rhs, rw_range_sett &rw_set)
Definition: goto_rw.cpp:721
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
Definition: goto_rw.cpp:733
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:704
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
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:2291
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:1506
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1855
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1745
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1900
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040
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:832
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1082