Use patricia-tree library more

[sim642]

This is on top of #2002.

Changes

1. Remove slow merge from MapDomain interface altogether. All of its uses have possibly more efficient alternatives in the patricia-tree library.
2. Use PatriciaMapBot for other domains than base values.
3. Add lifted versions of Patricia functors to MapDomain.

TODO

• Use patricia-tree also in SetDomain? Not sure what this would improve, sets don't do such value operations.

[sim642]

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 merge from MapDomain interface, making it much harder to carelessly introduce similar bottlenecks.

[Copilot]

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 merge from the MapDomain interface and introduces difference plus *_inter_filter operations to express common patterns more directly.
• Adds “lifted” Patricia-based MapDomain functors (PatriciaMapBot_LiftTop, PatriciaMapTop_LiftBot) and uses them in several analyses/domains.
• Extends CilType.Fundec and CilType.Stmt with tag so they can be used as patricia-tree keys.

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.