Descargar pytea - Descargar el código fuente de pytea

pytea

Otras categorias

Initial release

Descargar

Pytea: analizador de error de forma de tensor de pytorch

página del proyecto en papel

Requisitos

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

Cómo instalar y 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

Cómo construir

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

# build
npm run build

Documentación

Configuración
Construir y depurar
Cómo agregar una nueva API

Breve explicación del resultado del análisis

Pytea está compuesta por dos analizadores.

Análisis en línea: Node.js (TypeScript / JavaScript)
- Encuentre el desajuste de forma numérico basado en el rango y el mal uso del argumento API. Si Pytea ha encontrado algún error al analizar el código, se detendrá en esa posición e informará los errores e violará las limitaciones al usuario.
Análisis fuera de línea: Z3 / Python
- Las restricciones generadas se pasan a Z3py. Z3 resolverá los conjuntos de restricciones de cada ruta e imprimirá la primera restricción violada (si existe).

El resultado del analizador en línea se divide en tres clases:

Ruta de éxito potencial : el analizador no encuentra la falta de coincidencia de forma hasta ahora, pero el conjunto de restricciones finales se puede violar si Z3 lo analiza en una inspección más cercana.
Potencial ruta inalcanzable : el analizador encontró un mal estado de desajuste o mal uso de API, pero quedan restricciones de ruta . En resumen, la restricción de ruta es una condición de rama no resuelta; Eso significa que la ruta detenida podría ser inalcanzable si las restricciones de ruta restantes tienen una contradicción. Esos casos se distinguirán del análisis fuera de línea .
Ruta fallida inmediata : el analizador ha encontrado un error, detiene su análisis de inmediato.

Advertencia : si el código contiene pytorch u otras API de terceros que no hemos implementado, provocará falsas alarmas. Sin embargo, también registramos cada llamada de API no implementada. Consulte la sección LOGS desde el resultado y la búsqueda que se realiza la llamada API no implementada.

El resultado final del análisis fuera de línea se divide en varios casos.

Ruta válida : SMT Solver no ha encontrado ningún error. Cada restricción siempre se cumplirá.
Ruta no válida : el solucionador SMT encontró una condición que puede violar algunas limitaciones. Tenga en cuenta que esto no significa que el código siempre se bloquee, pero encontró un caso extremo que bloquea algunas ejecuciones.
Ruta indecidible : SMT Solucion ha cumplido restricciones insoluble, luego tiempos de espera. Algunas fórmulas no lineales se pueden clasificar en este caso.
Ruta inalámbrica : las limitaciones duras y de ruta contienen restricciones contradictorias; Este camino no se realizará desde el principio.