From d7d4e67fdb049dc35dc5fbd61a702d789394bf3d Mon Sep 17 00:00:00 2001 From: Zain K Aamer Date: Wed, 29 Jan 2025 13:33:03 -0500 Subject: [PATCH] [CN-Test-Gen] Add `TESTING.md` --- backend/cn/TESTING.md | 45 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 backend/cn/TESTING.md diff --git a/backend/cn/TESTING.md b/backend/cn/TESTING.md new file mode 100644 index 000000000..7d5971594 --- /dev/null +++ b/backend/cn/TESTING.md @@ -0,0 +1,45 @@ +# CN Testing + +CN has testing capabilities available via the `cn test` subcommand. + +## Overview + +Currently, CN supports only per-function tests, but additional types of testing may become available in the future. + +Running `cn test ` generates C files with the testing infrastructure, the instrumented program under test, and a build script named `run_tests.sh`. +This script compiles the C files and runs the tests. + +By default, running `cn test` will automatically run `run_tests.sh`, which produces a test executable `tests.out`. +This can be disabled by using the `--no-run` flag. + +The output directory for these files can be set by using `--output-dir=`. +If the directory does not already exist, it is created. + +### Per-function tests + +When testing, there are currently two types of tests, constant tests and generator-based tests. +For *each function with a body*, CN will create either a constant test or generator-based test. + +If a function takes no arguments, does not use accesses on global variables, and is correct, it should always return the same value and free any memory it allocates. +In this case, a constant test is generated, which runs the function once and uses [Fulminate](FULMINATE_README.md) to check for post-condition violations. + +In all other cases, it creates generator-based tests, which are in the style of property-based testing. +A "generator" is created, which randomly generates function arguments, values for globals accessed and heap states, all of which adhere to the given function's pre-condition. +It calls the function with this input and uses [Fulminate](FULMINATE_README.md) similar to the constant tests. + +#### Understanding errors + +Currently, the tool does not print out counterexamples, but this is [planned](https://github.com/rems-project/cerberus/issues/841). +Until then, `tests.out` can be run with the `--trap` flag in a debugger. +Since seeds are printed each time the tool runs, `--seed ` can be used to reproduce the test case. +The debugger should automatically pause right before rerunning the failing test case. + +#### Writing custom tests + +There is currently no way to write custom property-based tests. +However, once lemmas can be tested, a lemma describing the desired property could be written to test it. + +In terms of unit tests, one can simply define a function that performs the desired operations. +This function will get detected by `cn test` and turned into a constant test. +Any assertions that one would make about the result would have to be captured by the post-condition. +In the future, existing infrastructure like `cn_assert` might be adapted for general use.