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/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
38
49static 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{
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
78 for(const auto &object : points_to_set)
79 {
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
90 {
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 =
118 if(!true_case)
119 return {};
120 const auto false_case =
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,
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 =
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(),
166 typecast_exprt(if_expr.true_case(), pointer.type()),
169 typecast_exprt(if_expr.false_case(), pointer.type()),
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
184 std::swap(pointer_expr, offset_expr);
185
186 if(
187 can_cast_type<pointer_typet>(pointer_expr.type()) &&
190 {
191 exprt derefd_pointer = dereference(pointer_expr);
192 if(
193 auto derefd_with_offset =
195 return *derefd_with_offset;
196
197 // If any of this fails, fall through to use the normal byte-extract path.
198 }
199 }
200
202}
203
205 const exprt &pointer,
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
221
222 if(retained_values.size() >= 2 && should_use_local_definition_for(pointer))
223 {
225 pointer.type(),
226 "derefd_pointer",
227 "derefd_pointer",
231
233 }
234
235 auto values =
237 .map([&](const exprt &value) {
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
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
287
288 if(
289 const symbolt *failed_symbol =
291 {
292 // yes!
293 failure_value = failed_symbol->symbol_expr();
295 }
296 else
297 {
298 // else: produce new 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();
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;
335 while(object_unwrapped->id() == ID_pointer &&
337 {
340 }
342 {
343 return true;
344 }
345 else if(dereference_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),
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(
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 ||
382 (object_type.id()==ID_signedbv ||
383 object_type.id()==ID_unsignedbv) &&
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{
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
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
503 symbol_expr,
504 pointer_offset(pointer_expr),
505 memory_symbol.type.subtype());
506
507 result.value=index_expr;
509 }
510 else if(
512 memory_symbol.type.subtype(), dereference_type, ns))
513 {
515 symbol_expr,
516 pointer_offset(pointer_expr),
517 memory_symbol.type.subtype());
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
542
543 if(o.offset().is_zero())
544 {
545 result.pointer_guard = equal_exprt(
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
558
559 if(
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
567 result.pointer =
569 }
570 else if(
571 root_object_type.id() == ID_array &&
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
588
589 // are we doing a byte?
590 auto element_size =
592
593 if(!element_size.has_value() || *element_size == 0)
594 {
595 throw "unknown or invalid type size of:\n" +
597 }
598 else if(*element_size == 1)
599 {
600 // no need to adjust offset
601 adjusted_offset = offset;
602 }
603 else
604 {
606
608 offset, ID_div, element_size_expr, offset.type());
609
610 // TODO: need to assert well-alignedness
611 }
612
614 root_object,
616 to_array_type(root_object_type).element_type());
617 result.value =
621 }
622 else
623 {
624 // try to build a member/index expression - do not use byte_extract
627 if(subexpr.has_value())
628 simplify(subexpr.value(), ns);
629 if(
630 subexpr.has_value() &&
631 subexpr.value().id() != ID_byte_extract_little_endian &&
632 subexpr.value().id() != ID_byte_extract_big_endian)
633 {
634 // Successfully found a member, array index, or combination thereof
635 // that matches the desired type and offset:
636 result.value = subexpr.value();
639 return result;
640 }
641
642 // we extract something from the root object
643 result.value=o.root_object();
646
647 // this is relative to the root object
648 exprt offset;
649 if(o.offset().id()==ID_unknown)
650 offset=pointer_offset(pointer_expr);
651 else
652 offset=o.offset();
653
654 if(memory_model(result.value, dereference_type, offset, ns))
655 {
656 // ok, done
657 }
658 else
659 {
660 return valuet(); // give up, no way that this is ok
661 }
662 }
663 }
664
665 return result;
666}
667
668static bool is_a_bv_type(const typet &type)
669{
670 return type.id()==ID_unsignedbv ||
671 type.id()==ID_signedbv ||
672 type.id()==ID_bv ||
673 type.id()==ID_fixedbv ||
674 type.id()==ID_floatbv ||
675 type.id()==ID_c_enum_tag;
676}
677
687 exprt &value,
688 const typet &to_type,
689 const exprt &offset,
690 const namespacet &ns)
691{
692 // we will allow more or less arbitrary pointer type cast
693
694 const typet from_type=value.type();
695
696 // first, check if it's really just a type coercion,
697 // i.e., both have exactly the same (constant) size,
698 // for bit-vector types or pointers
699
700 if(
701 (is_a_bv_type(from_type) && is_a_bv_type(to_type)) ||
702 (from_type.id() == ID_pointer && to_type.id() == ID_pointer))
703 {
705 {
706 // avoid semantic conversion in case of
707 // cast to float or fixed-point,
708 // or cast from float or fixed-point
709
710 if(
711 to_type.id() != ID_fixedbv && to_type.id() != ID_floatbv &&
712 from_type.id() != ID_fixedbv && from_type.id() != ID_floatbv)
713 {
714 value = typecast_exprt::conditional_cast(value, to_type);
715 return true;
716 }
717 }
718 }
719
720 // otherwise, we will stitch it together from bytes
721
722 return memory_model_bytes(value, to_type, offset, ns);
723}
724
734 exprt &value,
735 const typet &to_type,
736 const exprt &offset,
737 const namespacet &ns)
738{
739 const typet from_type=value.type();
740
741 // We simply refuse to convert to/from code.
742 if(from_type.id()==ID_code || to_type.id()==ID_code)
743 return false;
744
745 // We won't do this without a commitment to an endianness.
747 return false;
748
749 // But everything else we will try!
750 // We just rely on byte_extract to do the job!
751
752 exprt result;
753
754 // See if we have an array of bytes already,
755 // and we want something byte-sized.
757
758 auto to_type_size = pointer_offset_size(to_type, ns);
759
760 if(
761 from_type.id() == ID_array && from_type_subtype_size.has_value() &&
762 *from_type_subtype_size == 1 && to_type_size.has_value() &&
763 *to_type_size == 1 &&
764 is_a_bv_type(to_array_type(from_type).element_type()) &&
765 is_a_bv_type(to_type))
766 {
767 // yes, can use 'index', but possibly need to convert
769 index_exprt(value, offset, to_array_type(from_type).element_type()),
770 to_type);
771 }
772 else
773 {
774 // no, use 'byte_extract'
775 result = make_byte_extract(value, offset, to_type);
776 }
777
778 value=result;
779
780 return true;
781}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
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:253
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:777
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.
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
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:64
bool is_constant() const
Return whether the expression is a constant.
Definition expr.cpp:26
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
const source_locationt & source_location() const
Definition expr.h:230
The trinary if-then-else operator.
Definition std_expr.h:2226
Array index operator.
Definition std_expr.h:1328
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:495
bool is_not_nil() const
Definition irep.h:380
const std::string & id_string() const
Definition irep.h:399
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
A let expression.
Definition std_expr.h:2973
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().
The NIL expression.
Definition std_expr.h:2874
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:914
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: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
bool is_lvalue
Definition symbol.h:66
The Boolean constant true.
Definition std_expr.h:2856
Semantic type conversion.
Definition std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
The type of an expression, extends irept.
Definition type.h:29
const typet & subtype() const
Definition type.h:48
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
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.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
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< 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_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 typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:953
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 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
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.