From 8d96fd2a541a2602544ced741552ebd17714c67d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 18 Sep 2019 19:06:32 +0200 Subject: Rename main modules --- src/VeriSmith/Reduce.hs | 609 ------------------------------------------------ 1 file changed, 609 deletions(-) delete mode 100644 src/VeriSmith/Reduce.hs (limited to 'src/VeriSmith/Reduce.hs') diff --git a/src/VeriSmith/Reduce.hs b/src/VeriSmith/Reduce.hs deleted file mode 100644 index c57b457..0000000 --- a/src/VeriSmith/Reduce.hs +++ /dev/null @@ -1,609 +0,0 @@ -{-| -Module : VeriSmith.Reduce -Description : Test case reducer implementation. -Copyright : (c) 2019, Yann Herklotz -License : GPL-3 -Maintainer : yann [at] yannherklotz [dot] com -Stability : experimental -Portability : POSIX - -Test case reducer implementation. --} - -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} - -module VeriSmith.Reduce - ( -- $strategy - 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 - - --- $strategy --- The reduction strategy has multiple different steps. 'reduce' will run these --- strategies one after another, starting at the most coarse grained one. The --- supported reduction strategies are the following: --- --- [Modules] First of all, the reducer will try and remove all the modules --- except the top module. --- --- [Module Items] Then, the module items will be reduced by using standard --- delta debugging. Half of the module items will be removed, and both --- versions will be tested. If both succeed, they will be divided further and --- tested further. Finally, the shortest version will be returned. --- --- [Statements] Once the module items have been reduced, the statements will --- be reduced as well. This is done using delta debugging, just like the --- module items. --- --- [Expressions] Finally, the expressions themselves will be reduced. This is --- done by splitting the top most binary expressions in half and testing each --- half. - --- | Replacement type that supports returning different kinds of reduced --- replacements that could be tried. -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 - --- | Split a list in two halves. -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 - --- | When given a Lens and a function that works on a lower replacement, it will --- go down, apply the replacement, and return a replacement of the original --- module. -combine :: Lens' a b -> Replace b -> Replace a -combine l f i = modify <$> f (i ^. l) where modify res = i & l .~ res - --- | Deletes Id 'Expr' if they are not part of the current scope, and replaces --- these by 0. -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 - --- | Checks if a declaration is part of the current scope. If not, it returns --- 'False', otherwise 'True', as it should be kept. ---filterDecl :: [Identifier] -> ModItem -> Bool ---filterDecl ids (Decl Nothing (Port _ _ _ i) _) = i `elem` ids ---filterDecl _ _ = True - --- | Checks if a continuous assignment is in the current scope, if not, it --- returns 'False'. -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 - --- | Remove all the undefined mod instances. -cleanModInst :: SourceInfo -> SourceInfo -cleanModInst srcInfo = srcInfo & infoSrc . _Wrapped .~ cleaned - where - validInst = srcInfo ^.. infoSrc . _Wrapped . traverse . modId - cleaned = cleanModInst' validInst <$> srcInfo ^. infoSrc . _Wrapped - --- | Clean all the undefined module instances in a specific module using a --- context. -cleanModInst' :: [Identifier] -> ModDecl -> ModDecl -cleanModInst' ids m = m & modItems .~ newModItem - where newModItem = filter (validModInst ids) $ m ^.. modItems . traverse - --- | Check if a mod instance is in the current context. -validModInst :: [Identifier] -> ModItem -> Bool -validModInst ids (ModInst i _ _) = i `elem` ids -validModInst _ _ = True - --- | Adds a 'ModDecl' to a 'SourceInfo'. -addMod :: ModDecl -> SourceInfo -> SourceInfo -addMod m srcInfo = srcInfo & infoSrc . _Wrapped %~ (m :) - --- | Split a module declaration in half by trying to remove assign --- statements. This is only done in the main module of the source. -halveAssigns :: Replace SourceInfo -halveAssigns = combine mainModule halveModAssign - --- | Checks if a module item is needed in the module declaration. -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 - --- | Pretending that expr is an LVal for the case that it is in a module --- instantiation. -exprName :: Expr -> [Identifier] -exprName (Id i ) = [i] -exprName (VecSelect i _) = [i] -exprName (RangeSelect i _) = [i] -exprName (Concat i ) = concat . NonEmpty.toList $ exprName <$> i -exprName _ = [] - --- | Returns the only identifiers that are directly tied to an expression. This --- is useful if one does not have to recurse deeper into the expressions. -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 - --- | Clean a specific module. Have to be carful that the module is in the --- 'SourceInfo', otherwise it will crash. -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 - --- | Returns true if the text matches the name of a module. -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 - --- | Removes half the modules randomly, until it reaches a minimal amount of --- modules. This is done by doing a binary search on the list of modules and --- removing the instantiations from the main module body. -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 - --- | Reducer for module items. It does a binary search on all the module items, --- except assignments to outputs and input-output declarations. -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 - --- | Reduce expressions by splitting them in half and keeping the half that --- succeeds. -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 - --- | Reduction using custom reduction strategies. -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 an input to a minimal representation. It follows the reduction --- strategy mentioned above. -reduce - :: MonadSh m - => (SourceInfo -> m Bool) -- ^ Failed or not. - -> SourceInfo -- ^ Input verilog source to be reduced. - -> m SourceInfo -- ^ Reduced output. -reduce eval src = - fmap removeDecl - $ red "Modules" moduleBot halveModules src - >>= redAll "Module Items" modItemBot halveModItems - >>= redAll "Statements" (const defaultBot) halveStatements - -- >>= redAll "Expressions" (const defaultBot) halveExpr - 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 - --- | Reduce using a script that is passed to it -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 - --- | Reduce a 'SourceInfo' using two 'Synthesiser' that are passed to it. -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 -- cgit