From 9e6e35ff818d67444410b97f2d3e01cfbee3ef55 Mon Sep 17 00:00:00 2001 From: "Mark R. Tuttle" Date: Wed, 21 Sep 2022 21:33:47 -0400 Subject: [PATCH 01/14] Correct doxygen \page commands in architectural documentation * Replace top-level section headings with \page command * Ensure a space between \ingroup and \page for pandoc parsing * Remove link to cprover-manual index from memory-analyzer, restrict-function pointer, etc, and make these pages subpages of the top-level architectural page --- doc/architectural/background-concepts.md | 1 + doc/architectural/cbmc-architecture.md | 1 + doc/architectural/code-walkthrough.md | 1 + .../compilation-and-development.md | 1 + doc/architectural/folder-walkthrough.md | 1 + doc/architectural/front-page.md | 10 +- doc/architectural/howto.md | 1 + doc/architectural/memory-analyzer.md | 3 +- doc/architectural/memory-bounds-checking.md | 1 + doc/architectural/nondet-volatile.md | 136 +++++++++++++ doc/architectural/other-tools.md | 1 + .../restrict-function-pointer.md | 182 ++++++++++++++++++ 12 files changed, 335 insertions(+), 4 deletions(-) create mode 100644 doc/architectural/nondet-volatile.md create mode 100644 doc/architectural/restrict-function-pointer.md diff --git a/doc/architectural/background-concepts.md b/doc/architectural/background-concepts.md index ba5f13206a0..f7a352aac34 100644 --- a/doc/architectural/background-concepts.md +++ b/doc/architectural/background-concepts.md @@ -1,4 +1,5 @@ \ingroup module_hidden + \page background-concepts Background Concepts \author Martin Brain, Peter Schrammel, Johannes Kloos diff --git a/doc/architectural/cbmc-architecture.md b/doc/architectural/cbmc-architecture.md index 143f789c04b..89cd8eb7a78 100644 --- a/doc/architectural/cbmc-architecture.md +++ b/doc/architectural/cbmc-architecture.md @@ -1,4 +1,5 @@ \ingroup module_hidden + \page cbmc-architecture CBMC Architecture \author Martin Brain, Peter Schrammel diff --git a/doc/architectural/code-walkthrough.md b/doc/architectural/code-walkthrough.md index ed65b8bef7f..4e686711f6e 100644 --- a/doc/architectural/code-walkthrough.md +++ b/doc/architectural/code-walkthrough.md @@ -1,4 +1,5 @@ \ingroup module_hidden + \page code-walkthrough Code Walkthrough \author Cesar Rodriguez, Owen Jones diff --git a/doc/architectural/compilation-and-development.md b/doc/architectural/compilation-and-development.md index 7a4fd69f8ab..03549f3dc1e 100644 --- a/doc/architectural/compilation-and-development.md +++ b/doc/architectural/compilation-and-development.md @@ -1,4 +1,5 @@ \ingroup module_hidden + \page compilation-and-development Compilation and Development \author Martin Brain, Peter Schrammel, Owen Jones diff --git a/doc/architectural/folder-walkthrough.md b/doc/architectural/folder-walkthrough.md index ad792cb2c1b..2c8f5c9c5db 100644 --- a/doc/architectural/folder-walkthrough.md +++ b/doc/architectural/folder-walkthrough.md @@ -1,4 +1,5 @@ \ingroup module_hidden + \page folder-walkthrough Folder Walkthrough \author Martin Brain, Peter Schrammel diff --git a/doc/architectural/front-page.md b/doc/architectural/front-page.md index 77150951ff9..0542e85660e 100644 --- a/doc/architectural/front-page.md +++ b/doc/architectural/front-page.md @@ -1,5 +1,5 @@ -CProver Developer Documentation -===================== + +\page cprover_documentation CProver documentation These pages contain user tutorials, automatically-generated API documentation, and higher-level architectural overviews for the @@ -66,6 +66,12 @@ Overview of Documentation you can access it here. +* \subpage memory-analyzer +* \subpage memory-bounds-checking +* \subpage nondet-volatile +* \subpage restricting-function-pointers +* \subpage satabs + ### For contributors: The following pages attempt to provide the information that a developer needs to diff --git a/doc/architectural/howto.md b/doc/architectural/howto.md index 894eb96266d..a20df144db3 100644 --- a/doc/architectural/howto.md +++ b/doc/architectural/howto.md @@ -1,4 +1,5 @@ \ingroup module_hidden + \page tutorial Tutorials \section cbmc_tutorial CBMC Developer Tutorial diff --git a/doc/architectural/memory-analyzer.md b/doc/architectural/memory-analyzer.md index 0af03ca7cf0..f10512a2ebe 100644 --- a/doc/architectural/memory-analyzer.md +++ b/doc/architectural/memory-analyzer.md @@ -1,6 +1,5 @@ -[CPROVER Manual TOC](../../) -## Memory Analyzer +\page memory-analyzer Memory Analyzer The memory analyzer is a front-end that runs and queries GDB in order to obtain a snapshot of the state of the input program at a particular program location. diff --git a/doc/architectural/memory-bounds-checking.md b/doc/architectural/memory-bounds-checking.md index 73933e27f27..e26fddd6c62 100644 --- a/doc/architectural/memory-bounds-checking.md +++ b/doc/architectural/memory-bounds-checking.md @@ -1,4 +1,5 @@ \ingroup module_hidden + \page memory-bounds-checking Memory Bounds Checking cbmc provides means to verify that pointers are within the bounds of (statically diff --git a/doc/architectural/nondet-volatile.md b/doc/architectural/nondet-volatile.md new file mode 100644 index 00000000000..c1714498189 --- /dev/null +++ b/doc/architectural/nondet-volatile.md @@ -0,0 +1,136 @@ +\ingroup module_hidden + +\page nondet-volatile Modelling of Volatile Variables + +This document describes the options available in goto-instrument for modelling +the behaviour of volatile variables. The following options are provided: + +- `--nondet-volatile` +- `--nondet-volatile-variable ` +- `--nondet-volatile-model :` + +By default, cbmc treats volatile variables the same as non-volatile variables. +That is, it assumes that a volatile variable does not change between subsequent +reads, unless it was written to by the program. With the above options, +goto-instrument can be instructed to instrument the given goto program such as +to (1) make reads from all volatile expressions non-deterministic +(`--nondet-volatile`), (2) make reads from specific variables non-deterministic +(`--nondet-volatile-variable`), or (3) model reads from specific variables by +given models (`--nondet-volatile-model`). + +Below we give two usage examples for the options. Consider the following test, +for function `get_celsius()` and with harness `test_get_celsius()`: + +```C +#include +#include +#include + +// hardware sensor for temperature in kelvin +extern volatile uint16_t temperature; + +int get_celsius() +{ + if(temperature > (1000 + 273)) + { + return INT_MIN; // value indicating error + } + + return temperature - 273; +} + +void test_get_celsius() +{ + int t = get_celsius(); + + assert(t == INT_MIN || t <= 1000); + assert(t == INT_MIN || t >= -273); +} +``` + +Here the variable `temperature` corresponds to a hardware sensor. It returns +the current temperature on each read. The `get_celsius()` function converts the +value in Kelvin to degrees Celsius, given the value is in the expected range. +However, it has a bug where it reads `temperature` a second time after the +check, which may yield a value for which the check would not succeed. Verifying +this program as is with cbmc would yield a verification success. We can use +goto-instrument to make reads from `temperature` non-deterministic: + +``` +goto-cc -o get_celsius_test.gb get_celsius_test.c +goto-instrument --nondet-volatile-variable temperature get_celsius_test.gb get_celsius_test-mod.gb +cbmc --function test_get_celsius get_celsius_test-mod.gb +``` + +Here the final invocation of cbmc correctly reports a verification failure. + +However, simply treating volatile variables as non-deterministic may for some +use cases be too inaccurate. Consider the following test, for function +`get_message()` and with harness `test_get_message()`: + +```C +#include +#include + +extern volatile uint32_t clock; + +typedef struct message { + uint32_t timestamp; + void *data; +} message_t; + +void *read_data(); + +message_t get_message() +{ + message_t msg; + + msg.timestamp = clock; + msg.data = read_data(); + + return msg; +} + +void test_get_message() +{ + message_t msg1 = get_message(); + message_t msg2 = get_message(); + + assert(msg1.timestamp <= msg2.timestamp); +} +``` + +The harness verifies that `get_message()` assigns non-decreasing timestamps to +the returned messages. However, simply treating `clock` as non-deterministic +would not allow to prove this property. Thus, we can supply a model for reads +from `clock`: + +```C +// model for reads of the variable clock +uint32_t clock_read_model() +{ + static uint32_t clock_value = 0; + + uint32_t increment; + __CPROVER_assume(increment <= 100); + + clock_value += increment; + + return clock_value; +} +``` + +The model is stateful in that it keeps the current clock value between +invocations in the variable `clock_value`. On each invocation, it increments +the clock by a non-determinstic value in the range 0 to 100. We can tell +goto-instrument to use the model `clock_read_model()` for reads from the +variable `clock` as follows: + +``` +goto-cc -o get_message_test.gb get_message_test.c +goto-instrument --nondet-volatile-model clock:clock_read_model get_message_test.gb get_message_test-mod.gb +cbmc --function get_message_test get_message_test-mod.gb +``` + +Now the final invocation of cbmc reports verification success. + diff --git a/doc/architectural/other-tools.md b/doc/architectural/other-tools.md index 2ede8a5184a..57f08df74b9 100644 --- a/doc/architectural/other-tools.md +++ b/doc/architectural/other-tools.md @@ -1,4 +1,5 @@ \ingroup module_hidden + \page other-tools Other Tools \author Martin Brain, Peter Schrammel diff --git a/doc/architectural/restrict-function-pointer.md b/doc/architectural/restrict-function-pointer.md new file mode 100644 index 00000000000..c781e6b25b1 --- /dev/null +++ b/doc/architectural/restrict-function-pointer.md @@ -0,0 +1,182 @@ + +\page restricting-function-pointers Restricting function pointers + +In this document, we describe the `goto-instrument` feature to replace calls +through function pointers by case distinctions over calls to given sets of +functions. + +### Motivation + +The CPROVER framework includes a goto program transformation pass +`remove_function_pointers()` to resolve calls to function pointers to direct +function calls. The pass is needed by `cbmc`, as symbolic execution itself can't +handle calls to function pointers. In practice, the transformation pass works as +follows: + +Given that there are functions with these signatures available in the program: + +``` +int f(int x); +int g(int x); +int h(int x); +``` + +And we have a call site like this: + +``` +typedef int(*fptr_t)(int x); +void call(fptr_t fptr) { + int r = fptr(10); + assert(r > 0); +} +``` + +Function pointer removal will turn this into code similar to this: + +``` +void call(fptr_t fptr) { + int r; + if(fptr == &f) { + r = f(10); + } else if(fptr == &g) { + r = g(10); + } else if(fptr == &h) { + r = h(10); + } else { + // sanity check + assert(false); + assume(false); + } + return r; +} +``` + +This works well enough for simple cases. However, this is a very simple +replacement only based on the signature of the function (and whether or not they +have their address taken somewhere in the program), so if there are many +functions matching a particular signature, or if some of these functions are +expensive in symex (e.g. functions with lots of loops or recursion), then this +can be a bit cumbersome - especially if we, as a user, already know that a +particular function pointer will only resolve to a single function or a small +set of functions. The `goto-instrument` option `--restrict-function-pointer` +allows to manually specify this set of functions. + +### Example + +Take the motivating example above. Let us assume that we know for a fact that +`call` will always receive pointers to either `f` or `g` during actual +executions of the program, and symbolic execution for `h` is too expensive to +simply ignore the cost of its branch. For this, we will label the places in each +function where function pointers are being called, to this pattern: + +``` +.function_pointer_call. +``` +where `N` is referring to which function call it is - so the first call to a +function pointer in a function will have `N=1`, the 5th `N=5` etc, or +``` +.