using simgrid::mc::remote;
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
- "Logging specific to MC communication determinism detection");
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc, "Logging specific to MC communication determinism detection");
/********** Global variables **********/
/********** Static functions ***********/
-static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2)
+static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1,
+ simgrid::mc::PatternCommunication* comm2)
{
if(comm1->type != comm2->type)
return TYPE_DIFF;
return NONE_DIFF;
}
-static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, simgrid::mc::PatternCommunication* comm, unsigned int cursor) {
- char *type, *res;
+static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process,
+ simgrid::mc::PatternCommunication* comm, unsigned int cursor)
+{
+ char* type;
+ char* res;
if (comm->type == simgrid::mc::PatternCommunicationType::send)
type = bprintf("The send communications pattern of the process %d is different!", process - 1);
return res;
}
-static void update_comm_pattern(
- simgrid::mc::PatternCommunication* comm_pattern,
- simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr)
+static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern,
+ simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr)
{
// HACK, type punning
simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
comm_pattern->dst_host = MC_smx_actor_get_host_name(dst_proc);
if (comm_pattern->data.size() == 0 && comm->src_buff != nullptr) {
size_t buff_size;
- mc_model_checker->process().read(
- &buff_size, remote(comm->dst_buff_size));
+ mc_model_checker->process().read(&buff_size, remote(comm->dst_buff_size));
comm_pattern->data.resize(buff_size);
- mc_model_checker->process().read_bytes(
- comm_pattern->data.data(), comm_pattern->data.size(),
- remote(comm->src_buff));
+ mc_model_checker->process().read_bytes(comm_pattern->data.data(), comm_pattern->data.size(),
+ remote(comm->src_buff));
}
}
namespace simgrid {
namespace mc {
-void CommunicationDeterminismChecker::deterministic_comm_pattern(
- int process, simgrid::mc::PatternCommunication* comm, int backtracking)
+void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm,
+ int backtracking)
{
simgrid::mc::PatternCommunicationList* list =
xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
if(!backtracking){
- e_mc_comm_pattern_difference_t diff =
- compare_comm_pattern(list->list[list->index_comm].get(), comm);
+ e_mc_comm_pattern_difference_t diff = compare_comm_pattern(list->list[list->index_comm].get(), comm);
if (diff != NONE_DIFF) {
if (comm->type == simgrid::mc::PatternCommunicationType::send) {
/********** Non Static functions ***********/
-void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
+void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request,
+ e_mc_call_type_t call_type, int backtracking)
{
const smx_actor_t issuer = MC_smx_simcall_get_issuer(request);
- simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
- initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
- xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
- incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
+ simgrid::mc::PatternCommunicationList* initial_pattern =
+ xbt_dynar_get_as(initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
+ xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
std::unique_ptr<simgrid::mc::PatternCommunication> pattern =
- std::unique_ptr<simgrid::mc::PatternCommunication>(
- new simgrid::mc::PatternCommunication());
- pattern->index =
- initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
+ std::unique_ptr<simgrid::mc::PatternCommunication>(new simgrid::mc::PatternCommunication());
+ pattern->index = initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
if (call_type == MC_CALL_TYPE_SEND) {
/* Create comm pattern */
pattern->comm_addr = simcall_comm_isend__get__result(request);
simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_synchro;
- mc_model_checker->process().read(temp_synchro, remote(
- static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
- simgrid::kernel::activity::Comm* synchro =
- static_cast<simgrid::kernel::activity::Comm*>(temp_synchro.getBuffer());
+ mc_model_checker->process().read(temp_synchro,
+ remote(static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
+ simgrid::kernel::activity::Comm* synchro = static_cast<simgrid::kernel::activity::Comm*>(temp_synchro.getBuffer());
char* remote_name = mc_model_checker->process().read<char*>(
(std::uint64_t)(synchro->mbox ? &synchro->mbox->name_ : &synchro->mbox_cpy->name_));
pattern->src_host = MC_smx_actor_get_host_name(issuer);
simgrid::smpi::Request mpi_request =
- mc_model_checker->process().read<simgrid::smpi::Request>(
- (std::uint64_t) simcall_comm_isend__get__data(request));
+ mc_model_checker->process().read<simgrid::smpi::Request>((std::uint64_t)simcall_comm_isend__get__data(request));
pattern->tag = mpi_request.tag();
- if (synchro->src_buff != nullptr){
+ if (synchro->src_buff != nullptr) {
pattern->data.resize(synchro->src_buff_size);
- mc_model_checker->process().read_bytes(
- pattern->data.data(), pattern->data.size(),
- remote(synchro->src_buff));
+ mc_model_checker->process().read_bytes(pattern->data.data(), pattern->data.size(), remote(synchro->src_buff));
}
if(mpi_request.detached()){
if (!this->initial_communications_pattern_done) {
/* Store comm pattern */
- simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(
- initial_communications_pattern, pattern->src_proc,
- simgrid::mc::PatternCommunicationList*);
+ simgrid::mc::PatternCommunicationList* list =
+ xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*);
list->list.push_back(std::move(pattern));
} else {
/* Evaluate comm determinism */
this->deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
- xbt_dynar_get_as(
- initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
- )->index_comm++;
+ xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*)
+ ->index_comm++;
}
return;
}
pattern->comm_addr = simcall_comm_irecv__get__result(request);
simgrid::smpi::Request mpi_request;
- mc_model_checker->process().read(
- &mpi_request, remote((simgrid::smpi::Request*)simcall_comm_irecv__get__data(request)));
+ mc_model_checker->process().read(&mpi_request,
+ remote((simgrid::smpi::Request*)simcall_comm_irecv__get__data(request)));
pattern->tag = mpi_request.tag();
simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
- mc_model_checker->process().read(temp_comm, remote(
- static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
+ mc_model_checker->process().read(temp_comm,
+ remote(static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
char* remote_name;
} else
xbt_die("Unexpected call_type %i", (int) call_type);
- XBT_DEBUG("Insert incomplete comm pattern %p for process %lu",
- pattern.get(), issuer->pid);
- xbt_dynar_t dynar =
- xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
+ XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern.get(), issuer->pid);
+ xbt_dynar_t dynar = xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
simgrid::mc::PatternCommunication* pattern2 = pattern.release();
xbt_dynar_push(dynar, &pattern2);
}
-
void CommunicationDeterminismChecker::complete_comm_pattern(
- xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr,
- unsigned int issuer, int backtracking)
+ xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr, unsigned int issuer,
+ int backtracking)
{
simgrid::mc::PatternCommunication* current_comm_pattern;
unsigned int cursor = 0;
update_comm_pattern(current_comm_pattern, comm_addr);
completed = 1;
simgrid::mc::PatternCommunication* temp;
- xbt_dynar_remove_at(
- xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
- cursor, &temp);
+ xbt_dynar_remove_at(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, &temp);
comm_pattern = std::unique_ptr<simgrid::mc::PatternCommunication>(temp);
XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
break;
if(!completed)
xbt_die("Corresponding communication not found!");
- simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
- initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
+ simgrid::mc::PatternCommunicationList* pattern =
+ xbt_dynar_get_as(initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
if (!this->initial_communications_pattern_done)
/* Store comm pattern */
}
}
-CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
- : Checker(session)
+CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session) : Checker(session)
{
-
}
CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default;
for (auto const& state : stack_) {
smx_simcall_t req = &state->executed_req;
if (req)
- trace.push_back(simgrid::mc::request_to_string(
- req, state->transition.argument, simgrid::mc::RequestType::executed));
+ trace.push_back(
+ simgrid::mc::request_to_string(req, state->transition.argument, simgrid::mc::RequestType::executed));
}
return trace;
}
void CommunicationDeterminismChecker::logState() // override
{
Checker::logState();
- if (_sg_mc_comms_determinism &&
- !this->recv_deterministic &&
- this->send_deterministic) {
+ if (_sg_mc_comms_determinism && !this->recv_deterministic && this->send_deterministic) {
XBT_INFO("******************************************************");
XBT_INFO("**** Only-send-deterministic communication pattern ****");
XBT_INFO("******************************************************");
XBT_INFO("%s", this->recv_diff);
- } else if(_sg_mc_comms_determinism &&
- !this->send_deterministic &&
- this->recv_deterministic) {
+ } else if (_sg_mc_comms_determinism && !this->send_deterministic && this->recv_deterministic) {
XBT_INFO("******************************************************");
XBT_INFO("**** Only-recv-deterministic communication pattern ****");
XBT_INFO("******************************************************");
XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
XBT_INFO("Send-deterministic : %s", !this->send_deterministic ? "No" : "Yes");
if (_sg_mc_comms_determinism)
- XBT_INFO("Recv-deterministic : %s",
- !this->recv_deterministic ? "No" : "Yes");
+ XBT_INFO("Recv-deterministic : %s", !this->recv_deterministic ? "No" : "Yes");
}
void CommunicationDeterminismChecker::prepare()
stack_.push_back(std::move(initial_state));
}
-static inline
-bool all_communications_are_finished()
+static inline bool all_communications_are_finished()
{
for (size_t current_actor = 1; current_actor < MC_smx_get_maxpid(); current_actor++) {
xbt_dynar_t pattern = xbt_dynar_get_as(incomplete_communications_pattern, current_actor, xbt_dynar_t);
void CommunicationDeterminismChecker::restoreState()
{
/* Intermediate backtracking */
- {
- simgrid::mc::State* state = stack_.back().get();
- if (state->system_state) {
- simgrid::mc::restore_snapshot(state->system_state);
- MC_restore_communications_pattern(state);
- return;
- }
+ simgrid::mc::State* state = stack_.back().get();
+ if (state->system_state) {
+ simgrid::mc::restore_snapshot(state->system_state);
+ MC_restore_communications_pattern(state);
+ return;
}
/* Restore the initial state */
smx_simcall_t req = nullptr;
while (!stack_.empty()) {
-
/* Get current state */
simgrid::mc::State* state = stack_.back().get();
XBT_DEBUG("**************************************************");
- XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)",
- stack_.size(), state->num,
+ XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)", stack_.size(), state->num,
state->interleaveSize());
/* Update statistics */
mc_model_checker->visited_states++;
- if (stack_.size() <= (std::size_t) _sg_mc_max_depth
- && (req = MC_state_get_request(state)) != nullptr
- && (visited_state == nullptr)) {
+ if (stack_.size() <= (std::size_t)_sg_mc_max_depth && (req = MC_state_get_request(state)) != nullptr &&
+ (visited_state == nullptr)) {
int req_num = state->transition.argument;
- XBT_DEBUG("Execute: %s",
- simgrid::mc::request_to_string(
- req, req_num, simgrid::mc::RequestType::simix).c_str());
+ XBT_DEBUG("Execute: %s", simgrid::mc::request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str());
std::string req_str;
if (dot_output != nullptr)
std::unique_ptr<simgrid::mc::State> next_state =
std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
- /* If comm determinism verification, we cannot stop the exploration if
- some communications are not finished (at least, data are transferred).
- These communications are incomplete and they cannot be analyzed and
- compared with the initial pattern. */
- bool compare_snapshots = all_communications_are_finished()
- && this->initial_communications_pattern_done;
+ /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at
+ * least, data are transferred). These communications are incomplete and they cannot be analyzed and compared
+ * with the initial pattern. */
+ bool compare_snapshots = all_communications_are_finished() && this->initial_communications_pattern_done;
if (_sg_mc_max_visited_states == 0 ||
(visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots)) ==
XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
visited_state->original_num == -1 ? visited_state->num : visited_state->original_num);
else
- XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
- stack_.size());
+ XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size());
if (!this->initial_communications_pattern_done)
this->initial_communications_pattern_done = 1;
/* Trash the current state, no longer needed */
- XBT_DEBUG("Delete state %d at depth %zi",
- state->num, stack_.size());
+ XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size());
stack_.pop_back();
visited_state = nullptr;
while (!stack_.empty()) {
std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
stack_.pop_back();
- if (state->interleaveSize()
- && stack_.size() < (std::size_t) _sg_mc_max_depth) {
+ if (state->interleaveSize() && stack_.size() < (std::size_t)_sg_mc_max_depth) {
/* We found a back-tracking point, let's loop */
- XBT_DEBUG("Back-tracking to state %d at depth %zi",
- state->num, stack_.size() + 1);
+ XBT_DEBUG("Back-tracking to state %d at depth %zi", state->num, stack_.size() + 1);
stack_.push_back(std::move(state));
this->restoreState();
- XBT_DEBUG("Back-tracking to state %d at depth %zi done",
- stack_.back()->num, stack_.size());
+ XBT_DEBUG("Back-tracking to state %d at depth %zi done", stack_.back()->num, stack_.size());
break;
} else {
- XBT_DEBUG("Delete state %d at depth %zi",
- state->num, stack_.size() + 1);
+ XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size() + 1);
}
}
}
#include "src/mc/mc_dwarf.hpp"
#include "src/mc/Type.hpp"
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, xbt,
- "Logging specific to mc_compare in mc");
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, xbt, "Logging specific to mc_compare in mc");
namespace simgrid {
namespace mc {
{
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_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);
} 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_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);
}
}
}
simgrid::mc::Process* process = &mc_model_checker->process();
/* Start comparison */
- size_t i1, i2, j1, j2, k;
- void *addr_block1, *addr_block2, *addr_frag1, *addr_frag2;
- int nb_diff1 = 0, nb_diff2 = 0;
-
- int equal, res_compare = 0;
+ size_t j1;
+ size_t j2;
+ size_t k;
+ void* addr_block2;
+ void* addr_frag1;
+ void* addr_frag2;
+ int nb_diff1 = 0;
+ int nb_diff2 = 0;
/* Check busy blocks */
- i1 = 1;
+ size_t i1 = 1;
- malloc_info heapinfo_temp1, heapinfo_temp2;
+ malloc_info heapinfo_temp1;
+ malloc_info heapinfo_temp2;
malloc_info heapinfo_temp2b;
mc_mem_region_t heap_region1 = MC_get_heap_region(snapshot1);
abort();
}
- addr_block1 =
- ((void *) (((ADDR2UINT(i1)) - 1) * BLOCKSIZE +
- (char *) state.std_heap_copy.heapbase));
+ void* addr_block1 = ((void*)(((ADDR2UINT(i1)) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase));
if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED) { /* Large block */
continue;
}
- i2 = 1;
- equal = 0;
- res_compare = 0;
+ size_t i2 = 1;
+ int equal = 0;
+ int res_compare = 0;
/* Try first to associate to same block in the other heap */
if (heapinfo2->type == heapinfo1->type
&& state.equals_to2_(i1, 0).valid == 0) {
- addr_block2 = (ADDR2UINT(i1) - 1) * BLOCKSIZE +
- (char *) state.std_heap_copy.heapbase;
- res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing,
- addr_block1, addr_block2, snapshot1, snapshot2,
- nullptr, nullptr, 0);
+ addr_block2 = (ADDR2UINT(i1) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
+ res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing, addr_block1, addr_block2, snapshot1,
+ snapshot2, nullptr, nullptr, 0);
if (res_compare != 1) {
for (k = 1; k < heapinfo2->busy_block.size; k++)
state.equals_to2_(i1 + k, 0) = HeapArea(i1, -1);
while (i2 < state.heaplimit && !equal) {
- addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE +
- (char *) state.std_heap_copy.heapbase;
+ addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
if (i2 == i1) {
i2++;
}
if (!equal) {
- XBT_DEBUG("Block %zu not found (size_used = %zu, addr = %p)", i1,
- heapinfo1->busy_block.busy_size, addr_block1);
+ XBT_DEBUG("Block %zu not found (size_used = %zu, addr = %p)", i1, heapinfo1->busy_block.busy_size, addr_block1);
i1 = state.heaplimit + 1;
nb_diff1++;
//i1++;
if (state.equals_to1_(i1, j1).valid)
continue;
- addr_frag1 =
- (void *) ((char *) addr_block1 + (j1 << heapinfo1->type));
+ addr_frag1 = (void*)((char*)addr_block1 + (j1 << heapinfo1->type));
i2 = 1;
equal = 0;
addr_frag2 =
(void *) ((char *) addr_block2 +
(j1 << heapinfo2->type));
- res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing,
- addr_frag1, addr_frag2, snapshot1, snapshot2,
- nullptr, nullptr, 0);
+ res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing, addr_frag1, addr_frag2, snapshot1,
+ snapshot2, nullptr, nullptr, 0);
if (res_compare != 1)
equal = 1;
}
-
-
while (i2 < state.heaplimit && !equal) {
const malloc_info* heapinfo2b = (const malloc_info*) MC_region_read(
if (state.equals_to2_(i2, j2).valid)
continue;
- addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE +
- (char *) state.std_heap_copy.heapbase;
- addr_frag2 =
- (void *) ((char *) addr_block2 +
- (j2 << heapinfo2b->type));
+ addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
+ addr_frag2 = (void*)((char*)addr_block2 + (j2 << heapinfo2b->type));
- res_compare = compare_heap_area(
- state, simgrid::mc::ProcessIndexMissing,
- addr_frag1, addr_frag2, snapshot2, snapshot2,
- nullptr, nullptr, 0);
+ res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing, addr_frag1, addr_frag2, snapshot2,
+ snapshot2, nullptr, nullptr, 0);
if (res_compare != 1) {
equal = 1;
break;
}
if (!equal) {
- XBT_DEBUG
- ("Block %zu, fragment %zu not found (size_used = %zd, address = %p)\n",
- i1, j1, heapinfo1->busy_frag.frag_size[j1],
- addr_frag1);
+ XBT_DEBUG("Block %zu, fragment %zu not found (size_used = %zd, address = %p)\n", i1, j1,
+ heapinfo1->busy_frag.frag_size[j1], addr_frag1);
i2 = state.heaplimit + 1;
i1 = state.heaplimit + 1;
nb_diff1++;
}
/* All blocks/fragments are equal to another block/fragment ? */
- size_t i = 1, j = 0;
+ size_t i = 1;
+ size_t j = 0;
for(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));
- if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED
- && i1 == state.heaplimit
- && heapinfo1->busy_block.busy_size > 0
- && !state.equals_to1_(i, 0).valid) {
- XBT_DEBUG("Block %zu not found (size used = %zu)", i,
- heapinfo1->busy_block.busy_size);
+ if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED && i1 == state.heaplimit && heapinfo1->busy_block.busy_size > 0 &&
+ !state.equals_to1_(i, 0).valid) {
+ XBT_DEBUG("Block %zu not found (size used = %zu)", i, heapinfo1->busy_block.busy_size);
nb_diff1++;
}
if (heapinfo1->type <= 0)
continue;
for (j = 0; j < (size_t) (BLOCKSIZE >> heapinfo1->type); j++)
- if (i1 == state.heaplimit
- && heapinfo1->busy_frag.frag_size[j] > 0
- && !state.equals_to1_(i, j).valid) {
- XBT_DEBUG("Block %zu, Fragment %zu not found (size used = %zd)",
- i, j, heapinfo1->busy_frag.frag_size[j]);
+ if (i1 == state.heaplimit && heapinfo1->busy_frag.frag_size[j] > 0 && !state.equals_to1_(i, j).valid) {
+ XBT_DEBUG("Block %zu, Fragment %zu not found (size used = %zd)", i, j, heapinfo1->busy_frag.frag_size[j]);
nb_diff1++;
}
}
return 0;
}
- simgrid::mc::Type *subtype, *subsubtype;
- int res, elm_size;
- const void *addr_pointed1, *addr_pointed2;
+ simgrid::mc::Type* subtype;
+ simgrid::mc::Type* subsubtype;
+ int res;
+ int elm_size;
+ const void* addr_pointed1;
+ const void* addr_pointed2;
mc_mem_region_t heap_region1 = MC_get_heap_region(snapshot1);
mc_mem_region_t heap_region2 = MC_get_heap_region(snapshot2);
if (member.offset() == offset)
return member.type;
} else {
- void *real_member = simgrid::dwarf::resolve_member(
- real_base_address, type, &member, snapshot, process_index);
- if ((char*) real_member - (char *) real_base_address == offset)
+ void* real_member = simgrid::dwarf::resolve_member(real_base_address, type, &member, snapshot, process_index);
+ if ((char*)real_member - (char*)real_base_address == offset)
return member.type;
}
}
simgrid::mc::Process* process = &mc_model_checker->process();
int res_compare;
- ssize_t block1, frag1, block2, frag2;
+ ssize_t block1;
+ ssize_t frag1;
+ ssize_t block2;
+ ssize_t frag2;
ssize_t size;
int check_ignore = 0;
- void *real_addr_block1, *real_addr_block2, *real_addr_frag1, *real_addr_frag2;
+ void* real_addr_block1;
+ void* real_addr_block2;
+ void* real_addr_frag1;
+ void* real_addr_frag2;
int type_size = -1;
- int offset1 = 0, offset2 = 0;
- int new_size1 = -1, new_size2 = -1;
- simgrid::mc::Type *new_type1 = nullptr, *new_type2 = nullptr;
+ int offset1 = 0;
+ int offset2 = 0;
+ int new_size1 = -1;
+ int new_size2 = -1;
+
+ simgrid::mc::Type* new_type1 = nullptr;
+ simgrid::mc::Type* new_type2 = nullptr;
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;
- 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), process_index);
+ const malloc_info* heapinfos2 = snapshot2->read(remote((const malloc_info**)heapinfo_address), process_index);
malloc_info heapinfo_temp1, heapinfo_temp2;
}
// Get block number:
- block1 =
- ((char *) area1 -
- (char *) state.std_heap_copy.heapbase) / BLOCKSIZE + 1;
- block2 =
- ((char *) area2 -
- (char *) state.std_heap_copy.heapbase) / BLOCKSIZE + 1;
+ block1 = ((char*)area1 - (char*)state.std_heap_copy.heapbase) / BLOCKSIZE + 1;
+ block2 = ((char*)area2 - (char*)state.std_heap_copy.heapbase) / BLOCKSIZE + 1;
// 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(simgrid::mc::makeHeapLocationPair(block1, -1, block2, -1));
if (match_pairs)
state.match_equals(previous);
return 0;
}
// If either block is not in the expected area of memory:
- if (((char *) area1 < (char *) state.std_heap_copy.heapbase)
- || (block1 > (ssize_t) state.processStates[0].heapsize) || (block1 < 1)
- || ((char *) area2 < (char *) state.std_heap_copy.heapbase)
- || (block2 > (ssize_t) state.processStates[1].heapsize) || (block2 < 1)) {
+ if (((char*)area1 < (char*)state.std_heap_copy.heapbase) || (block1 > (ssize_t)state.processStates[0].heapsize) ||
+ (block1 < 1) || ((char*)area2 < (char*)state.std_heap_copy.heapbase) ||
+ (block2 > (ssize_t)state.processStates[1].heapsize) || (block2 < 1)) {
return 1;
}
// Process address of the block:
- real_addr_block1 = (ADDR2UINT(block1) - 1) * BLOCKSIZE +
- (char *) state.std_heap_copy.heapbase;
- real_addr_block2 = (ADDR2UINT(block2) - 1) * BLOCKSIZE +
- (char *) state.std_heap_copy.heapbase;
+ real_addr_block1 = (ADDR2UINT(block1) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
+ real_addr_block2 = (ADDR2UINT(block2) - 1) * BLOCKSIZE + (char*)state.std_heap_copy.heapbase;
if (type) {
-
if (type->full_type)
type = type->full_type;
type = type->subtype;
// Find type_size:
- if (type->type == DW_TAG_pointer_type
- || (type->type == DW_TAG_base_type && !type->name.empty()
- && type->name == "char"))
+ if (type->type == DW_TAG_pointer_type ||
+ (type->type == DW_TAG_base_type && !type->name.empty() && type->name == "char"))
type_size = -1;
else
type_size = type->byte_size;
return 0;
}
- if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED
- && heapinfo2->type == MMALLOC_TYPE_UNFRAGMENTED) {
+ if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED && heapinfo2->type == MMALLOC_TYPE_UNFRAGMENTED) {
/* Complete block */
// TODO, lookup variable type from block type as done for fragmented blocks
- offset1 = (char *) area1 - (char *) real_addr_block1;
- offset2 = (char *) area2 - (char *) real_addr_block2;
+ offset1 = (char*)area1 - (char*)real_addr_block1;
+ offset2 = (char*)area2 - (char*)real_addr_block2;
- if (state.equals_to1_(block1, 0).valid
- && state.equals_to2_(block2, 0).valid
- && state.blocksEqual(block1, block2)) {
+ if (state.equals_to1_(block1, 0).valid && state.equals_to2_(block2, 0).valid && state.blocksEqual(block1, block2)) {
if (match_pairs)
state.match_equals(previous);
return 0;
if (heapinfo1->busy_block.busy_size != heapinfo2->busy_block.busy_size)
return 1;
- if (!previous->insert(simgrid::mc::makeHeapLocationPair(
- block1, -1, block2, -1)).second) {
+ if (!previous->insert(simgrid::mc::makeHeapLocationPair(block1, -1, block2, -1)).second) {
if (match_pairs)
state.match_equals(previous);
return 0;
} else if ((heapinfo1->type > 0) && (heapinfo2->type > 0)) { /* Fragmented block */
// Fragment number:
- frag1 =
- ((uintptr_t) (ADDR2UINT(area1) % (BLOCKSIZE))) >> heapinfo1->type;
- frag2 =
- ((uintptr_t) (ADDR2UINT(area2) % (BLOCKSIZE))) >> heapinfo2->type;
+ frag1 = ((uintptr_t)(ADDR2UINT(area1) % (BLOCKSIZE))) >> heapinfo1->type;
+ frag2 = ((uintptr_t)(ADDR2UINT(area2) % (BLOCKSIZE))) >> heapinfo2->type;
// Process address of the fragment:
- real_addr_frag1 =
- (void *) ((char *) real_addr_block1 +
- (frag1 << heapinfo1->type));
- real_addr_frag2 =
- (void *) ((char *) real_addr_block2 +
- (frag2 << heapinfo2->type));
+ real_addr_frag1 = (void*)((char*)real_addr_block1 + (frag1 << heapinfo1->type));
+ real_addr_frag2 = (void*)((char*)real_addr_block2 + (frag2 << heapinfo2->type));
// Check the size of the fragments against the size of the type:
if (type_size != -1) {
- if (heapinfo1->busy_frag.frag_size[frag1] == -1
- || heapinfo2->busy_frag.frag_size[frag2] == -1) {
+ if (heapinfo1->busy_frag.frag_size[frag1] == -1 || heapinfo2->busy_frag.frag_size[frag2] == -1) {
if (match_pairs)
state.match_equals(previous);
return -1;
}
// Check if the blocks are already matched together:
- if (state.equals_to1_(block1, frag1).valid
- && state.equals_to2_(block2, frag2).valid) {
+ if (state.equals_to1_(block1, frag1).valid && state.equals_to2_(block2, frag2).valid) {
if (offset1==offset2 && state.fragmentsEqual(block1, frag1, block2, frag2)) {
if (match_pairs)
state.match_equals(previous);
}
}
// Compare the size of both fragments:
- if (heapinfo1->busy_frag.frag_size[frag1] !=
- heapinfo2->busy_frag.frag_size[frag2]) {
+ if (heapinfo1->busy_frag.frag_size[frag1] != heapinfo2->busy_frag.frag_size[frag2]) {
if (type_size == -1) {
if (match_pairs)
state.match_equals(previous);
new_type2 = type;
}
// Type inference from the block type.
- else if (state.types1_(block1, frag1) != nullptr
- || state.types2_(block2, frag2) != nullptr) {
+ else if (state.types1_(block1, frag1) != nullptr || state.types2_(block2, frag2) != nullptr) {
- offset1 = (char *) area1 - (char *) real_addr_frag1;
- offset2 = (char *) area2 - (char *) real_addr_frag2;
+ 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) {
+ 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);
+ 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);
+ get_offset_type(real_addr_frag2, state.types2_(block2, frag2), offset1, size, snapshot2, process_index);
} else if (state.types1_(block1, frag1) != nullptr) {
new_type1 =
- get_offset_type(real_addr_frag1, state.types1_(block1, frag1),
- offset1, size, snapshot1, process_index);
+ 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);
+ get_offset_type(real_addr_frag2, state.types1_(block1, frag1), offset2, size, snapshot2, process_index);
} else if (state.types2_(block2, frag2) != nullptr) {
new_type1 =
- get_offset_type(real_addr_frag1, state.types2_(block2, frag2),
- offset1, size, snapshot1, process_index);
+ 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);
+ get_offset_type(real_addr_frag2, state.types2_(block2, frag2), offset2, size, snapshot2, process_index);
} else {
if (match_pairs)
state.match_equals(previous);
size = new_size1;
}
- if (offset1 == 0 && offset2 == 0
- && !previous->insert(simgrid::mc::makeHeapLocationPair(
- block1, frag1, block2, frag2)).second) {
- if (match_pairs)
- state.match_equals(previous);
- return 0;
- }
+ if (offset1 == 0 && offset2 == 0 &&
+ !previous->insert(simgrid::mc::makeHeapLocationPair(block1, frag1, block2, frag2)).second) {
+ if (match_pairs)
+ state.match_equals(previous);
+ return 0;
+ }
if (size <= 0) {
if (match_pairs)
return 0;
}
- if ((heapinfo1->busy_frag.ignore[frag1] > 0)
- && (heapinfo2->busy_frag.ignore[frag2] ==
- heapinfo1->busy_frag.ignore[frag1]))
+ if ((heapinfo1->busy_frag.ignore[frag1] > 0) &&
+ (heapinfo2->busy_frag.ignore[frag2] == heapinfo1->busy_frag.ignore[frag1]))
check_ignore = heapinfo1->busy_frag.ignore[frag1];
} else
/* Start comparison */
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, process_index, 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, process_index, area1, area2, snapshot1, snapshot2, previous,
+ size, check_ignore);
if (res_compare == 1)
return res_compare;
simgrid::mc::Type* subtype;
simgrid::mc::Type* subsubtype;
- int elm_size, i, res;
+ int elm_size;
+ int i;
+ int res;
top:
switch (type->type) {
case DW_TAG_base_type:
case DW_TAG_enumeration_type:
case DW_TAG_union_type:
- {
- return MC_snapshot_region_memcmp(
- real_area1, region1, real_area2, region2,
- type->byte_size) != 0;
- }
+ return MC_snapshot_region_memcmp(real_area1, region1, real_area2, region2, type->byte_size) != 0;
case DW_TAG_typedef:
case DW_TAG_volatile_type:
case DW_TAG_const_type:
