-
Notifications
You must be signed in to change notification settings - Fork 12
`bv sized` migration guide
Ben Selfridge edited this page Jun 11, 2020
·
2 revisions
This is a WIP migration guide for porting downstream libraries after the what4/bv-sized change.
- Constants (no Num instance): "0" becomes "BV.zero w"
- All Data.Bits operations
First pass: resolving Integer ~ BV.BV w mismatch
- Basically, there's two scenarios -- one where you want to turn the Integer into a BV w, and one where you just want to convert.
- asUnsignedBV x ==> BV.asUnsigned <$> asBV x
- fromConcreteUnsignedBV x ==> BV.asUnsigned (fromConcreteBV x)
- bvLit sym w x ==> bvLit sym w (BV.mkBV w x)
- i <- [0..n] ==> i <- BV.enumFromToUnsigned (BV.zero w) (BV.mkBV w n)
- minSigned ==> BV.minSigned
- functions from parameterized-utils that return Integers ==> functions from bv-sized that return BVs
- Num operators ==> BV operators
- Bits operators ==> BV operators
- shifting/masking ==> BV concat/select/trunc/zext/sext
- bvLit sym w (intValue w) ==> bvLit sym w (BV.width w)
Second pass: resolving "no Num instance"
- 0 ==> BV.zero w
- 1 ==> BV.one w
- for anything else, you probably should use BV.mkBV w