Zarith

Perhaps you are looking for something to do pending the upcoming release of Frama-C (someone called it \Nitrozen" once by accident in a commit message. I would like the name to stick but I anticipate it won't)…

Or you are already a serious user of the value analysis plug-in or of one of the plug-ins that rely on it…

Or you might be in the near future…

Then this blog post is for you because this blog post is about Zarith that you should install.

Zarith is a multiprecision library for OCaml created by Antoine Miné. Zarith relies on GMP for the actual computations on big integers. Small integers and there lies Zarith's advantage over previous multiprecision libraries for OCaml use the same unboxed representation as OCaml's 31/63-bit integers. For computing on small integers if you are not using some exotic architecture Zarith uses the processor's instruction set most efficiently relying on the processor's flags to detect whether the result can itself be represented as an unboxed integer.

The bottom line is that a multiprecision operation (say a multiplication) is most of the times executed as the processor's corresponding instruction with a couple of conditional branches before and after for handling the uncommon cases and a couple of memory accesses and jumps (including a computed one) for the OCaml ↔ C interface. This may seem like a lot but it's much less than the other multiprecision libraries. And of course the unboxed representation saves space too as small integers do not have to be allocated at all and just reside in the word that would otherwise have been a pointer to their representation.

Benchmarks comparing Carbon and Nitrogen will come later; these will include the gains from switching from Big_int to Zarith. For minimal fuss Frama-C will continue to compile with Big_int (the multiprecision library provided as part of the OCaml distribution) and perhaps I will include "Nitrogen compiled with Big_int" in the benchmarks just to make the point.

Meanwhile if you plan to use the value analysis for more than ten minutes trust me install Zarith now. If you already knew about Zarith and had installed it a long time ago I suggest you upgrade to benefit from bugfixes and so that Frama-C Nitrogen's -save and -load options work.

[EDIT: deleted compilation instruction for obsolete Frama-C version]