From 7bed09a53af92220c66e53e3434ca8e73cb74578 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Feb 2023 12:39:30 +0000 Subject: [PATCH 1/6] Remove (broken) code contracts link from CPROVER manual The underlying files were moved in e22a788588569b7a52f5. --- doc/cprover-manual/index.md | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/doc/cprover-manual/index.md b/doc/cprover-manual/index.md index 08b111f0268..0148bb44e81 100644 --- a/doc/cprover-manual/index.md +++ b/doc/cprover-manual/index.md @@ -10,15 +10,13 @@ * [Loop Unwinding](cbmc/unwinding/) * [Assertion Checking](cbmc/assertions/) -4. [Compositional Reasoning using Code Contracts](contracts/) +4. [Goto-Analyzer – Abstract Interpretation](goto-analyzer/) -5. [Goto-Analyzer – Abstract Interpretation](goto-analyzer/) +5. [Test Suite Generation](test-suite/) -6. [Test Suite Generation](test-suite/) +6. [Program Properties](properties/) -7. [Program Properties](properties/) - -8. Modeling +7. Modeling * [Nondeterminism](modeling/nondeterminism/) * [Assumptions](modeling/assumptions/) @@ -27,13 +25,13 @@ * [Generating Environments](goto-harness/) * [Memory-mapped I/O](modeling/mmio/) -9. Build Systems +8. Build Systems * [Integration into Build Systems with goto-cc](goto-cc/) * [Integration with Visual Studio builds](visual-studio/) -10. Solvers +9. Solvers * [Incremental SMT solver](smt2-incr/) -11. [The CPROVER API Reference](api/) +10. [The CPROVER API Reference](api/) From 0ad6a7b022f1e7be4791aafa6ec1061276cff350 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Feb 2023 12:55:57 +0000 Subject: [PATCH 2/6] CPROVER manual: consistent formatting of headings Use heading levels that match the nesting level within the overall index. --- doc/cprover-manual/api.md | 62 ++++++++++++------------- doc/cprover-manual/cbmc-assertions.md | 2 +- doc/cprover-manual/cbmc-tutorial.md | 20 ++++---- doc/cprover-manual/goto-analyzer.md | 20 ++++---- doc/cprover-manual/installation.md | 14 +++--- doc/cprover-manual/memory-primitives.md | 20 ++++---- doc/cprover-manual/properties.md | 10 ++-- doc/cprover-manual/static-functions.md | 6 +-- doc/cprover-manual/test-suite.md | 6 +-- 9 files changed, 80 insertions(+), 80 deletions(-) diff --git a/doc/cprover-manual/api.md b/doc/cprover-manual/api.md index 7c022b83ec0..4d3c38603bc 100644 --- a/doc/cprover-manual/api.md +++ b/doc/cprover-manual/api.md @@ -1,13 +1,13 @@ [CPROVER Manual TOC](../) -## The CPROVER API Reference +# The CPROVER API Reference The following sections summarize the functions available to programs that are passed to the CPROVER tools. -### Functions +## Functions -#### \_\_CPROVER\_assume, \_\_CPROVER\_assert, assert +### \_\_CPROVER\_assume, \_\_CPROVER\_assert, assert ```C void __CPROVER_assume(_Bool assumption); @@ -20,7 +20,7 @@ to the program. If the expression evaluates to false, the execution aborts without failure. More detail on the use of assumptions is in the section on [Assumptions](../modeling/assumptions/). -#### \_\_CPROVER\_input, \_\_CPROVER\_output +### \_\_CPROVER\_input, \_\_CPROVER\_output ```C void __CPROVER_input(const char *id, ...); @@ -35,7 +35,7 @@ using nondeterminism, as described [here](../modeling/nondeterminism/)). The string constant is followed by an arbitrary number of values of arbitrary types. -#### \_\_CPROVER\_printf +### \_\_CPROVER\_printf ```C void __CPROVER_printf(const char *format, ...); @@ -45,7 +45,7 @@ The function **\_\_CPROVER\_printf** implements the C `printf` function (without any return value). The observable effect is that its output is shown within a counterexample trace. -#### \_\_CPROVER\_cover +### \_\_CPROVER\_cover ```C void __CPROVER_cover(_Bool condition); @@ -54,7 +54,7 @@ void __CPROVER_cover(_Bool condition); This statement defines a custom coverage criterion, for usage with the [test suite generation feature](../test-suite/). -#### \_\_CPROVER\_isnan, \_\_CPROVER\_isfinite, \_\_CPROVER\_isinf, \_\_CPROVER\_isnormal, \_\_CPROVER\_sign +### \_\_CPROVER\_isnan, \_\_CPROVER\_isfinite, \_\_CPROVER\_isinf, \_\_CPROVER\_isnormal, \_\_CPROVER\_sign ```C _Bool __CPROVER_isnan(double f); @@ -83,7 +83,7 @@ number. This function **\_\_CPROVER\_sign** returns true if the double-precision floating-point number passed as argument is negative. -#### \_\_CPROVER\_abs, \_\_CPROVER\_labs, \_\_CPROVER\_fabs, \_\_CPROVER\_fabsl, \_\_CPROVER\_fabsf +### \_\_CPROVER\_abs, \_\_CPROVER\_labs, \_\_CPROVER\_fabs, \_\_CPROVER\_fabsl, \_\_CPROVER\_fabsf ```C int __CPROVER_abs(int x); @@ -95,7 +95,7 @@ float __CPROVER_fabsf(float x); These functions return the absolute value of the given argument. -#### \_\_CPROVER\_overflow\_minus, \_\_CPROVER\_overflow\_mult, \_\_CPROVER\_overflow\_plus, \_\_CPROVER\_overflow\_shl, \_\_CPROVER\_overflow\_unary\_minus +### \_\_CPROVER\_overflow\_minus, \_\_CPROVER\_overflow\_mult, \_\_CPROVER\_overflow\_plus, \_\_CPROVER\_overflow\_shl, \_\_CPROVER\_overflow\_unary\_minus ```C __CPROVER_bool __CPROVER_overflow_minus(); @@ -111,7 +111,7 @@ operation would overflow when applied to the arguments. For example, `__CPROVER_overflow_plus(x, y)` returns true if `x + y` would result in an arithmetic overflow. -#### \_\_CPROVER\_array\_equal, \_\_CPROVER\_array\_copy, \_\_CPROVER\_array\_set +### \_\_CPROVER\_array\_equal, \_\_CPROVER\_array\_copy, \_\_CPROVER\_array\_set ```C _Bool __CPROVER_array_equal(const void array1[], const void array2[]); @@ -126,7 +126,7 @@ the array **dest**. The function **\_\_CPROVER\_array\_set** initializes the array **dest** with the given value. -#### \_\_CPROVER\_enum\_is\_in\_range +### \_\_CPROVER\_enum\_is\_in\_range ```C __CPROVER_bool __CPROVER_enum_is_in_range(); @@ -157,16 +157,16 @@ int main() ``` -#### Uninterpreted Functions +## Uninterpreted Functions -Uninterpreted functions are documented [here](../modeling/nondeterminism/)). +Uninterpreted functions are documented [here](../modeling/nondeterminism/). -### Memory-Related Functions +## Memory-Related Functions The semantics of the primitives listed in this section is described in more detail in the document about [Memory Primitives](../memory-primitives/). -#### \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_same\_object +### \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_same\_object ```C __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *p); @@ -180,7 +180,7 @@ offset of the given pointer relative to the base address of the object. The function **\_\_CPROVER\_same\_object** returns true if the two pointers given as arguments point to the same object. -#### \_\_CPROVER\_OBJECT\_SIZE, \_\_CPROVER\_DYNAMIC\_OBJECT, \_\_CPROVER\_r\_ok, \_\_CPROVER\_w\_ok +### \_\_CPROVER\_OBJECT\_SIZE, \_\_CPROVER\_DYNAMIC\_OBJECT, \_\_CPROVER\_r\_ok, \_\_CPROVER\_w\_ok The following primitives require a pointer that is null or valid in order to have well-defined semantics in all usage cases. See the document about @@ -211,7 +211,7 @@ returns true when it is safe to do both. These predicates can be given an optional size; when the size argument is not given, the size of the subtype (which must not be **void**) of the pointer type is used. -#### \_\_CPROVER\_havoc\_object +### \_\_CPROVER\_havoc\_object This function requires a valid pointer and updates **all bytes** of the @@ -243,7 +243,7 @@ __CPROVER_assert(thefoo.y == 2, "fails because `thefoo.y` is now nondet"); __CPROVER_assert(thefoo.z == 3, "fails because `thefoo.z` is now nondet"); ``` -#### \_\_CPROVER\_havoc\_slice +### \_\_CPROVER\_havoc\_slice This function requires requires that `__CPROVER_w_ok(p, size)` holds, and updates `size` consecutive bytes of the underlying object, starting at `p`, @@ -262,9 +262,9 @@ void __CPROVER_havoc_slice(void *p, __CPROVER_size_t size); by the program, then havocing the slice is equivalent to making the interpretation of these bytes nondeterministic. -### Predefined Types and Symbols +## Predefined Types and Symbols -#### \_\_CPROVER\_bitvector +### \_\_CPROVER\_bitvector ```C __CPROVER_bitvector [ expression ] @@ -275,7 +275,7 @@ bit vector with arbitrary but fixed size. The usual integer type modifiers **signed** and **unsigned** can be applied. The usual arithmetic promotions will be applied to operands of this type. -#### \_\_CPROVER\_floatbv +### \_\_CPROVER\_floatbv ```C __CPROVER_floatbv [ expression ] [ expression ] @@ -287,7 +287,7 @@ parameter is the total size (in bits) of the number, and the second is the size (in bits) of the mantissa, or significand (not including the hidden bit, thus for single precision this should be 23). -#### \_\_CPROVER\_fixedbv +### \_\_CPROVER\_fixedbv ```C __CPROVER_fixedbv [ expression ] [ expression ] @@ -298,11 +298,11 @@ fixed-point bit vector with arbitrary but fixed size. The first parameter is the total size (in bits) of the type, and the second is the number of bits after the radix point. -#### \_\_CPROVER\_size\_t +### \_\_CPROVER\_size\_t The type of sizeof expressions. -#### \_\_CPROVER\_rounding\_mode +### \_\_CPROVER\_rounding\_mode ```C extern int __CPROVER_rounding_mode; @@ -310,16 +310,16 @@ extern int __CPROVER_rounding_mode; This variable contains the IEEE floating-point arithmetic rounding mode. -#### \_\_CPROVER\_constant\_infinity\_uint +### \_\_CPROVER\_constant\_infinity\_uint This is a constant that models a large unsigned integer. -#### \_\_CPROVER\_integer, \_\_CPROVER\_rational +### \_\_CPROVER\_integer, \_\_CPROVER\_rational **\_\_CPROVER\_integer** is an unbounded, signed integer type. **\_\_CPROVER\_rational** is an unbounded, signed rational number type. -#### \_\_CPROVER\_memory +### \_\_CPROVER\_memory ```C extern unsigned char __CPROVER_memory[]; @@ -327,22 +327,22 @@ extern unsigned char __CPROVER_memory[]; This array models the contents of integer-addressed memory. -#### \_\_CPROVER::unsignedbv<N> (C++ only) +### \_\_CPROVER::unsignedbv<N> (C++ only) This type is the equivalent of **unsigned \_\_CPROVER\_bitvector\[N\]** in the C++ front-end. -#### \_\_CPROVER::signedbv<N> (C++ only) +### \_\_CPROVER::signedbv<N> (C++ only) This type is the equivalent of **signed \_\_CPROVER\_bitvector\[N\]** in the C++ front-end. -#### \_\_CPROVER::fixedbv<N> (C++ only) +### \_\_CPROVER::fixedbv<N> (C++ only) This type is the equivalent of **\_\_CPROVER\_fixedbv\[N,m\]** in the C++ front-end. -### Concurrency +## Concurrency Asynchronous threads are created by preceding an instruction with a label with the prefix **\_\_CPROVER\_ASYNC\_**. diff --git a/doc/cprover-manual/cbmc-assertions.md b/doc/cprover-manual/cbmc-assertions.md index 2426863ca6a..8fc8395d377 100644 --- a/doc/cprover-manual/cbmc-assertions.md +++ b/doc/cprover-manual/cbmc-assertions.md @@ -1,6 +1,6 @@ [CPROVER Manual TOC](../../) -### Assertion Checking +## Assertion Checking [Assertions](http://en.wikipedia.org/wiki/Assertion_%28computing%29) are statements within the program that attempt to capture the programmer's diff --git a/doc/cprover-manual/cbmc-tutorial.md b/doc/cprover-manual/cbmc-tutorial.md index ac4109b52e3..2bed7d5d64f 100644 --- a/doc/cprover-manual/cbmc-tutorial.md +++ b/doc/cprover-manual/cbmc-tutorial.md @@ -1,6 +1,6 @@ [CPROVER Manual TOC](../../) -### Example: Buffer Overflows +## Example: Buffer Overflows To give a brief overview of the capabilities of CBMC we start with a simple example. The issue of *[buffer @@ -30,7 +30,7 @@ lower and upper bounds, even for arrays with dynamic size. A detailed discussion of the properties that CBMC can check automatically is [here](../../properties/). -### First Steps +## First Steps We assume you have already installed CBMC and the necessary support files on your system. If not so, please follow the instructions @@ -113,7 +113,7 @@ property for the object bounds of `argv` does not hold, and will display: [main.pointer_dereference.6] line 7 dereference failure: pointer outside object bounds in argv[(signed long int)2]: FAILURE ``` -### Counterexample Traces +## Counterexample Traces Let us have a closer look at this property and why it fails. To aid the understanding of the problem, CBMC can generate a *counterexample trace* @@ -137,7 +137,7 @@ possible output format. cbmc file1.c --bounds-check --pointer-check --trace --xml-ui ``` -### Verifying Modules +## Verifying Modules In the example above, we used a program that starts with a `main` function. However, CBMC is aimed at embedded software, and these kinds @@ -169,7 +169,7 @@ cbmc file2.c --function sum --bounds-check It is often necessary to build a suitable *harness* for the function in order to set up the environment appropriately. -### Loop Unwinding +## Loop Unwinding When running the previous example, you will have noted that CBMC unwinds the `for` loop in the program. As CBMC performs Bounded Model Checking, @@ -218,7 +218,7 @@ iterations. Thus, CBMC will report that the unwinding assertion has failed. As usual, a counterexample trace that documents this can be obtained with the option `--property`. -### Unbounded Loops +## Unbounded Loops CBMC can also be used for programs with unbounded loops. In this case, CBMC is used for bug hunting only; CBMC does not attempt to find all bugs. The @@ -293,7 +293,7 @@ but it can be helpful to find program bugs. The various command line options that CBMC offers for loop unwinding are described in the section on [understanding loop unwinding](../../cbmc/unwinding/). -### A Note About Compilers and the ANSI-C Library +## A Note About Compilers and the ANSI-C Library Most C programs make use of functions provided by a library; instances are functions from the standard ANSI-C library such as `malloc` or @@ -307,14 +307,14 @@ requirements: Most C compilers come with header files for the ANSI C library functions. We briefly discuss how to obtain/install these library files. -#### Linux +### Linux Linux systems that are able to compile software are usually equipped with the appropriate header files. Consult the documentation of your distribution on how to install the compiler and the header files. First try to compile some significant program before attempting to verify it. -#### Windows +### Windows On Microsoft Windows, CBMC is pre-configured to use the compiler that is part of Microsoft's Visual Studio. Microsoft's [Visual Studio @@ -331,7 +331,7 @@ comes with a small set of definitions, which includes functions such as `malloc`. Detailed information about the built-in definitions is [here](../../goto-cc/). -### Further Reading +## Further Reading - [Understanding Loop Unwinding](../../cbmc/unwinding/) - [Hardware Verification using ANSI-C Programs as a diff --git a/doc/cprover-manual/goto-analyzer.md b/doc/cprover-manual/goto-analyzer.md index 8a5bc3088b3..f5a84207e76 100644 --- a/doc/cprover-manual/goto-analyzer.md +++ b/doc/cprover-manual/goto-analyzer.md @@ -1,6 +1,6 @@ [CPROVER Manual TOC](../) -## Goto Analyzer +# Goto Analyzer `goto-analyzer` is an abstract interpreter which uses the same front-end and GOTO binary representation as CBMC. It is built along @@ -29,7 +29,7 @@ number of points of execution. * The [storage](#storage) that links points of execution and domains. -### Quick Start +## Quick Start As the space of configuration options is quite large and their interactions can sometimes be subtle and complex, here are some @@ -60,7 +60,7 @@ goto-analyzer --show --dot depgraph.dot --dependence-graph-vs -### Task +## Task `goto-analyzer` first runs the abstract interpreter until it reaches a fix-point, then it will perform the task the user has chosen. @@ -125,7 +125,7 @@ traces that reach them. -### Output +## Output These options control how the result of the task is output. The default is text to the standard output. In the case of tasks that @@ -148,7 +148,7 @@ only supported by some domains and tasks (for example `--show --dependence-graph`). -### Abstract Interpreter +## Abstract Interpreter These options control which abstract interpreter is used and how the analysis is performed. In principle this can significantly change @@ -187,7 +187,7 @@ If you are using `--vsd` this is recommended as it is more accurate with little extra cost. -### Domain +## Domain One of the most important options; this controls how the possible states at a given execution point are represented and manipulated. @@ -237,7 +237,7 @@ means it can be configured using the VSD options and give more precise analysis (for example, field aware) of the dependencies. -#### Configuration of the Variable Sensitivity Domain +### Configuration of the Variable Sensitivity Domain VSD has a wide range of options that allow you to choose what kind of abstract objects (and thus abstractions) are used to represent @@ -324,7 +324,7 @@ is why the default is to do the reduction. It can be useful for debugging issues with the reduction. -### History +## History To over-approximate what a program does, it is necessary to consider all of the paths of execution through the program. As there are a @@ -399,7 +399,7 @@ each function. -### Storage +## Storage The histories described above are used to keep track of where in the computation needs to be explored. The most precise option is to keep @@ -422,7 +422,7 @@ a significant increase in the amount of memory used. -### Other Options +## Other Options `goto-analyzer` supports a number of other options for the C/C++ frontend, the platform, displaying program representations and diff --git a/doc/cprover-manual/installation.md b/doc/cprover-manual/installation.md index 4a256ba5944..e076a15279f 100644 --- a/doc/cprover-manual/installation.md +++ b/doc/cprover-manual/installation.md @@ -1,8 +1,8 @@ [CPROVER Manual TOC](../) -## Installation +# Installation -### Requirements +## Requirements CBMC is available for Windows, i86 Linux, and MacOS X. CBMC requires a code pre-processing environment comprising of a suitable preprocessor @@ -32,7 +32,7 @@ exclusively within Eclipse, you can skip the installation of the CBMC executable. However, you still have to install the compiler environment as described above. -### Installing the CBMC Binaries +## Installing the CBMC Binaries 1. Download CBMC for your operating system. The binaries are available from http://www.cprover.org/cbmc/. @@ -42,13 +42,13 @@ described above. You are now ready to use CBMC. We recommend you follow the [tutorial](../cbmc/tutorial/). -### Building CBMC from Source +## Building CBMC from Source See the [CPROVER Developer Documentation](https://diffblue.github.io/cbmc/compilation-and-development.html). -## Installing the Eclipse Plugin +# Installing the Eclipse Plugin -### Requirements +## Requirements We provide a graphical user interface to CBMC which is realized as a plugin to the Eclipse framework. Eclipse is available at @@ -60,7 +60,7 @@ complex set of environment variables to identify the target architecture and the directories that contain the header files. You must run Eclipse from within the *Visual Studio Command Prompt*. -### Installing the Eclipse Plugin +## Installing the Eclipse Plugin The installation instructions for the Eclipse Plugin, including the link to the download site, are available diff --git a/doc/cprover-manual/memory-primitives.md b/doc/cprover-manual/memory-primitives.md index bb9cb7d0961..984ecd093ac 100644 --- a/doc/cprover-manual/memory-primitives.md +++ b/doc/cprover-manual/memory-primitives.md @@ -4,10 +4,10 @@ This document describes the semantics and usage of memory-related and pointer-related primitives in CBMC. -# Background +## Background -## Memory and pointers in CBMC +### Memory and pointers in CBMC When CBMC analyzes a program, by default it uses the architectural parameters of the platform it is running on. That is, on a 64-bit system, CBMC will treat @@ -41,7 +41,7 @@ the object IDs of the two given pointers. That is, it is true if and only if to apply these three primitives to a pointer (i.e., they do not have any special preconditions). -## Memory Objects +### Memory Objects Seeing that pointers consist of an object ID and an offset, it remains to describe how CBMC assigns object IDs to memory objects (such as local variables @@ -90,7 +90,7 @@ point into another memory object (such as could happen when running on a real machine). To verify that pointers stay within the bounds of their pointees, the CBMC option `--pointer-overflow-check` can be used. -### Malloc modelling +#### Malloc modelling CBMC ships a model of `malloc` that seeks to emulate the behaviour of the C standard library. This model is configurable to suit the assumptions the @@ -147,7 +147,7 @@ do so via \ref goto-instrument (using `goto-instrument --add-library`), then the malloc failure mode needs to be specified with that `goto-instrument` invocation, i.e., as an option to `goto-instrument`. -## Uninitialized pointers +### Uninitialized pointers In verification tools, uninitialized variables are typically treated as having a nondeterministic value. Programs can thus be verified on a set of potential @@ -169,7 +169,7 @@ pointers should be explicitely initialized to ensure that they are backed by valid memory. -# Memory Primitives +## Memory Primitives In this section, we describe further memory primitives of CBMC. Above, we have already encountered the primitives `__CPROVER_POINTER_OBJECT(p)`, @@ -194,7 +194,7 @@ null nor valid. CBMC has an option `--pointer-primitive-check` (see section to check that pointers used in the primitives are either null or valid. -## Retrieving the size of a memory object +### Retrieving the size of a memory object The following primitive can be used to retrieve the size of the memory object a pointer points to: @@ -209,7 +209,7 @@ necessarily to the start). The result is the same as if the pointer would point to the start of the memory object (i.e., would have offset 0). -## Checking if a pointer points to dynamic memory +### Checking if a pointer points to dynamic memory The following primitive can be used to check whether a pointer points to dynamic (malloced, heap) memory: @@ -223,7 +223,7 @@ unspecified. Like `__CPROVER_OBJECT_SIZE()`, it is valid to apply the primitive to pointers that point to within a memory object. -## Checking if a memory segment has at least a given size +### Checking if a memory segment has at least a given size The following two primitives can be used to check whether there is a memory segment starting at the given pointer and extending for at least the given @@ -247,7 +247,7 @@ assert(__CPROVER_r_ok(p, 3)); // valid assert(__CPROVER_r_ok(p, 10)); // fails ``` -# Detecting potential misuses of memory primitives +## Detecting potential misuses of memory primitives As described above, the primitives listed in the Memory Primitives section require a pointer that is either null or valid to have well-defined semantics. diff --git a/doc/cprover-manual/properties.md b/doc/cprover-manual/properties.md index 0a985f1f273..cd81a5d4635 100644 --- a/doc/cprover-manual/properties.md +++ b/doc/cprover-manual/properties.md @@ -1,8 +1,8 @@ [CPROVER Manual TOC](../) -## Automatically Generating Properties +# Automatically Generating Properties -### What is a "Property"? +## What is a "Property"? We have mentioned *properties* several times so far, but we never explained *what* kind of properties CBMC can verify. We cover @@ -67,7 +67,7 @@ of the Eclipse plugin can step through these counterexamples in a way that is similar to debugging programs. The installation of this plugin is explained [here](http://www.cprover.org/eclipse-plugin/). -### Using goto-instrument +## Using goto-instrument The goto-instrument static analyzer operates on goto-binaries, which is a binary representation of control-flow graphs. The goto-binary is @@ -207,7 +207,7 @@ unsigned foo(unsigned x) x = x + 2; ``` -#### Flag --nan-check limitations +### Flag --nan-check limitations Please note that `--nan-check` flag is adding not-a-number checks only for generation of NaN value. Current implementation of `--nan-check` flag is not @@ -222,7 +222,7 @@ float f = 0.0/0.0; // will generate NaN - CBMC will add assertion float g = NAN+0.0; // propagation of NaN value - no assertion generated ``` -#### Generating function bodies +### Generating function bodies Sometimes implementations for called functions are not available in the goto program, or it is desirable to replace bodies of functions with certain diff --git a/doc/cprover-manual/static-functions.md b/doc/cprover-manual/static-functions.md index f7fd33fe32f..67594f763d7 100644 --- a/doc/cprover-manual/static-functions.md +++ b/doc/cprover-manual/static-functions.md @@ -1,6 +1,6 @@ [CPROVER Manual TOC](../) -# Modular Verification of Static Functions +## Modular Verification of Static Functions This page describes how to use CBMC on static functions. @@ -48,7 +48,7 @@ The following commands build and check this function: > cbmc --function harness to_check.gb ``` -## Stubbing out static functions +### Stubbing out static functions For performance reasons, it might be desirable to analyze the API function independently of the static function. We can analyze the API @@ -81,7 +81,7 @@ object file: > cbmc --function harness to_check.gb ``` -## Separately checking static functions +### Separately checking static functions We should now also write a harness for `private_function`. However, since that function is marked `static`, it is not possible for functions diff --git a/doc/cprover-manual/test-suite.md b/doc/cprover-manual/test-suite.md index e6c27017f1c..0a6084e0de1 100644 --- a/doc/cprover-manual/test-suite.md +++ b/doc/cprover-manual/test-suite.md @@ -1,8 +1,8 @@ [CPROVER Manual TOC](../) -## Test Suite Generation with CBMC +# Test Suite Generation with CBMC -### A Small Tutorial with a Case Study +## A Small Tutorial with a Case Study We assume that CBMC is installed on your system. If not, follow [these instructions](../installation/). @@ -206,7 +206,7 @@ a PID controller case study. In addition to `--cover mcdc`, other coverage criteria such as `branch`, `decision`, and `path` are also available when calling CBMC. -### Coverage Criteria +## Coverage Criteria The table below summarizes the coverage criteria that CBMC supports. From cf4df699bcc58e9ff8f8f4dca376302d0fe54200 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Feb 2023 12:32:58 +0000 Subject: [PATCH 3/6] Add missing newline in help output We only ended up with reasonable output as the next line was a newline. --- src/goto-checker/bmc_util.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 40a6f5bd03c..ab4ae30a3c6 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -245,7 +245,7 @@ void run_property_decider( " complexity violations before the loop\n" \ " gets blacklisted\n" \ " --graphml-witness filename write the witness in GraphML format to filename\n" /* NOLINT(*) */ \ - " --symex-cache-dereferences enable caching of repeated dereferences" \ + " --symex-cache-dereferences enable caching of repeated dereferences\n" \ // clang-format on #endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H From 23b7037c2c0fef3a284b75b98265a539f2f2517f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Feb 2023 12:29:04 +0000 Subject: [PATCH 4/6] Synchronise help output with actual support for --fp-reachability-slice Neither CBMC nor JBMC actually interpret this option, despite it being advertised in help output (and man pages). Conversely, goto-instrument has support for `--reachability-slice-fb`, but it wasn't available on the command line. --- doc/man/cbmc.1 | 6 ----- doc/man/goto-instrument.1 | 4 +++ doc/man/jbmc.1 | 6 ----- jbmc/src/jbmc/jbmc_parse_options.cpp | 1 - src/cbmc/cbmc_parse_options.cpp | 1 - .../goto_instrument_parse_options.cpp | 2 +- .../goto_instrument_parse_options.h | 6 +++-- src/goto-instrument/reachability_slicer.h | 26 +++++++++---------- 8 files changed, 22 insertions(+), 30 deletions(-) diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index 6514c809b1f..7a2a54d4d12 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -258,12 +258,6 @@ set malloc failure mode to return null \fB\-\-string\-abstraction\fR track C string lengths and zero\-termination .TP -\fB\-\-fp\-reachability\-slice\fR f -remove instructions that cannot appear on a trace -that visits all given functions. The list of -functions has to be given as a comma separated -list f. -.TP \fB\-\-reachability\-slice\fR remove instructions that cannot appear on a trace from entry point to a property diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index 755f52c38ce..4810ac443b2 100644 --- a/doc/man/goto-instrument.1 +++ b/doc/man/goto-instrument.1 @@ -972,6 +972,10 @@ list \fIf\fR. remove instructions that cannot appear on a trace from entry point to a property .TP +\fB\-\-reachability\-slice\-fb\fR +remove instructions that cannot appear on a trace +from entry point through a property +.TP \fB\-\-full\-slice\fR slice away instructions that don't affect assertions .TP diff --git a/doc/man/jbmc.1 b/doc/man/jbmc.1 index 1482f67bd31..60356c0ac30 100644 --- a/doc/man/jbmc.1 +++ b/doc/man/jbmc.1 @@ -138,12 +138,6 @@ ignore user assumptions \fB\-\-mm\fR MM memory consistency model for concurrent programs .TP -\fB\-\-fp\-reachability\-slice\fR f -remove instructions that cannot appear on a trace -that visits all given functions. The list of -functions has to be given as a comma separated -list f. -.TP \fB\-\-reachability\-slice\fR remove instructions that cannot appear on a trace from entry point to a property diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index b1258d77d31..84cb29a4588 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -967,7 +967,6 @@ void jbmc_parse_optionst::help() " --no-assumptions ignore user assumptions\n" " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) HELP_REACHABILITY_SLICER - HELP_REACHABILITY_SLICER_FB " --full-slice run full slicer (experimental)\n" // NOLINT(*) "\n" "Java Bytecode frontend options:\n" diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index cad16ca9b96..c425e929e09 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -902,7 +902,6 @@ void cbmc_parse_optionst::help() " --mm MM memory consistency model for concurrent programs (default: sc)\n" // NOLINT(*) HELP_CONFIG_LIBRARY HELP_REACHABILITY_SLICER - HELP_REACHABILITY_SLICER_FB " --full-slice run full slicer (experimental)\n" // NOLINT(*) " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) " --havoc-undefined-functions\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 13903597f8d..0dad17e0c1e 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -95,7 +95,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "nondet_volatile.h" #include "points_to.h" #include "race_check.h" -#include "reachability_slicer.h" #include "remove_function.h" #include "rw_set.h" #include "show_locations.h" @@ -1971,6 +1970,7 @@ void goto_instrument_parse_optionst::help() "\n" "Slicing:\n" HELP_REACHABILITY_SLICER + HELP_FP_REACHABILITY_SLICER " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*) " --property id slice with respect to specific property only\n" // NOLINT(*) " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 2afed2316ec..07c0dfd9e1c 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -36,6 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "generate_function_bodies.h" #include "insert_final_assert_false.h" #include "nondet_volatile.h" +#include "reachability_slicer.h" #include "replace_calls.h" #include "uninitialized.h" #include "unwindset.h" @@ -77,8 +78,9 @@ Author: Daniel Kroening, kroening@kroening.com "(custom-bitvector-analysis)" \ "(show-struct-alignment)(interval-analysis)(show-intervals)" \ "(show-uninitialized)(show-locations)" \ - "(full-slice)(reachability-slice)(slice-global-inits)" \ - "(fp-reachability-slice):" \ + "(full-slice)(slice-global-inits)" \ + OPT_REACHABILITY_SLICER \ + OPT_FP_REACHABILITY_SLICER \ "(inline)(partial-inline)(function-inline):(log):(no-caching)" \ "(value-set-fi-fp-removal)" \ OPT_REMOVE_CONST_FUNCTION_POINTERS \ diff --git a/src/goto-instrument/reachability_slicer.h b/src/goto-instrument/reachability_slicer.h index 36fe5a4fef8..747287ec357 100644 --- a/src/goto-instrument/reachability_slicer.h +++ b/src/goto-instrument/reachability_slicer.h @@ -42,18 +42,18 @@ void reachability_slicer( message_handlert &); // clang-format off -#define OPT_REACHABILITY_SLICER \ - "(fp-reachability-slice):(reachability-slice)(reachability-slice-fb)" // NOLINT(*) - -#define HELP_REACHABILITY_SLICER \ - " --fp-reachability-slice f remove instructions that cannot appear on a trace\n" \ - " that visits all given functions. The list of\n" \ - " functions has to be given as a comma separated\n" \ - " list f.\n" \ - " --reachability-slice remove instructions that cannot appear on a trace\n" \ - " from entry point to a property\n" // NOLINT(*) -#define HELP_REACHABILITY_SLICER_FB \ - " --reachability-slice-fb remove instructions that cannot appear on a trace\n" \ - " from entry point through a property\n" // NOLINT(*) +#define OPT_FP_REACHABILITY_SLICER "(fp-reachability-slice):" +#define OPT_REACHABILITY_SLICER "(reachability-slice)(reachability-slice-fb)" + +#define HELP_FP_REACHABILITY_SLICER \ + " --fp-reachability-slice f remove instructions that cannot appear on\n" \ + " trace that visits all given functions.\n" \ + " The list of functions has to be given as a\n" \ + " comma separated list f.\n" +#define HELP_REACHABILITY_SLICER \ + " --reachability-slice remove instructions that cannot appear on\n" \ + " a trace from entry point to a property\n" \ + " --reachability-slice-fb remove instructions that cannot appear on\n" \ + " a trace from entry point through a property\n" // clang-format on #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H From c40ea7e0995fa5da717cdc480e7ec7445340106d Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 25 Nov 2021 15:57:32 +0000 Subject: [PATCH 5/6] Issue warnings when options may yield unsound verification results Also warn about options that aren't unsound by design, but are experimental in nature. --- jbmc/src/jbmc/jbmc_parse_options.cpp | 43 +++++++++++++++++-- src/cbmc/cbmc_parse_options.cpp | 42 ++++++++++++++++++ .../goto_instrument_parse_options.cpp | 4 ++ 3 files changed, 86 insertions(+), 3 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 84cb29a4588..324a0868fe3 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -187,6 +187,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) { options.set_option( "symex-complexity-limit", cmdline.get_value("symex-complexity-limit")); + log.warning() << "**** WARNING: Complexity-limited analysis may yield " + "unsound verification results" + << messaget::eom; } if(cmdline.isset("symex-complexity-failed-child-loops-limit")) @@ -194,18 +197,44 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option( "symex-complexity-failed-child-loops-limit", cmdline.get_value("symex-complexity-failed-child-loops-limit")); + if(!cmdline.isset("symex-complexity-limit")) + { + log.warning() << "**** WARNING: Complexity-limited analysis may yield " + "unsound verification results" + << messaget::eom; + } } if(cmdline.isset("unwind")) + { options.set_option("unwind", cmdline.get_value("unwind")); + if(!cmdline.isset("unwinding-assertions")) + { + log.warning() << "**** WARNING: Use --unwinding-assertions to obtain " + "sound verification results" + << messaget::eom; + } + } if(cmdline.isset("depth")) + { options.set_option("depth", cmdline.get_value("depth")); + log.warning() + << "**** WARNING: Depth-bounded analysis may yield unsound verification " + "results" + << messaget::eom; + } if(cmdline.isset("unwindset")) { options.set_option( "unwindset", cmdline.get_comma_separated_values("unwindset")); + if(!cmdline.isset("unwinding-assertions")) + { + log.warning() << "**** WARNING: Use --unwinding-assertions to obtain " + "sound verification results" + << messaget::eom; + } } // constant propagation @@ -234,9 +263,13 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("unwinding-assertions", true); // generate unwinding assumptions otherwise - options.set_option( - "partial-loops", - cmdline.isset("partial-loops")); + if(cmdline.isset("partial-loops")) + { + options.set_option("partial-loops", true); + log.warning() + << "**** WARNING: --partial-loops may yield unsound verification results" + << messaget::eom; + } // remove unused equations options.set_option( @@ -858,6 +891,10 @@ bool jbmc_parse_optionst::process_goto_functions( // full slice? if(cmdline.isset("full-slice")) { + log.warning() << "**** WARNING: Experimental option --full-slice, " + << "analysis results may be unsound. See " + << "https://github.com/diffblue/cbmc/issues/260" + << messaget::eom; log.status() << "Performing a full slice" << messaget::eom; if(cmdline.isset("property")) property_slicer(goto_model, cmdline.get_values("property")); diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index c425e929e09..aa1ffe69262 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -193,13 +193,26 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("mm", cmdline.get_value("mm")); if(cmdline.isset("symex-complexity-limit")) + { options.set_option( "symex-complexity-limit", cmdline.get_value("symex-complexity-limit")); + log.warning() << "**** WARNING: Complexity-limited analysis may yield " + "unsound verification results" + << messaget::eom; + } if(cmdline.isset("symex-complexity-failed-child-loops-limit")) + { options.set_option( "symex-complexity-failed-child-loops-limit", cmdline.get_value("symex-complexity-failed-child-loops-limit")); + if(!cmdline.isset("symex-complexity-limit")) + { + log.warning() << "**** WARNING: Complexity-limited analysis may yield " + "unsound verification results" + << messaget::eom; + } + } if(cmdline.isset("property")) options.set_option("property", cmdline.get_values("property")); @@ -243,10 +256,24 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("localize-faults", true); if(cmdline.isset("unwind")) + { options.set_option("unwind", cmdline.get_value("unwind")); + if(!cmdline.isset("unwinding-assertions")) + { + log.warning() << "**** WARNING: Use --unwinding-assertions to obtain " + "sound verification results" + << messaget::eom; + } + } if(cmdline.isset("depth")) + { options.set_option("depth", cmdline.get_value("depth")); + log.warning() + << "**** WARNING: Depth-bounded analysis may yield unsound verification " + "results" + << messaget::eom; + } if(cmdline.isset("slice-by-trace")) { @@ -258,6 +285,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) { options.set_option( "unwindset", cmdline.get_comma_separated_values("unwindset")); + if(!cmdline.isset("unwinding-assertions")) + { + log.warning() << "**** WARNING: Use --unwinding-assertions to obtain " + "sound verification results" + << messaget::eom; + } } // constant propagation @@ -280,7 +313,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) } if(cmdline.isset("partial-loops")) + { options.set_option("partial-loops", true); + log.warning() + << "**** WARNING: --partial-loops may yield unsound verification results" + << messaget::eom; + } // remove unused equations if(cmdline.isset("slice-formula")) @@ -840,6 +878,10 @@ bool cbmc_parse_optionst::process_goto_program( // full slice? if(options.get_bool_option("full-slice")) { + log.warning() << "**** WARNING: Experimental option --full-slice, " + << "analysis results may be unsound. See " + << "https://github.com/diffblue/cbmc/issues/260" + << messaget::eom; log.status() << "Performing a full slice" << messaget::eom; if(options.is_set("property")) property_slicer(goto_model, options.get_list_option("property")); diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 0dad17e0c1e..0f577067fbb 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1742,6 +1742,10 @@ void goto_instrument_parse_optionst::instrument_goto_program() do_indirect_call_and_rtti_removal(); do_remove_returns(); + log.warning() << "**** WARNING: Experimental option --full-slice, " + << "analysis results may be unsound. See " + << "https://github.com/diffblue/cbmc/issues/260" + << messaget::eom; log.status() << "Performing a full slice" << messaget::eom; if(cmdline.isset("property")) property_slicer(goto_model, cmdline.get_values("property")); From fde9ac5cbfefb037b88c77cbc19e9b1e36eae2d0 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 25 Nov 2021 15:59:01 +0000 Subject: [PATCH 6/6] Explain unsound and experimental options in documentation. Some use of CBMC or JBMC can yield verification results that must not be taken at face value. Co-authored-by: Michael Tautschnig --- doc/cprover-manual/index.md | 7 +-- doc/cprover-manual/unsound_options.md | 67 +++++++++++++++++++++++++++ 2 files changed, 71 insertions(+), 3 deletions(-) create mode 100644 doc/cprover-manual/unsound_options.md diff --git a/doc/cprover-manual/index.md b/doc/cprover-manual/index.md index 0148bb44e81..15e744592f6 100644 --- a/doc/cprover-manual/index.md +++ b/doc/cprover-manual/index.md @@ -30,8 +30,9 @@ * [Integration into Build Systems with goto-cc](goto-cc/) * [Integration with Visual Studio builds](visual-studio/) -9. Solvers +9. [The CPROVER API Reference](api/) - * [Incremental SMT solver](smt2-incr/) +10. Background Information on selected Command-line Options -10. [The CPROVER API Reference](api/) + * [Incremental SMT solver](smt2-incr/) + * [Unsound options](unsound_options/) diff --git a/doc/cprover-manual/unsound_options.md b/doc/cprover-manual/unsound_options.md new file mode 100644 index 00000000000..ebb3d290644 --- /dev/null +++ b/doc/cprover-manual/unsound_options.md @@ -0,0 +1,67 @@ +[CPROVER Manual TOC](../) + +## Unsound CLI options for various tools + +### Context + +In [#6480](https://github.com/diffblue/cbmc/issues/6480), there has been some extensive +conversation about what it means for certain options to produce *unsound* behavior. + +We concluded that *unsound* in this context is a proxy for the following two behaviors +that we want to avoid: + +* **A spurious counter example to an assertion**, which means that the tool may report + a coverage property (or a line of code) as reachable when in fact it is not, and +* **Wrong proof to an assertion**, which means that it might indicate an assertion passing + when it's not. + +We expect that, by default, CBMC and JBMC display none of the behavior we +described above (and if they do, it's an extremely serious bug that we aim to +fix on an ASAP basis), but be aware that certain tools, like `goto-instrument`, +may contain components that are experimental in nature and thus do +transformations that eventually lead to behavior such as the ones described +above. Furthermore, some options lead to unsound analysis results *by design*, +and some transformations performed by `goto-instrument` will yield verification +results that are (by design) unsound when taking verification of the +non-transformed program as reference. + +### Examples of Options that may yield Unsound Results + +The following options will produce a warning when used with CBMC or JBMC: + +* Use of `--unwind` or `--unwindset` without `--unwinding-assertions`, or the + use of `--partial-loops`. +* Depth or complexity-limited analysis (`--depth`, `--symex-complexity-limit`). + +See [Understanding Loop Unwinding](../cbmc/unwinding/) for an elaboration of +these options. + +### Experimental Options + +Be advised that the following command line options to `cbmc` and `goto-instrument` +have been reported to be unsound: + +* `--full-slice` has been reported to be unsound in issue [cbmc#260](https://github.com/diffblue/cbmc/issues/260) + In particular, `--full-slice` appears to lead to spurious counter examples, + because values that get assigned by a function whose body gets sliced out are + no longer present in the trace, but still result in flipped verification results. + +`cbmc` and `goto-instrument` have also been modified to warn that options used +are unsound as part of their output. An example of how that output looks is shown +below: + +```sh +$ cbmc --full-slice ~/Devel/cbmc_bugs/6394/before-slice.out +CBMC version 5.45.0 (cbmc-5.43.0-77-g99c5a92de1-dirty) 64-bit arm64 macos +Reading GOTO program from file +Reading: ~/Devel/cbmc_bugs/6394/before-slice.out +Generating GOTO Program +Adding CPROVER library (x86_64) +Removal of function pointers and virtual functions +Generic Property Instrumentation +**** WARNING: Experimental option --full-slice, analysis results may be unsound. See https://github.com/diffblue/cbmc/issues/260 +Performing a full slice +Running with 8 object bits, 56 offset bits (default) +Starting Bounded Model Checking +[...] +```