src/mc/mc_checkpoint.c

   1 /* Copyright (c) 2008-2014. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #define _GNU_SOURCE
   8 #define UNW_LOCAL_ONLY
   9
  10 #include <string.h>
  11 #include <link.h>
  12 #include "mc_private.h"
  13 #include "xbt/module.h"
  14 #include <xbt/mmalloc.h>
  15 #include "../smpi/private.h"
  16 #include <alloca.h>
  17
  18 #include "xbt/mmalloc/mmprivate.h"
  19
  20 #include "../simix/smx_private.h"
  21
  22 #include <libunwind.h>
  23 #include <libelf.h>
  24
  25 #include "mc_private.h"
  26 #include <mc/mc.h>
  27
  28 #include "mc_mmu.h"
  29
  30 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
  31                                 "Logging specific to mc_checkpoint");
  32
  33 char *libsimgrid_path;
  34
  35 /************************************  Free functions **************************************/
  36 /*****************************************************************************************/
  37
  38 static void MC_snapshot_stack_free(mc_snapshot_stack_t s)
  39 {
  40   if (s) {
  41     xbt_dynar_free(&(s->local_variables));
  42     xbt_dynar_free(&(s->stack_frames));
  43     xbt_free(s);
  44   }
  45 }
  46
  47 static void MC_snapshot_stack_free_voidp(void *s)
  48 {
  49   MC_snapshot_stack_free((mc_snapshot_stack_t) * (void **) s);
  50 }
  51
  52 static void local_variable_free(local_variable_t v)
  53 {
  54   xbt_free(v->name);
  55   xbt_free(v);
  56 }
  57
  58 static void local_variable_free_voidp(void *v)
  59 {
  60   local_variable_free((local_variable_t) * (void **) v);
  61 }
  62
  63 static void MC_region_destroy(mc_mem_region_t reg)
  64 {
  65   //munmap(reg->data, reg->size);
  66   xbt_free(reg->data);
  67   xbt_free(reg);
  68 }
  69
  70 void MC_free_snapshot(mc_snapshot_t snapshot)
  71 {
  72   unsigned int i;
  73   for (i = 0; i < NB_REGIONS; i++)
  74     MC_region_destroy(snapshot->regions[i]);
  75
  76   xbt_free(snapshot->stack_sizes);
  77   xbt_dynar_free(&(snapshot->stacks));
  78   xbt_dynar_free(&(snapshot->to_ignore));
  79   xbt_dynar_free(&snapshot->ignored_data);
  80
  81   if (snapshot->privatization_regions) {
  82     size_t n = xbt_dynar_length(snapshot->enabled_processes);
  83     for (i = 0; i != n; ++i) {
  84       MC_region_destroy(snapshot->privatization_regions[i]);
  85     }
  86     xbt_free(snapshot->privatization_regions);
  87   }
  88
  89   xbt_free(snapshot);
  90 }
  91
  92 /*******************************  Snapshot regions ********************************/
  93 /*********************************************************************************/
  94
  95 static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size, mc_mem_region_t ref_reg)
  96 {
  97   if (_sg_mc_sparse_checkpoint) {
  98     return mc_region_new_sparse(type, start_addr, size, ref_reg);
  99   }
 100
 101   mc_mem_region_t new_reg = xbt_new(s_mc_mem_region_t, 1);
 102   new_reg->start_addr = start_addr;
 103   new_reg->data = NULL;
 104   new_reg->size = size;
 105   new_reg->page_numbers = NULL;
 106   new_reg->data = xbt_malloc(size);
 107   memcpy(new_reg->data, start_addr, size);
 108   XBT_DEBUG("New region : type : %d, data : %p (real addr %p), size : %zu",
 109             type, new_reg->data, start_addr, size);
 110   return new_reg;
 111
 112 }
 113
 114 /** @brief Restore a region from a snapshot
 115  *
 116  *  If we are using per page snapshots, it is possible to use the reference
 117  *  region in order to do an incremental restoration of the region: the
 118  *  softclean pages which are shared between the two snapshots do not need
 119  *  to be restored.
 120  *
 121  *  @param reg     Target region
 122  *  @param reg_reg Current region (if not NULL), used for lazy per page restoration
 123  */
 124 static void MC_region_restore(mc_mem_region_t reg, mc_mem_region_t ref_reg)
 125 {
 126   /*FIXME: check if start_addr is still mapped, if it is not, then map it
 127     before copying the data */
 128   if (!reg->page_numbers) {
 129     memcpy(reg->start_addr, reg->data, reg->size);
 130   } else {
 131     mc_region_restore_sparse(reg, ref_reg);
 132   }
 133   return;
 134 }
 135
 136 static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type,
 137                                    void *start_addr, size_t size)
 138
 139 {
 140   mc_mem_region_t ref_reg =
 141     mc_model_checker->parent_snapshot ? mc_model_checker->parent_snapshot->regions[type] : NULL;
 142   mc_mem_region_t new_reg = MC_region_new(type, start_addr, size, ref_reg);
 143   snapshot->regions[type] = new_reg;
 144   return;
 145 }
 146
 147 static void MC_get_memory_regions(mc_snapshot_t snapshot)
 148 {
 149   size_t i;
 150
 151   void *start_heap = ((xbt_mheap_t) std_heap)->base;
 152   void *end_heap = ((xbt_mheap_t) std_heap)->breakval;
 153   MC_snapshot_add_region(snapshot, 0, start_heap,
 154                          (char *) end_heap - (char *) start_heap);
 155   snapshot->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
 156
 157   MC_snapshot_add_region(snapshot, 1, mc_libsimgrid_info->start_rw,
 158                          mc_libsimgrid_info->end_rw -
 159                          mc_libsimgrid_info->start_rw);
 160   if (!smpi_privatize_global_variables) {
 161     MC_snapshot_add_region(snapshot, 2, mc_binary_info->start_rw,
 162                            mc_binary_info->end_rw - mc_binary_info->start_rw);
 163     snapshot->privatization_regions = NULL;
 164     snapshot->privatization_index = -1;
 165   } else {
 166     snapshot->privatization_regions =
 167         xbt_new(mc_mem_region_t, SIMIX_process_count());
 168     for (i = 0; i < SIMIX_process_count(); i++) {
 169       // TODO, add support for sparse snapshot
 170       snapshot->privatization_regions[i] =
 171         MC_region_new(-1, mappings[i], size_data_exe, NULL);
 172     }
 173     snapshot->privatization_index = loaded_page;
 174   }
 175 }
 176
 177 /** @brief Finds the range of the different memory segments and binary paths */
 178 void MC_init_memory_map_info()
 179 {
 180
 181   unsigned int i = 0;
 182   s_map_region_t reg;
 183   memory_map_t maps = MC_get_memory_map();
 184
 185   maestro_stack_start = NULL;
 186   maestro_stack_end = NULL;
 187   libsimgrid_path = NULL;
 188
 189   while (i < maps->mapsize) {
 190     reg = maps->regions[i];
 191     if (maps->regions[i].pathname == NULL) {
 192       // Nothing to do
 193     } else if ((reg.prot & PROT_WRITE)
 194                && !memcmp(maps->regions[i].pathname, "[stack]", 7)) {
 195       maestro_stack_start = reg.start_addr;
 196       maestro_stack_end = reg.end_addr;
 197     } else if ((reg.prot & PROT_READ) && (reg.prot & PROT_EXEC)
 198                && !memcmp(basename(maps->regions[i].pathname), "libsimgrid",
 199                           10)) {
 200       if (libsimgrid_path == NULL)
 201         libsimgrid_path = strdup(maps->regions[i].pathname);
 202     }
 203     i++;
 204   }
 205
 206   xbt_assert(maestro_stack_start, "maestro_stack_start");
 207   xbt_assert(maestro_stack_end, "maestro_stack_end");
 208   xbt_assert(libsimgrid_path, "libsimgrid_path&");
 209
 210   MC_free_memory_map(maps);
 211
 212 }
 213
 214 /** \brief Fill/lookup the "subtype" field.
 215  */
 216 static void MC_resolve_subtype(mc_object_info_t info, dw_type_t type)
 217 {
 218
 219   if (type->dw_type_id == NULL)
 220     return;
 221   type->subtype = xbt_dict_get_or_null(info->types, type->dw_type_id);
 222   if (type->subtype == NULL)
 223     return;
 224   if (type->subtype->byte_size != 0)
 225     return;
 226   if (type->subtype->name == NULL)
 227     return;
 228   // Try to find a more complete description of the type:
 229   // We need to fix in order to support C++.
 230
 231   dw_type_t subtype =
 232       xbt_dict_get_or_null(info->full_types_by_name, type->subtype->name);
 233   if (subtype != NULL) {
 234     type->subtype = subtype;
 235   }
 236
 237 }
 238
 239 void MC_post_process_types(mc_object_info_t info)
 240 {
 241   xbt_dict_cursor_t cursor = NULL;
 242   char *origin;
 243   dw_type_t type;
 244
 245   // Lookup "subtype" field:
 246   xbt_dict_foreach(info->types, cursor, origin, type) {
 247     MC_resolve_subtype(info, type);
 248
 249     dw_type_t member;
 250     unsigned int i = 0;
 251     if (type->members != NULL)
 252       xbt_dynar_foreach(type->members, i, member) {
 253       MC_resolve_subtype(info, member);
 254       }
 255   }
 256 }
 257
 258 /** \brief Fills the position of the segments (executable, read-only, read/write).
 259  *
 260  * TODO, use dl_iterate_phdr to be more robust
 261  * */
 262 void MC_find_object_address(memory_map_t maps, mc_object_info_t result)
 263 {
 264
 265   unsigned int i = 0;
 266   s_map_region_t reg;
 267   const char *name = basename(result->file_name);
 268   while (i < maps->mapsize) {
 269     reg = maps->regions[i];
 270     if (maps->regions[i].pathname == NULL
 271         || strcmp(basename(maps->regions[i].pathname), name)) {
 272       // Nothing to do
 273     } else if ((reg.prot & PROT_WRITE)) {
 274       xbt_assert(!result->start_rw,
 275                  "Multiple read-write segments for %s, not supported",
 276                  maps->regions[i].pathname);
 277       result->start_rw = reg.start_addr;
 278       result->end_rw = reg.end_addr;
 279       // .bss is usually after the .data:
 280       s_map_region_t *next = &(maps->regions[i + 1]);
 281       if (next->pathname == NULL && (next->prot & PROT_WRITE)
 282           && next->start_addr == reg.end_addr) {
 283         result->end_rw = maps->regions[i + 1].end_addr;
 284       }
 285     } else if ((reg.prot & PROT_READ) && (reg.prot & PROT_EXEC)) {
 286       xbt_assert(!result->start_exec,
 287                  "Multiple executable segments for %s, not supported",
 288                  maps->regions[i].pathname);
 289       result->start_exec = reg.start_addr;
 290       result->end_exec = reg.end_addr;
 291     } else if ((reg.prot & PROT_READ) && !(reg.prot & PROT_EXEC)) {
 292       xbt_assert(!result->start_ro,
 293                  "Multiple read only segments for %s, not supported",
 294                  maps->regions[i].pathname);
 295       result->start_ro = reg.start_addr;
 296       result->end_ro = reg.end_addr;
 297     }
 298     i++;
 299   }
 300
 301   xbt_assert(result->file_name);
 302   xbt_assert(result->start_rw);
 303   xbt_assert(result->start_exec);
 304 }
 305
 306 /************************************* Take Snapshot ************************************/
 307 /****************************************************************************************/
 308
 309 /** \brief Checks whether the variable is in scope for a given IP.
 310  *
 311  *  A variable may be defined only from a given value of IP.
 312  *
 313  *  \param var   Variable description
 314  *  \param frame Scope description
 315  *  \param ip    Instruction pointer
 316  *  \return      true if the variable is valid
 317  * */
 318 static bool mc_valid_variable(dw_variable_t var, dw_frame_t scope,
 319                               const void *ip)
 320 {
 321   // The variable is not yet valid:
 322   if ((const void *) ((const char *) scope->low_pc + var->start_scope) > ip)
 323     return false;
 324   else
 325     return true;
 326 }
 327
 328 static void mc_fill_local_variables_values(mc_stack_frame_t stack_frame,
 329                                            dw_frame_t scope, xbt_dynar_t result)
 330 {
 331   void *ip = (void *) stack_frame->ip;
 332   if (ip < scope->low_pc || ip >= scope->high_pc)
 333     return;
 334
 335   unsigned cursor = 0;
 336   dw_variable_t current_variable;
 337   xbt_dynar_foreach(scope->variables, cursor, current_variable) {
 338
 339     if (!mc_valid_variable(current_variable, scope, (void *) stack_frame->ip))
 340       continue;
 341
 342     int region_type;
 343     if ((long) stack_frame->ip > (long) mc_libsimgrid_info->start_exec)
 344       region_type = 1;
 345     else
 346       region_type = 2;
 347
 348     local_variable_t new_var = xbt_new0(s_local_variable_t, 1);
 349     new_var->subprogram = stack_frame->frame;
 350     new_var->ip = stack_frame->ip;
 351     new_var->name = xbt_strdup(current_variable->name);
 352     new_var->type = current_variable->type;
 353     new_var->region = region_type;
 354
 355     if (current_variable->address != NULL) {
 356       new_var->address = current_variable->address;
 357     } else if (current_variable->locations.size != 0) {
 358       new_var->address =
 359           (void *) mc_dwarf_resolve_locations(&current_variable->locations,
 360                                               current_variable->object_info,
 361                                               &(stack_frame->unw_cursor),
 362                                               (void *) stack_frame->frame_base,
 363                                               NULL);
 364     } else {
 365       xbt_die("No address");
 366     }
 367
 368     xbt_dynar_push(result, &new_var);
 369   }
 370
 371   // Recursive processing of nested scopes:
 372   dw_frame_t nested_scope = NULL;
 373   xbt_dynar_foreach(scope->scopes, cursor, nested_scope) {
 374     mc_fill_local_variables_values(stack_frame, nested_scope, result);
 375   }
 376 }
 377
 378 static xbt_dynar_t MC_get_local_variables_values(xbt_dynar_t stack_frames)
 379 {
 380
 381   unsigned cursor1 = 0;
 382   mc_stack_frame_t stack_frame;
 383   xbt_dynar_t variables =
 384       xbt_dynar_new(sizeof(local_variable_t), local_variable_free_voidp);
 385
 386   xbt_dynar_foreach(stack_frames, cursor1, stack_frame) {
 387     mc_fill_local_variables_values(stack_frame, stack_frame->frame, variables);
 388   }
 389
 390   return variables;
 391 }
 392
 393 static void MC_stack_frame_free_voipd(void *s)
 394 {
 395   mc_stack_frame_t stack_frame = *(mc_stack_frame_t *) s;
 396   if (stack_frame) {
 397     xbt_free(stack_frame->frame_name);
 398     xbt_free(stack_frame);
 399   }
 400 }
 401
 402 static xbt_dynar_t MC_unwind_stack_frames(void *stack_context)
 403 {
 404   xbt_dynar_t result =
 405       xbt_dynar_new(sizeof(mc_stack_frame_t), MC_stack_frame_free_voipd);
 406
 407   unw_cursor_t c;
 408
 409   // TODO, check condition check (unw_init_local==0 means end of frame)
 410   if (unw_init_local(&c, (unw_context_t *) stack_context) != 0) {
 411
 412     xbt_die("Could not initialize stack unwinding");
 413
 414   } else
 415     while (1) {
 416
 417       mc_stack_frame_t stack_frame = xbt_new(s_mc_stack_frame_t, 1);
 418       xbt_dynar_push(result, &stack_frame);
 419
 420       stack_frame->unw_cursor = c;
 421
 422       unw_word_t ip, sp;
 423
 424       unw_get_reg(&c, UNW_REG_IP, &ip);
 425       unw_get_reg(&c, UNW_REG_SP, &sp);
 426
 427       stack_frame->ip = ip;
 428       stack_frame->sp = sp;
 429
 430       // TODO, use real addresses in frame_t instead of fixing it here
 431
 432       dw_frame_t frame = MC_find_function_by_ip((void *) ip);
 433       stack_frame->frame = frame;
 434
 435       if (frame) {
 436         stack_frame->frame_name = xbt_strdup(frame->name);
 437         stack_frame->frame_base =
 438             (unw_word_t) mc_find_frame_base(frame, frame->object_info, &c);
 439       } else {
 440         stack_frame->frame_base = 0;
 441         stack_frame->frame_name = NULL;
 442       }
 443
 444       /* Stop before context switch with maestro */
 445       if (frame != NULL && frame->name != NULL
 446           && !strcmp(frame->name, "smx_ctx_sysv_wrapper"))
 447         break;
 448
 449       int ret = ret = unw_step(&c);
 450       if (ret == 0) {
 451         xbt_die("Unexpected end of stack.");
 452       } else if (ret < 0) {
 453         xbt_die("Error while unwinding stack.");
 454       }
 455     }
 456
 457   if (xbt_dynar_length(result) == 0) {
 458     XBT_INFO("unw_init_local failed");
 459     xbt_abort();
 460   }
 461
 462   return result;
 463 };
 464
 465 static xbt_dynar_t MC_take_snapshot_stacks(mc_snapshot_t * snapshot, void *heap)
 466 {
 467
 468   xbt_dynar_t res =
 469       xbt_dynar_new(sizeof(s_mc_snapshot_stack_t),
 470                     MC_snapshot_stack_free_voidp);
 471
 472   unsigned int cursor = 0;
 473   stack_region_t current_stack;
 474
 475   xbt_dynar_foreach(stacks_areas, cursor, current_stack) {
 476     mc_snapshot_stack_t st = xbt_new(s_mc_snapshot_stack_t, 1);
 477     st->stack_frames = MC_unwind_stack_frames(current_stack->context);
 478     st->local_variables = MC_get_local_variables_values(st->stack_frames);
 479
 480     unw_word_t sp = xbt_dynar_get_as(st->stack_frames, 0, mc_stack_frame_t)->sp;
 481     st->stack_pointer =
 482         ((char *) heap + (size_t) (((char *) ((long) sp) - (char *) std_heap)));
 483
 484     st->real_address = current_stack->address;
 485     xbt_dynar_push(res, &st);
 486     (*snapshot)->stack_sizes =
 487         xbt_realloc((*snapshot)->stack_sizes, (cursor + 1) * sizeof(size_t));
 488     (*snapshot)->stack_sizes[cursor] =
 489         current_stack->size - ((char *) st->stack_pointer -
 490                                (char *) ((char *) heap +
 491                                          ((char *) current_stack->address -
 492                                           (char *) std_heap)));
 493   }
 494
 495   return res;
 496
 497 }
 498
 499 static xbt_dynar_t MC_take_snapshot_ignore()
 500 {
 501
 502   if (mc_heap_comparison_ignore == NULL)
 503     return NULL;
 504
 505   xbt_dynar_t cpy =
 506       xbt_dynar_new(sizeof(mc_heap_ignore_region_t),
 507                     heap_ignore_region_free_voidp);
 508
 509   unsigned int cursor = 0;
 510   mc_heap_ignore_region_t current_region;
 511
 512   xbt_dynar_foreach(mc_heap_comparison_ignore, cursor, current_region) {
 513     mc_heap_ignore_region_t new_region = NULL;
 514     new_region = xbt_new0(s_mc_heap_ignore_region_t, 1);
 515     new_region->address = current_region->address;
 516     new_region->size = current_region->size;
 517     new_region->block = current_region->block;
 518     new_region->fragment = current_region->fragment;
 519     xbt_dynar_push(cpy, &new_region);
 520   }
 521
 522   return cpy;
 523
 524 }
 525
 526 static void mc_free_snapshot_ignored_data_pvoid(void* data) {
 527   mc_snapshot_ignored_data_t ignored_data = (mc_snapshot_ignored_data_t) data;
 528   free(ignored_data->data);
 529 }
 530
 531 static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
 532 {
 533   snapshot->ignored_data = xbt_dynar_new(sizeof(s_mc_snapshot_ignored_data_t), mc_free_snapshot_ignored_data_pvoid);
 534
 535   // Copy the memory:
 536   unsigned int cursor = 0;
 537   mc_checkpoint_ignore_region_t region;
 538   xbt_dynar_foreach (mc_checkpoint_ignore, cursor, region) {
 539     s_mc_snapshot_ignored_data_t ignored_data;
 540     ignored_data.start = region->addr;
 541     ignored_data.size = region->size;
 542     ignored_data.data = malloc(region->size);
 543     memcpy(ignored_data.data, region->addr, region->size);
 544     xbt_dynar_push(snapshot->ignored_data, &ignored_data);
 545   }
 546
 547   // Zero the memory:
 548   xbt_dynar_foreach (mc_checkpoint_ignore, cursor, region) {
 549     memset(region->addr, 0, region->size);
 550   }
 551
 552 }
 553
 554 static void MC_snapshot_ignore_restore(mc_snapshot_t snapshot)
 555 {
 556   unsigned int cursor = 0;
 557   s_mc_snapshot_ignored_data_t ignored_data;
 558   xbt_dynar_foreach (snapshot->ignored_data, cursor, ignored_data) {
 559     memcpy(ignored_data.start, ignored_data.data, ignored_data.size);
 560   }
 561 }
 562
 563 /** @brief Can we remove this snapshot?
 564  *
 565  * Some snapshots cannot be removed (yet) because we need them
 566  * at this point.
 567  *
 568  * @param snapshot
 569  */
 570 int mc_important_snapshot(mc_snapshot_t snapshot)
 571 {
 572   // We need this snapshot in order to know which
 573   // pages needs to be stored in the next snapshot:
 574   if (_sg_mc_sparse_checkpoint && snapshot == mc_model_checker->parent_snapshot)
 575     return true;
 576
 577   return false;
 578 }
 579
 580 mc_snapshot_t MC_take_snapshot(int num_state)
 581 {
 582
 583   mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
 584   snapshot->enabled_processes = xbt_dynar_new(sizeof(int), NULL);
 585   smx_process_t process;
 586   xbt_swag_foreach(process, simix_global->process_list) {
 587     xbt_dynar_push_as(snapshot->enabled_processes, int, (int)process->pid);
 588   }
 589
 590   MC_snapshot_handle_ignore(snapshot);
 591
 592   /* Save the std heap and the writable mapped pages of libsimgrid and binary */
 593   MC_get_memory_regions(snapshot);
 594   if (_sg_mc_sparse_checkpoint) {
 595     mc_softdirty_reset();
 596   }
 597
 598   snapshot->to_ignore = MC_take_snapshot_ignore();
 599
 600   if (_sg_mc_visited > 0 || strcmp(_sg_mc_property_file, "")) {
 601     snapshot->stacks =
 602         MC_take_snapshot_stacks(&snapshot, snapshot->regions[0]->data);
 603     if (_sg_mc_hash && snapshot->stacks != NULL) {
 604       snapshot->hash = mc_hash_processes_state(num_state, snapshot->stacks);
 605     } else {
 606       snapshot->hash = 0;
 607     }
 608   } else {
 609     snapshot->hash = 0;
 610   }
 611
 612   MC_snapshot_ignore_restore(snapshot);
 613   mc_model_checker->parent_snapshot = snapshot;
 614   return snapshot;
 615 }
 616
 617 void MC_restore_snapshot(mc_snapshot_t snapshot)
 618 {
 619   mc_snapshot_t parent_snapshot = mc_model_checker->parent_snapshot;
 620
 621   unsigned int i;
 622   for (i = 0; i < NB_REGIONS; i++) {
 623     // For privatized, variables we decided it was not necessary to take the snapshot:
 624     if (snapshot->regions[i])
 625       MC_region_restore(snapshot->regions[i],
 626         parent_snapshot ? parent_snapshot->regions[i] : NULL);
 627   }
 628
 629   if (snapshot->privatization_regions) {
 630     for (i = 0; i < SIMIX_process_count(); i++) {
 631       if (snapshot->privatization_regions[i]) {
 632         MC_region_restore(snapshot->privatization_regions[i],
 633           parent_snapshot ? parent_snapshot->privatization_regions[i] : NULL);
 634       }
 635     }
 636     switch_data_segment(snapshot->privatization_index);
 637   }
 638
 639   MC_snapshot_ignore_restore(snapshot);
 640   if (_sg_mc_sparse_checkpoint) {
 641     mc_softdirty_reset();
 642   }
 643   mc_model_checker->parent_snapshot = snapshot;
 644 }
 645
 646 void *mc_translate_address(uintptr_t addr, mc_snapshot_t snapshot)
 647 {
 648
 649   // If not in a process state/clone:
 650   if (!snapshot) {
 651     return (uintptr_t *) addr;
 652   }
 653   // If it is in a snapshot:
 654   for (size_t i = 0; i != NB_REGIONS; ++i) {
 655     mc_mem_region_t region = snapshot->regions[i];
 656     uintptr_t start = (uintptr_t) region->start_addr;
 657     uintptr_t end = start + region->size;
 658
 659     // The address is in this region:
 660     if (addr >= start && addr < end) {
 661       uintptr_t offset = addr - start;
 662       return (void *) ((uintptr_t) region->data + offset);
 663     }
 664
 665   }
 666
 667   // It is not in a snapshot:
 668   return (void *) addr;
 669 }
 670
 671 uintptr_t mc_untranslate_address(void *addr, mc_snapshot_t snapshot)
 672 {
 673   if (!snapshot) {
 674     return (uintptr_t) addr;
 675   }
 676
 677   for (size_t i = 0; i != NB_REGIONS; ++i) {
 678     mc_mem_region_t region = snapshot->regions[i];
 679     if (addr >= region->data
 680         && addr <= (void *) (((char *) region->data) + region->size)) {
 681       size_t offset = (size_t) ((char *) addr - (char *) region->data);
 682       return ((uintptr_t) region->start_addr) + offset;
 683     }
 684   }
 685
 686   return (uintptr_t) addr;
 687 }
 688
 689 mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall)
 690 {
 691   return MC_take_snapshot(1);
 692 }
 693
 694 void *MC_snapshot(void)
 695 {
 696   return simcall_mc_snapshot();
 697 }