Use patricia-tree library more#2015
Conversation
sim642
added
performance
sim642
removed
the
pr-dependency
|
Unlike #2002, this doesn't seem to have notable impact. On sv-benchmarks there's no difference. On rsync this maybe improves by ~100s which is ~0.4%, but that could also be up to some noise. Still, I think this is a good idea because it eliminates the inefficient |
There was a problem hiding this comment.
Pull request overview
This PR expands use of the patricia-tree map implementation across the analyzer by refactoring MapDomain to rely on more specialized (and potentially more efficient) operations than the generic merge, and by switching multiple domains/analyses to PatriciaMapBot-based map domains.
Changes:
- Removes
mergefrom theMapDomaininterface and introducesdifferenceplus*_inter_filteroperations to express common patterns more directly. - Adds “lifted”
Patricia-basedMapDomainfunctors (PatriciaMapBot_LiftTop,PatriciaMapTop_LiftBot) and uses them in several analyses/domains. - Extends
CilType.FundecandCilType.Stmtwithtagso they can be used aspatricia-treekeys.
Reviewed changes
Copilot reviewed 9 out of 9 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| src/lifters/specLifters.ml | Switches context map domain from MapBot to PatriciaMapBot. |
| src/lifters/contextGasLifter.ml | Uses PatriciaMapBot_LiftTop for function gas tracking. |
| src/domain/mapDomain.ml | Refactors map interface (removes merge, adds difference and filtered intersections) and adds patricia-based lifted functors. |
| src/domain/disjointDomain.ml | Replaces merge-based logic with new difference / *_inter_filter operations. |
| src/common/util/cilType.ml | Adds tag implementations for Fundec and Stmt to support patricia keys. |
| src/cdomains/baseDomain.ml | Switches PartDeps map domain to PatriciaMapBot_LiftTop. |
| src/analyses/startStateAnalysis.ml | Switches analysis state map from MapBot to PatriciaMapBot. |
| src/analyses/loopTermination.ml | Switches loop statement map from MapBot to PatriciaMapBot. |
| src/analyses/commonPriv.ml | Switches lockset maps W/P to patricia-based lifted map domains. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
This is on top of #2002.
Changes
mergefromMapDomaininterface altogether. All of its uses have possibly more efficient alternatives in the patricia-tree library.PatriciaMapBotfor other domains than base values.Patriciafunctors toMapDomain.TODO
SetDomain? Not sure what this would improve, sets don't do such value operations.