Explain bounds proof failure caused by free variables in inferred/declared bounds #903

dopelsunce · 2020-08-18T18:00:06Z

This PR enables the compiler to emit an error when a free variable (defined below) is found in the declared/inferred bounds on bounds assignments, and passing arguments. A note is printed for each free variable found.

Free variables w.r.t. expressions

Assume the helper function VarSet(E) returns the set of variables in expression E.

Given two expressions SrcExpr and DstExpr, a set of equivalent expression sets EQ. A variable V in VarSet(SrcExpr) is free if:

(V does not equal to some constant) V is not an integer type, or there is no set in EQ that contains a constant and V; and,
(V does not have an alias in VarSet(DstExpr)) For each U in VarSet(DstExpr), there is not set in EQ that contains both V and U.

Free variables w.r.t. declared/inferred bounds

We extend the above definition for free variables with respect to the lower (or upper bounds) of the declared bounds (or inferred bounds). In other words, a variable used by the declared lower bounds may be free even if it is used in the inferred upper bounds.

Affected cases

Free variable is detected in the following cases:

On variable initialization or assignment, inferred bounds do not imply declared bounds. Error msg: "it is not possible to prove that the inferred bounds of p imply the declared bounds of p after ...".
On passing arguments, the inferred bounds do not imply the expected argument bounds. Error msg: "it is not possible to prove argument meets declared bounds for n-th parameter"

Note: we do not check free variables in static bounds cast.

Note for each free variable

We use the template: "note: the declared/inferred bounds use the value of the variable 'q', and there is no relational information between 'q' and any of the variables used by the inferred/declared bounds".

… bounds

* Simplify logic and improve comments

…der declared bounds as well

kkjeer · 2020-09-04T21:28:19Z

clang/lib/Sema/SemaBounds.cpp

@@ -1699,7 +1993,14 @@ namespace {
        llvm::outs() << "\nSource range:";
        SrcRange.Dump(llvm::outs());
 #endif
-        ProofResult R = SrcRange.InRange(DeclaredRange, Cause, EquivExprs, Facts);
+        // For static bounds cast, we do not check free variables.


This comment is somewhat confusing since it's not clear that checking static bounds cast will always pass a nullptr EquivExprs parameter. I suggest moving this logic into the InRangeWithFreeVars function, so that in InRangeWithFreeVars, if EquivExprs is null, simply return InRange without checking any free variables.

clang/lib/Sema/SemaBounds.cpp

dtarditi

Thanks for the work. I have another suggestion in addition to @kkjeer's suggestions. This could be done as follow-up work.

dtarditi · 2020-09-04T22:44:40Z

clang/test/CheckedC/static-checking/bounds-decl-checking-bsi.c

@@ -64,7 +66,9 @@ _Array_ptr<int> f14(unsigned num) {
 }

 _Array_ptr<int> f15(unsigned num1, unsigned num2){
-  _Array_ptr<int> p : byte_count(num1) = test_f13(num2); // expected-warning {{cannot prove declared bounds for 'p' are valid after initialization}} \
+  _Array_ptr<int> p : byte_count(num1) = test_f13(num2); // expected-error {{it is not possible to prove that the inferred bounds of 'p' imply the declared bounds of 'p' after initialization}} \
+                                                         // expected-note {{the declared upper bounds use the value of the variable 'num1', and there is no relational information between 'num1' and any of the variables used by the inferred upper bounds}} \


The notes about the bounds should be displayed before the note about lack of relational information. This will be confusing for a programmer to follow. This can be addressed in follow-up work.

Thanks for the suggestion @dtarditi. Created issue #912 to track this.

kkjeer · 2020-09-05T00:45:18Z

clang/lib/Sema/SemaBounds.cpp

                            // the source bounds.
+      HasFreeVariables = 0x200, // Source or destination has free variables.


Nit: change this value to 0x100 and remove trailing comma.

… for the declared bounds (#913)

* Fix issue #909 and #911 by ignoring casts in EquivExprs * Replace IgnoreCasts with IgnoreParenCasts and add test cases

dtarditi

The algorithm seems to have subtle complications that I didn't realize when we first discussed the idea. The basic idea is just to look at sets of variables, but there are subtleties involving expressions using those variables. Expressions that use those variables may have relational information between each other and may appear in equivalent expression sets. This relational information is being lost when we boil things down to just sets of variables.

@kkjeer and @dopelsunce, it may be worth discussing next steps before making changes. I think this may address some of the error messages that we're seeing be generated now.

clang/lib/Sema/SemaBounds.cpp

dtarditi · 2020-10-22T21:31:41Z

clang/lib/Sema/SemaBounds.cpp

+                                      FreeVariablePosition Pos2,
+                                      EquivExprSets *EquivExprs,
+                                      FreeVariableListTy &FreeVars) {
+        // If E1 or E2 accesses memory via poiter, we skip because we cannot


Typo in comment: poit->pointer.

dtarditi · 2020-10-22T22:01:56Z

clang/lib/Sema/SemaBounds.cpp

@@ -1172,6 +1270,43 @@ namespace {
        return ProofResult::Maybe;
      }

+      // InRangeWithFreeVars is the same as InRange, but gathers free variables


I think this function needs a better comment. This function is an extension of InRange. It tries to prove that R is within this range. If R is provably not within this range, it sets Cause to explain reasons why. This function takes into account variables that are free in one of the lower/upper bounds expressions that are being compared.

InRange compares the lower bounds from the two ranges and then the upper bounds from the two ragnes. Given a pair of lower (or upper) bounds expressions, a variable is free if it appears in one expression but does not appear in the other expression, and there is no known relation between that variable and variables in the other expression. In that situation, it is impossible to prove that the comparison is true, given the facts that the compiler has.

dtarditi · 2020-10-22T22:12:08Z

clang/lib/Sema/SemaBounds.cpp

+                          EquivExprSets *EquivExprs,
+                          std::pair<ComparisonSet, ComparisonSet> &Facts,
+                          FreeVariableListTy &FreeVariables) {
+        // If we do not have equivalence relational information (EquivExprs


I'd reword this comment:

If there is no relational information at all, then the compiler didn't attempt to gather any. To avoid confusing programmers, don't try to take free variables into account. There may be some simple fact the compiler doesn't know that would cause confusion about why the compiler is claiming that no fact is known.

@kkjeer, could you update this comment? Thanks.

dtarditi · 2020-10-23T03:45:32Z

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

@@ -426,7 +426,7 @@ void f42(void) {
 // CHECK: | `-DeclRefExpr {{0x[0-9a-f]+}} '_Array_ptr<int>' lvalue Var {{0x[0-9a-f]+}} 'p' '_Array_ptr<int>'
 // CHECK: `-IntegerLiteral {{0x[0-9a-f]+}} 'int' 1

-  _Array_ptr<int> r : count(1) = &p[0];
+  _Array_ptr<int> r : count(1) = &p[0]; // expected-error {{it is not possible to prove that the inferred bounds of 'r' imply the declared bounds of 'r' after initialization}}


This seems unexpected to me that we can no longer prove this. We seem to be missing the fact that r equals p.

The set EquivExprs contains { (_Array_ptr<int>)(&p[0]), r }. Without the changes in this PR, there would be a warning: "cannot prove declared bounds for 'r' are valid after initialization" since the bases p and r of the inferred bounds (p, p + 1) and declared bounds (r, r + 1) are not equal.

dtarditi · 2020-10-23T05:19:03Z

clang/lib/Sema/SemaBounds.cpp

+        return HasFreeVariables;
+      }
+
+      // AddFreeVariables maps each free variable in SrcVars w.r.t. DstVars


This comment isn't very clear. Given two sets of variables SrcVars and DstVars, for each variable v in SrcVars, it determines whether v occurs in DstVars. There are also some side conditions about v with respect to EquivExprs.

dtarditi · 2020-10-23T05:53:14Z

clang/lib/Sema/SemaBounds.cpp

+          return false;
+
+        bool HasFreeVariables = false;
+        EqualExprTy Vars1 = CollectVariableSet(S, E1);


This algorithm isn't correct because of its handling of equivalent expression sets. With equivalent expression sets, you may have two expressions that are known to be equal, such as "a.f == b.f", even though there is no equality of the variables used in the expressions. We don't know that a == b, for example.

We may need to generalize the notion of a variable v having relational information to another variable y. We need to check that there no expressions constructed from v or y that have relational information either.

dtarditi · 2020-10-23T06:00:37Z

clang/lib/Sema/SemaBounds.cpp

+
+        // EquivVars holds sets of DeclRefExpr and IntegerLiteral filtered from
+        // EquivExprs.
+        EquivExprSets EquivVars;


An implication of my comment is that we shouldn't be filtering EquivVars. We could be removing expressions that have equality relationships and that use variables.

dtarditi · 2020-10-23T06:04:09Z

clang/lib/Sema/SemaBounds.cpp

+      //   EquivExprs that contains both V and a constant (i.e. an integer-typed
+      //   value); and
+      //   2. for each variable U in DstVars, there is not set in EquivExprs
+      //   that contains both V and U.


I think condition 2 needs to be amended to work in terms of uses of variables. There is not a set in EquivExprs that contains two different expressions, where one expression uses V and the other expression uses U.

dtarditi · 2020-10-23T06:31:04Z

clang/include/clang/Basic/DiagnosticSemaKinds.td

+  def note_free_variable_decl_or_inferred : Note<
+    "the %select{declared|inferred}0 %select{lower |upper |}1bounds use the value "
+    "of the variable '%2', and there is no relational information between '%2' "
+    "and any of the variables used by the %select{inferred|declared}0 "


This may need to be reworded. There is no relational information involving v and any of the expressions used by the other bounds. Perhaps something along the lines of

"the %select{declared|inferred}0 %slect{lower | upper |}bound use the variable %2' and there is no relational information involving '%2' and any of expressions used by the %select{inferred|declared}0 "

* Change IsEqualToConstant to search for an rvalue cast of a variable * Add FindVarRelationship method to search for an indirect relationship between variables * Remove EquivVars set that filters out everything except DeclRefExprs and IntegerLiterals * Remove expected free variables errors where there are indirect variable relationships * Update note messages to mention lack of relational information between a free variable and expressions * Remove comma from expected notes * Fix comments * Make free variable-related methods non-static * Move top-level free variable method CheckFreeVarInExprs above other free variable methods * Fix comment typo * Update CheckFreeVarsInExprs comment Co-authored-by: Katherine Kjeer <[email protected]>

This test was originally in the checkedc/tests/typechecking directory but was moved to checkedc-clang since it tests compiler implementation details (diagnostic messages).

dtarditi

There are a few suggestions around comments that I'd like to see resolved. Also, there is a merge conflict according to GitHub. Once both of these are done, I'll approve the merge.

dtarditi · 2021-01-22T05:43:40Z

clang/lib/Sema/SemaBounds.cpp

+                          EquivExprSets *EquivExprs,
+                          std::pair<ComparisonSet, ComparisonSet> &Facts,
+                          FreeVariableListTy &FreeVariables) {
+        // If we do not have equivalence relational information (EquivExprs


@kkjeer, could you update this comment? Thanks.

dtarditi · 2021-01-22T05:44:24Z

clang/lib/Sema/SemaBounds.cpp

@@ -1172,6 +1270,43 @@ namespace {
        return ProofResult::Maybe;
      }

+      // InRangeWithFreeVars is the same as InRange, but gathers free variables


@kkjeer, could you update this comment?

dtarditi · 2021-01-22T05:46:41Z

clang/lib/Sema/SemaBounds.cpp

+    const EqualExprTy &GetVariableList() const { return VariableList; }
+
+    bool VisitDeclRefExpr(DeclRefExpr *E) {
+      if (!EqualExprsContainsExpr(SemaRef, VariableList, E, nullptr)) {


@kkjeer, is my comment still accurate? If so, could you leave a comment in the code about the algorithm being quadratic. I don't like to leave quadratic algorithms around in a compiler without calling them out.

…into non-equiv-exprs-in-bounds # Conflicts: # clang/lib/Sema/SemaBounds.cpp

We don't think it is important to the test, and since checkedc#903, it is causing a compiler error (which was previously a warning).

dopelsunce and others added 30 commits July 29, 2020 15:13

Target error message at assignments

5722d2d

Target subexpressions to blame on error messages for unknown inferred…

021e928

… bounds

Update tests to reflect fine-grained error messages

354a859

Update comments

2a82843

Remove unused variable

af5f9c3

* Also add (V, E) to BlameAssignments if E modifies the bounds of V

f6f3af5

* Simplify logic and improve comments

Update tests to reflect the missing case

7296d8b

Restore whitespace

70aa057

Restore whitespace

3abacfd

Restore whitespace

b22bd1a

Restore whitespace

29926f2

Refactor and address the missing case; fix tests

3317bce

Clarify the logic in BlameAssignmentWithinStmt

ff01d32

Reorder BoundsDeclarationCheck enum and update comments

d321731

Gather proof failure cause and new error message

6b84507

Update diagnostic messages

729e959

Convert offset constant to count

a22825d

Simplify error messages

edb3309

New error message

3df3205

Find free variables; use const modifier for some parameters

62c2af8

Clean up and small fix

13ecbba

Check equal variable

5c5729f

Traverse ImplicitCastExpr instead of DeclRefExpr

aba5112

Revert changes

84781f7

Remove extra changes

69c8870

Add wrapper for ProofBoundsDeclValidity

a1e0ebb

Add comments

f5be4c2

More comments

cfa45ef

Fix CollectVariableSet Helper

07f9d30

Exclude variables that equal to a constant from free variables; consi…

caf29d3

…der declared bounds as well

kkjeer reviewed Sep 4, 2020

View reviewed changes

dtarditi reviewed Sep 4, 2020

View reviewed changes

dopelsunce added 2 commits September 4, 2020 19:36

No free variable detection for static pointer casts and other cleanup

389e118

Clean up

7a0c884

kkjeer reviewed Sep 5, 2020

View reviewed changes

Minor fix

b20f1e4

kkjeer mentioned this pull request Sep 5, 2020

Add expected errors in widened-bounds-semantic-compare #913

Merged

Add expected errors where the compiler is able to create a base range…

6dba79a

… for the declared bounds (#913)

kkjeer mentioned this pull request Sep 15, 2020

Fix compile errors related to free variables microsoft/checkedc-llvm-test-suite#101

Merged

dopelsunce mentioned this pull request Oct 7, 2020

Free variables: fix #909 and #911 by ignoring casts in EquivExprs #919

Merged

Free variables: fix #909 and #911 by ignoring casts in EquivExprs (#919)

867cf58

* Fix issue #909 and #911 by ignoring casts in EquivExprs * Replace IgnoreCasts with IgnoreParenCasts and add test cases

dtarditi reviewed Oct 23, 2020

View reviewed changes

kkjeer and others added 2 commits January 14, 2021 15:51

Add free-variables.c test to CheckedC/static-checking

7db553c

This test was originally in the checkedc/tests/typechecking directory but was moved to checkedc-clang since it tests compiler implementation details (diagnostic messages).

dtarditi reviewed Jan 22, 2021

View reviewed changes

Katherine Kjeer added 3 commits January 21, 2021 23:42

Update InRangeWithFreeVars comment

c934e70

Update more InRangeWithFreeVars comments

7352252

Update EqualExprsContainsExpr comment

d46fc90

kkjeer mentioned this pull request Jan 22, 2021

Remove quadratic algorithm in CollectVariableSetHelper #966

Open

Katherine Kjeer added 2 commits January 22, 2021 00:13

Add TODO for quadratic algorithm in CollectVariableSetHelper

323e8ee

Merge branch 'master' of https://github.com/Microsoft/checkedc-clang …

ab80d34

…into non-equiv-exprs-in-bounds # Conflicts: # clang/lib/Sema/SemaBounds.cpp

kkjeer merged commit b7be752 into master Jan 26, 2021

kkjeer deleted the non-equiv-exprs-in-bounds branch January 26, 2021 01:02

mattmccutchen-cci mentioned this pull request Jan 28, 2021

Merge from Microsoft 2021-01-27 correctcomputation/checkedc-clang#407

Merged

john-h-kastner mentioned this pull request Jan 29, 2021

Unexpected bounds error after PR #903 #969

Closed

mattmccutchen-cci mentioned this pull request Feb 4, 2021

Wrong error from #903 when passing _Assume_bounds_cast directly to function with itype #974

Closed

This was referenced Jan 15, 2022

Add and update tests for checking free variables checkedc/checkedc-fork#417

Closed

Explain bounds proof failure caused by free variables in inferred/declared bounds checkedc/checkedc-llvm-project#899

Closed

		// the source bounds.
		HasFreeVariables = 0x200, // Source or destination has free variables.

Explain bounds proof failure caused by free variables in inferred/declared bounds #903

Explain bounds proof failure caused by free variables in inferred/declared bounds #903

Uh oh!

Conversation

dopelsunce commented Aug 18, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Free variables w.r.t. expressions

Free variables w.r.t. declared/inferred bounds

Affected cases

Note for each free variable

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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!

dtarditi left a comment

Choose a reason for hiding this comment

Uh oh!

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!

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!

Uh oh!

dopelsunce commented Aug 18, 2020 •

edited

Loading