ดาวน์โหลด pytea - ดาวน์โหลดซอร์สโค้ด pytea

pytea

หมวดหมู่อื่นๆ

Initial release

ดาวน์โหลด

Pytea: Pytorch Tensor Shape Error Analyzer

หน้าโครงการกระดาษ

ความต้องการ

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 ได้พบข้อ จำกัด ที่ไม่สามารถแก้ไขได้จากนั้นหมดเวลา สูตรที่ไม่ใช่เชิงเส้นบางอย่างสามารถจำแนกได้ในกรณีนี้
เส้นทางที่ไม่สามารถเข้าถึงได้ : ข้อ จำกัด ที่ยากและเส้นทางมีข้อ จำกัด ที่ขัดแย้งกัน เส้นทางนี้จะไม่เกิดขึ้นตั้งแต่ต้น