byte_operators.cpp File Reference

#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/endianness_map.h>
#include <util/expr_util.h>
#include <util/namespace.h>
#include <util/narrow.h>
#include <util/pointer_offset_size.h>
#include <util/simplify_expr.h>
#include <util/string_constant.h>
#include "expr_lowering.h"
#include <algorithm>

Include dependency graph for byte_operators.cpp:

Go to the source code of this file.

Classes
struct	boundst

Functions
static exprt	bv_to_expr (const exprt &bitvector_expr, const typet &target_type, const endianness_mapt &endianness_map, const namespacet &ns)
	Convert a bitvector-typed expression bitvector_expr to an expression of type target_type. More...
static boundst	map_bounds (const endianness_mapt &endianness_map, std::size_t lower_bound, std::size_t upper_bound)
	Map bit boundaries according to endianness. More...
bitvector_typet	adjust_width (const typet &src, std::size_t new_width)
	changes the width of the given bitvector type More...
static struct_exprt	bv_to_struct_expr (const exprt &bitvector_expr, const struct_typet &struct_type, const endianness_mapt &endianness_map, const namespacet &ns)
	Convert a bitvector-typed expression bitvector_expr to a struct-typed expression. More...
static union_exprt	bv_to_union_expr (const exprt &bitvector_expr, const union_typet &union_type, const endianness_mapt &endianness_map, const namespacet &ns)
	Convert a bitvector-typed expression bitvector_expr to a union-typed expression. More...
static array_exprt	bv_to_array_expr (const exprt &bitvector_expr, const array_typet &array_type, const endianness_mapt &endianness_map, const namespacet &ns)
	Convert a bitvector-typed expression bitvector_expr to an array-typed expression. More...
static vector_exprt	bv_to_vector_expr (const exprt &bitvector_expr, const vector_typet &vector_type, const endianness_mapt &endianness_map, const namespacet &ns)
	Convert a bitvector-typed expression bitvector_expr to a vector-typed expression. More...
static complex_exprt	bv_to_complex_expr (const exprt &bitvector_expr, const complex_typet &complex_type, const endianness_mapt &endianness_map, const namespacet &ns)
	Convert a bitvector-typed expression bitvector_expr to a complex-typed expression. More...
static exprt	unpack_rec (const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns, bool unpack_byte_array)
	Rewrite an object into its individual bytes. More...
static exprt::operandst	instantiate_byte_array (const exprt &src, std::size_t lower_bound, std::size_t upper_bound, const namespacet &ns)
	Build the individual bytes to be used in an update. More...
static exprt	unpack_array_vector_no_known_bounds (const exprt &src, std::size_t el_bytes, bool little_endian, const namespacet &ns)
	Rewrite an array or vector into its individual bytes when no maximum number of bytes is known. More...
static exprt	unpack_array_vector (const exprt &src, const optionalt< mp_integer > &src_size, const mp_integer &element_bits, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
	Rewrite an array or vector into its individual bytes. More...
static void	process_bit_fields (exprt::operandst &&bit_fields, std::size_t total_bits, exprt::operandst &dest, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
	Extract bytes from a sequence of bitvector-typed elements. More...
static array_exprt	unpack_struct (const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
	Rewrite a struct-typed expression into its individual bytes. More...
static array_exprt	unpack_complex (const exprt &src, bool little_endian, const namespacet &ns)
	Rewrite a complex_exprt into its individual bytes. More...
static exprt	lower_byte_extract_array_vector (const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const typet &subtype, const mp_integer &element_bits, const namespacet &ns)
	Rewrite a byte extraction of an array/vector-typed result to byte extraction of the individual components that make up an array_exprt or vector_exprt. More...
static optionalt< exprt >	lower_byte_extract_complex (const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const namespacet &ns)
	Rewrite a byte extraction of a complex-typed result to byte extraction of the individual components that make up a complex_exprt. More...
exprt	lower_byte_extract (const byte_extract_exprt &src, const namespacet &ns)
	rewrite byte extraction from an array to byte extraction from a concatenation of array index expressions More...
static exprt	lower_byte_update (const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
	Apply a byte update src using the byte array value_as_byte_array as update value. More...
static exprt	lower_byte_update_byte_array_vector_non_const (const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const namespacet &ns)
	Apply a byte update src to an array/vector of bytes using the byte-array typed expression value_as_byte_array as update value. More...
static exprt	lower_byte_update_byte_array_vector (const byte_update_exprt &src, const typet &subtype, const array_exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
	Apply a byte update src to an array/vector of bytes using the byte array value_as_byte_array as update value. More...
static exprt	lower_byte_update_array_vector_unbounded (const byte_update_exprt &src, const typet &subtype, const exprt &subtype_size, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const exprt &initial_bytes, const exprt &first_index, const exprt &first_update_value, const namespacet &ns)
	Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as update value, which has non-constant size. More...
static exprt	lower_byte_update_array_vector_non_const (const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
	Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as update value, when either the size of each element or the overall array/vector size is not constant. More...
static exprt	lower_byte_update_array_vector (const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
	Apply a byte update src to an array/vector typed operand using the byte array value_as_byte_array as update value. More...
static exprt	lower_byte_update_struct (const byte_update_exprt &src, const struct_typet &struct_type, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
	Apply a byte update src to a struct typed operand using the byte array value_as_byte_array as update value. More...
static exprt	lower_byte_update_union (const byte_update_exprt &src, const union_typet &union_type, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
	Apply a byte update src to a union typed operand using the byte array value_as_byte_array as update value. More...
exprt	lower_byte_update (const byte_update_exprt &src, const namespacet &ns)
	Rewrite a byte update expression to more fundamental operations. More...
bool	has_byte_operator (const exprt &src)
exprt	lower_byte_operators (const exprt &src, const namespacet &ns)
	Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental operations. More...

Function Documentation

adjust_width()

bitvector_typet adjust_width	(	const typet &	src,
		std::size_t	new_width
	)

changes the width of the given bitvector type

Definition at line 61 of file byte_operators.cpp.

bv_to_array_expr()

static array_exprt bv_to_array_expr ( const exprt &  bitvector_expr, const array_typet &  array_type, const endianness_mapt &  endianness_map, const namespacet &  ns  )

static

Convert a bitvector-typed expression bitvector_expr to an array-typed expression.

See bv_to_expr for an overview.

Definition at line 176 of file byte_operators.cpp.

bv_to_complex_expr()

static complex_exprt bv_to_complex_expr ( const exprt &  bitvector_expr, const complex_typet &  complex_type, const endianness_mapt &  endianness_map, const namespacet &  ns  )

static

Convert a bitvector-typed expression bitvector_expr to a complex-typed expression.

See bv_to_expr for an overview.

Definition at line 278 of file byte_operators.cpp.

bv_to_expr()

static exprt bv_to_expr ( const exprt &  bitvector_expr, const typet &  target_type, const endianness_mapt &  endianness_map, const namespacet &  ns  )

static

Convert a bitvector-typed expression bitvector_expr to an expression of type target_type.

If target_type is a bitvector type this may be a no-op or a typecast. For composite types such as structs, the bitvectors corresponding to the individual members are extracted and then a compound expression is built from those extracted members. When the size of a component isn't constant we fall back to computing its size based on the width of bitvector_expr.

Parameters

bitvector_expr	Bitvector-typed expression to extract from.
target_type	Type of the expression to build.
ns	Namespace to resolve tag types.
endianness_map	Endianness map.

Returns

Expression of type target_type constructed from sequences of bits from bitvector_expr.

Definition at line 333 of file byte_operators.cpp.

bv_to_struct_expr()

static struct_exprt bv_to_struct_expr ( const exprt &  bitvector_expr, const struct_typet &  struct_type, const endianness_mapt &  endianness_map, const namespacet &  ns  )

static

Convert a bitvector-typed expression bitvector_expr to a struct-typed expression.

See bv_to_expr for an overview.

Definition at line 80 of file byte_operators.cpp.

bv_to_union_expr()

static union_exprt bv_to_union_expr ( const exprt &  bitvector_expr, const union_typet &  union_type, const endianness_mapt &  endianness_map, const namespacet &  ns  )

static

Convert a bitvector-typed expression bitvector_expr to a union-typed expression.

See bv_to_expr for an overview.

Definition at line 128 of file byte_operators.cpp.

bv_to_vector_expr()

static vector_exprt bv_to_vector_expr ( const exprt &  bitvector_expr, const vector_typet &  vector_type, const endianness_mapt &  endianness_map, const namespacet &  ns  )

static

Convert a bitvector-typed expression bitvector_expr to a vector-typed expression.

See bv_to_expr for an overview.

Definition at line 231 of file byte_operators.cpp.

has_byte_operator()

bool has_byte_operator

(

const exprt &

src

)

Definition at line 2377 of file byte_operators.cpp.

instantiate_byte_array()

static exprt::operandst instantiate_byte_array ( const exprt &  src, std::size_t  lower_bound, std::size_t  upper_bound, const namespacet &  ns  )

static

Build the individual bytes to be used in an update.

Parameters

src	Source expression of array or vector type
lower_bound	First index into src to be included in the result
upper_bound	First index into src to be excluded from the result
ns	Namespace

Returns

Sequence of bytes.

Definition at line 419 of file byte_operators.cpp.

lower_byte_extract()

exprt lower_byte_extract	(	const byte_extract_exprt &	src,
		const namespacet &	ns
	)

rewrite byte extraction from an array to byte extraction from a concatenation of array index expressions

Rewrite a byte extract expression to more fundamental operations.

Definition at line 1099 of file byte_operators.cpp.

lower_byte_extract_array_vector()

static exprt lower_byte_extract_array_vector ( const byte_extract_exprt &  src, const byte_extract_exprt &  unpacked, const typet &  subtype, const mp_integer &  element_bits, const namespacet &  ns  )

static

Rewrite a byte extraction of an array/vector-typed result to byte extraction of the individual components that make up an array_exprt or vector_exprt.

Parameters

src	Original byte extract expression
unpacked	Byte extraction with root operand expanded into array (via unpack_rec)
subtype	Array/vector element type
element_bits	bit width of array/vector elements
ns	Namespace

Returns

An array or vector expression.

Definition at line 992 of file byte_operators.cpp.

lower_byte_extract_complex()

static optionalt<exprt> lower_byte_extract_complex ( const byte_extract_exprt &  src, const byte_extract_exprt &  unpacked, const namespacet &  ns  )

static

Rewrite a byte extraction of a complex-typed result to byte extraction of the individual components that make up a complex_exprt.

Parameters

src	Original byte extract expression
unpacked	Byte extraction with root operand expanded into array (via unpack_rec)
ns	Namespace

Returns

An expression if the subtype size is known, else nullopt so that a fall-back to more generic code can be used.

Definition at line 1068 of file byte_operators.cpp.

lower_byte_operators()

exprt lower_byte_operators	(	const exprt &	src,
		const namespacet &	ns
	)

Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental operations.

Parameters

src	Input expression
ns	Namespace

Returns

Semantically equivalent expression that does not contain any byte_extract_exprt or byte_update_exprt.

Definition at line 2392 of file byte_operators.cpp.

lower_byte_update() [1/2]

static exprt lower_byte_update ( const byte_update_exprt &  src, const exprt &  value_as_byte_array, const optionalt< exprt > &  non_const_update_bound, const namespacet &  ns  )

static

Apply a byte update src using the byte array value_as_byte_array as update value.

Parameters

src	Original byte-update expression
value_as_byte_array	Update value as an array of bytes
non_const_update_bound	If set, (symbolically) constrain updates such as to at most update non_const_update_bound elements
ns	Namespace

Returns

Expression reflecting all updates.

Definition at line 2080 of file byte_operators.cpp.

lower_byte_update() [2/2]

exprt lower_byte_update	(	const byte_update_exprt &	src,
		const namespacet &	ns
	)

Rewrite a byte update expression to more fundamental operations.

Parameters

src	Byte update expression
ns	Namespace

Returns

Semantically equivalent expression such that the top-level expression no longer is a byte_extract_exprt or byte_update_exprt. Use lower_byte_operators to also remove all byte operators from any operands of src.

Definition at line 2286 of file byte_operators.cpp.

lower_byte_update_array_vector()

static exprt lower_byte_update_array_vector ( const byte_update_exprt &  src, const typet &  subtype, const exprt &  value_as_byte_array, const optionalt< exprt > &  non_const_update_bound, const namespacet &  ns  )

static

Apply a byte update src to an array/vector typed operand using the byte array value_as_byte_array as update value.

Parameters

src	Original byte-update expression
subtype	Array/vector element type
value_as_byte_array	Update value as an array of bytes
non_const_update_bound	If set, (symbolically) constrain updates such as to at most update non_const_update_bound elements
ns	Namespace

Returns

Array/vector expression reflecting all updates.

Definition at line 1757 of file byte_operators.cpp.

lower_byte_update_array_vector_non_const()

static exprt lower_byte_update_array_vector_non_const ( const byte_update_exprt &  src, const typet &  subtype, const exprt &  value_as_byte_array, const optionalt< exprt > &  non_const_update_bound, const namespacet &  ns  )

static

Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as update value, when either the size of each element or the overall array/vector size is not constant.

Parameters

src	Original byte-update expression
subtype	Array/vector element type
value_as_byte_array	Update value as an array of bytes
non_const_update_bound	If set, (symbolically) constrain updates such as to at most update non_const_update_bound elements
ns	Namespace

Returns

Array/vector expression reflecting all updates.

Definition at line 1597 of file byte_operators.cpp.

lower_byte_update_array_vector_unbounded()

static exprt lower_byte_update_array_vector_unbounded ( const byte_update_exprt &  src, const typet &  subtype, const exprt &  subtype_size, const exprt &  value_as_byte_array, const exprt &  non_const_update_bound, const exprt &  initial_bytes, const exprt &  first_index, const exprt &  first_update_value, const namespacet &  ns  )

static

Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as update value, which has non-constant size.

Parameters

src	Original byte-update expression
subtype	Array/vector element type
subtype_size	Size (in bytes) of subtype
value_as_byte_array	Update value as an array of bytes
non_const_update_bound	Constrain updates such as to at most update non_const_update_bound elements
initial_bytes	Number of bytes from value_as_byte_array to use to update the array/vector element at first_index
first_index	Lowest index into the target array/vector of the update
first_update_value	Combined value of partially old and updated bytes to use at first_index
ns	Namespace

Returns

Array comprehension reflecting all updates.

Definition at line 1471 of file byte_operators.cpp.

lower_byte_update_byte_array_vector()

static exprt lower_byte_update_byte_array_vector ( const byte_update_exprt &  src, const typet &  subtype, const array_exprt &  value_as_byte_array, const optionalt< exprt > &  non_const_update_bound, const namespacet &  ns  )

static

Apply a byte update src to an array/vector of bytes using the byte array value_as_byte_array as update value.

Parameters

src	Original byte-update expression
subtype	Array/vector element type
value_as_byte_array	Update value as an array of bytes
non_const_update_bound	If set, (symbolically) constrain updates such as to at most update non_const_update_bound elements
ns	Namespace

Returns

Array/vector expression reflecting all updates.

Definition at line 1405 of file byte_operators.cpp.

lower_byte_update_byte_array_vector_non_const()

static exprt lower_byte_update_byte_array_vector_non_const ( const byte_update_exprt &  src, const typet &  subtype, const exprt &  value_as_byte_array, const exprt &  non_const_update_bound, const namespacet &  ns  )

static

Apply a byte update src to an array/vector of bytes using the byte-array typed expression value_as_byte_array as update value.

Parameters

src	Original byte-update expression
subtype	Array/vector element type
value_as_byte_array	Update value as an array of bytes
non_const_update_bound	Constrain updates such as to at most update non_const_update_bound elements
ns	Namespace

Returns

Array comprehension reflecting all updates.

Definition at line 1349 of file byte_operators.cpp.

lower_byte_update_struct()

static exprt lower_byte_update_struct ( const byte_update_exprt &  src, const struct_typet &  struct_type, const exprt &  value_as_byte_array, const optionalt< exprt > &  non_const_update_bound, const namespacet &  ns  )

static

Apply a byte update src to a struct typed operand using the byte array value_as_byte_array as update value.

Parameters

src	Original byte-update expression
struct_type	Type of the operand
value_as_byte_array	Update value as an array of bytes
non_const_update_bound	If set, (symbolically) constrain updates such as to at most update non_const_update_bound elements
ns	Namespace

Returns

Struct expression reflecting all updates.

Definition at line 1858 of file byte_operators.cpp.

lower_byte_update_union()

static exprt lower_byte_update_union ( const byte_update_exprt &  src, const union_typet &  union_type, const exprt &  value_as_byte_array, const optionalt< exprt > &  non_const_update_bound, const namespacet &  ns  )

static

Apply a byte update src to a union typed operand using the byte array value_as_byte_array as update value.

Parameters

src	Original byte-update expression
union_type	Type of the operand
value_as_byte_array	Update value as an array of bytes
non_const_update_bound	If set, (symbolically) constrain updates such as to at most update non_const_update_bound elements
ns	Namespace

Returns

Union expression reflecting all updates.

Definition at line 2048 of file byte_operators.cpp.

map_bounds()

static boundst map_bounds ( const endianness_mapt &  endianness_map, std::size_t  lower_bound, std::size_t  upper_bound  )

static

Map bit boundaries according to endianness.

Definition at line 38 of file byte_operators.cpp.

process_bit_fields()

static void process_bit_fields ( exprt::operandst &&  bit_fields, std::size_t  total_bits, exprt::operandst &  dest, bool  little_endian, const optionalt< mp_integer > &  offset_bytes, const optionalt< mp_integer > &  max_bytes, const namespacet &  ns  )

static

Extract bytes from a sequence of bitvector-typed elements.

Parameters

	bit_fields	operands to concatenate
	total_bits	total bit width of operands
[out]	dest	target to append unpacked bytes to
	little_endian	true, iff assumed endianness is little-endian
	offset_bytes	if set, bytes prior to this offset will be filled with nil values
	max_bytes	if set, use as upper bound of the number of bytes to unpack
	ns	namespace for type lookups

Definition at line 625 of file byte_operators.cpp.

unpack_array_vector()

static exprt unpack_array_vector ( const exprt &  src, const optionalt< mp_integer > &  src_size, const mp_integer &  element_bits, bool  little_endian, const optionalt< mp_integer > &  offset_bytes, const optionalt< mp_integer > &  max_bytes, const namespacet &  ns  )

static

Rewrite an array or vector into its individual bytes.

Parameters

src	array/vector to unpack
src_size	array/vector size; if not a constant and thus not set, max_bytes must be a known constant value to build an array expression, otherwise we fall back to building and array comprehension
element_bits	bit width of array/vector elements
little_endian	true, iff assumed endianness is little-endian
offset_bytes	if set, bytes prior to this offset will be filled with nil values
max_bytes	if set, use as upper bound of the number of bytes to unpack
ns	namespace for type lookups

Returns

Array expression holding unpacked elements or array comprehension

Definition at line 517 of file byte_operators.cpp.

unpack_array_vector_no_known_bounds()

static exprt unpack_array_vector_no_known_bounds ( const exprt &  src, std::size_t  el_bytes, bool  little_endian, const namespacet &  ns  )

static

Rewrite an array or vector into its individual bytes when no maximum number of bytes is known.

Parameters

src	array/vector to unpack
el_bytes	byte width of array/vector elements
little_endian	true, iff assumed endianness is little-endian
ns	namespace for type lookups

Returns

Array expression holding unpacked elements or array comprehension

Definition at line 458 of file byte_operators.cpp.

unpack_complex()

static array_exprt unpack_complex ( const exprt &  src, bool  little_endian, const namespacet &  ns  )

static

Rewrite a complex_exprt into its individual bytes.

Parameters

src	complex-typed expression to unpack
little_endian	true, iff assumed endianness is little-endian
ns	namespace for type lookups

Returns

array_exprt holding unpacked elements

Definition at line 778 of file byte_operators.cpp.

unpack_rec()

static exprt unpack_rec ( const exprt &  src, bool  little_endian, const optionalt< mp_integer > &  offset_bytes, const optionalt< mp_integer > &  max_bytes, const namespacet &  ns, bool  unpack_byte_array  )

static

Rewrite an object into its individual bytes.

Parameters

src	object to unpack
little_endian	true, iff assumed endianness is little-endian
offset_bytes	if set, bytes prior to this offset will be filled with nil values
max_bytes	if set, use as upper bound of the number of bytes to unpack
ns	namespace for type lookups
unpack_byte_array	if true, return unmodified src iff it is an

Returns

array of bytes in the sequence found in memory

Definition at line 824 of file byte_operators.cpp.

unpack_struct()

static array_exprt unpack_struct ( const exprt &  src, bool  little_endian, const optionalt< mp_integer > &  offset_bytes, const optionalt< mp_integer > &  max_bytes, const namespacet &  ns  )

static

Rewrite a struct-typed expression into its individual bytes.

Parameters

src	struct-typed expression to unpack
little_endian	true, iff assumed endianness is little-endian
offset_bytes	if set, bytes prior to this offset will be filled with nil values
max_bytes	if set, use as upper bound of the number of bytes to unpack
ns	namespace for type lookups

Returns

array_exprt holding unpacked elements

Definition at line 655 of file byte_operators.cpp.