{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Verismith.Reduce
(
reduceWithScript
, reduceSynth
, reduceSynthesis
, reduceSimIc
, reduce
, reduce_
, Replacement(..)
, halveModules
, halveModItems
, halveStatements
, halveExpr
, halveAssigns
, findActiveWires
, clean
, cleanSourceInfo
, cleanSourceInfoAll
, removeDecl
, removeConstInConcat
, takeReplace
, filterExpr
)
where
import Control.Lens hiding ((<.>))
import Control.Monad (void)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Data.ByteString (ByteString)
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 (fromText, (<.>))
import qualified Shelly
import Shelly.Lifted (MonadSh, liftSh, rm_rf, writefile)
import Verismith.Internal
import Verismith.Result
import Verismith.Tool
import Verismith.Tool.Icarus
import Verismith.Tool.Identity
import Verismith.Tool.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)
takeReplace :: (Monoid a) => Replacement a -> a
takeReplace (Single a) = a
takeReplace (Dual a _) = a
takeReplace None = mempty
removeConstInConcat :: Replace SourceInfo
removeConstInConcat = Single . mutExpr replace
where
replace :: Expr -> Expr
replace (Concat expr) = maybe (Number 0) Concat . NonEmpty.nonEmpty
$ NonEmpty.filter notConstant expr
replace e = e
notConstant (Number _) = False
notConstant _ = True
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
=> Shelly.FilePath
-> Text
-> Replace SourceInfo
-> (SourceInfo -> Bool)
-> (SourceInfo -> m Bool)
-> SourceInfo
-> m SourceInfo
reduce_ out title repl bot eval src = do
writefile out $ genSource src
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_ out title repl bot eval
reduce
:: MonadSh m
=> Shelly.FilePath
-> (SourceInfo -> m Bool)
-> SourceInfo
-> m SourceInfo
reduce fp eval src =
fmap removeDecl
$ red "Modules" moduleBot halveModules src
>>= redAll "Module items" modItemBot halveModItems
>>= redAll "Statements" (const defaultBot) halveStatements
>>= red "Remove constants in concat" defaultBot removeConstInConcat
where
red s bot a = reduce_ fp s a bot eval
red' s bot a t = reduce_ fp 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 (fromText "reduce_script.v") (runScript script file) srcInfo
reduceSynth
:: (Synthesiser a, Synthesiser b, MonadSh m)
=> Shelly.FilePath
-> a
-> b
-> SourceInfo
-> m SourceInfo
reduceSynth datadir a b = reduce (fromText $ "reduce_" <> toText a <> "_" <> toText b <> ".v") synth
where
synth src' = liftSh $ do
r <- runResultT $ do
runSynth a src'
runSynth b src'
runEquiv datadir a b src'
return $ case r of
Fail (EquivFail _) -> True
_ -> False
reduceSynthesis :: (Synthesiser a, MonadSh m) => a -> SourceInfo -> m SourceInfo
reduceSynthesis a = reduce (fromText $ "reduce_" <> toText a <> ".v") synth
where
synth src = liftSh $ do
r <- runResultT $ runSynth a src
return $ case r of
Fail SynthFail -> True
_ -> False
runInTmp :: Shelly.Sh a -> Shelly.Sh a
runInTmp a = Shelly.withTmpDir $ (\f -> do
dir <- Shelly.pwd
Shelly.cd f
r <- a
Shelly.cd dir
return r)
reduceSimIc :: (Synthesiser a, MonadSh m) => Shelly.FilePath -> [ByteString] -> a -> SourceInfo -> m SourceInfo
reduceSimIc fp bs a = reduce (fromText $ "reduce_sim_" <> toText a <> ".v") synth
where
synth src = liftSh . runInTmp $ do
r <- runResultT $ do
runSynth a src
runSynth defaultIdentity src
i <- runSimIc fp defaultIcarus defaultIdentity src bs Nothing
runSimIc fp defaultIcarus a src bs $ Just i
return $ case r of
Fail (SimFail _) -> True
_ -> False