diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index afc89c322e8e373f3408e907dc33065c8f1748bd..33989f466fab8af824d5db02ea2bdb8620290b19 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -69,6 +69,8 @@ share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c: CEA_
share/e-acsl/observation_model/segment_model/e_acsl_segment_timestamp_retrieval.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/observation_model/e_acsl_heap.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
index 3e48a5e1c20a2c871d095d3f5df7e011bba02089..4a68035f8c2dcabe21588acda40da18af398b203 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
@@ -634,3 +634,20 @@ void eacsl_block_info(char *p) {
}
#endif
/* }}} */
+
+/************************************************************************/
+/*** E-ACSL concurrency primitives {{{ ***/
+/************************************************************************/
+
+extern int pthread_create(pthread_t *restrict thread,
+ const pthread_attr_t *restrict attr,
+ pthread_routine_t start_routine, void *restrict arg);
+
+int eacsl_pthread_create(pthread_t *restrict thread,
+ const pthread_attr_t *restrict original_attr,
+ pthread_routine_t start_routine, void *restrict arg) {
+ private_abort("Concurrency is not supported for bittree model\n");
+ return EPERM;
+}
+
+/* }}} */
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
index c7a9fd1d2b26121ca08f1fe76ffd2b98307214c8..88c7501c2c04597650779e3fae9500678f9d4db4 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
@@ -103,6 +103,7 @@ int eacsl_separated(size_t count, ...) {
# include "segment_model/e_acsl_segment_omodel_debug.c"
# include "segment_model/e_acsl_segment_timestamp_retrieval.c"
# include "segment_model/e_acsl_segment_tracking.c"
+# include "segment_model/e_acsl_shadow_concurrency.c"
# include "segment_model/e_acsl_shadow_layout.c"
#elif defined E_ACSL_BITTREE_MMODEL
# include "bittree_model/e_acsl_bittree.c"
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
index 6bc4c9f7654a700397fd339f9a5f923154c57b04..c465c3b09d98cc8c45ac5a0f1e5fb301e17af6c0 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
@@ -31,6 +31,8 @@
#ifndef E_ACSL_OBSERVATION_MODEL_H
#define E_ACSL_OBSERVATION_MODEL_H
+#include <errno.h>
+#include <pthread.h>
#include <stddef.h>
#include <stdint.h>
@@ -82,6 +84,9 @@
#define eacsl_initialize export_alias(initialize)
#define eacsl_full_init export_alias(full_init)
+/* Concurrency */
+#define eacsl_pthread_create export_alias(pthread_create)
+
/* }}} */
/************************************************************************/
@@ -395,4 +400,34 @@ int eacsl_separated(size_t count, ...) __attribute__((FC_BUILTIN));
/* }}} */
+/************************************************************************/
+/*** E-ACSL concurrency primitives {{{ ***/
+/************************************************************************/
+
+/*! \brief Function pointer to a function given to \p pthread_create. */
+typedef void *(*pthread_routine_t)(void *);
+
+/*! \brief Drop-in replacement for \p pthread_create with memory tracking
+ * enabled.
+ *
+ * For further information, see \p pthread_create(3).
+ */
+// Specification extracted from share/libc/pthread.h in Frama-C
+/*@ requires valid_thread: \valid(thread);
+ requires valid_null_attr: attr == \null || \valid_read(attr);
+ requires valid_routine: \valid_function(start_routine);
+ requires valid_null_arg: arg == \null || \valid((char*)arg);
+ assigns *thread \from *attr;
+ assigns \result \from indirect:*attr;
+ ensures success_or_error:
+ \result == 0 ||
+ \result == EAGAIN || \result == EINVAL || \result == EPERM;
+ */
+int eacsl_pthread_create(pthread_t *restrict thread,
+ const pthread_attr_t *restrict attr,
+ pthread_routine_t start_routine, void *restrict arg)
+ __attribute__((FC_BUILTIN));
+
+/* }}} */
+
#endif // E_ACSL_OBSERVATION_MODEL_H
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c
index 973e1ab2d09deadcfcddf3d9759ff148a6c289ce..816b086f85923f2584bebc11a8cf791f4fa3f9a0 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c
@@ -27,6 +27,7 @@
#include <stdint.h>
+#include "../../internals/e_acsl_concurrency.h"
#include "../../internals/e_acsl_config.h"
#include "../../internals/e_acsl_malloc.h"
#include "../../internals/e_acsl_private_assert.h"
@@ -133,6 +134,8 @@ typedef struct pt_struct {
clean_leaf_fct_t clean_leaf_fct;
/*! \brief Function to print the content of a leaf. */
print_leaf_fct_t print_leaf_fct;
+ /*! \brief Read-write lock to concurrently access the trie. */
+ E_ACSL_RWLOCK_DECL(lock);
} pt_struct_t;
/* common prefix of two addresses */
@@ -187,12 +190,15 @@ pt_struct_t *pt_create(get_ptr_fct_t get_ptr_fct,
pt->contains_ptr_fct = contains_ptr_fct;
pt->clean_leaf_fct = clean_leaf_fct;
pt->print_leaf_fct = print_leaf_fct;
+
+ E_ACSL_RWINIT(pt->lock, NULL);
return pt;
}
void pt_destroy(pt_struct_t *pt) {
DASSERT(pt != NULL);
pt_clean(pt);
+ E_ACSL_RWDESTROY(pt->lock);
private_free(pt);
}
@@ -234,6 +240,8 @@ void pt_insert(pt_struct_t *pt, pt_leaf_t leaf) {
DASSERT(leaf != NULL);
pt_node_t *new_leaf_node;
+ E_ACSL_WLOCK(pt->lock);
+
uintptr_t ptr = (uintptr_t)pt->get_ptr_fct(leaf);
new_leaf_node = private_malloc(sizeof(pt_node_t));
@@ -294,6 +302,8 @@ void pt_insert(pt_struct_t *pt, pt_leaf_t leaf) {
DASSERT((parent->left == sibling && parent->right == new_leaf_node)
|| (parent->left == new_leaf_node && parent->right == sibling));
}
+
+ E_ACSL_RWUNLOCK(pt->lock);
}
/* called from pt_remove */
@@ -380,10 +390,15 @@ static void pt_remove_leaf_node(pt_struct_t *pt,
void pt_remove(pt_struct_t *pt, pt_leaf_t leaf) {
DASSERT(pt != NULL);
+
+ E_ACSL_WLOCK(pt->lock);
+
pt_node_t *leaf_node_to_delete = pt_get_leaf_node_from_leaf(pt, leaf);
DASSERT(leaf_node_to_delete->leaf == leaf);
pt_remove_leaf_node(pt, leaf_node_to_delete);
+
+ E_ACSL_RWUNLOCK(pt->lock);
}
/** Starting at `node`, remove all leaves that satisfy the given predicate from
@@ -414,13 +429,19 @@ int pt_remove_node_if(pt_struct_t *pt, pt_node_t *node,
void pt_remove_if(pt_struct_t *pt, pt_predicate_t predicate) {
DASSERT(pt != NULL);
+ E_ACSL_WLOCK(pt->lock);
pt_remove_node_if(pt, pt->root, predicate);
+ E_ACSL_RWUNLOCK(pt->lock);
}
pt_leaf_t pt_lookup(const pt_struct_t *pt, void *ptr) {
DASSERT(pt != NULL);
- DASSERT(pt->root != NULL);
DASSERT(ptr != NULL);
+
+ E_ACSL_RLOCK(pt->lock);
+ DASSERT(pt->root != NULL);
+
+ pt_leaf_t res;
pt_node_t *tmp = pt->root;
/*@ loop assigns tmp;
@@ -428,7 +449,8 @@ pt_leaf_t pt_lookup(const pt_struct_t *pt, void *ptr) {
while (!tmp->is_leaf) {
// if the ptr we are looking for does not share the prefix of tmp
if ((tmp->addr & tmp->mask) != ((uintptr_t)ptr & tmp->mask)) {
- return NULL;
+ res = NULL;
+ goto end;
}
// two children
@@ -441,21 +463,28 @@ pt_leaf_t pt_lookup(const pt_struct_t *pt, void *ptr) {
== ((uintptr_t)ptr & tmp->left->mask)) {
tmp = tmp->left;
} else {
- return NULL;
+ res = NULL;
+ goto end;
}
}
if (pt->get_ptr_fct(tmp->leaf) != ptr) {
- return NULL;
+ res = NULL;
}
- return tmp->leaf;
+
+end:
+ E_ACSL_RWUNLOCK(pt->lock);
+ return res;
}
pt_leaf_t pt_find(const pt_struct_t *pt, void *ptr) {
DASSERT(pt != NULL);
+ E_ACSL_RLOCK(pt->lock);
+ pt_leaf_t res;
if (pt->root == NULL || ptr == NULL) {
- return NULL;
+ res = NULL;
+ goto end;
}
pt_node_t *tmp = pt->root;
@@ -465,16 +494,19 @@ pt_leaf_t pt_find(const pt_struct_t *pt, void *ptr) {
if (tmp->is_leaf) {
/* tmp cannot contain ptr because its begin addr is higher */
if (tmp->addr > (uintptr_t)ptr) {
- return NULL;
+ res = NULL;
+ goto end;
}
/* tmp->addr <= ptr, tmp may contain ptr */
else if (pt->contains_ptr_fct(tmp->leaf, ptr)) {
- return tmp->leaf;
+ res = tmp->leaf;
+ goto end;
}
/* tmp->addr <= ptr, but tmp does not contain ptr */
else {
- return NULL;
+ res = NULL;
+ goto end;
}
}
@@ -490,13 +522,18 @@ pt_leaf_t pt_find(const pt_struct_t *pt, void *ptr) {
tmp = tmp->left;
} else {
if (other_choice == NULL) {
- return NULL;
+ res = NULL;
+ goto end;
} else {
tmp = other_choice;
other_choice = NULL;
}
}
}
+
+end:
+ E_ACSL_RWUNLOCK(pt->lock);
+ return res;
}
static pt_leaf_t pt_find_if_rec(pt_node_t *node, pt_predicate_t predicate) {
@@ -514,12 +551,17 @@ static pt_leaf_t pt_find_if_rec(pt_node_t *node, pt_predicate_t predicate) {
pt_leaf_t pt_find_if(const pt_struct_t *pt, pt_predicate_t predicate) {
DASSERT(pt != NULL);
+ E_ACSL_RLOCK(pt->lock);
+ pt_leaf_t res;
if (pt->root == NULL) {
- return NULL;
+ res = NULL;
} else {
- return pt_find_if_rec(pt->root, predicate);
+ res = pt_find_if_rec(pt->root, predicate);
}
+
+ E_ACSL_RWUNLOCK(pt->lock);
+ return res;
}
static void pt_clean_rec(const pt_struct_t *pt, pt_node_t *ptr) {
@@ -538,8 +580,10 @@ static void pt_clean_rec(const pt_struct_t *pt, pt_node_t *ptr) {
void pt_clean(pt_struct_t *pt) {
DASSERT(pt != NULL);
+ E_ACSL_WLOCK(pt->lock);
pt_clean_rec(pt, pt->root);
pt->root = NULL;
+ E_ACSL_RWUNLOCK(pt->lock);
}
#ifdef E_ACSL_DEBUG
@@ -564,7 +608,9 @@ static void pt_print_node(const pt_struct_t *pt, pt_node_t *node, int depth) {
void pt_print(const pt_struct_t *pt) {
DLOG("------------DEBUG\n");
if (pt != NULL) {
+ E_ACSL_RLOCK(pt->lock);
pt_print_node(pt, pt->root, 0);
+ E_ACSL_RWUNLOCK(pt->lock);
} else {
DLOG("Patricia trie is NULL\n");
}
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 90c2522e41f7247eecb27f2f6a02bc0183e5dea7..8ac970e200e4e7b11fadc9781136559efbaab2cf 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
@@ -30,6 +30,7 @@
#include <stdint.h>
#include "../../instrumentation_model/e_acsl_temporal.h"
+#include "../../internals/e_acsl_concurrency.h"
#include "../../internals/e_acsl_debug.h"
#include "../../internals/e_acsl_malloc.h"
#include "../../internals/e_acsl_private_assert.h"
@@ -41,95 +42,182 @@
#include "../e_acsl_observation_model.h"
#include "../internals/e_acsl_timestamp_retrieval.h"
+#ifdef E_ACSL_CONCURRENCY_PTHREAD
+/*! \brief Global read-write lock for the memory model. */
+static pthread_rwlock_t __e_acsl_segment_model_global_lock =
+ PTHREAD_RWLOCK_INITIALIZER;
+#endif
+
+void *malloc(size_t size) {
+ E_ACSL_WLOCK(__e_acsl_segment_model_global_lock);
+ void *result = unsafe_malloc(size);
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
+ return result;
+}
+
+void *calloc(size_t nbr_elt, size_t size_elt) {
+ E_ACSL_WLOCK(__e_acsl_segment_model_global_lock);
+ void *result = unsafe_calloc(nbr_elt, size_elt);
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
+ return result;
+}
+
+void *realloc(void *ptr, size_t size) {
+ E_ACSL_WLOCK(__e_acsl_segment_model_global_lock);
+ void *result = unsafe_realloc(ptr, size);
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
+ return result;
+}
+
+void free(void *ptr) {
+ E_ACSL_WLOCK(__e_acsl_segment_model_global_lock);
+ unsafe_free(ptr);
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
+}
+
+void *aligned_alloc(size_t alignment, size_t size) {
+ E_ACSL_WLOCK(__e_acsl_segment_model_global_lock);
+ void *result = unsafe_aligned_alloc(alignment, size);
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
+ return result;
+}
+
+int posix_memalign(void **memptr, size_t alignment, size_t size) {
+ E_ACSL_WLOCK(__e_acsl_segment_model_global_lock);
+ int result = unsafe_posix_memalign(memptr, alignment, size);
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
+ return result;
+}
+
void *eacsl_store_block(void *ptr, size_t size) {
+ E_ACSL_WLOCK(__e_acsl_segment_model_global_lock);
/* Only stack-global memory blocks are recorded explicitly via this function.
Heap blocks should be tracked internally using memory allocation functions
such as malloc or calloc. */
shadow_alloca(ptr, size);
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
return ptr;
}
void eacsl_delete_block(void *ptr) {
+ E_ACSL_WLOCK(__e_acsl_segment_model_global_lock);
/* Block deletion should be performed on stack/global addresses only,
* heap blocks should be deallocated manually via free/cfree/realloc. */
shadow_freea(ptr);
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
}
void *eacsl_store_block_duplicate(void *ptr, size_t size) {
+ E_ACSL_WLOCK(__e_acsl_segment_model_global_lock);
if (allocated((uintptr_t)ptr, size, (uintptr_t)ptr))
- eacsl_delete_block(ptr);
+ shadow_freea(ptr);
shadow_alloca(ptr, size);
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
return ptr;
}
/*! \brief Initialize a chunk of memory given by its start address (`addr`)
* and byte length (`n`). */
void eacsl_initialize(void *ptr, size_t n) {
- TRY_SEGMENT((uintptr_t)ptr, initialize_heap_region((uintptr_t)ptr, n),
- initialize_static_region((uintptr_t)ptr, n))
+ E_ACSL_WLOCK(__e_acsl_segment_model_global_lock);
+ unsafe_initialize(ptr, n);
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
}
void eacsl_full_init(void *ptr) {
- eacsl_initialize(ptr, _block_length(ptr));
+ E_ACSL_WLOCK(__e_acsl_segment_model_global_lock);
+ unsafe_initialize(ptr, _block_length(ptr));
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
}
void eacsl_mark_readonly(void *ptr) {
+ E_ACSL_WLOCK(__e_acsl_segment_model_global_lock);
mark_readonly_region((uintptr_t)ptr, _block_length(ptr));
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
}
/* ********************** */
/* E-ACSL annotations {{{ */
/* ********************** */
+int eacsl_freeable(void *ptr) {
+ E_ACSL_RLOCK(__e_acsl_segment_model_global_lock);
+ int result = unsafe_freeable(ptr);
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
+ return result;
+}
+
int eacsl_valid(void *ptr, size_t size, void *ptr_base, void *addrof_base) {
- return size == 0
- || (allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base)
+ int result = size == 0;
+ if (!result) {
+ E_ACSL_RLOCK(__e_acsl_segment_model_global_lock);
+ result = allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base)
&& !readonly(ptr)
#ifdef E_ACSL_TEMPORAL
&& temporal_valid(ptr_base, addrof_base)
#endif
- );
+ ;
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
+ }
+ return result;
}
int eacsl_valid_read(void *ptr, size_t size, void *ptr_base,
void *addrof_base) {
- return size == 0
- || (allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base)
+ int result = size == 0;
+ if (!result) {
+ E_ACSL_RLOCK(__e_acsl_segment_model_global_lock);
+ result = allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base)
#ifdef E_ACSL_TEMPORAL
&& temporal_valid(ptr_base, addrof_base)
#endif
- );
+ ;
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
+ }
+ return result;
}
/*! NB: The implementation for this function can also be specified via
\p _base_addr macro that will eventually call ::TRY_SEGMENT. The following
implementation is preferred for performance reasons. */
void *eacsl_base_addr(void *ptr) {
- TRY_SEGMENT(ptr, return (void *)heap_info((uintptr_t)ptr, 'B'),
- return (void *)static_info((uintptr_t)ptr, 'B'));
- return NULL;
+ void *result = NULL;
+ E_ACSL_RLOCK(__e_acsl_segment_model_global_lock);
+ TRY_SEGMENT(ptr, result = (void *)heap_info((uintptr_t)ptr, 'B'),
+ result = (void *)static_info((uintptr_t)ptr, 'B'));
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
+ return result;
}
/*! NB: Implementation of the following function can also be specified
via \p _block_length macro. A more direct approach via ::TRY_SEGMENT
is preferred for performance reasons. */
size_t eacsl_block_length(void *ptr) {
- TRY_SEGMENT(ptr, return heap_info((uintptr_t)ptr, 'L'),
- return static_info((uintptr_t)ptr, 'L'))
- return 0;
+ size_t result = 0;
+ E_ACSL_RLOCK(__e_acsl_segment_model_global_lock);
+ TRY_SEGMENT(ptr, result = heap_info((uintptr_t)ptr, 'L'),
+ result = static_info((uintptr_t)ptr, 'L'))
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
+ return result;
}
size_t eacsl_offset(void *ptr) {
- TRY_SEGMENT(ptr, return heap_info((uintptr_t)ptr, 'O'),
- return static_info((uintptr_t)ptr, 'O'));
- return 0;
+ size_t result = 0;
+ E_ACSL_RLOCK(__e_acsl_segment_model_global_lock);
+ TRY_SEGMENT(ptr, result = heap_info((uintptr_t)ptr, 'O'),
+ result = static_info((uintptr_t)ptr, 'O'));
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
+ return result;
}
int eacsl_initialized(void *ptr, size_t size) {
+ int result = 0;
uintptr_t addr = (uintptr_t)ptr;
- TRY_SEGMENT_WEAK(addr, return heap_initialized(addr, size),
- return static_initialized(addr, size));
- return 0;
+ E_ACSL_RLOCK(__e_acsl_segment_model_global_lock);
+ TRY_SEGMENT_WEAK(addr, result = heap_initialized(addr, size),
+ result = static_initialized(addr, size));
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
+ return result;
}
/* }}} */
@@ -196,67 +284,69 @@ static void argv_alloca(int *argc_ref, char ***argv_ref) {
/* Program initialization {{{ */
extern int main(void);
+static void do_mspaces_init() {
+ describe_run();
+ eacsl_make_memory_spaces(64 * MB, get_heap_size());
+ /* Allocate and log shadow memory layout of the execution.
+ Case of the segments available before main. */
+ init_shadow_layout_pre_main();
+}
+
void mspaces_init() {
- /* [already_run] avoids reentrancy issue (see Gitlab issue #83),
+ /* [E_ACSL_RUN_ONCE] avoids reentrancy issue (see Gitlab issue #83),
e.g. in presence of a GCC's constructors that invokes malloc possibly
several times before calling main. */
- static char already_run = 0;
- if (!already_run) {
- describe_run();
- eacsl_make_memory_spaces(64 * MB, get_heap_size());
- /* Allocate and log shadow memory layout of the execution.
- Case of the segments available before main. */
- init_shadow_layout_pre_main();
- already_run = 1;
- }
+ E_ACSL_RUN_ONCE(do_mspaces_init);
}
-void eacsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
- /* [already_run] avoids reentrancy issue (see Gitlab issue #83),
- e.g. in presence of a recursive call to 'main' */
- static char already_run = 0;
- if (!already_run) {
- mspaces_init();
- /* Verify that the given size of a pointer matches the one in the present
+void do_eacsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
+ mspaces_init();
+ /* 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);
- /* Lift stack limit to account for extra stack memory overhead. */
- increase_stack_limit(E_ACSL_STACK_SIZE * MB);
- /* Allocate and log shadow memory layout of the execution. Case of the
+ arch_assert(ptr_size);
+ /* Initialize report file with debug logs (only in debug mode). */
+ initialize_report_file(argc_ref, argv_ref);
+ /* Lift stack limit to account for extra stack memory overhead. */
+ increase_stack_limit(E_ACSL_STACK_SIZE * MB);
+ /* Allocate and log shadow memory layout of the execution. Case of the
segments available after main. */
- init_shadow_layout_main(argc_ref, argv_ref);
- //DEBUG_PRINT_LAYOUT;
- /* Make sure the layout holds */
- DVALIDATE_SHADOW_LAYOUT;
- /* Track program arguments. */
- if (argc_ref && argv_ref)
- argv_alloca(argc_ref, argv_ref);
- /* Track main function */
- 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)
- eacsl_initialize(addr, len);
- }
+ init_shadow_layout_main(argc_ref, argv_ref);
+ //DEBUG_PRINT_LAYOUT;
+ /* Make sure the layout holds */
+ DVALIDATE_SHADOW_LAYOUT;
+ /* Track program arguments. */
+ if (argc_ref && argv_ref)
+ argv_alloca(argc_ref, argv_ref);
+ /* Track main function */
+ 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);
}
- init_infinity_values();
- already_run = 1;
}
+ init_infinity_values();
+}
+
+void eacsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
+ /* [E_ACSL_RUN_ONCE_WITH_ARGS] avoids reentrancy issue (see Gitlab issue #83),
+ e.g. in presence of a recursive call to 'main'. */
+ E_ACSL_RUN_ONCE_WITH_ARGS(do_eacsl_memory_init, argc_ref, argv_ref, ptr_size);
}
void eacsl_memory_clean(void) {
+ E_ACSL_WLOCK(__e_acsl_segment_model_global_lock);
clean_shadow_layout();
report_heap_leaks();
+ E_ACSL_RWUNLOCK(__e_acsl_segment_model_global_lock);
}
/* }}} */
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 56f7535cec778d4d5b9f3d9eaa8840dd7fa1c750..add2d3db74d22f5f1f4df3727e732ddd0fcffdc5 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
@@ -584,8 +584,7 @@ static void set_heap_segment(void *ptr, size_t size, size_t alloc_size,
}
}
-void *malloc(size_t size) {
-
+void *unsafe_malloc(size_t size) {
size_t alloc_size = ALLOC_SIZE(size);
/* Return NULL if the size is too large to be aligned */
@@ -604,7 +603,7 @@ void *malloc(size_t size) {
return res;
}
-void *calloc(size_t nmemb, size_t size) {
+void *unsafe_calloc(size_t nmemb, size_t size) {
/* Since both `nmemb` and `size` are both of size `size_t` the multiplication
* of the arguments (which gives the actual allocation size) might lead to an
* integer overflow. The below code checks for an overflow and sets the
@@ -631,7 +630,7 @@ void *calloc(size_t nmemb, size_t size) {
}
void *shadow_copy(const void *ptr, size_t size, int init) {
- char *ret = (init) ? calloc(1, size) : malloc(size);
+ char *ret = (init) ? unsafe_calloc(1, size) : unsafe_malloc(size);
private_assert(ret != NULL, "Shadow copy failed\n", NULL);
/* Shadow copy is internal, therefore heap status should not be updated.
Since it is set via `set_heap_segment`, it needs to be reverted back. */
@@ -678,7 +677,7 @@ static void unset_heap_segment(void *ptr, int init, const char *function) {
}
}
-void free(void *ptr) {
+void unsafe_free(void *ptr) {
if (ptr == NULL) {
/* Fail if instructed to treat NULL input to free as invalid. */
#ifdef E_ACSL_FREE_VALID_ADDRESS
@@ -688,7 +687,7 @@ void free(void *ptr) {
}
if (ptr != NULL) { /* NULL is a valid behaviour */
- if (eacsl_freeable(ptr)) {
+ if (unsafe_freeable(ptr)) {
unset_heap_segment(ptr, 1, "free");
public_free(ptr);
} else {
@@ -699,17 +698,17 @@ void free(void *ptr) {
/* }}} */
/* Heap reallocation (realloc) {{{ */
-void *realloc(void *ptr, size_t size) {
+void *unsafe_realloc(void *ptr, size_t size) {
char *res = NULL; /* Resulting pointer */
/* If the pointer is NULL then realloc is equivalent to malloc(size) */
if (ptr == NULL)
- return malloc(size);
+ return unsafe_malloc(size);
/* If the pointer is not NULL and the size is zero then realloc is
* equivalent to free(ptr) */
else if (ptr != NULL && size == 0) {
- free(ptr);
+ unsafe_free(ptr);
} else {
- if (eacsl_freeable(ptr)) { /* ... and can be used as an input to `free` */
+ if (unsafe_freeable(ptr)) { /* ... and can be used as an input to `free` */
size_t alloc_size = ALLOC_SIZE(size);
res = public_realloc(ptr, alloc_size);
DVALIDATE_ALIGNMENT(res);
@@ -822,7 +821,7 @@ void *realloc(void *ptr, size_t size) {
/* }}} */
/* Heap aligned allocation (aligned_alloc) {{{ */
-void *aligned_alloc(size_t alignment, size_t size) {
+void *unsafe_aligned_alloc(size_t alignment, size_t size) {
/* Check if:
* - size and alignment are greater than zero
* - alignment is a power of 2
@@ -841,7 +840,7 @@ void *aligned_alloc(size_t alignment, size_t size) {
/* }}} */
/* Heap aligned allocation (posix_memalign) {{{ */
-int posix_memalign(void **memptr, size_t alignment, size_t size) {
+int unsafe_posix_memalign(void **memptr, size_t alignment, size_t size) {
/* Check if:
* - size and alignment are greater than zero
* - alignment is a power of 2 and a multiple of sizeof(void*) */
@@ -892,7 +891,7 @@ int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr) {
return 0;
}
-int eacsl_freeable(void *ptr) { /* + */
+int unsafe_freeable(void *ptr) { /* + */
uintptr_t addr = (uintptr_t)ptr;
/* Address is not on the program's heap, so cannot be freed */
if (!IS_ON_HEAP(addr))
@@ -1019,6 +1018,13 @@ void initialize_heap_region(uintptr_t addr, long len) {
}
/* }}} */
+/* Heap or static initialization {{{ */
+void unsafe_initialize(void *ptr, size_t n) {
+ TRY_SEGMENT((uintptr_t)ptr, initialize_heap_region((uintptr_t)ptr, n),
+ initialize_static_region((uintptr_t)ptr, n))
+}
+/* }}} */
+
/* Internal state print (debug mode) {{{ */
#ifdef E_ACSL_DEBUG
void printbyte(unsigned char c, char buf[], size_t bufsize) {
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
index 6f2c8cc80a9412f7086617177e742958d48dc96d..de93d8999bf64a8b9f78535b2f9819e13c9f10d7 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
@@ -401,11 +401,19 @@ void static_store_temporal_referent(uintptr_t addr, uint32_t ref);
#endif /*}}} E_ACSL_TEMPORAL*/
/* }}} */
-/* Static initialization {{{ */
-/*! \brief The following function marks n bytes starting from the address
- * given by addr as initialized. `size` equating to zero indicates that the
- * whole block should be marked as initialized. */
+/* Initialization {{{ */
+
+/*! \brief Unsafe version of `eacsl_initialize()` that does not lock the memory
+ model. */
+void unsafe_initialize(void *ptr, size_t n);
+
+/*! \brief The following function marks n bytes on a static region starting from
+ * the address given by addr as initialized. `size` equating to zero indicates
+ * that the whole block should be marked as initialized. */
void initialize_static_region(uintptr_t addr, long size);
+
+/*! \brief Mark n bytes on the heap starting from address addr as initialized */
+void initialize_heap_region(uintptr_t addr, long len);
/* }}} */
/* Read-only {{{ */
@@ -418,6 +426,27 @@ void mark_readonly_region(uintptr_t addr, long size);
/* }}} */
/* Heap allocation {{{ (malloc/calloc) */
+
+/*! \brief Unsafe version of `malloc()` that does not lock the memory model. */
+void *unsafe_malloc(size_t size);
+
+/*! \brief Unsafe version of `calloc()` that does not lock the memory model. */
+void *unsafe_calloc(size_t nbr_elt, size_t size_elt);
+
+/*! \brief Unsafe version of `realloc()` that does not lock the memory model. */
+void *unsafe_realloc(void *ptr, size_t size);
+
+/*! \brief Unsafe version of `free()` that does not lock the memory model. */
+void unsafe_free(void *ptr);
+
+/*! \brief Unsafe version of `aligned_alloc()` that does not lock the memory
+ model. */
+void *unsafe_aligned_alloc(size_t alignment, size_t size);
+
+/*! \brief Unsafe version of `posix_memalign()` that does not lock the memory
+ model. */
+int unsafe_posix_memalign(void **memptr, size_t alignment, size_t size);
+
/** \brief Return shadowed copy of a memory chunk on a program's heap using.
* If `init` parameter is set to a non-zero value the memory occupied by the
* resulting block is set to be initialized and uninitialized otherwise. */
@@ -443,13 +472,16 @@ void *shadow_copy(const void *ptr, size_t size, int init);
* only legal if both `p` and `p+i` point to the same block. */
int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr);
-/*! \brief Return a non-zero value if a given address is a base address of a
+/*! \brief Unsafe version of `eacsl_freeable()` that does not lock the memory
+ * model.
+ *
+ * Return a non-zero value if a given address is a base address of a
* heap-allocated memory block that `addr` belongs to.
*
* As some of the other functions, \b \\freeable can be expressed using
* ::IS_ON_HEAP, ::heap_allocated and ::_base_addr. Here direct
* implementation is preferred for performance reasons. */
-int eacsl_freeable(void *ptr);
+int unsafe_freeable(void *ptr);
/*! \brief Querying information about a specific heap memory address.
* This function is similar to ::static_info except it returns data
@@ -474,11 +506,6 @@ uint32_t heap_temporal_info(uintptr_t addr, int origin);
void heap_store_temporal_referent(uintptr_t addr, uint32_t ref);
#endif /*}}} E_ACSL_TEMPORAL*/
-/* Heap initialization {{{ */
-/*! \brief Mark n bytes on the heap starting from address addr as initialized */
-void initialize_heap_region(uintptr_t addr, long len);
-/* }}} */
-
/* Internal state print (debug mode) {{{ */
#ifdef E_ACSL_DEBUG
/* ! \brief Print human-readable representation of a byte in a primary
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
new file mode 100644
index 0000000000000000000000000000000000000000..0365a26d2d6cc92abf2f06cac3421a22ed290ab7
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c
@@ -0,0 +1,425 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2021 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+/*! ***********************************************************************
+ * \file
+ * \brief Implementation of E-ACSL concurrency support for the shadow memory
+ * model.
+***************************************************************************/
+
+#include "e_acsl_shadow_concurrency.h"
+
+#ifdef E_ACSL_CONCURRENCY_PTHREAD
+
+# include <pthread.h>
+# include <stdlib.h>
+# include <string.h>
+
+# include "../../internals/e_acsl_concurrency.h"
+# include "../../internals/e_acsl_rtl_error.h"
+# include "../internals/e_acsl_patricia_trie.h"
+# include "e_acsl_shadow_layout.h"
+
+/************************************************************************/
+/*** Patricia trie for the thread memory partitions {{{ ***/
+/* Each thread has its own stack and TLS segment. To be able to monitor the
+ * threaded code, we need to track those memory segments and quickly determine
+ * on which segment is a given pointer.
+ * The patricia trie structure offers great lookup performance and adequate
+ * insertion and removal performance for this use-case.
+ */
+/************************************************************************/
+
+/*! Leaf of the patricia trie containing a memory segment belonging to a
+ thread. */
+typedef struct thread_partition {
+ /*! Id of the thread */
+ pthread_t id;
+ /*! Memory segment belonging to a thread */
+ memory_partition p;
+} thread_partition_t;
+
+/*! \param leaf Leaf of the patricia trie.
+ \return The start address of the memory segment on the given leaf. */
+static void *tp_get_ptr(pt_leaf_t leaf) {
+ DASSERT(leaf != NULL);
+ return (void *)((thread_partition_t *)leaf)->p.application.start;
+}
+
+/*! \param leaf Leaf of the patricia trie.
+ \param ptr Pointer address that we are looking for.
+ \return true (!= 0) if the pointer is contained in the memory segment
+ represented by the leaf, false (== 0) otherwise. */
+static int tp_contains_ptr(pt_leaf_t leaf, void *ptr) {
+ DASSERT(leaf != NULL);
+ thread_partition_t *tp = (thread_partition_t *)leaf;
+ return IS_ON(ptr, tp->p.application);
+}
+
+/*! \brief Deallocate the leaf, i.e. deallocate the shadow regions used by the
+ runtime analysis for the given leaf, and the leaf itself. */
+static void tp_clean(pt_leaf_t leaf) {
+ DASSERT(leaf != NULL);
+ thread_partition_t *tp = (thread_partition_t *)leaf;
+ if (tp->p.primary.mspace) {
+ eacsl_destroy_mspace(tp->p.primary.mspace);
+ }
+ if (tp->p.secondary.mspace) {
+ eacsl_destroy_mspace(tp->p.secondary.mspace);
+ }
+# ifdef E_ACSL_TEMPORAL
+ if (tp->p.temporal_primary.mspace) {
+ eacsl_destroy_mspace(tp->p.temporal_primary.mspace);
+ }
+ if (tp->p.temporal_secondary.mspace) {
+ eacsl_destroy_mspace(tp->p.temporal_secondary.mspace);
+ }
+# endif
+ private_free(tp);
+}
+
+/*! \brief Print the content of the given leaf */
+static void tp_print(pt_leaf_t leaf) {
+# if defined(E_ACSL_DEBUG)
+ DASSERT(leaf != NULL);
+ thread_partition_t *tp = (thread_partition_t *)leaf;
+ DLOG("thread id: %lu\n", tp->id);
+ print_memory_partition(&tp->p);
+# endif
+}
+
+/*! \return true (!= 0) if the leaf corresponds to the current thread, false
+ (== 0) otherwise. */
+static int tp_is_same_thread(pt_leaf_t leaf) {
+ DASSERT(leaf != NULL);
+ pthread_t id = pthread_self();
+ return pthread_equal(id, ((thread_partition_t *)leaf)->id);
+}
+
+/*! Instance of patricia trie to store the memory segments of the threads. */
+pt_struct_t *thread_partitions = NULL;
+
+/*! \brief Creates the thread partitions trie. This function should be used with
+ E_ACSL_RUN_ONCE. */
+static void create_thread_partitions_trie() {
+ DVASSERT(thread_partitions == NULL,
+ "Thread partitions trie already created\n");
+ thread_partitions =
+ pt_create(tp_get_ptr, tp_contains_ptr, tp_clean, tp_print);
+}
+
+/* }}} */
+
+/************************************************************************/
+/*** Thread shadow layout {{{ ***/
+/************************************************************************/
+
+/*! \brief Fill the given `memory_partition` with the addresses of the stack
+ segment for the current thread. */
+static void fill_thread_layout_stack(memory_partition *pstack,
+ size_t stack_size) {
+ // Scan /proc/self/maps to retrieve the memory segment corresponding to the
+ // current thread stack
+ FILE *maps = fopen("/proc/self/maps", "r");
+ DVASSERT(maps != NULL, "Unable to open /proc/self/maps: %s\n",
+ rtl_strerror(errno));
+
+ int result;
+ // Use the address of the local variable `maps`, stored on the stack, to find
+ // the segment corresponding to the current stack
+ uintptr_t stack_addr = (uintptr_t)&maps;
+ uintptr_t start, end;
+ char buffer[255];
+ while (fgets(buffer, sizeof(buffer), maps) != NULL) {
+ result = sscanf(buffer, "%lx-%lx", &start, &end);
+ DVASSERT(result == 2, "Reading /proc/self/maps failed: %s\n",
+ rtl_strerror(errno));
+
+ if (start <= stack_addr && stack_addr <= end) {
+ break;
+ }
+ }
+
+ result = fclose(maps);
+ DVASSERT(result == 0, "Unable to close /proc/self/maps: %s\n",
+ rtl_strerror(errno));
+
+ // Allocate shadow memory spaces and compute offsets
+ set_application_segment(&pstack->application, start, stack_size,
+ "thread_stack", NULL);
+ set_shadow_segment(&pstack->primary, &pstack->application, 1,
+ "thread_stack_primary");
+ set_shadow_segment(&pstack->secondary, &pstack->application, 1,
+ "thread_stack_secondary");
+# ifdef E_ACSL_TEMPORAL
+ set_shadow_segment(&pstack->temporal_primary, &pstack->application, 1,
+ "temporal_thread_stack_primary");
+ set_shadow_segment(&pstack->temporal_secondary, &pstack->application, 1,
+ "temporal_thread_stack_secondary");
+# endif
+}
+
+/*! \brief Fill the given `memory_partition` with the addresses of the TLS
+ segment for the current thread. */
+static void fill_thread_layout_tls(memory_partition *ptls) {
+ // Since the TLS is by design specific to each thread, we can reuse the
+ // method used to identify the TLS segment in the main thread
+ set_application_segment(&ptls->application, get_tls_start(), get_tls_size(),
+ "thread_tls", NULL);
+ set_shadow_segment(&ptls->primary, &ptls->application, 1,
+ "thread_tls_primary");
+ set_shadow_segment(&ptls->secondary, &ptls->application, 1,
+ "thread_tls_secondary");
+# ifdef E_ACSL_TEMPORAL
+ set_shadow_segment(&ptls->temporal_primary, &ptls->application, 1,
+ "thread_temporal_tls_primary");
+ set_shadow_segment(&ptls->temporal_secondary, &ptls->application, 1,
+ "thread_temporal_tls_secondary");
+# endif
+}
+
+void init_thread_shadow_layout(size_t stack_size) {
+ DASSERT(thread_partitions != NULL);
+
+ pthread_t id = pthread_self();
+
+ thread_partition_t *stack = private_malloc(sizeof(thread_partition_t));
+ stack->id = id;
+ fill_thread_layout_stack(&stack->p, stack_size);
+ pt_insert(thread_partitions, (pt_leaf_t)stack);
+
+ thread_partition_t *tls = private_malloc(sizeof(thread_partition_t));
+ tls->id = id;
+ fill_thread_layout_tls(&tls->p);
+ pt_insert(thread_partitions, (pt_leaf_t)tls);
+
+# if defined(E_ACSL_DEBUG) && defined(E_ACSL_DEBUG_VERBOSE)
+ DLOG(">>> Thread stack -------------\n");
+ print_memory_partition(&stack->p);
+ DLOG(">>> Thread TLS ---------------\n");
+ print_memory_partition(&tls->p);
+# endif
+}
+
+void clean_thread_shadow_layout() {
+ DASSERT(thread_partitions != NULL);
+ pt_remove_if(thread_partitions, tp_is_same_thread);
+}
+
+/*! \return The memory segment corresponding to the given address or NULL if no
+ memory segment can be found. */
+static memory_partition *find_thread_partition(uintptr_t addr) {
+ memory_partition *result = NULL;
+ if (thread_partitions != NULL) {
+ thread_partition_t *tp =
+ (thread_partition_t *)pt_find(thread_partitions, (void *)addr);
+ if (tp != NULL) {
+ result = &tp->p;
+ }
+ }
+ return result;
+}
+
+int is_on_thread(uintptr_t addr) {
+ memory_partition *thread_partition = find_thread_partition(addr);
+ return thread_partition != NULL;
+}
+
+intptr_t primary_thread_shadow(uintptr_t addr) {
+ memory_partition *thread_partition = find_thread_partition(addr);
+ return SHADOW_ACCESS(addr, thread_partition->primary.shadow_offset);
+}
+
+intptr_t secondary_thread_shadow(uintptr_t addr) {
+ memory_partition *thread_partition = find_thread_partition(addr);
+ return SHADOW_ACCESS(addr, thread_partition->secondary.shadow_offset);
+}
+
+# ifdef E_ACSL_TEMPORAL
+intptr_t temporal_primary_thread_shadow(uintptr_t addr) {
+ memory_partition *thread_partition = find_thread_partition(addr);
+ return SHADOW_ACCESS(addr, thread_partition->temporal_primary.shadow_offset);
+}
+
+intptr_t temporal_secondary_thread_shadow(uintptr_t addr) {
+ memory_partition *thread_partition = find_thread_partition(addr);
+ return SHADOW_ACCESS(addr,
+ thread_partition->temporal_secondary.shadow_offset);
+}
+# endif // E_ACSL_TEMPORAL
+
+/* }}} */
+
+/************************************************************************/
+/*** Pthread integration {{{ ***/
+/************************************************************************/
+
+/*! Wrapper around the original argument used in `pthread_create`. */
+typedef struct eacsl_pthread_wrapper {
+ /*! The original function pointer given to `pthread_create`. */
+ pthread_routine_t start_routine;
+ /*! The original argument given to `pthread_create`. */
+ void *restrict arg;
+ /*! The stack size of the created thread. */
+ size_t stack_size;
+} eacsl_pthread_wrapper_t;
+
+/*! \brief Cleanup function called before destroying the thread.
+
+ The shadow layout for the thread is destroyed and the memory allocated for
+ the wrapper is freed. */
+static void eacsl_pthread_cleanup(void *arg) {
+ clean_thread_shadow_layout();
+ private_free((eacsl_pthread_wrapper_t *)arg);
+}
+
+/*! \brief Wrapper function given to `pthread_create` instead of the original
+ function.
+
+ Initialize the shadow layout and register the cleanup function. */
+static void *eacsl_pthread_wrapper(void *arg) {
+ void *res = NULL;
+ eacsl_pthread_wrapper_t *wrapped = (eacsl_pthread_wrapper_t *)arg;
+ init_thread_shadow_layout(wrapped->stack_size);
+
+ // Register cleanup function
+ pthread_cleanup_push(eacsl_pthread_cleanup, arg);
+ // Execute original thread function
+ res = wrapped->start_routine(wrapped->arg);
+ // Pop and execute (argument is 1) the cleanup function
+ pthread_cleanup_pop(1);
+ return res;
+}
+
+int eacsl_pthread_create(pthread_t *restrict thread,
+ const pthread_attr_t *restrict original_attr,
+ pthread_routine_t start_routine, void *restrict arg) {
+ // Initialize the thread partitions trie on the first execution of this
+ // function
+ E_ACSL_RUN_ONCE(create_thread_partitions_trie);
+
+ // Create a wrapper for the original routine and arguments
+ eacsl_pthread_wrapper_t *wrapped =
+ private_malloc(sizeof(eacsl_pthread_wrapper_t));
+ wrapped->start_routine = start_routine;
+ wrapped->arg = arg;
+
+ // We need pthread creation attributes to customize the stack size for the
+ // thread. If the user already provided pthread creation attributes, we can
+ // update those, otherwise we need to use our own structure
+ pthread_attr_t attr;
+ pthread_attr_t *pattr;
+ if (original_attr == NULL) {
+ // There are no original attributes, initialize a new structure
+ pthread_attr_init(&attr);
+ pattr = &attr;
+ } else {
+ // There are original attributes, use them
+ pattr = (pthread_attr_t *)original_attr;
+ }
+
+ // Update the stack size for the new thread, either to the default value set
+ // in E-ACSL, or twice the original stack size if the original stack size is
+ // already greater than the default value of E-ACSL
+ size_t original_stack_size;
+ pthread_attr_getstacksize(pattr, &original_stack_size);
+ if (original_stack_size >= E_ACSL_THREAD_STACK_SIZE * MB) {
+ wrapped->stack_size = original_stack_size * 2;
+ } else {
+ wrapped->stack_size = E_ACSL_THREAD_STACK_SIZE * MB;
+ }
+ pthread_attr_setstacksize(pattr, wrapped->stack_size);
+
+ // Create the thread using our custom wrapper routine
+ int result = pthread_create(thread, pattr, eacsl_pthread_wrapper, wrapped);
+
+ // Destroy the attributes if we created them earlier, or restore the stack
+ // size to its original value otherwise
+ if (original_attr == NULL) {
+ pthread_attr_destroy(pattr);
+ } else {
+ pthread_attr_setstacksize(pattr, original_stack_size);
+ }
+
+ return result;
+}
+
+/* }}} */
+
+#else // E_ACSL_CONCURRENCY_PTHREAD
+
+# include <errno.h>
+
+# include "../../internals/e_acsl_private_assert.h"
+
+# define CONCURRENCY_ABORT_MESSAGE \
+ "Compile with option '--concurrency' of e-acsl-gcc.sh to support " \
+ "concurrency.\n" \
+ "When compiling without e-acsl-gcc.sh, E_ACSL_CONCURRENCY_PTHREAD must\n " \
+ "be defined and the pthread library linked.\n"
+
+void init_thread_shadow_layout(size_t stack_size) {
+ private_abort(CONCURRENCY_ABORT_MESSAGE);
+}
+
+void clean_thread_shadow_layout() {
+ private_abort(CONCURRENCY_ABORT_MESSAGE);
+}
+
+int is_on_thread(uintptr_t addr) {
+ return 0;
+}
+
+intptr_t primary_thread_shadow(uintptr_t addr) {
+ private_abort(CONCURRENCY_ABORT_MESSAGE);
+ return 0;
+}
+
+intptr_t secondary_thread_shadow(uintptr_t addr) {
+ private_abort(CONCURRENCY_ABORT_MESSAGE);
+ return 0;
+}
+
+# ifdef E_ACSL_TEMPORAL
+intptr_t temporal_primary_thread_shadow(uintptr_t addr) {
+ private_abort(CONCURRENCY_ABORT_MESSAGE);
+ return 0;
+}
+
+intptr_t temporal_secondary_thread_shadow(uintptr_t addr) {
+ private_abort(CONCURRENCY_ABORT_MESSAGE);
+ return 0;
+}
+# endif // E_ACSL_TEMPORAL
+
+extern int pthread_create(pthread_t *restrict thread,
+ const pthread_attr_t *restrict attr,
+ pthread_routine_t start_routine, void *restrict arg);
+
+int eacsl_pthread_create(pthread_t *restrict thread,
+ const pthread_attr_t *restrict original_attr,
+ pthread_routine_t start_routine, void *restrict arg) {
+ private_abort(CONCURRENCY_ABORT_MESSAGE);
+ return EPERM;
+}
+
+#endif // E_ACSL_CONCURRENCY_PTHREAD
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.h b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.h
new file mode 100644
index 0000000000000000000000000000000000000000..73debfe97a012dfd45e06091ea398b5e5b8b42f6
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.h
@@ -0,0 +1,66 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2021 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+/*! ***********************************************************************
+ * \file
+ * \brief E-ACSL concurrency support for the shadow memory model.
+***************************************************************************/
+
+#ifndef E_ACSL_SHADOW_CONCURRENCY_H
+#define E_ACSL_SHADOW_CONCURRENCY_H
+
+/* Default size of a thread stack tracked via shadow memory */
+#ifndef E_ACSL_THREAD_STACK_SIZE
+# define E_ACSL_THREAD_STACK_SIZE 4
+#endif
+
+/*! \brief Initialize memory layout for the current thread, i.e. determine
+ bounds of program segments, allocate shadow memory spaces and compute
+ offsets.
+
+ \param stack_size The stack size of the current thread. */
+void init_thread_shadow_layout(size_t stack_size);
+
+/*! \brief Deallocate shadow regions used by the runtime analysis for the
+ current thread. */
+void clean_thread_shadow_layout();
+
+/*! \brief Evaluate to true if `addr` is a thread address. */
+int is_on_thread(uintptr_t addr);
+
+/*! \brief Convert a thread address into its primary shadow counterpart. */
+intptr_t primary_thread_shadow(uintptr_t addr);
+
+/*! \brief Convert a thread address into its secondary shadow counterpart. */
+intptr_t secondary_thread_shadow(uintptr_t addr);
+
+#ifdef E_ACSL_TEMPORAL
+/*! \brief Convert a thread address into its primary temporal shadow
+ counterpart. */
+intptr_t temporal_primary_thread_shadow(uintptr_t addr);
+
+/*! \brief Convert a thread address into its secondary temporal shadow
+ counterpart. */
+intptr_t temporal_secondary_thread_shadow(uintptr_t addr);
+#endif
+
+#endif // E_ACSL_SHADOW_CONCURRENCY_H
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 0b52b6595c18fbceb288f85df8a6e757d950356a..8086b280e3a560876fa2a2430598b53b59e446ac 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
@@ -163,7 +163,7 @@ static size_t get_global_size() {
*/
/*! \brief Return byte-size of the TLS segment */
-inline static size_t get_tls_size() {
+inline size_t get_tls_size() {
return PGM_TLS_SIZE;
}
@@ -219,7 +219,7 @@ static void grow_bounds_for_size(uintptr_t *min_bound, uintptr_t *max_bound,
}
/*! \brief Return start address of a program's TLS */
-static uintptr_t get_tls_start() {
+uintptr_t get_tls_start() {
size_t tls_size = get_tls_size();
uintptr_t data = (uintptr_t)&id_tdata, bss = (uintptr_t)&id_tbss;
uintptr_t min_addr = data < bss ? data : bss;
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 3ed69e3d42a564beee5d663e5b2140c70494d4c1..dfc069364e436f22c07b71f5efc0a040308e0fa1 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
@@ -33,6 +33,7 @@
#include "../../internals/e_acsl_config.h"
#include "../../internals/e_acsl_malloc.h"
+#include "e_acsl_shadow_concurrency.h"
/* Default size of a program's heap tracked via shadow memory */
#ifndef E_ACSL_HEAP_SIZE
@@ -109,6 +110,14 @@ size_t get_stack_size();
size_t get_heap_size();
/** }}} */
+/** Thread-local storage information {{{ */
+/*! \brief Return byte-size of the TLS segment */
+size_t get_tls_size();
+
+/*! \brief Return start address of a program's TLS */
+uintptr_t get_tls_start();
+/** }}} */
+
/** Shadow Layout {{{ */
/*****************************************************************************
* Memory Layout *************************************************************
@@ -363,6 +372,13 @@ void clean_shadow_layout();
# define SECONDARY_VDSO_SHADOW(_addr) \
SHADOW_ACCESS(_addr, vdso_secondary_offset)
+/*! \brief Convert a thread address into its primary shadow counterpart */
+# define PRIMARY_THREAD_SHADOW(_addr) primary_thread_shadow((uintptr_t)_addr)
+
+/*! \brief Convert a thread address into its secondary shadow counterpart */
+# define SECONDARY_THREAD_SHADOW(_addr) \
+ secondary_thread_shadow((uintptr_t)_addr)
+
#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)
@@ -431,6 +447,7 @@ void clean_shadow_layout();
: IS_ON_GLOBAL(_addr) ? _region##_GLOBAL_SHADOW(_addr) \
: IS_ON_TLS(_addr) ? _region##_TLS_SHADOW(_addr) \
: IS_ON_VDSO(_addr) ? _region##_VDSO_SHADOW(_addr) \
+ : IS_ON_THREAD(_addr) ? _region##_THREAD_SHADOW(_addr) \
: (intptr_t)0)
// clang-format on
#elif E_ACSL_OS_IS_WINDOWS
@@ -478,11 +495,14 @@ void clean_shadow_layout();
/*! \brief Evaluate to true if _addr is a VDSO address */
# define IS_ON_VDSO(_addr) IS_ON(_addr, mem_layout.vdso.application)
+/*! \brief Evaluate to true if _addr is a thread address */
+# define IS_ON_THREAD(_addr) is_on_thread((uintptr_t)_addr)
+
/*! \brief Shortcut for evaluating an address via ::IS_ON_STACK,
- * ::IS_ON_GLOBAL or ::IS_ON_TLS */
+ * ::IS_ON_GLOBAL, ::IS_ON_TLS or ::IS_ON_THREAD */
# define IS_ON_STATIC(_addr) \
(IS_ON_STACK(_addr) || IS_ON_GLOBAL(_addr) || IS_ON_TLS(_addr) \
- || IS_ON_VDSO(_addr))
+ || IS_ON_VDSO(_addr) || IS_ON_THREAD(_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)
@@ -555,6 +575,14 @@ void clean_shadow_layout();
# define TEMPORAL_SECONDARY_VDSO_SHADOW(_addr) \
SHADOW_ACCESS(_addr, mem_layout.vdso.temporal_secondary.shadow_offset)
+/*! \brief Convert a thread address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_THREAD_SHADOW(_addr) \
+ temporal_primary_thread_shadow((uintptr_t)_addr)
+
+/*! \brief Convert a thread address into its secondary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_THREAD_SHADOW(_addr) \
+ temporal_secondary_thread_shadow((uintptr_t)_addr)
+
# elif E_ACSL_OS_IS_WINDOWS
/*! \brief Convert a text address into its primary temporal shadow counterpart */
# define TEMPORAL_PRIMARY_TEXT_SHADOW(_addr) \