From b3f922c35c9d7a7e15b0a70b0d0526aac7023da8 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 9 Nov 2021 16:03:02 +0100
Subject: [PATCH] [eacsl] Add locks for RTL log printing
---
.../instrumentation_model/e_acsl_assert.c | 6 +++++
.../share/e-acsl/internals/e_acsl_debug.c | 2 ++
.../share/e-acsl/internals/e_acsl_rtl_io.c | 24 +++++++++++++++++++
.../share/e-acsl/internals/e_acsl_rtl_io.h | 17 +++++++++++++
.../share/e-acsl/internals/e_acsl_trace.c | 2 ++
.../internals/e_acsl_patricia_trie.c | 2 ++
.../segment_model/e_acsl_segment_tracking.c | 4 ++++
.../segment_model/e_acsl_shadow_concurrency.c | 2 ++
8 files changed, 59 insertions(+)
diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c
index b2b3ad1e9e3..0d1158d3b7b 100644
--- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c
+++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c
@@ -50,6 +50,7 @@ void eacsl_print_values(eacsl_assert_data_t *data) {
void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) {
if (eacsl_runtime_sound_verdict) {
if (!predicate) {
+ RTL_IO_LOCK();
// clang-format off
STDERR("%s: In function '%s'\n"
"%s:%d: Error: %s failed:\n"
@@ -60,6 +61,7 @@ void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) {
data->pred_txt);
// clang-format on
eacsl_print_values(data);
+ RTL_IO_UNLOCK();
if (data->blocking) {
# ifndef E_ACSL_NO_ASSERT_FAIL /* Do fail on assertions */
# ifdef E_ACSL_FAIL_EXITCODE /* Fail by exit with a given code */
@@ -72,6 +74,7 @@ void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) {
}
# ifdef E_ACSL_DEBUG_ASSERT
else {
+ RTL_IO_LOCK();
// clang-format off
STDERR("%s: In function '%s'\n"
"%s:%d: %s valid:\n"
@@ -81,9 +84,11 @@ void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) {
data->pred_txt);
// clang-format on
eacsl_print_values(data);
+ RTL_IO_UNLOCK();
}
# endif
} else {
+ RTL_IO_LOCK();
// clang-format off
STDERR("%s: In function '%s'\n"
"%s:%d: Warning: no sound verdict for %s (guess: %s).\n"
@@ -94,6 +99,7 @@ void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) {
data->pred_txt);
// clang-format on
eacsl_print_values(data);
+ RTL_IO_UNLOCK();
}
}
#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c
index 9e7ee446a82..15ce0534410 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c
@@ -88,6 +88,7 @@ void initialize_report_file(int *argc, char ***argv) {
void describe_run() {
#if defined(E_ACSL_VERBOSE)
+ RTL_IO_LOCK();
rtl_printf(
"/* ========================================================= */\n");
rtl_printf(" * E-ACSL instrumented run\n");
@@ -99,5 +100,6 @@ void describe_run() {
rtl_printf(" * Format Checks: %s\n", E_ACSL_FORMAT_VALIDITY_DESC);
rtl_printf(
"/* ========================================================= */\n");
+ RTL_IO_UNLOCK();
#endif
}
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c
index 45bfaacbd04..78989ecd128 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c
@@ -45,6 +45,7 @@
#include <stdint.h>
#include <unistd.h>
+#include "e_acsl_concurrency.h"
#include "e_acsl_rtl_io.h"
/*! \brief Test if we can still write `n + 1` characters to the buffer according
@@ -68,6 +69,23 @@
typedef void (*putcf)(void *, size_t *, char);
+#ifdef E_ACSL_CONCURRENCY_PTHREAD
+static pthread_mutex_t rtl_io_global_mutex_value;
+
+static void rtl_io_initialize_global_mutex() {
+ pthread_mutexattr_t attr;
+ pthread_mutexattr_init(&attr);
+ pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE);
+ pthread_mutex_init(&rtl_io_global_mutex_value, &attr);
+ pthread_mutexattr_destroy(&attr);
+}
+
+pthread_mutex_t *rtl_io_global_mutex() {
+ E_ACSL_RUN_ONCE(rtl_io_initialize_global_mutex);
+ return &rtl_io_global_mutex_value;
+}
+#endif
+
/* Unsigned long integers to string conversion (%u) */
static void uli2a(unsigned long int num, unsigned int base, int uc, char *bf) {
int n = 0;
@@ -424,7 +442,9 @@ int rtl_printf(char *fmt, ...) {
}
int rtl_vprintf(char *fmt, va_list vlist) {
+ RTL_IO_LOCK();
_format(NULL, NULL, _charc_stdout, fmt, vlist);
+ RTL_IO_UNLOCK();
return 1;
}
@@ -437,7 +457,9 @@ int rtl_eprintf(char *fmt, ...) {
}
int rtl_veprintf(char *fmt, va_list vlist) {
+ RTL_IO_LOCK();
_format(NULL, NULL, _charc_stderr, fmt, vlist);
+ RTL_IO_UNLOCK();
return 1;
}
@@ -450,8 +472,10 @@ int rtl_dprintf(int fd, char *fmt, ...) {
}
int rtl_vdprintf(int fd, char *fmt, va_list vlist) {
+ RTL_IO_LOCK();
intptr_t fd_long = fd;
_format((void *)fd_long, NULL, _charc_file, fmt, vlist);
+ RTL_IO_UNLOCK();
return 1;
}
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h
index f26a145efd2..779bc360524 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h
@@ -77,6 +77,23 @@
#define STDOUT(...) rtl_printf(__VA_ARGS__)
#define STDERR(...) rtl_eprintf(__VA_ARGS__)
+#ifdef E_ACSL_CONCURRENCY_PTHREAD
+# include <pthread.h>
+
+/*! \brief Returns the global mutex for RTL printing. This mutex is recursive so
+ multiple locks can be acquired from the same thread. */
+pthread_mutex_t *rtl_io_global_mutex();
+
+/*! \brief Lock the global RTL printing mutex. */
+# define RTL_IO_LOCK() pthread_mutex_lock(rtl_io_global_mutex());
+
+/*! \brief Unlock the global RTL printing mutex. */
+# define RTL_IO_UNLOCK() pthread_mutex_unlock(rtl_io_global_mutex());
+#else
+# define RTL_IO_LOCK()
+# define RTL_IO_UNLOCK()
+#endif
+
/* Replacement for printf with support for the above specifiers */
int rtl_printf(char *fmt, ...);
int rtl_vprintf(char *fmt, va_list vlist);
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
index 60888729cb2..631322b9826 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
@@ -77,6 +77,7 @@ static int native_backtrace(void **array, int size) {
void trace() {
#if E_ACSL_OS_IS_LINUX
+ RTL_IO_LOCK();
int size = 24;
void **bb = private_malloc(sizeof(void *) * size);
@@ -112,5 +113,6 @@ void trace() {
counter++;
}
STDERR("/***************************************/\n");
+ RTL_IO_UNLOCK();
#endif /* E_ACSL_OS_IS_LINUX */
}
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 816b086f859..4872e5ce2bf 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
@@ -606,6 +606,7 @@ static void pt_print_node(const pt_struct_t *pt, pt_node_t *node, int depth) {
}
void pt_print(const pt_struct_t *pt) {
+ RTL_IO_LOCK();
DLOG("------------DEBUG\n");
if (pt != NULL) {
E_ACSL_RLOCK(pt->lock);
@@ -615,5 +616,6 @@ void pt_print(const pt_struct_t *pt) {
DLOG("Patricia trie is NULL\n");
}
DLOG("-----------------\n");
+ RTL_IO_UNLOCK();
}
#endif // E_ACSL_DEBUG
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 add2d3db74d..f1f378fd017 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
@@ -1111,10 +1111,12 @@ void print_heap_shadows(uintptr_t addr) {
}
void print_shadows(uintptr_t addr, size_t size) {
+ RTL_IO_LOCK();
if (IS_ON_STATIC(addr))
print_static_shadows(addr, size);
else if (IS_ON_HEAP(addr))
print_heap_shadows(addr);
+ RTL_IO_UNLOCK();
}
void print_memory_segment(struct memory_segment *p, char *lab, int off) {
@@ -1147,6 +1149,7 @@ void print_memory_partition(struct memory_partition *p) {
}
void print_shadow_layout() {
+ RTL_IO_LOCK();
DLOG(">>> HEAP ---------------------\n");
print_memory_partition(&mem_layout.heap);
DLOG(">>> STACK --------------------\n");
@@ -1171,6 +1174,7 @@ void print_shadow_layout() {
print_memory_partition(&mem_layout.rdata);
# endif
DLOG(">>> --------------------------\n");
+ RTL_IO_UNLOCK();
}
const char *which_segment(uintptr_t addr) {
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 7ac2d7d13bd..042eef56fbc 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
@@ -213,10 +213,12 @@ void init_thread_shadow_layout(size_t stack_size) {
pt_insert(thread_partitions, (pt_leaf_t)tls);
# if defined(E_ACSL_DEBUG) && defined(E_ACSL_DEBUG_VERBOSE)
+ RTL_IO_LOCK();
DLOG(">>> Thread stack -------------\n");
print_memory_partition(&stack->p);
DLOG(">>> Thread TLS ---------------\n");
print_memory_partition(&tls->p);
+ RTL_IO_UNLOCK();
# endif
// Safe location tracking for thread-specific locations
--
GitLab