-
Notifications
You must be signed in to change notification settings - Fork 19
Open
Milestone
Description
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) ...
wherep
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.
Metadata
Metadata
Assignees
Labels
No labels
Type
Projects
Status
In Progress