From: Gabriel Corona Date: Thu, 2 Jan 2014 12:57:16 +0000 (+0100) Subject: [mc] Add plt/got in mc_object_info_t X-Git-Tag: v3_11~199^2~2^2~35^2~25 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/fc5167a345c9569b12237d14937523d733fb041f [mc] Add plt/got in mc_object_info_t --- diff --git a/examples/msg/mc/bugged1.tesh b/examples/msg/mc/bugged1.tesh index 464633f5a9..bcebdf8c9d 100644 --- a/examples/msg/mc/bugged1.tesh +++ b/examples/msg/mc/bugged1.tesh @@ -5,6 +5,8 @@ $ ${bindir:=.}/bugged1 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" > [ 0.000000] (0:@) Configuration change: Set 'model-check' to '1' > [ 0.000000] (0:@) Check a safety property +> [ 0.000000] (0:@) Get debug information ... +> [ 0.000000] (0:@) Get debug information done ! > [ 0.000000] (2:client@HostB) Sent! > [ 0.000000] (3:client@HostC) Sent! > [ 0.000000] (1:server@HostA) OK diff --git a/examples/msg/mc/bugged2.tesh b/examples/msg/mc/bugged2.tesh index 2fe18e9581..df06aafaaf 100644 --- a/examples/msg/mc/bugged2.tesh +++ b/examples/msg/mc/bugged2.tesh @@ -5,6 +5,8 @@ $ ${bindir:=.}/bugged2 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" > [ 0.000000] (0:@) Configuration change: Set 'model-check' to '1' > [ 0.000000] (0:@) Check a safety property +> [ 0.000000] (0:@) Get debug information ... +> [ 0.000000] (0:@) Get debug information done ! > [ 0.000000] (2:client@HostB) Send 1! > [ 0.000000] (3:client@HostC) Send 2! > [ 0.000000] (1:server@HostA) Received 1 diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index ae0262150f..56209f5571 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -22,6 +22,8 @@ void *start_plt_binary, *end_plt_binary; void *start_got_plt_binary, *end_got_plt_binary; char *libsimgrid_path; +static void MC_get_plt_section(mc_object_info_t info); + /************************************ Free functions **************************************/ /*****************************************************************************************/ @@ -265,10 +267,11 @@ mc_object_info_t MC_find_object_address(memory_map_t maps, char* name) { xbt_assert(result->start_data); xbt_assert(result->start_text); + MC_get_plt_section(result); return result; } -void MC_get_libsimgrid_plt_section(){ +static void MC_get_plt_section(mc_object_info_t info){ FILE *fp; char *line = NULL; /* Temporal storage for each line that is readed */ @@ -279,7 +282,7 @@ void MC_get_libsimgrid_plt_section(){ int i, plt_found = 0; unsigned long int size, offset; - char *command = bprintf("LANG=C objdump --section-headers %s", libsimgrid_path); + char *command = bprintf("LANG=C objdump --section-headers %s", info->file_name); fp = popen(command, "r"); @@ -301,7 +304,7 @@ void MC_get_libsimgrid_plt_section(){ if(lfields[0] == NULL) continue; - if(strcmp(lfields[0], "Sections:") == 0 || strcmp(lfields[0], "Idx") == 0 || strncmp(lfields[0], libsimgrid_path, strlen(libsimgrid_path)) == 0) + if(strcmp(lfields[0], "Sections:") == 0 || strcmp(lfields[0], "Idx") == 0 || strncmp(lfields[0], info->file_name, strlen(info->file_name)) == 0) continue; for (i = 1; i < 7 && lfields[i - 1] != NULL; i++) { @@ -312,14 +315,14 @@ void MC_get_libsimgrid_plt_section(){ if(strcmp(lfields[1], ".plt") == 0){ size = strtoul(lfields[2], NULL, 16); offset = strtoul(lfields[5], NULL, 16); - start_plt_libsimgrid = (char *)start_text_libsimgrid + offset; - end_plt_libsimgrid = (char *)start_plt_libsimgrid + size; + info->start_plt = (char *) info->start_text + offset; + info->end_plt = (char *) info->start_plt + size; plt_found++; }else if(strcmp(lfields[1], ".got.plt") == 0){ size = strtoul(lfields[2], NULL, 16); offset = strtoul(lfields[5], NULL, 16); - start_got_plt_libsimgrid = (char *)start_text_libsimgrid + offset; - end_got_plt_libsimgrid = (char *)start_got_plt_libsimgrid + size; + info->start_got_plt = (char *) info->start_text + offset; + info->end_got_plt = (char *) info->start_plt + size; plt_found++; } @@ -333,69 +336,6 @@ void MC_get_libsimgrid_plt_section(){ } -void MC_get_binary_plt_section(){ - - FILE *fp; - char *line = NULL; /* Temporal storage for each line that is readed */ - ssize_t read; /* Number of bytes readed */ - size_t n = 0; /* Amount of bytes to read by xbt_getline */ - - char *lfields[7]; - int i, plt_found = 0; - unsigned long int size; - - char *command = bprintf("LANG=C objdump --section-headers %s", xbt_binary_name); - - fp = popen(command, "r"); - - if(fp == NULL){ - perror("popen failed"); - xbt_abort(); - } - - while ((read = xbt_getline(&line, &n, fp)) != -1 && plt_found != 2) { - - if(n == 0) - continue; - - /* Wipeout the new line character */ - line[read - 1] = '\0'; - - lfields[0] = strtok(line, " "); - - if(lfields[0] == NULL) - continue; - - if(strcmp(lfields[0], "Sections:") == 0 || strcmp(lfields[0], "Idx") == 0 || strncmp(lfields[0], basename(xbt_binary_name), strlen(xbt_binary_name)) == 0) - continue; - - for (i = 1; i < 7 && lfields[i - 1] != NULL; i++) { - lfields[i] = strtok(NULL, " "); - } - - if(i>=6){ - if(strcmp(lfields[1], ".plt") == 0){ - size = strtoul(lfields[2], NULL, 16); - start_plt_binary = (void *)strtoul(lfields[3], NULL, 16); - end_plt_binary = (char *)start_plt_binary + size; - plt_found++; - }else if(strcmp(lfields[1], ".got.plt") == 0){ - size = strtoul(lfields[2], NULL, 16); - start_got_plt_binary = (char *)strtoul(lfields[3], NULL, 16); - end_got_plt_binary = (char *)start_got_plt_binary + size; - plt_found++; - } - } - - - } - - xbt_free(command); - xbt_free(line); - pclose(fp); - -} - /************************************* Take Snapshot ************************************/ /****************************************************************************************/ diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index e2999d6c0d..8a6b04696f 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -180,6 +180,11 @@ mc_object_info_t MC_new_object_info() { res->file_name = NULL; res->start_text = NULL; res->start_data = NULL; + res->start_bss = NULL; + res->start_plt = NULL; + res->end_plt = NULL; + res->start_got_plt = NULL; + res->end_got_plt = NULL; res->local_variables = xbt_dict_new_homogeneous(NULL); res->global_variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp); res->types = xbt_dict_new_homogeneous(NULL); @@ -1737,19 +1742,8 @@ static void MC_dump_ignored_global_variables(void){ } -void MC_init(){ - - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); - - compare = 0; - - /* Initialize the data structures that must be persistent across every - iteration of the model-checker (in RAW memory) */ - - MC_SET_RAW_MEM; - - MC_init_memory_map_info(); - +static void MC_init_debug_info(); +static void MC_init_debug_info() { XBT_INFO("Get debug information ..."); memory_map_t maps = MC_get_memory_map(); @@ -1762,21 +1756,43 @@ void MC_init(){ mc_libsimgrid_info = MC_find_object_address(maps, libsimgrid_path); MC_dwarf_get_variables(mc_libsimgrid_info); + MC_free_memory_map(maps); + + /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */ + start_plt_libsimgrid = mc_libsimgrid_info->start_plt; + end_plt_libsimgrid = mc_libsimgrid_info->end_plt; + start_plt_binary = mc_binary_info->start_plt; + end_plt_binary = mc_binary_info->end_plt; + start_got_plt_libsimgrid = mc_libsimgrid_info->start_got_plt; + end_got_plt_libsimgrid = mc_libsimgrid_info->end_got_plt; + start_got_plt_binary = mc_binary_info->start_got_plt; + end_got_plt_binary = mc_binary_info->end_got_plt; + + XBT_INFO("Get debug information done !"); +} + +void MC_init(){ + + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + + compare = 0; + + /* Initialize the data structures that must be persistent across every + iteration of the model-checker (in RAW memory) */ + + MC_SET_RAW_MEM; + + MC_init_memory_map_info(); + MC_init_debug_info(); /* Remove variables ignored before getting list of variables */ MC_dump_ignored_local_variables(); MC_dump_ignored_global_variables(); - - /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */ - MC_get_libsimgrid_plt_section(); - MC_get_binary_plt_section(); /* Init parmap */ parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT); - MC_free_memory_map(maps); - MC_UNSET_RAW_MEM; /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */ @@ -1907,8 +1923,7 @@ void MC_modelcheck_safety(void) }else{ MC_SET_RAW_MEM; MC_init_memory_map_info(); - MC_get_libsimgrid_plt_section(); - MC_get_binary_plt_section(); + MC_init(); MC_UNSET_RAW_MEM; } diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index f1e802f7ce..7b04bee1cd 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -218,8 +218,6 @@ typedef struct s_memory_map { void MC_init_memory_map_info(void); memory_map_t MC_get_memory_map(void); void MC_free_memory_map(memory_map_t map); -void MC_get_libsimgrid_plt_section(void); -void MC_get_binary_plt_section(void); extern char *libsimgrid_path; extern void *start_plt_libsimgrid; @@ -330,10 +328,14 @@ typedef struct s_mc_object_info { char* file_name; char* start_text; char* start_data; + char* start_bss; + void* start_plt; + void* end_plt; + void* start_got_plt; + void* end_got_plt; xbt_dict_t local_variables; xbt_dynar_t global_variables; xbt_dict_t types; - // TODO, add start_data, end _data ... } s_mc_object_info_t, *mc_object_info_t; mc_object_info_t MC_new_object_info();