From 79bc44c7fb8ea2c3b8fdbb3d886628ed7634614e Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 21 Apr 2020 19:21:56 -0700 Subject: [PATCH 1/9] Clang Tidy test --- .github/workflows/ci.yml | 6 +++ .github/workflows/run-clang-tidy.py | 57 +++++++++++++++++++++++++++++ CMakeLists.txt | 2 + 3 files changed, 65 insertions(+) create mode 100755 .github/workflows/run-clang-tidy.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 810f4b925ea..84d0ed38ae2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -29,6 +29,7 @@ jobs: - name: debug config: debug --symfpu --lfsc --no-debug-symbols + run-clang-tidy: true cache-key: debug - name: debug-cln @@ -171,3 +172,8 @@ jobs: ctest -j2 --output-on-failure working-directory: examples + - name: Run Clang-Tidy + if: matrix.run-clang-tidy && runner.os == 'Linux' + run: | + ../.github/workflows/run-clang-tidy.py + working-directory: build diff --git a/.github/workflows/run-clang-tidy.py b/.github/workflows/run-clang-tidy.py new file mode 100755 index 00000000000..b609bc32650 --- /dev/null +++ b/.github/workflows/run-clang-tidy.py @@ -0,0 +1,57 @@ +#!/usr/bin/env python3 + +import requests +import os + + +def report_github_status(repo, token, sha, findings): + url = "https://api.github.com/repos/{}/check-runs".format(repo) + annotations = [] + for path, findings in findings.items(): + for f in findings: + annotations.append({ + 'path': path, + 'annotation_level': 'warning', + 'start_line': f.line, + 'end_line': f.line, + 'message': f.text + }) + + data = { + 'name': 'clang-tidy', + 'head_sha': sha, + 'status': 'completed', + 'conclusion': 'neutral', + 'output': { + 'title': 'clang-tidy', + 'summary': 'Found {} items'.format(len(annotations)), + 'annotations': annotations + } + } + + headers = { + 'Content-Type': 'application/json', + 'Accept': 'application/vnd.github.antiope-preview+json', + 'Authorization': 'Bearer {}'.format(token), + } + + r = requests.post(url, json=data, headers=headers) + + +def main(): + findings = { + 'CMakeLists': { + 'line': 5, + 'text': 'foo' + } + } + + if 'GITHUB_TOKEN' in os.environ: + repo = os.environ['GITHUB_REPOSITORY'] + sha = os.environ['GITHUB_SHA'] + token = os.environ['GITHUB_TOKEN'] + report_github_status(repo, token, sha, findings) + + +if __name__ == '__main__': + main() diff --git a/CMakeLists.txt b/CMakeLists.txt index c535890e184..b570a5b9cee 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -3,6 +3,8 @@ cmake_minimum_required(VERSION 3.2) #-----------------------------------------------------------------------------# # Project configuration +message("hello") + project(cvc4) set(CVC4_MAJOR 1) # Major component of the version of CVC4. From 73b137f2d1a47536a4248014cc40be7cc16343f7 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 21 Apr 2020 19:24:48 -0700 Subject: [PATCH 2/9] change --- .github/workflows/ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 84d0ed38ae2..a5f5ed057bc 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -49,6 +49,7 @@ jobs: sudo apt-get update sudo apt-get install -y \ ccache \ + clang-tidy \ cxxtest \ libcln-dev \ libgmp-dev \ From 3ab75b6bb0f64178e968bc193f5294ae38f213e3 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 21 Apr 2020 21:50:08 -0700 Subject: [PATCH 3/9] print info --- .github/workflows/run-clang-tidy.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/run-clang-tidy.py b/.github/workflows/run-clang-tidy.py index b609bc32650..7efadbc0786 100755 --- a/.github/workflows/run-clang-tidy.py +++ b/.github/workflows/run-clang-tidy.py @@ -36,6 +36,8 @@ def report_github_status(repo, token, sha, findings): } r = requests.post(url, json=data, headers=headers) + print(r) + print(r.text) def main(): From 7ab88ab8dc41162fee2dfc7a6804c9aa91586b93 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 21 Apr 2020 23:02:17 -0700 Subject: [PATCH 4/9] print all --- .github/workflows/ci.yml | 2 +- .github/workflows/run-clang-tidy.py | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a5f5ed057bc..d9bd00f5d51 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -143,7 +143,7 @@ jobs: run: ccache -s - name: Run CTest - run: make -j2 check + run: true env: ARGS: --output-on-failure -LE regress[1-4] CVC4_REGRESSION_ARGS: --no-early-exit diff --git a/.github/workflows/run-clang-tidy.py b/.github/workflows/run-clang-tidy.py index 7efadbc0786..6611f042c54 100755 --- a/.github/workflows/run-clang-tidy.py +++ b/.github/workflows/run-clang-tidy.py @@ -48,6 +48,7 @@ def main(): } } + print(os.environ) if 'GITHUB_TOKEN' in os.environ: repo = os.environ['GITHUB_REPOSITORY'] sha = os.environ['GITHUB_SHA'] From 49726734d89c284053788186bcf5d5a447649dcb Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 21 Apr 2020 23:18:17 -0700 Subject: [PATCH 5/9] gh token? --- .github/workflows/ci.yml | 2 ++ .github/workflows/run-clang-tidy.py | 1 - 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d9bd00f5d51..85132563b57 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -178,3 +178,5 @@ jobs: run: | ../.github/workflows/run-clang-tidy.py working-directory: build + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/.github/workflows/run-clang-tidy.py b/.github/workflows/run-clang-tidy.py index 6611f042c54..7efadbc0786 100755 --- a/.github/workflows/run-clang-tidy.py +++ b/.github/workflows/run-clang-tidy.py @@ -48,7 +48,6 @@ def main(): } } - print(os.environ) if 'GITHUB_TOKEN' in os.environ: repo = os.environ['GITHUB_REPOSITORY'] sha = os.environ['GITHUB_SHA'] From 4636322597769638a594911e787a68cccc18693e Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 21 Apr 2020 23:53:22 -0700 Subject: [PATCH 6/9] fix? --- .github/workflows/run-clang-tidy.py | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/.github/workflows/run-clang-tidy.py b/.github/workflows/run-clang-tidy.py index 7efadbc0786..8f1a01e4a23 100755 --- a/.github/workflows/run-clang-tidy.py +++ b/.github/workflows/run-clang-tidy.py @@ -1,8 +1,10 @@ #!/usr/bin/env python3 +import collections import requests import os +Finding = collections.namedtuple("Finding", ["line", "text"]) def report_github_status(repo, token, sha, findings): url = "https://api.github.com/repos/{}/check-runs".format(repo) @@ -42,10 +44,7 @@ def report_github_status(repo, token, sha, findings): def main(): findings = { - 'CMakeLists': { - 'line': 5, - 'text': 'foo' - } + 'CMakeLists': [Finding(5, 'foobar')] } if 'GITHUB_TOKEN' in os.environ: From c420f74ccad50de7f860b12f4cd251fe389e4b04 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 22 Apr 2020 00:13:41 -0700 Subject: [PATCH 7/9] change file name --- .github/workflows/run-clang-tidy.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/run-clang-tidy.py b/.github/workflows/run-clang-tidy.py index 8f1a01e4a23..13d9c784f28 100755 --- a/.github/workflows/run-clang-tidy.py +++ b/.github/workflows/run-clang-tidy.py @@ -44,7 +44,7 @@ def report_github_status(repo, token, sha, findings): def main(): findings = { - 'CMakeLists': [Finding(5, 'foobar')] + 'CMakeLists.txt': [Finding(5, 'foobar')] } if 'GITHUB_TOKEN' in os.environ: From 2203ac90903e6c0be018f57c2a67054a7b0a9ab0 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 22 Apr 2020 00:58:51 -0700 Subject: [PATCH 8/9] test --- .github/workflows/ci.yml | 4 +-- .github/workflows/run-clang-tidy.py | 44 ++++++++++++++++++++++++++--- src/prop/theory_proxy.cpp | 2 +- 3 files changed, 42 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 85132563b57..268191db3d8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -175,8 +175,6 @@ jobs: - name: Run Clang-Tidy if: matrix.run-clang-tidy && runner.os == 'Linux' - run: | - ../.github/workflows/run-clang-tidy.py - working-directory: build + run: .github/workflows/run-clang-tidy.py env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/.github/workflows/run-clang-tidy.py b/.github/workflows/run-clang-tidy.py index 13d9c784f28..309cef41bab 100755 --- a/.github/workflows/run-clang-tidy.py +++ b/.github/workflows/run-clang-tidy.py @@ -1,11 +1,48 @@ #!/usr/bin/env python3 import collections +import re import requests +import subprocess import os Finding = collections.namedtuple("Finding", ["line", "text"]) +def checkable_file(fn): + if any(fn.endswith(ext) for ext in ['.h', '.cpp']): + return '_template.' not in fn + return False + +def get_commit_files(sha): + cmd = ['git', 'diff-tree', '--no-commit-id', '--name-only', '-r', sha] + files = subprocess.check_output(cmd).decode().splitlines() + return [fn for fn in files if checkable_file(fn)] + +def parse_clang_output(output): + error_re = ".*:(\d+):\d+: (.*)" + out = [] + for l in output.splitlines(): + m = re.match(error_re, l) + if m: + line = int(m.group(1)) + msg = m.group(2) + out.append(Finding(line=line, text=msg)) + + return out + +def get_findings(files): + result = {} + for fn in files: + cmd = ['clang-tidy', '-p', 'build', fn] + proc = subprocess.Popen( + cmd, + stdin=subprocess.PIPE, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE) + out, err = proc.communicate() + result[fn] = parse_clang_output(out.decode()) + return result + def report_github_status(repo, token, sha, findings): url = "https://api.github.com/repos/{}/check-runs".format(repo) annotations = [] @@ -43,13 +80,12 @@ def report_github_status(repo, token, sha, findings): def main(): - findings = { - 'CMakeLists.txt': [Finding(5, 'foobar')] - } + sha = os.environ['GITHUB_SHA'] + files = get_commit_files(sha) + findings = get_findings(files) if 'GITHUB_TOKEN' in os.environ: repo = os.environ['GITHUB_REPOSITORY'] - sha = os.environ['GITHUB_SHA'] token = os.environ['GITHUB_TOKEN'] report_github_status(repo, token, sha, findings) diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 38c99f551aa..64886e15c37 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -87,7 +87,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: " << std::endl; - proofRecipe->dump("pf::sat"); + proofRecipe->dump("pf::satxx"); delete proofRecipe; proofRecipe = NULL; From 83717fb353f283ca6141e39f9a4fbb0e9d4e206a Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 22 Apr 2020 01:00:38 -0700 Subject: [PATCH 9/9] test2 --- .github/workflows/run-clang-tidy.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/run-clang-tidy.py b/.github/workflows/run-clang-tidy.py index 309cef41bab..6d2cdd99628 100755 --- a/.github/workflows/run-clang-tidy.py +++ b/.github/workflows/run-clang-tidy.py @@ -80,12 +80,13 @@ def report_github_status(repo, token, sha, findings): def main(): - sha = os.environ['GITHUB_SHA'] + sha = os.environ['GITHUB_BASE_REF'] files = get_commit_files(sha) findings = get_findings(files) if 'GITHUB_TOKEN' in os.environ: repo = os.environ['GITHUB_REPOSITORY'] + sha = os.environ['GITHUB_SHA'] token = os.environ['GITHUB_TOKEN'] report_github_status(repo, token, sha, findings)