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

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:

quoted

On Wed, 17 Nov 2021, Prathamesh Kulkarni via Gcc-patches wrote:

quoted

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