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

.. post:: Jan 07, 2020
   :tags: ada, ada_2022

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

requeue文とAccessibility_Check
------------------------------

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

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

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

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

.. code-block:: ada

 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型を経由するとわからなくなる場合もあります。

.. code-block:: ada

 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 202xで修正されました。

デフォルト初期化とpredicate
---------------------------

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

.. code-block:: ada

 declare
    subtype S1 is Integer range 1 .. Integer'Last;
    X : S1; -- uninitialized and unchecked
 begin
    X := 1; -- checked
    X := 0; -- checked, Constraint_Error

.. code-block:: ada

 declare
    subtype P1 is Integer with Dynamic_Predicate => P1 > 0;
    X : P1; -- uninitialized and unchecked
 begin
    X := 1; -- checked
    X := 0; -- checked, Assertion_Error

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

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

.. code-block:: ada

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

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

outパラメータとpredicate
------------------------

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

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

.. code-block:: ada

 declare
    subtype P1 is Integer with Dynamic_Predicate => P1 > 0;
    
    procedure Proc (Item : out P1) is
    begin
       Item := 1; -- checked
    end Proc;
    
    X : Integer;
 begin
    Proc (X); -- uninitialized and checked

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

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

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

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

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

不変条件の抜け穴
++++++++++++++++

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

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

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

``Type_Invariant`` は多態しませんのでダウンキャストも迂回ルートになります。
:doc:`26日目 </2019/12/26_1>`\ も参照。

.. code-block:: ada

 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**

.. _`AI12-0167-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0167-1.txt
.. _`AI12-0191-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0191-1.txt
.. _`AI12-0210-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0210-1.txt
.. _`AI12-0301-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0301-1.txt
.. _`AI12-0333-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0333-1.txt
.. _`AI12-0335-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0335-1.txt
.. _`AI12-0338-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0338-1.txt