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 9385d11fa79f8aeeaafc9aaa96d3ad72d98c0c9e..96c5b76e1288414dcd4d17e8d81dfd1c8a91eb11 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
@@ -26,13 +26,16 @@
* model. See e_acsl_mmodel_api.h for details.
***************************************************************************/
-static int valid(void*, size_t, void*, void*);
-static int valid_read(void*, size_t, void*, void*);
-
#include "e_acsl_shadow_layout.h"
#include "e_acsl_segment_tracking.h"
#include "e_acsl_mmodel_api.h"
+/* Forward declarations */
+static int valid(void*, size_t, void*, void*);
+static int valid_read(void*, size_t, void*, void*);
+
+#define ALLOCATED(_ptr,_size) allocated((uintptr_t)_ptr, _size, (uintptr_t)_ptr)
+
static void * store_block(void * ptr, size_t size) {
/* Only stack-global memory blocks are recorded explicitly via this function.
* Heap blocks should be tracked internally using memory allocation functions
@@ -62,9 +65,9 @@ static void mark_readonly(void * ptr) {
mark_readonly_region((uintptr_t)ptr, block_length(ptr));
}
-/* ****************** */
-/* E-ACSL annotations */
-/* ****************** */
+/* ********************** */
+/* E-ACSL annotations {{{ */
+/* ********************** */
/** \brief Return 1 if a given memory location is read-only and 0 otherwise */
static int readonly (void *ptr) {
@@ -72,11 +75,13 @@ static int readonly (void *ptr) {
return IS_ON_GLOBAL(addr) && global_readonly(addr) ? 1 : 0;
}
-static int valid(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
- return allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base) && !readonly(ptr);
+static int valid(void * ptr, size_t size, void *ptr_base, void *addrof_base) {
+ return
+ allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base) &&
+ !readonly(ptr);
}
-static int valid_read(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
+static int valid_read(void * ptr, size_t size, void *ptr_base, void *addrof_base) {
return allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base);
}
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 75983f80bbb4296aaf809db2c37c5ca93b31d1ce..2cce518310298d074f5a4fe8a43fc243a842ac68 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
@@ -353,6 +353,25 @@ static void validate_memory_layout() {
} \
}
+/* Assert neither of `_len` addresses immediately preceding `_addr` are
+ * base addresses of some other block and that `_len` addresses past
+ * `_addr` are free */
+#define DVALIDATE_STATIC_SUFFICIENTLY_ALIGNED(_addr, _len) { \
+ int _i; \
+ for (_i = 0; _i < _len; _i++) { \
+ uintptr_t _prev = _addr - _i; \
+ if (static_allocated_one(_prev)) { \
+ vassert(base_addr(_prev) != _prev, \
+ "Potential backward overlap of: \n previous block [%a]\n" \
+ " with allocated block [%a]\n", _prev, _addr); \
+ } \
+ uintptr_t _next = _addr + _i; \
+ vassert(!static_allocated_one(_next), \
+ "Potential forward overlap of:\n following block location [%a]\n" \
+ " with allocated block [%a]\n", _next, _addr); \
+ } \
+}
+
/* Assert that a memory block [_addr, _addr + _size] is nullified */
# define DVALIDATE_NULLIFIED(_addr, _size) \
DVASSERT(zeroed_out((void *)_addr, _size), \
@@ -369,7 +388,7 @@ static void validate_memory_layout() {
# define DVALIDATE_RW_ACCESS(_addr, _size) { \
DVALIDATE_ALLOCATED((uintptr_t)_addr, _size, (uintptr_t)_addr); \
DVASSERT(!readonly((void*)_addr), \
- "Unexpected readonly address: %lu\n", _addr) \
+ "Unexpected readonly address: %lu\n", _addr); \
}
/* Assert that memory block [_addr, _addr + _size] is allocated */
@@ -396,13 +415,21 @@ static void validate_memory_layout() {
# define DVALIDATE_HEAP_FREE
# define DVALIDATE_RO_ACCESS
# define DVALIDATE_RW_ACCESS
-# define DVALIDATE_ALLOCATED
+# define DVALIDATE_ALLOCATED
+# define DVALIDATE_STATIC_SUFFICIENTLY_ALIGNED
/*! \endcond */
#endif
/* }}} */
+/* Runtime assertions {{{ */
+#define VALIDATE_HEAP_ALLOCATION(_res, _size) \
+ vassert(mem_layout.heap.end > (uintptr_t)_res + _size, \
+ "e-acsl error: Insufficient heap size %lu\n", E_ACSL_HEAP_SIZE);
+/* }}} */
+
/* E-ACSL predicates {{{ */
/* See definitions for documentation */
+static void *shadow_copy(const void *ptr, size_t size, int init);
static uintptr_t heap_info(uintptr_t addr, char type);
static uintptr_t static_info(uintptr_t addr, char type);
static int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr);
@@ -825,8 +852,11 @@ static void* shadow_malloc(size_t size) {
char* res = alloc_size ?
(char*)native_aligned_alloc(HEAP_SEGMENT, alloc_size) : NULL;
- if (res)
+ if (res) {
+ /* Make sure there is sufficient room in shadow */
+ VALIDATE_HEAP_ALLOCATION(res, alloc_size);
set_heap_segment(res, size, alloc_size, 0, "malloc");
+ }
return res;
}
@@ -843,15 +873,23 @@ static void* shadow_calloc(size_t nmemb, size_t size) {
/* Since aligned size is required by the model do the allocation through
* `malloc` and nullify the memory space by hand */
- char* res = size ? (char*)native_malloc(alloc_size) : NULL;
+ char* res =
+ size ? (char*)native_aligned_alloc(HEAP_SEGMENT, alloc_size) : NULL;
if (res) {
+ /* Make sure there is sufficient room in shadow */
+ VALIDATE_HEAP_ALLOCATION(res, alloc_size);
memset(res, 0, size);
set_heap_segment(res, size, alloc_size, 1, "calloc");
}
-
return res;
}
+
+/** \brief Return shadowed copy of a memory chunk on a program's heap */
+static void *shadow_copy(const void *ptr, size_t size, int init) {
+ char *ret = (init) ? shadow_calloc(1, size) : shadow_malloc(size);
+ return memcpy(ret, ptr, size);
+}
/* }}} */
/* Heap deallocation (free) {{{ */
@@ -908,6 +946,7 @@ static void* shadow_realloc(void *ptr, size_t size) {
if (freeable(ptr)) { /* ... and can be used as an input to `free` */
size_t alloc_size = ALLOC_SIZE(size);
res = native_realloc(ptr, alloc_size);
+ VALIDATE_HEAP_ALLOCATION(res, alloc_size);
DVALIDATE_ALIGNMENT(res);
/* realloc succeeds, otherwise nothing needs to be done */
@@ -965,8 +1004,11 @@ static void *shadow_aligned_alloc(size_t alignment, size_t size) {
return NULL;
char *res = native_aligned_alloc(alignment, size);
- if (res)
+
+ if (res) {
+ VALIDATE_HEAP_ALLOCATION(res, ALLOC_SIZE(size));
set_heap_segment(res, size, ALLOC_SIZE(size), 0, "aligned_alloc");
+ }
return (void*)res;
}
@@ -987,6 +1029,7 @@ static int shadow_posix_memalign(void **memptr, size_t alignment, size_t size) {
int res = native_posix_memalign(memptr, alignment, size);
if (!res) {
+ VALIDATE_HEAP_ALLOCATION(*memptr, ALLOC_SIZE(size));
set_heap_segment(*memptr, size, ALLOC_SIZE(size), 0, "posix_memalign");
}
return res;
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 f2490f3164db9695de05dd67b7205f15ec3e0abb..ef8d8ed379d90dd9ed383f40981e4a85d1d9bd84 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
@@ -25,6 +25,16 @@
* \brief Setup for memory tracking using shadowing
***************************************************************************/
+/* Default size of a program's heap tracked via shadow memory */
+#ifndef E_ACSL_HEAP_SIZE
+#define E_ACSL_HEAP_SIZE 512
+#endif
+
+/* Default size of a program's stack tracked via shadow memory */
+#ifndef E_ACSL_STACK_SIZE
+#define E_ACSL_STACK_SIZE 64
+#endif
+
/* Symbols exported by the linker script */
/*!\brief The first address past the end of the text segment. */
@@ -68,7 +78,7 @@ char *strerror(int errnum);
/** Hardcoded sizes of tracked program segments {{{ */
/*! \brief Size of a program's heap */
-#define PGM_HEAP_SIZE (512 * MB)
+#define PGM_HEAP_SIZE (E_ACSL_HEAP_SIZE * MB)
/*! \brief Size of a program's Thread-local storage (TLS) */
#define PGM_TLS_SIZE (16 * MB)
@@ -117,14 +127,40 @@ static uintptr_t get_tls_start() {
/** Program stack information {{{ */
extern char ** environ;
+/*! \brief Set a new soft stack limit
+ * \param size - new stack size in bytes */
+static size_t increase_stack_limit(const size_t size) {
+ const rlim_t stacksz = (rlim_t)size;
+ struct rlimit rl;
+ int result = getrlimit(RLIMIT_STACK, &rl);
+ if (result == 0) {
+ if (rl.rlim_cur < stacksz) {
+ rl.rlim_cur = stacksz;
+ result = setrlimit(RLIMIT_STACK, &rl);
+ if (result != 0) {
+ vabort("setrlimit: %s \n", strerror(errno));
+ }
+ }
+ }
+ return size;
+}
+
/*! \brief Return byte-size of a program's stack. The return value is the soft
* stack limit, i.e., it can be programmatically increased at runtime. */
-static size_t get_stack_size() {
+static size_t get_default_stack_size() {
struct rlimit rlim;
assert(!getrlimit(RLIMIT_STACK, &rlim));
return rlim.rlim_cur;
}
+static size_t get_stack_size() {
+#ifndef E_ACSL_STACK_SIZE
+ return get_default_stack_size();
+#else
+ return increase_stack_limit(E_ACSL_STACK_SIZE*MB);
+#endif
+}
+
/*! \brief Return greatest (known) address on a program's stack.
* This function presently determines the address using the address of the
* last string in `environ`. That is, it assumes that argc and argv are
@@ -145,23 +181,6 @@ static uintptr_t get_stack_start(int *argc_ref, char *** argv_ref) {
uintptr_t stack_start = stack_end - get_stack_size();
return stack_start;
}
-
-/*! \brief Set a new soft stack limit
- * \param size - new stack size in bytes */
-static void increase_stack_limit(const size_t size) {
- const rlim_t stacksz = (rlim_t)size;
- struct rlimit rl;
- int result = getrlimit(RLIMIT_STACK, &rl);
- if (result == 0) {
- if (rl.rlim_cur < stacksz) {
- rl.rlim_cur = stacksz;
- result = setrlimit(RLIMIT_STACK, &rl);
- if (result != 0) {
- vabort("setrlimit: %s \n", strerror(errno));
- }
- }
- }
-}
/* }}} */
/** Program heap information {{{ */
@@ -345,7 +364,7 @@ static void set_shadow_segment(struct memory_segment *seg, uintptr_t start,
* allocate shadow memory spaces and compute offsets. This function populates
* global struct ::mem_layout holding that information with data. */
static void init_memory_layout(int *argc_ref, char ***argv_ref) {
- /* Use DEBUG_PRINT_LAYOUT to output the details (if they are needed) */
+ /* Use DEBUG_PRINT_LAYOUT to output the details */
set_shadow_segment(&mem_layout.heap,
get_heap_start(), get_heap_size(), 1, 8, "heap");
set_shadow_segment(&mem_layout.stack,
@@ -367,7 +386,6 @@ void clean_memory_segment(struct memory_segment *seg) {
/*! \brief Deallocate shadow regions used by runtime analysis */
static void clean_memory_layout() {
- DLOG("<<< Clean shadow layout >>>\n");
if (mem_layout.initialized) {
clean_memory_segment(&mem_layout.heap);
clean_memory_segment(&mem_layout.stack);