{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Verismith.Reduce
(
reduceWithScript
, reduceSynth
, reduceSynthesis
, reduce
, reduce_
, Replacement(..)
, halveModules
, halveModItems
, halveStatements
, halveExpr
, halveAssigns
, findActiveWires
, clean
, cleanSourceInfo
, cleanSourceInfoAll
, removeDecl
, filterExpr
)
where
import Control.Lens hiding ((<.>))
import Control.Monad (void)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Data.Foldable (foldrM)
import Data.List (nub)
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Maybe (mapMaybe)
import Data.Text (Text)
import Shelly ((<.>))
import qualified Shelly
import Shelly.Lifted (MonadSh, liftSh)
import Verismith.Internal
import Verismith.Result
import Verismith.Sim
import Verismith.Sim.Internal
import Verismith.Verilog
import Verismith.Verilog.AST
import Verismith.Verilog.Mutate
import Verismith.Verilog.Parser
data Replacement a = Dual a a
| Single a
| None
deriving (Show, Eq)
type Replace a = a -> Replacement a
instance Functor Replacement where
fmap f (Dual a b) = Dual (f a) $ f b
fmap f (Single a) = Single $ f a
fmap _ None = None
instance Applicative Replacement where
pure = Single
(Dual a b) <*> (Dual c d) = Dual (a c) $ b d
(Dual a b) <*> (Single c) = Dual (a c) $ b c
(Single a) <*> (Dual b c) = Dual (a b) $ a c
(Single a) <*> (Single b) = Single $ a b
None <*> _ = None
_ <*> None = None
instance Foldable Replacement where
foldMap _ None = mempty
foldMap f (Single a) = f a
foldMap f (Dual a b) = f a <> f b
instance Traversable Replacement where
traverse _ None = pure None
traverse f (Single a) = Single <$> f a
traverse f (Dual a b) = Dual <$> f a <*> f b
halve :: Replace [a]
halve [] = Single []
halve [_] = Single []
halve l = Dual a b where (a, b) = splitAt (length l `div` 2) l
halveNonEmpty :: Replace (NonEmpty a)
halveNonEmpty l = case NonEmpty.splitAt (length l `div` 2) l of
([] , [] ) -> None
([] , a : b) -> Single $ a :| b
(a : b, [] ) -> Single $ a :| b
(a : b, c : d) -> Dual (a :| b) $ c :| d
combine :: Lens' a b -> Replace b -> Replace a
combine l f i = modify <$> f (i ^. l) where modify res = i & l .~ res
filterExpr :: [Identifier] -> Expr -> Expr
filterExpr ids (Id i) = if i `elem` ids then Id i else Number 0
filterExpr ids (VecSelect i e) =
if i `elem` ids then VecSelect i e else Number 0
filterExpr ids (RangeSelect i r) =
if i `elem` ids then RangeSelect i r else Number 0
filterExpr _ e = e
filterAssigns :: [Port] -> ModItem -> Bool
filterAssigns out (ModCA (ContAssign i _)) =
elem i $ out ^.. traverse . portName
filterAssigns _ _ = True
clean :: (Mutate a) => [Identifier] -> a -> a
clean ids = mutExpr (transform $ filterExpr ids)
cleanUndefined :: [Identifier] -> [ModItem] -> [ModItem]
cleanUndefined ids mis = clean usedWires mis
where
usedWires = mis ^.. traverse . modContAssign . contAssignNetLVal <> ids
halveModAssign :: Replace ModDecl
halveModAssign m = cleanMod m $ modify <$> assigns (m ^. modItems)
where
assigns = halve . filter (filterAssigns $ m ^. modOutPorts)
modify l = m & modItems .~ l
cleanMod :: ModDecl -> Replacement ModDecl -> Replacement ModDecl
cleanMod m newm = modify . change <$> newm
where
mis = m ^. modItems
modify l = m & modItems .~ l
change l =
cleanUndefined (m ^.. modInPorts . traverse . portName)
. combineAssigns (head $ m ^. modOutPorts)
. (filter (not . filterAssigns []) mis <>)
$ l
^. modItems
halveIndExpr :: Replace Expr
halveIndExpr (Concat l ) = Concat <$> halveNonEmpty l
halveIndExpr (BinOp e1 _ e2) = Dual e1 e2
halveIndExpr (Cond _ e1 e2) = Dual e1 e2
halveIndExpr (UnOp _ e ) = Single e
halveIndExpr (Appl _ e ) = Single e
halveIndExpr e = Single e
halveModExpr :: Replace ModItem
halveModExpr (ModCA ca) = ModCA <$> combine contAssignExpr halveIndExpr ca
halveModExpr a = Single a
cleanModInst :: SourceInfo -> SourceInfo
cleanModInst srcInfo = srcInfo & infoSrc . _Wrapped .~ cleaned
where
validInst = srcInfo ^.. infoSrc . _Wrapped . traverse . modId
cleaned = cleanModInst' validInst <$> srcInfo ^. infoSrc . _Wrapped
cleanModInst' :: [Identifier] -> ModDecl -> ModDecl
cleanModInst' ids m = m & modItems .~ newModItem
where newModItem = filter (validModInst ids) $ m ^.. modItems . traverse
validModInst :: [Identifier] -> ModItem -> Bool
validModInst ids (ModInst i _ _) = i `elem` ids
validModInst _ _ = True
addMod :: ModDecl -> SourceInfo -> SourceInfo
addMod m srcInfo = srcInfo & infoSrc . _Wrapped %~ (m :)
halveAssigns :: Replace SourceInfo
halveAssigns = combine mainModule halveModAssign
relevantModItem :: ModDecl -> ModItem -> Bool
relevantModItem (ModDecl _ out _ _ _) (ModCA (ContAssign i _)) =
i `elem` fmap _portName out
relevantModItem _ Decl{} = True
relevantModItem _ _ = False
isAssign :: Statement -> Bool
isAssign (BlockAssign _) = True
isAssign (NonBlockAssign _) = True
isAssign _ = False
lValName :: LVal -> [Identifier]
lValName (RegId i ) = [i]
lValName (RegExpr i _) = [i]
lValName (RegSize i _) = [i]
lValName (RegConcat e) = mapMaybe getId . concat $ universe <$> e
where
getId (Id i) = Just i
getId _ = Nothing
exprName :: Expr -> [Identifier]
exprName (Id i ) = [i]
exprName (VecSelect i _) = [i]
exprName (RangeSelect i _) = [i]
exprName (Concat i ) = concat . NonEmpty.toList $ exprName <$> i
exprName _ = []
exprId :: Expr -> Maybe Identifier
exprId (Id i ) = Just i
exprId (VecSelect i _) = Just i
exprId (RangeSelect i _) = Just i
exprId _ = Nothing
eventId :: Event -> Maybe Identifier
eventId (EId i) = Just i
eventId (EPosEdge i) = Just i
eventId (ENegEdge i) = Just i
eventId _ = Nothing
portToId :: Port -> Identifier
portToId (Port _ _ _ i) = i
paramToId :: Parameter -> Identifier
paramToId (Parameter i _) = i
isModule :: Identifier -> ModDecl -> Bool
isModule i (ModDecl n _ _ _ _) = i == n
modInstActive :: [ModDecl] -> ModItem -> [Identifier]
modInstActive decl (ModInst n _ i) = case m of
Nothing -> []
Just m' -> concat $ calcActive m' <$> zip i [0 ..]
where
m = safe head $ filter (isModule n) decl
calcActive (ModDecl _ o _ _ _) (ModConn e, n') | n' < length o = exprName e
| otherwise = []
calcActive (ModDecl _ o _ _ _) (ModConnNamed i' e, _)
| i' `elem` fmap _portName o = exprName e
| otherwise = []
modInstActive _ _ = []
fixModInst :: SourceInfo -> ModItem -> ModItem
fixModInst (SourceInfo _ (Verilog decl)) (ModInst n g i) = case m of
Nothing -> error "Moditem not found"
Just m' -> ModInst n g . mapMaybe (fixModInst' m') $ zip i [0 ..]
where
m = safe head $ filter (isModule n) decl
fixModInst' (ModDecl _ o i' _ _) (ModConn e, n')
| n' < length o + length i' = Just $ ModConn e
| otherwise = Nothing
fixModInst' (ModDecl _ o i'' _ _) (ModConnNamed i' e, _)
| i' `elem` fmap _portName (o <> i'') = Just $ ModConnNamed i' e
| otherwise = Nothing
fixModInst _ a = a
findActiveWires :: Identifier -> SourceInfo -> [Identifier]
findActiveWires t src =
nub
$ assignWires
<> assignStat
<> fmap portToId i
<> fmap portToId o
<> fmap paramToId p
<> modinstwires
where
assignWires = m ^.. modItems . traverse . modContAssign . contAssignNetLVal
assignStat =
concatMap lValName
$ (allStat ^.. traverse . stmntBA . assignReg)
<> (allStat ^.. traverse . stmntNBA . assignReg)
allStat = filter isAssign . concat $ fmap universe stat
stat =
(m ^.. modItems . traverse . _Initial)
<> (m ^.. modItems . traverse . _Always)
modinstwires =
concat $ modInstActive (src ^. infoSrc . _Wrapped) <$> m ^. modItems
m@(ModDecl _ o i _ p) = src ^. aModule t
cleanSourceInfo :: Identifier -> SourceInfo -> SourceInfo
cleanSourceInfo t src = src & aModule t %~ clean (findActiveWires t src)
cleanSourceInfoAll :: SourceInfo -> SourceInfo
cleanSourceInfoAll src = foldr cleanSourceInfo src allMods
where allMods = src ^.. infoSrc . _Wrapped . traverse . modId
matchesModName :: Identifier -> ModDecl -> Bool
matchesModName top (ModDecl i _ _ _ _) = top == i
halveStatement :: Replace Statement
halveStatement (SeqBlock [s]) = halveStatement s
halveStatement (SeqBlock s) = SeqBlock <$> halve s
halveStatement (CondStmnt _ (Just s1) (Just s2)) = Dual s1 s2
halveStatement (CondStmnt _ (Just s1) Nothing) = Single s1
halveStatement (CondStmnt _ Nothing (Just s1)) = Single s1
halveStatement (EventCtrl e (Just s)) = EventCtrl e . Just <$> halveStatement s
halveStatement (TimeCtrl e (Just s)) = TimeCtrl e . Just <$> halveStatement s
halveStatement a = Single a
halveAlways :: Replace ModItem
halveAlways (Always s) = Always <$> halveStatement s
halveAlways a = Single a
halveModules :: Replace SourceInfo
halveModules srcInfo@(SourceInfo top _) =
cleanSourceInfoAll
. cleanModInst
. addMod main
<$> combine (infoSrc . _Wrapped) repl srcInfo
where
repl = halve . filter (not . matchesModName (Identifier top))
main = srcInfo ^. mainModule
moduleBot :: SourceInfo -> Bool
moduleBot (SourceInfo _ (Verilog [] )) = True
moduleBot (SourceInfo _ (Verilog [_])) = True
moduleBot (SourceInfo _ (Verilog _ )) = False
halveModItems :: Identifier -> Replace SourceInfo
halveModItems t srcInfo = cleanSourceInfo t . addRelevant <$> src
where
repl = halve . filter (not . relevantModItem main)
relevant = filter (relevantModItem main) $ main ^. modItems
main = srcInfo ^. aModule t
src = combine (aModule t . modItems) repl srcInfo
addRelevant = aModule t . modItems %~ (relevant ++)
modItemBot :: Identifier -> SourceInfo -> Bool
modItemBot t srcInfo | length modItemsNoDecl > 2 = False
| otherwise = True
where
modItemsNoDecl =
filter noDecl $ srcInfo ^.. aModule t . modItems . traverse
noDecl Decl{} = False
noDecl _ = True
halveStatements :: Identifier -> Replace SourceInfo
halveStatements t m =
cleanSourceInfo t <$> combine (aModule t . modItems) halves m
where halves = traverse halveAlways
halveExpr :: Identifier -> Replace SourceInfo
halveExpr t = combine contexpr $ traverse halveModExpr
where
contexpr :: Lens' SourceInfo [ModItem]
contexpr = aModule t . modItems
toIds :: [Expr] -> [Identifier]
toIds = nub . mapMaybe exprId . concatMap universe
toIdsConst :: [ConstExpr] -> [Identifier]
toIdsConst = toIds . fmap constToExpr
toIdsEvent :: [Event] -> [Identifier]
toIdsEvent = nub . mapMaybe eventId . concatMap universe
allStatIds' :: Statement -> [Identifier]
allStatIds' s = nub $ assignIds <> otherExpr <> eventProcessedIds
where
assignIds =
toIds
$ (s ^.. stmntBA . assignExpr)
<> (s ^.. stmntNBA . assignExpr)
<> (s ^.. forAssign . assignExpr)
<> (s ^.. forIncr . assignExpr)
otherExpr = toIds $ (s ^.. forExpr) <> (s ^.. stmntCondExpr)
eventProcessedIds = toIdsEvent $ s ^.. statEvent
allStatIds :: Statement -> [Identifier]
allStatIds s = nub . concat $ allStatIds' <$> universe s
fromRange :: Range -> [ConstExpr]
fromRange r = [rangeMSB r, rangeLSB r]
allExprIds :: ModDecl -> [Identifier]
allExprIds m =
nub
$ contAssignIds
<> modInstIds
<> modInitialIds
<> modAlwaysIds
<> modPortIds
<> modDeclIds
<> paramIds
where
contAssignIds =
toIds $ m ^.. modItems . traverse . modContAssign . contAssignExpr
modInstIds =
toIds $ m ^.. modItems . traverse . modInstConns . traverse . modExpr
modInitialIds =
nub . concatMap allStatIds $ m ^.. modItems . traverse . _Initial
modAlwaysIds =
nub . concatMap allStatIds $ m ^.. modItems . traverse . _Always
modPortIds =
nub
. concatMap (toIdsConst . fromRange)
$ m
^.. modItems
. traverse
. declPort
. portSize
modDeclIds = toIdsConst $ m ^.. modItems . traverse . declVal . _Just
paramIds =
toIdsConst
$ (m ^.. modItems . traverse . paramDecl . traverse . paramValue)
<> ( m
^.. modItems
. traverse
. localParamDecl
. traverse
. localParamValue
)
isUsedDecl :: [Identifier] -> ModItem -> Bool
isUsedDecl ids (Decl _ (Port _ _ _ i) _) = i `elem` ids
isUsedDecl _ _ = True
isUsedParam :: [Identifier] -> Parameter -> Bool
isUsedParam ids (Parameter i _) = i `elem` ids
isUsedPort :: [Identifier] -> Port -> Bool
isUsedPort ids (Port _ _ _ i) = i `elem` ids
removeDecl :: SourceInfo -> SourceInfo
removeDecl src = foldr fix removed allMods
where
removeDecl' t src' =
src'
& (\a -> a & aModule t . modItems %~ filter
(isUsedDecl (used <> findActiveWires t a))
)
. (aModule t . modParams %~ filter (isUsedParam used))
. (aModule t . modInPorts %~ filter (isUsedPort used))
where used = nub $ allExprIds (src' ^. aModule t)
allMods = src ^.. infoSrc . _Wrapped . traverse . modId
fix t a = a & aModule t . modItems %~ fmap (fixModInst a)
removed = foldr removeDecl' src allMods
defaultBot :: SourceInfo -> Bool
defaultBot = const False
reduce_
:: MonadSh m
=> Text
-> Replace SourceInfo
-> (SourceInfo -> Bool)
-> (SourceInfo -> m Bool)
-> SourceInfo
-> m SourceInfo
reduce_ title repl bot eval src = do
liftSh
. Shelly.echo
$ "Reducing "
<> title
<> " (Modules: "
<> showT (length . getVerilog $ _infoSrc src)
<> ", Module items: "
<> showT
(length
(src ^.. infoSrc . _Wrapped . traverse . modItems . traverse)
)
<> ")"
if bot src
then return src
else case repl src of
Single s -> do
red <- eval s
if red
then if cond s then recReduction s else return s
else return src
Dual l r -> do
red <- eval l
if red
then if cond l then recReduction l else return l
else do
red' <- eval r
if red'
then if cond r then recReduction r else return r
else return src
None -> return src
where
cond s = s /= src
recReduction = reduce_ title repl bot eval
reduce
:: MonadSh m
=> (SourceInfo -> m Bool)
-> SourceInfo
-> m SourceInfo
reduce eval src =
fmap removeDecl
$ red "Modules" moduleBot halveModules src
>>= redAll "Module Items" modItemBot halveModItems
>>= redAll "Statements" (const defaultBot) halveStatements
where
red s bot a = reduce_ s a bot eval
red' s bot a t = reduce_ s (a t) (bot t) eval
redAll s bot halve' src' = foldrM
(\t -> red' (s <> " (" <> getIdentifier t <> ")") bot halve' t)
src'
(src' ^.. infoSrc . _Wrapped . traverse . modId)
runScript
:: MonadSh m => Shelly.FilePath -> Shelly.FilePath -> SourceInfo -> m Bool
runScript fp file src = do
e <- liftSh $ do
Shelly.writefile file $ genSource src
noPrint . Shelly.errExit False $ Shelly.run_ fp []
Shelly.lastExitCode
return $ e == 0
reduceWithScript
:: (MonadSh m, MonadIO m)
=> Text
-> Shelly.FilePath
-> Shelly.FilePath
-> m ()
reduceWithScript top script file = do
liftSh . Shelly.cp file $ file <.> "original"
srcInfo <- liftIO . parseSourceInfoFile top $ Shelly.toTextIgnore file
void $ reduce (runScript script file) srcInfo
reduceSynth
:: (Synthesiser a, Synthesiser b, MonadSh m)
=> a
-> b
-> SourceInfo
-> m SourceInfo
reduceSynth a b = reduce synth
where
synth src' = liftSh $ do
r <- runResultT $ do
runSynth a src'
runSynth b src'
runEquiv a b src'
return $ case r of
Fail EquivFail -> True
Fail _ -> False
Pass _ -> False
reduceSynthesis :: (Synthesiser a, MonadSh m) => a -> SourceInfo -> m SourceInfo
reduceSynthesis a = reduce synth
where
synth src = liftSh $ do
r <- runResultT $ runSynth a src
return $ case r of
Fail SynthFail -> True
Fail _ -> False
Pass _ -> False