From 4268c75087e2bb68dbb2257d99e062a8cc897f8c Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 21 May 2021 05:22:40 +0200 Subject: [PATCH] Move option names out of struct (#6554) This PR moves the option names out of the option struct (which will be removed) to free constexpr string constants. --- src/options/mkoptions.py | 8 ++++++-- src/options/module_template.h | 7 +++++++ src/options/options_handler.cpp | 8 ++++---- src/smt/options_manager.cpp | 28 ++++++++++++++-------------- 4 files changed, 31 insertions(+), 20 deletions(-) diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index a7212641c..b6efb1695 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -122,12 +122,13 @@ TPL_HOLDER_MACRO_ATTR += " bool {name}__setByUser__ = false;" TPL_HOLDER_MACRO_ATTR_DEF = " {type} {name} = {default};\\\n" TPL_HOLDER_MACRO_ATTR_DEF += " bool {name}__setByUser__ = false;" +TPL_NAME_DECL = 'static constexpr const char* {name}__name = "{long_name}";' + TPL_OPTION_STRUCT_RW = \ """extern struct {name}__option_t {{ typedef {type} type; type operator()() const; - static constexpr const char* name = "{long_name}"; }} thread_local {name};""" TPL_DECL_SET = \ @@ -563,6 +564,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): # *_options.h includes = set() holder_specs = [] + option_names = [] decls = [] specs = [] inls = [] @@ -597,6 +599,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): else: long_name = "" decls.append(tpl_decl.format(name=option.name, type=option.type, long_name = long_name)) + option_names.append(TPL_NAME_DECL.format(name=option.name, type=option.type, long_name = long_name)) # Generate module specialization specs.append(TPL_DECL_SET.format(name=option.name)) @@ -668,9 +671,10 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): id_cap=module.id_cap, id=module.id, includes='\n'.join(sorted(list(includes))), - holder_spec=' \\\n'.join(holder_specs), + holder_spec='\n'.join(holder_specs), decls='\n'.join(decls), specs='\n'.join(specs), + option_names='\n'.join(option_names), inls='\n'.join(inls), modes=''.join(mode_decl))) diff --git a/src/options/module_template.h b/src/options/module_template.h index 4e031d843..219775dd6 100644 --- a/src/options/module_template.h +++ b/src/options/module_template.h @@ -53,6 +53,13 @@ ${holder_spec}$ ${decls}$ // clang-format on +namespace ${id}$ +{ +// clang-format off +${option_names}$ +// clang-format on +} + } // namespace options // clang-format off diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index ee5396dff..b80e5a3b8 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -256,22 +256,22 @@ void OptionsHandler::setStats(const std::string& option, bool value) std::string opt = option.substr(2); if (value) { - if (opt == options::statisticsAll.name) + if (option == options::base::statisticsAll__name) { d_options->base().statistics = true; } - else if (opt == options::statisticsEveryQuery.name) + else if (option == options::base::statisticsEveryQuery__name) { d_options->base().statistics = true; } - else if (opt == options::statisticsExpert.name) + else if (option == options::base::statisticsExpert__name) { d_options->base().statistics = true; } } else { - if (opt == options::statistics.name) + if (option == options::base::statistics__name) { d_options->base().statisticsAll = false; d_options->base().statisticsEveryQuery = false; diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index 05bad2727..3fc58ff05 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -33,31 +33,31 @@ OptionsManager::OptionsManager(Options* opts) : d_options(opts) // set options that must take effect immediately if (opts->wasSetByUser(options::defaultExprDepth)) { - notifySetOption(options::defaultExprDepth.name); + notifySetOption(options::expr::defaultExprDepth__name); } if (opts->wasSetByUser(options::defaultDagThresh)) { - notifySetOption(options::defaultDagThresh.name); + notifySetOption(options::expr::defaultDagThresh__name); } if (opts->wasSetByUser(options::dumpModeString)) { - notifySetOption(options::dumpModeString.name); + notifySetOption(options::smt::dumpModeString__name); } if (opts->wasSetByUser(options::printSuccess)) { - notifySetOption(options::printSuccess.name); + notifySetOption(options::base::printSuccess__name); } if (opts->wasSetByUser(options::diagnosticChannelName)) { - notifySetOption(options::diagnosticChannelName.name); + notifySetOption(options::smt::diagnosticChannelName__name); } if (opts->wasSetByUser(options::regularChannelName)) { - notifySetOption(options::regularChannelName.name); + notifySetOption(options::smt::regularChannelName__name); } if (opts->wasSetByUser(options::dumpToFileName)) { - notifySetOption(options::dumpToFileName.name); + notifySetOption(options::smt::dumpToFileName__name); } // set this as a listener to be notified of options changes from now on opts->setListener(this); @@ -69,7 +69,7 @@ void OptionsManager::notifySetOption(const std::string& key) { Trace("smt") << "SmtEnginePrivate::notifySetOption(" << key << ")" << std::endl; - if (key == options::defaultExprDepth.name) + if (key == options::expr::defaultExprDepth__name) { int depth = (*d_options)[options::defaultExprDepth]; Debug.getStream() << expr::ExprSetDepth(depth); @@ -80,7 +80,7 @@ void OptionsManager::notifySetOption(const std::string& key) Warning.getStream() << expr::ExprSetDepth(depth); // intentionally exclude Dump stream from this list } - else if (key == options::defaultDagThresh.name) + else if (key == options::expr::defaultDagThresh__name) { int dag = (*d_options)[options::defaultDagThresh]; Debug.getStream() << expr::ExprDag(dag); @@ -91,12 +91,12 @@ void OptionsManager::notifySetOption(const std::string& key) Warning.getStream() << expr::ExprDag(dag); Dump.getStream() << expr::ExprDag(dag); } - else if (key == options::dumpModeString.name) + else if (key == options::smt::dumpModeString__name) { const std::string& value = (*d_options)[options::dumpModeString]; Dump.setDumpFromString(value); } - else if (key == options::printSuccess.name) + else if (key == options::base::printSuccess__name) { bool value = (*d_options)[options::printSuccess]; Debug.getStream() << Command::printsuccess(value); @@ -107,15 +107,15 @@ void OptionsManager::notifySetOption(const std::string& key) Warning.getStream() << Command::printsuccess(value); *options::out() << Command::printsuccess(value); } - else if (key == options::regularChannelName.name) + else if (key == options::smt::regularChannelName__name) { d_managedRegularChannel.set(options::regularChannelName()); } - else if (key == options::diagnosticChannelName.name) + else if (key == options::smt::diagnosticChannelName__name) { d_managedDiagnosticChannel.set(options::diagnosticChannelName()); } - else if (key == options::dumpToFileName.name) + else if (key == options::smt::dumpToFileName__name) { d_managedDumpChannel.set(options::dumpToFileName()); } -- 2.30.2