1/*******************************************************************\
3Module: Symbolic Execution of ANSI-C
5Author: Daniel Kroening, kroening@kroening.com
7\*******************************************************************/
107static std::optional<exprt>
120 const auto true_case =
124 const auto false_case =
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
144 const exprt &pointer,
149 "dereference expected pointer type, but got " + pointer.
type().
pretty());
151 // we may get ifs due to recursive calls
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
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.
209 // If any of this fails, fall through to use the normal byte-extract path.
217 const exprt &pointer,
219{
// type of the object
222 // collect objects the pointer may point to
226 // get the values of these
249 .map([&](
const exprt &value) {
252 .collect<std::deque<valuet>>();
256 std::any_of(values.begin(), values.end(), [](
const valuet &value) {
257 return value.value.is_nil();
265 // now build big case split, but we only do "good" objects
269 for(
const auto &value : values)
273 if(result_value.
is_nil())
// first?
274 result_value = value.value;
276 result_value =
if_exprt(value.pointer_guard, value.value, result_value);
295 const exprt &pointer,
298 // first see if we have a "failed object" for this pointer
311 // else: produce new symbol
320 // make it a lvalue, so we can assign to it
342 const typet &object_type,
363 std::cout <<
"value_set_dereference: the dereference type has "
364 "too many ID_pointer levels"
366 std::cout <<
" object_type: " << object_type.
pretty() << std::endl;
373 return true;
// ok, they just match
375 // check for struct prefixes
388 return true;
// ok, dt is a prefix of ot
391 // we are generous about code pointers
396 // bitvectors of same width are ok
425 bool exclude_null_derefs,
462 const exprt &pointer_expr,
477 "unknown points-to: " + what.
id_string());
485 std::cout <<
"O: " <<
format(root_object) <<
'\n';
501 // constraint that it actually is a dynamic object
502 // this is also our guard
505 // can't remove here, turn into *p
513 // This is stuff like *((char *)5).
514 // This is turned into an access to __CPROVER_memory[...].
521 // Types match already, what a coincidence!
522 // We can use an index expression.
556 // We need to use byte_extract.
557 // Won't do this without a commitment to an endianness.
573 // something generic -- really has to be a symbol
587 const typet &object_type =
object.type();
594 // The simplest case: types match, and offset is zero!
595 // This is great, we are almost done.
604 // this is relative to the root object
619 // We have an array with a subtype that matches
620 // the dereferencing type.
622 // are we doing a byte?
647 // try to build a member/index expression - do not use byte_extract
657 // Successfully found a member, array index, or combination thereof
658 // that matches the desired type and offset:
665 // we extract something from the root object
672 // set pointer correctly
683 return {};
// give up, no way that this is ok
710 const typet &to_type,
714 // we will allow more or less arbitrary pointer type cast
718 // first, check if it's really just a type coercion,
719 // i.e., both have exactly the same (constant) size,
720 // for bit-vector types or pointers
728 // avoid semantic conversion in case of
729 // cast to float or fixed-point,
730 // or cast from float or fixed-point
742 // otherwise, we will stitch it together from bytes
757 const typet &to_type,
763 // We simply refuse to convert to/from code.
767 // We won't do this without a commitment to an endianness.
771 // But everything else we will try!
772 // We just rely on byte_extract to do the job!
776 // See if we have an array of bytes already,
777 // and we want something byte-sized.
781 : std::optional<mp_integer>{};
792 // yes, can use 'index', but possibly need to convert
803 // no, use 'byte_extract'
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)
bitvector_typet char_type()
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::size_t get_width() const
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.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
depth_iteratort depth_end()
depth_iteratort depth_begin()
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
const std::string & id_string() const
const irep_idt & id() const
Evaluates to true if the operand is a pointer to a dynamic object.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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.
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
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...
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)
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.
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)
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)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define CHECK_RETURN(CONDITION)
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.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_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 struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
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...