Bounded model checking is unit testing with superpowers. Thanks to symbolic simulation, you can test thousands – or billions – of cases simultaneously. You spend less time writing tests and more time finding broken edge cases.
I want to share a technique for applying bounded model checking that I recently started using. The advantages of this new technique are simplicity, flexibility, and clarity.
While it’s possible to run CBMC on entire programs, this is often impractical because whole programs can be slow to simulate. It also doesn’t apply to libraries. The more generic way to use CBMC is to create a set of carefully chosen entrypoints, which are called “harnesses” in CBMC’s documentation.
In some cases you might be able to use a function from your codebase directly as an entrypoint, but more generally you’ll want an entrypoint that is specifically crafted for CBMC. The reason is because that’s sometimes the only way you can express the properties you’re interested in.
One trick I figured out is to use a macro to selectively define the test harness functions in the source files. Something like this:
#ifdef CBMC_TEST
void
assert_float_from_int16_is_monotonic(void)
{
int16_t x, y;
__CPROVER_assume(x <= y);
assert(float_from_int16(x) <= float_from_int16(y));
}
#endif
In a production build, the test harness assert_float_from_int16_is_monotonic
doesn’t exist. But when running CBMC, it can be included by adding the
-D CBMC_TEST option.
I love how this approach puts code and specs in the same file! I think this is a great example of how advanced tooling can ease the life of a software developer.
It also helps to use a really nice build system, like Meson. Meson makes it easy to write correct build system code. I didn’t fully appreciate this until I tried to implement this CBMC technique with CMake. I got it working, but it wasn’t intuitive.
In Meson, it’s easy to define a set of entrypoints as a list, then iterate over it to declare a set of tests.
entry_points = [
'assert_float_from_int16_is_monotonic',
'assert_float_from_int16_is_injective',
'assert_float_from_int16_inverse',
]
foreach entry_point : entry_points
test(entry_point,
cbmc,
args: [
'-I', meson.current_source_dir(),
'--bounds-check',
'--compact-trace',
'--conversion-check',
'-D', 'CBMC_TEST',
'--div-by-zero-check',
'--enum-range-check',
'--float-overflow-check',
'--function', entry_point,
'--memory-leak-check',
'--nan-check',
'--pointer-check',
'--pointer-overflow-check',
'--signed-overflow-check',
'--undefined-shift-check',
'--unsigned-overflow-check',
sources,
],
)
endforeach
I probably have too many checks in here. The next step would be to let the set of checks vary by entrypoint. Meson’s support for dictionaries makes this improvement trivial.
I’m amazed by CBMC’s ability to add constraints (“nonfunctional requirements”) to software without changing the programming language. This reminds me of Rich Hickey’s opinion about type systems: he doesn’t want two languages – one for types, one for values – in one language (Clojure, in his case). Efforts to add constraints to systems programming languages (C++, Rust) have necessarily entailed syntactic complexity. You need a language to express the constraints!
CBMC’s approach refreshingly differs. You use C syntax to write both code and constraints. What’s different and brilliant is that your target has changed from C’s abstract machine to a nondeterministic abstract machine.
Developments like Meson and CBMC remind me that improvement is possible and actual. These improvements directly impact the wellbeing of embedded software engineers and the quality of their work.
Discuss this page by emailing my public inbox. Please note the etiquette guidelines.
© 2024 Karl Schultheisz