You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
There seem to be issues with the bounds-widening analysis in clang/lib/Sema/BoundsWideningAnalysis.cpp:
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 text was updated successfully, but these errors were encountered: