From a0f8d8c2ae6921807ff9247b2d3e853b71c16148 Mon Sep 17 00:00:00 2001
From: Guillaume Petiot <guillaume.petiot@cea.fr>
Date: Mon, 26 Nov 2012 08:52:54 +0000
Subject: [PATCH] + fix _valid_read
---
.../e-acsl/memory_model/e_acsl_bittree.c | 281 +++++------
.../share/e-acsl/memory_model/e_acsl_mmodel.c | 439 ++++++++----------
.../share/e-acsl/memory_model/e_acsl_mmodel.h | 30 ++
.../e-acsl/memory_model/e_acsl_mmodel_api.h | 34 +-
4 files changed, 386 insertions(+), 398 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
index 6a29dea436a..098964e17b2 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
@@ -93,18 +93,20 @@ int Teq[] = {0,-1,3,-3,6,-5,7,-7,12,-9,11,-11,14,-13,15,-15,24,-17,19,-19,22,-21
int Tneq[] = {0,0,1,-2,2,-4,5,-6,4,-8,9,-10,10,-12,13,-14,8,-16,17,-18,18,-20,21,-22,20,-24,25,-26,26,-28,29,-30,16,-32,33,-34,34,-36,37,-38,36,-40,41,-42,42,-44,45,-46,40,-48,49,-50,50,-52,53,-54,52,-56,57,-58,58,-60,61,-62,-63};
/* common bits of two addresses */
-
unsigned long mask(void * a, void * b) {
unsigned long nxor = ~((unsigned long)a ^ (unsigned long)b);
- int i = WORDBITS/2;
- __cpt_mask++;
+ int i = WORDBITS/2; /* dichotomic search, starting in the middle */
+
+ /* if the current mask matches we use transition from Teq, else from Tneq
+ we stop as soon as i is negative, meaning that we found the mask */
+ while(i > 0) i = (nxor >= Tmasks[i]) ? Teq[i] : Tneq[i];
- while(i > 0)
- i = (nxor >= Tmasks[i]) ? Teq[i] : Tneq[i];
+ /* a negative element i from Teq or Tneq means stop and return Tmasks[-i] */
return Tmasks[-i];
}
-/* binary conjuction of a bittree and a new node */
+
+/* logical AND of a bittree and a new node */
void* and(struct bittree * a, struct _block * b) {
return (void*) ((unsigned long)a->addr & (unsigned long)b->ptr);
}
@@ -114,106 +116,99 @@ int matches_mask(struct bittree * a, void * b) {
return ((unsigned long)a->addr & a->mask) == ((unsigned long)b & a->mask);
}
-/********************/
+/* remove the block from the structure */
void _remove_element (struct _block * ptr) {
struct bittree * curr = __root;
- if(__root == NULL || ptr == NULL)
- return;
+ assert(__root != NULL);
+ assert(ptr != NULL);
- if(__root->is_leaf) {
- if(__root->addr == ptr->ptr) {
- free(__root);
- __root = NULL;
- }
+ if(__root->is_leaf) {
+ assert(__root->addr == ptr->ptr);
+ free(__root);
+ __root = NULL;
return;
}
-
+
while(1) {
/* does not match the mask */
- if(!matches_mask(curr, ptr->ptr))
- break;
-
+ assert(matches_mask(curr, ptr->ptr));
+
/* element to delete */
if(curr->is_leaf) {
- struct bittree * to_up, * cf;
- assert(curr->father != NULL);
-
- to_up = (curr == curr->father->left)?
- curr->father->right : curr->father->left;
+ struct bittree * brother, * cf;
cf = curr->father;
- assert(to_up != NULL);
-
- cf->is_leaf = to_up->is_leaf;
- cf->addr = to_up->addr;
- cf->mask = to_up->mask;
- cf->left = to_up->left;
- cf->right = to_up->right;
- cf->leaf = to_up->leaf;
-
- if(!to_up->is_leaf) {
- to_up->left->father = cf;
- to_up->right->father = cf;
+ assert(cf != NULL);
+ brother = (curr == cf->left) ? cf->right : cf->left;
+ assert(brother != NULL);
+
+ cf->is_leaf = brother->is_leaf;
+ cf->addr = brother->addr;
+ cf->mask = brother->mask;
+ cf->left = brother->left;
+ cf->right = brother->right;
+ cf->leaf = brother->leaf;
+
+ if(!brother->is_leaf) {
+ brother->left->father = cf;
+ brother->right->father = cf;
}
- free(to_up);
+ free(brother);
free(curr);
-
break;
}
-
- /* visit child with most bits in common */
+
assert(curr->left != NULL && curr->right != NULL);
- curr = (mask(curr->left->addr, ptr->ptr)
- > mask(curr->right->addr, ptr->ptr))?
- curr->left : curr->right;
+
+ /* visit child with greatest common prefix,
+ if the bit next to the mask is set to 1, go to right child,
+ because its address is higher than the other */
+ curr = ((curr->mask >> 1) & ( ~ curr->mask ) & (unsigned long)ptr->ptr) ?
+ curr->right : curr->left;
}
}
-/************************/
+/* add a block in the structure */
void _add_element (struct _block * ptr) {
struct bittree * new_leaf;
- if(ptr == NULL)
- return;
-
+ assert(ptr != NULL);
+
new_leaf = malloc(sizeof(struct bittree));
+ assert(new_leaf != NULL);
new_leaf->is_leaf = 1;
new_leaf->addr = ptr->ptr;
- new_leaf->mask = ~0;
- new_leaf->left = NULL;
- new_leaf->right = NULL;
- new_leaf->father = NULL;
+ new_leaf->mask = ~0ul;
+ new_leaf->left = new_leaf->right = new_leaf->father = NULL;
new_leaf->leaf = ptr;
-
- if(__root == NULL)
- __root = new_leaf;
-
+
+ if(__root == NULL) __root = new_leaf;
else {
- struct bittree * curr = __root; /* __root != NULL */
-
+ struct bittree * curr = __root;
+
while(1) {
/* matches the mask */
if(matches_mask(curr, ptr->ptr)) {
- /* already stored */
- if(curr->is_leaf) {
- free(new_leaf);
- assert(ptr->ptr == curr->addr);
- break;
- }
- assert(curr->left != NULL
- && curr->right != NULL);
- /* visit child with most bits in common */
- curr = mask(curr->left->addr, ptr->ptr)
- > mask(curr->right->addr, ptr->ptr)
- ? curr->left
- : curr->right;
- }
+ /* is a leaf => already stored */
+ if(curr->is_leaf)
+ return;
+
+ assert(!curr->is_leaf);
+ assert(curr->left != NULL && curr->right != NULL);
+ /* visit child with greatest common prefix */
+ curr =
+ ((curr->mask >> 1) & ( ~ curr->mask ) & (unsigned long)ptr->ptr) ?
+ curr->right : curr->left;
+ }
+
/* does not match the mask : creating a new node */
else {
struct bittree * new_node;
new_node = malloc(sizeof(struct bittree));
+ assert(new_node != NULL);
+
new_node->is_leaf = curr->is_leaf;
new_node->addr = curr->addr;
new_node->mask = curr->mask;
@@ -223,163 +218,135 @@ void _add_element (struct _block * ptr) {
new_leaf->father = curr;
new_node->leaf = curr->leaf;
- if(!new_node->is_leaf) {
- new_node->left->father = new_node;
- new_node->right->father = new_node;
- }
-
+ if(!new_node->is_leaf)
+ new_node->left->father = new_node->right->father = new_node;
+
curr->is_leaf = 0;
- curr->addr = and(new_node, ptr);
curr->mask = mask(new_node->addr, ptr->ptr);
+ curr->addr = (void*)((unsigned long)and(new_node, ptr) & curr->mask);
+
+ /* smaller at left, higher at right */
if(new_node->addr < ptr->ptr) {
curr->left = new_node;
curr->right = new_leaf;
- } else {
+ }
+ else {
curr->left = new_leaf;
curr->right = new_node;
}
curr->leaf = NULL;
-
break;
}
}
}
}
-/**********************/
+/* return the block B such as : begin addr of B == ptr
+ we suppose that such a block exists, but we could return NULL if not */
struct _block * _get_exact (void * ptr) {
struct bittree * tmp = __root;
- if(__root == NULL || ptr == NULL)
- return NULL;
+ if(__root == NULL || ptr == NULL) return NULL;
while(1) {
/* does not match the mask */
- if(!matches_mask(tmp, ptr))
- break;
- /* the leaf we are looking for */
- if(tmp->is_leaf)
- return tmp->leaf;
- /* visit child with most bits in common */
- assert(tmp->left != NULL && tmp->right != NULL);
+ if(!matches_mask(tmp, ptr)) return NULL;
- tmp = (mask(tmp->left->addr, ptr)
- > mask(tmp->right->addr, ptr)) ?
- tmp->left :
- tmp->right;
- }
-
- return NULL;
-}
-
-/************************/
-
-struct _block * _get_next (void * ptr) {
- struct bittree * tmp = __root;
- if(__root == NULL || ptr == NULL)
- return NULL;
- if(__root->is_leaf)
- return NULL;
+ /* the leaf we are looking for */
+ if(tmp->is_leaf) return tmp->leaf;
- while(1) {
- /* does not match the mask */
- if(!matches_mask(tmp, ptr))
- break;
- if(tmp->is_leaf)
- break;
- /* visit child with most bits in common */
assert(tmp->left != NULL && tmp->right != NULL);
-
- tmp = (mask(tmp->left->addr, ptr)
- > mask(tmp->right->addr, ptr)) ?
- tmp->left :
- tmp->right;
+
+ /* visit child with greatest common prefix */
+ tmp = ((tmp->mask >> 1) & ( ~ tmp->mask ) & (unsigned long)ptr) ?
+ tmp->right : tmp->left;
}
-
- if(ptr < (void*)tmp->addr)
- return NULL;
- /* we move up, as long as we are on right branches */
- while(tmp->father != NULL && tmp == tmp->father->right)
- tmp = tmp->father;
- /* tmp is at bottom right => no next leaf */
- if(tmp == __root)
- return NULL;
- /* tmp has a father and is a left child */
- tmp = tmp->father->right;
- /* we move down, following left branches */
- while(!tmp->is_leaf)
- tmp = tmp->left;
- assert(ptr < (void*)tmp->addr);
- return tmp->leaf;
}
-/**************************/
+/* return the block B containing ptr, such as :
+ begin addr of B <= ptr < (begin addr + size) of B
+ or NULL if such a block does not exist */
struct _block * _get_cont (void * ptr) {
struct bittree * tmp = __root;
- if(__root == NULL || ptr == NULL)
- return NULL;
-
+ if(__root == NULL || ptr == NULL) return NULL;
+
while(1) {
if(tmp->is_leaf) {
- if(ptr < (void*)tmp->addr)
- return NULL;
- else
- if(ptr < (void*)(tmp->addr + tmp->leaf->size))
- return tmp->leaf;
+ /* tmp cannot contain ptr because its begin addr is higher */
+ if(tmp->addr > (char*)ptr) return NULL;
+ /* tmp->addr <= ptr, tmp may contain ptr
+ ptr is contained if tmp is large enough (begin addr + size) */
+ else if((char*)ptr < tmp->leaf->size + tmp->addr) return tmp->leaf;
+ /* tmp->addr <= ptr, but tmp->addr is not large enough */
return NULL;
}
+
assert(tmp->left != NULL && tmp->right != NULL);
+
+ /* the right child has the highest address, so we test it first */
if(((unsigned long)tmp->right->addr & tmp->right->mask)
<= ((unsigned long)ptr & tmp->right->mask))
tmp = tmp->right;
else if(((unsigned long)tmp->left->addr & tmp->left->mask)
<= ((unsigned long)ptr & tmp->left->mask))
tmp = tmp->left;
- else
- return NULL;
+ else return NULL;
}
}
-/**************************/
+/*******************/
+/* CLEAN */
+/*******************/
+
+
+/* recursively erase the content of the structure,
+ do not call directly */
void __clean_rec (struct bittree * ptr) {
- if(ptr == NULL)
- return;
- if(ptr->is_leaf) {
+ if(ptr == NULL) return;
+ else if(ptr->is_leaf) {
_clean_block(ptr->leaf);
ptr->leaf = NULL;
- } else {
+ }
+ else {
__clean_rec(ptr->left);
- ptr->left = NULL;
__clean_rec(ptr->right);
- ptr->right = NULL;
+ ptr->left = ptr->right = NULL;
}
free(ptr);
- ptr = NULL;
}
+/* erase the content of the structure */
void __clean_struct () {
__clean_rec(__root);
- /* printf("cpt mask: %i\n", __cpt_mask);*/
+ __root = NULL;
}
+
/*********************/
+/* DEBUG */
+/*********************/
+
+/* recursively print the content of the structure
+ do not call directly */
void __debug_rec (struct bittree * ptr) {
- if(ptr == NULL)
- return;
- if(ptr->is_leaf) {
+ if(ptr == NULL) return;
+ else if(ptr->is_leaf) {
printf("\t\t\t");
_print_block(ptr->leaf);
- } else {
+ }
+ else {
__debug_rec(ptr->left);
__debug_rec(ptr->right);
}
}
+/* print the content of the structure */
void __debug_struct () {
printf("\t\t\t------------DEBUG\n");
__debug_rec(__root);
printf("\t\t\t-----------------\n");
}
+
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
index f73c75b385b..c1e242e49a2 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
@@ -2,185 +2,96 @@
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
+#include <stdbool.h>
+#include <assert.h>
#include "e_acsl_bittree.h"
#include "e_acsl_mmodel_api.h"
-/*#define KEEP_FREED_MEMORY*/
+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,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,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,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,3,4,4,5,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
+};
-int __cpt_store = 0, __cpt_malloc = 0;
-void _clean_init (struct _block * ptr) {
- if(ptr->init_ptr != NULL) {
- free(ptr->init_ptr);
- ptr->init_ptr = NULL;
- }
- ptr->init_cpt = 0;
-}
-
-void _clean_block (struct _block * ptr) {
- if(ptr == NULL)
- return;
- _clean_init(ptr);
- free(ptr);
- ptr = NULL;
+size_t needed_bytes (size_t size) {
+ return (size % 8) == 0 ? (size/8) : (size/8 + 1);
}
-void _print_block (struct _block * ptr) {
- if (ptr != NULL) {
- printf("%p %zu %s ; [init] : %li ",
- ptr->ptr,
- ptr->size,
- ptr->valid? "valid":"invalid",
- ptr->init_cpt);
- if(ptr->init_ptr != NULL) {
- unsigned i;
- for(i = 0; i < ptr->size; i++)
- printf("%i", ptr->init_ptr[i]);
- }
- printf("\n");
- }
-}
-
-void* _store_block(void* tmp, size_t size) {
-#ifdef KEEP_FREED_MEMORY
- struct _block *cont, *next, *ptr;
-#else
- struct _block *ptr;
-#endif
- __cpt_store++;
-#ifdef KEEP_FREED_MEMORY
- cont = _get_cont(tmp);
- if(cont != NULL) {
- /* si cont commence avant => chevauchement à gauche */
- if(cont->ptr < tmp) {
- /* cont se termine en plein milieu */
- if(tmp + size >= cont->ptr + cont->size)
- cont->size = tmp - cont->ptr;
- /* cont se termine après => chevauchement à droite */
- else {
- struct _block * after;
- after = malloc(sizeof(struct _block));
- if(after == NULL)
- return NULL;
- after->ptr = tmp + size;
- after->size = cont->ptr + cont->size
- - after->ptr;
- after->valid = 0; /* false */
- cont->size = tmp - cont->ptr;
- _add_element(after);
- }
- }
- }
-
- for(; (next = _get_next(tmp)) != NULL ;) {
- if(next->ptr >= tmp + size)
- break;
- /* next se termine en plein milieu => on supprime */
- if(tmp + size >= next->ptr + next->size) {
- _remove_element(next);
- free(next);
- next = NULL;
- }
- /* next se termine après => chevauchement à droite */
- else {
- struct _block * after;
- after = malloc(sizeof(struct _block));
- if(after == NULL)
- return NULL;
- after->ptr = tmp + size;
- after->size = next->ptr + next->size - after->ptr;
- after->valid = 0; /* false */
- _remove_element(next);
- free(next);
- next = NULL;
- _add_element(after);
- }
- }
-#endif
- ptr = malloc(sizeof(struct _block));
- if(ptr == NULL)
- return NULL;
- ptr->ptr = tmp;
- ptr->size = size;
- ptr->valid = 1; /* true */
- ptr->init_ptr = NULL;
- ptr->init_cpt = 0;
- _add_element(ptr);
- return ptr->ptr;
+/* store the block of size bytes starting at ptr */
+void* _store_block(void* ptr, size_t size) {
+ struct _block * tmp;
+ assert(ptr != NULL);
+ tmp = malloc(sizeof(struct _block));
+ assert(tmp != NULL);
+ tmp->ptr = ptr;
+ tmp->size = size;
+ tmp->init_ptr = NULL;
+ tmp->init_cpt = 0;
+ tmp->is_litteral_string = false;
+ _add_element(tmp);
+ return ptr;
}
+/* remove the block starting at ptr */
void _delete_block(void* ptr) {
struct _block * tmp;
- if(ptr == NULL)
- return;
+ assert(ptr != NULL);
tmp = _get_exact(ptr);
- if(tmp == NULL)
- return;
+ assert(tmp != NULL);
_clean_init(tmp);
_remove_element(tmp);
free(tmp);
- tmp = NULL;
}
+/* allocate size bytes and store the returned block
+ * for further information, see malloc */
void* _malloc(size_t size) {
- void * tmp;
- if(size <= 0)
- return NULL;
+ void * tmp, * tmp2;
+ if(size <= 0) return NULL;
tmp = malloc(size);
- if(tmp == NULL)
- return NULL;
- __cpt_malloc++;
- return _store_block(tmp, size);
+ if(tmp == NULL) return NULL;
+ tmp2 = _store_block(tmp, size);
+ assert(tmp2 != NULL);
+ return tmp2;
}
+/* free the block starting at ptr,
+ * for further information, see free */
void _free(void* ptr) {
struct _block * tmp;
- if(ptr == NULL)
- return;
+ if(ptr == NULL) return;
tmp = _get_exact(ptr);
- if(tmp == NULL)
- return;
- free(tmp->ptr);
+ assert(tmp != NULL);
+ free(ptr);
_clean_init(tmp);
-#ifdef KEEP_FREED_MEMORY
- tmp->valid = 0; /* false */
-#else
_remove_element(tmp);
free(tmp);
- tmp = NULL;
-#endif
}
+/* resize the block starting at ptr to fit its new size,
+ * for further information, see realloc */
void* _realloc(void* ptr, size_t size) {
-#ifdef KEEP_FREED_MEMORY
- struct _block *tmp, *next;
-#else
- struct _block *tmp;
-#endif
-
- if(ptr == NULL)
- return _malloc(size);
+ struct _block * tmp, * next;
+ void * new_ptr;
+ if(ptr == NULL) return _malloc(size);
if(size <= 0) {
_free(ptr);
- ptr = NULL;
return NULL;
}
tmp = _get_exact(ptr);
- if(tmp == NULL)
- return NULL;
- tmp->ptr = realloc(tmp->ptr, size);
- tmp->valid = 1; /* true */
-
+ assert(tmp != NULL);
+ new_ptr = realloc(tmp->ptr, size);
+ if(new_ptr == NULL) return NULL;
+ tmp->ptr = new_ptr;
/* uninitialized, do nothing */
if(tmp->init_cpt == 0) ;
- /* already initialized block */
+ /* already fully initialized block */
else if (tmp->init_cpt == tmp->size) {
/* realloc smaller block */
if(size <= tmp->size)
@@ -188,81 +99,75 @@ void* _realloc(void* ptr, size_t size) {
tmp->init_cpt = size;
/* realloc bigger larger block */
else {
- tmp->init_ptr = malloc(size*sizeof(char));
- memset(tmp->init_ptr, 1, tmp->size);
- memset(tmp->init_ptr + tmp->size, 0, size - tmp->size);
+ int i, nb = needed_bytes(size);
+ tmp->init_ptr = malloc(nb);
+ memset(tmp->init_ptr, 0xFF, nb);
+ if(size%8 != 0)
+ tmp->init_ptr[size/8] <<= (8 - size%8);
}
}
/* contains initialized and uninitialized parts */
- else
- tmp->init_ptr = realloc(tmp->init_ptr, size*sizeof(char));
-
- tmp->size = size;
-#ifdef KEEP_FREED_MEMORY
- for(; (next = _get_next(tmp->ptr)) != NULL ;) {
- if(next->ptr >= tmp->ptr + size)
- break;
- /* next se termine en plein milieu => on supprime */
- if(tmp->ptr + size >= next->ptr + next->size) {
- _remove_element(next);
- free(next);
- next = NULL;
- }
- /* next se termine après => chevauchement à droite */
- else {
- struct _block * after;
- after = malloc(sizeof(struct _block));
- if(after == NULL)
- return NULL;
- after->ptr = tmp->ptr + size;
- after->size = next->ptr + next->size - after->ptr;
- after->valid = 0; /* false */
- _remove_element(next);
- free(next);
- next = NULL;
- _add_element(after);
+ else {
+ int nb = needed_bytes(size);
+ int nb_old = needed_bytes(tmp->size);
+ int i;
+ tmp->init_ptr = realloc(tmp->init_ptr, nb);
+ for(i = nb_old; i < nb; i++)
+ tmp->init_ptr[i] = 0;
+ tmp->init_cpt = 0;
+ for(i = 0; i < nb; i++)
+ tmp->init_cpt += nbr_bits_to_1[tmp->init_ptr[i]];
+ if(tmp->init_cpt == size || tmp->init_cpt == 0) {
+ free(tmp->init_ptr);
+ tmp->init_ptr = NULL;
}
}
-#endif
+ tmp->size = size;
return 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;
- if(nbr_block * size_block <= 0)
- return NULL;
+ void * tmp, * tmp2;
+ if(nbr_block * size_block <= 0) return NULL;
tmp = calloc(nbr_block, size_block);
- if(tmp == NULL)
- return NULL;
- return _store_block(tmp, nbr_block * size_block);
+ if(tmp == NULL) return NULL;
+ tmp2 = _store_block(tmp, nbr_block * size_block);
+ assert(tmp2 != NULL);
+ return tmp2;
}
+
+/* mark the size bytes of ptr as initialized */
void _initialize (void * ptr, size_t size) {
struct _block * tmp;
unsigned i;
- if(ptr == NULL || size <= 0)
- return;
+ assert(ptr != NULL);
+ assert(size > 0);
tmp = _get_cont(ptr);
- if(tmp == NULL)
- return;
-
+ assert(tmp != NULL);
+
/* already fully initialized, do nothing */
- if(tmp->init_cpt == tmp->size)
- return;
-
+ if(tmp->init_cpt == tmp->size) return;
+
/* fully uninitialized */
if(tmp->init_cpt == 0) {
- tmp->init_ptr = malloc(tmp->size * sizeof(char));
- memset(tmp->init_ptr, 0, tmp->size);
+ int nb = needed_bytes(tmp->size);
+ tmp->init_ptr = malloc(nb);
+ memset(tmp->init_ptr, 0, nb);
}
for(i = 0; i < size; i++) {
- if(!tmp->init_ptr[i + (char*)ptr /* JS: suspicious */ - tmp->ptr])
- tmp->init_cpt++;
- tmp->init_ptr[i + (char*)ptr /* JS: suspicious */ - tmp->ptr] = 1;
+ int byte_offset =(char*)ptr - tmp->ptr + i;
+ int ind = byte_offset / 8;
+ unsigned char mask_bit = 1U << (7 - (byte_offset % 8));
+ if((tmp->init_ptr[ind] & mask_bit) == 0) tmp->init_cpt++;
+ tmp->init_ptr[ind] |= mask_bit;
}
-
+
/* now fully initialized */
if(tmp->init_cpt == tmp->size) {
free(tmp->init_ptr);
@@ -270,102 +175,170 @@ void _initialize (void * ptr, size_t size) {
}
}
+
+/* mark all bytes of ptr as initialized */
void _full_init (void * ptr) {
struct _block * tmp;
- if(ptr == NULL)
- return;
+ assert(ptr != NULL);
tmp = _get_exact(ptr);
- if(tmp == NULL)
- return;
+ assert(tmp != NULL);
if (tmp->init_ptr != NULL) {
free(tmp->init_ptr);
tmp->init_ptr = NULL;
}
-
+
tmp->init_cpt = tmp->size;
}
+
+/* mark a block as litteral string */
+void _litteral_string (void * ptr) {
+ struct _block * tmp;
+ assert(ptr != NULL);
+ tmp = _get_exact(ptr);
+ assert(tmp != NULL);
+ tmp->is_litteral_string = true;
+}
+
+
+/* return whether the size bytes of ptr are initialized */
int _initialized (void * ptr, size_t size) {
struct _block * tmp;
unsigned i;
- if(ptr == NULL || size < 0)
- return 0; /* false */
+ assert(ptr != NULL);
+ assert(size > 0);
tmp = _get_cont(ptr);
- if(tmp == NULL)
- return 0; /* false */
-
+ assert(tmp != NULL);
+
/* fully uninitialized */
- if(tmp->init_cpt == 0)
- return 0; /* false */
+ if(tmp->init_cpt == 0) return false;
/* fully initialized */
- if(tmp->init_cpt == tmp->size)
- return 1; /* true */
-
- for(i = 0; i < size; i++)
+ if(tmp->init_cpt == tmp->size) return true;
+
+ for(i = 0; i < size; i++) {
/* if one byte is uninitialized */
- if(!tmp->init_ptr[i + (char*)ptr /* JS: suspicious */ - tmp->ptr])
- return 0; /* false */
- return 1; /* true */
+ int byte_offset =(char*)ptr - tmp->ptr + i;
+ int ind = byte_offset / 8;
+ unsigned char mask_bit = 1U << (7 - (byte_offset % 8));
+ if((tmp->init_ptr[ind] & mask_bit) == 0) return false;
+ }
+ return true;
}
-/* Do not verify whether PTR is valid! */
+/* return the length (in bytes) of the block containing ptr */
size_t _block_length(void* ptr) {
struct _block * tmp;
- if(ptr == NULL)
- return 0;
+ assert(ptr != NULL);
tmp = _get_cont(ptr);
- if(tmp == NULL)
- return 0;
- return tmp->ptr + tmp->size - (char*)ptr /* JS: suspicious */;
+ assert(tmp != NULL);
+ return tmp->size;
}
+/* return whether the size bytes of ptr are readable/writable */
int _valid(void* ptr, size_t size) {
struct _block * tmp;
- if(ptr == NULL || size < 0)
- return 0; /* false */
+ assert(ptr != NULL);
+ assert(size > 0);
tmp = _get_cont(ptr);
- if(tmp == NULL)
- return 0; /* false */
- return
- (tmp->ptr + tmp->size - (char*)ptr /* JS: suspicious */ >= size)
- && tmp->valid;
+ return (tmp == NULL) ?
+ false : ( tmp->size - ( (char*)ptr - tmp->ptr ) >= size
+ && !tmp->is_litteral_string);
}
-/* Do not verify whether PTR is valid ! */
+/* return whether the size bytes of ptr are readable */
+int _valid_read(void* ptr, size_t size) {
+ struct _block * tmp;
+ assert(ptr != NULL);
+ assert(size > 0);
+ tmp = _get_cont(ptr);
+ return (tmp == NULL) ?
+ false : ( tmp->size - ( (char*)ptr - tmp->ptr ) >= size );
+}
+
+
+/* return the base address of the block containing ptr */
void* _base_addr(void* ptr) {
struct _block * tmp;
- if(ptr == NULL)
- return NULL;
+ assert(ptr != NULL);
tmp = _get_cont(ptr);
- if(tmp == NULL)
- return NULL;
+ assert(tmp != NULL);
return tmp->ptr;
}
-/* Do not verify whether PTR is valid ! */
+/* return the offset of ptr within its block */
+/* TODO: remove `size` parameter */
int _offset(void* ptr, size_t size) {
- struct _block * tmp;
- if(ptr == NULL || size < 0)
- return -1; /* error */
- tmp = _get_cont(ptr);
- if(tmp == NULL)
- return -1; /* error */
- return ((char*)ptr /* JS: suspicious */ - tmp->ptr) / size;
+ struct _block * tmp;
+ assert(ptr != NULL);
+ tmp = _get_cont(ptr);
+ assert(tmp != NULL);
+ return ((char*)ptr - tmp->ptr);
}
+/*******************/
+/* PRINT */
+/*******************/
+
+
+/* print the information about a block */
+void _print_block (struct _block * ptr) {
+ if (ptr != NULL) {
+ printf("%p %zu (litt:%i); [init] : %li ",
+ ptr->ptr, ptr->size, ptr->is_litteral_string, ptr->init_cpt);
+ if(ptr->init_ptr != NULL) {
+ unsigned i;
+ for(i = 0; i < ptr->size; i++) {
+ int ind = i / 8;
+ int one_bit = (unsigned)1 << (8 - (i % 8) - 1);
+ printf("%i", (ptr->init_ptr[ind] & one_bit) != 0);
+ }
+ }
+ printf("\n");
+ }
+}
+
+
+/********************/
+/* CLEAN */
+/********************/
+
+
+/* erase information about initialization of a block */
+void _clean_init (struct _block * ptr) {
+ if(ptr->init_ptr != NULL) {
+ free(ptr->init_ptr);
+ ptr->init_ptr = NULL;
+ }
+ ptr->init_cpt = 0;
+}
+
+
+/* erase all information about a block */
+void _clean_block (struct _block * ptr) {
+ if(ptr == NULL) return;
+ _clean_init(ptr);
+ free(ptr);
+}
+
+
+/* erase the content of the abstract structure */
void __clean() {
__clean_struct();
- /* printf("cpt store: %i\n", __cpt_store);
- printf("cpt malloc: %i\n", __cpt_malloc);*/
}
+/**********************/
+/* DEBUG */
+/**********************/
+
+
+/* print the content of the abstract structure */
void __debug() {
__debug_struct();
}
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
index 90eb2862c9f..f66b49dd96d 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
@@ -4,65 +4,95 @@
#include "stdlib.h"
+/* allocate size bytes and store the returned block
+ * for further information, see malloc */
void * _malloc(size_t size)
__attribute__((FC_BUILTIN)) ;
+/* free the block starting at ptr,
+ * for further information, see free */
void _free(void * ptr)
__attribute__((FC_BUILTIN));
+/* resize the block starting at ptr to fit its new size,
+ * for further information, see realloc */
void * _realloc(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
+/* 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_elt, size_t size_elt)
__attribute__((FC_BUILTIN));
/* From outside the library, the following functions have no side effect */
+/* store the block of size bytes starting at ptr */
/*@ assigns \nothing; */
void * _store_block(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
+/* remove the block starting at ptr */
/*@ assigns \nothing; */
void _delete_block(void * ptr)
__attribute__((FC_BUILTIN));
+/* mark the size bytes of ptr as initialized */
/*@ assigns \nothing; */
void _initialize(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
+/* mark all bytes of ptr as initialized */
/*@ assigns \nothing; */
void _full_init(void * ptr)
__attribute__((FC_BUILTIN));
+/* marks a block as litteral string */
+/*@ assigns \nothing; */
+void _litteral_string(void * ptr);
+
/* ****************** */
/* E-ACSL annotations */
/* ****************** */
+/* return whether the first size bytes of ptr are readable/writable */
/*@ assigns \nothing; */
int _valid(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
+/* return whether the first size bytes of ptr are readable */
+/*@ assigns \nothing; */
+int _valid_read(void * ptr, size_t size)
+ __attribute__((FC_BUILTIN));
+
+/* return the base address of the block containing ptr */
/*@ assigns \nothing; */
void * _base_addr(void * ptr)
__attribute__((FC_BUILTIN));
+/* return the length (in bytes) of the block containing ptr */
/*@ assigns \nothing; */
size_t _block_length(void * ptr)
__attribute__((FC_BUILTIN));
+/* return the offset of ptr within its block */
/*@ assigns \nothing; */
int _offset(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
+/* return whether the size bytes of ptr are initialized */
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \initialized(((char *)ptr)+(0..size-1));
@ assigns \nothing; */
int _initialized(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
+/* print the content of the abstract structure */
void __debug(void)
__attribute__((FC_BUILTIN));
+/* erase the content of the abstract structure
+ * have to be called at the end of the `main` */
void __clean(void)
__attribute__((FC_BUILTIN));
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
index b7c50b67155..ab31e733eaf 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
@@ -2,29 +2,47 @@
#define E_ACSL_MMODEL_API
#include "stdlib.h"
+#include "stdbool.h"
/* Memory block allocated and may be deallocated */
struct _block {
- char* ptr; /* begin address */
- size_t size; /* size in bytes */
- int valid; /* whether the block has not been deallocated yet */
+ char * ptr; /* begin address */
+ size_t size; /* size in bytes */
/* Keep trace of initialized sub-blocks within a memory block */
- unsigned char * init_ptr; /* dynamic array of booleans */
- unsigned long init_cpt;
+ unsigned char * init_ptr; /* dynamic array of booleans */
+ unsigned long init_cpt;
+ _Bool is_litteral_string;
};
-void _print_block (struct _block * ptr);
-void _clean_init (struct _block * ptr);
-void _clean_block (struct _block * ptr);
+
+/* print the information about a block */
+void _print_block ( struct _block * ptr );
+/* erase information about initialization of a block */
+void _clean_init ( struct _block * ptr );
+/* erase all information about a block */
+void _clean_block ( struct _block * ptr );
+
/* functions to be implemented */
+
+/* remove the block from the structure */
void _remove_element ( struct _block * );
+/* add a block in the structure */
void _add_element ( struct _block * );
+/* return the block B such as : begin addr of B == ptr
+ we suppose that such a block exists, but we could return NULL if not */
struct _block * _get_exact ( void * );
+/* return the block B such as : begin addr of B > ptr
+ or NULL if such a block does not exist */
struct _block * _get_next ( void * );
+/* return the block B containing ptr, such as :
+ begin addr of B <= ptr < (begin addr + size) of B
+ or NULL if such a block does not exist */
struct _block * _get_cont ( void * );
+/* erase the content of the structure */
void __clean_struct ( );
+/* print the content of the structure */
void __debug_struct ( );
#endif
--
GitLab