search

GaloisInc / macaw

Open source binary analysis tools.
BSD 3-Clause "New" or "Revised" License
190 stars 19 forks source link

Replace `MemWord` with `BV` #359

Open langston-barrett opened 7 months ago

langston-barrett commented 7 months ago

Consider the MemWord type:

https://github.com/GaloisInc/macaw/blob/aaa5ea123429871b12cd406d694fdf6b30351d68/base/src/Data/Macaw/Memory.hs#L260-L264

and BV:

https://github.com/GaloisInc/bv-sized/blob/d8b0e400101d4491859d5060cf491153ae09ab86/src/Data/BitVector/Sized/Internal.hs#L89-L98

These maintain similar invariants (though the invariant is undocumented in the case of MemWord), and the latter seems strictly more general than the former. Perhaps we could replace MemWord with BV? This would be advantageous because libraries like What4 use BV, so we wouldn't have to convert between them. It also probably wouldn't be too hard to do, given that the constructor of MemWord is hidden.

It does appear that MemWord implements Bits, and BV does not. I'm not clear if clients use the Bits instance of MemWord, nor whether one could be provided for BV.

RyanGlScott commented 7 months ago

They are similar, but I think of them as conceptually different things, since MemWords are always guaranteed to be machine words that are 32 or 64 bits. Perhaps it would make sense to make MemWord a newtype around BV to share some parts of their implementations, but I'm not sure about making them the same type—I worry about the possibility of mixing up general-purpose BVs with machine-specific MemWords, especially if we use bv-sized in more parts of macaw.