--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on May 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



Thanks, Loïc —— good to know about these tricks, and I look forward to the new and more robust memory model.
By the way, I did get this specific example to work by changing the way I specified the separation; see below.
-Steve


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

/*@
  predicate Sep2d(int **a, int n, int m) =
  \forall integer i1, i2, j1, j2; 
    0<=i1<n && 0<=i2<n && 0<=j1<m && 0<=j2<m && (i1!=i2 || j1!=j2) ==>
      \separated(a[i1]+j1, a[i2]+j2);

  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 Sep2d(a, n, m);
  @ requires \forall integer i1, i2, j1, j2; 0<=i1<n && 0<=i2<n && 0<=j1<m && 0<=j2<m ==>
  @   \separated(a[i1]+j1, b[i2]+j2, &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++) {
      a[i][j] = b[i][j];
    }
  }
}


frama-c -wp -wp-rte copy2d.c
[kernel] Parsing copy2d.c (with preprocessing)
copy2d.c:30:[wp] warning: Ignored 'terminates' specification:
     \false
[rte] annotating function copy2d
[wp] 28 goals scheduled
[wp] Proved goals:   28 / 28
    Qed:            10  (0.99ms-35ms)
    Alt-Ergo:       18  (13ms-33ms-100ms) (254)




> On May 16, 2018, at 7:28 AM, Loïc Correnson <loic.correnson at cea.fr> wrote:
> 
> 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
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss