Bounds declaration checking involving signed->unsigned conversion

[dtarditi]

When malloc is used, there can be implicit conversions from signed to unsigned integers for arguments to malloc. These implicit conversions are causing checking of bounds declarations to warn that it cannot prove the validity of bounds declarations.

The following code shows the issue:

_Itype_for_any(T) void *alloc(unsigned int len): itype(_Array_ptr<T>) byte_count(len);
void test1(_Array_ptr<int> ip : byte_count(len), 
            int len) _Checked {
  ip = alloc<int>(len);
}

The Checked C compiler with changes for issue #594 generates the following warning:

tmp.c:6:6: warning: cannot prove declared bounds for ip are valid after
      assignment [-Wcheck-bounds-decls-checked-scope]
  ip = alloc<int>(len);
  ~~ ^ ~~~~~~~~~~~~~~~
tmp.c:6:3: note: (expanded) declared bounds are 'bounds((_Array_ptr<char>)ip,
      (_Array_ptr<char>)ip + len)'
  ip = alloc<int>(len);
  ^
tmp.c:6:8: note: (expanded) inferred bounds are 'bounds((_Array_ptr<char>)value
      of alloc(len), (_Array_ptr<char>)value of alloc(len) + (unsigned int)len)'
  ip = alloc<int>(len);
       ^~~~~~~~~~~~~~~
1 warning generated.

The difference is that the inferred bounds have an unsigned cast, while the declared bounds do not.

I believe the inferred bounds do imply the validity of the declared bounds. When len is < 0, the declared bounds are an empty range. Any bounds can imply the empty range. When len is > 0, the inferred upper bound and the declared upper bound evaluate to the same value, even when the inferred upper bound has a signed->unsigned cast.

This suggests add a rule for bounds checking . If an expression e1 has an array_ptr type, e2 has a signed integer type SI and type UI is the unsigned integer type with the same size SI, then bounds(e1, e1 + (UI) e2) implies the validity of bounds(e1, e1 + e2).