diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h
index 7f3d799a5653c5f96f1b2d490869d534a460cd4a..617807e4b7b2e1b43668884afe979097b3838676 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h
@@ -21,7 +21,7 @@
/**************************************************************************/
/*! ***********************************************************************
- * \file e_acsl_bittree.h
+ * \file e_acsl_bittree.h
* \brief Patricia Trie API Implementation
***************************************************************************/
@@ -468,7 +468,7 @@ static void bt_print_node(bt_node * ptr, int depth) {
}
}
-static void bt_print() {
+static void bt_print_tree() {
DLOG("------------DEBUG\n");
bt_print_node(bt_root, 0);
DLOG("-----------------\n");
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h
index 5f32ca605431b54c86ca074f0eb03e52c5b273ab..2913a829f55684b268d06caccad8a870389df99c 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h
@@ -46,7 +46,7 @@ typedef struct bt_block bt_block;
/*! \brief Structure representing a bittree node */
struct bt_node {
_Bool is_leaf;
- size_t addr, mask;
+ size_t addr, mask;
struct bt_node * left, * right, * parent;
bt_block * leaf;
};
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
index 8aab4628b7b58d77ca15fc02de73dc150c4b0aac..406eebb83b1f70074012f63812eef6fa62261e73 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
@@ -21,8 +21,8 @@
/**************************************************************************/
/*! ***********************************************************************
- * \file e_acsl_bittree_mmodel.c
- * \brief Implementation of E-ACSL public API using a memory model based
+ * \file e_acsl_bittree_mmodel.c
+ * \brief Implementation of E-ACSL public API using a memory model based
* on Patricia Trie. See e_acsl_mmodel_api.h for details.
***************************************************************************/
@@ -38,8 +38,9 @@
#include "e_acsl_mmodel_api.h"
#include "e_acsl_bittree.h"
-size_t __e_acsl_heap_size = 0;
-
+/**************************/
+/* SUPPORT {{{ */
+/**************************/
static const int nbr_bits_to_1[256] = {
0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,1,2,2,3,2,3,
3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,1,2,2,3,2,3,3,4,2,3,3,4,
@@ -50,182 +51,28 @@ static const int nbr_bits_to_1[256] = {
4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
};
-size_t __get_memory_size(void) {
- return __e_acsl_heap_size;
-}
-
/* given the size of the memory block (_size) return (or rather evaluate to)
* size in bytes requred to represent its partial initialization */
#define needed_bytes(_size) \
((_size % 8) == 0 ? (_size/8) : (_size/8 + 1))
+/* }}} */
/**************************/
-/* ALLOCATION */
+/* HEAP USAGE {{{ */
/**************************/
+static size_t heap_size = 0;
-/* store the block of size bytes starting at ptr, the new block is returned.
- * Warning: the return type is implicitly (bt_block*). */
-void* __e_acsl_store_block(void* ptr, size_t size) {
- bt_block * tmp;
- DASSERT(ptr != NULL);
- tmp = native_malloc(sizeof(bt_block));
- DASSERT(tmp != NULL);
- tmp->ptr = (size_t)ptr;
- tmp->size = size;
- tmp->init_ptr = NULL;
- tmp->init_bytes = 0;
- tmp->is_readonly = false;
- tmp->freeable = false;
- bt_insert(tmp);
- return tmp;
-}
-
-/* remove the block starting at ptr */
-void __e_acsl_delete_block(void* ptr) {
- DASSERT(ptr != NULL);
- bt_block * tmp = bt_lookup(ptr);
- DASSERT(tmp != NULL);
- bt_clean_block_init(tmp);
- bt_remove(tmp);
- native_free(tmp);
-}
-
-/* allocate size bytes and store the returned block
- * for further information, see malloc */
-void* malloc(size_t size) {
- void * tmp;
- bt_block * new_block;
- if(size <= 0)
- return NULL;
- tmp = native_malloc(size);
- if(tmp == NULL)
- return NULL;
- new_block = __e_acsl_store_block(tmp, size);
- __e_acsl_heap_size += size;
- DASSERT(new_block != NULL && (void*)new_block->ptr != NULL);
- new_block->freeable = true;
- return (void*)new_block->ptr;
-}
-
-/* free the block starting at ptr,
- * for further information, see free */
-void free(void* ptr) {
- bt_block * tmp;
- if(ptr == NULL)
- return;
- tmp = bt_lookup(ptr);
- DASSERT(tmp != NULL);
- native_free(ptr);
- bt_clean_block_init(tmp);
- __e_acsl_heap_size -= tmp->size;
- bt_remove(tmp);
- native_free(tmp);
-}
-
-int __e_acsl_freeable(void* ptr) {
- bt_block * tmp;
- if(ptr == NULL)
- return false;
- tmp = bt_lookup(ptr);
- if(tmp == NULL)
- return false;
- return tmp->freeable;
-}
-
-/* resize the block starting at ptr to fit its new size,
- * for further information, see realloc */
-void* realloc(void* ptr, size_t size) {
- bt_block * tmp;
- void * new_ptr;
- /* ptr is NULL - malloc */
- if(ptr == NULL)
- return malloc(size);
- /* size is zero - free */
- if(size == 0) {
- free(ptr);
- return NULL;
- }
- tmp = bt_lookup(ptr);
- DASSERT(tmp != NULL);
- new_ptr = native_realloc((void*)tmp->ptr, size);
- if(new_ptr == NULL)
- return NULL;
- __e_acsl_heap_size -= tmp->size;
- /* realloc changes start address -- re-enter the element */
- if (tmp->ptr != (size_t)new_ptr) {
- bt_remove(tmp);
- tmp->ptr = (size_t)new_ptr;
- bt_insert(tmp);
- }
- /* uninitialized, do nothing */
- if(tmp->init_bytes == 0) ;
- /* already fully initialized block */
- else if (tmp->init_bytes == tmp->size) {
- /* realloc smaller block */
- if(size <= tmp->size)
- /* adjust new size, allocation not necessary */
- tmp->init_bytes = size;
- /* realloc bigger larger block */
- else {
- /* size of tmp->init_ptr in the new block */
- int nb = needed_bytes(size);
- /* number of bits that need to be set in tmp->init_ptr */
- int nb_old = needed_bytes(tmp->size);
- /* allocate memory to store partial initialization */
- tmp->init_ptr = native_calloc(1, nb);
- /* carry out initialization of the old block */
- setbits(tmp->init_ptr, tmp->size);
- }
- }
- /* contains initialized and uninitialized parts */
- else {
- int nb = needed_bytes(size);
- int nb_old = needed_bytes(tmp->size);
- int i;
- tmp->init_ptr = native_realloc(tmp->init_ptr, nb);
- for(i = nb_old; i < nb; i++)
- tmp->init_ptr[i] = 0;
- tmp->init_bytes = 0;
- for(i = 0; i < nb; i++)
- tmp->init_bytes += nbr_bits_to_1[tmp->init_ptr[i]];
- if(tmp->init_bytes == size || tmp->init_bytes == 0) {
- native_free(tmp->init_ptr);
- tmp->init_ptr = NULL;
- }
- }
- tmp->size = size;
- tmp->freeable = true;
- __e_acsl_heap_size += size;
- return (void*)tmp->ptr;
-}
-
-/* allocate memory for an array of nbr_block elements of size_block size,
- * this memory is set to zero, the returned block is stored,
- * for further information, see calloc */
-void* calloc(size_t nbr_block, size_t size_block) {
- void * tmp;
- size_t size = nbr_block * size_block;
- bt_block * new_block;
- if(size <= 0)
- return NULL;
- tmp = native_calloc(nbr_block, size_block);
- if(tmp == NULL)
- return NULL;
- new_block = __e_acsl_store_block(tmp, size);
- __e_acsl_heap_size += nbr_block * size_block;
- DASSERT(new_block != NULL && (void*)new_block->ptr != NULL);
- /* Mark allocated block as freeable and initialized */
- new_block->freeable = true;
- new_block->init_bytes = size;
- return (void*)new_block->ptr;
+static size_t get_heap_size(void) {
+ return heap_size;
}
+/* }}} */
/**************************/
-/* INITIALIZATION */
+/* INITIALIZATION {{{ */
/**************************/
/* mark the size bytes of ptr as initialized */
-void __e_acsl_initialize (void * ptr, size_t size) {
+static void initialize (void * ptr, size_t size) {
bt_block * tmp;
if(!ptr)
return;
@@ -275,7 +122,7 @@ void __e_acsl_initialize (void * ptr, size_t size) {
}
/* mark all bytes of ptr as initialized */
-void __e_acsl_full_init (void * ptr) {
+static void full_init (void * ptr) {
bt_block * tmp;
if (ptr == NULL)
return;
@@ -292,7 +139,7 @@ void __e_acsl_full_init (void * ptr) {
}
/* mark a block as read-only */
-void __e_acsl_readonly (void * ptr) {
+static void readonly(void * ptr) {
bt_block * tmp;
if (ptr == NULL)
return;
@@ -301,13 +148,24 @@ void __e_acsl_readonly (void * ptr) {
return;
tmp->is_readonly = true;
}
+/* }}} */
/**************************/
-/* PREDICATES */
+/* PREDICATES {{{ */
/**************************/
+static int freeable(void* ptr) {
+ bt_block * tmp;
+ if(ptr == NULL)
+ return false;
+ tmp = bt_lookup(ptr);
+ if(tmp == NULL)
+ return false;
+ return tmp->freeable;
+}
+
/* return whether the size bytes of ptr are initialized */
-int __e_acsl_initialized (void * ptr, size_t size) {
+static int initialized(void * ptr, size_t size) {
unsigned i;
bt_block * tmp = bt_find(ptr);
if(tmp == NULL)
@@ -320,7 +178,7 @@ int __e_acsl_initialized (void * ptr, size_t size) {
if(tmp->init_bytes == tmp->size)
return true;
- /* see implementation of function __e_acsl_initialize for details */
+ /* see implementation of function `initialize` for details */
for(i = 0; i < size; i++) {
size_t offset = (uintptr_t)ptr - tmp->ptr + i;
int byte = offset/8;
@@ -332,90 +190,293 @@ int __e_acsl_initialized (void * ptr, size_t size) {
}
/* return the length (in bytes) of the block containing ptr */
-size_t __e_acsl_block_length(void* ptr) {
+static size_t block_length(void* ptr) {
bt_block * tmp = bt_find(ptr);
- /* Hard failure when un-allocated memory is used */
+ /* Hard failure when un-allocated memory is used */
vassert(tmp != NULL, "\\block_length of unallocated memory", NULL);
return tmp->size;
}
/* return whether the size bytes of ptr are readable/writable */
-int __e_acsl_valid(void* ptr, size_t size) {
- bt_block * tmp;
+static int valid(void* ptr, size_t size) {
if(ptr == NULL)
return false;
- tmp = bt_find(ptr);
- return (tmp == NULL) ?
- false : ( tmp->size - ( (size_t)ptr - tmp->ptr ) >= size
- && !tmp->is_readonly);
+ bt_block * tmp = bt_find(ptr);
+ return (tmp == NULL) ? false :
+ (tmp->size - ((size_t)ptr - tmp->ptr ) >= size && !tmp->is_readonly);
}
/* return whether the size bytes of ptr are readable */
-int __e_acsl_valid_read(void* ptr, size_t size) {
- bt_block * tmp;
+static int valid_read(void* ptr, size_t size) {
if(ptr == NULL)
return false;
- tmp = bt_find(ptr);
+ bt_block * tmp = bt_find(ptr);
return (tmp == NULL) ?
false : (tmp->size - ((size_t)ptr - tmp->ptr) >= size);
}
/* return the base address of the block containing ptr */
-void* __e_acsl_base_addr(void* ptr) {
+static void* base_addr(void* ptr) {
bt_block * tmp = bt_find(ptr);
vassert(tmp != NULL, "\\base_addr of unallocated memory", NULL);
return (void*)tmp->ptr;
}
/* return the offset of `ptr` within its block */
-int __e_acsl_offset(void* ptr) {
+static int offset(void* ptr) {
bt_block * tmp = bt_find(ptr);
vassert(tmp != NULL, "\\offset of unallocated memory", NULL);
- return ((size_t)ptr - tmp->ptr);
+ return ((uintptr_t)ptr - tmp->ptr);
}
+/* }}} */
/**************************/
-/* PROGRAM INITIALIZATION */
+/* ALLOCATION {{{ */
/**************************/
+/* STACK ALLOCATION {{{ */
+/* store the block of size bytes starting at ptr, the new block is returned.
+ * Warning: the return type is implicitly (bt_block*). */
+static void* store_block(void* ptr, size_t size) {
+ bt_block * tmp;
+ DASSERT(ptr != NULL);
+ tmp = native_malloc(sizeof(bt_block));
+ DASSERT(tmp != NULL);
+ tmp->ptr = (uintptr_t)ptr;
+ tmp->size = size;
+ tmp->init_ptr = NULL;
+ tmp->init_bytes = 0;
+ tmp->is_readonly = false;
+ tmp->freeable = false;
+ bt_insert(tmp);
+ return tmp;
+}
+
+/* remove the block starting at ptr */
+static void delete_block(void* ptr) {
+ DASSERT(ptr != NULL);
+ bt_block * tmp = bt_lookup(ptr);
+ DASSERT(tmp != NULL);
+ bt_clean_block_init(tmp);
+ bt_remove(tmp);
+ native_free(tmp);
+}
+/* }}} */
+
+/* HEAP ALLOCATION {{{ */
+/*! \brief Replacement for `malloc` with memory tracking */
+static void* bittree_malloc(size_t size) {
+ if(size == 0)
+ return NULL;
+
+ void *res = native_malloc(size);
+ if (res) {
+ bt_block * new_block = store_block(res, size);
+ heap_size += size;
+ new_block->freeable = true;
+ }
+ return res;
+}
+
+/*! \brief Replacement for `calloc` with memory tracking */
+static void* bittree_calloc(size_t nbr_block, size_t size_block) {
+ /* FIXME: Need an integer overflow check here */
+ size_t size = nbr_block * size_block;
+ if (size == 0)
+ return NULL;
+
+ void *res = native_calloc(nbr_block, size_block);
+ if (res) {
+ bt_block * new_block = store_block(res, size);
+ heap_size += size;
+ new_block->freeable = 1;
+ /* Mark allocated block as freeable and initialized */
+ new_block->init_bytes = size;
+ }
+ return res;
+}
+
+/*! \brief Replacement for `aligned_alloc` with memory tracking */
+static void *bittree_aligned_alloc(size_t alignment, size_t size) {
+ /* Check if:
+ * - size and alignment are greater than zero
+ * - alignment is a power of 2
+ * - size is a multiple of alignment */
+ if (!size || !alignment || !powof2(alignment) || (size%alignment))
+ return NULL;
+
+ void *res = native_aligned_alloc(alignment, size);
+ if (res) {
+ bt_block * new_block = store_block(res, size);
+ new_block->freeable = 1;
+ heap_size += size;
+ }
+ return res;
+}
+
+/*! \brief Replacement for `posix_memalign` with memory tracking */
+static int bittree_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*) */
+ if (!size || !alignment || !powof2(alignment) || alignment%sizeof(void*))
+ return -1;
+
+ /* Make sure that the first argument to posix memalign is indeed allocated */
+ vassert(valid(memptr, sizeof(void*)),
+ "\\invalid memptr in posix_memalign", NULL);
+
+ int res = native_posix_memalign(memptr, alignment, size);
+ if (!res) {
+ bt_block * new_block = store_block(*memptr, size);
+ new_block->freeable = 1;
+ heap_size += size;
+ }
+ return res;
+}
+
+/*! \brief Replacement for `realloc` with memory tracking */
+static void* bittree_realloc(void* ptr, size_t size) {
+ bt_block * tmp;
+ void * new_ptr;
+ /* ptr is NULL - malloc */
+ if(ptr == NULL)
+ return malloc(size);
+ /* size is zero - free */
+ if(size == 0) {
+ free(ptr);
+ return NULL;
+ }
+ tmp = bt_lookup(ptr);
+ DASSERT(tmp != NULL);
+ new_ptr = native_realloc((void*)tmp->ptr, size);
+ if(new_ptr == NULL)
+ return NULL;
+ heap_size -= tmp->size;
+ /* realloc changes start address -- re-enter the element */
+ if (tmp->ptr != (uintptr_t)new_ptr) {
+ bt_remove(tmp);
+ tmp->ptr = (uintptr_t)new_ptr;
+ bt_insert(tmp);
+ }
+ /* uninitialized, do nothing */
+ if(tmp->init_bytes == 0) ;
+ /* already fully initialized block */
+ else if (tmp->init_bytes == tmp->size) {
+ /* realloc smaller block */
+ if (size <= tmp->size) {
+ /* adjust new size, allocation not necessary */
+ tmp->init_bytes = size;
+ /* realloc bigger larger block */
+ } else {
+ /* size of tmp->init_ptr in the new block */
+ int nb = needed_bytes(size);
+ /* number of bits that need to be set in tmp->init_ptr */
+ int nb_old = needed_bytes(tmp->size);
+ /* allocate memory to store partial initialization */
+ tmp->init_ptr = native_calloc(1, nb);
+ /* carry out initialization of the old block */
+ setbits(tmp->init_ptr, tmp->size);
+ }
+ } else { /* contains initialized and uninitialized parts */
+ int nb = needed_bytes(size);
+ int nb_old = needed_bytes(tmp->size);
+ int i;
+ tmp->init_ptr = native_realloc(tmp->init_ptr, nb);
+ for (i = nb_old; i < nb; i++)
+ tmp->init_ptr[i] = 0;
+ tmp->init_bytes = 0;
+ for (i = 0; i < nb; i++)
+ tmp->init_bytes += nbr_bits_to_1[tmp->init_ptr[i]];
+ if (tmp->init_bytes == size || tmp->init_bytes == 0) {
+ native_free(tmp->init_ptr);
+ tmp->init_ptr = NULL;
+ }
+ }
+ tmp->size = size;
+ tmp->freeable = true;
+ heap_size += size;
+ return (void*)tmp->ptr;
+}
+
+/*! \brief Replacement for `free` with memory tracking */
+static void bittree_free(void* ptr) {
+ if (!ptr)
+ return;
+ bt_block * res = bt_lookup(ptr);
+ if (!res) {
+ vabort("Not a start of block (%a) in free\n", ptr);
+ } else {
+ heap_size -= res->size;
+ native_free(ptr);
+ bt_clean_block_init(res);
+ bt_remove(res);
+ }
+}
+/* }}} */
+/* }}} */
+
+/******************************/
+/* PROGRAM INITIALIZATION {{{ */
+/******************************/
+
/* erase the content of the abstract structure */
-void __e_acsl_memory_clean() {
+static void memory_clean() {
bt_clean();
}
/* add `argv` to the memory model */
-static void __init_argv(int argc, char **argv) {
+static void init_argv(int argc, char **argv) {
int i;
- __e_acsl_store_block(argv, (argc+1)*sizeof(char*));
- __e_acsl_full_init(argv);
+ store_block(argv, (argc+1)*sizeof(char*));
+ full_init(argv);
for (i = 0; i < argc; i++) {
- __e_acsl_store_block(argv[i], strlen(argv[i])+1);
- __e_acsl_full_init(argv[i]);
+ store_block(argv[i], strlen(argv[i])+1);
+ full_init(argv[i]);
}
}
-void __e_acsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
+static void memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
arch_assert(ptr_size);
if (argc_ref)
- __init_argv(*argc_ref, *argv_ref);
-}
-
-/**********************/
-/* DEBUG */
-/**********************/
-#ifdef E_ACSL_DEBUG
-/*! \brief print the information about a tracked block */
-void __e_acsl_print_block (bt_block * ptr) {
- bt_print_block(ptr);
-}
-
-/*! \brief print the content of the bittree */
-void __e_acsl_print_bittree() {
- bt_print();
+ init_argv(*argc_ref, *argv_ref);
}
+/* }}} */
+
+/* API BINDINGS {{{ */
+/* Heap allocation (native) */
+strong_alias(bittree_malloc, malloc)
+strong_alias(bittree_calloc, calloc)
+strong_alias(bittree_realloc, realloc)
+strong_alias(bittree_free, free)
+strong_alias(bittree_posix_memalign, posix_memalign)
+strong_alias(bittree_aligned_alloc, aligned_alloc)
+/* Explicit tracking */
+public_alias(delete_block)
+public_alias(store_block)
+/* Predicates */
+public_alias(offset)
+public_alias(base_addr)
+public_alias(valid_read)
+public_alias(valid)
+public_alias(block_length)
+public_alias(initialized)
+public_alias(freeable)
+public_alias(readonly)
+/* Block initialization */
+public_alias(initialize)
+public_alias(full_init)
+/* Memory state initialization */
+public_alias(memory_clean)
+public_alias(memory_init)
+/* Heap size */
+public_alias(get_heap_size)
+public_alias(heap_size)
+#ifdef E_ACSL_DEBUG /* Debug */
+public_alias(bt_print_block)
+public_alias(bt_print_tree)
#endif
+/* }}} */
#endif
-
-
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h
index e1e18e6993a5e1fff033bd9decd6f00c848206c8..1640746c7642518bd18f214fe892bda589f0c501 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h
@@ -21,7 +21,7 @@
/**************************************************************************/
/*! ***********************************************************************
- * \file e_acsl_malloc.h
+ * \file e_acsl_malloc.h
*
* \brief E-ACSL memory allocation bindings.
***************************************************************************/
@@ -34,12 +34,12 @@
#ifndef E_ACSL_MALLOC
#define E_ACSL_MALLOC
-/* Define ALIASNAME as a strong alias for NAME. */
+/** Define `aliasname` as a strong alias for `name`. */
# define strong_alias(name, aliasname) _strong_alias(name, aliasname)
# define _strong_alias(name, aliasname) \
extern __typeof (name) aliasname __attribute__ ((alias (#name)));
-/* Define ALIASNAME as a weak alias for NAME. */
+/** Define `aliasname` as a weak alias for `name`. */
# define weak_alias(name, aliasname) _weak_alias (name, aliasname)
# define _weak_alias(name, aliasname) \
extern __typeof (name) aliasname __attribute__ ((weak, alias (#name)));
@@ -47,25 +47,45 @@
# define preconcat(x,y) x ## y
# define concat(x,y) preconcat(x,y)
-/* Prefix added to all jemalloc functions, e.g., an actual jemalloc `malloc`
+/** Prefix added to all jemalloc functions, e.g., an actual jemalloc `malloc`
* is renamed to `__e_acsl_native_malloc` */
-# define native_prefix __e_acsl_native_
+# define native_prefix __e_acsl_native_
# define alloc_func_def(f,...) concat(native_prefix,f)(__VA_ARGS__)
-# define alloc_func_macro(f) concat(native_prefix,f)
+# define alloc_func_macro(f) concat(native_prefix,f)
+/** Prefix added to public functions of E-ACSL public API */
+# define public_prefix __e_acsl_
+/** Make a strong alias from some function named `f` to __e_acsl_f */
+# define public_alias(f) strong_alias(f, concat(public_prefix,f))
+/** Make a strong alias from some function named `f1` to __e_acsl_f2 */
+# define public_alias2(f1,f2) strong_alias(f1, concat(public_prefix,f2))
+
+/* The following declares jemalloc allocation functions.
+ * For instance:
+ * extern void *alloc_func_def(malloc, size_t);
+ * becomes:
+ * extern void *__e_acsl_native_malloc(size_t); */
extern void *alloc_func_def(malloc, size_t);
extern void *alloc_func_def(calloc, size_t, size_t);
extern void *alloc_func_def(realloc, void*, size_t);
-extern void alloc_func_def(free,void*);
+extern void *alloc_func_def(aligned_alloc, size_t, size_t);
extern int alloc_func_def(posix_memalign, void **, size_t, size_t);
+extern void alloc_func_def(free,void*);
-# define native_malloc alloc_func_macro(malloc)
-# define native_realloc alloc_func_macro(realloc)
-# define native_calloc alloc_func_macro(calloc)
-# define native_memalign alloc_func_macro(posix_memalign)
-# define native_free alloc_func_macro(free)
+/* Shortcuts for allocation functions used within this RTL (so they are not
+ * tracked). For example:
+ * native_malloc => __e_acsl_native_malloc */
+# define native_malloc alloc_func_macro(malloc)
+# define native_realloc alloc_func_macro(realloc)
+# define native_calloc alloc_func_macro(calloc)
+# define native_posix_memalign alloc_func_macro(posix_memalign)
+# define native_aligned_alloc alloc_func_macro(aligned_alloc)
+# define native_free alloc_func_macro(free)
+/* \return a true value if x is a power of 2 and false otherwise */
+static int powof2(size_t x) {
+ while (((x & 1) == 0) && x > 1) /* while x is even and > 1 */
+ x >>= 1;
+ return (x == 1);
+}
#endif
-
-
-
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
index 021af64d8d1e38f6c930031f0ac39cad2bd88dda..66b47387ada98ef2b3bfffc58c10198061a2bb3c 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
@@ -36,7 +36,7 @@
*
* For further information, see \p malloc(3). */
void * malloc(size_t size)
- __attribute__((FC_BUILTIN)) ;
+ __attribute__((FC_BUILTIN));
/*! \brief Drop-in replacement for \p calloc with memory tracking enabled.
*
@@ -56,6 +56,23 @@ void * realloc(void * ptr, size_t size)
void free(void * ptr)
__attribute__((FC_BUILTIN));
+/*! \brief Allocate `size` bytes of memory such that the allocation's base
+ * address is an even multiple of alignment.
+ *
+ * \param alignment - should be the power of two
+ * \param size - should be the multiple of alignment
+ * \return - pointer to the allocated memory if the restrictions placed on size
+ * and alignment parameters hold. NULL is returned otherwise. */
+void *aligned_alloc(size_t alignment, size_t size)
+ __attribute__((FC_BUILTIN));
+
+/*! \brief Allocate size bytes and place the address of the allocated memory in
+ * `*memptr`. The address of the allocated memory will be a multiple of
+ * `alignment`, which must be a power of two and a multiple of `sizeof(void*)`.
+ * If size is 0, then the value placed in *memptr is NULL. */
+int posix_memalign(void **memptr, size_t alignment, size_t size)
+ __attribute__((FC_BUILTIN));
+
/*! \brief Store stack or globally-allocated memory block
* starting at an address given by \p ptr.
*
@@ -102,8 +119,8 @@ int __e_acsl_freeable(void * ptr)
/*! \brief Implementation of the \b \\valid predicate of E-ACSL.
*
- * Return a non-zero value if the first \p size bytes starting at an address given
- * by \p ptr are readable and writable and 0 otherwise. */
+ * Return a non-zero value if the first \p size bytes starting at an address
+ * given by \p ptr are readable and writable and 0 otherwise. */
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \valid(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/memalign.c b/src/plugins/e-acsl/tests/e-acsl-runtime/memalign.c
new file mode 100644
index 0000000000000000000000000000000000000000..f88e16873420998d41e04aa21655e3ae9524e8c3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/memalign.c
@@ -0,0 +1,41 @@
+/* run.config
+ COMMENT: Check aligned heap memory allocation
+*/
+
+#include <stdlib.h>
+
+int posix_memalign(void **memptr, size_t alignment, size_t size);
+void *aligned_alloc(size_t alignment, size_t size);
+
+int main(int argc, const char **argv) {
+ char **memptr = malloc(sizeof(void*));
+ int res2 = posix_memalign((void**)memptr, 256, 15);
+
+ char *p = *memptr;
+ /*@assert \valid(p); */
+ /*@assert \block_length(p) == 15; */
+ /*@assert \freeable(p); */
+ free(p);
+ /*@assert ! \valid(p); */
+
+ char *a;
+ a = aligned_alloc(256, 12);
+ /*@assert a == \null; */
+
+ a = aligned_alloc(255, 512);
+ /*@assert a == \null; */
+
+ a = aligned_alloc(0, 512);
+ /*@assert a == \null; */
+
+ a = aligned_alloc(256, 512);
+ /*@assert a != \null; */
+ /*@assert \valid(a); */
+ /*@assert \block_length(a) == 512; */
+ /*@assert \freeable(a); */
+
+ free(a);
+ /*@assert ! \valid(a); */
+
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memalign.c
new file mode 100644
index 0000000000000000000000000000000000000000..12ea80643550b1c7d858a4de045856f0a9f9db4f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memalign.c
@@ -0,0 +1,137 @@
+/* Generated by Frama-C */
+int main(int argc, char const **argv)
+{
+ int __retres;
+ char **memptr;
+ int res2;
+ char *p;
+ char *a;
+ __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
+ __e_acsl_store_block((void *)(& a),8UL);
+ __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& memptr),8UL);
+ __e_acsl_full_init((void *)(& memptr));
+ memptr = (char **)malloc(sizeof(void *));
+ res2 = posix_memalign((void **)memptr,(unsigned long)256,(unsigned long)15);
+ __e_acsl_full_init((void *)(& p));
+ /*@ assert Value: mem_access: \valid_read(memptr); */
+ p = *memptr;
+ /*@ assert \valid(p); */
+ {
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+ sizeof(char *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(char));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(p)",15);
+ }
+ /*@ assert \block_length(p) ≡ 15; */
+ {
+ unsigned long __gen_e_acsl_block_length;
+ __gen_e_acsl_block_length = __e_acsl_block_length((void *)p);
+ __e_acsl_assert(__gen_e_acsl_block_length == 15UL,(char *)"Assertion",
+ (char *)"main",(char *)"\\block_length(p) == 15",16);
+ }
+ /*@ assert \freeable(p); */
+ {
+ int __gen_e_acsl_freeable;
+ __gen_e_acsl_freeable = __e_acsl_freeable((void *)p);
+ __e_acsl_assert(__gen_e_acsl_freeable,(char *)"Assertion",(char *)"main",
+ (char *)"\\freeable(p)",17);
+ }
+ free((void *)p);
+ /*@ assert ¬\valid(p); */
+ {
+ int __gen_e_acsl_initialized_2;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& p),
+ sizeof(char *));
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(char));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
+ }
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",(char *)"main",
+ (char *)"!\\valid(p)",19);
+ }
+ __e_acsl_full_init((void *)(& a));
+ a = (char *)aligned_alloc((unsigned long)256,(unsigned long)12);
+ /*@ assert a ≡ \null; */
+ __e_acsl_assert(a == (void *)0,(char *)"Assertion",(char *)"main",
+ (char *)"a == \\null",23);
+ __e_acsl_full_init((void *)(& a));
+ a = (char *)aligned_alloc((unsigned long)255,(unsigned long)512);
+ /*@ assert a ≡ \null; */
+ __e_acsl_assert(a == (void *)0,(char *)"Assertion",(char *)"main",
+ (char *)"a == \\null",26);
+ __e_acsl_full_init((void *)(& a));
+ a = (char *)aligned_alloc((unsigned long)0,(unsigned long)512);
+ /*@ assert a ≡ \null; */
+ __e_acsl_assert(a == (void *)0,(char *)"Assertion",(char *)"main",
+ (char *)"a == \\null",29);
+ __e_acsl_full_init((void *)(& a));
+ a = (char *)aligned_alloc((unsigned long)256,(unsigned long)512);
+ /*@ assert a ≢ \null; */
+ __e_acsl_assert(a != (void *)0,(char *)"Assertion",(char *)"main",
+ (char *)"a != \\null",32);
+ /*@ assert \valid(a); */
+ {
+ int __gen_e_acsl_initialized_3;
+ int __gen_e_acsl_and_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& a),
+ sizeof(char *));
+ if (__gen_e_acsl_initialized_3) {
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)a,sizeof(char));
+ __gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
+ }
+ else __gen_e_acsl_and_3 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_3,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(a)",33);
+ }
+ /*@ assert \block_length(a) ≡ 512; */
+ {
+ unsigned long __gen_e_acsl_block_length_2;
+ __gen_e_acsl_block_length_2 = __e_acsl_block_length((void *)a);
+ __e_acsl_assert(__gen_e_acsl_block_length_2 == 512UL,(char *)"Assertion",
+ (char *)"main",(char *)"\\block_length(a) == 512",34);
+ }
+ /*@ assert \freeable(a); */
+ {
+ int __gen_e_acsl_freeable_2;
+ __gen_e_acsl_freeable_2 = __e_acsl_freeable((void *)a);
+ __e_acsl_assert(__gen_e_acsl_freeable_2,(char *)"Assertion",
+ (char *)"main",(char *)"\\freeable(a)",35);
+ }
+ free((void *)a);
+ /*@ assert ¬\valid(a); */
+ {
+ int __gen_e_acsl_initialized_4;
+ int __gen_e_acsl_and_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& a),
+ sizeof(char *));
+ if (__gen_e_acsl_initialized_4) {
+ int __gen_e_acsl_valid_4;
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)a,sizeof(char));
+ __gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
+ }
+ else __gen_e_acsl_and_4 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_4,(char *)"Assertion",(char *)"main",
+ (char *)"!\\valid(a)",38);
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& a));
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_delete_block((void *)(& memptr));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memalign.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memalign.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memalign.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..48ed44b405da8727e629464d8dc8762c5640be83
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memalign.res.oracle
@@ -0,0 +1,18 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+tests/e-acsl-runtime/memalign.c:12:[kernel] warning: Neither code nor specification for function posix_memalign, generating default assigns from the prototype
+tests/e-acsl-runtime/memalign.c:14:[value] warning: out of bounds read. assert \valid_read(memptr);
+tests/e-acsl-runtime/memalign.c:15:[value] warning: assertion got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/memalign.c:16:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:17:[value] warning: assertion got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
+tests/e-acsl-runtime/memalign.c:19:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:22:[kernel] warning: Neither code nor specification for function aligned_alloc, generating default assigns from the prototype
+tests/e-acsl-runtime/memalign.c:23:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:26:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:29:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:32:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:33:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:34:[value] warning: assertion got status invalid (stopping propagation).