bennett@concour.CS.Concordia.CA (Anne Bennett) (06/16/89)
The following bug in Eiffel v2.1 was pointed out to me by
Paul Voda of Complete Logic Systems. It is somewhat similar to a
"Create" type insecurity outlined by Mark Utting (marku@cheops.eecs.
unsw.oz) in his posting of April 10.
Consider the following (severely abridged) Eiffel code:
----------------------------------------------------------------
Class A
feature
binary_op (other: like Current) is
deferred
end;
Class B
inherit A
feature
value: INTEGER;
binary_op (other: like Current) is
do
value := value + other.value
end;
Class C
inherit A
feature
value: REAL;
binary_op (other: like Current) is
do
value := value + other.value
end;
Class TEST -- This is the root class
feature
Create is
local
a1, a2: A;
b: B;
c: C
do
b.Create (3); a1 := b;
c.Create (5); a2 := c;
a1.binary_op(a2); -- THIS IS THE PROBLEMATIC INSTRUCTION
end;
----------------------------------------------------------------------------
Classes A,B, and C export "binary_op", as well as a "show" procedure which
enabled me to determine the following results:
Before "binary_op" is called:
a1 has dynamic type B and value INTEGER 3
a2 has dynamic type C and value REAL 5
After "binary_op" is called:
a1 has dynamic type B and value INTEGER 1084227587.
CONCLUSION: The call "a1.binary_op(a2)" was incorrectly type-checked by
the compiler; in B's binary_op, other.value was assumed to
return an INTEGER, when it really returns a REAL.
I believe that this problem can be corrected. I had the opportunity
to chat with Dr. Meyer when he gave a seminar in Montreal on June 8-9, and
he mentionned that a more sophisticated set of typing rules is on the way
(let me take this opportunity to remind Dr. Meyer that some of us are
awaiting the description of those rules with bated breath!). If I under-
stood him correctly, the new system will be able to check that a procedure
call is correct for any possible dynamic type of its receiver, and this will
be true notwithstanding the presence of export lists, according to which a
child may refuse to export a feature exported by its parent.
Let us assume that the assignment "a1 := b" in the example above
takes place in a condition statement, and that a1 might have received an
instance of B or C (this can be ascertained in a more general case without
recourse to code flow analysis, by a transitive closure mechanism which I
hope Dr. Meyer will explain to us soon). On encountering the call
"a1.binary_op(a2)", the compiler should say to itself:
"I can determine by transitive closure that a1 must be either
a B or a C.
"if a1 is a B, then B's binary_op will be used, therefore the
parameter must be a B (like Current, which is a B). However,
the actual parameter a2 is an A, which is not a descendant of B,
so I must signal a compile-time error.
"similarly, if a1 is a C, then C's binary_op will be used, and the
parameter must be a C, but a2 is not a descendant of C, so
again I must give a compile-time error."
In other words, it IS possible to type-check the above example,
but a conservative type-checker must disallow a call to a routine with a
"like Current" parameter whenever it is possible that the receiver may be
subject to polymorphism including sibling classes. If the receiver's
dynamic type could be any of several classes in a direct line of inheritance
(i.e. no siblings), the call will be correct only if the parameter has as
its static type the "youngest" of the polymorphs. Under these restrictions,
it might be wise to do away with anchored parameters altogether; anchored
result types and local variables are still ok.
Anne Bennett, bennett@concour.cs.concordia.ca
grad student, Computer Science, Concordia U., Montreal, Canada.marc@eiffel.UUCP (Jean-Marc Nerson) (06/20/89)
In <909@clyde.Concordia.CA>, Anne Bennet lists a small Eiffel example and concludes: >> ........................ (Example skipped) ......... >> ............................................................ >> CONCLUSION: The call "a1.binary_op(a2)" was incorrectly type-checked by the compiler ..... >> .............................................................. >> .... In other words, it IS possible to type-check the above example, >>but a conservative type-checker must disallow a call to a routine with a >>"like Current" parameter whenever it is possible that the receiver may be >>subject to polymorphism including sibling classes. If the receiver's >>dynamic type could be any of several classes in a direct line of inheritance >>(i.e. no siblings), the call will be correct only if the parameter has as >>its static type the "youngest" of the polymorphs. Under these restrictions, >>it might be wise to do away with anchored parameters altogether; anchored >>result types and local variables are still ok. >> ............................................................ Now, let's define the following classes: ------------------------------------------------------ class A feature x: A; f (u: A) is do x := u end end -- class A class B export f inherit A redefine x feature x: B -- !!!!!! the statement `x := u' of f is now not valid in B -- !!!!!! if the dynamic type of u is A or a (sub)sibling of B. end -- class B ------------------------------------------------------ The type checking problem highlighted in class B, occurs whenever there is a change of reference: - In assignments - In routine argument passing - In Accept operations (Release 2.2) This is not specifically due to declarations by association (``like''), but simply because of the ability to redefine with subtyping explicitly or implicitly. o Explicit type redefinition involves the use of a redefine subclause at inheritance time and leads to a change of the redefined feature's signature under conformance rules o Implicit type redefinition happens: - for a deferred routine implemented with a change of its signature under conformance rules - for a type defined ``like anchor'' with ``anchor'' redefined explicitly or implicitly because ``anchor'' was ``Current'' - for a type defined with generic parameter(s) instantiated at inheritance time. As Anne Bennet mentioned at the end of her message, Eiffel 3.0 will do a transitive closure type check in accordance with the separate compilation mechanism. This will remove all such cases. A detailed paper by B. Meyer is forthcoming. ------------------------ Jean-Marc Nerson marc@eiffel.com