src/mc/mc_diff.cpp

   1 /* mc_diff - Memory snapshooting and comparison                             */
   2
   3 /* Copyright (c) 2008-2015. The SimGrid Team.
   4  * All rights reserved.                                                     */
   5
   6 /* This program is free software; you can redistribute it and/or modify it
   7  * under the terms of the license (GNU LGPL) which comes with this package. */
   8
   9 #include "xbt/ex_interface.h"   /* internals of backtrace setup */
  10 #include "xbt/str.h"
  11 #include "mc/mc.h"
  12 #include "xbt/mmalloc.h"
  13 #include "mc_object_info.h"
  14 #include "mc/datatypes.h"
  15 #include "mc/mc_private.h"
  16 #include "mc/mc_snapshot.h"
  17 #include "mc/Type.hpp"
  18
  19 using simgrid::mc::remote;
  20
  21 extern "C" {
  22
  23 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_diff, xbt,
  24                                 "Logging specific to mc_diff in mc");
  25
  26 xbt_dynar_t mc_heap_comparison_ignore;
  27 xbt_dynar_t stacks_areas;
  28
  29
  30
  31 /********************************* Backtrace ***********************************/
  32 /******************************************************************************/
  33
  34 static void mmalloc_backtrace_block_display(void *heapinfo, int block)
  35 {
  36
  37   /* xbt_ex_t e; */
  38
  39   /* if (((malloc_info *)heapinfo)[block].busy_block.bt_size == 0) { */
  40   /*   fprintf(stderr, "No backtrace available for that block, sorry.\n"); */
  41   /*   return; */
  42   /* } */
  43
  44   /* memcpy(&e.bt,&(((malloc_info *)heapinfo)[block].busy_block.bt),sizeof(void*)*XBT_BACKTRACE_SIZE); */
  45   /* e.used = ((malloc_info *)heapinfo)[block].busy_block.bt_size; */
  46
  47   /* xbt_ex_setup_backtrace(&e); */
  48   /* if (e.used == 0) { */
  49   /*   fprintf(stderr, "(backtrace not set)\n"); */
  50   /* } else if (e.bt_strings == NULL) { */
  51   /*   fprintf(stderr, "(backtrace not ready to be computed. %s)\n",xbt_binary_name?"Dunno why":"xbt_binary_name not setup yet"); */
  52   /* } else { */
  53   /*   int i; */
  54
  55   /*   fprintf(stderr, "Backtrace of where the block %d was malloced (%d frames):\n", block ,e.used); */
  56   /*   for (i = 0; i < e.used; i++)       /\* no need to display "xbt_backtrace_display" *\/{ */
  57   /*     fprintf(stderr, "%d ---> %s\n",i, e.bt_strings[i] + 4); */
  58   /*   } */
  59   /* } */
  60 }
  61
  62 static void mmalloc_backtrace_fragment_display(void *heapinfo, int block,
  63                                                int frag)
  64 {
  65
  66   /* xbt_ex_t e; */
  67
  68   /* memcpy(&e.bt,&(((malloc_info *)heapinfo)[block].busy_frag.bt[frag]),sizeof(void*)*XBT_BACKTRACE_SIZE); */
  69   /* e.used = XBT_BACKTRACE_SIZE; */
  70
  71   /* xbt_ex_setup_backtrace(&e); */
  72   /* if (e.used == 0) { */
  73   /*   fprintf(stderr, "(backtrace not set)\n"); */
  74   /* } else if (e.bt_strings == NULL) { */
  75   /*   fprintf(stderr, "(backtrace not ready to be computed. %s)\n",xbt_binary_name?"Dunno why":"xbt_binary_name not setup yet"); */
  76   /* } else { */
  77   /*   int i; */
  78
  79   /*   fprintf(stderr, "Backtrace of where the fragment %d in block %d was malloced (%d frames):\n", frag, block ,e.used); */
  80   /*   for (i = 0; i < e.used; i++)       /\* no need to display "xbt_backtrace_display" *\/{ */
  81   /*     fprintf(stderr, "%d ---> %s\n",i, e.bt_strings[i] + 4); */
  82   /*   } */
  83   /* } */
  84
  85 }
  86
  87 static void mmalloc_backtrace_display(void *addr)
  88 {
  89
  90   /* size_t block, frag_nb; */
  91   /* int type; */
  92
  93   /* block = (((char*) (addr) - (char*) heap -> heapbase) / BLOCKSIZE + 1); */
  94
  95   /* type = heap->heapinfo[block].type; */
  96
  97   /* switch(type){ */
  98   /* case MMALLOC_TYPE_HEAPINFO :  */
  99   /* case MMALLOC_TYPE_FREE : /\* Free block *\/ */
 100   /*   fprintf(stderr, "Asked to display the backtrace of a block that is free. I'm puzzled\n"); */
 101   /*   xbt_abort(); */
 102   /*   break;  */
 103   /* case 0: /\* Large block *\/ */
 104   /*   mmalloc_backtrace_block_display(heap->heapinfo, block); */
 105   /*   break; */
 106   /* default: /\* Fragmented block *\/ */
 107   /*   frag_nb = RESIDUAL(addr, BLOCKSIZE) >> type; */
 108   /*   if(heap->heapinfo[block].busy_frag.frag_size[frag_nb] == -1){ */
 109   /*     fprintf(stderr , "Asked to display the backtrace of a fragment that is free. I'm puzzled\n"); */
 110   /*     xbt_abort(); */
 111   /*   } */
 112   /*   mmalloc_backtrace_fragment_display(heap->heapinfo, block, frag_nb); */
 113   /*   break; */
 114   /* } */
 115 }
 116
 117
 118 static int compare_backtrace(int b1, int f1, int b2, int f2)
 119 {
 120   /*int i = 0;
 121      if(f1 != -1){
 122      for(i=0; i< XBT_BACKTRACE_SIZE; i++){
 123      if(heapinfo1[b1].busy_frag.bt[f1][i] != heapinfo2[b2].busy_frag.bt[f2][i]){
 124      //mmalloc_backtrace_fragment_display((void*)heapinfo1, b1, f1);
 125      //mmalloc_backtrace_fragment_display((void*)heapinfo2, b2, f2);
 126      return 1;
 127      }
 128      }
 129      }else{
 130      for(i=0; i< heapinfo1[b1].busy_block.bt_size; i++){
 131      if(heapinfo1[b1].busy_block.bt[i] != heapinfo2[b2].busy_block.bt[i]){
 132      //mmalloc_backtrace_block_display((void*)heapinfo1, b1);
 133      //mmalloc_backtrace_block_display((void*)heapinfo2, b2);
 134      return 1;
 135      }
 136      }
 137      } */
 138   return 0;
 139 }
 140
 141
 142 /*********************************** Heap comparison ***********************************/
 143 /***************************************************************************************/
 144
 145 typedef char *type_name;
 146
 147 struct s_mc_diff {
 148   s_xbt_mheap_t std_heap_copy;
 149   size_t heaplimit;
 150   // Number of blocks in the heaps:
 151   size_t heapsize1, heapsize2;
 152   std::vector<s_mc_heap_ignore_region_t>* to_ignore1;
 153   std::vector<s_mc_heap_ignore_region_t>* to_ignore2;
 154   s_heap_area_t *equals_to1, *equals_to2;
 155   simgrid::mc::Type **types1;
 156   simgrid::mc::Type **types2;
 157   size_t available;
 158 };
 159
 160 #define equals_to1_(i,j) equals_to1[ MAX_FRAGMENT_PER_BLOCK*(i) + (j)]
 161 #define equals_to2_(i,j) equals_to2[ MAX_FRAGMENT_PER_BLOCK*(i) + (j)]
 162 #define types1_(i,j) types1[ MAX_FRAGMENT_PER_BLOCK*(i) + (j)]
 163 #define types2_(i,j) types2[ MAX_FRAGMENT_PER_BLOCK*(i) + (j)]
 164
 165 __thread struct s_mc_diff *mc_diff_info = NULL;
 166
 167 /*********************************** Free functions ************************************/
 168
 169 static void heap_area_pair_free(heap_area_pair_t pair)
 170 {
 171   xbt_free(pair);
 172   pair = NULL;
 173 }
 174
 175 static void heap_area_pair_free_voidp(void *d)
 176 {
 177   heap_area_pair_free((heap_area_pair_t) * (void **) d);
 178 }
 179
 180 static void heap_area_free(heap_area_t area)
 181 {
 182   xbt_free(area);
 183   area = NULL;
 184 }
 185
 186 /************************************************************************************/
 187
 188 static s_heap_area_t make_heap_area(int block, int fragment)
 189 {
 190   s_heap_area_t area;
 191   area.valid = 1;
 192   area.block = block;
 193   area.fragment = fragment;
 194   return area;
 195 }
 196
 197
 198 static int is_new_heap_area_pair(xbt_dynar_t list, int block1, int fragment1,
 199                                  int block2, int fragment2)
 200 {
 201
 202   unsigned int cursor = 0;
 203   heap_area_pair_t current_pair;
 204
 205   xbt_dynar_foreach(list, cursor, current_pair) {
 206     if (current_pair->block1 == block1 && current_pair->block2 == block2
 207         && current_pair->fragment1 == fragment1
 208         && current_pair->fragment2 == fragment2)
 209       return 0;
 210   }
 211
 212   return 1;
 213 }
 214
 215 static int add_heap_area_pair(xbt_dynar_t list, int block1, int fragment1,
 216                               int block2, int fragment2)
 217 {
 218
 219   if (is_new_heap_area_pair(list, block1, fragment1, block2, fragment2)) {
 220     heap_area_pair_t pair = NULL;
 221     pair = xbt_new0(s_heap_area_pair_t, 1);
 222     pair->block1 = block1;
 223     pair->fragment1 = fragment1;
 224     pair->block2 = block2;
 225     pair->fragment2 = fragment2;
 226
 227     xbt_dynar_push(list, &pair);
 228
 229     return 1;
 230   }
 231
 232   return 0;
 233 }
 234
 235 static ssize_t heap_comparison_ignore_size(std::vector<s_mc_heap_ignore_region_t>* ignore_list,
 236                                            const void *address)
 237 {
 238   int start = 0;
 239   int end = ignore_list->size() - 1;
 240
 241   while (start <= end) {
 242     unsigned int cursor = (start + end) / 2;
 243     s_mc_heap_ignore_region_t region = (*ignore_list)[cursor];
 244     if (region.address == address)
 245       return region.size;
 246     if (region.address < address)
 247       start = cursor + 1;
 248     if (region.address > address)
 249       end = cursor - 1;
 250   }
 251
 252   return -1;
 253 }
 254
 255 static int is_stack(const void *address)
 256 {
 257   unsigned int cursor = 0;
 258   stack_region_t stack;
 259
 260   xbt_dynar_foreach(stacks_areas, cursor, stack) {
 261     if (address == stack->address)
 262       return 1;
 263   }
 264
 265   return 0;
 266 }
 267
 268 // TODO, this should depend on the snapshot?
 269 static int is_block_stack(int block)
 270 {
 271   unsigned int cursor = 0;
 272   stack_region_t stack;
 273
 274   xbt_dynar_foreach(stacks_areas, cursor, stack) {
 275     if (block == stack->block)
 276       return 1;
 277   }
 278
 279   return 0;
 280 }
 281
 282 static void match_equals(struct s_mc_diff *state, xbt_dynar_t list)
 283 {
 284
 285   unsigned int cursor = 0;
 286   heap_area_pair_t current_pair;
 287
 288   xbt_dynar_foreach(list, cursor, current_pair) {
 289
 290     if (current_pair->fragment1 != -1) {
 291
 292       state->equals_to1_(current_pair->block1, current_pair->fragment1) =
 293           make_heap_area(current_pair->block2, current_pair->fragment2);
 294       state->equals_to2_(current_pair->block2, current_pair->fragment2) =
 295           make_heap_area(current_pair->block1, current_pair->fragment1);
 296
 297     } else {
 298
 299       state->equals_to1_(current_pair->block1, 0) =
 300           make_heap_area(current_pair->block2, current_pair->fragment2);
 301       state->equals_to2_(current_pair->block2, 0) =
 302           make_heap_area(current_pair->block1, current_pair->fragment1);
 303
 304     }
 305
 306   }
 307 }
 308
 309 /** Check whether two blocks are known to be matching
 310  *
 311  *  @param state  State used
 312  *  @param b1     Block of state 1
 313  *  @param b2     Block of state 2
 314  *  @return       if the blocks are known to be matching
 315  */
 316 static int equal_blocks(struct s_mc_diff *state, int b1, int b2)
 317 {
 318
 319   if (state->equals_to1_(b1, 0).block == b2
 320       && state->equals_to2_(b2, 0).block == b1)
 321     return 1;
 322
 323   return 0;
 324 }
 325
 326 /** Check whether two fragments are known to be matching
 327  *
 328  *  @param state  State used
 329  *  @param b1     Block of state 1
 330  *  @param f1     Fragment of state 1
 331  *  @param b2     Block of state 2
 332  *  @param f2     Fragment of state 2
 333  *  @return       if the fragments are known to be matching
 334  */
 335 static int equal_fragments(struct s_mc_diff *state, int b1, int f1, int b2,
 336                            int f2)
 337 {
 338
 339   if (state->equals_to1_(b1, f1).block == b2
 340       && state->equals_to1_(b1, f1).fragment == f2
 341       && state->equals_to2_(b2, f2).block == b1
 342       && state->equals_to2_(b2, f2).fragment == f1)
 343     return 1;
 344
 345   return 0;
 346 }
 347
 348 }
 349
 350 int init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2,
 351                           std::vector<s_mc_heap_ignore_region_t>* i1,
 352                           std::vector<s_mc_heap_ignore_region_t>* i2)
 353 {
 354   if (mc_diff_info == NULL) {
 355     mc_diff_info = xbt_new0(struct s_mc_diff, 1);
 356     mc_diff_info->equals_to1 = NULL;
 357     mc_diff_info->equals_to2 = NULL;
 358     mc_diff_info->types1 = NULL;
 359     mc_diff_info->types2 = NULL;
 360   }
 361   struct s_mc_diff *state = mc_diff_info;
 362
 363   if ((((struct mdesc *) heap1)->heaplimit !=
 364        ((struct mdesc *) heap2)->heaplimit)
 365       ||
 366       ((((struct mdesc *) heap1)->heapsize !=
 367         ((struct mdesc *) heap2)->heapsize)))
 368     return -1;
 369
 370   state->heaplimit = ((struct mdesc *) heap1)->heaplimit;
 371
 372   state->std_heap_copy = *mc_model_checker->process().get_heap();
 373
 374   state->heapsize1 = heap1->heapsize;
 375   state->heapsize2 = heap2->heapsize;
 376
 377   state->to_ignore1 = i1;
 378   state->to_ignore2 = i2;
 379
 380   if (state->heaplimit > state->available) {
 381     state->equals_to1 = (s_heap_area_t*)
 382         realloc(state->equals_to1,
 383                 state->heaplimit * MAX_FRAGMENT_PER_BLOCK *
 384                 sizeof(s_heap_area_t));
 385     state->types1 = (simgrid::mc::Type**)
 386         realloc(state->types1,
 387                 state->heaplimit * MAX_FRAGMENT_PER_BLOCK *
 388                 sizeof(simgrid::mc::Type*));
 389     state->equals_to2 = (s_heap_area_t*)
 390         realloc(state->equals_to2,
 391                 state->heaplimit * MAX_FRAGMENT_PER_BLOCK *
 392                 sizeof(s_heap_area_t));
 393     state->types2 = (simgrid::mc::Type**)
 394         realloc(state->types2,
 395                 state->heaplimit * MAX_FRAGMENT_PER_BLOCK *
 396                 sizeof(simgrid::mc::Type*));
 397     state->available = state->heaplimit;
 398   }
 399
 400   memset(state->equals_to1, 0,
 401          state->heaplimit * MAX_FRAGMENT_PER_BLOCK * sizeof(s_heap_area_t));
 402   memset(state->equals_to2, 0,
 403          state->heaplimit * MAX_FRAGMENT_PER_BLOCK * sizeof(s_heap_area_t));
 404   memset(state->types1, 0,
 405          state->heaplimit * MAX_FRAGMENT_PER_BLOCK * sizeof(type_name *));
 406   memset(state->types2, 0,
 407          state->heaplimit * MAX_FRAGMENT_PER_BLOCK * sizeof(type_name *));
 408
 409   return 0;
 410
 411 }
 412
 413 extern "C" {
 414
 415 void reset_heap_information()
 416 {
 417
 418 }
 419
 420 // TODO, have a robust way to find it in O(1)
 421 static inline
 422 mc_mem_region_t MC_get_heap_region(mc_snapshot_t snapshot)
 423 {
 424   size_t n = snapshot->snapshot_regions.size();
 425   for (size_t i=0; i!=n; ++i) {
 426     mc_mem_region_t region = snapshot->snapshot_regions[i].get();
 427     if (region->region_type() == simgrid::mc::RegionType::Heap)
 428       return region;
 429   }
 430   xbt_die("No heap region");
 431 }
 432
 433 int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
 434 {
 435   simgrid::mc::Process* process = &mc_model_checker->process();
 436   struct s_mc_diff *state = mc_diff_info;
 437
 438   /* Start comparison */
 439   size_t i1, i2, j1, j2, k;
 440   void *addr_block1, *addr_block2, *addr_frag1, *addr_frag2;
 441   int nb_diff1 = 0, nb_diff2 = 0;
 442
 443   int equal, res_compare = 0;
 444
 445   /* Check busy blocks */
 446
 447   i1 = 1;
 448
 449   malloc_info heapinfo_temp1, heapinfo_temp2;
 450   malloc_info heapinfo_temp2b;
 451
 452   mc_mem_region_t heap_region1 = MC_get_heap_region(snapshot1);
 453   mc_mem_region_t heap_region2 = MC_get_heap_region(snapshot2);
 454
 455   // This is the address of std_heap->heapinfo in the application process:
 456   void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo;
 457
 458   // This is in snapshot do not use them directly:
 459   const malloc_info* heapinfos1 = snapshot1->read<malloc_info*>(
 460     (std::uint64_t)heapinfo_address, simgrid::mc::ProcessIndexMissing);
 461   const malloc_info* heapinfos2 = snapshot2->read<malloc_info*>(
 462     (std::uint64_t)heapinfo_address, simgrid::mc::ProcessIndexMissing);
 463
 464   while (i1 <= state->heaplimit) {
 465
 466     const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(heap_region1, &heapinfo_temp1, &heapinfos1[i1], sizeof(malloc_info));
 467     const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(heap_region2, &heapinfo_temp2, &heapinfos2[i1], sizeof(malloc_info));
 468
 469     if (heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type == MMALLOC_TYPE_HEAPINFO) {      /* Free block */
 470       i1 ++;
 471       continue;
 472     }
 473
 474     if (heapinfo1->type < 0) {
 475       fprintf(stderr, "Unkown mmalloc block type.\n");
 476       abort();
 477     }
 478
 479     addr_block1 =
 480         ((void *) (((ADDR2UINT(i1)) - 1) * BLOCKSIZE +
 481                    (char *) state->std_heap_copy.heapbase));
 482
 483     if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED) {       /* Large block */
 484
 485       if (is_stack(addr_block1)) {
 486         for (k = 0; k < heapinfo1->busy_block.size; k++)
 487           state->equals_to1_(i1 + k, 0) = make_heap_area(i1, -1);
 488         for (k = 0; k < heapinfo2->busy_block.size; k++)
 489           state->equals_to2_(i1 + k, 0) = make_heap_area(i1, -1);
 490         i1 += heapinfo1->busy_block.size;
 491         continue;
 492       }
 493
 494       if (state->equals_to1_(i1, 0).valid) {
 495         i1++;
 496         continue;
 497       }
 498
 499       i2 = 1;
 500       equal = 0;
 501       res_compare = 0;
 502
 503       /* Try first to associate to same block in the other heap */
 504       if (heapinfo2->type == heapinfo1->type) {
 505
 506         if (state->equals_to2_(i1, 0).valid == 0) {
 507
 508           addr_block2 = (ADDR2UINT(i1) - 1) * BLOCKSIZE +
 509                          (char *) state->std_heap_copy.heapbase;
 510
 511           res_compare =
 512               compare_heap_area(simgrid::mc::ProcessIndexMissing, addr_block1, addr_block2, snapshot1, snapshot2,
 513                                 NULL, NULL, 0);
 514
 515           if (res_compare != 1) {
 516             for (k = 1; k < heapinfo2->busy_block.size; k++)
 517               state->equals_to2_(i1 + k, 0) = make_heap_area(i1, -1);
 518             for (k = 1; k < heapinfo1->busy_block.size; k++)
 519               state->equals_to1_(i1 + k, 0) = make_heap_area(i1, -1);
 520             equal = 1;
 521             i1 += heapinfo1->busy_block.size;
 522           }
 523
 524         }
 525
 526       }
 527
 528       while (i2 <= state->heaplimit && !equal) {
 529
 530         addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE +
 531                        (char *) state->std_heap_copy.heapbase;
 532
 533         if (i2 == i1) {
 534           i2++;
 535           continue;
 536         }
 537
 538         const malloc_info* heapinfo2b = (const malloc_info*) MC_region_read(heap_region2, &heapinfo_temp2b, &heapinfos2[i2], sizeof(malloc_info));
 539
 540         if (heapinfo2b->type != MMALLOC_TYPE_UNFRAGMENTED) {
 541           i2++;
 542           continue;
 543         }
 544
 545         if (state->equals_to2_(i2, 0).valid) {
 546           i2++;
 547           continue;
 548         }
 549
 550         res_compare =
 551             compare_heap_area(simgrid::mc::ProcessIndexMissing, addr_block1, addr_block2, snapshot1, snapshot2,
 552                               NULL, NULL, 0);
 553
 554         if (res_compare != 1) {
 555           for (k = 1; k < heapinfo2b->busy_block.size; k++)
 556             state->equals_to2_(i2 + k, 0) = make_heap_area(i1, -1);
 557           for (k = 1; k < heapinfo1->busy_block.size; k++)
 558             state->equals_to1_(i1 + k, 0) = make_heap_area(i2, -1);
 559           equal = 1;
 560           i1 += heapinfo1->busy_block.size;
 561         }
 562
 563         i2++;
 564
 565       }
 566
 567       if (!equal) {
 568         XBT_DEBUG("Block %zu not found (size_used = %zu, addr = %p)", i1,
 569                   heapinfo1->busy_block.busy_size, addr_block1);
 570         i1 = state->heaplimit + 1;
 571         nb_diff1++;
 572         //i1++;
 573       }
 574
 575     } else {                    /* Fragmented block */
 576
 577       for (j1 = 0; j1 < (size_t) (BLOCKSIZE >> heapinfo1->type); j1++) {
 578
 579         if (heapinfo1->busy_frag.frag_size[j1] == -1) /* Free fragment */
 580           continue;
 581
 582         if (state->equals_to1_(i1, j1).valid)
 583           continue;
 584
 585         addr_frag1 =
 586             (void *) ((char *) addr_block1 + (j1 << heapinfo1->type));
 587
 588         i2 = 1;
 589         equal = 0;
 590
 591         /* Try first to associate to same fragment in the other heap */
 592         if (heapinfo2->type == heapinfo1->type) {
 593
 594           if (state->equals_to2_(i1, j1).valid == 0) {
 595
 596             addr_block2 = (ADDR2UINT(i1) - 1) * BLOCKSIZE +
 597                            (char *) state->std_heap_copy.heapbase;
 598             addr_frag2 =
 599                 (void *) ((char *) addr_block2 +
 600                           (j1 << heapinfo2->type));
 601
 602             res_compare =
 603                 compare_heap_area(simgrid::mc::ProcessIndexMissing, addr_frag1, addr_frag2, snapshot1, snapshot2,
 604                                   NULL, NULL, 0);
 605
 606             if (res_compare != 1)
 607               equal = 1;
 608
 609           }
 610
 611         }
 612
 613         while (i2 <= state->heaplimit && !equal) {
 614
 615           const malloc_info* heapinfo2b = (const malloc_info*) MC_region_read(
 616             heap_region2, &heapinfo_temp2b, &heapinfos2[i2],
 617             sizeof(malloc_info));
 618
 619           if (heapinfo2b->type == MMALLOC_TYPE_FREE || heapinfo2b->type == MMALLOC_TYPE_HEAPINFO) {
 620             i2 ++;
 621             continue;
 622           }
 623
 624           // We currently do not match fragments with unfragmented blocks (maybe we should).
 625           if (heapinfo2b->type == MMALLOC_TYPE_UNFRAGMENTED) {
 626             i2++;
 627             continue;
 628           }
 629
 630           if (heapinfo2b->type < 0) {
 631             fprintf(stderr, "Unkown mmalloc block type.\n");
 632             abort();
 633           }
 634
 635           for (j2 = 0; j2 < (size_t) (BLOCKSIZE >> heapinfo2b->type);
 636                j2++) {
 637
 638             if (i2 == i1 && j2 == j1)
 639               continue;
 640
 641             if (state->equals_to2_(i2, j2).valid)
 642               continue;
 643
 644             addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE +
 645                            (char *) state->std_heap_copy.heapbase;
 646             addr_frag2 =
 647                 (void *) ((char *) addr_block2 +
 648                           (j2 << heapinfo2b->type));
 649
 650             res_compare =
 651                 compare_heap_area(simgrid::mc::ProcessIndexMissing, addr_frag1, addr_frag2, snapshot2, snapshot2,
 652                                   NULL, NULL, 0);
 653
 654             if (res_compare != 1) {
 655               equal = 1;
 656               break;
 657             }
 658
 659           }
 660
 661           i2++;
 662
 663         }
 664
 665         if (!equal) {
 666           XBT_DEBUG
 667               ("Block %zu, fragment %zu not found (size_used = %zd, address = %p)\n",
 668                i1, j1, heapinfo1->busy_frag.frag_size[j1],
 669                addr_frag1);
 670           i2 = state->heaplimit + 1;
 671           i1 = state->heaplimit + 1;
 672           nb_diff1++;
 673           break;
 674         }
 675
 676       }
 677
 678       i1++;
 679
 680     }
 681
 682   }
 683
 684   /* All blocks/fragments are equal to another block/fragment ? */
 685   size_t i = 1, j = 0;
 686
 687   for(i = 1; i <= state->heaplimit; i++) {
 688     const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(
 689       heap_region1, &heapinfo_temp1, &heapinfos1[i], sizeof(malloc_info));
 690     if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED) {
 691       if (i1 == state->heaplimit) {
 692         if (heapinfo1->busy_block.busy_size > 0) {
 693           if (state->equals_to1_(i, 0).valid == 0) {
 694             if (XBT_LOG_ISENABLED(mc_diff, xbt_log_priority_debug)) {
 695               // TODO, add address
 696               XBT_DEBUG("Block %zu not found (size used = %zu)", i,
 697                         heapinfo1->busy_block.busy_size);
 698               //mmalloc_backtrace_block_display((void*)heapinfo1, i);
 699             }
 700             nb_diff1++;
 701           }
 702         }
 703       }
 704     }
 705     if (heapinfo1->type > 0) {
 706       for (j = 0; j < (size_t) (BLOCKSIZE >> heapinfo1->type); j++) {
 707         if (i1 == state->heaplimit) {
 708           if (heapinfo1->busy_frag.frag_size[j] > 0) {
 709             if (state->equals_to1_(i, j).valid == 0) {
 710               if (XBT_LOG_ISENABLED(mc_diff, xbt_log_priority_debug)) {
 711                 // TODO, print fragment address
 712                 XBT_DEBUG
 713                     ("Block %zu, Fragment %zu not found (size used = %zd)",
 714                      i, j,
 715                      heapinfo1->busy_frag.frag_size[j]);
 716                 //mmalloc_backtrace_fragment_display((void*)heapinfo1, i, j);
 717               }
 718               nb_diff1++;
 719             }
 720           }
 721         }
 722       }
 723     }
 724   }
 725
 726   if (i1 == state->heaplimit)
 727     XBT_DEBUG("Number of blocks/fragments not found in heap1 : %d", nb_diff1);
 728
 729   for (i=1; i <= state->heaplimit; i++) {
 730     const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(
 731       heap_region2, &heapinfo_temp2, &heapinfos2[i], sizeof(malloc_info));
 732     if (heapinfo2->type == MMALLOC_TYPE_UNFRAGMENTED) {
 733       if (i1 == state->heaplimit) {
 734         if (heapinfo2->busy_block.busy_size > 0) {
 735           if (state->equals_to2_(i, 0).valid == 0) {
 736             if (XBT_LOG_ISENABLED(mc_diff, xbt_log_priority_debug)) {
 737               // TODO, print address of the block
 738               XBT_DEBUG("Block %zu not found (size used = %zu)", i,
 739                         heapinfo2->busy_block.busy_size);
 740               //mmalloc_backtrace_block_display((void*)heapinfo2, i);
 741             }
 742             nb_diff2++;
 743           }
 744         }
 745       }
 746     }
 747     if (heapinfo2->type > 0) {
 748       for (j = 0; j < (size_t) (BLOCKSIZE >> heapinfo2->type); j++) {
 749         if (i1 == state->heaplimit) {
 750           if (heapinfo2->busy_frag.frag_size[j] > 0) {
 751             if (state->equals_to2_(i, j).valid == 0) {
 752               if (XBT_LOG_ISENABLED(mc_diff, xbt_log_priority_debug)) {
 753                 // TODO, print address of the block
 754                 XBT_DEBUG
 755                     ("Block %zu, Fragment %zu not found (size used = %zd)",
 756                      i, j,
 757                      heapinfo2->busy_frag.frag_size[j]);
 758                 //mmalloc_backtrace_fragment_display((void*)heapinfo2, i, j);
 759               }
 760               nb_diff2++;
 761             }
 762           }
 763         }
 764       }
 765     }
 766   }
 767
 768   if (i1 == state->heaplimit)
 769     XBT_DEBUG("Number of blocks/fragments not found in heap2 : %d", nb_diff2);
 770
 771   return ((nb_diff1 > 0) || (nb_diff2 > 0));
 772 }
 773
 774 /**
 775  *
 776  * @param state
 777  * @param real_area1     Process address for state 1
 778  * @param real_area2     Process address for state 2
 779  * @param snapshot1      Snapshot of state 1
 780  * @param snapshot2      Snapshot of state 2
 781  * @param previous
 782  * @param size
 783  * @param check_ignore
 784  */
 785 static int compare_heap_area_without_type(struct s_mc_diff *state, int process_index,
 786                                           const void *real_area1, const void *real_area2,
 787                                           mc_snapshot_t snapshot1,
 788                                           mc_snapshot_t snapshot2,
 789                                           xbt_dynar_t previous, int size,
 790                                           int check_ignore)
 791 {
 792   simgrid::mc::Process* process = &mc_model_checker->process();
 793
 794   int i = 0;
 795   const void *addr_pointed1, *addr_pointed2;
 796   int pointer_align, res_compare;
 797   ssize_t ignore1, ignore2;
 798
 799   mc_mem_region_t heap_region1 = MC_get_heap_region(snapshot1);
 800   mc_mem_region_t heap_region2 = MC_get_heap_region(snapshot2);
 801
 802   while (i < size) {
 803
 804     if (check_ignore > 0) {
 805       if ((ignore1 =
 806            heap_comparison_ignore_size(state->to_ignore1,
 807                                        (char *) real_area1 + i)) != -1) {
 808         if ((ignore2 =
 809              heap_comparison_ignore_size(state->to_ignore2,
 810                                          (char *) real_area2 + i)) == ignore1) {
 811           if (ignore1 == 0) {
 812             check_ignore--;
 813             return 0;
 814           } else {
 815             i = i + ignore2;
 816             check_ignore--;
 817             continue;
 818           }
 819         }
 820       }
 821     }
 822
 823     if (MC_snapshot_region_memcmp(((char *) real_area1) + i, heap_region1, ((char *) real_area2) + i, heap_region2, 1) != 0) {
 824
 825       pointer_align = (i / sizeof(void *)) * sizeof(void *);
 826       addr_pointed1 = snapshot1->read(
 827         remote((void**)((char *) real_area1 + pointer_align)), process_index);
 828       addr_pointed2 = snapshot2->read(
 829         remote((void**)((char *) real_area2 + pointer_align)), process_index);
 830
 831       if (process->in_maestro_stack(remote(addr_pointed1))
 832         && process->in_maestro_stack(remote(addr_pointed2))) {
 833         i = pointer_align + sizeof(void *);
 834         continue;
 835       } else if (addr_pointed1 > state->std_heap_copy.heapbase
 836                  && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)
 837                  && addr_pointed2 > state->std_heap_copy.heapbase
 838                  && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2)) {
 839         // Both addreses are in the heap:
 840         res_compare =
 841             compare_heap_area(process_index, addr_pointed1, addr_pointed2, snapshot1,
 842                               snapshot2, previous, NULL, 0);
 843         if (res_compare == 1) {
 844           return res_compare;
 845         }
 846         i = pointer_align + sizeof(void *);
 847         continue;
 848       } else {
 849         return 1;
 850       }
 851
 852     }
 853
 854     i++;
 855
 856   }
 857
 858   return 0;
 859
 860 }
 861
 862 /**
 863  *
 864  * @param state
 865  * @param real_area1     Process address for state 1
 866  * @param real_area2     Process address for state 2
 867  * @param snapshot1      Snapshot of state 1
 868  * @param snapshot2      Snapshot of state 2
 869  * @param previous
 870  * @param type_id
 871  * @param area_size      either a byte_size or an elements_count (?)
 872  * @param check_ignore
 873  * @param pointer_level
 874  * @return               0 (same), 1 (different), -1 (unknown)
 875  */
 876 static int compare_heap_area_with_type(struct s_mc_diff *state, int process_index,
 877                                        const void *real_area1, const void *real_area2,
 878                                        mc_snapshot_t snapshot1,
 879                                        mc_snapshot_t snapshot2,
 880                                        xbt_dynar_t previous, simgrid::mc::Type* type,
 881                                        int area_size, int check_ignore,
 882                                        int pointer_level)
 883 {
 884 top:
 885   if (is_stack(real_area1) && is_stack(real_area2))
 886     return 0;
 887
 888   ssize_t ignore1, ignore2;
 889
 890   if ((check_ignore > 0)
 891       && ((ignore1 = heap_comparison_ignore_size(state->to_ignore1, real_area1))
 892           > 0)
 893       && ((ignore2 = heap_comparison_ignore_size(state->to_ignore2, real_area2))
 894           == ignore1)) {
 895     return 0;
 896   }
 897
 898   simgrid::mc::Type *subtype, *subsubtype;
 899   int res, elm_size;
 900   const void *addr_pointed1, *addr_pointed2;
 901
 902   mc_mem_region_t heap_region1 = MC_get_heap_region(snapshot1);
 903   mc_mem_region_t heap_region2 = MC_get_heap_region(snapshot2);
 904
 905   switch (type->type) {
 906   case DW_TAG_unspecified_type:
 907     return 1;
 908
 909   case DW_TAG_base_type:
 910     if (!type->name.empty() && type->name == "char") {        /* String, hence random (arbitrary ?) size */
 911       if (real_area1 == real_area2)
 912         return -1;
 913       else
 914         return (MC_snapshot_region_memcmp(real_area1, heap_region1, real_area2, heap_region2, area_size) != 0);
 915     } else {
 916       if (area_size != -1 && type->byte_size != area_size)
 917         return -1;
 918       else {
 919         return (MC_snapshot_region_memcmp(real_area1, heap_region1, real_area2, heap_region2, type->byte_size) != 0);
 920       }
 921     }
 922     break;
 923   case DW_TAG_enumeration_type:
 924     if (area_size != -1 && type->byte_size != area_size)
 925       return -1;
 926     else
 927       return (MC_snapshot_region_memcmp(real_area1, heap_region1, real_area2, heap_region2, type->byte_size) != 0);
 928     break;
 929   case DW_TAG_typedef:
 930   case DW_TAG_const_type:
 931   case DW_TAG_volatile_type:
 932     // Poor man's TCO:
 933     type = type->subtype;
 934     goto top;
 935     break;
 936   case DW_TAG_array_type:
 937     subtype = type->subtype;
 938     switch (subtype->type) {
 939     case DW_TAG_unspecified_type:
 940       return 1;
 941
 942     case DW_TAG_base_type:
 943     case DW_TAG_enumeration_type:
 944     case DW_TAG_pointer_type:
 945     case DW_TAG_reference_type:
 946     case DW_TAG_rvalue_reference_type:
 947     case DW_TAG_structure_type:
 948     case DW_TAG_class_type:
 949     case DW_TAG_union_type:
 950       if (subtype->full_type)
 951         subtype = subtype->full_type;
 952       elm_size = subtype->byte_size;
 953       break;
 954       // TODO, just remove the type indirection?
 955     case DW_TAG_const_type:
 956     case DW_TAG_typedef:
 957     case DW_TAG_volatile_type:
 958       subsubtype = subtype->subtype;
 959       if (subsubtype->full_type)
 960         subsubtype = subsubtype->full_type;
 961       elm_size = subsubtype->byte_size;
 962       break;
 963     default:
 964       return 0;
 965       break;
 966     }
 967     for (int i = 0; i < type->element_count; i++) {
 968       // TODO, add support for variable stride (DW_AT_byte_stride)
 969       res =
 970           compare_heap_area_with_type(state, process_index,
 971                                       (char *) real_area1 + (i * elm_size),
 972                                       (char *) real_area2 + (i * elm_size),
 973                                       snapshot1, snapshot2, previous,
 974                                       type->subtype, subtype->byte_size,
 975                                       check_ignore, pointer_level);
 976       if (res == 1)
 977         return res;
 978     }
 979     break;
 980   case DW_TAG_reference_type:
 981   case DW_TAG_rvalue_reference_type:
 982   case DW_TAG_pointer_type:
 983     if (type->subtype && type->subtype->type == DW_TAG_subroutine_type) {
 984       addr_pointed1 = snapshot1->read(remote((void**)real_area1), process_index);
 985       addr_pointed2 = snapshot2->read(remote((void**)real_area2), process_index);
 986       return (addr_pointed1 != addr_pointed2);;
 987     } else {
 988       pointer_level++;
 989       if (pointer_level > 1) {  /* Array of pointers */
 990         for (size_t i = 0; i < (area_size / sizeof(void *)); i++) {
 991           addr_pointed1 = snapshot1->read(
 992             remote((void**)((char*) real_area1 + i * sizeof(void *))),
 993             process_index);
 994           addr_pointed2 = snapshot2->read(
 995             remote((void**)((char*) real_area2 + i * sizeof(void *))),
 996             process_index);
 997           if (addr_pointed1 > state->std_heap_copy.heapbase
 998               && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)
 999               && addr_pointed2 > state->std_heap_copy.heapbase
1000               && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2))
1001             res =
1002                 compare_heap_area(process_index, addr_pointed1, addr_pointed2, snapshot1,
1003                                   snapshot2, previous, type->subtype,
1004                                   pointer_level);
1005           else
1006             res = (addr_pointed1 != addr_pointed2);
1007           if (res == 1)
1008             return res;
1009         }
1010       } else {
1011         addr_pointed1 = snapshot1->read(remote((void**)real_area1), process_index);
1012         addr_pointed2 = snapshot2->read(remote((void**)real_area2), process_index);
1013         if (addr_pointed1 > state->std_heap_copy.heapbase
1014             && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)
1015             && addr_pointed2 > state->std_heap_copy.heapbase
1016             && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2))
1017           return compare_heap_area(process_index, addr_pointed1, addr_pointed2, snapshot1,
1018                                    snapshot2, previous, type->subtype,
1019                                    pointer_level);
1020         else
1021           return (addr_pointed1 != addr_pointed2);
1022       }
1023     }
1024     break;
1025   case DW_TAG_structure_type:
1026   case DW_TAG_class_type:
1027     if (type->full_type)
1028       type = type->full_type;
1029     if (area_size != -1 && type->byte_size != area_size) {
1030       if (area_size > type->byte_size && area_size % type->byte_size == 0) {
1031         for (size_t i = 0; i < (size_t)(area_size / type->byte_size); i++) {
1032           res =
1033               compare_heap_area_with_type(state, process_index,
1034                                           (char *) real_area1 + i * type->byte_size,
1035                                           (char *) real_area2 + i * type->byte_size,
1036                                           snapshot1, snapshot2, previous, type, -1,
1037                                           check_ignore, 0);
1038           if (res == 1)
1039             return res;
1040         }
1041       } else {
1042         return -1;
1043       }
1044     } else {
1045       for(simgrid::mc::Type& member : type->members) {
1046         // TODO, optimize this? (for the offset case)
1047         void *real_member1 =
1048             mc_member_resolve(real_area1, type, &member, (simgrid::mc::AddressSpace*) snapshot1, process_index);
1049         void *real_member2 =
1050             mc_member_resolve(real_area2, type, &member, (simgrid::mc::AddressSpace*) snapshot2, process_index);
1051         res =
1052             compare_heap_area_with_type(state, process_index, real_member1, real_member2,
1053                                         snapshot1, snapshot2,
1054                                         previous, member.subtype, -1,
1055                                         check_ignore, 0);
1056         if (res == 1) {
1057           return res;
1058         }
1059       }
1060     }
1061     break;
1062   case DW_TAG_union_type:
1063     return compare_heap_area_without_type(state, process_index, real_area1, real_area2,
1064                                           snapshot1, snapshot2, previous,
1065                                           type->byte_size, check_ignore);
1066     break;
1067   default:
1068     break;
1069   }
1070
1071   return 0;
1072
1073 }
1074
1075 /** Infer the type of a part of the block from the type of the block
1076  *
1077  * TODO, handle DW_TAG_array_type as well as arrays of the object ((*p)[5], p[5])
1078  *
1079  * TODO, handle subfields ((*p).bar.foo, (*p)[5].bar…)
1080  *
1081  * @param  type_id            DWARF type ID of the root address
1082  * @param  area_size
1083  * @return                    DWARF type ID for given offset
1084  */
1085 static simgrid::mc::Type* get_offset_type(void *real_base_address, simgrid::mc::Type* type,
1086                                  int offset, int area_size,
1087                                  mc_snapshot_t snapshot, int process_index)
1088 {
1089
1090   // Beginning of the block, the infered variable type if the type of the block:
1091   if (offset == 0)
1092     return type;
1093
1094   switch (type->type) {
1095   case DW_TAG_structure_type:
1096   case DW_TAG_class_type:
1097     if (type->full_type)
1098       type = type->full_type;
1099
1100     if (area_size != -1 && type->byte_size != area_size) {
1101       if (area_size > type->byte_size && area_size % type->byte_size == 0)
1102         return type;
1103       else
1104         return NULL;
1105     } else {
1106       for(simgrid::mc::Type& member : type->members) {
1107
1108         if (member.has_offset_location()) {
1109           // We have the offset, use it directly (shortcut):
1110           if (member.offset() == offset)
1111             return member.subtype;
1112         } else {
1113           void *real_member =
1114             mc_member_resolve(real_base_address, type, &member,
1115               snapshot, process_index);
1116           if ((char*) real_member - (char *) real_base_address == offset)
1117             return member.subtype;
1118         }
1119
1120       }
1121       return NULL;
1122     }
1123     break;
1124   default:
1125     /* FIXME : other cases ? */
1126     return NULL;
1127     break;
1128   }
1129 }
1130
1131 /**
1132  *
1133  * @param area1          Process address for state 1
1134  * @param area2          Process address for state 2
1135  * @param snapshot1      Snapshot of state 1
1136  * @param snapshot2      Snapshot of state 2
1137  * @param previous       Pairs of blocks already compared on the current path (or NULL)
1138  * @param type_id        Type of variable
1139  * @param pointer_level
1140  * @return 0 (same), 1 (different), -1
1141  */
1142 int compare_heap_area(int process_index, const void *area1, const void *area2, mc_snapshot_t snapshot1,
1143                       mc_snapshot_t snapshot2, xbt_dynar_t previous,
1144                       simgrid::mc::Type* type, int pointer_level)
1145 {
1146   simgrid::mc::Process* process = &mc_model_checker->process();
1147
1148   struct s_mc_diff *state = mc_diff_info;
1149
1150   int res_compare;
1151   ssize_t block1, frag1, block2, frag2;
1152   ssize_t size;
1153   int check_ignore = 0;
1154
1155   void *real_addr_block1, *real_addr_block2, *real_addr_frag1, *real_addr_frag2;
1156   int type_size = -1;
1157   int offset1 = 0, offset2 = 0;
1158   int new_size1 = -1, new_size2 = -1;
1159   simgrid::mc::Type *new_type1 = NULL, *new_type2 = NULL;
1160
1161   int match_pairs = 0;
1162
1163   // This is the address of std_heap->heapinfo in the application process:
1164   void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo;
1165
1166   const malloc_info* heapinfos1 = snapshot1->read(
1167     remote((const malloc_info**)heapinfo_address), process_index);
1168   const malloc_info* heapinfos2 = snapshot2->read(
1169     remote((const malloc_info**)heapinfo_address), process_index);
1170
1171   malloc_info heapinfo_temp1, heapinfo_temp2;
1172
1173   if (previous == NULL) {
1174     previous =
1175         xbt_dynar_new(sizeof(heap_area_pair_t), heap_area_pair_free_voidp);
1176     match_pairs = 1;
1177   }
1178   // Get block number:
1179   block1 =
1180       ((char *) area1 -
1181        (char *) state->std_heap_copy.heapbase) / BLOCKSIZE + 1;
1182   block2 =
1183       ((char *) area2 -
1184        (char *) state->std_heap_copy.heapbase) / BLOCKSIZE + 1;
1185
1186   // If either block is a stack block:
1187   if (is_block_stack((int) block1) && is_block_stack((int) block2)) {
1188     add_heap_area_pair(previous, block1, -1, block2, -1);
1189     if (match_pairs) {
1190       match_equals(state, previous);
1191       xbt_dynar_free(&previous);
1192     }
1193     return 0;
1194   }
1195   // If either block is not in the expected area of memory:
1196   if (((char *) area1 < (char *) state->std_heap_copy.heapbase)
1197       || (block1 > (ssize_t) state->heapsize1) || (block1 < 1)
1198       || ((char *) area2 < (char *) state->std_heap_copy.heapbase)
1199       || (block2 > (ssize_t) state->heapsize2) || (block2 < 1)) {
1200     if (match_pairs) {
1201       xbt_dynar_free(&previous);
1202     }
1203     return 1;
1204   }
1205
1206   // Process address of the block:
1207   real_addr_block1 = (ADDR2UINT(block1) - 1) * BLOCKSIZE +
1208                  (char *) state->std_heap_copy.heapbase;
1209   real_addr_block2 = (ADDR2UINT(block2) - 1) * BLOCKSIZE +
1210                  (char *) state->std_heap_copy.heapbase;
1211
1212   if (type) {
1213
1214     if (type->full_type)
1215       type = type->full_type;
1216
1217     // This assume that for "boring" types (volatile ...) byte_size is absent:
1218     while (type->byte_size == 0 && type->subtype != NULL)
1219       type = type->subtype;
1220
1221     // Find type_size:
1222     if ((type->type == DW_TAG_pointer_type)
1223         || ((type->type == DW_TAG_base_type) && !type->name.empty()
1224             && type->name == "char"))
1225       type_size = -1;
1226     else
1227       type_size = type->byte_size;
1228
1229   }
1230
1231   mc_mem_region_t heap_region1 = MC_get_heap_region(snapshot1);
1232   mc_mem_region_t heap_region2 = MC_get_heap_region(snapshot2);
1233
1234   const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(
1235     heap_region1, &heapinfo_temp1, &heapinfos1[block1], sizeof(malloc_info));
1236   const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(
1237     heap_region2, &heapinfo_temp2, &heapinfos2[block2], sizeof(malloc_info));
1238
1239   if ((heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type==MMALLOC_TYPE_HEAPINFO)
1240     && (heapinfo2->type == MMALLOC_TYPE_FREE || heapinfo2->type ==MMALLOC_TYPE_HEAPINFO)) {
1241
1242     /* Free block */
1243     if (match_pairs) {
1244       match_equals(state, previous);
1245       xbt_dynar_free(&previous);
1246     }
1247     return 0;
1248
1249   } else if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED
1250     && heapinfo2->type == MMALLOC_TYPE_UNFRAGMENTED) {
1251     /* Complete block */
1252
1253     // TODO, lookup variable type from block type as done for fragmented blocks
1254
1255     offset1 = (char *) area1 - (char *) real_addr_block1;
1256     offset2 = (char *) area2 - (char *) real_addr_block2;
1257
1258     if (state->equals_to1_(block1, 0).valid
1259         && state->equals_to2_(block2, 0).valid) {
1260       if (equal_blocks(state, block1, block2)) {
1261         if (match_pairs) {
1262           match_equals(state, previous);
1263           xbt_dynar_free(&previous);
1264         }
1265         return 0;
1266       }
1267     }
1268
1269     if (type_size != -1) {
1270       if (type_size != (ssize_t) heapinfo1->busy_block.busy_size
1271           && type_size != (ssize_t)   heapinfo2->busy_block.busy_size
1272           && (type->name.empty() || type->name == "struct s_smx_context")) {
1273         if (match_pairs) {
1274           match_equals(state, previous);
1275           xbt_dynar_free(&previous);
1276         }
1277         return -1;
1278       }
1279     }
1280
1281     if (heapinfo1->busy_block.size !=
1282         heapinfo2->busy_block.size) {
1283       if (match_pairs) {
1284         xbt_dynar_free(&previous);
1285       }
1286       return 1;
1287     }
1288
1289     if (heapinfo1->busy_block.busy_size !=
1290         heapinfo2->busy_block.busy_size) {
1291       if (match_pairs) {
1292         xbt_dynar_free(&previous);
1293       }
1294       return 1;
1295     }
1296
1297     if (!add_heap_area_pair(previous, block1, -1, block2, -1)) {
1298       if (match_pairs) {
1299         match_equals(state, previous);
1300         xbt_dynar_free(&previous);
1301       }
1302       return 0;
1303     }
1304
1305     size = heapinfo1->busy_block.busy_size;
1306
1307     // Remember (basic) type inference.
1308     // The current data structure only allows us to do this for the whole block.
1309     if (type != NULL && area1 == real_addr_block1) {
1310       state->types1_(block1, 0) = type;
1311     }
1312     if (type != NULL && area2 == real_addr_block2) {
1313       state->types2_(block2, 0) = type;
1314     }
1315
1316     if (size <= 0) {
1317       if (match_pairs) {
1318         match_equals(state, previous);
1319         xbt_dynar_free(&previous);
1320       }
1321       return 0;
1322     }
1323
1324     frag1 = -1;
1325     frag2 = -1;
1326
1327     if ((heapinfo1->busy_block.ignore > 0)
1328         && (heapinfo2->busy_block.ignore ==
1329             heapinfo1->busy_block.ignore))
1330       check_ignore = heapinfo1->busy_block.ignore;
1331
1332   } else if ((heapinfo1->type > 0) && (heapinfo2->type > 0)) {      /* Fragmented block */
1333
1334     // Fragment number:
1335     frag1 =
1336         ((uintptr_t) (ADDR2UINT(area1) % (BLOCKSIZE))) >> heapinfo1->type;
1337     frag2 =
1338         ((uintptr_t) (ADDR2UINT(area2) % (BLOCKSIZE))) >> heapinfo2->type;
1339
1340     // Process address of the fragment:
1341     real_addr_frag1 =
1342         (void *) ((char *) real_addr_block1 +
1343                   (frag1 << heapinfo1->type));
1344     real_addr_frag2 =
1345         (void *) ((char *) real_addr_block2 +
1346                   (frag2 << heapinfo2->type));
1347
1348     // Check the size of the fragments against the size of the type:
1349     if (type_size != -1) {
1350       if (heapinfo1->busy_frag.frag_size[frag1] == -1
1351           || heapinfo2->busy_frag.frag_size[frag2] == -1) {
1352         if (match_pairs) {
1353           match_equals(state, previous);
1354           xbt_dynar_free(&previous);
1355         }
1356         return -1;
1357       }
1358       // ?
1359       if (type_size != heapinfo1->busy_frag.frag_size[frag1]
1360           || type_size != heapinfo2->busy_frag.frag_size[frag2]) {
1361         if (match_pairs) {
1362           match_equals(state, previous);
1363           xbt_dynar_free(&previous);
1364         }
1365         return -1;
1366       }
1367     }
1368
1369     // Check if the blocks are already matched together:
1370     if (state->equals_to1_(block1, frag1).valid
1371         && state->equals_to2_(block2, frag2).valid) {
1372       if (offset1==offset2 && equal_fragments(state, block1, frag1, block2, frag2)) {
1373         if (match_pairs) {
1374           match_equals(state, previous);
1375           xbt_dynar_free(&previous);
1376         }
1377         return 0;
1378       }
1379     }
1380     // Compare the size of both fragments:
1381     if (heapinfo1->busy_frag.frag_size[frag1] !=
1382         heapinfo2->busy_frag.frag_size[frag2]) {
1383       if (type_size == -1) {
1384         if (match_pairs) {
1385           match_equals(state, previous);
1386           xbt_dynar_free(&previous);
1387         }
1388         return -1;
1389       } else {
1390         if (match_pairs) {
1391           xbt_dynar_free(&previous);
1392         }
1393         return 1;
1394       }
1395     }
1396
1397     // Size of the fragment:
1398     size = heapinfo1->busy_frag.frag_size[frag1];
1399
1400     // Remember (basic) type inference.
1401     // The current data structure only allows us to do this for the whole fragment.
1402     if (type != NULL && area1 == real_addr_frag1) {
1403       state->types1_(block1, frag1) = type;
1404     }
1405     if (type != NULL && area2 == real_addr_frag2) {
1406       state->types2_(block2, frag2) = type;
1407     }
1408     // The type of the variable is already known:
1409     if (type) {
1410       new_type1 = type;
1411       new_type2 = type;
1412     }
1413     // Type inference from the block type.
1414     else if (state->types1_(block1, frag1) != NULL
1415              || state->types2_(block2, frag2) != NULL) {
1416
1417       offset1 = (char *) area1 - (char *) real_addr_frag1;
1418       offset2 = (char *) area2 - (char *) real_addr_frag2;
1419
1420       if (state->types1_(block1, frag1) != NULL
1421           && state->types2_(block2, frag2) != NULL) {
1422         new_type1 =
1423             get_offset_type(real_addr_frag1, state->types1_(block1, frag1),
1424                             offset1, size, snapshot1, process_index);
1425         new_type2 =
1426             get_offset_type(real_addr_frag2, state->types2_(block2, frag2),
1427                             offset1, size, snapshot2, process_index);
1428       } else if (state->types1_(block1, frag1) != NULL) {
1429         new_type1 =
1430             get_offset_type(real_addr_frag1, state->types1_(block1, frag1),
1431                             offset1, size, snapshot1, process_index);
1432         new_type2 =
1433             get_offset_type(real_addr_frag2, state->types1_(block1, frag1),
1434                             offset2, size, snapshot2, process_index);
1435       } else if (state->types2_(block2, frag2) != NULL) {
1436         new_type1 =
1437             get_offset_type(real_addr_frag1, state->types2_(block2, frag2),
1438                             offset1, size, snapshot1, process_index);
1439         new_type2 =
1440             get_offset_type(real_addr_frag2, state->types2_(block2, frag2),
1441                             offset2, size, snapshot2, process_index);
1442       } else {
1443         if (match_pairs) {
1444           match_equals(state, previous);
1445           xbt_dynar_free(&previous);
1446         }
1447         return -1;
1448       }
1449
1450       if (new_type1 != NULL && new_type2 != NULL && new_type1 != new_type2) {
1451
1452         type = new_type1;
1453         while (type->byte_size == 0 && type->subtype != NULL)
1454           type = type->subtype;
1455         new_size1 = type->byte_size;
1456
1457         type = new_type2;
1458         while (type->byte_size == 0 && type->subtype != NULL)
1459           type = type->subtype;
1460         new_size2 = type->byte_size;
1461
1462       } else {
1463         if (match_pairs) {
1464           match_equals(state, previous);
1465           xbt_dynar_free(&previous);
1466         }
1467         return -1;
1468       }
1469     }
1470
1471     if (new_size1 > 0 && new_size1 == new_size2) {
1472       type = new_type1;
1473       size = new_size1;
1474     }
1475
1476     if (offset1 == 0 && offset2 == 0) {
1477       if (!add_heap_area_pair(previous, block1, frag1, block2, frag2)) {
1478         if (match_pairs) {
1479           match_equals(state, previous);
1480           xbt_dynar_free(&previous);
1481         }
1482         return 0;
1483       }
1484     }
1485
1486     if (size <= 0) {
1487       if (match_pairs) {
1488         match_equals(state, previous);
1489         xbt_dynar_free(&previous);
1490       }
1491       return 0;
1492     }
1493
1494     if ((heapinfo1->busy_frag.ignore[frag1] > 0)
1495         && (heapinfo2->busy_frag.ignore[frag2] ==
1496             heapinfo1->busy_frag.ignore[frag1]))
1497       check_ignore = heapinfo1->busy_frag.ignore[frag1];
1498
1499   } else {
1500
1501     if (match_pairs) {
1502       xbt_dynar_free(&previous);
1503     }
1504     return 1;
1505
1506   }
1507
1508
1509   /* Start comparison */
1510   if (type) {
1511     res_compare =
1512         compare_heap_area_with_type(state, process_index, area1, area2, snapshot1, snapshot2,
1513                                     previous, type, size, check_ignore,
1514                                     pointer_level);
1515   } else {
1516     res_compare =
1517         compare_heap_area_without_type(state, process_index, area1, area2, snapshot1, snapshot2,
1518                                        previous, size, check_ignore);
1519   }
1520   if (res_compare == 1) {
1521     if (match_pairs)
1522       xbt_dynar_free(&previous);
1523     return res_compare;
1524   }
1525
1526   if (match_pairs) {
1527     match_equals(state, previous);
1528     xbt_dynar_free(&previous);
1529   }
1530
1531   return 0;
1532 }
1533
1534 /*********************************************** Miscellaneous ***************************************************/
1535 /****************************************************************************************************************/
1536
1537 // Not used and broken code:
1538 # if 0
1539
1540 // Not used:
1541 static int get_pointed_area_size(void *area, int heap)
1542 {
1543
1544   struct s_mc_diff *state = mc_diff_info;
1545
1546   int block, frag;
1547   malloc_info *heapinfo;
1548
1549   if (heap == 1)
1550     heapinfo = state->heapinfo1;
1551   else
1552     heapinfo = state->heapinfo2;
1553
1554   block =
1555       ((char *) area -
1556        (char *) state->std_heap_copy.heapbase) / BLOCKSIZE + 1;
1557
1558   if (((char *) area < (char *) state->std_heap_copy.heapbase)
1559       || (block > state->heapsize1) || (block < 1))
1560     return -1;
1561
1562   if (heapinfo[block].type == MMALLOC_TYPE_FREE || heapinfo[block].type == MMALLOC_TYPE_HEAPINFO) {     /* Free block */
1563     return -1;
1564   } else if (heapinfo[block].type == MMALLOC_TYPE_UNFRAGMENTED) {       /* Complete block */
1565     return (int) heapinfo[block].busy_block.busy_size;
1566   } else {
1567     frag =
1568         ((uintptr_t) (ADDR2UINT(area) % (BLOCKSIZE))) >> heapinfo[block].type;
1569     return (int) heapinfo[block].busy_frag.frag_size[frag];
1570   }
1571 }
1572
1573 #ifndef max
1574 #define max( a, b ) ( ((a) > (b)) ? (a) : (b) )
1575 #endif
1576
1577 // Not used:
1578 int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2)
1579 {
1580
1581   struct s_mc_diff *state = mc_diff_info;
1582
1583   if (heap1 == NULL && heap1 == NULL) {
1584     XBT_DEBUG("Malloc descriptors null");
1585     return 0;
1586   }
1587
1588   if (heap1->heaplimit != heap2->heaplimit) {
1589     XBT_DEBUG("Different limit of valid info table indices");
1590     return 1;
1591   }
1592
1593   /* Heap information */
1594   state->heaplimit = ((struct mdesc *) heap1)->heaplimit;
1595
1596   state->std_heap_copy = *mc_model_checker->process().get_heap();
1597
1598   state->heapbase1 = (char *) heap1 + BLOCKSIZE;
1599   state->heapbase2 = (char *) heap2 + BLOCKSIZE;
1600
1601   state->heapinfo1 =
1602       (malloc_info *) ((char *) heap1 +
1603                        ((uintptr_t)
1604                         ((char *) heap1->heapinfo - (char *) state->s_heap)));
1605   state->heapinfo2 =
1606       (malloc_info *) ((char *) heap2 +
1607                        ((uintptr_t)
1608                         ((char *) heap2->heapinfo - (char *) state->s_heap)));
1609
1610   state->heapsize1 = heap1->heapsize;
1611   state->heapsize2 = heap2->heapsize;
1612
1613   /* Start comparison */
1614   size_t i, j, k;
1615   void *addr_block1, *addr_block2, *addr_frag1, *addr_frag2;
1616
1617   int distance = 0;
1618
1619   /* Check busy blocks */
1620
1621   i = 1;
1622
1623   while (i <= state->heaplimit) {
1624
1625     addr_block1 =
1626         ((void *) (((ADDR2UINT(i)) - 1) * BLOCKSIZE +
1627                    (char *) state->heapbase1));
1628     addr_block2 =
1629         ((void *) (((ADDR2UINT(i)) - 1) * BLOCKSIZE +
1630                    (char *) state->heapbase2));
1631
1632     if (state->heapinfo1[i].type != state->heapinfo2[i].type) {
1633
1634       distance += BLOCKSIZE;
1635       XBT_DEBUG("Different type of blocks (%zu) : %d - %d -> distance = %d", i,
1636                 state->heapinfo1[i].type, state->heapinfo2[i].type, distance);
1637       i++;
1638
1639     } else {
1640
1641       if (state->heapinfo1[i].type == MMALLOC_TYPE_FREE
1642         || state->heapinfo1[i].type == MMALLOC_TYPE_HAPINFO) {     /* Free block */
1643         i++;
1644         continue;
1645       }
1646
1647       if (state->heapinfo1[i].type == MMALLOC_TYPE_UNFRAGMENTED) {      /* Large block */
1648
1649         if (state->heapinfo1[i].busy_block.size !=
1650             state->heapinfo2[i].busy_block.size) {
1651           distance +=
1652               BLOCKSIZE * max(state->heapinfo1[i].busy_block.size,
1653                               state->heapinfo2[i].busy_block.size);
1654           i += max(state->heapinfo1[i].busy_block.size,
1655                    state->heapinfo2[i].busy_block.size);
1656           XBT_DEBUG
1657               ("Different larger of cluster at block %zu : %zu - %zu -> distance = %d",
1658                i, state->heapinfo1[i].busy_block.size,
1659                state->heapinfo2[i].busy_block.size, distance);
1660           continue;
1661         }
1662
1663         /*if(heapinfo1[i].busy_block.busy_size != heapinfo2[i].busy_block.busy_size){
1664            distance += max(heapinfo1[i].busy_block.busy_size, heapinfo2[i].busy_block.busy_size);
1665            i += max(heapinfo1[i].busy_block.size, heapinfo2[i].busy_block.size);
1666            XBT_DEBUG("Different size used oin large cluster at block %zu : %zu - %zu -> distance = %d", i, heapinfo1[i].busy_block.busy_size, heapinfo2[i].busy_block.busy_size, distance);
1667            continue;
1668            } */
1669
1670         k = 0;
1671
1672         //while(k < (heapinfo1[i].busy_block.busy_size)){
1673         while (k < state->heapinfo1[i].busy_block.size * BLOCKSIZE) {
1674           if (memcmp((char *) addr_block1 + k, (char *) addr_block2 + k, 1) !=
1675               0) {
1676             distance++;
1677           }
1678           k++;
1679         }
1680
1681         i++;
1682
1683       } else {                  /* Fragmented block */
1684
1685         for (j = 0; j < (size_t) (BLOCKSIZE >> state->heapinfo1[i].type); j++) {
1686
1687           addr_frag1 =
1688               (void *) ((char *) addr_block1 + (j << state->heapinfo1[i].type));
1689           addr_frag2 =
1690               (void *) ((char *) addr_block2 + (j << state->heapinfo2[i].type));
1691
1692           if (state->heapinfo1[i].busy_frag.frag_size[j] == 0
1693               && state->heapinfo2[i].busy_frag.frag_size[j] == 0) {
1694             continue;
1695           }
1696
1697
1698           /*if(heapinfo1[i].busy_frag.frag_size[j] != heapinfo2[i].busy_frag.frag_size[j]){
1699              distance += max(heapinfo1[i].busy_frag.frag_size[j], heapinfo2[i].busy_frag.frag_size[j]);
1700              XBT_DEBUG("Different size used in fragment %zu in block %zu : %d - %d -> distance = %d", j, i, heapinfo1[i].busy_frag.frag_size[j], heapinfo2[i].busy_frag.frag_size[j], distance);
1701              continue;
1702              } */
1703
1704           k = 0;
1705
1706           //while(k < max(heapinfo1[i].busy_frag.frag_size[j], heapinfo2[i].busy_frag.frag_size[j])){
1707           while (k < (BLOCKSIZE / (BLOCKSIZE >> state->heapinfo1[i].type))) {
1708             if (memcmp((char *) addr_frag1 + k, (char *) addr_frag2 + k, 1) !=
1709                 0) {
1710               distance++;
1711             }
1712             k++;
1713           }
1714
1715         }
1716
1717         i++;
1718
1719       }
1720
1721     }
1722
1723   }
1724
1725   return distance;
1726
1727 }
1728 #endif
1729
1730 }