Hello Piotr.

I am not sure I have fully understood your requirements. For instance, I am not sure what you mean by "constraints over unshared dimensions": to my eyes, constraint y <= z is binding both shared and unshared dimensions. Please, take all of the following with a grain of salt, as I will write as I think, without proper testing of my ideas.

As far as I can tell, your join-like operator is not going to be well defined ...

Consider two polyhedra A and B, each one having a single, unshared dimension (i.e., no shared dimensions at all). A is defined by constraint a <= 1, B is defined by constraint b >= 0. Let's try and define your join-like polyhedron (on dimensions a and b).

One such polyhedron is C_0 defined by { a <= 1, b >= 0 }. However, for each integer k >= 1, we could take polyhedron C_k defined by { a <= 1, b >= 0, a <= b - k + 1}. Now (modulo silly mistakes on my side) for each C_k we have

proj_{a}(C_k) = A proj_{b}(C_k) = B

i.e., all of the C_k are good candidates as results for your join-like operation. When you have more than one candidate, the smaller the better, right? So, since C_k is a strict subset of C_{k-1}, C_k is better than C_{k-1}. The limit of this descending chain of polyhedra is C defined by { a <= 0, b >= 0 }. However, this polyhedron does not satisfy the required properties (namely, pi_{a}(C) is not a superset of A).

Can you confirm that here above I have not made silly mistakes?

Note: one may say that in the example above C_0 is going to be a better candidate since it is not "guessing" new constraints (namely, all its constraints occur in the arguments). However, I doubt such a "syntactic" way of reasoning would lead to a well defined operator either.

Are there other (implicit?) conditions that would make this operator well defined?

Enea.

On 04/25/2017 09:30 AM, Piotr Mardziel wrote:

Hello PPL developers;

I'm finding myself in need of a particular join-like operation but I'm having trouble finding the necessary operations in PPL to make it work. I figure that the need for this operation would be common especially when implementing inter-procedural program analyses so I'm suspicious that I'm just missing the right terminology for it. Let me explain this operation:

The setup has two polyhedra that model two sets of program variables with some variables shared but some variables not shared. For example:

polyhedron A has the constraint x ≤ y, w = 1 polyhedron B has the constraint y ≤ z, w = 2

Note that each of those two only has 3 space dimensions but the are not intended to represent the same 3 variables, hence I gave them names to distinguish them. Thus we see that y and w is shared between the two polyhedra, whereas x or z are only represented in A or B respectively.

Want I need is to join these two (thus requiring to first expand their dimensions to include all 4 dimensions) such that the result is a polyhedron C that "effectively" joins shared dimensions but preserves constraints over unshared dimensions, in this case I would like outcome C to have constraints x ≤ y ≤ z, 1 ≤ w ≤ 2 .

The problem is that to expand each input polyhedron to 4 dimensions, one either has to embed or project and then follow it up with either join or meet. The join doesn't handle the x,y,z portion of this problem correctly whereas meet doesn't handle the w portion correctly.

More technical, I need an operation over A, B to return a C with

     γ(A) ⊆ { π_{x,y,w} (e) | e ∈ γ(C) }
     γ(B) ⊆ { π_{y,z,w} (e) | e ∈ γ(C) }

Where γ is concretization, and π_{...}(e) is a projection of a tuple e to a subset of its dimensions. Top trivially satisfies this requirement but the polyhedron {x ≤ y ≤ z, 1 ≤ w ≤ 2} also satisfies it and does so much more precisely (is minimal in terms of a concretized subset relation).

Am I missing something obvious here? Any help would be greatly appreciated.

Best, Piotr (Peter) Mardziel _______________________________________________ PPL-devel mailing list PPL-devel@cs.unipr.it http://www.cs.unipr.it/mailman/listinfo/ppl-devel