value_set.h File Reference

#include <tuple>
#include <map>
#include <pointer-analysis/value_sets.h>
#include <optional>
#include <set>
#include <irep2/irep2.h>
#include <util/arith/mp_arith.h>
#include <util/symtab/namespace.h>
#include <util/base/numbering.h>
#include <util/expr/type_byte_size.h>
#include <util/persistent_map.h>

Include dependency graph for value_set.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	value_sett
class	value_sett::objectt
	Record for an object reference. More...
class	value_sett::object_map_dt
struct	value_sett::entryt
	Record for a particular value set: stores the identity of the variable that points at this set of objects, and the objects themselves (with associated offset data). More...
class	vsa_not_implemented_exception

Typedefs
typedef hash_numbering< expr2tc, irep2_hash >	object_numberingt
typedef hash_numbering< unsigned, std::hash< unsigned > >	object_number_numberingt

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.

Typedef Documentation

object_number_numberingt

typedef hash_numbering<unsigned, std::hash<unsigned> > object_number_numberingt

object_numberingt

typedef hash_numbering<expr2tc, irep2_hash> object_numberingt

Function Documentation

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.