[PPL-devel] Write constraints in JAVA interface as in C++ ?

[Enea Zaffanella]

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 at cs.unipr.it
> http://www.cs.unipr.it/mailman/listinfo/ppl-devel
>