SPARTA
SPARTA is a library of software components specially designed for building high-performance static analyzers based on the theory of Abstract Interpretation.
by facebookC++
Commit activity
Last 12 weeks · 9 commits
Community health
4 of 6 standards met
75
✓README✓License✓Contributing✓Code of Conduct○Issue Template○PR Template
Recent PRs & issues
Active · 1 in progress · Last activity 17h ago
See all on GitHub →
When using , the resulting abstract domain's "top" is not an identity element of "meet" and the resulting abstract domain's "bottom" is not an identity element of "join". This is described in more detail in #25. This PR proposes adding tests and changing the proc macro so that these tests pass. Depends on #26 (I'll re-base once that one is merged).
Recent fixes
The "bottom" element of a Lattice is the identity element of the "join" operation. The "top" element of a Lattice is the identity element of the "meet" operation. But when using the macro, I can create elements for which and . Reproducible Example These tests should pass: but they fail with the following error message: Solution replace https://github.com/facebook/SPARTA/blob/bd758a81954dc2c8fe75c8b32ab42d327fc4d895/rust-proc-macros/src/lib.rs#L87-L99 with
Problem The branch-vs-branch case of in had its two arms swapped. When the two compared Patricia trees have branch prefixes of different lengths (one prefix is a proper prefix of the other), both the implicit-value condition ( vs ) and the recursion direction were mirrored relative to the reference implementation in . This produces incorrect results for both map flavors: (implicit value = Bottom) (implicit value = Top) Concrete counterexample With Bottom implicit values, should be (the missing bindings in the smaller map are Bottom, which is any value), but the swapped arm short-circuited on and returned . Symmetrically, with Top implicit values, should be (the larger map's extra bindings are Top), but it returned . Fix Align the two arms with the C++ semantics: (s is deeper, s's keys are a subset of t's): require and recurse into the matching child of . (t is deeper, t's keys are a subset of s's): require and recurse into the matching child of . Tests Added to and to . Both fail before the fix and pass after it, and cover the direction in both directions.
Summary Upgrade GitHub Actions to their latest versions to ensure compatibility with Node 24, as Node 20 will reach end-of-life in April 2026. Changes Context Per GitHub's announcement, Node 20 is being deprecated and runners will begin using Node 24 by default starting March 4th, 2026. Why this matters Node 20 EOL: April 2026 Node 24 default: March 4th, 2026 Action**: Update to latest action versions that support Node 24 Security Note Actions that were previously pinned to commit SHAs remain pinned to SHAs (updated to the latest release SHA) to maintain the security benefits of immutable references. Testing These changes only affect CI/CD workflow configurations and should not impact application functionality. The workflows should be tested by running them on a branch before merging.
Structured data for AI agents
Repository: facebook/SPARTA. Description: SPARTA is a library of software components specially designed for building high-performance static analyzers based on the theory of Abstract Interpretation. Stars: 672, Forks: 57. Primary language: C++. Languages: C++ (78.9%), Rust (20.3%), CMake (0.8%), Shell (0.1%). License: MIT. Open PRs: 1, open issues: 1. Last activity: 17h ago. Community health: 75%. Top contributors: arthaud, NTillmann, nikolait-meta, ssj933, agampe, arnaudvenet, yuxuanchen1997, int3, zertosh, xuhdev and others.