xbt_die("No heap region");
}
-static
-int mmalloc_compare_heap(
- simgrid::mc::StateComparator& state, simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot* snapshot2)
+static bool mmalloc_heap_equal(simgrid::mc::StateComparator& state, simgrid::mc::Snapshot* snapshot1,
+ simgrid::mc::Snapshot* snapshot2)
{
simgrid::mc::RemoteClient* process = &mc_model_checker->process();
if (i1 == state.heaplimit)
XBT_DEBUG("Number of blocks/fragments not found in heap2: %d", nb_diff2);
- return nb_diff1 > 0 || nb_diff2 > 0;
+ return nb_diff1 == 0 && nb_diff2 == 0;
}
/**
simgrid::mc::Snapshot* snapshot2, HeapLocationPairs* previous,
simgrid::mc::Type* type, int area_size, int check_ignore, int pointer_level)
{
- do {
-
// HACK: This should not happen but in pratice, there are some
// DW_TAG_typedef without an associated DW_AT_type:
//<1><538832>: Abbrev Number: 111 (DW_TAG_typedef)
case DW_TAG_typedef:
case DW_TAG_const_type:
case DW_TAG_volatile_type:
- // Poor man's TCO:
- type = type->subtype;
- continue; // restart
+ return compare_heap_area_with_type(state, real_area1, real_area2, snapshot1, snapshot2, previous, type->subtype,
+ area_size, check_ignore, pointer_level);
case DW_TAG_array_type:
subtype = type->subtype;
case DW_TAG_union_type:
return compare_heap_area_without_type(state, real_area1, real_area2, snapshot1, snapshot2, previous,
type->byte_size, check_ignore);
-
- default:
- return 0;
}
-
- xbt_die("Unreachable");
- } while (true);
+ return 0;
}
/** Infer the type of a part of the block from the type of the block
int i;
int res;
- do {
xbt_assert(type != nullptr);
switch (type->type) {
case DW_TAG_unspecified_type:
case DW_TAG_typedef:
case DW_TAG_volatile_type:
case DW_TAG_const_type:
- // Poor man's TCO:
- type = type->subtype;
- continue; // restart
+ return compare_areas_with_type(state, real_area1, snapshot1, region1, real_area2, snapshot2, region2,
+ type->subtype, pointer_level);
case DW_TAG_array_type:
subtype = type->subtype;
switch (subtype->type) {
}
return 0;
- } while (true);
}
-static int compare_global_variables(simgrid::mc::StateComparator& state, simgrid::mc::ObjectInformation* object_info,
- simgrid::mc::Region* r1, simgrid::mc::Region* r2, simgrid::mc::Snapshot* snapshot1,
- simgrid::mc::Snapshot* snapshot2)
+static bool global_variables_equal(simgrid::mc::StateComparator& state, simgrid::mc::ObjectInformation* object_info,
+ simgrid::mc::Region* r1, simgrid::mc::Region* r2, simgrid::mc::Snapshot* snapshot1,
+ simgrid::mc::Snapshot* snapshot2)
{
xbt_assert(r1 && r2, "Missing region.");
XBT_VERB("Global variable %s (%p) is different between snapshots",
current_var.name.c_str(),
(char *) current_var.address);
- return 1;
+ return false;
}
}
- return 0;
+ return true;
}
-static int compare_local_variables(simgrid::mc::StateComparator& state,
- simgrid::mc::Snapshot* snapshot1,
- simgrid::mc::Snapshot* snapshot2,
- mc_snapshot_stack_t stack1,
- mc_snapshot_stack_t stack2)
+static bool local_variables_equal(simgrid::mc::StateComparator& state, simgrid::mc::Snapshot* snapshot1,
+ simgrid::mc::Snapshot* snapshot2, mc_snapshot_stack_t stack1,
+ mc_snapshot_stack_t stack2)
{
if (stack1->local_variables.size() != stack2->local_variables.size()) {
XBT_VERB("Different number of local variables");
- return 1;
+ return false;
}
- unsigned int cursor = 0;
- local_variable_t current_var1;
- local_variable_t current_var2;
- while (cursor < stack1->local_variables.size()) {
- current_var1 = &stack1->local_variables[cursor];
- current_var2 = &stack1->local_variables[cursor];
- if (current_var1->name != current_var2->name
- || current_var1->subprogram != current_var2->subprogram
- || current_var1->ip != current_var2->ip) {
- // TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
- XBT_VERB
- ("Different name of variable (%s - %s) "
- "or frame (%s - %s) or ip (%lu - %lu)",
- current_var1->name.c_str(),
- current_var2->name.c_str(),
- current_var1->subprogram->name.c_str(),
- current_var2->subprogram->name.c_str(),
- current_var1->ip, current_var2->ip);
- return 1;
- }
+ for (unsigned int cursor = 0; cursor < stack1->local_variables.size(); cursor++) {
+ local_variable_t current_var1 = &stack1->local_variables[cursor];
+ local_variable_t current_var2 = &stack2->local_variables[cursor];
+ if (current_var1->name != current_var2->name || current_var1->subprogram != current_var2->subprogram ||
+ current_var1->ip != current_var2->ip) {
// TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
+ XBT_VERB("Different name of variable (%s - %s) "
+ "or frame (%s - %s) or ip (%lu - %lu)",
+ current_var1->name.c_str(), current_var2->name.c_str(), current_var1->subprogram->name.c_str(),
+ current_var2->subprogram->name.c_str(), current_var1->ip, current_var2->ip);
+ return false;
+ }
+ // 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, 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
- XBT_VERB("Local variable %s (%p - %p) in frame %s "
- "is different between snapshots",
- current_var1->name.c_str(), current_var1->address, current_var2->address,
- current_var1->subprogram->name.c_str());
- return res;
- }
- cursor++;
+ if (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),
+ current_var1->type, 0) == 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.c_str(), current_var1->address, current_var2->address,
+ current_var1->subprogram->name.c_str());
+ return false;
}
- return 0;
+ }
+ return true;
}
namespace simgrid {
static std::unique_ptr<simgrid::mc::StateComparator> state_comparator;
-int snapshot_compare(Snapshot* s1, Snapshot* s2)
+bool snapshot_equal(Snapshot* s1, Snapshot* s2)
{
// TODO, make this a field of ModelChecker or something similar
if (state_comparator == nullptr)
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, s1->num_state_, s2->num_state_, s1->hash_,
- s2->hash_);
-#ifndef MC_DEBUG
- return 1;
-#endif
+ 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 false;
} else
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", s1->num_state_, s2->num_state_);
- return 1;
+ return false;
}
/* 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];
if (size_used1 != size_used2) {
-#ifdef MC_DEBUG
- XBT_DEBUG("(%d - %d) Different size used in stacks: %zu - %zu", s1->num_state, s2->num_state, size_used1,
- size_used2);
- errors++;
- is_diff = 1;
-#else
-#ifdef MC_VERBOSE
XBT_VERB("(%d - %d) Different size used in stacks: %zu - %zu", s1->num_state_, s2->num_state_, size_used1,
size_used2);
-#endif
- return 1;
-#endif
+ return false;
}
}
- 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),
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, nus1->num_state, s2->num_statem2);
- errors++;
-#else
-#ifdef MC_VERBOSE
XBT_VERB("(%d - %d) Different heap information", s1->num_state_, s2->num_state_);
-#endif
-
- return 1;
-#endif
+ return false;
}
/* 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 (compare_local_variables(*state_comparator, s1, s2, stack1, stack2) > 0) {
-#ifdef MC_DEBUG
- XBT_DEBUG("(%d - %d) Different local variables between stacks %d", num1,
- num2, cursor + 1);
- errors++;
-#else
-
-#ifdef MC_VERBOSE
+ if (not local_variables_equal(*state_comparator, s1, s2, stack1, stack2)) {
XBT_VERB("(%d - %d) Different local variables between stacks %u", s1->num_state_, s2->num_state_, cursor + 1);
-#endif
-
- return 1;
-#endif
+ return false;
}
}
size_t regions_count = s1->snapshot_regions_.size();
- // TODO, raise a difference instead?
- xbt_assert(regions_count == s2->snapshot_regions_.size());
+ if (regions_count != s2->snapshot_regions_.size())
+ return false;
for (size_t k = 0; k != regions_count; ++k) {
Region* region1 = s1->snapshot_regions_[k].get();
xbt_assert(region1->object_info());
/* Compare global variables */
- if (compare_global_variables(*state_comparator, region1->object_info(), region1, region2, s1, s2)) {
-
-#ifdef MC_DEBUG
- std::string const& name = region1->object_info()->file_name;
- XBT_DEBUG("(%d - %d) Different global variables in %s", s1->num_state, s2->num_state, name.c_str());
- errors++;
-#else
-#ifdef MC_VERBOSE
+ if (not global_variables_equal(*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());
-#endif
-
- return 1;
-#endif
+ return false;
}
}
/* Compare heap */
- if (mmalloc_compare_heap(*state_comparator, s1, s2) > 0) {
-
-#ifdef MC_DEBUG
- XBT_DEBUG("(%d - %d) Different heap (mmalloc_compare)", s1->num_state, s2->num_state);
- errors++;
-#else
-
-#ifdef MC_VERBOSE
+ if (not mmalloc_heap_equal(*state_comparator, s1, s2)) {
XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", s1->num_state_, s2->num_state_);
-#endif
- return 1;
-#endif
+ return false;
}
-#ifdef MC_VERBOSE
- if (errors || hash_result)
- XBT_VERB("(%d - %d) Difference found", s1->num_state_, s2->num_state_);
- else
XBT_VERB("(%d - %d) No difference found", s1->num_state_, s2->num_state_);
-#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) State equality hash test is %s %s", s1->num_state, s2->num_state,
- (hash_result != 0) == (errors != 0) ? "true" : "false", not hash_result ? "positive" : "negative");
- }
-#endif
- return errors > 0 || hash_result;
+ return true;
}
}
