cprover
|
#include "expr_lowering.h"
#include <algorithm>
#include <util/arith_tools.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/pointer_offset_size.h>
#include <util/replace_symbol.h>
#include <util/simplify_expr.h>
#include <util/string_constant.h>
Go to the source code of this file.
Classes | |
struct | boundst |
Functions | |
static optionalt< std::pair< struct_union_typet::componentt, mp_integer > > | find_widest_union_component (const union_typet &union_type, const namespacet &ns) |
Determine the member of maximum fixed bit width in a union type. More... | |
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... | |
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 (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 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... | |
|
static |
Convert a bitvector-typed expression bitvector_expr
to an array-typed expression.
See bv_to_expr for an overview.
Definition at line 193 of file byte_operators.cpp.
|
static |
Convert a bitvector-typed expression bitvector_expr
to a complex-typed expression.
See bv_to_expr for an overview.
Definition at line 291 of file byte_operators.cpp.
|
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
.
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. |
target_type
constructed from sequences of bits from bitvector_expr
. Definition at line 344 of file byte_operators.cpp.
|
static |
Convert a bitvector-typed expression bitvector_expr
to a struct-typed expression.
See bv_to_expr for an overview.
Definition at line 99 of file byte_operators.cpp.
|
static |
Convert a bitvector-typed expression bitvector_expr
to a union-typed expression.
See bv_to_expr for an overview.
Definition at line 146 of file byte_operators.cpp.
|
static |
Convert a bitvector-typed expression bitvector_expr
to a vector-typed expression.
See bv_to_expr for an overview.
Definition at line 246 of file byte_operators.cpp.
|
static |
Determine the member of maximum fixed bit width in a union type.
If no member, or no member of fixed and non-zero width can be found, return nullopt.
union_type | Type to determine the member of. |
ns | Namespace to resolve tag types. |
union_type
and the bit width of that member. Definition at line 32 of file byte_operators.cpp.
bool has_byte_operator | ( | const exprt & | src | ) |
Definition at line 2302 of file byte_operators.cpp.
|
static |
Build the individual bytes to be used in an update.
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 |
Definition at line 430 of file byte_operators.cpp.
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 999 of file byte_operators.cpp.
|
static |
Rewrite a byte extraction of a complex-typed result to byte extraction of the individual components that make up a complex_exprt.
src | Original byte extract expression |
unpacked | Byte extraction with root operand expanded into array (via unpack_rec) |
ns | Namespace |
nullopt
so that a fall-back to more generic code can be used. Definition at line 968 of file byte_operators.cpp.
exprt lower_byte_operators | ( | const exprt & | src, |
const namespacet & | ns | ||
) |
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental operations.
src | Input expression |
ns | Namespace |
Definition at line 2317 of file byte_operators.cpp.
|
static |
Apply a byte update src
using the byte array value_as_byte_array
as update value.
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 |
Definition at line 2057 of file byte_operators.cpp.
exprt lower_byte_update | ( | const byte_update_exprt & | src, |
const namespacet & | ns | ||
) |
Rewrite a byte update expression to more fundamental operations.
src | Byte update expression |
ns | Namespace |
src
. Definition at line 2256 of file byte_operators.cpp.
|
static |
Apply a byte update src
to an array/vector typed operand using the byte array value_as_byte_array
as update value.
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 |
Definition at line 1735 of file byte_operators.cpp.
|
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.
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 |
Definition at line 1575 of file byte_operators.cpp.
|
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.
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 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 |
Definition at line 1450 of file byte_operators.cpp.
|
static |
Apply a byte update src
to an array/vector of bytes using the byte array value_as_byte_array
as update value.
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 |
Definition at line 1384 of file byte_operators.cpp.
|
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.
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 |
Definition at line 1328 of file byte_operators.cpp.
|
static |
Apply a byte update src
to a struct typed operand using the byte array value_as_byte_array
as update value.
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 |
Definition at line 1836 of file byte_operators.cpp.
|
static |
Apply a byte update src
to a union typed operand using the byte array value_as_byte_array
as update value.
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 |
Definition at line 2025 of file byte_operators.cpp.
|
static |
Map bit boundaries according to endianness.
Definition at line 72 of file byte_operators.cpp.
|
static |
Extract bytes from a sequence of bitvector-typed elements.
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 609 of file byte_operators.cpp.
|
static |
Rewrite an array or vector into its individual bytes.
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 |
Definition at line 469 of file byte_operators.cpp.
|
static |
Rewrite a complex_exprt into its individual bytes.
src | complex-typed expression to unpack |
little_endian | true, iff assumed endianness is little-endian |
ns | namespace for type lookups |
Definition at line 762 of file byte_operators.cpp.
|
static |
Rewrite an object into its individual bytes.
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 |
Definition at line 808 of file byte_operators.cpp.
|
static |
Rewrite a struct-typed expression into its individual bytes.
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 |
Definition at line 639 of file byte_operators.cpp.