Question about result of solver for ConcatExpr of ReadExpr

[Reaper Lu (Dingisoul)]

Hi Vitaly,

      I have encountered a problem about the solver result for a ConcatExpr of ReadExpr, the solver result has confused me.

Bellow is the log from s2e

[State 8] Expr: (Read w8 0x0 v49_60ba40002108_61) Constraints: (Not (Eq 0x0 (ReadLSB w32 0x0 v41_0x40002108_0x60ba_0_4_49))) [State 8] Solve Expr: (Read w8 0x0 v49_60ba40002108_61) Value: 0x0

The above logs are mean to solve the Constraints to get value of the Read Expression with state->solver()->getValue().

However, as we can see, the result is not as correct as we thought.

I have also used the getRange() to get the result range, which start from 0x0 to 0xff.

One possible reason I think can explain this problem : The width of read in constraint is 32,

the width of the read expression I want to solve is 8, so the solver might think that other bytes can be non-zero to make the constraints correct

I designed my solve function using ReadExpr except ConcatExpr of ReaExprs is to avoid the shift expression tangling the constraints, I'm not sure if my design is right

Currently, I always return the maximum value of the result, Could you provide me with some solutions or point out any mistakes of my understanding?

Thanks,

Dingisoul

[Vitaly Chipounov]

Hi,

It looks like you have two symbolic values: v49_60ba40002108_61 and v41_0x40002108_0x60ba_0_4_49.

The "Value 0x0" comes from the first one, which is unconstrained and can be anything.

Make sure you didn't create a symbolic value accidentally.

Vitaly

--
You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/0bbba4ac-57e3-405e-adf3-08a4d8446e71n%40googlegroups.com.

[Reaper Lu (Dingisoul)]

Sorry about my mistake, I forget to paste one constraint

Constraints: (Not (Eq 0x0 (ReadLSB w32 0x0 v41_0x40002108_0x60ba_0_4_49))) (Eq (Read w8 0x0 v49_60ba40002108_61) (Read w8 0x0 v41_0x40002108_0x60ba_0_4_49))

[State 8] Solve Expr: (Read w8 0x0 v49_60ba40002108_61) Value: 0x0

Those are the contraints ( the EqExpr make the two constraints equally) and the ReadExpr I want to solve. 

Thanks,

Dingisoul

[Vitaly Chipounov]

Hi,

Not sure I see the issue, value looks ok. As you've mentioned, the constraint applies to the lower bits only, so 0 is a valid solution.

Vitaly

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/5f8d898a-8b55-4235-af03-1c9e5bd705e1n%40googlegroups.com.

[Reaper Lu (Dingisoul)]

Hi Vitaly,

In order to speed up my implementation, before solving the constraints, I will use the state->solver()->evaluate() function to check if the original value (0x0) of the newly created symbol is already correct.

I will only use the solver when the evaluate() function returns false.

In this case, only the lowest byte evaluates to false, so I use the solver, and it returns 0. As a result, the final result of this 32-bit symbolic value is 0, even though there is a "Not Equal" expression. This has tangled the entire execution.

I think I understand your point, and I will try to solve this issue in a different way.

Thanks, Dingisoul