From a3da9245a4dab1f24af304361403dedd5d2e557e Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Wed, 23 Mar 2022 16:42:21 -0400 Subject: [PATCH] Restore copyright check (#975) * Add script for copyright check and extend for modified headers * Simplify copyright step in workflow * Add copyright header to files that were missing it * Use variable to determine exit code --- .github/workflows/format-check.yml | 10 +- Cargo.toml | 3 + .../getting-started/result-types/Cargo.toml | 3 + .../getting-started/result-types/src/main.rs | 3 + rustfmt.toml | 3 + scripts/ci/copyright-exclude | 19 ++++ scripts/ci/copyright_check.py | 94 +++++++++++++++---- scripts/ci/run-copyright-check.sh | 16 ++++ tests/cargo-kani/assert-reach/Cargo.toml | 3 + tests/cargo-kani/assert-reach/foo/Cargo.toml | 3 + tests/cargo-kani/assert-reach/foo/src/lib.rs | 3 + tests/cargo-kani/assert-reach/src/lib.rs | 3 + tests/cargo-kani/output-format/Cargo.toml | 3 + tests/cargo-kani/output-format/src/main.rs | 3 + tests/cargo-kani/rectangle-example/Cargo.toml | 3 + tests/kani/ForeignItems/lib.c | 3 + 16 files changed, 149 insertions(+), 26 deletions(-) create mode 100644 scripts/ci/copyright-exclude create mode 100755 scripts/ci/run-copyright-check.sh diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index aca86c067f22..925bd97ce253 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -10,16 +10,8 @@ jobs: - name: Checkout Kani uses: actions/checkout@v2 - - name: Get paths for files added - id: git-diff - run: | - ignore='(.clang-format|.diff|.md|.props|expected|ignore|gitignore|Cargo.lock)$' - files=$(git diff --ignore-submodules=all --name-only --diff-filter=A ${{ github.event.pull_request.base.sha }} ${{ github.event.pull_request.head.sha }} | grep -v -E $ignore | xargs) - echo "::set-output name=paths::$files" - - name: Execute copyright check - if: ${{ steps.git-diff.outputs.paths }} - run: ./scripts/ci/copyright_check.py ${{ steps.git-diff.outputs.paths }} + run: ./scripts/ci/run-copyright-check.sh - name: Check C code formatting run: ./scripts/run-clang-format.sh -d diff --git a/Cargo.toml b/Cargo.toml index 5f83f91ad1d6..cc609ff409e1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 OR MIT + [workspace] members = [ "library/kani", diff --git a/docs/src/getting-started/result-types/Cargo.toml b/docs/src/getting-started/result-types/Cargo.toml index c12543b0b35f..8c3298b69b06 100644 --- a/docs/src/getting-started/result-types/Cargo.toml +++ b/docs/src/getting-started/result-types/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "result-types" version = "0.1.0" diff --git a/docs/src/getting-started/result-types/src/main.rs b/docs/src/getting-started/result-types/src/main.rs index 943c29ce3f2c..ff3986a5d19e 100644 --- a/docs/src/getting-started/result-types/src/main.rs +++ b/docs/src/getting-started/result-types/src/main.rs @@ -1,3 +1,6 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + #[kani::proof] // ANCHOR: success_example fn success_example() { diff --git a/rustfmt.toml b/rustfmt.toml index 979df8dee6a6..f196c0471624 100644 --- a/rustfmt.toml +++ b/rustfmt.toml @@ -1,3 +1,6 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 OR MIT + # Run rustfmt with this config (it should be picked up automatically). version = "Two" use_small_heuristics = "Max" diff --git a/scripts/ci/copyright-exclude b/scripts/ci/copyright-exclude new file mode 100644 index 000000000000..e5b63a0988fc --- /dev/null +++ b/scripts/ci/copyright-exclude @@ -0,0 +1,19 @@ +.clang-format +.diff +.md +.props +expected +ignore +editorconfig +gitignore +gitattributes +gitmodules +LICENSE-APACHE +LICENSE-MIT +Cargo.lock +.svg +.png +.woff +scripts/ci/copyright-exclude +tools/bookrunner/librustdoc +tools/bookrunner/rust-doc \ No newline at end of file diff --git a/scripts/ci/copyright_check.py b/scripts/ci/copyright_check.py index c3aa9127380b..7a9ef345213d 100755 --- a/scripts/ci/copyright_check.py +++ b/scripts/ci/copyright_check.py @@ -4,18 +4,42 @@ import re import sys import os.path as path +from enum import Enum -def copyright_check(filename): - # Only check regular files (skip symbolic link to directories) - if not path.isfile(filename): - return True +STANDARD_HEADER_PATTERN_1 = '(//|#) Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.' +STANDARD_HEADER_PATTERN_2 = '(//|#) SPDX-License-Identifier: Apache-2.0 OR MIT' + +MODIFIED_HEADER_PATTERN_1 = '(//|#) SPDX-License-Identifier: Apache-2.0 OR MIT' +MODIFIED_HEADER_PATTERN_2 = '(//|#)' +MODIFIED_HEADER_PATTERN_3 = '(//|#) Modifications Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.' +MODIFIED_HEADER_PATTERN_4 = '(//|#) See GitHub history for details.' + +class CheckResult(Enum): + FAIL = 1 + PASS_STANDARD = 2 + PASS_MODIFIED = 3 +def matches_header_lines(header, lines): + matches = [regex.search(lines[idx]) for (regex, idx) in header] + return all(matches) + +def get_header(has_shebang, regexes): + init_idx = 0 if not has_shebang else 1 + indices = range(init_idx, init_idx + len(regexes)) + return zip(regexes, indices) + +def result_into_bool(result): + if result == CheckResult.FAIL: + return False + return True + +def copyright_check(filename): fo = open(filename) lines = fo.readlines() # The check is failed if the file is empty if len(lines) == 0: - return False + return CheckResult.FAIL # Scripts may include in their first line a character sequence starting with # '#!' (also know as shebang) to indicate an interpreter for execution. @@ -27,31 +51,67 @@ def copyright_check(filename): # The check is failed if the file does not contain enough lines if len(lines) < min_lines: - return False + return CheckResult.FAIL - # Compile the regexes for copyright lines - fst_re = re.compile('(//|#) Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.') - snd_re = re.compile('(//|#) SPDX-License-Identifier: Apache-2.0 OR MIT') + # Compile the regexes for the standard header + regexes = [] + regexes.append(re.compile(STANDARD_HEADER_PATTERN_1)) + regexes.append(re.compile(STANDARD_HEADER_PATTERN_2)) - fst_idx = min_lines - 2 - snd_idx = min_lines - 1 + # We define a header as a list of pairs `(regex, idx)` + # where `regex` is matched against `lines[idx]` + header = get_header(has_shebang, regexes) # The copyright check succeeds if the regexes can be found - if fst_re.search(lines[fst_idx]) and snd_re.search(lines[snd_idx]): - return True - else: - return False + if matches_header_lines(header, lines): + return CheckResult.PASS_STANDARD + + # If there was no match, this may be a modified file which + # includes a 4-lines header (i.e., `min_lines` is greater) + min_lines = 5 if has_shebang else 4 + + # The check is failed if the file does not contain enough lines + if len(lines) < min_lines: + return CheckResult.FAIL + + # Compile the regexes for the modified header + regexes = [] + regexes.append(re.compile(MODIFIED_HEADER_PATTERN_1)) + regexes.append(re.compile(MODIFIED_HEADER_PATTERN_2)) + regexes.append(re.compile(MODIFIED_HEADER_PATTERN_3)) + regexes.append(re.compile(MODIFIED_HEADER_PATTERN_4)) + + header = get_header(has_shebang, regexes) + + if matches_header_lines(header, lines): + return CheckResult.PASS_MODIFIED + + # We fail if there were no matches + return CheckResult.FAIL if __name__ == "__main__": filenames = sys.argv[1:] + + # Only check regular files (skip symbolic link to directories) + filenames = [fname for fname in filenames if path.isfile(fname)] + + # Get the copyright check for each file checks = [copyright_check(fname) for fname in filenames] + all_checks_pass = True for i in range(len(filenames)): print(f'Copyright check - {filenames[i]}: ', end='') - print('PASS') if checks[i] else print('FAIL') - if all(checks): + if checks[i] == CheckResult.PASS_STANDARD: + print('PASS') + elif checks[i] == CheckResult.PASS_MODIFIED: + print('PASS (MODIFIED)') + else: + all_checks_pass = False + print('FAIL') + + if all_checks_pass: sys.exit(0) else: sys.exit(1) diff --git a/scripts/ci/run-copyright-check.sh b/scripts/ci/run-copyright-check.sh new file mode 100755 index 000000000000..da44ec8a8efd --- /dev/null +++ b/scripts/ci/run-copyright-check.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -o errexit +set -o pipefail +set -o nounset + +CI_SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" +export PATH=$CI_SCRIPT_DIR:$PATH +KANI_DIR=$CI_SCRIPT_DIR/../.. + +# Filter the files for copyright check based on the patterns in `copyright-exclude` +# Exclude rustdoc to reduce conflicts for now: +# https://github.com/model-checking/kani/issues/974 +git ls-files $KANI_DIR | grep -v -E -f $CI_SCRIPT_DIR/copyright-exclude | xargs ./scripts/ci/copyright_check.py diff --git a/tests/cargo-kani/assert-reach/Cargo.toml b/tests/cargo-kani/assert-reach/Cargo.toml index bb358ee8b126..d9c6e1f76385 100644 --- a/tests/cargo-kani/assert-reach/Cargo.toml +++ b/tests/cargo-kani/assert-reach/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "bar" version = "0.1.0" diff --git a/tests/cargo-kani/assert-reach/foo/Cargo.toml b/tests/cargo-kani/assert-reach/foo/Cargo.toml index 1d9cfe3176c1..5382aec0e26a 100644 --- a/tests/cargo-kani/assert-reach/foo/Cargo.toml +++ b/tests/cargo-kani/assert-reach/foo/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "foo" version = "0.1.0" diff --git a/tests/cargo-kani/assert-reach/foo/src/lib.rs b/tests/cargo-kani/assert-reach/foo/src/lib.rs index ec458ec26f68..9c9e1d409fdb 100644 --- a/tests/cargo-kani/assert-reach/foo/src/lib.rs +++ b/tests/cargo-kani/assert-reach/foo/src/lib.rs @@ -1,3 +1,6 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + pub fn foo(x: u32) -> u32 { let y = x / 2; let z = y * 2; diff --git a/tests/cargo-kani/assert-reach/src/lib.rs b/tests/cargo-kani/assert-reach/src/lib.rs index 9c4b67cd594b..f9ce54fe5764 100644 --- a/tests/cargo-kani/assert-reach/src/lib.rs +++ b/tests/cargo-kani/assert-reach/src/lib.rs @@ -1,3 +1,6 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + #[kani::proof] fn test() { let x = 4; diff --git a/tests/cargo-kani/output-format/Cargo.toml b/tests/cargo-kani/output-format/Cargo.toml index 2ac2a4ab5641..d7d5da9c8a0e 100644 --- a/tests/cargo-kani/output-format/Cargo.toml +++ b/tests/cargo-kani/output-format/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "output-format" version = "0.1.0" diff --git a/tests/cargo-kani/output-format/src/main.rs b/tests/cargo-kani/output-format/src/main.rs index 733139168be7..05bcce27d05e 100644 --- a/tests/cargo-kani/output-format/src/main.rs +++ b/tests/cargo-kani/output-format/src/main.rs @@ -1,3 +1,6 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + fn main() { assert!(1 + 1 == 2); } diff --git a/tests/cargo-kani/rectangle-example/Cargo.toml b/tests/cargo-kani/rectangle-example/Cargo.toml index ca5ab1bbcd70..730687bb91bb 100644 --- a/tests/cargo-kani/rectangle-example/Cargo.toml +++ b/tests/cargo-kani/rectangle-example/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "rectangle-example" version = "0.1.0" diff --git a/tests/kani/ForeignItems/lib.c b/tests/kani/ForeignItems/lib.c index 201ac4099119..0ce63dfd1194 100644 --- a/tests/kani/ForeignItems/lib.c +++ b/tests/kani/ForeignItems/lib.c @@ -1,3 +1,6 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + #include #include #include