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 **************************************/
/*****************************************************************************************/
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 */
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");
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++) {
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++;
}
}
-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 ************************************/
/****************************************************************************************/
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);
}
-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();
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 */
}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;
}
