From: Gabriel Corona <gabriel.corona@loria.fr>
Date: Thu, 12 Mar 2015 15:02:18 +0000 (+0100)
Subject: [mc] MCed memory access in MC_state_get_request()
X-Git-Tag: v3_12~732^2~107
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/435dd478ae98a4816330830b1320ecd04386393f

[mc] MCed memory access in MC_state_get_request()
---

diff --git a/src/mc/mc_process.c b/src/mc/mc_process.c
index 7e047abad8..ba3968cfbc 100644
--- a/src/mc/mc_process.c
+++ b/src/mc/mc_process.c
@@ -530,6 +530,16 @@ void MC_process_write(mc_process_t process, const void* local, void* remote, siz
   }
 }
 
+unsigned long MC_process_read_dynar_length(mc_process_t process, const void* remote_dynar)
+{
+  if (!remote_dynar)
+    return 0;
+  unsigned long res;
+  MC_process_read_simple(process, &res,
+    &((xbt_dynar_t)remote_dynar)->used, sizeof(res));
+  return res;
+}
+
 static pthread_once_t zero_buffer_flag = PTHREAD_ONCE_INIT;
 static const void* zero_buffer;
 static const int zero_buffer_size = 10 * 4096;
diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h
index 84d90cd6fe..770bf3c8f2 100644
--- a/src/mc/mc_process.h
+++ b/src/mc/mc_process.h
@@ -159,11 +159,12 @@ const void* MC_process_read(mc_process_t process,
   void* local, const void* remote, size_t len,
   int process_index);
 
+// Simplified versions/wrappers (whould be moved in mc_address_space):
 const void* MC_process_read_simple(mc_process_t process,
   void* local, const void* remote, size_t len);
-
 const void* MC_process_read_dynar_element(mc_process_t process,
   void* local, const void* remote_dynar, size_t i);
+unsigned long MC_process_read_dynar_length(mc_process_t process, const void* remote_dynar);
 
 /** Write data to a process memory
  *
diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index d67fe350d8..02dc8ad39e 100644
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -233,8 +233,8 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
         case SIMCALL_COMM_WAITANY:
           *value = -1;
           while (procstate->interleave_count <
-                 xbt_dynar_length(simcall_comm_waitany__get__comms
-                                  (&process->simcall))) {
+                MC_process_read_dynar_length(&mc_model_checker->process,
+                  simcall_comm_waitany__get__comms(&process->simcall))) {
             if (MC_request_is_enabled_by_idx
                 (&process->simcall, procstate->interleave_count++)) {
               *value = procstate->interleave_count - 1;
@@ -243,8 +243,8 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
           }
 
           if (procstate->interleave_count >=
-              xbt_dynar_length(simcall_comm_waitany__get__comms
-                               (&process->simcall)))
+              MC_process_read_dynar_length(&mc_model_checker->process,
+                simcall_comm_waitany__get__comms(&process->simcall)))
             procstate->state = MC_DONE;
 
           if (*value != -1)
@@ -256,8 +256,8 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
           start_count = procstate->interleave_count;
           *value = -1;
           while (procstate->interleave_count <
-                 xbt_dynar_length(simcall_comm_testany__get__comms
-                                  (&process->simcall))) {
+                  MC_process_read_dynar_length(&mc_model_checker->process,
+                    simcall_comm_testany__get__comms(&process->simcall))) {
             if (MC_request_is_enabled_by_idx
                 (&process->simcall, procstate->interleave_count++)) {
               *value = procstate->interleave_count - 1;
@@ -266,8 +266,8 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
           }
 
           if (procstate->interleave_count >=
-              xbt_dynar_length(simcall_comm_testany__get__comms
-                               (&process->simcall)))
+              MC_process_read_dynar_length(&mc_model_checker->process,
+                simcall_comm_testany__get__comms(&process->simcall)))
             procstate->state = MC_DONE;
 
           if (*value != -1 || start_count == 0)