Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : fix backtracking with comm determinism verification
[simgrid.git] / src / mc / mc_compare.c
1 /* Copyright (c) 2012-2014. The SimGrid Team.
2  * All rights reserved.                                                     */
3
4 /* This program is free software; you can redistribute it and/or modify it
5  * under the terms of the license (GNU LGPL) which comes with this package. */
6
7 #include <inttypes.h>
8
9 #include "mc_private.h"
10
11 #include "xbt/mmalloc.h"
12 #include "xbt/mmalloc/mmprivate.h"
13
14 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc,
15                                 "Logging specific to mc_compare");
16
17 typedef struct s_pointers_pair {
18   void *p1;
19   void *p2;
20 } s_pointers_pair_t, *pointers_pair_t;
21
22 __thread xbt_dynar_t compared_pointers;
23
24 /************************** Free functions ****************************/
25 /********************************************************************/
26
27 static void stack_region_free(stack_region_t s)
28 {
29   if (s) {
30     xbt_free(s->process_name);
31     xbt_free(s);
32   }
33 }
34
35 static void stack_region_free_voidp(void *s)
36 {
37   stack_region_free((stack_region_t) * (void **) s);
38 }
39
40 static void pointers_pair_free(pointers_pair_t p)
41 {
42   xbt_free(p);
43 }
44
45 static void pointers_pair_free_voidp(void *p)
46 {
47   pointers_pair_free((pointers_pair_t) * (void **) p);
48 }
49
50 /************************** Snapshot comparison *******************************/
51 /******************************************************************************/
52
53 /** \brief Try to add a pair a compared pointers to the set of compared pointers
54  *
55  *  \result !=0 if the pointers were added (they were not in the set),
56  *      0 otherwise (they were already in the set)
57  */
58 static int add_compared_pointers(void *p1, void *p2)
59 {
60
61   pointers_pair_t new_pair = xbt_new0(s_pointers_pair_t, 1);
62   new_pair->p1 = p1;
63   new_pair->p2 = p2;
64
65   if (xbt_dynar_is_empty(compared_pointers)) {
66     xbt_dynar_push(compared_pointers, &new_pair);
67     return 1;
68   }
69
70   unsigned int cursor = 0;
71   int start = 0;
72   int end = xbt_dynar_length(compared_pointers) - 1;
73   pointers_pair_t pair = NULL;
74
75   pointers_pair_t *p =
76       (pointers_pair_t *) xbt_dynar_get_ptr(compared_pointers, 0);
77
78   while (start <= end) {
79     cursor = (start + end) / 2;
80     pair = p[cursor];
81     if (pair->p1 < p1) {
82       start = cursor + 1;
83     } else if (pair->p1 > p1) {
84       end = cursor - 1;
85     } else if (pair->p2 < p2) {
86       start = cursor + 1;
87     } else if (pair->p2 > p2) {
88       end = cursor - 1;
89     } else {
90       pointers_pair_free(new_pair);
91       return 0;
92     }
93   }
94
95   if (pair->p1 < p1)
96     xbt_dynar_insert_at(compared_pointers, cursor + 1, &new_pair);
97   else if (pair->p1 > p1)
98     xbt_dynar_insert_at(compared_pointers, cursor, &new_pair);
99   else if (pair->p2 < p2)
100     xbt_dynar_insert_at(compared_pointers, cursor + 1, &new_pair);
101   else if (pair->p2 > p2)
102     xbt_dynar_insert_at(compared_pointers, cursor, &new_pair);
103   else
104     xbt_die("Unrecheable");
105
106   return 1;
107 }
108
109 static int compare_areas_with_type(void *area1, void *area2,
110                                    mc_snapshot_t snapshot1,
111                                    mc_snapshot_t snapshot2, dw_type_t type,
112                                    int region_size, int region_type,
113                                    void *start_data, int pointer_level)
114 {
115
116   unsigned int cursor = 0;
117   dw_type_t member, subtype, subsubtype;
118   int elm_size, i, res;
119   void *addr_pointed1, *addr_pointed2;
120
121   switch (type->type) {
122   case DW_TAG_unspecified_type:
123     return 1;
124
125   case DW_TAG_base_type:
126   case DW_TAG_enumeration_type:
127   case DW_TAG_union_type:
128     return (memcmp(area1, area2, type->byte_size) != 0);
129     break;
130   case DW_TAG_typedef:
131   case DW_TAG_volatile_type:
132   case DW_TAG_const_type:
133     return compare_areas_with_type(area1, area2, snapshot1, snapshot2,
134                                    type->subtype, region_size, region_type,
135                                    start_data, pointer_level);
136     break;
137   case DW_TAG_array_type:
138     subtype = type->subtype;
139     switch (subtype->type) {
140     case DW_TAG_unspecified_type:
141       return 1;
142
143     case DW_TAG_base_type:
144     case DW_TAG_enumeration_type:
145     case DW_TAG_pointer_type:
146     case DW_TAG_reference_type:
147     case DW_TAG_rvalue_reference_type:
148     case DW_TAG_structure_type:
149     case DW_TAG_class_type:
150     case DW_TAG_union_type:
151       if (subtype->full_type)
152         subtype = subtype->full_type;
153       elm_size = subtype->byte_size;
154       break;
155     case DW_TAG_const_type:
156     case DW_TAG_typedef:
157     case DW_TAG_volatile_type:
158       subsubtype = subtype->subtype;
159       if (subsubtype->full_type)
160         subsubtype = subsubtype->full_type;
161       elm_size = subsubtype->byte_size;
162       break;
163     default:
164       return 0;
165       break;
166     }
167     for (i = 0; i < type->element_count; i++) {
168       res =
169           compare_areas_with_type((char *) area1 + (i * elm_size),
170                                   (char *) area2 + (i * elm_size), snapshot1,
171                                   snapshot2, type->subtype, region_size,
172                                   region_type, start_data, pointer_level);
173       if (res == 1)
174         return res;
175     }
176     break;
177   case DW_TAG_pointer_type:
178   case DW_TAG_reference_type:
179   case DW_TAG_rvalue_reference_type:
180
181     addr_pointed1 = *((void **) (area1));
182     addr_pointed2 = *((void **) (area2));
183
184     if (type->subtype && type->subtype->type == DW_TAG_subroutine_type) {
185       return (addr_pointed1 != addr_pointed2);
186     } else {
187
188       if (addr_pointed1 == NULL && addr_pointed2 == NULL)
189         return 0;
190       if (!add_compared_pointers(addr_pointed1, addr_pointed2))
191         return 0;
192
193       pointer_level++;
194
195       // Some cases are not handled here:
196       // * the pointers lead to different areas (one to the heap, the other to the RW segment ...);
197       // * a pointer leads to the read-only segment of the current object;
198       // * a pointer lead to a different ELF object.
199
200       if (addr_pointed1 > std_heap
201           && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)) {
202         if (!
203             (addr_pointed2 > std_heap
204              && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2)))
205           return 1;
206         // The pointers are both in the heap:
207         return compare_heap_area(addr_pointed1, addr_pointed2, snapshot1,
208                                  snapshot2, NULL, type->subtype, pointer_level);
209       }
210       // The pointers are both in the current object R/W segment:
211       else if (addr_pointed1 > start_data
212                && (char *) addr_pointed1 <= (char *) start_data + region_size) {
213         if (!
214             (addr_pointed2 > start_data
215              && (char *) addr_pointed2 <= (char *) start_data + region_size))
216           return 1;
217         if (type->dw_type_id == NULL)
218           return (addr_pointed1 != addr_pointed2);
219         else {
220           void *translated_addr_pointer1 =
221               mc_translate_address((uintptr_t) addr_pointed1, snapshot1);
222           void *translated_addr_pointer2 =
223               mc_translate_address((uintptr_t) addr_pointed2, snapshot2);
224           return compare_areas_with_type(translated_addr_pointer1,
225                                          translated_addr_pointer2, snapshot1,
226                                          snapshot2, type->subtype, region_size,
227                                          region_type, start_data,
228                                          pointer_level);
229         }
230       }
231
232       else {
233         return (addr_pointed1 != addr_pointed2);
234       }
235     }
236     break;
237   case DW_TAG_structure_type:
238   case DW_TAG_class_type:
239     xbt_dynar_foreach(type->members, cursor, member) {
240       XBT_DEBUG("Compare member %s", member->name);
241       void *member1 =
242           mc_member_snapshot_resolve(area1, type, member, snapshot1);
243       void *member2 =
244           mc_member_snapshot_resolve(area2, type, member, snapshot2);
245       res =
246           compare_areas_with_type(member1, member2, snapshot1, snapshot2,
247                                   member->subtype, region_size, region_type,
248                                   start_data, pointer_level);
249       if (res == 1)
250         return res;
251     }
252     break;
253   case DW_TAG_subroutine_type:
254     return -1;
255     break;
256   default:
257     XBT_VERB("Unknown case : %d", type->type);
258     break;
259   }
260
261   return 0;
262 }
263
264 static int compare_global_variables(int region_type, mc_mem_region_t r1,
265                                     mc_mem_region_t r2, mc_snapshot_t snapshot1,
266                                     mc_snapshot_t snapshot2)
267 {
268
269   if (!compared_pointers) {
270     compared_pointers =
271         xbt_dynar_new(sizeof(pointers_pair_t), pointers_pair_free_voidp);
272   } else {
273     xbt_dynar_reset(compared_pointers);
274   }
275
276   xbt_dynar_t variables;
277   int res;
278   unsigned int cursor = 0;
279   dw_variable_t current_var;
280   size_t offset;
281   void *start_data;
282   void *start_data_binary = mc_binary_info->start_rw;
283   void *start_data_libsimgrid = mc_libsimgrid_info->start_rw;
284
285   mc_object_info_t object_info = NULL;
286   if (region_type == 2) {
287     object_info = mc_binary_info;
288     start_data = start_data_binary;
289   } else {
290     object_info = mc_libsimgrid_info;
291     start_data = start_data_libsimgrid;
292   }
293   variables = object_info->global_variables;
294
295   xbt_dynar_foreach(variables, cursor, current_var) {
296
297     // If the variable is not in this object, skip it:
298     // We do not expect to find a pointer to something which is not reachable
299     // by the global variables.
300     if ((char *) current_var->address < (char *) object_info->start_rw
301         || (char *) current_var->address > (char *) object_info->end_rw)
302       continue;
303
304     offset = (char *) current_var->address - (char *) object_info->start_rw;
305
306     dw_type_t bvariable_type = current_var->type;
307     res =
308         compare_areas_with_type((char *) r1->data + offset,
309                                 (char *) r2->data + offset, snapshot1,
310                                 snapshot2, bvariable_type, r1->size,
311                                 region_type, start_data, 0);
312     if (res == 1) {
313       XBT_VERB("Global variable %s (%p - %p) is different between snapshots",
314                current_var->name, (char *) r1->data + offset,
315                (char *) r2->data + offset);
316       xbt_dynar_free(&compared_pointers);
317       compared_pointers = NULL;
318       return 1;
319     }
320
321   }
322
323   xbt_dynar_free(&compared_pointers);
324   compared_pointers = NULL;
325
326   return 0;
327
328 }
329
330 static int compare_local_variables(mc_snapshot_t snapshot1,
331                                    mc_snapshot_t snapshot2,
332                                    mc_snapshot_stack_t stack1,
333                                    mc_snapshot_stack_t stack2, void *heap1,
334                                    void *heap2)
335 {
336   void *start_data_binary = mc_binary_info->start_rw;
337   void *start_data_libsimgrid = mc_libsimgrid_info->start_rw;
338
339   if (!compared_pointers) {
340     compared_pointers =
341         xbt_dynar_new(sizeof(pointers_pair_t), pointers_pair_free_voidp);
342   } else {
343     xbt_dynar_reset(compared_pointers);
344   }
345
346   if (xbt_dynar_length(stack1->local_variables) !=
347       xbt_dynar_length(stack2->local_variables)) {
348     XBT_VERB("Different number of local variables");
349     xbt_dynar_free(&compared_pointers);
350     compared_pointers = NULL;
351     return 1;
352   } else {
353     unsigned int cursor = 0;
354     local_variable_t current_var1, current_var2;
355     int offset1, offset2, res;
356     while (cursor < xbt_dynar_length(stack1->local_variables)) {
357       current_var1 =
358           (local_variable_t) xbt_dynar_get_as(stack1->local_variables, cursor,
359                                               local_variable_t);
360       current_var2 =
361           (local_variable_t) xbt_dynar_get_as(stack2->local_variables, cursor,
362                                               local_variable_t);
363       if (strcmp(current_var1->name, current_var2->name) != 0
364           || current_var1->subprogram != current_var1->subprogram
365           || current_var1->ip != current_var2->ip) {
366         xbt_dynar_free(&compared_pointers);
367         // TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
368         XBT_VERB
369             ("Different name of variable (%s - %s) or frame (%s - %s) or ip (%lu - %lu)",
370              current_var1->name, current_var2->name,
371              current_var1->subprogram->name, current_var2->subprogram->name,
372              current_var1->ip, current_var2->ip);
373         return 1;
374       }
375       offset1 = (char *) current_var1->address - (char *) std_heap;
376       offset2 = (char *) current_var2->address - (char *) std_heap;
377       // TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
378       XBT_DEBUG("Compare local variable %s of frame %s",
379                 current_var1->subprogram->name, current_var1->subprogram->name);
380
381
382       if (current_var1->region == 1) {
383         dw_type_t subtype = current_var1->type;
384         res =
385             compare_areas_with_type((char *) heap1 + offset1,
386                                     (char *) heap2 + offset2, snapshot1,
387                                     snapshot2, subtype, 0, 1,
388                                     start_data_libsimgrid, 0);
389       } else {
390         dw_type_t subtype = current_var2->type;
391         res =
392             compare_areas_with_type((char *) heap1 + offset1,
393                                     (char *) heap2 + offset2, snapshot1,
394                                     snapshot2, subtype, 0, 2, start_data_binary,
395                                     0);
396       }
397       if (res == 1) {
398         // TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
399         XBT_VERB
400             ("Local variable %s (%p - %p) in frame %s  is different between snapshots",
401              current_var1->name, (char *) heap1 + offset1,
402              (char *) heap2 + offset2, current_var1->subprogram->name);
403         xbt_dynar_free(&compared_pointers);
404         compared_pointers = NULL;
405         return res;
406       }
407       cursor++;
408     }
409     xbt_dynar_free(&compared_pointers);
410     compared_pointers = NULL;
411     return 0;
412   }
413 }
414
415 int snapshot_compare(void *state1, void *state2)
416 {
417
418   mc_snapshot_t s1, s2;
419   int num1, num2;
420
421   if (_sg_mc_property_file && _sg_mc_property_file[0] != '\0') {        /* Liveness MC */
422     s1 = ((mc_visited_pair_t) state1)->graph_state->system_state;
423     s2 = ((mc_visited_pair_t) state2)->graph_state->system_state;
424     num1 = ((mc_visited_pair_t) state1)->num;
425     num2 = ((mc_visited_pair_t) state2)->num;
426     /* Firstly compare automaton state */
427     /*if(xbt_automaton_state_compare(((mc_pair_t)state1)->automaton_state, ((mc_pair_t)state2)->automaton_state) != 0)
428        return 1;
429        if(xbt_automaton_propositional_symbols_compare_value(((mc_pair_t)state1)->atomic_propositions, ((mc_pair_t)state2)->atomic_propositions) != 0)
430        return 1; */
431   } else {                      /* Safety MC */
432     s1 = ((mc_visited_state_t) state1)->system_state;
433     s2 = ((mc_visited_state_t) state2)->system_state;
434     num1 = ((mc_visited_state_t) state1)->num;
435     num2 = ((mc_visited_state_t) state2)->num;
436   }
437
438   int errors = 0;
439   int res_init;
440
441   xbt_os_timer_t global_timer = xbt_os_timer_new();
442   xbt_os_timer_t timer = xbt_os_timer_new();
443
444   xbt_os_walltimer_start(global_timer);
445
446 #ifdef MC_DEBUG
447   xbt_os_walltimer_start(timer);
448 #endif
449
450   int hash_result = 0;
451   if (_sg_mc_hash) {
452     hash_result = (s1->hash != s2->hash);
453     if (hash_result) {
454       XBT_VERB("(%d - %d) Different hash : 0x%" PRIx64 "--0x%" PRIx64, num1,
455                num2, s1->hash, s2->hash);
456 #ifndef MC_DEBUG
457       return 1;
458 #endif
459     } else {
460       XBT_VERB("(%d - %d) Same hash : 0x%" PRIx64, num1, num2, s1->hash);
461     }
462   }
463
464   int i = 0;
465   size_t size_used1, size_used2;
466   int is_diff = 0;
467
468
469   /* Compare size of stacks */
470   while (i < xbt_dynar_length(s1->stacks)) {
471     size_used1 = s1->stack_sizes[i];
472     size_used2 = s2->stack_sizes[i];
473     if (size_used1 != size_used2) {
474 #ifdef MC_DEBUG
475       if (is_diff == 0) {
476         xbt_os_walltimer_stop(timer);
477         mc_comp_times->stacks_sizes_comparison_time =
478             xbt_os_timer_elapsed(timer);
479       }
480       XBT_DEBUG("(%d - %d) Different size used in stacks : %zu - %zu", num1,
481                 num2, size_used1, size_used2);
482       errors++;
483       is_diff = 1;
484 #else
485 #ifdef MC_VERBOSE
486       XBT_VERB("(%d - %d) Different size used in stacks : %zu - %zu", num1,
487                num2, size_used1, size_used2);
488 #endif
489
490       xbt_os_walltimer_stop(timer);
491       xbt_os_timer_free(timer);
492       xbt_os_walltimer_stop(global_timer);
493       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
494       xbt_os_timer_free(global_timer);
495
496       return 1;
497 #endif
498     }
499     i++;
500   }
501
502 #ifdef MC_DEBUG
503   if (is_diff == 0)
504     xbt_os_walltimer_stop(timer);
505   xbt_os_walltimer_start(timer);
506 #endif
507
508   /* Init heap information used in heap comparison algorithm */
509   res_init =
510       init_heap_information((xbt_mheap_t) s1->regions[0]->data,
511                             (xbt_mheap_t) s2->regions[0]->data, s1->to_ignore,
512                             s2->to_ignore);
513   if (res_init == -1) {
514 #ifdef MC_DEBUG
515     XBT_DEBUG("(%d - %d) Different heap information", num1, num2);
516     errors++;
517 #else
518 #ifdef MC_VERBOSE
519     XBT_VERB("(%d - %d) Different heap information", num1, num2);
520 #endif
521
522     xbt_os_walltimer_stop(global_timer);
523     mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
524     xbt_os_timer_free(global_timer);
525
526     return 1;
527 #endif
528   }
529 #ifdef MC_DEBUG
530   xbt_os_walltimer_start(timer);
531 #endif
532
533   /* Stacks comparison */
534   unsigned int cursor = 0;
535   int diff_local = 0;
536 #ifdef MC_DEBUG
537   is_diff = 0;
538 #endif
539   mc_snapshot_stack_t stack1, stack2;
540
541   while (cursor < xbt_dynar_length(s1->stacks)) {
542     stack1 =
543         (mc_snapshot_stack_t) xbt_dynar_get_as(s1->stacks, cursor,
544                                                mc_snapshot_stack_t);
545     stack2 =
546         (mc_snapshot_stack_t) xbt_dynar_get_as(s2->stacks, cursor,
547                                                mc_snapshot_stack_t);
548     diff_local =
549         compare_local_variables(s1, s2, stack1, stack2, s1->regions[0]->data,
550                                 s2->regions[0]->data);
551     if (diff_local > 0) {
552 #ifdef MC_DEBUG
553       if (is_diff == 0) {
554         xbt_os_walltimer_stop(timer);
555         mc_comp_times->stacks_comparison_time = xbt_os_timer_elapsed(timer);
556       }
557       XBT_DEBUG("(%d - %d) Different local variables between stacks %d", num1,
558                 num2, cursor + 1);
559       errors++;
560       is_diff = 1;
561 #else
562
563 #ifdef MC_VERBOSE
564       XBT_VERB("(%d - %d) Different local variables between stacks %d", num1,
565                num2, cursor + 1);
566 #endif
567
568       reset_heap_information();
569       xbt_os_walltimer_stop(timer);
570       xbt_os_timer_free(timer);
571       xbt_os_walltimer_stop(global_timer);
572       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
573       xbt_os_timer_free(global_timer);
574
575       return 1;
576 #endif
577     }
578     cursor++;
579   }
580
581
582
583   const char *names[3] = { "?", "libsimgrid", "binary" };
584 #ifdef MC_DEBUG
585   double *times[3] = {
586     NULL,
587     &mc_comp_times->libsimgrid_global_variables_comparison_time,
588     &mc_comp_times->binary_global_variables_comparison_time
589   };
590 #endif
591
592   int k = 0;
593   for (k = 2; k != 0; --k) {
594 #ifdef MC_DEBUG
595     if (is_diff == 0)
596       xbt_os_walltimer_stop(timer);
597     xbt_os_walltimer_start(timer);
598 #endif
599
600     /* Compare global variables */
601     is_diff =
602         compare_global_variables(k, s1->regions[k], s2->regions[k], s1, s2);
603     if (is_diff != 0) {
604 #ifdef MC_DEBUG
605       xbt_os_walltimer_stop(timer);
606       *times[k] = xbt_os_timer_elapsed(timer);
607       XBT_DEBUG("(%d - %d) Different global variables in %s", num1, num2,
608                 names[k]);
609       errors++;
610 #else
611 #ifdef MC_VERBOSE
612       XBT_VERB("(%d - %d) Different global variables in %s", num1, num2,
613                names[k]);
614 #endif
615
616       reset_heap_information();
617       xbt_os_walltimer_stop(timer);
618       xbt_os_timer_free(timer);
619       xbt_os_walltimer_stop(global_timer);
620       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
621       xbt_os_timer_free(global_timer);
622
623       return 1;
624 #endif
625     }
626   }
627
628 #ifdef MC_DEBUG
629   xbt_os_walltimer_start(timer);
630 #endif
631
632   /* Compare heap */
633   if (mmalloc_compare_heap(s1, s2, (xbt_mheap_t) s1->regions[0]->data,
634                            (xbt_mheap_t) s2->regions[0]->data) > 0) {
635
636 #ifdef MC_DEBUG
637     xbt_os_walltimer_stop(timer);
638     mc_comp_times->heap_comparison_time = xbt_os_timer_elapsed(timer);
639     XBT_DEBUG("(%d - %d) Different heap (mmalloc_compare)", num1, num2);
640     errors++;
641 #else
642
643 #ifdef MC_VERBOSE
644     XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", num1, num2);
645 #endif
646
647     reset_heap_information();
648     xbt_os_walltimer_stop(timer);
649     xbt_os_timer_free(timer);
650     xbt_os_walltimer_stop(global_timer);
651     mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
652     xbt_os_timer_free(global_timer);
653
654     return 1;
655 #endif
656   } else {
657 #ifdef MC_DEBUG
658     xbt_os_walltimer_stop(timer);
659 #endif
660   }
661
662   reset_heap_information();
663
664   xbt_os_walltimer_stop(timer);
665   xbt_os_timer_free(timer);
666
667 #ifdef MC_VERBOSE
668   xbt_os_walltimer_stop(global_timer);
669   mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
670 #endif
671
672   xbt_os_timer_free(global_timer);
673
674 #ifdef MC_DEBUG
675   print_comparison_times();
676 #endif
677
678 #ifdef MC_VERBOSE
679   if (errors || hash_result)
680     XBT_VERB("(%d - %d) Difference found", num1, num2);
681   else
682     XBT_VERB("(%d - %d) No difference found", num1, num2);
683 #endif
684
685 #if defined(MC_DEBUG) && defined(MC_VERBOSE)
686   if (_sg_mc_hash) {
687     // * false positive SHOULD be avoided.
688     // * There MUST not be any false negative.
689
690     XBT_VERB("(%d - %d) State equality hash test is %s %s", num1, num2,
691              (hash_result != 0) == (errors != 0) ? "true" : "false",
692              !hash_result ? "positive" : "negative");
693   }
694 #endif
695
696   return errors > 0 || hash_result;
697
698 }
699
700 /***************************** Statistics *****************************/
701 /*******************************************************************/
702
703 void print_comparison_times()
704 {
705   XBT_DEBUG("*** Comparison times ***");
706   XBT_DEBUG("- Nb processes : %f", mc_comp_times->nb_processes_comparison_time);
707   XBT_DEBUG("- Nb bytes used : %f", mc_comp_times->bytes_used_comparison_time);
708   XBT_DEBUG("- Stacks sizes : %f", mc_comp_times->stacks_sizes_comparison_time);
709   XBT_DEBUG("- Binary global variables : %f",
710             mc_comp_times->binary_global_variables_comparison_time);
711   XBT_DEBUG("- Libsimgrid global variables : %f",
712             mc_comp_times->libsimgrid_global_variables_comparison_time);
713   XBT_DEBUG("- Heap : %f", mc_comp_times->heap_comparison_time);
714   XBT_DEBUG("- Stacks : %f", mc_comp_times->stacks_comparison_time);
715 }
716
717 /**************************** MC snapshot compare simcall **************************/
718 /***********************************************************************************/
719
720 int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall,
721                                    mc_snapshot_t s1, mc_snapshot_t s2)
722 {
723   return snapshot_compare(s1, s2);
724 }
725
726 int MC_compare_snapshots(void *s1, void *s2)
727 {
728
729   return simcall_mc_compare_snapshots(s1, s2);
730
731 }