--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on March 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] About the memory separation and the usage of '\separated'



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>