Re: [PPL-devel] [Fwd: Fwd: Info on PPL]
Enea, thanks a lot for the prompt reply.
Giorgio Delzanno wrote:
Enea, together with Ahmed Rezine (in cc) we'd like to use PPL for defining a sort of "extrapolation" method (to be applied as a subroutine of a verification process). To give you an example, suppose we compute (forward) a sequence of tuples of values (valuation of variables) like (0,0) (1,1) (2,2)... From this we would like to "extrapolate" the constraint X=Y without fixing in advance the shape of equations (e.g. Y=MX+Q) we have to consider.
Is there some kind of acceleration/widening that can be applied in this case? Thanks in advance, Giorgio ps: ... eventually, we started using PPL :>
Giorgio,
the simple case above can be modeled using several (weakly) relational abstract domains, such as polyhedra, octagonal shapes and BD shapes, and probably using several variations of the standard widening of Cousot and Halbwachs.
Practically, suppose that you choose topologically closed polyhedra (i.e., class C_Polyhedron in the C++ interface of the PPL), using the standard widening (i.e., method H79_widening_assign in the C++ interface of the PPL). Let P_0, P_1, ..., P_i, ... be the sequence of polyhedra, where each P_i is a 2-dim polyhedron defined by the constraints { x = i, y = i }. Then, you will end up computing the sequence of Q_i where
Q_0 := P_0 = { x = 0, y = 0 };
Q_1 := hull_1.H79_widening_assign(Q_0) = { x = y, y >= 0 }, where hull_1 := the poly-hull of P_1 and Q_0 = { x = y, 0 <= y <= 1 }
Q_2 := hull_2.H79_widening_assign(Q_1) = Q_1 (fixpoint) where hull_2 := the poly-hull of P_2 and Q_1 = { x = y, 0 <= y <= 2 }
Hope this is what you really meant.
Ok. Is this the same as CH78 widening (based on constraint deletion)? We tried CC76_extrapolation on BDS but we probably forgot to compute the union.
To have a similar results for BDS, would it be correct to use something like
bds1= x=0,y=0 bds2= x=1,y=1
bds2=upper_bound_assign(bds1); // smallest bds union of bds1 and bds2 bd2=bds2.H79_widening_assign(bds1);
(I am writing from home and cannot test it right now). Thanks, Giorgio & Ahmed
Giorgio wrote:
Enea, thanks a lot for the prompt reply.
[...]
I made an small (irrelevant) error: clearly, the intermediate poly-hull hull_2 cannot have an upper bound constraint for dimension y:
Q_2 := hull_2.H79_widening_assign(Q_1) = Q_1 (fixpoint) where hull_2 := the poly-hull of P_2 and Q_1 = { x = y, 0 <= y <= 2 }
It is hull_2 = { x = y, 0 <= y } ( = Q_1)
Ok. Is this the same as CH78 widening (based on constraint deletion)?
It is basically that one, but enhanced so as to be well-defined even when the two arguments have a different affine dimension; the name H79 refers to the year of the PhD thesis of Halbwachs. For all the details, you can also have a look to
Precise Widening Operators for Convex Polyhedra. Roberto Bagnara, Patricia M. Hill, Elisa Ricci, and Enea Zaffanella. Science of Computer Programming, 58(1-2), pp. 28-56, 2005.
We tried CC76_extrapolation on BDS but we probably forgot to compute the union.
That is an important requirement: all the widening operators in the PPL assume that the current iterate, i.e., the object to be modified, is greater than (in lattice theoretic terms) of the previous iterate, i.e., the argument of the widening method. If such a requirement is not satisfied, the behavior is undefined. If you compile the library with assertions turned on, it will check the requirement automatically; however, this check is too costly to be included in the optimized build.
To have a similar results for BDS, would it be correct to use something like
bds1= x=0,y=0 bds2= x=1,y=1
bds2=upper_bound_assign(bds1); // smallest bds union of bds1 and bds2 bd2=bds2.H79_widening_assign(bds1);
(I am writing from home and cannot test it right now). Thanks, Giorgio & Ahmed
Yes, this should provide the very same result.
Cheers, Enea.
participants (2)
-
Enea Zaffanella -
Giorgio