model-checker : fix dynar index in algorithm to get local variable location

[simgrid.git] / src / mc / mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 8bb0aa6..2dd304f 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -73,7 +73,7 @@ mc_stats_t mc_stats = NULL;
 
 mc_stats_pair_t mc_stats_pair = NULL;
 xbt_fifo_t mc_stack_liveness = NULL;
-mc_snapshot_t initial_snapshot_liveness = NULL;
+mc_global_t initial_state_liveness = NULL;
 int compare;
 
 /* Local */
@@ -146,11 +146,8 @@ void MC_init_safety(void)
   MC_take_snapshot(initial_snapshot);
   MC_UNSET_RAW_MEM;
 
-
   if(raw_mem_set)
     MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
   
 }
 
@@ -166,12 +163,9 @@ void MC_modelcheck(void)
   MC_exit();
 }
 
-void MC_modelcheck_liveness(){
+void MC_init_liveness(){
 
   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
-  /* init stuff */
-  XBT_INFO("Start init mc");
   
   mc_time = xbt_new0(double, simix_process_maxpid);
 
@@ -198,6 +192,27 @@ void MC_modelcheck_liveness(){
   /* Get local variables in libsimgrid for state equality detection */
   xbt_dict_t libsimgrid_location_list = MC_get_location_list(ls_path);
   MC_get_local_variables(ls_path, libsimgrid_location_list, &mc_local_variables);
+
+  MC_UNSET_RAW_MEM;
+
+  MC_init_memory_map_info();
+
+  /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */
+  get_libsimgrid_plt_section();
+  get_binary_plt_section();
+
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
+
+}
+
+void MC_modelcheck_liveness(){
+
+  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_init_liveness();
+ 
+  MC_SET_RAW_MEM;
   
   /* Initialize statistics */
   mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
@@ -214,8 +229,7 @@ void MC_modelcheck_liveness(){
   /* We're done */
   MC_print_statistics_pairs(mc_stats_pair);
   xbt_free(mc_time);
-  MC_memory_exit();
-  exit(0);
+
 }
 
 
@@ -357,9 +371,10 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
   XBT_DEBUG("**** Begin Replay ****");
 
   /* Restore the initial state */
-  MC_restore_snapshot(initial_snapshot_liveness);
+  MC_restore_snapshot(initial_state_liveness->initial_snapshot);
   /* At the moment of taking the snapshot the raw heap was set, so restoring
    * it will set it back again, we have to unset it to continue  */
+  
   MC_UNSET_RAW_MEM;
 
   if(all_stack){
@@ -555,8 +570,6 @@ void MC_dump_stack_liveness(xbt_fifo_t stack){
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
 
 }
 
@@ -617,10 +630,14 @@ void MC_process_clock_add(smx_process_t process, double amount)
 
 double MC_process_clock_get(smx_process_t process)
 {
-  if(mc_time)
-    return mc_time[process->pid];
-  else
+  if(mc_time){
+    if(process != NULL)
+      return mc_time[process->pid];
+    else 
+      return -1;
+  }else{
     return 0;
+  }
 }
 
 void MC_automaton_load(const char *file){
@@ -638,8 +655,6 @@ void MC_automaton_load(const char *file){
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
 
 }
 
@@ -658,8 +673,6 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
   
 }
 
@@ -667,6 +680,8 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
 
 void MC_ignore(void *address, size_t size){
 
+  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
   MC_SET_RAW_MEM;
   
   if(mc_comparison_ignore == NULL)
@@ -699,10 +714,15 @@ void MC_ignore(void *address, size_t size){
   xbt_dynar_insert_at(mc_comparison_ignore, cursor, &region);
 
   MC_UNSET_RAW_MEM;
+
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
 }
 
 void MC_new_stack_area(void *stack, char *name, void* context){
 
+  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
   MC_SET_RAW_MEM;
 
   if(stacks_areas == NULL)
@@ -716,6 +736,9 @@ void MC_new_stack_area(void *stack, char *name, void* context){
   xbt_dynar_push(stacks_areas, &region);
   
   MC_UNSET_RAW_MEM;
+
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
 }
 
 /************ DWARF ***********/
@@ -1266,7 +1289,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_bregister_op;
         new_element->location.breg_op.reg = atoi(strtok(tok2, "DW_OP_breg"));
-        new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, 2, char*));
+        new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, 1, char*));
         xbt_dynar_push(loc->location.compose, &new_element);
       }else if(strncmp(tok2, "DW_OP_lit", 9) == 0){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);