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许可证