pytea Download - pytea Quellcode Download

pytea

Andere Kategorien

Initial release

Herunterladen

Pytea: Pytorch -Tensor -Formfehleranalysator

Papierprojektseite

Anforderungen

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

So installieren und verwenden Sie

 # 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

Wie man baut

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

# build
npm run build

Dokumentationen

Konfiguration
Bauen und debuggen
So fügen Sie neue API hinzu

Kurze Erklärung des Analyseergebnisses

Pytea besteht aus zwei Analysatoren.

Online -Analyse: node.js (TypeScript / JavaScript)
- Finden Sie numerisch-basierte Form-Mismatch und Missbrauch des API-Arguments. Wenn Pytea bei der Analyse des Codes Fehler festgestellt hat, wird an dieser Position eingestellt und die Fehler informiert und die Einschränkungen für den Benutzer verletzt.
Offline -Analyse: Z3 / Python
- Die erzeugten Einschränkungen werden an Z3PY übergeben. Z3 löst die Einschränkungen der einzelnen Pfad und druckt die erste verletzte Einschränkung (falls vorhanden).

Das Ergebnis des Online -Analysators ist in drei Klassen unterteilt:

Potenzieller Erfolgspfad : Der Analysator fand bisher keine Formfehlanpassung, aber der endgültige Einschränkungssatz kann verletzt werden, wenn Z3 sie bei näherer Betrachtung analysiert.
Potentieller unerreichbarer Weg : Der Analysator fand eine Formfehlanpassung oder eine API -Missverbrauchs, aber es bleiben Pfadbeschränkungen . Kurz gesagt, die Pfadbeschränkung ist ein ungelöster Zweigzustand; Das bedeutet, dass der gestoppte Pfad möglicherweise nicht erreichbar ist, wenn die verbleibenden Pfadbeschränkungen einen Widerspruch haben. Diese Fälle werden von der Offline -Analyse unterschieden.
Sofortiger fehlgeschlagener Pfad : Der Analysator hat einen Fehler gefunden und seine Analyse sofort gestoppt.

Vorbehalt : Wenn der Code Pytorch oder andere APIs von Drittanbietern enthält, die wir nicht implementiert haben, werden Fehlalarme ausgelöst. Trotzdem erfassen wir auch jeden nicht implementierten API -Anruf. Siehe Abschnitt LOGS Abschnitt" Aus dem Ergebnis und der Suche, die nicht implementierter API -Aufruf ausgeführt wird.

Das Endergebnis der Offline -Analyse ist in mehrere Fälle unterteilt.

Gültiger Pfad : SMT Solver hat keinen Fehler gefunden. Jede Einschränkung wird immer erfüllt.
Ungültiger Pfad : SMT Solver fand eine Erkrankung, die einige Einschränkungen verletzen kann. Beachten Sie, dass dies nicht bedeutet, dass der Code immer abstürzt, sondern einen extremen Fall gefunden hat, der einige Hinrichtungen abbricht.
Unentscheidbarer Pfad : SMT Solver hat unlösbare Einschränkungen, dann Zeitüberschreitungen erfüllt. Einige nichtlineare Formeln können in diesen Fall eingeteilt werden.
Unerreichbarer Weg : Harte und Pfadbeschränkungen enthalten widersprüchliche Einschränkungen; Dieser Weg wird von Anfang an nicht realisiert.