src/IR/BitVec.hs

module IR.BitVec where

import IR.Boolean

type BitVec = [BExpr]

bvConst :: Int -> Int -> BitVec
bvConst width val = [if testBit i then BTrue else BFalse | i <- [0..width-1]]
  where testBit i = (val `div` (2^i)) `mod` 2 == 1

bvVar :: Int -> Int -> BitVec
bvVar start width = [BVar (start + i) | i <- [0..width-1]]

bvNot :: BitVec -> BitVec
bvNot = map bnot

bvAnd :: BitVec -> BitVec -> BitVec
bvAnd = zipWith band

bvOr :: BitVec -> BitVec -> BitVec
bvOr = zipWith bor

bvXor :: BitVec -> BitVec -> BitVec
bvXor = zipWith bxor

halfAdder :: BExpr -> BExpr -> (BExpr, BExpr)
halfAdder a b = (bxor a b, band a b)

fullAdder :: BExpr -> BExpr -> BExpr -> (BExpr, BExpr)
fullAdder a b cin =
  let (s1, c1) = halfAdder a b
      (s2, c2) = halfAdder s1 cin
  in (s2, bor c1 c2)

bvAdd :: BitVec -> BitVec -> BitVec
bvAdd [] [] = []
bvAdd as bs = go as bs BFalse
  where
    go [] [] _ = []
    go (a:as') (b:bs') cin =
      let (s, cout) = fullAdder a b cin
      in s : go as' bs' cout
    go _ _ _ = []

bvEq :: BitVec -> BitVec -> BExpr
bvEq as bs = foldr band BTrue (zipWith xnor as bs)
  where xnor a b = bnot (bxor a b)