[mc] Fix MC_process_read_dynar_element

 * Add a length parameter and check it against dynar->elmsize;
 * Check out of bound access;
 * Fix the callers.

diff --git a/src/mc/mc_process.c b/src/mc/mc_process.c
index 47c907d..dd9c3ac 100644 (file)
--- a/src/mc/mc_process.c
+++ b/src/mc/mc_process.c
@@ -551,11 +551,15 @@ const void* MC_process_read_simple(mc_process_t process,
 }
 
 const void* MC_process_read_dynar_element(mc_process_t process,
-  void* local, const void* remote_dynar, size_t i)
+  void* local, const void* remote_dynar, size_t i, size_t len)
 {
   s_xbt_dynar_t d;
   MC_process_read_simple(process, &d, remote_dynar, sizeof(d));
-  MC_process_read_simple(process, local, xbt_dynar_get_ptr(&d, i), i);
+  if (i >= d.used)
+    xbt_die("Out of bound index %zi/%zi", i, d.used);
+  if (len != d.elmsize)
+    xbt_die("Bad size in MC_process_read_dynar_element");
+  MC_process_read_simple(process, local, xbt_dynar_get_ptr(&d, i), len);
   return local;
 }
 

diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h
index 3334096..8159b3e 100644 (file)
--- a/src/mc/mc_process.h
+++ b/src/mc/mc_process.h
@@ -163,7 +163,7 @@ const void* MC_process_read(mc_process_t process,
 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);
+  void* local, const void* remote_dynar, size_t i, size_t len);
 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_request.c b/src/mc/mc_request.c
index 47609e8..a4bd9d9 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -352,7 +352,8 @@ char *MC_request_to_string(smx_simcall_t req, int value)
     if (!xbt_dynar_is_empty(&comms)) {
       smx_synchro_t remote_sync;
       MC_process_read_dynar_element(&mc_model_checker->process,
-        &remote_sync, simcall_comm_waitany__get__comms(req), value);
+        &remote_sync, simcall_comm_waitany__get__comms(req), value,
+        sizeof(remote_sync));
       char* p = pointer_to_string(remote_sync);
       args = bprintf("comm=%s (%d of %lu)",
         p, value + 1, xbt_dynar_length(&comms));
@@ -481,7 +482,7 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
     smx_synchro_t act;
     MC_process_read_dynar_element(
       &mc_model_checker->process, &act, simcall_comm_waitany__get__comms(req),
-      idx);
+      idx, sizeof(act));
     }
     break;
 
@@ -489,7 +490,7 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
     s_smx_synchro_t act;
     MC_process_read_dynar_element(
       &mc_model_checker->process, &act, simcall_comm_testany__get__comms(req),
-      idx);
+      idx, sizeof(act));
     }
     break;
 

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index 2239ac9..0e0126b 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -101,7 +101,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
     state->internal_req.issuer = req->issuer;
     MC_process_read_dynar_element(&mc_model_checker->process,
       &state->internal_comm, simcall_comm_waitany__get__comms(req),
-      sizeof(state->internal_comm));
+      value, sizeof(state->internal_comm));
     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
     simcall_comm_wait__set__timeout(&state->internal_req, 0);
     break;
@@ -113,7 +113,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
     if (value > 0)
         MC_process_read_dynar_element(&mc_model_checker->process,
           &state->internal_comm, simcall_comm_testany__get__comms(req),
-          sizeof(state->internal_comm));
+          value, sizeof(state->internal_comm));
 
     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
     simcall_comm_test__set__result(&state->internal_req, value);