From cad050d7c31526be2dcc0e25b2b4aa2082f479f0 Mon Sep 17 00:00:00 2001 From: Sandeep Dasgupta Date: Wed, 6 Jun 2018 10:55:17 -0500 Subject: [PATCH] https://github.com/sdasgup3/binary-decompilation/issues/77: wip --- .../semantics/registerInstructions/xchgl_r32_r32.k | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/x86-semantics/semantics/registerInstructions/xchgl_r32_r32.k b/x86-semantics/semantics/registerInstructions/xchgl_r32_r32.k index df098e7a4..2aa2e357a 100644 --- a/x86-semantics/semantics/registerInstructions/xchgl_r32_r32.k +++ b/x86-semantics/semantics/registerInstructions/xchgl_r32_r32.k @@ -18,10 +18,16 @@ convToRegKeys(R2) |-> concatenateMInt( mi(32, 0), extractMInt( getParentValue(R1 requires notBool sameRegisters(R1, R2) + // There are several possible encodings for the instruction xchgl eax, eax, and + // only the two variants that hard-code one of the operands to be eax are affected. + // These essentially encode to nop. According to this, the following + // should not be nop. + /* rule execinstr (xchgl R1:R32, R1:R32, .Operands) => execinstr(nop .Operands) ... requires sameRegisters(R1, %eax) + */ endmodule module XCHGL-R32-R32-SEMANTICS