Reworked memory layout for shadowing

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)
 /* }}} */

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 */

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))
 /* }}} */