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 9A63D5D5 for ; Fri, 12 Jul 2019 18:58:56 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.63,483,1557180000"; d="scan'208";a="391637588" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 12 Jul 2019 20:58:55 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 7EA257ED69; Fri, 12 Jul 2019 20:58:55 +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 6F5427ED69 for ; Fri, 12 Jul 2019 19:44:32 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=monnier@iro.umontreal.ca; spf=Pass smtp.mailfrom=monnier@iro.umontreal.ca; spf=None smtp.helo=postmaster@mailscanner.iro.umontreal.ca IronPort-PHdr: =?us-ascii?q?9a23=3AytC1HRfGmeGSe0VvrjSpixbjlGMj4u6mDksu8pMi?= =?us-ascii?q?zoh2WeGdxcW+ZR7h7PlgxGXEQZ/co6odzbaP6ea9ASdZuM/JmUtBWaQEbwUCh8?= =?us-ascii?q?QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6?= =?us-ascii?q?OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MQu6oR/Ru8UKjoduN7s9xgbUqXZUZu?= =?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?zUotvrKakcUu61wqfKwjrNYPxZxTjz5ZPUchA4u/yAQa58fNDTxEQpCgjLjk+Q?= =?us-ascii?q?qYvgPz6Ny+oNr3aU7+R6WuKplmUprAZxoj6pxsctlIbJnJ8ex1fB9SV+xoY1I9?= =?us-ascii?q?y4R1BhYdO/EZtQrSaaO5FrQsMnRGFovjo6yqcYtpGheCgG0ogoyATGZvGBboOG?= =?us-ascii?q?7BXjVOOLLjd5gnJoYL2/hxeu8Uig1+3zTdO40FdNriZdjtbMrGoC1xrI6sSdTf?= =?us-ascii?q?t95Eih1DCS3A7Q8uFJOV04mKTFJ5I73LI8ipUevV7dEiL2gkn7jLOael059uS0?= =?us-ascii?q?5OnreKvqqoGCO4Nulw3yLKojltahDegmNgUDWXWQ9/6m273550L5Ra1Hjv0ona?= =?us-ascii?q?ndt5DXPcEbqbS4Aw9RyYYs9wywDzGg0NsGh3kLNlNFeAiAj4TzJlHOJff4DfGj?= =?us-ascii?q?g1S2jjhk3fTGMqf9DZrXNnTDkbHhcqhh60NE1QY+w85T64hKBr0dL///QFH9ud?= =?us-ascii?q?zCAhI5LwC42+PnB8981oMaV2KPGKiZMKbKvF+N4eIvJe+MZI4LtzbnMPUl5uTu?= =?us-ascii?q?jXgjlV8AeKmp2p0XaGyiHvt4OUqZZWDgjcsbHmsSpAoxUPTqiEGeUT5Uf3u9Q7?= =?us-ascii?q?gz5jQ/CI6/CYfDR5utgKCa0SegHpxWY3hGBUqWHXfpcYWEQfYMZziILs9viDxX?= =?us-ascii?q?HYSmHqAo3wuvuQuy8LFnI/DZ4GVMupvpztl446vInhE/7zFuJ8uY2mCJCWpzmz?= =?us-ascii?q?VbaSUx2fVEvUFzw1HL9K9+hf1VD5QH4vRPVAY3L7bd1es8FtX1XB7bc96NDl2v?= =?us-ascii?q?FIb1SQotR848loddK312HM+v21WehnP7UY9QrKSCAdkPyoyZ2nHwI8hnzHOfhP?= =?us-ascii?q?sglV5gX85IM3G8i6d7sQPaVdeQzxep0p2yfKFZ5xbjsX+ZxDPe7kBCV0htVKLD?= =?us-ascii?q?QWoSb0+Qpt2rvhqfHY/rMqwuN0568eDHKqZObYax31BPRfP4M93YZW+r3WaqAl?= =?us-ascii?q?CVw7SKcJDncmFb1yyPUEU=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BkAACXxShdhzIZzIRlGwEBAQEDAQEBB?= =?us-ascii?q?wMBAQGBZ4MBgQQohByIe4t2mh4DVAkBAwEMJQgCAQGEQAKCVhsHAQQ0EwEDAQE?= =?us-ascii?q?EAQECAQIDARMBAQEKCwkIKYVDDII6KYJnAQEBAQIBIx0BATcBBAsLGAICJgICF?= =?us-ascii?q?CghE4MiAYF7Dw+rP3GBMoJ5AQEFhzEDBiJqKIpCgR0XgX+EIz6CYQIBgR9Bgwq?= =?us-ascii?q?CWIwiMZ4TCYIbgh+EOY1OmAeUepAvgWeBeTMaCDA7gmyCQQsPCYJ6gziCMIVbI?= =?us-ascii?q?wEBMQEBgQEmEwsBjyIBAQ?= X-IPAS-Result: =?us-ascii?q?A0BkAACXxShdhzIZzIRlGwEBAQEDAQEBBwMBAQGBZ4MBgQQ?= =?us-ascii?q?ohByIe4t2mh4DVAkBAwEMJQgCAQGEQAKCVhsHAQQ0EwEDAQEEAQECAQIDARMBA?= =?us-ascii?q?QEKCwkIKYVDDII6KYJnAQEBAQIBIx0BATcBBAsLGAICJgICFCghE4MiAYF7Dw+?= =?us-ascii?q?rP3GBMoJ5AQEFhzEDBiJqKIpCgR0XgX+EIz6CYQIBgR9BgwqCWIwiMZ4TCYIbg?= =?us-ascii?q?h+EOY1OmAeUepAvgWeBeTMaCDA7gmyCQQsPCYJ6gziCMIVbIwEBMQEBgQEmEws?= =?us-ascii?q?BjyIBAQ?= X-IronPort-AV: E=Sophos;i="5.63,483,1557180000"; d="scan'208";a="313359624" X-MGA-submission: =?us-ascii?q?MDGLDAQxQDrgfPvmpnrfkVqqMvEXP7TV113hFp?= =?us-ascii?q?y8q+oW+8nDtmrWBh5Ej5/9CzrqvhfrP4Dm1xvQHaAiV1hI/hjXQqoOlL?= =?us-ascii?q?yEcnAkRAqQZ4zCcGbDPtEt7L/mfwo8y7mgB00jWh2pDCzIb5ggKvEMp/?= =?us-ascii?q?rP/fwaV62NNtpWC9DHqRJU9w=3D=3D?= Received: from mailscanner.iro.umontreal.ca ([132.204.25.50]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 12 Jul 2019 19:44:30 +0200 Received: from pmg1.iro.umontreal.ca (localhost.localdomain [127.0.0.1]) by pmg1.iro.umontreal.ca (Proxmox) with ESMTP id BE59E1006CE; Fri, 12 Jul 2019 13:44:26 -0400 (EDT) Received: from mail01.iro.umontreal.ca (unknown [172.31.2.1]) by pmg1.iro.umontreal.ca (Proxmox) with ESMTP id 9DFC1100641; Fri, 12 Jul 2019 13:44:23 -0400 (EDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=iro.umontreal.ca; s=mail; t=1562953463; bh=XshcHcIhUHM3lzDWYDU0fJc+kR0EdjmRQAjFvcaP1mQ=; h=From:To:Cc:Subject:References:Date:In-Reply-To:From; b=S07/mXpRHLafwaD1oAlVrF3+Sn92i+6FRc2kwJKV3QN6qb6u9pTzNU0ok5t3uYKs9 hUK+BcnzdkE2IfenEJVNXj6tVcoZIl1Ph6WYEvb3Vs0V+a24gPzz2i2kiVGODDWX8Q Y0wdZvTn/F5b9ZPOc/AiG8FhSAxYKWVuyL2pTAHMTfc5KyZX20MKwC/oG/FnDTOTyD T1Z1I07fKkqGl6KATVRk2XDEEa5kUR1ISextsxQ0TGZ/JzDguRFZ0FWOtNdQWNRVEl pDZa+sEJWyglHmY48cNuwzeaW8HdQa5VbTvAjaeyosAqa3PJUKHTsBEwmwbKupblpG WtQDK7ZMFeOIQ== Received: from pastel (104-222-123-229.cpe.teksavvy.com [104.222.123.229]) by mail01.iro.umontreal.ca (Postfix) with ESMTPSA id 5CCBD12096F; Fri, 12 Jul 2019 13:44:23 -0400 (EDT) From: Stefan Monnier To: Gabriel Scherer Cc: Glen =?windows-1252?Q?M=E9vel?= , caml users Message-ID: References: <10c67553-1e80-6dea-9ef8-13486746672d@crans.org> Date: Fri, 12 Jul 2019 13:44:22 -0400 In-Reply-To: (Gabriel Scherer's message of "Thu, 11 Jul 2019 08:44:11 +0200") User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.0.50 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-SPAM-INFO: Spam detection results: 0 ALL_TRUSTED -1 Passed through trusted hosts only via SMTP AWL 0.542 Adjusted score from AWL reputation of From: address BAYES_00 -1.9 Bayes spam probability is 0 to 1% DKIM_SIGNED 0.1 Message has a DKIM or DK signature, not necessarily valid DKIM_VALID -0.1 Message has at least one valid DKIM or DK signature DKIM_VALID_AU -0.1 Message has a valid DKIM or DK signature from author's domain X-SPAM-LEVEL: X-Validation-by: monnier@iro.umontreal.ca Subject: Re: [Caml-list] overflow checks on `int` operations Reply-To: Stefan Monnier X-Loop: caml-list@inria.fr X-Sequence: 17684 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: Thanks Gabriel and Glen, Not sure how I missed the version that's in Batteries, Stefan Gabriel Scherer [2019-07-11 08:44:11] wrote: > 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= 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: > > > https://ocaml-batteries-team.github.io/batteries-included/hdoc2/BatInt.Sa= fe_int.html > > On Thu, Jul 11, 2019 at 1:06 AM Glen M=C3=A9vel wr= ote: > >> 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 i= ntegers 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 wit= h. >> >> 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 overflowi= ng >> 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 >> >>