From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 780447EE35 for ; Mon, 2 May 2016 16:30:55 +0200 (CEST) IronPort-PHdr: 9a23:g2p/dRVpM9BsMoBWWWbg+kYpIbLV8LGtZVwlr6E/grcLSJyIuqrYZxCOt8tkgFKBZ4jH8fUM07OQ6PCwHz1Zqsnd+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq82VMlwD22b1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHj20+2AEX24Kvh1NCgnDpFGmD9ai+hf949H80iCBIcz7S4cUWDKu4r1mUle8syoNPiUl8WzRzOxxiq5Wuh+7jx152Y/dJo+PYr42darYeZsHXmdbRY4FXCVEBsa4bpATJ+sHJ+dR6Yfn8Qggtxy7UCalDvnuxzsAvXT20Lc3yax1HgjMxg0tG5QVu3TZttjvHKgXWOGxiqLPyGOQPLttxT7h5d2QIVgaqvaWUOc1LJPc Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-io0-f171.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.223.171 as permitted sender) identity=mailfrom; client-ip=209.85.223.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-io0-f171.google.com) identity=helo; client-ip=209.85.223.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-io0-f171.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0COAAACZCdXiKvfVdFdFoNANXcGBqc7gVGFXYsHAQ2BdiKFbgKBJAc4FAEBAQEBAQEBEQEBAQgLCwkfMYItghUBAQQSER0BGxIMAwwGBQsNAgIJHQICIgERAQUBChIGARIICgkHh3IBAxIJBZtDgTE+MYs7gWqCV4ZjChknAwpRg30BAQEBBgEBAQEBAQETAQUKBW2FJYRMhAQ5gwCCVgEEhjYMkVKBVYQniByBZ06HKIU0RYcghg4SHoEOHgEBgjoegXEgMAEBiQUBAQE X-IPAS-Result: A0COAAACZCdXiKvfVdFdFoNANXcGBqc7gVGFXYsHAQ2BdiKFbgKBJAc4FAEBAQEBAQEBEQEBAQgLCwkfMYItghUBAQQSER0BGxIMAwwGBQsNAgIJHQICIgERAQUBChIGARIICgkHh3IBAxIJBZtDgTE+MYs7gWqCV4ZjChknAwpRg30BAQEBBgEBAQEBAQETAQUKBW2FJYRMhAQ5gwCCVgEEhjYMkVKBVYQniByBZ06HKIU0RYcghg4SHoEOHgEBgjoegXEgMAEBiQUBAQE X-IronPort-AV: E=Sophos;i="5.24,567,1454972400"; d="scan'208";a="216645136" Received: from mail-io0-f171.google.com ([209.85.223.171]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 02 May 2016 16:30:54 +0200 Received: by mail-io0-f171.google.com with SMTP id f89so168933576ioi.0; Mon, 02 May 2016 07:30:54 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :content-transfer-encoding; bh=tZl/o2SBOkOKTBuz9XRpJ7pBr44qChhGYL/7ePePj2o=; b=Qjg6OdN9YIoMLDgx5Y8Erk1ztXfrybMormm2ehnlTB/YhrYYUYvNAmQLIhtCJvgu05 ydqXGuj+AhoKnTsUw1Otyce5ejfYoWJ2embBLEbH3NChAPFHz7gAI4CQZeF92P0Ovvyi PMaBSNN6lWlI68bmpLO5vwtPg6FqRkbe24+NNXluFPGKdQAUFqj9knmEX//oRTZT8rZE xHVJ0Hn6J9/WDeEag7sxTTM3Y/xc8nKeE8XTFe10cbZBLTgoNGkmH0948qhB4gUNIU16 ljraK2Je+EGEf46TdrfxjxMPOFUMiKu15XM1oxhybLnj07W6oOYT0L2HWsuvJ792+92A Wr4w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:content-transfer-encoding; bh=tZl/o2SBOkOKTBuz9XRpJ7pBr44qChhGYL/7ePePj2o=; b=EousO+9+fjB8S9dVGLChGFKyTFyK/PdaA9zaCH/TlQSRoiDhQyPX7Xt92Ds+zSWEVA /62p5hIOp2WFvdTTpjC/Kg73op+BRJkdL8KrrTxbZgPmsmR9hP9gpUR4LZqqOmnOf6Ou 65BrQ4yEhsQLAMJeEaamSdgxLcF+J5F1MvD5zq88zXQxTQBRDl6ZI+skVfF2+sgg3kuq v5NwFbmZJN63Uhd4iraanBtnj5LYq3USeV40WZQayWU9kAFk8IemXbXKxY1t2y9R7XiE hJLRVAE+7IjoRi8bhA4m5BYCdoXwLfXyks6kqMmjBAcKaHDPB0U/RgniiFiRMkUKALc1 K//w== X-Gm-Message-State: AOPr4FVwyXPdZ6YbEadbL3aFesjeM8nc4St8R1RUe0u1ikRNn7zkqJn8Z70EPDK6CkLJZqfcxnGQwc0vs8iXIQ== X-Received: by 10.107.169.13 with SMTP id s13mr37872584ioe.19.1462199452980; Mon, 02 May 2016 07:30:52 -0700 (PDT) MIME-Version: 1.0 Received: by 10.79.89.195 with HTTP; Mon, 2 May 2016 07:30:13 -0700 (PDT) In-Reply-To: <20160502082756.GC1971@pl-59055.rocqadm.inria.fr> References: <1461935860.9915.100.camel@e130.lan.sumadev.de> <5630123afc948279fc61d5e4c35d9014@in.tum.de> <1461939917.9915.110.camel@e130.lan.sumadev.de> <20160502082756.GC1971@pl-59055.rocqadm.inria.fr> From: Gabriel Scherer Date: Mon, 2 May 2016 10:30:13 -0400 Message-ID: To: =?UTF-8?Q?S=C3=A9bastien_Hinderer?= , caml users Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption? 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=C3=A9bastien Hinderer wrote: > Hi, > > Gerd Stolpmann (2016/04/29 16:25 +0200): >> Am Freitag, den 29.04.2016, 16:14 +0200 schrieb Markus Wei=C3=9Fmann: >> > 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=C3=A9bastien. > > -- > 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