Description
This issue was copied from checkedc/checkedc-clang#693
In the following code, a checked array is passed to a function sum, which declares wider bounds than the original declared bounds for the array.
#include <stdchecked.h>
#include <stdio_checked.h>
int sum(array_ptr<int> a : count(n+5), int n)
{
int i, s = 0;
for( i = 0; i < n+5; i++ )
s += a[i];
return s;
}
int foo(array_ptr<int> b: count(m), int m)
{
return sum(b, m);
}
int main()
{
int a checked[10];
int i;
for( i = 0; i < 10; i++ )
a[i] = i;
#ifdef DIRECT_CALL
printf("%d\n", sum(a, 10));
#else
printf("%d\n", foo(a, 10));
#endif
return 0;
}If we directly call the sum function (clang 009.c -DDIRECT_CALL), the following error will be given, which is the expected behavior (destination bounds are wider than the source bounds).
009.c:16:16: warning: cannot prove argument meets declared bounds for 1st parameter [-Wcheck-bounds-decls-unchecked-scope]
return sum(b, m);
^
009.c:16:16: note: (expanded) expected argument bounds are 'bounds(b, b + m + 5)'
009.c:16:16: note: (expanded) inferred bounds are 'bounds(b, b + m)'
return sum(b, m);
^
009.c:28:24: error: argument does not meet declared bounds for 1st parameter
printf("%d\n", sum(a, 10));
^
009.c:28:24: note: destination bounds are wider than the source bounds
009.c:28:24: note: destination upper bound is above source upper bound
009.c:28:24: note: (expanded) expected argument bounds are 'bounds(a, a + 10 + 5)'
009.c:28:24: note: (expanded) inferred bounds are 'bounds(a, a + 10)'
printf("%d\n", sum(a, 10));
^
1 warning and 1 error generated.
However, if we pass the pointer to a proxy function that only copies the incoming bounds, and calls the sum function, the compiler cannot prove that bounds are definitely wider and only gives us a warning. Compiling with clang 009.c, generates:
009.c:16:16: warning: cannot prove argument meets declared bounds for 1st parameter [-Wcheck-bounds-decls-unchecked-scope]
return sum(b, m);
^
009.c:16:16: note: (expanded) expected argument bounds are 'bounds(b, b + m + 5)'
009.c:16:16: note: (expanded) inferred bounds are 'bounds(b, b + m)'
return sum(b, m);
^
1 warning generated.
If I understand correctly, the current bounds checking logic, to be able to prove that b + m + 5 is larger than b + m, needs to have m + 5 > m in the collected fact list, which might be missing in this particular code. I suspect that is a likely reason that the compiler says "Maybe" as the proof result. But as David pointed out, this could be related to associativity and problem of what is it that is being compared exactly, as the parentheses are ignored/missing.