--- layout: fc_discuss_archives title: Message 3 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'



Thanks a lot for your helpful information about memory region!

I have practiced this method on several simple examples today.
And I encounter a problem when applying it on a user-defined struct type.

Here is the full content of my program.

//@ ghost int ALLOC = 3 ;
> struct Arr_struct{
>     int len;      // Array length
>     int *data;  // Array data
> };
> typedef struct Arr_struct Arr;
> /*@
>   axiomatic Malloc {


>   // WP Internals *(Should I set a pair of logic things for each type?)*
>
> *logic integer WPREGION_ARR(Arr *addr) reads addr ;**  logic Arr*
> WPALLOC_ARR(integer k) reads k;*
>   logic integer WPREGION_INT(int *addr) reads addr ;
>   logic int* WPALLOC_INT(integer k) reads k;


>   // Necessary precondition for any allocating function

  predicate Allocating{L} = 3 <= \at( ALLOC , L ) ;


>   // The k-th allocated address since FROM.
>   *logic Arr *Alloc_ARR{FROM}(integer k) =  *

*     WPALLOC_ARR(\at(ALLOC+k,FROM));*
>   logic int *Alloc_INT{FROM}(integer k) = WPALLOC_INT(\at(ALLOC+k,FROM));


>   // Designate the k-th allocated address since FROM.
>
>
> *predicate Allocated_ARR{FROM}(Arr *addr,integer k) =
> (WPREGION_ARR(addr) == \at(ALLOC+k,FROM)) &&**    (addr ==
> WPALLOC_ARR(\at(ALLOC+k,FROM))) ;*
>   predicate Allocated_INT{FROM}(int *addr,integer k) =
>     (WPREGION_INT(addr) == \at(ALLOC+k,FROM)) &&
>     (addr == WPALLOC_INT(\at(ALLOC+k,FROM))) ;
>
>   // Number of allocated between PRE and POST.
>   predicate Allocates{PRE,POST}(integer n) =
>         \at( ALLOC , POST ) ==
>         \at( ALLOC , PRE ) + n ;
>   }
> */
> /*@ requires 0 < len;
>   @ requires Allocating ;
>   @
>   @ ensures \valid(\result);
>   @ ensures 0 < \result->len;
>   @ ensures \result->len == len;
>   @ ensures \valid(\result->data +(0 .. len-1));
>   @ ensures \forall integer j;
>   @   (0 <= j < \result->len ==> \result->data[j] == 0);
>   @ *// Are the following usages of the **axiomatic contract correct?*
>
> *@ ensures Allocates{Pre,Post}(2) ;*
> *  @ ensures Allocated_ARR{Pre}(\result,1);**  @ ensures
> Allocated_INT{Pre}(\result->data,2);*
>   @ assigns ALLOC ;
>  */
> Arr * arr_init(int len);
> /*{
>     Arr * result = (Arr*)malloc(sizeof(Arr));
>     result->data = (int*)calloc(len, sizeof(int));
>     return result;
>  } // This is the implementation.

 */


> /*@ requires Allocating ;
>   @
>   @ requires \valid(in_arr);
>   @ requires 0 < in_arr->len;
>   @ requires \valid(in_arr->data +(0 .. in_arr->len-1));
>   @
>   @ ensures \valid(\result);
>   @ ensures 0 < \result->len;
>   @ ensures \result->len == in_arr->len;
>   @ ensures \valid(\result->data +(0 .. \result->len-1));
>   @ ensures \forall integer j;
>   @   (0 <= j < \result->len ==> \result->data[j] == in_arr->data[j]);
>   @ *// Are the following usages of the axiomatic contract correct?*
>
> *@ ensures Allocates{Pre,Post}(2) ;*
>
>
>
> *  @ ensures Allocated_ARR{Pre}(\result,1);  @ ensures
> Allocated_INT{Pre}(\result->data,2);  @ assigns Alloc_ARR{Pre}(1)->data[0
> .. \result->len-1];  @ assigns Alloc_INT{Pre}(2)[0 .. \result->len-1];**
> @ assigns ALLOC ;*
>  */
> Arr* arr_copy(Arr* in_arr){
>     int i = 0;
>     int len = in_arr->len;
>     Arr * out_arr = arr_init(len);

    // The following assertions can *NOT* be proved with my contract.
>     //@ assert \separated(in_arr, out_arr);
>     //@ assert \separated(in_arr->data +(0 .. len-1), out_arr->data +(0
> .. len-1));


>     /*@ loop invariant 0 <= i <= len;
>       @ loop invariant \forall integer j;
>       @      ((0 <= j < i) ==> out_arr->data[j] == in_arr->data[j]);
>       @ loop assigns out_arr->data[0 .. len-1], i;
>       @ loop variant (len-i);
>      */
>     while(i < len){
>         out_arr->data[i] = in_arr->data[i];
>         i = i + 1;
>     }
>     return out_arr;
> }


My questions are marked by *red*.
And the involved contract are marked by *dark-green*.

More specifically, I would like to ask for an example of applying the
region
method on *a user-defined struct, which has at least one pointer type
field,*
so that its initialization function would require *more than one
malloc/calloc *
*functions* returning pointers *in different type*.


For the program above, the current output by executing the command:

*frama-c -wp alloc2.c -wp-driver alloc.driver*


, the version of my frama-c is: Silicon-20161101
and the result is:

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no
> preprocessing)
> [kernel] Parsing alloc2.c (with preprocessing)
> [wp] warning: Missing RTE guards
> [wp] 29 goals scheduled
> [wp] [Alt-Ergo] Goal typed_alloc_arr_copy_post_4 : Unknown (Qed:1ms)
> (541ms)
> [wp] [Alt-Ergo] Goal typed_alloc_arr_copy_post_3 : Unknown (Qed:1ms)
> (539ms)
> [wp] [Alt-Ergo] Goal typed_alloc_arr_copy_post_2 : Unknown (Qed:2ms)
> (539ms)
> [wp] [Alt-Ergo] Goal typed_alloc_arr_copy_assert_2 : Unknown (Qed:0.96ms)
> (114ms)
> [wp] [Alt-Ergo] Goal typed_alloc_arr_copy_assert : Unknown (Qed:1ms)
> (113ms)
> [wp] [Alt-Ergo] Goal typed_alloc_arr_copy_assign_normal_part5 : Unknown
> (Qed:2ms) (4.8s)
> [wp] [Alt-Ergo] Goal typed_alloc_arr_copy_post_5 : Timeout (Qed:2ms) (10s)
> [wp] Proved goals:   22 / 29
>      Qed:            18  (0.19ms-0.97ms-3ms)
>      Alt-Ergo:        4  (10ms-134ms-466ms) (896) (interrupted: 1)
> (unknown: 6)



I really appreciate your super awesome help information !

Thanks a lot !!!


Sincerely,
Wenhao Wu


On Mon, Mar 6, 2017 at 6:07 AM, Loïc Correnson <loic.correnson at cea.fr>
wrote:

> 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
>
>
>
> _______________________________________________
> 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/20170307/f1d322a8/attachment-0001.html>