Adding CPROVER_assigns statement changes result

[polgreen]

CBMC version: 5.90.0 (cbmc-5.90.0-21-g6590981c4a
Operating system: MacOS 14.6.1
Exact command line resulting in the issue:
This is the file used:

#include <stdio.h>
#include <stdlib.h>

int main()
{
    int rows=3;
    int cols = 3;
    int* arr = malloc(rows * cols * sizeof(int));
    int *idx = &arr[0];

    for(int i=0; i<rows; i++)
    // __CPROVER_assigns(i,idx, *idx) //uncomment this line to make *idx unassignable
    __CPROVER_loop_invariant(0 <= i && i <= rows)
    __CPROVER_loop_invariant(idx == &arr[0]+i*rows)
    __CPROVER_loop_invariant(rows==3 && cols==3)
    {
        *idx=i; 
        idx+=cols;
    }
    return 1;
}

These are the commands run

goto-cc tmp.c
goto-instrument --apply-loop-contracts  a.out prcp.o
cbmc  prcp.o 

What behaviour did you expect:

I expect i, idx and *idx to be assignable (which they are, according to the results obtained using the inferred loop assigns statement). I also would not expect adding an explicit __CPROVER_assigns statement, which includes the same set of variables, to change the result.

What happened instead:
If you run the commands on the file above, 15 properties pass, including two that say:

[main.assigns.3] line 21 Check that *idx is assignable: SUCCESS
[main.assigns.6] line 21 Check that *idx is assignable: SUCCESS

If you add the __CPROVER_assigns statement, one of the check *idx is assignable properties fails:

[main.assigns.4] line 21 Check that *idx is assignable: SUCCESS
[main.assigns.7] line 21 Check that *idx is assignable: FAILURE

[remi-delmas-3000]

Hi,

The set of locations declared in the assigns clause is resolved once and for all upon loop entry, so when you write
__CPROVER_assigns(i, idx, *idx), *idx resolves to just &a[0]. Since idx itself is modified by the loop, CBMC finds a case where idx points to some other location than &a[0] and the check fails.

Since the loop assigns several cells within the array, an assigns clause that would work for this loop is rather:

__CPROVER_assigns(i, idx, __CPROVER_object_whole(idx))

This is what is inferred automatically by goto-instrument when you don't specify an assigns clause explicitly as shown in the tool output:

No assigns clause provided for loop main.0 at file ex.c line 11 function main. The inferred set {side_effect statement="function_call"(__CPROVER_object_whole, arguments(address_of(*main::1::idx))), main::1::idx, main::1::1::i} might be incomplete or imprecise, please provide an assigns clause if the analysis fails.

However, __CPROVER_object_whole(idx) may contain more than what the loop strictly assigns (if the loop uses some stride to skip over some cells) so the loop invariant may have to be strengthened to say that some cells retain their value.

Does this help ?

[polgreen]

OK, great, thanks.

Another related question: is there a way to tell cbmc that functions used in loop invariants are side-effect free? The option to disable this check seems to have been disabled in develop.

goto-cc says that this loop invariant is not side-effect free, which isn't right?

int foo()
{
    return 1;
}

int main()
{
  
    for(int i=0; i<3; i++)
    __CPROVER_loop_invariant(foo() == 1) // invariant is always true
    {
   // do some stuff
    }
    return 1;
}

[remi-delmas-3000]

Hi, I'd encourage you to use the latest version of cbmc/goto-instrument, where you can disable this check using --disable-loop-contracts-side-effect-check. Alternatively, use macros to factor out function-like parts in loop contracts.

Now for some background explanation:

• CBMC makes the distinction based on syntactic category alone, not on the actual semantics of the construct. You have the category of pure expressions and the category of potentially side effecting expressions or statements. A C function call is in the syntactic category "statement or expression with potential side effects". Checking that foo does not actually have side effects requires to look at the semantics of the instructions defining the function, which we do not yet do during instrumentation.
• If you use function contracts, C function calls are allowed in pre and post conditions, and we semantically check that they are side effect-free. We should extend that approach to loop contracts.