GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-12-04 03:13:56 +03:00
Code Issues Projects Releases Wiki Activity
99039964b8
what4/bv-sized-migration.md
Ben Selfridge 213b23099c
migration to bv-sized representation (#34) 
Update all `what4`-related packages to to concrete computation using the `bv-sized` library for fixed (but arbitrary) sized bitvector values.

Currently, the bitvector abstract domain computations are still being done directly on raw integers; we can revisit this in the future.

Co-authored-by: Ben Selfridge <benselfridge@000279.local>
Co-authored-by: Rob Dockins <rdockins@galois.com>
2020-06-04 15:07:57 -07:00

1.0 KiB
Raw Blame History

This is a WIP migration guide for porting downstream libraries after the what4/bv-sized change.

  • Constants (no Num instance): "0" because "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