macaw-x86-symbolic: Fix idiv/div semantics

When converting a Macaw value with the Macaw type `TupleType [x_1, ..., x_n]`
to Crucible, the resulting Crucible value will have the Crucible type
`StructType (EmptyCtx ::> ToCrucibleType x_n ::> ... ::> ToCrucibleType x_1)`.
(See `macawListToCrucible(M)` in `Data.Macaw.Symbolic.PersistentState` for
where this is implemented.) Note that the order of the tuple's fields is
reversed in the process of converting it to a Crucible struct. This is a
convention that one must keep in mind when dealing with Macaw tuples at the
Crucible level.

As it turns out, the part of `macaw-x86-symbolic` reponsible for interpreting
the semantics of the `idiv` instruction (for signed quotient/remainder) and the
`div` instruction (for unsigned quotient/remainder) were _not_ respecting this
convention. This is because the `macaw-x86-symbolic` semantics were returning a
Crucible struct consisting of `Empty :> quotient :> remainder)`, but at the
Macaw level, this was interpreted as the tuple `(remainder, quotient)`, which
is the opposite of the intended order. This led to subtle bugs such as those
observed in #393.

The solution is straightforward: have the `macaw-x86-symbolic` semantics
compute `Empty :> remainder :> quotient` instead. Somewhat counterintuitive,
but it does work.

Fixes #393.

x86_symbolic/src/Data/Macaw/X86/Crucible.hs

@@ -674,17 +674,24 @@ divNatReprClasses r x =
     M.DWordRepVal -> x
     M.QWordRepVal -> x
 
+-- | Construct a symbolic Macaw pair. Note that @'mkPair' sym x y@ returns the
+-- pair @(y, x)@ and /not/ @(x, y)@. This is because Macaw tuples have the order
+-- of their fields reversed when converted to a Crucible value (see
+-- 'macawListToCrucible' in "Data.Macaw.Symbolic.PersistentState" in
+-- @macaw-symbolic@), so we also reverse the order here to be consistent with
+-- this convention. (Not doing this can cause serious bugs, such as
+-- <https://github.com/GaloisInc/macaw/issues/393>).
 mkPair :: forall sym bak x y
        .  (IsSymBackend sym bak, KnownRepr TypeRepr x, KnownRepr TypeRepr y)
        => Sym sym bak
        -> RegValue sym x
        -> RegValue sym y
-       -> IO (RegValue sym (StructType (EmptyCtx ::> x ::> y)))
+       -> IO (RegValue sym (StructType (EmptyCtx ::> y ::> x)))
 mkPair sym q r = do
-  let pairType :: Ctx.Assignment TypeRepr (EmptyCtx ::> x ::> y)
+  let pairType :: Ctx.Assignment TypeRepr (EmptyCtx ::> y ::> x)
       pairType = Ctx.empty Ctx.:> knownRepr Ctx.:> knownRepr
-  let pairRes :: Ctx.Assignment (RegValue' sym) (EmptyCtx ::> x ::> y)
-      pairRes = Ctx.empty Ctx.:> RV q Ctx.:> RV r
+  let pairRes :: Ctx.Assignment (RegValue' sym) (EmptyCtx ::> y ::> x)
+      pairRes = Ctx.empty Ctx.:> RV r Ctx.:> RV q
   evalApp' sym (\v -> pure (unRV v)) $ MkStruct pairType pairRes
 
 

x86_symbolic/tests/pass/T393-division.c

@@ -0,0 +1,47 @@
+// A regression test for #393 which ensures that macaw-x86-symbolic's semantics
+// for the `idiv` (signed division) and `div` (unsigned division) instructions
+// compute the correct results.
+//
+// GCC is quite clever at optimizing away division-related instructions when one
+// of the operands is a constant, so we have to define things somewhat
+// indirectly to ensure that the resulting x86-64 assembly actually does contain
+// `idiv` and `div`.
+
+int __attribute__((noinline)) mod_signed(int x, int y) {
+  return x % y;
+}
+
+int __attribute__((noinline)) test_mod_signed(void) {
+  return mod_signed(1, 2);
+}
+
+int __attribute__((noinline)) div_signed(int x, int y) {
+  return x / y;
+}
+
+int __attribute__((noinline)) test_div_signed(void) {
+  return !div_signed(1, 2);
+}
+
+unsigned int __attribute__((noinline)) mod_unsigned(unsigned int x, unsigned int y) {
+  return x % y;
+}
+
+unsigned int __attribute__((noinline)) test_mod_unsigned(void) {
+  return mod_unsigned(1, 2);
+}
+
+unsigned int __attribute__((noinline)) div_unsigned(unsigned int x, unsigned int y) {
+  return x / y;
+}
+
+unsigned int __attribute__((noinline)) test_div_unsigned(void) {
+  return !div_unsigned(1, 2);
+}
+
+void _start(void) {
+  test_mod_signed();
+  test_div_signed();
+  test_mod_unsigned();
+  test_div_unsigned();
+};