search

PLASinCNU / op-eliminator

GNU General Public License v2.0
1 stars 0 forks source link

Overflow 이슈 #10

Closed manggoguy closed 4 years ago

manggoguy commented 5 years ago

miasm 도 Bitvec 를 이용합니다. Bitvec를 이용하는 와중에 전체 레지스터의 값을 제한하니 원래 되야 하는 것이 unsat으로 나오게 됩니다. 그래서 ExprCond를 구성하는 레지스터들만 값을 제한하였습니다. 이후에 어떻게 할건지 고민해야될 문제 같습니다.

fcmonoid commented 5 years ago

종환이 말대로, 덧셈, 뺄셈등 모든 연산을 성균이가 준 https://github.com/Z3Prover/z3/issues/574 이 이슈에 있는 bvumul_noovfl 같은 것으로 바꾸어 넣으면 해결되지 않을까 하는데 동의한다. https://css.csail.mit.edu/6.858/2019/labs/lab3.html 의 앞부분도 한번 참고 해보길.

mi-asm이나 python-z3 를 약간 건드려야할 수도 있겠다.

fcmonoid commented 5 years ago

관련 이슈: #13 , #8 지금은 보고서 작업때문에 close -> 좀 나중에 하기

fcmonoid commented 4 years ago

다른 Issue에서 open했음 (https://github.com/PLASLaboratory/op-eliminator/issues/15#issue-517748637)