[mc] Fix the translation of privatisation section in Process::read_bytes()

diff --git a/src/mc/mc_process.cpp b/src/mc/mc_process.cpp
index 0b4a9ba..9f944d3 100644 (file)
--- a/src/mc/mc_process.cpp
+++ b/src/mc/mc_process.cpp
@@ -534,10 +534,21 @@ const void *Process::read_bytes(void* buffer, std::size_t size,
     if (MC_object_info_is_privatized(info)) {
       if (process_index < 0)
         xbt_die("Missing process index");
     if (MC_object_info_is_privatized(info)) {
       if (process_index < 0)
         xbt_die("Missing process index");

+      if (process_index >= (int) MC_smpi_process_count())
+        xbt_die("Invalid process index");
+
+      // Read smpi_privatisation_regions from MCed:
+      smpi_privatisation_region_t remote_smpi_privatisation_regions =
+        mc_model_checker->process().read_variable<smpi_privatisation_region_t>(
+          "smpi_privatisation_regions");
+
+      s_smpi_privatisation_region_t privatisation_region =
+        mc_model_checker->process().read<s_smpi_privatisation_region_t>(
+          remote(remote_smpi_privatisation_regions + process_index));
+

       // Address translation in the privaization segment:
       // Address translation in the privaization segment:

-      // TODO, fix me (broken)

       size_t offset = address.address() - (std::uint64_t)info->start_rw;
       size_t offset = address.address() - (std::uint64_t)info->start_rw;

-      address = remote(address.address() - offset);
+      address = remote((char*)privatisation_region.address + offset);

     }
   }
 
     }
   }
 

diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h
index 238fa36..d26ca5b 100644 (file)
--- a/src/mc/mc_process.h
+++ b/src/mc/mc_process.h
@@ -71,6 +71,14 @@ public:
     remote_ptr<void> address, int process_index = ProcessIndexAny,
     ReadMode mode = Normal) const override;
   void read_variable(const char* name, void* target, size_t size) const;
     remote_ptr<void> address, int process_index = ProcessIndexAny,
     ReadMode mode = Normal) const override;
   void read_variable(const char* name, void* target, size_t size) const;

+  template<class T>
+  T read_variable(const char *name) const
+  {
+    static_assert(std::is_trivial<T>::value, "Cannot read a non-trivial type");
+    T res;
+    read_variable(name, &res, sizeof(T));
+    return res;
+  }

   char* read_string(remote_ptr<void> address) const;
 
   // Write memory:
   char* read_string(remote_ptr<void> address) const;
 
   // Write memory: