Skip to content

Use llvm::DenseSet for seadsa_heap_abs_impl::NodeSet#102

Open
LinerSu wants to merge 1 commit into
seahorn:dev14from
LinerSu:dev14
Open

Use llvm::DenseSet for seadsa_heap_abs_impl::NodeSet#102
LinerSu wants to merge 1 commit into
seahorn:dev14from
LinerSu:dev14

Conversation

@LinerSu

@LinerSu LinerSu commented May 11, 2026

Copy link
Copy Markdown
Contributor

Summary

  • Replace seadsa_heap_abs_impl::NodeSet backing storage from std::set to llvm::DenseSet.
  • Add orderedNodes to preserve deterministic node traversal where read/mod/new and equivalence-class results are built.
  • Update NodeSet union and difference helpers to use DenseSet insert and erase operations.

Why

std::set is inefficient for this use case because the node collections are primarily membership sets, so the tree ordering overhead is unnecessary. llvm::DenseSet is a better fit for lookup, insertion, and deletion. Where iteration order affects observable output, nodes are sorted explicitly by SeaDsa node ID before traversal.

Co-authored-by: Codex <codex@openai.com>
std::set_union(s1.begin(), s1.end(), s2.begin(), s2.end(),
std::inserter(s3, s3.end()));
std::swap(s3, s1);
void set_difference(NodeSet &s1, const NodeSet &s2) {

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The original implementation of set_difference and set_union runs in O(|s1| + |s2|) because it assumes that s1 and s2 are sorted. Your implementation runs in O(|s2| x log(|s1|) which is slower for large sets. What is your motivation for changing them?

std::set_difference(s1.begin(), s1.end(), s2.begin(), s2.end(),
std::inserter(s3, s3.end()));
std::swap(s3, s1);
OrderedNodeVec orderedNodes(const NodeSet &set) {

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This code is equivalent but cleaner in my opinion

OrderedNodeVec nodes(set.begin(), set.end());
std::sort(nodes.begin(), nodes.end(), NodeOrdering{});
return nodes;

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants