src/mc/compare.cpp

   1 /* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 /** \file compare.cpp Memory snapshotting and comparison                    */
   7
   8 #include "src/mc/mc_config.hpp"
   9 #include "src/mc/mc_private.hpp"
  10 #include "src/mc/sosp/RemoteProcessMemory.hpp"
  11 #include "src/mc/sosp/Snapshot.hpp"
  12 #include "xbt/ex.h"
  13
  14 #include <algorithm>
  15
  16 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc, "Logging specific to mc_compare in mc");
  17
  18 namespace simgrid::mc {
  19
  20 /*********************************** Heap comparison ***********************************/
  21 /***************************************************************************************/
  22
  23 class HeapLocation {
  24 public:
  25   int block_    = 0;
  26   int fragment_ = 0;
  27
  28   HeapLocation() = default;
  29   explicit HeapLocation(int block, int fragment = 0) : block_(block), fragment_(fragment) {}
  30
  31   bool operator==(HeapLocation const& that) const
  32   {
  33     return block_ == that.block_ && fragment_ == that.fragment_;
  34   }
  35   bool operator<(HeapLocation const& that) const
  36   {
  37     return std::make_pair(block_, fragment_) < std::make_pair(that.block_, that.fragment_);
  38   }
  39 };
  40
  41 using HeapLocationPair  = std::array<HeapLocation, 2>;
  42 using HeapLocationPairs = std::set<HeapLocationPair>;
  43
  44 class HeapArea : public HeapLocation {
  45 public:
  46   bool valid_ = false;
  47   HeapArea() = default;
  48   explicit HeapArea(int block) : valid_(true) { block_ = block; }
  49   HeapArea(int block, int fragment) : valid_(true)
  50   {
  51     block_    = block;
  52     fragment_ = fragment;
  53   }
  54 };
  55
  56 class ProcessComparisonState {
  57 public:
  58   const std::vector<IgnoredHeapRegion>* to_ignore = nullptr;
  59   std::vector<HeapArea> equals_to;
  60   std::vector<Type*> types;
  61   std::size_t heapsize = 0;
  62
  63   void initHeapInformation(const s_xbt_mheap_t* heap, const std::vector<IgnoredHeapRegion>& i);
  64 };
  65
  66 class StateComparator {
  67 public:
  68   s_xbt_mheap_t std_heap_copy;
  69   std::size_t heaplimit;
  70   std::array<ProcessComparisonState, 2> processStates;
  71
  72   std::unordered_set<std::pair<const void*, const void*>, simgrid::xbt::hash<std::pair<const void*, const void*>>>
  73       compared_pointers;
  74
  75   void clear()
  76   {
  77     compared_pointers.clear();
  78   }
  79
  80   int initHeapInformation(RemoteProcessMemory& appli, const s_xbt_mheap_t* heap1, const s_xbt_mheap_t* heap2,
  81                           const std::vector<IgnoredHeapRegion>& i1, const std::vector<IgnoredHeapRegion>& i2);
  82
  83   template <int rank> HeapArea& equals_to_(std::size_t i, std::size_t j)
  84   {
  85     return processStates[rank - 1].equals_to[MAX_FRAGMENT_PER_BLOCK * i + j];
  86   }
  87   template <int rank> Type*& types_(std::size_t i, std::size_t j)
  88   {
  89     return processStates[rank - 1].types[MAX_FRAGMENT_PER_BLOCK * i + j];
  90   }
  91
  92   template <int rank> HeapArea const& equals_to_(std::size_t i, std::size_t j) const
  93   {
  94     return processStates[rank - 1].equals_to[MAX_FRAGMENT_PER_BLOCK * i + j];
  95   }
  96   template <int rank> Type* const& types_(std::size_t i, std::size_t j) const
  97   {
  98     return processStates[rank - 1].types[MAX_FRAGMENT_PER_BLOCK * i + j];
  99   }
 100
 101   /** Check whether two blocks are known to be matching
 102    *
 103    *  @param b1     Block of state 1
 104    *  @param b2     Block of state 2
 105    *  @return       if the blocks are known to be matching
 106    */
 107   bool blocksEqual(int b1, int b2) const
 108   {
 109     return this->equals_to_<1>(b1, 0).block_ == b2 && this->equals_to_<2>(b2, 0).block_ == b1;
 110   }
 111
 112   /** Check whether two fragments are known to be matching
 113    *
 114    *  @param b1     Block of state 1
 115    *  @param f1     Fragment of state 1
 116    *  @param b2     Block of state 2
 117    *  @param f2     Fragment of state 2
 118    *  @return       if the fragments are known to be matching
 119    */
 120   int fragmentsEqual(int b1, int f1, int b2, int f2) const
 121   {
 122     return this->equals_to_<1>(b1, f1).block_ == b2 && this->equals_to_<1>(b1, f1).fragment_ == f2 &&
 123            this->equals_to_<2>(b2, f2).block_ == b1 && this->equals_to_<2>(b2, f2).fragment_ == f1;
 124   }
 125
 126   void match_equals(const HeapLocationPairs* list);
 127 };
 128
 129 } // namespace simgrid::mc
 130
 131 /************************************************************************************/
 132
 133 static ssize_t heap_comparison_ignore_size(const std::vector<simgrid::mc::IgnoredHeapRegion>* ignore_list,
 134                                            const void* address)
 135 {
 136   auto pos = std::lower_bound(ignore_list->begin(), ignore_list->end(), address,
 137                               [](auto const& reg, auto const* addr) { return reg.address < addr; });
 138   return (pos != ignore_list->end() && pos->address == address) ? pos->size : -1;
 139 }
 140
 141 static bool is_stack(const simgrid::mc::RemoteProcessMemory& process, const void* address)
 142 {
 143   auto const& stack_areas = process.stack_areas();
 144   return std::any_of(stack_areas.begin(), stack_areas.end(),
 145                      [address](auto const& stack) { return stack.address == address; });
 146 }
 147
 148 // TODO, this should depend on the snapshot?
 149 static bool is_block_stack(const simgrid::mc::RemoteProcessMemory& process, int block)
 150 {
 151   auto const& stack_areas = process.stack_areas();
 152   return std::any_of(stack_areas.begin(), stack_areas.end(),
 153                      [block](auto const& stack) { return stack.block == block; });
 154 }
 155
 156 namespace simgrid::mc {
 157
 158 void StateComparator::match_equals(const HeapLocationPairs* list)
 159 {
 160   for (auto const& pair : *list) {
 161     if (pair[0].fragment_ != -1) {
 162       this->equals_to_<1>(pair[0].block_, pair[0].fragment_) = HeapArea(pair[1].block_, pair[1].fragment_);
 163       this->equals_to_<2>(pair[1].block_, pair[1].fragment_) = HeapArea(pair[0].block_, pair[0].fragment_);
 164     } else {
 165       this->equals_to_<1>(pair[0].block_, 0) = HeapArea(pair[1].block_, pair[1].fragment_);
 166       this->equals_to_<2>(pair[1].block_, 0) = HeapArea(pair[0].block_, pair[0].fragment_);
 167     }
 168   }
 169 }
 170
 171 void ProcessComparisonState::initHeapInformation(const s_xbt_mheap_t* heap, const std::vector<IgnoredHeapRegion>& i)
 172 {
 173   auto heaplimit  = heap->heaplimit;
 174   this->heapsize  = heap->heapsize;
 175   this->to_ignore = &i;
 176   this->equals_to.assign(heaplimit * MAX_FRAGMENT_PER_BLOCK, HeapArea());
 177   this->types.assign(heaplimit * MAX_FRAGMENT_PER_BLOCK, nullptr);
 178 }
 179
 180 int StateComparator::initHeapInformation(simgrid::mc::RemoteProcessMemory& memory, const s_xbt_mheap_t* heap1,
 181                                          const s_xbt_mheap_t* heap2, const std::vector<IgnoredHeapRegion>& i1,
 182                                          const std::vector<IgnoredHeapRegion>& i2)
 183 {
 184   if ((heap1->heaplimit != heap2->heaplimit) || (heap1->heapsize != heap2->heapsize))
 185     return -1;
 186   this->heaplimit     = heap1->heaplimit;
 187   this->std_heap_copy = *memory.get_heap();
 188   this->processStates[0].initHeapInformation(heap1, i1);
 189   this->processStates[1].initHeapInformation(heap2, i2);
 190   return 0;
 191 }
 192
 193 // TODO, have a robust way to find it in O(1)
 194 static inline Region* MC_get_heap_region(const Snapshot& snapshot)
 195 {
 196   for (auto const& region : snapshot.snapshot_regions_)
 197     if (region->region_type() == RegionType::Heap)
 198       return region.get();
 199   xbt_die("No heap region");
 200 }
 201
 202 static bool heap_area_differ(const RemoteProcessMemory& process, StateComparator& state, const void* area1,
 203                              const void* area2, const Snapshot& snapshot1, const Snapshot& snapshot2,
 204                              HeapLocationPairs* previous, Type* type, int pointer_level);
 205
 206 /* Compares the content of each heap fragment between the two states, at the bit level.
 207  *
 208  * This operation is costly (about 5 seconds per snapshots' pair to compare on a small program),
 209  * but hard to optimize because our algorithm is too hackish.
 210  *
 211  * Going at bit level can trigger syntaxtic differences on states that are semantically equivalent.
 212  *
 213  * Padding bytes constitute the first source of such syntaxtic difference: Any malloced memory contains spaces that
 214  * are not used to enforce the memory alignment constraints of the CPU. So, cruft of irrelevant changes could get
 215  * added on these bits. But this case is handled properly, as any memory block is zeroed by mmalloc before being handled
 216  * back, not only for calloc but also for malloc. So the memory interstices due to padding bytes are properly zeroed.
 217  *
 218  * Another source of such change comes from the order of mallocs, that may well change from one execution path to
 219  * another. This will change the malloc fragment in which the data is stored and the pointer values (syntaxtic
 220  * difference) while the semantic of the state remains the same.
 221  *
 222  * To fix this, this code relies on a hugly hack. When we see a difference during the bit-level comparison,
 223  * we first check if it could be explained by a pointer-to-block difference. Ie, if when interpreting the memory
 224  * area containing that difference as a pointer, I get the pointer to a valid fragment in the heap (in both snapshots).
 225  *
 226  * This is why we cannot pre-compute a bit-level hash of the heap content: we discover the pointers to other memory
 227  * fragment when a difference is found during the bit-level exploration. Fixing this would require to save typing
 228  * information about the memory fragments, which is something that could be done with https://github.com/tudasc/TypeART
 229  * This would give us all pointers in the mallocated memory, allowing the graph traversal needed to precompute the hash.
 230  *
 231  * Using a hash without paying attention to malloc fragment reordering would lead to false negatives:
 232  * semantically equivalent states would be detected as [syntaxically] different. It's of no importance for the
 233  * state-equality reduction (we would re-explore semantically equivalent states), but it would endanger the soundness
 234  * of the liveness model-checker, as state-equality is used to detect the loops that constitute the accepting states of
 235  * the verified property. So we could miss counter-examples to the verified property. Not good. Not good at all.
 236  */
 237 static bool mmalloc_heap_differ(const RemoteProcessMemory& process, StateComparator& state, const Snapshot& snapshot1,
 238                                 const Snapshot& snapshot2)
 239 {
 240   /* Check busy blocks */
 241   size_t i1 = 1;
 242
 243   malloc_info heapinfo_temp1;
 244   malloc_info heapinfo_temp2;
 245   malloc_info heapinfo_temp2b;
 246
 247   const Region* heap_region1 = MC_get_heap_region(snapshot1);
 248   const Region* heap_region2 = MC_get_heap_region(snapshot2);
 249
 250   // This is the address of std_heap->heapinfo in the application process:
 251   uint64_t heapinfo_address = process.heap_address.address() + offsetof(s_xbt_mheap_t, heapinfo);
 252
 253   // This is in snapshot do not use them directly:
 254   const malloc_info* heapinfos1 = snapshot1.read(remote<malloc_info*>(heapinfo_address));
 255   const malloc_info* heapinfos2 = snapshot2.read(remote<malloc_info*>(heapinfo_address));
 256
 257   while (i1 < state.heaplimit) {
 258     const auto* heapinfo1 =
 259         static_cast<malloc_info*>(heap_region1->read(&heapinfo_temp1, &heapinfos1[i1], sizeof(malloc_info)));
 260     const auto* heapinfo2 =
 261         static_cast<malloc_info*>(heap_region2->read(&heapinfo_temp2, &heapinfos2[i1], sizeof(malloc_info)));
 262
 263     if (heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type == MMALLOC_TYPE_HEAPINFO) {      /* Free block */
 264       i1 ++;
 265       continue;
 266     }
 267
 268     xbt_assert(heapinfo1->type >= 0, "Unknown mmalloc block type: %d", heapinfo1->type);
 269
 270     void* addr_block1 = (ADDR2UINT(i1) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
 271
 272     if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED) { /* Large block */
 273       if (is_stack(process, addr_block1)) {
 274         for (size_t k = 0; k < heapinfo1->busy_block.size; k++)
 275           state.equals_to_<1>(i1 + k, 0) = HeapArea(i1, -1);
 276         for (size_t k = 0; k < heapinfo2->busy_block.size; k++)
 277           state.equals_to_<2>(i1 + k, 0) = HeapArea(i1, -1);
 278         i1 += heapinfo1->busy_block.size;
 279         continue;
 280       }
 281
 282       if (state.equals_to_<1>(i1, 0).valid_) {
 283         i1++;
 284         continue;
 285       }
 286
 287       size_t i2 = 1;
 288       bool equal = false;
 289
 290       /* Try first to associate to same block in the other heap */
 291       if (heapinfo2->type == heapinfo1->type && state.equals_to_<2>(i1, 0).valid_ == 0) {
 292         const void* addr_block2 = (ADDR2UINT(i1) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
 293         if (not heap_area_differ(process, state, addr_block1, addr_block2, snapshot1, snapshot2, nullptr, nullptr, 0)) {
 294           for (size_t k = 1; k < heapinfo2->busy_block.size; k++)
 295             state.equals_to_<2>(i1 + k, 0) = HeapArea(i1, -1);
 296           for (size_t k = 1; k < heapinfo1->busy_block.size; k++)
 297             state.equals_to_<1>(i1 + k, 0) = HeapArea(i1, -1);
 298           equal = true;
 299           i1 += heapinfo1->busy_block.size;
 300         }
 301       }
 302
 303       while (i2 < state.heaplimit && not equal) {
 304         const void* addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
 305
 306         if (i2 == i1) {
 307           i2++;
 308           continue;
 309         }
 310
 311         const auto* heapinfo2b =
 312             static_cast<malloc_info*>(heap_region2->read(&heapinfo_temp2b, &heapinfos2[i2], sizeof(malloc_info)));
 313
 314         if (heapinfo2b->type != MMALLOC_TYPE_UNFRAGMENTED) {
 315           i2++;
 316           continue;
 317         }
 318
 319         if (state.equals_to_<2>(i2, 0).valid_) {
 320           i2++;
 321           continue;
 322         }
 323
 324         if (not heap_area_differ(process, state, addr_block1, addr_block2, snapshot1, snapshot2, nullptr, nullptr, 0)) {
 325           for (size_t k = 1; k < heapinfo2b->busy_block.size; k++)
 326             state.equals_to_<2>(i2 + k, 0) = HeapArea(i1, -1);
 327           for (size_t k = 1; k < heapinfo1->busy_block.size; k++)
 328             state.equals_to_<1>(i1 + k, 0) = HeapArea(i2, -1);
 329           equal = true;
 330           i1 += heapinfo1->busy_block.size;
 331         }
 332         i2++;
 333       }
 334
 335       if (not equal) {
 336         XBT_DEBUG("Block %zu not found (size_used = %zu, addr = %p)", i1, heapinfo1->busy_block.busy_size, addr_block1);
 337         return true;
 338       }
 339     } else { /* Fragmented block */
 340       for (size_t j1 = 0; j1 < (size_t)(BLOCKSIZE >> heapinfo1->type); j1++) {
 341         if (heapinfo1->busy_frag.frag_size[j1] == -1) /* Free fragment_ */
 342           continue;
 343
 344         if (state.equals_to_<1>(i1, j1).valid_)
 345           continue;
 346
 347         void* addr_frag1 = (char*)addr_block1 + (j1 << heapinfo1->type);
 348
 349         size_t i2 = 1;
 350         bool equal = false;
 351
 352         /* Try first to associate to same fragment_ in the other heap */
 353         if (heapinfo2->type == heapinfo1->type && not state.equals_to_<2>(i1, j1).valid_) {
 354           const void* addr_block2 = (ADDR2UINT(i1) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
 355           const void* addr_frag2  = (const char*)addr_block2 + (j1 << heapinfo2->type);
 356           if (not heap_area_differ(process, state, addr_frag1, addr_frag2, snapshot1, snapshot2, nullptr, nullptr, 0))
 357             equal = true;
 358         }
 359
 360         while (i2 < state.heaplimit && not equal) {
 361           const auto* heapinfo2b =
 362               static_cast<malloc_info*>(heap_region2->read(&heapinfo_temp2b, &heapinfos2[i2], sizeof(malloc_info)));
 363
 364           if (heapinfo2b->type == MMALLOC_TYPE_FREE || heapinfo2b->type == MMALLOC_TYPE_HEAPINFO) {
 365             i2 ++;
 366             continue;
 367           }
 368
 369           // We currently do not match fragments with unfragmented blocks (maybe we should).
 370           if (heapinfo2b->type == MMALLOC_TYPE_UNFRAGMENTED) {
 371             i2++;
 372             continue;
 373           }
 374
 375           xbt_assert(heapinfo2b->type >= 0, "Unknown mmalloc block type: %d", heapinfo2b->type);
 376
 377           for (size_t j2 = 0; j2 < (size_t)(BLOCKSIZE >> heapinfo2b->type); j2++) {
 378             if (i2 == i1 && j2 == j1)
 379               continue;
 380
 381             if (state.equals_to_<2>(i2, j2).valid_)
 382               continue;
 383
 384             const void* addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
 385             const void* addr_frag2  = (const char*)addr_block2 + (j2 << heapinfo2b->type);
 386
 387             if (not heap_area_differ(process, state, addr_frag1, addr_frag2, snapshot1, snapshot2, nullptr, nullptr,
 388                                      0)) {
 389               equal = true;
 390               break;
 391             }
 392           }
 393           i2++;
 394         }
 395
 396         if (not equal) {
 397           XBT_DEBUG("Block %zu, fragment_ %zu not found (size_used = %zd, address = %p)\n", i1, j1,
 398                     heapinfo1->busy_frag.frag_size[j1], addr_frag1);
 399           return true;
 400         }
 401       }
 402       i1++;
 403     }
 404   }
 405
 406   /* All blocks/fragments are equal to another block/fragment_ ? */
 407   for (size_t i = 1; i < state.heaplimit; i++) {
 408     const auto* heapinfo1 =
 409         static_cast<malloc_info*>(heap_region1->read(&heapinfo_temp1, &heapinfos1[i], sizeof(malloc_info)));
 410
 411     if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED && i1 == state.heaplimit && heapinfo1->busy_block.busy_size > 0 &&
 412         not state.equals_to_<1>(i, 0).valid_) {
 413       XBT_DEBUG("Block %zu not found (size used = %zu)", i, heapinfo1->busy_block.busy_size);
 414       return true;
 415     }
 416
 417     if (heapinfo1->type <= 0)
 418       continue;
 419     for (size_t j = 0; j < (size_t)(BLOCKSIZE >> heapinfo1->type); j++)
 420       if (i1 == state.heaplimit && heapinfo1->busy_frag.frag_size[j] > 0 && not state.equals_to_<1>(i, j).valid_) {
 421         XBT_DEBUG("Block %zu, Fragment %zu not found (size used = %zd)", i, j, heapinfo1->busy_frag.frag_size[j]);
 422         return true;
 423       }
 424   }
 425
 426   for (size_t i = 1; i < state.heaplimit; i++) {
 427     const auto* heapinfo2 =
 428         static_cast<malloc_info*>(heap_region2->read(&heapinfo_temp2, &heapinfos2[i], sizeof(malloc_info)));
 429     if (heapinfo2->type == MMALLOC_TYPE_UNFRAGMENTED && i1 == state.heaplimit && heapinfo2->busy_block.busy_size > 0 &&
 430         not state.equals_to_<2>(i, 0).valid_) {
 431       XBT_DEBUG("Block %zu not found (size used = %zu)", i,
 432                 heapinfo2->busy_block.busy_size);
 433       return true;
 434     }
 435
 436     if (heapinfo2->type <= 0)
 437       continue;
 438
 439     for (size_t j = 0; j < (size_t)(BLOCKSIZE >> heapinfo2->type); j++)
 440       if (i1 == state.heaplimit && heapinfo2->busy_frag.frag_size[j] > 0 && not state.equals_to_<2>(i, j).valid_) {
 441         XBT_DEBUG("Block %zu, Fragment %zu not found (size used = %zd)",
 442           i, j, heapinfo2->busy_frag.frag_size[j]);
 443         return true;
 444       }
 445   }
 446   return false;
 447 }
 448
 449 /**
 450  *
 451  * @param state
 452  * @param real_area1     Process address for state 1
 453  * @param real_area2     Process address for state 2
 454  * @param snapshot1      Snapshot of state 1
 455  * @param snapshot2      Snapshot of state 2
 456  * @param previous
 457  * @param size
 458  * @param check_ignore
 459  * @return true when different, false otherwise (same or unknown)
 460  */
 461 static bool heap_area_differ_without_type(const RemoteProcessMemory& process, StateComparator& state,
 462                                           const void* real_area1, const void* real_area2, const Snapshot& snapshot1,
 463                                           const Snapshot& snapshot2, HeapLocationPairs* previous, int size,
 464                                           int check_ignore)
 465 {
 466   const Region* heap_region1  = MC_get_heap_region(snapshot1);
 467   const Region* heap_region2  = MC_get_heap_region(snapshot2);
 468
 469   for (int i = 0; i < size; ) {
 470     if (check_ignore > 0) {
 471       ssize_t ignore1 = heap_comparison_ignore_size(state.processStates[0].to_ignore, (const char*)real_area1 + i);
 472       if (ignore1 != -1) {
 473         ssize_t ignore2 = heap_comparison_ignore_size(state.processStates[1].to_ignore, (const char*)real_area2 + i);
 474         if (ignore2 == ignore1) {
 475           if (ignore1 == 0) {
 476             return false;
 477           } else {
 478             i = i + ignore2;
 479             check_ignore--;
 480             continue;
 481           }
 482         }
 483       }
 484     }
 485
 486     if (MC_snapshot_region_memcmp((const char*)real_area1 + i, heap_region1, (const char*)real_area2 + i, heap_region2,
 487                                   1) != 0) {
 488       int pointer_align = (i / sizeof(void *)) * sizeof(void *);
 489       const void* addr_pointed1 = snapshot1.read(remote((void* const*)((const char*)real_area1 + pointer_align)));
 490       const void* addr_pointed2 = snapshot2.read(remote((void* const*)((const char*)real_area2 + pointer_align)));
 491
 492       if (process.in_maestro_stack(remote(addr_pointed1)) && process.in_maestro_stack(remote(addr_pointed2))) {
 493         i = pointer_align + sizeof(void *);
 494         continue;
 495       }
 496
 497       if (snapshot1.on_heap(addr_pointed1) && snapshot2.on_heap(addr_pointed2)) {
 498         // Both addresses are in the heap:
 499         if (heap_area_differ(process, state, addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous, nullptr, 0))
 500           return true;
 501         i = pointer_align + sizeof(void *);
 502         continue;
 503       }
 504       return true;
 505     }
 506     i++;
 507   }
 508   return false;
 509 }
 510
 511 /**
 512  *
 513  * @param state
 514  * @param real_area1     Process address for state 1
 515  * @param real_area2     Process address for state 2
 516  * @param snapshot1      Snapshot of state 1
 517  * @param snapshot2      Snapshot of state 2
 518  * @param previous
 519  * @param type
 520  * @param area_size      either a byte_size or an elements_count (?)
 521  * @param check_ignore
 522  * @param pointer_level
 523  * @return               true when different, false otherwise (same or unknown)
 524  */
 525 static bool heap_area_differ_with_type(const simgrid::mc::RemoteProcessMemory& process, StateComparator& state,
 526                                        const void* real_area1, const void* real_area2, const Snapshot& snapshot1,
 527                                        const Snapshot& snapshot2, HeapLocationPairs* previous, const Type* type,
 528                                        int area_size, int check_ignore, int pointer_level)
 529 {
 530   // HACK: This should not happen but in practice, there are some
 531   // DW_TAG_typedef without an associated DW_AT_type:
 532   //<1><538832>: Abbrev Number: 111 (DW_TAG_typedef)
 533   //    <538833>   DW_AT_name        : (indirect string, offset: 0x2292f3): gregset_t
 534   //    <538837>   DW_AT_decl_file   : 98
 535   //    <538838>   DW_AT_decl_line   : 37
 536   if (type == nullptr)
 537     return false;
 538
 539   if (is_stack(process, real_area1) && is_stack(process, real_area2))
 540     return false;
 541
 542   if (check_ignore > 0) {
 543     ssize_t ignore1 = heap_comparison_ignore_size(state.processStates[0].to_ignore, real_area1);
 544     if (ignore1 > 0 && heap_comparison_ignore_size(state.processStates[1].to_ignore, real_area2) == ignore1)
 545       return false;
 546   }
 547
 548   const Type* subtype;
 549   const Type* subsubtype;
 550   int elm_size;
 551   const void* addr_pointed1;
 552   const void* addr_pointed2;
 553
 554   const Region* heap_region1 = MC_get_heap_region(snapshot1);
 555   const Region* heap_region2 = MC_get_heap_region(snapshot2);
 556
 557   switch (type->type) {
 558     case DW_TAG_unspecified_type:
 559       return true;
 560
 561     case DW_TAG_base_type:
 562       if (not type->name.empty() && type->name == "char") { /* String, hence random (arbitrary ?) size */
 563         if (real_area1 == real_area2)
 564           return false;
 565         else
 566           return MC_snapshot_region_memcmp(real_area1, heap_region1, real_area2, heap_region2, area_size) != 0;
 567       } else {
 568         if (area_size != -1 && type->byte_size != area_size)
 569           return false;
 570         else
 571           return MC_snapshot_region_memcmp(real_area1, heap_region1, real_area2, heap_region2, type->byte_size) != 0;
 572       }
 573
 574     case DW_TAG_enumeration_type:
 575       if (area_size != -1 && type->byte_size != area_size)
 576         return false;
 577       return MC_snapshot_region_memcmp(real_area1, heap_region1, real_area2, heap_region2, type->byte_size) != 0;
 578
 579     case DW_TAG_typedef:
 580     case DW_TAG_const_type:
 581     case DW_TAG_volatile_type:
 582       return heap_area_differ_with_type(process, state, real_area1, real_area2, snapshot1, snapshot2, previous,
 583                                         type->subtype, area_size, check_ignore, pointer_level);
 584
 585     case DW_TAG_array_type:
 586       subtype = type->subtype;
 587       switch (subtype->type) {
 588         case DW_TAG_unspecified_type:
 589           return true;
 590
 591         case DW_TAG_base_type:
 592         case DW_TAG_enumeration_type:
 593         case DW_TAG_pointer_type:
 594         case DW_TAG_reference_type:
 595         case DW_TAG_rvalue_reference_type:
 596         case DW_TAG_structure_type:
 597         case DW_TAG_class_type:
 598         case DW_TAG_union_type:
 599           if (subtype->full_type)
 600             subtype = subtype->full_type;
 601           elm_size  = subtype->byte_size;
 602           break;
 603         // TODO, just remove the type indirection?
 604         case DW_TAG_const_type:
 605         case DW_TAG_typedef:
 606         case DW_TAG_volatile_type:
 607           subsubtype = subtype->subtype;
 608           if (subsubtype->full_type)
 609             subsubtype = subsubtype->full_type;
 610           elm_size     = subsubtype->byte_size;
 611           break;
 612         default:
 613           return false;
 614       }
 615       for (int i = 0; i < type->element_count; i++) {
 616         // TODO, add support for variable stride (DW_AT_byte_stride)
 617         if (heap_area_differ_with_type(process, state, (const char*)real_area1 + (i * elm_size),
 618                                        (const char*)real_area2 + (i * elm_size), snapshot1, snapshot2, previous,
 619                                        type->subtype, subtype->byte_size, check_ignore, pointer_level))
 620           return true;
 621       }
 622       return false;
 623
 624     case DW_TAG_reference_type:
 625     case DW_TAG_rvalue_reference_type:
 626     case DW_TAG_pointer_type:
 627       if (type->subtype && type->subtype->type == DW_TAG_subroutine_type) {
 628         addr_pointed1 = snapshot1.read(remote((void* const*)real_area1));
 629         addr_pointed2 = snapshot2.read(remote((void* const*)real_area2));
 630         return (addr_pointed1 != addr_pointed2);
 631       }
 632       pointer_level++;
 633       if (pointer_level <= 1) {
 634         addr_pointed1 = snapshot1.read(remote((void* const*)real_area1));
 635         addr_pointed2 = snapshot2.read(remote((void* const*)real_area2));
 636         if (snapshot1.on_heap(addr_pointed1) && snapshot2.on_heap(addr_pointed2))
 637           return heap_area_differ(process, state, addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous,
 638                                   type->subtype, pointer_level);
 639         else
 640           return (addr_pointed1 != addr_pointed2);
 641       }
 642       for (size_t i = 0; i < (area_size / sizeof(void*)); i++) {
 643         addr_pointed1 = snapshot1.read(remote((void* const*)((const char*)real_area1 + i * sizeof(void*))));
 644         addr_pointed2 = snapshot2.read(remote((void* const*)((const char*)real_area2 + i * sizeof(void*))));
 645         bool differ   = snapshot1.on_heap(addr_pointed1) && snapshot2.on_heap(addr_pointed2)
 646                             ? heap_area_differ(process, state, addr_pointed1, addr_pointed2, snapshot1, snapshot2,
 647                                              previous, type->subtype, pointer_level)
 648                             : addr_pointed1 != addr_pointed2;
 649         if (differ)
 650           return true;
 651       }
 652       return false;
 653
 654     case DW_TAG_structure_type:
 655     case DW_TAG_class_type:
 656       if (type->full_type)
 657         type = type->full_type;
 658       if (type->byte_size == 0)
 659         return false;
 660       if (area_size != -1 && type->byte_size != area_size) {
 661         if (area_size <= type->byte_size || area_size % type->byte_size != 0)
 662           return false;
 663         for (size_t i = 0; i < (size_t)(area_size / type->byte_size); i++) {
 664           if (heap_area_differ_with_type(process, state, (const char*)real_area1 + i * type->byte_size,
 665                                          (const char*)real_area2 + i * type->byte_size, snapshot1, snapshot2, previous,
 666                                          type, -1, check_ignore, 0))
 667             return true;
 668         }
 669         } else {
 670           for (const simgrid::mc::Member& member : type->members) {
 671             // TODO, optimize this? (for the offset case)
 672             const void* real_member1 = dwarf::resolve_member(real_area1, type, &member, &snapshot1);
 673             const void* real_member2 = dwarf::resolve_member(real_area2, type, &member, &snapshot2);
 674             if (heap_area_differ_with_type(process, state, real_member1, real_member2, snapshot1, snapshot2, previous,
 675                                            member.type, -1, check_ignore, 0))
 676               return true;
 677           }
 678         }
 679         return false;
 680
 681     case DW_TAG_union_type:
 682       return heap_area_differ_without_type(process, state, real_area1, real_area2, snapshot1, snapshot2, previous,
 683                                            type->byte_size, check_ignore);
 684
 685     default:
 686       THROW_IMPOSSIBLE;
 687   }
 688 }
 689
 690 /** Infer the type of a part of the block from the type of the block
 691  *
 692  * TODO, handle DW_TAG_array_type as well as arrays of the object ((*p)[5], p[5])
 693  *
 694  * TODO, handle subfields ((*p).bar.foo, (*p)[5].bar…)
 695  *
 696  * @param  type               DWARF type ID of the root address
 697  * @param  area_size
 698  * @return                    DWARF type ID for given offset
 699  */
 700 static Type* get_offset_type(void* real_base_address, Type* type, int offset, int area_size, const Snapshot& snapshot)
 701 {
 702   // Beginning of the block, the inferred variable type if the type of the block:
 703   if (offset == 0)
 704     return type;
 705
 706   switch (type->type) {
 707   case DW_TAG_structure_type:
 708   case DW_TAG_class_type:
 709     if (type->full_type)
 710       type = type->full_type;
 711     if (area_size != -1 && type->byte_size != area_size) {
 712       if (area_size > type->byte_size && area_size % type->byte_size == 0)
 713         return type;
 714       else
 715         return nullptr;
 716     }
 717
 718     for (const simgrid::mc::Member& member : type->members) {
 719       if (member.has_offset_location()) {
 720         // We have the offset, use it directly (shortcut):
 721         if (member.offset() == offset)
 722           return member.type;
 723       } else {
 724         void* real_member = dwarf::resolve_member(real_base_address, type, &member, &snapshot);
 725         if ((char*)real_member - (char*)real_base_address == offset)
 726           return member.type;
 727       }
 728     }
 729     return nullptr;
 730
 731   default:
 732     /* FIXME: other cases ? */
 733     return nullptr;
 734   }
 735 }
 736
 737 /**
 738  *
 739  * @param area1          Process address for state 1
 740  * @param area2          Process address for state 2
 741  * @param snapshot1      Snapshot of state 1
 742  * @param snapshot2      Snapshot of state 2
 743  * @param previous       Pairs of blocks already compared on the current path (or nullptr)
 744  * @param type_id        Type of variable
 745  * @param pointer_level
 746  * @return true when different, false otherwise (same or unknown)
 747  */
 748 static bool heap_area_differ(const RemoteProcessMemory& process, StateComparator& state, const void* area1,
 749                              const void* area2, const Snapshot& snapshot1, const Snapshot& snapshot2,
 750                              HeapLocationPairs* previous, Type* type, int pointer_level)
 751 {
 752   ssize_t block1;
 753   ssize_t block2;
 754   ssize_t size;
 755   int check_ignore = 0;
 756
 757   int type_size = -1;
 758   int offset1   = 0;
 759   int offset2   = 0;
 760   int new_size1 = -1;
 761   int new_size2 = -1;
 762
 763   Type* new_type1 = nullptr;
 764
 765   bool match_pairs = false;
 766
 767   // This is the address of std_heap->heapinfo in the application process:
 768   uint64_t heapinfo_address = process.heap_address.address() + offsetof(s_xbt_mheap_t, heapinfo);
 769
 770   const malloc_info* heapinfos1 = snapshot1.read(remote<malloc_info*>(heapinfo_address));
 771   const malloc_info* heapinfos2 = snapshot2.read(remote<malloc_info*>(heapinfo_address));
 772
 773   malloc_info heapinfo_temp1;
 774   malloc_info heapinfo_temp2;
 775
 776   simgrid::mc::HeapLocationPairs current;
 777   if (previous == nullptr) {
 778     previous = &current;
 779     match_pairs = true;
 780   }
 781
 782   // Get block number:
 783   block1 = ((const char*)area1 - (const char*)state.std_heap_copy.heapbase) / BLOCKSIZE + 1;
 784   block2 = ((const char*)area2 - (const char*)state.std_heap_copy.heapbase) / BLOCKSIZE + 1;
 785
 786   // If either block is a stack block:
 787   if (is_block_stack(process, (int)block1) && is_block_stack(process, (int)block2)) {
 788     previous->insert(HeapLocationPair{{HeapLocation(block1, -1), HeapLocation(block2, -1)}});
 789     if (match_pairs)
 790       state.match_equals(previous);
 791     return false;
 792   }
 793
 794   // If either block is not in the expected area of memory:
 795   if (((const char*)area1 < (const char*)state.std_heap_copy.heapbase) ||
 796       (block1 > (ssize_t)state.processStates[0].heapsize) ||
 797       ((const char*)area2 < (const char*)state.std_heap_copy.heapbase) ||
 798       (block2 > (ssize_t)state.processStates[1].heapsize)) {
 799     return true;
 800   }
 801
 802   // Process address of the block:
 803   void* real_addr_block1 = (ADDR2UINT(block1) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
 804   void* real_addr_block2 = (ADDR2UINT(block2) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
 805
 806   if (type) {
 807     if (type->full_type)
 808       type = type->full_type;
 809
 810     // This assume that for "boring" types (volatile ...) byte_size is absent:
 811     while (type->byte_size == 0 && type->subtype != nullptr)
 812       type = type->subtype;
 813
 814     // Find type_size:
 815     if (type->type == DW_TAG_pointer_type ||
 816         (type->type == DW_TAG_base_type && not type->name.empty() && type->name == "char"))
 817       type_size = -1;
 818     else
 819       type_size = type->byte_size;
 820   }
 821
 822   const Region* heap_region1 = MC_get_heap_region(snapshot1);
 823   const Region* heap_region2 = MC_get_heap_region(snapshot2);
 824
 825   const auto* heapinfo1 =
 826       static_cast<malloc_info*>(heap_region1->read(&heapinfo_temp1, &heapinfos1[block1], sizeof(malloc_info)));
 827   const auto* heapinfo2 =
 828       static_cast<malloc_info*>(heap_region2->read(&heapinfo_temp2, &heapinfos2[block2], sizeof(malloc_info)));
 829
 830   if ((heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type==MMALLOC_TYPE_HEAPINFO)
 831     && (heapinfo2->type == MMALLOC_TYPE_FREE || heapinfo2->type ==MMALLOC_TYPE_HEAPINFO)) {
 832     /* Free block */
 833     if (match_pairs)
 834       state.match_equals(previous);
 835     return false;
 836   }
 837
 838   if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED && heapinfo2->type == MMALLOC_TYPE_UNFRAGMENTED) {
 839     /* Complete block */
 840
 841     // TODO, lookup variable type from block type as done for fragmented blocks
 842
 843     if (state.equals_to_<1>(block1, 0).valid_ && state.equals_to_<2>(block2, 0).valid_ &&
 844         state.blocksEqual(block1, block2)) {
 845       if (match_pairs)
 846         state.match_equals(previous);
 847       return false;
 848     }
 849
 850     if (type_size != -1 && type_size != (ssize_t)heapinfo1->busy_block.busy_size &&
 851         type_size != (ssize_t)heapinfo2->busy_block.busy_size && type->name.empty()) {
 852       if (match_pairs)
 853         state.match_equals(previous);
 854       return false;
 855     }
 856
 857     if (heapinfo1->busy_block.size != heapinfo2->busy_block.size ||
 858         heapinfo1->busy_block.busy_size != heapinfo2->busy_block.busy_size)
 859       return true;
 860
 861     if (not previous->insert(HeapLocationPair{{HeapLocation(block1, -1), HeapLocation(block2, -1)}}).second) {
 862       if (match_pairs)
 863         state.match_equals(previous);
 864       return false;
 865     }
 866
 867     size = heapinfo1->busy_block.busy_size;
 868
 869     // Remember (basic) type inference.
 870     // The current data structure only allows us to do this for the whole block.
 871     if (type != nullptr && area1 == real_addr_block1)
 872       state.types_<1>(block1, 0) = type;
 873     if (type != nullptr && area2 == real_addr_block2)
 874       state.types_<2>(block2, 0) = type;
 875
 876     if (size <= 0) {
 877       if (match_pairs)
 878         state.match_equals(previous);
 879       return false;
 880     }
 881
 882     if (heapinfo1->busy_block.ignore > 0 && heapinfo2->busy_block.ignore == heapinfo1->busy_block.ignore)
 883       check_ignore = heapinfo1->busy_block.ignore;
 884
 885   } else if ((heapinfo1->type > 0) && (heapinfo2->type > 0)) {      /* Fragmented block */
 886     // Fragment number:
 887     ssize_t frag1 = (ADDR2UINT(area1) % BLOCKSIZE) >> heapinfo1->type;
 888     ssize_t frag2 = (ADDR2UINT(area2) % BLOCKSIZE) >> heapinfo2->type;
 889
 890     // Process address of the fragment_:
 891     void* real_addr_frag1 = (char*)real_addr_block1 + (frag1 << heapinfo1->type);
 892     void* real_addr_frag2 = (char*)real_addr_block2 + (frag2 << heapinfo2->type);
 893
 894     // Check the size of the fragments against the size of the type:
 895     if (type_size != -1) {
 896       if (heapinfo1->busy_frag.frag_size[frag1] == -1 || heapinfo2->busy_frag.frag_size[frag2] == -1) {
 897         if (match_pairs)
 898           state.match_equals(previous);
 899         return false;
 900       }
 901       // ?
 902       if (type_size != heapinfo1->busy_frag.frag_size[frag1]
 903           || type_size != heapinfo2->busy_frag.frag_size[frag2]) {
 904         if (match_pairs)
 905           state.match_equals(previous);
 906         return false;
 907       }
 908     }
 909
 910     // Check if the blocks are already matched together:
 911     if (state.equals_to_<1>(block1, frag1).valid_ && state.equals_to_<2>(block2, frag2).valid_ &&
 912         state.fragmentsEqual(block1, frag1, block2, frag2)) {
 913       if (match_pairs)
 914         state.match_equals(previous);
 915       return false;
 916     }
 917     // Compare the size of both fragments:
 918     if (heapinfo1->busy_frag.frag_size[frag1] != heapinfo2->busy_frag.frag_size[frag2]) {
 919       if (type_size == -1) {
 920         if (match_pairs)
 921           state.match_equals(previous);
 922         return false;
 923       } else
 924         return true;
 925     }
 926
 927     // Size of the fragment_:
 928     size = heapinfo1->busy_frag.frag_size[frag1];
 929
 930     // Remember (basic) type inference.
 931     // The current data structure only allows us to do this for the whole fragment_.
 932     if (type != nullptr && area1 == real_addr_frag1)
 933       state.types_<1>(block1, frag1) = type;
 934     if (type != nullptr && area2 == real_addr_frag2)
 935       state.types_<2>(block2, frag2) = type;
 936
 937     // The type of the variable is already known:
 938     if (type) {
 939       new_type1 = type;
 940     }
 941     // Type inference from the block type.
 942     else if (state.types_<1>(block1, frag1) != nullptr || state.types_<2>(block2, frag2) != nullptr) {
 943       Type* new_type2 = nullptr;
 944
 945       offset1 = (const char*)area1 - (const char*)real_addr_frag1;
 946       offset2 = (const char*)area2 - (const char*)real_addr_frag2;
 947
 948       if (state.types_<1>(block1, frag1) != nullptr && state.types_<2>(block2, frag2) != nullptr) {
 949         new_type1 = get_offset_type(real_addr_frag1, state.types_<1>(block1, frag1), offset1, size, snapshot1);
 950         new_type2 = get_offset_type(real_addr_frag2, state.types_<2>(block2, frag2), offset1, size, snapshot2);
 951       } else if (state.types_<1>(block1, frag1) != nullptr) {
 952         new_type1 = get_offset_type(real_addr_frag1, state.types_<1>(block1, frag1), offset1, size, snapshot1);
 953         new_type2 = get_offset_type(real_addr_frag2, state.types_<1>(block1, frag1), offset2, size, snapshot2);
 954       } else if (state.types_<2>(block2, frag2) != nullptr) {
 955         new_type1 = get_offset_type(real_addr_frag1, state.types_<2>(block2, frag2), offset1, size, snapshot1);
 956         new_type2 = get_offset_type(real_addr_frag2, state.types_<2>(block2, frag2), offset2, size, snapshot2);
 957       } else {
 958         if (match_pairs)
 959           state.match_equals(previous);
 960         return false;
 961       }
 962
 963       if (new_type1 != nullptr && new_type2 != nullptr && new_type1 != new_type2) {
 964         type = new_type1;
 965         while (type->byte_size == 0 && type->subtype != nullptr)
 966           type = type->subtype;
 967         new_size1 = type->byte_size;
 968
 969         type = new_type2;
 970         while (type->byte_size == 0 && type->subtype != nullptr)
 971           type = type->subtype;
 972         new_size2 = type->byte_size;
 973
 974       } else {
 975         if (match_pairs)
 976           state.match_equals(previous);
 977         return false;
 978       }
 979     }
 980
 981     if (new_size1 > 0 && new_size1 == new_size2) {
 982       type = new_type1;
 983       size = new_size1;
 984     }
 985
 986     if (offset1 == 0 && offset2 == 0 &&
 987         not previous->insert(HeapLocationPair{{HeapLocation(block1, frag1), HeapLocation(block2, frag2)}}).second) {
 988       if (match_pairs)
 989         state.match_equals(previous);
 990       return false;
 991     }
 992
 993     if (size <= 0) {
 994       if (match_pairs)
 995         state.match_equals(previous);
 996       return false;
 997     }
 998
 999     if ((heapinfo1->busy_frag.ignore[frag1] > 0) &&
1000         (heapinfo2->busy_frag.ignore[frag2] == heapinfo1->busy_frag.ignore[frag1]))
1001       check_ignore = heapinfo1->busy_frag.ignore[frag1];
1002   } else
1003     return true;
1004
1005   /* Start comparison */
1006   if (type ? heap_area_differ_with_type(process, state, area1, area2, snapshot1, snapshot2, previous, type, size,
1007                                         check_ignore, pointer_level)
1008            : heap_area_differ_without_type(process, state, area1, area2, snapshot1, snapshot2, previous, size,
1009                                            check_ignore))
1010     return true;
1011
1012   if (match_pairs)
1013     state.match_equals(previous);
1014   return false;
1015 }
1016 } // namespace simgrid::mc
1017
1018 /************************** Snapshot comparison *******************************/
1019 /******************************************************************************/
1020
1021 static bool areas_differ_with_type(const simgrid::mc::RemoteProcessMemory& process, simgrid::mc::StateComparator& state,
1022                                    const void* real_area1, const simgrid::mc::Snapshot& snapshot1,
1023                                    simgrid::mc::Region* region1, const void* real_area2,
1024                                    const simgrid::mc::Snapshot& snapshot2, simgrid::mc::Region* region2,
1025                                    const simgrid::mc::Type* type, int pointer_level)
1026 {
1027   const simgrid::mc::Type* subtype;
1028   const simgrid::mc::Type* subsubtype;
1029   int elm_size;
1030
1031   xbt_assert(type != nullptr);
1032   switch (type->type) {
1033     case DW_TAG_unspecified_type:
1034       return true;
1035
1036     case DW_TAG_base_type:
1037     case DW_TAG_enumeration_type:
1038     case DW_TAG_union_type:
1039       return MC_snapshot_region_memcmp(real_area1, region1, real_area2, region2, type->byte_size) != 0;
1040     case DW_TAG_typedef:
1041     case DW_TAG_volatile_type:
1042     case DW_TAG_const_type:
1043       return areas_differ_with_type(process, state, real_area1, snapshot1, region1, real_area2, snapshot2, region2,
1044                                     type->subtype, pointer_level);
1045     case DW_TAG_array_type:
1046       subtype = type->subtype;
1047       switch (subtype->type) {
1048         case DW_TAG_unspecified_type:
1049           return true;
1050
1051         case DW_TAG_base_type:
1052         case DW_TAG_enumeration_type:
1053         case DW_TAG_pointer_type:
1054         case DW_TAG_reference_type:
1055         case DW_TAG_rvalue_reference_type:
1056         case DW_TAG_structure_type:
1057         case DW_TAG_class_type:
1058         case DW_TAG_union_type:
1059           if (subtype->full_type)
1060             subtype = subtype->full_type;
1061           elm_size  = subtype->byte_size;
1062           break;
1063         case DW_TAG_const_type:
1064         case DW_TAG_typedef:
1065         case DW_TAG_volatile_type:
1066           subsubtype = subtype->subtype;
1067           if (subsubtype->full_type)
1068             subsubtype = subsubtype->full_type;
1069           elm_size     = subsubtype->byte_size;
1070           break;
1071         default:
1072           return false;
1073       }
1074       for (int i = 0; i < type->element_count; i++) {
1075         size_t off = i * elm_size;
1076         if (areas_differ_with_type(process, state, (const char*)real_area1 + off, snapshot1, region1,
1077                                    (const char*)real_area2 + off, snapshot2, region2, type->subtype, pointer_level))
1078           return true;
1079       }
1080       break;
1081     case DW_TAG_pointer_type:
1082     case DW_TAG_reference_type:
1083     case DW_TAG_rvalue_reference_type: {
1084       const void* addr_pointed1 = MC_region_read_pointer(region1, real_area1);
1085       const void* addr_pointed2 = MC_region_read_pointer(region2, real_area2);
1086
1087       if (type->subtype && type->subtype->type == DW_TAG_subroutine_type)
1088         return (addr_pointed1 != addr_pointed2);
1089       if (addr_pointed1 == nullptr && addr_pointed2 == nullptr)
1090         return false;
1091       if (addr_pointed1 == nullptr || addr_pointed2 == nullptr)
1092         return true;
1093       if (not state.compared_pointers.insert(std::make_pair(addr_pointed1, addr_pointed2)).second)
1094         return false;
1095
1096       pointer_level++;
1097
1098       // Some cases are not handled here:
1099       // * the pointers lead to different areas (one to the heap, the other to the RW segment ...)
1100       // * a pointer leads to the read-only segment of the current object
1101       // * a pointer lead to a different ELF object
1102
1103       if (snapshot1.on_heap(addr_pointed1)) {
1104         if (not snapshot2.on_heap(addr_pointed2))
1105           return true;
1106         // The pointers are both in the heap:
1107         return simgrid::mc::heap_area_differ(process, state, addr_pointed1, addr_pointed2, snapshot1, snapshot2,
1108                                              nullptr, type->subtype, pointer_level);
1109
1110       } else if (region1->contain(simgrid::mc::remote(addr_pointed1))) {
1111         // The pointers are both in the current object R/W segment:
1112         if (not region2->contain(simgrid::mc::remote(addr_pointed2)))
1113           return true;
1114         if (not type->type_id)
1115           return (addr_pointed1 != addr_pointed2);
1116         else
1117           return areas_differ_with_type(process, state, addr_pointed1, snapshot1, region1, addr_pointed2, snapshot2,
1118                                         region2, type->subtype, pointer_level);
1119       } else {
1120         // TODO, We do not handle very well the case where
1121         // it belongs to a different (non-heap) region from the current one.
1122
1123         return (addr_pointed1 != addr_pointed2);
1124       }
1125     }
1126     case DW_TAG_structure_type:
1127     case DW_TAG_class_type:
1128       for (const simgrid::mc::Member& member : type->members) {
1129         const void* member1             = simgrid::dwarf::resolve_member(real_area1, type, &member, &snapshot1);
1130         const void* member2             = simgrid::dwarf::resolve_member(real_area2, type, &member, &snapshot2);
1131         simgrid::mc::Region* subregion1 = snapshot1.get_region(member1, region1); // region1 is hinted
1132         simgrid::mc::Region* subregion2 = snapshot2.get_region(member2, region2); // region2 is hinted
1133         if (areas_differ_with_type(process, state, member1, snapshot1, subregion1, member2, snapshot2, subregion2,
1134                                    member.type, pointer_level))
1135           return true;
1136       }
1137       break;
1138     case DW_TAG_subroutine_type:
1139       return false;
1140     default:
1141       XBT_VERB("Unknown case: %d", type->type);
1142       break;
1143   }
1144
1145   return false;
1146 }
1147
1148 static bool global_variables_differ(const simgrid::mc::RemoteProcessMemory& process,
1149                                     simgrid::mc::StateComparator& state,
1150                                     const simgrid::mc::ObjectInformation* object_info, simgrid::mc::Region* r1,
1151                                     simgrid::mc::Region* r2, const simgrid::mc::Snapshot& snapshot1,
1152                                     const simgrid::mc::Snapshot& snapshot2)
1153 {
1154   xbt_assert(r1 && r2, "Missing region.");
1155
1156   const std::vector<simgrid::mc::Variable>& variables = object_info->global_variables;
1157
1158   for (simgrid::mc::Variable const& current_var : variables) {
1159     // If the variable is not in this object, skip it:
1160     // We do not expect to find a pointer to something which is not reachable
1161     // by the global variables.
1162     if ((char*)current_var.address < object_info->start_rw || (char*)current_var.address > object_info->end_rw)
1163       continue;
1164
1165     const simgrid::mc::Type* bvariable_type = current_var.type;
1166     if (areas_differ_with_type(process, state, current_var.address, snapshot1, r1, current_var.address, snapshot2, r2,
1167                                bvariable_type, 0)) {
1168       XBT_VERB("Global variable %s (%p) is different between snapshots", current_var.name.c_str(), current_var.address);
1169       return true;
1170     }
1171   }
1172
1173   return false;
1174 }
1175
1176 static bool local_variables_differ(const simgrid::mc::RemoteProcessMemory& process, simgrid::mc::StateComparator& state,
1177                                    const simgrid::mc::Snapshot& snapshot1, const simgrid::mc::Snapshot& snapshot2,
1178                                    const_mc_snapshot_stack_t stack1, const_mc_snapshot_stack_t stack2)
1179 {
1180   if (stack1->local_variables.size() != stack2->local_variables.size()) {
1181     XBT_VERB("Different number of local variables");
1182     return true;
1183   }
1184
1185   for (unsigned int cursor = 0; cursor < stack1->local_variables.size(); cursor++) {
1186     const_local_variable_t current_var1 = &stack1->local_variables[cursor];
1187     const_local_variable_t current_var2 = &stack2->local_variables[cursor];
1188     if (current_var1->name != current_var2->name || current_var1->subprogram != current_var2->subprogram ||
1189         current_var1->ip != current_var2->ip) {
1190       // TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
1191       XBT_VERB("Different name of variable (%s - %s) or frame (%s - %s) or ip (%lu - %lu)", current_var1->name.c_str(),
1192                current_var2->name.c_str(), current_var1->subprogram->name.c_str(),
1193                current_var2->subprogram->name.c_str(), current_var1->ip, current_var2->ip);
1194       return true;
1195     }
1196
1197     if (areas_differ_with_type(process, state, current_var1->address, snapshot1,
1198                                snapshot1.get_region(current_var1->address), current_var2->address, snapshot2,
1199                                snapshot2.get_region(current_var2->address), current_var1->type, 0)) {
1200       XBT_VERB("Local variable %s (%p - %p) in frame %s is different between snapshots", current_var1->name.c_str(),
1201                current_var1->address, current_var2->address, current_var1->subprogram->name.c_str());
1202       return true;
1203     }
1204   }
1205   return false;
1206 }
1207
1208 namespace simgrid::mc {
1209 bool Snapshot::equals_to(const Snapshot& other, RemoteProcessMemory& memory)
1210 {
1211   /* TODO: the memory parameter should be eventually removed. It seems to be there because each snapshot lacks some sort
1212     of metadata. That's OK for now (letting appart the fact that we cannot have a nice operator== because we need that
1213     extra parameter), but it will fall short when we want to have parallel explorations, with more than one
1214     RemoteProcess. At the very least, snapshots will need to know the remote process they are corresponding to, and more
1215     probably they will need to embeed all their metadata to let the remoteprocesses die before the end of the
1216     exploration. */
1217
1218   /* TODO: This method should moved to Snapshot.cpp, but it needs the StateComparator that is declared locally to this
1219    * file only. */
1220
1221   static StateComparator state_comparator; // TODO, make this a field of a persistant state object
1222
1223   if (hash_ != other.hash_) {
1224     XBT_VERB("(%ld - %ld) Different hash: 0x%" PRIx64 "--0x%" PRIx64, this->num_state_, other.num_state_, this->hash_,
1225              other.hash_);
1226     return false;
1227   }
1228   XBT_VERB("(%ld - %ld) Same hash: 0x%" PRIx64, this->num_state_, other.num_state_, this->hash_);
1229
1230   /* TODO: re-enable the quick filter of counting enabled processes in each snapshots */
1231
1232   /* Compare size of stacks */
1233   for (unsigned long i = 0; i < this->stacks_.size(); i++) {
1234     size_t size_used1 = this->stack_sizes_[i];
1235     size_t size_used2 = other.stack_sizes_[i];
1236     if (size_used1 != size_used2) {
1237       XBT_VERB("(%ld - %ld) Different size used in stacks: %zu - %zu", num_state_, other.num_state_, size_used1,
1238                size_used2);
1239       return false;
1240     }
1241   }
1242
1243   /* Init heap information used in heap comparison algorithm */
1244   const s_xbt_mheap_t* heap1 = static_cast<xbt_mheap_t>(
1245       this->read_bytes(alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), memory.heap_address, ReadOptions::lazy()));
1246   const s_xbt_mheap_t* heap2 = static_cast<xbt_mheap_t>(
1247       other.read_bytes(alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), memory.heap_address, ReadOptions::lazy()));
1248   if (state_comparator.initHeapInformation(memory, heap1, heap2, this->to_ignore_, other.to_ignore_) == -1) {
1249     XBT_VERB("(%ld - %ld) Different heap information", this->num_state_, other.num_state_);
1250     return false;
1251   }
1252
1253   /* Stacks comparison */
1254   for (unsigned int cursor = 0; cursor < this->stacks_.size(); cursor++) {
1255     const_mc_snapshot_stack_t stack1 = &this->stacks_[cursor];
1256     const_mc_snapshot_stack_t stack2 = &other.stacks_[cursor];
1257
1258     if (local_variables_differ(memory, state_comparator, *this, other, stack1, stack2)) {
1259       XBT_VERB("(%ld - %ld) Different local variables between stacks %u", this->num_state_, other.num_state_,
1260                cursor + 1);
1261       return false;
1262     }
1263   }
1264
1265   size_t regions_count = this->snapshot_regions_.size();
1266   if (regions_count != other.snapshot_regions_.size())
1267     return false;
1268
1269   for (size_t k = 0; k != regions_count; ++k) {
1270     Region* region1 = this->snapshot_regions_[k].get();
1271     Region* region2 = other.snapshot_regions_[k].get();
1272
1273     // Preconditions:
1274     if (region1->region_type() != RegionType::Data)
1275       continue;
1276
1277     xbt_assert(region1->region_type() == region2->region_type());
1278     xbt_assert(region1->object_info() == region2->object_info());
1279     xbt_assert(region1->object_info());
1280
1281     /* Compare global variables */
1282     if (global_variables_differ(memory, state_comparator, region1->object_info(), region1, region2, *this, other)) {
1283       std::string const& name = region1->object_info()->file_name;
1284       XBT_VERB("(%ld - %ld) Different global variables in %s", this->num_state_, other.num_state_, name.c_str());
1285       return false;
1286     }
1287   }
1288
1289   XBT_VERB("   Compare heap...");
1290   /* Compare heap */
1291   if (mmalloc_heap_differ(memory, state_comparator, *this, other)) {
1292     XBT_VERB("(%ld - %ld) Different heap (mmalloc_heap_differ)", this->num_state_, other.num_state_);
1293     return false;
1294   }
1295
1296   XBT_VERB("(%ld - %ld) No difference found", this->num_state_, other.num_state_);
1297
1298   return true;
1299 }
1300 } // namespace simgrid::mc