value_set.cpp File Reference

#include <cassert>
#include <unordered_set>
#include <langapi/language_util.h>
#include <pointer-analysis/value_set.h>
#include <util/arith/arith_tools.h>
#include <util/expr/base_type.h>
#include <util/lang/c_types.h>
#include <util/config/config.h>
#include <util/symtab/context.h>
#include <util/expr/expr_util.h>
#include <util/base/i2string.h>
#include <irep2/irep2.h>
#include <util/message/message.h>
#include <util/message/format.h>
#include <util/base/prefix.h>
#include <util/irep/std_code.h>
#include <util/irep/std_expr.h>
#include <util/expr/type_byte_size.h>

Include dependency graph for value_set.cpp:

Functions
std::optional< std::pair< size_t, size_t > >	match_leading_component (const std::vector< irep_idt > &names, const std::string &rest)
	Code for tracking "value sets" across assignments in ESBMC.
static std::vector< std::string >	offset_paths (const type2tc &type, const BigInt &offset, bool offset_known, const type2tc &target, const namespacet &ns)
static std::vector< std::string >	union_alias_paths (const type2tc &type_in, const std::string &suffix, const type2tc &target, const namespacet &ns)
static bool	is_related_struct (const type2tc &lhs_type, const type2tc &rhs_type, const namespacet &ns)
	is_subclass_of is struct-only – it casts both operands with to_struct_type – and inheritance has no union analogue, so a union pair that is not base_type_eq is simply incompatible.
static bool	type_has_pointer (const type2tc &type, std::unordered_set< const type2t * > &seen)
static bool	type_has_pointer (const type2tc &type)

Function Documentation

is_related_struct()

bool is_related_struct ( const type2tc & lhs_type, const type2tc & rhs_type, const namespacet & ns )

static

is_subclass_of is struct-only – it casts both operands with to_struct_type – and inheritance has no union analogue, so a union pair that is not base_type_eq is simply incompatible.

match_leading_component()

std::optional< std::pair< size_t, size_t > > match_leading_component	(	const std::vector< irep_idt > &	names,
		const std::string &	rest )

Code for tracking "value sets" across assignments in ESBMC.

The values in a value set are /references/ to /objects/, and additional data about the reference itself. You can consider any level 1 renamed variable to be such an object; and a set of them can identify the set of things that a pointer points at.

The way ESBMC uses this is by keeping a mapping of (l1) pointer variables, and the set of data objects that they can point at. This mapping is then updated during the execution of the program, during which the assignments made are interpreted by the code in value_sett: pointer variable assignments are detected, their right hand sides interpreted to determine what objects may be referred to, and the mapping updated to show that the left hand side variable may point at those objects. Phi nodes are handled by merging the mappings of each pointer variable.

As well as keeping track of pointer variables and the set of things they can point at during symbolic execution, a static analysis also uses value_sett to track pointer variable assignments. This is on an even more abstract level, to compute a points-to analysis of all the code under test. That is, the outcome is a set of what all (l0) variables /might/ point at, This is done using exactly the same mapping/interpretation code, as well as logic (elsewhere) for computing a fixedpoint, and some black magic that attempts to statically track dynamically allocated memory.

The only data element stored is a map from l1 variable names (as strings) to a record of what objects are stored. Data objects are numbered, with the mapping for that stored in the thread-local static value_sett::object_numbering. The primary interfaces to the value_sett object itself are the 'assign' method (for interpreting a variable assignment) and the get_value_set method, that takes a variable and returns the set of things it might point at.

offset_paths()

std::vector< std::string > offset_paths ( const type2tc & type, const BigInt & offset, bool offset_known, const type2tc & target, const namespacet & ns )

static

type_has_pointer() [1/2]

bool type_has_pointer ( const type2tc & type )

static

type_has_pointer() [2/2]

bool type_has_pointer ( const type2tc & type, std::unordered_set< const type2t * > & seen )

static

union_alias_paths()

std::vector< std::string > union_alias_paths ( const type2tc & type_in, const std::string & suffix, const type2tc & target, const namespacet & ns )

static