Ada 2020 (38日目) - 実行時チェックのタイミング

実行時チェックが挿入されるタイミングにも細かい修正が入っています。

requeue文とAccessibility_Check

繰り返しますがAdaとは非常に動的な言語です。 (あくまで静的な型を持つ中では、です。)

静的と動的の境い目が曖昧であり静的に解決されるのが動的に解決されるのかでコードを書き分ける必要がありません。 エラーの検出も含めて静的に解決できるものはして、解決しきれなかったら実行時に持ち越しみたいな感じです。 この性質は特に generic で有用です。 (静的であることを意識しなければならない場合もあります。 16日目を参照。)

で、まあ、その抜けですね。 静的に解決できる場合は静的にチェックされますが、解決できなかった場合に動的にチェックされていなかったケースです。

requeue文で現在の accept があるブロックよりも寿命が短い task を指名するとエラーです。 キューに入った次の要求を受け取るのは accept を抜けた後だからです。

task Outer is
   entry E1;
end Outer;

task body Outer is
begin
   accept E1 do
      declare
         task Inner is
            entry E2;
         end Inner;
         -- Innerのbodyは省略
      begin
         requeue Inner.E2; -- error
      end;
   end E1;
end Outer;

この Inner の寿命は静的にわかりますが access 型を経由するとわからなくなる場合もあります。

task type Global_Task_Type is
   entry E3;
end Global_Task_Type;
-- Global_Task_Typeのbodyは省略

task Outer is
   entry E1;
end Outer;

task body Outer is
begin
   accept E1 do
      declare
         Inner : Global_Task_Type;
         Ref : not null access Global_Task_Type := Inner'Access;
      begin
         requeue Ref.all.E3;
      end;
   end E1;
end Outer;

型の Global_Task_Type 自体は外側で宣言されていますがオブジェクトの Inner は上と同じく accept があるブロックよりも寿命が短いです。 更に access 型を経由することで実際のオブジェクトの寿命をわからなくしています。 (この程度でしたらコンパイラが頑張れば検出できそうですが関数を経由する等で更に難解にできます。)

コンパイラは静的にチェックしきれなかったら実行時にチェックするコードを生成しないといけないわけですがrequeue文に関してはそのルールが規格から抜けていたという話です。

Ada 2020で修正されました。

デフォルト初期化とpredicate

基本的にはpredicateは部分範囲型のチェック (Range_Check) 同様に振る舞います。 中でも注目すべき点としまして、変数が初期化されなかった場合はpredicateもチェックされません。

declare
   subtype S1 is Integer range 1 .. Integer'Last;
   X : S1; -- uninitialized and unchecked
begin
   X := 1; -- checked
   X := 0; -- checked, Constraint_Error
declare
   subtype P1 is Integer with Dynamic_Predicate => T > 0;
   X : P1; -- uninitialized and unchecked
begin
   X := 1; -- checked
   X := 0; -- checked, Assertion_Error

しかしながらAda 2012で Default_Value アスペクトが追加されて record 型以外もデフォルト初期化できるようになりました。 その際にpredicateをチェックすることを求める記述が規格にありませんでした。

文面通りに捉えますとデフォルト初期化ではpredicateはチェックされないことになります。

declare
   type Defaulted_Integer is new Integer with Default_Value => 0;
   subtype P2 is Defaulted_Integer with Dynamic_Predicate => T > 0;
   X : P2; -- initialized to 0, but unchecked

Ada 2020で修正され、デフォルト初期化でもpredicateがチェックされるようになります。

outパラメータとpredicate

Ada 2012の文面では out パラメータに変数を渡したときにもpredicateがチェックされていました。 初期化されていない変数を渡した時にもチェックされてしまいます。

inin out であれば初期化してから渡すべきですが、 out パラメータは結果を受け取るためのパラメータですので初期化されていない変数を渡すのは普通です。

declare
   subtype P1 is Integer with Dynamic_Predicate => T > 0;

   procedure Proc (Item : out P1) is
   begin
      Item := 1; -- checked
   end Proc;

   X : Integer;
begin
   Proc (X); -- uninitialized and checked

これではスタックやレジスタに残っていたゴミがチェックされてしまい予想できない結果になります。

Ada 2020で修正され、 out パラメータに変数を渡した時点ではpredicateがチェックされなくなります。

勿論サブプログラムの中で変更されたときや、値渡しだった場合のサブプログラムを出るときのコピー戻しではチェックされます。

抜け穴が見逃されたケース

本来であればチェックしたほうがいいところをチェックしなくてもいいという結論になったケースもあります。

不変条件の抜け穴

基本的には Type_Invariant はサブプログラムから出るタイミングで out パラメータや関数の返値についてチェックされます。 Type_Invariant は抽象型にしか付けられず、抽象型はサブプログラムを通じてのみ変更されますのでサブプログラムを出るときにチェックすれば充分なはずです。

しかし場合によっては可視性が破られるケースもあります。 抽象型と同じパッケージやその子パッケージにあるサブプログラムからはその抽象型の中身が見えてしまいます。

そこでパラメータや返値以外から迂回してオブジェクトを参照して、要素のみを直接変更してしまえばチェックをすり抜けれられます。

Type_Invariant は多態しませんのでダウンキャストも迂回ルートになります。 26日目も参照。

package Base is
   type B is tagged private;
private
   type B is tagged null record;
end Base;

package Derived is
   type D is new Base.B with private;
   procedure Danger (Object : in out Base.B'Class)
     with Pre => Object in D'Class;
private
   type D is new Base.B with
      record
         Component : Integer := 1;
      end record
        with Type_Invariant => D.Component > 0;
end Derived;

package body Derived is

   procedure Danger (Object : in out Base.B'Class) is
   begin
      D (Object).Component := -1; -- unchecked
   end Danger;

end Derived;

この例ではダウンキャストを行って直接 Component を変更しています。 Danger から出るときにチェックされるのは Base.B 型の Type_Invariant ですので Derived.D 型の Type_Invariant はチェックされません。

もし次にチェックされる機会があれば、原因とは別の場所でエラーが捕捉されます。

ダウンキャスト以外にも access 型や generic もしくは limited with を使用した迂回ルートが見つかっています。 基底型と派生型が同じパッケージにある場合には派生型の中の基底部分でも起こり得ます。

コンパイラによってチェックすることが困難な上に、こんなコードを書くのはどうせわかっててやってるのだから、ということでしょうか。

関連AI

  • AI12-0167-1 Type_Invariants and tagged-type View Conversions

  • AI12-0191-1 Clarify “part” for type invariants

  • AI12-0210-1 Type Invariants and Generics

  • AI12-0301-1 Predicates should be checked like constraints for types with Default_Value

  • AI12-0333-1 Predicate checks on out parameters

  • AI12-0335-1 Dynamic accessibility check needed for some requeue targets

  • AI12-0338-1 type invariant checking and incomplete types