Jessie Plugin, страница 2

Since functionbinary_search accesses array t inside a loop, providing a precondition is not enough to make thegenerated VC provable. One must also provide a loop invariant. A loop invariant is a property thatremains true at each iteration of the loop. It is often necessary for the user to provide these properties tohelp Jessie reason about loops. Assuming that the right property has been provided, Jessie is then leftwith the easier task of generating and verifying VCs that ensure that the property indeed holds at thebeginning of each iteration.In this example, it is necessary to provide an invariant that states the guarantees provided on the arrayindex, despite its changing value. It states that the value of index l stays within the bounds of the arrayt.//@ requires n >= 0 && \valid_range(t,0,n−1);int binary_search(long t[], int n, long v) {int l = 0, u = n−1;//@ loop invariant 0 <= l && u <= n−1;C.

Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 20172.2 Integer Overflow Safety11Figure 2.2: Memory safety + integer overflow safetywhile (l <= u ) {...Launching again the IDE after adding these annotations, you should obtain that all VCs are nowproved.2.2Integer Overflow SafetyLet us now consider machine integers instead of idealized mathematical integers. This is obtained by removing the pragma JessieIntegerModel. Without this pragma, integer types are now interpretedas bounded machine integers. However, the default is a defensive interpretation, which forbids the arithmetic operations to overflow.1The result can be seen in Figure 2.2.

There are more subgoals to Safety VC, to check that integeroperations return a result within bounds, only one of which is not proved. With this exception, the resultsare nearly the same as with exact integersThe only unproved VC expresses that l+u does not overflow. Nothing prevents this from happeningwith our current precondition for function binary_search [7]. There are two possibilities here. Theeasiest is to strengthen the precondition by requiring that n is no more than half the maximal signedinteger INT_MAX.

The best way is to change the source of binary_search to prevent overflows evenin presence of large integers. It consists in changing the buggy lineint m = (l + u) / 2;into1In a context where it is intended for the operations to overflows, and thus operations are intentionnally done modulo, thesame pragma should be set to the value modulo, see Jessie manual.C. Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 201712Safety Checkingint m = l + (u - l) / 2;This is our choice here. All VCs are now proved automatically.2.3Checking TerminationThe last kind of safety property we want is termination.

To check it, we first remove the pragmaJessieTerminationPolicy. If we run the VC generation again, we get an additional VC thatrequires to prove the property 0 > 0. This VC is false, so our first step should be to help Jessie generatea more provable VC. The VC 0 > 0 is generated because we did not provide any loop variant for thewhile loop. A loop variant is a quantity which must decrease strictly at each loop iteration, while provably remaining non-negative for as long as the loop runs. In this example, a proper variant is u − l.

Soour annotated program now looks as follows://@ requires n >= 0 && \valid_range(t,0,n−1);int binary_search(long t[], int n, long v) {int l = 0, u = n−1;/*@ loop invariant 0 <= l && u <= n−1;@ loop variant u−l;@*/while (l <= u) {int m = l+(u−l) / 2;if (t[m] < v)l = m + 1;else if (t[m] > v)u = m − 1;else return m;}return −1;}The additional VC is now proved.Termination of recursive functions can be dealt with similarly by adding a decreases clause tothe function’s contract.

It is also possible to prove termination by using variants over any datatype dequipped with a well-founded relation. See the ACSL documentation for details.C. Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 2017Chapter 3Functional Verification3.13.1.1BehaviorsSimple functional propertyNow that the safety of function binary_search has been established, one can attempt the verificationof functional properties, like the input-output behavior of function binary_search. At the simplest,one can add a postcondition that binary_search should respect upon returning to its caller.

Here, weadd bounds on the value returned by binary_search. To prove this postcondition, strengthening theloop invariant is necessary./*@ requires n >= 0 && \valid_range(t,0,n−1);@ ensures −1 <= \result <= n−1;@*/int binary_search(int* t, int n, int v) {int l = 0, u = n−1;/*@ loop invariant 0 <= l && u <= n−1;@ loop variant u−l;@*/while (l <= u) {int m = l + (u − l) / 2;if (t[m] < v)l = m + 1;else if (t[m] > v)u = m − 1;else return m;}return −1;}All VCs are proved automatically here.3.1.2More advanced functional propertiesOne can be more precise and separate the postcondition according to different behaviors.

The assumesclause of a behavior gives precisely the context in which a behavior applies. Here, we state that functionbinary_search has two modes: a success mode and a failure mode. This directly relies on array t tobe sorted, thus we add this as a general requirement. The success mode states that whenever the callingcontext is such that value v is in the range of t searched, then the value returned is a valid index.

The14Functional VerificationFigure 3.1: Postconditions in behaviorsfailure mode states that whenever the calling context is such that value v is not in the range of t searched,then function binary_search returns -1. Again, it is necessary to strengthen the loop invariant toprove the VC generated./*@ requires n >= 0 && \valid_range(t,0,n−1);@ behavior success:@assumes // array t is sorted in increasing order@\forall integer k1, k2; 0 <= k1 <= k2 <= n−1 ==> t[k1] <= t[k2];@assumes // v appears somewhere in the array t@\exists integer k; 0 <= k <= n−1 && t[k] == v;@ensures 0 <= \result <= n−1;@ behavior failure:@assumes // v does not appear anywhere in the array t@\forall integer k; 0 <= k <= n−1 ==> t[k] != v;@ensures \result == −1;@*/int binary_search(long t[], int n, long v) {int l = 0, u = n−1;/*@ loop invariant 0 <= l && u <= n−1;@ for success:@loop invariant@\forall integer k; 0 <= k < n && t[k] == v ==> l <= k <= u;C.

Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 20173.2 Advanced Algebraic Modeling15@ loop variant u−l;@*/while (l <= u) {int m = l + (u − l) / 2;if (t[m] < v)l = m + 1;else if (t[m] > v)u = m − 1;else return m;}return −1;}Figure 3.1 summarizes the results obtained in that case, for each behavior.3.2Advanced Algebraic ModelingThe following example introduces use of algebraic specification.

The goal is the verify a simple sortingalgorithm (by extraction of the minimum).The first step is to introduce logical predicates to define the meanings for an array to be sorted in increasing order, to be a permutation of another. This is done as follows, in a separate file say sorting.h/*@ predicate Swap{L1,L2}(int *a, integer i, integer j) =@\at(a[i],L1) == \at(a[j],L2) &&@\at(a[j],L1) == \at(a[i],L2) &&@\forall integer k; k != i && k != j@==> \at(a[k],L1) == \at(a[k],L2);@*//*@ inductive Permut{L1,L2}(int *a, integer l, integer h) {@ case Permut_refl{L}:@\forall int *a, integer l, h; Permut{L,L}(a, l, h) ;@ case Permut_sym{L1,L2}:@\forall int *a, integer l, h;@Permut{L1,L2}(a, l, h) ==> Permut{L2,L1}(a, l, h) ;@ case Permut_trans{L1,L2,L3}:@\forall int *a, integer l, h;@Permut{L1,L2}(a, l, h) && Permut{L2,L3}(a, l, h) ==>@Permut{L1,L3}(a, l, h) ;@ case Permut_swap{L1,L2}:@\forall int *a, integer l, h, i, j;@l <= i <= h && l <= j <= h && Swap{L1,L2}(a, i, j) ==>@Permut{L1,L2}(a, l, h) ;@ }@*//*@ predicate Sorted{L}(int *a, integer l, integer h) =@\forall integer i,j; l <= i <= j < h ==> a[i] <= a[j] ;C.

Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 201716Functional Verification@*/The code is then annotated using these predicates as follows#pragma JessieIntegerModel(math)#include "sorting.h"/*@ requires \valid(t+i) && \valid(t+j);@ assigns t[i],t[j];@ ensures Swap{Old,Here}(t,i,j);@*/void swap(int t[], int i, int j) {int tmp = t[i];t[i] = t[j];t[j] = tmp;}/*@ requires \valid_range(t,0,n−1);@ behavior sorted:@ensures Sorted(t,0,n);@ behavior permutation:@ensures Permut{Old,Here}(t,0,n−1);@*/void sel_sort(int t[], int n) {int i,j;int mi,mv;if (n <= 0) return;/*@ loop invariant 0 <= i < n;@ for sorted:@ loop invariant@Sorted(t,0,i) &&@(\forall integer k1, k2 ;@0 <= k1 < i <= k2 < n ==> t[k1] <= t[k2]) ;@ for permutation:@ loop invariant Permut{Pre,Here}(t,0,n−1);@ loop variant n−i;@*/for (i=0; i<n−1; i++) {// look for minimum value among t[i..n−1]mv = t[i]; mi = i;/*@ loop invariant i < j && i <= mi < n;@ for sorted:@ loop invariant@mv == t[mi] &&@(\forall integer k; i <= k < j ==> t[k] >= mv);@ for permutation:@ loop invariant@Permut{Pre,Here}(t,0,n−1);@ loop variant n−j;@*/C.

Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 20173.2 Advanced Algebraic Modeling17for (j=i+1; j < n; j++) {if (t[j] < mv) {mi = j ; mv = t[j];}}L:swap(t,i,mi);//@ assert Permut{L,Here}(t,0,n−1);}}Each VC is proved by at least by Z3. The behavior “sorted” is the most diificult one. Indeed, if yousplit this one into subgolas, then all subgoals are proved by Alt-Ergo too.C. Marché, Y.

MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 201718C. Marché, Y. MoyFunctional VerificationWhy platform, Jessie plugin for Frama-CToccata, August 23, 2017Chapter 4Separation of Memory RegionsBy default, the Jessie plug-in assumes different pointers point into different memory regions. E.g., thefollowing postcondition can be proved on function max, because parameters r, i and j are assumed topoint into different regions./*@ requires \valid(i) && \valid(j);@ requires r == \null || \valid(r);@ ensures *i == \old(*i) && *j == \old(*j);@*/int max(int *r, int* i, int* j) {if (!r) return −1;*r = (*i < *j) ? *j : *i;return 0;}To change this default behavior, add the following line at the top of the file:# pragma SeparationPolicy(none)In this setting, the postcondition cannot be proved anymore.

Now, function max should only becalled in a context where parameters r, i and j indeed point into different regions, like the following:int main(int a, int b) {int c;max(&c,&a,&b);return c;}In this context, all VCs are proved.In fact, regions that are only read, like the regions pointed to by i and j, need not be disjoint. Sincenothing is written in these regions, it is still correct to prove their contract in a context where they areassumed disjoint, whereas they may not be disjoint in reality. It is the case in the following context:int main(int a, int b) {int c;max(&c,&a,&a);return c;}20Separation of Memory RegionsIn this context too, all VCs are proved.Finally, let’s consider the following case of a context in which a region that is read and a functionthat is written are not disjoint:int main(int a, int b) {int c;max(&a,&a,&b);return c;}The proof that regions are indeed disjoint boils down to proving that set of pointers {&a} and {&a}are disjoint (because function max only writes and reads *r and *i), which is obviously false.C.