From 5456122a5fdbcc87fc673df86604bd42dcb106bc Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Mon, 15 Jul 2024 17:43:50 +0100 Subject: [PATCH] invoke a debugger instead of going via addr2line and friends --- CMakeLists.txt | 19 ------- Debug/Assertion.cpp | 4 +- Debug/Assertion.hpp | 12 ++--- Debug/Tracer.cpp | 88 ++++++++++++++----------------- Debug/Tracer.hpp | 4 +- FMB/FiniteModelBuilder.cpp | 2 +- Lib/System.cpp | 8 +-- Lib/System.hpp | 10 ---- Makefile | 18 ++----- SAT/MinisatInterfacingNewSimp.cpp | 2 +- Test/UnitTesting.cpp | 4 -- vampire.cpp | 1 - 12 files changed, 58 insertions(+), 114 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 1d35d60b5e..bebc938108 100644 --- a/CMakeLists.txt +++ b/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) ################################################################ diff --git a/Debug/Assertion.cpp b/Debug/Assertion.cpp index d74bfa7c86..ee5dc39c40 100644 --- a/Debug/Assertion.cpp +++ b/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(); diff --git a/Debug/Assertion.hpp b/Debug/Assertion.hpp index 22524dedb1..1a3ba3653c 100644 --- a/Debug/Assertion.hpp +++ b/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(); diff --git a/Debug/Tracer.cpp b/Debug/Tracer.cpp index d063b45c3e..43732cab85 100644 --- a/Debug/Tracer.cpp +++ b/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() -#include -#define HAVE_EXECINFO -#endif - #include #include +// for getpid() +// TODO compile guards for this and similar headers +#include + #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"; +} diff --git a/Debug/Tracer.hpp b/Debug/Tracer.hpp index 013f3df3bf..d0e90fbcb6 100644 --- a/Debug/Tracer.hpp +++ b/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 diff --git a/FMB/FiniteModelBuilder.cpp b/FMB/FiniteModelBuilder.cpp index e25381e9d1..c88ccae7b3 100644 --- a/FMB/FiniteModelBuilder.cpp +++ b/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); } diff --git a/Lib/System.cpp b/Lib/System.cpp index 98ad5a95ed..b4cf175998 100644 --- a/Lib/System.cpp +++ b/Lib/System.cpp @@ -17,10 +17,6 @@ #include -// TODO these should probably be guarded -// for getpid -#include - #ifdef __linux__ #include #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); } diff --git a/Lib/System.hpp b/Lib/System.hpp index ae5ce876e3..199b12e8a9 100644 --- a/Lib/System.hpp +++ b/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; }; } diff --git a/Makefile b/Makefile index c3c55456a0..91047355c9 100644 --- a/Makefile +++ b/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 diff --git a/SAT/MinisatInterfacingNewSimp.cpp b/SAT/MinisatInterfacingNewSimp.cpp index 262057fc05..78d6481257 100644 --- a/SAT/MinisatInterfacingNewSimp.cpp +++ b/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); } diff --git a/Test/UnitTesting.cpp b/Test/UnitTesting.cpp index cab19075ef..5813a2e3f4 100644 --- a/Test/UnitTesting.cpp +++ b/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(argc - 2); diff --git a/vampire.cpp b/vampire.cpp index d06ede5e2b..3743fa3b46 100644 --- a/vampire.cpp +++ b/vampire.cpp @@ -738,7 +738,6 @@ void interactiveMetamode() */ int main(int argc, char* argv[]) { - System::registerArgv0(argv[0]); System::setSignalHandlers(); try {