51 bool seen_symbol =
false;
54 if(it->id() == ID_symbol)
68 const std::vector<exprt> &points_to_set,
69 const std::vector<exprt> &retained_values,
74 json_result[
"PointsToSetSize"] =
78 for(
const auto &
object : points_to_set)
83 json_result[
"PointsToSet"] = points_to_set_json;
85 json_result[
"RetainedValuesSetSize"] =
89 for(
auto &retained_value : retained_values)
95 json_result[
"RetainedValuesSet"] = retained_values_set_json;
104 const exprt &offset_elements)
106 if(
const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr))
112 offset_elements, index_expr->index().
type())}};
114 else if(
const auto *if_expr = expr_try_dynamic_cast<if_exprt>(expr))
116 const auto true_case =
120 const auto false_case =
124 return if_exprt{if_expr->
cond(), *true_case, *false_case};
133 const exprt &pointer,
134 bool display_points_to_sets)
136 if(pointer.
type().
id()!=ID_pointer)
137 throw "dereference expected pointer type, but got "+
141 if(pointer.
id()==ID_if)
149 else if(pointer.
id() == ID_typecast)
151 const exprt *underlying = &pointer;
154 while(underlying->
id() == ID_typecast &&
155 underlying->
type().
id() == ID_pointer)
160 if(underlying->
id() == ID_if && underlying->
type().
id() == ID_pointer)
162 const auto &if_expr =
to_if_expr(*underlying);
167 display_points_to_sets),
170 display_points_to_sets));
173 else if(pointer.
id() == ID_plus && pointer.
operands().size() == 2)
184 std::swap(pointer_expr, offset_expr);
193 auto derefd_with_offset =
195 return *derefd_with_offset;
205 const exprt &pointer,
206 bool display_points_to_sets)
211 const std::vector<exprt> points_to_set =
215 const std::vector<exprt> retained_values =
220 exprt compare_against_pointer = pointer;
232 compare_against_pointer = fresh_binder.
symbol_expr();
237 .map([&](
const exprt &value) {
240 .collect<std::deque<valuet>>();
242 const bool may_fail =
244 std::any_of(values.begin(), values.end(), [](
const valuet &value) {
245 return value.value.is_nil();
257 for(
const auto &value : values)
262 result_value = value.value;
264 result_value =
if_exprt(value.pointer_guard, value.value, result_value);
268 if(compare_against_pointer != pointer)
272 if(display_points_to_sets)
275 pointer, points_to_set, retained_values, result_value);
282 const exprt &pointer,
293 failure_value = failed_symbol->symbol_expr();
294 failure_value.
set(ID_C_invalid_object,
true);
311 failure_value.
set(ID_C_invalid_object,
true);
315 result.
value = failure_value;
329 const typet &object_type,
330 const typet &dereference_type,
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)
338 object_unwrapped = &object_unwrapped->
subtype();
339 dereference_unwrapped = &dereference_unwrapped->
subtype();
341 if(dereference_unwrapped->
id() == ID_empty)
345 else if(dereference_unwrapped->
id() == ID_pointer &&
346 object_unwrapped->
id() != ID_pointer)
349 std::cout <<
"value_set_dereference: the dereference type has "
350 "too many ID_pointer levels"
352 std::cout <<
" object_type: " << object_type.
pretty() << std::endl;
353 std::cout <<
" dereference_type: " << dereference_type.
pretty()
358 if(object_type == dereference_type)
364 dt_base=
ns.
follow(dereference_type);
366 if(ot_base.
id()==ID_struct &&
367 dt_base.id()==ID_struct)
375 if(dereference_type.
id()==ID_code &&
376 object_type.
id()==ID_code)
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) &&
408 bool exclude_null_derefs,
411 if(what.
id() == ID_unknown || what.
id() == ID_invalid)
419 if(root_object.
id() == ID_null_object)
423 else if(root_object.
id() == ID_integer_address)
445 const exprt &pointer_expr,
449 type_checked_cast<pointer_typet>(pointer_expr.
type());
452 if(what.
id()==ID_unknown ||
453 what.
id()==ID_invalid)
458 if(what.
id()!=ID_object_descriptor)
459 throw "unknown points-to: "+what.
id_string();
467 std::cout <<
"O: " <<
format(root_object) <<
'\n';
472 if(root_object.
id() == ID_null_object)
479 else if(root_object.
id()==ID_dynamic_object)
489 else if(root_object.
id()==ID_integer_address)
497 if(memory_symbol.
type.
subtype() == dereference_type)
507 result.
value=index_expr;
554 const typet &object_type =
object.type();
555 const typet &root_object_type = root_object.
type();
557 exprt root_object_subexpression=root_object;
571 root_object_type.
id() == ID_array &&
587 exprt adjusted_offset;
593 if(!element_size.has_value() || *element_size == 0)
595 throw "unknown or invalid type size of:\n" +
598 else if(*element_size == 1)
601 adjusted_offset = offset;
608 offset, ID_div, element_size_expr, offset.
type());
626 root_object_subexpression, o.
offset(), dereference_type,
ns);
627 if(subexpr.has_value())
630 subexpr.has_value() &&
631 subexpr.value().id() != ID_byte_extract_little_endian &&
632 subexpr.value().id() != ID_byte_extract_big_endian)
636 result.
value = subexpr.value();
670 return type.
id()==ID_unsignedbv ||
671 type.
id()==ID_signedbv ||
673 type.
id()==ID_fixedbv ||
674 type.
id()==ID_floatbv ||
675 type.
id()==ID_c_enum_tag;
688 const typet &to_type,
702 (
from_type.id() == ID_pointer && to_type.
id() == ID_pointer))
711 to_type.
id() != ID_fixedbv && to_type.
id() != ID_floatbv &&
735 const typet &to_type,
742 if(
from_type.id()==ID_code || to_type.
id()==ID_code)
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 &&
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)
Operator to return the address of an object.
const typet & element_type() const
The type of the elements of the array.
A base class for binary expressions.
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.
Base class for all expressions.
depth_iteratort depth_end()
depth_iteratort depth_begin()
bool is_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
The trinary if-then-else operator.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void set(const irep_idt &name, const irep_idt &value)
const std::string & id_string() const
const irep_idt & id() const
jsont & push_back(const jsont &json)
mstreamt & status() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
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.
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)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
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,...
symbol_tablet & new_symbol_table
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...
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.
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
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.
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)
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)
bool simplify(exprt &expr, const namespacet &ns)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
bool can_cast_expr< constant_exprt >(const exprt &base)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_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.
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...