Checked scopes and constructed types

[dtarditi]

We need to decide what to do about constructed types that contain unchecked pointer types in checked scopes. Currently we say in the spec that checked scope cannot have unchecked pointer types occurring in them. An example of such a pointer is something like:

ptr<int *>

However, we could allow a checked scope to have a checked pointer to an unchecked pointer. The code in a checked scope could pass around this pointer, but never dereference it. This seems problematic, though, as it could mask "unsafe behavior"

For example, should we allow

int g(ptr<int *> p) {
  return **p;
}

checked f(ptr<int *> p) {
 ... 
   int r = g(p);
}

I think it is important to make a decision about this and update the spec to be clearer about what is allowed.

[wonsubkim]

I appreciate that you bring up this issue
While I make test codes for checked scope, I wondered that checked pointer to unchecked pointer is checked pointer or not.
I have considered what the definition of checked pointer type is.
In conclusion, I think that a checked pointer to an unchecked pointer is not checked pointer because multiple dereference can't prevent invalid pointer access.

I think that a checked pointer to an unchecked pointer is not a common case we consider.
Using checked pointer types means that somebody intends to consider validity check of pointer behavior and user intentionally exploits checked pointer despite some inconveniences to guarantee valid pointer access.
If some semantic of checked pointer type can break validity of pointer access, I think that it is wrong
So, I think that checked pointer type to unchecked pointer type is regarded as unchecked pointer type in checked block.
I think that it is correct that checked pointer types must guarantee that pointee is not unchecked pointer type.

To guarantee this constraint, maybe I should check checked pointer types recursively.

How about your idea?

[wonsubkim]

void (*f)(int);
f is variable with function pointer type. Also it is unchecked pointer type
For checked function pointer type, is it correct?
checked void (*f)(int);

In conclusion, by default function pointer type is unchecked pointer type
For checked function pointer type, checked keyword is required.
Is it correct?

[dtarditi]

I agree with your analysis that you should check checked pointer types recursively. I think you'll need to check arrays and other constructed types.

For function pointer types, the type needs to be ptr<... function type>. For example, ptr<int (void)>.

There is a function declared in type.h (hasCheckedType()) that you can use as the base for your recursive checking. You would want hasUncheckedType instead.

[wonsubkim]

We have added implicit conversion rule between checked pointer types.
I have a question about constructed pointer types.

ptr<int> pa = 0;
array_ptr<int> apa : count(5) = 0
pa = apa; // compatible
apa = pa; // compatible

Actually, ptr<T> and array_ptr<T> is compatible.

ptr<ptr<int>> ppa = 0;
ptr<array_ptr<int>> papa = 0;
ppa = papa; // incompatible type error
papa = ppa; // incompatible type error

For constructed type, ptr<ptr<T>> and ptr<array_ptr<T>> is also compatible without considering bounds information?
ptr<ptr<T>> is compatible with array_ptr<ptr<T>>?
array_ptr<ptr<T>> is compatible with ptr<array_ptr<T>>?

For constructed type, how can we determine the compatibility bewteen types?

[wonsubkim]

For constructed pointer type, it is required to have same referent type.
It is treated incompatible type if pointer types have different referent type

[dtarditi]

Compatibility in C has a very specific meaning. It means that one type can be substituted or is equivalent to another type. We have a notion of assignment compatibility that is used when implicit conversions happen.

Even with assignment compatibility, we really can't say that a ptr <array_ptr<int>> is assignment compatible with ptr<ptr<int>>. I thought about this before and it could break the soundness of the type system for checked types. We are careful and require for now that the referent types be the same.

The problem is that we'd have to constrain the size of the referent type in some way, which we don't have a way to do. As an example, suppose we allowed:

ptr<ptr<int>> ppa = 0;
ptr<array_ptr<int>> papa = 0;
ppa = papa; 

Then a user could write code that breaks the Checked C type system:

void f(array_ptr<int> k : count(0),) {
  ptr<array_ptr<int>> papa = &k; //  pointer to array_ptr that we are not allowed to access through
  ptr<ptr<int>> ppa = papa;        // subvert type system because we aren't checking length
  int y = **ppa;  // access that array_ptr
}

Even if we checked length, it would still get tricky. We allow a longer array to be substituted for a shorter array:

array_ptr<int>p : count(10) = ...
array_ptr<int> r : count(1) = p ...

However, we can't apply that same rule when we have a pointer to p:

ptr<array_ptr<int> : count(10)> p1 = ...
ptr<array_ptr<int> : count(1)> p2 = p1

It would mean that we could substitute a pointer to a 1-element array in a context where a pointer to a 10-element array is expected. p1 and p2 alias the same memory location, so

*p2 = ...

affects the result of reading:

  ... *p1

[wonsubkim]

Thanks for your comments.
Assignment compatibility does not mean that checked pointer types of that are compatible with each other.
For constructed type, referent type must be same even though those are assignment compatible.

[dtarditi]

I think the specification is fine here. It is a good idea to not allow checked pointers to unchecked pointers in checked scopes. It is potentially confusing and more complicated to explain. Until we have a compelling example, I think we should leave the spec "as is".