Jessie Tutorial (811290), страница 3
Текст из файла (страница 3)
The goal is the verify a simple sorting algorithm(by extraction of the minimum).The first step is to introduce logical predicates to define the meanings for an array to be sorted in increasingorder, 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) ;15@ 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; l <= i < h ==> a[i] <= a[i+1] ;@*/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−1);@ behavior permutation:@ensures Permut{Old,Here}(t,0,n−1);@*/void min_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:16Figure 3.3: VCs for minimum sort@ 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;@*/for (j=i+1; j < n; j++) {if (t[j] < mv) {mi = j ; mv = t[j];}}swap(t,i,mi);}}Each VC is proved by at least one prover.
Figure 3.3 displays the results in GWhy, with emphasis on the VCfor preservation of the loop invariant for permutation behavior, which is the most difficult one, only proved byAlt-Ergo.17Chapter 4Inference of AnnotationsInference of annotations is an experimental feature of the Jessie plugin, whose theoretical bases are describedin [5, 6].4.1Postconditions and Loop InvariantsTo alleviate the annotation burden, it is possible to ask the Jessie plug-in to infer some of them, through a combination of abstract interpretation and weakest preconditions. This requires that APRON library for abstract interpretation is installed and Frama-C configuration recognized it.
Then, one can call> framac -jessie -jessie-atp=simplify -jessie-infer-annot inv max.cto perform abstract interpretation on program max.c, which computes necessary loop invariants and postconditions (meaning an overapproximation of the real ones).int max(int *r, int* i, int* j) {if (!r) return −1;*r = (*i < *j) ? *j : *i;return 0;}On our unannotated max.c program, this produces postcondition true for the first return and\valid(r) && \valid(i) && \valid(j) for the second return.Various domains from APRON library are available with option -jessie-abstract-domain:• box - domain of intervals, where an integer variables is bounded by constants.• oct - domain of octagons, where the sum and difference of two integer variables are bounded by constants.• poly - domain of polyhedrons, computing linear relations over integer variables.4.2Preconditions and Loop InvariantsPreconditions can also be computed by calling> framac -jessie -jessie-atp=simplify -jessie-infer-annot pre max.cwhich attemps to compute a sufficient precondition to guard against safety violations and prove functional properties.
In case it computes false as sufficient precondition, which occurs e.g. each time the property is beyondthe capabilities of our method, it simply ignores it. Still, our method can compute a stronger precondition thannecessary. E.g., on function max, it computes precondition \valid(r) && \valid(i) && \valid(j),while a more precise precondition would allow r to be null. Still, the generated precondition is indeed sufficientto prove the safety of function max:18Running Simplify on proof obligations(.
= valid * = invalid ? = unknown # = timeout ! = failure)simplify/max_why.sx: ......... (9/0/0/0/0)To improve on the precision of the generated precondition, various methods have been implemented:• Quantifier elimination - This method computes an invariant I at the program point where check C shouldhold, forms the quantified formula \forall x,y... ; I ==> C over local variables x,y..., andeliminates quantifiers from this formula, resulting in a suffcient precondition. This is the method called withoption -jessie-infer-annot pre.• Weakest preconditions with quantifier elimination - This method improves on direct quantifier elimination by propagating formula I ==> C backward in the control-flow graph of the function beforequantifying over local variables and eliminating quantifiers.
This is the method called with option-jessie-infer-annot wpre.• Modified weakest preconditions with quantifier elimination - This method strengthen the formula obtainedby weakest preconditions with quantifier elimination, by only considering tests and assignments which dealwith variables in the formula being propagated. Thus, it may result in a stronger precondition (i.e. a precondition less precise) but at a smaller computational cost. In particular, it may be applicable to programswhere weakest preconditions with quantifier elimination is too costly.
This is the method called with option-jessie-infer-annot spre.19Chapter 5Separation of Memory RegionsBy default, the Jessie plug-in assumes different pointers point into different memory regions. E.g., the followingpostcondition can be proved on function max, because parameters r, i and j are assumed to point into differentregions./*@ 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, call instead> frama-c -jessie -jessie-atp=simplify -jessie-no-regions max.cIn this setting, the postcondition cannot be proved:Running Simplify on proof obligations(. = valid * = invalid ? = unknown # = timeout ! = failure)simplify/max_why.sx: ?..?........
(10/0/2/0/0)Now, function max should only be called in a context where parameters r, i and j indeed point into differentregions, like the following:int main(int a, int b) {int c;max(&c,&a,&b);return c;}In this context, all VC are proved.In fact, regions that are only read, like the regions pointed to by i and j, need not be disjoint. Since nothingis written in these regions, it is still correct to prove their contract in a context where they are assumed 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;}20In this context too, all VC are proved.Finally, let’s consider the following case of a context in which a region that is read and a function that is writtenare 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.21Chapter 6Treatment of Unions and CastsUnions without pointer fields are translated to bitvectors, so that access in these unions are translated to lowlevel accesses.
Thus, the following code can be analyzed, but we do not yet provide a way to prove the resultingassertions, by asserting that any subset of bits from the bitvector representation of 0 is 0:union U {int i;struct { short s1; short s2; } s;};//@ requires \valid(x);void zero(union U* x) {x−>i = 0;//@ assert x−>s.s1 == 0;//@ assert x−>s.s2 == 0;}Unions with pointer fields (either direct fields or sub-fields of structure fields) are translated differently, becausewe treat pointers differently than other types, to allow an automatic analysis of separation of memory blocks. Thus,we treat unions with pointer fields as discriminated unions, so that writing in a field erases all information on otherfields.
This allows to verify the following program:union U {int i;int* p;};//@ requires \valid(x);void zero(union U* x) {x−>i = 0;//@ assert x−>i == 0;x−>p = (int*)malloc(sizeof(int));*x−>p = 1;//@ assert *x−>p == 1;}Finally, casts between pointer types are allowed, with the corresponding accesses to memory treated as lowlevel accesses to some bitvector. This allows to verify the safety of the following program://@ requires \valid(x);void zero(int* x) {char *c = (char*)x;*c = 0;c++;22*c = 0;c++;*c = 0;c++;*c = 0;}Notice that unions are allowed in logical annotations, but not pointer casts yet.23Chapter 7Reference Manual7.1General usageThe Jessie plug-in is activated by passing option -jessie to frama-c.
Running the Jessie plug-in on a file f.jcproduces the following files:• f.jessie: sub-directory where every generated files go• f.jessie/f.jc: translation of source file into intermediate Jessie language• f.jessie/f.cloc: trace file for source locationsThe plug-in will then automatically call the Jessie tool of the Why platform to analyze the generated file f.jcabove. By default, VCs are generated and displayed in the GWhy interface.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
