--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on May 2018 ---
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