memory_ops.cpp File Reference

#include <cassert>
#include <goto-symex/scheduler/execution_state.h>
#include <goto-symex/engine/goto_symex.h>
#include <goto-symex/scheduler/reachability_tree.h>
#include <string>
#include <vector>
#include <util/arith/arith_tools.h>
#include <util/lang/c_types.h>
#include <util/expr/expr_util.h>
#include <irep2/irep2.h>
#include <irep2/irep2_utils.h>
#include <util/message/message.h>
#include <util/message/format.h>
#include <util/irep/migrate.h>
#include <util/base/prefix.h>
#include <util/irep/std_types.h>
#include <algorithm>

Include dependency graph for memory_ops.cpp:

Functions
static const array_type2t *	multibyte_array (const expr2tc &object)
static expr2tc	object_byte (const expr2tc &object, uint64_t offset, bool big_endian)
	Byte offset of object.
static expr2tc	update_object_byte (const expr2tc &object, uint64_t offset, const expr2tc &byte, bool big_endian)
	object with byte offset replaced by byte.
static bool	target_is_big_endian ()
static size_t	byte_shift (const type2tc &type, size_t offset, size_t n)
static expr2tc	gen_byte_expression_byte_update (const type2tc &type, const expr2tc &src, const expr2tc &value, const size_t num_of_bytes, const size_t offset)
static expr2tc	gen_byte_expression (const type2tc &type, const expr2tc &src, const expr2tc &value, const size_t num_of_bytes, const size_t offset)
static bool	lacks_byte_model (const type2tc &type)
static expr2tc	gen_value_by_byte (const type2tc &type, const expr2tc &src, const expr2tc &value, const size_t num_of_bytes, const size_t offset)
static bool	member_byte_range (const struct_type2t &st, const type2tc &root_type, size_t i, uint64_t &offset, uint64_t &size)
static bool	spans_bytes (const type2tc &type, uint64_t n)
static bool	fits_bytes (const type2tc &type, uint64_t offset, uint64_t n)
static void	collect_subobjects (const expr2tc &root, uint64_t offset, uint64_t n, std::vector< expr2tc > &out)
static expr2tc	replace_subobject (const expr2tc &root, uint64_t offset, uint64_t n, const expr2tc &value)
static expr2tc	replace_in_struct (const expr2tc &root, uint64_t offset, uint64_t n, const expr2tc &value)
static expr2tc	object_bytes (const expr2tc &object, uint64_t offset, uint64_t n)
	The n bytes of object from byte offset, as one bit-vector in the target's byte order.
static expr2tc	copy_into_float (const expr2tc &dst, uint64_t dst_offset, const expr2tc &src, uint64_t src_offset, uint64_t n)
static expr2tc	copy_primitive (const expr2tc &dst, uint64_t dst_offset, const expr2tc &src, uint64_t src_offset, uint64_t n)
static expr2tc	do_memcpy_expression (const expr2tc &dst, const size_t &dst_offset, const expr2tc &src, const size_t &src_offset, const size_t num_of_bytes)
static void	offset_simplifier (expr2tc &e)

Function Documentation

byte_shift()

size_t byte_shift ( const type2tc & type, size_t offset, size_t n )

static

collect_subobjects()

void collect_subobjects ( const expr2tc & root, uint64_t offset, uint64_t n, std::vector< expr2tc > & out )

static

copy_into_float()

expr2tc copy_into_float ( const expr2tc & dst, uint64_t dst_offset, const expr2tc & src, uint64_t src_offset, uint64_t n )

static

copy_primitive()

expr2tc copy_primitive ( const expr2tc & dst, uint64_t dst_offset, const expr2tc & src, uint64_t src_offset, uint64_t n )

static

do_memcpy_expression()

expr2tc do_memcpy_expression ( const expr2tc & dst, const size_t & dst_offset, const expr2tc & src, const size_t & src_offset, const size_t num_of_bytes )

inlinestatic

fits_bytes()

bool fits_bytes ( const type2tc & type, uint64_t offset, uint64_t n )

static

gen_byte_expression()

expr2tc gen_byte_expression ( const type2tc & type, const expr2tc & src, const expr2tc & value, const size_t num_of_bytes, const size_t offset )

inlinestatic

The idea of this expression is to compute the object value in the case where every byte value was set up until num_of_bytes

Note: this function assumes that all memory checks have been done!

In summary, there are two main computations here:

A. Generate the byte representation, this is mostly through the result expression. The expression is initialized with zero and then, until the num_of_bytes is reached it will do a full byte left-shift followed by an bitor operation with the byte value:

For example, for a integer(4 bytes) with memset using 3 bytes and value 0xF1

step 1: 0x00000000 – left-shift 8 – 0x00000000 – bitor – 0x000000F1 step 2: 0x000000F1 – left-shift 8 – 0x0000F100 – bitor – 0x0000F1F1 step 3: 0x0000F1F1 – left-shift 8 – 0x00F1F100 – bitor – 0x00F1F1F1

Since we only want 3 bytes, the initialized object value would be 0x00F1F1F1

B. Generate a mask of the bits that were not set, this is done because skipped bits need to be returned back. The computation of this is simple, we initialize every bit that was changed by the byte-representation computation with a 1, which is then negated to be applied with an bitand in the original value:

Back to the example in A, we had the byte-representation of 0x00F1F1F1. If the original value was 0xA2A2A2A2, then we would have the following mask:

step 1: 0x00000000 – set-bits – 0x000000FF step 2: 0x000000FF – set-bits – 0x0000FFFF step 3: 0x0000FFFF – set-bits – 0x00FFFFFF

So, 0x00FFFFFF is the mask for all bits changed. We can negate it to: 0xFF000000

Then, we can apply it to the original source value with bitand

0xA2A2A2A2 AND 0xFF000000 --> 0xA2000000

Finally, we get the result from A and B and unify them through a bitor

0xA2000000 OR 0x00F1F1F1 --> 0xA2F1F1F1

Note about offsets: To handle them, we apply left shifts to the remaining offset after the computation of the object-value and initial mask representation

gen_byte_expression_byte_update()

expr2tc gen_byte_expression_byte_update ( const type2tc & type, const expr2tc & src, const expr2tc & value, const size_t num_of_bytes, const size_t offset )

inlinestatic

gen_value_by_byte()

expr2tc gen_value_by_byte ( const type2tc & type, const expr2tc & src, const expr2tc & value, const size_t num_of_bytes, const size_t offset )

inlinestatic

Construct a new object, initializing it with the memset equivalent

There are a few corner cases here:

1 - Primitives: these are simple: just generate the byte_expression directly 2 - Arrays: these are ok: just keep generating byte_expression for each member until a limit has arrived. Dynamic memory is dealt here. 3 - Structs/Union: these are the hardest as we have to take the alignment into account when dealing with it. Hopefully the clang-frontend already give it to us.

Similar to array, however get the size of each component

Unions are not nice, let's go through every member and get the biggest one! And then use it directly

Warning

there is a semantic difference on this when compared to c:@F@__memset_impl. While this function will yield the same result as clang would, ESBMC will handle the dereference (in the __memset_impl) using the first member, which can lead to overflows. See GitHub Issue #639

lacks_byte_model()

bool lacks_byte_model ( const type2tc & type )

static

member_byte_range()

bool member_byte_range ( const struct_type2t & st, const type2tc & root_type, size_t i, uint64_t & offset, uint64_t & size )

static

multibyte_array()

const array_type2t * multibyte_array ( const expr2tc & object )

static

object_byte()

expr2tc object_byte ( const expr2tc & object, uint64_t offset, bool big_endian )

static

Byte offset of object.

object_bytes()

expr2tc object_bytes ( const expr2tc & object, uint64_t offset, uint64_t n )

static

The n bytes of object from byte offset, as one bit-vector in the target's byte order.

offset_simplifier()

void offset_simplifier ( expr2tc & e )

static

replace_in_struct()

expr2tc replace_in_struct ( const expr2tc & root, uint64_t offset, uint64_t n, const expr2tc & value )

static

replace_subobject()

expr2tc replace_subobject ( const expr2tc & root, uint64_t offset, uint64_t n, const expr2tc & value )

static

spans_bytes()

bool spans_bytes ( const type2tc & type, uint64_t n )

static

target_is_big_endian()

bool target_is_big_endian ( )

static

update_object_byte()

expr2tc update_object_byte ( const expr2tc & object, uint64_t offset, const expr2tc & byte, bool big_endian )

static

object with byte offset replaced by byte.