From e8ff342894fb44f61acf7c48943824f87efb39be Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Mon, 27 Apr 2015 12:48:19 +0200 Subject: [PATCH] [mc] Cleanup mc_ignore/mcer_ignore --- src/mc/mc_ignore.cpp | 104 ++--------------------------------------- src/mc/mc_ignore.h | 1 - src/mc/mcer_ignore.cpp | 73 +++++++++++++++++++++++++++++ src/mc/mcer_ignore.h | 1 + 4 files changed, 78 insertions(+), 101 deletions(-) diff --git a/src/mc/mc_ignore.cpp b/src/mc/mc_ignore.cpp index 29bd63f225..a9f49f2c86 100644 --- a/src/mc/mc_ignore.cpp +++ b/src/mc/mc_ignore.cpp @@ -18,53 +18,6 @@ extern "C" { XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc, "Logging specific to MC ignore mechanism"); - -/**************************** Global variables ******************************/ -// Those structures live with the MCer and should be moved in the model_checker -// structure but they are currently used before the MC initialisation -// (in standalone mode). - - -extern xbt_dynar_t stacks_areas; - -/**************************** Structures ******************************/ -typedef struct s_mc_stack_ignore_variable { - char *var_name; - char *frame; -} s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t; - -/**************************** Free functions ******************************/ - -static void stack_ignore_variable_free(mc_stack_ignore_variable_t v) -{ - xbt_free(v->var_name); - xbt_free(v->frame); - xbt_free(v); -} - -static void stack_ignore_variable_free_voidp(void *v) -{ - stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v); -} - -static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r) -{ - xbt_free(r); -} - -static void checkpoint_ignore_region_free_voidp(void *r) -{ - checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r); -} - -xbt_dynar_t MC_checkpoint_ignore_new(void) -{ - return xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), - checkpoint_ignore_region_free_voidp); -} - -/***********************************************************************/ - // ***** Model-checked void MC_ignore_heap(void *address, size_t size) @@ -114,6 +67,10 @@ void MC_ignore_global_variable(const char *name) xbt_die("Unimplemented"); } +// ***** + +extern xbt_dynar_t stacks_areas; + void MC_stack_area_add(stack_region_t stack_area) { if (stacks_areas == NULL) @@ -162,57 +119,4 @@ void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t mmalloc_set_current_heap(heap); } -void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size) -{ - xbt_dynar_t checkpoint_ignore = process->checkpoint_ignore; - mc_checkpoint_ignore_region_t region = - xbt_new0(s_mc_checkpoint_ignore_region_t, 1); - region->addr = addr; - region->size = size; - - if (xbt_dynar_is_empty(checkpoint_ignore)) { - xbt_dynar_push(checkpoint_ignore, ®ion); - } else { - - unsigned int cursor = 0; - int start = 0; - int end = xbt_dynar_length(checkpoint_ignore) - 1; - mc_checkpoint_ignore_region_t current_region = NULL; - - while (start <= end) { - cursor = (start + end) / 2; - current_region = - (mc_checkpoint_ignore_region_t) xbt_dynar_get_as(checkpoint_ignore, - cursor, - mc_checkpoint_ignore_region_t); - if (current_region->addr == addr) { - if (current_region->size == size) { - checkpoint_ignore_region_free(region); - return; - } else if (current_region->size < size) { - start = cursor + 1; - } else { - end = cursor - 1; - } - } else if (current_region->addr < addr) { - start = cursor + 1; - } else { - end = cursor - 1; - } - } - - if (current_region->addr == addr) { - if (current_region->size < size) { - xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, ®ion); - } else { - xbt_dynar_insert_at(checkpoint_ignore, cursor, ®ion); - } - } else if (current_region->addr < addr) { - xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, ®ion); - } else { - xbt_dynar_insert_at(checkpoint_ignore, cursor, ®ion); - } - } -} - } diff --git a/src/mc/mc_ignore.h b/src/mc/mc_ignore.h index a5a6032c6b..3edc7eaa1d 100644 --- a/src/mc/mc_ignore.h +++ b/src/mc/mc_ignore.h @@ -12,7 +12,6 @@ SG_BEGIN_DECL(); -void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size); void MC_stack_area_add(stack_region_t stack_area); xbt_dynar_t MC_checkpoint_ignore_new(void); diff --git a/src/mc/mcer_ignore.cpp b/src/mc/mcer_ignore.cpp index 08cb7b098b..7e04041f8d 100644 --- a/src/mc/mcer_ignore.cpp +++ b/src/mc/mcer_ignore.cpp @@ -243,4 +243,77 @@ static void mc_ignore_local_variable_in_scope(const char *var_name, } } +// ****** Checkpoint ignore: + +static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r) +{ + xbt_free(r); +} + +static void checkpoint_ignore_region_free_voidp(void *r) +{ + checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r); +} + +xbt_dynar_t MC_checkpoint_ignore_new(void) +{ + return xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), + checkpoint_ignore_region_free_voidp); +} + +// ***** Generic memory ignore mechanism + +void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size) +{ + xbt_dynar_t checkpoint_ignore = process->checkpoint_ignore; + mc_checkpoint_ignore_region_t region = + xbt_new0(s_mc_checkpoint_ignore_region_t, 1); + region->addr = addr; + region->size = size; + + if (xbt_dynar_is_empty(checkpoint_ignore)) { + xbt_dynar_push(checkpoint_ignore, ®ion); + } else { + + unsigned int cursor = 0; + int start = 0; + int end = xbt_dynar_length(checkpoint_ignore) - 1; + mc_checkpoint_ignore_region_t current_region = NULL; + + while (start <= end) { + cursor = (start + end) / 2; + current_region = + (mc_checkpoint_ignore_region_t) xbt_dynar_get_as(checkpoint_ignore, + cursor, + mc_checkpoint_ignore_region_t); + if (current_region->addr == addr) { + if (current_region->size == size) { + checkpoint_ignore_region_free(region); + return; + } else if (current_region->size < size) { + start = cursor + 1; + } else { + end = cursor - 1; + } + } else if (current_region->addr < addr) { + start = cursor + 1; + } else { + end = cursor - 1; + } + } + + if (current_region->addr == addr) { + if (current_region->size < size) { + xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, ®ion); + } else { + xbt_dynar_insert_at(checkpoint_ignore, cursor, ®ion); + } + } else if (current_region->addr < addr) { + xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, ®ion); + } else { + xbt_dynar_insert_at(checkpoint_ignore, cursor, ®ion); + } + } +} + } diff --git a/src/mc/mcer_ignore.h b/src/mc/mcer_ignore.h index d8d3f3f80a..104bc8f24f 100644 --- a/src/mc/mcer_ignore.h +++ b/src/mc/mcer_ignore.h @@ -15,5 +15,6 @@ SG_BEGIN_DECL(); void MCer_ignore_global_variable(const char *var_name); void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region); void MC_heap_region_ignore_remove(void *address, size_t size); +void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size); SG_END_DECL(); -- 2.20.1