On 07/31/2012 11:47 AM, Zell wrote:
Dear all,
If I understand correctly, the input for a PPL solver is a linear constraint system $C$, and the output is a (not always) optimal polyhedron represented as linear constraints that cover the points satisfying the original constraint system $C$.
The sentence above is quite confusing, mainly because it is not using established terminology. You should try to be clearer, possibly by adopting the PPL terminology (or by properly introduce your own).
What is a "PPL solver"?
I can guess from the rest of your message that you were meaning a C_Polyhedron object. If the guess is correct, then it is OK to say that you can build a C_Polyhedron starting from a linear constraint system (the "input"). Probably, when you say "the output" you mean the constraint system that can be obtained back from a polyhedron using method constraints(). If that is the case, then the output *is* optimal (i.e., there can be no precision loss), unless the polyhedron has been subject to operations that are explicitly documented (in the PPL manuals) to be suboptimal.
My question is, to use the library in practice, what are we supposed to do to convert Cousot's propagation-rule into a PPL's input which is a linear constraint system. ( Sankaranarayanan gave an algorithm using dualization and Farkas's lemma to compile a linear transition system into a constraint system, however I think there should be other prefered ways to do that because Sankaranarayanan's paper appeared later than PPL. )
Even less clear (at least for me). Let me guess once again: in the following I will assume that you are meaning a standard forward analysis based on abstract interpretation.
Here is an example:
1 x=0; 2: while (x<10){ 3: x = x+1; 4 } 5
Denote X[i] to be the set of possible values of 'x' at the program point 'i'. Then, the propagation-rule à la Cousot should be direct
X[1] = \emptyset X[2] \supset {0} \union X[4] X[3] \supset X2 \intersect (-\infinity, 10) X[4] \supset {x+1 | x\in X[4]} X[5] \supset X2 \intersect [10,\infinity)
How can we convert these set-constraints into PPL's input ?
All you need to do is to approximate the equations above using polyhedra objects (for the equation variables and constants) and polyhedra operations and then plug them into a fixpoint solver.
Since there is only one program variable, we can use 1-dimensional polyhedra, naming the (one and only) space dimension as "x":
Variable x(0);
NOTE: in the following I will adopt a C++-like syntax (it should not be difficult to translate it in Java if that is your preferred language interface). I will use different polyhedra ph[i] for each program point X[i] (to the detriment of efficiency), so as to keep things clearer. These polyhedra are initially created empty:
ph[i] = C_Polyhedron(1, EMPTY);
The first equation you wrote seems to be wrong; you should probably replace \emptyset with the domain universe, because (in a simplified setting with no overflows) just before the assignment "x=0" the value of variable "x" can be anything. So, the polyhedron for X[1] has no constraints at all:
ph[1] = C_Polyhedron(1, UNIVERSE);
The constant {0} in the equation for X[2] can be expressed as a linear constraint system as {x = 0}, i.e.,
Constraint_System cs2; cs2.insert(x == 0);
The polyhedron for X[2] is then built using an upper bound (i.e., convex polyhedral hull) operation:
ph[2] = C_Polyhedron(cs2); ph[2].upper_bound_assign(ph[4]);
(Note: in general, in order to enforce termination of the fixpoint computation, this upper bound should be eventually replaced by a suitable widening).
For X[3], use intersection:
Constraint_System cs3; cs3.insert(x <= 9); // Assuming x is integral. ph[3] = C_Polyhedron(cs3); ph[3].intersection_assign(ph[2]);
Similarly for X[5]:
Constraint_System cs5; cs5.insert(x >= 10); ph[5] = C_Polyhedron(cs5); ph[5].intersection_assign(ph[2]);
The equation for X[4] is an affine transformation:
ph[4] = ph[3]; ph[4].affine_image(x, x + 1);
In summary, if you know what you are doing, things should be quite simple (for this toy example). The PPL manuals should also be of some help.
Cheers, Enea.
Thanks for your ideas. Zell.
PPL-devel mailing list PPL-devel@cs.unipr.it http://www.cs.unipr.it/mailman/listinfo/ppl-devel