diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
index 24963982abf4105729497815964daef086a88026..bb394a59ac9f8316287f85d421c77bb1d2fc451e 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
@@ -151,7 +151,9 @@ static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
increase_stack_limit(get_stack_size()*2);
/* Allocate and log shadow memory layout of the execution. */
init_memory_layout(argc_ref, argv_ref);
+ /* Make sure the layout holds and output it (only in debug mode) */
DEBUG_PRINT_LAYOUT;
+ DVALIDATE_SHADOW_LAYOUT;
/* Track program arguments. */
if (argc_ref && argv_ref)
argv_alloca(*argc_ref, *argv_ref);
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
index e1fb8c7bebb93ba1f091d6050ae82ec7b639ff20..10b20224d31c199aa419d93f513ce1c17940954b 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
@@ -194,37 +194,61 @@ const uint64_t static_readonly_masks [] = {
};
/* }}} */
-/* E-ACSL predicates {{{ */
-/* See definitions for documentation */
-static uintptr_t heap_info(uintptr_t addr, char type);
-static uintptr_t static_info(uintptr_t addr, char type, int global);
-static int heap_allocated(uintptr_t addr, size_t size);
-static int static_allocated(uintptr_t addr, long size, int global);
-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.
- * This macro really belongs where static_allocated is defined, but
- * since it is used across this whole file it needs to be defined here. */
-#define static_allocated_one(addr, global) \
- ((int)PRIMARY_SHADOW(addr, global))
-
-/* Runtime assertions */
-#define VALIDATE_ALIGNMENT(_addr) \
- vassert(((uintptr_t)_addr) % HEAP_SEGMENT == 0, \
+/* Runtime assertions (debug mode) {{{ */
+#ifdef E_ACSL_DEBUG
+#define DVALIDATE_ALIGNMENT(_addr) \
+ DVASSERT(((uintptr_t)_addr) % HEAP_SEGMENT == 0, \
"Heap base address %a is unaligned", _addr)
-/* Debug-level macros for validating memory accesses and allocation */
-#ifdef E_ACSL_DEBUG
-# define DVALIDATE_SHADOW_LAYOUT \
- DVASSERT(mem_layout.initialized != 0, "Un-initialized shadow layout", NULL)
+/* Debug function making sure that the order of program segments is as expected
+ * and that the program and the shadow segments used do not overlap. */
+static void validate_memory_layout() {
+ /* Check that the struct holding memory layout is marked as initialized. */
+ DVASSERT(mem_layout.initialized != 0, "Un-initialized shadow layout", NULL);
+ /* Make sure the order of program segments is as expected, i.e.,
+ * top to bittom: stack -> tls -> heap -> global*/
+
+ #define NO_MEM_SEGMENTS 11
+ uintptr_t segments[NO_MEM_SEGMENTS][2] = {
+ {mem_layout.stack.start, mem_layout.stack.end},
+ {mem_layout.stack.prim_start, mem_layout.stack.prim_end},
+ {mem_layout.stack.sec_start, mem_layout.stack.sec_end},
+ {mem_layout.tls.start, mem_layout.tls.end},
+ {mem_layout.tls.prim_start, mem_layout.tls.prim_end},
+ {mem_layout.tls.sec_start, mem_layout.tls.sec_end},
+ {mem_layout.global.start, mem_layout.global.end},
+ {mem_layout.global.prim_start, mem_layout.global.prim_end},
+ {mem_layout.global.sec_start, mem_layout.global.sec_end},
+ {mem_layout.heap.start, mem_layout.heap.end},
+ {mem_layout.heap.prim_start, mem_layout.heap.prim_end}
+ };
+
+ /* Make sure all segments (shadow or otherwise) are disjoint */
+ size_t i, j;
+ for (int i = 0; i < NO_MEM_SEGMENTS; i++) {
+ uintptr_t *src = segments[i];
+ DVASSERT(src[0] < src[1],
+ "Segment start is greater than segment end %lu < %lu\n", src[0], src[1]);
+ for (int j = 0; j < NO_MEM_SEGMENTS; j++) {
+ if (i != j) {
+ uintptr_t *dest = segments[j];
+ DVASSERT(src[1] < dest[0] || src[0] > dest[1],
+ "Segment [%lu, %lu] overlaps with segment [%lu, %lu]",
+ src[0], src[1], dest[0], dest[1]);
+ }
+ }
+ }
+ DVASSERT(mem_layout.stack.end > mem_layout.tls.end,
+ "Unexpected location of stack (above tls)", NULL);
+ DVASSERT(mem_layout.tls.end > mem_layout.heap.end,
+ "Unexpected location of tls (above heap)", NULL);
+ DVASSERT(mem_layout.heap.end > mem_layout.global.end,
+ "Unexpected location of heap (above global)", NULL);
+}
+
+# define DVALIDATE_SHADOW_LAYOUT validate_memory_layout()
# define DVALIDATE_HEAP_ACCESS(_addr, _size) \
- DVALIDATE_SHADOW_LAYOUT; \
DVASSERT(IS_ON_HEAP(_addr), \
"Expected heap location: %a\n ", _addr); \
DVASSERT(heap_allocated((uintptr_t)_addr, _size), \
@@ -232,7 +256,6 @@ static int freeable(void *ptr);
# define segstr(_global) ((_global) ? "global" : "stack")
# define DVALIDATE_STATIC_ACCESS(_addr, _size, _global) \
- DVALIDATE_SHADOW_LAYOUT; \
DVASSERT(IS_ON_STATIC(_addr, _global), \
"Expected %s location: %a\n ", segstr(_global), _addr); \
DVASSERT(static_allocated((uintptr_t)_addr, _size, _global), \
@@ -240,7 +263,6 @@ static int freeable(void *ptr);
segstr(_global), _addr, _size)
# define DVALIDATE_STATIC_LOCATION(_addr, _global) \
- DVALIDATE_SHADOW_LAYOUT; \
DVASSERT(IS_ON_STATIC(_addr, _global), \
"Expected %s location: %a\n ", segstr(_global), _addr); \
DVASSERT(static_allocated_one((uintptr_t)_addr, _global), \
@@ -251,8 +273,29 @@ static int freeable(void *ptr);
# define DVALIDATE_HEAP_ACCESS
# define DVALIDATE_STATIC_ACCESS
# define DVALIDATE_STATIC_LOCATION
+# define DVALIDATE_ALIGNMENT
/*! \endcond */
#endif
+/* }}} */
+
+/* E-ACSL predicates {{{ */
+/* See definitions for documentation */
+static uintptr_t heap_info(uintptr_t addr, char type);
+static uintptr_t static_info(uintptr_t addr, char type, int global);
+static int heap_allocated(uintptr_t addr, size_t size);
+static int static_allocated(uintptr_t addr, long size, int global);
+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.
+ * This macro really belongs where static_allocated is defined, but
+ * since it is used across this whole file it needs to be defined here. */
+#define static_allocated_one(addr, global) \
+ ((int)PRIMARY_SHADOW(addr, global))
/*! \brief Shortcut for executing statements based on the segment a given
* address belongs to.
@@ -334,8 +377,6 @@ static const char short_offsets_base [] = { 0, 1, 2, 4, 7, 11, 16, 22, 29 };
* \param global - if evaluates to a non-zero value then global region is used,
* otherwise program stack is used. */
static void shadow_alloca(void *ptr, size_t size, int global) {
- DVALIDATE_SHADOW_LAYOUT;
-
unsigned char *prim_shadow =
(unsigned char*)PRIMARY_SHADOW(ptr, global);
uint64_t *prim_shadow_alt =
@@ -408,7 +449,6 @@ static void static_shadow_freea(void *ptr, int global) {
* global memory block and 0 otherwise. Note, this function is only safe if
* applied to a stack or global address. */
static int static_allocated(uintptr_t addr, long size, int global) {
- DVALIDATE_SHADOW_LAYOUT;
unsigned char *prim_shadow = (unsigned char*)PRIMARY_SHADOW(addr, global);
/* Unless the address belongs to tracked allocation 0 is returned */
if (prim_shadow[0]) {
@@ -594,7 +634,6 @@ static void initialize_static_region(uintptr_t addr, long size, int global) {
static void mark_readonly (uintptr_t addr, long size) {
/* Since read-only blocks can only be stored in the globals segments (e.g.,
* TEXT), this function required ptr carry a global address. */
- DVALIDATE_SHADOW_LAYOUT;
DASSERT(IS_ON_GLOBAL(addr));
DASSERT(global_allocated(addr, 1));
DVASSERT(!(addr - base_addr(addr) + size > block_length(addr)),
@@ -643,7 +682,7 @@ static void set_heap_segment(void *ptr, size_t size, size_t init) {
if (!ptr)
return;
- VALIDATE_ALIGNMENT(ptr); /* Make sure alignment is right */
+ DVALIDATE_ALIGNMENT(ptr); /* Make sure alignment is right */
heap_allocation_size += size; /* Adjuct tracked allocation size */
/* Get aligned size of the block, i.e., an actual size of the
@@ -736,7 +775,6 @@ static void* shadow_calloc(size_t nmemb, size_t size) {
/* Heap deallocation (free) {{{ */
static void shadow_free(void *res) {
char *ptr = (char *)res;
- DVALIDATE_SHADOW_LAYOUT;
if (ptr != NULL) { /* NULL is a valid behaviour */
if (freeable(ptr)) {
size_t size = block_length(ptr);
@@ -754,7 +792,6 @@ static void shadow_free(void *res) {
/* Heap reallocation (realloc) {{{ */
static void* shadow_realloc(void *p, size_t size) {
- DVALIDATE_SHADOW_LAYOUT;
char *ptr = (char*)p;
char *res = NULL; /* Resulting pointer */
/* If the pointer is NULL then realloc is equivalent to malloc(size) */
@@ -768,7 +805,7 @@ static void* shadow_realloc(void *p, size_t size) {
if (freeable(ptr)) { /* ... and valid for free */
size_t alloc_size = ALLOC_SIZE(size);
res = native_realloc(ptr - HEAP_SEGMENT, alloc_size);
- VALIDATE_ALIGNMENT(res);
+ DVALIDATE_ALIGNMENT(res);
/* realloc succeeds, otherwise nothing needs to be done */
if (res != NULL) {
@@ -892,7 +929,6 @@ static int shadow_posix_memalign(void **memptr, size_t alignment, size_t size) {
* block and a 0 otherwise. Note, this function is only safe if applied to a
* heap address. */
static int heap_allocated(uintptr_t addr, size_t size) {
- DVALIDATE_SHADOW_LAYOUT;
/* Offset within the segment */
size_t block_offset = addr%HEAP_SEGMENT;
/* Address of the shadow segment the address belongs to */
@@ -925,7 +961,6 @@ static int heap_allocated(uintptr_t addr, size_t size) {
* implementation is preferred for performance reasons. */
static int freeable(void *ptr) {
uintptr_t addr = (uintptr_t)ptr;
- DVALIDATE_SHADOW_LAYOUT;
if (!IS_ON_HEAP(addr))
return 0;
/* Offset within the segment */
@@ -942,7 +977,6 @@ static int freeable(void *ptr) {
* memory. NB: If `addr` does not belong to a valid heap region this function
* returns 0. */
static int heap_initialized(uintptr_t addr, long len) {
- DVALIDATE_SHADOW_LAYOUT;
/* Unallocated heap address */
if (!heap_allocated(addr, len))
return 0;
@@ -1068,7 +1102,6 @@ static void initialize_heap_region(uintptr_t addr, long len) {
/*! \brief Initialize a chunk of memory given by its start address (`addr`)
* and byte length (`n`). */
static void initialize(void *ptr, size_t n) {
- DVALIDATE_SHADOW_LAYOUT;
TRY_SEGMENT(
(uintptr_t)ptr,
initialize_heap_region((uintptr_t)ptr, n),
@@ -1078,7 +1111,7 @@ static void initialize(void *ptr, size_t n) {
}
/* }}} */
-/* Internal state print {{{ */
+/* Internal state print (debug mode) {{{ */
#ifdef E_ACSL_DEBUG
/* ! \brief Print human-readable representation of a byte in a primary
* shadow */
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h
index 796ada15b3f7fa7e0e14a2986569467942cfcc68..12b0b9f56f73db1eba5c18f42a3906e02d7340f4 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h
@@ -253,19 +253,19 @@ NOTE: With mmap allocations heap does not necessarily grows from program break
* shadow spaces. */
struct memory_segment {
uintptr_t start; //!< Least address in application segment
- uintptr_t end; //!< Greatest address in application segment
+ uintptr_t end; //!< Greatest address in application segment
size_t shadow_size; //!< Byte-size of shadow area
- uintptr_t prim_start; //!< Least address in primary shadow
- uintptr_t prim_end; //!< Greatest address in primary shadow
+ uintptr_t prim_start; //!< Least address in primary shadow
+ uintptr_t prim_end; //!< Greatest address in primary shadow
uintptr_t prim_offset; //!< Primary shadow offset
- uintptr_t sec_start; //!< Least address secondary shadow
- uintptr_t sec_end; //!< Greatest address secondary shadow
+ uintptr_t sec_start; //!< Least address secondary shadow
+ uintptr_t sec_end; //!< Greatest address secondary shadow
uintptr_t sec_offset; //!< Secondary shadow offset
- int initialized;
+ int initialized; //! Notion on whether the layout is initialized
};
/*! \brief Full program memory layout. */
@@ -283,18 +283,18 @@ struct memory_layout {
static void set_shadow_segment(struct memory_segment *seg, uintptr_t start,
uintptr_t size, int secondary) {
seg->start = start;
- seg->end = seg->start + size;
+ seg->end = seg->start + size - 1;
seg->shadow_size = size;
void *prim_shadow = do_mmap(seg->shadow_size);
seg->prim_start = (uintptr_t)prim_shadow;
- seg->prim_end = seg->prim_start + seg->shadow_size;
+ seg->prim_end = seg->prim_start + seg->shadow_size - 1;
seg->prim_offset = shadow_offset(prim_shadow, start);
if (secondary) {
void *sec_shadow = do_mmap(seg->shadow_size);
seg->sec_start = (uintptr_t)sec_shadow;
- seg->sec_end = seg->sec_start + seg->shadow_size;
+ seg->sec_end = seg->sec_start + seg->shadow_size - 1;
seg->sec_offset = shadow_offset(sec_shadow, seg->start);
} else {
seg->sec_start = seg->sec_end = seg->sec_offset = 0;