Merge branch 'main' into output-improvements

.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

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",

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"

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() {

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"

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

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)

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

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"

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"

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;

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;

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"

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);
 }

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"

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 <assert.h>
 #include <stdarg.h>
 #include <stdint.h>