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.

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:

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:

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

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 구현에서 발생한 문제이므로, 다른 방식으로 구현함으로써 일단은 피해갈 수 있을 것 같습니다.

감사합니다.

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 결과를 냄.

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

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

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

Bumps node-notifier from 8.0.0 to 8.0.1.

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.