#include <cstddef>
#include <cstdint>
+#include <cxxabi.h>
+
#include <vector>
#include "mc_base.h"
#include "src/mc/mc_request.h"
#include "src/mc/mc_safety.h"
#include "src/mc/mc_snapshot.h"
-#include "src/mc/mc_liveness.h"
+#include "src/mc/LivenessChecker.hpp"
#include "src/mc/mc_private.h"
#include "src/mc/mc_unw.h"
#include "src/mc/mc_smx.h"
int user_max_depth_reached = 0;
/* MC global data structures */
-mc_state_t mc_current_state = nullptr;
+simgrid::mc::State* mc_current_state = nullptr;
char mc_replay_mode = false;
mc_stats_t mc_stats = nullptr;
char *req_str;
smx_simcall_t req = nullptr, saved_req = NULL;
xbt_fifo_item_t item, start_item;
- mc_state_t state;
+ simgrid::mc::State* state;
XBT_DEBUG("**** Begin Replay ****");
/* Intermediate backtracking */
if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) {
start_item = xbt_fifo_get_first_item(stack);
- state = (mc_state_t)xbt_fifo_get_item_content(start_item);
+ state = (simgrid::mc::State*)xbt_fifo_get_item_content(start_item);
if(state->system_state){
simgrid::mc::restore_snapshot(state->system_state);
if(_sg_mc_comms_determinism || _sg_mc_send_determinism)
item != xbt_fifo_get_first_item(stack);
item = xbt_fifo_get_prev_item(item)) {
- state = (mc_state_t) xbt_fifo_get_item_content(item);
+ state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
saved_req = MC_state_get_executed_request(state, &value);
if (saved_req) {
XBT_DEBUG("**** End Replay ****");
}
-/**
- * \brief Dumps the contents of a model-checker's stack and shows the actual
- * execution trace
- * \param stack The stack to dump
- */
-void MC_dump_stack_safety(xbt_fifo_t stack)
+void MC_show_deadlock(void)
{
- MC_show_stack_safety(stack);
-
- mc_state_t state;
-
- while ((state = (mc_state_t) xbt_fifo_pop(stack)) != nullptr)
- MC_state_delete(state, !state->in_visited_states ? 1 : 0);
-}
-
-
-void MC_show_stack_safety(xbt_fifo_t stack)
-{
- int value;
- mc_state_t state;
- xbt_fifo_item_t item;
- smx_simcall_t req;
- char *req_str = nullptr;
-
- for (item = xbt_fifo_get_last_item(stack);
- item; item = xbt_fifo_get_prev_item(item)) {
- state = (mc_state_t)xbt_fifo_get_item_content(item);
- req = MC_state_get_executed_request(state, &value);
- if (req) {
- req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
- XBT_INFO("%s", req_str);
- xbt_free(req_str);
- }
- }
-}
-
-void MC_show_deadlock(smx_simcall_t req)
-{
- /*char *req_str = nullptr; */
XBT_INFO("**************************");
XBT_INFO("*** DEAD-LOCK DETECTED ***");
XBT_INFO("**************************");
- XBT_INFO("Locked request:");
- /*req_str = simgrid::mc::request_to_string(req);
- XBT_INFO("%s", req_str);
- xbt_free(req_str); */
- XBT_INFO("Counter-example execution trace:");
- MC_dump_stack_safety(mc_stack);
- MC_print_statistics(mc_stats);
-}
-
-void MC_show_non_termination(void){
- XBT_INFO("******************************************");
- XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
- XBT_INFO("******************************************");
XBT_INFO("Counter-example execution trace:");
- MC_dump_stack_safety(mc_stack);
+ for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+ XBT_INFO("%s", s.c_str());
MC_print_statistics(mc_stats);
}
xbt_automaton_load(simgrid::mc::property_automaton, file);
}
+namespace simgrid {
+namespace mc {
+
+void dumpStack(FILE* file, unw_cursor_t cursor)
+{
+ int nframe = 0;
+ char buffer[100];
+
+ unw_word_t off;
+ do {
+ const char * name = !unw_get_proc_name(&cursor, buffer, 100, &off) ? buffer : "?";
+
+ int status;
+
+ // Demangle C++ names:
+ char* realname = abi::__cxa_demangle(name, 0, 0, &status);
+
+#if defined(__x86_64__)
+ unw_word_t rip = 0;
+ unw_word_t rsp = 0;
+ unw_get_reg(&cursor, UNW_X86_64_RIP, &rip);
+ unw_get_reg(&cursor, UNW_X86_64_RSP, &rsp);
+ fprintf(file, " %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n",
+ nframe, realname ? realname : name, (std::uint64_t) rip, (std::uint64_t) rsp);
+#else
+ fprintf(file, " %i: %s\n", nframe, realname ? realname : name);
+#endif
+
+ free(realname);
+ ++nframe;
+ } while(unw_step(&cursor));
+}
+
+}
+}
+
static void MC_dump_stacks(FILE* file)
{
int nstack = 0;
for (auto const& stack : mc_model_checker->process().stack_areas()) {
-
- fprintf(file, "Stack %i:\n", nstack);
-
- int nframe = 0;
- char buffer[100];
+ fprintf(file, "Stack %i:\n", nstack++);
simgrid::mc::UnwindContext context;
unw_context_t raw_context =
context.initialize(&mc_model_checker->process(), &raw_context);
unw_cursor_t cursor = context.cursor();
-
- unw_word_t off;
- do {
- const char * name = !unw_get_proc_name(&cursor, buffer, 100, &off) ? buffer : "?";
-#if defined(__x86_64__)
- unw_word_t rip = 0;
- unw_word_t rsp = 0;
- unw_get_reg(&cursor, UNW_X86_64_RIP, &rip);
- unw_get_reg(&cursor, UNW_X86_64_RSP, &rsp);
- fprintf(file, " %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n",
- nframe, name, (std::uint64_t) rip, (std::uint64_t) rsp);
-#else
- fprintf(file, " %i: %s\n", nframe, name);
-#endif
- ++nframe;
- } while(unw_step(&cursor));
-
- ++nstack;
+ simgrid::mc::dumpStack(file, cursor);
}
}
#endif
XBT_INFO("*** PROPERTY NOT VALID ***");
XBT_INFO("**************************");
XBT_INFO("Counter-example execution trace:");
- MC_record_dump_path(mc_stack);
- MC_dump_stack_safety(mc_stack);
+ simgrid::mc::dumpRecordPath();
+ for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+ XBT_INFO("%s", s.c_str());
MC_print_statistics(mc_stats);
}
else
XBT_INFO("No core dump was generated by the system.");
XBT_INFO("Counter-example execution trace:");
- MC_record_dump_path(mc_stack);
- MC_dump_stack_safety(mc_stack);
+ simgrid::mc::dumpRecordPath();
+ for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+ XBT_INFO("%s", s.c_str());
MC_print_statistics(mc_stats);
+ XBT_INFO("Stack trace:");
+ mc_model_checker->process().dumpStack();
}
#endif