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] About the memory separation and the usage of '\separated'

  • Subject: [Frama-c-discuss] About the memory separation and the usage of '\separated'
  • From: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Mon, 6 Mar 2017 12:07:36 +0100
  • In-reply-to: <CAGvSYBHNL-PvPH98RqC7NDmbvUd+AUkCjHvcyt=BhwSHhuTMLg@mail.gmail.com>
  • References: <CAGvSYBHNL-PvPH98RqC7NDmbvUd+AUkCjHvcyt=BhwSHhuTMLg@mail.gmail.com>
Hi Wenhao,

Actually, the WP-plugin is not already implementing the ACSL annotations describing allocation.
However, in the internal memory model of WP, addresses are partitioned into regions, described by
an internal `region(integer) : integer` logic function. Regions 0,1,2 and <0 are reserved for WP for formals, locals, etc.
You can use and region >= 3 for malloc.

Hence, using an axiomatic, you can specify in regular ACSL the behaviour of allocation, by axiomatising a logical function returning pointers, such that
the ‘k'-th returned pointer belongs to region 3+k (starting at 0).

We can introduce the ‘k’-th call to malloc with and the internal WP region with ACSL declarations and a ghost integer :

//@ ghost int ALLOC = 3 ;
logic integer WPREGION(int *addr) reads addr ;
logic int* WPALLOC(integer k) reads k;

To connect the WPREGION to the internal ‘region’ function of WP we use a driver and an additional alt-ergo definition :

$ cat alloc.driver
library Malloc: memory
altergo.file += "alloc.mlw" ;
logic integer WPREGION( addr ) = "region_base » ;
$ cat alloc.mlw
function region_base ( a : addr ) : int = region( a.base )

To help specifying, we introduce the following ACSL predicates:

  // Necessary pre-condition for any allocating function.
  predicate Allocating{L} = 3 <= \at( ALLOC , L ) ;

  // The k-th allocated address since FROM.
  logic int *Alloc{FROM}(integer k) = WPALLOC(\at(ALLOC+k,FROM));

  // Designate the k-th allocated address since FROM.
  predicate Allocated{FROM}(int *addr,integer k) =
     (WPREGION(addr) == \at(ALLOC+k,FROM)) &&
     (addr == WPALLOC(\at(ALLOC+k,FROM))) ;

  // Number of allocated pointers between PRE and POST.
  predicate Allocates{PRE,POST}(integer n) =
        \at( ALLOC , POST ) ==
        \at( ALLOC , PRE ) + n ;

Typically, your allocating function `arr_init` shall be specified as follows:
(modifications of your code in blue)

/*@ requires 0 < len;
  @ requires Allocating ;
  @ ensures \valid(\result+(0 .. len-1));
  @ ensures \forall integer j;
  @   (0 <= j < len ==> \result[j] == 0);
  @ ensures Allocates{Pre,Post}(1);
  @ ensures Allocated{Pre}(\result,1);
  @ assigns ALLOC ;
 */
int* arr_init(int len); //{ return (int*)calloc(len, sizeof(int)); }


Then, the copy-function can be specified as follows:

/*@ requires Allocating ;
  @ requires 0 < len;
  @ requires \valid(in_arr+(0 .. len-1));
  @ ensures \valid(\result+(0 .. len-1));
  @ ensures \forall integer j;
  @   (0 <= j < len ==> \result[j] == in_arr[j]);
  @ ensures Allocates{Pre,Post}(1);
  @ ensures Allocated{Pre}(\result,1);
  @ assigns Alloc{Pre}(1)[0..len-1];
  @ assigns ALLOC ;
 */
int* arr_copy1(int len, int* in_arr){
  ...
}

Then :

$ frama-c -wp alloc.c -wp-driver alloc.driver
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing alloc.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 22 goals scheduled
[wp] Proved goals:   22 / 22
     Qed:            15  (0.58ms-4ms-13ms)
     Alt-Ergo:        7  (14ms-58ms-243ms) (366)

All files in attachment.
Remark : in the experiment above, we keep your original separtion-assertion, which turned to be proved thanks to regions.
However, such an assertion is no more necessary to prove the specifications, and you can remove it from your code.






> Le 3 mars 2017 à 21:59, Wenhao Wu <wuwenhao at udel.edu> a écrit :
> 
> Hi all,
> 
> I am Wenhao Wu, a grad-student of the University of Delaware.
> Currently, I encounter a problem related with the notion '\separated'.
> 
> I am trying to verify a function that copies the data from a given input array 
> with a given length into a local pointer and then returns the pointer.
> 
> Here is the command of using frama-c
> 
> frama-c -wp -wp-model Typed+var+nat+real -wp-prover why3ide arr_copy.c
> 
> Here is the whole program:
> 
> /*@ requires 0 < len;
>   @ ensures \valid(\result+(0 .. len-1));
>   @ ensures \forall integer j;
>   @   (0 <= j < len ==> \result[j] == 0);
>  */
> int* arr_init(int len); //{ return (int*)calloc(len, sizeof(int)); }
> 
> /*@ requires 0 < len;
>   @ requires \valid(in_arr+(0 .. len-1));
>   @ ensures \valid(\result+(0 .. len-1));
>   @ ensures \forall integer j;
>   @   (0 <= j < len ==> \result[j] == in_arr[j]);
>  */
> int* arr_copy1(int len, int* in_arr){
>     int i = 0;
>     int * out_arr = arr_init(len);
>     //@ assert \separated(in_arr+(0 .. len-1), out_arr+(0 .. len-1));
>     
>     /*@ loop invariant 0 <= i <= len;
>       @ loop invariant \forall integer j;
>       @      ((0 <= j < i) ==> out_arr[j] == in_arr[j]);
>       @ loop assigns out_arr[0 .. len-1], i;
>       @ loop variant (len-i);
>      */
>     while(i < len){
>         out_arr[i] = in_arr[i];
>         i = i + 1;
>     }
>     return out_arr;
> }
> 
> The verification of the loop invariant (marked by blue color) depends on 
> that the assertion (marked by red color). 
> 
> If the local pointer 'out_arr' is assigned by the result returned by 
> the function 'init(int len)', which uses calloc(size_t num, size_t type) function, 
> then the assertion is expected to be true.
> 
> Thus, I wonder whether there is a way to assume a condition of
> ' \separated(in_arr+(0 .. len-1), out_arr+(0 .. len-1)) ' to be true,
> or to specify a pre-condition like 
> ' \separated(in_arr+(0 .. len-1), \result+(0 .. len-1)) '.
> 
> May I ask for some suggestions that help me to 
> verify the function " int* arr_copy1(int len, int* in_arr) "?
> Or is there any way to assume/define the memory space 
> allocated (by malloc or calloc) is separated from other 
> used memory space?
> 
> And another version of the function copying an array is proved.
> The function and its contract is shown here:
> 
> /*@ requires 0 < len;
>   @ requires \valid(in_arr+(0 .. len-1)) &&
>   @          \valid(out_arr+(0 .. len-1));
>   @ requires \separated(in_arr+(0 .. len-1), out_arr+(0 .. len-1));
>   @ ensures \valid(out_arr+(0 .. len-1));
>   @ ensures \forall integer j;
>   @   (0 <= j < len ==> in_arr[j] == out_arr[j]);
>   @ assigns out_arr[0 .. len-1];
>  */
> void array_copy2(int len, int * in_arr, int * out_arr){
>     int i = 0;
>     
>     /*@ loop invariant 0 <= i <= len;
>       @ loop invariant \forall integer j;
>       @      ((0 <= j < i) ==> out_arr[j] == in_arr[j]);
>       @ loop assigns out_arr[0 .. len-1], i;
>       @ loop variant (len-i);
>      */
>     while(i < len){
>         out_arr[i] = in_arr[i];
>         i = i + 1;
>     }
> }
> 
> All scheduled goals can be proved by Alt-Ergo (1.30)
> 
> Sincerely,
> Wenhao Wu
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0004.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: alloc.mlw
Type: application/octet-stream
Size: 59 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0003.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0005.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: alloc.driver
Type: application/octet-stream
Size: 102 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0004.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0006.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: alloc.c
Type: application/octet-stream
Size: 1910 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0005.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0007.html>