{-
Module           : What4.Protocol.VerilogWriter.AST
Copyright        : (c) Galois, Inc 2020
Maintainer       : Jennifer Paykin <jpaykin@galois.com>
License          : BSD3

An intermediate AST to use for generating Verilog modules from What4 expressions.
-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, ScopedTypeVariables,
  TypeApplications, PolyKinds, DataKinds, ExplicitNamespaces, TypeOperators,
  OverloadedStrings #-}

module What4.Protocol.VerilogWriter.AST
  where

import qualified Data.BitVector.Sized as BV
import qualified Data.Map as Map
import qualified Data.Text as T
import qualified Data.Set as Set
import           Data.String
import           Data.Word
import           Control.Monad (forM_)
import           Control.Monad.Except (ExceptT, MonadError(..))
import           Control.Monad.IO.Class (MonadIO(..))
import           Control.Monad.State (MonadState(), StateT(..), get, put, modify, gets)

import qualified What4.BaseTypes as WT
import           What4.Expr.Builder
import           Data.Parameterized.Classes (OrderingF(..), compareF)
import           Data.Parameterized.Nonce (Nonce, indexValue)
import           Data.Parameterized.Some (Some(..), viewSome)
import           Data.Parameterized.Pair
import           GHC.TypeNats ( type (<=) )

type Identifier = T.Text

-- | A type for Verilog binary operators that enforces well-typedness,
-- including bitvector size constraints.
data Binop (inTp :: WT.BaseType) (outTp :: WT.BaseType) where
  And :: Binop WT.BaseBoolType WT.BaseBoolType
  Or  :: Binop WT.BaseBoolType WT.BaseBoolType
  Xor :: Binop WT.BaseBoolType WT.BaseBoolType

  Eq :: Binop tp WT.BaseBoolType
  Ne :: Binop tp WT.BaseBoolType
  Lt :: Binop (WT.BaseBVType w) WT.BaseBoolType
  Le :: Binop (WT.BaseBVType w) WT.BaseBoolType

  BVAnd :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
  BVOr  :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
  BVXor :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
  BVAdd :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
  BVSub :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
  BVMul :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
  BVDiv :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
  BVRem :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
  BVPow :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
  BVShiftL :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
  BVShiftR :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
  BVShiftRA :: Binop (WT.BaseBVType w) (WT.BaseBVType w)

binopType ::
  Binop inTp outTp ->
  WT.BaseTypeRepr inTp ->
  WT.BaseTypeRepr outTp
binopType :: forall (inTp :: BaseType) (outTp :: BaseType).
Binop inTp outTp -> BaseTypeRepr inTp -> BaseTypeRepr outTp
binopType Binop inTp outTp
And BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Or  BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Xor BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Eq  BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Ne  BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Lt  BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Le  BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
BVAnd  BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVOr  BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVXor BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVAdd BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVSub BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVMul BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVDiv BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVRem BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVPow BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVShiftL BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVShiftR BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVShiftRA BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp

-- | A type for Verilog unary operators that enforces well-typedness.
data Unop (tp :: WT.BaseType) where
  Not :: Unop WT.BaseBoolType
  BVNot :: Unop (WT.BaseBVType w)

-- | A type for Verilog expression names that enforces well-typedness.
-- This type exists essentially to pair a name and type to avoid needing
-- to repeat them and ensure that all uses of the name are well-typed.
data IExp (tp :: WT.BaseType) where
  Ident   :: WT.BaseTypeRepr tp -> Identifier -> IExp tp

iexpType :: IExp tp -> WT.BaseTypeRepr tp
iexpType :: forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType (Ident BaseTypeRepr tp
tp Identifier
_) = BaseTypeRepr tp
tp

data LHS = LHS Identifier | LHSBit Identifier Integer

-- | A type for Verilog expressions that enforces well-typedness,
-- including bitvector size constraints.
data Exp (tp :: WT.BaseType) where
  IExp :: IExp tp -> Exp tp
  Binop :: Binop inTp outTp -> IExp inTp -> IExp inTp -> Exp outTp
  Unop :: Unop tp -> IExp tp -> Exp tp
  BVRotateL :: WT.NatRepr w -> IExp tp -> BV.BV w -> Exp tp
  BVRotateR :: WT.NatRepr w -> IExp tp -> BV.BV w -> Exp tp
  Mux :: IExp WT.BaseBoolType -> IExp tp -> IExp tp -> Exp tp
  Bit :: IExp (WT.BaseBVType w)
      -> Integer
      -> Exp WT.BaseBoolType
  BitSelect :: (1 WT.<= len, start WT.+ len WT.<= w)
      => IExp (WT.BaseBVType w)
      -> WT.NatRepr start
      -> WT.NatRepr len
      -> Exp (WT.BaseBVType len)
  Concat :: 1 <= w
          => WT.NatRepr w -> [Some IExp] -> Exp (WT.BaseBVType w)
  BVLit   :: (1 <= w)
          => WT.NatRepr w -- the width
          -> BV.BV w -- the value
          -> Exp (WT.BaseBVType w)
  BoolLit :: Bool -> Exp WT.BaseBoolType

expType :: Exp tp -> WT.BaseTypeRepr tp
expType :: forall (tp :: BaseType). Exp tp -> BaseTypeRepr tp
expType (IExp IExp tp
e) = forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
expType (Binop Binop inTp tp
op IExp inTp
e1 IExp inTp
_) = forall (inTp :: BaseType) (outTp :: BaseType).
Binop inTp outTp -> BaseTypeRepr inTp -> BaseTypeRepr outTp
binopType Binop inTp tp
op (forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp inTp
e1)
expType (BVRotateL NatRepr w
_ IExp tp
e BV w
_) = forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
expType (BVRotateR NatRepr w
_ IExp tp
e BV w
_) = forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
expType (Unop Unop tp
_ IExp tp
e) = forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
expType (Mux IExp 'BaseBoolType
_ IExp tp
e1 IExp tp
_) = forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e1
expType (Bit IExp (BaseBVType w)
_ Integer
_) = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
expType (BitSelect IExp (BaseBVType w)
_ NatRepr start
_ NatRepr len
n) = forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
WT.BaseBVRepr NatRepr len
n
expType (Concat NatRepr w
w [Some IExp]
_) = forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
WT.BaseBVRepr NatRepr w
w
expType (BVLit NatRepr w
w BV w
_) = forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
WT.BaseBVRepr NatRepr w
w
expType (BoolLit Bool
_) = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr


-- | Create a let binding, associating a name with an expression. In
-- Verilog, this is a new "wire".
mkLet :: Exp tp -> VerilogM sym n (IExp tp)
mkLet :: forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (IExp IExp tp
x) = forall (m :: Type -> Type) a. Monad m => a -> m a
return IExp tp
x
mkLet Exp tp
e = do
    let tp :: BaseTypeRepr tp
tp = forall (tp :: BaseType). Exp tp -> BaseTypeRepr tp
expType Exp tp
e
    Identifier
x <- forall (tp :: BaseType) sym n.
BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
addFreshWire BaseTypeRepr tp
tp Bool
False Identifier
"wr" Exp tp
e
    forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident BaseTypeRepr tp
tp Identifier
x)

-- | Indicate than an expression name is signed. This causes arithmetic
-- operations involving this name to be interpreted as signed
-- operations.
signed :: IExp tp -> VerilogM sym n (IExp tp)
signed :: forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
signed IExp tp
e = do
    let tp :: BaseTypeRepr tp
tp = forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
    Identifier
x <- forall (tp :: BaseType) sym n.
BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
addFreshWire BaseTypeRepr tp
tp Bool
True Identifier
"wr" (forall (tp :: BaseType). IExp tp -> Exp tp
IExp IExp tp
e)
    forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident BaseTypeRepr tp
tp Identifier
x)

-- | Apply a binary operation to two expressions and bind the result to
-- a new, returned name.
binop ::
  Binop inTp outTp ->
  IExp inTp -> IExp inTp ->
  VerilogM sym n (IExp outTp)
binop :: forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop inTp outTp
op IExp inTp
e1 IExp inTp
e2 = forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (w :: BaseType) (outTp :: BaseType).
Binop w outTp -> IExp w -> IExp w -> Exp outTp
Binop Binop inTp outTp
op IExp inTp
e1 IExp inTp
e2)

-- | A special binary operation for scalar multiplication. This avoids
-- the need to call `litBV` at every call site.
scalMult ::
  1 <= w =>
  WT.NatRepr w ->
  Binop (WT.BaseBVType w) (WT.BaseBVType w) ->
  BV.BV w ->
  IExp (WT.BaseBVType w) ->
  VerilogM sym n (IExp (WT.BaseBVType w))
scalMult :: forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w
-> Binop (BaseBVType w) (BaseBVType w)
-> BV w
-> IExp (BaseBVType w)
-> VerilogM sym n (IExp (BaseBVType w))
scalMult NatRepr w
w Binop (BaseBVType w) (BaseBVType w)
op BV w
n IExp (BaseBVType w)
e = do
  IExp (BaseBVType w)
n' <- forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w BV w
n
  forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop (BaseBVType w) (BaseBVType w)
op IExp (BaseBVType w)
n' IExp (BaseBVType w)
e

-- | A wrapper around the BV type allowing it to be put into a map or
-- set. We use this to make sure we generate only one instance of each
-- distinct constant.
data BVConst = BVConst (Pair WT.NatRepr BV.BV)
  deriving (BVConst -> BVConst -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BVConst -> BVConst -> Bool
$c/= :: BVConst -> BVConst -> Bool
== :: BVConst -> BVConst -> Bool
$c== :: BVConst -> BVConst -> Bool
Eq)

instance Ord BVConst where
  compare :: BVConst -> BVConst -> Ordering
compare (BVConst Pair NatRepr BV
cx) (BVConst Pair NatRepr BV
cy) =
    forall {k} (a :: k -> Type) (b :: k -> Type) c.
(forall (tp :: k). a tp -> b tp -> c) -> Pair a b -> c
viewPair (\NatRepr tp
wx BV tp
x -> forall {k} (a :: k -> Type) (b :: k -> Type) c.
(forall (tp :: k). a tp -> b tp -> c) -> Pair a b -> c
viewPair (\NatRepr tp
wy BV tp
y ->
      case forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF NatRepr tp
wx NatRepr tp
wy of
        OrderingF tp tp
LTF -> Ordering
LT
        OrderingF tp tp
EQF | forall (w :: Natural). BV w -> BV w -> Bool
BV.ult BV tp
x BV tp
y -> Ordering
LT
        OrderingF tp tp
EQF | forall (w :: Natural). BV w -> BV w -> Bool
BV.ult BV tp
y BV tp
x -> Ordering
GT
        OrderingF tp tp
EQF -> Ordering
EQ
        OrderingF tp tp
GTF -> Ordering
GT
    ) Pair NatRepr BV
cy) Pair NatRepr BV
cx

-- | Return the (possibly-cached) name for a literal bitvector value.
litBV ::
  (1 <= w) =>
  WT.NatRepr w ->
  BV.BV w ->
  VerilogM sym n (IExp (WT.BaseBVType w))
litBV :: forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w BV w
i = do
  Map BVConst Identifier
cache <- forall sym n. ModuleState sym n -> Map BVConst Identifier
vsBVCache forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: Type -> Type). MonadState s m => m s
get
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Pair NatRepr BV -> BVConst
BVConst (forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair NatRepr w
w BV w
i)) Map BVConst Identifier
cache of
    Just Identifier
x -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
WT.BaseBVRepr NatRepr w
w) Identifier
x)
    Maybe Identifier
Nothing -> do
      x :: IExp (BaseBVType w)
x@(Ident BaseTypeRepr (BaseBVType w)
_ Identifier
name) <- forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> Exp (BaseBVType w)
BVLit NatRepr w
w BV w
i)
      forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
s -> ModuleState sym n
s { vsBVCache :: Map BVConst Identifier
vsBVCache = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Pair NatRepr BV -> BVConst
BVConst (forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair NatRepr w
w BV w
i)) Identifier
name (forall sym n. ModuleState sym n -> Map BVConst Identifier
vsBVCache ModuleState sym n
s) }
      forall (m :: Type -> Type) a. Monad m => a -> m a
return IExp (BaseBVType w)
x

-- | Return the (possibly-cached) name for a literal Boolean value.
litBool :: Bool -> VerilogM sym n (IExp WT.BaseBoolType)
litBool :: forall sym n. Bool -> VerilogM sym n (IExp 'BaseBoolType)
litBool Bool
b = do
  Map Bool Identifier
cache <- forall sym n. ModuleState sym n -> Map Bool Identifier
vsBoolCache forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: Type -> Type). MonadState s m => m s
get
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Bool
b Map Bool Identifier
cache of
    Just Identifier
x -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr Identifier
x)
    Maybe Identifier
Nothing -> do
      x :: IExp 'BaseBoolType
x@(Ident BaseTypeRepr 'BaseBoolType
_ Identifier
name) <- forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (Bool -> Exp 'BaseBoolType
BoolLit Bool
b)
      forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
s -> ModuleState sym n
s { vsBoolCache :: Map Bool Identifier
vsBoolCache = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Bool
b Identifier
name (forall sym n. ModuleState sym n -> Map Bool Identifier
vsBoolCache ModuleState sym n
s) }
      forall (m :: Type -> Type) a. Monad m => a -> m a
return IExp 'BaseBoolType
x

-- | Apply a unary operation to an expression and bind the result to a
-- new, returned name.
unop :: Unop tp -> IExp tp -> VerilogM sym n (IExp tp)
unop :: forall (tp :: BaseType) sym n.
Unop tp -> IExp tp -> VerilogM sym n (IExp tp)
unop Unop tp
op IExp tp
e = forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (tp :: BaseType). Unop tp -> IExp tp -> Exp tp
Unop Unop tp
op IExp tp
e)

-- | Create a conditional, with the given condition, true, and false
-- branches, and bind the result to a new, returned name.
mux ::
  IExp WT.BaseBoolType ->
  IExp tp ->
  IExp tp ->
  VerilogM sym n (IExp tp)
mux :: forall (tp :: BaseType) sym n.
IExp 'BaseBoolType
-> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
mux IExp 'BaseBoolType
e IExp tp
e1 IExp tp
e2 = forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (tp :: BaseType).
IExp 'BaseBoolType -> IExp tp -> IExp tp -> Exp tp
Mux IExp 'BaseBoolType
e IExp tp
e1 IExp tp
e2)

-- | Extract a single bit from a bit vector and bind the result to a
-- new, returned name.
bit ::
  IExp (WT.BaseBVType w) ->
  Integer ->
  VerilogM sym n (IExp WT.BaseBoolType)
bit :: forall (w :: Natural) sym n.
IExp (BaseBVType w)
-> Integer -> VerilogM sym n (IExp 'BaseBoolType)
bit IExp (BaseBVType w)
e Integer
i = forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (w :: Natural).
IExp (BaseBVType w) -> Integer -> Exp 'BaseBoolType
Bit IExp (BaseBVType w)
e Integer
i)

-- | Extract a range of bits from a bit vector and bind the result to a
-- new, returned name. The two `NatRepr` values are the starting index
-- and the number of bits to extract, respectively.
bitSelect ::
  (1 WT.<= len, idx WT.+ len WT.<= w) =>
  IExp (WT.BaseBVType w) ->
  WT.NatRepr idx ->
  WT.NatRepr len ->
  VerilogM sym n (IExp (WT.BaseBVType len))
bitSelect :: forall (len :: Natural) (idx :: Natural) (w :: Natural) sym n.
(1 <= len, (idx + len) <= w) =>
IExp (BaseBVType w)
-> NatRepr idx
-> NatRepr len
-> VerilogM sym n (IExp (BaseBVType len))
bitSelect IExp (BaseBVType w)
e NatRepr idx
start NatRepr len
len = forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (w :: Natural) (start :: Natural) (w :: Natural).
(1 <= w, (start + w) <= w) =>
IExp (BaseBVType w)
-> NatRepr start -> NatRepr w -> Exp (BaseBVType w)
BitSelect IExp (BaseBVType w)
e NatRepr idx
start NatRepr len
len)

-- | Concatenate two bit vectors and bind the result to a new, returned
-- name.
concat2 ::
  (w ~ (w1 WT.+ w2), 1 <= w) =>
  WT.NatRepr w ->
  IExp (WT.BaseBVType w1) ->
  IExp (WT.BaseBVType w2) ->
  VerilogM sym n (IExp (WT.BaseBVType w))
concat2 :: forall (w :: Natural) (w1 :: Natural) (w2 :: Natural) sym n.
(w ~ (w1 + w2), 1 <= w) =>
NatRepr w
-> IExp (BaseBVType w1)
-> IExp (BaseBVType w2)
-> VerilogM sym n (IExp (BaseBVType w))
concat2 NatRepr w
w IExp (BaseBVType w1)
e1 IExp (BaseBVType w2)
e2 = forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> [Some IExp] -> Exp (BaseBVType w)
Concat NatRepr w
w [forall k (f :: k -> Type) (x :: k). f x -> Some f
Some IExp (BaseBVType w1)
e1, forall k (f :: k -> Type) (x :: k). f x -> Some f
Some IExp (BaseBVType w2)
e2])

-- | A data type for items that may show up in a Verilog module.
data Item where
  Input  :: WT.BaseTypeRepr tp -> Identifier -> Item
  Output :: WT.BaseTypeRepr tp -> Identifier -> Item
  Wire   :: WT.BaseTypeRepr tp -> Identifier -> Item
  Assign :: LHS -> Exp tp -> Item

-- | Necessary monadic operations

data ModuleState sym n =
    ModuleState { forall sym n.
ModuleState sym n -> [(Word64, Some BaseTypeRepr, Identifier)]
vsInputs :: [(Word64, Some WT.BaseTypeRepr, Identifier)]
                -- ^ All module inputs, in reverse order. We use Word64 for Nonces to avoid GHC bugs.
                -- For more detail:
                --   https://gitlab.haskell.org/ghc/ghc/-/issues/2595
                --   https://gitlab.haskell.org/ghc/ghc/-/issues/10856
                --   https://gitlab.haskell.org/ghc/ghc/-/issues/16501
                , forall sym n.
ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsOutputs :: [(Some WT.BaseTypeRepr, Bool, Identifier, Some Exp)]
                -- ^ All module outputs, in reverse order. Includes the
                -- type, signedness, name, and initializer of each.
                , forall sym n.
ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsWires :: [(Some WT.BaseTypeRepr, Bool, Identifier, Some Exp)]
                -- ^ All internal wires, in reverse order. Includes the
                -- type, signedness, name, and initializer of each.
                , forall sym n. ModuleState sym n -> Map Word64 Identifier
vsSeenNonces :: Map.Map Word64 Identifier
                -- ^ A map from the identifier nonces seen so far to
                -- their identifier names. These nonces exist for
                -- identifiers from the original term, but not
                -- intermediate Verilog variables.
                , forall sym n. ModuleState sym n -> Set Identifier
vsUsedIdentifiers :: Set.Set Identifier
                -- ^ A set of all the identifiers used so far, including
                -- intermediate Verilog variables.
                , forall sym n. ModuleState sym n -> IdxCache n IExp
vsExpCache :: IdxCache n IExp
                -- ^ An expression cache to preserve sharing present in
                -- the What4 representation.
                , forall sym n. ModuleState sym n -> Map BVConst Identifier
vsBVCache :: Map.Map BVConst Identifier
                -- ^ A cache of bit vector constants, to avoid duplicating constant declarations.
                , forall sym n. ModuleState sym n -> Map Bool Identifier
vsBoolCache :: Map.Map Bool Identifier
                -- ^ A cache of Boolean constants, to avoid duplicating constant declarations.
                , forall sym n. ModuleState sym n -> sym
vsSym :: sym
                -- ^ The What4 symbolic backend to use with `vsBVCache`.
                }

newtype VerilogM sym n a =
 VerilogM (StateT (ModuleState sym n) (ExceptT String IO) a)
 deriving ( forall a b. a -> VerilogM sym n b -> VerilogM sym n a
forall a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
forall sym n a b. a -> VerilogM sym n b -> VerilogM sym n a
forall sym n a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> VerilogM sym n b -> VerilogM sym n a
$c<$ :: forall sym n a b. a -> VerilogM sym n b -> VerilogM sym n a
fmap :: forall a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
$cfmap :: forall sym n a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
Functor
          , forall a. a -> VerilogM sym n a
forall sym n. Functor (VerilogM sym n)
forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
forall a b.
VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
forall sym n a. a -> VerilogM sym n a
forall a b c.
(a -> b -> c)
-> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
forall sym n a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
forall sym n a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
forall sym n a b.
VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
forall sym n a b c.
(a -> b -> c)
-> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
forall (f :: Type -> Type).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
$c<* :: forall sym n a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
*> :: forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
$c*> :: forall sym n a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
liftA2 :: forall a b c.
(a -> b -> c)
-> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
$cliftA2 :: forall sym n a b c.
(a -> b -> c)
-> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
<*> :: forall a b.
VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
$c<*> :: forall sym n a b.
VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
pure :: forall a. a -> VerilogM sym n a
$cpure :: forall sym n a. a -> VerilogM sym n a
Applicative
          , forall a. a -> VerilogM sym n a
forall sym n. Applicative (VerilogM sym n)
forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
forall a b.
VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
forall sym n a. a -> VerilogM sym n a
forall sym n a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
forall sym n a b.
VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
forall (m :: Type -> Type).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> VerilogM sym n a
$creturn :: forall sym n a. a -> VerilogM sym n a
>> :: forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
$c>> :: forall sym n a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
>>= :: forall a b.
VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
$c>>= :: forall sym n a b.
VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
Monad
          , MonadState (ModuleState sym n)
          , MonadError String
          , forall a. IO a -> VerilogM sym n a
forall sym n. Monad (VerilogM sym n)
forall sym n a. IO a -> VerilogM sym n a
forall (m :: Type -> Type).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> VerilogM sym n a
$cliftIO :: forall sym n a. IO a -> VerilogM sym n a
MonadIO
          )


newtype Module sym n = Module (ModuleState sym n)

-- | Create a Verilog module in the context of a given What4 symbolic
-- backend and a monadic computation that returns an expression name
-- that corresponds to the module's output.
mkModule ::
  sym ->
  [(Some (Expr n), T.Text)] ->
  [VerilogM sym n (Some IExp)] ->
  ExceptT String IO (Module sym n)
mkModule :: forall sym n.
sym
-> [(Some (Expr n), Identifier)]
-> [VerilogM sym n (Some IExp)]
-> ExceptT String IO (Module sym n)
mkModule sym
sym [(Some (Expr n), Identifier)]
ins [VerilogM sym n (Some IExp)]
ops = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall sym n. ModuleState sym n -> Module sym n
Module forall a b. (a -> b) -> a -> b
$ forall sym n a.
sym -> VerilogM sym n a -> ExceptT String IO (ModuleState sym n)
execVerilogM sym
sym forall a b. (a -> b) -> a -> b
$ do
    let addExprInput :: Some (Expr n) -> Identifier -> VerilogM sym n Identifier
addExprInput Some (Expr n)
e Identifier
ident =
          case Some (Expr n)
e of
            Some (BoundVarExpr ExprBoundVar n x
x) -> forall n (tp :: BaseType) sym.
ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier
addBoundInput ExprBoundVar n x
x Identifier
ident
            Some (Expr n)
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Input provided to mkModule isn't an input"
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall {n} {sym}.
Some (Expr n) -> Identifier -> VerilogM sym n Identifier
addExprInput) [(Some (Expr n), Identifier)]
ins
    [Some IExp]
es <- forall (t :: Type -> Type) (m :: Type -> Type) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [VerilogM sym n (Some IExp)]
ops
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Some IExp]
es forall a b. (a -> b) -> a -> b
$ \Some IExp
se ->
      do Identifier
out <- forall sym n. Identifier -> VerilogM sym n Identifier
freshIdentifier Identifier
"out"
         forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome (\IExp tp
e -> forall (tp :: BaseType) sym n.
BaseTypeRepr tp -> Identifier -> Exp tp -> VerilogM sym n ()
addOutput (forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e) Identifier
out (forall (tp :: BaseType). IExp tp -> Exp tp
IExp IExp tp
e)) Some IExp
se

initModuleState :: sym -> IO (ModuleState sym n)
initModuleState :: forall sym n. sym -> IO (ModuleState sym n)
initModuleState sym
sym = do
  IdxCache n IExp
cache <- forall (m :: Type -> Type) t (f :: BaseType -> Type).
MonadIO m =>
m (IdxCache t f)
newIdxCache
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ModuleState
           { vsInputs :: [(Word64, Some BaseTypeRepr, Identifier)]
vsInputs = []
           , vsOutputs :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsOutputs = []
           , vsWires :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsWires = []
           , vsSeenNonces :: Map Word64 Identifier
vsSeenNonces = forall k a. Map k a
Map.empty
           , vsUsedIdentifiers :: Set Identifier
vsUsedIdentifiers = forall a. Set a
Set.empty
           , vsExpCache :: IdxCache n IExp
vsExpCache = IdxCache n IExp
cache
           , vsBVCache :: Map BVConst Identifier
vsBVCache = forall k a. Map k a
Map.empty
           , vsBoolCache :: Map Bool Identifier
vsBoolCache = forall k a. Map k a
Map.empty
           , vsSym :: sym
vsSym = sym
sym
           }

runVerilogM ::
  VerilogM sym n a ->
  ModuleState sym n ->
  ExceptT String IO (a, ModuleState sym n)
runVerilogM :: forall sym n a.
VerilogM sym n a
-> ModuleState sym n -> ExceptT String IO (a, ModuleState sym n)
runVerilogM (VerilogM StateT (ModuleState sym n) (ExceptT String IO) a
op) = forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT StateT (ModuleState sym n) (ExceptT String IO) a
op

execVerilogM ::
  sym ->
  VerilogM sym n a ->
  ExceptT String IO (ModuleState sym n)
execVerilogM :: forall sym n a.
sym -> VerilogM sym n a -> ExceptT String IO (ModuleState sym n)
execVerilogM sym
sym VerilogM sym n a
op =
  do ModuleState sym n
s <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym n. sym -> IO (ModuleState sym n)
initModuleState sym
sym
     (a
_a,ModuleState sym n
m) <- forall sym n a.
VerilogM sym n a
-> ModuleState sym n -> ExceptT String IO (a, ModuleState sym n)
runVerilogM VerilogM sym n a
op ModuleState sym n
s
     forall (m :: Type -> Type) a. Monad m => a -> m a
return ModuleState sym n
m

addBoundInput ::
  ExprBoundVar n tp ->
  Identifier ->
  VerilogM sym n Identifier
addBoundInput :: forall n (tp :: BaseType) sym.
ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier
addBoundInput ExprBoundVar n tp
x Identifier
ident =
  forall {k} n sym.
Some (Nonce n)
-> Some BaseTypeRepr -> Identifier -> VerilogM sym n Identifier
addFreshInput (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Nonce n tp
idx) (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr tp
tp) Identifier
ident
    where
      tp :: BaseTypeRepr tp
tp = forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
bvarType ExprBoundVar n tp
x
      idx :: Nonce n tp
idx = forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar n tp
x

-- | Returns and records a fresh input with the given type and with a
-- name constructed from the given base.
addFreshInput ::
  Some (Nonce n) ->
  Some WT.BaseTypeRepr ->
  Identifier ->
  VerilogM sym n Identifier
addFreshInput :: forall {k} n sym.
Some (Nonce n)
-> Some BaseTypeRepr -> Identifier -> VerilogM sym n Identifier
addFreshInput Some (Nonce n)
n Some BaseTypeRepr
tp Identifier
base = do
  Map Word64 Identifier
seenNonces <- forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets forall sym n. ModuleState sym n -> Map Word64 Identifier
vsSeenNonces
  let idx :: Word64
idx = forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome forall k s (tp :: k). Nonce s tp -> Word64
indexValue Some (Nonce n)
n
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Word64
idx Map Word64 Identifier
seenNonces of
    Just Identifier
ident -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Identifier
ident
    Maybe Identifier
Nothing ->
      do Identifier
name <- forall sym n. Identifier -> VerilogM sym n Identifier
freshIdentifier Identifier
base
         forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
st -> ModuleState sym n
st { vsInputs :: [(Word64, Some BaseTypeRepr, Identifier)]
vsInputs = (Word64
idx, Some BaseTypeRepr
tp, Identifier
name) forall a. a -> [a] -> [a]
: forall sym n.
ModuleState sym n -> [(Word64, Some BaseTypeRepr, Identifier)]
vsInputs ModuleState sym n
st
                            , vsSeenNonces :: Map Word64 Identifier
vsSeenNonces = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Word64
idx Identifier
name Map Word64 Identifier
seenNonces
                            }
         forall (m :: Type -> Type) a. Monad m => a -> m a
return Identifier
name

-- | Add an output to the current Verilog module state, given a type, a
-- name, and an initializer expression.
addOutput ::
  WT.BaseTypeRepr tp ->
  Identifier ->
  Exp tp ->
  VerilogM sym n ()
addOutput :: forall (tp :: BaseType) sym n.
BaseTypeRepr tp -> Identifier -> Exp tp -> VerilogM sym n ()
addOutput BaseTypeRepr tp
tp Identifier
name Exp tp
e =
  forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
st -> ModuleState sym n
st { vsOutputs :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsOutputs = (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr tp
tp, Bool
False, Identifier
name, forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Exp tp
e) forall a. a -> [a] -> [a]
: forall sym n.
ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsOutputs ModuleState sym n
st }

-- | Add a new wire to the current Verilog module state, given a type, a
-- signedness flag, a name, and an initializer expression.
addWire ::
  WT.BaseTypeRepr tp ->
  Bool ->
  Identifier ->
  Exp tp ->
  VerilogM sym n ()
addWire :: forall (tp :: BaseType) sym n.
BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n ()
addWire BaseTypeRepr tp
tp Bool
isSigned Identifier
name Exp tp
e =
  forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
st -> ModuleState sym n
st { vsWires :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsWires = (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr tp
tp, Bool
isSigned, Identifier
name, forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Exp tp
e) forall a. a -> [a] -> [a]
: forall sym n.
ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsWires ModuleState sym n
st }

-- | Create a fresh identifier by concatenating the given base with the
-- current fresh identifier counter.
freshIdentifier :: T.Text -> VerilogM sym n Identifier
freshIdentifier :: forall sym n. Identifier -> VerilogM sym n Identifier
freshIdentifier Identifier
basename = do
  ModuleState sym n
st <- forall s (m :: Type -> Type). MonadState s m => m s
get
  let used :: Set Identifier
used = forall sym n. ModuleState sym n -> Set Identifier
vsUsedIdentifiers ModuleState sym n
st
  let nm :: Identifier
nm | Identifier
basename forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Identifier
used =
             [Identifier] -> Identifier
T.concat [Identifier
basename, Identifier
"_", forall a. IsString a => String -> a
fromString forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. Set a -> Int
Set.size Set Identifier
used ]
         | Bool
otherwise = Identifier
basename
  forall s (m :: Type -> Type). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ ModuleState sym n
st { vsUsedIdentifiers :: Set Identifier
vsUsedIdentifiers = forall a. Ord a => a -> Set a -> Set a
Set.insert Identifier
nm Set Identifier
used }
  forall (m :: Type -> Type) a. Monad m => a -> m a
return Identifier
nm

-- | Add a new wire to the current Verilog module state, given a type, a
-- signedness flag, the prefix of a name, and an initializer expression.
-- The name prefix will be freshened by appending current value of the
-- fresh variable counter.
addFreshWire ::
  WT.BaseTypeRepr tp ->
  Bool ->
  T.Text ->
  Exp tp ->
  VerilogM sym n Identifier
addFreshWire :: forall (tp :: BaseType) sym n.
BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
addFreshWire BaseTypeRepr tp
repr Bool
isSigned Identifier
basename Exp tp
e = do
  Identifier
x <- forall sym n. Identifier -> VerilogM sym n Identifier
freshIdentifier Identifier
basename
  forall (tp :: BaseType) sym n.
BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n ()
addWire BaseTypeRepr tp
repr Bool
isSigned Identifier
x Exp tp
e
  forall (m :: Type -> Type) a. Monad m => a -> m a
return Identifier
x