--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on March 2017 ---
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>