[Prev][Next][Index][Thread]

RE: Component Pascal type system is unsound

Late update on this one: the hole was closed almost
immediately after Fergus discovered it - by requiring
invariance on OUT parameters.

This is one of the humbling experiences where you are
reminded that soundness proofs are actually useful ;-)

- Clemens


> -----Original Message-----
> From: Fergus Henderson [mailto:fjh@cs.mu.oz.au] 
> Sent: Thursday, December 27, 2001 7:49 AM
> To: Types List
> Subject: Component Pascal type system is unsound
> 
> 
> [----- The Types Forum, 
> http://www.cis.upenn.edu/~bcpierce/types -----]
> 
> While we're on the topic of languages with unsound type 
> systems, let me mention another one: Component Pascal. 
> <http://www.oberon.ch/docu/language_report.html>.
> 
> According to www.oberon.ch, Component Pascal is a refined 
> version of Pascal, Modula-2, and Oberon, and moreover it is 
> advertised as being "type-safe".
> 
> However, in July this year, in response to some mail from 
> John Gough, I constructed an example which demonstrates a 
> hole in Component Pascal's type checking.
> 
> The basic problem arises due to the parameter compatibility 
> rules for "OUT"-mode parameters (which use pass-by-reference) 
> and "extended types" (Component Pascal's name for derived 
> classes). These rules allow, for instance, "OUT"-mode 
> parameters whose type is a pointer to an extended type to be 
> bound to variables whose type is a pointer to the base type.  
> This can lead to problems when such parameters are aliased.
> 
> Here's an example which shows the problem.
> 
> 	MODULE Foo;
> 	TYPE
> 		base = RECORD 
> 			x : INTEGER;
> 		END;
> 		derived1 = RECORD(base)
> 			y : INTEGER;
> 		END;
> 		derived2 = RECORD(base)
> 			z : INTEGER;
> 		END;
> 
> 	VAR
> 		b : POINTER to base;
> 
> 	PROCEDURE bar(OUT a1 : POINTER TO derived1;
> 	              OUT a2 : POINTER TO derived2);
> 	BEGIN
> 		NEW(a2);
> 		NEW(a1);
> 		a2^.z := 42;
> 	END bar;
> 
> 	BEGIN
> 		bar(b, b);
> 	END Foo.
> 
> Component Pascal allows this sort of code, but this program 
> ends up assigning to the `z' member of an object of type 
> `derived1', which does not have any `z' member.
> 
> (I probably have some of the details of this program wrong, 
> since I don't have a Component Pascal implementation around 
> to check it.  But John Gough has verified that the problem I 
> describe did occur for his Component Pascal implementation, 
> and last I heard the authors of the Component Pascal told him 
> that they are planning to revise the language to correct this 
> type loophole... in particular removing OUT parameter variance.)
> 
> -- 
> Fergus Henderson <fjh@cs.mu.oz.au>  |  "I have always known 
> that the pursuit
> The University of Melbourne         |  of excellence is a 
> lethal habit"
> WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words 
> of T. S. Garp.
>