Skip to content

Custom memory predicates don't work for non-pointer args #8692

@archigup

Description

@archigup

I was attempting to follow the docs section titled "Writing your own memory predicates" at https://diffblue.github.io/cbmc/contracts-memory-predicates.html.

However the memory predicates do not work for non-pointer args.

For example, lets start with this working file:

test.c:

#include <assert.h>
#include <stdbool.h>
#include <stddef.h>

struct Buffer {
    char *ptr;
    size_t len;
};

bool foo(struct Buffer buf)
    __CPROVER_requires(buf.len == 0 || __CPROVER_is_fresh(buf.ptr, buf.len)) {
    if (buf.len > 0) {
        return buf.ptr[buf.len - 1] == 0;
    }
    return false;
}

int main(void) {
    struct Buffer buf;
    foo(buf);
}

The above passes:

0$ goto-cc test.c -o test.goto 
$ goto-instrument --dfcc main --enforce-contract foo test.goto test.goto
Reading GOTO program from 'test.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Trying to force one backedge per target
Loading CPROVER C library (x86_64)
Adding the cprover_contracts library (x86_64)
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
Instrumenting harness function 'main'
Wrapping 'foo' with contract 'foo' in CHECK mode
Instrumenting 'malloc'
Instrumenting 'free'
Specializing cprover_contracts functions for assigns clauses of at most 0 targets
Removing unused functions
generate function bodies: No function name matched regex
Updating init function
Setting entry point to main
Writing GOTO program to 'test.goto'
$ cbmc test.goto 
CBMC version 6.7.1 (n/a) 64-bit x86_64 linux
Reading GOTO program from file test.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is UNSATISFIABLE

** Results:
<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_car_create
[__CPROVER_contracts_car_create.assertion.1] line 126 ptr NULL or writable up to size: SUCCESS
[__CPROVER_contracts_car_create.assertion.2] line 129 CAR size is less than __CPROVER_max_malloc_size: SUCCESS
[__CPROVER_contracts_car_create.assertion.3] line 133 no offset bits overflow on CAR upper bound computation: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_is_fresh
[__CPROVER_contracts_is_fresh.assertion.1] line 1317 __CPROVER_is_fresh max allocation size exceeded: SUCCESS
[__CPROVER_contracts_is_fresh.assertion.2] line 1331 __CPROVER_is_fresh does not conflict with other pointer predicate in assume context: SUCCESS
[__CPROVER_contracts_is_fresh.assertion.3] line 1374 __CPROVER_is_fresh requires size <= __CPROVER_max_malloc_size: SUCCESS
[__CPROVER_contracts_is_fresh.assertion.4] line 1389 __CPROVER_is_fresh does not conflict with other pointer predicate in assume context: SUCCESS
[__CPROVER_contracts_is_fresh.assertion.5] line 1444 __CPROVER_is_fresh does not conflict with other pointer predicate in assert context: SUCCESS
[__CPROVER_contracts_is_fresh.assertion.6] line 1462 __CPROVER_is_fresh is only called in requires or ensures clauses: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_make_invalid_pointer
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.1] line 1186 dereference failure: pointer NULL in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.2] line 1186 dereference failure: pointer invalid in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.3] line 1186 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.4] line 1186 dereference failure: dead object in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.5] line 1186 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.6] line 1186 dereference failure: invalid integer address in *ptr: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_obj_set_create_indexed_by_object_id
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.1] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.2] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.3] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS

test.c function foo
[foo.no_alloc_dealloc_in_ensures.1] line 10 Check that ensures do not allocate or deallocate memory: SUCCESS
[foo.no_alloc_dealloc_in_requires.1] line 10 Check that requires do not allocate or deallocate memory: SUCCESS
[foo.no_recursive_call.1] line 10 No recursive call to function foo when checking contract foo: SUCCESS
[foo.single_top_level_call.1] line 10 Only a single top-level call to function foo when checking contract foo: SUCCESS
[foo.pointer_dereference.1] line 13 dereference failure: pointer NULL in buf.ptr[(signed long int)(buf.len - (unsigned long int)1)]: SUCCESS
[foo.pointer_dereference.2] line 13 dereference failure: pointer invalid in buf.ptr[(signed long int)(buf.len - (unsigned long int)1)]: SUCCESS
[foo.pointer_dereference.3] line 13 dereference failure: deallocated dynamic object in buf.ptr[(signed long int)(buf.len - (unsigned long int)1)]: SUCCESS
[foo.pointer_dereference.4] line 13 dereference failure: dead object in buf.ptr[(signed long int)(buf.len - (unsigned long int)1)]: SUCCESS
[foo.pointer_dereference.5] line 13 dereference failure: pointer outside object bounds in buf.ptr[(signed long int)(buf.len - (unsigned long int)1)]: SUCCESS
[foo.pointer_dereference.6] line 13 dereference failure: invalid integer address in buf.ptr[(signed long int)(buf.len - (unsigned long int)1)]: SUCCESS

** 0 of 28 failed (1 iterations)
VERIFICATION SUCCESSFUL
$ 

Now we try to factor the structure of Buffer out to its own function:

test.c:

#include <assert.h>
#include <stdbool.h>
#include <stddef.h>

struct Buffer {
    char *ptr;
    size_t len;
};

bool is_buffer(struct Buffer buf) {
    return buf.len == 0 || __CPROVER_is_fresh(buf.ptr, buf.len);
}

bool foo(struct Buffer buf) __CPROVER_requires(is_buffer(buf)) {
    if (buf.len > 0) {
        return buf.ptr[buf.len - 1] == 0;
    }
    return false;
}

int main(void) {
    struct Buffer buf;
    foo(buf);
}

With the above code, that should be the same, we don't get a successful validation:

$ goto-cc test.c -o test.goto 
$ goto-instrument --dfcc main --enforce-contract foo test.goto test.goto
Reading GOTO program from 'test.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Trying to force one backedge per target
Loading CPROVER C library (x86_64)
Adding the cprover_contracts library (x86_64)
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
Instrumenting memory predicate 'is_buffer'
Instrumenting harness function 'main'
Wrapping 'foo' with contract 'foo' in CHECK mode
Instrumenting 'malloc'
Instrumenting 'free'
Specializing cprover_contracts functions for assigns clauses of at most 0 targets
Removing unused functions
generate function bodies: No function name matched regex
Updating init function
Setting entry point to main
Writing GOTO program to 'test.goto'
$ cbmc test.goto 
CBMC version 6.7.1 (n/a) 64-bit x86_64 linux
Reading GOTO program from file test.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker: instance is UNSATISFIABLE

** Results:
<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_car_create
[__CPROVER_contracts_car_create.assertion.1] line 126 ptr NULL or writable up to size: SUCCESS
[__CPROVER_contracts_car_create.assertion.2] line 129 CAR size is less than __CPROVER_max_malloc_size: SUCCESS
[__CPROVER_contracts_car_create.assertion.3] line 133 no offset bits overflow on CAR upper bound computation: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_is_fresh
[__CPROVER_contracts_is_fresh.assertion.1] line 1317 __CPROVER_is_fresh max allocation size exceeded: SUCCESS
[__CPROVER_contracts_is_fresh.assertion.2] line 1331 __CPROVER_is_fresh does not conflict with other pointer predicate in assume context: SUCCESS
[__CPROVER_contracts_is_fresh.assertion.3] line 1374 __CPROVER_is_fresh requires size <= __CPROVER_max_malloc_size: SUCCESS
[__CPROVER_contracts_is_fresh.assertion.4] line 1389 __CPROVER_is_fresh does not conflict with other pointer predicate in assume context: SUCCESS
[__CPROVER_contracts_is_fresh.assertion.5] line 1444 __CPROVER_is_fresh does not conflict with other pointer predicate in assert context: SUCCESS
[__CPROVER_contracts_is_fresh.assertion.6] line 1462 __CPROVER_is_fresh is only called in requires or ensures clauses: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_make_invalid_pointer
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.1] line 1186 dereference failure: pointer NULL in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.2] line 1186 dereference failure: pointer invalid in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.3] line 1186 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.4] line 1186 dereference failure: dead object in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.5] line 1186 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.6] line 1186 dereference failure: invalid integer address in *ptr: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_obj_set_create_indexed_by_object_id
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.1] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.2] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.3] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS

test.c function foo
[foo.no_alloc_dealloc_in_ensures.1] line 14 Check that ensures do not allocate or deallocate memory: SUCCESS
[foo.no_alloc_dealloc_in_requires.1] line 14 Check that requires do not allocate or deallocate memory: SUCCESS
[foo.no_recursive_call.1] line 14 No recursive call to function foo when checking contract foo: SUCCESS
[foo.single_top_level_call.1] line 14 Only a single top-level call to function foo when checking contract foo: SUCCESS
[foo.pointer_dereference.1] line 16 dereference failure: pointer NULL in buf.ptr[(signed long int)(buf.len - (unsigned long int)1)]: FAILURE
[foo.pointer_dereference.2] line 16 dereference failure: pointer invalid in buf.ptr[(signed long int)(buf.len - (unsigned long int)1)]: FAILURE
[foo.pointer_dereference.3] line 16 dereference failure: deallocated dynamic object in buf.ptr[(signed long int)(buf.len - (unsigned long int)1)]: FAILURE
[foo.pointer_dereference.4] line 16 dereference failure: dead object in buf.ptr[(signed long int)(buf.len - (unsigned long int)1)]: FAILURE
[foo.pointer_dereference.5] line 16 dereference failure: pointer outside object bounds in buf.ptr[(signed long int)(buf.len - (unsigned long int)1)]: FAILURE
[foo.pointer_dereference.6] line 16 dereference failure: invalid integer address in buf.ptr[(signed long int)(buf.len - (unsigned long int)1)]: FAILURE

** 6 of 28 failed (5 iterations)
VERIFICATION FAILED
10$ 

The result seems like the function is ignored.

After some time I figured out that it does work if the predicate is made to take a pointer to buf, even with the same conditions and no additional checks due to the pointer.

The following works:

#include <assert.h>
#include <stdbool.h>
#include <stddef.h>

struct Buffer {
    char *ptr;
    size_t len;
};

bool is_buffer(struct Buffer *buf) {
    return buf->len == 0 || __CPROVER_is_fresh(buf->ptr, buf->len);
}

bool foo(struct Buffer buf) __CPROVER_requires(is_buffer(&buf)) {
    if (buf.len > 0) {
        return buf.ptr[buf.len - 1] == 0;
    }
    return false;
}

int main(void) {
    struct Buffer buf;
    foo(buf);
}

Which is odd since de-referencing the argument shouldn't change anything?

If this isn't a bug, would be good to update the documentation for this.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions