Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : remove instruction pointer offset for local variables comparison
[simgrid.git] / src / mc / mc_compare.c
1 /* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
2
3 /* This program is free software; you can redistribute it and/or modify it
4  * under the terms of the license (GNU LGPL) which comes with this package. */
5
6 #include "mc_private.h"
7
8 #include "xbt/mmalloc.h"
9
10 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc,
11                                 "Logging specific to mc_compare");
12
13 static int data_program_region_compare(void *d1, void *d2, size_t size);
14 static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size);
15 static int heap_region_compare(void *d1, void *d2, size_t size);
16
17 static int compare_stack(stack_region_t s1, stack_region_t s2, void *sp1, void *sp2, void *heap1, void *heap2, xbt_dynar_t equals);
18 static int is_heap_equality(xbt_dynar_t equals, void *a1, void *a2);
19 static size_t ignore(void *address);
20
21 static void stack_region_free(stack_region_t s);
22 static void heap_equality_free(heap_equality_t e);
23
24 static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals);
25
26 static size_t ignore(void *address){
27   unsigned int cursor = 0;
28   int start = 0;
29   int end = xbt_dynar_length(mc_comparison_ignore) - 1;
30   mc_ignore_region_t region;
31
32   while(start <= end){
33     cursor = (start + end) / 2;
34     region = (mc_ignore_region_t)xbt_dynar_get_as(mc_comparison_ignore, cursor, mc_ignore_region_t);
35     if(region->address == address)
36       return region->size;
37     if(region->address < address)
38       start = cursor + 1;
39     if(region->address > address)
40       end = cursor - 1;   
41   }
42
43   return 0;
44 }
45
46 static int data_program_region_compare(void *d1, void *d2, size_t size){
47   int distance = 0;
48   size_t i = 0;
49   int pointer_align;
50   void *addr_pointed1 = NULL, *addr_pointed2 = NULL;
51   
52   for(i=0; i<size; i++){
53     if(memcmp(((char *)d1) + i, ((char *)d2) + i, 1) != 0){
54       pointer_align = (i / sizeof(void*)) * sizeof(void*);
55       addr_pointed1 = *((void **)((char *)d1 + pointer_align));
56       addr_pointed2 = *((void **)((char *)d2 + pointer_align));
57       if((addr_pointed1 > start_plt_binary && addr_pointed1 < end_plt_binary) || (addr_pointed2 > start_plt_binary && addr_pointed2 < end_plt_binary)){
58         continue;
59       }else{
60         XBT_DEBUG("Different byte (offset=%zu) (%p - %p) in data program region", i, (char *)d1 + i, (char *)d2 + i);
61         distance++;
62       }
63     }
64   }
65   
66   XBT_DEBUG("Hamming distance between data program regions : %d", distance);
67
68   return distance;
69 }
70
71 static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size){
72   int distance = 0;
73   size_t i = 0, ignore_size = 0;
74   int pointer_align;
75   void *addr_pointed1 = NULL, *addr_pointed2 = NULL;
76
77   for(i=0; i<size; i++){
78     if(memcmp(((char *)d1) + i, ((char *)d2) + i, 1) != 0){
79       if((ignore_size = ignore((char *)start_data_libsimgrid+i)) > 0){
80         i = i + ignore_size;
81         continue;
82       }
83       pointer_align = (i / sizeof(void*)) * sizeof(void*);
84       addr_pointed1 = *((void **)((char *)d1 + pointer_align));
85       addr_pointed2 = *((void **)((char *)d2 + pointer_align));
86       if((addr_pointed1 > start_plt_libsimgrid && addr_pointed1 < end_plt_libsimgrid) || (addr_pointed2 > start_plt_libsimgrid && addr_pointed2 < end_plt_libsimgrid)){
87         continue;
88       }else if(addr_pointed1 >= raw_heap && addr_pointed1 <= end_raw_heap && addr_pointed2 >= raw_heap && addr_pointed2 <= end_raw_heap){
89         continue;
90       }else{
91         XBT_DEBUG("Different byte (offset=%zu) (%p - %p) in data libsimgrid region", i, (char *)d1 + i, (char *)d2 + i);
92         XBT_DEBUG("Addresses pointed : %p - %p\n", addr_pointed1, addr_pointed2);
93         distance++;
94       }
95     }
96   }
97   
98   XBT_DEBUG("Hamming distance between data libsimgrid regions : %d", distance); fflush(NULL);
99   
100   return distance;
101 }
102
103 static int heap_region_compare(void *d1, void *d2, size_t size){
104   
105   int distance = 0;
106   size_t i = 0;
107   
108   for(i=0; i<size; i++){
109     if(memcmp(((char *)d1) + i, ((char *)d2) + i, 1) != 0){
110       XBT_DEBUG("Different byte (offset=%zu) (%p - %p) in heap region", i, (char *)d1 + i, (char *)d2 + i);
111       distance++;
112     }
113   }
114   
115   XBT_DEBUG("Hamming distance between heap regions : %d (total size : %zu)", distance, size);
116
117   return distance;
118 }
119
120 static void stack_region_free(stack_region_t s){
121   if(s){
122     xbt_free(s->process_name);
123     xbt_free(s);
124   }
125 }
126
127 void stack_region_free_voidp(void *s){
128   stack_region_free((stack_region_t) * (void **) s);
129 }
130
131 static void heap_equality_free(heap_equality_t e){
132   if(e){
133     xbt_free(e);
134   }
135 }
136
137 void heap_equality_free_voidp(void *e){
138   heap_equality_free((heap_equality_t) * (void **) e);
139 }
140
141 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
142
143   int errors = 0, i;
144   xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
145   xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
146   xbt_dynar_t equals = xbt_dynar_new(sizeof(heap_equality_t), heap_equality_free_voidp);
147
148   void *heap1 = NULL, *heap2 = NULL;
149   
150   if(s1->num_reg != s2->num_reg){
151     XBT_INFO("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg);
152     return 1;
153   }
154
155   for(i=0 ; i< s1->num_reg ; i++){
156     
157     if(s1->regions[i]->type != s2->regions[i]->type){
158       XBT_INFO("Different type of region");
159       errors++;
160     }
161     
162     switch(s1->regions[i]->type){
163     case 0 :
164       /* Compare heapregion */
165       if(s1->regions[i]->size != s2->regions[i]->size){
166         XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
167         xbt_dynar_free(&stacks1);
168         xbt_dynar_free(&stacks2);
169         xbt_dynar_free(&equals);
170         return 1;
171       }
172       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
173         XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
174         xbt_dynar_free(&stacks1);
175         xbt_dynar_free(&stacks2);
176         xbt_dynar_free(&equals);
177         return 1;
178       }
179       if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[i]->data, (xbt_mheap_t)s2->regions[i]->data, &stacks1, &stacks2, &equals)){
180         XBT_INFO("Different heap (mmalloc_compare)");
181         xbt_dynar_free(&stacks1);
182         xbt_dynar_free(&stacks2);
183         xbt_dynar_free(&equals);
184         return 1; 
185       }
186       heap1 = s1->regions[i]->data;
187       heap2 = s2->regions[i]->data;
188       break;
189     case 1 :
190       /* Compare data libsimgrid region */
191       if(s1->regions[i]->size != s2->regions[i]->size){
192         XBT_INFO("Different size of libsimgrid (data) (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
193         xbt_dynar_free(&stacks1);
194         xbt_dynar_free(&stacks2);
195         xbt_dynar_free(&equals);
196         return 1;
197       }
198       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
199         XBT_INFO("Different start addr of libsimgrid (data) (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
200         xbt_dynar_free(&stacks1);
201         xbt_dynar_free(&stacks2);
202         xbt_dynar_free(&equals);
203         return 1;
204       }
205       if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
206         XBT_INFO("Different memcmp for data in libsimgrid");
207         xbt_dynar_free(&stacks1);
208         xbt_dynar_free(&stacks2);
209         xbt_dynar_free(&equals);
210         return 1;
211       }
212       break;
213
214     case 2 :
215       /* Compare data program region */
216       if(s1->regions[i]->size != s2->regions[i]->size){
217         XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
218         xbt_dynar_free(&stacks1);
219         xbt_dynar_free(&stacks2);
220         xbt_dynar_free(&equals);
221         return 1;
222       }
223       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
224         XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
225         xbt_dynar_free(&stacks1);
226         xbt_dynar_free(&stacks2);
227         xbt_dynar_free(&equals);
228         return 1;
229       }
230       if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
231         XBT_INFO("Different memcmp for data in program");
232         xbt_dynar_free(&stacks1);
233         xbt_dynar_free(&stacks2);
234         xbt_dynar_free(&equals);
235         return 1;
236       }
237       break;
238  
239     }
240
241   }
242
243   /* Stacks comparison */
244   unsigned int cursor = 0;
245   stack_region_t stack_region1, stack_region2;
246   void *sp1, *sp2;
247   int diff = 0, diff_local = 0;
248
249   while(cursor < xbt_dynar_length(stacks1)){
250     XBT_INFO("Stack %d", cursor + 1); 
251     stack_region1 = (stack_region_t)(xbt_dynar_get_as(stacks1, cursor, stack_region_t));
252     stack_region2 = (stack_region_t)(xbt_dynar_get_as(stacks2, cursor, stack_region_t));
253     sp1 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->stack_pointer;
254     sp2 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->stack_pointer;
255     diff = compare_stack(stack_region1, stack_region2, sp1, sp2, heap1, heap2, equals);
256
257     if(diff >0){  
258       diff_local = compare_local_variables(((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, equals);
259       if(diff_local > 0){
260         XBT_INFO("Hamming distance between stacks : %d", diff);
261         xbt_dynar_free(&stacks1);
262         xbt_dynar_free(&stacks2);
263         xbt_dynar_free(&equals);
264         return 1;
265       }else{
266         XBT_INFO("Local variables are equals in stack %d", cursor + 1);
267       }
268     }else{
269       XBT_INFO("Same stacks");
270     }
271     cursor++;
272   }
273
274   xbt_dynar_free(&stacks1);
275   xbt_dynar_free(&stacks2);
276   xbt_dynar_free(&equals);
277   return 0;
278   
279 }
280
281 static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals){
282   
283   xbt_dynar_t tokens1 = xbt_str_split(s1, NULL);
284   xbt_dynar_t tokens2 = xbt_str_split(s2, NULL);
285
286   xbt_dynar_t s_tokens1, s_tokens2;
287   unsigned int cursor = 0;
288   void *addr1, *addr2;
289
290   int diff = 0;
291   
292   while(cursor < xbt_dynar_length(tokens1)){
293     s_tokens1 = xbt_str_split(xbt_dynar_get_as(tokens1, cursor, char *), "=");
294     s_tokens2 = xbt_str_split(xbt_dynar_get_as(tokens2, cursor, char *), "=");
295     if(xbt_dynar_length(s_tokens1) > 1 && xbt_dynar_length(s_tokens2) > 1){
296       if(strcmp(xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *)) != 0){
297         addr1 = (void *) strtoul(xbt_dynar_get_as(s_tokens1, 1, char *), NULL, 16);
298         addr2 = (void *) strtoul(xbt_dynar_get_as(s_tokens2, 1, char *), NULL, 16);
299         if(is_heap_equality(heap_equals, addr1, addr2) == 0){
300           XBT_INFO("Variable %s is different between stacks : %s - %s", xbt_dynar_get_as(s_tokens1, 0, char *), xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *));
301           diff++;
302         }
303       }
304     }
305     xbt_dynar_free(&s_tokens1);
306     xbt_dynar_free(&s_tokens2);
307     cursor++;
308   }
309
310   xbt_dynar_free(&tokens1);
311   xbt_dynar_free(&tokens2);
312   return diff;
313   
314 }
315
316 static int is_heap_equality(xbt_dynar_t equals, void *a1, void *a2){
317
318   unsigned int cursor = 0;
319   int start = 0;
320   int end = xbt_dynar_length(equals) - 1;
321   heap_equality_t current_equality;
322
323   while(start <= end){
324     cursor = (start + end) / 2;
325     current_equality = (heap_equality_t)xbt_dynar_get_as(equals, cursor, heap_equality_t);
326     if(current_equality->address1 == a1){
327       if(current_equality->address2 == a2)
328         return 1;
329       if(current_equality->address2 < a2)
330         start = cursor + 1;
331       if(current_equality->address2 > a2)
332         end = cursor - 1;
333     }
334     if(current_equality->address1 < a1)
335       start = cursor + 1;
336     if(current_equality->address1 > a1)
337       end = cursor - 1; 
338   }
339
340   return 0;
341
342 }
343
344
345 static int compare_stack(stack_region_t s1, stack_region_t s2, void *sp1, void *sp2, void *heap1, void *heap2, xbt_dynar_t equals){
346   
347   size_t k = 0, nb_diff = 0;
348   size_t size_used1 = s1->size - ((char*)sp1 - (char*)s1->address);
349   size_t size_used2 = s2->size - ((char*)sp2 - (char*)s2->address);
350
351   int pointer_align;
352   void *addr_pointed1 = NULL, *addr_pointed2 = NULL;  
353
354   if(size_used1 == size_used2){
355  
356     while(k < size_used1){
357       if(memcmp((char *)s1->address + s1->size - k, (char *)s2->address + s2->size - k, 1) != 0){
358         pointer_align = ((size_used1 - k) / sizeof(void*)) * sizeof(void*);
359         addr_pointed1 = *((void **)(((char*)s1->address + (s1->size - size_used1)) + pointer_align));
360         addr_pointed2 = *((void **)(((char*)s2->address + (s2->size - size_used2)) + pointer_align));
361         if(is_heap_equality(equals, addr_pointed1, addr_pointed2) == 0){
362           if((addr_pointed1 > std_heap) && (addr_pointed1 < (void *)((char *)std_heap + STD_HEAP_SIZE)) && (addr_pointed2 > std_heap) && (addr_pointed2 < (void *)((char *)std_heap + STD_HEAP_SIZE))){
363             if(is_free_area(addr_pointed1, (xbt_mheap_t)heap1) == 0 || is_free_area(addr_pointed2, (xbt_mheap_t)heap2) == 0){
364               //XBT_INFO("Difference at offset %zu (%p - %p)", k, (char *)s1->address + s1->size - k, (char *)s2->address + s2->size - k);
365               nb_diff++;
366             }
367           }else{
368             //XBT_INFO("Difference at offset %zu (%p - %p)", k, (char *)s1->address + s1->size - k, (char *)s2->address + s2->size - k);
369             nb_diff++;
370           } 
371         }
372       } 
373       k++;
374     }
375
376   }else{
377     XBT_INFO("Different size used between stacks");
378     return 1;
379   }
380
381   return nb_diff;
382 }