From df2fe4fa15d80bf6b15e648aa962d15a2a40a2c7 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 27 Sep 2012 18:28:14 +0200 Subject: [PATCH] model-checker : ignore stack areas in heap comparison algorithm for the comparison of local variables with dwarf --- include/xbt/mmalloc.h | 4 ++- src/include/mc/datatypes.h | 5 ++++ src/include/mc/mc.h | 2 ++ src/mc/mc_global.c | 12 +++++++++ src/simix/smx_context_base.c | 14 ++++++++++ src/xbt/mmalloc/mm_diff.c | 51 +++++++++++++++++++++++++++++++++--- 6 files changed, 84 insertions(+), 4 deletions(-) diff --git a/include/xbt/mmalloc.h b/include/xbt/mmalloc.h index f7a279e6a9..aa6eeaa7d9 100644 --- a/include/xbt/mmalloc.h +++ b/include/xbt/mmalloc.h @@ -18,6 +18,8 @@ # include /* for NULL */ #endif +#include "xbt/dynar.h" + /* Datatype representing a separate heap. The whole point of the mmalloc module * is to allow several such heaps in the process. It thus works by redefining * all the classical memory management functions (malloc and friends) with an @@ -56,7 +58,7 @@ extern xbt_mheap_t mmalloc_get_default_md(void); void mmalloc_set_current_heap(xbt_mheap_t new_heap); xbt_mheap_t mmalloc_get_current_heap(void); -int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2); +int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stacks1, xbt_dynar_t *stacks2); int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2); void mmalloc_backtrace_block_display(void* heapinfo, int block); diff --git a/src/include/mc/datatypes.h b/src/include/mc/datatypes.h index da5a3ca852..dba1759506 100644 --- a/src/include/mc/datatypes.h +++ b/src/include/mc/datatypes.h @@ -21,5 +21,10 @@ typedef struct s_mc_ignore_region{ size_t size; }s_mc_ignore_region_t, *mc_ignore_region_t; +typedef struct s_stack_region{ + void *address; + char *process_name; +}s_stack_region_t, *stack_region_t; + SG_END_DECL() #endif /* _MC_MC_H */ diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index cbc7ce302e..7a7956fa34 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -23,6 +23,7 @@ SG_BEGIN_DECL() extern char*_surf_mc_property_file; /* fixme: better location? */ extern xbt_dynar_t mmalloc_ignore; +extern xbt_dynar_t stacks_areas; /********************************* Global *************************************/ void _mc_cfg_cb_reduce(const char *name, int pos); @@ -42,6 +43,7 @@ void MC_automaton_load(const char *file); void MC_ignore_init(void); XBT_PUBLIC(void) MC_ignore(void *address, size_t size); +void MC_new_stack_area(void *stack, char *name); /********************************* Memory *************************************/ XBT_PUBLIC(void) MC_memory_init(void); /* Initialize the memory subsystem */ diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 9f46c20cd7..ccc32efccb 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -76,6 +76,7 @@ int compare; xbt_dynar_t mc_binary_local_variables = NULL; extern xbt_dynar_t mmalloc_ignore; +extern xbt_dynar_t stacks_areas; xbt_automaton_t _mc_property_automaton = NULL; @@ -651,6 +652,7 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) { void MC_ignore_init(){ MC_SET_RAW_MEM; mmalloc_ignore = xbt_dynar_new(sizeof(mc_ignore_region_t), NULL); + stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL); MC_UNSET_RAW_MEM; } @@ -682,6 +684,16 @@ void MC_ignore(void *address, size_t size){ MC_UNSET_RAW_MEM; } +void MC_new_stack_area(void *stack, char *name){ + MC_SET_RAW_MEM; + stack_region_t region = NULL; + region = xbt_new0(s_stack_region_t, 1); + region->address = stack; + region->process_name = strdup(name); + xbt_dynar_push(stacks_areas, ®ion); + MC_UNSET_RAW_MEM; +} + /************ DWARF ***********/ static e_dw_location_type get_location(char *expr, dw_location_t entry); diff --git a/src/simix/smx_context_base.c b/src/simix/smx_context_base.c index 8fd10e4865..c934a08e4b 100644 --- a/src/simix/smx_context_base.c +++ b/src/simix/smx_context_base.c @@ -10,6 +10,7 @@ #include "xbt/function_types.h" #include "simgrid/simix.h" #include "smx_private.h" +#include "mc/mc.h" XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(bindings); @@ -46,6 +47,16 @@ smx_ctx_base_factory_create_context_sized(size_t size, { smx_context_t context = xbt_malloc0(size); + /* Store the address of the stack in heap to compare it apart of heap comparison */ + if(MC_IS_ENABLED){ + + if(mmalloc_ignore == NULL) + MC_ignore_init(); + + MC_ignore(context, size); + + } + /* If the user provided a function for the process then use it. Otherwise, it is the context for maestro and we should set it as the current context */ @@ -59,6 +70,9 @@ smx_ctx_base_factory_create_context_sized(size_t size, } context->data = data; + if(MC_IS_ENABLED) + MC_new_stack_area(context, ((smx_process_t)context->data)->name); + return context; } diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c index 7b1d98315f..8bc6173235 100644 --- a/src/xbt/mmalloc/mm_diff.c +++ b/src/xbt/mmalloc/mm_diff.c @@ -8,6 +8,7 @@ #include "xbt/ex_interface.h" /* internals of backtrace setup */ #include "xbt/str.h" #include "mc/mc.h" +#include "xbt/mmalloc.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mm_diff, xbt, "Logging specific to mm_diff in mmalloc"); @@ -15,6 +16,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mm_diff, xbt, extern char *xbt_binary_name; xbt_dynar_t mmalloc_ignore; +xbt_dynar_t stacks_areas; typedef struct s_heap_area_pair{ int block1; @@ -34,6 +36,8 @@ static void match_equals(xbt_dynar_t list); static int in_mmalloc_ignore(int block, int fragment); static size_t heap_comparison_ignore(void *address); +static char* is_stack(void *address); + void mmalloc_backtrace_block_display(void* heapinfo, int block){ xbt_ex_t e; @@ -91,7 +95,7 @@ size_t heaplimit, heapsize1, heapsize2; int ignore_done; -int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ +int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stack1, xbt_dynar_t *stack2){ if(heap1 == NULL && heap1 == NULL){ XBT_DEBUG("Malloc descriptors null"); @@ -120,6 +124,8 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ /* Start comparison */ size_t i1, i2, j1, j2, k, current_block, current_fragment; void *addr_block1, *addr_block2, *addr_frag1, *addr_frag2; + void *real_addr_block1, *real_addr_block2; + char *stack_name; xbt_dynar_t previous = xbt_dynar_new(sizeof(heap_area_pair_t), heap_area_pair_free_voidp); @@ -172,6 +178,15 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ addr_block1 = ((void*) (((ADDR2UINT(i1)) - 1) * BLOCKSIZE + (char*)heapbase1)); if(heapinfo1[i1].type == 0){ /* Large block */ + + real_addr_block1 = (char*)((xbt_mheap_t)s_heap)->heapbase + (((char *)addr_block1) - (char *)heapbase1); + + if((stack_name = is_stack(real_addr_block1)) != NULL){ + stack_region_t stack = xbt_new0(s_stack_region_t, 1); + stack->address = addr_block1; + stack->process_name = strdup(stack_name); + xbt_dynar_push(*stack1, &stack); + } if(heapinfo1[i1].busy_block.busy_size == 0){ i1++; @@ -187,7 +202,17 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ if(heapinfo1[current_block].busy_block.busy_size == heapinfo2[current_block].busy_block.busy_size){ addr_block2 = ((void*) (((ADDR2UINT(current_block)) - 1) * BLOCKSIZE + (char*)heapbase2)); + + real_addr_block2 = (char*)((xbt_mheap_t)s_heap)->heapbase + (((char *)addr_block2) - (char *)heapbase2); + if((stack_name = is_stack(real_addr_block2)) != NULL){ + stack_region_t stack = xbt_new0(s_stack_region_t, 1); + stack->address = addr_block2; + stack->process_name = strdup(stack_name); + xbt_dynar_push(*stack2, &stack); + } + + add_heap_area_pair(previous, current_block, -1, current_block, -1); if(ignore_done < xbt_dynar_length(mmalloc_ignore)){ @@ -217,6 +242,17 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ while(i2 <= heaplimit && !equal){ + addr_block2 = ((void*) (((ADDR2UINT(i2)) - 1) * BLOCKSIZE + (char*)heapbase2)); + + real_addr_block2 = (char*)((xbt_mheap_t)s_heap)->heapbase + (((char *)addr_block2) - (char *)heapbase2); + + if((stack_name = is_stack(real_addr_block2)) != NULL){ + stack_region_t stack = xbt_new0(s_stack_region_t, 1); + stack->address = addr_block2; + stack->process_name = strdup(stack_name); + xbt_dynar_push(*stack2, &stack); + } + if(i2 == current_block){ i2++; continue; @@ -242,8 +278,6 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ continue; } - addr_block2 = ((void*) (((ADDR2UINT(i2)) - 1) * BLOCKSIZE + (char*)heapbase2)); - /* Comparison */ add_heap_area_pair(previous, i1, -1, i2, -1); @@ -842,3 +876,14 @@ int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ } +static char * is_stack(void *address){ + unsigned int cursor = 0; + stack_region_t stack; + + xbt_dynar_foreach(stacks_areas, cursor, stack){ + if(address == stack->address) + return stack->process_name; + } + + return NULL; +} -- 2.20.1