Open
Description
CBMC version: 5.37.0
Operating system: N/A
How to reproduce
#include <stdlib.h>
#include <stdbool.h>
typedef struct b_st {
int v;
} b_st;
static const b_st b1 = { .v = 1 };
static const b_st b2 = { .v = 2 };
typedef struct a_st {
int v;
struct b_st* b;
} a_st;
a_st * new_a() {
a_st *a = malloc(sizeof(*a));
a->v = 0;
a->b = nondet_int()%2 ? &b1 : &b2;
return a;
}
bool b_is_set(a_st *a) {
if (!__CPROVER_w_ok(a)) return false;
a->b = nondet_int()%2 ? &b1 : &b2;
return true;
}
int get_b(a_st *a)
__CPROVER_requires(__CPROVER_is_fresh(a, sizeof(*a)))
// __CPROVER_requires(b_is_set(a)) // PROBLEM 3
// __CPROVER_requires(__CPROVER_is_fresh(a->b, sizeof(*(a->b)))) // PROBLEM 1
__CPROVER_requires(a->b == &b1 || a->b == &b2)
// __CPROVER_requires(__CPROVER_is_fresh(a->b, sizeof(*(a->b)))) // PROBLEM 2
__CPROVER_ensures(__CPROVER_return_value == 1 || __CPROVER_return_value == 2)
{
// a->b = nondet_int()%2 ? &b1 : &b2; // PROBLEM 4
return a->b->v;
}all:
goto-cc --export-file-local-symbols example.c -o example.c1.goto
goto-cc --function get_b example.c1.goto -o example.c2.goto
goto-instrument --enforce-contract get_b example.c2.goto example.c3.goto
goto-instrument --drop-unused-functions example.c3.goto example.c4.goto
goto-instrument --slice-global-inits example.c4.goto example.c5.goto
goto-instrument --show-goto-functions example.c5.goto > example.c5.txt
cbmc --unwind 1 --flush --object-bits 8 --malloc-may-fail --malloc-fail-null --cover location example.c5.goto >coverage.txt 2>coverage-err.log
cbmc --unwind 1 --flush --object-bits 8 --pointer-primitive-check --malloc-may-fail --malloc-fail-null --bounds-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-check --pointer-overflow-check --pointer-primitive-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --show-properties $(XML_UI) example.c5.goto >property.txt 2>property-err.log
cbmc --program-only --unwind 1 --flush --object-bits 8 --pointer-primitive-check --malloc-may-fail --malloc-fail-null --bounds-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-check --pointer-overflow-check --pointer-primitive-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --trace $(XML_UI) example.c5.goto >result-program-only.txt 2>result-program-only-err.log
cbmc --unwind 1 --flush --object-bits 8 --pointer-primitive-check --malloc-may-fail --malloc-fail-null --bounds-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-check --pointer-overflow-check --pointer-primitive-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --trace $(XML_UI) example.c5.goto >result.txt 2>result-err.log
clean:
rm -f *.goto *.txt *.log *~
.PHONY: all cleanRun make all.
The issue
Using the current approach relying on __CPROVER_is_fresh(p,size) it is impossible to describe objects which are partly malloc'd and partly pointing to static objects.
In this example struct a has a field b that is meant to point to one of two static objects b1 or b2 (check the new_a() function).
In the get_b function contract, we want to express that a is fresh, and that a->b points to either static const b1 or static const b2.
problem 0
typedef struct b_st {
int v;
} b_st;
static const b_st b1 = { .v = 1 };
static const b_st b2 = { .v = 2 };
typedef struct a_st {
int v;
struct b_st* b;
} a_st;
a_st * new_a() {
a_st *a = malloc(sizeof(*a));
a->v = 0;
a->b = nondet_int()%2 ? &b1 : &b2;
return a;
}
int get_b(a_st *a)
__CPROVER_requires(__CPROVER_is_fresh(a, sizeof(*a)))
__CPROVER_requires(a->b == &b1 || a->b == &b2)
__CPROVER_ensures(__CPROVER_return_value == 1 || __CPROVER_return_value == 2)
{
return a->b->v;
}
Analysing this contract we get an error trace:
tail restult.txt
[pointer_primitives.1] file example.c line 80 pointer invalid in POINTER_OBJECT(tmp_cc$0->b): FAILURE
[pointer_primitives.4] file example.c line 80 pointer outside object bounds in POINTER_OBJECT(tmp_cc$0->b): FAILURE
[pointer_primitives.8] file example.c line 80 pointer outside object bounds in POINTER_OBJECT(tmp_cc$0->b): FAILURE
[pointer_primitives.12] file example.c line 80 pointer outside object bounds in POINTER_OBJECT(tmp_cc$0->b): FAILURE
[pointer_primitives.16] file example.c line 80 pointer outside object bounds in POINTER_OFFSET(tmp_cc$0->b): FAILURE
[pointer_primitives.20] file example.c line 80 pointer outside object bounds in POINTER_OFFSET(tmp_cc$0->b): FAILURE
[pointer_primitives.24] file example.c line 80 pointer outside object bounds in OBJECT_SIZE(tmp_cc$0->b): FAILURE
[postcondition.1] file example.c line 81 Check ensures clause: FAILURE
problem 1
Adding a requirement that a->b is some valid object using is_fresh
int get_b(a_st *a)
__CPROVER_requires(__CPROVER_is_fresh(a, sizeof(*a)))
__CPROVER_requires(__CPROVER_is_fresh(a->b, sizeof(*(a->b))))
__CPROVER_requires(a->b == &b1 || a->b == &b2)
__CPROVER_ensures(__CPROVER_return_value == 1 || __CPROVER_return_value == 2)
{
return a->b->v;
}
We get a vacuous instance: proving all assertions with zero code coverage
❯ tail result.txt
[get_b.pointer_dereference.6] line 84 dereference failure: invalid integer address in a->b: SUCCESS
[get_b.pointer_dereference.7] line 84 dereference failure: pointer NULL in a->b->v: SUCCESS
[get_b.pointer_dereference.8] line 84 dereference failure: pointer invalid in a->b->v: SUCCESS
[get_b.pointer_dereference.9] line 84 dereference failure: deallocated dynamic object in a->b->v: SUCCESS
[get_b.pointer_dereference.10] line 84 dereference failure: dead object in a->b->v: SUCCESS
[get_b.pointer_dereference.11] line 84 dereference failure: pointer outside object bounds in a->b->v: SUCCESS
[get_b.pointer_dereference.12] line 84 dereference failure: invalid integer address in a->b->v: SUCCESS
** 0 of 62 failed (1 iterations)
VERIFICATION SUCCESSFUL
❯ tail coverage.txt
[__CPROVER_contracts_original_get_b.coverage.1] file example.c line 84 function __CPROVER_contracts_original_get_b block 1 (lines example.c:get_b:84,85): FAILED
[get_b.coverage.13] file example.c line 82 function get_b block 13 (lines example.c::82; instrumented for code contracts::0): FAILED
[get_b.coverage.12] file example.c line 82 function get_b block 12 (lines example.c::82): FAILED
[get_b.coverage.6] file example.c line 81 function get_b block 6 (lines example.c::81): FAILED
problem 3
Adding the is_fresh assertion after the other assertion does not result in a vacuous instance but allows to falsify the post condition with a spurious trace.
int get_b(a_st *a)
__CPROVER_requires(__CPROVER_is_fresh(a, sizeof(*a)))
__CPROVER_requires(a->b == &b1 || a->b == &b2)
__CPROVER_requires(__CPROVER_is_fresh(a->b, sizeof(*(a->b))))
__CPROVER_ensures(__CPROVER_return_value == 1 || __CPROVER_return_value == 2)
{
return a->b->v;
}
❯ tail result.txt
Violated property:
file example.c function get_b line 82 thread 0
Check ensures clause
tmp_cc == 1 || tmp_cc == 2
** 1 of 62 failed (2 iterations)
VERIFICATION FAILED
❯ tail coverage.txt
[get_b.coverage.13] file example.c line 82 function get_b block 13 (lines example.c::82; instrumented for code contracts::0): SATISFIED
[get_b.coverage.12] file example.c line 82 function get_b block 12 (lines example.c::82): SATISFIED
[get_b.coverage.11] file example.c line 80 function get_b block 11 (lines example.c::80): SATISFIED
[get_b.coverage.9] file example.c line 81 function get_b block 9 (lines example.c::81): SATISFIED
[get_b.coverage.8] file example.c line 81 function get_b block 8 (lines example.c::81): SATISFIED
[get_b.coverage.7] file example.c line 81 function get_b block 7 (lines example.c::81): SATISFIED
[get_b.coverage.6] file example.c line 81 function get_b block 6 (lines example.c::81): SATISFIED
[get_b.coverage.5] file example.c line 80 function get_b block 5 (lines example.c::80): SATISFIED
[get_b.coverage.3] file example.c line 80 function get_b block 3 (lines example.c::80): SATISFIED
[get_b.coverage.2] file example.c line 79 function get_b block 2 (lines example.c::79,80): SATISFIED
[get_b.coverage.1] file example.c line 82 function get_b block 1 (lines example.c::79,82): SATISFIED
[get_b.coverage.4] file example.c line 80 function get_b block 4 (lines example.c::80): SATISFIED
[get_b.coverage.10] file example.c line 80 function get_b block 10 (lines example.c::80): SATISFIED
[__CPROVER_contracts_original_get_b.coverage.1] file example.c line 84 function __CPROVER_contracts_original_get_b block 1 (lines example.c:get_b:84,85): SATISFIED
workaround 1
Use a side-effecting predicate that assigns a->b in the preconditions which is not ideal.
bool b_is_set(a_st *a) {
if (!__CPROVER_w_ok(a)) return false;
a->b = nondet_int()%2 ? &b1 : &b2;
return true;
}
int get_b(a_st *a)
__CPROVER_requires(__CPROVER_is_fresh(a, sizeof(*a)))
__CPROVER_requires(b_is_set(a))
__CPROVER_ensures(__CPROVER_return_value == 1 || __CPROVER_return_value == 2)
{
return a->b->v;
}
workaround 2
assign a->b = nondet_int()%2 ? &b1 : &b2; in the function body. Works but modifies the code.