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由兩個分析儀組成。

• 在線分析：node.js（打字稿 / javaScript）
  • 找到基於數字範圍的形狀不匹配和濫用API參數。如果Pytea在分析代碼時發現了任何錯誤，它將停止該位置並告知錯誤並違反了對用戶的約束。
• 離線分析：Z3 / Python
  • 生成的約束傳遞給Z3PY。 Z3將解決每條路徑的約束集並打印第一個違反約束（如果存在的話）。

在線分析儀的結果分為三個類：

• 潛在的成功路徑：到目前為止，分析儀還沒有發現形狀不匹配，但是如果Z3在仔細檢查中對其進行分析，則最終約束集可能會違反。
• 潛在的無法達到的路徑：分析儀發現形狀不匹配或API濫用，但仍存在路徑限制。簡而言之，路徑約束是未解決的分支條件。這意味著，如果剩餘的路徑約束存在矛盾，則停止路徑可能是無法達到的。這些情況將與離線分析區分開。
• 立即失敗的路徑：分析儀發現錯誤，立即停止其分析。

警告：如果代碼包含我們尚未實施的Pytorch或其他第三方API，它將引起錯誤警報。但是，我們還記錄了每個未完成的API呼叫。請參閱結果的LOGS部分，並蒐索執行哪些未完成的API調用。

離線分析的最終結果分為幾種情況。

• 有效路徑：SMT求解器尚未發現任何錯誤。每個約束將始終得到滿足。
• 無效的路徑：SMT求解器發現了可能違反某些約束的條件。請注意，這並不意味著代碼總是會崩潰，而是發現了一個極端情況，該案例崩潰了一些執行。
• 不可確定的路徑：SMT求解器已達到無法分辨的約束，然後是超時。一些非線性公式可以分類為這種情況。
• 無法到達的路徑：硬路和路徑約束包含矛盾的約束；從一開始就無法實現這條路。

結果示例

• 通過在線分析發現的錯誤

• 通過離線分析發現的錯誤

執照

麻省理工學院許可證

該項目基於Pyright，也是MIT許可證