weird behaviour of assume with function arguments ?

[Ramon Bejar Torres]

Hi All,

I have found while working with some stundents a weird behavior with assume. Consider this file  (asc2.c):

#define N 20

int ascending(   int a[N] ) {

  int d, k;

  // int a[N];  (if a[N] is a local variable, then the example works OK)

  

   __CPROVER_assume( (a[0] == 0)  ); 

   d = a[0];

   k= 2;

   k = 3;

   d = a[0];

    __CPROVER_assert( d == 0 , "a[0] is 0" );

  

 }

when verified with cbmc 5-11 over Ubuntu , with flags:

   cbmc --trace --function ascending asc2.c

I get this counterexample (from line 8):

State 28 file asc2.c function ascending line 8 thread 0

----------------------------------------------------

  d=0 (00000000 00000000 00000000 00000000)

State 29 file asc2.c function ascending line 9 thread 0

----------------------------------------------------

  k=2 (00000000 00000000 00000000 00000010)

State 30 file asc2.c function ascending line 10 thread 0

----------------------------------------------------

  k=3 (00000000 00000000 00000000 00000011)

State 31 file asc2.c function ascending line 11 thread 0

----------------------------------------------------

  d=1 (00000000 00000000 00000000 00000001)

Violated property:

  file asc2.c function ascending line 12 thread 0

  a[0] is 0

  d == 0

So, it seems that a[0] changed from 0 to 1 (but the program did not change a[1]).

But if the array a[N] is created as a local variable, and not a parameter of the function, then the property checks OK.

Is this beacuse are we assuming that other "thread" can be modifying the array a[] ?  But If do not have any other threads in this simple program.

Regards,

Ramon Béjar

University of Lleida

 

[Ramon Bejar Torres]

Sorry, where I say:

  ->  So, it seems that a[0] changed from 0 to 1 (but the program did not change a[1])

I wanted to say:

So, it seems that a[0] changed from 0 to 1 (but the program did not change a[0])

[Martin Nyx Brain]

On Wed, 2021-05-26 at 08:23 -0700, Ramon Bejar Torres wrote:
> Hi All,
> I have found while working with some stundents a weird behavior with
> assume. Consider this file (asc2.c):
>
> #define N 20
>
> int ascending( int a[N] ) {
> int d, k;
> // int a[N]; (if a[N] is a local variable, then the example works
> OK)
>
> __CPROVER_assume( (a[0] == 0) );
> d = a[0];
> k= 2;
> k = 3;
> d = a[0];
> __CPROVER_assert( d == 0 , "a[0] is 0" );
>
> }

<snip>

> So, it seems that a[0] changed from 0 to 1 (but the program did not
> change
> a[1]).
> But if the array a[N] is created as a local variable, and not a
> parameter
> of the function, then the property checks OK.
> Is this beacuse are we assuming that other "thread" can be modifying
> the
> array a[] ? But If do not have any other threads in this simple
> program.

This is not intended behaviour; it shouldn't change. There are a
number of things that might cause this:

1. Generally, I would recommend using a newer CBMC version

https://github.com/diffblue/cbmc/releases

a lot has changed since 5.11.


2. Arrays as arguments, particularly to the main function lands you in
the world of "it's not 100% clear what the correct behaviour should
be". If CBMC is called with --function f00 where f00 takes a pointer
it is hard to work out what it should point to, should it be a valid
region, if so, how large, etc. It is better to structure the code as:

#define N 20

int ascending(int *array) {
// ...
}

int main (int argc, char **argv) {
// Build the environment here
int array[N];

ascending(array);

return 0;
}


3. There is a bug in the native back-end which affects equality between
arrays of non-constant size. It is only triggered in unusual use cases
and I haven't found an easy test case. It is possible that your code
is one. One check is whether this fails when run with an SMT solver.

HTH

Cheers,
- Martin