+
+dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name)
+{
+ const size_t n = process->object_infos_size;
+ size_t i;
+
+ // First lookup the variable in the executable shared object.
+ // A global variable used directly by the executable code from a library
+ // is reinstanciated in the executable memory .data/.bss.
+ // We need to look up the variable in the execvutable first.
+ if (process->binary_info) {
+ mc_object_info_t info = process->binary_info;
+ dw_variable_t var = MC_file_object_info_find_variable_by_name(info, name);
+ if (var)
+ return var;
+ }
+
+ for (i=0; i!=n; ++i) {
+ mc_object_info_t info =process->object_infos[i];
+ dw_variable_t var = MC_file_object_info_find_variable_by_name(info, name);
+ if (var)
+ return var;
+ }
+
+ return NULL;
+}
+
+void MC_process_read_variable(mc_process_t process, const char* name, void* target, size_t size)
+{
+ dw_variable_t var = MC_process_find_variable_by_name(process, name);
+ if (!var->address)
+ xbt_die("No simple location for this variable");
+ MC_process_read(process, MC_PROCESS_NO_FLAG, target, var->address, size,
+ MC_PROCESS_INDEX_ANY);
+}
+
+// ***** Memory access
+
+int MC_process_vm_open(pid_t pid, int flags)
+{
+ const size_t buffer_size = 30;
+ char buffer[buffer_size];
+ int res = snprintf(buffer, buffer_size, "/proc/%lli/mem", (long long) pid);
+ if (res < 0 || res >= buffer_size) {
+ errno = ENAMETOOLONG;
+ return -1;
+ }
+ return open(buffer, flags);
+}
+
+static void MC_process_open_memory_file(mc_process_t process)
+{
+ if (MC_process_is_self(process) || process->memory_file >= 0)
+ return;
+
+ int fd = MC_process_vm_open(process->pid, O_RDWR);
+ if (fd<0)
+ xbt_die("Could not open file for process virtual address space");
+ process->memory_file = fd;
+}
+
+static ssize_t pread_whole(int fd, void *buf, size_t count, off_t offset)
+{
+ char* buffer = (char*) buf;
+ ssize_t real_count = count;
+ while (count) {
+ ssize_t res = pread(fd, buffer, count, offset);
+ if (res > 0) {
+ count -= res;
+ buffer += res;
+ offset += res;
+ } else if (res==0) {
+ return -1;
+ } else if (errno != EINTR) {
+ return -1;
+ }
+ }
+ return real_count;
+}
+
+static ssize_t pwrite_whole(int fd, const void *buf, size_t count, off_t offset)
+{
+ const char* buffer = (const char*) buf;
+ ssize_t real_count = count;
+ while (count) {
+ ssize_t res = pwrite(fd, buffer, count, offset);
+ if (res > 0) {
+ count -= res;
+ buffer += res;
+ offset += res;
+ } else if (res==0) {
+ return -1;
+ } else if (errno != EINTR) {
+ return -1;
+ }
+ }
+ return real_count;
+}
+
+const void* MC_process_read(mc_process_t process, e_adress_space_read_flags_t flags,
+ void* local, const void* remote, size_t len,
+ int process_index)
+{
+ if (process_index != MC_PROCESS_INDEX_DISABLED) {
+ mc_object_info_t info = MC_process_find_object_info_rw(process, remote);
+ // Segment overlap is not handled.
+ if (MC_object_info_is_privatized(info)) {
+ if (process_index < 0)
+ xbt_die("Missing process index");
+ // Address translation in the privaization segment:
+ size_t offset = (const char*) remote - info->start_rw;
+ remote = (const char*) remote - offset;
+ }
+ }
+
+ if (MC_process_is_self(process)) {
+ if (flags & MC_ADDRESS_SPACE_READ_FLAGS_LAZY)
+ return remote;
+ else {
+ memcpy(local, remote, len);
+ return local;
+ }
+ } else {
+ if (pread_whole(process->memory_file, local, len, (off_t) remote) < 0)
+ xbt_die("Read from process %lli failed", (long long) process->pid);
+ return local;
+ }
+}
+
+const void* MC_process_read_simple(mc_process_t process,
+ void* local, const void* remote, size_t len)
+{
+ e_adress_space_read_flags_t flags = MC_PROCESS_NO_FLAG;
+ int index = MC_PROCESS_INDEX_ANY;
+ MC_process_read(process, flags, local, remote, len, index);
+ return local;
+}
+
+const void* MC_process_read_dynar_element(mc_process_t process,
+ void* local, const void* remote_dynar, size_t i)
+{
+ 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);
+ return local;
+}
+
+void MC_process_write(mc_process_t process, const void* local, void* remote, size_t len)
+{
+ if (MC_process_is_self(process)) {
+ memcpy(remote, local, len);
+ } else {
+ if (pwrite_whole(process->memory_file, local, len, (off_t) remote) < 0)
+ xbt_die("Write to process %lli failed", (long long) process->pid);
+ }
+}
+
+static pthread_once_t zero_buffer_flag = PTHREAD_ONCE_INIT;
+static const void* zero_buffer;
+static const int zero_buffer_size = 10 * 4096;
+
+static void MC_zero_buffer_init(void)
+{
+ int fd = open("/dev/zero", O_RDONLY);
+ if (fd<0)
+ xbt_die("Could not open /dev/zero");
+ zero_buffer = mmap(NULL, zero_buffer_size, PROT_READ, MAP_SHARED, fd, 0);
+ if (zero_buffer == MAP_FAILED)
+ xbt_die("Could not map the zero buffer");
+ close(fd);
+}
+
+void MC_process_clear_memory(mc_process_t process, void* remote, size_t len)
+{
+ if (MC_process_is_self(process)) {
+ memset(remote, 0, len);
+ } else {
+ pthread_once(&zero_buffer_flag, MC_zero_buffer_init);
+ while (len) {
+ size_t s = len > zero_buffer_size ? zero_buffer_size : len;
+ MC_process_write(process, zero_buffer, remote, s);
+ remote = (char*) remote + s;
+ len -= s;
+ }
+ }
+}
+
+void MC_simcall_handle(smx_simcall_t req, int value)
+{
+ if (MC_process_is_self(&mc_model_checker->process)) {
+ SIMIX_simcall_handle(req, value);
+ return;
+ }
+
+ MC_process_smx_refresh(&mc_model_checker->process);
+
+ unsigned i;
+ mc_smx_process_info_t pi = NULL;
+
+ xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) {
+ smx_process_t p = (smx_process_t) pi->address;
+ if (req == &pi->copy.simcall) {
+ smx_simcall_t real_req = &p->simcall;
+ // TODO, use a remote call
+ SIMIX_simcall_handle(real_req, value);
+ return;
+ }
+ }
+
+ // Check (remove afterwards):
+ xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) {
+ smx_process_t p = (smx_process_t) pi->address;
+ if (req == &p->simcall)
+ xbt_die("The real simcall was passed. We expected the local copy.");
+ }
+
+ xbt_die("Could not find the request");
+}