OCaml DSL for specifying LibraryFunctions

[sim642]

This is an experiment to address #719 by designing an OCaml DSL, which allows specifying LibraryFunctions such that all the problems mentioned in the issue are avoided and all the goals are fulfilled.

The DSL implementation is a mixture of the following:

• So-called first-class patterns inspired by ppxlib's Ast_pattern: https://github.com/ocaml-ppx/ppxlib/blob/main/src/ast_pattern.ml. The three-type-parameter continuation-based internals of the patterns are hidden from actually specifying functions.
• A custom list-like type (using the standard list constructors to allow abusing normal OCaml list notation), but as a GADT to allow composing the first-class patterns in a type-safe manner. The GADT internals are hidden from actually specifying functions.
• A set of helper functions to construct such specifications in a readable way.

The DSL in LibraryDsl is just a convenient way to construct newly-introduced LibraryDesc objects, which combine the corresponding classify function, invalidate actions (with more precision) and other function-related attributes (e.g. being thread unsafe #723 or invalidating all globals).

The usage is (hopefully sufficiently) extensively documented both in the OCaml code and in the developer documentation.
The usage can be seen at the beginning of LibraryFunctions and LibraryDslTest.

TODO

• Document LibraryDesc.
• Document LibraryDsl.
• Implement shallow vs deep distinction in access analysis correctly. Function arguments are always directly read on call, but the access depth actually concerns MPT/reach. So there are actually three levels of access for reading function arguments.
• Fix new "Function definition missing" errors.
• Separate specifications lists:
  • C standard library
  • POSIX standard library
  • Pthread
  • Linux kernel
• Add selection for separate specifications lists. To be done in the future, when all old-style specifications have been ported.