-/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved. */
+/* Copyright (c) 2008-2013. The SimGrid Team.
+ * All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
#include <sys/types.h>
#include <sys/wait.h>
#include <sys/time.h>
+#include <libgen.h>
#include "simgrid/sg_config.h"
#include "../surf/surf_private.h"
int user_max_depth_reached = 0;
-extern int _sg_init_status;
void _mc_cfg_cb_reduce(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
char *val= xbt_cfg_get_string(_sg_cfg_set, name);
}
void _mc_cfg_cb_checkpoint(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
}
void _mc_cfg_cb_property(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_property_file= xbt_cfg_get_string(_sg_cfg_set, name);
}
void _mc_cfg_cb_timeout(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name);
}
void _mc_cfg_cb_max_depth(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_max_depth= xbt_cfg_get_int(_sg_cfg_set, name);
}
void _mc_cfg_cb_visited(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
}
void _mc_cfg_cb_dot_output(const char *name, int pos) {
- if (_sg_init_status && !_sg_do_model_check) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
mc_state_t mc_current_state = NULL;
char mc_replay_mode = FALSE;
double *mc_time = NULL;
-mc_comparison_times_t mc_comp_times = NULL;
-double mc_snapshot_comparison_time;
+__thread mc_comparison_times_t mc_comp_times = NULL;
+__thread double mc_snapshot_comparison_time;
mc_stats_t mc_stats = NULL;
/* Safety */
xbt_automaton_t _mc_property_automaton = NULL;
/* Variables */
-xbt_dict_t mc_local_variables_libsimgrid = NULL;
-xbt_dict_t mc_local_variables_binary = NULL;
-xbt_dynar_t mc_global_variables_libsimgrid = NULL;
-xbt_dynar_t mc_global_variables_binary = NULL;
-xbt_dict_t mc_variables_type_libsimgrid = NULL;
-xbt_dict_t mc_variables_type_binary = NULL;
+mc_object_info_t mc_libsimgrid_info = NULL;
+mc_object_info_t mc_binary_info = NULL;
/* Ignore mechanism */
xbt_dynar_t mc_stack_comparison_ignore;
dw_variable_free((dw_variable_t) * (void **) t);
}
+// object_info
+
+mc_object_info_t MC_new_object_info() {
+ mc_object_info_t res = xbt_new(s_mc_object_info_t, 1);
+ 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);
+ return res;
+}
+
+void MC_free_object_info(mc_object_info_t* info) {
+ xbt_free(&(*info)->file_name);
+ xbt_dict_free(&(*info)->local_variables);
+ xbt_dynar_free(&(*info)->global_variables);
+ xbt_dict_free(&(*info)->types);
+ xbt_free(info);
+ info = NULL;
+}
+
/*************************************************************************/
static dw_location_t MC_dwarf_get_location(xbt_dict_t location_list, char *expr){
}
+/** @brief Extract the location lists from an ELF file (.debug_loc)
+ *
+ * @return A map from the offset in the list (in hexadecimal string)
+ * into a location list (dynar of dw_location_entry_t).
+ */
static xbt_dict_t MC_dwarf_get_location_list(const char *elf_file){
- char *command = bprintf("objdump -Wo %s", elf_file);
+ char *command = bprintf("LANG=C objdump -Wo %s", elf_file);
FILE *fp = popen(command, "r");
xbt_str_strip_spaces(line);
split = xbt_str_split(line, " ");
+ char *key = NULL;
while(read != -1 && strcmp("<End", (char *)xbt_dynar_get_as(split, 1, char *)) != 0){
+ // Take the key from the first line of the list:
+ if(key==NULL){
+ key = bprintf("%d", (int)strtoul((char *)xbt_dynar_get_as(split, 0, char *), NULL, 16));
+ }
+
dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
new_entry->lowpc = strtoul((char *)xbt_dynar_get_as(split, 1, char *), NULL, 16);
new_entry->highpc = strtoul((char *)xbt_dynar_get_as(split, 2, char *), NULL, 16);
}
- char *key = bprintf("%d", (int)strtoul((char *)xbt_dynar_get_as(split, 0, char *), NULL, 16));
xbt_dict_set(location_list, key, loclist, NULL);
xbt_free(key);
}
+static void MC_dwarf_get_variables(mc_object_info_t info){
+ mc_object_info_t result = info;
+ const char *elf_file = info->file_name;
-static void MC_dwarf_get_variables(const char *elf_file, xbt_dict_t location_list, xbt_dict_t *local_variables, xbt_dynar_t *global_variables, xbt_dict_t *types){
+ xbt_dict_t location_list = MC_dwarf_get_location_list(elf_file);
- char *command = bprintf("objdump -Wi %s", elf_file);
+ char *command = bprintf("LANG=C objdump -Wi %s", elf_file);
FILE *fp = popen(command, "r");
if(fp == NULL)
perror("popen for objdump failed");
+ xbt_dict_t *local_variables = &result->local_variables;
+ xbt_dynar_t *global_variables = &result->global_variables;
+ xbt_dict_t *types = &result->types;
+
char *line = NULL, *origin, *abstract_origin, *current_frame = NULL,
*subprogram_name = NULL, *subprogram_start = NULL, *subprogram_end = NULL,
*node_type = NULL, *location_type = NULL, *variable_name = NULL,
node_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
if(strcmp(node_type, "(DW_TAG_subprogram)") == 0){ /* New frame */
+ /* We build/complete a dw_frame_t object
+ * and append it if necessary to the local_variables dictionnary */
dw_frame_t frame = NULL;
}else if(strcmp(node_type, "(DW_TAG_variable)") == 0){ /* New variable */
+ /* We build a dw_variable_t object and append it either to
+ the list of variables of the frame (local variable)
+ or to the list of global variables (global variables). */
dw_variable_t var = NULL;
xbt_dynar_free(&split2);
split2 = xbt_str_split(loc_expr, " ");
if(strcmp(elf_file, xbt_binary_name) != 0)
- var->address.address = (char *)start_text_libsimgrid + (long)((void *)strtoul(xbt_dynar_get_as(split2, xbt_dynar_length(split2) - 1, char*), NULL, 16));
+ var->address.address = (char *) info->start_text + (long)((void *)strtoul(xbt_dynar_get_as(split2, xbt_dynar_length(split2) - 1, char*), NULL, 16));
else
+ // Why is it different ?
var->address.address = (void *)strtoul(xbt_dynar_get_as(split2, xbt_dynar_length(split2) - 1, char*), NULL, 16);
}else{
var->address.location = MC_dwarf_get_location(NULL, loc_expr);
global_address = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
xbt_str_rtrim(global_address, ")");
if(strcmp(elf_file, xbt_binary_name) != 0)
- var->address.address = (char *)start_text_libsimgrid + (long)((void *)strtoul(global_address, NULL, 16));
+ var->address.address = (char *) info->start_text + (long)((void *)strtoul(global_address, NULL, 16));
else
+ // Why is it different ?
var->address.address = (void *)strtoul(global_address, NULL, 16);
xbt_free(global_address);
global_address = NULL;
new_variable = 1;
}else if(strcmp(node_type, "(DW_TAG_inlined_subroutine)") == 0){
+ /* Update the information on the frame (we should duplicate it instead). */
read = xbt_getline(&line, &n, fp);
|| strcmp(node_type, "(DW_TAG_volatile_type)") == 0
|| (is_pointer = !strcmp(node_type, "(DW_TAG_pointer_type)"))){
+ /* Create the and add it to the types dictionnary */
+
if(strcmp(node_type, "(DW_TAG_base_type)") == 0)
type_type = e_dw_base_type;
else if(strcmp(node_type, "(DW_TAG_enumeration_type)") == 0)
xbt_dict_free(&subprograms_origin);
xbt_free(line);
xbt_free(command);
+ xbt_dict_free(&location_list);
+
pclose(fp);
-
}
else
xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion);
- MC_UNSET_RAW_MEM;
-
- if(raw_mem_set)
- MC_SET_RAW_MEM;
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
}
void MC_remove_ignore_heap(void *address, size_t size){
MC_remove_ignore_heap(address, size);
}
- MC_UNSET_RAW_MEM;
-
- if(raw_mem_set)
- MC_SET_RAW_MEM;
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
}
MC_SET_RAW_MEM;
- if(mc_global_variables_libsimgrid){
+ if(mc_libsimgrid_info){
unsigned int cursor = 0;
dw_variable_t current_var;
int start = 0;
- int end = xbt_dynar_length(mc_global_variables_libsimgrid) - 1;
+ int end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
while(start <= end){
cursor = (start + end) /2;
- current_var = (dw_variable_t)xbt_dynar_get_as(mc_global_variables_libsimgrid, cursor, dw_variable_t);
+ current_var = (dw_variable_t)xbt_dynar_get_as(mc_libsimgrid_info->global_variables, cursor, dw_variable_t);
if(strcmp(current_var->name, name) == 0){
- xbt_dynar_remove_at(mc_global_variables_libsimgrid, cursor, NULL);
+ xbt_dynar_remove_at(mc_libsimgrid_info->global_variables, cursor, NULL);
start = 0;
- end = xbt_dynar_length(mc_global_variables_libsimgrid) - 1;
+ end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
}else if(strcmp(current_var->name, name) < 0){
start = cursor + 1;
}else{
}
}
- MC_UNSET_RAW_MEM;
-
- if(raw_mem_set)
- MC_SET_RAW_MEM;
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
}
void MC_ignore_local_variable(const char *var_name, const char *frame_name){
MC_SET_RAW_MEM;
- if(mc_local_variables_libsimgrid){
+ if(mc_libsimgrid_info){
unsigned int cursor = 0;
dw_variable_t current_var;
int start, end;
xbt_dict_cursor_t dict_cursor;
char *current_frame_name;
dw_frame_t frame;
- xbt_dict_foreach(mc_local_variables_libsimgrid, dict_cursor, current_frame_name, frame){
+ xbt_dict_foreach(mc_libsimgrid_info->local_variables, dict_cursor, current_frame_name, frame){
+ start = 0;
+ end = xbt_dynar_length(frame->variables) - 1;
+ while(start <= end){
+ cursor = (start + end) / 2;
+ current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
+ if(strcmp(current_var->name, var_name) == 0){
+ xbt_dynar_remove_at(frame->variables, cursor, NULL);
+ start = 0;
+ end = xbt_dynar_length(frame->variables) - 1;
+ }else if(strcmp(current_var->name, var_name) < 0){
+ start = cursor + 1;
+ }else{
+ end = cursor - 1;
+ }
+ }
+ }
+ xbt_dict_foreach(mc_binary_info->local_variables, dict_cursor, current_frame_name, frame){
start = 0;
end = xbt_dynar_length(frame->variables) - 1;
while(start <= end){
}
}
}else{
- xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(mc_local_variables_libsimgrid, frame_name))->variables;
+ xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(
+ mc_libsimgrid_info->local_variables, frame_name))->variables;
start = 0;
end = xbt_dynar_length(variables_list) - 1;
while(start <= end){
}
}
- MC_UNSET_RAW_MEM;
-
- if(raw_mem_set)
- MC_SET_RAW_MEM;
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
}
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
MC_SET_RAW_MEM;
+
if(stacks_areas == NULL)
stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
region->size = size;
region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
xbt_dynar_push(stacks_areas, ®ion);
-
- MC_UNSET_RAW_MEM;
- if(raw_mem_set)
- MC_SET_RAW_MEM;
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
}
void MC_ignore(void *addr, size_t size){
unsigned int cursor = 0;
int start = 0;
int end = xbt_dynar_length(mc_checkpoint_ignore) -1;
- mc_checkpoint_ignore_region_t current_region;
+ mc_checkpoint_ignore_region_t current_region = NULL;
while(start <= end){
cursor = (start + end) / 2;
}
+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();
+
+ /* Get local variables for state equality detection */
+
+ mc_binary_info = MC_find_object_address(maps, xbt_binary_name);
+ MC_dwarf_get_variables(mc_binary_info);
+
+ mc_libsimgrid_info = MC_find_object_address(maps, libsimgrid_path);
+ MC_dwarf_get_variables(mc_libsimgrid_info);
+
+ MC_free_memory_map(maps);
+
+ 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
MC_SET_RAW_MEM;
MC_init_memory_map_info();
-
- mc_local_variables_libsimgrid = xbt_dict_new_homogeneous(NULL);
- mc_local_variables_binary = xbt_dict_new_homogeneous(NULL);
- mc_global_variables_libsimgrid = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
- mc_global_variables_binary = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
- mc_variables_type_libsimgrid = xbt_dict_new_homogeneous(NULL);
- mc_variables_type_binary = xbt_dict_new_homogeneous(NULL);
-
- XBT_INFO("Get debug information ...");
-
- /* Get local variables in binary for state equality detection */
- xbt_dict_t binary_location_list = MC_dwarf_get_location_list(xbt_binary_name);
- MC_dwarf_get_variables(xbt_binary_name, binary_location_list, &mc_local_variables_binary, &mc_global_variables_binary, &mc_variables_type_binary);
-
- /* Get local variables in libsimgrid for state equality detection */
- xbt_dict_t libsimgrid_location_list = MC_dwarf_get_location_list(libsimgrid_path);
- MC_dwarf_get_variables(libsimgrid_path, libsimgrid_location_list, &mc_local_variables_libsimgrid, &mc_global_variables_libsimgrid, &mc_variables_type_libsimgrid);
-
- xbt_dict_free(&libsimgrid_location_list);
- xbt_dict_free(&binary_location_list);
-
- XBT_INFO("Get debug information done !");
+ 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_UNSET_RAW_MEM;
MC_ignore_global_variable("mc_snapshot_comparison_time");
MC_ignore_global_variable("mc_time");
MC_ignore_global_variable("smpi_current_rank");
- MC_ignore_global_variable("smx_current_context_serial");
- MC_ignore_global_variable("smx_current_context_key");
- MC_ignore_global_variable("sysv_maestro_context");
MC_ignore_global_variable("counter"); /* Static variable used for tracing */
+ MC_ignore_global_variable("maestro_stack_start");
+ MC_ignore_global_variable("maestro_stack_end");
+
+ MC_ignore_heap(&(simix_global->process_to_run), sizeof(simix_global->process_to_run));
+ MC_ignore_heap(&(simix_global->process_that_ran), sizeof(simix_global->process_that_ran));
+ MC_ignore_heap(simix_global->process_to_run, sizeof(*(simix_global->process_to_run)));
+ MC_ignore_heap(simix_global->process_that_ran, sizeof(*(simix_global->process_that_ran)));
+
+ smx_process_t process;
+ xbt_swag_foreach(process, simix_global->process_list){
+ MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
+ }
if(raw_mem_set)
MC_SET_RAW_MEM;
}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;
}
MC_SET_RAW_MEM;
/* Save the initial state */
initial_state_safety = xbt_new0(s_mc_global_t, 1);
- initial_state_safety->snapshot = MC_take_snapshot();
+ initial_state_safety->snapshot = MC_take_snapshot(0);
MC_UNSET_RAW_MEM;
MC_dpor();
