-
Notifications
You must be signed in to change notification settings - Fork 74
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #1192 from secure-sw-dev/3c-jan-2022-update
Update 3C conversion tool to latest changes from Correct Computation
- Loading branch information
Showing
226 changed files
with
8,297 additions
and
4,207 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,144 @@ | ||
# 3C Developer's Guide | ||
|
||
This file collects information that is important or useful to know | ||
when developing 3C as well as some standards we generally expect the | ||
code to follow. (Some other standards are covered in the [contribution | ||
guide](CONTRIBUTING.md)). If you could use help with something that's | ||
not documented here, feel free to ask. | ||
|
||
## Regression tests | ||
|
||
3C has a regression test suite located in `clang/test/3C`. The easiest | ||
way to run it is to run the following in your build directory: | ||
|
||
``` | ||
ninja check-3c | ||
``` | ||
|
||
This command will build everything needed that hasn't already been | ||
built, run the test suite, report success or failure (exit 0 or 1, so | ||
you can use it in scripts), and display some information about any | ||
failures, which may or may not be enough for you to understand what | ||
went wrong. | ||
|
||
For deeper troubleshooting, run the following in your build directory | ||
to build all dependencies of the test suite: | ||
|
||
``` | ||
ninja check-3c-deps | ||
``` | ||
|
||
Then run the following in the `clang/test/3C` directory: | ||
|
||
``` | ||
llvm-lit -vv TEST.c | ||
``` | ||
|
||
where `TEST.c` is the path of the test you want to run (you can also | ||
specify more than one test). This assumes you've put the `bin` | ||
subdirectory of your build directory on your `$PATH` or arranged some | ||
other means of running `llvm-lit` from there. The first `-v` makes | ||
`llvm-lit` display the stdout and stderr of failed tests; the second | ||
makes it display the `RUN` commands as they execute so you can tell | ||
which one failed. | ||
|
||
Every `.c` file under `clang/test/3C` is a test file. There are a few | ||
in subdirectories, so `*.c` will not pick up all of them; instead you | ||
can use `llvm-lit -vv .` to specify all test files under the current | ||
directory. | ||
|
||
### Diagnostic verification | ||
|
||
3C supports the standard Clang diagnostic verifier | ||
([`VerifyDiagnosticConsumer`](https://clang.llvm.org/doxygen/classclang_1_1VerifyDiagnosticConsumer.html#details)) | ||
for testing errors and warnings reported by 3C via its main `DiagnosticsEngine`. | ||
(Some 3C errors and warnings are reported via other means and cannot be tested | ||
this way; the best solution we have for them right now is to `grep` the stderr | ||
of 3C.) Diagnostic verification can be enabled via the usual `-Xclang -verify` | ||
compiler option; other diagnostic verification options (`-Xclang | ||
-verify=PREFIX`, etc.) should also work as normal. These must be passed as | ||
_compiler_ options, not `3c` options; for example, if you are using `--` on the | ||
`3c` command line, these options must be passed _after_ the `--`. | ||
|
||
Some notes about diagnostic verification in the context of 3C: | ||
|
||
* Parsing of the source files uses some of the compiler logic and thus may | ||
generate compiler warnings, just as if you ran `clang` on the code. These are | ||
sent to the diagnostic verifier along with diagnostics generated by 3C's | ||
analysis. If you find it distracting to have to include the compiler warnings | ||
in the set of expected diagnostics for a test, you can turn them off via the | ||
`-Wno-everything` compiler option (which does not affect diagnostics generated | ||
by 3C's analysis). | ||
|
||
* The `3c` tool works in several passes, where each pass runs on all translation | ||
units: first `3c` parses the source files, then it runs several passes of | ||
analysis. If a pass encounters at least one error, `3c` exits at the end of | ||
that pass. Diagnostic verification does not change the _point_ at which `3c` | ||
exits, but it changes the exit _code_ to indicate the result of verification | ||
rather than the presence of errors. The verification includes the diagnostics | ||
from all passes up to the point at which `3c` exits (i.e., the same | ||
diagnostics that would be displayed if verification were not used). However, | ||
an error that doesn't go via the main `DiagnosticsEngine` will cause an | ||
unsuccessful exit code regardless of diagnostic verification. (This is | ||
typically the behavior you want for a test.) | ||
|
||
* Diagnostic verification is independent for each translation unit, so in tests | ||
with multiple translation units, you'll have to be careful that preprocessing | ||
of each translation unit sees the correct set of `expected-*` directives for | ||
the diagnostics generated for that translation unit (or an | ||
`expected-no-diagnostics` directive if that translation unit generates no | ||
diagnostics, even if other translation units do generate diagnostics). Be | ||
warned that since which translation unit generated a given diagnostic isn't | ||
visible to a normal user, we don't put much work into coming up with sensible | ||
rules for this, but it should at least be deterministic for testing. | ||
|
||
Note that some 3C tests use diagnostic verification on calls to `clang` rather | ||
than `3c`, so if you see `expected-*` directives in a test, you can look at the | ||
`RUN` commands to see which command has `-Xclang -verify` and is using the | ||
directives. If you want to verify diagnostics of more than one `RUN` command in | ||
the same test, you can use different directive prefixes (`-Xclang | ||
-verify=PREFIX`). | ||
|
||
## Debugging | ||
|
||
### AST dumping | ||
|
||
`3c` honors the usual `-Xclang -ast-dump` compiler option to dump the | ||
AST to stdout before running its analysis. (This must be passed as a | ||
compiler option, not a `3c` option, e.g., _after_ the `--` on the | ||
command line if applicable.) The dump includes the AST node memory | ||
addresses (e.g., `VarDecl 0x5569e5ef3988 ...`), so if you see in the | ||
debugger that (for example) a `Decl *` variable in 3C has the value | ||
`0x5569e5ef3988`, you can look for that memory address in the AST dump | ||
to quickly see what AST node it is (modulo pointer adjustments for | ||
multiple inheritance; adding a debugger watch with a cast to the | ||
pointer type used in the AST dump can help with this). | ||
|
||
## Coding guidelines | ||
|
||
Please follow [LLVM coding | ||
standards](https://llvm.org/docs/CodingStandards.html#name-types-functions-variables-and-enumerators-properly) | ||
in your code. Specifically: | ||
|
||
* The maximum length of a line: 80 chars | ||
|
||
* All comments should start with a Capital letter. | ||
|
||
* All Local variables, including fields and parameters, should start | ||
with a Capital letter (similar to PascalCase). Short names are | ||
preferred. | ||
|
||
* A space between the conditional keyword and `(` i.e., `if (`, | ||
`while (`, ``for (` etc. | ||
|
||
* Space after the type name, i.e., `Type *K` _not_ `Type* K`. | ||
|
||
* Space before and after `:` in iterators, i.e., `for (auto &k : List)` | ||
|
||
Our goal is that all files should be formatted with `clang-format` and | ||
pass `clang-tidy` ([more information](clang-tidy.md)), and nonempty | ||
files should have a final newline (surprisingly, `clang-format` cannot | ||
enforce this). However, until we have better automation, we decided it | ||
isn't reasonable to require contributors to manually run these tools | ||
and fix style nits in each change; instead, we periodically run the | ||
tools on the entire 3C codebase. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.