From 320da328ef22a0621375d4969ad85170332c72f0 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Wed, 29 Apr 2020 16:40:31 +0100 Subject: [PATCH 01/12] Add tests verifying the incremental status is output --- regression/cbmc-incr-oneloop/alarm2/test-json-output.desc | 1 + regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc | 1 + regression/cbmc-incr-oneloop/alarm2/test.desc | 6 ++++++ 3 files changed, 8 insertions(+) diff --git a/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc b/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc index 0e8d52fad24..904c5d51283 100644 --- a/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc +++ b/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc @@ -5,5 +5,6 @@ main.c ^SIGNAL=0$ "messageText": "VERIFICATION FAILED" "currentUnwinding": 1 +"incrementalStatus": "INCONCLUSIVE" -- ^warning: ignoring diff --git a/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc b/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc index 90a3dfe16e2..c967c1fb2db 100644 --- a/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc +++ b/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc @@ -6,5 +6,6 @@ main.c VERIFICATION FAILED 1 1 +INCONCLUSIVE -- ^warning: ignoring diff --git a/regression/cbmc-incr-oneloop/alarm2/test.desc b/regression/cbmc-incr-oneloop/alarm2/test.desc index 2c5f198ab70..576ae8bac92 100644 --- a/regression/cbmc-incr-oneloop/alarm2/test.desc +++ b/regression/cbmc-incr-oneloop/alarm2/test.desc @@ -1,9 +1,15 @@ CORE main.c --incremental-loop main.0 --unwind-min 5 --unwind-max 10 +activate-multi-line-match Current unwinding: 1 +Incremental status: INCONCLUSIVE +Current unwinding: 5\nUnwinding .*\nIncremental status: INCONCLUSIVE +Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -- ^warning: ignoring +-- +The multi-line match is added to verify that an incremental status is printed immediately after each unwinding From 0604d8e61b61e3a965b0390f0d654de452a5d27e Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 1 May 2020 16:51:09 +0100 Subject: [PATCH 02/12] Move documentation of more advanced features from the user manual to the developer manual --- doc/{cprover-manual => architectural}/goto-harness.md | 0 doc/{cprover-manual => architectural}/memory-analyzer.md | 0 .../restrict-function-pointer.md | 0 doc/cprover-manual/index.md | 5 +---- 4 files changed, 1 insertion(+), 4 deletions(-) rename doc/{cprover-manual => architectural}/goto-harness.md (100%) rename doc/{cprover-manual => architectural}/memory-analyzer.md (100%) rename doc/{cprover-manual => architectural}/restrict-function-pointer.md (100%) diff --git a/doc/cprover-manual/goto-harness.md b/doc/architectural/goto-harness.md similarity index 100% rename from doc/cprover-manual/goto-harness.md rename to doc/architectural/goto-harness.md diff --git a/doc/cprover-manual/memory-analyzer.md b/doc/architectural/memory-analyzer.md similarity index 100% rename from doc/cprover-manual/memory-analyzer.md rename to doc/architectural/memory-analyzer.md diff --git a/doc/cprover-manual/restrict-function-pointer.md b/doc/architectural/restrict-function-pointer.md similarity index 100% rename from doc/cprover-manual/restrict-function-pointer.md rename to doc/architectural/restrict-function-pointer.md diff --git a/doc/cprover-manual/index.md b/doc/cprover-manual/index.md index 9be7116c2a9..5ea3dd3026e 100644 --- a/doc/cprover-manual/index.md +++ b/doc/cprover-manual/index.md @@ -8,10 +8,7 @@ [A Short Tutorial](cbmc/tutorial/), [Loop Unwinding](cbmc/unwinding/), -[Assertion Checking](cbmc/assertions/), -[Restricting function pointers](cbmc/restrict-function-pointer/), -[Memory Analyzer](cbmc/memory-analyzer/), -[Program Harness](cbmc/goto-harness/) +[Assertion Checking](cbmc/assertions/) ## 4. [Test Suite Generation](test-suite/) From 93b9e97980a01b9431917c8c129e10eae420e1d7 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 1 May 2020 16:54:09 +0100 Subject: [PATCH 03/12] Fix dead links in cprover manual --- doc/cprover-manual/api.md | 2 +- doc/cprover-manual/cbmc-assertions.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/cprover-manual/api.md b/doc/cprover-manual/api.md index 85996bbbf26..e785f0cc2b1 100644 --- a/doc/cprover-manual/api.md +++ b/doc/cprover-manual/api.md @@ -18,7 +18,7 @@ void assert(_Bool assertion); The function **\_\_CPROVER\_assume** adds an expression as a constraint 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.md). +section on [Assumptions](../modeling/assumptions/). #### \_\_CPROVER\_r_ok, \_\_CPROVER\_w_ok diff --git a/doc/cprover-manual/cbmc-assertions.md b/doc/cprover-manual/cbmc-assertions.md index 8bbfb6ddd20..2426863ca6a 100644 --- a/doc/cprover-manual/cbmc-assertions.md +++ b/doc/cprover-manual/cbmc-assertions.md @@ -33,7 +33,7 @@ properties together with the condition. The assertion language of the CPROVER tools is identical to the language used for expressions. Note that -[nondeterminism](./modeling-nondeterminism.md) can be exploited in order +[nondeterminism](../../modeling/nondeterminism/) can be exploited in order to check a range of choices. As an example, the following code fragment asserts that **all** elements of the array are zero: From d4c5e9952c091e7ffd54c0698c445b82c3f9d9df Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Wed, 29 Apr 2020 17:20:47 +0100 Subject: [PATCH 04/12] Tests for incremental status with multiple properties The incremental status should report failure from the first unwinding for which one property is falsified. --- .../multiple-asserts/test-no-cp.desc | 19 +++++++++++++++++++ .../cbmc-incr-oneloop/multiple-asserts/test.c | 9 +++++++++ .../multiple-asserts/test.desc | 17 +++++++++++++++++ 3 files changed, 45 insertions(+) create mode 100644 regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc create mode 100644 regression/cbmc-incr-oneloop/multiple-asserts/test.c create mode 100644 regression/cbmc-incr-oneloop/multiple-asserts/test.desc diff --git a/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc b/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc new file mode 100644 index 00000000000..d581fd8198f --- /dev/null +++ b/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc @@ -0,0 +1,19 @@ +CORE +test.c +--incremental-loop main.0 --no-propagation +activate-multi-line-match +Current unwinding: 1\nUnwinding .*\nIncremental status: INCONCLUSIVE +Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE +Current unwinding: 7\nUnwinding .*\nIncremental status: FAILURE +Current unwinding: 9\nUnwinding .*\nIncremental status: FAILURE +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +-- +Ensure that with multiple properties, the incremental status +switches to failure as soon as one property has been falsified +but keeps unwinding till it has resolved them all + +Use `--no-propagation` to ensure that even the output is the same regardless of whether the asserts are checked via the solver or the constant propagator diff --git a/regression/cbmc-incr-oneloop/multiple-asserts/test.c b/regression/cbmc-incr-oneloop/multiple-asserts/test.c new file mode 100644 index 00000000000..b59f9ef2ad5 --- /dev/null +++ b/regression/cbmc-incr-oneloop/multiple-asserts/test.c @@ -0,0 +1,9 @@ +int main() +{ + for(int i = 0; i < 10; ++i) + { + assert(i != 5); + assert(i != 8); + } + return 0; +} diff --git a/regression/cbmc-incr-oneloop/multiple-asserts/test.desc b/regression/cbmc-incr-oneloop/multiple-asserts/test.desc new file mode 100644 index 00000000000..56cefb5161f --- /dev/null +++ b/regression/cbmc-incr-oneloop/multiple-asserts/test.desc @@ -0,0 +1,17 @@ +CORE +test.c +--incremental-loop main.0 +activate-multi-line-match +Current unwinding: 1\nUnwinding .*\nIncremental status: INCONCLUSIVE +Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE +Current unwinding: 7\nUnwinding .*\nIncremental status: FAILURE +Current unwinding: 9\nUnwinding .*\nIncremental status: FAILURE +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +-- +Ensure that with multiple properties, the incremental status +switches to failure as soon as one property has been falsified +but keeps unwinding till it has resolved them all From 22bce6fc6eceb58496130774382f9eee07811ccf Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Wed, 22 Apr 2020 18:24:19 +0100 Subject: [PATCH 05/12] Print incremental-status when doing incremental solving It is not possible to conclude successful verification before the unwinding has finished, so this prints inconclusive until the analysis is complete. However, if one property has been falsified, then even though the analysis can continue to check other properties, the verification will certainly fail. --- .../single_loop_incremental_symex_checker.cpp | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/src/goto-checker/single_loop_incremental_symex_checker.cpp index 0c2e12770f7..ee3eef4db11 100644 --- a/src/goto-checker/single_loop_incremental_symex_checker.cpp +++ b/src/goto-checker/single_loop_incremental_symex_checker.cpp @@ -47,6 +47,23 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert( prop_conv_solver->set_all_frozen(); } +void output_incremental_status( + const propertiest &properties, + messaget &message_hander) +{ + const auto any_failures = std::any_of( + properties.begin(), + properties.end(), + [](const std::pair &property) { + return property.second.status == property_statust::FAIL; + }); + std::string status = any_failures ? "FAILURE" : "INCONCLUSIVE"; + structured_datat incremental_status{ + {{labelt({"incremental", "status"}), + structured_data_entryt::data_node(json_stringt(status))}}}; + message_hander.statistics() << incremental_status; +} + incremental_goto_checkert::resultt single_loop_incremental_symex_checkert:: operator()(propertiest &properties) { @@ -64,6 +81,8 @@ operator()(propertiest &properties) update_properties_status_from_symex_target_equation( properties, result.updated_properties, equation); + output_incremental_status(properties, log); + initial_equation_generated = true; } @@ -162,6 +181,8 @@ operator()(propertiest &properties) properties, result.updated_properties, equation); current_equation_converted = false; + + output_incremental_status(properties, log); } return result; From fdbbf7e8f2c892e4a20c61ecd2d747649eb481d6 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 1 May 2020 18:13:59 +0100 Subject: [PATCH 06/12] Tweak where we print the incremental status We want to print the status after we've done any solving for that unwind, but before we've done an extra step of symexing. We should not print in the event the full equation has been generated, as then we have a full solution so ins't incremental. Ditto we don't need to print the status if we've found a failure, as this function will be called again to do the next symex invocation if there are further propreties to check --- src/goto-checker/single_loop_incremental_symex_checker.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/src/goto-checker/single_loop_incremental_symex_checker.cpp index ee3eef4db11..e4fae0efa07 100644 --- a/src/goto-checker/single_loop_incremental_symex_checker.cpp +++ b/src/goto-checker/single_loop_incremental_symex_checker.cpp @@ -81,8 +81,6 @@ operator()(propertiest &properties) update_properties_status_from_symex_target_equation( properties, result.updated_properties, equation); - output_incremental_status(properties, log); - initial_equation_generated = true; } @@ -171,6 +169,8 @@ operator()(propertiest &properties) break; } + output_incremental_status(properties, log); + // We continue symbolic execution full_equation_generated = !symex.resume(goto_symext::get_goto_function(goto_model)); @@ -181,8 +181,6 @@ operator()(propertiest &properties) properties, result.updated_properties, equation); current_equation_converted = false; - - output_incremental_status(properties, log); } return result; From 0e6cfbf190eff86f117049dd8ed7d7ee415b345e Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 1 May 2020 18:15:06 +0100 Subject: [PATCH 07/12] Adapt tests for printing We now print after all solving, and the last thing before the next increment, therefore the printing checks are easier to check immediately precedes the next unwinding, rather than checking appears after the increment we are talking about. --- regression/cbmc-incr-oneloop/alarm1/test.desc | 2 ++ regression/cbmc-incr-oneloop/alarm2/test.desc | 4 ++-- .../cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc | 7 +++---- regression/cbmc-incr-oneloop/multiple-asserts/test.desc | 7 +++---- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/regression/cbmc-incr-oneloop/alarm1/test.desc b/regression/cbmc-incr-oneloop/alarm1/test.desc index 70a9179b47d..87b0754ad15 100644 --- a/regression/cbmc-incr-oneloop/alarm1/test.desc +++ b/regression/cbmc-incr-oneloop/alarm1/test.desc @@ -1,8 +1,10 @@ CORE main.c --incremental-loop main.0 --unwind-max 15 +activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ +Incremental status: INCONCLUSIVE\nCurrent unwinding: 15 -- ^warning: ignoring diff --git a/regression/cbmc-incr-oneloop/alarm2/test.desc b/regression/cbmc-incr-oneloop/alarm2/test.desc index 576ae8bac92..e36848a5583 100644 --- a/regression/cbmc-incr-oneloop/alarm2/test.desc +++ b/regression/cbmc-incr-oneloop/alarm2/test.desc @@ -4,8 +4,8 @@ main.c activate-multi-line-match Current unwinding: 1 Incremental status: INCONCLUSIVE -Current unwinding: 5\nUnwinding .*\nIncremental status: INCONCLUSIVE -Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE +Incremental status: INCONCLUSIVE\nCurrent unwinding: 6 +Incremental status: INCONCLUSIVE\nCurrent unwinding: 7 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc b/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc index d581fd8198f..6eff8fddefd 100644 --- a/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc +++ b/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc @@ -2,10 +2,9 @@ CORE test.c --incremental-loop main.0 --no-propagation activate-multi-line-match -Current unwinding: 1\nUnwinding .*\nIncremental status: INCONCLUSIVE -Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE -Current unwinding: 7\nUnwinding .*\nIncremental status: FAILURE -Current unwinding: 9\nUnwinding .*\nIncremental status: FAILURE +Incremental status: INCONCLUSIVE\nCurrent unwinding: 2 +Incremental status: INCONCLUSIVE\nCurrent unwinding: 6 +Incremental status: FAILURE\nCurrent unwinding: 7 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/multiple-asserts/test.desc b/regression/cbmc-incr-oneloop/multiple-asserts/test.desc index 56cefb5161f..11e06f6d641 100644 --- a/regression/cbmc-incr-oneloop/multiple-asserts/test.desc +++ b/regression/cbmc-incr-oneloop/multiple-asserts/test.desc @@ -2,10 +2,9 @@ CORE test.c --incremental-loop main.0 activate-multi-line-match -Current unwinding: 1\nUnwinding .*\nIncremental status: INCONCLUSIVE -Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE -Current unwinding: 7\nUnwinding .*\nIncremental status: FAILURE -Current unwinding: 9\nUnwinding .*\nIncremental status: FAILURE +Incremental status: INCONCLUSIVE\nCurrent unwinding: 2 +Incremental status: INCONCLUSIVE\nCurrent unwinding: 6 +Incremental status: FAILURE\nCurrent unwinding: 7 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ From 3f6f0ca56ad90a9d1e6f9e09a7859a921f3635ef Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 1 May 2020 18:15:36 +0100 Subject: [PATCH 08/12] Add tests for when the program verifies In this case, the status is inconclusive until completion, at which point success will be reported by CBMC overall. --- .../cbmc-incr-oneloop/valid-asserts/test.c | 8 ++++++++ .../cbmc-incr-oneloop/valid-asserts/test.desc | 16 ++++++++++++++++ 2 files changed, 24 insertions(+) create mode 100644 regression/cbmc-incr-oneloop/valid-asserts/test.c create mode 100644 regression/cbmc-incr-oneloop/valid-asserts/test.desc diff --git a/regression/cbmc-incr-oneloop/valid-asserts/test.c b/regression/cbmc-incr-oneloop/valid-asserts/test.c new file mode 100644 index 00000000000..6654dc75460 --- /dev/null +++ b/regression/cbmc-incr-oneloop/valid-asserts/test.c @@ -0,0 +1,8 @@ +int main() +{ + for(int i = 0; i < 10; ++i) + { + assert(i != 10); + } + return 0; +} diff --git a/regression/cbmc-incr-oneloop/valid-asserts/test.desc b/regression/cbmc-incr-oneloop/valid-asserts/test.desc new file mode 100644 index 00000000000..36ddf206c3a --- /dev/null +++ b/regression/cbmc-incr-oneloop/valid-asserts/test.desc @@ -0,0 +1,16 @@ +CORE +test.c +--incremental-loop main.0 +activate-multi-line-match +Incremental status: INCONCLUSIVE\nCurrent unwinding: 2 +Incremental status: INCONCLUSIVE\nCurrent unwinding: 10 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +Incremental status: SUCCESS +-- +Check that for valid asserts, the incremental status is inconclusive +as it is only after the incrementer has been stopped we conclude is +verified. From 4972f5491793e888bf491bb601d3e0efe17ac129 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 1 May 2020 18:19:54 +0100 Subject: [PATCH 09/12] Add test to check for no incremental status when no properties to check --- regression/cbmc-incr-oneloop/no-asserts/test.c | 8 ++++++++ regression/cbmc-incr-oneloop/no-asserts/test.desc | 11 +++++++++++ 2 files changed, 19 insertions(+) create mode 100644 regression/cbmc-incr-oneloop/no-asserts/test.c create mode 100644 regression/cbmc-incr-oneloop/no-asserts/test.desc diff --git a/regression/cbmc-incr-oneloop/no-asserts/test.c b/regression/cbmc-incr-oneloop/no-asserts/test.c new file mode 100644 index 00000000000..1acd435d55a --- /dev/null +++ b/regression/cbmc-incr-oneloop/no-asserts/test.c @@ -0,0 +1,8 @@ +int main() +{ + for(int i = 0; i < 10; ++i) + { + } + // nothing to check + return 0; +} diff --git a/regression/cbmc-incr-oneloop/no-asserts/test.desc b/regression/cbmc-incr-oneloop/no-asserts/test.desc new file mode 100644 index 00000000000..a5c2f27a5d6 --- /dev/null +++ b/regression/cbmc-incr-oneloop/no-asserts/test.desc @@ -0,0 +1,11 @@ +CORE +test.c +--incremental-loop main.0 +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +Incremental status +-- +Verify no incremental status updates when no properties to check From 74a76480387ab783ffe26784ccf78c5d8c0edad8 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 4 May 2020 22:38:21 +0100 Subject: [PATCH 10/12] Add documentation for memory primitives --- doc/architectural/memory-primitives.md | 216 +++++++++++++++++++++++++ 1 file changed, 216 insertions(+) create mode 100644 doc/architectural/memory-primitives.md diff --git a/doc/architectural/memory-primitives.md b/doc/architectural/memory-primitives.md new file mode 100644 index 00000000000..7ce7dbcf3d8 --- /dev/null +++ b/doc/architectural/memory-primitives.md @@ -0,0 +1,216 @@ +\ingroup module_hidden +\page memory-primitives Memory Primitives + +This document describes the semantics and usage of memory-related and +pointer-related primitives in CBMC. + + +# Background + + +## 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 +pointers as having 64 bits. This can be changed by various options (see section +"C/C++ frontend options" in the output of `cbmc --help`). + +Memory is represented in CBMC as a set of objects. Each object represents a +contiguous sequence of bytes and is identified via a numeric object ID. For +example, assuming integers of width 4 and chars of with 1, a global integer +variable would correspond to an object of size 4, and memory allocated via +`malloc(10)` would correspond to an object of size 10. + +A pointer then consists of two parts: the upper n bits form the object ID, and +the remaining bits form the offset. The object ID part holds the ID of the +object the pointer is pointing to, and the offset part holds the byte offset +within that object. The offset is signed.1 The null pointer is the +pointer with object ID 0 and offset 0. CBMC uses 8 bits by default to represent +the object ID. This can be changed via the `--object-bits ` option. + +There are three primitives which directly operate on the value of a pointer: + +- `__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *p)` +- `__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *p)` +- `_Bool __CPROVER_same_object(const void *p, const void *q)` + +The primitive `__CPROVER_POINTER_OBJECT(p)` retrieves the object ID part of a +pointer, and the primitive `__CPROVER_POINTER_OFFSET(p)` retrieves the offset +part of a pointer. The `__CPROVER_same_object(p, q)` primitive simply compares +the object IDs of the two given pointers. That is, it is true if and only if +`__CPROVER_POINTER_OBJECT(p) == __CPROVER_POINTER_OBJECT(q)`. It is always valid +to apply these three primitives to a pointer (i.e., they do not have any special +preconditions). + +## 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 +or malloced memory). CBMC deterministically assigns consecutive object IDs to +memory objects as it encounters them. For example: + +```C +... +char c; + +char *p = &c; // object ID n +char *q = malloc(10); // object ID n + 1 + +``` + +Here the pointers `p` and `q` would contain consecutive IDs in their object ID +parts (as retrieved by `__CPROVER_POINTER_OBJECT()`). Due to the deterministic +assignment of object IDs, bugs that can only be exposed with specific pointer +values cannot be found by CBMC. For example: + +```C +char *p = malloc(1); // assume cbmc assigns object ID 0xE to the malloced memory +assert(p != (char *)0x0F00000000000000); +``` + +CBMC will report verification successful for this code snippet (assuming it +assigns an object ID other than 0x0F to the malloced memory). However, assuming +that `malloc()` could allocate memory at any address, the assertion could fail. + +Moreover, CBMC does not reuse object IDs for malloced memory. For example: + +```C +char *p = malloc(1); +free(p); +char *q = malloc(1); +assert(p != q); +``` + +CBMC would report verification successful on this code snippet. However, +assuming that `malloc()` could reuse deallocated addresses, the assertion could +fail. + +The memory objects in CBMC are independent of each other. That is, for example, +when incrementing a pointer past the bounds of an object, the pointer will never +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. + +## 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 +inputs. For example: + +```C +int i; +__CPROVER_assume(i < 0); +int result = rectify(i); +assert(result == 0); +``` + +Here, the value of `i` is nondeterministically chosen from all the possible +integer values, and then constrained to negative values via the assumption. +In CBMC, like uninitialized integers, uninitialized pointers are treated as +having a nondeterministic value. That is, the value of the pointer itself is +nondeterministically chosen, though **no memory is allocated**. Therefore, +pointers should be explicitely initialized to ensure that they are backed by +valid memory. + + +# Memory Primitives + +In this section, we describe further memory primitives of CBMC. Above, we have +already encountered the primitives `__CPROVER_POINTER_OBJECT(p)`, +`__CPROVER_POINTER_OFFSET(p)`, and `__CPROVER_same_object(p, q)`. These +primitives just retrieve the object ID part or offset part of a pointer, or +compare the object ID parts of two pointers. It is always valid to apply these +primitives to a pointer (i.e., they do not have any special preconditions). + +In the following, we need the concept of a valid pointer. A pointer is *valid* +if it points to a live memory object. That is, it points to the start or to +somewhere within the sequence of bytes that makes up the memory object. + +Conversely, a pointer is invalid if it is null, uninitialized, points to +deallocated dynamic memory, points to an out-of-scope local variable, or has a +value that does not point to (dynamically, automatically, or statically) +allocated memory, or is out of bounds of the memory object it points to (i.e., +the memory object identified by `__CPROVER_POINTER_OBJECT(p)`). + +The primitives below have unspecified semantics on pointers that are neither +null nor valid. CBMC has an option `--pointer-primitive-check` (see section +[Detecting potential misuses of memory primitives](#detecting-potential-misuses-of-memory-primitives) below) +to check that pointers used in the primitives are either null or valid. + + +## 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: + +- `__CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *p)` + +If `p` is the null pointer, the primitive returns 0. If `p` is valid, the +primitive returns the size of the memory object the pointer points to. +Otherwise, the semantics is unspecified. In particular, it is valid to apply +this primitive to a pointer that points to within a memory object (i.e., not +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 + +The following primitive can be used to check whether a pointer points to dynamic +(malloced, heap) memory: + +- `_Bool __CPROVER_DYNAMIC_OBJECT(const void *p)` + +If `p` is the null pointer, the primitive returns false. If `p` is valid, the +primitive returns true if the pointer points to dynamically allocated memory, +and false otherwise. If `p` is neither null nor valid, the semantics is +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 + +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 +number of bytes: + +- `_Bool __CPROVER_r_ok(const void *p, size_t size)` +- `_Bool __CPROVER_w_ok(const void *p, size_t size)` + +At present, both primitives are equivalent as all memory in CBMC is considered +both readable and writeable. If `p` is the null pointer, the primitives return +false. If `p` is valid, the primitives return true if the memory segment +starting at the pointer has at least the given size, and false otherwise. If `p` +is neither null nor valid, the semantics is unspecified. It is valid to apply +the primitive to pointers that point to within a memory object. For example: + +```C +char *p = malloc(10); +assert(__CPROVER_r_ok(p, 10)); // valid +p += 5; +assert(__CPROVER_r_ok(p, 3)); // valid +assert(__CPROVER_r_ok(p, 10)); // fails +``` + +# 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. +CBMC has the option `--pointer-primitive-check` to detect potential misuses of +the memory primitives. It checks that the pointers that appear in the following +primitives are either null or valid: + +- `__CPROVER_POINTER_OBJECT` +- `__CPROVER_POINTER_OFFSET` +- `__CPROVER_same_object` +- `__CPROVER_OBJECT_SIZE` +- `__CPROVER_DYNAMIC_OBJECT` +- `__CPROVER_r_ok` +- `__CPROVER_w_ok` + +While the first three primitives have well-defined semantics even on invalid +pointers, using them on invalid pointers is usually unintended in user programs. +Thus, they have been included in the `--pointer-primitive-check` option. + +1 Pointers with negative offsets never point to memory objects. +Negative values are used internally to detect pointer underflows. + From 62a4b557d7cf9e9be59e118d1fac5d937ae79394 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 5 May 2020 11:49:49 +0100 Subject: [PATCH 11/12] Adapt user manual description of memory primitives --- doc/cprover-manual/api.md | 68 +++++++++++++++++++++++---------------- 1 file changed, 41 insertions(+), 27 deletions(-) diff --git a/doc/cprover-manual/api.md b/doc/cprover-manual/api.md index e785f0cc2b1..5d191cc212c 100644 --- a/doc/cprover-manual/api.md +++ b/doc/cprover-manual/api.md @@ -20,33 +20,6 @@ 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\_r_ok, \_\_CPROVER\_w_ok - -```C -void __CPROVER_r_ok(const void *, size_t size); -void __CPROVER_w_ok(const void *, size_t size); -``` - -The function **\_\_CPROVER\_r_ok** returns true if reading the piece of -memory starting at the given pointer with the given size is safe. -**\_\_CPROVER\_w_ok** does the same with writing. - -#### \_\_CPROVER\_same\_object, \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_DYNAMIC\_OBJECT - -```C -_Bool __CPROVER_same_object(const void *, const void *); -__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *p); -__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *p); -_Bool __CPROVER_DYNAMIC_OBJECT(const void *p); -``` - -The function **\_\_CPROVER\_same\_object** returns true if the two -pointers given as arguments point to the same object. The function -**\_\_CPROVER\_POINTER\_OFFSET** returns the offset of the given pointer -relative to the base address of the object. The function -**\_\_CPROVER\_DYNAMIC\_OBJECT** returns true if the pointer passed as -arguments points to a dynamically allocated object. - #### \_\_CPROVER\_input, \_\_CPROVER\_output ```C @@ -156,6 +129,47 @@ the array **dest** with the given value. Uninterpreted functions are documented [here](./modeling-nondeterminism.md)). +### Memory-Related Functions + +The semantics of the primitives listed in this section is described in more detail in the +document about [Memory Primitives](http://cprover.diffblue.com/memory-primitives.html). + +#### \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_same\_object + +```C +__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *p); +__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *p); +_Bool __CPROVER_same_object(const void *p, const void *q); +``` + +The function **\_\_CPROVER\_POINTER\_OBJECT** returns the ID of the object the +pointer points to. The function **\_\_CPROVER\_POINTER\_OFFSET** returns the +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 + +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 +[Memory Primitives](http://cprover.diffblue.com/memory-primitives.html) +for more details. It also includes a description of the `--pointer-primitive-check` +option to verify the preconditions of the primitives. + +```C +__CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *p); +_Bool __CPROVER_DYNAMIC_OBJECT(const void *p); +void __CPROVER_r_ok(const void *p, size_t size); +void __CPROVER_w_ok(const void *p, size_t size); +``` + +The function **\_\_CPROVER_\_OBJECT\_SIZE** returns the size of the object the +given pointer points to. The function **\_\_CPROVER\_DYNAMIC\_OBJECT** returns +true if the pointer passed as an argument points to a dynamically allocated +object. The function **\_\_CPROVER\_r_ok** returns true if reading the piece of +memory starting at the given pointer with the given size is safe. +**\_\_CPROVER\_w_ok** does the same with writing. + ### Predefined Types and Symbols #### \_\_CPROVER\_bitvector From 5b3640ada52f23f41d1c967b44205fbd60b8cd8a Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 17 Apr 2020 18:32:09 +0100 Subject: [PATCH 12/12] Correct typo in comment --- regression/validate-trace-xml-schema/check.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index eaec65c09c7..2d4b55f6c95 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -12,7 +12,7 @@ # some tests in the cbmc suite don't work for the trace checks for one reason or another ExcludedTests = list(map(lambda s: os.path.join(test_base_dir, s), [ - # these tests except input from stdin + # these tests expect input from stdin 'json-interface1/test_wrong_option.desc', 'json-interface1/test.desc', 'json-interface1/test_wrong_flag.desc',