[PPL-devel] Re: Help with alias analysis framework

[Roberto Bagnara]

Ber Past wrote:
> Looking at the library documentation, it seems it fits exactly my needs. 
> I have only one question (probably stupid, but my knowledge of the 
> library is not yet very good): is there any operator/function that 
> allows to calculate the complement of a Polyhedron?
> 
> Thanks for your help.

Dear Ber,

I am not sure I understand what you need, so I will give
you two alternatives.

Our library (PPL) provides an operation called "poly-difference"
that yields the smallest convex polyhedron containing
the set-theoretic difference of its two arguments.
Computing the poly-difference of the universe polyhedron
and a polyhedron ph gives an upper approximation of the
complement.  This approximation can of course be extremely
coarse unless your application generates only a very
restricted class of polyhedra.

Alternatively, the PPL can represent the genuine complement
of a given convex polyhedron by a (finite) set of convex
polyhedra.  Sets of polyhedra are fully supported by
version 0.6 of the library, which has just been released.
Here is a small program to give you an idea of what you
can do:

-------------------------------- %< %< %< --------------------------------
#include <ppl.hh>

using namespace std;
using namespace Parma_Polyhedra_Library;
using namespace Parma_Polyhedra_Library::IO_Operators;

template <typename PH>
Polyhedra_PowerSet<NNC_Polyhedron>
complement(const PH& ph) {
   pair<PH, Polyhedra_PowerSet<NNC_Polyhedron> > partition
     = linear_partition(ph, PH(ph.space_dimension(), Polyhedron::UNIVERSE));
   return partition.second;
}

int main() {
   Variable x(0);
   Variable y(1);

   C_Polyhedron p(2, Polyhedron::EMPTY);
   p.add_generator(point(x));
   p.add_generator(point(y));
   p.add_generator(point(-x));
   p.add_generator(point(-y));

   cout << "p = " << p << endl;

   Polyhedra_PowerSet<NNC_Polyhedron> p_c = complement(p);

   cout << "complement(p) = " << p_c << endl;

   C_Polyhedron q(2);
   q.add_constraint(x >= -1);
   q.add_constraint(x <=  1);
   q.add_constraint(y >=  1);
   q.add_constraint(y <=  3);

   cout << "q = " << q << endl;

   Polyhedra_PowerSet<NNC_Polyhedron> q_c = complement(q);

   cout << "complement(q) = " << q_c << endl;

   return 0;
}
-------------------------------- %< %< %< --------------------------------

And here is the output of the program (newlines added for readability):

p = -A - B >= -1, -A + B >= -1, A - B >= -1, A + B >= -1
complement(p) = { { A + B > 1 }, { -A - B >= -1, A - B > 1 },
                   { -A - B >= -1, -A + B > 1 },
                   { -A - B > 1, -A + B >= -1, A - B >= -1 } }
q = -A >= -1, -B >= -3, B >= 1, A >= -1
complement(q) = { { A > 1 }, { -A >= -1, B > 3 },
                   { -A >= -1, -B > -1 }, { -A > 1, -B >= -3, B >= 1 } }

Notice that, in general, there are several possible representations
of the complement of a polyhedron as a set of polyhedra.  This
implementation guarantees that the resulting set is a partition
of the complement of the given polyhedron (i.e., that the members
of the set are pairwise disjoint).  It should also be possible
to prove that the partition returned has a reasonable number
of elements (such as the number of facets of the argument).
I hope this helps.  Please do not hesitate to come back to us
in case it doesn't.
All the best,

     Roberto

>> From: Roberto Bagnara <bagnara at cs.unipr.it>
>> To: BerPast <berpast at hotmail.com>
>> Subject: Re: Help with alias analysis framework
>> Date: Sat, 14 Aug 2004 09:30:12 +0200
>>
>> BerPast wrote:
>>
>>> In the paper "Interprocedural may-alias analysis for pointers: beyond
>>> k-limiting", the author presents a parametric framework for the
>>> analysis of pointer aliases.
>>> The framework is parametrised by a numeric lattice V#.
>>> The lattice has to have some abstract operators; the 4th are 5th are
>>> for me the most complex:
>>> 4) resolution of a linear system: given a system S, I need to compute
>>> a member of the lattice which is an upper approximation of the integer
>>> solutions to S;
>>> 5) intersection with a linear system: if S is a system of linear
>>> equations and K is a member of the lattice, I need to compute an upper
>>> approximation of the solutions to S that are also in K (no empty
>>> intersection with K I guess).
>>>
>>> I need to implement the lattice operators, but I have no idea of how
>>> to do this. Probably using Fourier-Motzkin projection I can solve the
>>> problem for the lattice obtained by the smash product of the interval
>>> lattice (any other, more efficient method?), but how can this problem
>>> be solved for a generic lattice?
>>> Can someone point out to me some documentation and (if available code
>>> implemenation) explaining how to solve this problem for a generic
>>> lattice?
>>
>>
>> I am not sure I understand what you mean by "[solving] this problem [...]
>> for a generic lattice."  All the numerical abstractions provided by the
>> Parma Polyhedra Library (http://www.cs.unipr.it/ppl/) come with the
>> operations that a numeric lattice must possess in Alain Deutsch's 
>> framework.
>> All the best,
>>
>>     Roberto Bagnara
>>
>> -- 
>> Prof. Roberto Bagnara
>> Computer Science Group
>> Department of Mathematics, University of Parma, Italy
>> http://www.cs.unipr.it/~bagnara/
>> mailto:bagnara at cs.unipr.it

-- 
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it