Téléchargement de pytea - Téléchargement du code source pytea

pytea

Autres catégories

Initial release

Télécharger

Pytea: analyseur d'erreur de forme du tenseur du tenseur pytorch

page du projet papier

Exigences

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

Comment installer et utiliser

 # 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

Comment construire

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

# build
npm run build

Documentations

Configuration
Construire et déboguer
Comment ajouter une nouvelle API

Brève explication du résultat de l'analyse

Pytea est composé de deux analyseurs.

Analyse en ligne: Node.js (TypeScript / JavaScript)
- Trouvez une inadéquation de forme basée sur la plage numérique et une mauvaise utilisation de l'argument de l'API. Si Pytea a trouvé une erreur lors de l'analyse du code, elle s'arrêtera à cette position et éclairera les erreurs et les contraintes violées à l'utilisateur.
Analyse hors ligne: Z3 / Python
- Les contraintes générées sont transmises à Z3PY. Z3 résoudra les ensembles de contraintes de chaque chemin et imprimera la première contrainte violée (s'il existe).

Le résultat de l'analyseur en ligne est divisé en trois classes:

Chemin de réussite potentiel : L'analyseur n'a pas trouvé de décalage de forme jusqu'à présent, mais l'ensemble de contraintes finales peut être violé si Z3 l'analyse en inspection plus approfondie.
Path potentiel inaccessible : L'analyseur a trouvé une inadéquation de forme ou des abus d'API, mais il reste des contraintes de chemin . En bref, la contrainte de chemin est une condition de branche non résolue; Cela signifie que le chemin arrêté peut être inaccessible si les contraintes de chemin restantes ont une contradiction. Ces cas seront distingués de l'analyse hors ligne .
Chemin immédiat défaillant : L'analyseur a trouvé une erreur, arrête immédiatement son analyse.

Caveat : Si le code contient Pytorch ou d'autres API tierces que nous n'avons pas implémentées, elle relèvera de fausses alarmes. Néanmoins, nous enregistrons également chaque appel API non implémenté. Voir la section LOGS à partir du résultat et de la recherche de l'appel API non implémenté.

Le résultat final de l'analyse hors ligne est divisé en plusieurs cas.

Chemin valide : le solveur SMT n'a trouvé aucune erreur. Chaque contrainte sera toujours remplie.
Chemin non valide : SMT Solver a trouvé une condition qui peut violer certaines contraintes. Notez que cela ne signifie pas que le code se bloquera toujours, mais il a trouvé un cas extrême qui plante certaines exécutions.
Chemin indécidable : le solveur SMT a rencontré des contraintes insolubles, puis des délais d'attente. Certaines formules non linéaires peuvent être classées dans ce cas.
Chemin inaccessible : les contraintes dures et de chemin contiennent des contraintes contradictoires; Ce chemin ne sera pas réalisé dès le début.