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 f7ba3981504b6408c277a986d77cea0bc13c813c..4169419fdbf5030345e5414704ab2888925a738b 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 68fa0d17bda37fc3b989c204c532ef8e5054ab6d..19c05fec0687b9af6b35c7628e81a2b2962cf20f 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 8ac970e200e4e7b11fadc9781136559efbaab2cf..c04006b9e98c9e6e8607d83afdc1f636cdc3a22a 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 0365a26d2d6cc92abf2f06cac3421a22ed290ab7..7ac2d7d13bd975cd92aa75f0bb2d682e4fc58b56 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 8086b280e3a560876fa2a2430598b53b59e446ac..258cc25fde89442abd39671ac57a6d50ace6b9d0 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 dfc069364e436f22c07b71f5efc0a040308e0fa1..79dc3eb2b3761a9f0ab00fcac3bed040e32923b6 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(); /* }}} */