[INFO] syncConstraints: Incorrect constraints are inserted

[enlighten5]

Hi!

I noticed that when running SymQEMU, the following error shows up in the log.
[INFO] syncConstraints: Incorrect constraints are inserted
Any idea about what's the reason and how to solve it? (run SymQEMU on objdump and specint benchmarks and observe the same error.)

Thanks!

[vanhauser-thc]

I see this also with very simple targets. no clue why.

[sebastianpoeplau]

What the message means is that SymQEMU is trying to add path constraint that contradicts the already asserted statements. For example, you would see this error if x > 7 was already part of the constraints and SymQEMU then tried to add x == 2.

Usually, it's a sign that we've implemented an instruction incorrectly or that we're missing something. The latter is typically the case when uninstrumented code (such as QEMU's helpers for some CISC instructions) modifies memory that is subsequently read by instrumented code (which then makes wrong assumptions about its content). A minimal example would be very helpful to debug the issue.