Loading...

Searching...

No Matches

lower_byte_operators.cpp File Reference

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

+ Include dependency graph for lower_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.

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.

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

changes the width of the given bitvector type

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.

static 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.

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.

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.

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.

static exprt unpack_rec (const exprt &src, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns, bool unpack_byte_array)

Rewrite an object into its individual bytes.

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

Build the individual bytes to be used in an update.

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

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

static exprt unpack_array_vector (const exprt &src, const std::optional< mp_integer > &src_size, const mp_integer &element_bits, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)

Rewrite an array or vector into its individual bytes.

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

Extract bytes from a sequence of bitvector-typed elements.

static array_exprt unpack_struct (const exprt &src, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)

Rewrite a struct-typed expression into its individual bytes.

static array_exprt unpack_complex (const exprt &src, bool little_endian, const std::size_t bits_per_byte, const namespacet &ns)

Rewrite a complex_exprt into its individual bytes.

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.

static std::optional< 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.

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

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

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

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.

static exprt lower_byte_update_byte_array_vector (const byte_update_exprt &src, const typet &subtype, const array_exprt &value_as_byte_array, const std::optional< 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.

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.

static exprt lower_byte_update_array_vector_non_const (const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const std::optional< 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.

static exprt lower_byte_update_single_element (const byte_update_exprt &src, const mp_integer &offset_bits, const exprt &element_to_update, const mp_integer &subtype_bits, const mp_integer &bits_already_set, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)

Byte update a struct/array/vector element.

static exprt lower_byte_update_array_vector (const byte_update_exprt &src, const typet &subtype, const std::optional< mp_integer > &subtype_bits, const exprt &value_as_byte_array, const std::optional< 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.

static exprt lower_byte_update_struct (const byte_update_exprt &src, const struct_typet &struct_type, const exprt &value_as_byte_array, const std::optional< 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.

static exprt lower_byte_update_union (const byte_update_exprt &src, const union_typet &union_type, const exprt &value_as_byte_array, const std::optional< 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.

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

Rewrite a byte update expression to more fundamental operations.

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

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

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 59 of file lower_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 175 of file lower_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 275 of file lower_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 330 of file lower_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 78 of file lower_byte_operators.cpp.

◆ bv_to_union_expr()

static 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 127 of file lower_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 229 of file lower_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 std::size_t bits_per_byte,

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

bits_per_byte number of bits that make up a byte

ns Namespace

Returns: Sequence of bytes.

Definition at line 424 of file lower_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 1242 of file lower_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 1129 of file lower_byte_operators.cpp.

◆ lower_byte_extract_complex()

static std::optional< 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 1210 of file lower_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 2665 of file lower_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 std::optional< 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 2343 of file lower_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 2572 of file lower_byte_operators.cpp.

◆ lower_byte_update_array_vector()

static exprt lower_byte_update_array_vector ( const byte_update_exprt & src,

const typet & subtype,

const std::optional< mp_integer > & subtype_bits,

const exprt & value_as_byte_array,

const std::optional< 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

subtype_bits Bit width of subtype

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 2123 of file lower_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 std::optional< 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 1798 of file lower_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 1658 of file lower_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 std::optional< 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 1585 of file lower_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 1516 of file lower_byte_operators.cpp.

◆ lower_byte_update_single_element()

static exprt lower_byte_update_single_element ( const byte_update_exprt & src,

const mp_integer & offset_bits,

const exprt & element_to_update,

const mp_integer & subtype_bits,

const mp_integer & bits_already_set,

const exprt & value_as_byte_array,

const std::optional< exprt > & non_const_update_bound,

const namespacet & ns

)

static

Byte update a struct/array/vector element.

Parameters: src Original byte-update expression

offset_bits Offset in src expressed as bits

element_to_update struct/array/vector element

subtype_bits Bit width of element_to_update

bits_already_set Number of bits in the original target object that have been updated already

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 1948 of file lower_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 std::optional< 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 2207 of file lower_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 std::optional< 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 2311 of file lower_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 36 of file lower_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 std::optional< mp_integer > & offset_bytes,

const std::optional< mp_integer > & max_bytes,

const std::size_t bits_per_byte,

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

bits_per_byte number of bits that make up a byte

ns namespace for type lookups

Definition at line 665 of file lower_byte_operators.cpp.

◆ unpack_array_vector()

static exprt unpack_array_vector ( const exprt & src,

const std::optional< mp_integer > & src_size,

const mp_integer & element_bits,

bool little_endian,

const std::optional< mp_integer > & offset_bytes,

const std::optional< mp_integer > & max_bytes,

const std::size_t bits_per_byte,

const namespacet & ns

)

static

Rewrite an array or vector into its individual bytes.

Parameters: src array/vector to unpack

src_size number of elements in src, if the array/vector size is constant; if the array/vector size is not constant (and this argument thus not set), max_bytes needs to be a known constant value to build an array expression, else we fall back to building an 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

bits_per_byte number of bits that make up a byte

ns namespace for type lookups

Returns: Array expression holding unpacked elements or array comprehension

Definition at line 550 of file lower_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 std::size_t bits_per_byte,

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

bits_per_byte number of bits that make up a byte

ns namespace for type lookups

Returns: Array expression holding unpacked elements or array comprehension

Definition at line 468 of file lower_byte_operators.cpp.

◆ unpack_complex()

static array_exprt unpack_complex ( const exprt & src,

bool little_endian,

const std::size_t bits_per_byte,

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

bits_per_byte number of bits that make up a byte

ns namespace for type lookups

Returns: array_exprt holding unpacked elements

Definition at line 856 of file lower_byte_operators.cpp.

◆ unpack_rec()

static exprt unpack_rec ( const exprt & src,

bool little_endian,

const std::optional< mp_integer > & offset_bytes,

const std::optional< mp_integer > & max_bytes,

const std::size_t bits_per_byte,

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

bits_per_byte number of bits that make up a byte

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 910 of file lower_byte_operators.cpp.

◆ unpack_struct()

static array_exprt unpack_struct ( const exprt & src,

bool little_endian,

const std::optional< mp_integer > & offset_bytes,

const std::optional< mp_integer > & max_bytes,

const std::size_t bits_per_byte,

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

bits_per_byte number of bits that make up a byte

ns namespace for type lookups

Returns: array_exprt holding unpacked elements

Definition at line 703 of file lower_byte_operators.cpp.