Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] 2d array and \separated with WP

Hi Stephen,

The \separated predicate is supposed to be correctly interpreted by Frama-C.
However, there can be some bugs with complex ranges like in your example, we will check that.

However, relying on \separated to describe memory is generally a bad idea.
Few reasons for that:
 - the semantics of n-ary \separated must be decomposed into n(n-2)/2 atomic separation of 2 sets
 - then, the semantics of separation between two sets (except 1-dimension ranges) must be decomposed into universally quantified proposition
 - finally, the semantics of separation between two address ranges, including single scalars, must be decomposed by SAT-solvers into a disjunction of at least 3 cases
(different bases, same base with left-to-right offset ordering, and same base with right-to-left offset ordering).

All these decomposition into sub-cases make the search state very large for SMT-solvers, and they usually fail to prove separation or use it for reasoning
on read-after-write into memory.

**Remark** we are working on new memory models where disjoint memory regions can be declared as pre-conditions, and verified at call site in a much more
expressive and efficient ways. But this will not be released soon.

So, in the meanwhile, you must find tricks in order ease reasoning on separation between pointers.

Typical solutions include locally alias pointer parameters to ghost variable and arrays.
Of course, those techniques requires to prove the function contract in a local context that is not general, but shall be representative for all the call-sites.
This means that you don’t use exactly the same contract when proving the function, and when calling the function, but this is consistent with the modular
approach promoted by WP.

In your case, your separation clauses are faithfully represented by the following special context :

#define N 1000
#define M 1000
ghost int D[N][M] ;
ghost int *A[N] ;

/*@
  requires a == A ;
  requires n <= N && m <= M ;
  requires \forall integer i ; a[i] == D[i] ;
*/

At the call-sites of your function, of course, you will not be able to prove such requires, but may check (by any method of your choice)
that each call-site fits into this general case.

After all, this what everyone do in math when proving \forall x, P(x) : you first introduce a fresh element e (in our case, the ghost variables),
then you prove P(e) (in our case, you prove the contract on ghost variables), finally you generalize to any e (in our case, you drop the aliasing requires).

	L.

> Le 16 mai 2018 à 11:07, Stephen Siegel <siegel at udel.edu> a écrit :
> 
> Hello Frama-C list,
> I’m trying to prove (using WP) some simple programs dealing with 2-dimensional arrays, represented as arrays of pointers.   I’m running into trouble reasoning about separation.  Can anyone tell me if the following lemma is valid?   It may be that I am misunderstanding the meaning of \separated.  In any case, I haven’t been able to prove this lemma…
> 
> /*@
>  predicate Sep2d(int **a, int n, int m) =
>    \separated(a[0..n-1]+(0..m-1));
> 
>  predicate SepRows(int **a, int n, int m) =
>    \forall integer i1, i2, j1, j2;
>      (0<=i1<n && 0<=i2<n && i1!=i2 && 0<=j1<m && 0<=j2<m) ==>
>        \separated(&a[i1][j1], &a[i2][j2]);
> 
>  lemma SepLem1: \forall int **a, int n, int m;
>    (n>=0 && m>=0 && Sep2d(a, n, m)) ==> SepRows(a, n, m);
> 
> */
> 
> One thing I noticed, using the Frama-C GUI and Why3 as prover, is that my Sep2d predicate seems to have been translated to “true”. 
> 
> Below is the actual function I am trying to prove, which copies a 2d array:
> 
> /*@
>  predicate EqualRange(int *a, integer n, int *b) =
>  \forall integer i; 0<=i<n ==> a[i] == b[i];
> 
>  predicate EqualRange2d(int **a, integer n, integer m, int **b) =
>  \forall integer i; 0<=i<n ==> EqualRange(a[i], m, b[i]);
> 
>  predicate Valid2d(int **a, integer n, integer m) =
>  \valid(a + (0..n-1)) && \valid(a[0..n-1] + (0..m-1));
> */
> 
> /*@ requires n>=0 && m>=0;
>  @ requires Valid2d(a, n, m);
>  @ requires Valid2d(b, n, m);
>  @ requires \separated(a + (0..n-1), a[0..n-1] + (0..m-1), b + (0..n-1), b[0..n-1] + (0..m-1), &n, &m);
>  @ assigns a[0..n-1][0..m-1];
>  @ ensures EqualRange2d(a, n, m, b);
>  @*/
> void copy2d(int **a, int n, int m, int **b) {
>  /*@ loop invariant i1: 0<=i<=n;
>    @ loop invariant i2: EqualRange2d(a, i, m, b);
>    @ loop assigns i, a[0..n-1][0..m-1];
>    @ loop variant n - i;
>    @*/
>  for (int i=0; i<n; i++) {
>    /*@ loop invariant 0<=j<=m;
>      @ loop invariant z1: EqualRange2d(a, i, m, b);
>      @ loop invariant z2: EqualRange(a[i], j, b[i]);
>      @ loop assigns j, a[i][0..m-1];
>      @ loop variant m - j;
>      @*/
>    for (int j=0; j<m; j++) {
>      // I can’t prove the following assertion …
>      //@ assert sep1 : \separated(&a[i][j], a[0..i-1] + (0..m-1));
>      a[i][j] = b[i][j];
>    }
>  }
> }
> 
> -Steve
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss