Add flags for graphical output of exploration

doc/manual.tex

@@ -2,6 +2,7 @@
 
 \usepackage[utf8]{inputenc}
 \usepackage{amssymb}
+\usepackage[colorlinks,linkcolor=black]{hyperref}
 
 \title{Nidhugg -- Manual\\\large{Version %%NIDHUGGVERSION%%}}
 \author{}
@@ -365,6 +366,38 @@ \subsubsection{Transformation Switches}\label{sec:transform:switches}
   high-level language.
 \end{description}
 
+\subsubsection{Tracing Switches}
+
+Nidhugg has some switches that can show how it is exploring a program
+and what operations it considers racing. There operations output graphs
+in Graphviz\footnote{\url{https://graphviz.org}} DOT format.
+
+\begin{description}
+\item{\texttt{--dump-tree=$OUTFILE$}}
+%
+  After analysis, write a graph that visualises the exploration tree to
+  $OUTFILE$.
+
+\item{\texttt{--dump-traces=$OUTFILE$}}
+%
+  After analysis, write a graph of the happens-before orders of all explored
+  traces to $OUTFILE$.
+%
+  \limitsupport{SC, TSO, PSO}
+
+\item{\texttt{--dump-spec=$OUTFILE$}}
+%
+  This option is primarily useful to developers of Nidhugg. After analysis,
+  write a minimised \texttt{DPORDriver\_test::trace\_set\_\hspace{0pt}spec}
+  characterising the explored set of traces, excluding sleepset-blocked ones, to
+  $OUTFILE$. Useful for creating regression tests after an issue has been fixed,
+  and the test program is not small enough to make writing a
+  \texttt{DPORDriver\_test::trace\_set\_spec} by hand feasible.
+%
+  \limitsupport{SC, TSO, PSO}
+
+\end{description}
+
 \subsubsection{Exit Status}
 
 Exit status for Nidhugg.

src/CPid.cpp

@@ -121,6 +121,10 @@ int CPid::get_aux_index() const{
   return aux_idx;
 }
 
+int CPid::get_child_index() const{
+  return proc_seq.back();
+}
+
 CPidSystem::CPidSystem(){
   real_children.push_back({});
   aux_children.push_back({});

src/CPid.h

@@ -71,6 +71,9 @@ class CPid{
    */
   int get_aux_index() const;
 
+  /* Returns pn where this CPid is <p0.....pn/i>. */
+  int get_child_index() const;
+
   std::string to_string() const;
 
   /* Comparison implements a total order over CPids. */

src/Configuration.cpp

@@ -99,6 +99,24 @@ static llvm::cl::opt<bool> cl_debug_print_on_reset
 ("debug-print-on-reset",llvm::cl::Hidden,
  llvm::cl::desc("Print debug info after exploring each trace."));
 
+static llvm::cl::OptionCategory cl_dump_cat
+("Trace Dumping");
+
+static llvm::cl::opt<std::string> cl_dump_traces
+("dump-traces",llvm::cl::NotHidden,llvm::cl::cat(cl_dump_cat),
+ llvm::cl::value_desc("FILE"),
+ llvm::cl::desc("Write graph of explored equivalence classes to FILE."));
+
+static llvm::cl::opt<std::string> cl_dump_tree
+("dump-tree",llvm::cl::NotHidden,llvm::cl::cat(cl_dump_cat),
+ llvm::cl::value_desc("FILE"),
+ llvm::cl::desc("Write graph of exploration tree to FILE."));
+
+static llvm::cl::opt<std::string> cl_dump_spec
+("dump-spec",llvm::cl::NotHidden,llvm::cl::cat(cl_dump_cat),
+ llvm::cl::value_desc("FILE"),
+ llvm::cl::desc("Write minimal trace_set_spec to FILE."));
+
 const std::set<std::string> &Configuration::commandline_opts(){
   static std::set<std::string> opts = {
     "dpor-explore-all",
@@ -113,7 +131,10 @@ const std::set<std::string> &Configuration::commandline_opts(){
     "no-spin-assume",
     "unroll",
     "print-progress",
-    "print-progress-estimate"
+    "print-progress-estimate",
+    "dump-traces",
+    "dump-tree",
+    "dump-spec",
   };
   return opts;
 }
@@ -137,6 +158,13 @@ void Configuration::assign_by_commandline(){
   print_progress = cl_print_progress || cl_print_progress_estimate;
   print_progress_estimate = cl_print_progress_estimate;
   debug_print_on_reset = cl_debug_print_on_reset;
+  trace_dump_file = cl_dump_traces;
+  debug_collect_all_traces |= !cl_dump_traces.empty();
+  tree_dump_file = cl_dump_tree;
+  debug_collect_all_traces |= !cl_dump_tree.empty();
+  ee_store_trace           |= !cl_dump_tree.empty();
+  spec_dump_file = cl_dump_spec;
+  debug_collect_all_traces |= !cl_dump_spec.empty();
   argv.resize(1);
   argv[0] = get_default_program_name();
   for(std::string a : cl_program_arguments){
@@ -226,6 +254,14 @@ void Configuration::check_commandline(){
         Debug::warn("Configuration::check_commandline:mm:robustness")
           << "WARNING: --robustness ignored under memory model " << mm << ".\n";
       }
+      if (cl_dump_traces != ""){
+        Debug::warn("Configuration::check_commandline:mm:dump-traces")
+          << "WARNING: --dump-traces not implemented for memory model " << mm << ".\n";
+      }
+      if (cl_dump_spec != ""){
+        Debug::warn("Configuration::check_commandline:mm:dump-spec")
+          << "WARNING: --dump-spec ignored under memory model " << mm << ".\n";
+      }
     }
     if (cl_dpor_algorithm == Configuration::OPTIMAL
         && cl_memory_model != Configuration::SC

src/Configuration.h

@@ -184,6 +184,12 @@ class Configuration{
    * traces.
    */
   bool print_progress_estimate;
+  /* File to dump graph of equivalence classes to. */
+  std::string trace_dump_file;
+  /* File to dump graph of exploration tree to. */
+  std::string tree_dump_file;
+  /* File to dump minimal trace set specification to. */
+  std::string spec_dump_file;
   /* The arguments that will be passed to the program under test */
   std::vector<std::string> argv;
   /* The default program name to send to the program under test as

src/DPORDriver_test.cpp

@@ -99,17 +99,16 @@ namespace DPORDriver_test {
     return res;
   }
 
-  int find(const IIDSeqTrace *_t, const IID<CPid> &iid){
-    const std::vector<IID<CPid> > &t = _t->get_computation();
-    for(int i = 0; i < int(t.size()); ++i){
-      if(t[i] == iid){
+  int find(const IIDVCSeqTrace *t, const IID<CPid> &iid){
+    for(int i = 0; i < int(t->size()); ++i){
+      if(t->get_iid(i) == iid){
         return i;
       }
     }
     return -1;
   }
 
-  bool check_trace(const IIDSeqTrace *t, const trace_spec &spec){
+  bool check_trace(const IIDVCSeqTrace *t, const trace_spec &spec){
     for(unsigned i = 0; i < spec.size(); ++i){
       int a_i = find(t,spec[i].a);
       int b_i = find(t,spec[i].b);
@@ -122,11 +121,12 @@ namespace DPORDriver_test {
 
   /* Returns true iff the indices of the IIDs of each process is
    * strictly increasing along the computation of t. */
-  bool all_clocks_increasing(const IIDSeqTrace *t){
+  bool all_clocks_increasing(const IIDVCSeqTrace *t){
     VClock<CPid> pcs;
-    for(auto it = t->get_computation().begin(); it != t->get_computation().end(); ++it){
-      if(it->get_index() <= pcs[it->get_pid()]) return false;
-      pcs[it->get_pid()] = it->get_index();
+    for(unsigned i = 0; i < t->size(); ++i){
+      const IID<CPid> &iid = t->get_iid(i);
+      if(iid.get_index() <= pcs[iid.get_pid()]) return false;
+      pcs[iid.get_pid()] = iid.get_index();
     }
     return true;
   }
@@ -141,7 +141,7 @@ namespace DPORDriver_test {
     }
     bool retval = true;
     for(unsigned i = 0; i < res.all_traces.size(); ++i){
-      if(!all_clocks_increasing(static_cast<const IIDSeqTrace*>(res.all_traces[i]))){
+      if(!all_clocks_increasing(static_cast<const IIDVCSeqTrace*>(res.all_traces[i]))){
         llvm::dbgs() << "DPORDriver_test::check_all_traces: "
                      << "Non increasing instruction index in trace.\n";
         retval = false;
@@ -160,7 +160,7 @@ namespace DPORDriver_test {
       int prev_match = -1;
       for(unsigned j = 0; j < res.all_traces.size(); ++j){
         if(res.all_traces[j]->is_blocked()) continue;
-        if(check_trace(static_cast<const IIDSeqTrace*>(res.all_traces[j]),spec[i])){
+        if(check_trace(static_cast<const IIDVCSeqTrace*>(res.all_traces[j]),spec[i])){
           if(found){
             // Multiple traces match the same specification
             llvm::dbgs() << "DPORDriver_test::check_all_traces: Multiple traces (#"
@@ -215,12 +215,12 @@ namespace DPORDriver_test {
   static bool trace_equiv(const Trace *a, const Trace *b){
     if (a->get_errors().size() != b->get_errors().size()) return false;
     std::list<Error*> bes;
-    for (Error *be : b->get_errors()) {
-      bes.push_back(be);
+    for (const std::unique_ptr<Error> &be : b->get_errors()) {
+      bes.push_back(be.get());
     }
-    for (Error *ae : a->get_errors()) {
-      auto bei = std::find_if(bes.begin(), bes.end(), [ae](const Error *be){
-          return error_equiv(ae, be);
+    for (const std::unique_ptr<Error> &ae : a->get_errors()) {
+      auto bei = std::find_if(bes.begin(), bes.end(), [&ae](const Error *be){
+          return error_equiv(ae.get(), be);
         });
       if (bei == bes.end()) return false;
       bei = bes.erase(bei);

src/DPORDriver_test.h

@@ -18,7 +18,6 @@
  */
 
 #include <config.h>
-#ifdef HAVE_BOOST_UNIT_TEST_FRAMEWORK
 
 #ifndef __DPOR_DRIVER_TEST_H__
 #define __DPOR_DRIVER_TEST_H__
@@ -34,15 +33,6 @@
  */
 namespace DPORDriver_test {
 
-  /* A configuration with memory_model == TSO (resp. SC, PSO), and
-   * debug_collect_all_traces == true.
-   */
-  const Configuration &get_tso_conf();
-  const Configuration &get_sc_conf();
-  const Configuration &get_pso_conf();
-  const Configuration &get_power_conf();
-  const Configuration &get_arm_conf();
-
   /* An IIDOrder object {a,b} should be interpreted as a predicate
    * over traces, with the meaning "a precedes b in time".
    */
@@ -64,6 +54,17 @@ namespace DPORDriver_test {
    */
   typedef std::vector<trace_spec> trace_set_spec;
 
+#ifdef HAVE_BOOST_UNIT_TEST_FRAMEWORK
+
+  /* A configuration with memory_model == TSO (resp. SC, PSO), and
+   * debug_collect_all_traces == true.
+   */
+  const Configuration &get_tso_conf();
+  const Configuration &get_sc_conf();
+  const Configuration &get_pso_conf();
+  const Configuration &get_power_conf();
+  const Configuration &get_arm_conf();
+
   /* Returns the cross product of specs. */
   trace_set_spec spec_xprod(const std::vector<trace_set_spec> &specs);
 
@@ -103,7 +104,7 @@ namespace DPORDriver_test {
                            const DPORDriver::Result &optimal_res,
                            const Configuration &conf);
 
+#endif /* defined(HAVE_BOOST_UNIT_TEST_FRAMEWORK) */
 }
 
 #endif
-#endif

src/Makefile.am

@@ -32,6 +32,7 @@ libnidhugg_a_SOURCES = \
   SymAddr.cpp SymAddr.h \
   Trace.cpp Trace.h \
   TraceBuilder.cpp TraceBuilder.h \
+  TraceDumper.cpp TraceDumper.h \
   Transform.cpp Transform.h \
   TSOInterpreter.cpp TSOInterpreter.h \
   TSOPSOTraceBuilder.h \

src/POWERARMTraceBuilder.cpp

@@ -51,6 +51,11 @@ std::string PATB_impl::PATrace::to_string(int _ind) const{
   return ss.str();
 }
 
+IID<CPid> PATB_impl::PATrace::get_iid(int index) const{
+  IID<int> iiid = events[index].iid;
+  return {cpids[iiid.get_pid()], iiid.get_index()};
+}
+
 std::string PATB_impl::TraceRecorder::to_string(int ind) const{
   std::stringstream ss;
   for(const Line &L : lines){
@@ -94,11 +99,11 @@ bool PATB_impl::TraceRecorder::source_line(int proc, const llvm::MDNode *md, std
   if(md){
     int lineno;
     std::string fname, dname;
-    if(get_location(md,&lineno,&fname,&dname)){
+    if(Trace::get_location(md,&lineno,&fname,&dname)){
       success = true;
       std::stringstream ss;
-      ss << basename(fname) << ":" << lineno
-         << " " << get_src_line_verbatim(md);
+      ss << Trace::basename(fname) << ":" << lineno
+         << " " << Trace::get_src_line_verbatim(md);
       ln += ss.str();
     }
   }
@@ -112,13 +117,15 @@ void PATB_impl::TraceRecorder::trace_register_metadata(int proc, const llvm::MDN
   std::string ln;
   int cpid_indent;
   source_line(proc,md,&ln,&cpid_indent);
+  std::string indent = "";
+  for(int i = 0; i < cpid_indent; ++i) indent += " ";
   lines.push_back({proc,ln});
   if(!last_committed.consumed){
     last_committed.consumed = true;
     int load_count = 0;
+    event_descs[last_committed.iid] += ln;
     for(const Access &A : last_committed.accesses){ // One line per access
       ln = "";
-      for(int i = 0; i < cpid_indent; ++i) ln += " "; // Indentation
       if(A.type == Access::LOAD){
         ln += "load 0x";
         std::stringstream ss;
@@ -164,7 +171,8 @@ void PATB_impl::TraceRecorder::trace_register_metadata(int proc, const llvm::MDN
            << "]";
         ln += ss.str();
       }
-      lines.push_back({proc,ln});
+      event_descs[last_committed.iid] += "\n" + ln;
+      lines.push_back({proc,indent+ln});
     }
   }
 }

src/POWERARMTraceBuilder.h

@@ -95,6 +95,8 @@ class POWERARMTraceBuilder : public TraceBuilder {
   /********************************
    * Methods for Recording Traces *
    ********************************/
+  /* Enables trace recording until the next reset. */
+  virtual void enable_tracing() = 0;
   /* When recording a trace, trace_register_metadata(proc,md) should
    * be called by the ExecutionEngine when an instruction has been
    * committed. proc should be the committing thread and md should be