noreturn attribute doesn't work in smatch

noreturn attribute doesn't work in smatch

[John Levon]

./smatch: a.c:20 main() error: double free of 'str'

given:

```
#include <stdlib.h>
#include <string.h>

__attribute__((__noreturn__)) void
die(void)
{
        exit(1);
}

int
main(void)
{
        char *str = strdup("test");

        if (str != NULL) {
                free(str);
                die();
        }

        free(str);

        return (0);
}
```

As far as I can figure out, this looks like a sparse problem: an
'inline' or 'extern' specifier in this position gets marked as the
relevant MOD_* flag for the function, but the noreturn doesn't bubble
up in the same way. Some quick lame attempts to add ctx->is_noreturn did
not go well.

I think this might be the underlying issue behind sparse's failing test
validation/function-redecl2.c but I'm not positive.

We can do:

```
#ifdef __CHECKER__
#define SMATCH_NORETURN __attribute__((__noreturn__))
#else
#define SMATCH_NORETURN /* would break gcc otherwise */
#endif

__attribute__((__noreturn__)) void
die(void) SMATCH_NORETURN
{
```

but it's ... unlovely.

Any thoughts?

thanks
john

Re: noreturn attribute doesn't work in smatch

[John Levon]

I took another pass, and this works for me:

diff --git a/parse.c b/parse.c
index ca4726b8..44c59707 100644
--- a/parse.c
+++ b/parse.c
@@ -2859,6 +2859,7 @@ struct token *external_declaration(struct token
*token, struct symbol_list **lis
        /* Parse declaration-specifiers, if any */
        token = declaration_specifiers(token, &ctx);
        mod = storage_modifiers(&ctx);
+       mod |= ctx.ctype.modifiers & MOD_NORETURN;
        decl = alloc_symbol(token->pos, SYM_NODE);
        /* Just a type declaration? */
        if (match_op(token, ';')) {

(I suppose a proper fix would collate all function-level attributes
but...)


However, it seems like smatch is still not quite passing its knowledge
along: if I have:

extern void die() __attribute((__noreturn__));

void mydie()
{
	die();
}

then the die() call is nullified, but smatch doesn't realise that means
all paths of mydie() are __noreturn__ too.

regards
john

Re: noreturn attribute doesn't work in smatch

[Dan Carpenter]

On Thu, Aug 15, 2019 at 12:12:37PM +0100, John Levon wrote:
> 
> I took another pass, and this works for me:
> 
> diff --git a/parse.c b/parse.c
> index ca4726b8..44c59707 100644
> --- a/parse.c
> +++ b/parse.c
> @@ -2859,6 +2859,7 @@ struct token *external_declaration(struct token
> *token, struct symbol_list **lis
>         /* Parse declaration-specifiers, if any */
>         token = declaration_specifiers(token, &ctx);
>         mod = storage_modifiers(&ctx);
> +       mod |= ctx.ctype.modifiers & MOD_NORETURN;
>         decl = alloc_symbol(token->pos, SYM_NODE);
>         /* Just a type declaration? */
>         if (match_op(token, ';')) {
> 
> (I suppose a proper fix would collate all function-level attributes
> but...)
> 

This patch seems like a hack, but I will apply it...

> 
> However, it seems like smatch is still not quite passing its knowledge
> along: if I have:
> 
> extern void die() __attribute((__noreturn__));
> 
> void mydie()
> {
> 	die();
> }
> 
> then the die() call is nullified, but smatch doesn't realise that means
> all paths of mydie() are __noreturn__ too.

The code to handle that is really ancient.  You need to do:
    ./smatch --info test.c | tee warns.txt
    grep no_return_funcs warns.txt || echo FAIL
    ./smatch_scripts/gen_no_return_funcs.sh warns.txt -p=levon
    mv levon.no_return_funcs smatch_data/

Then pass -p=levon to smatch on the next run.

regards,
dan carpenter

Re: noreturn attribute doesn't work in smatch

[John Levon]

On Thu, Aug 22, 2019 at 04:30:34PM +0300, Dan Carpenter wrote:

> On Thu, Aug 15, 2019 at 12:12:37PM +0100, John Levon wrote:
> > 
> > I took another pass, and this works for me:
> > 
> > diff --git a/parse.c b/parse.c
> > index ca4726b8..44c59707 100644
> > --- a/parse.c
> > +++ b/parse.c
> > @@ -2859,6 +2859,7 @@ struct token *external_declaration(struct token
> > *token, struct symbol_list **lis
> >         /* Parse declaration-specifiers, if any */
> >         token = declaration_specifiers(token, &ctx);
> >         mod = storage_modifiers(&ctx);
> > +       mod |= ctx.ctype.modifiers & MOD_NORETURN;
> >         decl = alloc_symbol(token->pos, SYM_NODE);
> >         /* Just a type declaration? */
> >         if (match_op(token, ';')) {
> > 
> > (I suppose a proper fix would collate all function-level attributes
> > but...)
> 
> This patch seems like a hack, but I will apply it...

I agree, it would be nice to see this cleaned up properly, but as the
above is sufficient for us, it'll do for us! Thanks!

> > However, it seems like smatch is still not quite passing its knowledge
> > along: if I have:
> > 
> > extern void die() __attribute((__noreturn__));
> > 
> > void mydie()
> > {
> > 	die();
> > }
> > 
> > then the die() call is nullified, but smatch doesn't realise that means
> > all paths of mydie() are __noreturn__ too.
> 
> The code to handle that is really ancient.  You need to do:
>     ./smatch --info test.c | tee warns.txt
>     grep no_return_funcs warns.txt || echo FAIL
>     ./smatch_scripts/gen_no_return_funcs.sh warns.txt -p=levon
>     mv levon.no_return_funcs smatch_data/
> 
> Then pass -p=levon to smatch on the next run.

OK, thanks. That doesn't match too well with the way we use smatch, but
this is much less of a big deal (I only needed to annotate this in a
couple of places).

regards
john

Re: noreturn attribute doesn't work in smatch

[Dan Carpenter]

On Thu, Aug 22, 2019 at 02:46:03PM +0100, John Levon wrote:
> On Thu, Aug 22, 2019 at 04:30:34PM +0300, Dan Carpenter wrote:
> > The code to handle that is really ancient.  You need to do:
> >     ./smatch --info test.c | tee warns.txt
> >     grep no_return_funcs warns.txt || echo FAIL
> >     ./smatch_scripts/gen_no_return_funcs.sh warns.txt -p=levon
> >     mv levon.no_return_funcs smatch_data/
> > 
> > Then pass -p=levon to smatch on the next run.
> 
> OK, thanks. That doesn't match too well with the way we use smatch, but
> this is much less of a big deal (I only needed to annotate this in a
> couple of places).

It should be the the DB, right?  Would that work for you?

It's sort of an awkward thing because I publish the list of no return
functions used in the kernel, but I don't publish the DB.  So I probably
have to keep both methods...

regards,
dan carpenter

Re: noreturn attribute doesn't work in smatch

[John Levon]

On Thu, Aug 22, 2019 at 06:05:29PM +0300, Dan Carpenter wrote:

> On Thu, Aug 22, 2019 at 02:46:03PM +0100, John Levon wrote:
> > On Thu, Aug 22, 2019 at 04:30:34PM +0300, Dan Carpenter wrote:
> > > The code to handle that is really ancient.  You need to do:
> > >     ./smatch --info test.c | tee warns.txt
> > >     grep no_return_funcs warns.txt || echo FAIL
> > >     ./smatch_scripts/gen_no_return_funcs.sh warns.txt -p=levon
> > >     mv levon.no_return_funcs smatch_data/
> > > 
> > > Then pass -p=levon to smatch on the next run.
> > 
> > OK, thanks. That doesn't match too well with the way we use smatch, but
> > this is much less of a big deal (I only needed to annotate this in a
> > couple of places).
> 
> It should be the the DB, right?  Would that work for you?

There's few enough that it's preferable to just explicitly mark the
source as noreturn too, rather than keep a separate list.

regards
john