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 c1553b7d0b1522944e20bfa89be3e53c188ce7d2..24963982abf4105729497815964daef086a88026 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
@@ -136,21 +136,29 @@ static int initialized(void * ptr, size_t size) {
return 0;
}
-static size_t get_heap_size(void) {
- return heap_size;
+static size_t get_heap_allocation_size(void) {
+ return heap_allocation_size;
}
static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
+ /** Verify that the given size of a pointer matches the one in the present
+ * architecture. This is a guard against Frama-C instrumentations using
+ * architectures different to the given one. */
arch_assert(ptr_size);
+ /* Initialize report file with debug logs (only in debug mode). */
initialize_report_file(argc_ref, argv_ref);
- init_pgm_layout(argc_ref, argv_ref);
+ /* Lift stack limit to account for extra stack memory overhead. */
+ increase_stack_limit(get_stack_size()*2);
+ /* Allocate and log shadow memory layout of the execution. */
+ init_memory_layout(argc_ref, argv_ref);
+ DEBUG_PRINT_LAYOUT;
+ /* Track program arguments. */
if (argc_ref && argv_ref)
argv_alloca(*argc_ref, *argv_ref);
- DEBUG_PRINT_LAYOUT;
}
static void memory_clean(void) {
- clean_pgm_layout();
+ clean_memory_layout();
}
/* API BINDINGS {{{ */
@@ -181,6 +189,6 @@ public_alias(full_init)
public_alias(memory_clean)
public_alias(memory_init)
/* Heap size */
-public_alias(get_heap_size)
-public_alias(heap_size)
+public_alias(get_heap_allocation_size)
+public_alias(heap_allocation_size)
/* }}} */
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 abc3fdc4405344d6602dadb44f8010d4c04a2ce2..ebc8c99abef6253f19a0f4e6774c782112acce8f 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
@@ -43,10 +43,10 @@
/*! \brief Size (in bytes) of a long block on the stack. */
#define LONG_BLOCK 8
-/*! \brief Bit offset in a short shadow byte that represents initialization. */
+/*! \brief Bit offset in a primary shadow byte that represents initialization. */
#define INIT_BIT 0
-/*! \brief Bit offset in a short shadow byte that represents read-only or
+/*! \brief Bit offset in a primary shadow byte that represents read-only or
* read-write access.
*
* This is such that the value of 1 is read-only, and 0 is read/write */
@@ -67,16 +67,16 @@
/*! \brief Short shadow of a long block consists of a 8-byte segment + a
* remainder. For instance, a 18-byte block is represented by two 8-byte
- * segments + 2 bytes. Each byte of a segment stores an offset in the long
+ * segments + 2 bytes. Each byte of a segment stores an offset in the secondary
* shadow. The offsets for each such segment can be expressed using the
* following number obtained by compressing all eight bytes with offsets set
* into a single block. */
#define LONG_BLOCK_MASK 15913703276567643328UL
/*! \brief 6 higher bytes of a memory cell on stack that belongs to a long
- * memory block store offsets relative to meta-data in long shadow. The offsets
- * start with the below number. E.g., if the bits store 51, then the offset at
- * which to read meta-data is (51 - 48). */
+ * memory block store offsets relative to meta-data in the secondary shadow. The
+ * offsets start with the below number. E.g., if the bits store 51, then the
+ * offset at which to read meta-data is (51 - 48). */
#define LONG_BLOCK_INDEX_START 48
/*! \brief Increase the size to a multiple of a segment size. */
@@ -211,7 +211,7 @@ static int freeable(void *ptr);
* 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)SHORT_SHADOW(addr, global))
+ ((int)PRIMARY_SHADOW(addr, global))
/* Runtime assertions */
#define VALIDATE_ALIGNMENT(_addr) \
@@ -221,7 +221,7 @@ static int freeable(void *ptr);
/* Debug-level macros for validating memory accesses and allocation */
#ifdef E_ACSL_DEBUG
# define DVALIDATE_SHADOW_LAYOUT \
- DVASSERT(pgm_layout.initialized != 0, "Un-initialized shadow layout", NULL)
+ DVASSERT(mem_layout.initialized != 0, "Un-initialized shadow layout", NULL)
# define DVALIDATE_HEAP_ACCESS(_addr, _size) \
DVALIDATE_SHADOW_LAYOUT; \
@@ -326,8 +326,8 @@ static uintptr_t predicate(uintptr_t addr, char p) {
* 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 };
-/*! \brief Static (stack or global) memory-allocation. Record allocation of a
- * given memory block and update shadow regions.
+/*! \brief Stack or global memory-allocation. Record allocation of a
+ * given memory block and update shadows.
*
* \param ptr - pointer to a base memory address of the stack memory block.
* \param size - size of the stack memory block.
@@ -337,11 +337,11 @@ static void shadow_alloca(void *ptr, size_t size, int global) {
DVALIDATE_SHADOW_LAYOUT;
unsigned char *short_shadowed =
- (unsigned char*)SHORT_SHADOW((uintptr_t)ptr, global);
+ (unsigned char*)PRIMARY_SHADOW(ptr, global);
uint64_t *short_shadowed_alt =
- (uint64_t *)SHORT_SHADOW((uintptr_t)ptr, global);
+ (uint64_t *)PRIMARY_SHADOW(ptr, global);
unsigned int *long_shadowed =
- (unsigned int*)LONG_SHADOW((uintptr_t)ptr, global);
+ (unsigned int*)SECONDARY_SHADOW(ptr, global);
/* 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
@@ -391,8 +391,8 @@ static void static_shadow_freea(void *ptr, int global) {
size_t size = block_length(ptr);
- memset((void*)SHORT_SHADOW(ptr, global), 0, size);
- memset((void*)LONG_SHADOW(ptr, global), 0, size);
+ memset((void*)PRIMARY_SHADOW(ptr, global), 0, size);
+ memset((void*)SECONDARY_SHADOW(ptr, global), 0, size);
}
/*! \brief Wrapper around ::static_shadow_freea for stack addresses */
@@ -409,7 +409,7 @@ static void static_shadow_freea(void *ptr, int global) {
* applied to a stack or global address. */
static int static_allocated(uintptr_t addr, long size, int global) {
DVALIDATE_SHADOW_LAYOUT;
- unsigned char *short_shadowed = (unsigned char*)SHORT_SHADOW(addr, global);
+ unsigned char *short_shadowed = (unsigned char*)PRIMARY_SHADOW(addr, global);
/* Unless the address belongs to tracked allocation 0 is returned */
if (short_shadowed[0]) {
unsigned int code = (short_shadowed[0] >> 2);
@@ -418,7 +418,7 @@ static int static_allocated(uintptr_t addr, long size, int global) {
if (long_block) {
offset = code - LONG_BLOCK_INDEX_START;
unsigned int *long_shadowed =
- (unsigned int*)LONG_SHADOW(addr - offset, global) ;
+ (unsigned int*)SECONDARY_SHADOW(addr - offset, global) ;
length = long_shadowed[0];
offset = long_shadowed[1] + offset;
} else {
@@ -444,7 +444,7 @@ static int static_initialized(uintptr_t addr, long size, int global) {
DVALIDATE_STATIC_ACCESS(addr, size, global);
int result = 1;
- uint64_t *shadow = (uint64_t*)SHORT_SHADOW(addr, global);
+ uint64_t *shadow = (uint64_t*)PRIMARY_SHADOW(addr, global);
while (size > 0) {
int rem = (size >= ULONG_BYTES) ? ULONG_BYTES : size;
uint64_t mask = static_init_masks[rem];
@@ -471,7 +471,7 @@ static int static_initialized(uintptr_t addr, long size, int global) {
* read-only parts, that is to check whether the block has read-only access it
* is sufficient to check any of its bytes. */
#define global_readonly(_addr) \
- checkbit(READONLY_BIT, (*(char*)SHORT_GLOBAL_SHADOW(addr)))
+ checkbit(READONLY_BIT, (*(char*)PRIMARY_GLOBAL_SHADOW(addr)))
/*! \brief Querying information about a specific global or stack memory address
* (based on the value of parameter `global'). The return value is interpreted
@@ -490,7 +490,7 @@ static int static_initialized(uintptr_t addr, long size, int global) {
* unspecified. */
static uintptr_t static_info(uintptr_t addr, char type, int global) {
DVALIDATE_STATIC_LOCATION(addr, global);
- unsigned char *short_shadowed = (unsigned char*)SHORT_SHADOW(addr, global);
+ unsigned char *short_shadowed = (unsigned char*)PRIMARY_SHADOW(addr, global);
/* Unless the address belongs to tracked allocation 0 is returned */
if (short_shadowed[0]) {
@@ -499,7 +499,7 @@ static uintptr_t static_info(uintptr_t addr, char type, int global) {
if (long_block) {
unsigned int offset = code - LONG_BLOCK_INDEX_START;
unsigned int *long_shadowed =
- (unsigned int*)LONG_SHADOW(addr - offset, global) ;
+ (unsigned int*)SECONDARY_SHADOW(addr - offset, global) ;
switch(type) {
case 'B': /* Base address */
return addr - offset - long_shadowed[1];
@@ -567,7 +567,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
* significant bit in *shadow. */
- uint64_t *shadow = (uint64_t*)SHORT_SHADOW(addr, global);
+ uint64_t *shadow = (uint64_t*)PRIMARY_SHADOW(addr, global);
while (size > 0) {
int rem = (size >= ULONG_BYTES) ? ULONG_BYTES : size;
size -= ULONG_BYTES;
@@ -603,7 +603,7 @@ static void mark_readonly (uintptr_t addr, long size) {
size, addr, block_length(addr), base_addr(addr));
/* See comments in ::initialize_static_region for details */
- uint64_t *shadow = (uint64_t*)SHORT_GLOBAL_SHADOW(addr);
+ uint64_t *shadow = (uint64_t*)PRIMARY_GLOBAL_SHADOW(addr);
while (size > 0) {
int rem = (size >= ULONG_BYTES) ? ULONG_BYTES : size;
size -= ULONG_BYTES;
@@ -632,7 +632,7 @@ static void argv_alloca(int argc, char ** argv) {
/*! \brief Amount of heap memory allocated by the program.
* Variable visible externally. */
-static size_t heap_size = 0;
+static size_t heap_allocation_size = 0;
/*! \brief Create a heap shadow for an allocated memory block starting at `ptr`
* and of length `size`. Optionally mark it as initialized if `init`
@@ -644,7 +644,7 @@ static void set_heap_segment(void *ptr, size_t size, size_t init) {
return;
VALIDATE_ALIGNMENT(ptr); /* Make sure alignment is right */
- heap_size += size; /* Adjuct tracked allocation size */
+ heap_allocation_size += size; /* Adjuct tracked allocation size */
/* Get aligned size of the block, i.e., an actual size of the
* allocated block */
@@ -743,8 +743,8 @@ static void shadow_free(void *res) {
void *meta_shadow = (void*)(HEAP_SHADOW(ptr) - HEAP_SEGMENT);
memset(meta_shadow, 0, HEAP_SHADOW_BLOCK_SIZE(size));
native_free(ptr - HEAP_SEGMENT);
- /* Adjuct tracked allocation size carried via `__e_acsl_heap_size` */
- heap_size -= size;
+ /* Adjuct tracked allocation size carried via `__e_acsl_heap_allocation_size` */
+ heap_allocation_size -= size;
} else {
vabort("Not a start of block (%a) in free\n", ptr);
}
@@ -780,7 +780,7 @@ static void* shadow_realloc(void *p, size_t size) {
/* Number of block segments in the new allocation */
size_t new_segments = BLOCK_SEGMENTS(size);
/* Adjuct tracked allocation size */
- heap_size += -old_size + size;
+ heap_allocation_size += -old_size + size;
/* Address of the meta-block in old allocation */
uintptr_t *meta_shadow = (uintptr_t*)(HEAP_SHADOW(ptr) - HEAP_SEGMENT);
@@ -1080,7 +1080,7 @@ static void initialize(void *ptr, size_t n) {
/* Internal state print {{{ */
#ifdef E_ACSL_DEBUG
-/* ! \brief Print human-readable representation of a byte in a short (byte)
+/* ! \brief Print human-readable representation of a byte in a primary
* shadow */
static void printbyte(unsigned char c, char buf[]) {
if (c >> 2 < LONG_BLOCK_INDEX_START) {
@@ -1095,13 +1095,13 @@ static void printbyte(unsigned char c, char buf[]) {
}
/*! \brief Print human-readable (well, ish) representation of a memory block
- * using short (byte) and long (block) shadow regions */
+ * using primary and secondary shadows. */
static void print_static_shadows(uintptr_t addr, size_t size, int global) {
char short_buf[256];
char long_buf[256];
- unsigned char *short_shadowed = (unsigned char*)SHORT_SHADOW(addr, global);
- unsigned int *long_shadowed = (unsigned int*)LONG_SHADOW(addr, global);
+ unsigned char *short_shadowed = (unsigned char*)PRIMARY_SHADOW(addr, global);
+ unsigned int *long_shadowed = (unsigned int*)SECONDARY_SHADOW(addr, global);
int i, j = 0;
for (i = 0; i < size; i++) {
@@ -1152,60 +1152,27 @@ static void print_shadows(uintptr_t addr, size_t size) {
print_heap_shadows(addr, size);
}
-static void print_pgm_layout() {
- DLOG("| --- Stack ------------------------------------\n");
- DLOG("|Stack Shadow Size: %16lu MB\n",
- MB_SZ(pgm_layout.stack_shadow_size));
- DLOG("|Stack Start: %19lu\n", pgm_layout.stack_start);
- DLOG("|Stack End: %19lu\n", pgm_layout.stack_end);
- DLOG("|Stack Soft Bound: %19lu\n", pgm_layout.stack_soft_bound);
- DLOG("| --- Short Stack Shadow -----------------------\n");
- DLOG("|Short Stack Shadow Offset: %19lu\n",
- pgm_layout.short_stack_shadow_offset);
- DLOG("|Short Stack Shadow Start: %19lu\n",
- pgm_layout.short_stack_shadow_start);
- DLOG("|Short Stack Shadow End: %19lu\n",
- pgm_layout.short_stack_shadow_end);
- DLOG("| --- Long Stack Shadow ------------------------\n");
- DLOG("|Long Stack Shadow Offset: %19lu\n",
- pgm_layout.long_stack_shadow_offset);
- DLOG("|Long Stack Shadow Start: %19lu\n",
- pgm_layout.long_stack_shadow_start);
- DLOG("|Long Stack Shadow End: %19lu\n",
- pgm_layout.long_stack_shadow_end);
- DLOG("| --- Heap -------------------------------------\n");
- DLOG("|Heap Shadow Size: %16lu MB\n",
- MB_SZ(pgm_layout.heap_shadow_size));
- DLOG("|Heap Shadow Offset: %19lu\n", pgm_layout.heap_shadow_offset);
- DLOG("|Heap Start: %19lu\n", pgm_layout.heap_start);
- DLOG("|Heap End: %19lu\n", pgm_layout.heap_end);
- DLOG("|Heap Shadow Start: %19lu\n", pgm_layout.heap_shadow_start);
- DLOG("|Heap Shadow End: %19lu\n", pgm_layout.heap_shadow_end);
- DLOG("| --- Global -----------------------------------\n");
- DLOG("|Global Shadow Size: %16lu MB\n", MB_SZ(pgm_layout.global_shadow_size));
- DLOG("|Global Start: %19lu\n", pgm_layout.global_start);
- DLOG("|Global End: %19lu\n", pgm_layout.global_end);
- DLOG("| --- Short Global Shadow ----------------------\n");
- DLOG("|Short Global Shadow Offset: %19lu\n", pgm_layout.short_global_shadow_offset);
- DLOG("|Short Global Shadow Start: %19lu\n", pgm_layout.short_global_shadow_start);
- DLOG("|Short Global Shadow End: %19lu\n", pgm_layout.short_global_shadow_end);
- DLOG("| --- Long Global Shadow -----------------------\n");
- DLOG("|Long Global Shadow Offset: %19lu\n", pgm_layout.long_global_shadow_offset);
- DLOG("|Long Global Shadow Start: %19lu\n", pgm_layout.long_global_shadow_start);
- DLOG("|Long Global Shadow End: %19lu\n", pgm_layout.long_global_shadow_end);
- DLOG("| --- TLS -----------------------------------\n");
- DLOG("|TLS Shadow Size: %16lu MB\n", MB_SZ(pgm_layout.tls_shadow_size));
- DLOG("|TLS Start: %19lu\n", pgm_layout.tls_start);
- DLOG("|TLS End: %19lu\n", pgm_layout.tls_end);
- DLOG("| --- Short TLS Shadow ----------------------\n");
- DLOG("|Short TLS Shadow Offset: %19lu\n", pgm_layout.short_tls_shadow_offset);
- DLOG("|Short TLS Shadow Start: %19lu\n", pgm_layout.short_tls_shadow_start);
- DLOG("|Short TLS Shadow End: %19lu\n", pgm_layout.short_tls_shadow_end);
- DLOG("| --- Long TLS Shadow -----------------------\n");
- DLOG("|Long TLS Shadow Offset: %19lu\n", pgm_layout.long_tls_shadow_offset);
- DLOG("|Long TLS Shadow Start: %19lu\n", pgm_layout.long_tls_shadow_start);
- DLOG("|Long TLS Shadow End: %19lu\n", pgm_layout.long_tls_shadow_end);
- DLOG("------------------------------------------------\n");
+static void print_memory_segment(struct memory_segment *seg, const char *name) {
+ DLOG(" --- %s ------------------------------------------\n", name);
+ DLOG("%s Shadow Size: %16lu MB\n", name, MB_SZ(seg->shadow_size));
+ DLOG("%s Start: %19lu\n", name, seg->start);
+ DLOG("%s End: %19lu\n", name, seg->end);
+ DLOG("%s Primary Shadow Offset: %19lu\n", name, seg->prim_offset);
+ DLOG("%s Primary Shadow Start: %19lu\n", name, seg->prim_start);
+ DLOG("%s Primary Shadow End: %19lu\n", name, seg->prim_end);
+ if (seg->sec_start) {
+ DLOG("%s Secondary Shadow Offset: %19lu\n", name, seg->sec_offset);
+ DLOG("%s Secondary Shadow Start: %19lu\n", name, seg->sec_start);
+ DLOG("%s Secondary Shadow End: %19lu\n", name, seg->sec_end);
+ }
+}
+
+static void print_memory_layout() {
+ print_memory_segment(&mem_layout.heap, "Heap");
+ print_memory_segment(&mem_layout.stack, "Stack");
+ print_memory_segment(&mem_layout.global, "Global");
+ print_memory_segment(&mem_layout.tls, "TLS");
+ DLOG("-----------------------------------------------------\n");
}
/*! \brief Output the shadow segment the address belongs to */
@@ -1229,7 +1196,7 @@ static void which_segment(uintptr_t addr) {
/*! \brief Print program layout. This function outputs start/end addresses of
* various program segments, their shadow counterparts and sizes of shadow
* regions used. */
-#define DEBUG_PRINT_LAYOUT print_pgm_layout()
+#define DEBUG_PRINT_LAYOUT print_memory_layout()
void ___e_acsl_debug_print_layout() { DEBUG_PRINT_LAYOUT; }
/*! \brief Print the shadow segment address addr belongs to */
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 896d6c272c1843922f842a4d980397b893b886ff..73f591d3909083416f4304ca05cf06a476fac4d3 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,8 +25,7 @@
* \brief Setup for memory tracking using shadowing
***************************************************************************/
-/*! \brief The first address past the end of the uninitialized data (BSS)
- * segment . */
+/*! \brief The first address past the end of BSS segment */
extern char end;
/* \cond */
@@ -49,15 +48,6 @@ char *strerror(int errnum);
#define MB_SZ(_s) (_s/MB) //!< Convert bytes to megabytes
#define GB_SZ(_s) (_s/GB) //!< Convert bytes to gigabytes
-/*! \brief Size of the heap shadow */
-#define HEAP_SHADOW_SIZE (1024 * MB)
-
-/*! \brief Size of a stack shadow */
-#define STACK_SHADOW_SIZE (72 * MB)
-
-/*! \brief Size of the TLS shadow */
-#define TLS_SHADOW_SIZE (64 * MB)
-
/*! \brief Pointer size (in bytes) for a given system */
#define PTR_SZ sizeof(uintptr_t)
@@ -68,7 +58,15 @@ char *strerror(int errnum);
#define ULONG_BYTES 8
#define ULONG_BITS 64
-/* Thread-local storage information {{{ */
+/** Hardcoded sizes of tracked program segments {{{ */
+/*! \brief Size of the heap segment */
+#define PGM_HEAP_SIZE (256 * MB)
+
+/*! \brief Size of the TLS segment */
+#define PGM_TLS_SIZE (8 * MB)
+/* }}} */
+
+/** Thread-local storage information {{{ */
/*! Thread-local storage (TLS) keeps track of copies of per-thread variables.
* Even though at the present stage RTL of E-ACSL is not thread-safe, some
@@ -90,32 +88,43 @@ char *strerror(int errnum);
* start TLS address (&id_bss - TLS_SHADOW_SIZE/2)
*/
+/*! Get byte-size of TLS segment */
+static size_t get_tls_size() {
+ return PGM_TLS_SIZE;
+}
+
static __thread int id_tdata = 1;
static __thread int id_tbss;
/*! Set TLS size and its end and start addresses. */
-static void set_tls_bounds(uintptr_t *tls_end,
- uintptr_t *tls_start, uintptr_t *tls_size) {
- uintptr_t
- data = (uintptr_t)&id_tdata,
- bss = (uintptr_t)&id_tbss;
-
- *tls_end = ((data > bss) ? data : bss) + TLS_SHADOW_SIZE/2;
- *tls_start = ((data > bss) ? bss : data) - TLS_SHADOW_SIZE/2,
- *tls_size = *tls_end - *tls_start;
+static uintptr_t get_tls_start() {
+ size_t tls_size = get_tls_size();
+ uintptr_t data = (uintptr_t)&id_tdata,
+ bss = (uintptr_t)&id_tbss;
+ return ((data > bss ? bss : data) - tls_size/2);
}
+
/* }}} */
-/* Program stack information {{{ */
+/** Program stack information {{{ */
extern char ** environ;
+/*! \brief Get the stack size (in bytes) as used by the program. The return
+ * value is the soft stack limit, i.e., it can be programmatically increased
+ * at runtime */
+static size_t get_stack_size() {
+ struct rlimit rlim;
+ assert(!getrlimit(RLIMIT_STACK, &rlim));
+ return rlim.rlim_cur;
+}
+
/*! \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
* stored below environ, which holds for GCC/GLIBC but is not necessarily
* true. In general, a reliable way of detecting the upper bound of a stack
* segment is needed. */
-static uintptr_t get_stack_end(int *argc_ref, char *** argv_ref) {
+static uintptr_t get_stack_start(int *argc_ref, char *** argv_ref) {
char **env = environ;
while (env[1])
env++;
@@ -126,16 +135,9 @@ static uintptr_t get_stack_end(int *argc_ref, char *** argv_ref) {
* to be able to set initialization and read-only bits ::ULONG_BITS
* at a time. If not respected, this may cause a segfault in
* ::argv_alloca. */
- return addr + ULONG_BITS;
-}
-
-/*! \brief Get the stack size (in bytes) as used by the program. The return
- * value is the soft stack limit, i.e., it can be programmatically increased
- * at runtime */
-static size_t get_stack_size() {
- struct rlimit rlim;
- assert(!getrlimit(RLIMIT_STACK, &rlim));
- return rlim.rlim_cur;
+ uintptr_t stack_end = addr + ULONG_BITS;
+ uintptr_t stack_start = stack_end - get_stack_size();
+ return stack_start;
}
/*! \brief Set a new stack limit
@@ -156,6 +158,30 @@ static void increase_stack_limit(const size_t size) {
}
/* }}} */
+/** Program heap information {{{ */
+static uintptr_t get_heap_start() {
+ return (uintptr_t)sbrk(0);
+}
+
+static size_t get_heap_size() {
+ return PGM_HEAP_SIZE;
+}
+/** }}} */
+
+/** Program global information {{{ */
+static uintptr_t get_global_start() {
+ return (uintptr_t)(PTR_SZ*2);
+}
+
+/*! \brief Get byte-size of global segment */
+static size_t get_global_size() {
+/* In all likelihood it is reasonably safe to assume that first
+ * 2x*pointer-size bytes of the memory space will not be used. */
+ return ((uintptr_t)&end - get_global_start());
+}
+/** }}} */
+
+
/** MMAP allocation {{{ */
/*! \brief Allocate a memory block of `size` bytes with `mmap` and return a
* pointer to its base address. Since this function is used to set-up shadowing
@@ -176,15 +202,12 @@ static void *do_mmap(size_t size) {
* start address of a segment */
static uintptr_t shadow_offset(void *shadow, uintptr_t start_addr) {
uintptr_t start_shadow = (uintptr_t)shadow;
-
return (start_shadow > start_addr) ?
start_shadow - start_addr : start_addr - start_shadow;
}
/* }}} */
-/* Program Layout {{{ */
-
-
+/** Program Layout {{{ */
/*****************************************************************************
* Memory Layout *************************************************************
*****************************************************************************
@@ -227,197 +250,89 @@ NOTE: With mmap allocations heap does not necessarily grows from program break
upwards from program break.
*/
-static struct program_layout pgm_layout;
-
-/*! \brief Structure for tracking shadow regions and boundaries of memory
- * segments. */
-struct program_layout {
- uintptr_t stack_start; //!< Least address in program stack
- uintptr_t stack_end; //!< Greatest address in program stack.
- uintptr_t stack_soft_bound; /*!< \brief Address of the soft stack bound.
- A program using stack addresses beyond (i.e., less than) the soft bound
- runs into a stack overflow. */
- size_t stack_shadow_size; /*!< \brief Size (in bytes) of a stack shadow.
- Same size if used for short and long shadow regions. */
-
- uintptr_t short_stack_shadow_start; //!< Least address in short shadow region
- uintptr_t short_stack_shadow_end; //!< Greatest address in short shadow region
- uintptr_t short_stack_shadow_offset; /*!< \brief Short shadow offset.
- The offset is kept as a positive (unsigned) integer
- relative to the stack shadow region situated below the stack. That is,
- to get a shadow address from an actual one the offset needs to be
- subtracted. */
-
- uintptr_t long_stack_shadow_start; //!< Least address in long shadow region
- uintptr_t long_stack_shadow_end; //!< Greatest address in long shadow region
- uintptr_t long_stack_shadow_offset; /*!< \brief Long shadow offset. Similar
- to #short_stack_shadow_offset */
-
- uintptr_t heap_start; //!< Least address in a program's heap.
- uintptr_t heap_end; //!< Greatest address in a program's heap.
-
- uintptr_t heap_shadow_start; /*!< \brief Least address in a program's shadow
- heap region. */
- uintptr_t heap_shadow_end; /*!< \brief Greatest address in a program's
- shadow heap region. */
- size_t heap_shadow_size; //!< Size (in bytes) of the heap shadow region. */
- uintptr_t heap_shadow_offset; /*!< \brief Short shadow offset.
- * The offset is kept as a positive (unsigned) integer
- * relative to the heap shadow region situated above the heap. That is,
- * unlike stack shadow, to get a shadow address from an actual one the
- * offset needs to be added. */
-
- /* Same as `stack_...` but for shadowing globals */
- uintptr_t global_end;
- uintptr_t global_start;
- size_t global_shadow_size;
-
- uintptr_t short_global_shadow_end;
- uintptr_t short_global_shadow_start;
- uintptr_t short_global_shadow_offset;
-
- uintptr_t long_global_shadow_end;
- uintptr_t long_global_shadow_start;
- uintptr_t long_global_shadow_offset;
-
- /* Same as `global_...` but for shadowing thread-local storage */
- uintptr_t tls_end;
- uintptr_t tls_start;
- size_t tls_shadow_size;
-
- uintptr_t short_tls_shadow_end;
- uintptr_t short_tls_shadow_start;
- uintptr_t short_tls_shadow_offset;
-
- uintptr_t long_tls_shadow_end;
- uintptr_t long_tls_shadow_start;
- uintptr_t long_tls_shadow_offset;
-
- /*! Carries a non-zero value if shadow layout has been initialized and
- * evaluates to zero otherwise. */
+struct memory_segment {
+ uintptr_t start; //!< Least address
+ uintptr_t end; //!< Greatest address
+
+ size_t shadow_size; //!< Byte-size of 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 in secondary shadow
+ uintptr_t sec_end; //!< Greatest address in secondary shadow
+ uintptr_t sec_offset; //!< Secondary shadow offset
+
int initialized;
};
-/*! \brief Setting program layout for analysys, namely:
- * - Detect boundaries of different program segments
- * - Allocate shadow regions (1 heap region + 2 stack regions)
- * - Compute shadow offsets
- *
- * *TODO*: This function should be a part of ::__e_acsl_memory_init visible
- * externally */
-static void init_pgm_layout(int *argc_ref, char ***argv_ref) {
- DLOG("<<< Initialize shadow layout >>>\n");
- /* Setting up stack. Stack grows downwards starting from the stack end
- * address initialization. */
- pgm_layout.stack_shadow_size = STACK_SHADOW_SIZE;
- pgm_layout.stack_end = get_stack_end(argc_ref, argv_ref);
- pgm_layout.stack_start =
- pgm_layout.stack_end - pgm_layout.stack_shadow_size;
- /* Soft bound can be increased programmatically, thus detecting
- * stack overflows using this stack bound needs to take into account such
- * changes. Very approximate for the moment, */
- pgm_layout.stack_soft_bound = pgm_layout.stack_end - get_stack_size();
-
- /* Primary stack shadow region */
- void * short_stack_shadow = do_mmap(pgm_layout.stack_shadow_size);
- pgm_layout.short_stack_shadow_start = (uintptr_t)short_stack_shadow;
- pgm_layout.short_stack_shadow_end =
- (uintptr_t)short_stack_shadow + pgm_layout.stack_shadow_size;
- pgm_layout.short_stack_shadow_offset =
- shadow_offset(short_stack_shadow, pgm_layout.stack_start);
-
- /* Secondary stack shadow region */
- void *long_stack_shadow = do_mmap(pgm_layout.stack_shadow_size);
- pgm_layout.long_stack_shadow_start = (uintptr_t)long_stack_shadow;
- pgm_layout.long_stack_shadow_end =
- (uintptr_t)long_stack_shadow + pgm_layout.stack_shadow_size;
- pgm_layout.long_stack_shadow_offset =
- shadow_offset(long_stack_shadow, pgm_layout.stack_start);
-
- /* Setting heap. Heap grows upwards starting from the current program break.
- Alternative approach would be to use the end of BSS but in fact the end of
- BSS and the current program break are not really close to each other, so
- some space will be wasted. Another reason is that sbrk is likely to return
- an aligned address which makes the access faster. */
- pgm_layout.heap_start = (uintptr_t)sbrk(0);
- pgm_layout.heap_shadow_size = HEAP_SHADOW_SIZE;
- pgm_layout.heap_end = pgm_layout.heap_start + pgm_layout.heap_shadow_size;
-
- void* heap_shadow = do_mmap(pgm_layout.heap_shadow_size);
- pgm_layout.heap_shadow_start = (uintptr_t)heap_shadow;
- pgm_layout.heap_shadow_end =
- (uintptr_t)heap_shadow + pgm_layout.heap_shadow_size;
- pgm_layout.heap_shadow_offset =
- shadow_offset(heap_shadow, pgm_layout.heap_start);
-
- /* Setting shadow for globals */
- /* In all likelihood it is reasonably safe to assume that first
- * 2x*pointer-size bytes of the memory space will not be used. */
- pgm_layout.global_start = PTR_SZ*2;
- pgm_layout.global_end = (uintptr_t)&end;
- pgm_layout.global_shadow_size
- = pgm_layout.global_end - pgm_layout.global_start;
-
- /* Primary global shadow region */
- void * short_global_shadow = do_mmap(pgm_layout.global_shadow_size);
- pgm_layout.short_global_shadow_start = (uintptr_t)short_global_shadow;
- pgm_layout.short_global_shadow_end =
- (uintptr_t)short_global_shadow + pgm_layout.global_shadow_size;
- pgm_layout.short_global_shadow_offset =
- shadow_offset(short_global_shadow, pgm_layout.global_start);
-
- /* Secondary global shadow */
- void *long_global_shadow = do_mmap(pgm_layout.global_shadow_size);
- pgm_layout.long_global_shadow_start = (uintptr_t)long_global_shadow;
- pgm_layout.long_global_shadow_end =
- (uintptr_t)long_global_shadow + pgm_layout.global_shadow_size;
- pgm_layout.long_global_shadow_offset =
- shadow_offset(long_global_shadow, pgm_layout.global_start);
-
- /* Setting shadow for thread-local storage (TLS). */
- set_tls_bounds(&pgm_layout.tls_end, &pgm_layout.tls_start,
- &pgm_layout.tls_shadow_size);
-
- /* Primary TLS shadow */
- void * short_tls_shadow = do_mmap(pgm_layout.tls_shadow_size);
- pgm_layout.short_tls_shadow_start = (uintptr_t)short_tls_shadow;
- pgm_layout.short_tls_shadow_end =
- (uintptr_t)short_tls_shadow + pgm_layout.tls_shadow_size;
- pgm_layout.short_tls_shadow_offset =
- shadow_offset(short_tls_shadow, pgm_layout.tls_start);
-
- /* Secondary TLS shadow */
- void *long_tls_shadow = do_mmap(pgm_layout.tls_shadow_size);
- pgm_layout.long_tls_shadow_start = (uintptr_t)long_tls_shadow;
- pgm_layout.long_tls_shadow_end =
- (uintptr_t)long_tls_shadow + pgm_layout.tls_shadow_size;
- pgm_layout.long_tls_shadow_offset =
- shadow_offset(long_tls_shadow, pgm_layout.tls_start);
-
- /* The shadow layout has been initialized */
- pgm_layout.initialized = 1;
+static struct memory_layout mem_layout;
+
+struct memory_layout {
+ struct memory_segment heap;
+ struct memory_segment stack;
+ struct memory_segment global;
+ struct memory_segment tls;
+ int initialized;
+};
+
+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->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_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_offset = shadow_offset(sec_shadow, seg->start);
+ } else {
+ seg->sec_start = seg->sec_end = seg->sec_offset = 0;
+ }
}
-/*! \brief Unmap (de-allocate) shadow regions used by runtime analysis */
-static void clean_pgm_layout() {
+static void init_memory_layout(int *argc_ref, char ***argv_ref) {
+ DLOG("<<< Initialize heap shadow >>>\n");
+ struct memory_segment *heap = &mem_layout.heap;
+ set_shadow_segment(heap, get_heap_start(), get_heap_size(), 0);
+
+ DLOG("<<< Initialize stack shadow >>>\n");
+ struct memory_segment *stack = &mem_layout.stack;
+ set_shadow_segment(stack, get_stack_start(argc_ref, argv_ref), get_stack_size(), 1);
+
+ DLOG("<<< Initialize global shadow >>>\n");
+ struct memory_segment *global = &mem_layout.global;
+ set_shadow_segment(global, get_global_start(), get_global_size(), 1);
+
+ DLOG("<<< Initialize TLS shadow >>>\n");
+ struct memory_segment *tls = &mem_layout.tls;
+ set_shadow_segment(tls, get_tls_start(), get_tls_size(), 1);
+
+ mem_layout.initialized = 1;
+}
+
+/*! \brief Deallocate a shadow segment */
+void clean_memory_segment(struct memory_segment *seg, int secondary) {
+ munmap((void*)seg->prim_start, seg->shadow_size);
+ if (secondary)
+ munmap((void*)seg->sec_start, seg->shadow_size);
+}
+
+/*! \brief Deallocate shadow regions used by runtime analysis */
+static void clean_memory_layout() {
DLOG("<<< Clean shadow layout >>>\n");
- /* Unmap global shadows */
- if (pgm_layout.long_global_shadow_start)
- munmap((void*)pgm_layout.long_global_shadow_start,
- pgm_layout.global_shadow_size);
- if (pgm_layout.short_global_shadow_start)
- munmap((void*)pgm_layout.short_global_shadow_start,
- pgm_layout.global_shadow_size);
- /* Unmap stack shadows */
- if (pgm_layout.long_stack_shadow_start)
- munmap((void*)pgm_layout.long_stack_shadow_start,
- pgm_layout.stack_shadow_size);
- if (pgm_layout.short_stack_shadow_start)
- munmap((void*)pgm_layout.short_stack_shadow_start,
- pgm_layout.stack_shadow_size);
- /* Unmap heap shadow */
- if (pgm_layout.heap_shadow_start)
- munmap((void*)pgm_layout.heap_shadow_start, pgm_layout.heap_shadow_size);
+ if (mem_layout.initialized) {
+ clean_memory_segment(&mem_layout.heap, 0);
+ clean_memory_segment(&mem_layout.stack, 1);
+ clean_memory_segment(&mem_layout.global, 1);
+ clean_memory_segment(&mem_layout.tls, 1);
+ }
}
/* }}} */
@@ -437,60 +352,66 @@ static void clean_pgm_layout() {
* are given using the following macros.
*/
-/*! \brief Convert a stack address into its short (byte) shadow counterpart */
-#define SHORT_STACK_SHADOW(_addr) \
- ((uintptr_t)((uintptr_t)_addr - pgm_layout.short_stack_shadow_offset))
-/*! \brief Convert a stack address into its long (block) shadow counterpart */
-#define LONG_STACK_SHADOW(_addr) \
- ((uintptr_t)((uintptr_t)_addr - pgm_layout.long_stack_shadow_offset))
+/*! \brief Convert a stack address into its primary shadow counterpart */
+#define PRIMARY_STACK_SHADOW(_addr) \
+ ((uintptr_t)((uintptr_t)_addr - mem_layout.stack.prim_offset))
+/*! \brief Convert a stack address into its secondary shadow counterpart */
+#define SECONDARY_STACK_SHADOW(_addr) \
+ ((uintptr_t)((uintptr_t)_addr - mem_layout.stack.sec_offset))
-/*! \brief Convert a global address into its short (byte) shadow counterpart */
-#define SHORT_GLOBAL_SHADOW(_addr) \
- ((uintptr_t)((uintptr_t)_addr + pgm_layout.short_global_shadow_offset))
-/*! \brief Convert a global address into its long (block) shadow counterpart */
-#define LONG_GLOBAL_SHADOW(_addr) \
- ((uintptr_t)((uintptr_t)_addr + pgm_layout.long_global_shadow_offset))
+/*! \brief Convert a global address into its primary shadow counterpart */
+#define PRIMARY_GLOBAL_SHADOW(_addr) \
+ ((uintptr_t)((uintptr_t)_addr + mem_layout.global.prim_offset))
+/*! \brief Convert a global address into its secondary shadow counterpart */
+#define SECONDARY_GLOBAL_SHADOW(_addr) \
+ ((uintptr_t)((uintptr_t)_addr + mem_layout.global.sec_offset))
/*! \brief Select stack or global shadow based on the value of `_global`
*
- * - SHORT_SHADOW(_addr, 0) is equivalent to STACK_SHORT_SHADOW(_addr)
- * - SHORT_SHADOW(_addr, 1) is equivalent to GLOBAL_SHORT_SHADOW(_addr) */
-#define SHORT_SHADOW(_addr, _global) \
- (_global ? SHORT_GLOBAL_SHADOW(_addr) : SHORT_STACK_SHADOW(_addr))
+ * - PRIMARY_SHADOW(_addr, 0) is equivalent to PRIMARY_STACK_SHADOW(_addr)
+ * - PRIMARY_SHADOW(_addr, 1) is equivalent to PRIMARY_GLOBAL_SHADOW(_addr) */
+#define PRIMARY_SHADOW(_addr, _global) \
+ (_global ? PRIMARY_GLOBAL_SHADOW(_addr) : PRIMARY_STACK_SHADOW(_addr))
-/*! \brief Same as above but for long stack/global shadows */
-#define LONG_SHADOW(_addr, _global) \
- (_global ? LONG_GLOBAL_SHADOW(_addr) : LONG_STACK_SHADOW(_addr))
+/*! \brief Same as above but for secondary stack/global shadows */
+#define SECONDARY_SHADOW(_addr, _global) \
+ (_global ? SECONDARY_GLOBAL_SHADOW(_addr) : SECONDARY_STACK_SHADOW(_addr))
/*! \brief Convert a heap address into its shadow counterpart */
#define HEAP_SHADOW(_addr) \
- ((uintptr_t)((uintptr_t)_addr + pgm_layout.heap_shadow_offset))
+ ((uintptr_t)((uintptr_t)_addr + mem_layout.heap.prim_offset))
/*! \brief Evaluate to a true value if a given address is a heap address */
#define IS_ON_HEAP(_addr) ( \
- ((uintptr_t)_addr) >= pgm_layout.heap_start && \
- ((uintptr_t)_addr) <= pgm_layout.heap_end \
+ ((uintptr_t)_addr) >= mem_layout.heap.start && \
+ ((uintptr_t)_addr) <= mem_layout.heap.end \
)
/*! \brief Evaluate to a true value if a given address is a stack address */
#define IS_ON_STACK(_addr) ( \
- ((uintptr_t)_addr) >= pgm_layout.stack_start && \
- ((uintptr_t)_addr) <= pgm_layout.stack_end \
+ ((uintptr_t)_addr) >= mem_layout.stack.start && \
+ ((uintptr_t)_addr) <= mem_layout.stack.end \
)
/*! \brief Evaluate to a true value if a given address is a global address */
#define IS_ON_GLOBAL(_addr) ( \
- ((uintptr_t)_addr) >= pgm_layout.global_start && \
- ((uintptr_t)_addr) <= pgm_layout.global_end \
+ ((uintptr_t)_addr) >= mem_layout.global.start && \
+ ((uintptr_t)_addr) <= mem_layout.global.end \
+)
+
+/*! \brief Evaluate to a true value if a given address is a TLS address */
+#define IS_ON_TLS(_addr) ( \
+ ((uintptr_t)_addr) >= mem_layout.tls.start && \
+ ((uintptr_t)_addr) <= mem_layout.tls.end \
)
/*! \brief Shortcut for evaluating an address via ::IS_ON_STACK or
- * ::IS_ON_GLOBAL based on the valua of the second parameter */
+ * ::IS_ON_GLOBAL based on the value of the second parameter */
#define IS_ON_STATIC(_addr, _global) \
(_global ? IS_ON_GLOBAL(_addr) : IS_ON_STACK(_addr))
/*! \brief Evaluate to a true value if a given address belongs to tracked
- * allocation (i.e., found within stack, heap oor globally) */
+ * allocation (i.e., found within stack, heap or globally) */
#define IS_ON_VALID(_addr) \
(IS_ON_STACK(_addr) || IS_ON_HEAP(_addr) || IS_ON_GLOBAL(_addr))
/* }}} */