From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,3a7c118fd2cc64f9,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news3.google.com!feeder.news-service.com!news.osn.de!diablo2.news.osn.de!news.belwue.de!LF.net!news.enyo.de!not-for-mail
From: Florian Weimer <fw@deneb.enyo.de>
Newsgroups: comp.lang.ada
Subject: A hole in Ada type safety
Date: Sat, 30 Apr 2011 10:41:17 +0200
Message-ID: <87oc3odtci.fsf@mid.deneb.enyo.de>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Trace: ruchba.enyo.de 1304152877 11185 172.17.135.6 (30 Apr 2011 08:41:17
 GMT)
X-Complaints-To: news@enyo.de
Cancel-Lock: sha1:PQXgDS3whC/gglNe9lHtNv2EIZ0=
Xref: g2news1.google.com comp.lang.ada:19098
Date: 2011-04-30T10:41:17+02:00
List-Id: <comp.lang.ada>

I don't know if this is a new observation---I couldn't find
documentation for it.  I plan to incorporate feedback into
<http://www.enyo.de/fw/notes/ada-type-safety.html>.

The standard way to show that type safety has been broken in a
language is to implement a cast function Conversion from any type
Source to any type Target:

    generic
       type Source is private;
       type Target is private;
    function Conversion (S : Source) return Target;

This generic function can be used like Ada.Unchecked_Conversion:

    with Ada.Text_IO;
    with Ada.Unchecked_Conversion;

    with Conversion;

    procedure Convert_Test is
       type Integer_Access is access all Integer;
       
       J : aliased Integer;
       J_Access : Integer_Access := J'Access;
       
       function Convert is new Conversion (Integer_Access, Integer);
       function Unchecked_Convert is new Ada.Unchecked_Conversion
         (Integer_Access, Integer);
       
    begin
       Ada.Text_IO.Put_Line (Integer'Image (Convert (J_Access)));
       Ada.Text_IO.Put_Line (Integer'Image (Unchecked_Convert (J_Access)));
    end Convert_Test;

How can we implement Conversion? It turns out that discriminant
records with defaults combined with aliasing do the trick:

    function Conversion (S : Source) return Target is
       type Source_Wrapper is tagged record
          S : Source;
       end record;
       type Target_Wrapper is tagged record
          T : Target;
       end record;
       
       type Selector is (Source_Field, Target_Field);
       type Magic (Sel : Selector := Target_Field) is record
          case Sel is
    	 when Source_Field =>
    	    S : Source_Wrapper;
    	 when Target_Field =>
    	    T : Target_Wrapper;
          end case;
       end record;
       
       M : Magic;
       
       function Convert (T : Target_Wrapper) return Target is
       begin
          M := (Sel => Source_Field, S => (S => S));
          return T.T;
       end Convert;
       
    begin
       return Convert (M.T);
    end Conversion;

When the inner function Convert is called, the discriminant Sel of M
has the value Target_Field, thus the component M.T can be
dereferenced. The assignment statement in Convert changes the
discriminant and the value. But the source value S is still reachable
as an object of type Target because the parameter T aliases the
component M.T, so the return statement executes without raising an
exception.

The two tagged records are used to force that the inner Convert
function receives its parameter by reference. Without them, an
implementation would be free to pass the discriminant record Magic by
copy, and aliasing would not occur.

Our implementation lacks the full power of Ada.Unchecked_Conversion
because it does not supported limited or unconstrained types. However,
it is sufficient to break type safety.