diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index 8c3bf917e67240eafef14c38769cbac2bb745a7a..996b34f14ad9132fca838ee078775934f6b0554c 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -162,7 +162,7 @@ VERSION_FILE=$(FRAMAC_ROOT_SRCDIR)/VERSION EACSL_VERSION:=$(shell sed -e 's/\\(.*\\)/\\1/' $(VERSION_FILE)) -$(EACSL_PLUGIN_DIR)/src/local_config.ml: $(EACSL_PLUGIN_DIR)/Makefile.in $(VERSION_FILE) +$(EACSL_PLUGIN_DIR)/src/local_config.ml: $(EACSL_PLUGIN_DIR)/Makefile $(VERSION_FILE) $(PRINT_MAKING) $@ $(RM) $@ $(ECHO) "(* This file was automatically generated from $<. Don't edit it. *)" >> $@ @@ -272,9 +272,11 @@ EACSL_DLMALLOC_FLAGS = \ -DMSPACES=1 \ -DONLY_MSPACES \ -DMALLOC_ALIGNMENT=32 \ - -DMSPACE_PREFIX="__e_acsl_" + -DMSPACE_PREFIX="__e_acsl_" \ + -DUSE_LOCKS=1 \ + -DUSE_SPIN_LOCKS=1 -$(EACSL_DLMALLOC_LIB): $(EACSL_DLMALLOC_SRC) +$(EACSL_DLMALLOC_LIB): $(EACSL_DLMALLOC_SRC) $(EACSL_PLUGIN_DIR)/Makefile $(MKDIR) $(EACSL_LIBDIR) echo 'CC $<' $(CC) $< -c -O2 -g3 -o$(EACSL_DLMALLOC_OBJ) $(EACSL_DLMALLOC_FLAGS) diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index 063db8bb0c953fde94a122d0501593672f80b3a2..4094ebaa8eee0e8db91424ce5407f67c9989b70f 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -925,6 +925,8 @@ if [ "$OPTION_DLMALLOC_FROM_SOURCES" = "1" -o \ -DONLY_MSPACES \ -DMALLOC_ALIGNMENT=32 \ -DMSPACE_PREFIX=__e_acsl_ \ + -DUSE_LOCKS=1 \ + -DUSE_SPIN_LOCKS=1 \ $OPTION_DLMALLOC_COMPILE_FLAGS " diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c index 984c884ee94e12e6342ae260c6702994fed42d44..b2d2c5fbd2c80412164ffacfd7a4ca3bc839ed05 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c @@ -22,6 +22,10 @@ #include "e_acsl_malloc.h" +#define eacsl_create_mspace export_alias(create_mspace) + +extern mspace eacsl_create_mspace(size_t, int); + struct memory_spaces mem_spaces = { .rtl_mspace = NULL, .heap_mspace = NULL, @@ -32,12 +36,16 @@ struct memory_spaces mem_spaces = { .heap_mspace_least = 0, }; +mspace eacsl_create_locked_mspace(size_t size) { + return eacsl_create_mspace(size, 1); +} + /* \brief Create two memory spaces, one for RTL and the other for application memory. This function *SHOULD* be called before any allocations are made otherwise execution fails */ void eacsl_make_memory_spaces(size_t rtl_size, size_t heap_size) { - mem_spaces.rtl_mspace = eacsl_create_mspace(rtl_size, 0); - mem_spaces.heap_mspace = eacsl_create_mspace(heap_size, 0); + mem_spaces.rtl_mspace = eacsl_create_locked_mspace(rtl_size); + mem_spaces.heap_mspace = eacsl_create_locked_mspace(heap_size); /* Do not use `eacsl_mspace_least_addr` here, as it returns the address of the mspace header. */ mem_spaces.rtl_start = diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h index 83cd59e275e133e57ef7a65cc949124f060f5c3f..57505489d1d105bbf665dce92e122160f7d2b964 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h @@ -28,7 +28,7 @@ * is split into two mspaces (memory spaces). Memory allocation itself is * delegated to a slightly customised version of dlmalloc shipped with the * RTL. The overall pattern is as follows: - * mspace space = eacsl_create_mspace(capacity, locks); + * mspace space = eacsl_create_locked_mspace(capacity); * char *p = eacsl_mspace_malloc(space, size); **************************************************************************/ @@ -70,7 +70,7 @@ void eacsl_destroy_memory_spaces(); /*** Mspace allocators (from dlmalloc) {{{ ***/ /************************************************************************/ -#define eacsl_create_mspace export_alias(create_mspace) +#define eacsl_create_locked_mspace export_alias(create_locked_mspace) #define eacsl_destroy_mspace export_alias(destroy_mspace) #define eacsl_mspace_least_addr export_alias(mspace_least_addr) #define eacsl_mspace_malloc export_alias(mspace_malloc) @@ -93,7 +93,7 @@ struct memory_spaces { }; extern struct memory_spaces mem_spaces; -extern mspace eacsl_create_mspace(size_t, int); +/* Original functions from dlmalloc */ extern size_t eacsl_destroy_mspace(mspace); extern void *eacsl_mspace_malloc(mspace, size_t); extern void eacsl_mspace_free(mspace, void *); @@ -103,6 +103,10 @@ extern void *eacsl_mspace_aligned_alloc(mspace, size_t, size_t); extern int eacsl_mspace_posix_memalign(mspace, void **, size_t, size_t); extern void *eacsl_mspace_least_addr(mspace); +/*! \brief Wrapper around `eacsl_create_mspace` to always create a thread-safe + * mspace. */ +mspace eacsl_create_locked_mspace(size_t size); + /* }}} */ /************************************************************************/ 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 9d1361b8938cc05a4997c58605263386dd829d07..a98804dd8c7e33dfde380cf70b32a980177e2a67 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 @@ -675,7 +675,7 @@ void set_shadow_segment(memory_segment *seg, memory_segment *parent, seg->name = name; seg->shadow_ratio = ratio; seg->size = parent->size / seg->shadow_ratio; - seg->mspace = eacsl_create_mspace(seg->size + SHADOW_SEGMENT_PADDING, 0); + seg->mspace = eacsl_create_locked_mspace(seg->size + SHADOW_SEGMENT_PADDING); seg->start = (uintptr_t)eacsl_mspace_malloc(seg->mspace, 1); seg->end = seg->start + seg->size - 1; seg->shadow_offset = parent->start - seg->start;