Logo AND Algorithmique Numérique Distribuée

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