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