Jessie Tutorial (811290), страница 2
Текст из файла (страница 2)
Typically, one can rely on preconditionsor loop invariants to prove safety.• To prove a VC in Default behavior, one can rely on VC in Safety. Typically, one can rely on ranges of valuesimplied by safety to prove loop invariants and postconditions.• To prove a VC in a Normal behavior, one can rely on VC in both Safety and Default behavior.Next, we detail how to prove each group of VC.7Chapter 2Safety CheckingA preliminary to any verification task using the Jessie plug-in is to verify the safety of functions. Safety has severalcomponents: memory safety, integer safety, termination. Memory safety deals with validity of memory accessesto allocated memory. Integer safety deals with absence of integer overflows and validity of operations on integers,such as the absence of division by zero.
Termination amounts to check whether loops are always terminating, andalso are recursive or mutually recursive functions.2.1Memory SafetyOur running example will be the famous binary_search function, which searches an element in an orderedarray of such elements.
On success, it returns the index at which the element appears in the array. On failure, itreturns -1.#pragma JessieIntegerModel(math)#pragma JessieTerminationPolicy(user)int binary_search(long t[], int n, long v) {int l = 0, u = n−1;while (l <= u) {int m = (l + u) / 2;if (t[m] < v)l = m + 1;else if (t[m] > v)u = m − 1;else return m;}return −1;}To concentrate first on memory safety only, we declare two pragmas as above. The first pragma dictates thatintegers in C programs behave as infinite-precision mathematical integers, without overflows. The second pragmatells the plugin to ignore termination issues.Let’s call Frama-C with the Jessie plug-in on this program:> frama-c -jessie binary-search.cAs seen on Figure 2.1, we get 3 VC, an obvious one that states the divisor 2 is not null, and two more thatstate the array access t[m] should be within bounds.
This is due to the memory model used, that decomposesany access check into two: one that states the access is above the minimal bound allowed, and one that states theaccess is below the maximal bound allowed.The obvious VC is trivially proved by all provers, while the two VC for memory safety cannot be proved.Indeed, it is false that, in any context, function binary_search is memory safe.
To ensure memory safety,binary_search must be called in a context which requires n to be positive and array t to be valid between8Figure 2.1: Memory safety with no annotationsindices 0 and n-1 included. Since function binary_search accesses array t inside a loop, it is not enough togive a function precondition to make the generated VC provable. Classically, one must add a loop invariant thatstates the guarantees provided on the array index, despite its changing value. It states that the value of index lstays within the bounds of the array t.//@ 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;while (l <= u ) {...There are now 7 VC generated: 2 to guarantee the loop invariant is initially established (because the conjunctis split), 2 to guarantee the same loop invariant is preserved through the loop, and the 3 VC seen previously.
Not allVC generated are proved automatically with these annotations. Of the 3 VC seen previously, the maximal boundcheck is still not proved. And the preservation of the loop invariant that deals with an upper bound on u is notproved either. It comes from the non-linear expression assigned to min the loop, that is difficult to take into accountautomatically.We solve this problem by adding an assertion to help automatic provers, providing some form of hint in theproof.
This can be done by inserting assertions in the code, or to add a globallemma, that should be proved usingavailable axioms, and used as an axiom in proving the VC for safety. This is working on our example./*@ lemma mean :@\forall integer x, y; x <= y ==> x <= (x+y)/2 <= y;@*///@ requires n >= 0 && \valid_range(t,0,n−1);int binary_search(long t[], int n, long v) {...}The results are shown on Figure 2.2, where all VCs, are proved by some prover.
This guarantees the memorysafety of function binary_search. The lemma itself is proved by Alt-Ergo, which has a little knowledge ofthe division operator. Given the lemma, other VCs are fully proved by Simplify and Z3, and partly by Yices andCVC3.2.2Integer Overflow SafetyLet’s now consider machine integers instead of idealized mathematical integers. This is obtained be remove thepragma JessieIntegerModel. The interpretation of integer types are now the true machine integers. How9Figure 2.2: Memory safety with precondition and loop invariantFigure 2.3: Memory safety + integer overflow safetyever, the default is a defensive interpretation, which forbids the arithmetic operations to overflow.1The result can be seen in Figure 2.3.There are 10 more VC to check integer operations return a result within1 In a context where it is intended for the operations to overflows, and thus operations are intentionnally done modulo, the same pragmashould be set to the value modulo, see Jessie manual.10Figure 2.4: Safety for patched programbounds, one of which only is not proved.
Except that, the result is nearly the same as with exact integers, exceptproving the lemma takes more time, due to the added layer of encoding for bounded integers.The only VC not proved checks that l+u does not overflow a machine integer. Nothing prevents this fromhappening with our current precondition for function binary_search [7]. There are two possibilities here. Theeasiest one is to strengthen the precondition by requiring that n is no more than half the maximal signed integerINT_MAX. The best one is to change the source of binary_search to prevent overflows even in presence oflarge integers.
It consists in changing the buggy lineint m = (l + u) / 2;intoint m = l + (u - l) / 2;This is our choice here. As shown in Figure 2.4, all VC 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 which asks toprove the wrong property 0 > 0. This is because we did not give any loop variant to the while loop.
A loopvariant is a quantity which must strictly decrease at each loop iteration, while remaining non-negative. In thisexample, a proper variant is u − l. So our annotated program now looks as follows./*@ lemma mean :@\forall integer x, y; x <= y ==> x <= (x+y)/2 <= y;@*///@ 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;11@*/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 to function’scontract.
It is also possible to prove termination by using variant on any datatype d equipped with any well-foundedrelation on d. See ACSL documentation for details.12Chapter 3Functional Verification3.13.1.1BehaviorsSimple functional propertyNow that the safety of function binary_search is proved, one can attempt the verification of functional properties, like the input-output behavior of function binary_search.
At the simplest, one can add a postconditionthat binary_search should respect upon returning to its caller. Here, we add bounds on the value returned bybinary_search. To prove this postcondition, strengthening the loop invariant is necessary./*@ lemma mean : \forall integer x, y; x <= y ==> x <= (x+y)/2 <= y; *//*@ 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;}As shown in Figure 3.1, all VC are proved automatically here.3.1.2More advanced functional propertiesOne can be more precise and separate the postcondition according to different behaviors. The assumes clause of abehavior gives precisely the context in which a behavior applies.
Here, we state that function binary_searchhas two modes: a success mode and a failure mode. This directly relies on array t to be sorted, thus we add thisas a general requirement. The success mode states that whenever the calling context is such that value v is in therange of t searched, then the value returned is a valid index. The failure mode states that whenever the callingcontext 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 to prove the VC generated.13Figure 3.1: General postcondition//@ lemma mean : \forall integer x, y; x <= y ==> x <= (x+y)/2 <= y;/*@ 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;@ 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;14Figure 3.2: Postconditions in behaviors}Figure 3.2 summarizes the results obtained in that case, for each behavior.3.2Advanced Algebraic ModelingThe following example introduces use of algebraic specification.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
