diff options
| -rw-r--r-- | src/Makefile.am | 4 | ||||
| -rw-r--r-- | src/util/Makefile.am | 46 | ||||
| -rw-r--r-- | src/util/configuration.cpp | 40 | ||||
| -rw-r--r-- | src/util/configuration.h | 6 | ||||
| -rw-r--r-- | src/util/options.cpp | 36 |
5 files changed, 110 insertions, 22 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 9ffe249ee..e6c00c943 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -78,9 +78,11 @@ subversion_versioninfo.cpp: svninfo echo "const unsigned ::CVC4::Configuration::SUBVERSION_REVISION = $$rev;"; \ echo "const bool ::CVC4::Configuration::SUBVERSION_HAS_MODIFICATIONS = $$mods;"; \ ) >"$@" +# This .tmp business is to keep from having to re-compile options.cpp +# (and then re-link the libraries) if nothing has changed. svninfo: svninfo.tmp $(AM_V_GEN)diff -q svninfo.tmp svninfo &>/dev/null || mv svninfo.tmp svninfo || true -# .PHONY ensures it's always rebuilt +# .PHONY ensures the .tmp version is always rebuilt (to check for any changes) .PHONY: svninfo.tmp svninfo.tmp: $(AM_V_GEN)(cd "$(top_srcdir)" && svn info && echo "Modifications: `test -z \"\`svn status -q\`\" && echo false || echo true`") >"$@" 2>/dev/null || true diff --git a/src/util/Makefile.am b/src/util/Makefile.am index bf975d513..7f5fb459e 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -75,14 +75,31 @@ libutilcudd_la_SOURCES = \ BUILT_SOURCES = \ rational.h \ integer.h \ - tls.h \ - debug_tags.h + tls.h +if CVC4_DEBUG +# listing Debug_tags too ensures that make doesn't auto-remove it +# after building (if it does, we don't get the "cached" effect with +# the .tmp files below, and we have to re-compile and re-link each +# time, even when there are no changes). +BUILT_SOURCES += \ + Debug_tags.h \ + Debug_tags +endif +if CVC4_TRACING +# listing Trace_tags too ensures that make doesn't auto-remove it +# after building (if it does, we don't get the "cached" effect with +# the .tmp files below, and we have to re-compile and re-link each +# time, even when there are no changes). +BUILT_SOURCES += \ + Trace_tags.h \ + Trace_tags +endif -debug_tags.h: debug_tags +%_tags.h: %_tags $(AM_V_GEN)( \ - echo 'const char* debug_tags[] = {'; \ + echo 'static char const *const $^[] = {'; \ first=1; \ - for tag in `cat debug_tags`; \ + for tag in `cat $^`; \ do \ if [ $$first -eq 1 ]; then first=0; else echo ','; fi; \ echo -n "\"$$tag\""; \ @@ -90,14 +107,19 @@ debug_tags.h: debug_tags echo; \ echo '};' \ ) >"$@" - -debug_tags: - $(AM_V_GEN)\ - grep 'Debug(\".*\")' `find @srcdir@/../ -name "*.cpp" -or -name "*.h" -or -name "*.cc" -or -name "*.g"` | \ - sed s/'.*Debug(\"'//g | sed s/'\".*'//g | sort | uniq >"$@" - -.PHONY: debug_tags +# This .tmp business is to keep from having to re-compile options.cpp +# (and then re-link the libraries) if nothing has changed. +%_tags: %_tags.tmp + $(AM_V_GEN)\ + diff -q "$^" "$@" &>/dev/null || mv "$^" "$@" || true +# .PHONY ensures the .tmp version is always rebuilt (to check for any changes) +.PHONY: Debug_tags.tmp Trace_tags.tmp +Debug_tags.tmp Trace_tags.tmp: + $(AM_V_GEN)\ + grep '\<$(@:_tags.tmp=) *( *\".*\" *)' \ + `find @srcdir@/../ -name "*.cpp" -or -name "*.h" -or -name "*.cc" -or -name "*.g"` | \ + sed 's/.*\<$(@:_tags.tmp=) *( *\"\([^"]*\)\".*/\1/g' | sort | uniq >"$@" if CVC4_CLN_IMP libutil_la_SOURCES += \ diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index c13b63e3f..062aca478 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -25,6 +25,14 @@ #include "util/configuration_private.h" #include "cvc4autoconfig.h" +#ifdef CVC4_DEBUG +# include "util/Debug_tags.h" +#endif /* CVC4_DEBUG */ + +#ifdef CVC4_TRACING +# include "util/Trace_tags.h" +#endif /* CVC4_TRACING */ + using namespace std; namespace CVC4 { @@ -117,6 +125,38 @@ bool Configuration::isBuiltWithTlsSupport() { return USING_TLS; } +unsigned Configuration::getNumDebugTags() { +#if CVC4_DEBUG + return sizeof(Debug_tags) / sizeof(Debug_tags[0]); +#else /* CVC4_DEBUG */ + return 0; +#endif /* CVC4_DEBUG */ +} + +char const* const* Configuration::getDebugTags() { +#if CVC4_DEBUG + return Debug_tags; +#else /* CVC4_DEBUG */ + return NULL; +#endif /* CVC4_DEBUG */ +} + +unsigned Configuration::getNumTraceTags() { +#if CVC4_TRACING + return sizeof(Trace_tags) / sizeof(Trace_tags[0]); +#else /* CVC4_TRACING */ + return 0; +#endif /* CVC4_TRACING */ +} + +char const* const* Configuration::getTraceTags() { +#if CVC4_TRACING + return Trace_tags; +#else /* CVC4_TRACING */ + return NULL; +#endif /* CVC4_TRACING */ +} + bool Configuration::isSubversionBuild() { return IS_SUBVERSION_BUILD; } diff --git a/src/util/configuration.h b/src/util/configuration.h index cb207298c..b4caf842c 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -87,6 +87,12 @@ public: static bool isBuiltWithTlsSupport(); + static unsigned getNumDebugTags(); + static char const* const* getDebugTags(); + + static unsigned getNumTraceTags(); + static char const* const* getTraceTags(); + static bool isSubversionBuild(); static const char* getSubversionBranchName(); static unsigned getSubversionRevision(); diff --git a/src/util/options.cpp b/src/util/options.cpp index a6042c3a9..009bc73b8 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -32,7 +32,6 @@ #include "util/language.h" #include "util/options.h" #include "util/output.h" -#include "util/debug_tags.h" #include "cvc4autoconfig.h" @@ -117,7 +116,8 @@ static const string optionsDescription = "\ --quiet | -q decrease verbosity (may be repeated)\n\ --trace | -t trace something (e.g. -t pushpop), can repeat\n\ --debug | -d debug something (e.g. -d arith), can repeat\n\ - --show-debug-tags show all avalable tags for debug tracing\n\ + --show-debug-tags show all avalable tags for debugging\n\ + --show-trace-tags show all avalable tags for tracing\n\ --stats give statistics on exit\n\ --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\ --print-expr-types print types with variables when printing exprs\n\ @@ -270,6 +270,7 @@ enum OptionValue { NO_THEORY_REGISTRATION, USE_MMAP, SHOW_DEBUG_TAGS, + SHOW_TRACE_TAGS, SHOW_CONFIG, STRICT_PARSING, DEFAULT_EXPR_DEPTH, @@ -331,7 +332,8 @@ static struct option cmdlineOptions[] = { { "stats" , no_argument , NULL, STATS }, { "no-checking", no_argument , NULL, NO_CHECKING }, { "no-theory-registration", no_argument, NULL, NO_THEORY_REGISTRATION }, - { "show-debug-tags", no_argument, NULL, SHOW_DEBUG_TAGS }, + { "show-debug-tags", no_argument , NULL, SHOW_DEBUG_TAGS }, + { "show-trace-tags", no_argument , NULL, SHOW_TRACE_TAGS }, { "show-config", no_argument , NULL, SHOW_CONFIG }, { "segv-nospin", no_argument , NULL, SEGV_NOSPIN }, { "help" , no_argument , NULL, 'h' }, @@ -768,15 +770,31 @@ throw(OptionException) { break; case SHOW_DEBUG_TAGS: - printf("available tags:"); - if (Configuration::isTracingBuild()) { - unsigned nTags = sizeof(debug_tags) / sizeof(debug_tags[0]); - for (unsigned i = 0; i < nTags; ++ i) { - printf(" %s", debug_tags[i]); + if(Configuration::isDebugBuild()) { + printf("available tags:"); + unsigned ntags = Configuration::getNumDebugTags(); + char const* const* tags = Configuration::getDebugTags(); + for(unsigned i = 0; i < ntags; ++ i) { + printf(" %s", tags[i]); } printf("\n"); } else { - printf(" not available in this build"); + throw OptionException("debug tags not available in non-debug build"); + } + exit(0); + break; + + case SHOW_TRACE_TAGS: + if(Configuration::isTracingBuild()) { + printf("available tags:"); + unsigned ntags = Configuration::getNumTraceTags(); + char const* const* tags = Configuration::getTraceTags(); + for (unsigned i = 0; i < ntags; ++ i) { + printf(" %s", tags[i]); + } + printf("\n"); + } else { + throw OptionException("trace tags not available in non-tracing build"); } exit(0); break; |