src/mc/compare.cpp

   1 /* Copyright (c) 2008-2019. 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 snapshooting and comparison                    */
   7
   8 #include "src/mc/mc_config.hpp"
   9 #include "src/mc/mc_private.hpp"
  10 #include "src/mc/mc_smx.hpp"
  11 #include "src/mc/sosp/mc_snapshot.hpp"
  12
  13 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, xbt, "Logging specific to mc_compare in mc");
  14
  15 namespace simgrid {
  16 namespace mc {
  17
  18 struct HeapLocation;
  19 typedef std::array<HeapLocation, 2> HeapLocationPair;
  20 typedef std::set<HeapLocationPair> HeapLocationPairs;
  21 struct HeapArea;
  22 struct ProcessComparisonState;
  23 struct StateComparator;
  24
  25 static int compare_heap_area(
  26   StateComparator& state,
  27   int process_index, const void *area1, const void* area2,
  28   Snapshot* snapshot1, Snapshot* snapshot2,
  29   HeapLocationPairs* previous, Type* type, int pointer_level);
  30
  31 }
  32 }
  33
  34 using simgrid::mc::remote;
  35
  36 /*********************************** Heap comparison ***********************************/
  37 /***************************************************************************************/
  38
  39 namespace simgrid {
  40 namespace mc {
  41
  42 class HeapLocation {
  43 public:
  44   int block_    = 0;
  45   int fragment_ = 0;
  46
  47   HeapLocation() = default;
  48   HeapLocation(int block, int fragment = 0) : block_(block), fragment_(fragment) {}
  49
  50   bool operator==(HeapLocation const& that) const
  51   {
  52     return block_ == that.block_ && fragment_ == that.fragment_;
  53   }
  54   bool operator<(HeapLocation const& that) const
  55   {
  56     return std::make_pair(block_, fragment_) < std::make_pair(that.block_, that.fragment_);
  57   }
  58 };
  59
  60 static inline
  61 HeapLocationPair makeHeapLocationPair(int block1, int fragment1, int block2, int fragment2)
  62 {
  63   return simgrid::mc::HeapLocationPair{{
  64     simgrid::mc::HeapLocation(block1, fragment1),
  65     simgrid::mc::HeapLocation(block2, fragment2)
  66   }};
  67 }
  68
  69 class HeapArea : public HeapLocation {
  70 public:
  71   bool valid_ = false;
  72   HeapArea() = default;
  73   explicit HeapArea(int block) : valid_(true) { block_ = block; }
  74   HeapArea(int block, int fragment) : valid_(true)
  75   {
  76     block_    = block;
  77     fragment_ = fragment;
  78   }
  79 };
  80
  81 class ProcessComparisonState {
  82 public:
  83   std::vector<simgrid::mc::IgnoredHeapRegion>* to_ignore = nullptr;
  84   std::vector<HeapArea> equals_to;
  85   std::vector<simgrid::mc::Type*> types;
  86   std::size_t heapsize = 0;
  87
  88   void initHeapInformation(xbt_mheap_t heap, std::vector<simgrid::mc::IgnoredHeapRegion>* i);
  89 };
  90
  91 namespace {
  92
  93 /** A hash which works with more stuff
  94  *
  95  *  It can hash pairs: the standard hash currently doesn't include this.
  96  */
  97 template <class X> class hash : public std::hash<X> {
  98 };
  99
 100 template <class X, class Y> class hash<std::pair<X, Y>> {
 101 public:
 102   std::size_t operator()(std::pair<X,Y>const& x) const
 103   {
 104     hash<X> h1;
 105     hash<X> h2;
 106     return h1(x.first) ^ h2(x.second);
 107   }
 108 };
 109
 110 }
 111
 112 class StateComparator {
 113 public:
 114   s_xbt_mheap_t std_heap_copy;
 115   std::size_t heaplimit;
 116   std::array<ProcessComparisonState, 2> processStates;
 117
 118   std::unordered_set<std::pair<void*, void*>, hash<std::pair<void*, void*>>> compared_pointers;
 119
 120   void clear()
 121   {
 122     compared_pointers.clear();
 123   }
 124
 125   int initHeapInformation(
 126     xbt_mheap_t heap1, xbt_mheap_t heap2,
 127     std::vector<simgrid::mc::IgnoredHeapRegion>* i1,
 128     std::vector<simgrid::mc::IgnoredHeapRegion>* i2);
 129
 130   HeapArea& equals_to1_(std::size_t i, std::size_t j)
 131   {
 132     return processStates[0].equals_to[ MAX_FRAGMENT_PER_BLOCK * i + j];
 133   }
 134   HeapArea& equals_to2_(std::size_t i, std::size_t j)
 135   {
 136     return processStates[1].equals_to[ MAX_FRAGMENT_PER_BLOCK * i + j];
 137   }
 138   Type*& types1_(std::size_t i, std::size_t j)
 139   {
 140     return processStates[0].types[ MAX_FRAGMENT_PER_BLOCK * i + j];
 141   }
 142   Type*& types2_(std::size_t i, std::size_t j)
 143   {
 144     return processStates[1].types[ MAX_FRAGMENT_PER_BLOCK * i + j];
 145   }
 146
 147   HeapArea const& equals_to1_(std::size_t i, std::size_t j) const
 148   {
 149     return processStates[0].equals_to[ MAX_FRAGMENT_PER_BLOCK * i + j];
 150   }
 151   HeapArea const& equals_to2_(std::size_t i, std::size_t j) const
 152   {
 153     return processStates[1].equals_to[ MAX_FRAGMENT_PER_BLOCK * i + j];
 154   }
 155   Type* const& types1_(std::size_t i, std::size_t j) const
 156   {
 157     return processStates[0].types[ MAX_FRAGMENT_PER_BLOCK * i + j];
 158   }
 159   Type* const& types2_(std::size_t i, std::size_t j) const
 160   {
 161     return processStates[1].types[ MAX_FRAGMENT_PER_BLOCK * i + j];
 162   }
 163
 164   /** Check whether two blocks are known to be matching
 165    *
 166    *  @param b1     Block of state 1
 167    *  @param b2     Block of state 2
 168    *  @return       if the blocks are known to be matching
 169    */
 170   bool blocksEqual(int b1, int b2) const
 171   {
 172     return this->equals_to1_(b1, 0).block_ == b2 && this->equals_to2_(b2, 0).block_ == b1;
 173   }
 174
 175   /** Check whether two fragments are known to be matching
 176    *
 177    *  @param b1     Block of state 1
 178    *  @param f1     Fragment of state 1
 179    *  @param b2     Block of state 2
 180    *  @param f2     Fragment of state 2
 181    *  @return       if the fragments are known to be matching
 182    */
 183   int fragmentsEqual(int b1, int f1, int b2, int f2) const
 184   {
 185     return this->equals_to1_(b1, f1).block_ == b2 && this->equals_to1_(b1, f1).fragment_ == f2 &&
 186            this->equals_to2_(b2, f2).block_ == b1 && this->equals_to2_(b2, f2).fragment_ == f1;
 187   }
 188
 189   void match_equals(HeapLocationPairs* list);
 190 };
 191
 192 }
 193 }
 194
 195 /************************************************************************************/
 196
 197 static ssize_t heap_comparison_ignore_size(
 198   std::vector<simgrid::mc::IgnoredHeapRegion>* ignore_list,
 199   const void *address)
 200 {
 201   int start = 0;
 202   int end = ignore_list->size() - 1;
 203
 204   while (start <= end) {
 205     unsigned int cursor = (start + end) / 2;
 206     simgrid::mc::IgnoredHeapRegion const& region = (*ignore_list)[cursor];
 207     if (region.address == address)
 208       return region.size;
 209     if (region.address < address)
 210       start = cursor + 1;
 211     if (region.address > address)
 212       end = cursor - 1;
 213   }
 214
 215   return -1;
 216 }
 217
 218 static bool is_stack(const void *address)
 219 {
 220   for (auto const& stack : mc_model_checker->process().stack_areas())
 221     if (address == stack.address)
 222       return true;
 223   return false;
 224 }
 225
 226 // TODO, this should depend on the snapshot?
 227 static bool is_block_stack(int block)
 228 {
 229   for (auto const& stack : mc_model_checker->process().stack_areas())
 230     if (block == stack.block)
 231       return true;
 232   return false;
 233 }
 234
 235 namespace simgrid {
 236 namespace mc {
 237
 238 void StateComparator::match_equals(HeapLocationPairs* list)
 239 {
 240   for (auto const& pair : *list) {
 241     if (pair[0].fragment_ != -1) {
 242       this->equals_to1_(pair[0].block_, pair[0].fragment_) = simgrid::mc::HeapArea(pair[1].block_, pair[1].fragment_);
 243       this->equals_to2_(pair[1].block_, pair[1].fragment_) = simgrid::mc::HeapArea(pair[0].block_, pair[0].fragment_);
 244     } else {
 245       this->equals_to1_(pair[0].block_, 0) = simgrid::mc::HeapArea(pair[1].block_, pair[1].fragment_);
 246       this->equals_to2_(pair[1].block_, 0) = simgrid::mc::HeapArea(pair[0].block_, pair[0].fragment_);
 247     }
 248   }
 249 }
 250
 251 void ProcessComparisonState::initHeapInformation(xbt_mheap_t heap,
 252                         std::vector<simgrid::mc::IgnoredHeapRegion>* i)
 253 {
 254   auto heaplimit  = heap->heaplimit;
 255   this->heapsize  = heap->heapsize;
 256   this->to_ignore = i;
 257   this->equals_to.assign(heaplimit * MAX_FRAGMENT_PER_BLOCK, HeapArea());
 258   this->types.assign(heaplimit * MAX_FRAGMENT_PER_BLOCK, nullptr);
 259 }
 260
 261 int StateComparator::initHeapInformation(xbt_mheap_t heap1, xbt_mheap_t heap2,
 262                           std::vector<simgrid::mc::IgnoredHeapRegion>* i1,
 263                           std::vector<simgrid::mc::IgnoredHeapRegion>* i2)
 264 {
 265   if ((heap1->heaplimit != heap2->heaplimit) || (heap1->heapsize != heap2->heapsize))
 266     return -1;
 267   this->heaplimit     = heap1->heaplimit;
 268   this->std_heap_copy = *mc_model_checker->process().get_heap();
 269   this->processStates[0].initHeapInformation(heap1, i1);
 270   this->processStates[1].initHeapInformation(heap2, i2);
 271   return 0;
 272 }
 273
 274 // TODO, have a robust way to find it in O(1)
 275 static inline RegionSnapshot* MC_get_heap_region(Snapshot* snapshot)
 276 {
 277   for (auto const& region : snapshot->snapshot_regions_)
 278     if (region->region_type() == simgrid::mc::RegionType::Heap)
 279       return region.get();
 280   xbt_die("No heap region");
 281 }
 282
 283 static
 284 int mmalloc_compare_heap(
 285   simgrid::mc::StateComparator& state, simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot* snapshot2)
 286 {
 287   simgrid::mc::RemoteClient* process = &mc_model_checker->process();
 288
 289   /* Start comparison */
 290   int nb_diff1 = 0;
 291   int nb_diff2 = 0;
 292   bool equal;
 293
 294   /* Check busy blocks */
 295   size_t i1 = 1;
 296
 297   malloc_info heapinfo_temp1;
 298   malloc_info heapinfo_temp2;
 299   malloc_info heapinfo_temp2b;
 300
 301   simgrid::mc::RegionSnapshot* heap_region1 = MC_get_heap_region(snapshot1);
 302   simgrid::mc::RegionSnapshot* heap_region2 = MC_get_heap_region(snapshot2);
 303
 304   // This is the address of std_heap->heapinfo in the application process:
 305   void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo;
 306
 307   // This is in snapshot do not use them directly:
 308   const malloc_info* heapinfos1 = snapshot1->read<malloc_info*>(
 309       RemotePtr<malloc_info*>((std::uint64_t)heapinfo_address), simgrid::mc::ProcessIndexMissing);
 310   const malloc_info* heapinfos2 = snapshot2->read<malloc_info*>(
 311       RemotePtr<malloc_info*>((std::uint64_t)heapinfo_address), simgrid::mc::ProcessIndexMissing);
 312
 313   while (i1 < state.heaplimit) {
 314
 315     const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(heap_region1, &heapinfo_temp1, &heapinfos1[i1], sizeof(malloc_info));
 316     const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(heap_region2, &heapinfo_temp2, &heapinfos2[i1], sizeof(malloc_info));
 317
 318     if (heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type == MMALLOC_TYPE_HEAPINFO) {      /* Free block */
 319       i1 ++;
 320       continue;
 321     }
 322
 323     if (heapinfo1->type < 0) {
 324       fprintf(stderr, "Unkown mmalloc block type.\n");
 325       abort();
 326     }
 327
 328     void* addr_block1 = ((void*)(((ADDR2UINT(i1)) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase));
 329
 330     if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED) {       /* Large block */
 331
 332       if (is_stack(addr_block1)) {
 333         for (size_t k = 0; k < heapinfo1->busy_block.size; k++)
 334           state.equals_to1_(i1 + k, 0) = HeapArea(i1, -1);
 335         for (size_t k = 0; k < heapinfo2->busy_block.size; k++)
 336           state.equals_to2_(i1 + k, 0) = HeapArea(i1, -1);
 337         i1 += heapinfo1->busy_block.size;
 338         continue;
 339       }
 340
 341       if (state.equals_to1_(i1, 0).valid_) {
 342         i1++;
 343         continue;
 344       }
 345
 346       size_t i2 = 1;
 347       equal     = false;
 348
 349       /* Try first to associate to same block in the other heap */
 350       if (heapinfo2->type == heapinfo1->type && state.equals_to2_(i1, 0).valid_ == 0) {
 351         void* addr_block2 = (ADDR2UINT(i1) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
 352         int res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing, addr_block1, addr_block2,
 353                                             snapshot1, snapshot2, nullptr, nullptr, 0);
 354         if (res_compare != 1) {
 355           for (size_t k = 1; k < heapinfo2->busy_block.size; k++)
 356             state.equals_to2_(i1 + k, 0) = HeapArea(i1, -1);
 357           for (size_t k = 1; k < heapinfo1->busy_block.size; k++)
 358             state.equals_to1_(i1 + k, 0) = HeapArea(i1, -1);
 359           equal = true;
 360           i1 += heapinfo1->busy_block.size;
 361         }
 362       }
 363
 364       while (i2 < state.heaplimit && not equal) {
 365
 366         void* addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
 367
 368         if (i2 == i1) {
 369           i2++;
 370           continue;
 371         }
 372
 373         const malloc_info* heapinfo2b = (const malloc_info*) MC_region_read(heap_region2, &heapinfo_temp2b, &heapinfos2[i2], sizeof(malloc_info));
 374
 375         if (heapinfo2b->type != MMALLOC_TYPE_UNFRAGMENTED) {
 376           i2++;
 377           continue;
 378         }
 379
 380         if (state.equals_to2_(i2, 0).valid_) {
 381           i2++;
 382           continue;
 383         }
 384
 385         int res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing, addr_block1, addr_block2,
 386                                             snapshot1, snapshot2, nullptr, nullptr, 0);
 387
 388         if (res_compare != 1) {
 389           for (size_t k = 1; k < heapinfo2b->busy_block.size; k++)
 390             state.equals_to2_(i2 + k, 0) = HeapArea(i1, -1);
 391           for (size_t k = 1; k < heapinfo1->busy_block.size; k++)
 392             state.equals_to1_(i1 + k, 0) = HeapArea(i2, -1);
 393           equal = true;
 394           i1 += heapinfo1->busy_block.size;
 395         }
 396
 397         i2++;
 398       }
 399
 400       if (not equal) {
 401         XBT_DEBUG("Block %zu not found (size_used = %zu, addr = %p)", i1, heapinfo1->busy_block.busy_size, addr_block1);
 402         i1 = state.heaplimit + 1;
 403         nb_diff1++;
 404       }
 405
 406     } else {                    /* Fragmented block */
 407
 408       for (size_t j1 = 0; j1 < (size_t)(BLOCKSIZE >> heapinfo1->type); j1++) {
 409
 410         if (heapinfo1->busy_frag.frag_size[j1] == -1) /* Free fragment_ */
 411           continue;
 412
 413         if (state.equals_to1_(i1, j1).valid_)
 414           continue;
 415
 416         void* addr_frag1 = (void*)((char*)addr_block1 + (j1 << heapinfo1->type));
 417
 418         size_t i2 = 1;
 419         equal     = false;
 420
 421         /* Try first to associate to same fragment_ in the other heap */
 422         if (heapinfo2->type == heapinfo1->type && not state.equals_to2_(i1, j1).valid_) {
 423           void* addr_block2 = (ADDR2UINT(i1) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
 424           void* addr_frag2  = (void*)((char*)addr_block2 + (j1 << heapinfo2->type));
 425           int res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing, addr_frag1, addr_frag2,
 426                                               snapshot1, snapshot2, nullptr, nullptr, 0);
 427           if (res_compare != 1)
 428             equal = true;
 429         }
 430
 431         while (i2 < state.heaplimit && not equal) {
 432
 433           const malloc_info* heapinfo2b = (const malloc_info*) MC_region_read(
 434             heap_region2, &heapinfo_temp2b, &heapinfos2[i2],
 435             sizeof(malloc_info));
 436
 437           if (heapinfo2b->type == MMALLOC_TYPE_FREE || heapinfo2b->type == MMALLOC_TYPE_HEAPINFO) {
 438             i2 ++;
 439             continue;
 440           }
 441
 442           // We currently do not match fragments with unfragmented blocks (maybe we should).
 443           if (heapinfo2b->type == MMALLOC_TYPE_UNFRAGMENTED) {
 444             i2++;
 445             continue;
 446           }
 447
 448           if (heapinfo2b->type < 0) {
 449             fprintf(stderr, "Unknown mmalloc block type.\n");
 450             abort();
 451           }
 452
 453           for (size_t j2 = 0; j2 < (size_t)(BLOCKSIZE >> heapinfo2b->type); j2++) {
 454
 455             if (i2 == i1 && j2 == j1)
 456               continue;
 457
 458             if (state.equals_to2_(i2, j2).valid_)
 459               continue;
 460
 461             void* addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
 462             void* addr_frag2  = (void*)((char*)addr_block2 + (j2 << heapinfo2b->type));
 463
 464             int res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing, addr_frag1, addr_frag2,
 465                                                 snapshot2, snapshot2, nullptr, nullptr, 0);
 466             if (res_compare != 1) {
 467               equal = true;
 468               break;
 469             }
 470           }
 471
 472           i2++;
 473         }
 474
 475         if (not equal) {
 476           XBT_DEBUG("Block %zu, fragment_ %zu not found (size_used = %zd, address = %p)\n", i1, j1,
 477                     heapinfo1->busy_frag.frag_size[j1], addr_frag1);
 478           i1 = state.heaplimit + 1;
 479           nb_diff1++;
 480           break;
 481         }
 482       }
 483
 484       i1++;
 485     }
 486   }
 487
 488   /* All blocks/fragments are equal to another block/fragment_ ? */
 489   for (size_t i = 1; i < state.heaplimit; i++) {
 490     const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(
 491       heap_region1, &heapinfo_temp1, &heapinfos1[i], sizeof(malloc_info));
 492
 493     if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED && i1 == state.heaplimit && heapinfo1->busy_block.busy_size > 0 &&
 494         not state.equals_to1_(i, 0).valid_) {
 495       XBT_DEBUG("Block %zu not found (size used = %zu)", i, heapinfo1->busy_block.busy_size);
 496       nb_diff1++;
 497     }
 498
 499     if (heapinfo1->type <= 0)
 500       continue;
 501     for (size_t j = 0; j < (size_t)(BLOCKSIZE >> heapinfo1->type); j++)
 502       if (i1 == state.heaplimit && heapinfo1->busy_frag.frag_size[j] > 0 && not state.equals_to1_(i, j).valid_) {
 503         XBT_DEBUG("Block %zu, Fragment %zu not found (size used = %zd)", i, j, heapinfo1->busy_frag.frag_size[j]);
 504         nb_diff1++;
 505       }
 506   }
 507
 508   if (i1 == state.heaplimit)
 509     XBT_DEBUG("Number of blocks/fragments not found in heap1: %d", nb_diff1);
 510
 511   for (size_t i = 1; i < state.heaplimit; i++) {
 512     const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(
 513       heap_region2, &heapinfo_temp2, &heapinfos2[i], sizeof(malloc_info));
 514     if (heapinfo2->type == MMALLOC_TYPE_UNFRAGMENTED && i1 == state.heaplimit && heapinfo2->busy_block.busy_size > 0 &&
 515         not state.equals_to2_(i, 0).valid_) {
 516       XBT_DEBUG("Block %zu not found (size used = %zu)", i,
 517                 heapinfo2->busy_block.busy_size);
 518       nb_diff2++;
 519     }
 520
 521     if (heapinfo2->type <= 0)
 522       continue;
 523
 524     for (size_t j = 0; j < (size_t)(BLOCKSIZE >> heapinfo2->type); j++)
 525       if (i1 == state.heaplimit && heapinfo2->busy_frag.frag_size[j] > 0 && not state.equals_to2_(i, j).valid_) {
 526         XBT_DEBUG("Block %zu, Fragment %zu not found (size used = %zd)",
 527           i, j, heapinfo2->busy_frag.frag_size[j]);
 528         nb_diff2++;
 529       }
 530
 531   }
 532
 533   if (i1 == state.heaplimit)
 534     XBT_DEBUG("Number of blocks/fragments not found in heap2: %d", nb_diff2);
 535
 536   return nb_diff1 > 0 || nb_diff2 > 0;
 537 }
 538
 539 /**
 540  *
 541  * @param state
 542  * @param real_area1     Process address for state 1
 543  * @param real_area2     Process address for state 2
 544  * @param snapshot1      Snapshot of state 1
 545  * @param snapshot2      Snapshot of state 2
 546  * @param previous
 547  * @param size
 548  * @param check_ignore
 549  */
 550 static int compare_heap_area_without_type(
 551   simgrid::mc::StateComparator& state, int process_index,
 552   const void *real_area1, const void *real_area2,
 553   simgrid::mc::Snapshot* snapshot1,
 554   simgrid::mc::Snapshot* snapshot2,
 555   HeapLocationPairs* previous, int size,
 556   int check_ignore)
 557 {
 558   simgrid::mc::RemoteClient* process = &mc_model_checker->process();
 559   simgrid::mc::RegionSnapshot* heap_region1 = MC_get_heap_region(snapshot1);
 560   simgrid::mc::RegionSnapshot* heap_region2 = MC_get_heap_region(snapshot2);
 561
 562   for (int i = 0; i < size; ) {
 563
 564     if (check_ignore > 0) {
 565       ssize_t ignore1 = heap_comparison_ignore_size(
 566         state.processStates[0].to_ignore, (char *) real_area1 + i);
 567       if (ignore1 != -1) {
 568         ssize_t ignore2 = heap_comparison_ignore_size(
 569           state.processStates[1].to_ignore, (char *) real_area2 + i);
 570         if (ignore2 == ignore1) {
 571           if (ignore1 == 0) {
 572             check_ignore--;
 573             return 0;
 574           } else {
 575             i = i + ignore2;
 576             check_ignore--;
 577             continue;
 578           }
 579         }
 580       }
 581     }
 582
 583     if (MC_snapshot_region_memcmp(((char *) real_area1) + i, heap_region1, ((char *) real_area2) + i, heap_region2, 1) != 0) {
 584
 585       int pointer_align = (i / sizeof(void *)) * sizeof(void *);
 586       const void* addr_pointed1 = snapshot1->read(
 587         remote((void**)((char *) real_area1 + pointer_align)), process_index);
 588       const void* addr_pointed2 = snapshot2->read(
 589         remote((void**)((char *) real_area2 + pointer_align)), process_index);
 590
 591       if (process->in_maestro_stack(remote(addr_pointed1))
 592         && process->in_maestro_stack(remote(addr_pointed2))) {
 593         i = pointer_align + sizeof(void *);
 594         continue;
 595       }
 596
 597       if (addr_pointed1 > state.std_heap_copy.heapbase
 598            && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)
 599            && addr_pointed2 > state.std_heap_copy.heapbase
 600            && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2)) {
 601         // Both addreses are in the heap:
 602         int res_compare = compare_heap_area(state ,process_index,
 603           addr_pointed1, addr_pointed2,
 604           snapshot1, snapshot2, previous, nullptr, 0);
 605         if (res_compare == 1)
 606           return res_compare;
 607         i = pointer_align + sizeof(void *);
 608         continue;
 609       }
 610
 611       return 1;
 612     }
 613
 614     i++;
 615   }
 616
 617   return 0;
 618 }
 619
 620 /**
 621  *
 622  * @param state
 623  * @param real_area1     Process address for state 1
 624  * @param real_area2     Process address for state 2
 625  * @param snapshot1      Snapshot of state 1
 626  * @param snapshot2      Snapshot of state 2
 627  * @param previous
 628  * @param type
 629  * @param area_size      either a byte_size or an elements_count (?)
 630  * @param check_ignore
 631  * @param pointer_level
 632  * @return               0 (same), 1 (different), -1 (unknown)
 633  */
 634 static int compare_heap_area_with_type(
 635   simgrid::mc::StateComparator& state, int process_index,
 636   const void *real_area1, const void *real_area2,
 637   simgrid::mc::Snapshot* snapshot1,
 638   simgrid::mc::Snapshot* snapshot2,
 639   HeapLocationPairs* previous, simgrid::mc::Type* type,
 640   int area_size, int check_ignore,
 641   int pointer_level)
 642 {
 643   do {
 644
 645     // HACK: This should not happen but in pratice, there are some
 646     // DW_TAG_typedef without an associated DW_AT_type:
 647     //<1><538832>: Abbrev Number: 111 (DW_TAG_typedef)
 648     //    <538833>   DW_AT_name        : (indirect string, offset: 0x2292f3): gregset_t
 649     //    <538837>   DW_AT_decl_file   : 98
 650     //    <538838>   DW_AT_decl_line   : 37
 651     if (type == nullptr)
 652       return 0;
 653
 654     if (is_stack(real_area1) && is_stack(real_area2))
 655       return 0;
 656
 657     if (check_ignore > 0) {
 658       ssize_t ignore1 = heap_comparison_ignore_size(state.processStates[0].to_ignore, real_area1);
 659       if (ignore1 > 0 && heap_comparison_ignore_size(state.processStates[1].to_ignore, real_area2) == ignore1)
 660         return 0;
 661     }
 662
 663     simgrid::mc::Type* subtype;
 664     simgrid::mc::Type* subsubtype;
 665     int elm_size;
 666     const void* addr_pointed1;
 667     const void* addr_pointed2;
 668
 669     simgrid::mc::RegionSnapshot* heap_region1 = MC_get_heap_region(snapshot1);
 670     simgrid::mc::RegionSnapshot* heap_region2 = MC_get_heap_region(snapshot2);
 671
 672     switch (type->type) {
 673       case DW_TAG_unspecified_type:
 674         return 1;
 675
 676       case DW_TAG_base_type:
 677         if (not type->name.empty() && type->name == "char") { /* String, hence random (arbitrary ?) size */
 678           if (real_area1 == real_area2)
 679             return -1;
 680           else
 681             return MC_snapshot_region_memcmp(real_area1, heap_region1, real_area2, heap_region2, area_size) != 0;
 682         } else {
 683           if (area_size != -1 && type->byte_size != area_size)
 684             return -1;
 685           else
 686             return MC_snapshot_region_memcmp(real_area1, heap_region1, real_area2, heap_region2, type->byte_size) != 0;
 687         }
 688
 689       case DW_TAG_enumeration_type:
 690         if (area_size != -1 && type->byte_size != area_size)
 691           return -1;
 692         return MC_snapshot_region_memcmp(real_area1, heap_region1, real_area2, heap_region2, type->byte_size) != 0;
 693
 694       case DW_TAG_typedef:
 695       case DW_TAG_const_type:
 696       case DW_TAG_volatile_type:
 697         // Poor man's TCO:
 698         type = type->subtype;
 699         continue; // restart
 700
 701       case DW_TAG_array_type:
 702         subtype = type->subtype;
 703         switch (subtype->type) {
 704           case DW_TAG_unspecified_type:
 705             return 1;
 706
 707           case DW_TAG_base_type:
 708           case DW_TAG_enumeration_type:
 709           case DW_TAG_pointer_type:
 710           case DW_TAG_reference_type:
 711           case DW_TAG_rvalue_reference_type:
 712           case DW_TAG_structure_type:
 713           case DW_TAG_class_type:
 714           case DW_TAG_union_type:
 715             if (subtype->full_type)
 716               subtype = subtype->full_type;
 717             elm_size  = subtype->byte_size;
 718             break;
 719           // TODO, just remove the type indirection?
 720           case DW_TAG_const_type:
 721           case DW_TAG_typedef:
 722           case DW_TAG_volatile_type:
 723             subsubtype = subtype->subtype;
 724             if (subsubtype->full_type)
 725               subsubtype = subsubtype->full_type;
 726             elm_size     = subsubtype->byte_size;
 727             break;
 728           default:
 729             return 0;
 730         }
 731         for (int i = 0; i < type->element_count; i++) {
 732           // TODO, add support for variable stride (DW_AT_byte_stride)
 733           int res = compare_heap_area_with_type(state, process_index, (char*)real_area1 + (i * elm_size),
 734                                                 (char*)real_area2 + (i * elm_size), snapshot1, snapshot2, previous,
 735                                                 type->subtype, subtype->byte_size, check_ignore, pointer_level);
 736           if (res == 1)
 737             return res;
 738         }
 739         return 0;
 740
 741       case DW_TAG_reference_type:
 742       case DW_TAG_rvalue_reference_type:
 743       case DW_TAG_pointer_type:
 744         if (type->subtype && type->subtype->type == DW_TAG_subroutine_type) {
 745           addr_pointed1 = snapshot1->read(remote((void**)real_area1), process_index);
 746           addr_pointed2 = snapshot2->read(remote((void**)real_area2), process_index);
 747           return (addr_pointed1 != addr_pointed2);
 748         }
 749         pointer_level++;
 750         if (pointer_level <= 1) {
 751           addr_pointed1 = snapshot1->read(remote((void**)real_area1), process_index);
 752           addr_pointed2 = snapshot2->read(remote((void**)real_area2), process_index);
 753           if (addr_pointed1 > state.std_heap_copy.heapbase && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1) &&
 754               addr_pointed2 > state.std_heap_copy.heapbase && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2))
 755             return compare_heap_area(state, process_index, addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous,
 756                                      type->subtype, pointer_level);
 757           else
 758             return (addr_pointed1 != addr_pointed2);
 759         }
 760         for (size_t i = 0; i < (area_size / sizeof(void*)); i++) {
 761           addr_pointed1 = snapshot1->read(remote((void**)((char*)real_area1 + i * sizeof(void*))), process_index);
 762           addr_pointed2 = snapshot2->read(remote((void**)((char*)real_area2 + i * sizeof(void*))), process_index);
 763           int res;
 764           if (addr_pointed1 > state.std_heap_copy.heapbase && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1) &&
 765               addr_pointed2 > state.std_heap_copy.heapbase && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2))
 766             res = compare_heap_area(state, process_index, addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous,
 767                                     type->subtype, pointer_level);
 768           else
 769             res = (addr_pointed1 != addr_pointed2);
 770           if (res == 1)
 771             return res;
 772         }
 773         return 0;
 774
 775       case DW_TAG_structure_type:
 776       case DW_TAG_class_type:
 777         if (type->full_type)
 778           type = type->full_type;
 779         if (area_size != -1 && type->byte_size != area_size) {
 780           if (area_size <= type->byte_size || area_size % type->byte_size != 0)
 781             return -1;
 782           for (size_t i = 0; i < (size_t)(area_size / type->byte_size); i++) {
 783             int res = compare_heap_area_with_type(state, process_index, (char*)real_area1 + i * type->byte_size,
 784                                                   (char*)real_area2 + i * type->byte_size, snapshot1, snapshot2,
 785                                                   previous, type, -1, check_ignore, 0);
 786             if (res == 1)
 787               return res;
 788           }
 789         } else {
 790           for (simgrid::mc::Member& member : type->members) {
 791             // TODO, optimize this? (for the offset case)
 792             void* real_member1 = simgrid::dwarf::resolve_member(real_area1, type, &member,
 793                                                                 (simgrid::mc::AddressSpace*)snapshot1, process_index);
 794             void* real_member2 = simgrid::dwarf::resolve_member(real_area2, type, &member,
 795                                                                 (simgrid::mc::AddressSpace*)snapshot2, process_index);
 796             int res = compare_heap_area_with_type(state, process_index, real_member1, real_member2, snapshot1,
 797                                                   snapshot2, previous, member.type, -1, check_ignore, 0);
 798             if (res == 1)
 799               return res;
 800           }
 801         }
 802         return 0;
 803
 804       case DW_TAG_union_type:
 805         return compare_heap_area_without_type(state, process_index, real_area1, real_area2, snapshot1, snapshot2,
 806                                               previous, type->byte_size, check_ignore);
 807
 808       default:
 809         return 0;
 810     }
 811
 812     xbt_die("Unreachable");
 813   } while (true);
 814 }
 815
 816 /** Infer the type of a part of the block from the type of the block
 817  *
 818  * TODO, handle DW_TAG_array_type as well as arrays of the object ((*p)[5], p[5])
 819  *
 820  * TODO, handle subfields ((*p).bar.foo, (*p)[5].bar…)
 821  *
 822  * @param  type               DWARF type ID of the root address
 823  * @param  area_size
 824  * @return                    DWARF type ID for given offset
 825  */
 826 static simgrid::mc::Type* get_offset_type(void *real_base_address, simgrid::mc::Type* type,
 827                                  int offset, int area_size,
 828                                  simgrid::mc::Snapshot* snapshot, int process_index)
 829 {
 830
 831   // Beginning of the block, the infered variable type if the type of the block:
 832   if (offset == 0)
 833     return type;
 834
 835   switch (type->type) {
 836
 837   case DW_TAG_structure_type:
 838   case DW_TAG_class_type:
 839     if (type->full_type)
 840       type = type->full_type;
 841     if (area_size != -1 && type->byte_size != area_size) {
 842       if (area_size > type->byte_size && area_size % type->byte_size == 0)
 843         return type;
 844       else
 845         return nullptr;
 846     }
 847
 848     for (simgrid::mc::Member& member : type->members) {
 849       if (member.has_offset_location()) {
 850         // We have the offset, use it directly (shortcut):
 851         if (member.offset() == offset)
 852           return member.type;
 853       } else {
 854         void* real_member = simgrid::dwarf::resolve_member(real_base_address, type, &member, snapshot, process_index);
 855         if ((char*)real_member - (char*)real_base_address == offset)
 856           return member.type;
 857       }
 858     }
 859     return nullptr;
 860
 861   default:
 862     /* FIXME: other cases ? */
 863     return nullptr;
 864
 865   }
 866 }
 867
 868 /**
 869  *
 870  * @param area1          Process address for state 1
 871  * @param area2          Process address for state 2
 872  * @param snapshot1      Snapshot of state 1
 873  * @param snapshot2      Snapshot of state 2
 874  * @param previous       Pairs of blocks already compared on the current path (or nullptr)
 875  * @param type_id        Type of variable
 876  * @param pointer_level
 877  * @return 0 (same), 1 (different), -1
 878  */
 879 static
 880 int compare_heap_area(simgrid::mc::StateComparator& state, int process_index,
 881                       const void *area1, const void *area2,
 882                       simgrid::mc::Snapshot* snapshot1,
 883                       simgrid::mc::Snapshot* snapshot2,
 884                       HeapLocationPairs* previous,
 885                       simgrid::mc::Type* type, int pointer_level)
 886 {
 887   simgrid::mc::RemoteClient* process = &mc_model_checker->process();
 888
 889   ssize_t block1;
 890   ssize_t block2;
 891   ssize_t size;
 892   int check_ignore = 0;
 893
 894   int type_size = -1;
 895   int offset1   = 0;
 896   int offset2   = 0;
 897   int new_size1 = -1;
 898   int new_size2 = -1;
 899
 900   simgrid::mc::Type* new_type1 = nullptr;
 901   simgrid::mc::Type* new_type2 = nullptr;
 902
 903   bool match_pairs = false;
 904
 905   // This is the address of std_heap->heapinfo in the application process:
 906   void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo;
 907
 908   const malloc_info* heapinfos1 = snapshot1->read(remote((const malloc_info**)heapinfo_address), process_index);
 909   const malloc_info* heapinfos2 = snapshot2->read(remote((const malloc_info**)heapinfo_address), process_index);
 910
 911   malloc_info heapinfo_temp1;
 912   malloc_info heapinfo_temp2;
 913
 914   simgrid::mc::HeapLocationPairs current;
 915   if (previous == nullptr) {
 916     previous = &current;
 917     match_pairs = true;
 918   }
 919
 920   // Get block number:
 921   block1 = ((char*)area1 - (char*)state.std_heap_copy.heapbase) / BLOCKSIZE + 1;
 922   block2 = ((char*)area2 - (char*)state.std_heap_copy.heapbase) / BLOCKSIZE + 1;
 923
 924   // If either block is a stack block:
 925   if (is_block_stack((int) block1) && is_block_stack((int) block2)) {
 926     previous->insert(simgrid::mc::makeHeapLocationPair(block1, -1, block2, -1));
 927     if (match_pairs)
 928       state.match_equals(previous);
 929     return 0;
 930   }
 931
 932   // If either block is not in the expected area of memory:
 933   if (((char*)area1 < (char*)state.std_heap_copy.heapbase) || (block1 > (ssize_t)state.processStates[0].heapsize) ||
 934       (block1 < 1) || ((char*)area2 < (char*)state.std_heap_copy.heapbase) ||
 935       (block2 > (ssize_t)state.processStates[1].heapsize) || (block2 < 1)) {
 936     return 1;
 937   }
 938
 939   // Process address of the block:
 940   void* real_addr_block1 = (ADDR2UINT(block1) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
 941   void* real_addr_block2 = (ADDR2UINT(block2) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
 942
 943   if (type) {
 944     if (type->full_type)
 945       type = type->full_type;
 946
 947     // This assume that for "boring" types (volatile ...) byte_size is absent:
 948     while (type->byte_size == 0 && type->subtype != nullptr)
 949       type = type->subtype;
 950
 951     // Find type_size:
 952     if (type->type == DW_TAG_pointer_type ||
 953         (type->type == DW_TAG_base_type && not type->name.empty() && type->name == "char"))
 954       type_size = -1;
 955     else
 956       type_size = type->byte_size;
 957
 958   }
 959
 960   simgrid::mc::RegionSnapshot* heap_region1 = MC_get_heap_region(snapshot1);
 961   simgrid::mc::RegionSnapshot* heap_region2 = MC_get_heap_region(snapshot2);
 962
 963   const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(
 964     heap_region1, &heapinfo_temp1, &heapinfos1[block1], sizeof(malloc_info));
 965   const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(
 966     heap_region2, &heapinfo_temp2, &heapinfos2[block2], sizeof(malloc_info));
 967
 968   if ((heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type==MMALLOC_TYPE_HEAPINFO)
 969     && (heapinfo2->type == MMALLOC_TYPE_FREE || heapinfo2->type ==MMALLOC_TYPE_HEAPINFO)) {
 970     /* Free block */
 971     if (match_pairs)
 972       state.match_equals(previous);
 973     return 0;
 974   }
 975
 976   if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED && heapinfo2->type == MMALLOC_TYPE_UNFRAGMENTED) {
 977     /* Complete block */
 978
 979     // TODO, lookup variable type from block type as done for fragmented blocks
 980
 981     if (state.equals_to1_(block1, 0).valid_ && state.equals_to2_(block2, 0).valid_ &&
 982         state.blocksEqual(block1, block2)) {
 983       if (match_pairs)
 984         state.match_equals(previous);
 985       return 0;
 986     }
 987
 988     if (type_size != -1 && type_size != (ssize_t)heapinfo1->busy_block.busy_size &&
 989         type_size != (ssize_t)heapinfo2->busy_block.busy_size &&
 990         (type->name.empty() || type->name == "struct s_smx_context")) {
 991       if (match_pairs)
 992         state.match_equals(previous);
 993       return -1;
 994     }
 995
 996     if (heapinfo1->busy_block.size != heapinfo2->busy_block.size)
 997       return 1;
 998     if (heapinfo1->busy_block.busy_size != heapinfo2->busy_block.busy_size)
 999       return 1;
1000
1001     if (not previous->insert(simgrid::mc::makeHeapLocationPair(block1, -1, block2, -1)).second) {
1002       if (match_pairs)
1003         state.match_equals(previous);
1004       return 0;
1005     }
1006
1007     size = heapinfo1->busy_block.busy_size;
1008
1009     // Remember (basic) type inference.
1010     // The current data structure only allows us to do this for the whole block.
1011     if (type != nullptr && area1 == real_addr_block1)
1012       state.types1_(block1, 0) = type;
1013     if (type != nullptr && area2 == real_addr_block2)
1014       state.types2_(block2, 0) = type;
1015
1016     if (size <= 0) {
1017       if (match_pairs)
1018         state.match_equals(previous);
1019       return 0;
1020     }
1021
1022     if (heapinfo1->busy_block.ignore > 0
1023         && heapinfo2->busy_block.ignore == heapinfo1->busy_block.ignore)
1024       check_ignore = heapinfo1->busy_block.ignore;
1025
1026   } else if ((heapinfo1->type > 0) && (heapinfo2->type > 0)) {      /* Fragmented block */
1027
1028     // Fragment number:
1029     ssize_t frag1 = ((uintptr_t)(ADDR2UINT(area1) % (BLOCKSIZE))) >> heapinfo1->type;
1030     ssize_t frag2 = ((uintptr_t)(ADDR2UINT(area2) % (BLOCKSIZE))) >> heapinfo2->type;
1031
1032     // Process address of the fragment_:
1033     void* real_addr_frag1 = (void*)((char*)real_addr_block1 + (frag1 << heapinfo1->type));
1034     void* real_addr_frag2 = (void*)((char*)real_addr_block2 + (frag2 << heapinfo2->type));
1035
1036     // Check the size of the fragments against the size of the type:
1037     if (type_size != -1) {
1038       if (heapinfo1->busy_frag.frag_size[frag1] == -1 || heapinfo2->busy_frag.frag_size[frag2] == -1) {
1039         if (match_pairs)
1040           state.match_equals(previous);
1041         return -1;
1042       }
1043       // ?
1044       if (type_size != heapinfo1->busy_frag.frag_size[frag1]
1045           || type_size != heapinfo2->busy_frag.frag_size[frag2]) {
1046         if (match_pairs)
1047           state.match_equals(previous);
1048         return -1;
1049       }
1050     }
1051
1052     // Check if the blocks are already matched together:
1053     if (state.equals_to1_(block1, frag1).valid_ && state.equals_to2_(block2, frag2).valid_ && offset1 == offset2 &&
1054         state.fragmentsEqual(block1, frag1, block2, frag2)) {
1055       if (match_pairs)
1056         state.match_equals(previous);
1057       return 0;
1058     }
1059     // Compare the size of both fragments:
1060     if (heapinfo1->busy_frag.frag_size[frag1] != heapinfo2->busy_frag.frag_size[frag2]) {
1061       if (type_size == -1) {
1062         if (match_pairs)
1063           state.match_equals(previous);
1064         return -1;
1065       } else
1066         return 1;
1067     }
1068
1069     // Size of the fragment_:
1070     size = heapinfo1->busy_frag.frag_size[frag1];
1071
1072     // Remember (basic) type inference.
1073     // The current data structure only allows us to do this for the whole fragment_.
1074     if (type != nullptr && area1 == real_addr_frag1)
1075       state.types1_(block1, frag1) = type;
1076     if (type != nullptr && area2 == real_addr_frag2)
1077       state.types2_(block2, frag2) = type;
1078
1079     // The type of the variable is already known:
1080     if (type) {
1081       new_type1 = new_type2 = type;
1082     }
1083     // Type inference from the block type.
1084     else if (state.types1_(block1, frag1) != nullptr || state.types2_(block2, frag2) != nullptr) {
1085
1086       offset1 = (char*)area1 - (char*)real_addr_frag1;
1087       offset2 = (char*)area2 - (char*)real_addr_frag2;
1088
1089       if (state.types1_(block1, frag1) != nullptr && state.types2_(block2, frag2) != nullptr) {
1090         new_type1 =
1091             get_offset_type(real_addr_frag1, state.types1_(block1, frag1), offset1, size, snapshot1, process_index);
1092         new_type2 =
1093             get_offset_type(real_addr_frag2, state.types2_(block2, frag2), offset1, size, snapshot2, process_index);
1094       } else if (state.types1_(block1, frag1) != nullptr) {
1095         new_type1 =
1096             get_offset_type(real_addr_frag1, state.types1_(block1, frag1), offset1, size, snapshot1, process_index);
1097         new_type2 =
1098             get_offset_type(real_addr_frag2, state.types1_(block1, frag1), offset2, size, snapshot2, process_index);
1099       } else if (state.types2_(block2, frag2) != nullptr) {
1100         new_type1 =
1101             get_offset_type(real_addr_frag1, state.types2_(block2, frag2), offset1, size, snapshot1, process_index);
1102         new_type2 =
1103             get_offset_type(real_addr_frag2, state.types2_(block2, frag2), offset2, size, snapshot2, process_index);
1104       } else {
1105         if (match_pairs)
1106           state.match_equals(previous);
1107         return -1;
1108       }
1109
1110       if (new_type1 != nullptr && new_type2 != nullptr && new_type1 != new_type2) {
1111
1112         type = new_type1;
1113         while (type->byte_size == 0 && type->subtype != nullptr)
1114           type = type->subtype;
1115         new_size1 = type->byte_size;
1116
1117         type = new_type2;
1118         while (type->byte_size == 0 && type->subtype != nullptr)
1119           type = type->subtype;
1120         new_size2 = type->byte_size;
1121
1122       } else {
1123         if (match_pairs)
1124           state.match_equals(previous);
1125         return -1;
1126       }
1127     }
1128
1129     if (new_size1 > 0 && new_size1 == new_size2) {
1130       type = new_type1;
1131       size = new_size1;
1132     }
1133
1134     if (offset1 == 0 && offset2 == 0 &&
1135         not previous->insert(simgrid::mc::makeHeapLocationPair(block1, frag1, block2, frag2)).second) {
1136       if (match_pairs)
1137         state.match_equals(previous);
1138       return 0;
1139     }
1140
1141     if (size <= 0) {
1142       if (match_pairs)
1143         state.match_equals(previous);
1144       return 0;
1145     }
1146
1147     if ((heapinfo1->busy_frag.ignore[frag1] > 0) &&
1148         (heapinfo2->busy_frag.ignore[frag2] == heapinfo1->busy_frag.ignore[frag1]))
1149       check_ignore = heapinfo1->busy_frag.ignore[frag1];
1150
1151   } else
1152     return 1;
1153
1154
1155   /* Start comparison */
1156   int res_compare;
1157   if (type)
1158     res_compare = compare_heap_area_with_type(state, process_index, area1, area2, snapshot1, snapshot2, previous, type,
1159                                               size, check_ignore, pointer_level);
1160   else
1161     res_compare = compare_heap_area_without_type(state, process_index, area1, area2, snapshot1, snapshot2, previous,
1162                                                  size, check_ignore);
1163
1164   if (res_compare == 1)
1165     return res_compare;
1166
1167   if (match_pairs)
1168     state.match_equals(previous);
1169   return 0;
1170 }
1171
1172 }
1173 }
1174
1175 /************************** Snapshot comparison *******************************/
1176 /******************************************************************************/
1177
1178 static int compare_areas_with_type(simgrid::mc::StateComparator& state, int process_index, void* real_area1,
1179                                    simgrid::mc::Snapshot* snapshot1, simgrid::mc::RegionSnapshot* region1,
1180                                    void* real_area2, simgrid::mc::Snapshot* snapshot2,
1181                                    simgrid::mc::RegionSnapshot* region2, simgrid::mc::Type* type, int pointer_level)
1182 {
1183   simgrid::mc::RemoteClient* process = &mc_model_checker->process();
1184
1185   simgrid::mc::Type* subtype;
1186   simgrid::mc::Type* subsubtype;
1187   int elm_size;
1188   int i;
1189   int res;
1190
1191   do {
1192     xbt_assert(type != nullptr);
1193     switch (type->type) {
1194       case DW_TAG_unspecified_type:
1195         return 1;
1196
1197       case DW_TAG_base_type:
1198       case DW_TAG_enumeration_type:
1199       case DW_TAG_union_type:
1200         return MC_snapshot_region_memcmp(real_area1, region1, real_area2, region2, type->byte_size) != 0;
1201       case DW_TAG_typedef:
1202       case DW_TAG_volatile_type:
1203       case DW_TAG_const_type:
1204         // Poor man's TCO:
1205         type = type->subtype;
1206         continue; // restart
1207       case DW_TAG_array_type:
1208         subtype = type->subtype;
1209         switch (subtype->type) {
1210           case DW_TAG_unspecified_type:
1211             return 1;
1212
1213           case DW_TAG_base_type:
1214           case DW_TAG_enumeration_type:
1215           case DW_TAG_pointer_type:
1216           case DW_TAG_reference_type:
1217           case DW_TAG_rvalue_reference_type:
1218           case DW_TAG_structure_type:
1219           case DW_TAG_class_type:
1220           case DW_TAG_union_type:
1221             if (subtype->full_type)
1222               subtype = subtype->full_type;
1223             elm_size  = subtype->byte_size;
1224             break;
1225           case DW_TAG_const_type:
1226           case DW_TAG_typedef:
1227           case DW_TAG_volatile_type:
1228             subsubtype = subtype->subtype;
1229             if (subsubtype->full_type)
1230               subsubtype = subsubtype->full_type;
1231             elm_size     = subsubtype->byte_size;
1232             break;
1233           default:
1234             return 0;
1235         }
1236         for (i = 0; i < type->element_count; i++) {
1237           size_t off = i * elm_size;
1238           res        = compare_areas_with_type(state, process_index, (char*)real_area1 + off, snapshot1, region1,
1239                                         (char*)real_area2 + off, snapshot2, region2, type->subtype, pointer_level);
1240           if (res == 1)
1241             return res;
1242         }
1243         break;
1244       case DW_TAG_pointer_type:
1245       case DW_TAG_reference_type:
1246       case DW_TAG_rvalue_reference_type: {
1247         void* addr_pointed1 = MC_region_read_pointer(region1, real_area1);
1248         void* addr_pointed2 = MC_region_read_pointer(region2, real_area2);
1249
1250         if (type->subtype && type->subtype->type == DW_TAG_subroutine_type)
1251           return (addr_pointed1 != addr_pointed2);
1252         if (addr_pointed1 == nullptr && addr_pointed2 == nullptr)
1253           return 0;
1254         if (addr_pointed1 == nullptr || addr_pointed2 == nullptr)
1255           return 1;
1256         if (not state.compared_pointers.insert(std::make_pair(addr_pointed1, addr_pointed2)).second)
1257           return 0;
1258
1259         pointer_level++;
1260
1261         // Some cases are not handled here:
1262         // * the pointers lead to different areas (one to the heap, the other to the RW segment ...)
1263         // * a pointer leads to the read-only segment of the current object
1264         // * a pointer lead to a different ELF object
1265
1266         if (addr_pointed1 > process->heap_address && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)) {
1267           if (not(addr_pointed2 > process->heap_address && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2)))
1268             return 1;
1269           // The pointers are both in the heap:
1270           return simgrid::mc::compare_heap_area(state, process_index, addr_pointed1, addr_pointed2, snapshot1,
1271                                                 snapshot2, nullptr, type->subtype, pointer_level);
1272
1273         } else if (region1->contain(simgrid::mc::remote(addr_pointed1))) {
1274           // The pointers are both in the current object R/W segment:
1275           if (not region2->contain(simgrid::mc::remote(addr_pointed2)))
1276             return 1;
1277           if (not type->type_id)
1278             return (addr_pointed1 != addr_pointed2);
1279           else
1280             return compare_areas_with_type(state, process_index, addr_pointed1, snapshot1, region1, addr_pointed2,
1281                                            snapshot2, region2, type->subtype, pointer_level);
1282         } else {
1283
1284           // TODO, We do not handle very well the case where
1285           // it belongs to a different (non-heap) region from the current one.
1286
1287           return (addr_pointed1 != addr_pointed2);
1288         }
1289       }
1290       case DW_TAG_structure_type:
1291       case DW_TAG_class_type:
1292         for (simgrid::mc::Member& member : type->members) {
1293           void* member1 = simgrid::dwarf::resolve_member(real_area1, type, &member, snapshot1, process_index);
1294           void* member2 = simgrid::dwarf::resolve_member(real_area2, type, &member, snapshot2, process_index);
1295           simgrid::mc::RegionSnapshot* subregion1 = snapshot1->get_region(member1, process_index, region1); // region1 is hinted
1296           simgrid::mc::RegionSnapshot* subregion2 = snapshot2->get_region(member2, process_index, region2); // region2 is hinted
1297           res = compare_areas_with_type(state, process_index, member1, snapshot1, subregion1, member2, snapshot2,
1298                                         subregion2, member.type, pointer_level);
1299           if (res == 1)
1300             return res;
1301         }
1302         break;
1303       case DW_TAG_subroutine_type:
1304         return -1;
1305       default:
1306         XBT_VERB("Unknown case: %d", type->type);
1307         break;
1308     }
1309
1310     return 0;
1311   } while (true);
1312 }
1313
1314 static int compare_global_variables(simgrid::mc::StateComparator& state, simgrid::mc::ObjectInformation* object_info,
1315                                     int process_index, simgrid::mc::RegionSnapshot* r1, simgrid::mc::RegionSnapshot* r2,
1316                                     simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot* snapshot2)
1317 {
1318   xbt_assert(r1 && r2, "Missing region.");
1319
1320   std::vector<simgrid::mc::Variable>& variables = object_info->global_variables;
1321
1322   for (simgrid::mc::Variable const& current_var : variables) {
1323
1324     // If the variable is not in this object, skip it:
1325     // We do not expect to find a pointer to something which is not reachable
1326     // by the global variables.
1327     if ((char *) current_var.address < (char *) object_info->start_rw
1328         || (char *) current_var.address > (char *) object_info->end_rw)
1329       continue;
1330
1331     simgrid::mc::Type* bvariable_type = current_var.type;
1332     int res = compare_areas_with_type(state, process_index,
1333                                 (char *) current_var.address, snapshot1, r1,
1334                                 (char *) current_var.address, snapshot2, r2,
1335                                 bvariable_type, 0);
1336     if (res == 1) {
1337       XBT_VERB("Global variable %s (%p) is different between snapshots",
1338                current_var.name.c_str(),
1339                (char *) current_var.address);
1340       return 1;
1341     }
1342   }
1343
1344   return 0;
1345 }
1346
1347 static int compare_local_variables(simgrid::mc::StateComparator& state,
1348                                    int process_index,
1349                                    simgrid::mc::Snapshot* snapshot1,
1350                                    simgrid::mc::Snapshot* snapshot2,
1351                                    mc_snapshot_stack_t stack1,
1352                                    mc_snapshot_stack_t stack2)
1353 {
1354   if (stack1->local_variables.size() != stack2->local_variables.size()) {
1355     XBT_VERB("Different number of local variables");
1356     return 1;
1357   }
1358
1359     unsigned int cursor = 0;
1360     local_variable_t current_var1;
1361     local_variable_t current_var2;
1362     while (cursor < stack1->local_variables.size()) {
1363       current_var1 = &stack1->local_variables[cursor];
1364       current_var2 = &stack1->local_variables[cursor];
1365       if (current_var1->name != current_var2->name
1366           || current_var1->subprogram != current_var2->subprogram
1367           || current_var1->ip != current_var2->ip) {
1368         // TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
1369         XBT_VERB
1370             ("Different name of variable (%s - %s) "
1371              "or frame (%s - %s) or ip (%lu - %lu)",
1372              current_var1->name.c_str(),
1373              current_var2->name.c_str(),
1374              current_var1->subprogram->name.c_str(),
1375              current_var2->subprogram->name.c_str(),
1376              current_var1->ip, current_var2->ip);
1377         return 1;
1378       }
1379       // TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
1380
1381         simgrid::mc::Type* subtype = current_var1->type;
1382         int res =
1383             compare_areas_with_type(state, process_index, current_var1->address, snapshot1,
1384                                     snapshot1->get_region(current_var1->address, process_index), current_var2->address,
1385                                     snapshot2, snapshot2->get_region(current_var2->address, process_index), subtype, 0);
1386
1387         if (res == 1) {
1388           // TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
1389           XBT_VERB("Local variable %s (%p - %p) in frame %s "
1390                    "is different between snapshots",
1391                    current_var1->name.c_str(), current_var1->address, current_var2->address,
1392                    current_var1->subprogram->name.c_str());
1393           return res;
1394       }
1395       cursor++;
1396     }
1397     return 0;
1398 }
1399
1400 namespace simgrid {
1401 namespace mc {
1402
1403 static std::unique_ptr<simgrid::mc::StateComparator> state_comparator;
1404
1405 int snapshot_compare(Snapshot* s1, Snapshot* s2)
1406 {
1407   // TODO, make this a field of ModelChecker or something similar
1408   if (state_comparator == nullptr)
1409     state_comparator.reset(new StateComparator());
1410   else
1411     state_comparator->clear();
1412
1413   RemoteClient* process = &mc_model_checker->process();
1414
1415   int errors = 0;
1416
1417   int hash_result = 0;
1418   if (_sg_mc_hash) {
1419     hash_result = (s1->hash_ != s2->hash_);
1420     if (hash_result) {
1421       XBT_VERB("(%d - %d) Different hash: 0x%" PRIx64 "--0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_,
1422                s2->hash_);
1423 #ifndef MC_DEBUG
1424       return 1;
1425 #endif
1426     } else
1427       XBT_VERB("(%d - %d) Same hash: 0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_);
1428   }
1429
1430   /* Compare enabled processes */
1431   if (s1->enabled_processes_ != s2->enabled_processes_) {
1432     XBT_VERB("(%d - %d) Different amount of enabled processes", s1->num_state_, s2->num_state_);
1433     return 1;
1434   }
1435
1436   /* Compare size of stacks */
1437   int is_diff = 0;
1438   for (unsigned long i = 0; i < s1->stacks_.size(); i++) {
1439     size_t size_used1 = s1->stack_sizes_[i];
1440     size_t size_used2 = s2->stack_sizes_[i];
1441     if (size_used1 != size_used2) {
1442 #ifdef MC_DEBUG
1443       XBT_DEBUG("(%d - %d) Different size used in stacks: %zu - %zu", s1->num_state, s2->num_state, size_used1,
1444                 size_used2);
1445       errors++;
1446       is_diff = 1;
1447 #else
1448 #ifdef MC_VERBOSE
1449       XBT_VERB("(%d - %d) Different size used in stacks: %zu - %zu", s1->num_state_, s2->num_state_, size_used1,
1450                size_used2);
1451 #endif
1452       return 1;
1453 #endif
1454     }
1455   }
1456   if (is_diff) // do not proceed if there is any stacks that don't match
1457     return 1;
1458
1459   /* Init heap information used in heap comparison algorithm */
1460   xbt_mheap_t heap1 = (xbt_mheap_t)s1->read_bytes(
1461     alloca(sizeof(struct mdesc)), sizeof(struct mdesc),
1462     remote(process->heap_address),
1463     simgrid::mc::ProcessIndexMissing, simgrid::mc::ReadOptions::lazy());
1464   xbt_mheap_t heap2 = (xbt_mheap_t)s2->read_bytes(
1465     alloca(sizeof(struct mdesc)), sizeof(struct mdesc),
1466     remote(process->heap_address),
1467     simgrid::mc::ProcessIndexMissing, simgrid::mc::ReadOptions::lazy());
1468   int res_init = state_comparator->initHeapInformation(heap1, heap2, &s1->to_ignore_, &s2->to_ignore_);
1469
1470   if (res_init == -1) {
1471 #ifdef MC_DEBUG
1472     XBT_DEBUG("(%d - %d) Different heap information", num1, nus1->num_state, s2->num_statem2);
1473     errors++;
1474 #else
1475 #ifdef MC_VERBOSE
1476     XBT_VERB("(%d - %d) Different heap information", s1->num_state_, s2->num_state_);
1477 #endif
1478
1479     return 1;
1480 #endif
1481   }
1482
1483   /* Stacks comparison */
1484   int diff_local = 0;
1485   for (unsigned int cursor = 0; cursor < s1->stacks_.size(); cursor++) {
1486     mc_snapshot_stack_t stack1 = &s1->stacks_[cursor];
1487     mc_snapshot_stack_t stack2 = &s2->stacks_[cursor];
1488
1489     if (stack1->process_index != stack2->process_index) {
1490       diff_local = 1;
1491       XBT_DEBUG("(%d - %d) Stacks with different process index (%i vs %i)", s1->num_state_, s2->num_state_,
1492                 stack1->process_index, stack2->process_index);
1493     }
1494     else diff_local = compare_local_variables(*state_comparator,
1495       stack1->process_index, s1, s2, stack1, stack2);
1496     if (diff_local > 0) {
1497 #ifdef MC_DEBUG
1498       XBT_DEBUG("(%d - %d) Different local variables between stacks %d", num1,
1499                 num2, cursor + 1);
1500       errors++;
1501 #else
1502
1503 #ifdef MC_VERBOSE
1504       XBT_VERB("(%d - %d) Different local variables between stacks %u", s1->num_state_, s2->num_state_, cursor + 1);
1505 #endif
1506
1507       return 1;
1508 #endif
1509     }
1510   }
1511
1512   size_t regions_count = s1->snapshot_regions_.size();
1513   // TODO, raise a difference instead?
1514   xbt_assert(regions_count == s2->snapshot_regions_.size());
1515
1516   for (size_t k = 0; k != regions_count; ++k) {
1517     RegionSnapshot* region1 = s1->snapshot_regions_[k].get();
1518     RegionSnapshot* region2 = s2->snapshot_regions_[k].get();
1519
1520     // Preconditions:
1521     if (region1->region_type() != RegionType::Data)
1522       continue;
1523
1524     xbt_assert(region1->region_type() == region2->region_type());
1525     xbt_assert(region1->object_info() == region2->object_info());
1526     xbt_assert(region1->object_info());
1527
1528     /* Compare global variables */
1529     if (compare_global_variables(*state_comparator, region1->object_info(), simgrid::mc::ProcessIndexDisabled, region1,
1530                                  region2, s1, s2)) {
1531
1532 #ifdef MC_DEBUG
1533       std::string const& name = region1->object_info()->file_name;
1534       XBT_DEBUG("(%d - %d) Different global variables in %s", s1->num_state, s2->num_state, name.c_str());
1535       errors++;
1536 #else
1537 #ifdef MC_VERBOSE
1538       std::string const& name = region1->object_info()->file_name;
1539       XBT_VERB("(%d - %d) Different global variables in %s", s1->num_state_, s2->num_state_, name.c_str());
1540 #endif
1541
1542       return 1;
1543 #endif
1544     }
1545   }
1546
1547   /* Compare heap */
1548   if (mmalloc_compare_heap(*state_comparator, s1, s2) > 0) {
1549
1550 #ifdef MC_DEBUG
1551     XBT_DEBUG("(%d - %d) Different heap (mmalloc_compare)", s1->num_state, s2->num_state);
1552     errors++;
1553 #else
1554
1555 #ifdef MC_VERBOSE
1556     XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", s1->num_state_, s2->num_state_);
1557 #endif
1558     return 1;
1559 #endif
1560   }
1561
1562 #ifdef MC_VERBOSE
1563   if (errors || hash_result)
1564     XBT_VERB("(%d - %d) Difference found", s1->num_state_, s2->num_state_);
1565   else
1566     XBT_VERB("(%d - %d) No difference found", s1->num_state_, s2->num_state_);
1567 #endif
1568
1569 #if defined(MC_DEBUG) && defined(MC_VERBOSE)
1570   if (_sg_mc_hash) {
1571     // * false positive SHOULD be avoided.
1572     // * There MUST not be any false negative.
1573
1574     XBT_VERB("(%d - %d) State equality hash test is %s %s", s1->num_state, s2->num_state,
1575              (hash_result != 0) == (errors != 0) ? "true" : "false", not hash_result ? "positive" : "negative");
1576   }
1577 #endif
1578
1579   return errors > 0 || hash_result;
1580 }
1581
1582 }
1583 }