/** \file compare.cpp Memory snapshooting and comparison */
-#include <cinttypes>
-
-#include <array>
-#include <memory>
-#include <set>
-#include <utility>
-#include <unordered_set>
-
-#include "xbt/dynar.h"
-#include "xbt/sysdep.h"
-#include <xbt/mmalloc.h>
-
-#include <mc/mc.h>
-#include <mc/datatypes.h>
-
-#include "src/internal_config.h"
-
-#include "src/xbt/mmalloc/mmprivate.h"
-
-#if HAVE_SMPI
-#include "src/smpi/include/private.hpp"
-#endif
-
-#include "src/mc/Frame.hpp"
-#include "src/mc/ObjectInformation.hpp"
-#include "src/mc/Type.hpp"
-#include "src/mc/Variable.hpp"
#include "src/mc/mc_config.hpp"
-#include "src/mc/mc_dwarf.hpp"
-#include "src/mc/mc_forward.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_smx.hpp"
-#include "src/mc/sosp/mc_snapshot.hpp"
+#include "src/mc/sosp/Snapshot.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, xbt, "Logging specific to mc_compare in mc");
struct ProcessComparisonState;
struct StateComparator;
-static int compare_heap_area(
- StateComparator& state,
- int process_index, const void *area1, const void* area2,
- Snapshot* snapshot1, Snapshot* snapshot2,
- HeapLocationPairs* previous, Type* type, int pointer_level);
-
+static int compare_heap_area(StateComparator& state, const void* area1, const void* area2, Snapshot* snapshot1,
+ Snapshot* snapshot2, HeapLocationPairs* previous, Type* type, int pointer_level);
}
}
}
// TODO, have a robust way to find it in O(1)
-static inline RegionSnapshot* MC_get_heap_region(Snapshot* snapshot)
+static inline Region* MC_get_heap_region(Snapshot* snapshot)
{
- for (auto const& region : snapshot->snapshot_regions)
+ for (auto const& region : snapshot->snapshot_regions_)
if (region->region_type() == simgrid::mc::RegionType::Heap)
return region.get();
xbt_die("No heap region");
malloc_info heapinfo_temp2;
malloc_info heapinfo_temp2b;
- simgrid::mc::RegionSnapshot* heap_region1 = MC_get_heap_region(snapshot1);
- simgrid::mc::RegionSnapshot* heap_region2 = MC_get_heap_region(snapshot2);
+ simgrid::mc::Region* heap_region1 = MC_get_heap_region(snapshot1);
+ simgrid::mc::Region* heap_region2 = MC_get_heap_region(snapshot2);
// This is the address of std_heap->heapinfo in the application process:
void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo;
// This is in snapshot do not use them directly:
- const malloc_info* heapinfos1 = snapshot1->read<malloc_info*>(
- RemotePtr<malloc_info*>((std::uint64_t)heapinfo_address), simgrid::mc::ProcessIndexMissing);
- const malloc_info* heapinfos2 = snapshot2->read<malloc_info*>(
- RemotePtr<malloc_info*>((std::uint64_t)heapinfo_address), simgrid::mc::ProcessIndexMissing);
+ const malloc_info* heapinfos1 =
+ snapshot1->read<malloc_info*>(RemotePtr<malloc_info*>((std::uint64_t)heapinfo_address));
+ const malloc_info* heapinfos2 =
+ snapshot2->read<malloc_info*>(RemotePtr<malloc_info*>((std::uint64_t)heapinfo_address));
while (i1 < state.heaplimit) {
- const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(heap_region1, &heapinfo_temp1, &heapinfos1[i1], sizeof(malloc_info));
- const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(heap_region2, &heapinfo_temp2, &heapinfos2[i1], sizeof(malloc_info));
+ const malloc_info* heapinfo1 =
+ (const malloc_info*)heap_region1->read(&heapinfo_temp1, &heapinfos1[i1], sizeof(malloc_info));
+ const malloc_info* heapinfo2 =
+ (const malloc_info*)heap_region2->read(&heapinfo_temp2, &heapinfos2[i1], sizeof(malloc_info));
if (heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type == MMALLOC_TYPE_HEAPINFO) { /* Free block */
i1 ++;
/* Try first to associate to same block in the other heap */
if (heapinfo2->type == heapinfo1->type && state.equals_to2_(i1, 0).valid_ == 0) {
void* addr_block2 = (ADDR2UINT(i1) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
- int res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing, addr_block1, addr_block2,
- snapshot1, snapshot2, nullptr, nullptr, 0);
+ int res_compare = compare_heap_area(state, addr_block1, addr_block2, snapshot1, snapshot2, nullptr, nullptr, 0);
if (res_compare != 1) {
for (size_t k = 1; k < heapinfo2->busy_block.size; k++)
state.equals_to2_(i1 + k, 0) = HeapArea(i1, -1);
continue;
}
- const malloc_info* heapinfo2b = (const malloc_info*) MC_region_read(heap_region2, &heapinfo_temp2b, &heapinfos2[i2], sizeof(malloc_info));
+ const malloc_info* heapinfo2b =
+ (const malloc_info*)heap_region2->read(&heapinfo_temp2b, &heapinfos2[i2], sizeof(malloc_info));
if (heapinfo2b->type != MMALLOC_TYPE_UNFRAGMENTED) {
i2++;
continue;
}
- int res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing, addr_block1, addr_block2,
- snapshot1, snapshot2, nullptr, nullptr, 0);
+ int res_compare = compare_heap_area(state, addr_block1, addr_block2, snapshot1, snapshot2, nullptr, nullptr, 0);
if (res_compare != 1) {
for (size_t k = 1; k < heapinfo2b->busy_block.size; k++)
if (heapinfo2->type == heapinfo1->type && not state.equals_to2_(i1, j1).valid_) {
void* addr_block2 = (ADDR2UINT(i1) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
void* addr_frag2 = (void*)((char*)addr_block2 + (j1 << heapinfo2->type));
- int res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing, addr_frag1, addr_frag2,
- snapshot1, snapshot2, nullptr, nullptr, 0);
+ int res_compare = compare_heap_area(state, addr_frag1, addr_frag2, snapshot1, snapshot2, nullptr, nullptr, 0);
if (res_compare != 1)
equal = true;
}
while (i2 < state.heaplimit && not equal) {
- const malloc_info* heapinfo2b = (const malloc_info*) MC_region_read(
- heap_region2, &heapinfo_temp2b, &heapinfos2[i2],
- sizeof(malloc_info));
+ const malloc_info* heapinfo2b =
+ (const malloc_info*)heap_region2->read(&heapinfo_temp2b, &heapinfos2[i2], sizeof(malloc_info));
if (heapinfo2b->type == MMALLOC_TYPE_FREE || heapinfo2b->type == MMALLOC_TYPE_HEAPINFO) {
i2 ++;
void* addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
void* addr_frag2 = (void*)((char*)addr_block2 + (j2 << heapinfo2b->type));
- int res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing, addr_frag1, addr_frag2,
- snapshot2, snapshot2, nullptr, nullptr, 0);
+ int res_compare =
+ compare_heap_area(state, addr_frag1, addr_frag2, snapshot2, snapshot2, nullptr, nullptr, 0);
if (res_compare != 1) {
equal = true;
break;
/* All blocks/fragments are equal to another block/fragment_ ? */
for (size_t i = 1; i < state.heaplimit; i++) {
- const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(
- heap_region1, &heapinfo_temp1, &heapinfos1[i], sizeof(malloc_info));
+ const malloc_info* heapinfo1 =
+ (const malloc_info*)heap_region1->read(&heapinfo_temp1, &heapinfos1[i], sizeof(malloc_info));
if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED && i1 == state.heaplimit && heapinfo1->busy_block.busy_size > 0 &&
not state.equals_to1_(i, 0).valid_) {
XBT_DEBUG("Number of blocks/fragments not found in heap1: %d", nb_diff1);
for (size_t i = 1; i < state.heaplimit; i++) {
- const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(
- heap_region2, &heapinfo_temp2, &heapinfos2[i], sizeof(malloc_info));
+ const malloc_info* heapinfo2 =
+ (const malloc_info*)heap_region2->read(&heapinfo_temp2, &heapinfos2[i], sizeof(malloc_info));
if (heapinfo2->type == MMALLOC_TYPE_UNFRAGMENTED && i1 == state.heaplimit && heapinfo2->busy_block.busy_size > 0 &&
not state.equals_to2_(i, 0).valid_) {
XBT_DEBUG("Block %zu not found (size used = %zu)", i,
* @param size
* @param check_ignore
*/
-static int compare_heap_area_without_type(
- simgrid::mc::StateComparator& state, int process_index,
- const void *real_area1, const void *real_area2,
- simgrid::mc::Snapshot* snapshot1,
- simgrid::mc::Snapshot* snapshot2,
- HeapLocationPairs* previous, int size,
- int check_ignore)
+static int compare_heap_area_without_type(simgrid::mc::StateComparator& state, const void* real_area1,
+ const void* real_area2, simgrid::mc::Snapshot* snapshot1,
+ simgrid::mc::Snapshot* snapshot2, HeapLocationPairs* previous, int size,
+ int check_ignore)
{
simgrid::mc::RemoteClient* process = &mc_model_checker->process();
- simgrid::mc::RegionSnapshot* heap_region1 = MC_get_heap_region(snapshot1);
- simgrid::mc::RegionSnapshot* heap_region2 = MC_get_heap_region(snapshot2);
+ simgrid::mc::Region* heap_region1 = MC_get_heap_region(snapshot1);
+ simgrid::mc::Region* heap_region2 = MC_get_heap_region(snapshot2);
for (int i = 0; i < size; ) {
if (MC_snapshot_region_memcmp(((char *) real_area1) + i, heap_region1, ((char *) real_area2) + i, heap_region2, 1) != 0) {
int pointer_align = (i / sizeof(void *)) * sizeof(void *);
- const void* addr_pointed1 = snapshot1->read(
- remote((void**)((char *) real_area1 + pointer_align)), process_index);
- const void* addr_pointed2 = snapshot2->read(
- remote((void**)((char *) real_area2 + pointer_align)), process_index);
+ const void* addr_pointed1 = snapshot1->read(remote((void**)((char*)real_area1 + pointer_align)));
+ const void* addr_pointed2 = snapshot2->read(remote((void**)((char*)real_area2 + pointer_align)));
if (process->in_maestro_stack(remote(addr_pointed1))
&& process->in_maestro_stack(remote(addr_pointed2))) {
&& addr_pointed2 > state.std_heap_copy.heapbase
&& addr_pointed2 < mc_snapshot_get_heap_end(snapshot2)) {
// Both addreses are in the heap:
- int res_compare = compare_heap_area(state ,process_index,
- addr_pointed1, addr_pointed2,
- snapshot1, snapshot2, previous, nullptr, 0);
+ int res_compare =
+ compare_heap_area(state, addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous, nullptr, 0);
if (res_compare == 1)
return res_compare;
i = pointer_align + sizeof(void *);
* @param pointer_level
* @return 0 (same), 1 (different), -1 (unknown)
*/
-static int compare_heap_area_with_type(
- simgrid::mc::StateComparator& state, int process_index,
- const void *real_area1, const void *real_area2,
- simgrid::mc::Snapshot* snapshot1,
- simgrid::mc::Snapshot* snapshot2,
- HeapLocationPairs* previous, simgrid::mc::Type* type,
- int area_size, int check_ignore,
- int pointer_level)
+static int compare_heap_area_with_type(simgrid::mc::StateComparator& state, const void* real_area1,
+ const void* real_area2, simgrid::mc::Snapshot* snapshot1,
+ simgrid::mc::Snapshot* snapshot2, HeapLocationPairs* previous,
+ simgrid::mc::Type* type, int area_size, int check_ignore, int pointer_level)
{
do {
const void* addr_pointed1;
const void* addr_pointed2;
- simgrid::mc::RegionSnapshot* heap_region1 = MC_get_heap_region(snapshot1);
- simgrid::mc::RegionSnapshot* heap_region2 = MC_get_heap_region(snapshot2);
+ simgrid::mc::Region* heap_region1 = MC_get_heap_region(snapshot1);
+ simgrid::mc::Region* heap_region2 = MC_get_heap_region(snapshot2);
switch (type->type) {
case DW_TAG_unspecified_type:
}
for (int i = 0; i < type->element_count; i++) {
// TODO, add support for variable stride (DW_AT_byte_stride)
- int res = compare_heap_area_with_type(state, process_index, (char*)real_area1 + (i * elm_size),
+ int res = compare_heap_area_with_type(state, (char*)real_area1 + (i * elm_size),
(char*)real_area2 + (i * elm_size), snapshot1, snapshot2, previous,
type->subtype, subtype->byte_size, check_ignore, pointer_level);
if (res == 1)
case DW_TAG_rvalue_reference_type:
case DW_TAG_pointer_type:
if (type->subtype && type->subtype->type == DW_TAG_subroutine_type) {
- addr_pointed1 = snapshot1->read(remote((void**)real_area1), process_index);
- addr_pointed2 = snapshot2->read(remote((void**)real_area2), process_index);
+ addr_pointed1 = snapshot1->read(remote((void**)real_area1));
+ addr_pointed2 = snapshot2->read(remote((void**)real_area2));
return (addr_pointed1 != addr_pointed2);
}
pointer_level++;
if (pointer_level <= 1) {
- addr_pointed1 = snapshot1->read(remote((void**)real_area1), process_index);
- addr_pointed2 = snapshot2->read(remote((void**)real_area2), process_index);
+ addr_pointed1 = snapshot1->read(remote((void**)real_area1));
+ addr_pointed2 = snapshot2->read(remote((void**)real_area2));
if (addr_pointed1 > state.std_heap_copy.heapbase && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1) &&
addr_pointed2 > state.std_heap_copy.heapbase && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2))
- return compare_heap_area(state, process_index, addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous,
- type->subtype, pointer_level);
+ return compare_heap_area(state, addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous, type->subtype,
+ pointer_level);
else
return (addr_pointed1 != addr_pointed2);
}
for (size_t i = 0; i < (area_size / sizeof(void*)); i++) {
- addr_pointed1 = snapshot1->read(remote((void**)((char*)real_area1 + i * sizeof(void*))), process_index);
- addr_pointed2 = snapshot2->read(remote((void**)((char*)real_area2 + i * sizeof(void*))), process_index);
+ addr_pointed1 = snapshot1->read(remote((void**)((char*)real_area1 + i * sizeof(void*))));
+ addr_pointed2 = snapshot2->read(remote((void**)((char*)real_area2 + i * sizeof(void*))));
int res;
if (addr_pointed1 > state.std_heap_copy.heapbase && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1) &&
addr_pointed2 > state.std_heap_copy.heapbase && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2))
- res = compare_heap_area(state, process_index, addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous,
- type->subtype, pointer_level);
+ res = compare_heap_area(state, addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous, type->subtype,
+ pointer_level);
else
res = (addr_pointed1 != addr_pointed2);
if (res == 1)
if (area_size <= type->byte_size || area_size % type->byte_size != 0)
return -1;
for (size_t i = 0; i < (size_t)(area_size / type->byte_size); i++) {
- int res = compare_heap_area_with_type(state, process_index, (char*)real_area1 + i * type->byte_size,
+ int res = compare_heap_area_with_type(state, (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)
} else {
for (simgrid::mc::Member& member : type->members) {
// TODO, optimize this? (for the offset case)
- void* real_member1 = simgrid::dwarf::resolve_member(real_area1, type, &member,
- (simgrid::mc::AddressSpace*)snapshot1, process_index);
- void* real_member2 = simgrid::dwarf::resolve_member(real_area2, type, &member,
- (simgrid::mc::AddressSpace*)snapshot2, process_index);
- int res = compare_heap_area_with_type(state, process_index, real_member1, real_member2, snapshot1,
- snapshot2, previous, member.type, -1, check_ignore, 0);
+ void* real_member1 =
+ simgrid::dwarf::resolve_member(real_area1, type, &member, (simgrid::mc::AddressSpace*)snapshot1);
+ void* real_member2 =
+ simgrid::dwarf::resolve_member(real_area2, type, &member, (simgrid::mc::AddressSpace*)snapshot2);
+ int res = compare_heap_area_with_type(state, real_member1, real_member2, snapshot1, snapshot2, previous,
+ member.type, -1, check_ignore, 0);
if (res == 1)
return res;
}
return 0;
case DW_TAG_union_type:
- return compare_heap_area_without_type(state, process_index, real_area1, real_area2, snapshot1, snapshot2,
- previous, type->byte_size, check_ignore);
+ return compare_heap_area_without_type(state, real_area1, real_area2, snapshot1, snapshot2, previous,
+ type->byte_size, check_ignore);
default:
return 0;
* @param area_size
* @return DWARF type ID for given offset
*/
-static simgrid::mc::Type* get_offset_type(void *real_base_address, simgrid::mc::Type* type,
- int offset, int area_size,
- simgrid::mc::Snapshot* snapshot, int process_index)
+static simgrid::mc::Type* get_offset_type(void* real_base_address, simgrid::mc::Type* type, int offset, int area_size,
+ simgrid::mc::Snapshot* snapshot)
{
// Beginning of the block, the infered variable type if the type of the block:
if (member.offset() == offset)
return member.type;
} else {
- void* real_member = simgrid::dwarf::resolve_member(real_base_address, type, &member, snapshot, process_index);
+ void* real_member = simgrid::dwarf::resolve_member(real_base_address, type, &member, snapshot);
if ((char*)real_member - (char*)real_base_address == offset)
return member.type;
}
* @param pointer_level
* @return 0 (same), 1 (different), -1
*/
-static
-int compare_heap_area(simgrid::mc::StateComparator& state, int process_index,
- const void *area1, const void *area2,
- simgrid::mc::Snapshot* snapshot1,
- simgrid::mc::Snapshot* snapshot2,
- HeapLocationPairs* previous,
- simgrid::mc::Type* type, int pointer_level)
+static int compare_heap_area(simgrid::mc::StateComparator& state, const void* area1, const void* area2,
+ simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot* snapshot2,
+ HeapLocationPairs* previous, simgrid::mc::Type* type, int pointer_level)
{
simgrid::mc::RemoteClient* process = &mc_model_checker->process();
// This is the address of std_heap->heapinfo in the application process:
void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo;
- const malloc_info* heapinfos1 = snapshot1->read(remote((const malloc_info**)heapinfo_address), process_index);
- const malloc_info* heapinfos2 = snapshot2->read(remote((const malloc_info**)heapinfo_address), process_index);
+ const malloc_info* heapinfos1 = snapshot1->read(remote((const malloc_info**)heapinfo_address));
+ const malloc_info* heapinfos2 = snapshot2->read(remote((const malloc_info**)heapinfo_address));
malloc_info heapinfo_temp1;
malloc_info heapinfo_temp2;
}
- simgrid::mc::RegionSnapshot* heap_region1 = MC_get_heap_region(snapshot1);
- simgrid::mc::RegionSnapshot* heap_region2 = MC_get_heap_region(snapshot2);
+ simgrid::mc::Region* heap_region1 = MC_get_heap_region(snapshot1);
+ simgrid::mc::Region* heap_region2 = MC_get_heap_region(snapshot2);
- const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(
- heap_region1, &heapinfo_temp1, &heapinfos1[block1], sizeof(malloc_info));
- const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(
- heap_region2, &heapinfo_temp2, &heapinfos2[block2], sizeof(malloc_info));
+ const malloc_info* heapinfo1 =
+ (const malloc_info*)heap_region1->read(&heapinfo_temp1, &heapinfos1[block1], sizeof(malloc_info));
+ const malloc_info* heapinfo2 =
+ (const malloc_info*)heap_region2->read(&heapinfo_temp2, &heapinfos2[block2], sizeof(malloc_info));
if ((heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type==MMALLOC_TYPE_HEAPINFO)
&& (heapinfo2->type == MMALLOC_TYPE_FREE || heapinfo2->type ==MMALLOC_TYPE_HEAPINFO)) {
offset2 = (char*)area2 - (char*)real_addr_frag2;
if (state.types1_(block1, frag1) != nullptr && state.types2_(block2, frag2) != nullptr) {
- new_type1 =
- get_offset_type(real_addr_frag1, state.types1_(block1, frag1), offset1, size, snapshot1, process_index);
- new_type2 =
- get_offset_type(real_addr_frag2, state.types2_(block2, frag2), offset1, size, snapshot2, process_index);
+ new_type1 = get_offset_type(real_addr_frag1, state.types1_(block1, frag1), offset1, size, snapshot1);
+ new_type2 = get_offset_type(real_addr_frag2, state.types2_(block2, frag2), offset1, size, snapshot2);
} else if (state.types1_(block1, frag1) != nullptr) {
- new_type1 =
- get_offset_type(real_addr_frag1, state.types1_(block1, frag1), offset1, size, snapshot1, process_index);
- new_type2 =
- get_offset_type(real_addr_frag2, state.types1_(block1, frag1), offset2, size, snapshot2, process_index);
+ new_type1 = get_offset_type(real_addr_frag1, state.types1_(block1, frag1), offset1, size, snapshot1);
+ new_type2 = get_offset_type(real_addr_frag2, state.types1_(block1, frag1), offset2, size, snapshot2);
} else if (state.types2_(block2, frag2) != nullptr) {
- new_type1 =
- get_offset_type(real_addr_frag1, state.types2_(block2, frag2), offset1, size, snapshot1, process_index);
- new_type2 =
- get_offset_type(real_addr_frag2, state.types2_(block2, frag2), offset2, size, snapshot2, process_index);
+ new_type1 = get_offset_type(real_addr_frag1, state.types2_(block2, frag2), offset1, size, snapshot1);
+ new_type2 = get_offset_type(real_addr_frag2, state.types2_(block2, frag2), offset2, size, snapshot2);
} else {
if (match_pairs)
state.match_equals(previous);
/* Start comparison */
int res_compare;
if (type)
- res_compare = compare_heap_area_with_type(state, process_index, area1, area2, snapshot1, snapshot2, previous, type,
- size, check_ignore, pointer_level);
+ res_compare = 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, process_index, area1, area2, snapshot1, snapshot2, previous,
- size, check_ignore);
+ res_compare =
+ compare_heap_area_without_type(state, area1, area2, snapshot1, snapshot2, previous, size, check_ignore);
if (res_compare == 1)
return res_compare;
/************************** Snapshot comparison *******************************/
/******************************************************************************/
-static int compare_areas_with_type(simgrid::mc::StateComparator& state, int process_index, void* real_area1,
- simgrid::mc::Snapshot* snapshot1, simgrid::mc::RegionSnapshot* region1,
- void* real_area2, simgrid::mc::Snapshot* snapshot2,
- simgrid::mc::RegionSnapshot* region2, simgrid::mc::Type* type, int pointer_level)
+static int compare_areas_with_type(simgrid::mc::StateComparator& state, void* real_area1,
+ simgrid::mc::Snapshot* snapshot1, simgrid::mc::Region* region1, void* real_area2,
+ simgrid::mc::Snapshot* snapshot2, simgrid::mc::Region* region2,
+ simgrid::mc::Type* type, int pointer_level)
{
simgrid::mc::RemoteClient* process = &mc_model_checker->process();
}
for (i = 0; i < type->element_count; i++) {
size_t off = i * elm_size;
- res = compare_areas_with_type(state, process_index, (char*)real_area1 + off, snapshot1, region1,
- (char*)real_area2 + off, snapshot2, region2, type->subtype, pointer_level);
+ res = compare_areas_with_type(state, (char*)real_area1 + off, snapshot1, region1, (char*)real_area2 + off,
+ snapshot2, region2, type->subtype, pointer_level);
if (res == 1)
return res;
}
if (not(addr_pointed2 > process->heap_address && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2)))
return 1;
// The pointers are both in the heap:
- return simgrid::mc::compare_heap_area(state, process_index, addr_pointed1, addr_pointed2, snapshot1,
- snapshot2, nullptr, type->subtype, pointer_level);
+ return simgrid::mc::compare_heap_area(state, addr_pointed1, addr_pointed2, snapshot1, snapshot2, nullptr,
+ type->subtype, pointer_level);
} else if (region1->contain(simgrid::mc::remote(addr_pointed1))) {
// The pointers are both in the current object R/W segment:
if (not type->type_id)
return (addr_pointed1 != addr_pointed2);
else
- return compare_areas_with_type(state, process_index, addr_pointed1, snapshot1, region1, addr_pointed2,
- snapshot2, region2, type->subtype, pointer_level);
+ return compare_areas_with_type(state, addr_pointed1, snapshot1, region1, addr_pointed2, snapshot2, region2,
+ type->subtype, pointer_level);
} else {
// TODO, We do not handle very well the case where
case DW_TAG_structure_type:
case DW_TAG_class_type:
for (simgrid::mc::Member& member : type->members) {
- void* member1 = simgrid::dwarf::resolve_member(real_area1, type, &member, snapshot1, process_index);
- void* member2 = simgrid::dwarf::resolve_member(real_area2, type, &member, snapshot2, process_index);
- simgrid::mc::RegionSnapshot* subregion1 = mc_get_region_hinted(member1, snapshot1, process_index, region1);
- simgrid::mc::RegionSnapshot* subregion2 = mc_get_region_hinted(member2, snapshot2, process_index, region2);
- res = compare_areas_with_type(state, process_index, member1, snapshot1, subregion1, member2, snapshot2,
- subregion2, member.type, pointer_level);
+ void* member1 = simgrid::dwarf::resolve_member(real_area1, type, &member, snapshot1);
+ void* member2 = simgrid::dwarf::resolve_member(real_area2, type, &member, snapshot2);
+ simgrid::mc::Region* subregion1 = snapshot1->get_region(member1, region1); // region1 is hinted
+ simgrid::mc::Region* subregion2 = snapshot2->get_region(member2, region2); // region2 is hinted
+ res = compare_areas_with_type(state, member1, snapshot1, subregion1, member2, snapshot2, subregion2,
+ member.type, pointer_level);
if (res == 1)
return res;
}
}
static int compare_global_variables(simgrid::mc::StateComparator& state, simgrid::mc::ObjectInformation* object_info,
- int process_index, simgrid::mc::RegionSnapshot* r1, simgrid::mc::RegionSnapshot* r2,
- simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot* snapshot2)
+ simgrid::mc::Region* r1, simgrid::mc::Region* r2, simgrid::mc::Snapshot* snapshot1,
+ simgrid::mc::Snapshot* snapshot2)
{
xbt_assert(r1 && r2, "Missing region.");
-#if HAVE_SMPI
- if (r1->storage_type() == simgrid::mc::StorageType::Privatized) {
- xbt_assert(process_index >= 0);
- if (r2->storage_type() != simgrid::mc::StorageType::Privatized)
- return 1;
-
- size_t process_count = MC_smpi_process_count();
- xbt_assert(process_count == r1->privatized_data().size()
- && process_count == r2->privatized_data().size());
-
- // Compare the global variables separately for each simulates process:
- for (size_t i = 0; i < process_count; i++) {
- if (compare_global_variables(state, object_info, i, &r1->privatized_data()[i], &r2->privatized_data()[i],
- snapshot1, snapshot2))
- return 1;
- }
- return 0;
- }
-#else
- xbt_assert(r1->storage_type() != simgrid::mc::StorageType::Privatized);
-#endif
- xbt_assert(r2->storage_type() != simgrid::mc::StorageType::Privatized);
-
std::vector<simgrid::mc::Variable>& variables = object_info->global_variables;
for (simgrid::mc::Variable const& current_var : variables) {
continue;
simgrid::mc::Type* bvariable_type = current_var.type;
- int res = compare_areas_with_type(state, process_index,
- (char *) current_var.address, snapshot1, r1,
- (char *) current_var.address, snapshot2, r2,
- bvariable_type, 0);
+ int res = compare_areas_with_type(state, (char*)current_var.address, snapshot1, r1, (char*)current_var.address,
+ snapshot2, r2, bvariable_type, 0);
if (res == 1) {
XBT_VERB("Global variable %s (%p) is different between snapshots",
current_var.name.c_str(),
}
static int compare_local_variables(simgrid::mc::StateComparator& state,
- int process_index,
simgrid::mc::Snapshot* snapshot1,
simgrid::mc::Snapshot* snapshot2,
mc_snapshot_stack_t stack1,
// TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
simgrid::mc::Type* subtype = current_var1->type;
- int res = compare_areas_with_type(
- state, process_index, current_var1->address, snapshot1,
- mc_get_snapshot_region(current_var1->address, snapshot1, process_index), current_var2->address, snapshot2,
- mc_get_snapshot_region(current_var2->address, snapshot2, process_index), subtype, 0);
+ int res = compare_areas_with_type(state, current_var1->address, snapshot1,
+ snapshot1->get_region(current_var1->address), current_var2->address,
+ snapshot2, snapshot2->get_region(current_var2->address), subtype, 0);
if (res == 1) {
// TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
static std::unique_ptr<simgrid::mc::StateComparator> state_comparator;
-int snapshot_compare(int num1, Snapshot* s1, int num2, Snapshot* s2)
+int snapshot_compare(Snapshot* s1, Snapshot* s2)
{
// TODO, make this a field of ModelChecker or something similar
-
if (state_comparator == nullptr)
state_comparator.reset(new StateComparator());
else
RemoteClient* process = &mc_model_checker->process();
- int errors = 0;
-
- int hash_result = 0;
if (_sg_mc_hash) {
- hash_result = (s1->hash != s2->hash);
- if (hash_result) {
- XBT_VERB("(%d - %d) Different hash: 0x%" PRIx64 "--0x%" PRIx64, num1, num2, s1->hash, s2->hash);
-#ifndef MC_DEBUG
+ if (s1->hash_ != s2->hash_) {
+ XBT_VERB("(%d - %d) Different hash: 0x%" PRIx64 "--0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_,
+ s2->hash_);
return 1;
-#endif
} else
- XBT_VERB("(%d - %d) Same hash: 0x%" PRIx64, num1, num2, s1->hash);
+ XBT_VERB("(%d - %d) Same hash: 0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_);
}
/* Compare enabled processes */
- if (s1->enabled_processes != s2->enabled_processes) {
- XBT_VERB("(%d - %d) Different amount of enabled processes", num1, num2);
+ if (s1->enabled_processes_ != s2->enabled_processes_) {
+ XBT_VERB("(%d - %d) Different amount of enabled processes", s1->num_state_, s2->num_state_);
return 1;
}
/* Compare size of stacks */
int is_diff = 0;
- for (unsigned long i = 0; i < s1->stacks.size(); i++) {
- size_t size_used1 = s1->stack_sizes[i];
- size_t size_used2 = s2->stack_sizes[i];
+ for (unsigned long i = 0; i < s1->stacks_.size(); i++) {
+ size_t size_used1 = s1->stack_sizes_[i];
+ size_t size_used2 = s2->stack_sizes_[i];
if (size_used1 != size_used2) {
-#ifdef MC_DEBUG
- XBT_DEBUG("(%d - %d) Different size used in stacks: %zu - %zu", num1, num2, size_used1, size_used2);
- errors++;
- is_diff = 1;
-#else
-#ifdef MC_VERBOSE
- XBT_VERB("(%d - %d) Different size used in stacks: %zu - %zu", num1, num2, size_used1, size_used2);
-#endif
+ XBT_VERB("(%d - %d) Different size used in stacks: %zu - %zu", s1->num_state_, s2->num_state_, size_used1,
+ size_used2);
return 1;
-#endif
}
}
if (is_diff) // do not proceed if there is any stacks that don't match
return 1;
/* Init heap information used in heap comparison algorithm */
- xbt_mheap_t heap1 = (xbt_mheap_t)s1->read_bytes(
- alloca(sizeof(struct mdesc)), sizeof(struct mdesc),
- remote(process->heap_address),
- simgrid::mc::ProcessIndexMissing, simgrid::mc::ReadOptions::lazy());
- xbt_mheap_t heap2 = (xbt_mheap_t)s2->read_bytes(
- alloca(sizeof(struct mdesc)), sizeof(struct mdesc),
- remote(process->heap_address),
- simgrid::mc::ProcessIndexMissing, simgrid::mc::ReadOptions::lazy());
- int res_init = state_comparator->initHeapInformation(heap1, heap2, &s1->to_ignore, &s2->to_ignore);
+ xbt_mheap_t heap1 = (xbt_mheap_t)s1->read_bytes(alloca(sizeof(struct mdesc)), sizeof(struct mdesc),
+ remote(process->heap_address), simgrid::mc::ReadOptions::lazy());
+ xbt_mheap_t heap2 = (xbt_mheap_t)s2->read_bytes(alloca(sizeof(struct mdesc)), sizeof(struct mdesc),
+ remote(process->heap_address), simgrid::mc::ReadOptions::lazy());
+ int res_init = state_comparator->initHeapInformation(heap1, heap2, &s1->to_ignore_, &s2->to_ignore_);
if (res_init == -1) {
-#ifdef MC_DEBUG
- XBT_DEBUG("(%d - %d) Different heap information", num1, num2);
- errors++;
-#else
-#ifdef MC_VERBOSE
- XBT_VERB("(%d - %d) Different heap information", num1, num2);
-#endif
-
+ XBT_VERB("(%d - %d) Different heap information", s1->num_state_, s2->num_state_);
return 1;
-#endif
}
/* Stacks comparison */
- int diff_local = 0;
- for (unsigned int cursor = 0; cursor < s1->stacks.size(); cursor++) {
- mc_snapshot_stack_t stack1 = &s1->stacks[cursor];
- mc_snapshot_stack_t stack2 = &s2->stacks[cursor];
-
- if (stack1->process_index != stack2->process_index) {
- diff_local = 1;
- XBT_DEBUG("(%d - %d) Stacks with different process index (%i vs %i)", num1, num2,
- stack1->process_index, stack2->process_index);
- }
- else diff_local = compare_local_variables(*state_comparator,
- stack1->process_index, s1, s2, stack1, stack2);
- if (diff_local > 0) {
-#ifdef MC_DEBUG
- XBT_DEBUG("(%d - %d) Different local variables between stacks %d", num1,
- num2, cursor + 1);
- errors++;
-#else
-
-#ifdef MC_VERBOSE
- XBT_VERB("(%d - %d) Different local variables between stacks %u", num1, num2, cursor + 1);
-#endif
+ // int diff_local = 0;
+ for (unsigned int cursor = 0; cursor < s1->stacks_.size(); cursor++) {
+ mc_snapshot_stack_t stack1 = &s1->stacks_[cursor];
+ mc_snapshot_stack_t stack2 = &s2->stacks_[cursor];
+ if (compare_local_variables(*state_comparator, s1, s2, stack1, stack2) > 0) {
+ XBT_VERB("(%d - %d) Different local variables between stacks %u", s1->num_state_, s2->num_state_, cursor + 1);
return 1;
-#endif
}
}
- size_t regions_count = s1->snapshot_regions.size();
+ size_t regions_count = s1->snapshot_regions_.size();
// TODO, raise a difference instead?
- xbt_assert(regions_count == s2->snapshot_regions.size());
+ xbt_assert(regions_count == s2->snapshot_regions_.size());
for (size_t k = 0; k != regions_count; ++k) {
- RegionSnapshot* region1 = s1->snapshot_regions[k].get();
- RegionSnapshot* region2 = s2->snapshot_regions[k].get();
+ Region* region1 = s1->snapshot_regions_[k].get();
+ Region* region2 = s2->snapshot_regions_[k].get();
// Preconditions:
if (region1->region_type() != RegionType::Data)
xbt_assert(region1->object_info() == region2->object_info());
xbt_assert(region1->object_info());
- std::string const& name = region1->object_info()->file_name;
-
/* Compare global variables */
- if (compare_global_variables(*state_comparator, region1->object_info(), simgrid::mc::ProcessIndexDisabled, region1,
- region2, s1, s2)) {
-
-#ifdef MC_DEBUG
- XBT_DEBUG("(%d - %d) Different global variables in %s",
- num1, num2, name.c_str());
- errors++;
-#else
-#ifdef MC_VERBOSE
- XBT_VERB("(%d - %d) Different global variables in %s",
- num1, num2, name.c_str());
-#endif
-
+ if (compare_global_variables(*state_comparator, region1->object_info(), region1, region2, s1, s2)) {
+ std::string const& name = region1->object_info()->file_name;
+ XBT_VERB("(%d - %d) Different global variables in %s", s1->num_state_, s2->num_state_, name.c_str());
return 1;
-#endif
}
}
/* Compare heap */
if (mmalloc_compare_heap(*state_comparator, s1, s2) > 0) {
-
-#ifdef MC_DEBUG
- XBT_DEBUG("(%d - %d) Different heap (mmalloc_compare)", num1, num2);
- errors++;
-#else
-
-#ifdef MC_VERBOSE
- XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", num1, num2);
-#endif
+ XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", s1->num_state_, s2->num_state_);
return 1;
-#endif
}
-#ifdef MC_VERBOSE
- if (errors || hash_result)
- XBT_VERB("(%d - %d) Difference found", num1, num2);
- else
- XBT_VERB("(%d - %d) No difference found", num1, num2);
-#endif
-
-#if defined(MC_DEBUG) && defined(MC_VERBOSE)
- if (_sg_mc_hash) {
- // * false positive SHOULD be avoided.
- // * There MUST not be any false negative.
+ XBT_VERB("(%d - %d) No difference found", s1->num_state_, s2->num_state_);
- XBT_VERB("(%d - %d) State equality hash test is %s %s", num1, num2,
- (hash_result != 0) == (errors != 0) ? "true" : "false", not hash_result ? "positive" : "negative");
- }
-#endif
-
- return errors > 0 || hash_result;
+ return 0;
}
}
