int _sg_mc_timeout=0;
int _sg_mc_max_depth=1000;
int _sg_mc_visited=0;
+char *_sg_mc_dot_output_file = NULL;
extern int _sg_init_status;
void _mc_cfg_cb_reduce(const char *name, int pos) {
_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) {
+ 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 global data structures */
extern xbt_dynar_t mc_heap_comparison_ignore;
extern xbt_dynar_t stacks_areas;
+FILE *dot_output = NULL;
+const char* colors[10];
+
xbt_automaton_t _mc_property_automaton = NULL;
/* Static functions */
MC_SET_RAW_MEM;
mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
MC_UNSET_RAW_MEM;
+
+ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
+ MC_init_dot_output();
if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
if (mc_reduce_kind==e_mc_reduce_unset)
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
- mc_time = xbt_new0(double, simix_process_maxpid);
-
- /* mc_time refers to clock for each process -> ignore it for heap comparison */
- int i;
- for(i = 0; i<simix_process_maxpid; i++)
- MC_ignore_heap(&(mc_time[i]), sizeof(double));
-
compare = 0;
/* Initialize the data structures that must be persistent across every
get_libsimgrid_plt_section();
get_binary_plt_section();
- MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times));
- MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time));
-
/* Get global variables */
MC_get_global_variables(xbt_binary_name);
MC_get_global_variables(libsimgrid_path);
MC_ignore_stack("next_context", "smx_ctx_sysv_suspend_serial");
MC_ignore_stack("i", "smx_ctx_sysv_suspend_serial");
+ MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times));
+ MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time));
+ MC_ignore_data_bss(&mc_time, sizeof(mc_time));
+
if(raw_mem_set)
MC_SET_RAW_MEM;
}
+void MC_init_dot_output(){
+
+ colors[0] = "blue";
+ colors[1] = "red";
+ colors[2] = "green";
+ colors[3] = "pink";
+ colors[4] = "brown";
+ colors[5] = "purple";
+ colors[6] = "yellow";
+ colors[7] = "orange";
+
+ dot_output = fopen(_sg_mc_dot_output_file, "w");
+
+ if(dot_output == NULL){
+ perror("Error open dot output file");
+ xbt_abort();
+ }
+
+ fprintf(dot_output, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.20; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
+
+}
+
void MC_modelcheck_safety(void)
{
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
mc_time = xbt_new0(double, simix_process_maxpid);
+ /* mc_time refers to clock for each process -> ignore it for heap comparison */
+ MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
+
/* Initialize the data structures that must be persistent across every
iteration of the model-checker (in RAW memory) */
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
MC_init();
+
+ mc_time = xbt_new0(double, simix_process_maxpid);
+
+ /* mc_time refers to clock for each process -> ignore it for heap comparison */
+ MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
MC_SET_RAW_MEM;
void MC_exit(void)
{
+ MC_SET_RAW_MEM;
+ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
+ fprintf(dot_output, "}\n");
+ fclose(dot_output);
+ }
+ MC_UNSET_RAW_MEM;
+
xbt_free(mc_time);
MC_memory_exit();
xbt_abort();
}
+int SIMIX_pre_mc_random(smx_simcall_t simcall){
+
+ return simcall->mc_value;
+}
+
-int MC_random(int min, int max)
+int MC_random(void)
{
/*FIXME: return mc_current_state->executed_transition->random.value;*/
- return 0;
+ return simcall_mc_random();
}
/**
/************ MC_ignore ***********/
void heap_ignore_region_free(mc_heap_ignore_region_t r){
- if(r)
- xbt_free(r);
+ xbt_free(r);
}
void heap_ignore_region_free_voidp(void *r){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
MC_SET_RAW_MEM;
-
- if(mc_heap_comparison_ignore == NULL)
- mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp);
mc_heap_ignore_region_t region = NULL;
region = xbt_new0(s_mc_heap_ignore_region_t, 1);
region->address = address;
region->size = size;
-
+
region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment] = 1;
}
+
+ if(mc_heap_comparison_ignore == NULL){
+ mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp);
+ xbt_dynar_push(mc_heap_comparison_ignore, ®ion);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
+ return;
+ }
unsigned int cursor = 0;
mc_heap_ignore_region_t current_region;
- xbt_dynar_foreach(mc_heap_comparison_ignore, cursor, current_region){
+ int start = 0;
+ int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
+
+ while(start <= end){
+ cursor = (start + end) / 2;
+ current_region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
+ if(current_region->address == address){
+ heap_ignore_region_free(region);
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
+ return;
+ }
+ if(current_region->address < address)
+ start = cursor + 1;
if(current_region->address > address)
- break;
+ end = cursor - 1;
}
- xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion);
+ if(current_region->address < address)
+ xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, ®ion);
+ else
+ xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion);
MC_UNSET_RAW_MEM;
if(mc_data_bss_comparison_ignore == NULL)
mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), NULL);
- if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
+ mc_data_bss_ignore_variable_t var = NULL;
+ var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
+ var->address = address;
+ var->size = size;
- mc_data_bss_ignore_variable_t var = NULL;
- var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
- var->address = address;
- var->size = size;
+ if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var);
if(current_var->address > address)
end = cursor - 1;
}
-
- mc_data_bss_ignore_variable_t var = NULL;
- var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
- var->address = address;
- var->size = size;
if(current_var->address < address)
xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
}
+ /* Remove variable from mc_global_variables */
+
+ if(mc_global_variables != NULL){
+
+ unsigned int cursor = 0;
+ int start = 0;
+ int end = xbt_dynar_length(mc_global_variables) - 1;
+ global_variable_t current_var;
+ int var_found;
+
+ while(start <= end){
+ cursor = (start + end) / 2;
+ current_var = (global_variable_t)xbt_dynar_get_as(mc_global_variables, cursor, global_variable_t);
+ if(current_var->address == var->address){
+ var_found = 1;
+ break;
+ }
+ if(current_var->address < address)
+ start = cursor + 1;
+ if(current_var->address > address)
+ end = cursor - 1;
+ }
+
+ if(var_found)
+ xbt_dynar_remove_at(mc_global_variables, cursor, NULL);
+
+ }
+
MC_UNSET_RAW_MEM;
if(raw_mem_set)
-void MC_ignore_stack(const char *var_name, const char *frame){
+void MC_ignore_stack(const char *var_name, const char *frame_name){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
mc_stack_ignore_variable_t var = NULL;
var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
var->var_name = strdup(var_name);
- var->frame = strdup(frame);
+ var->frame = strdup(frame_name);
xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
while(start <= end){
cursor = (start + end) / 2;
current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
- if(strcmp(current_var->frame, frame) == 0){
+ if(strcmp(current_var->frame, frame_name) == 0){
if(strcmp(current_var->var_name, var_name) == 0){
MC_UNSET_RAW_MEM;
if(raw_mem_set)
if(strcmp(current_var->var_name, var_name) > 0)
end = cursor - 1;
}
- if(strcmp(current_var->frame, frame) < 0)
+ if(strcmp(current_var->frame, frame_name) < 0)
start = cursor + 1;
- if(strcmp(current_var->frame, frame) > 0)
+ if(strcmp(current_var->frame, frame_name) > 0)
end = cursor - 1;
}
mc_stack_ignore_variable_t var = NULL;
var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
var->var_name = strdup(var_name);
- var->frame = strdup(frame);
+ var->frame = strdup(frame_name);
- if(strcmp(current_var->frame, frame) < 0)
+ if(strcmp(current_var->frame, frame_name) < 0)
xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
else
xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
}
+ /* Remove variable from mc_local_variables */
+
+ if(mc_local_variables != NULL){
+
+ if(strcmp(frame_name, "*") != 0){
+ dw_frame_t frame = xbt_dict_get_or_null(mc_local_variables, frame_name);
+ if(frame != NULL)
+ xbt_dict_remove(frame->variables, var_name);
+ }
+
+ }
+
MC_UNSET_RAW_MEM;
if(raw_mem_set)
int cursor_remove;
xbt_dynar_t split = NULL;
- while ((read = getline(&line, &n, fp)) != -1) {
+ while ((read = xbt_getline(&line, &n, fp)) != -1) {
/* Wipeout the new line character */
line[read - 1] = '\0';
xbt_dynar_free(&split);
free(loc_expr);
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
if(read != -1){
line[read - 1] = '\0';
xbt_str_strip_spaces(line);
int new_frame = 0, new_variable = 0;
dw_frame_t variable_frame, subroutine_frame = NULL;
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
while (read != -1) {
if(n == 0){
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
continue;
}
line[read - 1] = '\0';
if(strlen(line) == 0){
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
continue;
}
xbt_str_strip_spaces(line);
if(line[0] != '<'){
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
continue;
}
subprogram_start = strdup(strtok(NULL, "<"));
xbt_str_rtrim(subprogram_start, ">:");
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
while(read != -1){
if(n == 0){
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
continue;
}
line[read - 1] = '\0';
if(strlen(line) == 0){
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
continue;
}
}
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
}
}
xbt_free(subprogram_start);
- if(subprogram_end != NULL){
- xbt_free(subprogram_end);
- subprogram_end = NULL;
- }
+ xbt_free(subprogram_end);
+ subprogram_end = NULL;
}else if(strcmp(node_type, "(DW_TAG_variable)") == 0){ /* New variable */
origin = strdup(strtok(NULL, "<"));
xbt_str_rtrim(origin, ">:");
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
while(read != -1){
if(n == 0){
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
continue;
}
line[read - 1] = '\0';
if(strlen(line) == 0){
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
continue;
}
}
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
}
origin = strdup(strtok(NULL, "<"));
xbt_str_rtrim(origin, ">:");
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
while(read != -1){
line[read - 1] = '\0';
if(n == 0){
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
continue;
}
if(strlen(line) == 0){
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
continue;
}
subroutine_frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
}
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
}
}else{
- read = getline(&line, &n, fp);
+ read = xbt_getline(&line, &n, fp);
}
int type = strcmp(elf_file, xbt_binary_name); /* 0 = binary, other = libsimgrid */
- while ((read = getline(&line, &n, fp)) != -1){
+ while ((read = xbt_getline(&line, &n, fp)) != -1){
if(n == 0)
continue;
|| (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), ".data") == 0)
|| (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), ".bss") == 0)
|| (strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "stderr", 6) == 0)
- || (strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "counter", 7) == 0)
- || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heapinfo1") == 0)
- || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heapinfo2") == 0)
- || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heapbase1") == 0)
- || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heapbase2") == 0)
- || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heapsize1") == 0)
- || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heapsize2") == 0)
- || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heaplimit") == 0)
- || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "ignore_done") == 0)
- || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "s_heap") == 0)
- || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "to_ignore1") == 0)
- || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "to_ignore2") == 0)
|| ((size_t)strtoul(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 2, char*), NULL, 16) == 0))
continue;
var->size = (size_t)strtoul(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 2, char*), NULL, 16);
var->name = strdup(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*));
- if(data_bss_ignore_size(var->address) > 0)
+ if(data_bss_ignore_size(var->address) > 0){
global_variable_free(var);
- else
- xbt_dynar_push(mc_global_variables, &var);
+ }else{
+ if(xbt_dynar_is_empty(mc_global_variables)){
+ xbt_dynar_push(mc_global_variables, &var);
+ }else{
+ unsigned int cursor = 0;
+ int start = 0;
+ int end = xbt_dynar_length(mc_global_variables) - 1;
+ global_variable_t current_var = NULL;
+
+ while(start <= end){
+ cursor = (start + end) / 2;
+ current_var = (global_variable_t)xbt_dynar_get_as(mc_global_variables, cursor, global_variable_t);
+ if(current_var->address == var->address)
+ break;
+ if(current_var->address < var->address)
+ start = cursor + 1;
+ if(current_var->address > var->address)
+ end = cursor - 1;
+ }
+
+ if(current_var->address < var->address)
+ xbt_dynar_insert_at(mc_global_variables, cursor + 1, &var);
+ else
+ xbt_dynar_insert_at(mc_global_variables, cursor, &var);
+ }
+ }
xbt_dynar_free(&line_tokens);
