From 57de807335402741c6371f66cbdd3d3f47863341 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Sat, 18 Sep 2021 02:13:16 +0200 Subject: [PATCH] Refactor tag suggestion mechanism (#7199) This refactors the internal tag suggestion mechanism to no longer rely on C-style char arrays, but use a C++ vector of strings instead. --- src/base/collect_tags.py | 10 ++++- src/base/configuration.cpp | 79 +++++++-------------------------- src/base/configuration.h | 13 +++--- src/options/didyoumean.h | 4 ++ src/options/options_handler.cpp | 51 ++++++++------------- 5 files changed, 50 insertions(+), 107 deletions(-) diff --git a/src/base/collect_tags.py b/src/base/collect_tags.py index 43e183b99..86cc94053 100644 --- a/src/base/collect_tags.py +++ b/src/base/collect_tags.py @@ -44,10 +44,16 @@ def collect_tags(basedir): def write_file(filename, type, tags): """Render the header file to the given filename.""" with open(filename, 'w') as out: - out.write('static char const* const {}_tags[] = {{\n'.format(type)) + out.write('static const std::vector {}_tags = {{\n'.format(type)) + if type == 'Debug': + out.write('#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)\n') + elif type == 'Trace': + out.write('#if defined(CVC5_TRACING)\n') + else: + raise 'type is neither Debug nor Trace: {}'.format(type) for t in tags: out.write('"{}",\n'.format(t)) - out.write('nullptr\n') + out.write('#endif\n') out.write('};\n') diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index a370a0c47..b4f6cae7f 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -18,20 +18,15 @@ #include #include +#include #include #include +#include "base/Debug_tags.h" +#include "base/Trace_tags.h" #include "base/configuration_private.h" #include "base/cvc5config.h" -#if defined(CVC5_DEBUG) && defined(CVC5_TRACING) -# include "base/Debug_tags.h" -#endif /* CVC5_DEBUG && CVC5_TRACING */ - -#ifdef CVC5_TRACING -# include "base/Trace_tags.h" -#endif /* CVC5_TRACING */ - using namespace std; namespace cvc5 { @@ -253,70 +248,26 @@ bool Configuration::isBuiltWithPoly() return IS_POLY_BUILD; } -unsigned Configuration::getNumDebugTags() { -#if defined(CVC5_DEBUG) && defined(CVC5_TRACING) - /* -1 because a NULL pointer is inserted as the last value */ - return (sizeof(Debug_tags) / sizeof(Debug_tags[0])) - 1; -#else /* CVC5_DEBUG && CVC5_TRACING */ - return 0; -#endif /* CVC5_DEBUG && CVC5_TRACING */ -} - -char const* const* Configuration::getDebugTags() { -#if defined(CVC5_DEBUG) && defined(CVC5_TRACING) +const std::vector& Configuration::getDebugTags() +{ return Debug_tags; -#else /* CVC5_DEBUG && CVC5_TRACING */ - static char const* no_tags[] = { NULL }; - return no_tags; -#endif /* CVC5_DEBUG && CVC5_TRACING */ -} - -int strcmpptr(const char **s1, const char **s2){ - return strcmp(*s1,*s2); -} - -bool Configuration::isDebugTag(char const *tag){ -#if defined(CVC5_DEBUG) && defined(CVC5_TRACING) - unsigned ntags = getNumDebugTags(); - char const* const* tags = getDebugTags(); - for (unsigned i = 0; i < ntags; ++ i) { - if (strcmp(tag, tags[i]) == 0) { - return true; - } - } -#endif /* CVC5_DEBUG && CVC5_TRACING */ - return false; } -unsigned Configuration::getNumTraceTags() { -#if CVC5_TRACING - /* -1 because a NULL pointer is inserted as the last value */ - return sizeof(Trace_tags) / sizeof(Trace_tags[0]) - 1; -#else /* CVC5_TRACING */ - return 0; -#endif /* CVC5_TRACING */ +bool Configuration::isDebugTag(const std::string& tag) +{ + return std::find(Debug_tags.begin(), Debug_tags.end(), tag) + != Debug_tags.end(); } -char const* const* Configuration::getTraceTags() { -#if CVC5_TRACING +const std::vector& Configuration::getTraceTags() +{ return Trace_tags; -#else /* CVC5_TRACING */ - static char const* no_tags[] = { NULL }; - return no_tags; -#endif /* CVC5_TRACING */ } -bool Configuration::isTraceTag(char const * tag){ -#if CVC5_TRACING - unsigned ntags = getNumTraceTags(); - char const* const* tags = getTraceTags(); - for (unsigned i = 0; i < ntags; ++ i) { - if (strcmp(tag, tags[i]) == 0) { - return true; - } - } -#endif /* CVC5_TRACING */ - return false; +bool Configuration::isTraceTag(const std::string& tag) +{ + return std::find(Trace_tags.begin(), Trace_tags.end(), tag) + != Trace_tags.end(); } bool Configuration::isGitBuild() { diff --git a/src/base/configuration.h b/src/base/configuration.h index 71c79c22e..01579526d 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -20,6 +20,7 @@ #define CVC5__CONFIGURATION_H #include +#include #include "cvc5_export.h" @@ -111,19 +112,15 @@ public: static bool isBuiltWithPoly(); - /* Return the number of debug tags */ - static unsigned getNumDebugTags(); /* Return a sorted array of the debug tags name */ - static char const* const* getDebugTags(); + static const std::vector& getDebugTags(); /* Test if the given argument is a known debug tag name */ - static bool isDebugTag(char const *); + static bool isDebugTag(const std::string& tag); - /* Return the number of trace tags */ - static unsigned getNumTraceTags(); /* Return a sorted array of the trace tags name */ - static char const* const* getTraceTags(); + static const std::vector& getTraceTags(); /* Test if the given argument is a known trace tag name */ - static bool isTraceTag(char const *); + static bool isTraceTag(const std::string& tag); static bool isGitBuild(); static const char* getGitBranchName(); diff --git a/src/options/didyoumean.h b/src/options/didyoumean.h index e588dd36d..0118f1484 100644 --- a/src/options/didyoumean.h +++ b/src/options/didyoumean.h @@ -36,6 +36,10 @@ class CVC5_EXPORT DidYouMean { ~DidYouMean() {} void addWord(std::string word) { d_words.insert(std::move(word)); } + void addWords(const std::vector& words) + { + d_words.insert(words.begin(), words.end()); + } std::vector getMatch(const std::string& input); diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 1b6cff519..bf2def05b 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -372,12 +372,12 @@ void OptionsHandler::showConfiguration(const std::string& option, exit(0); } -static void printTags(unsigned ntags, char const* const* tags) +static void printTags(const std::vector& tags) { std::cout << "available tags:"; - for (unsigned i = 0; i < ntags; ++ i) + for (const auto& t : tags) { - std::cout << " " << tags[i] << std::endl; + std::cout << " " << t << std::endl; } std::cout << std::endl; } @@ -393,8 +393,8 @@ void OptionsHandler::showDebugTags(const std::string& option, { throw OptionException("debug tags not available in non-tracing builds"); } - printTags(Configuration::getNumDebugTags(),Configuration::getDebugTags()); - exit(0); + printTags(Configuration::getDebugTags()); + std::exit(0); } void OptionsHandler::showTraceTags(const std::string& option, @@ -404,29 +404,17 @@ void OptionsHandler::showTraceTags(const std::string& option, { throw OptionException("trace tags not available in non-tracing build"); } - printTags(Configuration::getNumTraceTags(), Configuration::getTraceTags()); - exit(0); + printTags(Configuration::getTraceTags()); + std::exit(0); } -static std::string suggestTags(char const* const* validTags, +static std::string suggestTags(const std::vector& validTags, std::string inputTag, - char const* const* additionalTags) + const std::vector& additionalTags) { DidYouMean didYouMean; - - const char* opt; - for (size_t i = 0; (opt = validTags[i]) != nullptr; ++i) - { - didYouMean.addWord(validTags[i]); - } - if (additionalTags != nullptr) - { - for (size_t i = 0; (opt = additionalTags[i]) != nullptr; ++i) - { - didYouMean.addWord(additionalTags[i]); - } - } - + didYouMean.addWords(validTags); + didYouMean.addWords(additionalTags); return didYouMean.getMatchAsString(inputTag); } @@ -438,18 +426,17 @@ void OptionsHandler::enableTraceTag(const std::string& option, { throw OptionException("trace tags not available in non-tracing builds"); } - else if(!Configuration::isTraceTag(optarg.c_str())) + else if (!Configuration::isTraceTag(optarg)) { if (optarg == "help") { - printTags( - Configuration::getNumTraceTags(), Configuration::getTraceTags()); - exit(0); + printTags(Configuration::getTraceTags()); + std::exit(0); } throw OptionException( std::string("trace tag ") + optarg + std::string(" not available.") - + suggestTags(Configuration::getTraceTags(), optarg, nullptr)); + + suggestTags(Configuration::getTraceTags(), optarg, {})); } Trace.on(optarg); } @@ -467,14 +454,12 @@ void OptionsHandler::enableDebugTag(const std::string& option, throw OptionException("debug tags not available in non-tracing builds"); } - if (!Configuration::isDebugTag(optarg.c_str()) - && !Configuration::isTraceTag(optarg.c_str())) + if (!Configuration::isDebugTag(optarg) && !Configuration::isTraceTag(optarg)) { if (optarg == "help") { - printTags( - Configuration::getNumDebugTags(), Configuration::getDebugTags()); - exit(0); + printTags(Configuration::getDebugTags()); + std::exit(0); } throw OptionException(std::string("debug tag ") + optarg -- 2.30.2