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

clang/include/clang/Basic/DiagnosticSemaKinds.td

@@ -10172,6 +10172,23 @@ def err_bounds_type_annotation_lost_checking : Error<
     "%select{assignment|decrement|increment|initialization|statement}0">,
     InGroup<CheckBoundsDeclsChecked>;
 
+  def error_bounds_declaration_unprovable : Error<
+    "it is not possible to prove that the inferred bounds of %1 "
+    "imply the declared bounds of %1 after "
+    "%select{assignment|decrement|increment|initialization|statement}0">;
+
+  def note_free_variable_decl_or_inferred : Note<
+    "the %select{declared|inferred}0 %select{lower |upper |}1bounds use the "
+    "variable '%2' and there is no relational information involving '%2' "
+    "and any of the expressions used by the %select{inferred|declared}0 "
+    "%select{lower |upper |}1bounds">;
+
+  def note_free_variable_in_expected_args : Note<
+    "the %select{expected argument|inferred}0 %select{lower |upper |}1bounds use the "
+    "variable '%2' and there is no relational information involving '%2' "
+    "and any of the expressions used by the %select{inferred|expected argument}0 "
+    "%select{lower |upper |}1bounds">;
+
   def error_bounds_declaration_invalid : Error<
     "declared bounds for %1 are invalid after "
     "%select{assignment|decrement|increment|initialization|statement}0">;
@@ -10203,6 +10220,9 @@ def err_bounds_type_annotation_lost_checking : Error<
    "argument must be a non-modifying expression because %ordinal0 parameter "
    "is used in a bounds expression">;
 
+  def error_argument_bounds_unprovable : Error<
+    "it is not possible to prove argument meets declared bounds for %ordinal0 parameter">;
+
   def warn_argument_bounds_invalid : Warning<
     "cannot prove argument meets declared bounds for %ordinal0 parameter">,
     InGroup<CheckBoundsDeclsUnchecked>;

clang/lib/AST/CanonBounds.cpp

@@ -336,7 +336,7 @@ Result Lexicographic::CompareExpr(const Expr *Arg1, const Expr *Arg2) {
 #include "clang/AST/StmtNodes.inc"
        llvm_unreachable("cannot compare a statement");  
      case Expr::PredefinedExprClass: Cmp = Compare<PredefinedExpr>(E1, E2); break;
-     case Expr::DeclRefExprClass: return Compare<DeclRefExpr>(E1, E2);
+     case Expr::DeclRefExprClass: Cmp = Compare<DeclRefExpr>(E1, E2); break;
      case Expr::IntegerLiteralClass: return Compare<IntegerLiteral>(E1, E2);
      case Expr::FloatingLiteralClass: return Compare<FloatingLiteral>(E1, E2);
      case Expr::ImaginaryLiteralClass: break;

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

@@ -616,9 +616,11 @@ void assign7(
   // Observed bounds context before assignment: { a => bounds(a, a + 1), b => bounds(a, a + 1), c => bounds(a, a + 1) }
   // Original value of a: b
   // Observed bounds context after assignment:  { a => bounds(b, b + 1), b => bounds(b, b + 1), c => bounds(b, b + 1) }
-  a = c; // expected-warning {{cannot prove declared bounds for 'a' are valid after assignment}} \
-         // expected-warning {{cannot prove declared bounds for 'b' are valid after assignment}} \
-         // expected-warning {{cannot prove declared bounds for 'c' are valid after assignment}} \
+  a = c; // expected-error {{it is not possible to prove that the inferred bounds of 'a' imply the declared bounds of 'a' after assignment}} \
+         // expected-error {{it is not possible to prove that the inferred bounds of 'b' imply the declared bounds of 'b' after assignment}} \
+         // expected-error {{it is not possible to prove that the inferred bounds of 'c' imply the declared bounds of 'c' after assignment}} \
+         // expected-note 3 {{the declared bounds use the variable 'a' and there is no relational information involving 'a' and any of the expressions used by the inferred bounds}} \
+         // expected-note 3 {{the inferred bounds use the variable 'b' and there is no relational information involving 'b' and any of the expressions used by the declared bounds}} \
          // expected-note 3 {{(expanded) inferred bounds are 'bounds(b, b + 1)'}}
   // CHECK: Statement S:
   // CHECK-NEXT: BinaryOperator {{.*}} '='

clang/test/CheckedC/inferred-bounds/compound-literals.c

@@ -140,4 +140,4 @@ void f2(_Array_ptr<struct S> arr : count(1), struct S s) {
   // CHECK:  |-UnaryOperator {{0x[0-9a-f]+}} '_Array_ptr<struct S>' prefix '&' cannot overflow
   // CHECK:  | `-BoundsValueExpr {{0x[0-9a-f]+}} 'struct S':'struct S' lvalue _BoundTemporary
   // CHECK:  `-IntegerLiteral {{0x[0-9a-f]+}} 'int' 1
-}
+}

clang/test/CheckedC/inferred-bounds/member-reference.c

@@ -10,8 +10,7 @@
 //
 // This line is for the clang test infrastructure:
 // RUN: %clang_cc1 -fcheckedc-extension -fdump-inferred-bounds -verify -verify-ignore-unexpected=warning -verify-ignore-unexpected=note -fdump-inferred-bounds %s | FileCheck %s
-// expected-no-diagnostics
-
+
 struct S1 {
   _Array_ptr<int> p : count(len);
   int len;
@@ -101,7 +100,7 @@ void f1(struct S1 a1, struct S2 b2) {
 int global_arr1[5];
 void f2(struct S1 a3) {
   // TODO: need bundled block.
-  a3.p = global_arr1;
+  a3.p = global_arr1; // expected-error {{it is not possible to prove that the inferred bounds of a3.p imply the declared bounds of a3.p after assignment}}
   a3.len = 5;
 
 // CHECK: BinaryOperator {{0x[0-9a-f]+}} '_Array_ptr<int>' '='
@@ -265,7 +264,7 @@ void f10(struct Interop_S1 a1, struct Interop_S2 b2,
 _Checked void f11(struct Interop_S1 a1, struct Interop_S2 b2,
                   struct Interop_S4 c3) {
   _Array_ptr<int> ap : count(a1.len) = a1.p;
-  
+
 // CHECK: VarDecl {{.*}}  '_Array_ptr<int>' cinit
 // CHECK: |-CountBoundsExpr {{0x[0-9a-f]+}} <col:24, col:36> 'NULL TYPE' Element
 // CHECK: | `-ImplicitCastExpr {{0x[0-9a-f]+}} <col:30, col:33> 'int' <LValueToRValue>
@@ -348,7 +347,7 @@ int global_arr2 _Checked[5];
 
 void f12(struct Interop_S1 a1) {
   // TODO: need bundled block.
-  a1.p = global_arr2;
+  a1.p = global_arr2; // expected-error {{it is not possible to prove that the inferred bounds of a1.p imply the declared bounds of a1.p after assignment}}
   a1.len = 5;
 }
 
@@ -381,7 +380,7 @@ void f12(struct Interop_S1 a1) {
 
 _Checked void f13(struct Interop_S1 a1) {
   // TODO: need bundled block.
-  a1.p = global_arr2;
+  a1.p = global_arr2; // expected-error {{it is not possible to prove that the inferred bounds of a1.p imply the declared bounds of a1.p after assignment}}
   a1.len = 5;
 }
 

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

@@ -1,12 +1,10 @@
 // Tests for bounds widening of _Nt_array_ptr's using function to semantically
 // compare two expressions.
 //
-// RUN: %clang_cc1 -fdump-widened-bounds -verify -verify-ignore-unexpected=note -verify-ignore-unexpected=warning %s 2>&1 | FileCheck %s
-
-// expected-no-diagnostics
+// RUN: %clang_cc1 -fdump-widened-bounds -verify -verify-ignore-unexpected=note -verify-ignore-unexpected=warning %s | FileCheck %s
 
 void f1(int i) {
-  _Nt_array_ptr<char> p : bounds(p, p + i) = "a";
+  _Nt_array_ptr<char> p : bounds(p, p + i) = "a"; // expected-error {{it is not possible to prove that the inferred bounds of 'p' imply the declared bounds of 'p' after initialization}}
 
   if (*(i + p)) {}
 
@@ -16,7 +14,7 @@ void f1(int i) {
 }
 
 void f2(int i, int j) {
-  _Nt_array_ptr<char> p : bounds(p, p + (i + j)) = "a";
+  _Nt_array_ptr<char> p : bounds(p, p + (i + j)) = "a"; // expected-error {{it is not possible to prove that the inferred bounds of 'p' imply the declared bounds of 'p' after initialization}}
 
   if (*(p + (j + i))) {}
 
@@ -26,7 +24,7 @@ void f2(int i, int j) {
 }
 
 void f3(int i, int j) {
-  _Nt_array_ptr<char> p : bounds(p, p + (i * j)) = "a";
+  _Nt_array_ptr<char> p : bounds(p, p + (i * j)) = "a"; // expected-error {{it is not possible to prove that the inferred bounds of 'p' imply the declared bounds of 'p' after initialization}}
 
   if (*(p + (j * i))) {}
 
@@ -66,7 +64,7 @@ void f6(int i, int j) {
 }
 
 void f7(int i, int j) {
-  _Nt_array_ptr<char> p : bounds(p, p + i * j) = "a";
+  _Nt_array_ptr<char> p : bounds(p, p + i * j) = "a"; // expected-error {{it is not possible to prove that the inferred bounds of 'p' imply the declared bounds of 'p' after initialization}}
 
   if (*(p + i + j)) {}
 

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

@@ -169,7 +169,7 @@ void f8() {
 }
 
 void f9(int i) {
-  _Nt_array_ptr<char> p : bounds(p, p + i) = "a";
+_Nt_array_ptr<char> p : bounds(p, p + i) = "a"; // expected-error {{it is not possible to prove that the inferred bounds of 'p' imply the declared bounds of 'p' after initialization}}
 
   if (*p)
     if (*(p + i))
@@ -209,7 +209,7 @@ void f10(int i) {
 }
 
 void f11(int i, int j) {
-  _Nt_array_ptr<char> p : bounds(p + i, p + j) = "a";
+  _Nt_array_ptr<char> p : bounds(p + i, p + j) = "a"; // expected-error {{it is not possible to prove that the inferred bounds of 'p' imply the declared bounds of 'p' after initialization}}
 
   if (*(p + j)) {
     i = 0; // expected-error {{inferred bounds for 'p' are unknown after assignment}}
@@ -307,7 +307,7 @@ void f14(int i) {
 }
 
 void f15(int i) {
-  _Nt_array_ptr<char> p : bounds(p, p - i) = "a";
+  _Nt_array_ptr<char> p : bounds(p, p - i) = "a"; // expected-error {{it is not possible to prove that the inferred bounds of 'p' imply the declared bounds of 'p' after initialization}}
   if (*(p - i)) {}
 
 // CHECK: In function: f15
@@ -349,8 +349,8 @@ void f15(int i) {
 }
 
 void f16(_Nt_array_ptr<char> p : bounds(p, p)) {
-  _Nt_array_ptr<char> q : bounds(p, p) = "a";
-  _Nt_array_ptr<char> r : bounds(p, p + 1) = "a";
+  _Nt_array_ptr<char> q : bounds(p, p) = "a"; // expected-error {{it is not possible to prove that the inferred bounds of 'q' imply the declared bounds of 'q' after initialization}}
+  _Nt_array_ptr<char> r : bounds(p, p + 1) = "a"; // expected-error {{it is not possible to prove that the inferred bounds of 'r' imply the declared bounds of 'r' after initialization}}
 
   if (*(p))
     if (*(p + 1))
@@ -370,8 +370,8 @@ void f16(_Nt_array_ptr<char> p : bounds(p, p)) {
 }
 
 void f17(char p _Nt_checked[] : count(1)) {
-  _Nt_array_ptr<char> q : bounds(p, p + 1) = "a";
-  _Nt_array_ptr<char> r : bounds(p, p) = "a";
+  _Nt_array_ptr<char> q : bounds(p, p + 1) = "a"; // expected-error {{it is not possible to prove that the inferred bounds of 'q' imply the declared bounds of 'q' after initialization}}
+  _Nt_array_ptr<char> r : bounds(p, p) = "a"; // expected-error {{it is not possible to prove that the inferred bounds of 'r' imply the declared bounds of 'r' after initialization}}
 
   if (*(p))
     if (*(p + 1))

clang/test/CheckedC/regression-cases/bug_457_null_ptr_warning.c

@@ -1,5 +1,5 @@
 //
-// These is a regression test case for 
+// These is a regression test case for
 // https://github.com/Microsoft/checkedc-clang/issues/457
 //
 // This test checks that bounds declaration checking does not
@@ -20,9 +20,10 @@ static void myfunc2(_Array_ptr<int> data : count(len), int len) {
 
 int main(void) {
   int a _Checked[5];
-  myfunc1(a, 0);  // expected-warning {{cannot prove argument meets declared bounds}} \
-                  // expected-note {{expected argument bounds}} \
-                  // expected-note {{inferred bounds}}
+  myfunc1(a, 0);  // expected-error {{it is not possible to prove argument meets declared bounds for 1st parameter}} \
+                  // expected-note {{the inferred bounds use the variable 'a' and there is no relational information involving 'a' and any of the expressions used by the expected argument bounds}} \
+                  // expected-note {{(expanded) expected argument bounds are 'bounds((_Array_ptr<char>)0, (_Array_ptr<char>)0 + 5)'}} \
+                  // expected-note {{(expanded) inferred bounds are 'bounds(a, a + 5)'}}
   myfunc2(0, 0);
   return 0;
 }

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

@@ -50,7 +50,9 @@ _Array_ptr<int> f11(unsigned num) {
 }
 
 _Array_ptr<int> f12(unsigned num1, unsigned num2){
-  _Array_ptr<int> p : count(num1) = test_f10(num2); // expected-warning {{cannot prove declared bounds for 'p' are valid after initialization}} \
+  _Array_ptr<int> p : count(num1) = test_f10(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 variable 'num1' and there is no relational information involving 'num1' and any of the expressions used by the inferred upper bounds}} \
+                                                    // expected-note {{the inferred upper bounds use the variable 'num2' and there is no relational information involving 'num2' and any of the expressions used by the declared upper bounds}} \
                                                     // expected-note {{(expanded) declared bounds are 'bounds(p, p + num1)'}} \
                                                     // expected-note {{(expanded) inferred bounds are 'bounds(value of test_f10(num2), value of test_f10(num2) + num2)'}}
   return p;
@@ -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 variable 'num1' and there is no relational information involving 'num1' and any of the expressions used by the inferred upper bounds}} \
+                                                         // expected-note {{the inferred upper bounds use the variable 'num2' and there is no relational information involving 'num2' and any of the expressions used by the declared upper bounds}} \
                                                          // expected-note {{(expanded) declared bounds are 'bounds((_Array_ptr<char>)p, (_Array_ptr<char>)p + num1)'}} \
                                                          // expected-note {{inferred bounds are 'bounds((_Array_ptr<char>)value of test_f13(num2), (_Array_ptr<char>)value of test_f13(num2) + num2)'}}
   return p;