Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix issues in bounds-widening analysis in for Nt_array_ptrs #1205

Open
dtarditi opened this issue Jul 2, 2023 · 0 comments
Open

Fix issues in bounds-widening analysis in for Nt_array_ptrs #1205

dtarditi opened this issue Jul 2, 2023 · 0 comments
Assignees

Comments

@dtarditi
Copy link
Member

dtarditi commented Jul 2, 2023

There seem to be issues with the bounds-widening analysis in clang/lib/Sema/BoundsWideningAnalysis.cpp:

  • It uses bounds declarations from where clauses but SemaBounds.cpp isn't validating the bounds declarations in where clauses. This is a soundness issue and causes the Checked C compiler to accept incorrect code.
  • It generates widened bounds expressions that SemaBounds.cpp can't prove imply declared bounds. SemaBounds.cpp seems to have a hack in ValidateBoundsContext that suppresses diagnostic messages for bounds declaration checking for this case. It seems like the hack could suppress diagnostic messages involving statements with invertible assignments that cause a bounds declaration to be violated. This is another potential soundness issues.
  • SemaBounds.cpp prioritizes the results from the bounds widening analysis when determining the bounds of a variable. The bounds widening analysis sets the bounds of a variable to the declared bounds when the widened bounds is killed. This happens, for example, when the variable is assigned to. This doesn't interact well with checking bounds declaration in where clauses when I implemented it. SemaBounds.cpp may determine an observed bounds that makes the where clause bounds declaration valid, but bounds widening analysis is returning the declared bounds, which is prioritized over the observed bounds.
  • The bounds widening analysis implementation and design doc is quite confused about out sets for basic blocks. The out sets need to be per-successor edge out sets because the analysis is flow-sensitive. The analysis looks for code of the form if (*p) ... where p is a _Nt_array_ptr and widens bounds in the non-null check branch. However, the implementation has only single out sets, which doesn't make sense. It seems to have hacky code that introduces the flow-sensitivity on out sets in the computation of in sets.
  • The CFG examples in the code for while loops and the design document are confused. This needs to be investigated further.
@dtarditi dtarditi moved this to In Progress in Checked C Board Jul 11, 2023
@dtarditi dtarditi added this to the Checked C v1.0 release milestone Jul 11, 2023
@dtarditi dtarditi self-assigned this Jul 11, 2023
dtarditi added a commit that referenced this issue Sep 28, 2024
Fix up URLs in Checked C docs.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
Status: In Progress
Development

No branches or pull requests

1 participant