Skip to content

Warnings and Dead Code Handling for noreturn#953

Merged
michael-schwarz merged 6 commits intogoblint:masterfrom
just-max:noreturn_support_58
Feb 2, 2023
Merged

Warnings and Dead Code Handling for noreturn#953
michael-schwarz merged 6 commits intogoblint:masterfrom
just-max:noreturn_support_58

Conversation

@just-max
Copy link
Copy Markdown
Contributor

@just-max just-max commented Dec 21, 2022

Resolves #501.

Changes:

  • on return of a function, warn if the function is marked noreturn,
  • after call of a function, raise Deadcode if the option sem.noreturn.dead_code is enabled.

Added an Other variant to undefined_behavior for the message category, but could also just as well be category Unknown.

However, from what I can tell there's an issue here with how CIL handles noreturn. Here are the CFGs generated for the following function, once marked with noreturn and once unmarked:

void without_noreturn(int x) {
  if (x)
    abort();
}

noreturn void with_noreturn(int x) {
  if (x)
    abort();
}

CFG for without_noreturn

image

CFG for with_noreturn

image

My guess is that reaching the end of a noreturn function is undefined behaviour, so CIL is allowed to do this.

@michael-schwarz michael-schwarz mentioned this pull request Dec 21, 2022
Closed
@just-max just-max force-pushed the noreturn_support_58 branch from 8cf3ad9 to 54f03d9 Compare January 17, 2023 16:32
@just-max
Copy link
Copy Markdown
Contributor Author

just-max commented Jan 25, 2023

We found the problem to be that the CFG construction in Goblint checks the number of (real) successors of an If statement. In the case of two successors, these would typically be the first statements of the true and of the false blocks. If there is only one successor, Goblint assumes it to be the successor in both branches. That's an assumption that doesn't hold if there is no else block and nothing after the if statement in the function. This is the case in a noreturn function processed in CIL, which is why the CFG ends up having the Neg edge to the successor in the true block (abort(), in this case).

We decided to add an option in CIL so that functions that fall through (can reach the end of the body), yet don't contain return statements, always get a return statement added by CIL—even those marked noreturn, which was previously not the case. PR for CIL incoming.

@just-max just-max mentioned this pull request Jan 25, 2023
Merged
@just-max
Copy link
Copy Markdown
Contributor Author

just-max commented Jan 31, 2023

still depends on goblint/cil#129, otherwise ready to merge

@just-max just-max force-pushed the noreturn_support_58 branch from 75049d5 to f3d71f4 Compare January 31, 2023 18:32
@just-max just-max marked this pull request as ready for review January 31, 2023 18:32
@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Feb 1, 2023 •
edited
Loading

I merged the CIL PR. Could you update the pin in the opam files so we can see if the CI is happy then?

@just-max
Copy link
Copy Markdown
Contributor Author

just-max commented Feb 1, 2023

should be ready now

michael-schwarz
michael-schwarz approved these changes Feb 1, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, thank you!

just-max
just-max commented Feb 2, 2023
View reviewed changes
sim642
sim642 requested changes Feb 2, 2023
View reviewed changes
just-max
just-max commented Feb 2, 2023
View reviewed changes
@michael-schwarz michael-schwarz merged commit c53d263 into goblint:master Feb 2, 2023
@sim642 sim642 added this to the v2.2.0 milestone Apr 5, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sim642 sim642 sim642 approved these changes

@michael-schwarz michael-schwarz michael-schwarz approved these changes

Assignees

No one assigned

Labels

c11 feature student-job

Projects

None yet

Milestone

v2.2.0

Development

Successfully merging this pull request may close these issues.

Warn when control flow reaches end of a _Noreturn function

3 participants

@just-max @michael-schwarz @sim642