Download de pytea - Download de código -fonte pytea

pytea

Outras categorias

Initial release

Baixar

Pytea: analisador de erro de forma de tensor Pytorch

Página do projeto em papel

Requisitos

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

Como instalar e usar

 # 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

Como construir

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

# build
npm run build

Documentações

Configuração
Construir e depurar
Como adicionar nova API

Breve explicação do resultado da análise

O Pytea é composto por dois analisadores.

Análise online: Node.js (TypeScript / JavaScript)
- Encontre incompatibilidade de formas baseadas em range numéricas e uso indevido do argumento da API. Se a Pytea encontrar algum erro ao analisar o código, ele parará nessa posição e informará os erros e violou restrições ao usuário.
Análise offline: Z3 / Python
- As restrições geradas são passadas para o Z3PY. Z3 resolverá os conjuntos de restrições de cada caminho e imprimirá a primeira restrição violada (se existir).

O resultado do analisador on -line é dividido em três classes:

Caminho de sucesso potencial : o analisador não encontrou incompatibilidade de forma até agora, mas o conjunto de restrições finais pode ser violado se o Z3 o analisar em uma inspeção mais detalhada.
Caminho potencial inacessível : o analisador encontrou uma incompatibilidade de forma ou os usos incorretos da API, mas permanecem restrições de caminho . Em resumo, a restrição de caminho é uma condição de ramo não resolvida; Isso significa que o caminho parado pode ser inacessível se as restrições de caminho restantes tiverem uma contradição. Esses casos serão distinguidos da análise offline .
Caminho de falha imediata : o analisador encontrou um erro, interrompe sua análise imediatamente.

Advertência : Se o código contiver pytorch ou outras APIs de terceiros que não implementamos, ele aumentará alarmes falsos. No entanto, também registramos cada chamada de API não implementada. Consulte a seção LOGS do resultado e pesquisa cuja chamada API não implementada é executada.

O resultado final da análise offline é dividido em vários casos.

Caminho válido : o SMT Solver não encontrou nenhum erro. Toda restrição sempre será cumprida.
Caminho inválido : o SMT Solver encontrou uma condição que pode violar algumas restrições. Observe que isso não significa que o código sempre trava, mas encontrou um caso extremo que trava algumas execuções.
Caminho indecidível : o SMT Solver atendeu a restrições insolúveis, depois tem tempo limite. Algumas fórmulas não lineares podem ser classificadas neste caso.
Caminho inacessível : restrições duras e de caminho contêm restrições contraditórias; Este caminho não será realizado desde o início.