Analysis of the Remaining Warnings

After inspecting the remaining compiler warnings in checkedc-parson, we discovered the causes of them as described below.

1. More General Bound Representation is Needed

The bound representation is still not as general as we need. Currently, a bound consists of a Base and an Offset both of which are expressions. When splitting an expression into Base and Offset, the sub-expression that is a pointer will be the Base, and the rest will serve as the Offset. However, this can lead to false warnings. For instance, in the following piece of code,

void f(nt_array_ptr<const char> string : bounds(string, string + string_len), size_t string_len) {
  nt_array_ptr<const char> string_end = string + string_len; // warning
}

the ranges that are being compared are:

declared bounds: 'bounds(string_end, string_end + 0)'
inferred bounds: 'bounds(string, string + string_len)'

Another example:

void g(nt_array_ptr<char> buf : bounds(buf_start, buf_start + buf_len),
       nt_array_ptr<const char> string,
       nt_array_ptr<char> buf_start : byte_count(buf_len),
       size_t buf_len) {
  size_t len = strlen(string);
  array_ptr<char> str : count(len) = 0;
  memcpy<char>(buf, // warning
               str, len);
}

The ranges that are being compared in this case are:

expected argument bounds: 'bounds((_Array_ptr<char>)buf, (_Array_ptr<char>)buf + len)'
inferred bounds: 'bounds(buf_start, buf_start + buf_len)'

2. Facts Can Be Stated as Pre-conditions

There can be a case in which a function is called only when a certain condition holds. On the other hand, the dataflow analysis that collects the facts, works on one function at a time. Therefore, these pre-conditions are not collected even though they can be helpful in proving some facts. For example, in the following piece of code,

void resize(_Ptr<JSON_Array> array, size_t new_capacity) {
  _Array_ptr<_Ptr<JSON_Value>> new_items : byte_count(new_capacity * sizeof(_Ptr<JSON_Value>)) = 0;
  new_items = malloc<_Ptr<JSON_Value>>(new_capacity * sizeof(_Ptr<JSON_Value>));
  memcpy<_Ptr<JSON_Value>>(new_items,
                           array->items, // warning
                           array->count * sizeof(_Ptr<JSON_Value>));
}
...
  if (array->capacity >= array->count)
    resize(array, new_capacity);
...

The ranges that are being compared in this case are:

expected argument bounds: 'bounds((_Array_ptr<char>)(_Array_ptr<_Ptr<JSON_Value> const>)array->items, (_Array_ptr<char>)(_Array_ptr<_Ptr<JSON_Value> const>)array->items + array->count * sizeof(_Ptr<JSON_Value>))'
inferred bounds: 'bounds(array->items, array->items + array->capacity)'

3. Simple Assignments Can Serve as Facts

In some cases, simple integer variable assignments can be helpful in proving bounds declarations. An example of such case is illustrated below:

array->capacity = new_capacity;
array->items = new_items; // warning

Here, the ranges that must be checked are:

declared bounds: 'bounds(array->items, array->items + array->capacity)'
inferred bounds: 'bounds((_Array_ptr<char>)new_items, (_Array_ptr<char>)new_items + new_capacity * sizeof(_Ptr<JSON_Value>))'

Since we assign new_capacity to array->capacity beforehand, we should be able to use this piece of information when proving the bounds.