allocated and writeable in RTL as functions instead of macros

src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c

@@ -29,6 +29,9 @@
 # include "e_acsl_bittree_api.h"
 # include "e_acsl_bittree.h"
 
+static inline int allocated(uintptr_t addr, long size, uintptr_t base_ptr);
+static inline int writeable(uintptr_t addr, long size, uintptr_t base_ptr);
+
 /* Public API {{{ */
 /* Debug */
 #ifdef E_ACSL_DEBUG
@@ -43,18 +46,19 @@
 #define E_ACSL_MMODEL_DESC "patricia trie"
 
 /* Assertions in debug mode */
-#define ALLOCATED(_ptr,_size, _base) \
-  ((allocated(_ptr, _size, _base) == NULL) ? 0 : 1)
-
 #ifdef E_ACSL_DEBUG
-#define DVALIDATE_ALLOCATED(_ptr, _size, _base) \
-  vassert(ALLOCATED(_ptr, _size, _base), \
-  "Not allocated [%a, %a + %lu]", (uintptr_t)_ptr, _size)
-
-#define DVALIDATE_WRITEABLE(_ptr, _size, _base) { \
-  DVALIDATE_ALLOCATED(_ptr, _size, _base); \
-  vassert(!readonly(_ptr), "Location %a is read-only", (uintptr_t)_ptr); \
-}
+/* Assert that memory block [_addr, _addr + _size] is allocated */
+# define DVALIDATE_ALLOCATED(_addr, _size, _base) \
+  vassert(allocated((uintptr_t)_addr, _size, (uintptr_t)_base), \
+    "Operation on unallocated block [%a + %lu] with base %a\n", \
+    _addr, _size, _base);
+
+/* Assert that memory block [_addr, _addr + _size] is allocated
+ * and can be written to */
+# define DVALIDATE_WRITEABLE(_addr, _size, _base) \
+  vassert(writeable((uintptr_t)_addr, _size, (uintptr_t)_base), \
+    "Operation on unallocated block [%a + %lu] with base %a\n", \
+    _addr, _size, _base);
 #else
 #define DVALIDATE_ALLOCATED(_ptr, _size, _base)
 #define DVALIDATE_WRITEABLE(_ptr, _size, _base)
@@ -80,7 +84,7 @@ static const int nbr_bits_to_1[256] = {
 /* }}} */
 
 /**************************/
-/* DEBUG              {{{ */
+/* LOCATION (DEBUG MODE) {{{ */
 /**************************/
 #ifdef E_ACSL_DEBUG
 /* Notion of current location for debugging purposes  */
@@ -215,7 +219,7 @@ int initialized(void * ptr, size_t size) {
   return 1;
 }
 
-/* return the length (in bytes) of the block containing ptr */
+/** \brief \return the length (in bytes) of the block containing ptr */
 size_t block_length(void* ptr) {
   bt_block * blk = bt_find(ptr);
   /* Hard failure when un-allocated memory is used */
@@ -223,7 +227,11 @@ size_t block_length(void* ptr) {
   return blk->size;
 }
 
-static bt_block* allocated(void* ptr, size_t size, void *ptr_base) {
+/** \brief check whether a memory block containing address given via `ptr`
+    of length `size` and with base address `ptr_base` belongs to tracked
+    allocation and return corresponding `bt_block` if so. Return NULL
+    otherwise. */
+static bt_block* lookup_allocated(void* ptr, size_t size, void *ptr_base) {
   bt_block * blk = bt_find(ptr);
   if (blk == NULL)
     return NULL;
@@ -235,6 +243,14 @@ static bt_block* allocated(void* ptr, size_t size, void *ptr_base) {
   return (blk->size - ((size_t)ptr - blk->ptr) >= size) ? blk : NULL;
 }
 
+/** \brief same as ::lookup_allocated but return either `1` or `0` depending
+    on whether the memory block described by this function's arguments is
+    allocated or not.
+    NOTE: Should have same signature in all models. */
+static inline int allocated(uintptr_t addr, long size, uintptr_t base) {
+  return lookup_allocated((void*)addr, size, (void*)base) == NULL ? 0 : 1;
+}
+
 /** \brief Return 1 if a given memory location is read-only and 0 otherwise */
 static int readonly (void *ptr) {
   bt_block * blk = bt_find(ptr);
@@ -242,9 +258,15 @@ static int readonly (void *ptr) {
   return blk->is_readonly;
 }
 
+/** \brief same as ::allocated but returns `0` if the memory block described
+     by the arguments cannot be written to */
+static inline int writeable(uintptr_t addr, long size, uintptr_t base_ptr) {
+  return allocated(addr, size, base_ptr) && !readonly((void*)addr);
+}
+
 /* return whether the size bytes of ptr are readable/writable */
 int valid(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
-  bt_block * blk = allocated(ptr, size, ptr_base);
+  bt_block * blk = lookup_allocated(ptr, size, ptr_base);
   return blk != NULL && !blk->is_readonly
 #ifdef E_ACSL_TEMPORAL
     && temporal_valid(ptr_base, addrof_base)
@@ -254,7 +276,7 @@ int valid(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
 
 /* return whether the size bytes of ptr are readable */
 int valid_read(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
-  bt_block * blk = allocated(ptr, size, ptr_base);
+  bt_block * blk = lookup_allocated(ptr, size, ptr_base);
   return blk != NULL
 #ifdef E_ACSL_TEMPORAL
     && temporal_valid(ptr_base, addrof_base)
@@ -284,13 +306,13 @@ size_t offset(void* ptr) {
 /* STACK ALLOCATION {{{ */
 /* store the block of size bytes starting at ptr, the new block is returned.
  * Warning: the return type is implicitly (bt_block*). */
-void* store_block(void* ptr, size_t size) {
+void* store_block(void *ptr, size_t size) {
 #ifdef E_ACSL_DEBUG
   if (ptr == NULL)
     vabort("Attempt to record NULL block");
   else {
     char *check = (char*)ptr;
-    bt_block * exitsing_block = bt_find(ptr);
+    bt_block *exitsing_block = bt_find(ptr);
     if (exitsing_block) {
       vabort("\nRecording %a [%lu] at %s:%d failed."
         " Overlapping block %a [%lu] found at %s:%d\n",
@@ -307,7 +329,7 @@ void* store_block(void* ptr, size_t size) {
     }
   }
 #endif
-  bt_block * tmp = NULL;
+  bt_block *tmp = NULL;
   if (ptr) {
     tmp = private_malloc(sizeof(bt_block));
     tmp->ptr = (uintptr_t)ptr;
@@ -333,7 +355,7 @@ void* store_block(void* ptr, size_t size) {
 /* Track a heap block. This is a wrapper for all memory allocation functions
   that create new bittree nodes. It applies to all memory allocating functions
   but realloc that modifies nodes rather than create them */
-static void* store_freeable_block(void* ptr, size_t size, int init_bytes) {
+static void *store_freeable_block(void *ptr, size_t size, int init_bytes) {
   bt_block *blk = NULL;
   if (ptr) {
     blk = store_block(ptr, size);
@@ -346,14 +368,14 @@ static void* store_freeable_block(void* ptr, size_t size, int init_bytes) {
 }
 
 /* remove the block starting at ptr */
-void delete_block(void* ptr) {
+void delete_block(void *ptr) {
 #ifdef E_ACSL_DEBUG
   /* Make sure the recorded block is not NULL */
   if (!ptr)
     vabort("Attempt to delete NULL block");
 #endif
   if (ptr != NULL) {
-    bt_block * tmp = bt_lookup(ptr);
+    bt_block *tmp = bt_lookup(ptr);
 #ifdef E_ACSL_DEBUG
     /* Make sure the removed block exists in the tracked allocation */
     if (!tmp)
@@ -415,9 +437,9 @@ void* calloc(size_t nbr_block, size_t size_block) {
 /*! \brief Replacement for `aligned_alloc` with memory tracking */
 void *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 */
+     - 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;
 
@@ -435,7 +457,7 @@ int posix_memalign(void **memptr, size_t alignment, size_t size) {
     return -1;
 
   /* Make sure that the first argument to posix memalign is indeed allocated */
-  DVALIDATE_WRITEABLE((void*)memptr, sizeof(void*), (void*)memptr);
+  DVALIDATE_WRITEABLE(memptr, sizeof(void*), memptr);
 
   int res = public_posix_memalign(memptr, alignment, size);
   if (!res)
@@ -444,7 +466,7 @@ int posix_memalign(void **memptr, size_t alignment, size_t size) {
 }
 
 /*! \brief Replacement for `realloc` with memory tracking */
-void* realloc(void* ptr, size_t size) {
+void* realloc(void *ptr, size_t size) {
   bt_block * tmp;
   void * new_ptr;
   /* ptr is NULL - malloc */
@@ -512,7 +534,7 @@ void* realloc(void* ptr, size_t size) {
 }
 
 /*! \brief Replacement for `free` with memory tracking */
-void free(void* ptr) {
+void free(void *ptr) {
   if (ptr == NULL) {
 /* Fail if instructed to treat NULL input to free as invalid. */
 #ifdef E_ACSL_FREE_VALID_ADDRESS
@@ -520,7 +542,7 @@ void free(void* ptr) {
 #endif
     return;
   }
-  bt_block * res = bt_lookup(ptr);
+  bt_block *res = bt_lookup(ptr);
   if (!res) {
     vabort("Not a start of block (%a) in free\n", ptr);
   } else {
@@ -606,8 +628,11 @@ void memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
 }
 /* }}} */
 
-#ifdef E_ACSL_DEBUG
+/******************************/
+/* DEBUG PRINT {{{ */
+/******************************/
 
+#ifdef E_ACSL_DEBUG
 /* Debug version of store block with location tracking. This function is aimed
  * at manual debugging.  While there is no easy way of traking file/line numbers
  * recorded memory blocks with the use of the following macros placed after the
@@ -650,6 +675,7 @@ void block_info(char *p) {
   }
 }
 #endif
+/* }}} */
 
 /* Local operations on temporal timestamps {{{ */
 /* Remaining functionality (shared between all models) is located in e_acsl_temporal.h */
@@ -660,7 +686,7 @@ static uint32_t origin_timestamp(void *ptr) {
 }
 
 static uintptr_t temporal_referent_shadow(void *ptr) {
-  bt_block * blk = bt_find(ptr);
+  bt_block *blk = bt_find(ptr);
   vassert(blk != NULL,
     "referent timestamp on unallocated memory address %a", (uintptr_t)ptr);
   vassert(blk->temporal_shadow != NULL,

src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c

@@ -33,23 +33,21 @@
 
 #define E_ACSL_MMODEL_DESC "shadow memory"
 
-#define ALLOCATED(_ptr,_size) allocated((uintptr_t)_ptr, _size, (uintptr_t)_ptr)
-
-void * store_block(void * ptr, size_t size) {
+void * store_block(void *ptr, size_t size) {
   /* 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. */
+     Heap blocks should be tracked internally using memory allocation functions
+     such as malloc or calloc. */
   shadow_alloca(ptr, size);
   return ptr;
 }
 
-void delete_block(void * ptr) {
+void delete_block(void *ptr) {
   /* Block deletion should be performed on stack/global addresses only,
    * heap blocks should be deallocated manually via free/cfree/realloc. */
   shadow_freea(ptr);
 }
 
-void * store_block_duplicate(void * ptr, size_t size) {
+void * store_block_duplicate(void *ptr, size_t size) {
   if (allocated((uintptr_t)ptr, size, (uintptr_t)ptr))
     delete_block(ptr);
   shadow_alloca(ptr, size);
@@ -66,11 +64,11 @@ void initialize(void *ptr, size_t n) {
   )
 }
 
-void full_init(void * ptr) {
+void full_init(void *ptr) {
   initialize(ptr, _block_length(ptr));
 }
 
-void mark_readonly(void * ptr) {
+void mark_readonly(void *ptr) {
   mark_readonly_region((uintptr_t)ptr, _block_length(ptr));
 }
 
@@ -78,13 +76,7 @@ void mark_readonly(void * ptr) {
 /* E-ACSL annotations {{{ */
 /* ********************** */
 
-/** \brief Return 1 if a given memory location is read-only and 0 otherwise */
-static int readonly (void *ptr) {
-  uintptr_t addr = (uintptr_t)ptr;
-  return IS_ON_GLOBAL(addr) && global_readonly(addr) ? 1 : 0;
-}
-
-int valid(void * ptr, size_t size, void *ptr_base, void *addrof_base) {
+int valid(void *ptr, size_t size, void *ptr_base, void *addrof_base) {
   return
     allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base)
     && !readonly(ptr)
@@ -94,19 +86,18 @@ int valid(void * ptr, size_t size, void *ptr_base, void *addrof_base) {
   ;
 }
 
-int valid_read(void * ptr, size_t size, void *ptr_base, void *addrof_base) {
+int valid_read(void *ptr, size_t size, void *ptr_base, void *addrof_base) {
   return allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base)
 #ifdef E_ACSL_TEMPORAL
     && temporal_valid(ptr_base, addrof_base)
 #endif
   ;
-
 }
 
 /*! 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 * base_addr(void * ptr) {
+   \p _base_addr macro that will eventually call ::TRY_SEGMENT. The following
+   implementation is preferred for performance reasons. */
+void * base_addr(void *ptr) {
   TRY_SEGMENT(ptr,
     return (void*)heap_info((uintptr_t)ptr, 'B'),
     return (void*)static_info((uintptr_t)ptr, 'B'));
@@ -114,9 +105,9 @@ void * base_addr(void * ptr) {
 }
 
 /*! 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 block_length(void * ptr) {
+   via \p _block_length macro. A more direct approach via ::TRY_SEGMENT
+   is preferred for performance reasons. */
+size_t block_length(void *ptr) {
   TRY_SEGMENT(ptr,
     return heap_info((uintptr_t)ptr, 'L'),
     return static_info((uintptr_t)ptr, 'L'))
@@ -130,7 +121,7 @@ size_t offset(void *ptr) {
   return 0;
 }
 
-int initialized(void * ptr, size_t size) {
+int initialized(void *ptr, size_t size) {
   uintptr_t addr = (uintptr_t)ptr;
   TRY_SEGMENT_WEAK(addr,
     return heap_initialized(addr, size),
@@ -168,9 +159,9 @@ static void argv_alloca(int *argc_ref,  char *** argv_ref) {
        therefore more than welcome. */
     *argv = shadow_copy(*argv, arglen, 1);
     /* TODO: These heap allocations are never freed in fact. Not super
-     * important, but for completeness purposes it may be feasible to define
-     * a buffer of implicitly allocated memory locations which need to be
-     * freed before a program exists. */
+       important, but for completeness purposes it may be feasible to define
+       a buffer of implicitly allocated memory locations which need to be
+       freed before a program exists. */
 #else
     shadow_alloca(*argv, arglen);
     initialize_static_region((uintptr_t)*argv, arglen);

src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h

@@ -383,18 +383,16 @@ static void validate_shadow_layout() {
 
 /* Assert that memory block [_addr, _addr + _size] is allocated */
 # define DVALIDATE_ALLOCATED(_addr, _size, _base) \
-  DVASSERT(allocated((uintptr_t)_addr, _size, (uintptr_t)_base), \
+  vassert(allocated((uintptr_t)_addr, _size, (uintptr_t)_base), \
     "Operation on unallocated block [%a + %lu] with base %a\n", \
-    _addr, _size, _base)
+    _addr, _size, _base);
 
 /* Assert that memory block [_addr, _addr + _size] is allocated
  * and can be written to */
-# define DVALIDATE_WRITEABLE(_addr, _size, _base) { \
-  DVALIDATE_ALLOCATED((uintptr_t)_addr, _size, (uintptr_t)_base); \
-  DVASSERT(!readonly((void*)_addr), \
-    "Unexpected readonly address: %lu\n", _addr); \
-}
-
+# define DVALIDATE_WRITEABLE(_addr, _size, _base) \
+  vassert(writeable((uintptr_t)_addr, _size, (uintptr_t)_base), \
+    "Operation on unallocated block [%a + %lu] with base %a\n", \
+    _addr, _size, _base);
 #else
 /*! \cond exclude from doxygen */
 #  define DVALIDATE_MEMORY_INIT
@@ -428,6 +426,8 @@ static uintptr_t static_info(uintptr_t addr, char type);
 static int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr);
 static int static_allocated(uintptr_t addr, long size, uintptr_t base_ptr);
 static int allocated(uintptr_t addr, long size, uintptr_t base_ptr);
+static int writeable(uintptr_t addr, long size, uintptr_t base_ptr);
+static int readonly (void *ptr);
 
 /*! \brief Quick test to check if a static location belongs to allocation.
  * This macro really belongs where static_allocated is defined, but
@@ -1303,6 +1303,16 @@ static int allocated(uintptr_t addr, long size, uintptr_t base) {
     return 0;
   return 0;
 }
+
+/** \brief Return 1 if a given memory location is read-only and 0 otherwise */
+static inline int readonly (void *ptr) {
+  uintptr_t addr = (uintptr_t)ptr;
+  return IS_ON_GLOBAL(addr) && global_readonly(addr) ? 1 : 0;
+}
+
+static inline int writeable(uintptr_t addr, long size, uintptr_t base_ptr) {
+  return allocated(addr, size, base_ptr) && !readonly((void*)addr);
+}
 /* }}} */
 
 /* Internal state print (debug mode) {{{ */