-- |
-- Module      : Verismith.Verilog.Eval
-- Description : Evaluation of Verilog expressions and statements.
-- Copyright   : (c) 2019, Yann Herklotz Grave
-- License     : GPL-3
-- Maintainer  : yann [at] yannherklotz [dot] com
-- Stability   : experimental
-- Portability : POSIX
--
-- Evaluation of Verilog expressions and statements.
module Verismith.Verilog.Eval
  ( evaluateConst,
    resize,
  )
where

import Data.Bits
import Data.Foldable (fold)
import Data.Functor.Foldable hiding (fold)
import Data.Maybe (listToMaybe)
import Verismith.Verilog.AST
import Verismith.Verilog.BitVec

type Bindings = [Parameter]

paramIdent_ :: Parameter -> Identifier
paramIdent_ :: Parameter -> Identifier
paramIdent_ (Parameter Identifier
i ConstExpr
_) = Identifier
i

paramValue_ :: Parameter -> ConstExpr
paramValue_ :: Parameter -> ConstExpr
paramValue_ (Parameter Identifier
_ ConstExpr
v) = ConstExpr
v

applyUnary :: (Num a, FiniteBits a) => UnaryOperator -> a -> a
applyUnary :: forall a. (Num a, FiniteBits a) => UnaryOperator -> a -> a
applyUnary UnaryOperator
UnPlus a
a = a
a
applyUnary UnaryOperator
UnMinus a
a = a -> a
forall a. Num a => a -> a
negate a
a
applyUnary UnaryOperator
UnLNot a
a
  | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 = a
0
  | Bool
otherwise = a
1
applyUnary UnaryOperator
UnNot a
a = a -> a
forall a. Bits a => a -> a
complement a
a
applyUnary UnaryOperator
UnAnd a
a
  | a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize a
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Int
forall a. Bits a => a -> Int
popCount a
a = a
1
  | Bool
otherwise = a
0
applyUnary UnaryOperator
UnNand a
a
  | a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize a
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Int
forall a. Bits a => a -> Int
popCount a
a = a
0
  | Bool
otherwise = a
1
applyUnary UnaryOperator
UnOr a
a
  | a -> Int
forall a. Bits a => a -> Int
popCount a
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = a
0
  | Bool
otherwise = a
1
applyUnary UnaryOperator
UnNor a
a
  | a -> Int
forall a. Bits a => a -> Int
popCount a
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = a
1
  | Bool
otherwise = a
0
applyUnary UnaryOperator
UnXor a
a
  | a -> Int
forall a. Bits a => a -> Int
popCount a
a Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = a
0
  | Bool
otherwise = a
1
applyUnary UnaryOperator
UnNxor a
a
  | a -> Int
forall a. Bits a => a -> Int
popCount a
a Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = a
1
  | Bool
otherwise = a
0
applyUnary UnaryOperator
UnNxorInv a
a
  | a -> Int
forall a. Bits a => a -> Int
popCount a
a Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = a
1
  | Bool
otherwise = a
0

compXor :: (Bits c) => c -> c -> c
compXor :: forall c. Bits c => c -> c -> c
compXor c
a = c -> c
forall a. Bits a => a -> a
complement (c -> c) -> (c -> c) -> c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> c -> c
forall c. Bits c => c -> c -> c
xor c
a

toIntegral :: (Num p) => (t1 -> t2 -> Bool) -> t1 -> t2 -> p
toIntegral :: forall p t1 t2. Num p => (t1 -> t2 -> Bool) -> t1 -> t2 -> p
toIntegral t1 -> t2 -> Bool
a t1
b t2
c = if t1 -> t2 -> Bool
a t1
b t2
c then p
1 else p
0

toInt :: (Integral a, Num t1) => (t2 -> t1 -> t3) -> t2 -> a -> t3
toInt :: forall a t1 t2 t3.
(Integral a, Num t1) =>
(t2 -> t1 -> t3) -> t2 -> a -> t3
toInt t2 -> t1 -> t3
a t2
b a
c = t2 -> t1 -> t3
a t2
b (t1 -> t3) -> t1 -> t3
forall a b. (a -> b) -> a -> b
$ a -> t1
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
c

applyBinary :: (Integral a, Bits a) => BinaryOperator -> a -> a -> a
applyBinary :: forall a. (Integral a, Bits a) => BinaryOperator -> a -> a -> a
applyBinary BinaryOperator
BinPlus = a -> a -> a
forall a. Num a => a -> a -> a
(+)
applyBinary BinaryOperator
BinMinus = (-)
applyBinary BinaryOperator
BinTimes = a -> a -> a
forall a. Num a => a -> a -> a
(*)
applyBinary BinaryOperator
BinDiv = a -> a -> a
forall a. Integral a => a -> a -> a
quot
applyBinary BinaryOperator
BinMod = a -> a -> a
forall a. Integral a => a -> a -> a
rem
applyBinary BinaryOperator
BinEq = (a -> a -> Bool) -> a -> a -> a
forall p t1 t2. Num p => (t1 -> t2 -> Bool) -> t1 -> t2 -> p
toIntegral a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)
applyBinary BinaryOperator
BinNEq = (a -> a -> Bool) -> a -> a -> a
forall p t1 t2. Num p => (t1 -> t2 -> Bool) -> t1 -> t2 -> p
toIntegral a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(/=)
applyBinary BinaryOperator
BinCEq = (a -> a -> Bool) -> a -> a -> a
forall p t1 t2. Num p => (t1 -> t2 -> Bool) -> t1 -> t2 -> p
toIntegral a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)
applyBinary BinaryOperator
BinCNEq = (a -> a -> Bool) -> a -> a -> a
forall p t1 t2. Num p => (t1 -> t2 -> Bool) -> t1 -> t2 -> p
toIntegral a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(/=)
applyBinary BinaryOperator
BinLAnd = a -> a -> a
forall a. HasCallStack => a
undefined
applyBinary BinaryOperator
BinLOr = a -> a -> a
forall a. HasCallStack => a
undefined
applyBinary BinaryOperator
BinLT = (a -> a -> Bool) -> a -> a -> a
forall p t1 t2. Num p => (t1 -> t2 -> Bool) -> t1 -> t2 -> p
toIntegral a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<)
applyBinary BinaryOperator
BinLEq = (a -> a -> Bool) -> a -> a -> a
forall p t1 t2. Num p => (t1 -> t2 -> Bool) -> t1 -> t2 -> p
toIntegral a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
applyBinary BinaryOperator
BinGT = (a -> a -> Bool) -> a -> a -> a
forall p t1 t2. Num p => (t1 -> t2 -> Bool) -> t1 -> t2 -> p
toIntegral a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>)
applyBinary BinaryOperator
BinGEq = (a -> a -> Bool) -> a -> a -> a
forall p t1 t2. Num p => (t1 -> t2 -> Bool) -> t1 -> t2 -> p
toIntegral a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>=)
applyBinary BinaryOperator
BinAnd = a -> a -> a
forall c. Bits c => c -> c -> c
(.&.)
applyBinary BinaryOperator
BinOr = a -> a -> a
forall c. Bits c => c -> c -> c
(.|.)
applyBinary BinaryOperator
BinXor = a -> a -> a
forall c. Bits c => c -> c -> c
xor
applyBinary BinaryOperator
BinXNor = a -> a -> a
forall c. Bits c => c -> c -> c
compXor
applyBinary BinaryOperator
BinXNorInv = a -> a -> a
forall c. Bits c => c -> c -> c
compXor
applyBinary BinaryOperator
BinPower = a -> a -> a
forall a. HasCallStack => a
undefined
applyBinary BinaryOperator
BinLSL = (a -> Int -> a) -> a -> a -> a
forall a t1 t2 t3.
(Integral a, Num t1) =>
(t2 -> t1 -> t3) -> t2 -> a -> t3
toInt a -> Int -> a
forall a. Bits a => a -> Int -> a
shiftL
applyBinary BinaryOperator
BinLSR = (a -> Int -> a) -> a -> a -> a
forall a t1 t2 t3.
(Integral a, Num t1) =>
(t2 -> t1 -> t3) -> t2 -> a -> t3
toInt a -> Int -> a
forall a. Bits a => a -> Int -> a
shiftR
applyBinary BinaryOperator
BinASL = (a -> Int -> a) -> a -> a -> a
forall a t1 t2 t3.
(Integral a, Num t1) =>
(t2 -> t1 -> t3) -> t2 -> a -> t3
toInt a -> Int -> a
forall a. Bits a => a -> Int -> a
shiftL
applyBinary BinaryOperator
BinASR = (a -> Int -> a) -> a -> a -> a
forall a t1 t2 t3.
(Integral a, Num t1) =>
(t2 -> t1 -> t3) -> t2 -> a -> t3
toInt a -> Int -> a
forall a. Bits a => a -> Int -> a
shiftR

-- | Evaluates a 'ConstExpr' using a context of 'Bindings' as input.
evaluateConst :: Bindings -> ConstExprF BitVec -> BitVec
evaluateConst :: Bindings -> ConstExprF BitVec -> BitVec
evaluateConst Bindings
_ (ConstNumF BitVec
b) = BitVec
b
evaluateConst Bindings
p (ParamIdF Identifier
i) =
  (Base ConstExpr BitVec -> BitVec) -> ConstExpr -> BitVec
forall t a. Recursive t => (Base t a -> a) -> t -> a
forall a. (Base ConstExpr a -> a) -> ConstExpr -> a
cata (Bindings -> ConstExprF BitVec -> BitVec
evaluateConst Bindings
p) (ConstExpr -> BitVec)
-> (Bindings -> ConstExpr) -> Bindings -> BitVec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstExpr
-> (Parameter -> ConstExpr) -> Maybe Parameter -> ConstExpr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ConstExpr
0 Parameter -> ConstExpr
paramValue_ (Maybe Parameter -> ConstExpr)
-> (Bindings -> Maybe Parameter) -> Bindings -> ConstExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bindings -> Maybe Parameter
forall a. [a] -> Maybe a
listToMaybe (Bindings -> BitVec) -> Bindings -> BitVec
forall a b. (a -> b) -> a -> b
$
    (Parameter -> Bool) -> Bindings -> Bindings
forall a. (a -> Bool) -> [a] -> [a]
filter
      ((Identifier -> Identifier -> Bool
forall a. Eq a => a -> a -> Bool
== Identifier
i) (Identifier -> Bool)
-> (Parameter -> Identifier) -> Parameter -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parameter -> Identifier
paramIdent_)
      Bindings
p
evaluateConst Bindings
_ (ConstConcatF NonEmpty BitVec
c) = NonEmpty BitVec -> BitVec
forall m. Monoid m => NonEmpty m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold NonEmpty BitVec
c
evaluateConst Bindings
_ (ConstUnOpF UnaryOperator
unop BitVec
c) = UnaryOperator -> BitVec -> BitVec
forall a. (Num a, FiniteBits a) => UnaryOperator -> a -> a
applyUnary UnaryOperator
unop BitVec
c
evaluateConst Bindings
_ (ConstBinOpF BitVec
a BinaryOperator
binop BitVec
b) = BinaryOperator -> BitVec -> BitVec -> BitVec
forall a. (Integral a, Bits a) => BinaryOperator -> a -> a -> a
applyBinary BinaryOperator
binop BitVec
a BitVec
b
evaluateConst Bindings
_ (ConstCondF BitVec
a BitVec
b BitVec
c) = if BitVec
a BitVec -> BitVec -> Bool
forall a. Ord a => a -> a -> Bool
> BitVec
0 then BitVec
b else BitVec
c
evaluateConst Bindings
_ (ConstStrF Text
_) = BitVec
0

-- | Apply a function to all the bitvectors. Would be fixed by having a
-- 'Functor' instance for a polymorphic 'ConstExpr'.
applyBitVec :: (BitVec -> BitVec) -> ConstExpr -> ConstExpr
applyBitVec :: (BitVec -> BitVec) -> ConstExpr -> ConstExpr
applyBitVec BitVec -> BitVec
f (ConstNum BitVec
b) = BitVec -> ConstExpr
ConstNum (BitVec -> ConstExpr) -> BitVec -> ConstExpr
forall a b. (a -> b) -> a -> b
$ BitVec -> BitVec
f BitVec
b
applyBitVec BitVec -> BitVec
f (ConstConcat NonEmpty ConstExpr
c) = NonEmpty ConstExpr -> ConstExpr
ConstConcat (NonEmpty ConstExpr -> ConstExpr)
-> NonEmpty ConstExpr -> ConstExpr
forall a b. (a -> b) -> a -> b
$ (ConstExpr -> ConstExpr)
-> NonEmpty ConstExpr -> NonEmpty ConstExpr
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((BitVec -> BitVec) -> ConstExpr -> ConstExpr
applyBitVec BitVec -> BitVec
f) NonEmpty ConstExpr
c
applyBitVec BitVec -> BitVec
f (ConstUnOp UnaryOperator
unop ConstExpr
c) = UnaryOperator -> ConstExpr -> ConstExpr
ConstUnOp UnaryOperator
unop (ConstExpr -> ConstExpr) -> ConstExpr -> ConstExpr
forall a b. (a -> b) -> a -> b
$ (BitVec -> BitVec) -> ConstExpr -> ConstExpr
applyBitVec BitVec -> BitVec
f ConstExpr
c
applyBitVec BitVec -> BitVec
f (ConstBinOp ConstExpr
a BinaryOperator
binop ConstExpr
b) =
  ConstExpr -> BinaryOperator -> ConstExpr -> ConstExpr
ConstBinOp ((BitVec -> BitVec) -> ConstExpr -> ConstExpr
applyBitVec BitVec -> BitVec
f ConstExpr
a) BinaryOperator
binop ((BitVec -> BitVec) -> ConstExpr -> ConstExpr
applyBitVec BitVec -> BitVec
f ConstExpr
b)
applyBitVec BitVec -> BitVec
f (ConstCond ConstExpr
a ConstExpr
b ConstExpr
c) = ConstExpr -> ConstExpr -> ConstExpr -> ConstExpr
ConstCond (ConstExpr -> ConstExpr
abv ConstExpr
a) (ConstExpr -> ConstExpr
abv ConstExpr
b) (ConstExpr -> ConstExpr
abv ConstExpr
c)
  where
    abv :: ConstExpr -> ConstExpr
abv = (BitVec -> BitVec) -> ConstExpr -> ConstExpr
applyBitVec BitVec -> BitVec
f
applyBitVec BitVec -> BitVec
_ ConstExpr
a = ConstExpr
a

-- | This probably could be implemented using some recursion scheme in the
-- future. It would also be fixed by having a polymorphic expression type.
resize :: Int -> ConstExpr -> ConstExpr
resize :: Int -> ConstExpr -> ConstExpr
resize Int
n = (BitVec -> BitVec) -> ConstExpr -> ConstExpr
applyBitVec (Int -> BitVec -> BitVec
forall {a}. Int -> BitVecF a -> BitVecF a
resize' Int
n) where resize' :: Int -> BitVecF a -> BitVecF a
resize' Int
n' (BitVec Int
_ a
a) = Int -> a -> BitVecF a
forall a. Int -> a -> BitVecF a
BitVec Int
n' a
a