[CFE] Missing override error => soundness issue in vm

[eernstg]

Consider the following program:

class A {
  num foo(int n) {
    print(n.runtimeType); // 'double'
    return 1.1;
  }
}

abstract class B<X> {
  X foo(X x);
}

class C extends A with B<num> {}

void main() {
  C a = C();
  a.foo(1.2);
}

This program is rejected by the analyzer, as it should be:

error • 'A.foo' ('num Function(int)') isn't a valid concrete implementation of 'B.foo' ('num Function(num)'). • n034.dart:12:7 • invalid_implementation_override

However, the CFE does not detect this override error. With dart, it generates code where A.foo isn't overridden, and A.foo does not check the type of the actual argument, so we reach print(n.runtimeType) and it prints 'double', which is a soundness violation.

Note that this isn't exclusively a matter for the CFE: dart2js does perform the type check at the invocation of foo, so it does throw.

[johnniwinther]

The CFE inserts a concrete forwarding stub, which is currently replaced by a clone of the abstract B.foo member. The concrete forwarding stub was meant to check the covariant argument, but alas, its type is signature is num Function(covariant num) and therefore allows double to be passed.

Either we shouldn't allow this in the first place - for that we need a clear(er) guide for when (not) to insert concrete forwarding stubs - or we should add the needed check to the passed argument in the concrete forwarding stub. That is, generate this concrete forwarding stub:

num foo(covariant num x) => super.foo(x as int);

instead of the current

num foo(covariant num x) => super.foo(x);

[eernstg]

We discussed whether the situation is specified. I believe it is actually covered by the current language specification:

A with B<num> is treated as a fresh class that implements B<num>, and the interface of B<num> contains the member signature num foo(num).

Note that the parameter it is not marked covariant, because the covariance in B is by-class, not by-declaration. The member signature has the modifier covariant on a parameter if and only if there is a superinterface where the corresponding parameter has that modifier as actual source code.

We would then get an error because C has a concrete member foo which is not a correct override of that member signature (it has member signature num foo(int)). So the declaration of C is a compile-time error.

The most tricky part here is probably that the member signature of the inherited implementation may or may not include the covariant modifier on certain parameters, and that's determined by the inherited declaration itself, not by a hypothetical copied-down version of the declaration:

class A { num foo(num n) => 1.1; }
abstract class B { num foo(covariant num x); }
class C extends A with B {} // Error

The error arises here because the interface of A with B contains the member signature num foo(covariant num), and num foo(num) from A is not a correct override of that.

If we had written num foo(num n) => 1.1; in the body of C then it would have had the member signature num foo(covariant num), and there would not have been any errors. The difference is that the declaration in C implicitly gets a covariant parameter by occurring in a class body whose interface has a member with that property already, but that's not the case for the declaration in A, and it doesn't magically obtain that property just because it is inherited by C.

We don't specify exactly in which situations a class must have an implicitly induced forwarding method (with or without a dynamic type check on some parameters), it is up to each implementation to ensure that the resulting program behavior is sound, and this could be achieved by adding such forwarding methods when necessary, but there could also be other compilation strategies (e.g., adding a parameter type check to the body of A.foo, even though it isn't needed for invocations where the receiver has type A).

[eernstg]

Thinking about this some more, I do think we need to add a paragraph to the language specification about the error that is caused by a missing covariant marker in a member signature: dart-lang/language#1729.