a22_acl2_01 のバックアップ(No.3)

acl2ライブラリ

acl2ライブラリは、できるだけC言語が使いやすくなるようにするためのライブラリです。このライブラリが提供するマクロや関数などは、すべてAかaで始まる名前が付けられています。

裏方はこうなっています。

#define AClass0(nam)   typedef struct nam##_ nam
#define AClass1(nam)   struct nam##_
#define AClass(nam)    AClass0(nam); AClass1(nam)

構造体の最初のメンバは、デスクトラクタ関数（deinit関数）のポインタが入っていることが望ましいです。この取り決めがあれば、素性のよくわからないオブジェクトであっても、少なくともデストラクタは呼べるということになります。
デストラクタ関数は、第一引数がオブジェクトへのポインタで、第二引数が整数値になっています。この第二引数で、デストラクト処理の状況を知らせます。0なら通常の終了で、1なら緊急の終了です。一般に緊急の終了の場合は、longjmpなどのような正常なネスト処理が行えない状況などに対応していて、それに配慮した処理が期待されます（正しい順序でデストラクタ関数を呼べていなくてもエラーにはしないとか）。ということで、基本的には通常終了を選んでください。
多くのオブジェクトでは、0でも1でも同じ終了処理をしています。

ただまあ、このルールは、acl2ライブラリが提供するオブジェクトが守っているルールであって、acl2ライブラリを使う側のプログラムは、この制約を守る義務はありません。

acl2ライブラリが提供する関数群は、勝手にmallocやfreeを呼び出すことはありません。必ずメモリ管理オブジェクトを経由してメモリ管理を行います（AMC）。これによりライブラリ利用者は、acl2ライブラリが勝手にメモリを確保したり開放したりすることを心配しないで済みます。もし自前のメモリ管理アルゴリズムを使いたい場合は、簡単に適用できます。
この機能のおかげで、オブジェクトごとにメモリ管理の方法を選択するようなこともできます。

ADbgLvというマクロ定数を定義すると、デバッグ向けの機能が有効になります。定義しないとデフォルト動作になり、ADbgLv=0とみなされます。
ADbgLv=1で、負荷の小さいデバッグ支援機能が有効になります。消費メモリを確認できるようになるのもこのレベルです。
ADbgLv=2で、すべてのデバッグ支援機能が有効になります。
ADbgLv=0でも消費メモリ量くらいは確認できるようにすべきだと思うかもしれませんが、「もうとにかくしてもしなくてもいい処理は全部カットして、速度最優先でやってくれ」というのがADbgLv=0に課された使命ですので、消費メモリレポート機能が動かなくなっても問題はないのです。
なお、デバッグレベルによって、構造体の大きさが変わることはありません。デバッグに必要なメンバ変数はADbgLv=0でも確保されます。・・・たいていはそこはポインタになっていて、ポインタの先でデバッグ情報を管理します。こうすることで、ADbgLv=0時のメモリの無駄使いを小さくしています。また、デバッグ情報のためのAMCと通常のAMCは別々になっているので、デバッグ時の消費メモリ確認において、デバッグ情報のためのメモリが計上されることはありません。