linux-toolchains.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
From: Martin Sebor <msebor@gmail.com>
To: David Malcolm <dmalcolm@redhat.com>,
	Joseph Myers <joseph@codesourcery.com>,
	Prathamesh Kulkarni <prathamesh.kulkarni@linaro.org>
Cc: gcc-patches@gcc.gnu.org, linux-toolchains@vger.kernel.org
Subject: Re: [PATCH 2/6] Add returns_zero_on_success/failure attributes
Date: Mon, 6 Dec 2021 11:34:40 -0700	[thread overview]
Message-ID: <a6cb9482-4f68-e71b-c71f-78f6d9c1506d@gmail.com> (raw)
In-Reply-To: <fca23371db74968d4574b828b6b648978f77ef3f.camel@redhat.com>

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 <http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2825.htm>
>> 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
> 
> 
> 
> 
> 


  reply	other threads:[~2021-12-06 18:34 UTC|newest]

Thread overview: 39+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2021-11-13 20:37 [PATCH 0/6] RFC: adding support to GCC for detecting trust boundaries David Malcolm
2021-11-13 20:37 ` [PATCH 1a/6] RFC: Implement "#pragma GCC custom_address_space" David Malcolm
2021-11-13 20:37 ` [PATCH 1b/6] Add __attribute__((untrusted)) David Malcolm
2021-12-09 22:54   ` Martin Sebor
2022-01-06 15:10     ` David Malcolm
2022-01-06 18:59       ` Martin Sebor
2021-11-13 20:37 ` [PATCH 2/6] Add returns_zero_on_success/failure attributes David Malcolm
2021-11-15  7:03   ` Prathamesh Kulkarni
2021-11-15 14:45     ` Peter Zijlstra
2021-11-15 22:30       ` David Malcolm
2021-11-15 22:12     ` David Malcolm
2021-11-17  9:23       ` Prathamesh Kulkarni
2021-11-17 22:43         ` Joseph Myers
2021-11-18 20:08           ` Segher Boessenkool
2021-11-18 23:45             ` David Malcolm
2021-11-19 21:52               ` Segher Boessenkool
2021-11-18 23:34           ` David Malcolm
2021-12-06 18:34             ` Martin Sebor [this message]
2021-11-18 23:15         ` David Malcolm
2021-11-13 20:37 ` [PATCH 4a/6] analyzer: implement region::untrusted_p in terms of custom address spaces David Malcolm
2021-11-13 20:37 ` [PATCH 4b/6] analyzer: implement region::untrusted_p in terms of __attribute__((untrusted)) David Malcolm
2021-11-13 20:37 ` [PATCH 5/6] analyzer: use region::untrusted_p in taint detection David Malcolm
2021-11-13 20:37 ` [PATCH 6/6] Add __attribute__ ((tainted)) David Malcolm
2022-01-06 14:08   ` PING (C/C++): " David Malcolm
2022-01-10 21:36     ` PING^2 " David Malcolm
2022-01-12  4:36       ` Jason Merrill
2022-01-12 15:33         ` David Malcolm
2022-01-13 19:08           ` Jason Merrill
2022-01-14  1:25             ` [committed] Add __attribute__ ((tainted_args)) David Malcolm
2021-11-13 23:20 ` [PATCH 0/6] RFC: adding support to GCC for detecting trust boundaries Peter Zijlstra
2021-11-14  2:54   ` David Malcolm
2021-11-14 13:54 ` Miguel Ojeda
2021-12-06 18:12 ` Martin Sebor
2021-12-06 19:40   ` Segher Boessenkool
2021-12-09  0:06     ` David Malcolm
2021-12-09  0:41       ` Segher Boessenkool
2021-12-09 16:42     ` Martin Sebor
2021-12-09 23:40       ` Segher Boessenkool
2021-12-08 23:11   ` David Malcolm

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=a6cb9482-4f68-e71b-c71f-78f6d9c1506d@gmail.com \
    --to=msebor@gmail.com \
    --cc=dmalcolm@redhat.com \
    --cc=gcc-patches@gcc.gnu.org \
    --cc=joseph@codesourcery.com \
    --cc=linux-toolchains@vger.kernel.org \
    --cc=prathamesh.kulkarni@linaro.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).