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.
This bumps the `what4` submodule to the 1.6.* version series and updates the
`.cabal` files in the `macaw` repo accordingly.
Bumping the `what4` submodule also requires bringing in corresponding changes
in the `crucible`, `llvm-pretty`, and `llvm-pretty-bc-parser` submodules, so I
have done that as well.
Refinement frequently tried to add duplicate edges to the cfg
when encountering jump tables, since jump tables often have common targets
(e.g. because of a `default` case).
Instead of panicking, this is now handled as a benign case where no edge
insertion is needed.
This introduces a `HasMacawLazySimulatorState` data type, which provides a
"classy lens" for accessing a `MacawLazySimulatorState` within some Crucible
personality type. It also generalizes the lazy `macaw-symbolic` memory model in
`Data.Macaw.Symbolic.Memory.Lazy` to be polymorphic over
`HasMacawLazySimulatorState` instances. The upside is that it is now possible
to use the lazy memory model at other personality types besides just
`MacawLazySimulatorState`, making it much easier to extend the memory model.
Because there is a `HasMacawLazySimulatorState` instance for
`MacawLazySimulatorState`, existing code that uses `MacawLazySimulatorState`
should continue to compile without changes.
Fixes#357.
Rather than `error`ing, we now generate fresh constants for all possible
`macaw` `Type`s that are supplied to the `MacawFreshSymbolic` operation.
Fixes#301.
Now that `macaw-aarch32` and `macaw-ppc` properly handle position-independent
code, the `InstructionAtUnmappedAddr` error (which could only be thrown if an
IP address was found in position-independent code) is never thrown. Let's
delete it.
`macaw-ppc` was previously assuming that addresses are absolute, which is not
true for position independent executables. Extracting the offset from the
address is sufficient for our purposes here (note that taking the offset from
the `MemSegmentOffset` would not be right, as that offset is relative to the
segment start).
This is the exact same issue that was noticed in
37d8029c00
(in `macaw-aarch32`), but that commit forgot to fix things on the `macaw-ppc`
end.
