[mc] Do not take NULL to mean 'the current address space' in dwarf expressions

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

diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c
index 38e0999..3dea427 100644 (file)
--- a/src/mc/mc_safety.c
+++ b/src/mc/mc_safety.c
@@ -4,11 +4,14 @@
 /* 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 <assert.h>
+
 #include "mc_state.h"
 #include "mc_request.h"
 #include "mc_safety.h"
 #include "mc_private.h"
 #include "mc_record.h"
+#include "mc_smx.h"
 
 #include "xbt/mmalloc/mmprivate.h"
 
@@ -34,21 +37,15 @@ static int is_exploration_stack_state(mc_state_t current_state){
  */
 void MC_pre_modelcheck_safety()
 {
-
-  int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
   mc_state_t initial_state = NULL;
   smx_process_t process;
 
-  /* Create the initial state and push it into the exploration stack */
-  if (!mc_mem_set)
-    MC_SET_MC_HEAP;
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
   if (_sg_mc_visited > 0)
     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
 
   initial_state = MC_state_new();
-
   MC_SET_STD_HEAP;
 
   XBT_DEBUG("**************************************************");
@@ -60,18 +57,16 @@ void MC_pre_modelcheck_safety()
   MC_SET_MC_HEAP;
 
   /* Get an enabled process and insert it in the interleave set of the initial state */
-  xbt_swag_foreach(process, simix_global->process_list) {
+  MC_EACH_SIMIX_PROCESS(process,
     if (MC_process_is_enabled(process)) {
       MC_state_interleave_process(initial_state, process);
       if (mc_reduce_kind != e_mc_reduce_none)
         break;
     }
-  }
+  );
 
   xbt_fifo_unshift(mc_stack, initial_state);
-
-  if (!mc_mem_set)
-    MC_SET_STD_HEAP;
+  mmalloc_set_current_heap(heap);
 }
 
 
@@ -122,7 +117,7 @@ void MC_modelcheck_safety(void)
       mc_stats->executed_transitions++;
 
       /* Answer the request */
-      SIMIX_simcall_handle(req, value);
+      MC_simcall_handle(req, value);
 
       /* Wait for requests (schedules processes) */
       MC_wait_for_requests();
@@ -140,13 +135,13 @@ void MC_modelcheck_safety(void)
       if ((visited_state = is_visited_state(next_state)) == NULL) {
 
         /* Get an enabled process and insert it in the interleave set of the next state */
-        xbt_swag_foreach(process, simix_global->process_list) {
+        MC_EACH_SIMIX_PROCESS(process,
           if (MC_process_is_enabled(process)) {
             MC_state_interleave_process(next_state, process);
             if (mc_reduce_kind != e_mc_reduce_none)
               break;
           }
-        }
+        );
 
         if (dot_output != NULL)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
@@ -213,6 +208,7 @@ void MC_modelcheck_safety(void)
       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
         if (mc_reduce_kind == e_mc_reduce_dpor) {
           req = MC_state_get_internal_request(state);
+          const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
             if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
@@ -227,8 +223,8 @@ void MC_modelcheck_safety(void)
                 xbt_free(req_str);
               }
 
-              if (!MC_state_process_is_done(prev_state, req->issuer))
-                MC_state_interleave_process(prev_state, req->issuer);
+              if (!MC_state_process_is_done(prev_state, issuer))
+                MC_state_interleave_process(prev_state, issuer);
               else
                 XBT_DEBUG("Process %p is in done set", req->issuer);
 
@@ -241,10 +237,11 @@ void MC_modelcheck_safety(void)
 
             } else {
 
+              const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
-                        req->call, req->issuer->pid, state->num,
+                        req->call, issuer->pid, state->num,
                         MC_state_get_internal_request(prev_state)->call,
-                        MC_state_get_internal_request(prev_state)->issuer->pid,
+                        previous_issuer->pid,
                         prev_state->num);
 
             }