This repo contains a version of clang that is modified to support Checked C. Checked C is an extension to C that lets programmers write C code with bounds checking and improved type-safety.
13
stars
19
forks
source link
Fix issues in bounds-widening analysis in for Nt_array_ptrs #1205
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.
There seem to be issues with the bounds-widening analysis in clang/lib/Sema/BoundsWideningAnalysis.cpp:
if (*p) ...wherepis a_Nt_array_ptrand 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.