cprover
Loading...
Searching...
No Matches
value_set_dereference.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution of ANSI-C
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
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/c_types.h>
21#include <util/config.h>
22#include <util/cprover_prefix.h>
23#include <util/expr_iterator.h>
24#include <util/expr_util.h>
25#include <util/format_expr.h>
26#include <util/fresh_symbol.h>
27#include <util/json.h>
28#include <util/message.h>
29#include <util/namespace.h>
30#include <util/pointer_expr.h>
33#include <util/range.h>
34#include <util/simplify_expr.h>
35#include <util/symbol.h>
36
38
39#include <deque>
40
51static bool should_use_local_definition_for(const exprt &expr)
52{
53 bool seen_symbol = false;
54 for(auto it = expr.depth_begin(), itend = expr.depth_end(); it != itend; ++it)
55 {
56 if(it->id() == ID_symbol)
57 {
58 if(seen_symbol)
59 return true;
60 else
61 seen_symbol = true;
62 }
63 }
64
65 return false;
66}
67
69 const exprt &pointer,
70 const std::vector<exprt> &points_to_set,
71 const std::vector<exprt> &retained_values,
72 const exprt &value)
73{
74 json_objectt json_result;
75 json_result["Pointer"] = json_stringt{format_to_string(pointer)};
76 json_result["PointsToSetSize"] =
77 json_numbert{std::to_string(points_to_set.size())};
78
79 json_arrayt points_to_set_json;
80 for(const auto &object : points_to_set)
81 {
82 points_to_set_json.push_back(json_stringt{format_to_string(object)});
83 }
84
85 json_result["PointsToSet"] = points_to_set_json;
86
87 json_result["RetainedValuesSetSize"] =
88 json_numbert{std::to_string(points_to_set.size())};
89
90 json_arrayt retained_values_set_json;
91 for(auto &retained_value : retained_values)
92 {
93 retained_values_set_json.push_back(
94 json_stringt{format_to_string(retained_value)});
95 }
96
97 json_result["RetainedValuesSet"] = retained_values_set_json;
98
99 json_result["Value"] = json_stringt{format_to_string(value)};
100
101 return json_result;
102}
103
107static std::optional<exprt>
108try_add_offset_to_indices(const exprt &expr, const exprt &offset_elements)
109{
110 if(const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr))
111 {
112 return index_exprt{
113 index_expr->array(),
114 plus_exprt{index_expr->index(),
116 offset_elements, index_expr->index().type())}};
117 }
118 else if(const auto *if_expr = expr_try_dynamic_cast<if_exprt>(expr))
119 {
120 const auto true_case =
121 try_add_offset_to_indices(if_expr->true_case(), offset_elements);
122 if(!true_case)
123 return {};
124 const auto false_case =
125 try_add_offset_to_indices(if_expr->false_case(), offset_elements);
126 if(!false_case)
127 return {};
128 return if_exprt{if_expr->cond(), *true_case, *false_case};
129 }
130 else if(can_cast_expr<typecast_exprt>(expr))
131 {
132 // the case of a type cast is _not_ handled here, because that would require
133 // doing arithmetic on the offset, and may result in an offset into some
134 // sub-element
135 return {};
136 }
137 else
138 {
139 return {};
140 }
141}
142
144 const exprt &pointer,
145 bool display_points_to_sets)
146{
148 pointer.type().id() == ID_pointer,
149 "dereference expected pointer type, but got " + pointer.type().pretty());
150
151 // we may get ifs due to recursive calls
152 if(pointer.id()==ID_if)
153 {
154 const if_exprt &if_expr=to_if_expr(pointer);
155 exprt true_case = dereference(if_expr.true_case(), display_points_to_sets);
156 exprt false_case =
157 dereference(if_expr.false_case(), display_points_to_sets);
158 return if_exprt(if_expr.cond(), true_case, false_case);
159 }
160 else if(pointer.id() == ID_typecast)
161 {
162 const exprt *underlying = &pointer;
163 // Note this isn't quite the same as skip_typecast, which would also skip
164 // things such as int-to-ptr typecasts which we shouldn't ignore
165 while(underlying->id() == ID_typecast &&
166 underlying->type().id() == ID_pointer)
167 {
168 underlying = &to_typecast_expr(*underlying).op();
169 }
170
171 if(underlying->id() == ID_if && underlying->type().id() == ID_pointer)
172 {
173 const auto &if_expr = to_if_expr(*underlying);
174 return if_exprt(
175 if_expr.cond(),
177 typecast_exprt(if_expr.true_case(), pointer.type()),
178 display_points_to_sets),
180 typecast_exprt(if_expr.false_case(), pointer.type()),
181 display_points_to_sets));
182 }
183 }
184 else if(pointer.id() == ID_plus && pointer.operands().size() == 2)
185 {
186 // Try to improve results for *(p + i) where p points to known offsets but
187 // i is non-constant-- if `p` points to known positions in arrays or array-members
188 // of structs then we can add the non-constant expression `i` to the index
189 // instead of using a byte-extract expression.
190
191 exprt pointer_expr = to_plus_expr(pointer).op0();
192 exprt offset_expr = to_plus_expr(pointer).op1();
193
194 if(can_cast_type<pointer_typet>(offset_expr.type()))
195 std::swap(pointer_expr, offset_expr);
196
197 if(
198 can_cast_type<pointer_typet>(pointer_expr.type()) &&
199 !can_cast_type<pointer_typet>(offset_expr.type()) &&
200 !can_cast_expr<constant_exprt>(offset_expr))
201 {
202 exprt derefd_pointer = dereference(pointer_expr);
203 if(
204 auto derefd_with_offset =
205 try_add_offset_to_indices(derefd_pointer, offset_expr))
206 return *derefd_with_offset;
207
208 // If any of this fails, fall through to use the normal byte-extract path.
209 }
210 }
211
212 return handle_dereference_base_case(pointer, display_points_to_sets);
213}
214
216 const exprt &pointer,
217 bool display_points_to_sets)
218{ // type of the object
219 const typet &type = to_pointer_type(pointer.type()).base_type();
220
221 // collect objects the pointer may point to
222 const std::vector<exprt> points_to_set =
224
225 // get the values of these
226 const std::vector<exprt> retained_values =
227 make_range(points_to_set).filter([&](const exprt &value) {
229 });
230
231 exprt compare_against_pointer = pointer;
232
233 if(retained_values.size() >= 2 && should_use_local_definition_for(pointer))
234 {
235 symbolt fresh_binder = get_fresh_aux_symbol(
236 pointer.type(),
237 "derefd_pointer",
238 "derefd_pointer",
239 pointer.find_source_location(),
242
243 compare_against_pointer = fresh_binder.symbol_expr();
244 }
245
246 auto values =
247 make_range(retained_values)
248 .map([&](const exprt &value) {
249 return build_reference_to(value, compare_against_pointer, ns);
250 })
251 .collect<std::deque<valuet>>();
252
253 const bool may_fail =
254 values.empty() ||
255 std::any_of(values.begin(), values.end(), [](const valuet &value) {
256 return value.value.is_nil();
257 });
258
259 if(may_fail)
260 {
261 values.push_front(get_failure_value(pointer, type));
262 }
263
264 // now build big case split, but we only do "good" objects
265
266 exprt result_value = nil_exprt{};
267
268 for(const auto &value : values)
269 {
270 if(value.value.is_not_nil())
271 {
272 if(result_value.is_nil()) // first?
273 result_value = value.value;
274 else
275 result_value = if_exprt(value.pointer_guard, value.value, result_value);
276 }
277 }
278
279 if(compare_against_pointer != pointer)
280 result_value =
281 let_exprt(to_symbol_expr(compare_against_pointer), pointer, result_value);
282
283 if(display_points_to_sets)
284 {
287 pointer, points_to_set, retained_values, result_value);
288 }
289
290 return result_value;
291}
292
294 const exprt &pointer,
295 const typet &type)
296{
297 // first see if we have a "failed object" for this pointer
298 exprt failure_value;
299
300 if(
301 const symbolt *failed_symbol =
303 {
304 // yes!
305 failure_value = failed_symbol->symbol_expr();
306 failure_value.set(ID_C_invalid_object, true);
307 }
308 else
309 {
310 // else: produce new symbol
312 type,
313 "symex",
314 "invalid_object",
315 pointer.source_location(),
318
319 // make it a lvalue, so we can assign to it
320 symbol.is_lvalue = true;
321
322 failure_value = symbol.symbol_expr();
323 failure_value.set(ID_C_invalid_object, true);
324 }
325
326 valuet result{};
327 result.value = failure_value;
328 result.pointer_guard = true_exprt();
329 return result;
330}
331
341 const typet &object_type,
342 const typet &dereference_type,
343 const namespacet &ns)
344{
345 const typet *object_unwrapped = &object_type;
346 const typet *dereference_unwrapped = &dereference_type;
347 while(object_unwrapped->id() == ID_pointer &&
348 dereference_unwrapped->id() == ID_pointer)
349 {
350 object_unwrapped = &to_pointer_type(*object_unwrapped).base_type();
351 dereference_unwrapped =
352 &to_pointer_type(*dereference_unwrapped).base_type();
353 }
354 if(dereference_unwrapped->id() == ID_empty)
355 {
356 return true;
357 }
358 else if(dereference_unwrapped->id() == ID_pointer &&
359 object_unwrapped->id() != ID_pointer)
360 {
361#ifdef DEBUG
362 std::cout << "value_set_dereference: the dereference type has "
363 "too many ID_pointer levels"
364 << std::endl;
365 std::cout << " object_type: " << object_type.pretty() << std::endl;
366 std::cout << " dereference_type: " << dereference_type.pretty()
367 << std::endl;
368#endif
369 }
370
371 if(object_type == dereference_type)
372 return true; // ok, they just match
373
374 // check for struct prefixes
375 const typet &ot_base = object_type.id() == ID_struct_tag
376 ? ns.follow_tag(to_struct_tag_type(object_type))
377 : object_type;
378 const typet &dt_base = dereference_type.id() == ID_struct_tag
379 ? ns.follow_tag(to_struct_tag_type(dereference_type))
380 : dereference_type;
381
382 if(ot_base.id()==ID_struct &&
383 dt_base.id()==ID_struct)
384 {
385 if(to_struct_type(dt_base).is_prefix_of(
386 to_struct_type(ot_base)))
387 return true; // ok, dt is a prefix of ot
388 }
389
390 // we are generous about code pointers
391 if(dereference_type.id()==ID_code &&
392 object_type.id()==ID_code)
393 return true;
394
395 // bitvectors of same width are ok
396 if((dereference_type.id()==ID_signedbv ||
397 dereference_type.id()==ID_unsignedbv) &&
398 (object_type.id()==ID_signedbv ||
399 object_type.id()==ID_unsignedbv) &&
400 to_bitvector_type(dereference_type).get_width()==
401 to_bitvector_type(object_type).get_width())
402 return true;
403
404 // really different
405
406 return false;
407}
408
423 const exprt &what,
424 bool exclude_null_derefs,
425 const irep_idt &language_mode)
426{
427 if(what.id() == ID_unknown || what.id() == ID_invalid)
428 {
429 return false;
430 }
431
433
434 const exprt &root_object = o.root_object();
435 if(root_object.id() == ID_null_object)
436 {
437 return exclude_null_derefs;
438 }
439 else if(root_object.id() == ID_integer_address)
440 {
441 return language_mode == ID_java;
442 }
443
444 return false;
445}
446
460 const exprt &what,
461 const exprt &pointer_expr,
462 const namespacet &ns)
463{
466 const typet &dereference_type = pointer_type.base_type();
467
468 if(what.id()==ID_unknown ||
469 what.id()==ID_invalid)
470 {
471 return valuet();
472 }
473
475 what.id() == ID_object_descriptor,
476 "unknown points-to: " + what.id_string());
477
479
480 const exprt &root_object=o.root_object();
481 const exprt &object=o.object();
482
483 #if 0
484 std::cout << "O: " << format(root_object) << '\n';
485 #endif
486
487 if(root_object.id() == ID_null_object)
488 {
489 if(!o.offset().is_zero())
490 return {};
491
492 valuet result;
494 return result;
495 }
496 else if(root_object.id()==ID_dynamic_object)
497 {
498 valuet result;
499
500 // constraint that it actually is a dynamic object
501 // this is also our guard
502 result.pointer_guard = is_dynamic_object_exprt(pointer_expr);
503
504 // can't remove here, turn into *p
505 result.value = dereference_exprt{pointer_expr};
506 result.pointer = pointer_expr;
507
508 return result;
509 }
510 else if(root_object.id()==ID_integer_address)
511 {
512 // This is stuff like *((char *)5).
513 // This is turned into an access to __CPROVER_memory[...].
514
515 const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");
516 const symbol_exprt symbol_expr(memory_symbol.name, memory_symbol.type);
517
518 if(to_array_type(memory_symbol.type).element_type() == dereference_type)
519 {
520 // Types match already, what a coincidence!
521 // We can use an index expression.
522
523 const index_exprt index_expr(
524 symbol_expr,
526 pointer_offset(pointer_expr),
527 to_array_type(memory_symbol.type).index_type()),
528 to_array_type(memory_symbol.type).element_type());
529
530 valuet result;
531 result.value=index_expr;
532 result.pointer = address_of_exprt{index_expr};
533 return result;
534 }
536 to_array_type(memory_symbol.type).element_type(),
537 dereference_type,
538 ns))
539 {
540 const index_exprt index_expr(
541 symbol_expr,
543 pointer_offset(pointer_expr),
544 to_array_type(memory_symbol.type).index_type()),
545 to_array_type(memory_symbol.type).element_type());
546
547 valuet result;
548 result.value=typecast_exprt(index_expr, dereference_type);
549 result.pointer =
551 return result;
552 }
553 else
554 {
555 // We need to use byte_extract.
556 // Won't do this without a commitment to an endianness.
557
559 return {};
560
561 valuet result;
562 result.value = make_byte_extract(
563 symbol_expr, pointer_offset(pointer_expr), dereference_type);
564 result.pointer = address_of_exprt{result.value};
565 return result;
566 }
567 }
568 else
569 {
570 valuet result;
571
572 // something generic -- really has to be a symbol
573 address_of_exprt object_pointer(object);
574
575 if(o.offset().is_zero())
576 {
577 result.pointer_guard = equal_exprt(
578 typecast_exprt::conditional_cast(pointer_expr, object_pointer.type()),
579 object_pointer);
580 }
581 else
582 {
583 result.pointer_guard=same_object(pointer_expr, object_pointer);
584 }
585
586 const typet &object_type = object.type();
587 const typet &root_object_type = root_object.type();
588
589 if(
590 dereference_type_compare(object_type, dereference_type, ns) &&
591 o.offset().is_zero())
592 {
593 // The simplest case: types match, and offset is zero!
594 // This is great, we are almost done.
595
596 result.value = typecast_exprt::conditional_cast(object, dereference_type);
597 result.pointer =
599
600 return result;
601 }
602
603 // this is relative to the root object
604 exprt offset;
605 if(o.offset().is_constant())
606 offset = o.offset();
607 else
608 offset = simplify_expr(pointer_offset(pointer_expr), ns);
609
610 if(
611 root_object_type.id() == ID_array &&
613 to_array_type(root_object_type).element_type(), dereference_type, ns) &&
614 pointer_offset_bits(to_array_type(root_object_type).element_type(), ns) ==
615 pointer_offset_bits(dereference_type, ns) &&
616 offset.is_constant())
617 {
618 // We have an array with a subtype that matches
619 // the dereferencing type.
620
621 // are we doing a byte?
622 auto element_size =
623 pointer_offset_size(to_array_type(root_object_type).element_type(), ns);
624 CHECK_RETURN(element_size.has_value());
625 CHECK_RETURN(*element_size > 0);
626
627 const auto offset_int =
629
630 if(offset_int % *element_size == 0)
631 {
632 index_exprt index_expr{
633 root_object,
635 offset_int / *element_size,
636 to_array_type(root_object_type).index_type())};
637 result.value =
638 typecast_exprt::conditional_cast(index_expr, dereference_type);
640 address_of_exprt{index_expr}, pointer_type);
641
642 return result;
643 }
644 }
645
646 // try to build a member/index expression - do not use byte_extract
647 auto subexpr = get_subexpression_at_offset(
648 root_object, o.offset(), dereference_type, ns);
649 if(subexpr.has_value())
650 simplify(subexpr.value(), ns);
651 if(
652 subexpr.has_value() &&
653 subexpr.value().id() != ID_byte_extract_little_endian &&
654 subexpr.value().id() != ID_byte_extract_big_endian)
655 {
656 // Successfully found a member, array index, or combination thereof
657 // that matches the desired type and offset:
658 result.value = subexpr.value();
660 address_of_exprt{skip_typecast(subexpr.value())}, pointer_type);
661 return result;
662 }
663
664 // we extract something from the root object
665 result.value = o.root_object();
668
669 if(memory_model(result.value, dereference_type, offset, ns))
670 {
671 // set pointer correctly
675 result.pointer,
677 offset),
679 }
680 else
681 {
682 return {}; // give up, no way that this is ok
683 }
684
685 return result;
686 }
687}
688
689static bool is_a_bv_type(const typet &type)
690{
691 return type.id()==ID_unsignedbv ||
692 type.id()==ID_signedbv ||
693 type.id()==ID_bv ||
694 type.id()==ID_fixedbv ||
695 type.id()==ID_floatbv ||
696 type.id()==ID_c_enum_tag;
697}
698
708 exprt &value,
709 const typet &to_type,
710 const exprt &offset,
711 const namespacet &ns)
712{
713 // we will allow more or less arbitrary pointer type cast
714
715 const typet from_type=value.type();
716
717 // first, check if it's really just a type coercion,
718 // i.e., both have exactly the same (constant) size,
719 // for bit-vector types or pointers
720
721 if(
722 (is_a_bv_type(from_type) && is_a_bv_type(to_type)) ||
723 (from_type.id() == ID_pointer && to_type.id() == ID_pointer))
724 {
726 {
727 // avoid semantic conversion in case of
728 // cast to float or fixed-point,
729 // or cast from float or fixed-point
730
731 if(
732 to_type.id() != ID_fixedbv && to_type.id() != ID_floatbv &&
733 from_type.id() != ID_fixedbv && from_type.id() != ID_floatbv)
734 {
735 value = typecast_exprt::conditional_cast(value, to_type);
736 return true;
737 }
738 }
739 }
740
741 // otherwise, we will stitch it together from bytes
742
743 return memory_model_bytes(value, to_type, offset, ns);
744}
745
755 exprt &value,
756 const typet &to_type,
757 const exprt &offset,
758 const namespacet &ns)
759{
760 const typet from_type=value.type();
761
762 // We simply refuse to convert to/from code.
763 if(from_type.id()==ID_code || to_type.id()==ID_code)
764 return false;
765
766 // We won't do this without a commitment to an endianness.
768 return false;
769
770 // But everything else we will try!
771 // We just rely on byte_extract to do the job!
772
773 exprt result;
774
775 // See if we have an array of bytes already,
776 // and we want something byte-sized.
777 auto from_type_element_type_size =
778 from_type.id() == ID_array
780 : std::optional<mp_integer>{};
781
782 auto to_type_size = pointer_offset_size(to_type, ns);
783
784 if(
785 from_type.id() == ID_array && from_type_element_type_size.has_value() &&
786 *from_type_element_type_size == 1 && to_type_size.has_value() &&
787 *to_type_size == 1 &&
788 is_a_bv_type(to_array_type(from_type).element_type()) &&
789 is_a_bv_type(to_type))
790 {
791 // yes, can use 'index', but possibly need to convert
794 value,
796 offset, to_array_type(from_type).index_type()),
797 to_array_type(from_type).element_type()),
798 to_type);
799 }
800 else
801 {
802 // no, use 'byte_extract'
803 result = make_byte_extract(value, offset, to_type);
804 }
805
806 value=result;
807
808 return true;
809}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
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.
Expression classes for byte-level operators.
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
bitvector_typet char_type()
Definition c_types.cpp:106
Operator to return the address of an object.
typet index_type() const
The type of the index expressions into any instance of this type.
Definition std_types.cpp:34
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:827
std::size_t get_width() const
Definition std_types.h:925
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
depth_iteratort depth_end()
Definition expr.cpp:249
depth_iteratort depth_begin()
Definition expr.cpp:247
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
The trinary if-then-else operator.
Definition std_expr.h:2375
exprt & cond()
Definition std_expr.h:2392
exprt & false_case()
Definition std_expr.h:2412
exprt & true_case()
Definition std_expr.h:2402
Array index operator.
Definition std_expr.h:1470
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
bool is_not_nil() const
Definition irep.h:372
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
Evaluates to true if the operand is a pointer to a dynamic object.
jsont & push_back(const jsont &json)
Definition json.h:212
A let expression.
Definition std_expr.h:3209
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & status() const
Definition message.h:406
exprt & op1()
Definition std_expr.h:938
exprt & op0()
Definition std_expr.h:932
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:3086
The null pointer constant.
Split an expression into a base object and a (byte) offset.
static const exprt & root_object(const exprt &expr)
The plus expression Associativity is not specified.
Definition std_expr.h:1002
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
Expression to hold a symbol (variable)
Definition std_expr.h:131
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:72
The Boolean constant true.
Definition std_expr.h:3068
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:391
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...
symbol_table_baset & new_symbol_table
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...
message_handlert & message_handler
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)
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...
#define CPROVER_PREFIX
Pointer Dereferencing.
auto type_checked_cast(TType &base) -> typename detail::expr_dynamic_cast_return_typet< T, TType >::type
Cast a reference to a generic typet to a specific derived class and checks that the type could be con...
Definition expr_cast.h:242
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
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
Deprecated expression utility functions.
static format_containert< T > format(const T &o)
Definition format.h:37
std::string format_to_string(const T &o)
Definition format.h:43
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)
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.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
std::optional< 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)
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:522
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition std_expr.h:2091
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1041
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition std_expr.h:3034
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2455
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3050
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
endiannesst endianness
Definition config.h:209
Symbol table entry.
static std::optional< exprt > try_add_offset_to_indices(const exprt &expr, const exprt &offset_elements)
If expr is of the form (c1 ? e1[o1] : c2 ? e2[o2] : c3 ? ...) then return c1 ? e1[o1 + offset] : e2[o...
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.