Better solution for intersection of multiple sets?

[Laschoking]

Hi,
I am searching for a solution that is more clean than my current implementation. I would be glad about advise / some hints from more experienced souffle-users.

I want to implement Available Expression Analysis in doop at Basic Block level, which requires to calculate the intersection of multiple branches.
example:

 if () z = a+b; 
 else g = a+b;
 stmt;

at stmt both branches have met and a+b is available since the expression is computed on all incoming paths.

What I want is an approach how to (better) implement IntersectionOfPred(), which is used to find common expressions if there is more than one Predecessor.

 .decl BinaryExpressionBB(?BB:Instruction, ?exp:BinExp)
 .decl CFGEdge(?fromBB:Instruction, toBB:Instruction)
 .decl NrOfPred(?BB:Instruction, ?nr:number)
 .decl IntersectionOfPred(?BB:Instruction, ?exp:BinExp)
 .decl PotentialIntersection(?toBB:Instruction, ?fromBB:Instruction, ?exp:BinExp)

 BinaryExpressionBB(?toBB, ?exp):-
     BinaryExpressionBB(?fromBB, ?exp),
     CFGEdge(?fromBB, ?toBB),
     NrOfPred(?toBB, 1).
 
 PotentialIntersection(?toBB, ?fromBB, ?exp):-
     BinaryExpressionBB(?fromBB, ?exp),
     CFGEdge(?fromBB, ?toBB),
     NrOfPred(?toBB, ?nr),
     ?nr > 1.

 BinaryExpressionBB(?toBB, ?exp):-
     NrOfPred(?toBB, ?nr),
     ?nr > 1,
     IntersectionOfPred(?toBB,?exp).

One difficulty is that any amount of branches can join at a program point, so I need a solution that finds the intersection of all incoming branches.
Second problem is that I was not able to rely on Negation & Aggregate Functions inside IntersectionOfPred(), because it both adds facts to BinaryExpressionBB and relies on BinaryExpressionBB facts from the predecessor BB.

First Approach: Find all expressions that are not in ALL Predecessors, and then negate the set:
-> error due to stratified negation

 .decl NotJoin(?toBB:Instruction, ?exp:BinExp)

 NotJoin(?toBB, ?exp):-
     PotentialIntersection(?toBB, ?fromBB1, ?exp),
     !PotentialIntersection(?toBB, ?fromBB2, ?exp),
     ?fromBB1 != ?fromBB2.
 
 IntersectionOfPred(?toBB, ?exp):-
     PotentialIntersection(?toBB, ?fromBB, ?exp),
     !NotJoin(?toBB, ?exp).

Second approach: Counting the number of equivalent expressions & compare it to the number of predecessors
-> cyclic aggregation error, because PotentialIntersection leads to adding facts into BinaryExpressionBB, which in turn can create more PotentialIntersections.

IntersectionOfPred(?toBB, ?exp):-
     NrOfPred(?toBB, ?nr),
     ?nr > 1,
     ?d = count : {PotentialIntersection(?toBB, _, ?exp)},
     ?d = ?nr.

Third approach: pairwise intersection with help of string concatenation to keep track which predecessor expression were joined already:
-> kind of ugly work-around
-> for use of contains & cat-operation I replaced all types of Instruction by symbol (so it is handled like a string)

 .decl OneRandomPredecessor(?fromBB:symbol, ?toBB:symbol) choice-domain ?toBB
 .decl IntersectExpressions(?BB:symbol,?exp:BinExp,?catBB:symbol, ?nrJoins:number),

OneRandomPredecessor(?fromBB, ?toBB):-
    CFGEdge(?fromBB, ?toBB).
 
 IntersectExpressions(?toBB,?exp,?fromBB,1):-
     OneRandomPredecessor(?fromBB, ?toBB),
     NrOfPredBB(?toBB, ?c),
     ?c > 1,
     BinaryExpressionBB(?fromBB,?exp,?to).
 
 IntersectExpressions(?toBB,?exp,?catBBNew,?nrJoinsNew):-
     IntersectExpressions(?toBB,?exp,?catBB,?nrJoins),
     BinaryExpressionBB(?fromBB, ?exp),
     CFGEdge(?fromBB, ?toBB),
     !contains(?BB2,?catBB),
     ?catBBNew = cat(?catBB, ?fromBB).
 
 BinaryExpressionBB(?toBB, ?exp):-
     IntersectExpressions(?toBB, ?exp, _, ?nrJoins),
     NrOfPredBB(?toBB, ?nrJoins).

This approach works but it feels clumsy and I am wondering if you can suggest a better way.

[quentin]

The simple way to achieve this in your case would be to enforce that each node has at most N predecessors, then write the intersection rules to merge N branches, N-1 branches ... 1 branch. With N=2 being a good choice, you only need a rule for 2 branches intersection and 1 branch intersection (trivial).

Another solution would be to use user-defined aggregates (#2282). The semantics checkers is currently not very strict about them and you might be able to call user-defined aggregates in a recursive relation.

Last solution, not available yet, would be recursive aggregates (#2263).

[Laschoking]

Thanks for the reply. Breaking down multiple branches down, and recursively merging only two at a time worked out fine.

[quentin]

With the recent introduction of .lattice, there is an alternative solution to the merge problem if you are able to express your sets as a lattice domain.

See #2438