Re: [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption?

[Gabriel Scherer <gabriel.scherer@gmail.com>]

In 2006 there was work on a static analysis tool to check OCaml C
stubs called "Saffire", which you can read about in detail here:
  http://www.cs.umd.edu/~jfoster/papers/cs-tr-4845.html

Adrien Nader extracted the implementation and loaded it on the OCaml
Forge in 2012, anyone interested in fixing/updating the project should
probably get in touch with him:
  https://forge.ocamlcore.org/projects/saffire/

I have always been curious about how it would fare on the C bindings
in the wild -- my guess is that it may have bitrotten a bit but that
it would find a few issues, and also be very helpful during the
development phase (where you iteratively hunt for segfaults), if it
was an "opam install" away and easy to run.

I have been trying to motivate the Frama-C people to find an excellent
intern to write a specification of the OCaml memory model in ACSL
(their specification language for C, http://frama-c.com/acsl.html );
the dream is that one may then be able to use Frama-C to check for
safety of the C stubs, and even possibly verify some parts of the C
codebase in the compiler distribution (probably not the runtime
implementation itself, which precisely breaks the abstraction of the
memory model, but at least large parts of C implementation of
primitives, otherlibs/, etc.). I think they are interested as well,
but I'm not sure they have found the time and people to work on this.

Finally, note that Jeremy Yallop's Ctypes (
https://github.com/ocamllabs/ocaml-ctypes ) may be the better solution
to write correct C bindings. I think that it is complementary with the
above-mentioned efforts:
- Saffire could be used to check legacy C stubs, of which there are many
- A more precise model of the OCaml value representation and exposed
runtime interface could help verify Ctypes itself and other future
projects interacting with the runtime at a lower level.

Ctypes is slightly more restricted than general C stubs, but
substantially more safe (and more convenient). In my experience the
unsafety of C bindings is a huge time sink, so starting with a Ctypes
binding is almost certainly the most productive choice.

On Mon, May 2, 2016 at 4:27 AM, Sébastien Hinderer
<Sebastien.Hinderer@inria.fr> wrote:
> Hi,
>
> Gerd Stolpmann (2016/04/29 16:25 +0200):
>> Am Freitag, den 29.04.2016, 16:14 +0200 schrieb Markus Weißmann:
>> > The value comes from C bindings, but from a string-value via Char.code.
>> > It is then passed through a constructor-function to create the record;
>> > I added a check there to see if the C bindings are to blame:
>>
>> Well, there are other types of errors in C bindings that could also
>> cause this. Imagine what happens when the C bindings do not properly
>> handle pointers (e.g. do not declare them as local roots), and an
>> outdated pointer to an int is followed by the GC because of this.
>> Because the minor GC moves values to the major heap, this could cause
>> that the int is overwritten then.
>>
>> In my experience, it's always the C binding!
>>
>> Unfortunately, there's no code for investigations.
>
> Do you think there is room for improvement at this level?
>
> Do you already have a bit more precise ideas about the kind of tools that
> coould be helpful?
>
> Cheers,
>
> Sébastien.
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs