Opcode NOT operation is confused about oyente HOT 6 CLOSED

Can you please check this @inian?

from oyente.

Hey, so I think -1 - x is used when x is not a symbolic expression and ~ x is used when x is a symbolic expression where ~ is the z3 bvnot

from oyente.

link here python has built-in ~ operator for a real value. In the link, ~ equals to (-x-1) not (-1-x). Anyway, in some test cases I tried ~x the result is correct but some I tried
(2**256 - 1) - x is correct while ~x is incorrect. What do you think about this @inian ?

from oyente.

Hey just realized that the entire code can just be simplified to

first = stack.pop(0)
computed = ~first
stack.insert(0, computed)

can you give me an example where ~x is incorrect? I will also check

from oyente.

"code" : "0x600019600055" which is converted to opcodes:
[1] PUSH1 0x00
[2] NOT
[4] PUSH1 0x00
[5] SSTORE
And the result should be:
"0x00" : "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff"

The number we care about here is 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff which is the result of:
[1] PUSH1 0x00
[2] NOT
This is the test case not0 in vmBitwiseLogicOperationTest.json file

from oyente.

@luongnt95 can u verify if this is fixed?

from oyente.