Skip to content
Snippets Groups Projects
Commit 992f2813 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Extract patricia trie from bittree

parent 80fcbf98
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 770 additions and 465 deletions
src/plugins/e-acsl/headers/header_spec.txt
+ 2
− 0
View file @ 992f2813
......@@ -56,6 +56,8 @@ share/e-acsl/observation_model/bittree_model/e_acsl_bittree_timestamp_retrieval.
share/e-acsl/observation_model/internals/e_acsl_heap_tracking.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/observation_model/internals/e_acsl_heap_tracking.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/observation_model/internals/e_acsl_omodel_debug.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/observation_model/internals/e_acsl_safe_locations.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/observation_model/internals/e_acsl_safe_locations.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/observation_model/internals/e_acsl_timestamp_retrieval.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
......
src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
+ 89
− 414
View file @ 992f2813
......@@ -22,464 +22,139 @@
/*! ***********************************************************************
* \file
* \brief Patricia Trie API Implementation
* \brief Bittree implemented with a patricia trie.
**************************************************************************/
#include "../../internals/e_acsl_config.h"
#include "../../internals/e_acsl_malloc.h"
#include "../../internals/e_acsl_private_assert.h"
#include "../internals/e_acsl_patricia_trie.h"
#include "e_acsl_bittree.h"
#if E_ACSL_OS_IS_LINUX
# define WORDBITS __WORDSIZE
#elif E_ACSL_OS_IS_WINDOWS
// On windows, __WORDSIZE is not available
# ifdef _WIN64
# define WORDBITS 64
# else
# define WORDBITS 32
# endif
#else
# error "Unsupported OS"
#endif
static size_t mask(size_t, size_t);
#if WORDBITS == 16
static const size_t Tmasks[] = {0x0, 0x8000, 0xc000, 0xe000, 0xf000, 0xf800,
0xfc00, 0xfe00, 0xff00, 0xff80, 0xffc0, 0xffe0,
0xfff0, 0xfff8, 0xfffc, 0xfffe, 0xffff};
static const int Teq[] = {0, -1, 3, -3, 6, -5, 7, -7, 12,
-9, 11, -11, 14, -13, 15, 16, -16};
static const int Tneq[] = {0, 0, 1, -2, 2, -4, 5, -6, 4,
-8, 9, -10, 10, -12, 13, -14, -15};
#elif WORDBITS == 32
static const size_t Tmasks[] = {
0x0, 0x80000000, 0xc0000000, 0xe0000000, 0xf0000000, 0xf8000000,
0xfc000000, 0xfe000000, 0xff000000, 0xff800000, 0xffc00000, 0xffe00000,
0xfff00000, 0xfff80000, 0xfffc0000, 0xfffe0000, 0xffff0000, 0xffff8000,
0xffffc000, 0xffffe000, 0xfffff000, 0xfffff800, 0xfffffc00, 0xfffffe00,
0xffffff00, 0xffffff80, 0xffffffc0, 0xffffffe0, 0xfffffff0, 0xfffffff8,
0xfffffffc, 0xfffffffe, 0xffffffff};
static const int Teq[] = {0, -1, 3, -3, 6, -5, 7, -7, 12, -9, 11,
-11, 14, -13, 15, -15, 24, -17, 19, -19, 22, -21,
23, -23, 28, -25, 27, -27, 30, -29, 31, 32, -32};
static const 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, -31};
#else /* WORDBITS == 64 */
// clang-format off
static const size_t Tmasks[] = {
0x0,0x8000000000000000,0xc000000000000000,0xe000000000000000,0xf000000000000000,
0xf800000000000000,0xfc00000000000000,0xfe00000000000000,0xff00000000000000,
0xff80000000000000,0xffc0000000000000,0xffe0000000000000,0xfff0000000000000,
0xfff8000000000000,0xfffc000000000000,0xfffe000000000000,0xffff000000000000,
0xffff800000000000,0xffffc00000000000,0xffffe00000000000,0xfffff00000000000,
0xfffff80000000000,0xfffffc0000000000,0xfffffe0000000000,0xffffff0000000000,
0xffffff8000000000,0xffffffc000000000,0xffffffe000000000,0xfffffff000000000,
0xfffffff800000000,0xfffffffc00000000,0xfffffffe00000000,0xffffffff00000000,
0xffffffff80000000,0xffffffffc0000000,0xffffffffe0000000,0xfffffffff0000000,
0xfffffffff8000000,0xfffffffffc000000,0xfffffffffe000000,0xffffffffff000000,
0xffffffffff800000,0xffffffffffc00000,0xffffffffffe00000,0xfffffffffff00000,
0xfffffffffff80000,0xfffffffffffc0000,0xfffffffffffe0000,0xffffffffffff0000,
0xffffffffffff8000,0xffffffffffffc000,0xffffffffffffe000,0xfffffffffffff000,
0xfffffffffffff800,0xfffffffffffffc00,0xfffffffffffffe00,0xffffffffffffff00,
0xffffffffffffff80,0xffffffffffffffc0,0xffffffffffffffe0,0xfffffffffffffff0,
0xfffffffffffffff8,0xfffffffffffffffc,0xfffffffffffffffe,0xffffffffffffffff};
// clang-format on
static const int Teq[] = {0, -1, 3, -3, 6, -5, 7, -7, 12, -9, 11,
-11, 14, -13, 15, -15, 24, -17, 19, -19, 22, -21,
23, -23, 28, -25, 27, -27, 30, -29, 31, -31, 48,
-33, 35, -35, 38, -37, 39, -39, 44, -41, 43, -43,
46, -45, 47, -47, 56, -49, 51, -51, 54, -53, 55,
-55, 60, -57, 59, -59, 62, -61, 63, 64, -64};
static const 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};
#endif
/*! \brief Root node of the bitree */
static bt_node *bt_root = NULL;
/* common prefix of two addresses */
/*@ assigns \nothing;
@ ensures \forall int i;
0 <= i <= WORDBITS
==> (Tmasks[i] & a) == (Tmasks[i] & b)
==> \result >= Tmasks[i];
@ ensures (a & \result) == (b & \result);
@ ensures \exists int i; 0 <= i <= WORDBITS && \result == Tmasks[i];
@*/
static size_t mask(size_t a, size_t b) {
size_t nxor = ~(a ^ b), ret;
int i = WORDBITS / 2; /* dichotomic search, starting in the middle */
/*cpt_mask++;*/
/* 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
a negative element i from Teq or Tneq means stop and return Tmasks[-i] */
/*@ loop invariant -WORDBITS <= i <= WORDBITS;
@ loop assigns i;
@*/
while (i > 0) {
//@ assert 0 < i <= WORDBITS;
//@ assert \valid(Tmasks+i);
if (nxor >= Tmasks[i])
//@ assert \valid(Teq+i);
i = Teq[i];
else
//@ assert \valid(Tneq+i);
i = Tneq[i];
}
static pt_struct_t *bittree = NULL;
//@ assert -WORDBITS <= i <= 0;
ret = Tmasks[-i];
DASSERT((a & ret) == (b & ret));
return ret;
static void *bt_get_ptr(pt_leaf_t block) {
return (void *)((bt_block *)block)->ptr;
}
/* called from bt_remove */
/* the block we are looking for has to be in the tree */
/*@ requires \valid(ptr);
@ requires \valid(bt_root);
@ assigns \nothing;
@ ensures \valid(\result);
@ ensures \result->leaf == ptr;
@*/
static bt_node *bt_get_leaf_from_block(bt_block *ptr) {
bt_node *curr = bt_root;
DASSERT(bt_root != NULL);
DASSERT(ptr != NULL);
/*@ loop assigns curr;
@*/
while (!curr->is_leaf) {
// the prefix is consistent
DASSERT((curr->addr & curr->mask) == (ptr->ptr & curr->mask));
// two children
DASSERT(curr->left != NULL && curr->right != NULL);
// the prefix of one child is consistent
if ((curr->right->addr & curr->right->mask)
== (ptr->ptr & curr->right->mask))
curr = curr->right;
else if ((curr->left->addr & curr->left->mask)
== (ptr->ptr & curr->left->mask))
curr = curr->left;
else
private_abort("Unreachable\n");
}
DASSERT(curr->is_leaf);
DASSERT(curr->leaf == ptr);
return curr;
static int bt_contains_ptr(pt_leaf_t block, void *ptr) {
uintptr_t ptr_ui = (uintptr_t)ptr;
bt_block *b = (bt_block *)block;
return ptr_ui >= b->ptr
&& (ptr_ui < b->ptr + b->size || (b->size == 0 && ptr_ui == b->ptr));
}
/* remove the block from the structure */
/* the block we are looking for has to be in the tree */
/*@ requires \valid(ptr);
@*/
static void bt_remove(bt_block *ptr) {
bt_node *leaf_to_delete = bt_get_leaf_from_block(ptr);
DASSERT(leaf_to_delete->leaf == ptr);
if (leaf_to_delete->parent == NULL)
// the leaf is the root
bt_root = NULL;
else {
bt_node *sibling, *parent;
parent = leaf_to_delete->parent;
sibling = (leaf_to_delete == parent->left) ? parent->right : parent->left;
DASSERT(sibling != NULL);
// copying all sibling's fields into the parent's
parent->is_leaf = sibling->is_leaf;
parent->addr = sibling->addr;
parent->mask = sibling->mask;
parent->left = sibling->left;
parent->right = sibling->right;
parent->leaf = sibling->leaf;
if (!sibling->is_leaf) {
sibling->left->parent = parent;
sibling->right->parent = parent;
}
private_free(sibling);
/* necessary ? -- begin */
if (parent->parent != NULL) {
parent->parent->mask =
mask(parent->parent->left->addr & parent->parent->left->mask,
parent->parent->right->addr & parent->parent->right->mask);
}
/* necessary ? -- end */
/* erase information about initialization of a block */
void bt_clean_block_init(bt_block *ptr) {
if (ptr->init_ptr != NULL) {
private_free(ptr->init_ptr);
ptr->init_ptr = NULL;
}
private_free(leaf_to_delete);
ptr->init_bytes = 0;
}
/* called from bt_insert */
/* the returned node will be the sibling of the soon to be added node */
/*@ requires \valid(ptr);
@ requires \valid(bt_root);
@ assigns \nothing;
@ ensures \valid(\result);
@*/
static bt_node *bt_most_similar_node(bt_block *ptr) {
bt_node *curr = bt_root;
size_t left_prefix, right_prefix;
DASSERT(ptr != NULL);
DASSERT(bt_root != NULL);
while (1) {
if (curr->is_leaf)
return curr;
DASSERT(curr->left != NULL && curr->right != NULL);
left_prefix = mask(curr->left->addr & curr->left->mask, ptr->ptr);
right_prefix = mask(curr->right->addr & curr->right->mask, ptr->ptr);
if (left_prefix > right_prefix)
curr = curr->left;
else if (right_prefix > left_prefix)
curr = curr->right;
else
return curr;
}
bt_block *bt_alloc_block(uintptr_t ptr, size_t size) {
bt_block *res = private_malloc(sizeof(bt_block));
res->ptr = (uintptr_t)ptr;
res->size = size;
res->init_ptr = NULL;
res->init_bytes = 0;
res->is_readonly = 0;
res->is_freeable = 0;
#ifdef E_ACSL_DEBUG
res->line = 0;
res->file = "undefined";
#endif
#ifdef E_ACSL_TEMPORAL
res->timestamp = NEW_TEMPORAL_TIMESTAMP();
res->temporal_shadow = (size >= sizeof(void *)) ? private_malloc(size) : NULL;
#endif
return res;
}
/* add a block in the structure */
/*@ requires \valid(ptr);
@*/
static void bt_insert(bt_block *ptr) {
bt_node *new_leaf;
DASSERT(ptr != NULL);
new_leaf = private_malloc(sizeof(bt_node));
DASSERT(new_leaf != NULL);
new_leaf->is_leaf = 1;
new_leaf->addr = ptr->ptr;
new_leaf->mask = Tmasks[WORDBITS]; /* ~0ul */
new_leaf->left = NULL;
new_leaf->right = NULL;
new_leaf->parent = NULL;
new_leaf->leaf = ptr;
if (bt_root == NULL)
bt_root = new_leaf;
else {
bt_node *sibling = bt_most_similar_node(ptr), *parent, *aux;
DASSERT(sibling != NULL);
parent = private_malloc(sizeof(bt_node));
DASSERT(parent != NULL);
parent->is_leaf = 0;
parent->addr = sibling->addr & new_leaf->addr;
/*parent->mask = mask(sibling->addr & sibling->mask, ptr->ptr);*/
parent->leaf = NULL;
if (new_leaf->addr <= sibling->addr) {
parent->left = new_leaf;
parent->right = sibling;
} else {
parent->left = sibling;
parent->right = new_leaf;
}
new_leaf->parent = parent;
if (sibling == bt_root) {
parent->parent = NULL;
parent->mask = mask(sibling->addr & sibling->mask, ptr->ptr);
bt_root = parent;
} else {
if (sibling->parent->left == sibling)
sibling->parent->left = parent;
else
sibling->parent->right = parent;
parent->parent = sibling->parent;
/* necessary ? -- begin */
aux = parent;
aux->mask = mask(aux->left->addr & aux->left->mask,
aux->right->addr & aux->right->mask);
/* necessary ? -- end */
void bt_clean_and_free_block(bt_block *blk, int deallocate) {
if (blk) {
bt_clean_block_init(blk);
if (deallocate) {
#ifdef E_ACSL_TEMPORAL
private_free(blk->temporal_shadow);
#endif
private_free(blk);
}
sibling->parent = parent;
if (!sibling->is_leaf)
sibling->mask = mask(sibling->left->addr & sibling->left->mask,
sibling->right->addr & sibling->right->mask);
DASSERT((parent->left == sibling && parent->right == new_leaf)
|| (parent->left == new_leaf && parent->right == sibling));
}
}
/* return the block B such as: begin addr of B == ptr if such a block exists,
return NULL otherwise */
/*@ assigns \nothing;
@ ensures \valid(\result);
@ ensures \result == \null || \result->ptr == (size_t)ptr;
@*/
static bt_block *bt_lookup(void *ptr) {
bt_node *tmp = bt_root;
DASSERT(bt_root != NULL);
DASSERT(ptr != NULL);
/*@ loop assigns tmp;
@*/
while (!tmp->is_leaf) {
// if the ptr we are looking for does not share the prefix of tmp
if ((tmp->addr & tmp->mask) != ((size_t)ptr & tmp->mask))
return NULL;
// two children
DASSERT(tmp->left != NULL && tmp->right != NULL);
// the prefix of one child is consistent
if ((tmp->right->addr & tmp->right->mask)
== ((size_t)ptr & tmp->right->mask))
tmp = tmp->right;
else if ((tmp->left->addr & tmp->left->mask)
== ((size_t)ptr & tmp->left->mask))
tmp = tmp->left;
else
return NULL;
}
if (tmp->leaf->ptr != (size_t)ptr)
return NULL;
return tmp->leaf;
void bt_free_block(bt_block *blk) {
bt_clean_and_free_block(blk, 1);
}
/* 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 */
static bt_block *bt_find(void *ptr) {
bt_node *tmp = bt_root;
if (bt_root == NULL || ptr == NULL)
return NULL;
bt_node *other_choice = NULL;
while (1) {
if (tmp->is_leaf) {
/* tmp cannot contain ptr because its begin addr is higher */
if (tmp->addr > (size_t)ptr)
return NULL;
/* tmp->addr <= ptr, tmp may contain ptr
ptr is contained if tmp is large enough (begin addr + size) */
else if ((size_t)ptr < tmp->leaf->size + tmp->addr
|| (tmp->leaf->size == 0 && (size_t)ptr == tmp->leaf->ptr))
return tmp->leaf;
/* tmp->addr <= ptr, but tmp->addr is not large enough */
else
return NULL;
}
DASSERT(tmp->left != NULL && tmp->right != NULL);
/* erase all information about a block */
static int bt_clean_with_deallocation = 0;
static void bt_clean_block(pt_leaf_t ptr) {
bt_clean_and_free_block((bt_block *)ptr, bt_clean_with_deallocation);
}
/* the right child has the highest address, so we test it first */
if (((size_t)tmp->right->addr & tmp->right->mask)
<= ((size_t)ptr & tmp->right->mask)) {
other_choice = tmp->left;
tmp = tmp->right;
} else if (((size_t)tmp->left->addr & tmp->left->mask)
<= ((size_t)ptr & tmp->left->mask))
tmp = tmp->left;
else {
if (other_choice == NULL)
return NULL;
else {
tmp = other_choice;
other_choice = NULL;
}
static void bt_print_block(pt_leaf_t block) {
if (block != NULL) {
bt_block *b = (bt_block *)block;
DLOG("%a; %lu Bytes; %slitteral; [init] : %d ", (char *)b->ptr, b->size,
b->is_readonly ? "" : "not ", b->init_bytes);
if (b->init_ptr != NULL) {
unsigned i;
for (i = 0; i < b->size / 8; i++)
DLOG("%b ", b->init_ptr[i]);
}
DLOG("\n");
}
}
/*******************/
/* CLEAN */
/*******************/
/* erase information about initialization of a block */
static void bt_clean_block_init(bt_block *ptr) {
if (ptr->init_ptr != NULL) {
private_free(ptr->init_ptr);
ptr->init_ptr = NULL;
void bt_insert(bt_block *b) {
if (bittree == NULL) {
bittree =
pt_create(bt_get_ptr, bt_contains_ptr, bt_clean_block, bt_print_block);
}
ptr->init_bytes = 0;
pt_insert(bittree, (pt_leaf_t)b);
}
/* erase all information about a block */
static void bt_clean_block(bt_block *ptr) {
if (ptr) {
bt_clean_block_init(ptr);
private_free(ptr);
void bt_remove(bt_block *b) {
DASSERT(bittree != NULL);
pt_remove(bittree, (pt_leaf_t)b);
}
bt_block *bt_lookup(void *ptr) {
if (bittree == NULL) {
return NULL;
} else {
return pt_lookup(bittree, ptr);
}
}
/* called from bt_clean */
/* recursively erase the content of the structure */
static void bt_clean_rec(bt_node *ptr) {
if (ptr == NULL)
return;
else if (ptr->is_leaf) {
bt_clean_block(ptr->leaf);
ptr->leaf = NULL;
bt_block *bt_find(void *ptr) {
if (bittree == NULL) {
return NULL;
} else {
bt_clean_rec(ptr->left);
bt_clean_rec(ptr->right);
ptr->left = ptr->right = NULL;
return pt_find(bittree, ptr);
}
private_free(ptr);
}
/* erase the content of the structure */
static void bt_clean() {
bt_clean_rec(bt_root);
bt_root = NULL;
void bt_clean() {
DASSERT(bittree != NULL);
// Indicates to `bt_clean` (called by `pt_destroy`) that it should deallocate
// the leaves of the tree
bt_clean_with_deallocation = 1;
pt_destroy(bittree);
bt_clean_with_deallocation = 0;
bittree = NULL;
}
/*********************/
/* DEBUG */
/*********************/
#ifdef E_ACSL_DEBUG
static void eacsl_bt_print_block(bt_block *ptr) {
if (ptr != NULL) {
DLOG("%a; %lu Bytes; %slitteral; [init] : %d ", (char *)ptr->ptr, ptr->size,
ptr->is_readonly ? "" : "not ", ptr->init_bytes);
if (ptr->init_ptr != NULL) {
unsigned i;
for (i = 0; i < ptr->size / 8; i++)
DLOG("%b ", ptr->init_ptr[i]);
}
DLOG("\n");
}
}
static void bt_print_node(bt_node *ptr, int depth) {
int i;
if (ptr == NULL)
return;
for (i = 0; i < depth; i++)
DLOG(" ");
if (ptr->is_leaf)
eacsl_bt_print_block(ptr->leaf);
else {
DLOG("%p -- %p\n", (void *)ptr->mask, (void *)ptr->addr);
bt_print_node(ptr->left, depth + 1);
bt_print_node(ptr->right, depth + 1);
}
void eacsl_bt_print_block(bt_block *ptr) {
bt_print_block((pt_leaf_t)ptr);
}
static void eacsl_bt_print_tree() {
DLOG("------------DEBUG\n");
bt_print_node(bt_root, 0);
DLOG("-----------------\n");
void eacsl_bt_print_tree() {
pt_print(bittree);
}
#endif
src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h
+ 25
− 28
View file @ 992f2813
......@@ -22,8 +22,8 @@
/*! ***********************************************************************
* \file
* \brief Patricia Trie API
**************************************************************************/
* \brief Bittree API
***************************************************************************/
#ifndef E_ACSL_BITTREE
#define E_ACSL_BITTREE
......@@ -31,9 +31,17 @@
#include <stddef.h>
#include <stdint.h>
/* Public API {{{ */
/* Debug */
#ifdef E_ACSL_DEBUG
# define eacsl_bt_print_block export_alias(bt_print_block)
# define eacsl_bt_print_tree export_alias(bt_print_tree)
#endif
/* }}} */
/*! \brief Structure representing an allocated memory block */
struct bt_block {
size_t ptr; //!< Base address
uintptr_t ptr; //!< Base address
size_t size; //!< Block length (in bytes)
unsigned char *init_ptr; //!< Per-bit initialization
size_t init_bytes; //!< Number of initialized bytes within a block
......@@ -51,54 +59,43 @@ struct bt_block {
typedef struct bt_block bt_block;
/*! \brief Structure representing a bittree node */
struct bt_node {
int is_leaf;
size_t addr, mask;
struct bt_node *left, *right, *parent;
bt_block *leaf;
};
typedef struct bt_node bt_node;
/*! \brief Remove a block from the structure */
static void bt_remove(bt_block *b);
void bt_remove(bt_block *b);
/*! \brief Add a block to the structure */
static void bt_insert(bt_block *b);
void bt_insert(bt_block *b);
/*! \brief Look-up a memory block by its base address
NB: The function assumes that such a block exists. */
static bt_block *bt_lookup(void *ptr);
bt_block *bt_lookup(void *ptr);
/*! \brief Find a memory block containing a given memory address
*
* Return block B such that:
* `\base_addr(B->ptr) <= ptr < (\base_addr(B->ptr) + size)`
* or NULL if such a block does not exist. */
static bt_block *bt_find(void *ptr);
bt_block *bt_find(void *ptr);
/*! \brief Erase the contents of the structure */
static void bt_clean(void);
void bt_clean(void);
/*! \brief Erase information about a block's initialization */
static void bt_clean_block_init(bt_block *b);
void bt_clean_block_init(bt_block *b);
/*! \brief Allocates a `bt_block` for a block of memory at address `ptr` and
with the given size. */
bt_block *bt_alloc_block(uintptr_t ptr, size_t size);
/*! \brief Erase all information about a given block */
static void bt_clean_block(bt_block *b);
/*! \brief Frees the given `bt_block`. */
void bt_free_block(bt_block *blk);
#ifdef E_ACSL_DEBUG
/*! \brief Print information about a given block */
static void eacsl_bt_print_block(bt_block *b);
/*! \brief Recursively print the contents of the bittree starting from a
* given node */
/*@ assigns \nothing; */
static void bt_print_node(bt_node *ptr, int depth);
void eacsl_bt_print_block(bt_block *b);
/*! \brief Print the contents of the entire bittree */
/*@ assigns \nothing; */
static void bt_print();
void eacsl_bt_print_tree();
#endif
#endif // E_ACSL_BITTREE
src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
+ 2
− 23
View file @ 992f2813
......@@ -39,8 +39,6 @@
/* Public API {{{ */
/* Debug */
#ifdef E_ACSL_DEBUG
# define eacsl_bt_print_block export_alias(bt_print_block)
# define eacsl_bt_print_tree export_alias(bt_print_tree)
# define eacsl_block_info export_alias(block_info)
# define eacsl_store_block_debug export_alias(store_block_debug)
# define eacsl_delete_block_debug export_alias(delete_block_debug)
......@@ -304,23 +302,8 @@ void *eacsl_store_block(void *ptr, size_t size) {
#endif
bt_block *tmp = NULL;
if (ptr) {
tmp = private_malloc(sizeof(bt_block));
tmp->ptr = (uintptr_t)ptr;
tmp->size = size;
tmp->init_ptr = NULL;
tmp->init_bytes = 0;
tmp->is_readonly = 0;
tmp->is_freeable = 0;
tmp = bt_alloc_block((uintptr_t)ptr, size);
bt_insert(tmp);
#ifdef E_ACSL_DEBUG
tmp->line = 0;
tmp->file = "undefined";
#endif
#ifdef E_ACSL_TEMPORAL
tmp->timestamp = NEW_TEMPORAL_TIMESTAMP();
tmp->temporal_shadow =
(size >= sizeof(void *)) ? private_malloc(size) : NULL;
#endif
}
return tmp;
}
......@@ -355,12 +338,8 @@ void eacsl_delete_block(void *ptr) {
private_abort("Attempt to delete untracked block\n");
#endif
if (tmp) {
bt_clean_block_init(tmp);
#ifdef E_ACSL_TEMPORAL
private_free(tmp->temporal_shadow);
#endif
bt_remove(tmp);
private_free(tmp);
bt_free_block(tmp);
}
}
}
......
src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
+ 1
− 0
View file @ 992f2813
......@@ -93,6 +93,7 @@ int eacsl_separated(size_t count, ...) {
/************************************************************************/
#include "internals/e_acsl_heap_tracking.c"
#include "internals/e_acsl_patricia_trie.c"
#include "internals/e_acsl_safe_locations.c"
/* Select memory model, either segment-based or bittree-based model should
......
src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c 0 → 100644
+ 503
− 0
View file @ 992f2813
/**************************************************************************/
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
/* Copyright (C) 2012-2021 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
/* you can redistribute it and/or modify it under the terms of the GNU */
/* Lesser General Public License as published by the Free Software */
/* Foundation, version 2.1. */
/* */
/* It is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
/* GNU Lesser General Public License for more details. */
/* */
/* See the GNU Lesser General Public License version 2.1 */
/* for more details (enclosed in the file licenses/LGPLv2.1). */
/* */
/**************************************************************************/
/*! ***********************************************************************
* \file
* \brief Patricia Trie API Implementation
***************************************************************************/
#include <stdint.h>
#include "../../internals/e_acsl_config.h"
#include "../../internals/e_acsl_malloc.h"
#include "../../internals/e_acsl_private_assert.h"
#include "e_acsl_patricia_trie.h"
#if E_ACSL_OS_IS_LINUX
# define WORDBITS __WORDSIZE
#elif E_ACSL_OS_IS_WINDOWS
// On windows, __WORDSIZE is not available
# ifdef _WIN64
# define WORDBITS 64
# else
# define WORDBITS 32
# endif
#else
# error "Unsupported OS"
#endif
#if WORDBITS == 16
static const uintptr_t PT_MASKS[] = {
0x0, 0x8000, 0xc000, 0xe000, 0xf000, 0xf800, 0xfc00, 0xfe00, 0xff00,
0xff80, 0xffc0, 0xffe0, 0xfff0, 0xfff8, 0xfffc, 0xfffe, 0xffff};
static const int PT_EQ[] = {0, -1, 3, -3, 6, -5, 7, -7, 12,
-9, 11, -11, 14, -13, 15, 16, -16};
static const int PT_NEQ[] = {0, 0, 1, -2, 2, -4, 5, -6, 4,
-8, 9, -10, 10, -12, 13, -14, -15};
#elif WORDBITS == 32
static const uintptr_t PT_MASKS[] = {
0x0, 0x80000000, 0xc0000000, 0xe0000000, 0xf0000000, 0xf8000000,
0xfc000000, 0xfe000000, 0xff000000, 0xff800000, 0xffc00000, 0xffe00000,
0xfff00000, 0xfff80000, 0xfffc0000, 0xfffe0000, 0xffff0000, 0xffff8000,
0xffffc000, 0xffffe000, 0xfffff000, 0xfffff800, 0xfffffc00, 0xfffffe00,
0xffffff00, 0xffffff80, 0xffffffc0, 0xffffffe0, 0xfffffff0, 0xfffffff8,
0xfffffffc, 0xfffffffe, 0xffffffff};
static const int PT_EQ[] = {0, -1, 3, -3, 6, -5, 7, -7, 12,
-9, 11, -11, 14, -13, 15, -15, 24, -17,
19, -19, 22, -21, 23, -23, 28, -25, 27,
-27, 30, -29, 31, 32, -32};
static const int PT_NEQ[] = {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, -31};
#else /* WORDBITS == 64 */
// clang-format off
static const size_t PT_MASKS[] = {
0x0,0x8000000000000000,0xc000000000000000,0xe000000000000000,0xf000000000000000,
0xf800000000000000,0xfc00000000000000,0xfe00000000000000,0xff00000000000000,
0xff80000000000000,0xffc0000000000000,0xffe0000000000000,0xfff0000000000000,
0xfff8000000000000,0xfffc000000000000,0xfffe000000000000,0xffff000000000000,
0xffff800000000000,0xffffc00000000000,0xffffe00000000000,0xfffff00000000000,
0xfffff80000000000,0xfffffc0000000000,0xfffffe0000000000,0xffffff0000000000,
0xffffff8000000000,0xffffffc000000000,0xffffffe000000000,0xfffffff000000000,
0xfffffff800000000,0xfffffffc00000000,0xfffffffe00000000,0xffffffff00000000,
0xffffffff80000000,0xffffffffc0000000,0xffffffffe0000000,0xfffffffff0000000,
0xfffffffff8000000,0xfffffffffc000000,0xfffffffffe000000,0xffffffffff000000,
0xffffffffff800000,0xffffffffffc00000,0xffffffffffe00000,0xfffffffffff00000,
0xfffffffffff80000,0xfffffffffffc0000,0xfffffffffffe0000,0xffffffffffff0000,
0xffffffffffff8000,0xffffffffffffc000,0xffffffffffffe000,0xfffffffffffff000,
0xfffffffffffff800,0xfffffffffffffc00,0xfffffffffffffe00,0xffffffffffffff00,
0xffffffffffffff80,0xffffffffffffffc0,0xffffffffffffffe0,0xfffffffffffffff0,
0xfffffffffffffff8,0xfffffffffffffffc,0xfffffffffffffffe,0xffffffffffffffff};
// clang-format on
static const int PT_EQ[] = {
0, -1, 3, -3, 6, -5, 7, -7, 12, -9, 11, -11, 14,
-13, 15, -15, 24, -17, 19, -19, 22, -21, 23, -23, 28, -25,
27, -27, 30, -29, 31, -31, 48, -33, 35, -35, 38, -37, 39,
-39, 44, -41, 43, -43, 46, -45, 47, -47, 56, -49, 51, -51,
54, -53, 55, -55, 60, -57, 59, -59, 62, -61, 63, 64, -64};
static const int PT_NEQ[] = {
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};
#endif
typedef struct pt_node {
uintptr_t addr, mask;
struct pt_node *left, *right, *parent;
pt_leaf_t leaf;
int is_leaf;
} pt_node_t;
typedef struct pt_struct {
/*! \brief Root node of the trie. */
pt_node_t *root;
/*! \brief Function to extract the pointer of a leaf. */
get_ptr_fct_t get_ptr_fct;
/*! \brief Function to test if a leaf contains a pointer. */
contains_ptr_fct_t contains_ptr_fct;
/*! \brief Function to clean the content of a leaf. */
clean_leaf_fct_t clean_leaf_fct;
/*! \brief Function to print the content of a leaf. */
print_leaf_fct_t print_leaf_fct;
} pt_struct_t;
/* common prefix of two addresses */
/*@ assigns \nothing;
@ ensures \forall int i;
0 <= i <= WORDBITS
==> (PT_MASKS[i] & a) == (PT_MASKS[i] & b)
==> \result >= PT_MASKS[i];
@ ensures (a & \result) == (b & \result);
@ ensures \exists int i; 0 <= i <= WORDBITS && \result == PT_MASKS[i];
@*/
static uintptr_t pt_mask(uintptr_t a, uintptr_t b) {
uintptr_t nxor = ~(a ^ b), ret;
int i = WORDBITS / 2; /* dichotomic search, starting in the middle */
/* if the current mask matches we use transition from PT_EQ, else from PT_NEQ
we stop as soon as i is negative, meaning that we found the mask
a negative element i from PT_EQ or PT_NEQ means stop and return PT_MASKS[-i] */
/*@ loop invariant -WORDBITS <= i <= WORDBITS;
@ loop assigns i;
@*/
while (i > 0) {
//@ assert 0 < i <= WORDBITS;
//@ assert \valid(PT_MASKS+i);
if (nxor >= PT_MASKS[i])
//@ assert \valid(PT_EQ+i);
i = PT_EQ[i];
else
//@ assert \valid(PT_NEQ+i);
i = PT_NEQ[i];
}
//@ assert -WORDBITS <= i <= 0;
ret = PT_MASKS[-i];
DASSERT((a & ret) == (b & ret));
return ret;
}
pt_struct_t *pt_create(get_ptr_fct_t get_ptr_fct,
contains_ptr_fct_t contains_ptr_fct,
clean_leaf_fct_t clean_leaf_fct,
print_leaf_fct_t print_leaf_fct) {
DASSERT(get_ptr_fct != NULL);
DASSERT(contains_ptr_fct != NULL);
DASSERT(clean_leaf_fct != NULL);
DASSERT(print_leaf_fct != NULL);
pt_struct_t *pt = private_malloc(sizeof(pt_struct_t));
DASSERT(pt != NULL);
pt->root = NULL;
pt->get_ptr_fct = get_ptr_fct;
pt->contains_ptr_fct = contains_ptr_fct;
pt->clean_leaf_fct = clean_leaf_fct;
pt->print_leaf_fct = print_leaf_fct;
return pt;
}
void pt_destroy(pt_struct_t *pt) {
DASSERT(pt != NULL);
pt_clean(pt);
private_free(pt);
}
/* called from pt_insert */
/* the returned node will be the sibling of the soon to be added node */
/*@ requires \valid_read(pt);
@ requires \valid_read(pt->root);
@ requires \valid_read(leaf);
@ assigns \nothing;
@ ensures \valid(\result); */
static pt_node_t *pt_most_similar_node(const pt_struct_t *pt, pt_leaf_t leaf) {
DASSERT(pt != NULL);
DASSERT(pt->root != NULL);
DASSERT(leaf != NULL);
pt_node_t *curr = pt->root;
uintptr_t left_prefix, right_prefix;
uintptr_t ptr = (uintptr_t)pt->get_ptr_fct(leaf);
while (1) {
if (curr->is_leaf) {
return curr;
}
DASSERT(curr->left != NULL && curr->right != NULL);
left_prefix = pt_mask(curr->left->addr & curr->left->mask, ptr);
right_prefix = pt_mask(curr->right->addr & curr->right->mask, ptr);
if (left_prefix > right_prefix) {
curr = curr->left;
} else if (right_prefix > left_prefix) {
curr = curr->right;
} else {
return curr;
}
}
}
void pt_insert(pt_struct_t *pt, pt_leaf_t leaf) {
DASSERT(pt != NULL);
DASSERT(leaf != NULL);
pt_node_t *new_leaf_node;
uintptr_t ptr = (uintptr_t)pt->get_ptr_fct(leaf);
new_leaf_node = private_malloc(sizeof(pt_node_t));
DASSERT(new_leaf_node != NULL);
new_leaf_node->is_leaf = 1;
new_leaf_node->addr = ptr;
new_leaf_node->mask = PT_MASKS[WORDBITS]; /* ~0ul */
new_leaf_node->left = NULL;
new_leaf_node->right = NULL;
new_leaf_node->parent = NULL;
new_leaf_node->leaf = leaf;
if (pt->root == NULL) {
pt->root = new_leaf_node;
} else {
pt_node_t *sibling = pt_most_similar_node(pt, leaf), *parent, *aux;
DASSERT(sibling != NULL);
parent = private_malloc(sizeof(pt_node_t));
DASSERT(parent != NULL);
parent->is_leaf = 0;
parent->addr = sibling->addr & new_leaf_node->addr;
/*parent->mask = pt_mask(sibling->addr & sibling->mask, ptr);*/
parent->leaf = NULL;
if (new_leaf_node->addr <= sibling->addr) {
parent->left = new_leaf_node;
parent->right = sibling;
} else {
parent->left = sibling;
parent->right = new_leaf_node;
}
new_leaf_node->parent = parent;
if (sibling == pt->root) {
parent->parent = NULL;
parent->mask = pt_mask(sibling->addr & sibling->mask, ptr);
pt->root = parent;
} else {
if (sibling->parent->left == sibling) {
sibling->parent->left = parent;
} else {
sibling->parent->right = parent;
}
parent->parent = sibling->parent;
/* necessary ? -- begin */
aux = parent;
aux->mask = pt_mask(aux->left->addr & aux->left->mask,
aux->right->addr & aux->right->mask);
/* necessary ? -- end */
}
sibling->parent = parent;
if (!sibling->is_leaf) {
sibling->mask = pt_mask(sibling->left->addr & sibling->left->mask,
sibling->right->addr & sibling->right->mask);
}
DASSERT((parent->left == sibling && parent->right == new_leaf_node)
|| (parent->left == new_leaf_node && parent->right == sibling));
}
}
/* called from pt_remove */
/* the leaf we are looking for has to be in the tree */
/*@ requires \valid_read(pt);
@ requires \valid_read(pt->root);
@ requires \valid_read(leaf);
@ assigns \nothing;
@ ensures \valid(\result);
@ ensures \result->leaf == ptr; */
static pt_node_t *pt_get_leaf_node_from_leaf(const pt_struct_t *pt,
pt_leaf_t leaf) {
DASSERT(pt != NULL);
DASSERT(pt->root != NULL);
DASSERT(leaf != NULL);
pt_node_t *curr = pt->root;
uintptr_t ptr = (uintptr_t)pt->get_ptr_fct(leaf);
/*@ loop assigns curr; */
while (!curr->is_leaf) {
// the prefix is consistent
DASSERT((curr->addr & curr->mask) == (ptr & curr->mask));
// two children
DASSERT(curr->left != NULL && curr->right != NULL);
// the prefix of one child is consistent
if ((curr->right->addr & curr->right->mask) == (ptr & curr->right->mask)) {
curr = curr->right;
} else if ((curr->left->addr & curr->left->mask)
== (ptr & curr->left->mask)) {
curr = curr->left;
} else {
private_abort("Unreachable\n");
}
}
DASSERT(curr->is_leaf);
DASSERT(curr->leaf == leaf);
return curr;
}
void pt_remove(pt_struct_t *pt, pt_leaf_t leaf) {
pt_node_t *leaf_node_to_delete = pt_get_leaf_node_from_leaf(pt, leaf);
DASSERT(leaf_node_to_delete->leaf == leaf);
if (leaf_node_to_delete->parent == NULL) {
// the leaf is the root
pt->root = NULL;
} else {
pt_node_t *sibling, *parent;
parent = leaf_node_to_delete->parent;
sibling =
(leaf_node_to_delete == parent->left) ? parent->right : parent->left;
DASSERT(sibling != NULL);
// copying all sibling's fields into the parent's
parent->is_leaf = sibling->is_leaf;
parent->addr = sibling->addr;
parent->mask = sibling->mask;
parent->left = sibling->left;
parent->right = sibling->right;
parent->leaf = sibling->leaf;
if (!sibling->is_leaf) {
sibling->left->parent = parent;
sibling->right->parent = parent;
}
private_free(sibling);
/* necessary ? -- begin */
if (parent->parent != NULL) {
parent->parent->mask =
pt_mask(parent->parent->left->addr & parent->parent->left->mask,
parent->parent->right->addr & parent->parent->right->mask);
}
/* necessary ? -- end */
}
private_free(leaf_node_to_delete);
}
pt_leaf_t pt_lookup(const pt_struct_t *pt, void *ptr) {
DASSERT(pt != NULL);
DASSERT(pt->root != NULL);
DASSERT(ptr != NULL);
pt_node_t *tmp = pt->root;
/*@ loop assigns tmp;
@*/
while (!tmp->is_leaf) {
// if the ptr we are looking for does not share the prefix of tmp
if ((tmp->addr & tmp->mask) != ((uintptr_t)ptr & tmp->mask)) {
return NULL;
}
// two children
DASSERT(tmp->left != NULL && tmp->right != NULL);
// the prefix of one child is consistent
if ((tmp->right->addr & tmp->right->mask)
== ((uintptr_t)ptr & tmp->right->mask)) {
tmp = tmp->right;
} else if ((tmp->left->addr & tmp->left->mask)
== ((uintptr_t)ptr & tmp->left->mask)) {
tmp = tmp->left;
} else {
return NULL;
}
}
if (pt->get_ptr_fct(tmp->leaf) != ptr) {
return NULL;
}
return tmp->leaf;
}
pt_leaf_t pt_find(const pt_struct_t *pt, void *ptr) {
DASSERT(pt != NULL);
if (pt->root == NULL || ptr == NULL) {
return NULL;
}
pt_node_t *tmp = pt->root;
pt_node_t *other_choice = NULL;
while (1) {
if (tmp->is_leaf) {
/* tmp cannot contain ptr because its begin addr is higher */
if (tmp->addr > (uintptr_t)ptr) {
return NULL;
}
/* tmp->addr <= ptr, tmp may contain ptr */
else if (pt->contains_ptr_fct(tmp->leaf, ptr)) {
return tmp->leaf;
}
/* tmp->addr <= ptr, but tmp does not contain ptr */
else {
return NULL;
}
}
DASSERT(tmp->left != NULL && tmp->right != NULL);
/* the right child has the highest address, so we test it first */
if ((tmp->right->addr & tmp->right->mask)
<= ((uintptr_t)ptr & tmp->right->mask)) {
other_choice = tmp->left;
tmp = tmp->right;
} else if ((tmp->left->addr & tmp->left->mask)
<= ((uintptr_t)ptr & tmp->left->mask)) {
tmp = tmp->left;
} else {
if (other_choice == NULL) {
return NULL;
} else {
tmp = other_choice;
other_choice = NULL;
}
}
}
}
static void pt_clean_rec(const pt_struct_t *pt, pt_node_t *ptr) {
if (ptr == NULL) {
return;
} else if (ptr->is_leaf) {
pt->clean_leaf_fct(ptr->leaf);
ptr->leaf = NULL;
} else {
pt_clean_rec(pt, ptr->left);
pt_clean_rec(pt, ptr->right);
ptr->left = ptr->right = NULL;
}
private_free(ptr);
}
void pt_clean(pt_struct_t *pt) {
DASSERT(pt != NULL);
pt_clean_rec(pt, pt->root);
pt->root = NULL;
}
#ifdef E_ACSL_DEBUG
static void pt_print_node(const pt_struct_t *pt, pt_node_t *node, int depth) {
if (node == NULL) {
return;
}
// Indentation
for (int i = 0; i < depth; ++i) {
DLOG(" ");
}
// Print node
if (node->is_leaf) {
pt->print_leaf_fct(node->leaf);
} else {
DLOG("%p -- %p\n", (void *)node->mask, (void *)node->addr);
pt_print_node(pt, node->left, depth + 1);
pt_print_node(pt, node->right, depth + 1);
}
}
void pt_print(const pt_struct_t *pt) {
DLOG("------------DEBUG\n");
if (pt != NULL) {
pt_print_node(pt, pt->root, 0);
} else {
DLOG("Patricia trie is NULL\n");
}
DLOG("-----------------\n");
}
#endif // E_ACSL_DEBUG
src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h 0 → 100644
+ 148
− 0
View file @ 992f2813
/**************************************************************************/
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
/* Copyright (C) 2012-2021 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
/* you can redistribute it and/or modify it under the terms of the GNU */
/* Lesser General Public License as published by the Free Software */
/* Foundation, version 2.1. */
/* */
/* It is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
/* GNU Lesser General Public License for more details. */
/* */
/* See the GNU Lesser General Public License version 2.1 */
/* for more details (enclosed in the file licenses/LGPLv2.1). */
/* */
/**************************************************************************/
/*! ***********************************************************************
* \file
* \brief Patricia Trie API
***************************************************************************/
#ifndef E_ACSL_PATRICIA_TRIE
#define E_ACSL_PATRICIA_TRIE
#ifdef __FC_FEATURES_H
# include <__fc_alloc_axiomatic.h>
#else
/*@ ghost extern int __fc_heap_status; */
#endif
/*! \brief Opaque pointer representing a leaf on the patricia trie. */
typedef void *pt_leaf_t;
/*! \brief Function pointer to a function that retrieves the pointer of a
leaf. */
typedef void *(*get_ptr_fct_t)(pt_leaf_t);
/*! \brief Function pointer to a function that tests whether a leaf contains the
given pointer. */
typedef int (*contains_ptr_fct_t)(pt_leaf_t, void *);
/*! \brief Function pointer to a function that cleans (i.e. free memory) the
content of a leaf. */
typedef void (*clean_leaf_fct_t)(pt_leaf_t);
/*! \brief Function pointer to a function that prints the content of a leaf. */
typedef void (*print_leaf_fct_t)(pt_leaf_t);
/*! \brief Opaque structure of a patricia trie. */
typedef struct pt_struct pt_struct_t;
/*! \brief Create a patricia trie.
\param get_ptr_fct Function to extract the pointer of a leaf.
\param contains_ptr_fct Function to test if a leaf contains a pointer.
\param clean_leaf_fct Function to clean the content of a leaf.
\param print_leaf_fct Function to print the content of a leaf.
\return The newly created patricia trie. */
/*@ requires \valid_function(get_ptr_fct_t get_ptr_fct);
@ requires \valid_function(contains_ptr_fct_t contains_ptr_fct);
@ requires \valid_function(clean_leaf_fct_t clean_leaf_fct);
@ requires \valid_function(print_leaf_fct_t print_leaf_fct);
@ allocates \result;
@ assigns *\result \from get_ptr_fct, contains_ptr_fct, clean_leaf_fct,
print_leaf_fct;
@ admit ensures \valid(\result); */
pt_struct_t *pt_create(get_ptr_fct_t get_ptr_fct,
contains_ptr_fct_t contains_ptr_fct,
clean_leaf_fct_t clean_leaf_fct,
print_leaf_fct_t print_leaf_fct);
/*! \brief Clean and destroy the patricia trie.
\param pt The patricia trie to destroy. */
/*@ requires \valid(pt);
@ frees pt; */
void pt_destroy(pt_struct_t *pt);
/*! \brief Insert a new leaf to the patricia trie.
\param pt Patricia trie to update.
\param leaf Leaf to add to the trie. */
/*@ requires \valid(pt);
@ assigns __fc_heap_status \from __fc_heap_status;
@ assigns *pt \from *pt, leaf, indirect:__fc_heap_status; */
void pt_insert(pt_struct_t *pt, pt_leaf_t leaf);
/*! \brief Remove an existing leaf from the patricia trie.
\param pt Patricia trie to update.
\param leaf Leaf to remove from the trie. */
/*@ requires \valid(pt);
@ assigns __fc_heap_status \from __fc_heap_status;
@ assigns *pt \from *pt, leaf, indirect:__fc_heap_status; */
void pt_remove(pt_struct_t *pt, pt_leaf_t leaf);
/*! \brief Look for the leaf representing exactly the given pointer.
Given the function `get_fct_ptr` provided at the trie creation and a leaf
`l`, the leaf representing exactly the given pointer `ptr` is the leaf such
that `get_fct_ptr(l) == ptr`.
\param pt Patricia trie where to look for.
\param ptr Pointer to look for in the leaves of the patricia trie.
\return The leaf representing exactly the given pointer. */
/*@ requires \valid_read(pt);
@ requires ptr != \null;
@ assigns \result \from *pt, indirect:ptr; */
pt_leaf_t pt_lookup(const pt_struct_t *pt, void *ptr);
/*! \brief Look for the leaf containing the given pointer.
Given the function `contains_ptr_fct` provided at the trie creation and a
leaf `l`, the leaf containing the given pointer is the leaf such that
`contains_ptr_fct(l, ptr) != 0`.
\param pt Patricia trie where to look for.
\param ptr Pointer to look for in the leaves of the patricia trie.
\return The leaf containing the given pointer. */
/*@ requires \valid_read(pt);
@ assigns \result \from *pt, indirect:ptr; */
pt_leaf_t pt_find(const pt_struct_t *pt, void *ptr);
/*! \brief Clean the content of the given patricia trie.
Contrary to `pt_destroy()`, this function removes all leaves of the trie but
does not destroy the trie. The function `pt_insert()` can still be called on
the trie afterward.
\param pt Patricia trie to update. */
/*@ requires \valid(pt);
@ assigns __fc_heap_status \from __fc_heap_status;
@ assigns *pt \from *pt, indirect:__fc_heap_status; */
void pt_clean(pt_struct_t *pt);
#ifdef E_ACSL_DEBUG
/*! \brief Print the content of the given patricia trie.
The function `print_leaf_fct` provided at the trie creation is used to print
the leaves.
\param pt The patricia trie to print. */
/*@ requires pt == \null || \valid_read(pt);
@ assigns \nothing; */
void pt_print(const pt_struct_t *pt);
#endif // E_ACSL_DEBUG
#endif // E_ACSL_PATRICIA_TRIE
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment