x86isa instruction issues #1528
Comments
|
Brian, thank you so much for reporting these here! I will fix these as soon as I can -- maybe over the next week, but it will probably be by the week after. |
|
This is very interesting! Can you say more about how you found these issues? |
Sorry, I forgot to reply to this before. Once we had a Sail version of the model I was able to adapt a randomised testing tool that I previously built for the Morello project. This picks some instructions randomly, runs them in our Isla symbolic execution tool, then uses the resulting path constraint to pick an initial state with Z3 that should replicate that execution. Finally a test running harness compares the result of execution on different targets; I was using an Intel processor via gdbserver, qemu, and the Sail model itself. |
These were in `x86-call-FF/2-Op/En-M`: 1. An old stack pointer was used to push the return address, instead of the updated stack pointer. 2. The pushed address was the called address instead of the return address. 3. The size of the instruction pointer was the instruction address size, but instead it should be the code segment size. The first two bugs were reported in GitHub Issue #1528. The third bug was found while looking at this instruction to fix the first two bugs.
This was reported in GitHub Issue #1528.
The immediate was not properly sign-extended. This was reported in GitHub Issue #1528.
As part of the ETC project we did some model-based test generation on a version of x86isa translated into the Sail language. As well as identifying some problems with our translation, we encountered some issues which appear to affect the ACL2 model. (These are all in 64-bit user-mode.)
I found several stack instructions didn't use REX.W when they should:
x86-pop-general-registerx86-push-general-registerx86-push-iA couple of instruction misbehave when there's an unnecessary REX.W:
x86-add/adc/sub/sbb/or/and/xor/cmp-test-rax-iuses the wrong size for rax when there's a bogus REX.W on a 8 or 16-bit instruction.x86-sal/sar/shl/shr/rcl/rcr/rol/rorcan use the wrongcountmask.The other issues are more semantically interesting:
shld-spec-16/32/64.x86-call-ff/2-op/en-muses the old stack pointer when writing the return pointer, and writes the wrong value to it.x86-cmovccthe upper 32 bits need to be zeroed when there isn't a move in IA32-e modes.x86-imul-op/en-rmidoesn't sign extend the immediate operand.The text was updated successfully, but these errors were encountered: