PyTea: PyTorch Tensor shape error analyzer

Overview

PyTea: PyTorch Tensor Shape Error Analyzer

paper project page

Requirements

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

How to install and use

# 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

How to build

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

# build
npm run build

Documentations

Brief explanation of the analysis result

PyTea is composed of two analyzers.

  • Online analysis: node.js (TypeScript / JavaScript)
    • Find numeric range-based shape mismatch and misuse of API argument. If PyTea has found any error while analyzing the code, it will stop at that position and inform the errors and violated constraints to the user.
  • Offline analysis: Z3 / Python
    • The generated constraints are passed to Z3Py. Z3 will solve the constraint sets of each path and print the first violated constraint (if it exists).

The result of the Online analyzer is divided into three classes:

  • potential success path: the analyzer does not found shape mismatch until now, but the final constraint set can be violated if Z3 analyzes it on closer inspection.
  • potential unreachable path: the analyzer found a shape mismatch or API misuses, but there remain path constraints. In short, path constraint is an unresolved branch condition; that means the stopped path might be unreachable if remaining path constraints have a contradiction. Those cases will be distinguished from Offline analysis.
  • immediate failed path: the analyzer has found an error, stops its analysis immediately.

CAVEAT: If the code contains PyTorch or other third-party APIs that we have not implemented, it will raise false alarms. Nevertheless, we also record each unimplemented API call. See LOGS section from the result and search which unimplemented API call is performed.

The final result of the Offline analysis is divided into several cases.

  • Valid path: SMT solver has not found any error. Every constraint will always be fulfilled.
  • Invalid path: SMT solver found a condition that can violate some constraints. Notice that this does not mean the code will always crash, but it found an extreme case that crashes some executions.
  • Undecidable path: SMT solver has met unsolvable constraints, then timeouts. Some non-linear formulae can be classified into this case.
  • Unreachable path: Hard and Path constraints contain contradicting constraints; this path will not be realized from the beginning.

Result examples

  • Error found by Online analysis

test1

  • Error found by Offline analysis

test2

License

MIT License

This project is based on Pyright, also MIT License

Comments
  • LSTM/GRU input_size tensor shape errors

    LSTM/GRU input_size tensor shape errors

    Hi, I have met a problem while detecting LSTM tensor shape errors. The testing file below is runnable and pytea returns correctly.

    import torch
    import torch.nn as nn
    import torch.nn.functional as F
    
    
    class Model(nn.Module):
    
        def __init__(self):
            super().__init__()
            self.cnn = nn.Conv2d(3, 1, 3, 1, 1)
            self.rnn = nn.LSTM(32, 64, 1, batch_first=True)
            self.pool = nn.MaxPool2d(2, 2)
            self.fc = nn.Linear(64, 16)
    
        def forward(self, x):
            x = self.pool(F.relu(self.cnn(x)))
            x = x.view(-1, 32, 32)
            x, _ = self.rnn(x)
            x = x[:, -1, :].squeeze(1)
            x = F.relu(self.fc(x))
            x = F.softmax(x, dim=-1)
            return x
    
    
    if __name__ == "__main__":
        net = Model()
        x = torch.randn(2, 3, 64, 64)
        y = net(x)
        target = torch.argmax(torch.randn(2, 16), dim=-1)
        loss = F.cross_entropy(y, target.long())
        loss.backward()
        print(y.size())
    

    However, If I change self.rnn = nn.LSTM(32, 64, 1, batch_first=True) into self.rnn = nn.LSTM(64, 64, 1, batch_first=True), torch will report a RuntimeError: Expected 64, got 32. pytea didn't return any CONSTRAINTS information, as it supposed to.

    Then I tried to more LSTM input_size shape errors, all failed. Same situation with GRU. I think it is a bug, because I can detect Conv2d, Linear error successfully.

    opened by MCplayerFromPRC 4
  • Inconsistent with document description

    Inconsistent with document description

    Hello, I have encountered the following problems:

    First question: The content of my source file is:

       import torch
       import torch.nn as nn
    
      class Net(nn.Module):
          def __init__(self):
              super(Net, self).__init__()
              self.layers = nn.Sequential(
                  nn.Linear(28 * 28, 120),
                  nn.ReLU(),
                  nn.Linear(80, 10))
      
          def a(self):
              pass
    
        if __name__ == "__main__":
            n = Net()
    

    But when I execute the command, I get the following results:

    image

    There should be a problem with defining shape in this model.

    Second question: I used it https://github.com/pytorch/examples/blob/master/mnist/main.py , but the command is stuck and no result is returned. As follows:

    image
    opened by dejavu6 2
  • Ternary expression (A if B else C) bug report

    Ternary expression (A if B else C) bug report

    아래와 같은 코드 실행에서 문제가 발생한다는 것을 깨달았습니다.

    x = 0 if 0 <= 1 else 1
    
    # runtime output
    REDUCED HEAP: (size: 250)
      x => 1
    

    파이썬의 삼항연산자가 x = (((0 <= 1) and 0) or 1)로 파싱됩니다. Logical statement가 True, true-value가 0일 때 발생하는 오류인 것으로 보입니다.

    당장 벤치마크 코드에서 나타나는 문제는 아닙니다. Pylib builtin 구현에서 발생한 문제이므로, 다른 방식으로 구현함으로써 일단은 피해갈 수 있을 것 같습니다.

    감사합니다.

    opened by lego0901 1
  • Develop sehoon

    Develop sehoon

    UT-1~6 코드 분석에 필요한 torch API 구현 완료.

    UT-2: epoch을 1로 수정하지 않으면 timeout이됨. UT-3: Python 빌트인 함수 iter, next의 구현은 우선 넘어갔음. UT-6: buggy 코드에서 target이 free variable인데, 이를 처리해 주지 않고 분석을 실행하면 아무것도 출력하지 않는 버그가 있음.

    위 특이사항을 적절히 처리해주고 분석을 실행하면 1~6 모두 buggy 코드는 invalid, fix 코드는 valid 결과를 냄.

    opened by Sehun0819 0
  • path constraint check

    path constraint check

    분석중 한 패스에서 (텐서 모양 오류 등의) 에러를 만나면 해당 패스는 처리됨. 문제는 분기 조건문에 의해 실제로는 진행되지 않는 패스여도 로 처리가 되는 것.

    따라서 분석중 에러를 만났을 때 그 패스가 path constraint를 갖고 있으면 로 처리하여 z3단에 넘기게 수정하였음.

    TODO: z3단에 넘기기 전에 path constraint를 계산하여 Valid면 , Unsat이면 로 처리하기(else )

    opened by Sehun0819 0
  • Bump node-notifier from 8.0.0 to 8.0.1 in /packages/pyright-internal

    Bump node-notifier from 8.0.0 to 8.0.1 in /packages/pyright-internal

    Bumps node-notifier from 8.0.0 to 8.0.1.

    Changelog

    Sourced from node-notifier's changelog.

    v8.0.1

    • fixes possible injection issue for notify-send
    Commits

    Dependabot compatibility score

    Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.


    Dependabot commands and options

    You can trigger Dependabot actions by commenting on this PR:

    • @dependabot rebase will rebase this PR
    • @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
    • @dependabot merge will merge this PR after your CI passes on it
    • @dependabot squash and merge will squash and merge this PR after your CI passes on it
    • @dependabot cancel merge will cancel a previously requested merge and block automerging
    • @dependabot reopen will reopen this PR if it is closed
    • @dependabot close will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually
    • @dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
    • @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
    • @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
    • @dependabot use these labels will set the current labels as the default for future PRs for this repo and language
    • @dependabot use these reviewers will set the current reviewers as the default for future PRs for this repo and language
    • @dependabot use these assignees will set the current assignees as the default for future PRs for this repo and language
    • @dependabot use this milestone will set the current milestone as the default for future PRs for this repo and language

    You can disable automated security fix PRs for this repo from the Security Alerts page.

    dependencies 
    opened by dependabot[bot] 0
Releases(v0.1.0)
Owner
ROPAS Lab.
ROPAS Lab. @ Seoul National University
ROPAS Lab.
The sixth place winning solution (6/220) in 2021 Gaofen Challenge.

SwinTransformer + OBBDet The sixth place winning solution (6/220) in the track of Fine-grained Object Recognition in High-Resolution Optical Images, 2

ming71 46 Dec 02, 2022
Character Controllers using Motion VAEs

Character Controllers using Motion VAEs This repo is the codebase for the SIGGRAPH 2020 paper with the title above. Please find the paper and demo at

Electronic Arts 165 Jan 03, 2023
Serverless proxy for Spark cluster

Hydrosphere Mist Hydrosphere Mist is a serverless proxy for Spark cluster. Mist provides a new functional programming framework and deployment model f

hydrosphere.io 317 Dec 01, 2022
Reading list for research topics in Masked Image Modeling

awesome-MIM Reading list for research topics in Masked Image Modeling(MIM). We list the most popular methods for MIM, if I missed something, please su

ligang 231 Dec 07, 2022
Attention-based Transformation from Latent Features to Point Clouds (AAAI 2022)

Attention-based Transformation from Latent Features to Point Clouds This repository contains a PyTorch implementation of the paper: Attention-based Tr

12 Nov 11, 2022
Self-Supervised Pre-Training for Transformer-Based Person Re-Identification

Self-Supervised Pre-Training for Transformer-Based Person Re-Identification [pdf] The official repository for Self-Supervised Pre-Training for Transfo

Hao Luo 116 Jan 04, 2023
Machine Learning Time-Series Platform

cesium: Open-Source Platform for Time Series Inference Summary cesium is an open source library that allows users to: extract features from raw time s

632 Dec 26, 2022
PyTorch implementation of Deformable Convolution

Deformable Convolutional Networks in PyTorch This repo is an implementation of Deformable Convolution. Ported from author's MXNet implementation. Buil

411 Dec 16, 2022
A PyTorch implementation of Implicit Q-Learning

IQL-PyTorch This repository houses a minimal PyTorch implementation of Implicit Q-Learning (IQL), an offline reinforcement learning algorithm, along w

Garrett Thomas 30 Dec 12, 2022
Official implementation of our paper "Learning to Bootstrap for Combating Label Noise"

Learning to Bootstrap for Combating Label Noise This repo is the official implementation of our paper "Learning to Bootstrap for Combating Label Noise

21 Apr 09, 2022
ADB-IP-ROTATION - Use your mobile phone to gain a temporary IP address using ADB and data tethering

ADB IP ROTATE This an Python script based on Android Debug Bridge (adb) shell sc

Dor Bismuth 2 Jul 12, 2022
Extracts essential Mediapipe face landmarks and arranges them in a sequenced order.

simplified_mediapipe_face_landmarks Extracts essential Mediapipe face landmarks and arranges them in a sequenced order. The default 478 Mediapipe face

Irfan 13 Oct 04, 2022
Benchmark for evaluating open-ended generation

OpenMEVA Contributed by Jian Guan, Zhexin Zhang. Thank Jiaxin Wen for DeBugging. OpenMEVA is a benchmark for evaluating open-ended story generation me

25 Nov 15, 2022
This is an official implementation for "ResT: An Efficient Transformer for Visual Recognition".

ResT By Qing-Long Zhang and Yu-Bin Yang [State Key Laboratory for Novel Software Technology at Nanjing University] This repo is the official implement

zhql 222 Dec 13, 2022
Fast, flexible and easy to use probabilistic modelling in Python.

Please consider citing the JMLR-MLOSS Manuscript if you've used pomegranate in your academic work! pomegranate is a package for building probabilistic

Jacob Schreiber 3k Dec 29, 2022
PyTorch code for our ECCV 2018 paper "Image Super-Resolution Using Very Deep Residual Channel Attention Networks"

PyTorch code for our ECCV 2018 paper "Image Super-Resolution Using Very Deep Residual Channel Attention Networks"

Yulun Zhang 1.2k Dec 26, 2022
This repository holds code and data for our PETS'22 article 'From "Onion Not Found" to Guard Discovery'.

From "Onion Not Found" to Guard Discovery (PETS'22) This repository holds the code and data for our PETS'22 paper titled 'From "Onion Not Found" to Gu

Lennart Oldenburg 3 May 04, 2022
Prototype python implementation of the ome-ngff table spec

Prototype python implementation of the ome-ngff table spec

Kevin Yamauchi 8 Nov 20, 2022
Incremental Cross-Domain Adaptation for Robust Retinopathy Screening via Bayesian Deep Learning

Incremental Cross-Domain Adaptation for Robust Retinopathy Screening via Bayesian Deep Learning Update (September 18th, 2021) A supporting document de

Taimur Hassan 1 Mar 16, 2022
Code used to generate the results appearing in "Train longer, generalize better: closing the generalization gap in large batch training of neural networks"

Train longer, generalize better - Big batch training This is a code repository used to generate the results appearing in "Train longer, generalize bet

Elad Hoffer 145 Sep 16, 2022