|
CBMC
|
#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. | |
| 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. | |
| 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. | |
| 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.
|
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.
|
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.
|
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 330 of file lower_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 78 of file lower_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 127 of file lower_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 229 of file lower_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 |
| bits_per_byte | number of bits that make up a byte |
| ns | Namespace |
Definition at line 424 of file lower_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 1215 of file lower_byte_operators.cpp.
|
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.
| 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 |
Definition at line 1102 of file lower_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 1183 of file lower_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 2638 of file lower_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 2316 of file lower_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 2545 of file lower_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 |
| 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 |
Definition at line 2096 of file lower_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 1771 of file lower_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 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 1631 of file lower_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 1558 of file lower_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 1489 of file lower_byte_operators.cpp.
|
static |
Byte update a struct/array/vector element.
| 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 |
Definition at line 1921 of file lower_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 2180 of file lower_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 2284 of file lower_byte_operators.cpp.
|
static |
Map bit boundaries according to endianness.
Definition at line 36 of file lower_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 | |
| bits_per_byte | number of bits that make up a byte | |
| ns | namespace for type lookups |
Definition at line 652 of file lower_byte_operators.cpp.
|
static |
Rewrite an array or vector into its individual bytes.
| 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 |
Definition at line 537 of file lower_byte_operators.cpp.
|
static |
Rewrite an array or vector into its individual bytes when no maximum number of bytes is known.
| 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 |
Definition at line 468 of file lower_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 |
| bits_per_byte | number of bits that make up a byte |
| ns | namespace for type lookups |
Definition at line 843 of file lower_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 |
| 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 |
Definition at line 897 of file lower_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 |
| bits_per_byte | number of bits that make up a byte |
| ns | namespace for type lookups |
Definition at line 690 of file lower_byte_operators.cpp.