bchurchill
commented
9 years ago I think you're right. Another possibility is that the wrong sandbox is being used for the holdout verifier, as I messed with isolating the sandboxes for different verifiers not too long ago.
On 11/01/2015 09:33 PM, Stefan Heule wrote:
This has been causing me a headache for a while, but I'm getting closer to the problem. I'm seeing STOKE find programs that seem to work on all testcases (during the hold_out verification at the end of the search), but are actually not correct. And in fact, if I run |stoke debug verify| with hold_out verification using the same testcases right after, then STOKE tells me the program is wrong. Here's an example:
|Target: seta %ah
Result from STOKE search: movq $0x0, %rax callq .set_pf movq $0xfffffffffffffff8, %rbx cqto callq .move_032_016_edx_r10w_r11w setnbe %dl callq .move_byte_5_of_rbx_to_r9b setnbe %spl cmpl %ebx, %edx retq
Result simplified: movq $0x0, %rax retq |
Clearly the STOKE search result is wrong, even though STOKE reports it as "verified" at the end of the search.
My theory is that the opcode width and opcode tranform is wrong, and takes an _RH instruction, and changes it to an _R8 instruction (or vice versa), but messes the operands up, confusing %ah with %spl, etc (due to the index-off-by-4 thing).
@bchurchill https://github.com/bchurchill: Does that seem possible? Other theories? You wrote this code, so I'm hoping you have a better sense of whether it's doing the right thing or not.
Looking at the code, both transforms seem wrong to me, but I may be misunderstanding. Here's a snipped:
|instr.set_opcode(opc);
// Check that the instruction is valid if (!instr.check()) { return ti; } |
Why do we not have to update the operands? If you change the operand width in the operand width transform, then it seems that one could start with incb %spl (opcode INCB_R8) and change it to opcode INCB_RH. I /think/ the instr.check would pass, and now we have an instruction where the operand type is not right. In fact, it may be still displayed as incb %spl, but it may get executed as incb %ah (because the operand is supposed to have type RH, and interpreting %spl as RH gives you %ah).
— Reply to this email directly or view it on GitHub https://github.com/StanfordPL/stoke/issues/765.
stefanheule
This has been causing me a headache for a while, but I'm getting closer to the problem. I'm seeing STOKE find programs that seem to work on all testcases (during the hold_out verification at the end of the search), but are actually not correct. And in fact, if I run
stoke debug verifywith hold_out verification using the same testcases right after, then STOKE tells me the program is wrong. Here's an example:Clearly the STOKE search result is wrong, even though STOKE reports it as "verified" at the end of the search.
My theory is that the opcode width and opcode tranform is wrong, and takes an _RH instruction, and changes it to an _R8 instruction (or vice versa), but messes the operands up, confusing %ah with %spl, etc (due to the index-off-by-4 thing).
@bchurchill: Does that seem possible? Other theories? You wrote this code, so I'm hoping you have a better sense of whether it's doing the right thing or not.
Looking at the code, both transforms seem wrong to me, but I may be misunderstanding. Here's a snipped:
Why do we not have to update the operands? If you change the operand width in the operand width transform, then it seems that one could start with incb %spl (opcode INCB_R8) and change it to opcode INCB_RH. I think the instr.check would pass, and now we have an instruction where the operand type is not right. In fact, it may be still displayed as incb %spl, but it may get executed as incb %ah (because the operand is supposed to have type RH, and interpreting %spl as RH gives you %ah).