Re: [PATCH 2/6] Add returns_zero_on_success/failure attributes

[Martin Sebor <msebor@gmail.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
> 
> 
> 
> 
>