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는 2 개의 분석기로 구성됩니다.

온라인 분석 : node.js (TypeScript / JavaScript)
- API 인수의 숫자 범위 기반 모양 불일치 및 오용을 찾으십시오. PYTEA가 코드를 분석하는 동안 오류를 발견 한 경우 해당 위치에서 중지하고 오류를 알려주고 사용자에게 제약을 위반했습니다.
오프라인 분석 : Z3 / Python
- 생성 된 제약 조건은 z3py로 전달됩니다. Z3은 각 경로의 제약 세트를 해결하고 첫 번째 위반 된 제약 조건을 인쇄합니다 (존재하는 경우).

온라인 분석기의 결과는 세 가지 클래스로 나뉩니다.

잠재적 성공 경로 : 분석기는 지금까지 모양 불일치를 찾지 못하지만 Z3가 면밀한 검사에서 분석하면 최종 제약 세트를 위반할 수 있습니다.
잠재적 인 처리 할 수없는 경로 : 분석기는 모양 불일치 또는 API 오용을 발견했지만 경로 제약 조건이 남아 있습니다. 요컨대, 경로 제약은 해결되지 않은 분기 조건입니다. 이는 나머지 경로 제약이 모순이있는 경우 중지 경로가 도달 할 수 없을 수 있음을 의미합니다. 이러한 경우는 오프라인 분석 과 구별됩니다.
즉시 실패한 경로 : 분석기는 오류를 발견하고 즉시 분석을 중지합니다.

경고 : 코드에 우리가 구현하지 않은 Pytorch 또는 기타 타사 API가 포함되어 있으면 잘못된 경보가 발생합니다. 그럼에도 불구하고, 우리는 또한 구현되지 않은 각 API 호출을 기록합니다. 결과의 LOGS 섹션을 참조하고 구현되지 않은 API 호출이 수행되는 검색을 참조하십시오.

오프라인 분석의 최종 결과는 여러 사례로 나뉩니다.

유효한 경로 : SMT 솔버는 오류를 찾지 못했습니다. 모든 제약은 항상 충족됩니다.
유효하지 않은 경로 : SMT Solver는 일부 제약을 위반할 수있는 조건을 찾았습니다. 이것이 코드가 항상 충돌한다는 의미는 아니지만 일부 실행이 충돌하는 극단적 인 경우를 발견했습니다.
명확하지 않은 경로 : SMT 솔버는 해결할 수없는 제약 조건을 충족 한 다음 시간 초과를 만났습니다. 일부 비선형 공식은이 경우에 분류 될 수 있습니다.
도달 할 수없는 경로 : 단단하고 경로 제약에는 모순되는 제약이 포함됩니다. 이 경로는 처음부터 실현되지 않습니다.