From a27b7cd435294d62935a32330fa83608aa4974d9 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 20 Nov 2012 16:41:55 +0100 Subject: [PATCH] model-checker : ignore coverage variables --- src/mc/mc_compare.c | 17 +++++++++-- src/mc/mc_global.c | 72 +++++++++++++++++++++++++++++++++++++++++++-- src/mc/mc_private.h | 16 ++++++---- 3 files changed, 95 insertions(+), 10 deletions(-) diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 116e5db6c5..15040a91b2 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -56,8 +56,12 @@ static size_t data_bss_ignore_size(void *address){ var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t); if(var->address == address) return var->size; - if(var->address < address) - start = cursor + 1; + if(var->address < address){ + if((void *)((char *)var->address + var->size) > address) + return (char *)var->address + var->size - (char*)address; + else + start = cursor + 1; + } if(var->address > address) end = cursor - 1; } @@ -67,12 +71,19 @@ static size_t data_bss_ignore_size(void *address){ static int data_bss_program_region_compare(void *d1, void *d2, size_t size){ - size_t i = 0; + size_t i = 0, ignore_size = 0; int pointer_align; void *addr_pointed1 = NULL, *addr_pointed2 = NULL; for(i=0; i 0){ + i = i + ignore_size; + continue; + }else if((ignore_size = data_bss_ignore_size((char *)start_bss_binary+i)) > 0){ + i = i + ignore_size; + continue; + } pointer_align = (i / sizeof(void*)) * sizeof(void*); addr_pointed1 = *((void **)((char *)d1 + pointer_align)); addr_pointed2 = *((void **)((char *)d2 + pointer_align)); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index edc9339637..4dfb227d16 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -115,6 +115,7 @@ xbt_automaton_t _mc_property_automaton = NULL; static void MC_assert_pair(int prop); static dw_location_t get_location(xbt_dict_t location_list, char *expr); static dw_frame_t get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset); +static void ignore_coverage_variables(char *executable, int region_type); void MC_do_the_modelcheck_for_real() { if (!_surf_mc_property_file || _surf_mc_property_file[0]=='\0') { @@ -170,14 +171,17 @@ void MC_init(){ xbt_dict_t libsimgrid_location_list = MC_get_location_list(ls_path); MC_get_local_variables(ls_path, libsimgrid_location_list, &mc_local_variables); - MC_UNSET_RAW_MEM; - MC_init_memory_map_info(); /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */ get_libsimgrid_plt_section(); get_binary_plt_section(); + ignore_coverage_variables(libsimgrid_path, 1); + ignore_coverage_variables(xbt_binary_name, 2); + + MC_UNSET_RAW_MEM; + /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */ MC_ignore_stack("e", "*"); MC_ignore_stack("__ex_cleanup", "*"); @@ -719,6 +723,70 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) { /************ MC_ignore ***********/ +static void ignore_coverage_variables(char *executable, int region_type){ + + FILE *fp; + + char *command = bprintf("objdump --syms %s", executable); + + fp = popen(command, "r"); + + if(fp == NULL){ + perror("popen failed"); + xbt_abort(); + } + + char *line = NULL; + ssize_t read; + size_t n = 0; + + xbt_dynar_t line_tokens = NULL; + unsigned long int size, offset; + void *address; + + while ((read = getline(&line, &n, fp)) != -1){ + + if(n == 0) + continue; + + /* Wipeout the new line character */ + line[read - 1] = '\0'; + + xbt_str_strip_spaces(line); + xbt_str_ltrim(line, NULL); + + line_tokens = xbt_str_split(line, NULL); + + if(xbt_dynar_length(line_tokens) < 3 || strcmp(xbt_dynar_get_as(line_tokens, 0, char *), "SYMBOL") == 0) + continue; + + if(((strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char *), "gcov", 4) == 0) + || (strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char *), "__gcov", 6) == 0)) + && (((strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 3, char *), ".bss") == 0) + || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 3, char *), ".data") == 0)))){ + if(region_type == 1){ /* libsimgrid */ + offset = strtoul(xbt_dynar_get_as(line_tokens, 0, char*), NULL, 16); + size = strtoul(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 2, char *), NULL, 16); + //XBT_DEBUG("Add ignore at address %p (size %lu)", (char *)start_text_libsimgrid+offset, size); + MC_ignore_data_bss((char *)start_text_libsimgrid+offset, size); + }else{ /* binary */ + address = (void *)strtoul(xbt_dynar_get_as(line_tokens, 0, char*), NULL, 16); + size = strtoul(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 2, char *), NULL, 16); + //XBT_DEBUG("Add ignore at address %p (size %lu)", address, size); + MC_ignore_data_bss(address, size); + } + } + + xbt_dynar_free(&line_tokens); + + } + + free(command); + free(line); + pclose(fp); + +} + void MC_ignore_heap(void *address, size_t size){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 92f7d93c8b..cc11df95ea 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -194,6 +194,16 @@ void get_binary_plt_section(void); extern void *start_data_libsimgrid; extern void *end_raw_heap; +extern void *start_data_binary; +extern void *start_bss_binary; +extern char *libsimgrid_path; +extern void *start_text_libsimgrid; +extern void *start_bss_libsimgrid; +extern void *start_plt_libsimgrid; +extern void *end_plt_libsimgrid; +extern void *start_plt_binary; +extern void *end_plt_binary; + /********************************** DPOR for safety **************************************/ typedef enum { @@ -217,13 +227,9 @@ extern xbt_fifo_t mc_stack_liveness; extern mc_global_t initial_state_liveness; extern xbt_automaton_t _mc_property_automaton; extern int compare; -extern void *start_plt_libsimgrid; -extern void *end_plt_libsimgrid; -extern void *start_plt_binary; -extern void *end_plt_binary; extern xbt_dynar_t mc_stack_comparison_ignore; extern xbt_dynar_t mc_data_bss_comparison_ignore; -extern void *start_bss_libsimgrid; + typedef struct s_mc_pair{ mc_snapshot_t system_state; -- 2.20.1