One Patricia tree library for four analysis tools

Outcome

CEA List's analysis tools now draw on a shared Patricia tree library rather than on variants maintained separately inside each project.

Six changes were merged upstream into patricia-tree: two new map operations, nonidempotent_union and nonidempotent_inter_filter_no_share; a correctness fix so that nonreflexive_same_domain_for_all2 returns the right answer for empty trees; a benchmark suite; model-based testing with QCheck; and coverage instrumentation through bisect_ppx. The changes reached Frama-C and Colibri2 through merge requests on CEA List's own infrastructure.

CEA List validated the work in a closing meeting. The performance regressions found along the way were resolved, and the small differences that remain follow from a library choice on their side rather than from the consolidation.

The project was funded by CEA-List.

Approach

The engagement began with review rather than code. Which Patricia tree variants did each project actually use, and in what respects did they differ: endianness, sharing, hashconsing, heterogeneous keys? Which functions were genuinely called, as opposed to merely defined? And what did the wider OCaml ecosystem already provide?

Only then came a proposed interface and a decision about where the shared code should live. Implementation followed, with benchmarks and tests built alongside it, and finally the conversion of existing projects.

Testing mattered more than usual here. These structures sit at the centre of tools whose results must not change unexpectedly, so the work added QCheck model-based tests and coverage instrumentation, making it possible to compare behaviour against a reference rather than trusting a reading of the code.

Tarides worked in CEA List's repositories and review processes throughout, and the library changes were made in public.

Challenge

At CEA List, the Laboratory for Software Safety and Security develops Frama-C, the Colibri2 solver, the Codex abstract interpreter and the Binsec binary analyser. All four analyse critical software, where a wrong answer is expensive.

Each had grown its own Patricia trees, extended over years to fit the project in front of it. That duplication costs maintenance, and it means an improvement made in one tool does not reach the others.

Consolidation is easy to propose and hard to do. These data structures are on the hot path of every analysis, so the shared version has to be at least as fast as each of the variants it replaces, while preserving behaviour exactly.