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'

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>