Bounds widening for _Nt_array_ptr's

[secure-sw-dev-bot]

This issue was copied from checkedc/checkedc-clang#728

---

_Nt_array_ptr's are terminated by a null terminator. If we determine that the dereference of a
_Nt_array_ptr is non-null then we can widen the bounds of the pointer by 1 because there will always be at least the null terminator in the string.

Formally we can state the problem as:
∀ p | p ∈ _Nt_array_ptr & bounds(p) = [l, u)
*p != 0 => bounds(p) = [l, u + 1)

Example:
_Nt_array_ptr<char> p : count(0) = "abc"; // bounds = [0, 0]
if (*p) { // bounds = [0, 1) }

[secure-sw-dev-bot]

Comment from @mgrang:

Dataflow equations:

Let p ∈ _Nt_array_ptr.
For each basic block B:

If there is an edge B1->B2 and the edge condition is of the form "if (*( p + i))", then Gen[B1] = {B2, p:i+1}

In a block B, if p is assigned to, then Kill[B] = {p}

In[B] = ∩ Out[B*->B], where B* are all preds(B)

Out[B1->B2] = (In[B1] - Kill[B1]) ∪ Gen[B1->B2]

[secure-sw-dev-bot]

Comment from @mgrang:

Please review this PR as WIP. I am currently testing it out. Will add unit tests soon.

[secure-sw-dev-bot]

Comment from @mgrang:

Is it useful to have a base class for "DataFlowAnalysis" and implement case specific uses?
There is a very similar implementation with a different usage in AvailableFactAnalysis.

Yes, the goal is ultimately to have a common base. We can do that in a separate clean-up PR.

[secure-sw-dev-bot]

Comment from @mgrang:

Thanks for your review, David. If we change Gen to be an expression instead of a constant offset how would we compute the intersection of sets? One option is to assign a number to each expression in Gen. Numbers would increase from entry to exit for a particular V. Then to compute intersection we choose the expr with the smaller number. This would represent the LUB of the sets.

[secure-sw-dev-bot]

Comment from @mgrang:

@mgrang, you are correct that changing gen sets to be expressions would complicate the algorithm. The gen set entries should be constant offsets relative to the declared upper bound of an nt_array_ptr variable. Given

nt_array_ptr<char> p : bounds(e1, e2)

it is not correct to widen p given *p. p should be widened given a dereference of the form *(e2 + k), where k is a constant integer.

Note that we have methods for determining whether some expression e3 is equivalent to the expression e2. See AST\CanonBounds.

Thanks David. I think we still have a complication. Let's say we have a case like:
nt_array_ptr<char> p : bounds(p, p + 1)

and then we encounter *(p + 2) which is essentially *((p + 1) + 1). How do we separate k from *(e) here? What about accesses like *(i + j + e + k + l). This can get complicated quickly!

I think a simpler option is to keep the implementation we have now as is, meaning the bounds widened by this algorithm are not relative to the declared upper bound. Instead we "adjust" the widened bounds at the call site of this algorithm. Let's say the widened bounds for p returned by this algorithm is k and the declared bounds of p are (l, u).

If (l + k) <= u, we do not need to widen.
If (l + k) > u, we can widen the bounds by l + k - u.

For example:
nt_array_ptr<char> p : bounds(p, p + 2)

if (*p) // calc_bounds: 1, adjusted_bounds: p + 1 <= p + 2 => no widening done
   if (*(p + 1)) // calc_bounds: 2, adjusted_bounds: p + 2 <= p + 2 => no widening done
     if (*(p + 2)) // calc_bounds: 3, adjusted_bounds: p + 3 > p + 2 => bounds widened by (p + 3) - (p + 2) = 1.
       if (*(p + 3)) // calc_bounds: 4, adjusted_bounds: p + 4 > p + 2 => bounds widened by (p + 4) - (p + 2) = 2

[secure-sw-dev-bot]

Comment from @dtarditi:

I agree it could get complicated quickly. The way we will handle this is by putting expressions in a standard form, such that the constant is on the outside. We already face similar problems when checking bounds declarations.

The problem with the approach that you propose is that we cannot handle simple cases like widening bounds of a variable v with bounds(v, v + len).

I think it would be appropriate to address additional cases and using standard forms in separate PRs, and finish this PR. How about you add a check that the upper bound is the variable v? This would bring it into agreement with what I am proposing, and let us finish the current PR.

[secure-sw-dev-bot]

Comment from @mgrang:

< How about you add a check that the upper bound is the variable v?
David, could you please clarify this? Should we only allow bounds widening when nt_array_ptr<T> v : bounds(v, v)? Or when the dereference is at the upper bound?

[secure-sw-dev-bot]

Comment from @dtarditi:

I am suggesting that in this PR, we only widen bounds for nt_array_ptr variables whose bounds are bounds(v, v) or count(0). I am suggesting that in a future PR, we generalize this to widen bounds for dereferences involving constant offsets from the declared upper bound of a variable.

[secure-sw-dev-bot]

Comment from @mgrang:

Done. Latest PR widens bounds only when the declared bounds are count(0) or bounds(v, v). Also removed the more generic tests and replaced them with only tests specific to count(0) bounds.

[secure-sw-dev-bot]

Comment from @mgrang:

ADO Validations Passed:
https://dev.azure.com/msresearch/CheckedC/_build/results?buildId=395620