typedef std::array<HeapLocation, 2> HeapLocationPair;
typedef std::set<HeapLocationPair> HeapLocationPairs;
-struct ProcessComparisonState;
-struct StateComparator;
-
-static inline
-HeapLocationPair makeHeapLocationPair(int block1, int fragment1, int block2, int fragment2)
-{
- return HeapLocationPair{{HeapLocation(block1, fragment1), HeapLocation(block2, fragment2)}};
-}
-
class HeapArea : public HeapLocation {
public:
bool valid_ = false;
void initHeapInformation(xbt_mheap_t heap, std::vector<simgrid::mc::IgnoredHeapRegion>* i);
};
-static bool heap_area_differ(StateComparator& state, const void* area1, const void* area2, Snapshot* snapshot1,
- Snapshot* snapshot2, HeapLocationPairs* previous, Type* type, int pointer_level);
-
class StateComparator {
public:
s_xbt_mheap_t std_heap_copy;
std::vector<simgrid::mc::IgnoredHeapRegion>* i1,
std::vector<simgrid::mc::IgnoredHeapRegion>* i2);
- HeapArea& equals_to1_(std::size_t i, std::size_t j)
+ template <int rank> HeapArea& equals_to_(std::size_t i, std::size_t j)
{
- return processStates[0].equals_to[ MAX_FRAGMENT_PER_BLOCK * i + j];
+ return processStates[rank - 1].equals_to[MAX_FRAGMENT_PER_BLOCK * i + j];
}
- HeapArea& equals_to2_(std::size_t i, std::size_t j)
+ template <int rank> Type*& types_(std::size_t i, std::size_t j)
{
- return processStates[1].equals_to[ MAX_FRAGMENT_PER_BLOCK * i + j];
- }
- Type*& types1_(std::size_t i, std::size_t j)
- {
- return processStates[0].types[ MAX_FRAGMENT_PER_BLOCK * i + j];
- }
- Type*& types2_(std::size_t i, std::size_t j)
- {
- return processStates[1].types[ MAX_FRAGMENT_PER_BLOCK * i + j];
+ return processStates[rank - 1].types[MAX_FRAGMENT_PER_BLOCK * i + j];
}
- HeapArea const& equals_to1_(std::size_t i, std::size_t j) const
- {
- return processStates[0].equals_to[ MAX_FRAGMENT_PER_BLOCK * i + j];
- }
- HeapArea const& equals_to2_(std::size_t i, std::size_t j) const
- {
- return processStates[1].equals_to[ MAX_FRAGMENT_PER_BLOCK * i + j];
- }
- Type* const& types1_(std::size_t i, std::size_t j) const
+ template <int rank> HeapArea const& equals_to_(std::size_t i, std::size_t j) const
{
- return processStates[0].types[ MAX_FRAGMENT_PER_BLOCK * i + j];
+ return processStates[rank - 1].equals_to[MAX_FRAGMENT_PER_BLOCK * i + j];
}
- Type* const& types2_(std::size_t i, std::size_t j) const
+ template <int rank> Type* const& types_(std::size_t i, std::size_t j) const
{
- return processStates[1].types[ MAX_FRAGMENT_PER_BLOCK * i + j];
+ return processStates[rank - 1].types[MAX_FRAGMENT_PER_BLOCK * i + j];
}
/** Check whether two blocks are known to be matching
*/
bool blocksEqual(int b1, int b2) const
{
- return this->equals_to1_(b1, 0).block_ == b2 && this->equals_to2_(b2, 0).block_ == b1;
+ return this->equals_to_<1>(b1, 0).block_ == b2 && this->equals_to_<2>(b2, 0).block_ == b1;
}
/** Check whether two fragments are known to be matching
*/
int fragmentsEqual(int b1, int f1, int b2, int f2) const
{
- return this->equals_to1_(b1, f1).block_ == b2 && this->equals_to1_(b1, f1).fragment_ == f2 &&
- this->equals_to2_(b2, f2).block_ == b1 && this->equals_to2_(b2, f2).fragment_ == f1;
+ return this->equals_to_<1>(b1, f1).block_ == b2 && this->equals_to_<1>(b1, f1).fragment_ == f2 &&
+ this->equals_to_<2>(b2, f2).block_ == b1 && this->equals_to_<2>(b2, f2).fragment_ == f1;
}
void match_equals(HeapLocationPairs* list);
{
for (auto const& pair : *list) {
if (pair[0].fragment_ != -1) {
- this->equals_to1_(pair[0].block_, pair[0].fragment_) = simgrid::mc::HeapArea(pair[1].block_, pair[1].fragment_);
- this->equals_to2_(pair[1].block_, pair[1].fragment_) = simgrid::mc::HeapArea(pair[0].block_, pair[0].fragment_);
+ this->equals_to_<1>(pair[0].block_, pair[0].fragment_) = simgrid::mc::HeapArea(pair[1].block_, pair[1].fragment_);
+ this->equals_to_<2>(pair[1].block_, pair[1].fragment_) = simgrid::mc::HeapArea(pair[0].block_, pair[0].fragment_);
} else {
- this->equals_to1_(pair[0].block_, 0) = simgrid::mc::HeapArea(pair[1].block_, pair[1].fragment_);
- this->equals_to2_(pair[1].block_, 0) = simgrid::mc::HeapArea(pair[0].block_, pair[0].fragment_);
+ this->equals_to_<1>(pair[0].block_, 0) = simgrid::mc::HeapArea(pair[1].block_, pair[1].fragment_);
+ this->equals_to_<2>(pair[1].block_, 0) = simgrid::mc::HeapArea(pair[0].block_, pair[0].fragment_);
}
}
}
xbt_die("No heap region");
}
+static bool heap_area_differ(StateComparator& state, const void* area1, const void* area2, Snapshot* snapshot1,
+ Snapshot* snapshot2, HeapLocationPairs* previous, Type* type, int pointer_level);
+
static bool mmalloc_heap_differ(simgrid::mc::StateComparator& state, simgrid::mc::Snapshot* snapshot1,
simgrid::mc::Snapshot* snapshot2)
{
- simgrid::mc::RemoteClient* process = &mc_model_checker->process();
+ const simgrid::mc::RemoteClient& process = mc_model_checker->process();
/* Check busy blocks */
size_t i1 = 1;
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;
+ void* heapinfo_address = &((xbt_mheap_t)process.heap_address)->heapinfo;
// This is in snapshot do not use them directly:
const malloc_info* heapinfos1 =
if (is_stack(addr_block1)) {
for (size_t k = 0; k < heapinfo1->busy_block.size; k++)
- state.equals_to1_(i1 + k, 0) = HeapArea(i1, -1);
+ state.equals_to_<1>(i1 + k, 0) = HeapArea(i1, -1);
for (size_t k = 0; k < heapinfo2->busy_block.size; k++)
- state.equals_to2_(i1 + k, 0) = HeapArea(i1, -1);
+ state.equals_to_<2>(i1 + k, 0) = HeapArea(i1, -1);
i1 += heapinfo1->busy_block.size;
continue;
}
- if (state.equals_to1_(i1, 0).valid_) {
+ if (state.equals_to_<1>(i1, 0).valid_) {
i1++;
continue;
}
bool equal = false;
/* Try first to associate to same block in the other heap */
- if (heapinfo2->type == heapinfo1->type && state.equals_to2_(i1, 0).valid_ == 0) {
+ if (heapinfo2->type == heapinfo1->type && state.equals_to_<2>(i1, 0).valid_ == 0) {
void* addr_block2 = (ADDR2UINT(i1) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
if (not heap_area_differ(state, addr_block1, addr_block2, snapshot1, snapshot2, nullptr, nullptr, 0)) {
for (size_t k = 1; k < heapinfo2->busy_block.size; k++)
- state.equals_to2_(i1 + k, 0) = HeapArea(i1, -1);
+ state.equals_to_<2>(i1 + k, 0) = HeapArea(i1, -1);
for (size_t k = 1; k < heapinfo1->busy_block.size; k++)
- state.equals_to1_(i1 + k, 0) = HeapArea(i1, -1);
+ state.equals_to_<1>(i1 + k, 0) = HeapArea(i1, -1);
equal = true;
i1 += heapinfo1->busy_block.size;
}
continue;
}
- if (state.equals_to2_(i2, 0).valid_) {
+ if (state.equals_to_<2>(i2, 0).valid_) {
i2++;
continue;
}
if (not heap_area_differ(state, addr_block1, addr_block2, snapshot1, snapshot2, nullptr, nullptr, 0)) {
for (size_t k = 1; k < heapinfo2b->busy_block.size; k++)
- state.equals_to2_(i2 + k, 0) = HeapArea(i1, -1);
+ state.equals_to_<2>(i2 + k, 0) = HeapArea(i1, -1);
for (size_t k = 1; k < heapinfo1->busy_block.size; k++)
- state.equals_to1_(i1 + k, 0) = HeapArea(i2, -1);
+ state.equals_to_<1>(i1 + k, 0) = HeapArea(i2, -1);
equal = true;
i1 += heapinfo1->busy_block.size;
}
if (heapinfo1->busy_frag.frag_size[j1] == -1) /* Free fragment_ */
continue;
- if (state.equals_to1_(i1, j1).valid_)
+ if (state.equals_to_<1>(i1, j1).valid_)
continue;
void* addr_frag1 = (void*)((char*)addr_block1 + (j1 << heapinfo1->type));
bool equal = false;
/* Try first to associate to same fragment_ in the other heap */
- if (heapinfo2->type == heapinfo1->type && not state.equals_to2_(i1, j1).valid_) {
+ if (heapinfo2->type == heapinfo1->type && not state.equals_to_<2>(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));
if (not heap_area_differ(state, addr_frag1, addr_frag2, snapshot1, snapshot2, nullptr, nullptr, 0))
if (i2 == i1 && j2 == j1)
continue;
- if (state.equals_to2_(i2, j2).valid_)
+ if (state.equals_to_<2>(i2, j2).valid_)
continue;
void* addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
(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_) {
+ not state.equals_to_<1>(i, 0).valid_) {
XBT_DEBUG("Block %zu not found (size used = %zu)", i, heapinfo1->busy_block.busy_size);
return true;
}
if (heapinfo1->type <= 0)
continue;
for (size_t j = 0; j < (size_t)(BLOCKSIZE >> heapinfo1->type); j++)
- if (i1 == state.heaplimit && heapinfo1->busy_frag.frag_size[j] > 0 && not state.equals_to1_(i, j).valid_) {
+ if (i1 == state.heaplimit && heapinfo1->busy_frag.frag_size[j] > 0 && not state.equals_to_<1>(i, j).valid_) {
XBT_DEBUG("Block %zu, Fragment %zu not found (size used = %zd)", i, j, heapinfo1->busy_frag.frag_size[j]);
return true;
}
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_) {
+ not state.equals_to_<2>(i, 0).valid_) {
XBT_DEBUG("Block %zu not found (size used = %zu)", i,
heapinfo2->busy_block.busy_size);
return true;
continue;
for (size_t j = 0; j < (size_t)(BLOCKSIZE >> heapinfo2->type); j++)
- if (i1 == state.heaplimit && heapinfo2->busy_frag.frag_size[j] > 0 && not state.equals_to2_(i, j).valid_) {
+ if (i1 == state.heaplimit && heapinfo2->busy_frag.frag_size[j] > 0 && not state.equals_to_<2>(i, j).valid_) {
XBT_DEBUG("Block %zu, Fragment %zu not found (size used = %zd)",
i, j, heapinfo2->busy_frag.frag_size[j]);
return true;
simgrid::mc::Snapshot* snapshot2, HeapLocationPairs* previous, int size,
int check_ignore)
{
- simgrid::mc::RemoteClient* process = &mc_model_checker->process();
+ const simgrid::mc::RemoteClient& process = mc_model_checker->process();
simgrid::mc::Region* heap_region1 = MC_get_heap_region(snapshot1);
simgrid::mc::Region* heap_region2 = MC_get_heap_region(snapshot2);
const void* addr_pointed1 = snapshot1->read(remote((void**)((const char*)real_area1 + pointer_align)));
const void* addr_pointed2 = snapshot2->read(remote((void**)((const char*)real_area2 + pointer_align)));
- if (process->in_maestro_stack(remote(addr_pointed1))
- && process->in_maestro_stack(remote(addr_pointed2))) {
+ if (process.in_maestro_stack(remote(addr_pointed1)) && process.in_maestro_stack(remote(addr_pointed2))) {
i = pointer_align + sizeof(void *);
continue;
}
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();
+ const simgrid::mc::RemoteClient& process = mc_model_checker->process();
ssize_t block1;
ssize_t block2;
bool match_pairs = false;
// This is the address of std_heap->heapinfo in the application process:
- void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo;
+ void* heapinfo_address = &((xbt_mheap_t)process.heap_address)->heapinfo;
const malloc_info* heapinfos1 = snapshot1->read(remote((const malloc_info**)heapinfo_address));
const malloc_info* heapinfos2 = snapshot2->read(remote((const malloc_info**)heapinfo_address));
// If either block is a stack block:
if (is_block_stack((int) block1) && is_block_stack((int) block2)) {
- previous->insert(simgrid::mc::makeHeapLocationPair(block1, -1, block2, -1));
+ previous->insert(HeapLocationPair{{HeapLocation(block1, -1), HeapLocation(block2, -1)}});
if (match_pairs)
state.match_equals(previous);
return false;
// TODO, lookup variable type from block type as done for fragmented blocks
- if (state.equals_to1_(block1, 0).valid_ && state.equals_to2_(block2, 0).valid_ &&
+ if (state.equals_to_<1>(block1, 0).valid_ && state.equals_to_<2>(block2, 0).valid_ &&
state.blocksEqual(block1, block2)) {
if (match_pairs)
state.match_equals(previous);
heapinfo1->busy_block.busy_size != heapinfo2->busy_block.busy_size)
return true;
- if (not previous->insert(simgrid::mc::makeHeapLocationPair(block1, -1, block2, -1)).second) {
+ if (not previous->insert(HeapLocationPair{{HeapLocation(block1, -1), HeapLocation(block2, -1)}}).second) {
if (match_pairs)
state.match_equals(previous);
return false;
// Remember (basic) type inference.
// The current data structure only allows us to do this for the whole block.
if (type != nullptr && area1 == real_addr_block1)
- state.types1_(block1, 0) = type;
+ state.types_<1>(block1, 0) = type;
if (type != nullptr && area2 == real_addr_block2)
- state.types2_(block2, 0) = type;
+ state.types_<2>(block2, 0) = type;
if (size <= 0) {
if (match_pairs)
}
// Check if the blocks are already matched together:
- if (state.equals_to1_(block1, frag1).valid_ && state.equals_to2_(block2, frag2).valid_ && offset1 == offset2 &&
+ if (state.equals_to_<1>(block1, frag1).valid_ && state.equals_to_<2>(block2, frag2).valid_ && offset1 == offset2 &&
state.fragmentsEqual(block1, frag1, block2, frag2)) {
if (match_pairs)
state.match_equals(previous);
// Remember (basic) type inference.
// The current data structure only allows us to do this for the whole fragment_.
if (type != nullptr && area1 == real_addr_frag1)
- state.types1_(block1, frag1) = type;
+ state.types_<1>(block1, frag1) = type;
if (type != nullptr && area2 == real_addr_frag2)
- state.types2_(block2, frag2) = type;
+ state.types_<2>(block2, frag2) = type;
// The type of the variable is already known:
if (type) {
new_type1 = new_type2 = type;
}
// Type inference from the block type.
- else if (state.types1_(block1, frag1) != nullptr || state.types2_(block2, frag2) != nullptr) {
+ else if (state.types_<1>(block1, frag1) != nullptr || state.types_<2>(block2, frag2) != nullptr) {
offset1 = (char*)area1 - (char*)real_addr_frag1;
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);
- 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);
- 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);
- new_type2 = get_offset_type(real_addr_frag2, state.types2_(block2, frag2), offset2, size, snapshot2);
+ if (state.types_<1>(block1, frag1) != nullptr && state.types_<2>(block2, frag2) != nullptr) {
+ new_type1 = get_offset_type(real_addr_frag1, state.types_<1>(block1, frag1), offset1, size, snapshot1);
+ new_type2 = get_offset_type(real_addr_frag2, state.types_<2>(block2, frag2), offset1, size, snapshot2);
+ } else if (state.types_<1>(block1, frag1) != nullptr) {
+ new_type1 = get_offset_type(real_addr_frag1, state.types_<1>(block1, frag1), offset1, size, snapshot1);
+ new_type2 = get_offset_type(real_addr_frag2, state.types_<1>(block1, frag1), offset2, size, snapshot2);
+ } else if (state.types_<2>(block2, frag2) != nullptr) {
+ new_type1 = get_offset_type(real_addr_frag1, state.types_<2>(block2, frag2), offset1, size, snapshot1);
+ new_type2 = get_offset_type(real_addr_frag2, state.types_<2>(block2, frag2), offset2, size, snapshot2);
} else {
if (match_pairs)
state.match_equals(previous);
}
if (offset1 == 0 && offset2 == 0 &&
- not previous->insert(simgrid::mc::makeHeapLocationPair(block1, frag1, block2, frag2)).second) {
+ not previous->insert(HeapLocationPair{{HeapLocation(block1, frag1), HeapLocation(block2, frag2)}}).second) {
if (match_pairs)
state.match_equals(previous);
return false;
namespace simgrid {
namespace mc {
-static std::unique_ptr<simgrid::mc::StateComparator> state_comparator;
-
bool snapshot_equal(Snapshot* s1, Snapshot* s2)
{
// TODO, make this a field of ModelChecker or something similar
- if (state_comparator == nullptr)
- state_comparator.reset(new StateComparator());
- else
- state_comparator->clear();
+ static StateComparator state_comparator;
- RemoteClient* process = &mc_model_checker->process();
+ const RemoteClient& process = mc_model_checker->process();
if (s1->hash_ != s2->hash_) {
XBT_VERB("(%d - %d) Different hash: 0x%" PRIx64 "--0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_,
/* 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::ReadOptions::lazy());
+ 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());
- if (state_comparator->initHeapInformation(heap1, heap2, &s1->to_ignore_, &s2->to_ignore_) == -1) {
+ remote(process.heap_address), simgrid::mc::ReadOptions::lazy());
+ if (state_comparator.initHeapInformation(heap1, heap2, &s1->to_ignore_, &s2->to_ignore_) == -1) {
XBT_VERB("(%d - %d) Different heap information", s1->num_state_, s2->num_state_);
return false;
}
mc_snapshot_stack_t stack1 = &s1->stacks_[cursor];
mc_snapshot_stack_t stack2 = &s2->stacks_[cursor];
- if (local_variables_differ(*state_comparator, s1, s2, stack1, stack2)) {
+ if (local_variables_differ(state_comparator, s1, s2, stack1, stack2)) {
XBT_VERB("(%d - %d) Different local variables between stacks %u", s1->num_state_, s2->num_state_, cursor + 1);
return false;
}
xbt_assert(region1->object_info());
/* Compare global variables */
- if (global_variables_differ(*state_comparator, region1->object_info(), region1, region2, s1, s2)) {
+ if (global_variables_differ(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 false;
}
/* Compare heap */
- if (mmalloc_heap_differ(*state_comparator, s1, s2)) {
+ if (mmalloc_heap_differ(state_comparator, s1, s2)) {
XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", s1->num_state_, s2->num_state_);
return false;
}
