From 79cf0bb909f6c6b9885c928b427344911b708144 Mon Sep 17 00:00:00 2001
From: Gabriel Corona <gabriel.corona@loria.fr>
Date: Fri, 25 Mar 2016 17:08:14 +0100
Subject: [PATCH] [mc] Dump the current trace when the model-checked crashes

---
 src/mc/Process.cpp   | 34 +++++++++++++++++++++++++++
 src/mc/Process.hpp   |  2 ++
 src/mc/mc_global.cpp | 55 ++++++++++++++++++++++++++------------------
 src/mc/mc_unw.h      |  4 ++++
 4 files changed, 72 insertions(+), 23 deletions(-)

diff --git a/src/mc/Process.cpp b/src/mc/Process.cpp
index 12a1499d48..dd04f153ae 100644
--- a/src/mc/Process.cpp
+++ b/src/mc/Process.cpp
@@ -11,6 +11,10 @@
 #include <stdint.h>
 #include <errno.h>
 
+#include <sys/ptrace.h>
+
+#include <cstdio>
+
 #include <sys/types.h>
 #include <fcntl.h>
 #include <unistd.h>
@@ -680,5 +684,35 @@ std::vector<simgrid::mc::SimixProcessInformation>& Process::old_simix_processes(
   return smx_old_process_infos;
 }
 
+void Process::dumpStack()
+{
+  unw_addr_space_t as = unw_create_addr_space(&_UPT_accessors, __BYTE_ORDER);
+  if (as == nullptr) {
+    XBT_ERROR("Could not initialize ptrace address space");
+    return;
+  }
+
+  void* context = _UPT_create(this->pid_);
+  if (context == nullptr) {
+    unw_destroy_addr_space(as);
+    XBT_ERROR("Could not initialize ptrace context");
+    return;
+  }
+
+  unw_cursor_t cursor;
+  if (unw_init_remote(&cursor, as, context) != 0) {
+    _UPT_destroy(context);
+    unw_destroy_addr_space(as);
+    XBT_ERROR("Could not initialiez ptrace cursor");
+    return;
+  }
+
+  simgrid::mc::dumpStack(stderr, cursor);
+
+  _UPT_destroy(context);
+  unw_destroy_addr_space(as);
+  return;
+}
+
 }
 }
diff --git a/src/mc/Process.hpp b/src/mc/Process.hpp
index 5a9e3068f7..150f7d1827 100644
--- a/src/mc/Process.hpp
+++ b/src/mc/Process.hpp
@@ -216,6 +216,8 @@ public:
   std::vector<simgrid::mc::SimixProcessInformation>& simix_processes();
   std::vector<simgrid::mc::SimixProcessInformation>& old_simix_processes();
 
+  void dumpStack();
+
 private:
   void init_memory_map_info();
   void refresh_heap();
diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 4885373fd1..0d804882f7 100644
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -259,15 +259,39 @@ void MC_automaton_load(const char *file)
   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 : "?";
+#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));
+}
+
+}
+}
+
 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 =
@@ -276,24 +300,7 @@ static void MC_dump_stacks(FILE* file)
     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
@@ -343,6 +350,8 @@ void MC_report_crash(int status)
   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
diff --git a/src/mc/mc_unw.h b/src/mc/mc_unw.h
index 3625d26990..87d3fa9f6c 100644
--- a/src/mc/mc_unw.h
+++ b/src/mc/mc_unw.h
@@ -87,6 +87,10 @@ public:
   static unw_addr_space_t createUnwindAddressSpace();
 };
 
+void MC_dump_stack_unw(FILE* file, unw_cursor_t cursor);
+void dumpStack(FILE* file, unw_cursor_t cursor);
+void dumpStack(FILE* file, pid_t pid);
+
 }
 }
 
-- 
2.20.1