muellerberndt / laser-ethereum

Symbolic virtual machine for Ethereum
MIT License
68 stars 20 forks source link

No real value exists in class environment #39

Open KennyFood opened 6 years ago

KennyFood commented 6 years ago

My question is we don't know the exact value of environment arguments. In the first place, I'm wondering what the values we append to the machine stack are when we deal with the opcode CALLDATALOAD. And i find the code: `elif op == 'CALLDATALOAD':

unpack 32 bytes from calldata into a word and put it on the stack

            op0 = state.stack.pop()

            try:
                offset = helper.get_concrete_int(simplify(op0))
                b = environment.calldata[offset]`

The comment which suggests we put a word on the stack make me confused. Then I turn to the environment.calldata and i find the code: `# Initialize the execution environment

    environment = Environment(
        self.accounts[main_address],
        BitVec("caller", 256),
        [],
        BitVec("gasprice", 256),
        BitVec("callvalue", 256),
        BitVec("origin", 256),
        calldata_type=CalldataType.SYMBOLIC,
    )

I think the function BitVec belongs to Z3 so I also read some blogs about symbolic execution. Finally I don't get the answer :(. In total, what are real values of arguments such as gasprice and callvalue. Are they symbols? unpack 32 bytes from calldata into a word and put it on the stack` What does the comment mean? What if we need compare the callvalue with a exact value? I'm sorry I know my question is not clear. I hope your support @b-mueller . Thanks a lot!

KennyFood commented 6 years ago

@b-mueller Hi, sorry to bother you, but I can't find your contact information. So May I have your Email please? I really want to contact you. BTW, It's not about the question. Thank you so much.