From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id E19075D5 for ; Thu, 11 Jul 2019 06:43:35 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.63,476,1557180000"; d="scan'208,217";a="391354526" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 11 Jul 2019 08:43:34 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id C9AF3826CE; Thu, 11 Jul 2019 08:43:34 +0200 (CEST) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 58F757ED69 for ; Thu, 11 Jul 2019 08:43:28 +0200 (CEST) Authentication-Results: mail3-smtp-sop.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-yw1-f53.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AyUXQCxd03GEFNVyQQuYStyKXlGMj4u6mDksu8pMi?= =?us-ascii?q?zoh2WeGdxcW5ZR7h7PlgxGXEQZ/co6odzbaP6ea8BidZucnJmUtBWaQEbwUCh8?= =?us-ascii?q?QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6?= =?us-ascii?q?OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MQu6oR/eu8QUjoduN7o9xxnUqXZUZu?= =?us-ascii?q?pawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnF?= =?us-ascii?q?VguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hC?= =?us-ascii?q?oBKjU063/chNBug61HoRKhvx1/zJDSYIGJL/p1Y6fRccoHSWZdQspdUipMDYSh?= =?us-ascii?q?YYsSFOoBJfhXoJXhp1UAqhu+ABOjBOLpyjRVgnP70qk33+EnHArb3gIvAsgOvW?= =?us-ascii?q?zbo9X7NqgcUe67wqrVwzvdc/xbwi3y5JTSfx07vf2AQbB9fMzMwkcvDQPFiVCQ?= =?us-ascii?q?pJTkMTyPzesNqWmb4PRkVemylmAotwFxrSa1xsgykInCm4UYyl/e+ipi2oY1JM?= =?us-ascii?q?O3SEphbd6/DJRQtz+VN5FoTcM4WGxotyM6xacHuZ6/ZiQF1JMnxxvGZvGBboOG?= =?us-ascii?q?7BXjVOOLLjd5gnJoYLe/hxep8Ue80OH8U8203E5FripEjtnMtm0N2AfJ5sSdS/?= =?us-ascii?q?t9+V+t2TmO1wDP6uFEPFs7mbDaK54m2rI/ioATvl7FHi/tgkn2i7WWdkoi9+O1?= =?us-ascii?q?6Orneq3rqoGAO4JwkA3zMaQjltaiDek5LwQCRWiW9Oq62bb+50P2Wq9Kgeczkq?= =?us-ascii?q?TBsJDVO8AbpqmhDg9QyIkj6hK/Ay6m0dUWgHULNVxFdRKJgoTzNFHOJ/f4Dfi7?= =?us-ascii?q?g1uyijtk2/fGPrj5DpXMKHjMjqvhcK5j50JAzAc/19NS6pJOBr0cIf//R1X9ud?= =?us-ascii?q?zWAxMhNgy72efnCNFz1oMEXmKPB7eUMKzIvlCT/OIvIveDZIsPtDbmN/cl5+Dh?= =?us-ascii?q?jWUnll8HZqSp0p4XZ2q5HvRiOUmWfX3sgtIZHWcQogU+VPDqiEGFUTNLe3m9Ra?= =?us-ascii?q?c85jUiBIKiDIfDXZytjaea3Ca7G51WfnpJBkqNEXfubYWEWu0DZDicIs97wXQ4?= =?us-ascii?q?Uu2OT4In4jQvqgL+g+5oKufSvCgVq5/n/NNv7uvI0xYo+monId6a1jSiRmtun2?= =?us-ascii?q?4MDwQ93K1lrFY1nliK27J5jvgeDtdT6ulESC81MJfdy6pxDNWkCVGJRcuAVFvz?= =?us-ascii?q?GobuOjo2VN9khoJXOhsvK5CZlhnGmhGSLfoVmriMXsFm96vd2z3gOJ84xSudkq?= =?us-ascii?q?YmiFYiT41EMmj03vcjpTiWPJbAlgCir4jvbb4VhXef+2KKzG7It0ZdAlYpAPf1?= =?us-ascii?q?GEsHb06TluzXo0bLTrugE7Mia1ITxsuLK68MYdrs3wxL?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AcAgDu2SZdhzWhVdFlHgEGBwaBZ4I/Q?= =?us-ascii?q?lEzKIQcgR1CghyOYYIPilSIIYcmA1QJAQMBDCUKAQGDCYE3AoJOGwcBBDQTAQM?= =?us-ascii?q?BAQQBAQIBAgMBEwEBAQgNCQgphUMMgjopgmgBBAEjHQEbHQEDAQsGBQs3AgIiA?= =?us-ascii?q?REBBQEcBhODIgGBaQEDDg8PoSQ8iyGBFQUBF4J6BYQ6ChknDV8DgTsCBxKBIot?= =?us-ascii?q?fgVc/hCM+gmECAYEfboJdglgEjBgxng0HAoIbXQSFd40wG4MZlGiUcpAZDyGBR?= =?us-ascii?q?oF5MxojUDGCOwmCOAsPCYNOgmSBPHSFQUAwAQGPVQEB?= X-IPAS-Result: =?us-ascii?q?A0AcAgDu2SZdhzWhVdFlHgEGBwaBZ4I/QlEzKIQcgR1Cghy?= =?us-ascii?q?OYYIPilSIIYcmA1QJAQMBDCUKAQGDCYE3AoJOGwcBBDQTAQMBAQQBAQIBAgMBE?= =?us-ascii?q?wEBAQgNCQgphUMMgjopgmgBBAEjHQEbHQEDAQsGBQs3AgIiAREBBQEcBhODIgG?= =?us-ascii?q?BaQEDDg8PoSQ8iyGBFQUBF4J6BYQ6ChknDV8DgTsCBxKBIotfgVc/hCM+gmECA?= =?us-ascii?q?YEfboJdglgEjBgxng0HAoIbXQSFd40wG4MZlGiUcpAZDyGBRoF5MxojUDGCOwm?= =?us-ascii?q?COAsPCYNOgmSBPHSFQUAwAQGPVQEB?= X-IronPort-AV: E=Sophos;i="5.63,476,1557180000"; d="scan'208,217";a="313139865" X-MGA-submission: =?us-ascii?q?MDHXEnyhgZ3+io+XCjckQKFcBOPpXfRtEpE5Qa?= =?us-ascii?q?dLLJuko4VnBK5GtJjO3nZVrMeg7Rb7OXfl6IgAwD4cgZ9c5x4KsnVzA+?= =?us-ascii?q?uuvLYXnj9VUvum/EYbRE2Nkn6Il/R59P2nRlHUZOc+cBgPLztqfC7nzX?= =?us-ascii?q?hF8+9+bAlTaHnpGfh11hf7rQ=3D=3D?= Received: from mail-yw1-f53.google.com ([209.85.161.53]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 11 Jul 2019 08:43:26 +0200 Received: by mail-yw1-f53.google.com with SMTP id m16so1979617ywh.12 for ; Wed, 10 Jul 2019 23:43:26 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=8YO5xfT6b3rRwbf+GLpHaeMHavYJnCkfGfTgdq62uSU=; b=ENBPZ+i/FZxheBGBBL3F2FL7R2FflYHyL1/2rhCIeRd2ouXf39JZarJ9abra2PvLXr 8S1mjM+iUWq9mlkX8cnOCwv3gFbE+HG75l4EO1jhFuqVlN28dsTzD7ZrreDwSkaIBNi1 PyeYufjW9vJA09G4yD1cqGx3OUrFlYEsM54pALiRjfsFkgXTPqb0+hKLQSt9gSOq/loV iOtY5Zrt3aGOqebP7L/0lvAqj2StgCtow3pKWtCj0cUYYAlE4Ju56oJf7KxAdpsNodvo onbtpBB+lKhWDM+rEsrh2/+1vls86ReIiVe35IF3NUn+iO6DoGb0AV+I7v7xg3MSs6rL BVcA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=8YO5xfT6b3rRwbf+GLpHaeMHavYJnCkfGfTgdq62uSU=; b=WyCoWg5KcCQ1kXZ2nKG58H3GHRJL97GR0to/IQQD5YflNS6OmNq2IPznFOLaavSnER fMk+0JQFq33NiXXnc5SA/6p5UGVcgCDsMtG6WzE50PrAtgfdq5Dq+yHdB8Jd6Pljq2sT FSfKI3fpDSdLol8MjzKWgfE5UUbUHRS/ybWMPQkADkt2jcvBxlitoaf10aorXyjPD3T/ +GtqQw3oW8rp8J4sofUK/n6tduz2cFzPHrU5U5Hus0H5ZRmWdxvdSF7Mq1omDBNA7nDy WvEeqBJ8g7kRRPHOnHLiBVOWuyRT377or+4sKpg3RJ8zCL7ZTvc386b4SczeCxwz4WYA ZTiQ== X-Gm-Message-State: APjAAAUsDNPFirYoD4WLXoLklVhv0dh1XvxeGY+Vv8aQkeYzdEQl/1zC TFzE97VI7mRsqSbfPP3Zs1RZJkl/WBuXYIYbbek= X-Google-Smtp-Source: APXvYqxdc0eqN8gFdb5Z3n0pEz969nYYSb5MR9/9diJsqiyGkfkPPbYyLUfz51qbUoV5lhX2mmoJroBBSI3z1VA0Dso= X-Received: by 2002:a37:7604:: with SMTP id r4mr1502021qkc.395.1562827405238; Wed, 10 Jul 2019 23:43:25 -0700 (PDT) MIME-Version: 1.0 References: <10c67553-1e80-6dea-9ef8-13486746672d@crans.org> In-Reply-To: <10c67553-1e80-6dea-9ef8-13486746672d@crans.org> From: Gabriel Scherer Date: Thu, 11 Jul 2019 08:44:11 +0200 Message-ID: To: =?UTF-8?Q?Glen_M=C3=A9vel?= Cc: caml users , Stefan Monnier Content-Type: multipart/alternative; boundary="00000000000055a72d058d621c33" Subject: Re: [Caml-list] overflow checks on `int` operations Reply-To: Gabriel Scherer X-Loop: caml-list@inria.fr X-Sequence: 17681 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --00000000000055a72d058d621c33 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable The compiler has defined predicates (in utils/misc.ml) that test whether the operation would overflow on the given inputs. let no_overflow_add a b =3D (a lxor b) lor (a lxor (lnot (a+b))) < 0 let no_overflow_sub a b =3D (a lxor (lnot b)) lor (b lxor (a-b)) < 0 (* Taken from Hacker's Delight, chapter "Overflow Detection" *) let no_overflow_mul a b =3D not ((a =3D min_int && b < 0) || (b <> 0 && (a * b) / b <> a)) let no_overflow_lsl a k =3D 0 <=3D k && k < Sys.word_size && min_int asr k <=3D a && a <=3D max_int a= sr k Batteries exposes functions similar in spirit to Glen's Arith module (they raise an exception on overflow) as part of the Int.SafeInt module: https://ocaml-batteries-team.github.io/batteries-included/hdoc2/BatInt.Safe= _int.html On Thu, Jul 11, 2019 at 1:06 AM Glen M=C3=A9vel wrot= e: > Stefan Monnier wrote (2019-07-10 22:36): > > What's the "standard" way to perform arithmetic operations on `int` > > with overflow checking (e.g. returning an `Option` or signaling an > > exception on overflow)? > I don=E2=80=99t know whether there is a =E2=80=9Cstandard=E2=80=9D for in= tegers specifically, > but the rationale for option vs. exception is the following: exceptions > are used for behaviours that are not meant to happen, (ie. program > errors), whereas options are used for the normal course of a program. > For instance, depending on your application, the fact that an element is > unbound in a hash table may be an expected fact that should be dealt with= . > > In this case, I would advocate for exceptions, because an overflow is > clearly a failure of the program: the bounds on native integers are only > related to the internals of the OCaml runtime, thus it is very unlikely > to have any meaning in your application. It is also likely that you may > not work around an overflow, except by running the same computation with > zarith. If you expect overflows with int, maybe you should use zarith. > > Throwing an exception allows you to interrupt your program and track > precisely where the overflow occurred (with the stack trace), either by > wrapping your whole computation in a single exception handler, or by > letting the runtime handle the exception. > > With options, by contrast, either you would write an option handler > around each problematic operation, or you would propagate the option, > which implies (1) rewriting your whole computation in a monadic style > and (2) losing the provenance of a None. And you would pay a penalty for > boxing your integers. > > > Currently I do the checks by hand but it occurred to me that maybe I'm > > not the first one to want that. > > You=E2=80=99re not indeed. For my own needs, I wrote carefully overflowin= g > versions of some usual arithmetic functions[1]. But more serious > projects may be available, I guess. > > [1]: > https://gitlab.crans.org/mevel/project-euler-lib/blob/master/Arith.mli > > -- > Glen M=C3=A9vel > > --00000000000055a72d058d621c33 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
The compiler has defined predicates (in utils/misc.ml) that test whether the operation would over= flow on the given inputs.

let no_overflow_add a b =3D (a lxor b) lor (a lxo= r (lnot (a+b))) < 0

let no_overflow_sub a b =3D (a lxor (lnot b))= lor (b lxor (a-b)) < 0

(* Taken from Hacker's Delight, chapt= er "Overflow Detection" *)
let no_overflow_mul a b =3D
=C2= =A0 not ((a =3D min_int && b < 0) || (b <> 0 && (a= * b) / b <> a))

let no_overflow_lsl a k =3D
=C2=A0 0 <= =3D k && k < Sys.word_size && min_int asr k <=3D a &a= mp;& a <=3D max_int asr k

Batteries = exposes functions similar in spirit to Glen's Arith module (they raise = an exception on overflow) as part of the Int.SafeInt module:

=

On Thu, Jul 11, = 2019 at 1:06 AM Glen M=C3=A9vel <glen.mevel@crans.org> wrote:
Stefan Monnier wrote (2019-07-10 22:36):
> What's the "standard" way to perform arithmetic operatio= ns on `int`
> with overflow checking (e.g. returning an `Option` or signaling an
> exception on overflow)?
I don=E2=80=99t know whether there is a =E2=80=9Cstandard=E2=80=9D for inte= gers specifically,
but the rationale for option vs. exception is the following: exceptions
are used for behaviours that are not meant to happen, (ie. program
errors), whereas options are used for the normal course of a program.
For instance, depending on your application, the fact that an element is unbound in a hash table may be an expected fact that should be dealt with.<= br>
In this case, I would advocate for exceptions, because an overflow is
clearly a failure of the program: the bounds on native integers are only related to the internals of the OCaml runtime, thus it is very unlikely
to have any meaning in your application. It is also likely that you may
not work around an overflow, except by running the same computation with zarith. If you expect overflows with int, maybe you should use zarith.

Throwing an exception allows you to interrupt your program and track
precisely where the overflow occurred (with the stack trace), either by
wrapping your whole computation in a single exception handler, or by
letting the runtime handle the exception.

With options, by contrast, either you would write an option handler
around each problematic operation, or you would propagate the option,
which implies (1) rewriting your whole computation in a monadic style
and (2) losing the provenance of a None. And you would pay a penalty for boxing your integers.

> Currently I do the checks by hand but it occurred to me that maybe I&#= 39;m
> not the first one to want that.

You=E2=80=99re not indeed. For my own needs, I wrote carefully overflowing<= br> versions of some usual arithmetic functions[1]. But more serious
projects may be available, I guess.

[1]: https://gitlab.crans.org/= mevel/project-euler-lib/blob/master/Arith.mli

--
Glen M=C3=A9vel

--00000000000055a72d058d621c33--