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;
static void MC_assert_pair(int prop);
+static e_dw_location_type get_location(char *expr, dw_location_t entry);
+
+static void MC_get_binary_local_variables(void);
+static void print_local_variables(xbt_dynar_t list);
void MC_do_the_modelcheck_for_real() {
if (!_surf_mc_property_file || _surf_mc_property_file[0]=='\0') {
iteration of the model-checker (in RAW memory) */
MC_SET_RAW_MEM;
-
- mc_binary_local_variables = xbt_dynar_new(sizeof(dw_frame_t), NULL);
+
+ /* Get local variables in binary for state equality detection */
+ MC_get_binary_local_variables();
/* Initialize statistics */
mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
MC_UNSET_RAW_MEM;
- /* Get local variables in binary for state equality detection */
- MC_get_binary_local_variables();
-
MC_ddfs_init();
/* We're done */
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;
}
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);
+static void MC_get_binary_local_variables(){
-void MC_get_binary_local_variables(){
+ mc_binary_local_variables = xbt_dynar_new(sizeof(dw_frame_t), NULL);
- char *command = bprintf("dwarfdump -i %s", xbt_binary_name);
+ char *command = bprintf("dwarfdump -i %s", xbt_binary_name);
FILE* fp = popen(command, "r");
if(fp == NULL)
perror("popen failed");
- char *line = NULL, *tmp_line = NULL, *tmp_location = NULL, *frame_name = NULL;
+ char *line = NULL, *tmp_line = NULL, *tmp_location, *frame_name = NULL;
ssize_t read;
size_t n = 0;
int valid_variable = 1, valid_frame = 1;
- char *node_type = NULL, *location_type = NULL, *variable_name = NULL, *lowpc = NULL, *highpc = NULL;
+ char *node_type, *location_type, *variable_name = NULL, *lowpc, *highpc;
xbt_dynar_t split = NULL;
+ void *low_pc = NULL, *old_low_pc = NULL;
+
+ int compile_unit_found = 0; /* Detect if the program has been compiled with -g */
+
read = getline(&line, &n, fp);
while (read != -1) {
if(line[0] == '<'){
+ /* If the program hasn't been compiled with -g, no symbol (line starting with '<' ) found */
+ compile_unit_found = 1;
+
/* Get node type */
strtok(line, " ");
strtok(NULL, " ");
if(node_type != NULL && strcmp(node_type, "DW_AT_name") == 0){
frame_name = strdup(strtok(NULL, " "));
+ xbt_str_trim(frame_name, NULL);
+ xbt_str_trim(frame_name, "\"");
read = getline(&line, &n, fp);
}else if(node_type != NULL && strcmp(node_type, "DW_AT_frame_base") == 0){
frame->name = strdup(frame_name);
frame->variables = xbt_dynar_new(sizeof(dw_local_variable_t), NULL);
frame->location = xbt_new0(s_dw_location_t, 1);
+ free(frame_name);
location_type = strtok(NULL, " ");
while(read != -1 && line[0] == '['){
strtok(line, "<");
- lowpc = strdup(strtok(NULL, "<"));
- highpc = strdup(strtok(NULL, ">"));
- tmp_location = strdup(strtok(NULL, ">"));
+ lowpc = strtok(NULL, "<");
+ highpc = strtok(NULL, ">");
+ tmp_location = strtok(NULL, ">");
lowpc[strlen(lowpc) - 1] = '\0'; /* Remove last character '>' */
dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
- strtok(lowpc, "=");
- new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
- strtok(highpc, "=");
- new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
+ if(low_pc == NULL){
+ strtok(lowpc, "=");
+ new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
+ strtok(highpc, "=");
+ new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
+ }else{
+ strtok(lowpc, "=");
+ old_low_pc = (void *)strtoul(strtok(NULL, "="), NULL, 16);
+ new_entry->lowpc = (char *)low_pc + (long)old_low_pc;
+ strtok(highpc, "=");
+ new_entry->highpc = (char*)low_pc + ((char *)((void *)strtoul(strtok(NULL, "="), NULL, 16)) - (char*)old_low_pc);
+ }
new_entry->location = xbt_new0(s_dw_location_t, 1);
read = getline(&line, &n, fp);
xbt_str_ltrim(line, NULL);
+
}
}else{
read = getline(&line, &n, fp);
- }
+ }
}
}else if(strcmp(node_type, "DW_TAG_variable") == 0){ /* New variable */
- variable_name = NULL;
- location_type = NULL;
-
read = getline(&line, &n, fp);
while(read != -1 && line[0] != '<'){
if(node_type != NULL && strcmp(node_type, "DW_AT_name") == 0){
variable_name = strdup(strtok(NULL, " "));
+ xbt_str_trim(variable_name, NULL);
+ xbt_str_trim(variable_name, "\"");
read = getline(&line, &n, fp);
}else if(node_type != NULL && strcmp(node_type, "DW_AT_location") == 0){
if(valid_variable == 1){
- location_type = strdup(strtok(NULL, " "));
+ location_type = strtok(NULL, " ");
dw_local_variable_t variable = xbt_new0(s_dw_local_variable_t, 1);
variable->name = strdup(variable_name);
variable->location = xbt_new0(s_dw_location_t, 1);
+ free(variable_name);
if(strcmp(location_type, "<loclist") == 0){
while(read != -1 && line[0] == '['){
strtok(line, "<");
- lowpc = strdup(strtok(NULL, "<"));
- highpc = strdup(strtok(NULL, ">"));
- tmp_location = strdup(strtok(NULL, ">"));
+ lowpc = strtok(NULL, "<");
+ highpc = strtok(NULL, ">");
+ tmp_location = strtok(NULL, ">");
lowpc[strlen(lowpc) - 1] = '\0'; /* Remove last character '>' */
dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
- strtok(lowpc, "=");
- new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
- strtok(highpc, "=");
- new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
+ if(low_pc == NULL){
+ strtok(lowpc, "=");
+ new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
+ strtok(highpc, "=");
+ new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
+ }else{
+ strtok(lowpc, "=");
+ old_low_pc = (void *)strtoul(strtok(NULL, "="), NULL, 16);
+ new_entry->lowpc = (char *)low_pc + (long)old_low_pc;
+ strtok(highpc, "=");
+ new_entry->highpc = (char*)low_pc + ((char *)((void *)strtoul(strtok(NULL, "="), NULL, 16)) - (char*)old_low_pc);
+ }
new_entry->location = xbt_new0(s_dw_location_t, 1);
read = getline(&line, &n, fp);
xbt_str_ltrim(line, NULL);
+
}
}else{
variable->location->type = get_location(location_type, variable->location);
read = getline(&line, &n, fp);
+ xbt_dynar_free(&split);
+ free(location_type);
+
}
xbt_dynar_push(((dw_frame_t)xbt_dynar_get_as(mc_binary_local_variables, xbt_dynar_length(mc_binary_local_variables) - 1, dw_frame_t))->variables, &variable);
read = getline(&line, &n, fp);
}
+
+ //free(tmp_line);
}
valid_variable = 1;
+ }else if(strcmp(node_type, "DW_TAG_compile_unit") == 0){
+
+ read = getline(&line, &n, fp);
+
+ while(read != -1 && line[0] != '<'){
+
+ if(n == 0)
+ continue;
+
+ node_type = strtok(line, " ");
+
+ if(node_type != NULL && strcmp(node_type, "DW_AT_low_pc") == 0){
+ low_pc = (void *) strtoul(strtok(NULL, " "), NULL, 16);
+ }
+
+ read = getline(&line, &n, fp);
+
+ }
+
}else{
read = getline(&line, &n, fp);
}
+
}else{
read = getline(&line, &n, fp);
}
+
}
+ free(line);
+ free(command);
+ pclose(fp);
+
+ if(compile_unit_found == 0){
+ XBT_INFO("Your program must be compiled with -g");
+ xbt_abort();
+ }
+
if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug))
print_local_variables(mc_binary_local_variables);
- free(line); free(tmp_line); free(tmp_location); free(frame_name);
- free(node_type); free(location_type); free(variable_name); free(lowpc); free(highpc);
- free(command);
- pclose(fp);
+
}
void print_local_variables(xbt_dynar_t list){
}
- free(tok);
- free(tmp_tok);
- /*xbt_dynar_free(&tokens);*/
+ xbt_dynar_free(&tokens);
return e_dw_compose;
entry->type = e_dw_unsupported;
}
- free(tok);
- free(tmp_tok);
+ xbt_dynar_free(&tokens);
return entry->type;
