mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-29 21:44:11 +03:00
a6ff58f473
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. |
||
|---|---|---|
| .. | ||
| src/Data/Macaw/X86 | ||
| tests | ||
| LICENSE | ||
| macaw-x86-symbolic.cabal | ||