macaw-x86: Handle sign-extended immediates in def_push

See `Note [Sign-extending immediate operands in push]` in
`Data.Macaw.X86.Semantics` for the full story. I have also added a test case
in `macaw-x86-symbolic` which ensures that the stack-pointer-decrementing
logic behaves as one would expect.

Bumps in the `flexdis86` submodule to bring in GaloisInc/flexdis86#37.

Fixes #235.

deps/flexdis86

@@ -1 +1 @@
-Subproject commit 6d6e8c39e754dc4c9910b1c0dc494e2eef8e309f
+Subproject commit 9b899ed652c80dd22aa7dd9f6920d0d13a077bf6

x86/src/Data/Macaw/X86/Semantics.hs

@@ -374,7 +374,7 @@ def_pop =
 
 def_push :: InstructionDef
 def_push =
-  defUnary "push" $ \_ii val -> do
+  defUnary "push" $ \ii val -> do
     Some (HasRepSize rep v) <-
       case val of
         F.SegmentValue _ ->
@@ -399,6 +399,22 @@ def_push =
           pure $ Some $ HasRepSize DWordRepVal $ getImm32 i
         F.QWordImm (F.UImm64Concrete  w) ->
           pure $ Some $ HasRepSize QWordRepVal $ bvLit n64 (toInteger w)
+        -- See Note [Sign-extending immediate operands in push]
+        F.ByteSignedImm w ->
+          let bvW = bvLit n8 (toInteger w) in
+          pure $ if F.iiPrefixes ii ^. F.prOSO
+                 then Some $ HasRepSize WordRepVal  $ sext n16 bvW
+                 else Some $ HasRepSize QWordRepVal $ sext n64 bvW
+        F.WordSignedImm w ->
+          let bvW = bvLit n16 (toInteger w) in
+          pure $ if F.iiPrefixes ii ^. F.prOSO
+                 then Some $ HasRepSize WordRepVal bvW
+                 else Some $ HasRepSize QWordRepVal $ sext n64 bvW
+        F.DWordSignedImm w
+          |  F.iiPrefixes ii ^. F.prOSO
+          -> fail "push: Unexpected 32-bit immediate with 16-bit operand size"
+          |  otherwise
+          -> pure $ Some $ HasRepSize QWordRepVal $ sext n64 $ bvLit n32 (toInteger w)
         _ -> fail $ "Unexpected argument to push"
     let repr = repValSizeMemRepr rep
     old_sp <- get rsp
@@ -407,6 +423,30 @@ def_push =
     MemoryAddr new_sp repr .= v
     rsp     .= new_sp
 
+{-
+Note [Sign-extending immediate operands in push]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The `push` instruction is surprisingly nuaned with respect to how large
+immediate operands can be. The ISA manual
+(https://www.felixcloutier.com/x86/push) says this: "If the source operand is
+an immediate of size less than the operand size, a sign-extended value is
+pushed on the stack." So what is the operand size? In 64-bit mode, the default
+operand size for the `push` instruction is 64 bits (ignoring the REX prefix),
+and it can be changed to 16 bits if an operand-size override prefix is
+specified. The story is different for modes besides 64-bit mode, but for now,
+we assume the semantics of 64-bit mode. (If this causes issues for you, please
+file an issue.)
+
+In implementation terms, whenever we try to push a {Byte,Word,DWord}SignedImm,
+we first check if prOSO is set. If prOSO is set, we return a 16-bit operand,
+sign-extending if necessary. If prOSO is not set, we return a 64-bit operand
+instead, again sign-extending if necessary.
+
+Getting this right is important since we use the size of the sign-extended
+operand to determine how many bytes to decrement the stack pointer by. We don't
+want to use the size of the source immediate, which could be smaller.
+-}
+
 -- | Sign extend ax -> dx:ax, eax -> edx:eax, rax -> rdx:rax, resp.
 def_cwd :: InstructionDef
 def_cwd = defNullary "cwd" $ do

x86_symbolic/tests/pass/T237.c

@@ -0,0 +1,36 @@
+#include <stdint.h>
+
+// A test case which ensures that the `push` instruction decrements the stack
+// pointer by 8 bytes in 64-bit mode, even if the source operand is an
+// immediate that is less than 8 bytes.
+
+int __attribute__((noinline)) test_push() {
+  uint64_t ret = 0;
+  __asm__(
+    // 1. Save the address of the stack pointer to %13.
+    "leaq 0x0(%%rsp), %%r13;"
+    // 2. Push an immediate (which should be sign-extended to 8 bytes) on the
+    //    stack.
+    "pushq $0x0;"
+    // 3. Save the difference between the old and new stack pointer addresses
+    //    to %r13.
+    "leaq 0x0(%%rsp), %%r14;"
+    "subq %%r14, %%r13;"
+    // 4. Pop the previously pushed immediate. (We no longer need %r14, so it
+    //    is fine to write a temporary value here.)
+    "popq %%r14;"
+    // 5. Check if the stack pointer address difference is 8 bytes.
+    //    If so, return 1. Otherwise, return 0.
+    "cmpq $0x8, %%r13;"
+    "sete %%al;"
+    "movzbq %%al, %0;"
+    : "=r"(ret) /* Outputs */
+    : /* Inputs */
+    : "%r13", "%r14" /* Clobbered registers */
+    );
+  return ret;
+}
+
+void _start() {
+  test_push();
+}