The function contract doesn't work when using loop

[wcventure]

Hi there,

I followed the cprover-manual/contracts-functions.md and tried to use function contracts in my project. However, the function contracts don't seem to work correctly in some situations. Could you help me look at the following issue?

The foo function contract doesn't work when using it in the loop body

I have written a function foo that Iteratively checks whether the two arrays have the same elements. If yes, it returns 0, otherwise, it returns -1. And I try to use its function contract in the main function. Unfortunately, I got an unexpected result that all wrong assertions are Judged as SUCCESS (When this function contract is not placed in the loop, the result is correct. But when it is put into a meaningless loop, the result is not correct).

//main.c
#include <stdlib.h>
#include <string.h>
#include <stdint.h>
#include <assert.h>

#define SIZE 10

int foo(uint32_t *map, uint32_t *key, uint32_t len)
/* Precondition */
__CPROVER_requires(len <= SIZE)
__CPROVER_requires(__CPROVER_is_fresh(map, sizeof(uint32_t)*len))
__CPROVER_requires(__CPROVER_is_fresh(key, sizeof(uint32_t)*len))
/* Postconditions */
__CPROVER_ensures(__CPROVER_return_value == 0 || __CPROVER_return_value == -1)
__CPROVER_ensures(__CPROVER_return_value == -1 ==> __CPROVER_forall {int i; (0 <= i && i < len) ==> map[i] != key[i]})
__CPROVER_ensures(__CPROVER_return_value == 0 ==> __CPROVER_exists {int i; (0 <= i && i < len) && map[i] == key[i]})
{
	int ret = -1;
	for (int i = 0; i < len; i++)
	__CPROVER_assigns(i)
	__CPROVER_loop_invariant(0 <= i && i <= len)
	__CPROVER_loop_invariant(ret == -1 || ret == 0)
	__CPROVER_loop_invariant((ret == -1)==> __CPROVER_forall {int j; (0 <= j && j < len) ==> ( j < i ==> map[j] != key[j])})
	__CPROVER_loop_invariant((ret == 0) ==> map[i] == key[i])
	__CPROVER_decreases(len - i)
	{
		if (map[i] == key[i])
		{
			ret = 0;
			break;
		}
	}
	return ret;
}

int main()
{
    uint32_t *map = malloc(sizeof(uint32_t)*SIZE);
    uint32_t *key = malloc(sizeof(uint32_t)*SIZE);
    memset(map, 0, sizeof(uint32_t)*SIZE);
    memset(key, 0, sizeof(uint32_t)*SIZE);
    key[0] = 1;
    map[0] = 2;

    int ret;
    for (int i = 1; i < SIZE; i++) {
        ret = foo(map, key, i);
    }
    assert(ret == 0);
    assert(ret == -1);
    assert(0);
}

You can use the following command to see the ensures clause failure.

goto-cc -o main.goto main.c
goto-instrument --replace-call-with-contract foo main.goto main-using-foo-contract.goto
cbmc main-using-foo-contract.goto

Then you will see all assertion success unexpectedly. The assert(0) doesn't fail which also means that the function exit is not reachable. However, if you change the loop body for (int i = 1; i < SIZE; i++) { ret = foo(map, key, i); } to ret = foo(map, key, SIZE);, the result become correct.

** Results:
[precondition.1] Check requires clause: FAILURE
/mnt/e/Github-Bitbucket/CBMC_Frama-C_By_examples/CBMCExamples/foo_and_sum_contract/loop_contract.c function main
[main.precondition_instance.1] line 41 memset destination region writeable: SUCCESS
[main.precondition_instance.2] line 42 memset destination region writeable: SUCCESS
[main.assertion.1] line 50 assertion ret == 0: SUCCESS
[main.assertion.2] line 51 assertion ret == -1: SUCCESS
[main.assertion.3] line 52 assertion 0: SUCCESS

<builtin-library-malloc> function malloc
[malloc.assertion.1] line 26 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 31 max allocation may fail: SUCCESS

** 1 of 8 failed (2 iterations)
VERIFICATION FAILED

[martin-cs]

Thank you for the extensive examples and work-through. This really helps.

@jimgrundy / @SaswatPadhi / @remi-delmas-3000 / @feliperodri is this something your team could look? I am pretty sure these issues would affect you too.

[jimgrundy]

Yes, one of us will try to reproduce.

[tautschnig]

It seems not quite all assertions succeed -- quoting from the output (which I was able to reproduce):

[precondition.1] Check requires clause: FAILURE

Given this failing precondition, no further steps will be considered. I believe the root cause of your problem is that __CPROVER_is_fresh will not hold once you go around the loop at least two times (it can only be fresh once).

Edit: the semantics we documented for __CPROVER_is_fresh state: "When using a contract as an abstraction in place of a call to the function a __CPROVER_is_fresh in a requires clause will check that the argument supplied is fresh," which you are not fulfilling as stated above.

[martin-cs]

@jimgrundy Thank you!

[jimgrundy]

Hi @wcventure, thanks for trying this out. The function and loop contracts features are very much under development, so I'm not surprised that you are finding issues, but I am grateful to hear about them and we will try to address.

Here are my thoughts so far:

Let's not use __CPROVER_is_fresh in your pre-condition for now. You shouldn't need to because you are allocating what you need via malloc in the proof harness. The idea eventually is that you won't need a proof harness at all because simply assuming that a pointer is fresh will cause it to exist. This is proving complex in general so for now my advice is to keep using a proof harness to do the memory allocation and then don't use __CPROVER_is_fresh in your contract.

Can you try this out and report back (I'll try to find time myself later).

[wcventure]

Given this failing precondition, no further steps will be considered. I believe the root cause of your problem is that __CPROVER_is_fresh will not hold once you go around the loop at least two times (it can only be fresh once).

We can delete the precondition of foo, the assert(0) still could be successful.

Let's not use __CPROVER_is_fresh in your pre-condition for now.

Hi @jimgrundy, I have tried to delete the precondition of foo, but the result is still not correct. However, removing the loop body in main and calling foo contract by ret = foo(map, key, SIZE); can get the correct result.

[tautschnig]

It seems that having the three preconditions

__CPROVER_ensures(__CPROVER_return_value == 0 || __CPROVER_return_value == -1)
__CPROVER_ensures(__CPROVER_return_value == -1 ==> __CPROVER_forall {int i; (0 <= i && i < len) ==> map[i] != key[i]})
__CPROVER_ensures(__CPROVER_return_value == 0 ==> __CPROVER_exists {int i; (0 <= i && i < len) && map[i] == key[i]})

together is causing the trouble. Removing anyone of them will make the assertions fail as expected.

[tautschnig]

I have done some further experiments, with the following now being the result of replacing the loop by:

    ret = foo(map, key, 1); // 1 is important here, using a higher value like 3 will make things work
    ret = foo(map, key, 2);

This yields, among other things, the following goto program instructions:

        DECL main::1::ret : signedbv[32]
        // 15 file 6483.c line 11
        ASSERT cast(1, unsignedbv[32]) ≤ cast(10, unsignedbv[32]) // Check requires clause
        // 16 no location
        ASSUME (main::1::ret = 0 ∨ main::1::ret = -1) ∧ ((main::1::ret = -1) ⇒ ∀ ::tmp_cc::tmp_cc : signedbv[32] . (0 ≤ ::tmp_cc::tmp_cc ∧ cast(::tmp_cc::tmp_cc, unsignedbv[32]) < cast(1, unsignedbv[32])) ⇒ (*(main::1::map + cast(::tmp_cc::tmp_cc, signedbv[64])) ≠ *(main::1::key + cast(::tmp_cc::tmp_cc, signedbv[64])))) ∧ ((main::1::ret = 0) ⇒ ∃ ::tmp_cc::tmp_cc$0 : signedbv[32] . (0 ≤ ::tmp_cc::tmp_cc$0 ∧ cast(::tmp_cc::tmp_cc$0, unsignedbv[32]) < cast(1, unsignedbv[32])) ∧ *(main::1::map + cast(::tmp_cc::tmp_cc$0, signedbv[64])) = *(main::1::key + cast(::tmp_cc::tmp_cc$0, signedbv[64])))
        // 17 file 6483.c line 11
        ASSERT cast(2, unsignedbv[32]) ≤ cast(10, unsignedbv[32]) // Check requires clause
        // 18 no location
        ASSUME (main::1::ret = 0 ∨ main::1::ret = -1) ∧ ((main::1::ret = -1) ⇒ ∀ ::tmp_cc::tmp_cc$1 : signedbv[32] . (0 ≤ ::tmp_cc::tmp_cc$1 ∧ cast(::tmp_cc::tmp_cc$1, unsignedbv[32]) < cast(2, unsignedbv[32])) ⇒ (*(main::1::map + cast(::tmp_cc::tmp_cc$1, signedbv[64])) ≠ *(main::1::key + cast(::tmp_cc::tmp_cc$1, signedbv[64])))) ∧ ((main::1::ret = 0) ⇒ ∃ ::tmp_cc::tmp_cc$2 : signedbv[32] . (0 ≤ ::tmp_cc::tmp_cc$2 ∧ cast(::tmp_cc::tmp_cc$2, unsignedbv[32]) < cast(2, unsignedbv[32])) ∧ *(main::1::map + cast(::tmp_cc::tmp_cc$2, signedbv[64])) = *(main::1::key + cast(::tmp_cc::tmp_cc$2, signedbv[64])))
        // 19 file 6483.c line 61 function main
        ASSERT main::1::ret = 0 // assertion ret == 0

Note that main::1::ret is not updated between the (replaced) calls.

[jimgrundy]

Thanks @wcventure for reporting this. This is a bug. We are missing a nondeterministic assignment to the return value when we replace the contract, which can result an accumulation of assumptions about the return value between two calls. We should be able to fix this soon.