Z3을 처음 접했고 온라인 Python 튜토리얼을 확인하고있었습니다.Z3으로 오버플로 확인
그런 다음 BitVecs에서 오버플로 동작을 확인할 수 있다고 생각했습니다.
는이 코드 썼다x = BitVec('x', 3)
y = Int('y')
solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))
및 I는 기대 하였다 Y = 7 X = 7 (즉, 값이 동일하지만, X + 1은 0 Y되기 때문에 후계자하지 + 1 8)
그러나 Z3은 [y = 0, x = 0]으로 대답합니다.
내가 뭘 잘못하고 있니?
난 당신이 뭔가 잘못을하고 있다고 생각하지 않습니다는 BV2Int이 버그가 다음과 같습니다
x = BitVec('x', 3)
prove(x <= 3)
prove(BV2Int(x) <= 3)
Z3py가 첫 번째 증명,하지만 두 번째의 카운터 - 예를 x=0을 제공합니다. 그건 맞지 않아. (유일한 설명은 이상한 파이썬 일 수도 있지만, 어떻게 보이지는 않습니다.)
+은 파이썬 바인딩에서 비트 벡터를 부호있는 숫자로 처리하는지 여부에 따라 달라집니다. 나는 그것이 사실이라고 믿는다. 그러나 BV2Int은 서명되지 않은 값으로 간주하여 처리하지 않을 수 있습니다. 이것은 문제를 더욱 복잡하게 만듭니다.
어쨌든 BV2Int처럼 보이지는 않습니다. 나는 Z3 사람들의 공식적인 답변이있을 때까지 그것에서 떨어져있을 것입니다.
이것에 대해 우려하는 다른 사람들에게 이것은 어느 시점에서 해결 된 것 같습니다. 이 예제를 최신 버전의 z3 (초기 게시물 이후 몇 년)으로 다시 실행했으며 7,7을 반환합니다.