[mc] Reset the softdirty bits *before* restoring the ignored bytes (not after)

[simgrid.git] / src / mc / mc_checkpoint.c

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 9d575f2..c07f666 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -462,7 +462,7 @@ static xbt_dynar_t MC_unwind_stack_frames(void *stack_context)
   return result;
 };
 
-static xbt_dynar_t MC_take_snapshot_stacks(mc_snapshot_t * snapshot, void *heap)
+static xbt_dynar_t MC_take_snapshot_stacks(mc_snapshot_t * snapshot)
 {
 
   xbt_dynar_t res =
@@ -585,7 +585,7 @@ mc_snapshot_t MC_take_snapshot(int num_state)
 
   /* Save the std heap and the writable mapped pages of libsimgrid and binary */
   MC_get_memory_regions(snapshot);
-  if (_sg_mc_sparse_checkpoint) {
+  if (_sg_mc_sparse_checkpoint && _sg_mc_soft_dirty) {
     mc_softdirty_reset();
   }
 
@@ -593,7 +593,7 @@ mc_snapshot_t MC_take_snapshot(int num_state)
 
   if (_sg_mc_visited > 0 || strcmp(_sg_mc_property_file, "")) {
     snapshot->stacks =
-        MC_take_snapshot_stacks(&snapshot, snapshot->regions[0]->data);
+        MC_take_snapshot_stacks(&snapshot);
     if (_sg_mc_hash && snapshot->stacks != NULL) {
       snapshot->hash = mc_hash_processes_state(num_state, snapshot->stacks);
     } else {
@@ -630,54 +630,12 @@ void MC_restore_snapshot(mc_snapshot_t snapshot)
     switch_data_segment(snapshot->privatization_index);
   }
 
-  MC_snapshot_ignore_restore(snapshot);
-  if (_sg_mc_sparse_checkpoint) {
+  if (_sg_mc_sparse_checkpoint && _sg_mc_soft_dirty) {
     mc_softdirty_reset();
   }
-  mc_model_checker->parent_snapshot = snapshot;
-}
-
-void *mc_translate_address(uintptr_t addr, mc_snapshot_t snapshot)
-{
-
-  // If not in a process state/clone:
-  if (!snapshot) {
-    return (uintptr_t *) addr;
-  }
-  // If it is in a snapshot:
-  for (size_t i = 0; i != NB_REGIONS; ++i) {
-    mc_mem_region_t region = snapshot->regions[i];
-    uintptr_t start = (uintptr_t) region->start_addr;
-    uintptr_t end = start + region->size;
-
-    // The address is in this region:
-    if (addr >= start && addr < end) {
-      uintptr_t offset = addr - start;
-      return (void *) ((uintptr_t) region->data + offset);
-    }
-
-  }
-
-  // It is not in a snapshot:
-  return (void *) addr;
-}
-
-uintptr_t mc_untranslate_address(void *addr, mc_snapshot_t snapshot)
-{
-  if (!snapshot) {
-    return (uintptr_t) addr;
-  }
 
-  for (size_t i = 0; i != NB_REGIONS; ++i) {
-    mc_mem_region_t region = snapshot->regions[i];
-    if (addr >= region->data
-        && addr <= (void *) (((char *) region->data) + region->size)) {
-      size_t offset = (size_t) ((char *) addr - (char *) region->data);
-      return ((uintptr_t) region->start_addr) + offset;
-    }
-  }
-
-  return (uintptr_t) addr;
+  MC_snapshot_ignore_restore(snapshot);
+  mc_model_checker->parent_snapshot = snapshot;
 }
 
 mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall)