public inbox for gcc@gcc.gnu.org
 help / color / mirror / Atom feed
From: Alex Colomar <alx.manpages@gmail.com>
To: "Uecker, Martin" <Martin.Uecker@med.uni-goettingen.de>,
	"matz@suse.de" <matz@suse.de>
Cc: "gcc@gcc.gnu.org" <gcc@gcc.gnu.org>,
	"linux-man@vger.kernel.org" <linux-man@vger.kernel.org>,
	"joseph@codesourcery.com" <joseph@codesourcery.com>,
	"schwarze@usta.de" <schwarze@usta.de>,
	"wg14@soasis.org" <wg14@soasis.org>
Subject: Re: [PATCH] Various pages: SYNOPSIS: Use VLA syntax in function parameters
Date: Tue, 29 Nov 2022 18:28:51 +0100	[thread overview]
Message-ID: <7697ff60-aa2a-a41e-9d08-ab25423ee750@gmail.com> (raw)
In-Reply-To: <6aa43dfb80210f62be70fd1fd076c72260423c38.camel@med.uni-goettingen.de>


[-- Attachment #1.1: Type: text/plain, Size: 6055 bytes --]

Hi Martin and Michael,

On 11/29/22 17:58, Uecker, Martin wrote:
> 
> Hi,
> 
> Am Dienstag, dem 29.11.2022 um 15:44 +0000 schrieb Michael Matz:
>> Hey,
>>
>> On Tue, 29 Nov 2022, Uecker, Martin wrote:
>>
>>> It does not require any changes on how arrays are represented.
>>>
>>> As part of VM-types the size becomes part of the type and this
>>> can be used for static or dynamic analysis, e.g. you can
>>> - today - get a run-time bounds violation with the sanitizer:
>>>
>>> void foo(int n, char (*buf)[n])
>>> {
>>>    (*buf)[n] = 1;
>>> }
>>
>> This can already statically analyzed as being wrong, no need for
>> dynamic checking.
> 
> In this toy example, but in general in can be checked
> only at run-time by using the information about the
> dynamic bound.
> 
>> What I mean is the checking of the claimed contract.
>> Above you assure for the function body that buf has n elements.
> 
> Yes.
> 
>> This is also a pre-condition for calling this function and
>> _that_ can't be checked in all  cases because:
>>
>>    void foo (int n, char (*buf)[n]) { (*buf)[n-1] = 1; }
>>    void callfoo(char * buf) { foo(10, buf); }
>>
>> buf doesn't have a known size.
> 
> This does not type check.
> 
>>   And a pre-condition that can't be checked
>> is no pre-condition at all, as only then it can become a guarantee
>> for the body.
> 
> The example above should look like:
> 
> void foo(int n, char (*buf)[n]);
> 
> void callfoo(char (*buf)[12]) { foo(10, buf); }
> 
> This could be checked by an UB sanitizer as calling
> the function with an argument of incompatible type
> is UB (but we currently do not do this)
> 
> 
> If you think about
> 
> void foo(int n, char buf[n]);
> 
> void callfoo(char *buf) { foo(10, buf); }
> 
> 
> Then you are right that this can not be checked at this
> time. But this  does not mean it is useless because we
> still can detect inconsistencies in other cases:
> 
> void callfoo(int n, char buf[n - 1]) { foo(n, buf); }
> 
> We could also - in the future - have a warning about all
> situations where bound information is lost, making sure
> that preconditions are always checked for people who
> consistently use these annotations.
> 
> 
>> The compiler has no choice than to trust the user that the pre-
>> condition  for calling foo is fulfilled.  I can see how
>> being able to just check half  of the contract might be
>> useful, but if it doesn't give full checking then
>> any proposal for syntax should be even more obviously
>> orthogonal than the current one.
> 
> Your argument is not clear to me.
> 
> 
>>> For
>>>
>>> void foo(int n, char buf[n]);
>>>
>>> it semantically has no meaning according to the C standard,
>>> but a compiler could still warn.
>>
>> Hmm?  Warn about what in this decl?
> 
> I meant, we could warn about something like this
> because it is likely an error:
> 
> void foo(int n, char buf[n])
> {
>    buf[n] = 1;
> }
> 
> 
>>> It could also warn for
>>>
>>> void foo(int n, char buf[n]);
>>>
>>> int main()
>>> {
>>>      char buf[9];
>>>      foo(buf);
>>> }
>>
>> You mean if you write 'foo(10,buf)' (the above, as is, is simply a
>> syntax error for non-matching number of args).  Or was it a mispaste
>> and you mean  the one from the godbolt link, i.e.:
> 
> I meant:
> 
> char buf[9];
> foo(10, buf);
> 
> In fact, it turns out we warn already:
> 
> https://godbolt.org/z/qcvsv87Ev
> 
>> void foo(char buf[10]){ buf[9] = 1; }
>> int main()
>> {
>>      char buf[9];
>>      foo(buf);
>> }
>>
>> ?  If so, yeah, we warn already.  I don't think this is an argument
>> for (or against) introducing new syntax.
>> ...
> 
> It is argument for having this syntax, because we could
> extend such warning (those we already have and those we
> could still add) to more common cases such as
> 
> void foo(char buf[.n], size_t n);
> 
> In my opinion, this would a huge step forward for
> safety of C programs as we already have a lot of
> infrastructure for checking bounds.
> 
> Of course, the existing GNU extension would achieve
> the same thing:
> 
> void foo(size_t n; char buf[n], size_t n);
> 
> 
> 
>>> But in general: This feature is useful not only for documentation
>>> but also for analysis.
>>
>> Which feature we're talking about now?  The ones you used all work
>> today,
>> as you demonstrated.  I thought we would be talking about that
>> ".whatever"
>> syntax to refer to arbitrary parameters, even following ones?  I
>> think a
>> disrupting syntax change like that should have a higher bar than "in
>> some
>> cases, depending on circumstance, we might even be able to warn".
> 
> We can use our existing features and then apply them
> to cases where the bound is specified after the pointer,
> which is more common in practice.

Yep; basically adding some (not perfect, but some) static analysis to 
many libc function calls.

Also, considering the issues with sizeof and arrays, and the lack of a 
_Nitems() [proposed as _Lengthof()] operator, there's a lot of manual 
work in array (read pointer) parameters.

However, a hypothetical _Nitems() operator could make use of this 
syntactic sugar, and be more useful than just providing static analysis. 
  Using _Nitems() on a VMT (including pointer parameters) could be 
specified to return the number of elements, so I foresee code like:


void foo(int arr[nmemb], size_t nmemb)
{
         // _Nitems() evaluates to nmemb
         for (size_t i = 0; i < _Nitems(arr); i++)
                 arr[i] = i;
}


void bar(int arr[])
{
         // Constraint violation
         for (size_t i = 0; i < _Nitems(arr); i++)
                 arr[i] = i;
}


This is probably the most useful part of this feature (but admittedly 
it's not only about this feature, or even could be added without this 
feature).

> 
> 
> Martin
> 

Cheers,

Alex

-- 
<http://www.alejandro-colomar.es/>


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 833 bytes --]

  reply	other threads:[~2022-11-29 17:28 UTC|newest]

Thread overview: 69+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
     [not found] <20220826210710.35237-1-alx.manpages@gmail.com>
     [not found] ` <Ywn7jMtB5ppSW0PB@asta-kit.de>
     [not found]   ` <89d79095-d1cd-ab2b-00e4-caa31126751e@gmail.com>
     [not found]     ` <YwoXTGD8ljB8Gg6s@asta-kit.de>
     [not found]       ` <e29de088-ae10-bbc8-0bfd-90bbb63aaf06@gmail.com>
     [not found]         ` <5ba53bad-019e-8a94-d61e-85b2f13223a9@gmail.com>
     [not found]           ` <CACqA6+mfaj6Viw+LVOG=nE350gQhCwVKXRzycVru5Oi4EJzgTg@mail.gmail.com>
     [not found]             ` <491a930d-47eb-7c86-c0c4-25eef4ac0be0@gmail.com>
2022-09-02 21:57               ` Alejandro Colomar
2022-09-03 12:47                 ` Martin Uecker
2022-09-03 13:29                   ` Ingo Schwarze
2022-09-03 15:08                     ` Alejandro Colomar
2022-09-03 13:41                   ` Alejandro Colomar
2022-09-03 14:35                     ` Martin Uecker
2022-09-03 14:59                       ` Alejandro Colomar
2022-09-03 15:31                         ` Martin Uecker
2022-09-03 20:02                           ` Alejandro Colomar
2022-09-05 14:31                             ` Alejandro Colomar
2022-11-10  0:06                           ` Alejandro Colomar
2022-11-10  0:09                             ` Alejandro Colomar
2022-11-10  1:33                             ` Joseph Myers
2022-11-10  1:39                               ` Joseph Myers
2022-11-10  6:21                                 ` Martin Uecker
2022-11-10 10:09                                   ` Alejandro Colomar
2022-11-10 23:19                                   ` Joseph Myers
2022-11-10 23:28                                     ` Alejandro Colomar
2022-11-11 19:52                                     ` Martin Uecker
2022-11-12  1:09                                       ` Joseph Myers
2022-11-12  7:24                                         ` Martin Uecker
2022-11-12 12:34                                     ` Alejandro Colomar
2022-11-12 12:46                                       ` Alejandro Colomar
2022-11-12 13:03                                       ` Joseph Myers
2022-11-12 13:40                                         ` Alejandro Colomar
2022-11-12 13:58                                           ` Alejandro Colomar
2022-11-12 14:54                                           ` Joseph Myers
2022-11-12 15:35                                             ` Alejandro Colomar
2022-11-12 17:02                                               ` Joseph Myers
2022-11-12 17:08                                                 ` Alejandro Colomar
2022-11-12 15:56                                             ` Martin Uecker
2022-11-13 13:19                                               ` Alejandro Colomar
2022-11-13 13:33                                                 ` Alejandro Colomar
2022-11-13 14:02                                                   ` Alejandro Colomar
2022-11-13 14:58                                                     ` Martin Uecker
2022-11-13 15:15                                                       ` Alejandro Colomar
2022-11-13 15:32                                                         ` Martin Uecker
2022-11-13 16:25                                                           ` Alejandro Colomar
2022-11-13 16:28                                                         ` Alejandro Colomar
2022-11-13 16:31                                                           ` Alejandro Colomar
2022-11-13 16:34                                                             ` Alejandro Colomar
2022-11-13 16:56                                                               ` Alejandro Colomar
2022-11-13 19:05                                                                 ` Alejandro Colomar
2022-11-14 18:13                                                           ` Joseph Myers
2022-11-28 22:59                                                             ` Alex Colomar
2022-11-28 23:18                                                       ` Alex Colomar
2022-11-29  0:05                                                         ` Joseph Myers
2022-11-29 14:58                                                         ` Michael Matz
2022-11-29 15:17                                                           ` Uecker, Martin
2022-11-29 15:44                                                             ` Michael Matz
2022-11-29 16:58                                                               ` Uecker, Martin
2022-11-29 17:28                                                                 ` Alex Colomar [this message]
2022-11-29 16:49                                                           ` Joseph Myers
2022-11-29 16:53                                                             ` Jonathan Wakely
2022-11-29 17:00                                                               ` Martin Uecker
2022-11-29 17:19                                                                 ` Alex Colomar
2022-11-29 17:29                                                                   ` Alex Colomar
2022-12-03 21:03                                                                     ` Alejandro Colomar
2022-12-03 21:13                                                                       ` Andrew Pinski
2022-12-03 21:15                                                                       ` Martin Uecker
2022-12-03 21:18                                                                         ` Alejandro Colomar
2022-12-06  2:08                                                                       ` Joseph Myers
2022-11-14 17:52                                                 ` Joseph Myers
2022-11-14 17:57                                                   ` Alejandro Colomar
2022-11-14 18:26                                                     ` Joseph Myers
2022-11-28 23:02                                                       ` Alex Colomar
2022-11-10  9:40                             ` G. Branden Robinson
2022-11-10 10:59                               ` Alejandro Colomar
2022-11-10 22:25                                 ` G. Branden Robinson

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=7697ff60-aa2a-a41e-9d08-ab25423ee750@gmail.com \
    --to=alx.manpages@gmail.com \
    --cc=Martin.Uecker@med.uni-goettingen.de \
    --cc=gcc@gcc.gnu.org \
    --cc=joseph@codesourcery.com \
    --cc=linux-man@vger.kernel.org \
    --cc=matz@suse.de \
    --cc=schwarze@usta.de \
    --cc=wg14@soasis.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 read-only IMAP folder(s) and NNTP newsgroup(s).