From c8de39f74a325137f3dd0a65781d1f90322a259f Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 17 Jun 2014 14:06:04 +0200 Subject: [PATCH] [mc] Use mc_snapshot_read in mc_diff (compatibility with per-page snapshots) --- src/mc/mc_diff.c | 88 ++++++++++++-------------------------------- src/mc/mc_private.h | 9 +++++ src/mc/mc_snapshot.c | 12 ++++++ 3 files changed, 44 insertions(+), 65 deletions(-) diff --git a/src/mc/mc_diff.c b/src/mc/mc_diff.c index 5876c96b21..0b5c881391 100644 --- a/src/mc/mc_diff.c +++ b/src/mc/mc_diff.c @@ -788,8 +788,6 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2) * @param state * @param real_area1 Process address for state 1 * @param real_area2 Process address for state 2 - * @param area1 Snapshot address for state 1 - * @param area2 Snapshot address for state 2 * @param snapshot1 Snapshot of state 1 * @param snapshot2 Snapshot of state 2 * @param previous @@ -798,7 +796,6 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2) */ static int compare_heap_area_without_type(struct s_mc_diff *state, void *real_area1, void *real_area2, - void *area1, void *area2, mc_snapshot_t snapshot1, mc_snapshot_t snapshot2, xbt_dynar_t previous, int size, @@ -831,11 +828,11 @@ static int compare_heap_area_without_type(struct s_mc_diff *state, } } - if (memcmp(((char *) area1) + i, ((char *) area2) + i, 1) != 0) { + if (mc_snapshot_memcp(((char *) real_area1) + i, snapshot1, ((char *) real_area2) + i, snapshot2, 1) != 0) { pointer_align = (i / sizeof(void *)) * sizeof(void *); - addr_pointed1 = *((void **) ((char *) area1 + pointer_align)); - addr_pointed2 = *((void **) ((char *) area2 + pointer_align)); + addr_pointed1 = mc_snapshot_read_pointer((char *) real_area1 + pointer_align, snapshot1); + addr_pointed2 = mc_snapshot_read_pointer((char *) real_area2 + pointer_align, snapshot2); if (addr_pointed1 > maestro_stack_start && addr_pointed1 < maestro_stack_end @@ -875,8 +872,6 @@ static int compare_heap_area_without_type(struct s_mc_diff *state, * @param state * @param real_area1 Process address for state 1 * @param real_area2 Process address for state 2 - * @param area1 Snapshot address for state 1 - * @param area2 Snapshot address for state 2 * @param snapshot1 Snapshot of state 1 * @param snapshot2 Snapshot of state 2 * @param previous @@ -888,7 +883,6 @@ static int compare_heap_area_without_type(struct s_mc_diff *state, */ static int compare_heap_area_with_type(struct s_mc_diff *state, void *real_area1, void *real_area2, - void *area1, void *area2, mc_snapshot_t snapshot1, mc_snapshot_t snapshot2, xbt_dynar_t previous, dw_type_t type, @@ -924,12 +918,12 @@ static int compare_heap_area_with_type(struct s_mc_diff *state, if (real_area1 == real_area2) return -1; else - return (memcmp(area1, area2, area_size) != 0); + return (mc_snapshot_memcp(real_area1, snapshot1, real_area2, snapshot2, area_size) != 0); } else { if (area_size != -1 && type->byte_size != area_size) return -1; else { - return (memcmp(area1, area2, type->byte_size) != 0); + return (mc_snapshot_memcp(real_area1, snapshot1, real_area2, snapshot2, type->byte_size) != 0); } } break; @@ -937,13 +931,13 @@ 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 (memcmp(area1, area2, type->byte_size) != 0); + return (mc_snapshot_memcp(real_area1, snapshot1, real_area2, snapshot2, 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, area1, - area2, snapshot1, snapshot2, previous, + return compare_heap_area_with_type(state, real_area1, real_area2, + snapshot1, snapshot2, previous, type->subtype, area_size, check_ignore, pointer_level); break; @@ -984,8 +978,6 @@ static int compare_heap_area_with_type(struct s_mc_diff *state, compare_heap_area_with_type(state, (char *) real_area1 + (i * elm_size), (char *) real_area2 + (i * elm_size), - (char *) area1 + (i * elm_size), - (char *) area2 + (i * elm_size), snapshot1, snapshot2, previous, type->subtype, subtype->byte_size, check_ignore, pointer_level); @@ -997,15 +989,15 @@ static int compare_heap_area_with_type(struct s_mc_diff *state, case DW_TAG_rvalue_reference_type: case DW_TAG_pointer_type: if (type->subtype && type->subtype->type == DW_TAG_subroutine_type) { - addr_pointed1 = *((void **) (area1)); - addr_pointed2 = *((void **) (area2)); + addr_pointed1 = mc_snapshot_read_pointer(real_area1, snapshot1); + addr_pointed2 = mc_snapshot_read_pointer(real_area2, snapshot2); return (addr_pointed1 != addr_pointed2);; } else { pointer_level++; if (pointer_level > 1) { /* Array of pointers */ for (i = 0; i < (area_size / sizeof(void *)); i++) { - addr_pointed1 = *((void **) ((char *) area1 + (i * sizeof(void *)))); - addr_pointed2 = *((void **) ((char *) area2 + (i * sizeof(void *)))); + addr_pointed1 = mc_snapshot_read_pointer((char*) real_area1 + i * sizeof(void *), snapshot1); + addr_pointed2 = mc_snapshot_read_pointer((char*) real_area2 + i * sizeof(void *), snapshot2); if (addr_pointed1 > state->s_heap && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1) && addr_pointed2 > state->s_heap @@ -1020,8 +1012,8 @@ static int compare_heap_area_with_type(struct s_mc_diff *state, return res; } } else { - addr_pointed1 = *((void **) (area1)); - addr_pointed2 = *((void **) (area2)); + addr_pointed1 = mc_snapshot_read_pointer(real_area1, snapshot1); + addr_pointed2 = mc_snapshot_read_pointer(real_area2, snapshot2); if (addr_pointed1 > state->s_heap && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1) && addr_pointed2 > state->s_heap @@ -1043,15 +1035,9 @@ static int compare_heap_area_with_type(struct s_mc_diff *state, for (i = 0; i < (area_size / type->byte_size); i++) { res = compare_heap_area_with_type(state, - (char *) real_area1 + - (i * type->byte_size), - (char *) real_area2 + - (i * type->byte_size), - (char *) area1 + - (i * type->byte_size), - (char *) area2 + - (i * type->byte_size), snapshot1, - snapshot2, previous, type, -1, + (char *) real_area1 + i * type->byte_size, + (char *) real_area2 + i * type->byte_size, + snapshot1, snapshot2, previous, type, -1, check_ignore, 0); if (res == 1) return res; @@ -1067,13 +1053,9 @@ static int compare_heap_area_with_type(struct s_mc_diff *state, mc_member_resolve(real_area1, type, member, snapshot1); char *real_member2 = mc_member_resolve(real_area2, type, member, snapshot2); - char *member1 = - mc_translate_address((uintptr_t) real_member1, snapshot1); - char *member2 = - mc_translate_address((uintptr_t) real_member2, snapshot2); res = compare_heap_area_with_type(state, real_member1, real_member2, - member1, member2, snapshot1, snapshot2, + snapshot1, snapshot2, previous, member->subtype, -1, check_ignore, 0); if (res == 1) { @@ -1083,8 +1065,8 @@ static int compare_heap_area_with_type(struct s_mc_diff *state, } break; case DW_TAG_union_type: - return compare_heap_area_without_type(state, real_area1, real_area2, area1, - area2, snapshot1, snapshot2, previous, + return compare_heap_area_without_type(state, real_area1, real_area2, + snapshot1, snapshot2, previous, type->byte_size, check_ignore); break; default: @@ -1175,9 +1157,8 @@ int compare_heap_area(void *area1, void *area2, mc_snapshot_t snapshot1, ssize_t size; int check_ignore = 0; - void *addr_block1, *addr_block2, *addr_frag1, *addr_frag2, *real_addr_block1, + void *real_addr_block1, *real_addr_block2, *real_addr_frag1, *real_addr_frag2; - void *area1_to_compare, *area2_to_compare; int type_size = -1; int offset1 = 0, offset2 = 0; int new_size1 = -1, new_size2 = -1; @@ -1217,13 +1198,6 @@ int compare_heap_area(void *area1, void *area2, mc_snapshot_t snapshot1, } return 1; } - // Snapshot address of the block: - addr_block1 = - ((void *) (((ADDR2UINT(block1)) - 1) * BLOCKSIZE + - (char *) state->heapbase1)); - addr_block2 = - ((void *) (((ADDR2UINT(block2)) - 1) * BLOCKSIZE + - (char *) state->heapbase2)); // Process address of the block: real_addr_block1 = @@ -1333,9 +1307,6 @@ int compare_heap_area(void *area1, void *area2, mc_snapshot_t snapshot1, frag1 = -1; frag2 = -1; - area1_to_compare = addr_block1; - area2_to_compare = addr_block2; - if ((state->heapinfo1[block1].busy_block.ignore > 0) && (state->heapinfo2[block2].busy_block.ignore == state->heapinfo1[block1].busy_block.ignore)) @@ -1351,14 +1322,6 @@ int compare_heap_area(void *area1, void *area2, mc_snapshot_t snapshot1, ((uintptr_t) (ADDR2UINT(area2) % (BLOCKSIZE))) >> state-> heapinfo2[block2].type; - // Snapshot address of the fragment: - addr_frag1 = - (void *) ((char *) addr_block1 + - (frag1 << state->heapinfo1[block1].type)); - addr_frag2 = - (void *) ((char *) addr_block2 + - (frag2 << state->heapinfo2[block2].type)); - // Process address of the fragment: real_addr_frag1 = (void *) ((char *) real_addr_block1 + @@ -1489,9 +1452,6 @@ int compare_heap_area(void *area1, void *area2, mc_snapshot_t snapshot1, } } - area1_to_compare = (char *) addr_frag1 + offset1; - area2_to_compare = (char *) addr_frag2 + offset2; - if (new_size1 > 0 && new_size1 == new_size2) { type = new_type1; size = new_size1; @@ -1533,14 +1493,12 @@ int compare_heap_area(void *area1, void *area2, mc_snapshot_t snapshot1, /* Start comparison */ if (type) { res_compare = - compare_heap_area_with_type(state, area1, area2, area1_to_compare, - area2_to_compare, snapshot1, snapshot2, + compare_heap_area_with_type(state, area1, area2, snapshot1, snapshot2, previous, type, size, check_ignore, pointer_level); } else { res_compare = - compare_heap_area_without_type(state, area1, area2, area1_to_compare, - area2_to_compare, snapshot1, snapshot2, + compare_heap_area_without_type(state, area1, area2, snapshot1, snapshot2, previous, size, check_ignore); } if (res_compare == 1) { diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index d5d01de568..9d07e71052 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -156,6 +156,15 @@ static inline bool mc_snapshot_region_linear(mc_mem_region_t region) { void* mc_snapshot_read_region(void* addr, mc_mem_region_t region, void* target, size_t size); void* mc_snapshot_read(void* addr, mc_snapshot_t snapshot, void* target, size_t size); +int mc_snapshot_memcp( + void* addr1, mc_snapshot_t snapshot1, + void* addr2, mc_snapshot_t snapshot2, size_t size); + +static inline void* mc_snapshot_read_pointer(void* addr, mc_snapshot_t snapshot) +{ + void* res; + return *(void**) mc_snapshot_read(addr, snapshot, &res, sizeof(void*)); +} /** @brief State of the model-checker (global variables for the model checker) * diff --git a/src/mc/mc_snapshot.c b/src/mc/mc_snapshot.c index 86046fb26f..71b038e139 100644 --- a/src/mc/mc_snapshot.c +++ b/src/mc/mc_snapshot.c @@ -164,3 +164,15 @@ void* mc_snapshot_read(void* addr, mc_snapshot_t snapshot, void* target, size_t return addr; } } + +int mc_snapshot_memcp( + void* addr1, mc_snapshot_t snapshot1, + void* addr2, mc_snapshot_t snapshot2, size_t size) +{ + void* buffer1 = mc_snapshot_read(addr1, snapshot1, alloca(size), size); + void* buffer2 = mc_snapshot_read(addr2, snapshot2, alloca(size), size); + if (buffer1 == buffer2) { + return 0; + } + return memcmp(buffer1, buffer2, size); +} -- 2.20.1