From f994842a34c67ef9655f5fc25ae1e5c3e9446fc6 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 16 Nov 2021 17:51:09 +0100
Subject: [PATCH] [eacsl] Register safe locations for each newly created thread
---
.../internals/e_acsl_safe_locations.c | 5 +++--
.../internals/e_acsl_safe_locations.h | 2 ++
.../e_acsl_segment_observation_model.c | 14 +------------
.../segment_model/e_acsl_shadow_concurrency.c | 3 +++
.../segment_model/e_acsl_shadow_layout.c | 20 +++++++++++++++++++
.../segment_model/e_acsl_shadow_layout.h | 12 +++++++++++
6 files changed, 41 insertions(+), 15 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c
index f7ba3981504..4169419fdbf 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c
@@ -29,11 +29,12 @@
/* An array storing safe locations up to `safe_location_counter` position.
* This array should be initialized via a below function called
* `collect_safe_locations`. */
-static memory_location safe_locations[16];
-static int safe_location_counter = 0;
+static __thread memory_location safe_locations[16];
+static __thread int safe_location_counter = 0;
#define add_safe_location(_addr, _len, _init, _on_static) \
do { \
+ safe_locations[safe_location_counter].name = #_addr; \
safe_locations[safe_location_counter].address = _addr; \
safe_locations[safe_location_counter].length = _len; \
safe_locations[safe_location_counter].is_initialized = _init; \
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h
index 68fa0d17bda..19c05fec068 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h
@@ -36,6 +36,8 @@
/*! Simple representation of a safe location */
struct memory_location {
+ /*! Name of the safe location (for debug purposes) */
+ const char *name;
/*! Address */
uintptr_t address;
/*! Byte-length */
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
index 8ac970e200e..c04006b9e98 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
@@ -35,7 +35,6 @@
#include "../../internals/e_acsl_malloc.h"
#include "../../internals/e_acsl_private_assert.h"
#include "../../numerical_model/e_acsl_floating_point.h"
-#include "../internals/e_acsl_safe_locations.h"
#include "e_acsl_segment_tracking.h"
#include "e_acsl_shadow_layout.h"
@@ -322,18 +321,7 @@ void do_eacsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
shadow_alloca(&main, sizeof(&main));
initialize_static_region((uintptr_t)&main, sizeof(&main));
/* Tracking safe locations */
- collect_safe_locations();
- int i;
- for (i = 0; i < get_safe_locations_count(); i++) {
- memory_location *loc = get_safe_location(i);
- if (loc->is_on_static) {
- void *addr = (void *)loc->address;
- uintptr_t len = loc->length;
- shadow_alloca(addr, len);
- if (loc->is_initialized)
- unsafe_initialize(addr, len);
- }
- }
+ register_safe_locations(E_ACSL_REGISTER_ALL_LOCS);
init_infinity_values();
}
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c
index 0365a26d2d6..7ac2d7d13bd 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c
@@ -218,6 +218,9 @@ void init_thread_shadow_layout(size_t stack_size) {
DLOG(">>> Thread TLS ---------------\n");
print_memory_partition(&tls->p);
# endif
+
+ // Safe location tracking for thread-specific locations
+ register_safe_locations(E_ACSL_REGISTER_THREAD_LOCS);
}
void clean_thread_shadow_layout() {
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 8086b280e3a..258cc25fde8 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
@@ -25,6 +25,8 @@
#include "../../internals/e_acsl_malloc.h"
#include "../../internals/e_acsl_private_assert.h"
#include "../../internals/e_acsl_rtl_error.h"
+#include "../internals/e_acsl_safe_locations.h"
+#include "e_acsl_segment_tracking.h"
#include "e_acsl_shadow_layout.h"
@@ -706,6 +708,24 @@ void init_shadow_layout_main(int *argc_ref, char ***argv_ref) {
mem_layout.is_initialized_main = 1;
}
+void register_safe_locations(int thread_only) {
+ collect_safe_locations();
+ int count = get_safe_locations_count();
+ for (int i = 0; i < count; ++i) {
+ memory_location *loc = get_safe_location(i);
+ if (loc->is_on_static) {
+ void *addr = (void *)loc->address;
+ size_t len = loc->length;
+ if (!thread_only || IS_ON_THREAD(addr)) {
+ shadow_alloca(addr, len);
+ if (loc->is_initialized) {
+ unsafe_initialize(addr, len);
+ }
+ }
+ }
+ }
+}
+
void clean_shadow_layout() {
if (mem_layout.is_initialized_pre_main && mem_layout.is_initialized_main) {
int i;
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 dfc069364e4..79dc3eb2b37 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
@@ -272,6 +272,18 @@ void init_shadow_layout_pre_main();
* of the program). */
void init_shadow_layout_main(int *argc_ref, char ***argv_ref);
+/*! \brief Register safe locations in the memory model.
+ * \param thread_only If true, only register safe locations specific to the
+ current thread, otherwise register all available safe locations. */
+void register_safe_locations(int thread_only);
+
+/*! \brief True value for the parameter of `register_safe_locations()`
+ * function. */
+#define E_ACSL_REGISTER_THREAD_LOCS 1
+/*! \brief False value for the parameter of `register_safe_locations()`
+ * function. */
+#define E_ACSL_REGISTER_ALL_LOCS 0
+
/*! \brief Deallocate shadow regions used by runtime analysis */
void clean_shadow_layout();
/* }}} */
--
GitLab