Skip to content
Snippets Groups Projects
Commit 0aba9984 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Enable TLS storage tracking

parent 35d9f5a6
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
+ 16
− 23
View file @ 0aba9984
...@@ -46,18 +46,14 @@ static void * store_block(void * ptr, size_t size) { ...@@ -46,18 +46,14 @@ static void * store_block(void * ptr, size_t size) {
/* Only stack-global memory blocks are recorded explicitly via this function. /* Only stack-global memory blocks are recorded explicitly via this function.
* Heap blocks should be tracked internally using memory allocation functions * Heap blocks should be tracked internally using memory allocation functions
* such as malloc or calloc. */ * such as malloc or calloc. */
shadow_alloca(ptr, size, IS_ON_GLOBAL(ptr)); shadow_alloca(ptr, size);
return ptr; return ptr;
} }
static void delete_block(void * ptr) { static void delete_block(void * ptr) {
/* Block deletion should be performed on stack/global addresses only, /* Block deletion should be performed on stack/global addresses only,
* heap blocks should be deallocated manually via free/cfree/realloc. */ * heap blocks should be deallocated manually via free/cfree/realloc. */
if (IS_ON_STACK(ptr)) { shadow_freea(ptr);
stack_shadow_freea(ptr);
} else if (IS_ON_GLOBAL(ptr)) {
global_shadow_freea(ptr);
}
} }
static void full_init(void * ptr) { static void full_init(void * ptr) {
...@@ -74,23 +70,24 @@ static void readonly(void * ptr) { ...@@ -74,23 +70,24 @@ static void readonly(void * ptr) {
static int valid(void * ptr, size_t size) { static int valid(void * ptr, size_t size) {
uintptr_t addr = (uintptr_t)ptr; uintptr_t addr = (uintptr_t)ptr;
if (!IS_ON_VALID(addr)) if (IS_ON_HEAP(addr))
return heap_allocated(addr, size);
else if (IS_ON_STACK(addr))
return static_allocated(addr, size);
else if (IS_ON_GLOBAL(addr))
return static_allocated(addr, size) && !global_readonly(addr);
else if (!IS_ON_VALID(addr))
return 0; return 0;
TRY_SEGMENT(addr,
return heap_allocated(addr, size),
return stack_allocated(addr, size),
return global_allocated(addr, size) && !global_readonly(addr));
return 0; return 0;
} }
static int valid_read(void * ptr, size_t size) { static int valid_read(void * ptr, size_t size) {
uintptr_t addr = (uintptr_t)ptr; uintptr_t addr = (uintptr_t)ptr;
if (!IS_ON_VALID(addr))
return 0;
TRY_SEGMENT(addr, TRY_SEGMENT(addr,
return heap_allocated(addr, size), return heap_allocated(addr, size),
return stack_allocated(addr, size), return static_allocated(addr, size));
return global_allocated(addr, size)); if (!IS_ON_VALID(addr))
return 0;
return 0; return 0;
} }
...@@ -100,8 +97,7 @@ static int valid_read(void * ptr, size_t size) { ...@@ -100,8 +97,7 @@ static int valid_read(void * ptr, size_t size) {
static void * segment_base_addr(void * ptr) { static void * segment_base_addr(void * ptr) {
TRY_SEGMENT(ptr, TRY_SEGMENT(ptr,
return (void*)heap_info((uintptr_t)ptr, 'B'), return (void*)heap_info((uintptr_t)ptr, 'B'),
return (void*)stack_info((uintptr_t)ptr, 'B'), return (void*)static_info((uintptr_t)ptr, 'B'));
return (void*)global_info((uintptr_t)ptr, 'B'));
return NULL; return NULL;
} }
...@@ -111,8 +107,7 @@ static void * segment_base_addr(void * ptr) { ...@@ -111,8 +107,7 @@ static void * segment_base_addr(void * ptr) {
static size_t segment_block_length(void * ptr) { static size_t segment_block_length(void * ptr) {
TRY_SEGMENT(ptr, TRY_SEGMENT(ptr,
return heap_info((uintptr_t)ptr, 'L'), return heap_info((uintptr_t)ptr, 'L'),
return stack_info((uintptr_t)ptr, 'L'), return static_info((uintptr_t)ptr, 'L'))
return global_info((uintptr_t)ptr, 'L'))
return 0; return 0;
} }
...@@ -122,8 +117,7 @@ static size_t segment_block_length(void * ptr) { ...@@ -122,8 +117,7 @@ static size_t segment_block_length(void * ptr) {
static int segment_offset(void *ptr) { static int segment_offset(void *ptr) {
TRY_SEGMENT(ptr, TRY_SEGMENT(ptr,
return heap_info((uintptr_t)ptr, 'O'), return heap_info((uintptr_t)ptr, 'O'),
return stack_info((uintptr_t)ptr, 'O'), return static_info((uintptr_t)ptr, 'O'));
return global_info((uintptr_t)ptr, 'O'));
return 0; return 0;
} }
...@@ -131,8 +125,7 @@ static int initialized(void * ptr, size_t size) { ...@@ -131,8 +125,7 @@ static int initialized(void * ptr, size_t size) {
uintptr_t addr = (uintptr_t)ptr; uintptr_t addr = (uintptr_t)ptr;
TRY_SEGMENT_WEAK(addr, TRY_SEGMENT_WEAK(addr,
return heap_initialized(addr, size), return heap_initialized(addr, size),
return stack_initialized(addr, size), return static_initialized(addr, size));
return global_initialized(addr, size));
return 0; return 0;
} }
......
src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+ 79
− 130
View file @ 0aba9984
...@@ -254,19 +254,16 @@ static void validate_memory_layout() { ...@@ -254,19 +254,16 @@ static void validate_memory_layout() {
DVASSERT(heap_allocated((uintptr_t)_addr, _size), \ DVASSERT(heap_allocated((uintptr_t)_addr, _size), \
"Operation on unallocated heap block [%a + %lu]\n ", _addr, _size) "Operation on unallocated heap block [%a + %lu]\n ", _addr, _size)
# define segstr(_global) ((_global) ? "global" : "stack") # define DVALIDATE_STATIC_ACCESS(_addr, _size) \
# define DVALIDATE_STATIC_ACCESS(_addr, _size, _global) \ DVASSERT(IS_ON_STATIC(_addr), \
DVASSERT(IS_ON_STATIC(_addr, _global), \ "Expected location: %a\n ", _addr); \
"Expected %s location: %a\n ", segstr(_global), _addr); \ DVASSERT(static_allocated((uintptr_t)_addr, _size), \
DVASSERT(static_allocated((uintptr_t)_addr, _size, _global), \ "Operation on unallocated block [%a + %lu]\n ", _addr, _size)
"Operation on unallocated %s block [%a + %lu]\n ", \
segstr(_global), _addr, _size) # define DVALIDATE_STATIC_LOCATION(_addr) \
DVASSERT(IS_ON_STATIC(_addr), "Expected location: %a\n ", _addr); \
# define DVALIDATE_STATIC_LOCATION(_addr, _global) \ DVASSERT(static_allocated_one((uintptr_t)_addr), \
DVASSERT(IS_ON_STATIC(_addr, _global), \ "Operation on unallocated block [%a]\n ", _addr)
"Expected %s location: %a\n ", segstr(_global), _addr); \
DVASSERT(static_allocated_one((uintptr_t)_addr, _global), \
"Operation on unallocated %s block [%a]\n ", segstr(_global), _addr)
#else #else
/*! \cond exclude from doxygen */ /*! \cond exclude from doxygen */
# define DVALIDATE_SHADOW_LAYOUT # define DVALIDATE_SHADOW_LAYOUT
...@@ -281,35 +278,39 @@ static void validate_memory_layout() { ...@@ -281,35 +278,39 @@ static void validate_memory_layout() {
/* E-ACSL predicates {{{ */ /* E-ACSL predicates {{{ */
/* See definitions for documentation */ /* See definitions for documentation */
static uintptr_t heap_info(uintptr_t addr, char type); static uintptr_t heap_info(uintptr_t addr, char type);
static uintptr_t static_info(uintptr_t addr, char type, int global); static uintptr_t static_info(uintptr_t addr, char type);
static int heap_allocated(uintptr_t addr, size_t size); static int heap_allocated(uintptr_t addr, size_t size);
static int static_allocated(uintptr_t addr, long size, int global); static int static_allocated(uintptr_t addr, long size);
static int freeable(void *ptr); static int freeable(void *ptr);
/*! \brief Wrapper around ::static_allocated for stack addresses. */
#define stack_allocated(_addr, _size) static_allocated(_addr, _size, 0)
/*! \brief Wrapper around ::static_allocated for global addresses. */
#define global_allocated(_addr, _size) static_allocated(_addr, _size, 1)
/*! \brief Quick test to check if a static location belongs to allocation. /*! \brief Quick test to check if a static location belongs to allocation.
* This macro really belongs where static_allocated is defined, but * This macro really belongs where static_allocated is defined, but
* since it is used across this whole file it needs to be defined here. */ * since it is used across this whole file it needs to be defined here. */
#define static_allocated_one(addr, global) \ #define static_allocated_one(addr) \
((int)PRIMARY_SHADOW(addr, global)) ((int)PRIMARY_SHADOW(addr))
/*! \brief Shortcut for executing statements based on the segment a given
* address belongs to.
* \param intptr_t _addr - a memory address
* \param code_block _heap_stmt - code executed if `_addr` is a heap address
* \param code_block _static_stmt - code executed if `_addr` is a static address */
#define TRY_SEGMENT_WEAK(_addr, _heap_stmt, _static_stmt) \
if (IS_ON_HEAP(_addr)) { \
_heap_stmt; \
} else if (IS_ON_STATIC(_addr)) { \
_static_stmt; \
} \
/*! \brief Shortcut for executing statements based on the segment a given /*! \brief Shortcut for executing statements based on the segment a given
* address belongs to. * address belongs to.
* \param intptr_t _addr - a memory address * \param intptr_t _addr - a memory address
* \param code_block _heap_stmt - code executed if `_addr` is a heap address * \param code_block _heap_stmt - code executed if `_addr` is a heap address
* \param code_block _stack_stmt - code executed if `_addr` is a stack address * \param code_block _static_stmt - code executed if `_addr` is a static address */
* \param code_block _glob_stmt - code executed if `_addr` is a global address */ #define TRY_SEGMENT_WEAK(_addr, _heap_stmt, _static_stmt) \
#define TRY_SEGMENT_WEAK(_addr, _heap_stmt, _stack_stmt, _glob_stmt) \
if (IS_ON_HEAP(_addr)) { \ if (IS_ON_HEAP(_addr)) { \
_heap_stmt; \ _heap_stmt; \
} else if (IS_ON_STACK(_addr)) { \ } else if (IS_ON_STATIC(_addr)) { \
_stack_stmt; \ _static_stmt; \
} else if (IS_ON_GLOBAL(_addr)) { \
_glob_stmt; \
} \ } \
/*! \brief Same as TRY_SEGMENT but performs additional checks aborting the /*! \brief Same as TRY_SEGMENT but performs additional checks aborting the
...@@ -319,8 +320,8 @@ static int freeable(void *ptr); ...@@ -319,8 +320,8 @@ static int freeable(void *ptr);
* *
* The \b WEAK notion refers to the behaviour where no action is performed if * The \b WEAK notion refers to the behaviour where no action is performed if
* the given address does not belong to any of the known segments. */ * the given address does not belong to any of the known segments. */
#define TRY_SEGMENT(_addr, _heap_stmt, _stack_stmt, _glob_stmt) { \ #define TRY_SEGMENT(_addr, _heap_stmt, _static_stmt) { \
TRY_SEGMENT_WEAK(_addr, _heap_stmt, _stack_stmt, _glob_stmt) \ TRY_SEGMENT_WEAK(_addr, _heap_stmt, _static_stmt) \
else if (_addr == 0) { \ else if (_addr == 0) { \
vassert(0, "Unexpected null pointer\n", NULL); \ vassert(0, "Unexpected null pointer\n", NULL); \
} else { \ } else { \
...@@ -330,8 +331,8 @@ static int freeable(void *ptr); ...@@ -330,8 +331,8 @@ static int freeable(void *ptr);
/*! \brief Wrapper around ::heap_info and ::static_info functions that /*! \brief Wrapper around ::heap_info and ::static_info functions that
* dispatches one of the above functions based on the type of supplied memory * dispatches one of the above functions based on the type of supplied memory
* address (`addr`) (static, global or heap). For the case when the supplied * address (`addr`) (static, global, tls or heap). For the case when the
* address does not belong to the track segments 0 is returned. * supplied address does not belong to the track segments 0 is returned.
* *
* \param uintptr_t addr - a memory address * \param uintptr_t addr - a memory address
* \param char p - predicate type. See ::static_info for further details. */ * \param char p - predicate type. See ::static_info for further details. */
...@@ -339,8 +340,7 @@ static uintptr_t predicate(uintptr_t addr, char p) { ...@@ -339,8 +340,7 @@ static uintptr_t predicate(uintptr_t addr, char p) {
TRY_SEGMENT( TRY_SEGMENT(
addr, addr,
return heap_info((uintptr_t)addr, p), return heap_info((uintptr_t)addr, p),
return static_info((uintptr_t)addr, p, 0), return static_info((uintptr_t)addr, p));
return static_info((uintptr_t)addr, p, 1));
return 0; return 0;
} }
...@@ -369,20 +369,15 @@ static uintptr_t predicate(uintptr_t addr, char p) { ...@@ -369,20 +369,15 @@ static uintptr_t predicate(uintptr_t addr, char p) {
* and then for a block of 5 bytes its base offset if 11 etc. */ * and then for a block of 5 bytes its base offset if 11 etc. */
static const char short_offsets_base [] = { 0, 1, 2, 4, 7, 11, 16, 22, 29 }; static const char short_offsets_base [] = { 0, 1, 2, 4, 7, 11, 16, 22, 29 };
/*! \brief Stack or global memory-allocation. Record allocation of a /*! \brief Record allocation of a given memory block and update shadows
* given memory block and update shadows. * using offset-based encoding.
* *
* \param ptr - pointer to a base memory address of the stack memory block. * \param ptr - pointer to a base memory address of the stack memory block.
* \param size - size of the stack memory block. * \param size - size of the stack memory block. */
* \param global - if evaluates to a non-zero value then global region is used, static void shadow_alloca(void *ptr, size_t size) {
* otherwise program stack is used. */ unsigned char *prim_shadow = (unsigned char*)PRIMARY_SHADOW(ptr);
static void shadow_alloca(void *ptr, size_t size, int global) { uint64_t *prim_shadow_alt = (uint64_t *)PRIMARY_SHADOW(ptr);
unsigned char *prim_shadow = unsigned int *sec_shadow = (unsigned int*)SECONDARY_SHADOW(ptr);
(unsigned char*)PRIMARY_SHADOW(ptr, global);
uint64_t *prim_shadow_alt =
(uint64_t *)PRIMARY_SHADOW(ptr, global);
unsigned int *sec_shadow =
(unsigned int*)SECONDARY_SHADOW(ptr, global);
/* Flip read-only bit for zero-size blocks. That is, physically it exists /* Flip read-only bit for zero-size blocks. That is, physically it exists
* but one cannot write to it. Further, the flipped read-only bit will also * but one cannot write to it. Further, the flipped read-only bit will also
...@@ -413,43 +408,29 @@ static void shadow_alloca(void *ptr, size_t size, int global) { ...@@ -413,43 +408,29 @@ static void shadow_alloca(void *ptr, size_t size, int global) {
} }
} }
} }
/*! \brief Wrapper around ::shadow_alloca for stack blocks */
#define stack_shadow_alloca(_ptr, _size) shadow_alloca(_ptr, _size, 0)
/*! \brief Wrapper around ::shadow_alloca for global blocks */
#define global_shadow_alloca(_ptr, _size) shadow_alloca(_ptr, _size, 1)
/* }}} */ /* }}} */
/* Deletion of static blocks {{{ */ /* Deletion of static blocks {{{ */
/*! \brief Nullifies shadow regions of a memory block given by its address. /*! \brief Nullifies shadow regions of a memory block given by its address.
* \param ptr - base memory address of the stack memory block. * \param ptr - base memory address of the stack memory block. */
* \param global - if non-zero them `ptr` is assumed to carry a global address static void shadow_freea(void *ptr) {
* and a stack address otherwise */ DVALIDATE_STATIC_LOCATION(ptr);
static void static_shadow_freea(void *ptr, int global) {
DVALIDATE_STATIC_LOCATION(ptr, global);
DASSERT(ptr == (void*)base_addr(ptr)); DASSERT(ptr == (void*)base_addr(ptr));
size_t size = block_length(ptr); size_t size = block_length(ptr);
memset((void*)PRIMARY_SHADOW(ptr), 0, size);
memset((void*)PRIMARY_SHADOW(ptr, global), 0, size); memset((void*)SECONDARY_SHADOW(ptr), 0, size);
memset((void*)SECONDARY_SHADOW(ptr, global), 0, size);
} }
/*! \brief Wrapper around ::static_shadow_freea for stack addresses */
#define global_shadow_freea(_addr) static_shadow_freea(_addr, 1)
/*! \brief Wrapper around ::static_shadow_freea for global addresses */
#define stack_shadow_freea(_addr) static_shadow_freea(_addr, 0)
/* }}} */ /* }}} */
/* Static querying {{{ */ /* Static querying {{{ */
/*! \brief Return a non-zero value if a memory region of length `size` /*! \brief Return a non-zero value if a memory region of length `size`
* starting at address `addr` belongs to an allocated (tracked) stack or * starting at address `addr` belongs to a tracked stack, tls or
* global memory block and 0 otherwise. Note, this function is only safe if * global memory block and 0 otherwise.
* applied to a stack or global address. */ * This function is only safe if applied to a tls, stack or global address. */
static int static_allocated(uintptr_t addr, long size, int global) { static int static_allocated(uintptr_t addr, long size) {
unsigned char *prim_shadow = (unsigned char*)PRIMARY_SHADOW(addr, global); unsigned char *prim_shadow = (unsigned char*)PRIMARY_SHADOW(addr);
/* Unless the address belongs to tracked allocation 0 is returned */ /* Unless the address belongs to tracked allocation 0 is returned */
if (prim_shadow[0]) { if (prim_shadow[0]) {
unsigned int code = (prim_shadow[0] >> 2); unsigned int code = (prim_shadow[0] >> 2);
...@@ -458,7 +439,7 @@ static int static_allocated(uintptr_t addr, long size, int global) { ...@@ -458,7 +439,7 @@ static int static_allocated(uintptr_t addr, long size, int global) {
if (long_block) { if (long_block) {
offset = code - LONG_BLOCK_INDEX_START; offset = code - LONG_BLOCK_INDEX_START;
unsigned int *sec_shadow = unsigned int *sec_shadow =
(unsigned int*)SECONDARY_SHADOW(addr - offset, global) ; (unsigned int*)SECONDARY_SHADOW(addr - offset) ;
length = sec_shadow[0]; length = sec_shadow[0];
offset = sec_shadow[1] + offset; offset = sec_shadow[1] + offset;
} else { } else {
...@@ -470,21 +451,18 @@ static int static_allocated(uintptr_t addr, long size, int global) { ...@@ -470,21 +451,18 @@ static int static_allocated(uintptr_t addr, long size, int global) {
return 0; return 0;
} }
/*! \brief Return a non-zero value if a statically allocated memory block starting /*! \brief Return a non-zero value if a statically allocated memory block
* at `addr` of length `size` is fully initialized (i.e., each of its cells * starting at `addr` of length `size` is fully initialized (i.e., each of
* is initialized). If the third argument (`global`) evaluates to a non-zero * its cells is initialized). */
* value then the memory block is assumed to belong to the global allocation static int static_initialized(uintptr_t addr, long size) {
* and to the stack allocation otherwise. A 0 is returned if the given address
* does not belong to static allocation */
static int static_initialized(uintptr_t addr, long size, int global) {
/* Return 0 right away if the address does not belong to /* Return 0 right away if the address does not belong to
* static allocation */ * static allocation */
if (!static_allocated(addr, size, global)) if (!static_allocated(addr, size))
return 0; return 0;
DVALIDATE_STATIC_ACCESS(addr, size, global); DVALIDATE_STATIC_ACCESS(addr, size);
int result = 1; int result = 1;
uint64_t *shadow = (uint64_t*)PRIMARY_SHADOW(addr, global); uint64_t *shadow = (uint64_t*)PRIMARY_SHADOW(addr);
while (size > 0) { while (size > 0) {
int rem = (size >= ULONG_BYTES) ? ULONG_BYTES : size; int rem = (size >= ULONG_BYTES) ? ULONG_BYTES : size;
uint64_t mask = static_init_masks[rem]; uint64_t mask = static_init_masks[rem];
...@@ -498,13 +476,6 @@ static int static_initialized(uintptr_t addr, long size, int global) { ...@@ -498,13 +476,6 @@ static int static_initialized(uintptr_t addr, long size, int global) {
return result; return result;
} }
/*! \brief Wrapper around ::static_initialized for checking initialization of
* stack blocks */
#define stack_initialized(_addr, _size) static_initialized(_addr, _size, 0)
/*! \brief Wrapper around ::static_initialized for checking initialization of
* global blocks */
#define global_initialized(_addr, _size) static_initialized(_addr, _size, 1)
/*! \brief Checking whether a globally allocated memory block containing an /*! \brief Checking whether a globally allocated memory block containing an
* address _addr has read-only access. Note, this is light checking that * address _addr has read-only access. Note, this is light checking that
* relies on the fact that a single block cannot contain read/write and * relies on the fact that a single block cannot contain read/write and
...@@ -528,9 +499,9 @@ static int static_initialized(uintptr_t addr, long size, int global) { ...@@ -528,9 +499,9 @@ static int static_initialized(uintptr_t addr, long size, int global) {
* That is, for the cases when addr does not refer to a valid memory address * That is, for the cases when addr does not refer to a valid memory address
* belonging to static allocation the return value for this function is * belonging to static allocation the return value for this function is
* unspecified. */ * unspecified. */
static uintptr_t static_info(uintptr_t addr, char type, int global) { static uintptr_t static_info(uintptr_t addr, char type) {
DVALIDATE_STATIC_LOCATION(addr, global); DVALIDATE_STATIC_LOCATION(addr);
unsigned char *prim_shadow = (unsigned char*)PRIMARY_SHADOW(addr, global); unsigned char *prim_shadow = (unsigned char*)PRIMARY_SHADOW(addr);
/* Unless the address belongs to tracked allocation 0 is returned */ /* Unless the address belongs to tracked allocation 0 is returned */
if (prim_shadow[0]) { if (prim_shadow[0]) {
...@@ -539,7 +510,7 @@ static uintptr_t static_info(uintptr_t addr, char type, int global) { ...@@ -539,7 +510,7 @@ static uintptr_t static_info(uintptr_t addr, char type, int global) {
if (long_block) { if (long_block) {
unsigned int offset = code - LONG_BLOCK_INDEX_START; unsigned int offset = code - LONG_BLOCK_INDEX_START;
unsigned int *sec_shadow = unsigned int *sec_shadow =
(unsigned int*)SECONDARY_SHADOW(addr - offset, global) ; (unsigned int*)SECONDARY_SHADOW(addr - offset) ;
switch(type) { switch(type) {
case 'B': /* Base address */ case 'B': /* Base address */
return addr - offset - sec_shadow[1]; return addr - offset - sec_shadow[1];
...@@ -565,21 +536,14 @@ static uintptr_t static_info(uintptr_t addr, char type, int global) { ...@@ -565,21 +536,14 @@ static uintptr_t static_info(uintptr_t addr, char type, int global) {
} }
return 0; return 0;
} }
/*! \brief Wrapper around ::static_info for stack addresses */
#define stack_info(_addr, _pred) static_info(_addr, _pred, 0)
/*! \brief Wrapper around ::static_info for global addresses */
#define global_info(_addr, _pred) static_info(_addr, _pred, 1)
/* }}} */ /* }}} */
/* Static initialization {{{ */ /* Static initialization {{{ */
/*! \brief The following function marks n bytes starting from the address /*! \brief The following function marks n bytes starting from the address
* given by addr as initialized. `size` equating to zero indicates that the * given by addr as initialized. `size` equating to zero indicates that the
* whole block should be marked as initialized. Parameter global indicates * whole block should be marked as initialized. */
* the shadow region addr can be found in, such that 0 indicates stack static void initialize_static_region(uintptr_t addr, long size) {
* allocation and a non-zero value indicates global allocation. */ DVALIDATE_STATIC_ACCESS(addr, size);
static void initialize_static_region(uintptr_t addr, long size, int global) {
DVALIDATE_STATIC_ACCESS(addr, size, global);
DVASSERT(!(addr - base_addr(addr) + size > block_length(addr)), DVASSERT(!(addr - base_addr(addr) + size > block_length(addr)),
"Attempt to initialize %lu bytes past block boundaries\n" "Attempt to initialize %lu bytes past block boundaries\n"
"starting at %a with block length %lu at base address %a\n", "starting at %a with block length %lu at base address %a\n",
...@@ -607,7 +571,7 @@ static void initialize_static_region(uintptr_t addr, long size, int global) { ...@@ -607,7 +571,7 @@ static void initialize_static_region(uintptr_t addr, long size, int global) {
* That is, `*shadow |= static_init_masks[1]` will set only the least * That is, `*shadow |= static_init_masks[1]` will set only the least
* significant bit in *shadow. */ * significant bit in *shadow. */
uint64_t *shadow = (uint64_t*)PRIMARY_SHADOW(addr, global); uint64_t *shadow = (uint64_t*)PRIMARY_SHADOW(addr);
while (size > 0) { while (size > 0) {
int rem = (size >= ULONG_BYTES) ? ULONG_BYTES : size; int rem = (size >= ULONG_BYTES) ? ULONG_BYTES : size;
size -= ULONG_BYTES; size -= ULONG_BYTES;
...@@ -615,15 +579,6 @@ static void initialize_static_region(uintptr_t addr, long size, int global) { ...@@ -615,15 +579,6 @@ static void initialize_static_region(uintptr_t addr, long size, int global) {
shadow++; shadow++;
} }
} }
/*! \brief Wrapper around ::initialize_static_region for stack regions */
#define initialize_stack_region(_addr, _n) \
initialize_static_region(_addr, _n, 0)
/*! \brief Wrapper around ::initialize_static_region for global regions */
#define initialize_global_region(_addr, _n) \
initialize_static_region(_addr, _n, 1)
/* }}} */ /* }}} */
/* Read-only {{{ */ /* Read-only {{{ */
...@@ -635,7 +590,7 @@ static void mark_readonly (uintptr_t addr, long size) { ...@@ -635,7 +590,7 @@ static void mark_readonly (uintptr_t addr, long size) {
/* Since read-only blocks can only be stored in the globals segments (e.g., /* Since read-only blocks can only be stored in the globals segments (e.g.,
* TEXT), this function required ptr carry a global address. */ * TEXT), this function required ptr carry a global address. */
DASSERT(IS_ON_GLOBAL(addr)); DASSERT(IS_ON_GLOBAL(addr));
DASSERT(global_allocated(addr, 1)); DASSERT(static_allocated(addr, 1));
DVASSERT(!(addr - base_addr(addr) + size > block_length(addr)), DVASSERT(!(addr - base_addr(addr) + size > block_length(addr)),
"Attempt to mark read-only %lu bytes past block boundaries\n" "Attempt to mark read-only %lu bytes past block boundaries\n"
"starting at %a with block length %lu at base address %a\n", "starting at %a with block length %lu at base address %a\n",
...@@ -655,13 +610,13 @@ static void mark_readonly (uintptr_t addr, long size) { ...@@ -655,13 +610,13 @@ static void mark_readonly (uintptr_t addr, long size) {
/* Track program arguments (ARGC/ARGV) {{{ */ /* Track program arguments (ARGC/ARGV) {{{ */
static void argv_alloca(int argc, char ** argv) { static void argv_alloca(int argc, char ** argv) {
/* Track a top-level container (i.e., `*argv`) */ /* Track a top-level container (i.e., `*argv`) */
stack_shadow_alloca(argv, (argc + 1)*sizeof(char*)); shadow_alloca(argv, (argc + 1)*sizeof(char*));
initialize_stack_region((uintptr_t)argv, (argc + 1)*sizeof(char*)); initialize_static_region((uintptr_t)argv, (argc + 1)*sizeof(char*));
/* Track argument strings */ /* Track argument strings */
while (*argv) { while (*argv) {
size_t arglen = strlen(*argv) + 1; size_t arglen = strlen(*argv) + 1;
stack_shadow_alloca(*argv, arglen); shadow_alloca(*argv, arglen);
initialize_stack_region((uintptr_t)*argv, arglen); initialize_static_region((uintptr_t)*argv, arglen);
argv++; argv++;
} }
} }
...@@ -1105,8 +1060,7 @@ static void initialize(void *ptr, size_t n) { ...@@ -1105,8 +1060,7 @@ static void initialize(void *ptr, size_t n) {
TRY_SEGMENT( TRY_SEGMENT(
(uintptr_t)ptr, (uintptr_t)ptr,
initialize_heap_region((uintptr_t)ptr, n), initialize_heap_region((uintptr_t)ptr, n),
initialize_stack_region((uintptr_t)ptr, n), initialize_static_region((uintptr_t)ptr, n)
initialize_global_region((uintptr_t)ptr, n)
) )
} }
/* }}} */ /* }}} */
...@@ -1129,12 +1083,12 @@ static void printbyte(unsigned char c, char buf[]) { ...@@ -1129,12 +1083,12 @@ static void printbyte(unsigned char c, char buf[]) {
/*! \brief Print human-readable (well, ish) representation of a memory block /*! \brief Print human-readable (well, ish) representation of a memory block
* using primary and secondary shadows. */ * using primary and secondary shadows. */
static void print_static_shadows(uintptr_t addr, size_t size, int global) { static void print_static_shadows(uintptr_t addr, size_t size) {
char prim_buf[256]; char prim_buf[256];
char sec_buf[256]; char sec_buf[256];
unsigned char *prim_shadow = (unsigned char*)PRIMARY_SHADOW(addr, global); unsigned char *prim_shadow = (unsigned char*)PRIMARY_SHADOW(addr);
unsigned int *sec_shadow = (unsigned int*)SECONDARY_SHADOW(addr, global); unsigned int *sec_shadow = (unsigned int*)SECONDARY_SHADOW(addr);
int i, j = 0; int i, j = 0;
for (i = 0; i < size; i++) { for (i = 0; i < size; i++) {
...@@ -1154,9 +1108,6 @@ static void print_static_shadows(uintptr_t addr, size_t size, int global) { ...@@ -1154,9 +1108,6 @@ static void print_static_shadows(uintptr_t addr, size_t size, int global) {
} }
} }
#define print_stack_shadows(addr, size) print_static_shadows(addr, size, 0)
#define print_global_shadows(addr, size) print_static_shadows(addr, size, 1)
/*! \brief Print human-readable representation of a heap shadow region for a /*! \brief Print human-readable representation of a heap shadow region for a
* memory block of length `size` starting at address `addr`. */ * memory block of length `size` starting at address `addr`. */
static void print_heap_shadows(uintptr_t addr, size_t size) { static void print_heap_shadows(uintptr_t addr, size_t size) {
...@@ -1177,10 +1128,8 @@ static void print_heap_shadows(uintptr_t addr, size_t size) { ...@@ -1177,10 +1128,8 @@ static void print_heap_shadows(uintptr_t addr, size_t size) {
} }
static void print_shadows(uintptr_t addr, size_t size) { static void print_shadows(uintptr_t addr, size_t size) {
if (IS_ON_STACK(addr)) if (IS_ON_STATIC(addr))
print_stack_shadows(addr, size); print_static_shadows(addr, size);
if (IS_ON_GLOBAL(addr))
print_global_shadows(addr, size);
else if (IS_ON_HEAP(addr)) else if (IS_ON_HEAP(addr))
print_heap_shadows(addr, size); print_heap_shadows(addr, size);
} }
......
src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h
+ 11
− 12
View file @ 0aba9984
...@@ -398,16 +398,15 @@ static void clean_memory_layout() { ...@@ -398,16 +398,15 @@ static void clean_memory_layout() {
#define SECONDARY_TLS_SHADOW(_addr) \ #define SECONDARY_TLS_SHADOW(_addr) \
HIGHER_SHADOW_ACCESS(_addr, mem_layout.tls.sec_offset) HIGHER_SHADOW_ACCESS(_addr, mem_layout.tls.sec_offset)
/*! \brief Select stack or global shadow based on the value of `_global` #define SHADOW_REGION_ADDRESS(_addr, _region) \
* (IS_ON_STACK(_addr) ? _region##_STACK_SHADOW(_addr) : \
* - PRIMARY_SHADOW(_addr, 0) is equivalent to PRIMARY_STACK_SHADOW(_addr) IS_ON_GLOBAL(_addr) ? _region##_GLOBAL_SHADOW(_addr) : \
* - PRIMARY_SHADOW(_addr, 1) is equivalent to PRIMARY_GLOBAL_SHADOW(_addr) */ IS_ON_TLS(_addr) ? _region##_TLS_SHADOW(_addr) : 0)
#define PRIMARY_SHADOW(_addr, _global) \
(_global ? PRIMARY_GLOBAL_SHADOW(_addr) : PRIMARY_STACK_SHADOW(_addr))
/*! \brief Same as above but for secondary stack/global shadows */ /*! \brief Primary shadow address of a non-dynamic region */
#define SECONDARY_SHADOW(_addr, _global) \ #define PRIMARY_SHADOW(_addr) SHADOW_REGION_ADDRESS(_addr, PRIMARY)
(_global ? SECONDARY_GLOBAL_SHADOW(_addr) : SECONDARY_STACK_SHADOW(_addr)) /*! \brief Secondary shadow address of a non-dynamic region */
#define SECONDARY_SHADOW(_addr) SHADOW_REGION_ADDRESS(_addr, SECONDARY)
/*! \brief Convert a heap address into its shadow counterpart */ /*! \brief Convert a heap address into its shadow counterpart */
#define HEAP_SHADOW(_addr) \ #define HEAP_SHADOW(_addr) \
...@@ -436,11 +435,11 @@ static void clean_memory_layout() { ...@@ -436,11 +435,11 @@ static void clean_memory_layout() {
/*! \brief Shortcut for evaluating an address via ::IS_ON_STACK or /*! \brief Shortcut for evaluating an address via ::IS_ON_STACK or
* ::IS_ON_GLOBAL based on the value of the second parameter */ * ::IS_ON_GLOBAL based on the value of the second parameter */
#define IS_ON_STATIC(_addr, _global) \ #define IS_ON_STATIC(_addr) \
(_global ? IS_ON_GLOBAL(_addr) : IS_ON_STACK(_addr)) (IS_ON_STACK(_addr) || IS_ON_GLOBAL(_addr) || IS_ON_TLS(_addr))
/*! \brief Evaluate to a true value if a given address belongs to tracked /*! \brief Evaluate to a true value if a given address belongs to tracked
* allocation (i.e., found within stack, heap or globally) */ * allocation (i.e., found within stack, heap or globally) */
#define IS_ON_VALID(_addr) \ #define IS_ON_VALID(_addr) \
(IS_ON_STACK(_addr) || IS_ON_HEAP(_addr) || IS_ON_GLOBAL(_addr)) (IS_ON_STACK(_addr) || IS_ON_HEAP(_addr) || IS_ON_GLOBAL(_addr) || IS_ON_TLS(_addr))
/* }}} */ /* }}} */
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment