скачать pytea - скачать исходный код pytea

pytea

Другие категории

Initial release

Скачать

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 (TypeScript / JavaScript)
- Найти числовое несоответствие формы на основе диапазона и неправильное использование аргумента API. Если Pytea обнаружила какую -либо ошибку при анализе кода, она остановится на этой позиции, сообщит об ошибках и нарушает пользователь.
Офлайн -анализ: Z3 / Python
- Сгенерированные ограничения передаются в Z3Py. Z3 решит наборы ограничений каждого пути и распечатает первое нарушенное ограничение (если оно существует).

Результат онлайн -анализатора разделен на три класса:

Потенциальный путь успеха : анализатор не обнаружил несоответствия форм до сих пор, но окончательный набор ограничений может быть нарушен, если Z3 анализирует его при ближайшем рассмотрении.
Потенциальный недоступный путь : анализатор обнаружил несоответствие формы или неправильные призывы API, но остаются ограничения пути . Короче говоря, ограничение пути является неразрешенным условием ветви; Это означает, что остановленный путь может быть недоступным, если оставшиеся ограничения пути имеют противоречие. Эти случаи будут отличаться от автономного анализа .
Немедленный неудачный путь : Анализатор обнаружил ошибку, немедленно останавливает свой анализ.

Предостережение : если код содержит Pytorch или другие сторонние API, которые мы не реализовали, он поднимет ложные тревоги. Тем не менее, мы также записываем каждый невыраженный вызов API. См. Раздел LOGS из результата и поиск, какой невыполненный вызов API выполняется.

Окончательный результат в автономном анализе разделен на несколько случаев.

Допустимый путь : SMT Solver не нашел никакой ошибки. Каждое ограничение всегда будет выполнено.
Неверный путь : SMT Solver обнаружил условие, которое может нарушить некоторые ограничения. Обратите внимание, что это не означает, что код всегда будет разбиться, но он обнаружил крайний случай, который сбивает некоторые выполнения.
Невыразимый путь : SMT Solver получил неразрешимые ограничения, а затем тайм -ауты. Некоторые нелинейные формулы могут быть классифицированы в этом случае.
Непотабевой путь : жесткие и пути пути содержат противоречивые ограничения; Этот путь не будет реализован с самого начала.