Bounds widening for _Nt_array_ptr's #728

mgrang · 2019-11-13T23:46:19Z

_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) }

Strings in Checked C are declared as _Nt_array_ptr which means they are terminated by a null terminator. If we determine that the dereference of an _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) }

mgrang · 2019-11-14T19:44:34Z

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]

mgrang · 2019-11-18T21:20:18Z

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

mgrang · 2019-11-18T23:15:05Z

clang/lib/Sema/BoundsAnalysis.cpp

+namespace clang {
+
+void BoundsAnalysis::WidenBounds() {
+  llvm::dbgs() << "### Debug bounds analysis\n";


Will remove the debug messages soon.

saeednj

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.

clang/lib/Sema/BoundsAnalysis.cpp

mgrang · 2019-11-22T00:15:40Z

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.

mgrang · 2019-12-17T04:15:04Z

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.

dtarditi

@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.

dtarditi · 2019-12-17T16:05:39Z

clang/test/CheckedC/inferred-bounds/widened-bounds.c

+// CHECK: [B8]
+// CHECK:   1: p = "xy"
+// CHECK:   2: *(p + 1)
+// CHECK: upper_bound(p) = 1


This is wrong. You need to widen against the upper bound of p, which is declared to p + j.

dtarditi · 2019-12-17T16:11:09Z

clang/lib/Sema/BoundsAnalysis.cpp

+
+void BoundsAnalysis::ComputeGenSets(BlockMapTy BlockMap) {
+  // If there is an edge B1->B2 and the edge condition is of the form
+  // "if (*(p + i))" then Gen[B1] = {B2, p:i} .


Could you clarify whether i is a constant or a variable? I know that i is a constant from context, but it could confuse people later on.

Gen sets should be constant offsets relative to the declared upper bound of a pointer. If p has declared upper bounds of e, and this is a dereference of *(e + i), then Gen[B1] = i. You'll need to handle expressions that are equivalent to e + i. Note that we already have methods for checking the equivalence of expressions.

dtarditi · 2019-12-17T16:15:36Z

clang/lib/Sema/BoundsAnalysis.cpp

+    // For conditions of the form "if (*p)".
+    if (const auto *D = dyn_cast<DeclRefExpr>(Exp)) {
+      if (const auto *V = dyn_cast<VarDecl>(D->getDecl())) {
+        if (V->getType()->isCheckedPointerNtArrayType()) {


I agree that gen can remain a constant offset. However, it should be a constant offset relative to the declared upper bound of a pointer variable.

…-clang into widen_bounds3

mgrang · 2019-12-17T21:23:35Z

@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

dtarditi · 2019-12-17T21:43:55Z

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.

mgrang · 2019-12-17T23:47:03Z

< 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?

dtarditi · 2019-12-18T01:02:28Z

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.

mgrang · 2019-12-18T04:22:53Z

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.

mgrang · 2019-12-18T19:14:54Z

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

dtarditi

I noticed that in the testing code, you removed code that testeds nested conditionals of the form:

if (*p) {
  if (*(p + 1)) {
    if (*(p + 2)) {
   ...

Could you add a test of this back?

Added. Because we converted warnings to errors I cannot add more intensive tests for this commit. An nt_array_ptr with a non-zero upper bound won't do any widening because we explicitly test for zero upper bound. On the other hand, for an nt_array_ptr with zero upper bound, I cannot dereference anything other than *p without running into out-of-bounds access errors.

dtarditi

Looks good! Thanks.

Mandeep Singh Grang and others added 3 commits November 13, 2019 15:43

Move pch tests to a precompiled-headers subdirectory (#729)

fec2c12

Update1

76b23ab

Mandeep Singh Grang added 2 commits November 15, 2019 12:22

Update2

c09858f

Update3

07e5464

mgrang requested review from dtarditi and kkjeer November 18, 2019 21:18

Update4

050d321

Update5

03c33d3

mgrang commented Nov 18, 2019

View reviewed changes

Mandeep Singh Grang added 5 commits November 18, 2019 15:43

Update6

a4d7033

Update7

67707cf

Update8

f4703d8

Update9

4deafb0

Update10

7797697

mgrang requested a review from saeednj November 20, 2019 23:14

mgrang changed the title ~~Implement bounds widening for _Nt_array_ptr's~~ Bounds widening for _Nt_array_ptr's Nov 21, 2019

Update11

4f2f328

saeednj reviewed Nov 21, 2019

View reviewed changes

clang/lib/Sema/BoundsAnalysis.cpp Outdated Show resolved Hide resolved

clang/lib/Sema/BoundsAnalysis.cpp Outdated Show resolved Hide resolved

Update12

160b7e9

Mandeep Singh Grang added 7 commits November 21, 2019 16:42

Update13

3e202ff

Update14

082bbc3

Update15

6e1d49d

Update16

3e628d0

Update17

f7879f4

Update18

45a2b15

Update19

48ee6f5

Mandeep Singh Grang added 10 commits December 16, 2019 12:31

Update 28

7f155d2

Update 29

e530600

Update 30

0249a89

Update 31

370e1b1

Update 32

3bcb3c1

Update 33

6a9c696

Update 34

2aed17c

Update 35

6cc2ec2

Update 36

4f99a4f

Update 37

3cbdec1

dtarditi reviewed Dec 17, 2019

View reviewed changes

Mandeep Singh Grang added 2 commits December 17, 2019 11:35

Update 38

0002ab9

Merge branch 'widen_bounds3' of https://github.com/Microsoft/checkedc…

30384f9

…-clang into widen_bounds3

Update 39

777fc0c

Update 40

8bda928

dtarditi reviewed Dec 19, 2019

View reviewed changes

Update 41

87b9020

dtarditi approved these changes Dec 19, 2019

View reviewed changes

mgrang merged commit 86b63d0 into master Dec 20, 2019

mgrang deleted the widen_bounds3 branch December 20, 2019 01:05

mgrang mentioned this pull request Feb 3, 2021

Infer widened bounds for pointers to null-terminated arrays #467

Closed

This was referenced Jan 16, 2022

Infer widened bounds for pointers to null-terminated arrays checkedc/checkedc-llvm-project#466

Closed

Bounds widening for _Nt_array_ptr's checkedc/checkedc-llvm-project#724

Closed

Bounds widening for _Nt_array_ptr's #728

Bounds widening for _Nt_array_ptr's #728

Uh oh!

Conversation

mgrang commented Nov 13, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mgrang commented Nov 14, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mgrang commented Nov 18, 2019

Uh oh!

mgrang Nov 18, 2019

Choose a reason for hiding this comment

Uh oh!

saeednj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mgrang commented Nov 22, 2019

Uh oh!

mgrang commented Dec 17, 2019

Uh oh!

dtarditi left a comment

Choose a reason for hiding this comment

Uh oh!

dtarditi Dec 17, 2019

Choose a reason for hiding this comment

Uh oh!

dtarditi Dec 17, 2019

Choose a reason for hiding this comment

Uh oh!

dtarditi Dec 17, 2019

Choose a reason for hiding this comment

Uh oh!

mgrang commented Dec 17, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

dtarditi commented Dec 17, 2019

Uh oh!

mgrang commented Dec 17, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

dtarditi commented Dec 18, 2019

Uh oh!

mgrang commented Dec 18, 2019

Uh oh!

mgrang commented Dec 18, 2019

Uh oh!

dtarditi left a comment • edited by mgrang Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dtarditi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mgrang commented Nov 13, 2019 •

edited

Loading

mgrang commented Nov 14, 2019 •

edited

Loading

mgrang commented Dec 17, 2019 •

edited

Loading

mgrang commented Dec 17, 2019 •

edited

Loading

dtarditi left a comment •

edited by mgrang

Loading