struct_encoding.cpp File Reference

#include "struct_encoding.h"
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/bitvector_types.h>
#include <util/c_types.h>
#include <util/make_unique.h>
#include <util/namespace.h>
#include <util/range.h>
#include <util/simplify_expr.h>
#include <solvers/flattening/boolbv_width.h>
#include <solvers/smt2_incremental/encoding/nondet_padding.h>
#include <algorithm>
#include <numeric>
#include <queue>

Include dependency graph for struct_encoding.cpp:

Go to the source code of this file.

Functions
static optionalt< std::size_t >	needs_width (const typet &type, const boolbv_widtht &boolbv_width)
	If the given type needs re-encoding as a bit-vector then this function.
static std::unordered_map< irep_idt, exprt >	extricate_updates (const with_exprt &struct_expr)
	Extracts the component/field names and new values from a with_exprt which expresses a new struct value where one or more members of a struct have had their values substituted with new values.
static exprt	encode (const with_exprt &with, const namespacet &ns)
static exprt	empty_encoding ()
	Empty structs and unions are encoded as a zero byte.
static exprt	encode (const struct_exprt &struct_expr)
	Structs are flattened into a large bit vector using concatenation to express all the member operands of struct_expr.
static exprt	encode (const union_exprt &union_expr, const boolbv_widtht &bit_width)
static std::size_t	count_trailing_bit_width (const struct_typet &type, const irep_idt name, const boolbv_widtht &boolbv_width)

Function Documentation

count_trailing_bit_width()

static std::size_t count_trailing_bit_width ( const struct_typet & type, const irep_idt name, const boolbv_widtht & boolbv_width )

static

Definition at line 163 of file struct_encoding.cpp.

empty_encoding()

static exprt empty_encoding ( )

static

Empty structs and unions are encoded as a zero byte.

This has useful properties such as -

• A zero byte is valid SMT, unlike zero length bit vectors.
• Any two zero byte instances are always equal. This property would not be true of two instances of a non-det byte for instance.

Definition at line 130 of file struct_encoding.cpp.

encode() [1/3]

static exprt encode ( const struct_exprt & struct_expr )

static

Structs are flattened into a large bit vector using concatenation to express all the member operands of struct_expr.

Definition at line 138 of file struct_encoding.cpp.

encode() [2/3]

static exprt encode ( const union_exprt & union_expr, const boolbv_widtht & bit_width )

static

Definition at line 148 of file struct_encoding.cpp.

encode() [3/3]

static exprt encode ( const with_exprt & with, const namespacet & ns )

static

Definition at line 105 of file struct_encoding.cpp.

extricate_updates()

static std::unordered_map< irep_idt, exprt > extricate_updates ( const with_exprt & struct_expr )

static

Extracts the component/field names and new values from a with_exprt which expresses a new struct value where one or more members of a struct have had their values substituted with new values.

Note

This is implemented using direct access to the operands and other underlying irept interfaces, because the interface for with_exprt only supports a single where / new_value pair and does not support extracting the name from the where operand.

Definition at line 82 of file struct_encoding.cpp.

needs_width()

static optionalt< std::size_t > needs_width ( const typet & type, const boolbv_widtht & boolbv_width )

static

If the given type needs re-encoding as a bit-vector then this function.

Returns

the width of the new bitvector type. The width calculation is delegated to boolbv_width.

Definition at line 38 of file struct_encoding.cpp.