Stack filled with wrong data.

[yaroslavyaroslav]

Description

I'm trying to access to a stack into my custom detector.

I'm doing it like global_state.mstate.stack[-4].

And I've got full stack filled with exact this data call_value1, instead of a useful one.

So regarding to this my detector is failing. Since it doesn't expect this value.

This value appears from exact here sympbolic.execute_contract_creation as line 191.

Nailing it down leads me that solver just coping that value over and over again, to fill stack up to required depth to perform a CALL. And worth to say, that this behaviour appears occasionally. I mean in some contracts my custom detector working well (e.g. stack filled with the right data), but on other ones it filled with such trash.

So I'm confused in both ways:

1. Why execute_contract_creation even called in the detector scope?
2. Why mythril doesn't emulate stack rather to fill with trash data?

[norhh]

Why execute_contract_creation even called in the detector scope? The detectors are executed whenever they encounter an opcode, call_value1 exists in the stack because an instruction triggered msg.value(likely the payable check for constructor) during the execution of constructor, which is the callvalue1.

Why mythril doesn't emulate stack rather to fill with trash data? It's not a trash value, as call_value1 is possibly constrained with some constraints. This is how symbolic execution works, Since there is no information on what the value can be, a symbol is used which is further constrained during the execution.

[yaroslavyaroslav]

It's not a trash value, as call_value1 is possibly constrained with some constraints Yep, I've got that. But why they (symbolic values) appears at that stage? I mean, I looked carefully at your detectors code — there's no solve this boi pre-step. You're just reading a values from a memo or a stack or a machine state, setting some constraints, and if they succeeded you mark it as a solved.

Anyway. Is there a way how to reach/solve those values under that symbolic placeholder, to check whether they fits constraints or not?

[norhh]

some constraints, and if they succeeded you mark it as a solved. Yes I append some new constraints using these values to path condition of the received global state. When the new path condition has a solution, that means the conditions appended are feasible for the global state that I received.

[yaroslavyaroslav]

@norhh could you please point me out where exactly in code do you do this?

[norhh]

This is the function which solves the constraints and gets the transaction sequence that satisfies those constraints: https://github.com/ConsenSys/mythril/blob/1d4e90f577702ccbfec152ad58c40cc2b7fc4a89/mythril/analysis/module/modules/suicide.py#L78

[yaroslavyaroslav]

@norhh thank you for pointing me out.

Could you as well point me out, how can I set a constraint for a case that contract having a given value in memory on the given step. The code above did not working well pretty often.

offset = state.mstate.stack[-2] # let's assume that this stack depth lays memory pointer.

mem_value = state.mstate.memory.getword(offset) # let's assume that I'm sure that there should be a two bytes pointer like 0x12fd

constraint += mem_value == solver.simbolic_factory(0x12fd, 256)

So I have a case when this is returns as unsat. I'm printing mem_value out in the debugging purposes and it prints out exact that number 0x12fd in a symbolic type. So it obviously is satable. But it fails to be satisfied with this code. Also if I change the constraint to following it will be satisfied constraint += mem_value > solver.simbolic_factory(1, 256).

Is there a way how I can work around that?

[norhh]

for getwordat(), I think you will get something like 64 bits. Add print statements to your code (or log.info if you prefer that) to check if you are getting what you want for some super simple examples.

[yaroslavyaroslav]

@norhh It's actually throws an error with the statement that the worddata (the value that is compared to it) should be 256. Anyway this is exactly what I'm doing, wrapping the code with the print around and trying to figure out how add memory value constraints.

And here we're coming to the my original question: On my test case I got call_value1 print output for state.mstate.stack[-2] and it kept there forever. I mean it never gets desymbilicated (at least within that test case). On some other cases it gets desymbalicated, but I speculate that it's direct opposite actually, like It's the less set that is working well, and a bigger one, that is never got desymbolicated.