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/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 <optional>
#include <queue>

Include dependency graph for struct_encoding.cpp:

Go to the source code of this file.

Functions
static std::optional< 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. More...
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. More...
static exprt	encode (const with_exprt &with, const namespacet &ns)
static exprt	empty_encoding ()
	Empty structs and unions are encoded as a zero byte. More...
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. More...
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 162 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 129 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 137 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 147 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 std::optional<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.