Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Replace MemWord with BV #359

Open
langston-barrett opened this issue Dec 13, 2023 · 1 comment
Open

Replace MemWord with BV #359

langston-barrett opened this issue Dec 13, 2023 · 1 comment

Comments

@langston-barrett
Copy link
Contributor

Consider the MemWord type:

-- | This represents a bitvector value with `w` bits.
--
-- Operations on it require the `MemWidth` constraint to be satisfied, so in practice
-- this only works for 32 and 64-bit values.
newtype MemWord (w :: Nat) = MemWord { memWordValue :: Word64 }

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
Copy link
Contributor

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants