[analysis] Add an abstraction lattice #8036

tlively · 2025-11-10T02:53:29Z

The abstraction lattice is composed of increasingly abstract
sub-lattices. Elements of the abstraction lattice are variants that may
hold the elements of any of its constituent lattices. When elements from
different sub-lattices are compared or joined, the more concrete element
is first abstracted into the lattice of the other element. Unrelated
elements in the same lattice may be abstracted before they are joined.
This choice and the abstraction operation itself are provided by CRTP
subclasses of Abstraction.

This is an important building block for eventually reconstructing
PossibleContents on top of the lattice framework.

The abstraction lattice is composed of increasingly abstract sub-lattices. Elements of the abstraction lattice are variants that may hold the elements of any of its constituent lattices. When elements from different sub-lattices are compared or joined, the more concrete element is first abstracted into the lattice of the other element. Unrelated elements in the same lattice may be abstracted before they are joined. This choice and the abstraction operation itself are provided by CRTP subclasses of Abstraction. This is an important building block for eventually reconstructing PossibleContents on top of the lattice framework.

kripken · 2025-11-10T17:42:47Z

src/analysis/lattices/abstraction.h

+//   template<size_t I, typename E>
+//   bool shouldAbstract(const E&. const E&) const
+//
+// shouldAbstract is only queries for unrelated elements. Related elements of


Suggested change

// shouldAbstract is only queries for unrelated elements. Related elements of

// shouldAbstract is only queried for unrelated elements. Related elements of

kripken · 2025-11-10T17:45:30Z

test/gtest/lattices.cpp

 }
+
+using OddEvenInt = analysis::Flat<uint32_t>;
+using OddEvenBool = analysis::Flat<bool>;


What does "odd even int" mean? Every integer is already even or odd. This seems like just an integer?

"odd even bool" I can see as being interpreted as "a boolean saying whether it is even or odd"- is that right?

Yes, this is just an integer. I could use a namespace instead of the OddEven name prefix, perhaps. Yes, the bool is true for even, false for odd, and top when it can be either.

kripken · 2025-11-10T21:08:28Z

src/analysis/lattices/abstraction.h

+          return LESS;
+        case NO_RELATION:
+        case GREATER:
+          return NO_RELATION;


I don't follow this. We abstract a, then compare - but we turn that outcome into either "less" or "no"? Why can't we return "greater"or "equal"?

The element a came from a more concrete lattice than element b, so a cannot possibly be equal to or greater than b, even if its abstracted version is.

Ah, then my mental model is all wrong here.

I was thinking "an abstraction lattice has items from a tower of types. when it needs to, it abstracts - moves a type up the tower. but otherwise it works normally, i.e., when it has two values to compare, it abstracts the ones it needs to, then compares - and that result can be anything at all".

From what you are saying, it seems there is a ordering of some kind in the tower... is that right? How precisely?

(My mental model is based on the example test, where it seems it abstracts an int to an even/odd as needed, and after such abstraction, the result can be anything... so I may have misunderstood that too.)

Yes, there's a tower of sub-lattices. But elements from a lower sub-lattice are always less than elements from higher sub-lattices. Otherwise the user would have to provide complete implementations of comparisons and joins across sub-lattices, so the user code would become quadratic in the number of sub-lattices rather than linear.

The test lattice looks like this:

top / \ even odd /|\... /|\... ... ... \ / \ / 0 1 2 3 ... \ \ / / bot

All the integer elements are less than the even/odd bool elements.

Yes, for sure. But abstract(X) is a different lattice element than X, so abstract(X) > Y does not imply that X > Y. And indeed we know that either X < Y or X <> Y if X had to be abstracted to be in the same sub-lattice as Y.

But abstract(X) is a different lattice element than X, so abstract(X) > Y does not imply that X > Y.

Then I do not understand the motivation for this lattice.

My sense was "abstract as you need, until you can compare things." So if my lattice has integers and even/odd, then given 42 and odd, I must abstract the 42 - but after doing so, I then compare it. And, if even/odd was not flat, that outcome could go either way.

That seems obviously useful in practice - when given 42,1337, the comparison just works; when given even,odd, the same; when given a mix like 42/odd, we abstract "just enough", looking at a higher level, which misses details but at least we get some useful abstraction out of our abstract interpretation.

Put another way, given 42,1337, we could also abstract them both before comparing. Maybe that makes sense for some reason, like distilling them to the core information we care about. We abstract to the properties we care about, then compare/operate.

If, instead, abstract(X) > Y does not imply that X > Y, then I'm not sure how this would be used in practice - can you please elaborate?

The elements 42 and 1337 are not related, but when they are joined they are both abstracted, becoming even and odd, which are still not related. But there is no further abstraction possible, so they are then joined to become top.

To take another example, 42 and even are related. 42 is less than even. When 42 and even are joined, the 42 is abstracted to even and then joined with the other even, producing even.

For yet another example, 42 and 2 are not related. When they are joined, they are both abstracted to even and the result is even. If I understand the way you are thinking we should do things, then to compare 42 and 2 we would first abstract them and then compare. But that would give EQUALS, and 42 is clearly not equal to 2.

The elements 42 and 1337 are not related, but when they are joined they are both abstracted, becoming even and odd, which are still not related.

And if the even/odd lattice was not flat? Say odd < even. What happens then?

We figured out offline that the issue is that the abstraction transformation must be monotonic. With that in place, the weird situations I was envisioning are ruled out.

kripken · 2025-11-11T21:40:11Z

src/analysis/lattices/abstraction.h

+        }
+      }...};
+  }
+  static constexpr auto shouldAbstracts() noexcept {


"should abstracts" doesn't sound grammatical... am I reading it wrong?

It's because it's generating a table with multiple shouldAbstract methods in it :D

We could call this shouldAbstractTable() instead.

or makeShouldAbstracts?

tlively requested a review from kripken November 10, 2025 02:53

tlively force-pushed the lattice-abstraction branch from 0ed9242 to 82ce454 Compare November 10, 2025 02:54

tlively force-pushed the lattice-abstraction branch from 82ce454 to 7b596ad Compare November 10, 2025 02:59

kripken reviewed Nov 10, 2025

View reviewed changes

tlively added 4 commits November 10, 2025 16:24

queries -> queried

a5ebc6b

simplify type indexing

d8da812

Move specializations out of class scope for older compilers

b9a05f2

more tests

44b8a23

kripken reviewed Nov 11, 2025

View reviewed changes

	// shouldAbstract is only queries for unrelated elements. Related elements of
	// shouldAbstract is only queried for unrelated elements. Related elements of

[analysis] Add an abstraction lattice #8036

Are you sure you want to change the base?

[analysis] Add an abstraction lattice #8036

Conversation

tlively commented Nov 10, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants