Extend static bounds declaration checking by ppashakhanloo · Pull Request #624 · checkedc/checkedc-clang

ppashakhanloo · 2019-07-02T17:45:05Z

I have not added the tests yet.

Everytime in bounds declaration checking we encounter a comparison between zero and an unsigned integer, we can use the fact that 0 <= any unsigned integer expression. In this commit, the representation of ranges has been extended. Instead of ConstantSizedRange, a new representation is introduced: BaseRange. InRange() checks whether the range is constant-sized or variable-sized, and compare lower/upper offsets based on that. CreateBaseRange() is responsible for setting the correct RangeType to a range.

dtarditi

Thanks for making this change. I think with variable-sized ranges, there are additional cases that you need to check. I think the code would benefit from checking upper/lower bounds independently and then combining the results. This would handle the additional cases and make the code simpler.

dtarditi · 2019-07-08T17:03:21Z

+    // const2 as signed (APSInt) integers.  They must have the same bitsize. A
+    // variable-sized range is a range that has the form (e1 + e2, e1 + e3), where
+    // e1, e2, and e3 are all expressions.
+    class BaseRange {


I think ranges are more complex than this comment indicates. A variable sized range has the form (e1 + e2, e1 + e3), where one or both of e2 and e3 are non-constant expressions.

I think it will be useful to state the invariant about the representation:

If a range is constant sized, the LowerOffsetExpr and UpperOffsetExpr should be null.

For a variable sized range, you'll need to think about to indicate whether to use the constant offset or the expression.

In theory, you could just check whether the expression is constant or not. We don't want to do this in practice because that's expensive to determine. So we want to compute this when handed the expression.

dtarditi · 2019-07-08T17:04:24Z

      }

+      bool IsConstantSizedRange() {
+        return BaseRangeType == RangeType::ConstantSized && !UpperOffsetExpr && !LowerOffsetExpr;


I think the check that UpperOffsetExpr and LowerOffsetExpr are null should be an assert. This is part of the invariant about the representation of ranges.

dtarditi · 2019-07-08T17:05:57Z

+      bool IsConstantSizedRange() {
+        return BaseRangeType == RangeType::ConstantSized && !UpperOffsetExpr && !LowerOffsetExpr;
+      }
+


I would recommend adding a matching method IsVariableSizedRange().

dtarditi · 2019-07-08T17:10:59Z


      // Is R in range of this range?
-      ProofResult InRange(ConstantSizedRange &R, ProofFailure &Cause, EquivExprSets *EquivExprs) {
+      ProofResult InRange(BaseRange &R, ProofFailure &Cause, EquivExprSets *EquivExprs) {


We should probably change that comment at line 1754 for clarity: Is R a subrange of this range?

dtarditi · 2019-07-08T17:46:26Z

+              Result = ProofResult::False;
+            }
+          } else { // at least one of the ranges is not constant-sized
+            Result = ProofResult::Maybe;


I think the logic needs to be reworked to check the lower and upper bound separately. For each bound, you can them come to the conclusion that:

this range's lower bound <= R's lower bound (true, false, or maybe).

R's upper bounds <= his range's upper bound (true, false, or maybe).

If 1 and 2 are true, the result is true.
If 1 or 2 are false, the result is false.
Otherwise the result is maybe.

For each bound involved in a ej <= ek, comparison, you need to handle the cases where

ej and ek are constant

ej is 0 and ek is an unsigned integer expression.

If you follow this approach, there is no need to handle variable vs. constant-sized ranges separately.

dtarditi · 2019-07-08T17:51:58Z


      // Does R partially overlap this range?
-      ProofResult PartialOverlap(ConstantSizedRange &R) {
+      ProofResult PartialOverlap(BaseRange &R) {


I think this could be generalized.

I addressed all the above comments (except this one) in my newest commit.
Can you please elaborate more on this comment?

dtarditi

I have additional suggestions for the code.

dtarditi · 2019-07-17T19:50:22Z

+        // If both ranges are constant-sized, the constant integer values of the offsets are compared.
+        // If at least one of the ranges is variable-sized, then in some special cases
+        // we can prove the lower bound is correct.
+        if (IsConstantSizedRange() && R.IsConstantSizedRange()) {


Instead of checking that the ranges are constant sized, how about checking that both lower bounds are constant? Then you can eliminate the last case at lines 1794 - 1796.

After reading this code, I think having fields named LowerOffsetExpr and LowerOffset (as well UpperOffsetExpr and UpperOffset) are confusing. The Expr suffix doesn't mean much. LowerOffsetVariable and LowerOffsetConstant instead. It is also worth introducing predicate functions IsLowerOffsetConstant and IsLowerOffsetVariable, as that makes the code easier to read.

dtarditi · 2019-07-17T19:51:32Z

+    //   They must have the same bitsize.
+    //   In this case, UpperOffsetExpr and LowerOffsetExpr should be both null.
+    // - If one or both of e2 and e3 are non-constant expressions, the range is Variable-sized.
+    //   TODO: elaborate more.


Please state the invariants for the representation.

@dtarditi For
I will add the following lines to the comment:

for constant-sized range:
More specifically: (UpperOffsetExpr == nullptr && LowerOffsetExpr == nullptr && BaseRangeKind == Kind::ConstantSized)

for variable-sized range:
More specifically: ((UpperOffsetExpr != nullptr || LowerOffsetExpr != nullptr) && BaseRangeKind == Kind::VariableSized)

Is that enough?

Yes, that will be good.

dtarditi · 2019-07-17T19:58:50Z

          }
-          if (UpperOffset < R.UpperOffset) {
+        } else if (LowerOffsetExpr && R.LowerOffsetExpr &&
+                   !EqualValue(S.Context, LowerOffsetExpr, R.LowerOffsetExpr, EquivExprs))


What about the case when the offset expressions are equal?

dtarditi · 2019-07-17T20:56:49Z

    // integer that will fit pointer width.
    void SplitIntoBaseAndOffset(Expr *E, Expr *&Base,
-                                llvm::APSInt &Offset) {
+                                llvm::APSInt &Offset, Expr *&OffsetExpr,


Instead of adding the extra parameter OnlyConstant, I suggest always letting this function always split expressions if possible and checking the results returned by the function. I think you will need to change the function to return a value indicating what it did.

- remove RangeType field from BaseRange - rename fields to better reflect their purpose - introduce predicate functions for lower and upper bound kinds

ppashakhanloo · 2019-07-18T20:36:42Z

@dtarditi I have made some new changes. The code is ready to be reviewed.

dtarditi

Looks very good! I have a few more suggested changes.

dtarditi · 2019-07-18T20:58:56Z

-            R->SetLower(LowerOffset);
-            R->SetUpper(UpperOffset);
-            return true;
+            if (LowerOffsetKind == BaseRange::Kind::ConstantSized && UpperOffsetKind == BaseRange::Kind::ConstantSized) {


It is OK for one of the upper bounds or lower bounds to be constant and the other to be variable. I think you should set the lower/upper bounds independently of each other:

if (LowerOffsetKind == BaseRange::Kind::ConstantSized) { … } else if (LowerOffsetKind == BaseRange::Kind::VariableSize) { … } else return BaseRange::KInd::Invalid

dtarditi · 2019-07-18T21:58:11Z

+          if (UpperOffsetConstant.getExtValue() == 0 &&
+              R.UpperOffsetConstant.getExtValue() == 0)
+            return ProofResult::True;
+          if (SignsMatch(UpperOffsetConstant, R.UpperOffsetConstant) &&


I don't think that you need to check that the signs match for the integer constants. We always represent integers using signed integers.

ppashakhanloo · 2019-07-19T00:11:12Z

@dtarditi Thank you very much for your comments. New changes are ready for review.

dtarditi

I have some additional suggestions.

dtarditi · 2019-07-19T17:48:26Z

            // R.LowerOffset is within this range, but R.UpperOffset is above the range
-            if (LowerOffset <= R.LowerOffset && R.LowerOffset < UpperOffset &&
-                UpperOffset < R.UpperOffset)
+            if (LowerOffsetConstant <= R.LowerOffsetConstant && R.LowerOffsetConstant < UpperOffsetConstant &&


I think you need to check that the two ranges are constant-sized here.

dtarditi · 2019-07-19T17:50:36Z

+    // Convert an expression E into a base and offset form.
    // - If E is pointer arithmetic involving addition or subtraction of a
    //   constant integer, return the base and offset.
+    // - If E is a pointer arithmetic involving addition or subtraction of


This comment needs to be updated. OnlyConstant is gone now.

dtarditi · 2019-07-19T17:51:56Z

  return p;
 }

+_Array_ptr<int> test_f70(int c) : byte_count(c);


Could you add some tests for _Nt_array_ptr too?

@dtarditi Yes, I added some tests for _Nt_array_ptr and will push the changes shortly. There are more tests (for both nt_array_ptr and array_ptr) in CheckedC repo.

ppashakhanloo · 2019-07-19T21:27:36Z

@dtarditi Thanks for the suggestions. I pushed the new changes to the branch.

ppashakhanloo · 2019-07-20T00:50:21Z

@dtarditi I improved the comments of various functions. I hope they are precise enough!

dtarditi

Looks good! Thank you.

…rectory. (#624) * Follow new guideline: Avoid `cd DIR && FOO` in RUN lines. Instead, put `FOO` on a separate run line. `cd` affects later RUN lines, and `cd DIR && FOO` could mislead the reader that it doesn't and that's why we needed to put both parts on one line. I added the proposed guideline to #346. I'm changing the existing tests before changing more tests to use `cd` as part of this PR. * Add `-o /dev/null` to clang commands that use `-` as input. * Add -working-directory to clang commands with named input files. * `cd` to a temporary directory for `3c -dump-stats` commands.

ppashakhanloo added 2 commits July 1, 2019 13:08

Forcing ProveMemoryAccess to only work with ConstantSizedRanges

758073b

ppashakhanloo changed the title ~~WIP: Extend static analyzer~~ Extend static analyzer Jul 2, 2019

dtarditi reviewed Jul 8, 2019

View reviewed changes

ppashakhanloo added 2 commits July 9, 2019 09:35

Rework the logic of InRange

d9b9595

Add todo item regarding the generalization of PartialOverlap

24a5b2e

ppashakhanloo changed the title ~~Extend static analyzer~~ Extend static bounds declaration checking Jul 10, 2019

ppashakhanloo added 5 commits July 10, 2019 15:23

Fix unsigned/signed bug

81869e6

Add tests for unsgined/signed bug

81aa370

Check if offset expressions are equal or not

d51f14b

Add expected-notes

d34661e

Correct expected-note lines

cdedc28

dtarditi reviewed Jul 17, 2019

View reviewed changes

ppashakhanloo added 6 commits July 17, 2019 16:17

Return kind of the created range

1772548

Make the code more readable

4e209bc

- remove RangeType field from BaseRange - rename fields to better reflect their purpose - introduce predicate functions for lower and upper bound kinds

Check lower and upper bounds kinds instead of range kinds

4bd4cb3

State the invariants for the representation

5bbf2a4

Add new field to Dump function

976f070

Clarify and rename some parts of the code

da9735a

dtarditi reviewed Jul 18, 2019

View reviewed changes

ppashakhanloo added 2 commits July 18, 2019 16:39

Check sign in IsEmpty and not when comparing bounds

918650a

Remove intermediate variable

18c512c

dtarditi reviewed Jul 19, 2019

View reviewed changes

ppashakhanloo added 2 commits July 19, 2019 14:11

Add tests for nt_array_ptr

3fae2bb

Add ConstantSized check and update comments

c17d964

Improve function comments

b8d1c79

ppashakhanloo mentioned this pull request Jul 23, 2019

Removing unnecessary dynamic_bounds_casts after teaching the compiler that 0<=unsigned integer microsoft/checkedc-parson#14

Open

dtarditi approved these changes Jul 24, 2019

View reviewed changes

dtarditi merged commit bf6b7ac into checkedc:master Jul 24, 2019

This was referenced Jul 24, 2019

Use facts about unsigned 0 when checking ranges. #599

Closed

Support variable sized ranges when checking out-of-bounds accesses #640

Open

secure-sw-dev-bot mentioned this pull request Jan 16, 2022

Extend static bounds declaration checking checkedc/checkedc-llvm-project#620

Closed

Conversation

ppashakhanloo commented Jul 2, 2019

Uh oh!

dtarditi left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dtarditi left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ppashakhanloo commented Jul 18, 2019

Uh oh!

dtarditi left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ppashakhanloo commented Jul 19, 2019

Uh oh!

dtarditi left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ppashakhanloo commented Jul 19, 2019

Uh oh!

ppashakhanloo commented Jul 20, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

dtarditi left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

ppashakhanloo commented Jul 20, 2019 •

edited

Loading