A Hole in Ada Type Safety
Florian WeimerAda aims to restrict unsafe language features which break type safety to a set of constructs which can be easily spotted in source case. Examples include unchecked deallocation, unchecked conversion and explicit address handling. This note shows that a combination of safe-looking language features can be used to undermine type safety, too.
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 support limited or unconstrained types. However, it is sufficient to break type safety.
Addendum: Robert A Duff noted that this was already known in the Ada 83 timeframe. According to paragraph 3.7.2(4)
in the standard (Ada 95 Annotated Reference Manual with Technical Corrigendum 1, MITRE Corporation, 2000, retrieved 2011-04-30), the call to Convert is erroneous on its own, and not the return statement which uses the stale reference.
Addendum (2015): A Rust variant (for the unsafe language extension) of this approach has been published as A Type Safety Hole in Unsafe Rust).
Revisions
2011-04-30: published
2011-04-30: Add note that this was already known in the Ada 83 timeframe.
2012-09-11: Minor corrections.
2015-03-22: Add reference to Rust variant.