Frama-C-discuss mailing list archives

loic.correnson at cea.fr (Loïc Correnson) · Wed, 8 Mar 2017 10:01:59 +0100

This is a matter of choice. I just highlighted an idea of a general. Of course, you have to deal with
different pointer types. At the low level of WP internals, all pointers have `address` logical type, but from the ACSL point of view, they are
distinct logic types. You should use the same ALLOC counter for all pointers, but different logic functions for each type.
Consider reasoning on the k-th pointer allocated (whatever its type), and use different logic functions for each pointer.
Hence, you would have a unique ALLOC counter, a unique `Allocated` and `Allocating` predicates, but several allocating logic functions.

It is not a problem to have both `T1 *AllocT1(k)` and `T2 *AllocT2(k)` both potentially returning two different pointers of the corresponding types for the same value of `k`,
providing you never use both of them at the same time (because would live in the same region `k` and you could not reason about their separation).

Finishing the machinery is now up to you !
	L.

> Le 8 mars 2017 Ã  00:20, Wenhao Wu <wuwenhao at udel.edu> a Ã©crit :
> 
> 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 <mailto: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 <mailto: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 <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss <http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss>
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr>
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss <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/20170308/135056b9/attachment-0001.html>

Frama-C-discuss mailing list archives

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