Refactor collection of debug and trace tags (#5996)

We have a mechanism to collect all debug and trace tags used throughout the code base to allow checking for valid tags.
This mechanism relies on a collection of more or less readable shell scripts.
#5921 hinted to a problem with the current setup, as it passes all source files via command line.
This PR refactors this setup so that the scripts collect the files internally, and only the base directory is passed on the command line.
As I was touching this code anyway, I ported everything to python and combined it into a single script, in the hope to make it more maintainable.
Fixes #5921.

7 files changed, 67 insertions, 160 deletions

diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt
index e28bd78cc..e73c82d76 100644
--- a/src/base/CMakeLists.txt
+++ b/src/base/CMakeLists.txt
@@ -40,9 +40,7 @@ libcvc4_add_sources(GENERATED git_versioninfo.cpp)
 #-----------------------------------------------------------------------------#
 # Generate code for debug/trace tags
 
-set(gentmptags_script ${CMAKE_CURRENT_LIST_DIR}/gentmptags.sh)
-set(gentags_script ${CMAKE_CURRENT_LIST_DIR}/gentags.sh)
-set(genheader_script ${CMAKE_CURRENT_LIST_DIR}/genheader.sh)
+set(collect_tags_script ${CMAKE_CURRENT_LIST_DIR}/collect_tags.py)
 
 file(GLOB_RECURSE source_files
      ${PROJECT_SOURCE_DIR}/src/*.cpp
@@ -52,41 +50,15 @@ file(GLOB_RECURSE source_files
 string(REPLACE ";" " " source_files_list "${source_files}")
 
 add_custom_command(
-  OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp
-  COMMAND
-    ${gentmptags_script} ${CMAKE_CURRENT_LIST_DIR} Debug ${source_files_list}
-  DEPENDS mktags ${gentmptags_script} ${source_files}
-)
-
-add_custom_command(
-  OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp
-  COMMAND
-    ${gentmptags_script} ${CMAKE_CURRENT_LIST_DIR} Trace ${source_files_list}
-  DEPENDS mktags ${gentmptags_script} ${source_files}
-)
-
-add_custom_command(
-  OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags
-  COMMAND ${gentags_script} Debug
-  DEPENDS ${gentags_script} ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp
-)
-
-add_custom_command(
-  OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags
-  COMMAND ${gentags_script} Trace
-  DEPENDS ${gentags_script} ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp
-)
-
-add_custom_command(
   OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.h
-  COMMAND ${genheader_script} ${CMAKE_CURRENT_LIST_DIR} Debug
-  DEPENDS mktagheaders ${genheader_script} ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags
+  COMMAND ${PYTHON_EXECUTABLE} ${collect_tags_script} ${CMAKE_CURRENT_BINARY_DIR}/ Debug ${PROJECT_SOURCE_DIR}/src
+  DEPENDS ${collect_tags_script} ${source_files}
 )
 
 add_custom_command(
   OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.h
-  COMMAND ${genheader_script} ${CMAKE_CURRENT_LIST_DIR} Trace
-  DEPENDS mktagheaders ${genheader_script} ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags
+  COMMAND ${PYTHON_EXECUTABLE} ${collect_tags_script} ${CMAKE_CURRENT_BINARY_DIR}/ Trace ${PROJECT_SOURCE_DIR}/src
+  DEPENDS ${collect_tags_script} ${source_files}
 )
 
 add_custom_target(gen-tags
diff --git a/src/base/collect_tags.py b/src/base/collect_tags.py
new file mode 100644
index 000000000..ea4938d6b
--- /dev/null
+++ b/src/base/collect_tags.py
@@ -0,0 +1,62 @@
+#!/usr/bin/env python3
+
+import argparse
+import glob
+import os
+import re
+import shutil
+import subprocess
+
+
+def parse_args():
+    """Parse command line arguments and return them."""
+    ap = argparse.ArgumentParser(description='collect debug and trace tags')
+    ap.add_argument('destdir', help='where to put the results')
+    ap.add_argument('type', choices=['Debug', 'Trace'], help='which tags to collect')
+    ap.add_argument('basedir', help='where to look for source file')
+    return ap.parse_args()
+
+
+def collect_tags(basedir):
+    """Collect all tags used in filed within the given base directory.
+    Return them sorted lexicographically."""
+    tags = set()
+    for ext in ['.cc', '.cpp', '.g', '.h']:
+        for filename in glob.iglob('{}/**/*{}'.format(basedir, ext), recursive=True):
+            content = open(filename).read()
+            for tag in RE_PAT.finditer(content):
+                tags.add(tag.group(1))
+    return sorted(tags)
+
+
+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))
+        for t in tags:
+            out.write('"{}",\n'.format(t))
+        out.write('nullptr\n')
+        out.write('};\n')
+
+
+if __name__ == '__main__':
+    # setup
+    opts = parse_args()
+    RE_PAT = re.compile('{}(?:\\.isOn)?\\("([^"]+)"\\)'.format(opts.type))
+    FILENAME_TMP = '{}/{}_tags.tmp'.format(opts.destdir, opts.type)
+    FILENAME_DEST = '{}/{}_tags.h'.format(opts.destdir, opts.type)
+
+    # collect tags
+    tags = collect_tags(opts.basedir)
+    # write header file
+    write_file(FILENAME_TMP, opts.type, tags)
+
+    if not os.path.isfile(FILENAME_DEST):
+        # file does not exist yet
+        shutil.copy(FILENAME_TMP, FILENAME_DEST)
+    elif subprocess.run(
+        ['diff', FILENAME_TMP, FILENAME_DEST],
+        stdout=subprocess.PIPE
+    ).returncode == 1:
+        # file needs to change
+        shutil.copy(FILENAME_TMP, FILENAME_DEST)
diff --git a/src/base/genheader.sh b/src/base/genheader.sh
deleted file mode 100755
index 2091f7781..000000000
--- a/src/base/genheader.sh
+++ /dev/null
@@ -1,21 +0,0 @@
-#!/bin/sh
-#
-# Convenience wrapper for cmake in src/base/CMakeLists.txt
-#
-# Create Debug_tags.h/Trace_tags.h header files.
-#
-# Usage: genheader.sh <directory-mktags> Debug|Trace
-
-path="$1"
-shift
-tags_type="$1" # Debug/Trace
-tags_file="${tags_type}_tags"
-
-if [ "${tags_type}" != "Debug" ] && [ "${tags_type}" != "Trace" ]; then
-  echo "$0: Invalid tags type '${tags_type}' (must be 'Debug' or 'Trace')"
-  exit 1
-fi
-
-[ ! -e "${tags_file}" ] && echo "$0: ${tags_file} does not exist" && exit 1
-
-"${path}/mktagheaders" "${tags_file}" "${tags_file}" > "${tags_file}.h"
diff --git a/src/base/gentags.sh b/src/base/gentags.sh
deleted file mode 100755
index 67888b3f5..000000000
--- a/src/base/gentags.sh
+++ /dev/null
@@ -1,26 +0,0 @@
-#!/bin/sh
-#
-# Convenience wrapper for cmake in src/base/CMakeLists.txt
-#
-# Update Debug_tags/Trace_tags in case that debug/trace tags have been
-# modified. Use diff to compare the contents of the *.tmp files with the
-# corresponding *_tags file.
-#
-# Usage: gentags.sh Debug|Trace
-
-tags_type="$1" # Debug/Trace
-tags_file="${tags_type}_tags"
-
-if [ "${tags_type}" != "Debug" ] && [ "${tags_type}" != "Trace" ]; then
-  echo "$0: Invalid tags type '${tags_type}' (must be 'Debug' or 'Trace')"
-  exit 1
-fi
-
-[ ! -e "${tags_file}.tmp" ] && \
-    echo "$0: ${tags_file}.tmp does not exist" && exit 1
-
-if [ -e "${tags_file}" ]; then
-  # Do not update file if tags didn't change.
-  diff -q "${tags_file}.tmp" "${tags_file}" > /dev/null 2>&1 && exit 0
-fi
-mv "${tags_file}.tmp" "${tags_file}"
diff --git a/src/base/gentmptags.sh b/src/base/gentmptags.sh
deleted file mode 100755
index 566fa1747..000000000
--- a/src/base/gentmptags.sh
+++ /dev/null
@@ -1,21 +0,0 @@
-#!/bin/sh
-#
-# Convenience wrapper for cmake in src/base/CMakeLists.txt
-#
-# Create Debug_tags.tmp/Trace_tags.tmp files from given source files.
-#
-# Usage: gentmptags.sh <directory-mktags> Debug|Trace <source files ...>
-
-path="$1"
-shift
-tags_type="$1"
-tags_file="${tags_type}_tags"
-shift
-source_files_list="$*"
-
-if [ "${tags_type}" != "Debug" ] && [ "${tags_type}" != "Trace" ]; then
-  echo "$0: Invalid tags type '${tags_type}' (must be 'Debug' or 'Trace')"
-  exit 1
-fi
-
-"${path}/mktags" "${tags_type}" "${source_files_list}" > "${tags_file}.tmp"
diff --git a/src/base/mktagheaders b/src/base/mktagheaders
deleted file mode 100755
index af44cee8d..000000000
--- a/src/base/mktagheaders
+++ /dev/null
@@ -1,24 +0,0 @@
-#!/bin/bash
-#
-# mktagheaders
-#
-# The purpose of this script is to generate the *_tag.h header file from the
-# *_tags file.
-#
-# Invocation:
-#
-#    mktagheaders <tag-name> <tag-file>
-#
-# <tag-name> will be the name of the generated array.
-# <tag-file> each line of this file is turned into a string in the generated
-#   array.
-
-TAG_NAME=$1
-TAG_FILE=$2
-
-echo 'static char const* const '$TAG_NAME'[] = {';
-for tag in `cat $TAG_FILE`; do
-  echo "\"$tag\",";
-done;
-echo 'NULL';
-echo '};'
diff --git a/src/base/mktags b/src/base/mktags
deleted file mode 100755
index 090e57014..000000000
--- a/src/base/mktags
+++ /dev/null
@@ -1,35 +0,0 @@
-#!/bin/bash
-#
-# mktags
-#
-# The purpose of this script is to create Debug_tags and Trace_tags files.
-# Note that in the Makefile workflow these are first stored in a *_tags.tmp
-# file. This file contains a list of all of the strings that occur in things
-# like Debug("foo") or Debug.isOn("bar") in a given directory. The list is
-# seperated by newlines.  The expected Debug_tags file for the previous two
-# tags would be:
-# bar
-# foo
-#
-# Invocation:
-#
-#    mktags {Debug,Trace} <input-files>
-#
-# <input-files> is expected to be passed a single space separated list of files.
-#  One can use quotes to achieve this. This is one reason to use "$(...)"
-#  instead of back ticks `...`.
-
-DebugOrTrace=$1
-InputFiles=$2
-
-grep -h '\<'$DebugOrTrace'\(\.isOn\)* *( *\".*\" *)' \
-  $InputFiles | \
-  sed 's/\/\/.*//;s/^'$DebugOrTrace'\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]'$DebugOrTrace'\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | \
-  LC_ALL=C sort | \
-  uniq
-
-
-# Reference copy of what this is replacing.
-# 	grep -h '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \
-#		`find @srcdir@/../ -name "*.cpp" -o -name "*.h" -o -name "*.cc" -o -name "*.g"` | \
-#	sed 's/\/\/.*//;s/^$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | LC_ALL=C sort | uniq