From 79e1a39038b5307b96a3cb1ee684002c6927e851 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 12 Jul 2024 15:12:57 -0400 Subject: [PATCH] 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 | 15 ++++-- x86_symbolic/tests/pass/T393-division.c | 47 ++++++++++++++++++ x86_symbolic/tests/pass/T393-division.opt.exe | Bin 0 -> 9552 bytes .../tests/pass/T393-division.unopt.exe | Bin 0 -> 9664 bytes 4 files changed, 58 insertions(+), 4 deletions(-) create mode 100644 x86_symbolic/tests/pass/T393-division.c create mode 100755 x86_symbolic/tests/pass/T393-division.opt.exe create mode 100755 x86_symbolic/tests/pass/T393-division.unopt.exe diff --git a/x86_symbolic/src/Data/Macaw/X86/Crucible.hs b/x86_symbolic/src/Data/Macaw/X86/Crucible.hs index 998e0a2e..18dacdf0 100644 --- a/x86_symbolic/src/Data/Macaw/X86/Crucible.hs +++ b/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 +-- ). 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 diff --git a/x86_symbolic/tests/pass/T393-division.c b/x86_symbolic/tests/pass/T393-division.c new file mode 100644 index 00000000..30076d66 --- /dev/null +++ b/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(); +}; diff --git a/x86_symbolic/tests/pass/T393-division.opt.exe b/x86_symbolic/tests/pass/T393-division.opt.exe new file mode 100755 index 0000000000000000000000000000000000000000..b358e47da7b5acc335f64f9c7b30fcc2b7dcd5e4 GIT binary patch literal 9552 zcmeHN!Alfj6n|@$TE=b>5g0k72O}JI)q{1Y2`fEBX(>dPY1bKb!JUoNeUlVIjR)0?{ z&c*8up!gL%v%jVX-mlBy`rJUg{vt%yS3Z}^~zbauiu#)X4+#-|vU&)C3tf^j+%bbbKpEOD$TfAd7$pwt)9u8+n_SnZH0<-NgrSpACX$CAhoTnh+3AkS=)$7O0tnwd|gz6 zmma(b9{d;dAYzLKdhmfr=|zMdyc7aGhzho7CC=USNOe+<-=ZhMort=dj!ayL2MN)G(2yBg)!#Sf$aOA zfky|v&BjMZi@wb4c|3a)Qp%J9N&%&SQa~x76i^B%1(X6x0i}Ra;2%}sYx%bCJ;%~B z>1zw=)coDnh5K{Y=F^kC6P$RC5AZMW={Gx>%jMj}B8Cfl>ZhRoR;K)3ru<39EpT|x zP|~^7a^2o8-Hlo91w9?#E!i;}062RNw|lrvz&6@Df$fzk1(X6x0i}RaKq;UUPzopo zlmbctrGQf4zfb`G6Gro0=@PzSzpt{axMUQb_O}3r>*J?ft^x~M*ZOZ4w5%!WfC9?x z2mfJ({CUVvL4Ff>hu`kSma88`m`@Hdd(>dkk%`EkHsuF!uP@)^iidih;0 ze*y5Z75Z-h9mXNQ-OE2M`E4yN`?T7gzEsRgY4!DblOCw6PuXGp^@avL(6ozSBrk9H z!%Cs}oXf9R2f%vxw|Yb6NHP+S>HWeola>Lok%}cF12Ho!k!U<@P;3}|$)u6ALJ7;Q&aZXYh8Yf7Az_%Y zun>B3Bx;5Fz*`CF2l*6>Tc$n`OX)+2_>h^fMuhG_eW}Q$a9t!UbjuvJgl-NR7ZRbU zDfIq$G-}2ycyoVgcpr*k;jeUPJkP>&Cz_4A8_%^cqQk+<=eZW1cd6k*^6-gSWQQTb z&#*JILid~JZk+iYVqvY<+8{uTU%$|TGObDH%<;(3naiP2bix7o0S3r7SINWfJe>P` zz0=!MJ4pNvDrAjVzs*!z3Z7?dJaqANhm4|L5YF6}Vf>yi#ovivT(Gm!IeR|;7eoG4 A5dZ)H literal 0 HcmV?d00001