Go to the documentation of this file.
52 bool seen_symbol =
false;
55 if(it->id() == ID_symbol)
69 const std::vector<exprt> &points_to_set,
70 const std::vector<exprt> &retained_values,
75 json_result[
"PointsToSetSize"] =
79 for(
const auto &
object : points_to_set)
84 json_result[
"PointsToSet"] = points_to_set_json;
86 json_result[
"RetainedValuesSetSize"] =
90 for(
auto &retained_value : retained_values)
96 json_result[
"RetainedValuesSet"] = retained_values_set_json;
105 const exprt &offset_elements)
107 if(
const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr))
113 offset_elements, index_expr->index().
type())}};
115 else if(
const auto *if_expr = expr_try_dynamic_cast<if_exprt>(expr))
117 const auto true_case =
121 const auto false_case =
125 return if_exprt{if_expr->
cond(), *true_case, *false_case};
134 const exprt &pointer,
135 bool display_points_to_sets)
137 if(pointer.
type().
id()!=ID_pointer)
138 throw "dereference expected pointer type, but got "+
142 if(pointer.
id()==ID_if)
150 else if(pointer.
id() == ID_typecast)
152 const exprt *underlying = &pointer;
155 while(underlying->
id() == ID_typecast &&
156 underlying->
type().
id() == ID_pointer)
161 if(underlying->
id() == ID_if && underlying->
type().
id() == ID_pointer)
163 const auto &if_expr =
to_if_expr(*underlying);
168 display_points_to_sets),
171 display_points_to_sets));
174 else if(pointer.
id() == ID_plus && pointer.
operands().size() == 2)
185 std::swap(pointer_expr, offset_expr);
194 auto derefd_with_offset =
196 return *derefd_with_offset;
206 const exprt &pointer,
207 bool display_points_to_sets)
212 const std::vector<exprt> points_to_set =
216 const std::vector<exprt> retained_values =
221 exprt compare_against_pointer = pointer;
233 compare_against_pointer = fresh_binder.
symbol_expr();
238 .map([&](
const exprt &value) {
241 .collect<std::deque<valuet>>();
243 const bool may_fail =
245 std::any_of(values.begin(), values.end(), [](
const valuet &value) {
246 return value.value.is_nil();
258 for(
const auto &value : values)
263 result_value = value.
value;
269 if(compare_against_pointer != pointer)
273 if(display_points_to_sets)
276 pointer, points_to_set, retained_values, result_value);
283 const exprt &pointer,
294 failure_value = failed_symbol->symbol_expr();
295 failure_value.
set(ID_C_invalid_object,
true);
312 failure_value.
set(ID_C_invalid_object,
true);
316 result.
value = failure_value;
330 const typet &object_type,
331 const typet &dereference_type,
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)
339 object_unwrapped = &object_unwrapped->
subtype();
340 dereference_unwrapped = &dereference_unwrapped->
subtype();
342 if(dereference_unwrapped->
id() == ID_empty)
346 else if(dereference_unwrapped->
id() == ID_pointer &&
347 object_unwrapped->
id() != ID_pointer)
350 std::cout <<
"value_set_dereference: the dereference type has "
351 "too many ID_pointer levels"
353 std::cout <<
" object_type: " << object_type.
pretty() << std::endl;
354 std::cout <<
" dereference_type: " << dereference_type.
pretty()
359 if(object_type == dereference_type)
365 dt_base=
ns.
follow(dereference_type);
367 if(ot_base.
id()==ID_struct &&
368 dt_base.id()==ID_struct)
376 if(dereference_type.
id()==ID_code &&
377 object_type.
id()==ID_code)
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) &&
409 bool exclude_null_derefs,
412 if(what.
id() == ID_unknown || what.
id() == ID_invalid)
420 if(root_object.
id() == ID_null_object)
424 else if(root_object.
id() == ID_integer_address)
446 const exprt &pointer_expr,
450 type_checked_cast<pointer_typet>(pointer_expr.
type());
453 if(what.
id()==ID_unknown ||
454 what.
id()==ID_invalid)
459 if(what.
id()!=ID_object_descriptor)
460 throw "unknown points-to: "+what.
id_string();
468 std::cout <<
"O: " <<
format(root_object) <<
'\n';
473 if(root_object.
id() == ID_null_object)
480 else if(root_object.
id()==ID_dynamic_object)
490 else if(root_object.
id()==ID_integer_address)
498 if(memory_symbol.
type.
subtype() == dereference_type)
508 result.
value=index_expr;
558 const typet &object_type =
object.type();
559 const typet &root_object_type = root_object.
type();
561 exprt root_object_subexpression=root_object;
575 root_object_type.
id() == ID_array &&
577 root_object_type.
subtype(), dereference_type,
ns))
591 exprt adjusted_offset;
596 if(!element_size.has_value() || *element_size == 0)
598 throw "unknown or invalid type size of:\n" +
601 else if(*element_size == 1)
604 adjusted_offset = offset;
611 offset, ID_div, element_size_expr, offset.
type());
627 root_object_subexpression, o.
offset(), dereference_type,
ns);
628 if(subexpr.has_value())
634 result.
value = subexpr.value();
668 return type.
id()==ID_unsignedbv ||
669 type.
id()==ID_signedbv ||
671 type.
id()==ID_fixedbv ||
672 type.
id()==ID_floatbv ||
673 type.
id()==ID_c_enum_tag;
686 const typet &to_type,
700 (
from_type.id() == ID_pointer && to_type.
id() == ID_pointer))
709 to_type.
id() != ID_fixedbv && to_type.
id() != ID_floatbv &&
733 const typet &to_type,
740 if(
from_type.id()==ID_code || to_type.
id()==ID_code)
759 from_type.id() == ID_array && from_type_subtype_size.has_value() &&
760 *from_type_subtype_size == 1 && to_type_size.has_value() &&
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static exprt conditional_cast(const exprt &expr, const typet &type)
const typet & subtype() const
Return value for build_reference_to; see that method for documentation.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
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...
depth_iteratort depth_begin()
The type of an expression, extends irept.
Fresh auxiliary symbol creation.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
mstreamt & status() const
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
typet type
Type of symbol.
Operator to dereference a pointer.
The trinary if-then-else operator.
Various predicates over pointers in programs.
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)
const irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
Split an expression into a base object and a (byte) offset.
The plus expression Associativity is not specified.
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.
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
Base class for all expressions.
valuet get_failure_value(const exprt &pointer, const typet &type)
A base class for binary expressions.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
virtual const symbolt * get_or_create_failed_symbol(const exprt &expr)=0
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
exprt dynamic_object(const exprt &pointer)
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...
struct configt::ansi_ct ansi_c
Expression to hold a symbol (variable)
virtual std::vector< exprt > get_value_set(const exprt &expr) const =0
symbol_tablet & new_symbol_table
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
irep_idt byte_extract_id()
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression classes for byte-level operators.
The null pointer constant.
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...
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
dereference_callbackt & dereference_callback
API to expression classes for Pointers.
const std::string & id_string() const
bool simplify(exprt &expr, const namespacet &ns)
pointer_typet pointer_type(const typet &subtype)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
Ranges: pair of begin and end iterators, which can be initialized from containers,...
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...
const exprt & root_object() const
nonstd::optional< T > optionalt
exprt pointer_offset(const exprt &pointer)
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
bool is_zero() const
Return whether the expression is a constant representing 0.
Deprecated expression utility functions.
static bool is_a_bv_type(const typet &type)
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.
Forward depth-first search iterators These iterators' copy operations are expensive,...
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void set(const irep_namet &name, const irep_idt &value)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
bool is_constant() const
Return whether the expression is a constant.
exprt same_object(const exprt &p1, const exprt &p2)
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...
bool can_cast_expr< constant_exprt >(const exprt &base)
Operator to return the address of an object.
Semantic type conversion.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
The Boolean constant true.
depth_iteratort depth_end()
const source_locationt & source_location() const
ranget< iteratort > make_range(iteratort begin, iteratort end)
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 ...
irep_idt name
The unique identifier.
jsont & push_back(const jsont &json)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
exprt dereference(const exprt &pointer, bool display_points_to_sets=false)
Dereference the given pointer-expression.
exprt handle_dereference_base_case(const exprt &pointer, bool display_points_to_sets)