From 7124a4f00e536b4d5323a7488c1f65469dddb102 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 12 May 2020 12:21:36 +0100 Subject: Format with ormolu --- src/Verismith.hs | 503 +++++++++++++++++++++++++++++-------------------------- 1 file changed, 264 insertions(+), 239 deletions(-) (limited to 'src/Verismith.hs') diff --git a/src/Verismith.hs b/src/Verismith.hs index e709ff4..4fb52ac 100644 --- a/src/Verismith.hs +++ b/src/Verismith.hs @@ -1,133 +1,137 @@ -{-| -Module : Verismith -Description : Verismith -Copyright : (c) 2018-2019, Yann Herklotz -License : GPL-3 -Maintainer : yann [at] yannherklotz [dot] com -Stability : experimental -Portability : POSIX --} - {-# OPTIONS_GHC -Wno-unused-top-binds #-} +-- | +-- Module : Verismith +-- Description : Verismith +-- Copyright : (c) 2018-2019, Yann Herklotz +-- License : GPL-3 +-- Maintainer : yann [at] yannherklotz [dot] com +-- Stability : experimental +-- Portability : POSIX module Verismith - ( defaultMain + ( defaultMain, + -- * Types - , Opts(..) - , SourceInfo(..) + Opts (..), + SourceInfo (..), + -- * Run functions - , runEquivalence - , runSimulation - , runReduce - , draw + runEquivalence, + runSimulation, + runReduce, + draw, + -- * Verilog generation functions - , procedural - , proceduralIO - , proceduralSrc - , proceduralSrcIO - , randomMod + procedural, + proceduralIO, + proceduralSrc, + proceduralSrcIO, + randomMod, + -- * Extra modules - , module Verismith.Verilog - , module Verismith.Config - , module Verismith.Circuit - , module Verismith.Tool - , module Verismith.Fuzz - , module Verismith.Report - ) + module Verismith.Verilog, + module Verismith.Config, + module Verismith.Circuit, + module Verismith.Tool, + module Verismith.Fuzz, + module Verismith.Report, + ) where -import Control.Concurrent -import Control.Lens hiding ((<.>)) -import Control.Monad.IO.Class (liftIO) -import Data.ByteString (ByteString) -import Data.ByteString.Builder (byteStringHex, toLazyByteString) -import qualified Data.ByteString.Lazy as L -import qualified Data.Graph.Inductive as G +import Control.Concurrent +import Control.Lens hiding ((<.>)) +import Control.Monad.IO.Class (liftIO) +import Data.ByteString (ByteString) +import Data.ByteString.Builder (byteStringHex, toLazyByteString) +import qualified Data.ByteString.Lazy as L +import qualified Data.Graph.Inductive as G import qualified Data.Graph.Inductive.Dot as G -import Data.Maybe (isNothing) -import Data.Text (Text) -import qualified Data.Text as T -import Data.Text.Encoding (decodeUtf8) -import qualified Data.Text.IO as T -import Hedgehog (Gen) -import qualified Hedgehog.Gen as Hog -import Hedgehog.Internal.Seed (Seed) -import Options.Applicative -import Paths_verismith (getDataDir) -import Prelude hiding (FilePath) -import Shelly hiding (command) -import Shelly.Lifted (liftSh) -import System.Random (randomIO) -import Verismith.Circuit -import Verismith.Config -import Verismith.Fuzz -import Verismith.Generate -import Verismith.OptParser -import Verismith.Reduce -import Verismith.Report -import Verismith.Result -import Verismith.Tool -import Verismith.Tool.Internal -import Verismith.Verilog -import Verismith.Verilog.Parser (parseSourceInfoFile) +import Data.Maybe (isNothing) +import Data.Text (Text) +import qualified Data.Text as T +import Data.Text.Encoding (decodeUtf8) +import qualified Data.Text.IO as T +import Hedgehog (Gen) +import qualified Hedgehog.Gen as Hog +import Hedgehog.Internal.Seed (Seed) +import Options.Applicative +import Paths_verismith (getDataDir) +import Shelly hiding (command) +import Shelly.Lifted (liftSh) +import System.Random (randomIO) +import Verismith.Circuit +import Verismith.Config +import Verismith.Fuzz +import Verismith.Generate +import Verismith.OptParser +import Verismith.Reduce +import Verismith.Report +import Verismith.Result +import Verismith.Tool +import Verismith.Tool.Internal import Verismith.Utils (generateByteString) +import Verismith.Verilog +import Verismith.Verilog.Parser (parseSourceInfoFile) +import Prelude hiding (FilePath) toFP :: String -> FilePath toFP = fromText . T.pack myForkIO :: IO () -> IO (MVar ()) myForkIO io = do - mvar <- newEmptyMVar - _ <- forkFinally io (\_ -> putMVar mvar ()) - return mvar + mvar <- newEmptyMVar + _ <- forkFinally io (\_ -> putMVar mvar ()) + return mvar getConfig :: Maybe FilePath -> IO Config getConfig s = - maybe (return defaultConfig) parseConfigFile $ T.unpack . toTextIgnore <$> s + maybe (return defaultConfig) parseConfigFile $ T.unpack . toTextIgnore <$> s getGenerator :: Config -> Text -> Maybe FilePath -> IO (Gen (SourceInfo ())) getGenerator config top s = - maybe (return $ proceduralSrc top config) (fmap return . parseSourceInfoFile top) - $ toTextIgnore <$> s + maybe (return $ proceduralSrc top config) (fmap return . parseSourceInfoFile top) $ + toTextIgnore <$> s -- | Randomly remove an option by setting it to 0. randDelete :: Int -> IO Int randDelete i = do - r <- randomIO - return $ if r then i else 0 + r <- randomIO + return $ if r then i else 0 randomise :: Config -> IO Config randomise config@(Config a _ c d e) = do - mia <- return $ cm ^. probModItemAssign - misa <- return $ cm ^. probModItemSeqAlways - mica <- return $ cm ^. probModItemCombAlways - mii <- return $ cm ^. probModItemInst - ssb <- return $ cs ^. probStmntBlock - ssnb <- return $ cs ^. probStmntNonBlock - ssc <- return $ cs ^. probStmntCond - ssf <- return $ cs ^. probStmntFor - en <- return $ ce ^. probExprNum - keep_out <- return $ cmo ^. probModDropOutput - drop_out <- randDelete $ cmo ^. probModDropOutput - ei <- randDelete $ ce ^. probExprId - ers <- randDelete $ ce ^. probExprRangeSelect - euo <- randDelete $ ce ^. probExprUnOp - ebo <- randDelete $ ce ^. probExprBinOp - ec <- randDelete $ ce ^. probExprCond - eco <- randDelete $ ce ^. probExprConcat - estr <- randDelete $ ce ^. probExprStr - esgn <- randDelete $ ce ^. probExprSigned - eus <- randDelete $ ce ^. probExprUnsigned - return $ Config - a - (Probability (ProbModItem mia misa mica mii) - (ProbStatement ssb ssnb ssc ssf) - (ProbExpr en ei ers euo ebo ec eco estr esgn eus) - (ProbMod drop_out keep_out) - ) - c - d - e + mia <- return $ cm ^. probModItemAssign + misa <- return $ cm ^. probModItemSeqAlways + mica <- return $ cm ^. probModItemCombAlways + mii <- return $ cm ^. probModItemInst + ssb <- return $ cs ^. probStmntBlock + ssnb <- return $ cs ^. probStmntNonBlock + ssc <- return $ cs ^. probStmntCond + ssf <- return $ cs ^. probStmntFor + en <- return $ ce ^. probExprNum + keep_out <- return $ cmo ^. probModDropOutput + drop_out <- randDelete $ cmo ^. probModDropOutput + ei <- randDelete $ ce ^. probExprId + ers <- randDelete $ ce ^. probExprRangeSelect + euo <- randDelete $ ce ^. probExprUnOp + ebo <- randDelete $ ce ^. probExprBinOp + ec <- randDelete $ ce ^. probExprCond + eco <- randDelete $ ce ^. probExprConcat + estr <- randDelete $ ce ^. probExprStr + esgn <- randDelete $ ce ^. probExprSigned + eus <- randDelete $ ce ^. probExprUnsigned + return $ + Config + a + ( Probability + (ProbModItem mia misa mica mii) + (ProbStatement ssb ssnb ssc ssf) + (ProbExpr en ei ers euo ebo ec eco estr esgn eus) + (ProbMod drop_out keep_out) + ) + c + d + e where cm = config ^. configProbability . probModItem cs = config ^. configProbability . probStmnt @@ -136,91 +140,107 @@ randomise config@(Config a _ c d e) = do handleOpts :: Opts -> IO () handleOpts (Fuzz o configF f k n nosim noequiv noreduction file top cc checker) = do - config <- getConfig configF - gen <- getGenerator config top file - datadir <- getDataDir - _ <- runFuzz - (FuzzOpts (Just $ fromText o) - f k n nosim noequiv noreduction config (toFP datadir) cc checker) - defaultYosys - (fuzzMultiple gen) - return () + config <- getConfig configF + gen <- getGenerator config top file + datadir <- getDataDir + _ <- + runFuzz + ( FuzzOpts + (Just $ fromText o) + f + k + n + nosim + noequiv + noreduction + config + (toFP datadir) + cc + checker + ) + defaultYosys + (fuzzMultiple gen) + return () handleOpts (Generate f c) = do - config <- getConfig c - source <- proceduralIO "top" config :: IO (Verilog ()) - maybe (T.putStrLn $ genSource source) (flip T.writeFile $ genSource source) - $ T.unpack - . toTextIgnore - <$> f + config <- getConfig c + source <- proceduralIO "top" config :: IO (Verilog ()) + maybe (T.putStrLn $ genSource source) (flip T.writeFile $ genSource source) $ + T.unpack + . toTextIgnore + <$> f handleOpts (Parse f t o rc) = do - verilogSrc <- T.readFile file - case parseVerilog (T.pack file) verilogSrc of - Left l -> print l - Right v -> - case (o, GenVerilog - . mapply rc (takeReplace . removeConstInConcat) - $ SourceInfo t v) of - (Nothing, a) -> print a - (Just o', a) -> writeFile (T.unpack $ toTextIgnore o') $ show a + verilogSrc <- T.readFile file + case parseVerilog (T.pack file) verilogSrc of + Left l -> print l + Right v -> + case ( o, + GenVerilog + . mapply rc (takeReplace . removeConstInConcat) + $ SourceInfo t v + ) of + (Nothing, a) -> print a + (Just o', a) -> writeFile (T.unpack $ toTextIgnore o') $ show a where file = T.unpack . toTextIgnore $ f mapply i f = if i then f else id handleOpts (Reduce f t _ ls' False) = do - src <- parseSourceInfoFile t (toTextIgnore f) - datadir <- getDataDir - case descriptionToSynth <$> ls' of - a : b : _ -> do - putStrLn "Reduce with equivalence check" - shelly $ do - make dir - pop dir $ do - src' <- reduceSynth Nothing (toFP datadir) a b src :: Sh (SourceInfo ()) - writefile (fromText ".." dir <.> "v") $ genSource src' - a : _ -> do - putStrLn "Reduce with synthesis failure" - shelly $ do - make dir - pop dir $ do - src' <- reduceSynthesis a src - writefile (fromText ".." dir <.> "v") $ genSource src' - _ -> do - putStrLn "Not reducing because no synthesiser was specified" - return () - where dir = fromText "reduce" + src <- parseSourceInfoFile t (toTextIgnore f) + datadir <- getDataDir + case descriptionToSynth <$> ls' of + a : b : _ -> do + putStrLn "Reduce with equivalence check" + shelly $ do + make dir + pop dir $ do + src' <- reduceSynth Nothing (toFP datadir) a b src :: Sh (SourceInfo ()) + writefile (fromText ".." dir <.> "v") $ genSource src' + a : _ -> do + putStrLn "Reduce with synthesis failure" + shelly $ do + make dir + pop dir $ do + src' <- reduceSynthesis a src + writefile (fromText ".." dir <.> "v") $ genSource src' + _ -> do + putStrLn "Not reducing because no synthesiser was specified" + return () + where + dir = fromText "reduce" handleOpts (Reduce f t _ ls' True) = do - src <- parseSourceInfoFile t (toTextIgnore f) :: IO (SourceInfo ()) - datadir <- getDataDir - case descriptionToSynth <$> ls' of - a : b : _ -> do - putStrLn "Starting equivalence check" - res <- shelly . runResultT $ do - make dir - pop dir $ do - runSynth a src - runSynth b src - runEquiv Nothing (toFP datadir) a b src - case res of - Pass _ -> putStrLn "Equivalence check passed" - Fail (EquivFail _) -> putStrLn "Equivalence check failed" - Fail TimeoutError -> putStrLn "Equivalence check timed out" - Fail _ -> putStrLn "Equivalence check error" - return () - as -> do - putStrLn "Synthesis check" - _ <- shelly . runResultT $ mapM (flip runSynth src) as - return () - where dir = fromText "equiv" + src <- parseSourceInfoFile t (toTextIgnore f) :: IO (SourceInfo ()) + datadir <- getDataDir + case descriptionToSynth <$> ls' of + a : b : _ -> do + putStrLn "Starting equivalence check" + res <- shelly . runResultT $ do + make dir + pop dir $ do + runSynth a src + runSynth b src + runEquiv Nothing (toFP datadir) a b src + case res of + Pass _ -> putStrLn "Equivalence check passed" + Fail (EquivFail _) -> putStrLn "Equivalence check failed" + Fail TimeoutError -> putStrLn "Equivalence check timed out" + Fail _ -> putStrLn "Equivalence check error" + return () + as -> do + putStrLn "Synthesis check" + _ <- shelly . runResultT $ mapM (flip runSynth src) as + return () + where + dir = fromText "equiv" handleOpts (ConfigOpt c conf r) = do - config <- if r then getConfig conf >>= randomise else getConfig conf - maybe (T.putStrLn . encodeConfig $ config) (`encodeConfigFile` config) - $ T.unpack - . toTextIgnore - <$> c + config <- if r then getConfig conf >>= randomise else getConfig conf + maybe (T.putStrLn . encodeConfig $ config) (`encodeConfigFile` config) $ + T.unpack + . toTextIgnore + <$> c defaultMain :: IO () defaultMain = do - optsparsed <- execParser opts - handleOpts optsparsed + optsparsed <- execParser opts + handleOpts optsparsed makeSrcInfo :: (ModDecl ann) -> (SourceInfo ann) makeSrcInfo m = SourceInfo (getIdentifier $ m ^. modId) (Verilog [m]) @@ -229,10 +249,10 @@ makeSrcInfo m = SourceInfo (getIdentifier $ m ^. modId) (Verilog [m]) -- can be seen. draw :: IO () draw = do - gr <- Hog.sample $ rDups . getCircuit <$> Hog.resize 10 randomDAG - let dot = G.showDot . G.fglToDotString $ G.nemap show (const "") gr - writeFile "file.dot" dot - shelly $ run_ "dot" ["-Tpng", "-o", "file.png", "file.dot"] + gr <- Hog.sample $ rDups . getCircuit <$> Hog.resize 10 randomDAG + let dot = G.showDot . G.fglToDotString $ G.nemap show (const "") gr + writeFile "file.dot" dot + shelly $ run_ "dot" ["-Tpng", "-o", "file.png", "file.dot"] -- | Function to show a bytestring in a hex format. showBS :: ByteString -> Text @@ -247,80 +267,85 @@ runSimulation = do -- shelly $ run_ "dot" ["-Tpng", "-o", "file.png", "file.dot"] -- let circ = -- head $ (nestUpTo 30 . generateAST $ Circuit gr) ^.. getVerilog . traverse . getDescription - rand <- generateByteString Nothing 32 20 - rand2 <- Hog.sample (randomMod 10 100) :: IO (ModDecl ()) - val <- shelly . runResultT $ runSim defaultIcarus (makeSrcInfo rand2) rand - case val of - Pass a -> T.putStrLn $ showBS a - _ -> T.putStrLn "Test failed" - + rand <- generateByteString Nothing 32 20 + rand2 <- Hog.sample (randomMod 10 100) :: IO (ModDecl ()) + val <- shelly . runResultT $ runSim defaultIcarus (makeSrcInfo rand2) rand + case val of + Pass a -> T.putStrLn $ showBS a + _ -> T.putStrLn "Test failed" -- | Code to be executed on a failure. Also checks if the failure was a timeout, -- as the timeout command will return the 124 error code if that was the -- case. In that case, the error will be moved to a different directory. onFailure :: Text -> RunFailed -> Sh (Result Failed ()) onFailure t _ = do - ex <- lastExitCode - case ex of - 124 -> do - logger "Test TIMEOUT" - chdir ".." $ cp_r (fromText t) $ fromText (t <> "_timeout") - return $ Fail EmptyFail - _ -> do - logger "Test FAIL" - chdir ".." $ cp_r (fromText t) $ fromText (t <> "_failed") - return $ Fail EmptyFail + ex <- lastExitCode + case ex of + 124 -> do + logger "Test TIMEOUT" + chdir ".." $ cp_r (fromText t) $ fromText (t <> "_timeout") + return $ Fail EmptyFail + _ -> do + logger "Test FAIL" + chdir ".." $ cp_r (fromText t) $ fromText (t <> "_failed") + return $ Fail EmptyFail checkEquivalence :: Show ann => SourceInfo ann -> Text -> IO Bool checkEquivalence src dir = shellyFailDir $ do - mkdir_p (fromText dir) - curr <- toTextIgnore <$> pwd - datadir <- liftIO getDataDir - setenv "VERISMITH_ROOT" curr - cd (fromText dir) - catch_sh - ((runResultT $ runEquiv Nothing (toFP datadir) defaultYosys defaultVivado src) >> return True) - ((\_ -> return False) :: RunFailed -> Sh Bool) + mkdir_p (fromText dir) + curr <- toTextIgnore <$> pwd + datadir <- liftIO getDataDir + setenv "VERISMITH_ROOT" curr + cd (fromText dir) + catch_sh + ((runResultT $ runEquiv Nothing (toFP datadir) defaultYosys defaultVivado src) >> return True) + ((\_ -> return False) :: RunFailed -> Sh Bool) -- | Run a fuzz run and check if all of the simulators passed by checking if the -- generated Verilog files are equivalent. -runEquivalence - :: Maybe Seed - -> Gen (Verilog ()) -- ^ Generator for the Verilog file. - -> Text -- ^ Name of the folder on each thread. - -> Text -- ^ Name of the general folder being used. - -> Bool -- ^ Keep flag. - -> Int -- ^ Used to track the recursion. - -> IO () +runEquivalence :: + Maybe Seed -> + -- | Generator for the Verilog file. + Gen (Verilog ()) -> + -- | Name of the folder on each thread. + Text -> + -- | Name of the general folder being used. + Text -> + -- | Keep flag. + Bool -> + -- | Used to track the recursion. + Int -> + IO () runEquivalence seed gm t d k i = do - (_, m) <- shelly $ sampleSeed seed gm - let srcInfo = SourceInfo "top" m - rand <- generateByteString Nothing 32 20 - datadir <- getDataDir - shellyFailDir $ do - mkdir_p (fromText d fromText n) - curr <- toTextIgnore <$> pwd - setenv "VERISMITH_ROOT" curr - cd (fromText "output" fromText n) - _ <- - catch_sh - ( runResultT - $ runEquiv Nothing (toFP datadir) defaultYosys defaultVivado srcInfo - >> liftSh (logger "Test OK") - ) - $ onFailure n - _ <- - catch_sh - ( runResultT - $ runSim (Icarus "iverilog" "vvp") srcInfo rand - >>= (\b -> liftSh $ logger ("RTL Sim: " <> showBS b)) - ) - $ onFailure n - cd ".." - unless k . rm_rf $ fromText n - when (i < 5 && isNothing seed) (runEquivalence seed gm t d k $ i + 1) - where n = t <> "_" <> T.pack (show i) + (_, m) <- shelly $ sampleSeed seed gm + let srcInfo = SourceInfo "top" m + rand <- generateByteString Nothing 32 20 + datadir <- getDataDir + shellyFailDir $ do + mkdir_p (fromText d fromText n) + curr <- toTextIgnore <$> pwd + setenv "VERISMITH_ROOT" curr + cd (fromText "output" fromText n) + _ <- + catch_sh + ( runResultT $ + runEquiv Nothing (toFP datadir) defaultYosys defaultVivado srcInfo + >> liftSh (logger "Test OK") + ) + $ onFailure n + _ <- + catch_sh + ( runResultT $ + runSim (Icarus "iverilog" "vvp") srcInfo rand + >>= (\b -> liftSh $ logger ("RTL Sim: " <> showBS b)) + ) + $ onFailure n + cd ".." + unless k . rm_rf $ fromText n + when (i < 5 && isNothing seed) (runEquivalence seed gm t d k $ i + 1) + where + n = t <> "_" <> T.pack (show i) runReduce :: (SourceInfo ()) -> IO (SourceInfo ()) runReduce s = - shelly $ reduce "reduce.v" (\s' -> not <$> liftIO (checkEquivalence s' "reduce")) s + shelly $ reduce "reduce.v" (\s' -> not <$> liftIO (checkEquivalence s' "reduce")) s -- cgit