Conversation
When converting existing code, a common pattern is to write a null-terminator after copying data to an nt_array_ptr. This can lead to attempting to write a null-terminator exactly at the upper bound of the null-terminated array, when the entire is filled with deta. This was not allowed under Checked C rules. It's legal to allow a write of a null-terminator at the upper bound of a null-terminated array: the invariant for a null-terminated array is still met. This change adds support for writing a null-terminator at exactly the upper bound of an null-termianted array. We only allow this for simple assignments. It is not allowed for compound assigments. This was a little awkward to implement because all bounds checks are currently done as part of lvalue-expression evaluation. In this case, we need to know the value that is being written. I didn't want to move the bounds check insertion to all places that use lvalues. Instead, we skip inserting the check when constructing an lvalue for this specific case. We have a special case check in assignment. We might to revisit this in the future and move the checks. Testing: - Added new tests to the nullterm_pointers.c file in the Checked C repo. The tests check writing null values and non-null values exactly at the upper bounds of nt_array_ptr and regular array_ptrs.
When we allow a write of 0 at the upper bound of a pointer to a null-terminated array, we have to expand the range of allowed memory to include the first element of the null terminated sequence. It is possible for even this range to be empty. If so, the write needs to fail with a runtime fault. This adjusts the bounds check for a write of 0 at the upper bound to also check the lower bound. This prevents a write to an empty expanded memory range. Testing: - Add tests to nullterm_pointers.c in the Checked C repo. The tests check writes of 0 at the upper bound where the expanded range has 1 element or no elements.
This was referenced Nov 30, 2017
sulekhark
pushed a commit
that referenced
this pull request
Jul 8, 2021
* split variable adder and constraint adder passes * populate typedef map during variable adder phase * avoid numparam crash * Add ReasonFailed to brainTransplant; Refactor insertNewFVConstraint * another assert * add tests proto vs body * formatting, clarity * remove xfail from tests, add grep * wording: 'new'->'seen' * more mergefailure reasons * remove calls to braintransplant (regression fail: 80) * split add variable phase at higher level * only save merged FVC (regression fail: 24) * make special case match description * remove code for braintransplant * restore the safety of PragramVariableAdder * first pass comments; assert for backwards merge * second comment pass - usage and defn * add test for #427, now solved
This was referenced Jan 15, 2022
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
In existing C code, a common pattern is to write a null terminator after copying data to a null-terminated array. When converting the code to Checked C, this can lead to attempting to write a null-terminator exactly at the upper bound of an nt_array_ptr, when the entire array is filled with data. This was not allowed under Checked C bounds checking rules. Even though it was not allowed, it is OK to allow it because the invariant for null-terminated arrays is preserved by the write.
This change relaxes the bounds checking for nt_array_ptrs to allow writing null values exactly at upper bounds. There is a matching Checked C pull request that updates the specification and tests: checkedc/checkedc#242.
We only allow this for simple assignments. It is not allowed for compound assignments. This was a little awkward to implement because all bounds checks are currently done as part of lvalue-expression evaluation. In this case, we need to know the value that is being written. I didn't want to move the bounds check insertion to all places that use lvalues. Instead, we skip inserting the check when constructing an lvalue for this specific case. We have a special case check in assignment. We might to revisit this in the future and move the checks.
The generated LLVM IR for the check for the upper bound case is larger than necessary. Given bounds (lb, ub), a destination pointer p,, and a value v, we check three conditions: p == ub && lb <= p and v == 0. The lower bound check is needed to handle empty ranges properly. We could avoid generating code for it by changing the regular bounds check to use branches instead of AND'ing conditions together. That's a significant change that should be evaluated separately because it could have performance effects.
Testing: