From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 30D63C433EF for ; Mon, 6 Dec 2021 18:34:43 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S238059AbhLFSiL (ORCPT ); Mon, 6 Dec 2021 13:38:11 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:49424 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S237265AbhLFSiL (ORCPT ); Mon, 6 Dec 2021 13:38:11 -0500 Received: from mail-oi1-x22b.google.com (mail-oi1-x22b.google.com [IPv6:2607:f8b0:4864:20::22b]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 4DCE5C061746 for ; Mon, 6 Dec 2021 10:34:42 -0800 (PST) Received: by mail-oi1-x22b.google.com with SMTP id o4so23039753oia.10 for ; Mon, 06 Dec 2021 10:34:42 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding; bh=4njs70WndioRLu7tRoGylE37YzkRVdsiQD0VHDl2LxE=; b=pq08mwh+EAxGKzezk9NQeojj9s/ItyCRZAWSyJdSmYXjb4XDf+EECLiiiJd3E4EbpW Hq0ybQspFh6/PuPwHRe72qQNnmU9Di3Y3s2QLENsyUSBAGVtgX2GoeOszeDlyGGiKX/q aGhu1t0xBkSHA7F9AFq9o4sYl4Tl8n1AYXhy6eV4wOY1WQV6T9RPyT36R2gXx91fiO3j GcPUvs1ROXzUe3c1SXLSk6Xpmwljd38szMXucagClw0n7zT2n6/dO+wKiiwlwd58wNRa 4dwJWPMOLe269iyDRL+5T+ioHM0qKyShvz5V/pt/cJ8+Ji2hiD8AaNASdwGru3E3Z87i pDOg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:subject:to:cc:references:from:message-id:date :user-agent:mime-version:in-reply-to:content-language :content-transfer-encoding; bh=4njs70WndioRLu7tRoGylE37YzkRVdsiQD0VHDl2LxE=; b=tq3ZxxT8oIhwKcsaZyCExMbdwxJPOPd3NsL822RcGRRWVHrvHKA7q26UQdXYUdFtZ1 VzHc3KLT3A6fPCgtRU84JD/6jX9Xf9LT1JswKhZFTY8wamuXBM43G168eP2Ak0zRDNGm AjGauJmIij4bGZoP+RpVZQVhubRvblFLIplB+9YEe1eBmhAWu6w08J2Ax0yQxloUeGLP N/FCpGLW9vGNM8Oa7T9STF738jFoIrhJLYswZyr7fEG6a6MhBF0SyBC5jRpoMMCaKtkm k8KegrDSWjvL0fuyHl4+DCgqrX05sMpJRzxCpHikXXxHCeS7fhuqYOno5ZpICOB65qAd T/Eg== X-Gm-Message-State: AOAM533THZbEpJCPJGjrZ3jFDxMxhid71Q9HkBBJe/vcX64rYwz9vmxz RG48jbxzHbSAaETDNkHNNAZ5o1Pz0x4= X-Google-Smtp-Source: ABdhPJwT0WHfKuFNh+Cfyel+Fv/plljoywCnt3mUq0cfZgCYcHlxd5cBW4qOmcyrbNK1xuBYwTdeWQ== X-Received: by 2002:aca:b68a:: with SMTP id g132mr238906oif.139.1638815681454; Mon, 06 Dec 2021 10:34:41 -0800 (PST) Received: from [192.168.0.41] (184-96-227-137.hlrn.qwest.net. [184.96.227.137]) by smtp.gmail.com with ESMTPSA id a6sm2786687oic.39.2021.12.06.10.34.40 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 06 Dec 2021 10:34:41 -0800 (PST) Subject: Re: [PATCH 2/6] Add returns_zero_on_success/failure attributes To: David Malcolm , Joseph Myers , Prathamesh Kulkarni Cc: gcc-patches@gcc.gnu.org, linux-toolchains@vger.kernel.org References: <20211113203732.2098220-1-dmalcolm@redhat.com> <20211113203732.2098220-4-dmalcolm@redhat.com> <15adb3a2a70b0d2973c30dd6d7da383ad62f413a.camel@redhat.com> From: Martin Sebor Message-ID: Date: Mon, 6 Dec 2021 11:34:40 -0700 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.2.2 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-US Content-Transfer-Encoding: 8bit Precedence: bulk List-ID: X-Mailing-List: linux-toolchains@vger.kernel.org On 11/18/21 4:34 PM, David Malcolm via Gcc-patches wrote: > On Wed, 2021-11-17 at 22:43 +0000, Joseph Myers wrote: >> On Wed, 17 Nov 2021, Prathamesh Kulkarni via Gcc-patches wrote: >> >>> More generally, would it be a good idea to provide attributes for >>> mod/ref anaylsis ? >>> So sth like: >>> void foo(void) __attribute__((modifies(errno))); >>> which would state that foo modifies errno, but neither reads nor >>> modifies any other global var. >>> and >>> void bar(void) __attribute__((reads(errno))) >>> which would state that bar only reads errno, and doesn't modify or >>> read any other global var. >> >> Many math.h functions are const except for possibly setting errno, >> possibly raising floating-point exceptions (which might have other >> effects >> when using alternate exception handling) and possibly reading the >> rounding >> mode.  To represent that, it might be useful for such attributes to >> be >> able to describe state (such as the floating-point environment) that >> doesn't correspond to a C identifier.  (errno tends to be a macro, so >> referring to it as such in an attribute may be awkward as well.) >> >> (See also >> with >> some proposals for features to describe const/pure-like properties of >> functions.) >> > > Thanks for the link. > > As noted in my reply to Prathamesh, these ideas sound interesting, but > this thread seems to be entering scope creep - I don't need these ideas > to implement this patch kit (but I do need the attributes specified in > the patch, or similar). > > Do the specific attributes I posted sound reasonable? (without > necessarily going in to a full review). > > If we're thinking longer term, I want the ability to express that a > function can have multiple outcomes (e.g. "success" vs "failure" or > "found" vs "not found", etc), and it might be good to have a way to > attach attributes to those outcomes. Unfortunately the attribute > syntax is flat, but maybe there could be a two level hierarchy, > something like: > > int foo (args) > __attribute__((outcome("success") > __attribute__((return_value(0)))) > __attribute__((outcome("failure") > __attribute__((return_value_ne(0)) > __attribute__((modifies(errno))))); > > Or given that we're enamored by Lisp-ish DSLs we could go the whole hog > and have something like: > > int foo (args) > __attribute ((semantics( > "(def-outcomes (success (return-value (eq 0))" > " (failure (return-value (ne 0)" > " modifies (errno))))"))); > > which may be over-engineering things :) For a fully general solution, one that can express (nearly) arbitrarily complex pre-conditions and invariants, I'd look at the ideas in the C++ contracts papers. I don't know if any of the proposals (there were quite a few) made it possible to specify postconditions involving function return values, but I'd think that could be overcome by introducing some special token like __retval. Syntactically, one of the nice things about contracts that I hope should be possible to implement in our attributes is a way to refer to formal function arguments by name rather than by their position in the argument list. With that, the expressivity goes up dramatically because it becomes possible to use any C expression. Martin > Going back to the patch itself, returns_zero_on_success/failure get me > what I want to express for finding trust boundaries in the Linux > kernel, have obvious meaning to a programmer (helpful even w/o compiler > support), and could interoperate with one the more elaborate ideas in > this thread. > > Hope this is constructive > Dave > > > > >