model-checker : fix visited states reduction with comm determinism verification

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

diff --git a/src/mc/mc_diff.c b/src/mc/mc_diff.c
index aa77406..336897d 100644 (file)
--- a/src/mc/mc_diff.c
+++ b/src/mc/mc_diff.c
@@ -434,6 +434,9 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
   malloc_info heapinfo_temp1, heapinfo_temp2;
   malloc_info heapinfo_temp2b;
 
+  mc_mem_region_t heap_region1 = snapshot1->regions[0];
+  mc_mem_region_t heap_region2 = snapshot2->regions[0];
+
   // This is in snapshot do not use them directly:
   malloc_info* heapinfos1 = mc_snapshot_read_pointer(&((xbt_mheap_t)std_heap)->heapinfo, snapshot1);
   malloc_info* heapinfos2 = mc_snapshot_read_pointer(&((xbt_mheap_t)std_heap)->heapinfo, snapshot2);
@@ -441,8 +444,8 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
   while (i1 <= state->heaplimit) {
 
     // TODO, lookup in the correct region in order to speed it up:
-    malloc_info* heapinfo1 = mc_snapshot_read(&heapinfos1[i1], snapshot1, &heapinfo_temp1, sizeof(malloc_info));
-    malloc_info* heapinfo2 = mc_snapshot_read(&heapinfos2[i1], snapshot2, &heapinfo_temp2, sizeof(malloc_info));
+    malloc_info* heapinfo1 = mc_snapshot_read_region(&heapinfos1[i1], heap_region1, &heapinfo_temp1, sizeof(malloc_info));
+    malloc_info* heapinfo2 = mc_snapshot_read_region(&heapinfos2[i1], heap_region2, &heapinfo_temp2, sizeof(malloc_info));
 
     if (heapinfo1->type == -1) {      /* Free block */
       i1++;
@@ -512,7 +515,7 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
           continue;
         }
 
-        malloc_info* heapinfo2b = mc_snapshot_read(&heapinfos2[i2], snapshot2, &heapinfo_temp2b, sizeof(malloc_info));
+        malloc_info* heapinfo2b = mc_snapshot_read_region(&heapinfos2[i2], heap_region2, &heapinfo_temp2b, sizeof(malloc_info));
 
         if (heapinfo2b->type != 0) {
           i2++;
@@ -595,7 +598,7 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
 
         while (i2 <= state->heaplimit && !equal) {
 
-          malloc_info* heapinfo2b = mc_snapshot_read(&heapinfos2[i2], snapshot2, &heapinfo_temp2b, sizeof(malloc_info));
+          malloc_info* heapinfo2b = mc_snapshot_read_region(&heapinfos2[i2], heap_region2, &heapinfo_temp2b, sizeof(malloc_info));
           if (heapinfo2b->type <= 0) {
             i2++;
             continue;
@@ -659,7 +662,7 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
   size_t i = 1, j = 0;
 
   for(i = 1; i <= state->heaplimit; i++) {
-    malloc_info* heapinfo1 = mc_snapshot_read(&heapinfos1[i], snapshot1, &heapinfo_temp1, sizeof(malloc_info));
+    malloc_info* heapinfo1 = mc_snapshot_read_region(&heapinfos1[i], heap_region1, &heapinfo_temp1, sizeof(malloc_info));
     if (heapinfo1->type == 0) {
       if (i1 == state->heaplimit) {
         if (heapinfo1->busy_block.busy_size > 0) {
@@ -700,7 +703,7 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
     XBT_DEBUG("Number of blocks/fragments not found in heap1 : %d", nb_diff1);
 
   for (i=1; i <= state->heaplimit; i++) {
-    malloc_info* heapinfo2 = mc_snapshot_read(&heapinfos2[i], snapshot2, &heapinfo_temp2, sizeof(malloc_info));
+    malloc_info* heapinfo2 = mc_snapshot_read_region(&heapinfos2[i], heap_region2, &heapinfo_temp2, sizeof(malloc_info));
     if (heapinfo2->type == 0) {
       if (i1 == state->heaplimit) {
         if (heapinfo2->busy_block.busy_size > 0) {
@@ -768,6 +771,9 @@ static int compare_heap_area_without_type(struct s_mc_diff *state,
   int pointer_align, res_compare;
   ssize_t ignore1, ignore2;
 
+  mc_mem_region_t heap_region1 = snapshot1->regions[0];
+  mc_mem_region_t heap_region2 = snapshot2->regions[0];
+
   while (i < size) {
 
     if (check_ignore > 0) {
@@ -789,7 +795,7 @@ static int compare_heap_area_without_type(struct s_mc_diff *state,
       }
     }
 
-    if (mc_snapshot_memcp(((char *) real_area1) + i, snapshot1, ((char *) real_area2) + i, snapshot2, 1) != 0) {
+    if (mc_snapshot_region_memcp(((char *) real_area1) + i, heap_region1, ((char *) real_area2) + i, heap_region2, 1) != 0) {
 
       pointer_align = (i / sizeof(void *)) * sizeof(void *);
       addr_pointed1 = mc_snapshot_read_pointer((char *) real_area1 + pointer_align, snapshot1);
@@ -850,7 +856,7 @@ static int compare_heap_area_with_type(struct s_mc_diff *state,
                                        int area_size, int check_ignore,
                                        int pointer_level)
 {
-
+top:
   if (is_stack(real_area1) && is_stack(real_area2))
     return 0;
 
@@ -870,6 +876,9 @@ static int compare_heap_area_with_type(struct s_mc_diff *state,
   dw_type_t member;
   void *addr_pointed1, *addr_pointed2;;
 
+  mc_mem_region_t heap_region1 = snapshot1->regions[0];
+  mc_mem_region_t heap_region2 = snapshot2->regions[0];
+
   switch (type->type) {
   case DW_TAG_unspecified_type:
     return 1;
@@ -879,12 +888,12 @@ static int compare_heap_area_with_type(struct s_mc_diff *state,
       if (real_area1 == real_area2)
         return -1;
       else
-        return (mc_snapshot_memcp(real_area1, snapshot1, real_area2, snapshot2, area_size) != 0);
+        return (mc_snapshot_region_memcp(real_area1, heap_region1, real_area2, heap_region2, area_size) != 0);
     } else {
       if (area_size != -1 && type->byte_size != area_size)
         return -1;
       else {
-        return (mc_snapshot_memcp(real_area1, snapshot1, real_area2, snapshot2, type->byte_size) != 0);
+        return (mc_snapshot_region_memcp(real_area1, heap_region1, real_area2, heap_region2, type->byte_size) != 0);
       }
     }
     break;
@@ -892,15 +901,14 @@ static int compare_heap_area_with_type(struct s_mc_diff *state,
     if (area_size != -1 && type->byte_size != area_size)
       return -1;
     else
-      return (mc_snapshot_memcp(real_area1, snapshot1, real_area2, snapshot2, type->byte_size) != 0);
+      return (mc_snapshot_region_memcp(real_area1, heap_region1, real_area2, heap_region2, type->byte_size) != 0);
     break;
   case DW_TAG_typedef:
   case DW_TAG_const_type:
   case DW_TAG_volatile_type:
-    return compare_heap_area_with_type(state, real_area1, real_area2,
-                                       snapshot1, snapshot2, previous,
-                                       type->subtype, area_size, check_ignore,
-                                       pointer_level);
+    // Poor man's TCO:
+    type = type->subtype;
+    goto top;
     break;
   case DW_TAG_array_type:
     subtype = type->subtype;
@@ -1192,8 +1200,11 @@ int compare_heap_area(void *area1, void *area2, mc_snapshot_t snapshot1,
 
   }
 
-  malloc_info* heapinfo1 = mc_snapshot_read(&heapinfos1[block1], snapshot1, &heapinfo_temp1, sizeof(malloc_info));
-  malloc_info* heapinfo2 = mc_snapshot_read(&heapinfos2[block2], snapshot2, &heapinfo_temp2, sizeof(malloc_info));
+  mc_mem_region_t heap_region1 = snapshot1->regions[0];
+  mc_mem_region_t heap_region2 = snapshot2->regions[0];
+
+  malloc_info* heapinfo1 = mc_snapshot_read_region(&heapinfos1[block1], heap_region1, &heapinfo_temp1, sizeof(malloc_info));
+  malloc_info* heapinfo2 = mc_snapshot_read_region(&heapinfos2[block2], heap_region2, &heapinfo_temp2, sizeof(malloc_info));
 
   if ((heapinfo1->type == -1) && (heapinfo2->type == -1)) { /* Free block */