smt_bitcast.cpp File Reference

#include <solvers/smt/smt_solver.h>
#include <util/expr/type_byte_size.h>
#include <functional>

Include dependency graph for smt_bitcast.cpp:

Classes
struct	flattened_pointert
	The pointer whose flattened representation is bits [lo, lo + width) of e whenever untouched holds (nil: always), looking through extracts, byte updates that leave those bits alone and the member layout of flatten_to_bitvector. More...

Functions
template<typename Extract>
static expr2tc	concat_tree (size_t start, size_t n, const Extract &extract)
	Constructs the tree-like concatenation of expressions from a sequence.
bool	lowest_address_high ()
	Whether an object's lowest address sits in the most significant bits of its bit-vector encoding: true on a big-endian target, so the bit-vector reads as the object's bytes in memory order, as byte_extract assumes.
unsigned	flattened_position (unsigned offset, unsigned width, unsigned total)
	Lowest bit of the width bits at bit offset offset of a total bit object's bit-vector encoding.
expr2tc	union_member_bits (const expr2tc &bits, unsigned width)
	The width bits of a union member within the union's bits bits: those at the union's lowest address.
expr2tc	union_bits_with_member (const expr2tc &rest, const expr2tc &member, unsigned bits)
	The bits wide bits of a union whose lowest-addressed bits hold member and whose other bits are those of rest.
expr2tc	union_bits_of_member (const expr2tc &member, unsigned bits)
	A union member's bits member widened to the union's bits, as the bits at the union's lowest address; zero-extension is left to the caller.
static size_t	flattened_index (size_t i, size_t n)
static expr2tc	flatten_to_bitvector (const expr2tc &new_expr)
static flattened_pointert	pointer_flattened_at (const expr2tc &e, unsigned lo, unsigned width)
static flattened_pointert	flattened_past_byte_update (const byte_update2t &bu, unsigned lo, unsigned width)
static flattened_pointert	flattened_in_struct (const expr2tc &from, unsigned lo, unsigned width)
static expr2tc	in_memory_order (const expr2tc &bits)
static expr2tc	to_memory_order (const expr2tc &value)
static expr2tc	from_memory_order (const expr2tc &bits, const type2tc &type)
static expr2tc	object_bits (const expr2tc &value)
	The object representation of value, lowest address in the low bits.
static expr2tc	from_object_bits (const expr2tc &bits, const type2tc &type)
	Read an object of type back from its representation bits.
static expr2tc	lanewise_bitcast (const expr2tc &from, const type2tc &to)
static bool	is_vector_bitcast (const type2tc &from, const type2tc &to)

Function Documentation

concat_tree()

template<typename Extract>

expr2tc concat_tree ( size_t start, size_t n, const Extract & extract )

static

Constructs the tree-like concatenation of expressions from a sequence.

Invokes extract for each index in [start,start+n) and concatenates the results to one expression, which is is returned. The expression forms a binary tree of minimal height with the extract(i) expressions at its leaves and concat2t expressions otherwise.

For each valid index i in the above range, extract(i) should return the iths sub-expression to concatenate.

Parameters

start	The initial index to invoke extract for
n	The number of successive elements to extract starting at start; note: n > 0 only
extract	Callback to invoke for each valid index

Returns

An expression corresponding to the concatenation (in order, from start to start+n-1) of the extract results and its size

flatten_to_bitvector()

expr2tc flatten_to_bitvector ( const expr2tc & new_expr )

static

flattened_in_struct()

flattened_pointert flattened_in_struct ( const expr2tc & from, unsigned lo, unsigned width )

static

flattened_index()

size_t flattened_index ( size_t i, size_t n )

static

flattened_past_byte_update()

flattened_pointert flattened_past_byte_update ( const byte_update2t & bu, unsigned lo, unsigned width )

static

flattened_position()

unsigned flattened_position	(	unsigned	offset,
		unsigned	width,
		unsigned	total )

Lowest bit of the width bits at bit offset offset of a total bit object's bit-vector encoding.

from_memory_order()

expr2tc from_memory_order ( const expr2tc & bits, const type2tc & type )

static

from_object_bits()

expr2tc from_object_bits ( const expr2tc & bits, const type2tc & type )

static

Read an object of type back from its representation bits.

in_memory_order()

expr2tc in_memory_order ( const expr2tc & bits )

static

is_vector_bitcast()

bool is_vector_bitcast ( const type2tc & from, const type2tc & to )

static

lanewise_bitcast()

expr2tc lanewise_bitcast ( const expr2tc & from, const type2tc & to )

static

lowest_address_high()

bool lowest_address_high

(

)

Whether an object's lowest address sits in the most significant bits of its bit-vector encoding: true on a big-endian target, so the bit-vector reads as the object's bytes in memory order, as byte_extract assumes.

object_bits()

expr2tc object_bits ( const expr2tc & value )

static

The object representation of value, lowest address in the low bits.

pointer_flattened_at()

flattened_pointert pointer_flattened_at ( const expr2tc & e, unsigned lo, unsigned width )

static

to_memory_order()

expr2tc to_memory_order ( const expr2tc & value )

static

union_bits_of_member()

expr2tc union_bits_of_member	(	const expr2tc &	member,
		unsigned	bits )

A union member's bits member widened to the union's bits, as the bits at the union's lowest address; zero-extension is left to the caller.

union_bits_with_member()

expr2tc union_bits_with_member	(	const expr2tc &	rest,
		const expr2tc &	member,
		unsigned	bits )

The bits wide bits of a union whose lowest-addressed bits hold member and whose other bits are those of rest.

union_member_bits()

expr2tc union_member_bits	(	const expr2tc &	bits,
		unsigned	width )

The width bits of a union member within the union's bits bits: those at the union's lowest address.