Helpers for constructing bitvectors 0 and 1

langston-barrett commented 7 months ago

It's common to construct literal bitvectors representing 0 or 1:

The best way to do that in the current interface is:

bvLit sym w (BV.zero w)
bvLit sym w (BV.one w)

This is a bit of a pain, since you have to repeat the width repr, and to use functions from two separate packages. Instead, it might be nice to export

bvZero, bvOne :: IsSymInterface sym => NatRepr w -> IO (SymBV sym w)

The names also make the intent more obvious.

sauclovian-g commented 7 months ago

This is something of a drive-by comment because I don't know the context, but: if you have zero and one you almost always also want minusone too. Or allones, or some such name for that value.

langston-barrett commented 7 months ago

It looks like we have helpers for all of these except bvOne already:

  -- | Return the bitvector of the desired width with all 0 bits;
  --   this is the minimum unsigned integer.
  minUnsignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
  minUnsignedBV sym w = bvLit sym w (BV.zero w)

  -- | Return the bitvector of the desired width with all bits set;
  --   this is the maximum unsigned integer.
  maxUnsignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
  maxUnsignedBV sym w = bvLit sym w (BV.maxUnsigned w)

  -- | Return the bitvector representing the largest 2's complement
  --   signed integer of the given width.  This consists of all bits
  --   set except the MSB.
  maxSignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
  maxSignedBV sym w = bvLit sym w (BV.maxSigned w)

  -- | Return the bitvector representing the smallest 2's complement
  --   signed integer of the given width. This consists of all 0 bits
  --   except the MSB, which is set.
  minSignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
  minSignedBV sym w = bvLit sym w (BV.minSigned w)

A related question, then, is whether it would be worth it to add "aliases" like bvZero for minUnsignedBv. This would have the downside of providing two names for the same function, but would have the upside of being more concise and potentially convey intent better.

langston-barrett commented 7 months ago

A related question, then, is whether it would be worth it to add "aliases" like bvZero for minUnsignedBv. This would have the downside of providing two names for the same function, but would have the upside of being more concise and potentially convey intent better.

One data point in favor of such an alias: there are only two uses of minUnsignedBv in Galois repos, and both of them are in What4 source code, whereas the explicit construction given in the OP is widespread.

GaloisInc / what4

Helpers for constructing bitvectors 0 and 1 #257