Improve how MFP handles dual powersets in the monotone framework
This is a small issue regarding the monotone framework internals. I'm happy to implement a fix below, but I wanted to get the okay from @VMatthijs in case I'm not understanding something.
I've been adding a simple monotone analysis that uses an intersection as its meet. I found that it fit a dual powerset as included with the monotone framework. I noticed that, because of the way our MFP implementation works, I needed to provide the total set of properties as the lattice bottom in order for intersection to work properly. In my case, this means traversing the whole MIR to find all RHS variables. In the case of lazy expressions, it means traversing to find all expressions. This adds a bit of complexity and computational cost. I see two solutions:
- Instead of using sets as properties directly, use a sum type with sets plus a 'Total' constructor, whose purpose is to be an identity for intersections. As far as I understand it, total sets are currently only required to act as an identity for intersections.
- Change the MFP to take the LUB over all predecessors at a time, rather than the LUB between the current properties of a node and the transfer of each predecessor individually. This is how I've seen the monotone framework and MFP formulated, and how I expected the LUB to be used, but I see that it would require changing the current (efficient looking) implementation.
Number 1 would be easy to do and I'd be happy to implement it. Number 2 would make the framework more intuitive to me, but would probably require re-implementing MFP, which is probably not a good idea.
Matthijs said he's going to be head down on a grant application for the next two weeks and won't have time for most stanc3 stuff - maybe @enetsee can take a look and advise?
Yeah, I figured - this really isn't time sensitive, since what's implemented now works, it's just might be a bit more complex and expensive than ideal.