cil-project / cil

C Intermediate Language
Other
348 stars 86 forks source link

Replace Num with ZArith for Cilint (for OCaml 4.06.0). #41

Open clegoues opened 6 years ago

clegoues commented 6 years ago

OCaml 4.06.0 pulls the Num module out of stdlib into its own separate project. Nominally it's possible to maintain backwards compatibility by simply installing the now-separate Num (opam!) and presumably tweaking package info to pull in the now-external dependency. But as far as I can tell, it's totally impossible to do this on a machine that's ever had any previous version of ocaml installed. It may not be possible to do it on a fresh install, either; I wouldn't know.

tl;dr: ocamlfind couldn't find the new Num. There seems to be a solution involving pinning ocamlfind back to some previous version (see: https://github.com/BinaryAnalysisPlatform/bap/issues/742), but that didn't work for me.

So. The recommendation is to use ZArith instead of Num anyway. Zarith is apparently a better, faster implementation of arbitrary-precision integers/rationals (https://github.com/ocaml/Zarith). Since building CIL with 4.06 involve adding an external dependency (to either Num or Zarith) and Num was giving me nightmares, I thought I'd try my hand at just replacing Num with Zarith and updating Cilint accordingly.

(TBH the rationale for continuing to wrap what-used-to-be-Bigint in Cilint isn't obvious to me, but that was a bigger refactor than I was willing to make without confirmation/blessing from the project owners/maintainers.)

Confirmed to build on 4.06+trunk, on Darwin and some arbitrary Ubuntu flavor (don't remember which one, I can check if you care), passes no fewer tests after than before.

Tricky bits: