[analysis] Add a generic powerset lattice #6059

tlively · 2023-10-27T20:50:02Z

Add Powerset2<Set> that implements the lattice of sets concretely represented
as Set ordered by subset as well as the full lattice FinitePowerset2<Set>
that is additionally configurted with the universe of set elements so it can
produce a top element, which is the set of everything in the universe.

The "2" in the name serves to temporarily differentiate these new powerset
lattices from the existing powerset lattices, which are less flexible and will
be replaced with the new powerset lattices in a future PR.

Also add a new BitSet utility that implements a set interface matching e.g.
std::set<size_t> or std::unordered_set<size_t> in terms of a
std::vector<bool> bit vector. Use BitSet as the concrete set implementation
used to fuzz Powerset2 and FinitePowerset2.

tlively · 2023-10-27T20:50:09Z

Current dependencies on/for this PR:

main
- PR [analysis][NFC] Rename parameters to join and meet methods #6056
  - PR [analysis] Implement an array lattice #6057
    - PR [analysis] Implement a vector lattice #6058
      - PR [analysis] Add a tuple lattice #6062
        
        PR [analysis] Add a lattice for value types #6064
        
        PR [analysis][NFC] Refactor lattice unit tests #6065
        
        PR [analysis] Add a "Shared" lattice to represent shared state #6067
        
        PR [analysis] Simplify the stack lattice #6069
        
        PR [analysis] Allow joining a single vector element efficiently #6071
        
        PR [analysis] Add a generic powerset lattice #6059 👈

This stack of pull requests is managed by Graphite.

kripken

Maybe pull out bitset to its own PR and add dedicated testing for it?

kripken · 2023-10-30T20:13:21Z

src/analysis/lattices/powerset2.h

+namespace wasm::analysis {
+
+// A powerset lattice whose elements are sets (represented concretely with type
+// `Set`) ordered by subset.


Perhaps we could call this a "Set Lattice", that is, a lattice over sets and ordered by the natural subset relation? "Powerset" is a specific mathematical operation to generate all subsets but this lattice here does not create a powerset nor does it require that the elements actually be a powerset IIANM.

If so then the one below could be "Powerset Lattice" (without "finite" in the name, which feels odd there to me).

It's true we never materialize the full powerset, but this lattice does represent a powerset. The lattice itself is the powerset, since its elements are subsets of the set of all T. For that reason, and to be consistent with the literature, we should continue calling this a powerset lattice.

Fair enough, but why is the latter called "finite" then, if both are finite?

The first one is not necessarily finite. There is no bound on the size of the elements it supports.

kripken · 2023-10-30T20:15:04Z

src/analysis/lattices/powerset2.h

+};
+
+// A powerset lattice initialized with a list of all elements in the universe,
+// making it possible to produce a top elements that contains all of them.


Suggested change

// making it possible to produce a top elements that contains all of them.

// making it possible to produce a top element that contains all of them.

kripken · 2023-10-30T20:16:51Z

src/support/bitset.h

+
+namespace wasm {
+
+// Represent a set of integers in [0, N) with a bitvector of size N, where a 1


Suggested change

// Represent a set of integers in [0, N) with a bitvector of size N, where a 1

// Represent a set of integers 0 <= k < N with a bitvector of size N, where a 1

Because the notation [0, N) is used in math to imply a half-open interval of real numbers. It's technically fine either way though.

Oh, I didn't know the interval notation typically implied real numbers. Will update.

Link for the curious: https://en.wikipedia.org/wiki/Interval_(mathematics)#Notations_for_intervals

kripken · 2023-10-30T20:21:19Z

src/support/bitset.h

+      const auto size = parent->size();
+      while (index < size && !(*parent)[index]) {
+        ++index;
+      }


Looks like this code advances to the first item in the set? A comment might help.

Yeah, I'll pull this out into a separate PR and add comments, as you suggest.

kripken · 2023-10-30T20:24:12Z

src/support/bitset.h

+  size_t size() const noexcept {
+    size_t result = 0;
+    for (auto it = begin(); it != end(); ++it, ++result) {
+    }


Wouldn't it be possibly simpler and faster to iterate on the underlying std::vector<bool>?

auto* super = (std::vector<bool>*)this; for (auto x : super) result += x;

(possibly simpler & faster since the current code will have nested loops)

I would hope it would optimize to the same thing, but yes, I can rewrite the code to use the underlying vector directly.

The elements of `Array<L, N>` lattice are arrays of length `N` of elements of `L`, compared pairwise with each other. This lattice is a concrete implementation of what would be written L^N with pen and paper.

The vector lattice is nearly identical to the array lattice, except that the size of the elements is specified at runtime when the lattice object is created rather than at compile time. The code and tests are largely copy-pasted and fixed up from the array implementation, but there are a couple differences. First, initializing vector elements does not need the template magic used to initialize array elements. Second, the obvious implementations of join and meet do not work for vectors of bools because they might be specialized to be bit vectors, so we need workarounds for that particular case.

This lattice combines any number of other lattices into a single lattice whose elements are tuples of elements of the other lattices. This will be one of the most important lattices in the analysis framework because it will be used to combine information about different parts of the program, e.g. locals and the value stack, into a single lattice.

Add `Powerset2<Set>` that implements the lattice of sets concretely represented as `Set` ordered by subset as well as the full lattice `FinitePowerset2<Set>` that is additionally configurted with the universe of set elements so it can produce a top element, which is the set of everything in the universe. The "2" in the name serves to temporarily differentiate these new powerset lattices from the existing powerset lattices, which are less flexible and will be replaced with the new powerset lattices in a future PR. Also add a new `BitSet` utility that implements a set interface matching e.g. `std::set<size_t>` or `std::unordered_set<size_t>` in terms of a `std::vector<bool>` bit vector. Use `BitSet` as the concrete set implementation used to fuzz `Powerset2` and `FinitePowerset2`.

tlively requested review from ashleynh and kripken October 27, 2023 20:50

This was referenced Oct 27, 2023

[analysis][NFC] Rename parameters to join and meet methods #6056

Merged

[analysis] Implement an array lattice #6057

Merged

This was referenced Oct 27, 2023

[analysis] Implement a vector lattice #6058

Merged

[analysis] Add a tuple lattice #6062

Merged

kripken reviewed Oct 30, 2023

View reviewed changes

tlively added 5 commits October 30, 2023 13:31

[analysis] Implement an array lattice

aff38de

The elements of `Array<L, N>` lattice are arrays of length `N` of elements of `L`, compared pairwise with each other. This lattice is a concrete implementation of what would be written L^N with pen and paper.

expand comment

8601941

expand comment

8efecb1

tlively force-pushed the vector-lattice branch from c5a6478 to 8efecb1 Compare October 30, 2023 21:15

tlively force-pushed the powerset-lattice branch from a34cf69 to 776ece1 Compare October 30, 2023 21:15

tlively changed the base branch from vector-lattice to tuple-lattice October 30, 2023 21:15

tlively marked this pull request as draft October 30, 2023 21:20

This was referenced Oct 30, 2023

[analysis] Add a lattice for value types #6064

Merged

[analysis][NFC] Refactor lattice unit tests #6065

Merged

tlively added 3 commits October 30, 2023 17:35

fix lint error about | with bools

b4d82c2

lint

da3663a

tlively force-pushed the powerset-lattice branch from 776ece1 to da3663a Compare October 31, 2023 00:35

tlively marked this pull request as ready for review October 31, 2023 00:35

tlively mentioned this pull request Oct 31, 2023

[analysis] Add a "Shared" lattice to represent shared state #6067

Merged

tlively force-pushed the tuple-lattice branch from b4d82c2 to 1458a3a Compare October 31, 2023 03:29

Base automatically changed from tuple-lattice to main October 31, 2023 04:10

This was referenced Nov 1, 2023

[analysis] Simplify the stack lattice #6069

Merged

[analysis] Allow joining a single vector element efficiently #6071

Merged

tlively marked this pull request as draft November 1, 2023 19:38

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[analysis] Add a generic powerset lattice #6059

[analysis] Add a generic powerset lattice #6059

tlively commented Oct 27, 2023

tlively commented Oct 27, 2023 •

edited

Loading

kripken left a comment

kripken Oct 30, 2023

tlively Oct 30, 2023

kripken Oct 30, 2023

tlively Oct 30, 2023

kripken Oct 30, 2023

kripken Oct 30, 2023

kripken Oct 30, 2023

tlively Oct 30, 2023

kripken Oct 30, 2023 •

edited

Loading

kripken Oct 30, 2023

tlively Oct 30, 2023

kripken Oct 30, 2023

kripken Oct 30, 2023

tlively Oct 30, 2023

	// making it possible to produce a top elements that contains all of them.
	// making it possible to produce a top element that contains all of them.


		namespace wasm {

		// Represent a set of integers in [0, N) with a bitvector of size N, where a 1

	// Represent a set of integers in [0, N) with a bitvector of size N, where a 1
	// Represent a set of integers 0 <= k < N with a bitvector of size N, where a 1

[analysis] Add a generic powerset lattice #6059

Are you sure you want to change the base?

[analysis] Add a generic powerset lattice #6059

Conversation

tlively commented Oct 27, 2023

tlively commented Oct 27, 2023 • edited Loading

kripken left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kripken Oct 30, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tlively commented Oct 27, 2023 •

edited

Loading

kripken Oct 30, 2023 •

edited

Loading