pytea

Pytea：Pytorchテンソル形状エラーアナライザー

ペーパープロジェクトページ

要件

• node.js >= 12.x
• python >= 3.8
  • z3-solver >= 4.8

インストールと使用方法

 # install node.js
sudo apt-get install nodejs

# install python z3-solver
pip install z3-solver

# download pytea
wget https://github.com/ropas/pytea/releases/download/v0.1.0/pytea.zip
unzip pytea.zip

# run pytea
python bin/pytea.py path/to/source.py

# run example file
python bin/pytea.py packages/pytea/pytest/basics/scratch.py

構築方法

 # install dependencies
npm run install:all
pip install z3-solver

# build
npm run build

ドキュメント

• 構成
• ビルドとデバッグ
• 新しいAPIを追加する方法

分析結果の簡単な説明

Pyteaは2つのアナライザーで構成されています。

• オンライン分析：node.js（typescript / javascript）
  • 数値範囲ベースの形状の不一致とAPI引数の誤用を見つけます。 Pyteaがコードの分析中にエラーを見つけた場合、その位置で停止し、ユーザーへのエラーと違反の制約を通知します。
• オフライン分析：Z3 / Python
  • 生成された制約はZ3PYに渡されます。 Z3は各パスの制約セットを解き、最初の違反された制約を印刷します（存在する場合）。

オンラインアナライザーの結果は、次の3つのクラスに分かれています。

• 潜在的な成功パス：アナライザーはこれまでシェイプの不一致を見つけませんでしたが、Z3が詳細な検査で分析すると、最終的な制約セットに違反する可能性があります。
• 潜在的な到達不可能なパス：アナライザーは、形状の不一致またはAPIの誤用を発見しましたが、パスの制約が残っています。要するに、パス制約は未解決の分岐条件です。つまり、残りのパスの制約に矛盾がある場合、停止されたパスが到達できない可能性があります。これらのケースは、オフライン分析と区別されます。
• すぐに失敗したパス：アナライザーがエラーを見つけ、すぐに分析を停止します。

警告：コードに、実装していないPytorchまたは他のサードパーティAPIが含まれている場合、誤ったアラームが発生します。それにもかかわらず、実装されていない各API呼び出しも記録します。結果のLOGSセクションを参照して、実装されていないAPI呼び出しを検索します。

オフライン分析の最終結果は、いくつかのケースに分割されます。

• 有効なパス：SMTソルバーにはエラーが見つかりませんでした。すべての制約は常に満たされます。
• 無効なパス：SMTソルバーは、いくつかの制約に違反する可能性のある条件を見つけました。これは、コードが常にクラッシュすることを意味しないことに注意してください。しかし、いくつかの実行をクラッシュさせる極端なケースが見つかりました。
• 決定不可能なパス：SMTソルバーは、解決不可能な制約を満たし、その後タイムアウトを満たしました。いくつかの非線形式をこのケースに分類できます。
• 到達不可能なパス：ハードおよびパスの制約には、矛盾する制約が含まれています。このパスは最初から実現されません。

結果の例

• オンライン分析によって見つかったエラー

• オフライン分析によって見つかったエラー

ライセンス

MITライセンス

このプロジェクトは、MITライセンスのPyrightに基づいています