diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
index 20fae255f71e303f2379d555d6a5a1f126577f83..c65253afe997590a6af6ed375f0e93630ec74c14 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
@@ -1137,6 +1137,8 @@ void print_shadow_layout() {
print_memory_partition(&mem_layout.global);
DLOG(">>> TLS ----------------------\n");
print_memory_partition(&mem_layout.tls);
+ DLOG(">>> VDSO ---------------------\n");
+ print_memory_partition(&mem_layout.vdso);
# elif E_ACSL_OS_IS_WINDOWS
DLOG(">>> TEXT ---------------------\n");
print_memory_partition(&mem_layout.text);
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
index 9b910aaa18097903a66cdcd1844a72159be31db0..2a9a7a0063a7b61b113ffe8eb94ab58281ecad30 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
@@ -30,7 +30,13 @@
#if E_ACSL_OS_IS_LINUX
+# include <fcntl.h>
+# include <inttypes.h>
+# include <stdio.h>
+# include <string.h>
+# include <sys/auxv.h>
# include <sys/resource.h>
+# include <unistd.h>
/** Program stack information {{{ */
@@ -229,6 +235,93 @@ static void init_shadow_layout_tls() {
# endif
}
+static void init_shadow_layout_vdso() {
+ // Retrieve the start address of the VDSO segment
+ uintptr_t vdso = getauxval(AT_SYSINFO_EHDR);
+ private_assert(
+ vdso != 0,
+ "Start address of VDSO segment not found in auxiliary vector.\n");
+
+ // Use /proc/self/maps to retrieve the end address of the VDSO segment
+ // (using open() instead of fopen() to avoid a dynamic allocation)
+ int maps_fd = open("/proc/self/maps", O_RDONLY);
+ private_assert(maps_fd >= 0, "Unable to open /proc/self/maps: %s\n",
+ strerror(errno));
+
+ int result;
+ uintptr_t start, end;
+ ssize_t count;
+ off_t offset;
+ char *newline;
+ // Buffer to read /proc/self/maps. 255 should be enough to read one line.
+ char buffer[255];
+ while (1) {
+ count = read(maps_fd, buffer, sizeof(buffer) - 1);
+ if (count == 0) {
+ // If the VDSO segment has not been found, use 0 as start and end
+ // addresses
+ DVABORT("VDSO segment not found at address %a in /proc/self/maps\n",
+ vdso);
+ start = 0;
+ end = 0;
+ break;
+ } else if (count < 0) {
+ DVABORT("Reading /proc/self/maps failed: %s\n", strerror(errno));
+ break;
+ } else {
+ // Scan the start and end addresses of the segment
+ buffer[count] = '\0';
+ result = sscanf(buffer, "%" SCNxPTR "-%" SCNxPTR, &start, &end);
+ DVASSERT(result == 2,
+ "Scanning for addresses in /proc/self/maps failed, expected 2 "
+ "addresses, found: %d, error: %s\n",
+ result, strerror(errno));
+
+ if (start <= vdso && vdso < end) {
+ break;
+ }
+
+ // Set the file offset to the next line
+ do {
+ // Look for a newline character
+ buffer[count] = '\0';
+ newline = strchr(buffer, '\n');
+ if (newline != NULL) {
+ // Newline character found, set the file offset to the character
+ // after the newline
+ offset = count - (newline - buffer + 1);
+ offset = lseek(maps_fd, -offset, SEEK_CUR);
+ DVASSERT(offset != -1,
+ "Unable to move file offset of /proc/self/maps: %s\n",
+ strerror(errno));
+ break;
+ } else {
+ // No newline found on the current buffer, continue reading the file
+ count = read(maps_fd, buffer, sizeof(buffer) - 1);
+ }
+ } while (count > 0);
+ }
+ }
+
+ result = close(maps_fd);
+ DVASSERT(result == 0, "Unable to close /proc/self/maps: %s\n",
+ strerror(errno));
+
+ // Initialize the memory partition
+ memory_partition *pvdso = &mem_layout.vdso;
+ set_application_segment(&pvdso->application, start, end - start, "vdso",
+ NULL);
+ set_shadow_segment(&pvdso->primary, &pvdso->application, 1, "vdso_primary");
+ set_shadow_segment(&pvdso->secondary, &pvdso->application, 1,
+ "vdso_secondary");
+# ifdef E_ACSL_TEMPORAL
+ set_shadow_segment(&pvdso->temporal_primary, &pvdso->application, 1,
+ "temporal_vdso_primary");
+ set_shadow_segment(&pvdso->temporal_secondary, &pvdso->application, 1,
+ "temporal_vdso_secondary");
+# endif
+}
+
static void init_shadow_layout_stack(int *argc_ref, char ***argv_ref) {
memory_partition *pstack = &mem_layout.stack;
set_application_segment(&pstack->application,
@@ -489,6 +582,7 @@ void init_shadow_layout_pre_main() {
#if E_ACSL_OS_IS_LINUX
init_shadow_layout_global();
+ init_shadow_layout_vdso();
init_shadow_layout_tls();
#elif E_ACSL_OS_IS_WINDOWS
HANDLE module = GetModuleHandle(NULL);
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h
index f64825206dd86c8579ab4bb78b8ff16eb91e6996..9bdc0138ea97f61c70653e4c2a83da8e8131c8dc 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h
@@ -70,9 +70,11 @@
Standard streams stdin, stdout and stderr are put here.
Some libraries such as libxml use it quite a lot:
it may occur that the given size is not enough,
- in which case it MUST be increased. */
+ in which case it MUST be increased.
+ However since the TLS is next to the VDSO segment in the program layout, the
+ default size is small enough so that both segments do not overlap. */
#ifndef PGM_TLS_SIZE
-# define PGM_TLS_SIZE (64 * MB)
+# define PGM_TLS_SIZE (2 * MB)
#endif
/*! \brief Mspace padding used by shadow segments. This is to make sure that
@@ -191,6 +193,8 @@ struct memory_layout {
memory_partition global;
// The TLS is in a specific section and identifiable
memory_partition tls;
+ // The VDSO is a small shared library used for some kernel functions
+ memory_partition vdso;
#elif E_ACSL_OS_IS_WINDOWS
// On windows
// The text, bss and data segments are not necessarily contiguous so each one
@@ -214,11 +218,9 @@ struct memory_layout mem_layout = {
/*! \brief Array of used partitions */
memory_partition *mem_partitions[] = {
- &mem_layout.heap,
- &mem_layout.stack,
+ &mem_layout.heap, &mem_layout.stack,
#if E_ACSL_OS_IS_LINUX
- &mem_layout.global,
- &mem_layout.tls,
+ &mem_layout.global, &mem_layout.tls, &mem_layout.vdso,
#elif E_ACSL_OS_IS_WINDOWS
&mem_layout.text, &mem_layout.bss, &mem_layout.data,
&mem_layout.idata, &mem_layout.rdata,
@@ -291,6 +293,8 @@ void clean_shadow_layout();
# define global_secondary_offset mem_layout.global.secondary.shadow_offset
# define tls_primary_offset mem_layout.tls.primary.shadow_offset
# define tls_secondary_offset mem_layout.tls.secondary.shadow_offset
+# define vdso_primary_offset mem_layout.vdso.primary.shadow_offset
+# define vdso_secondary_offset mem_layout.vdso.secondary.shadow_offset
#elif E_ACSL_OS_IS_WINDOWS
# define text_primary_offset mem_layout.text.primary.shadow_offset
# define text_secondary_offset mem_layout.text.secondary.shadow_offset
@@ -351,6 +355,14 @@ void clean_shadow_layout();
/*! \brief Convert a TLS address into its secondary shadow counterpart */
# define SECONDARY_TLS_SHADOW(_addr) SHADOW_ACCESS(_addr, tls_secondary_offset)
+
+/*! \brief Convert a VDSO address into its primary shadow counterpart */
+# define PRIMARY_VDSO_SHADOW(_addr) SHADOW_ACCESS(_addr, vdso_primary_offset)
+
+/*! \brief Convert a VDSO address into its secondary shadow counterpart */
+# define SECONDARY_VDSO_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, vdso_secondary_offset)
+
#elif E_ACSL_OS_IS_WINDOWS
/*! \brief Convert a text address into its primary shadow counterpart */
# define PRIMARY_TEXT_SHADOW(_addr) SHADOW_ACCESS(_addr, text_primary_offset)
@@ -418,6 +430,7 @@ void clean_shadow_layout();
(IS_ON_STACK(_addr) ? _region##_STACK_SHADOW(_addr) \
: IS_ON_GLOBAL(_addr) ? _region##_GLOBAL_SHADOW(_addr) \
: IS_ON_TLS(_addr) ? _region##_TLS_SHADOW(_addr) \
+ : IS_ON_VDSO(_addr) ? _region##_VDSO_SHADOW(_addr) \
: (intptr_t)0)
// clang-format on
#elif E_ACSL_OS_IS_WINDOWS
@@ -462,10 +475,14 @@ void clean_shadow_layout();
/*! \brief Evaluate to true if _addr is a TLS address */
# define IS_ON_TLS(_addr) IS_ON(_addr, mem_layout.tls.application)
+/*! \brief Evaluate to true if _addr is a VDSO address */
+# define IS_ON_VDSO(_addr) IS_ON(_addr, mem_layout.vdso.application)
+
/*! \brief Shortcut for evaluating an address via ::IS_ON_STACK,
* ::IS_ON_GLOBAL or ::IS_ON_TLS */
# define IS_ON_STATIC(_addr) \
- (IS_ON_STACK(_addr) || IS_ON_GLOBAL(_addr) || IS_ON_TLS(_addr))
+ (IS_ON_STACK(_addr) || IS_ON_GLOBAL(_addr) || IS_ON_TLS(_addr) \
+ || IS_ON_VDSO(_addr))
#elif E_ACSL_OS_IS_WINDOWS
/*! \brief Evaluate to true if `_addr` is a text address */
# define IS_ON_TEXT(_addr) IS_ON(_addr, mem_layout.text.application)
@@ -529,6 +546,15 @@ void clean_shadow_layout();
/*! \brief Convert a TLS address into its secondary temporal shadow counterpart */
# define TEMPORAL_SECONDARY_TLS_SHADOW(_addr) \
SHADOW_ACCESS(_addr, mem_layout.tls.temporal_secondary.shadow_offset)
+
+/*! \brief Convert a VDSO address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_VDSO_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.vdso.temporal_primary.shadow_offset)
+
+/*! \brief Convert a VDSO address into its secondary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_VDSO_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.vdso.temporal_secondary.shadow_offset)
+
# elif E_ACSL_OS_IS_WINDOWS
/*! \brief Convert a text address into its primary temporal shadow counterpart */
# define TEMPORAL_PRIMARY_TEXT_SHADOW(_addr) \