cprover
value_set_dereference.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "value_set_dereference.h"
13 
14 #ifdef DEBUG
15 #include <iostream>
16 #endif
17 
18 #include <util/arith_tools.h>
19 #include <util/array_name.h>
20 #include <util/byte_operators.h>
21 #include <util/c_types.h>
22 #include <util/config.h>
23 #include <util/cprover_prefix.h>
24 #include <util/expr_iterator.h>
25 #include <util/expr_util.h>
26 #include <util/format_expr.h>
27 #include <util/format_type.h>
28 #include <util/fresh_symbol.h>
29 #include <util/json_irep.h>
30 #include <util/options.h>
31 #include <util/pointer_expr.h>
34 #include <util/range.h>
35 #include <util/simplify_expr.h>
36 #include <util/ssa_expr.h>
37 
38 #include <deque>
39 
50 static bool should_use_local_definition_for(const exprt &expr)
51 {
52  bool seen_symbol = false;
53  for(auto it = expr.depth_begin(), itend = expr.depth_end(); it != itend; ++it)
54  {
55  if(it->id() == ID_symbol)
56  {
57  if(seen_symbol)
58  return true;
59  else
60  seen_symbol = true;
61  }
62  }
63 
64  return false;
65 }
66 
68  const exprt &pointer,
69  const std::vector<exprt> &points_to_set,
70  const std::vector<exprt> &retained_values,
71  const exprt &value)
72 {
73  json_objectt json_result;
74  json_result["Pointer"] = json_stringt{format_to_string(pointer)};
75  json_result["PointsToSetSize"] =
76  json_numbert{std::to_string(points_to_set.size())};
77 
78  json_arrayt points_to_set_json;
79  for(const auto &object : points_to_set)
80  {
81  points_to_set_json.push_back(json_stringt{format_to_string(object)});
82  }
83 
84  json_result["PointsToSet"] = points_to_set_json;
85 
86  json_result["RetainedValuesSetSize"] =
87  json_numbert{std::to_string(points_to_set.size())};
88 
89  json_arrayt retained_values_set_json;
90  for(auto &retained_value : retained_values)
91  {
92  retained_values_set_json.push_back(
93  json_stringt{format_to_string(retained_value)});
94  }
95 
96  json_result["RetainedValuesSet"] = retained_values_set_json;
97 
98  json_result["Value"] = json_stringt{format_to_string(value)};
99 
100  return json_result;
101 }
102 
104  const exprt &expr,
105  const exprt &offset_elements)
106 {
107  if(const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr))
108  {
109  return index_exprt{
110  index_expr->array(),
111  plus_exprt{index_expr->index(),
113  offset_elements, index_expr->index().type())}};
114  }
115  else if(const auto *if_expr = expr_try_dynamic_cast<if_exprt>(expr))
116  {
117  const auto true_case =
118  try_add_offset_to_indices(if_expr->true_case(), offset_elements);
119  if(!true_case)
120  return {};
121  const auto false_case =
122  try_add_offset_to_indices(if_expr->false_case(), offset_elements);
123  if(!false_case)
124  return {};
125  return if_exprt{if_expr->cond(), *true_case, *false_case};
126  }
127  else
128  {
129  return {};
130  }
131 }
132 
134  const exprt &pointer,
135  bool display_points_to_sets)
136 {
137  if(pointer.type().id()!=ID_pointer)
138  throw "dereference expected pointer type, but got "+
139  pointer.type().pretty();
140 
141  // we may get ifs due to recursive calls
142  if(pointer.id()==ID_if)
143  {
144  const if_exprt &if_expr=to_if_expr(pointer);
145  exprt true_case = dereference(if_expr.true_case(), display_points_to_sets);
146  exprt false_case =
147  dereference(if_expr.false_case(), display_points_to_sets);
148  return if_exprt(if_expr.cond(), true_case, false_case);
149  }
150  else if(pointer.id() == ID_typecast)
151  {
152  const exprt *underlying = &pointer;
153  // Note this isn't quite the same as skip_typecast, which would also skip
154  // things such as int-to-ptr typecasts which we shouldn't ignore
155  while(underlying->id() == ID_typecast &&
156  underlying->type().id() == ID_pointer)
157  {
158  underlying = &to_typecast_expr(*underlying).op();
159  }
160 
161  if(underlying->id() == ID_if && underlying->type().id() == ID_pointer)
162  {
163  const auto &if_expr = to_if_expr(*underlying);
164  return if_exprt(
165  if_expr.cond(),
166  dereference(
167  typecast_exprt(if_expr.true_case(), pointer.type()),
168  display_points_to_sets),
169  dereference(
170  typecast_exprt(if_expr.false_case(), pointer.type()),
171  display_points_to_sets));
172  }
173  }
174  else if(pointer.id() == ID_plus && pointer.operands().size() == 2)
175  {
176  // Try to improve results for *(p + i) where p points to known offsets but
177  // i is non-constant-- if `p` points to known positions in arrays or array-members
178  // of structs then we can add the non-constant expression `i` to the index
179  // instead of using a byte-extract expression.
180 
181  exprt pointer_expr = to_plus_expr(pointer).op0();
182  exprt offset_expr = to_plus_expr(pointer).op1();
183 
184  if(can_cast_type<pointer_typet>(offset_expr.type()))
185  std::swap(pointer_expr, offset_expr);
186 
187  if(
188  can_cast_type<pointer_typet>(pointer_expr.type()) &&
189  !can_cast_type<pointer_typet>(offset_expr.type()) &&
190  !can_cast_expr<constant_exprt>(offset_expr))
191  {
192  exprt derefd_pointer = dereference(pointer_expr);
193  if(
194  auto derefd_with_offset =
195  try_add_offset_to_indices(derefd_pointer, offset_expr))
196  return *derefd_with_offset;
197 
198  // If any of this fails, fall through to use the normal byte-extract path.
199  }
200  }
201 
202  return handle_dereference_base_case(pointer, display_points_to_sets);
203 }
204 
206  const exprt &pointer,
207  bool display_points_to_sets)
208 { // type of the object
209  const typet &type=pointer.type().subtype();
210 
211  // collect objects the pointer may point to
212  const std::vector<exprt> points_to_set =
214 
215  // get the values of these
216  const std::vector<exprt> retained_values =
217  make_range(points_to_set).filter([&](const exprt &value) {
219  });
220 
221  exprt compare_against_pointer = pointer;
222 
223  if(retained_values.size() >= 2 && should_use_local_definition_for(pointer))
224  {
225  symbolt fresh_binder = get_fresh_aux_symbol(
226  pointer.type(),
227  "derefd_pointer",
228  "derefd_pointer",
232 
233  compare_against_pointer = fresh_binder.symbol_expr();
234  }
235 
236  auto values =
237  make_range(retained_values)
238  .map([&](const exprt &value) {
239  return build_reference_to(value, compare_against_pointer, ns);
240  })
241  .collect<std::deque<valuet>>();
242 
243  const bool may_fail =
244  values.empty() ||
245  std::any_of(values.begin(), values.end(), [](const valuet &value) {
246  return value.value.is_nil();
247  });
248 
249  if(may_fail)
250  {
251  values.push_front(get_failure_value(pointer, type));
252  }
253 
254  // now build big case split, but we only do "good" objects
255 
256  exprt result_value = nil_exprt{};
257 
258  for(const auto &value : values)
259  {
260  if(value.value.is_not_nil())
261  {
262  if(result_value.is_nil()) // first?
263  result_value = value.value;
264  else
265  result_value = if_exprt(value.pointer_guard, value.value, result_value);
266  }
267  }
268 
269  if(compare_against_pointer != pointer)
270  result_value =
271  let_exprt(to_symbol_expr(compare_against_pointer), pointer, result_value);
272 
273  if(display_points_to_sets)
274  {
276  pointer, points_to_set, retained_values, result_value);
277  }
278 
279  return result_value;
280 }
281 
283  const exprt &pointer,
284  const typet &type)
285 {
286  // first see if we have a "failed object" for this pointer
287  exprt failure_value;
288 
289  if(
290  const symbolt *failed_symbol =
292  {
293  // yes!
294  failure_value = failed_symbol->symbol_expr();
295  failure_value.set(ID_C_invalid_object, true);
296  }
297  else
298  {
299  // else: produce new symbol
300  symbolt &symbol = get_fresh_aux_symbol(
301  type,
302  "symex",
303  "invalid_object",
304  pointer.source_location(),
307 
308  // make it a lvalue, so we can assign to it
309  symbol.is_lvalue = true;
310 
311  failure_value = symbol.symbol_expr();
312  failure_value.set(ID_C_invalid_object, true);
313  }
314 
315  valuet result{};
316  result.value = failure_value;
317  result.pointer_guard = true_exprt();
318  return result;
319 }
320 
330  const typet &object_type,
331  const typet &dereference_type,
332  const namespacet &ns)
333 {
334  const typet *object_unwrapped = &object_type;
335  const typet *dereference_unwrapped = &dereference_type;
336  while(object_unwrapped->id() == ID_pointer &&
337  dereference_unwrapped->id() == ID_pointer)
338  {
339  object_unwrapped = &object_unwrapped->subtype();
340  dereference_unwrapped = &dereference_unwrapped->subtype();
341  }
342  if(dereference_unwrapped->id() == ID_empty)
343  {
344  return true;
345  }
346  else if(dereference_unwrapped->id() == ID_pointer &&
347  object_unwrapped->id() != ID_pointer)
348  {
349 #ifdef DEBUG
350  std::cout << "value_set_dereference: the dereference type has "
351  "too many ID_pointer levels"
352  << std::endl;
353  std::cout << " object_type: " << object_type.pretty() << std::endl;
354  std::cout << " dereference_type: " << dereference_type.pretty()
355  << std::endl;
356 #endif
357  }
358 
359  if(object_type == dereference_type)
360  return true; // ok, they just match
361 
362  // check for struct prefixes
363 
364  const typet ot_base=ns.follow(object_type),
365  dt_base=ns.follow(dereference_type);
366 
367  if(ot_base.id()==ID_struct &&
368  dt_base.id()==ID_struct)
369  {
370  if(to_struct_type(dt_base).is_prefix_of(
371  to_struct_type(ot_base)))
372  return true; // ok, dt is a prefix of ot
373  }
374 
375  // we are generous about code pointers
376  if(dereference_type.id()==ID_code &&
377  object_type.id()==ID_code)
378  return true;
379 
380  // bitvectors of same width are ok
381  if((dereference_type.id()==ID_signedbv ||
382  dereference_type.id()==ID_unsignedbv) &&
383  (object_type.id()==ID_signedbv ||
384  object_type.id()==ID_unsignedbv) &&
385  to_bitvector_type(dereference_type).get_width()==
386  to_bitvector_type(object_type).get_width())
387  return true;
388 
389  // really different
390 
391  return false;
392 }
393 
408  const exprt &what,
409  bool exclude_null_derefs,
410  const irep_idt &language_mode)
411 {
412  if(what.id() == ID_unknown || what.id() == ID_invalid)
413  {
414  return false;
415  }
416 
418 
419  const exprt &root_object = o.root_object();
420  if(root_object.id() == ID_null_object)
421  {
422  return exclude_null_derefs;
423  }
424  else if(root_object.id() == ID_integer_address)
425  {
426  return language_mode == ID_java;
427  }
428 
429  return false;
430 }
431 
445  const exprt &what,
446  const exprt &pointer_expr,
447  const namespacet &ns)
448 {
449  const pointer_typet &pointer_type =
450  type_checked_cast<pointer_typet>(pointer_expr.type());
451  const typet &dereference_type = pointer_type.subtype();
452 
453  if(what.id()==ID_unknown ||
454  what.id()==ID_invalid)
455  {
456  return valuet();
457  }
458 
459  if(what.id()!=ID_object_descriptor)
460  throw "unknown points-to: "+what.id_string();
461 
463 
464  const exprt &root_object=o.root_object();
465  const exprt &object=o.object();
466 
467  #if 0
468  std::cout << "O: " << format(root_object) << '\n';
469  #endif
470 
471  valuet result;
472 
473  if(root_object.id() == ID_null_object)
474  {
475  if(o.offset().is_zero())
477  else
478  return valuet{};
479  }
480  else if(root_object.id()==ID_dynamic_object)
481  {
482  // constraint that it actually is a dynamic object
483  // this is also our guard
484  result.pointer_guard = dynamic_object(pointer_expr);
485 
486  // can't remove here, turn into *p
487  result.value = dereference_exprt{pointer_expr};
488  result.pointer = pointer_expr;
489  }
490  else if(root_object.id()==ID_integer_address)
491  {
492  // This is stuff like *((char *)5).
493  // This is turned into an access to __CPROVER_memory[...].
494 
495  const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");
496  const symbol_exprt symbol_expr(memory_symbol.name, memory_symbol.type);
497 
498  if(memory_symbol.type.subtype() == dereference_type)
499  {
500  // Types match already, what a coincidence!
501  // We can use an index expression.
502 
503  const index_exprt index_expr(
504  symbol_expr,
505  pointer_offset(pointer_expr),
506  memory_symbol.type.subtype());
507 
508  result.value=index_expr;
509  result.pointer = address_of_exprt{index_expr};
510  }
511  else if(
513  memory_symbol.type.subtype(), dereference_type, ns))
514  {
515  const index_exprt index_expr(
516  symbol_expr,
517  pointer_offset(pointer_expr),
518  memory_symbol.type.subtype());
519  result.value=typecast_exprt(index_expr, dereference_type);
520  result.pointer =
522  }
523  else
524  {
525  // We need to use byte_extract.
526  // Won't do this without a commitment to an endianness.
527 
529  {
530  }
531  else
532  {
533  result.value = byte_extract_exprt(
534  byte_extract_id(),
535  symbol_expr,
536  pointer_offset(pointer_expr),
537  dereference_type);
538  result.pointer = address_of_exprt{result.value};
539  }
540  }
541  }
542  else
543  {
544  // something generic -- really has to be a symbol
545  address_of_exprt object_pointer(object);
546 
547  if(o.offset().is_zero())
548  {
549  result.pointer_guard = equal_exprt(
550  typecast_exprt::conditional_cast(pointer_expr, object_pointer.type()),
551  object_pointer);
552  }
553  else
554  {
555  result.pointer_guard=same_object(pointer_expr, object_pointer);
556  }
557 
558  const typet &object_type = object.type();
559  const typet &root_object_type = root_object.type();
560 
561  exprt root_object_subexpression=root_object;
562 
563  if(
564  dereference_type_compare(object_type, dereference_type, ns) &&
565  o.offset().is_zero())
566  {
567  // The simplest case: types match, and offset is zero!
568  // This is great, we are almost done.
569 
570  result.value = typecast_exprt::conditional_cast(object, dereference_type);
571  result.pointer =
573  }
574  else if(
575  root_object_type.id() == ID_array &&
577  root_object_type.subtype(), dereference_type, ns))
578  {
579  // We have an array with a subtype that matches
580  // the dereferencing type.
581  // We will require well-alignedness!
582 
583  exprt offset;
584 
585  // this should work as the object is essentially the root object
586  if(o.offset().is_constant())
587  offset=o.offset();
588  else
589  offset=pointer_offset(pointer_expr);
590 
591  exprt adjusted_offset;
592 
593  // are we doing a byte?
594  auto element_size = pointer_offset_size(root_object_type.subtype(), ns);
595 
596  if(!element_size.has_value() || *element_size == 0)
597  {
598  throw "unknown or invalid type size of:\n" +
599  root_object_type.subtype().pretty();
600  }
601  else if(*element_size == 1)
602  {
603  // no need to adjust offset
604  adjusted_offset = offset;
605  }
606  else
607  {
608  exprt element_size_expr = from_integer(*element_size, offset.type());
609 
610  adjusted_offset=binary_exprt(
611  offset, ID_div, element_size_expr, offset.type());
612 
613  // TODO: need to assert well-alignedness
614  }
615 
616  const index_exprt &index_expr =
617  index_exprt(root_object, adjusted_offset, root_object_type.subtype());
618  result.value =
619  typecast_exprt::conditional_cast(index_expr, dereference_type);
621  address_of_exprt{index_expr}, pointer_type);
622  }
623  else
624  {
625  // try to build a member/index expression - do not use byte_extract
626  auto subexpr = get_subexpression_at_offset(
627  root_object_subexpression, o.offset(), dereference_type, ns);
628  if(subexpr.has_value())
629  simplify(subexpr.value(), ns);
630  if(subexpr.has_value() && subexpr.value().id() != byte_extract_id())
631  {
632  // Successfully found a member, array index, or combination thereof
633  // that matches the desired type and offset:
634  result.value = subexpr.value();
636  address_of_exprt{skip_typecast(subexpr.value())}, pointer_type);
637  return result;
638  }
639 
640  // we extract something from the root object
641  result.value=o.root_object();
644 
645  // this is relative to the root object
646  exprt offset;
647  if(o.offset().id()==ID_unknown)
648  offset=pointer_offset(pointer_expr);
649  else
650  offset=o.offset();
651 
652  if(memory_model(result.value, dereference_type, offset, ns))
653  {
654  // ok, done
655  }
656  else
657  {
658  return valuet(); // give up, no way that this is ok
659  }
660  }
661  }
662 
663  return result;
664 }
665 
666 static bool is_a_bv_type(const typet &type)
667 {
668  return type.id()==ID_unsignedbv ||
669  type.id()==ID_signedbv ||
670  type.id()==ID_bv ||
671  type.id()==ID_fixedbv ||
672  type.id()==ID_floatbv ||
673  type.id()==ID_c_enum_tag;
674 }
675 
685  exprt &value,
686  const typet &to_type,
687  const exprt &offset,
688  const namespacet &ns)
689 {
690  // we will allow more or less arbitrary pointer type cast
691 
692  const typet from_type=value.type();
693 
694  // first, check if it's really just a type coercion,
695  // i.e., both have exactly the same (constant) size,
696  // for bit-vector types or pointers
697 
698  if(
699  (is_a_bv_type(from_type) && is_a_bv_type(to_type)) ||
700  (from_type.id() == ID_pointer && to_type.id() == ID_pointer))
701  {
703  {
704  // avoid semantic conversion in case of
705  // cast to float or fixed-point,
706  // or cast from float or fixed-point
707 
708  if(
709  to_type.id() != ID_fixedbv && to_type.id() != ID_floatbv &&
710  from_type.id() != ID_fixedbv && from_type.id() != ID_floatbv)
711  {
712  value = typecast_exprt::conditional_cast(value, to_type);
713  return true;
714  }
715  }
716  }
717 
718  // otherwise, we will stitch it together from bytes
719 
720  return memory_model_bytes(value, to_type, offset, ns);
721 }
722 
732  exprt &value,
733  const typet &to_type,
734  const exprt &offset,
735  const namespacet &ns)
736 {
737  const typet from_type=value.type();
738 
739  // We simply refuse to convert to/from code.
740  if(from_type.id()==ID_code || to_type.id()==ID_code)
741  return false;
742 
743  // We won't do this without a commitment to an endianness.
745  return false;
746 
747  // But everything else we will try!
748  // We just rely on byte_extract to do the job!
749 
750  exprt result;
751 
752  // See if we have an array of bytes already,
753  // and we want something byte-sized.
754  auto from_type_subtype_size = pointer_offset_size(from_type.subtype(), ns);
755 
756  auto to_type_size = pointer_offset_size(to_type, ns);
757 
758  if(
759  from_type.id() == ID_array && from_type_subtype_size.has_value() &&
760  *from_type_subtype_size == 1 && to_type_size.has_value() &&
761  *to_type_size == 1 && is_a_bv_type(from_type.subtype()) &&
762  is_a_bv_type(to_type))
763  {
764  // yes, can use 'index', but possibly need to convert
766  index_exprt(value, offset, from_type.subtype()), to_type);
767  }
768  else
769  {
770  // no, use 'byte_extract'
771  result = byte_extract_exprt(byte_extract_id(), value, offset, to_type);
772  }
773 
774  value=result;
775 
776  return true;
777 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Misc Utilities.
Expression classes for byte-level operators.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
Operator to return the address of an object.
Definition: pointer_expr.h:200
A base class for binary expressions.
Definition: std_expr.h:551
Expression of type type extracted from some object op starting at position offset (given in number of...
struct configt::ansi_ct ansi_c
virtual const symbolt * get_or_create_failed_symbol(const exprt &expr)=0
virtual std::vector< exprt > get_value_set(const exprt &expr) const =0
Operator to dereference a pointer.
Definition: pointer_expr.h:256
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1140
Base class for all expressions.
Definition: expr.h:54
depth_iteratort depth_end()
Definition: expr.cpp:281
depth_iteratort depth_begin()
Definition: expr.cpp:279
const source_locationt & source_location() const
Definition: expr.h:234
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:78
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
operandst & operands()
Definition: expr.h:96
The trinary if-then-else operator.
Definition: std_expr.h:2087
exprt & true_case()
Definition: std_expr.h:2114
exprt & false_case()
Definition: std_expr.h:2124
exprt & cond()
Definition: std_expr.h:2104
Array index operator.
Definition: std_expr.h:1243
exprt & array()
Definition: std_expr.h:1259
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:492
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
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
bool is_nil() const
Definition: irep.h:387
jsont & push_back(const jsont &json)
Definition: json.h:212
A let expression.
Definition: std_expr.h:2816
mstreamt & status() const
Definition: message.h:414
exprt & op1()
Definition: std_expr.h:767
exprt & op0()
Definition: std_expr.h:761
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
The NIL expression.
Definition: std_expr.h:2735
The null pointer constant.
Definition: std_expr.h:2751
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:21
const exprt & root_object() const
The plus expression Associativity is not specified.
Definition: std_expr.h:831
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
Expression to hold a symbol (variable)
Definition: std_expr.h:81
Symbol table entry.
Definition: symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_lvalue
Definition: symbol.h:66
The Boolean constant true.
Definition: std_expr.h:2717
Semantic type conversion.
Definition: std_expr.h:1781
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
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:294
Return value for build_reference_to; see that method for documentation.
static bool memory_model_bytes(exprt &value, const typet &type, const exprt &offset, const namespacet &ns)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
valuet get_failure_value(const exprt &pointer, const typet &type)
exprt handle_dereference_base_case(const exprt &pointer, bool display_points_to_sets)
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
static bool dereference_type_compare(const typet &object_type, const typet &dereference_type, const namespacet &ns)
Check if the two types have matching number of ID_pointer levels, with the dereference type eventuall...
dereference_callbackt & dereference_callback
exprt dereference(const exprt &pointer, bool display_points_to_sets=false)
Dereference the given pointer-expression.
const irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
optionalt< exprt > try_add_offset_to_indices(const exprt &expr, const exprt &offset)
If expr is of the form (c1 ? e1[o1] : c2 ? e2[o2] : c3 ? ...) then return c1 ? e1[o1 + offset] : e2[o...
static bool should_ignore_value(const exprt &what, bool exclude_null_derefs, const irep_idt &language_mode)
Determine whether possible alias what should be ignored when replacing a pointer by its referees.
static bool memory_model(exprt &value, const typet &type, const exprt &offset, const namespacet &ns)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
configt config
Definition: config.cpp:24
#define CPROVER_PREFIX
Forward depth-first search iterators These iterators' copy operations are expensive,...
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:218
Deprecated expression utility functions.
std::string format_to_string(const T &o)
Definition: format.h:43
static format_containert< T > format(const T &o)
Definition: format.h:37
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
nonstd::optional< T > optionalt
Definition: optional.h:35
Options.
API to expression classes for Pointers.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: pointer_expr.h:88
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt dynamic_object(const exprt &pointer)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
bool simplify(exprt &expr, const namespacet &ns)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:2690
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:870
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: std_types.h:1520
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1096
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
endiannesst endianness
Definition: config.h:157
irep_idt byte_extract_id()
static bool is_a_bv_type(const typet &type)
static json_objectt value_set_dereference_stats_to_json(const exprt &pointer, const std::vector< exprt > &points_to_set, const std::vector< exprt > &retained_values, const exprt &value)
static bool should_use_local_definition_for(const exprt &expr)
Returns true if expr is complicated enough that a local definition (using a let expression) is prefer...
Pointer Dereferencing.