Use Codex patricia-tree library for base map domain

[sim642]

Closes #1967.

During the AnalyzeThat 2026 workshop the Codex team told us that they have specifically published on opam the patricia-tree library which provides efficient merging with idempotent operators. This is an attempt to use it for the map domain in the base analysis.
I noticed that some part of Frama-C is also possibly switching to this library: https://git.frama-c.com/pub/frama-c/-/merge_requests/18.

Note that the library doesn't completely replace Stdlib.Map.Make: patricia-tree requires keys to have unique int values.
Luckily, base analysis map domain has varinfos which have vid, so it should work.
But we have plenty of other usages of MapDomain with more complex keys, so this PR tries to generalize MapDomain to allow both to be used.

Apparently this causes one test with int domain refinement and narrowing to fail again because the narrow is not idempotent.

TODO

• rsync benchmark.
• sv-benchmarks.
• Look through code TODOs.
• Figure out what to do with int domain refinement narrowing test. Using non-idempotent merging with meet and narrow due to possible int domain refinement issues for now.

[sim642]

For flow-sensitive analysis of rsync, this reduces the analysis time from ~9h 23min to ~7h 17min, which is about -22% (goblint/bench@7f22f21).

Around 20% of the time is still spent on GC. A lot of time is still spent in the inner join, etc. operations which can be optimized separately. My guess is that they haven't been written to carefully preserve physical equality but rather allocate new copies for identical arguments. The patricia-tree library exploits physical equality extensively for efficiency.

I'm now also doing a run on sv-benchmarks although I don't expect much change there.

[michael-schwarz]

I was confused about what Codex had to do with it, but then realized it's the Lemerre et al. Codex. For anyone also confused: https://codex.top/.

[sim642]

I'm now also doing a run on sv-benchmarks although I don't expect much change there.

There's a lot more than I expected. I did before vs after runs with level01 with 60s and 1GB. There's ~53 new trues: https://goblint.cs.ut.ee/results/328-all-level01-pr-2002-before/table-generator-cmp.diff.html#/table?filter=0(0*status*(status(notIn()),category(notIn()))),1(0*status*(status(notIn()),category(in(correct)))). Some are borderline noise flips, but some are due to significant differences.

CPU time

Average 9% improvement, up to 2×:

(https://goblint.cs.ut.ee/results/328-all-level01-pr-2002-before/table-generator-cmp.table.html#/scatter?toolX=0&columnX=2&toolY=1&columnY=2&filter=0(0*status*(status(notIn()),category(notIn(error)))),1(0*status*(status(notIn()),category(notIn(error))))&results=All&regression=Linear&scaling=Logarithmic&line=2)

Memory

Average 15% improvement, up to 3×:

(https://goblint.cs.ut.ee/results/328-all-level01-pr-2002-before/table-generator-cmp.table.html#/scatter?toolX=0&columnX=4&toolY=1&columnY=4&filter=0(0*status*(status(notIn()),category(notIn(error)))),1(0*status*(status(notIn()),category(notIn(error))))&results=All&regression=Linear&scaling=Logarithmic&line=3)

[michael-schwarz]

There's also one we lose that is unrelated to timing changes. Maybe worth taking a look, I guess this should behave exactly as the old one apart from runtime / memory concerns.

[sim642]

There's also one we lose that is unrelated to timing changes. Maybe worth taking a look, I guess this should behave exactly as the old one apart from runtime / memory concerns.

I also noticed that. It's from #1984 (comment).