return 1;
}
-static int compare_areas_with_type(void *area1, void *area2,
- mc_snapshot_t snapshot1,
- mc_snapshot_t snapshot2, dw_type_t type,
- int region_size, int region_type,
- void *start_data, int pointer_level)
+static int compare_areas_with_type(void* real_area1, mc_snapshot_t snapshot1, mc_mem_region_t region1,
+ void* real_area2, mc_snapshot_t snapshot2, mc_mem_region_t region2,
+ dw_type_t type, int pointer_level)
{
-
unsigned int cursor = 0;
dw_type_t member, subtype, subsubtype;
int elm_size, i, res;
- void *addr_pointed1, *addr_pointed2;
+ top:
switch (type->type) {
case DW_TAG_unspecified_type:
return 1;
case DW_TAG_base_type:
case DW_TAG_enumeration_type:
case DW_TAG_union_type:
- return (memcmp(area1, area2, type->byte_size) != 0);
+ {
+ void* data1 =
+ mc_snapshot_read_region(real_area1, region1, alloca(type->byte_size), type->byte_size);
+ void* data2 =
+ mc_snapshot_read_region(real_area2, region1, alloca(type->byte_size), type->byte_size);
+ return (memcmp(data1, data2, type->byte_size) != 0);
break;
+ }
case DW_TAG_typedef:
case DW_TAG_volatile_type:
case DW_TAG_const_type:
- return compare_areas_with_type(area1, area2, snapshot1, snapshot2,
- type->subtype, region_size, region_type,
- start_data, pointer_level);
- break;
+ // Poor man's TCO:
+ type = type->subtype;
+ goto top;
case DW_TAG_array_type:
subtype = type->subtype;
switch (subtype->type) {
break;
}
for (i = 0; i < type->element_count; i++) {
- res =
- compare_areas_with_type((char *) area1 + (i * elm_size),
- (char *) area2 + (i * elm_size), snapshot1,
- snapshot2, type->subtype, region_size,
- region_type, start_data, pointer_level);
+ size_t off = i * elm_size;
+ res = compare_areas_with_type(
+ (char*) real_area1 + off, snapshot1, region1,
+ (char*) real_area2 + off, snapshot2, region2,
+ type->subtype, pointer_level);
if (res == 1)
return res;
}
case DW_TAG_pointer_type:
case DW_TAG_reference_type:
case DW_TAG_rvalue_reference_type:
-
- addr_pointed1 = *((void **) (area1));
- addr_pointed2 = *((void **) (area2));
+ {
+ void* temp;
+ void* addr_pointed1 = *(void**) mc_snapshot_read_region(real_area1, region1, &temp, sizeof(void**));
+ void* addr_pointed2 = *(void**) mc_snapshot_read_region(real_area2, region2, &temp, sizeof(void**));
if (type->subtype && type->subtype->type == DW_TAG_subroutine_type) {
return (addr_pointed1 != addr_pointed2);
snapshot2, NULL, type->subtype, pointer_level);
}
// The pointers are both in the current object R/W segment:
- else if (addr_pointed1 > start_data
- && (char *) addr_pointed1 <= (char *) start_data + region_size) {
+ else if (addr_pointed1 > region1->start_addr
+ && (char *) addr_pointed1 <= (char *) region1->start_addr + region1->size) {
if (!
- (addr_pointed2 > start_data
- && (char *) addr_pointed2 <= (char *) start_data + region_size))
+ (addr_pointed2 > region2->start_addr
+ && (char *) addr_pointed2 <= (char *) region2->start_addr + region2->size))
return 1;
if (type->dw_type_id == NULL)
return (addr_pointed1 != addr_pointed2);
else {
- void *translated_addr_pointer1 =
- mc_translate_address((uintptr_t) addr_pointed1, snapshot1);
- void *translated_addr_pointer2 =
- mc_translate_address((uintptr_t) addr_pointed2, snapshot2);
- return compare_areas_with_type(translated_addr_pointer1,
- translated_addr_pointer2, snapshot1,
- snapshot2, type->subtype, region_size,
- region_type, start_data,
- pointer_level);
+ return compare_areas_with_type(addr_pointed1, snapshot1, region1,
+ addr_pointed2, snapshot2, region2,
+ type->subtype, pointer_level);
}
}
}
}
break;
+ }
case DW_TAG_structure_type:
case DW_TAG_class_type:
xbt_dynar_foreach(type->members, cursor, member) {
- XBT_DEBUG("Compare member %s", member->name);
void *member1 =
- mc_member_snapshot_resolve(area1, type, member, snapshot1);
+ mc_member_resolve(real_area1, type, member, snapshot1);
void *member2 =
- mc_member_snapshot_resolve(area2, type, member, snapshot2);
+ mc_member_resolve(real_area2, type, member, snapshot2);
+ mc_mem_region_t subregion1 = mc_get_region_hinted(member1, snapshot1, region1);
+ mc_mem_region_t subregion2 = mc_get_region_hinted(member2, snapshot2, region2);
res =
- compare_areas_with_type(member1, member2, snapshot1, snapshot2,
- member->subtype, region_size, region_type,
- start_data, pointer_level);
+ compare_areas_with_type(member1, snapshot1, subregion1,
+ member2, snapshot2, subregion2,
+ member->subtype, pointer_level);
if (res == 1)
return res;
}
int res;
unsigned int cursor = 0;
dw_variable_t current_var;
- size_t offset;
- void *start_data;
- void *start_data_binary = mc_binary_info->start_rw;
- void *start_data_libsimgrid = mc_libsimgrid_info->start_rw;
mc_object_info_t object_info = NULL;
if (region_type == 2) {
object_info = mc_binary_info;
- start_data = start_data_binary;
} else {
object_info = mc_libsimgrid_info;
- start_data = start_data_libsimgrid;
}
variables = object_info->global_variables;
|| (char *) current_var->address > (char *) object_info->end_rw)
continue;
- offset = (char *) current_var->address - (char *) object_info->start_rw;
-
dw_type_t bvariable_type = current_var->type;
res =
- compare_areas_with_type((char *) r1->data + offset,
- (char *) r2->data + offset, snapshot1,
- snapshot2, bvariable_type, r1->size,
- region_type, start_data, 0);
+ compare_areas_with_type((char *) current_var->address, snapshot1, r1,
+ (char *) current_var->address, snapshot2, r2,
+ bvariable_type, 0);
if (res == 1) {
- XBT_VERB("Global variable %s (%p - %p) is different between snapshots",
- current_var->name, (char *) r1->data + offset,
- (char *) r2->data + offset);
+ XBT_VERB("Global variable %s (%p) is different between snapshots",
+ current_var->name, (char *) current_var->address);
xbt_dynar_free(&compared_pointers);
compared_pointers = NULL;
return 1;
static int compare_local_variables(mc_snapshot_t snapshot1,
mc_snapshot_t snapshot2,
mc_snapshot_stack_t stack1,
- mc_snapshot_stack_t stack2, void *heap1,
- void *heap2)
+ mc_snapshot_stack_t stack2)
{
- void *start_data_binary = mc_binary_info->start_rw;
- void *start_data_libsimgrid = mc_libsimgrid_info->start_rw;
-
if (!compared_pointers) {
compared_pointers =
xbt_dynar_new(sizeof(pointers_pair_t), pointers_pair_free_voidp);
} else {
unsigned int cursor = 0;
local_variable_t current_var1, current_var2;
- int offset1, offset2, res;
+ int res;
while (cursor < xbt_dynar_length(stack1->local_variables)) {
current_var1 =
(local_variable_t) xbt_dynar_get_as(stack1->local_variables, cursor,
current_var1->ip, current_var2->ip);
return 1;
}
- offset1 = (char *) current_var1->address - (char *) std_heap;
- offset2 = (char *) current_var2->address - (char *) std_heap;
// TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
- XBT_DEBUG("Compare local variable %s of frame %s",
- current_var1->subprogram->name, current_var1->subprogram->name);
-
- if (current_var1->region == 1) {
dw_type_t subtype = current_var1->type;
res =
- compare_areas_with_type((char *) heap1 + offset1,
- (char *) heap2 + offset2, snapshot1,
- snapshot2, subtype, 0, 1,
- start_data_libsimgrid, 0);
- } else {
- dw_type_t subtype = current_var2->type;
- res =
- compare_areas_with_type((char *) heap1 + offset1,
- (char *) heap2 + offset2, snapshot1,
- snapshot2, subtype, 0, 2, start_data_binary,
- 0);
- }
+ compare_areas_with_type(current_var1->address, snapshot1, mc_get_snapshot_region(current_var1->address, snapshot1),
+ current_var2->address, snapshot2, mc_get_snapshot_region(current_var2->address, snapshot2),
+ subtype, 0);
+
if (res == 1) {
// TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
XBT_VERB
("Local variable %s (%p - %p) in frame %s is different between snapshots",
- current_var1->name, (char *) heap1 + offset1,
- (char *) heap2 + offset2, current_var1->subprogram->name);
+ current_var1->name, current_var1->address, current_var2->address,
+ current_var1->subprogram->name);
xbt_dynar_free(&compared_pointers);
compared_pointers = NULL;
return res;
mc_snapshot_t s1, s2;
int num1, num2;
- if (_sg_mc_property_file && _sg_mc_property_file[0] != '\0') { /* Liveness MC */
+ if (_sg_mc_liveness) { /* Liveness MC */
s1 = ((mc_visited_pair_t) state1)->graph_state->system_state;
s2 = ((mc_visited_pair_t) state2)->graph_state->system_state;
num1 = ((mc_visited_pair_t) state1)->num;
num2 = ((mc_visited_pair_t) state2)->num;
- /* Firstly compare automaton state */
- /*if(xbt_automaton_state_compare(((mc_pair_t)state1)->automaton_state, ((mc_pair_t)state2)->automaton_state) != 0)
- return 1;
- if(xbt_automaton_propositional_symbols_compare_value(((mc_pair_t)state1)->atomic_propositions, ((mc_pair_t)state2)->atomic_propositions) != 0)
- return 1; */
- } else { /* Safety MC */
+ } else { /* Safety or comm determinism MC */
s1 = ((mc_visited_state_t) state1)->system_state;
s2 = ((mc_visited_state_t) state2)->system_state;
num1 = ((mc_visited_state_t) state1)->num;
}
}
+ /* Compare enabled processes */
+ unsigned int cursor;
+ int pid;
+ xbt_dynar_foreach(s1->enabled_processes, cursor, pid){
+ if(!xbt_dynar_member(s2->enabled_processes, &pid))
+ XBT_VERB("(%d - %d) Different enabled processes", num1, num2);
+ }
+
int i = 0;
size_t size_used1, size_used2;
int is_diff = 0;
-
/* Compare size of stacks */
while (i < xbt_dynar_length(s1->stacks)) {
size_used1 = s1->stack_sizes[i];
#endif
/* Stacks comparison */
- unsigned int cursor = 0;
+ cursor = 0;
int diff_local = 0;
#ifdef MC_DEBUG
is_diff = 0;
(mc_snapshot_stack_t) xbt_dynar_get_as(s2->stacks, cursor,
mc_snapshot_stack_t);
diff_local =
- compare_local_variables(s1, s2, stack1, stack2, s1->regions[0]->data,
- s2->regions[0]->data);
+ compare_local_variables(s1, s2, stack1, stack2);
if (diff_local > 0) {
#ifdef MC_DEBUG
if (is_diff == 0) {
#endif
/* Compare heap */
- if (mmalloc_compare_heap(s1, s2, (xbt_mheap_t) s1->regions[0]->data,
- (xbt_mheap_t) s2->regions[0]->data) > 0) {
+ if (mmalloc_compare_heap(s1, s2) > 0) {
#ifdef MC_DEBUG
xbt_os_walltimer_stop(timer);
