invoke a debugger instead of going via addr2line and friends

CMakeLists.txt

@@ -5,7 +5,6 @@ cmake_minimum_required (VERSION 3.14.0)
 project(Vampire)
 
 include(CheckIPOSupported)
-include(CheckPIESupported)
 
 # require the compiler to use C++17
 set(CMAKE_CXX_STANDARD 17)
@@ -986,24 +985,6 @@ if(CMAKE_BUILD_TYPE STREQUAL Release AND IPO)
   set_property(TARGET vampire PROPERTY INTERPROCEDURAL_OPTIMIZATION true)
 endif()
 
-# do not generate position-independent code:
-# 1. it has some overhead
-# 2. it's used for ASLR, which isn't a huge concern for us and messes with our backtrace support
-check_pie_supported(OUTPUT_VARIABLE PIE_ERROR LANGUAGES CXX)
-if(NOT CMAKE_CXX_LINK_PIE_SUPPORTED)
-  message(STATUS "disabling position-independent code not supported, stack traces may be broken")
-  message(STATUS "${PIE_ERROR}")
-endif()
-
-# FIXME this guard should not be necessary but is currently because of how we do static linking above
-if(BUILD_SHARED_LIBS)
-  set_property(TARGET vampire PROPERTY POSITION_INDEPENDENT_CODE false)
-  if(COMPILE_TESTS)
-    set_property(TARGET vtest PROPERTY POSITION_INDEPENDENT_CODE false)
-  endif()
-endif()
-
-
 ################################################################
 # subsat (standalone version of the SAT solver used for subsumption and subsumption resolution)
 ################################################################

Debug/Assertion.cpp

@@ -46,7 +46,7 @@ void Assertion::violated(const char* file, int line, const char* cond)
          << " violated:\n"
          << cond << "\n"
          << "----- stack dump -----\n";
-    Tracer::printStack(std::cout);
+    Tracer::printStack();
     std::cout << "----- end of stack dump -----" << std::endl;
   }
   abortAfterViolation();
@@ -62,7 +62,7 @@ void Assertion::violatedStrEquality(const char* file, int line, const char* val1
               << val1Str << " == \"" << val1 << "\"\n"
               << val2Str << " == \"" << val2 << "\"\n"
               << "----- stack dump -----\n";
-    Tracer::printStack(std::cout);
+    Tracer::printStack();
     std::cout << "----- end of stack dump -----\n";
   }
   abortAfterViolation();

Debug/Assertion.hpp

@@ -238,7 +238,7 @@ void Debug::Assertion::violated(const char* file, int line, const char* cond,
          << cond << "\n"
          << "Value of " << repStr << " is: " << rep
          << "\n----- stack dump -----\n";
-    Tracer::printStack(std::cout);
+    Tracer::printStack();
     std::cout << "----- end of stack dump -----\n";
   }
   abortAfterViolation();
@@ -255,7 +255,7 @@ void Debug::Assertion::violated(const char* file, int line, const char* cond,
          << "Value of " << repStr << " is: " << rep << "\n"
          << "Value of " << repStr2 << " is: " << rep2
          << "\n----- stack dump -----\n";
-    Tracer::printStack(std::cout);
+    Tracer::printStack();
     std::cout << "----- end of stack dump -----\n";
   }
   abortAfterViolation();
@@ -271,7 +271,7 @@ void Debug::Assertion::violatedEquality(const char* file, int line, const char*
               << val1Str << " == " << val1 << "\n"
               << val2Str << " == " << val2 << "\n"
               << "----- stack dump -----\n";
-    Tracer::printStack(std::cout);
+    Tracer::printStack();
     std::cout << "----- end of stack dump -----\n";
   }
   abortAfterViolation();
@@ -287,7 +287,7 @@ void Debug::Assertion::violatedNonequality(const char* file, int line, const cha
               << val1Str << " == " << val1 << "\n"
               << val2Str << " == " << val2 << "\n"
               << "----- stack dump -----\n";
-    Tracer::printStack(std::cout);
+    Tracer::printStack();
     std::cout << "----- end of stack dump -----\n";
   }
   abortAfterViolation();
@@ -319,7 +319,7 @@ void Debug::Assertion::violatedComparison(const char* file, int line, const char
               << val1Str << " == " << val1 << "\n"
               << val2Str << " == " << val2 << "\n"
               << "----- stack dump -----\n";
-    Tracer::printStack(std::cout);
+    Tracer::printStack();
     std::cout << "----- end of stack dump -----\n";
   }
   abortAfterViolation();
@@ -334,7 +334,7 @@ void Debug::Assertion::violatedMethod(const char* file, int line, const T& obj,
               << file << ", line " << line << " was violated for:\n"
               << objStr << " == " << obj << "\n"
               << "----- stack dump -----\n";
-    Tracer::printStack(std::cout);
+    Tracer::printStack();
     std::cout << "----- end of stack dump -----\n";
   }
   abortAfterViolation();

Debug/Tracer.cpp

@@ -17,70 +17,62 @@
  *
  * @since 01/05/2002 Manchester
  * @since 25/12/2023 Mísečky invoke system binary for backtrace
+ * @since 25/07/2024 Oxford invoke debugger for general sanity
  */
 
-#if __has_include(<execinfo.h>)
-#include <execinfo.h>
-#define HAVE_EXECINFO
-#endif
-
 #include <cstdlib>
 #include <sstream>
 
+// for getpid()
+// TODO compile guards for this and similar headers
+#include <unistd.h>
+
 #include "Tracer.hpp"
-#include "Lib/System.hpp"
 #include "Lib/Environment.hpp"
+#include "Lib/System.hpp"
 #include "Shell/Options.hpp"
 
 // define in version.cpp.in
 extern const char* VERSION_STRING;
 
-// if we have a callstack, the maximum number to actually retrieve
-const unsigned MAX_CALLS = 1024;
+// try and invoke the GNU debugger in batch mode on this process
+static bool try_gdb(pid_t pid) {
+  std::stringstream command;
+  command
+    // ask for a traceback in batch mode
+    << "gdb --batch -ex bt --pid="
+    << pid;
+  std::cout << command.str() << '\n';
+  return std::system(command.str().c_str()) == 0;
+}
+
+// try and invoke the LLVM debugger in batch mode on this process
+static bool try_lldb(pid_t pid) {
+  std::stringstream command;
+  command
+    // ask for a traceback in batch mode
+    << "lldb --batch -o bt "
+    //<< argv0
+    << " --attach-pid "
+    << pid;
+  std::cout << command.str() << '\n';
+  return std::system(command.str().c_str()) == 0;
+}
 
 /**
- * Print the stack.
+ * Print the stack if --traceback on
  * @since 24/10/2002 Manchester
  * @since 12/7/2023 using platform-specific calls to get the stack trace
  */
-void Debug::Tracer::printStack(std::ostream& str) {
-  str << "Version : " << VERSION_STRING << "\n";
-
-#ifdef HAVE_EXECINFO
-  void *call_stack[MAX_CALLS];
-  int sz = ::backtrace(call_stack, MAX_CALLS);
-  str << "call stack:";
-  for(int i = 0; i < sz; i++)
-    str << ' ' << call_stack[sz - (i + 1)];
-  str << std::endl;
-
-  if (env.options->traceback()) {
-// UNIX-like systems, including BSD and Linux but not MacOS
-#if defined(__unix__)
-  str << "invoking addr2line(1) ..." << std::endl;
-  std::stringstream out;
-  out << "addr2line -Cfe " << Lib::System::getArgv0();
-  for(int i = 0; i < sz; i++)
-    out << ' ' << call_stack[sz - (i + 1)];
-  std::system(out.str().c_str());
-// Apple things
-#elif defined(__APPLE__)
-  str << "invoking atos(1) ..." << std::endl;
-  std::stringstream out;
-  out << "atos -o " << Lib::System::getArgv0();
-  for(int i = 0; i < sz; i++)
-    out << ' ' << call_stack[sz - (i + 1)];
-  std::system(out.str().c_str());
-#else
-  // TODO symbol lookup support for other platforms
-  str << "no symbol lookup support for this platform yet" << std::endl;
-#endif
+void Debug::Tracer::printStack() {
+  std::cout << "Version : " << VERSION_STRING << "\n";
+  if(!env.options->traceback()) {
+    std::cout << "(use '--traceback on' to invoke a debugger and get a human-readable stack trace)\n";
+    return;
   }
-  else
-    str << "(use '--traceback on' to get a human-readable stack trace)" << std::endl;
 
-#else
-  // TODO backtrace support for other platforms
-  str << "no call stack support for this platform yet" << std::endl;
-#endif
-} // Tracer::printStack (ostream& str)
+  pid_t pid = getpid();
+  // is your favourite debugger not here? add it!
+  if(!try_gdb(pid) && !try_lldb(pid))
+    std::cout << "(neither GDB nor LLDB worked: perhaps you need to install one of them?)\n";
+}

Debug/Tracer.hpp

@@ -27,8 +27,8 @@
 namespace Debug {
 
 namespace Tracer {
-  // print the current stack
-  void printStack(std::ostream &out);
+  // print the current stack to stdout
+  void printStack();
 };
 
 template<class... As>

FMB/FiniteModelBuilder.cpp

@@ -2603,7 +2603,7 @@ void FiniteModelBuilder::SmtBasedDSAE::reportZ3OutOfMemory()
   if(env.statistics) {
     env.statistics->print(std::cout);
   }
-  Debug::Tracer::printStack(std::cout);
+  Debug::Tracer::printStack();
   System::terminateImmediately(1);
 }
 

Lib/System.cpp

@@ -17,10 +17,6 @@
 
 #include <csignal>
 
-// TODO these should probably be guarded
-// for getpid
-#include <unistd.h>
-
 #ifdef __linux__
 #include <sys/prctl.h>
 #endif
@@ -37,8 +33,6 @@
 
 namespace Lib {
 
-const char* System::s_argv0 = 0;
-
 const char* signalToString (int sigNum)
 {
   switch (sigNum)
@@ -123,7 +117,7 @@ void handleSignal (int sigNum)
       if (!Shell::UIHelper::portfolioParent) {
         if(env.statistics)
           env.statistics->print(std::cout);
-        Debug::Tracer::printStack(std::cout);
+        Debug::Tracer::printStack();
       }
       System::terminateImmediately(VAMP_RESULT_STATUS_OTHER_SIGNAL);
     }

Lib/System.hpp

@@ -38,16 +38,6 @@ class System {
   }
 
   static void registerForSIGHUPOnParentDeath();
-
-  /**
-   * Register the value of the argv[0] argument of the main function, so that
-   * it can be later used to determine the executable directory
-   */
-  static void registerArgv0(const char* argv0) { s_argv0 = argv0; }
-  static const char *getArgv0() { return s_argv0; }
-
-private:
-  static const char* s_argv0;
 };
 
 }

Makefile

@@ -23,19 +23,11 @@
 #   CHECK_LEAKS      - test for memory leaks (debugging mode only)
 #   VZ3              - compile with Z3
 
-COMPILE_ONLY = -fno-pie
-
-OS = $(shell uname)
-ifeq ($(OS),Darwin)
-LINK_ONLY = -Wl,-no_pie
-else
-LINK_ONLY = -no-pie
-endif
-
 COMMON_FLAGS = -DVTIME_PROFILING=0
 
 DBG_FLAGS = $(COMMON_FLAGS) -g  -DVDEBUG=1 -DCHECK_LEAKS=0 # debugging for spider
 REL_FLAGS = $(COMMON_FLAGS) -O3 -DVDEBUG=0 -D NDEBUG # no debugging
+
 GCOV_FLAGS = -O0 --coverage #-pedantic
 
 MINISAT_DBG_FLAGS = -D DEBUG
@@ -528,15 +520,15 @@ obj/%X: | obj
 
 $(CONF_ID)/%.o : %.cpp | $(CONF_ID)
 	mkdir -p `dirname $@`
-	$(CXX) $(CXXFLAGS) $(COMPILE_ONLY) -c -o $@ $*.cpp -MMD -MF $(CONF_ID)/$*.d
+	$(CXX) $(CXXFLAGS) -c -o $@ $*.cpp -MMD -MF $(CONF_ID)/$*.d
 
 %.o : %.c 
 $(CONF_ID)/%.o : %.c | $(CONF_ID)
-	$(CC) $(CCFLAGS) $(COMPILE_ONLY) -c -o $@ $*.c -MMD -MF $(CONF_ID)/$*.d
+	$(CC) $(CCFLAGS) -c -o $@ $*.c -MMD -MF $(CONF_ID)/$*.d
 
 %.o : %.cc
 $(CONF_ID)/%.o : %.cc | $(CONF_ID)
-	$(CXX) $(CXXFLAGS) $(COMPILE_ONLY) -c -o $@ $*.cc $(MINISAT_FLAGS) -MMD -MF $(CONF_ID)/$*.d
+	$(CXX) $(CXXFLAGS) -c -o $@ $*.cc $(MINISAT_FLAGS) -MMD -MF $(CONF_ID)/$*.d
 
 ################################################################
 # targets for executables
@@ -548,7 +540,7 @@ VSAT_OBJ := $(addprefix $(CONF_ID)/, $(VSAT_DEP))
 TKV_OBJ := $(addprefix $(CONF_ID)/, $(TKV_DEP))
 
 define COMPILE_CMD
-$(CXX) $(CXXFLAGS) $(LINK_ONLY) $(filter -l%, $+) $(filter %.o, $^) -o $@_$(BRANCH)_$(COM_CNT) $(Z3LIB)
+$(CXX) $(CXXFLAGS) $(filter -l%, $+) $(filter %.o, $^) -o $@_$(BRANCH)_$(COM_CNT) $(Z3LIB)
 @#$(CXX) -static $(CXXFLAGS) $(Z3LIB) $(filter %.o, $^) -o $@
 @#strip $@
 endef

SAT/MinisatInterfacingNewSimp.cpp

@@ -52,7 +52,7 @@ void MinisatInterfacingNewSimp::reportMinisatOutOfMemory() {
   if(env.statistics) {
     env.statistics->print(std::cout);
   }
-  Debug::Tracer::printStack(std::cout);
+  Debug::Tracer::printStack();
   System::terminateImmediately(1);
 }
 

Test/UnitTesting.cpp

@@ -225,10 +225,6 @@ int main(int argc, const char** argv)
   using namespace Lib;
   using namespace std;
 
-  // enable tracebacks in failing unit tests by default
-  System::registerArgv0(argv[0]);
-  env.options->setTraceback(true);
-
   bool success;
   auto cmd = std::string(argv[1]);
   auto args = Stack<std::string>(argc - 2);

vampire.cpp

@@ -738,7 +738,6 @@ void interactiveMetamode()
  */
 int main(int argc, char* argv[])
 {
-  System::registerArgv0(argv[0]);
   System::setSignalHandlers();
 
   try {