|
| 1 | +# Coding conventions |
| 2 | + |
| 3 | +## Formatting |
| 4 | + |
| 5 | +We automate most of our formatting preferences. Our CI will run format checkers for PRs and pushes. |
| 6 | +These checks are required for merging any PR. |
| 7 | + |
| 8 | +For Rust, we use [rustfmt](https://github.com/rust-lang/rustfmt) |
| 9 | +which is configured via the [rustfmt.toml](https://github.com/model-checking/kani/blob/main/rustfmt.toml) file. |
| 10 | +We are also in the process of enabling `clippy`. |
| 11 | +Because of that, we still have a couple of lints disabled (see [.cargo/config](https://github.com/model-checking/kani/blob/main/.cargo/config.toml) for the updated list). |
| 12 | + |
| 13 | +We also have a bit of C and Python code in our repository. |
| 14 | +For C we use `clang-format` and for Python scripts we use `autopep8`. |
| 15 | +See [.clang-format](https://githubcom/model-checking/kani/blob/main/.clang-format) |
| 16 | +and [pyproject.toml](https://github.com/model-checking/kani/blob/main/scripts/pyproject.toml) |
| 17 | +for their configuration. |
| 18 | + |
| 19 | + |
| 20 | +### Exceptions |
| 21 | + |
| 22 | +We recognize that in some cases, the formatting and lints automation may not be applicable to a specific code. |
| 23 | +In those cases, we usually prefer explicitly allowing exceptions by locally disabling the check. |
| 24 | +E.g., use `#[allow]` annotation instead of disabling a link on a crate or project level. |
| 25 | + |
| 26 | +### Copyright notice |
| 27 | + |
| 28 | +All source code files begin with a copyright and license notice. If this is a new file, please add the following notice: |
| 29 | + |
| 30 | +```rust |
| 31 | +// Copyright Kani Contributors |
| 32 | +// SPDX-License-Identifier: Apache-2.0 OR MIT |
| 33 | +``` |
| 34 | + |
| 35 | +When modifying a file from another project, please keep their headers as is and append the following notice after them: |
| 36 | + |
| 37 | +```rust |
| 38 | +// ... existing licensing headers ... |
| 39 | + |
| 40 | +// Modifications Copyright Kani Contributors |
| 41 | +// See GitHub history for details. |
| 42 | +``` |
| 43 | + |
| 44 | +Note: The comment escape characters will depend on the type of file you are working with. E.g.: For rust start the |
| 45 | +header with `//`, but for python start with `#`. |
| 46 | + |
| 47 | +We also have automated checks for the copyright notice. |
| 48 | +There are a few file types where this rule doesn't apply. |
| 49 | +You can see that list in the [copyright-exclude]( |
| 50 | +https://github.com/model-checking/kani/blob/main/scripts/ci/copyright-exclude) file. |
| 51 | + |
| 52 | + |
| 53 | +## Code for soundness |
| 54 | + |
| 55 | +We are developing Kani to provide assurance that critical Rust components are verifiably free of certain classes of |
| 56 | +security and correctness issues. |
| 57 | +Thus, it is critical that we provide a verification tool that is sound. |
| 58 | +For the class of errors that Kani can verify, we should not produce a "No Error" result if there was in fact an |
| 59 | +error in the code being verified, i.e., it has no |
| 60 | +"False Negatives". |
| 61 | + |
| 62 | +Because of that, we bias on the side of correctness. |
| 63 | +Any incorrect modeling |
| 64 | +that may trigger an unsound analysis that cannot be fixed in the short term should be mitigated. |
| 65 | +Here are a few ways how we do that. |
| 66 | + |
| 67 | +### Compilation errors |
| 68 | + |
| 69 | +Make sure to add user-friendly errors for constructs that we can't handle. |
| 70 | +For example, Kani cannot handle the panic unwind strategy, and it will fail compilation if the crate uses this |
| 71 | +configuration. |
| 72 | + |
| 73 | +### Internal compiler errors |
| 74 | + |
| 75 | +Even though this doesn't provide users the best experience, you are encouraged to add checks in the compiler for any |
| 76 | +assumptions you make during development. |
| 77 | +Those check can be on the form of `assert!()` or `unreachable!()` |
| 78 | +statement. |
| 79 | +Please provide a meaningful message to help user understand why something failed, and try to explain, at least with |
| 80 | +a comment, why this is the case. |
| 81 | + |
| 82 | +We don't formally use any specific formal representation of [function contract](https://en.wikipedia.org/wiki/Design_by_contract), |
| 83 | +but whenever possible we do instrument the code with assertions that may represent the function pre- and |
| 84 | +post-conditions to ensure we are modeling the user code correctly. |
| 85 | + |
| 86 | +### Verification errors |
| 87 | + |
| 88 | +In cases where Kani fails to model a certain instruction or local construct that doesn't have a global effect, |
| 89 | +we encode this failure as a verification error. |
| 90 | +I.e., we generate an assertion failure instead of the construct we are modeling using |
| 91 | +[`codegen_unimplemented()`](https://github.com/model-checking/kani/blob/f719b565968568335d9be03ef27c5d05bb8fd0b7/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs#L50), |
| 92 | +which blocks the execution whenever this construct is reached. |
| 93 | + |
| 94 | +This will allow users to verify their crate successfully as long as |
| 95 | +that construct is not reachable in any harness. If a harness has at least one possible execution path that reaches |
| 96 | +such construct, Kani will fail the verification, and it will mark all checks, other than failed checks, with |
| 97 | +`UNDETERMINED` status. |
| 98 | + |
| 99 | +### Create detailed issues for "TODO" tasks |
| 100 | + |
| 101 | +It is OK to add "TODO" comments as long as they don't compromise user experience or the tool correctness. |
| 102 | +When doing so, please create an issue that captures the task. |
| 103 | +Add details about the task at hand including any impact to the user. |
| 104 | +Finally, add the link to the issue that captures the "TODO" task as part of your comment. |
| 105 | + |
| 106 | +E.g.: |
| 107 | +```rust |
| 108 | +// TODO: This function assumes type cannot be ZST. Check if that's always the case. |
| 109 | +// https://github.com/model-checking/kani/issues/XXXX |
| 110 | +assert!(!typ.is_zst(), "Unexpected ZST type"); |
| 111 | +``` |
| 112 | + |
| 113 | +## Performant but readable |
| 114 | + |
| 115 | +We aim at writing code that is performant but also readable and easy to maintain. |
| 116 | +Avoid compromising the code quality if the performance gain is not significant. |
| 117 | + |
| 118 | +Here are few tips that can help the readability of your code: |
| 119 | + |
| 120 | +- Sort match arms, enum variants, and struct fields alphabetically. |
| 121 | +- Prefer concise but meaningful names. |
| 122 | +- Prefer exhaustive matches. |
| 123 | +- Prefer declarative over imperative programming. |
0 commit comments