From 992f2813718d8b0c303bd47194ec37402d19345a Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 5 Oct 2021 16:36:29 +0200
Subject: [PATCH] [eacsl] Extract patricia trie from bittree
---
src/plugins/e-acsl/headers/header_spec.txt | 2 +
.../bittree_model/e_acsl_bittree.c | 503 ++++--------------
.../bittree_model/e_acsl_bittree.h | 53 +-
.../e_acsl_bittree_observation_model.c | 25 +-
.../e_acsl_observation_model.c | 1 +
.../internals/e_acsl_patricia_trie.c | 503 ++++++++++++++++++
.../internals/e_acsl_patricia_trie.h | 148 ++++++
7 files changed, 770 insertions(+), 465 deletions(-)
create mode 100644 src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c
create mode 100644 src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 03276ab748e..c367bfc6aaf 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -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
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
index 4c45a5defa9..21495817006 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
@@ -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
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h
index c17dd5f4b4d..710226ace62 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h
@@ -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
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
index ea30641feaa..3e48a5e1c20 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
@@ -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);
}
}
}
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
index 59316ab4f16..c7a9fd1d2b2 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
@@ -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
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c
new file mode 100644
index 00000000000..d8c669d7f95
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c
@@ -0,0 +1,503 @@
+/**************************************************************************/
+/* */
+/* 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
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h
new file mode 100644
index 00000000000..ad237b701de
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h
@@ -0,0 +1,148 @@
+/**************************************************************************/
+/* */
+/* 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
--
GitLab