Unduh pytea - Unduh Kode Sumber pytea

pytea

Kategori lainnya

Initial release

Unduh

Pytea: Pytorch Tensor Bentuk Kesalahan Analisis

halaman proyek kertas

Persyaratan

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

Cara menginstal dan menggunakan

 # 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

Cara membangun

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

# build
npm run build

Dokumentasi

Konfigurasi
Membangun dan men -debug
Cara Menambahkan API Baru

Penjelasan singkat tentang hasil analisis

Pytea terdiri dari dua analisis.

Analisis Online: Node.js (TypeScript / JavaScript)
- Temukan ketidakcocokan bentuk berbasis rentang numerik dan penyalahgunaan argumen API. Jika Pytea telah menemukan kesalahan saat menganalisis kode, itu akan berhenti pada posisi itu dan menginformasikan kesalahan dan melanggar kendala kepada pengguna.
Analisis offline: Z3 / Python
- Kendala yang dihasilkan diteruskan ke z3py. Z3 akan menyelesaikan set kendala dari setiap jalur dan mencetak kendala pertama yang dilanggar (jika ada).

Hasil penganalisa online dibagi menjadi tiga kelas:

Potensi Sukses Jalur : Penyaling tidak menemukan ketidakcocokan bentuk sampai sekarang, tetapi himpunan kendala akhir dapat dilanggar jika Z3 menganalisisnya pada pemeriksaan lebih dekat.
Potensi Potensi yang Tidak Dapat Diperjuang : Penyalahgunaan penganalisa menemukan ketidakcocokan atau API menyalahgunakan, tetapi tetap ada kendala jalur . Singkatnya, kendala jalur adalah kondisi cabang yang belum terselesaikan; Itu berarti jalan yang dihentikan mungkin tidak dapat dijangkau jika kendala jalur yang tersisa memiliki kontradiksi. Kasus -kasus tersebut akan dibedakan dari analisis offline .
Jalur Gagal Segera : Penganalisa telah menemukan kesalahan, segera menghentikan analisisnya.

Peringatan : Jika kode berisi Pytorch atau API pihak ketiga lainnya yang belum kami terapkan, itu akan meningkatkan alarm palsu. Namun demikian, kami juga merekam setiap panggilan API yang tidak diimplementasikan. Lihat bagian LOGS dari hasil dan cari panggilan API yang tidak diterapkan.

Hasil akhir dari analisis offline dibagi menjadi beberapa kasus.

Jalur yang valid : SMT Solver belum menemukan kesalahan. Setiap kendala akan selalu terpenuhi.
Jalur Invalid : SMT Solver menemukan suatu kondisi yang dapat melanggar beberapa kendala. Perhatikan bahwa ini tidak berarti kode akan selalu macet, tetapi menemukan kasus ekstrem yang merusak beberapa eksekusi.
Jalur yang tidak dapat diputuskan : SMT Solver telah memenuhi kendala yang tidak dapat diselesaikan, lalu batas waktu. Beberapa formula non-linear dapat diklasifikasikan ke dalam kasus ini.
Jalur yang tidak dapat dijangkau : kendala keras dan jalan mengandung kendala yang bertentangan; Jalan ini tidak akan direalisasikan sejak awal.