diff options
Diffstat (limited to 'src/Verismith/Fuzz.hs')
| -rw-r--r-- | src/Verismith/Fuzz.hs | 742 |
1 files changed, 389 insertions, 353 deletions
diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs index 7771f6a..2fb9f00 100644 --- a/src/Verismith/Fuzz.hs +++ b/src/Verismith/Fuzz.hs @@ -1,114 +1,121 @@ -{-| -Module : Verismith.Fuzz -Description : Environment to run the simulator and synthesisers in a matrix. -Copyright : (c) 2019, Yann Herklotz -License : GPL-3 -Maintainer : yann [at] yannherklotz [dot] com -Stability : experimental -Portability : POSIX - -Environment to run the simulator and synthesisers in a matrix. --} - -{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TemplateHaskell #-} - +{-# LANGUAGE TemplateHaskell #-} + +-- | +-- Module : Verismith.Fuzz +-- Description : Environment to run the simulator and synthesisers in a matrix. +-- Copyright : (c) 2019, Yann Herklotz +-- License : GPL-3 +-- Maintainer : yann [at] yannherklotz [dot] com +-- Stability : experimental +-- Portability : POSIX +-- +-- Environment to run the simulator and synthesisers in a matrix. module Verismith.Fuzz - ( Fuzz (..) - , FuzzOpts (..) - , fuzz - , fuzzInDir - , fuzzMultiple - , runFuzz - , sampleSeed + ( Fuzz (..), + FuzzOpts (..), + fuzz, + fuzzInDir, + fuzzMultiple, + runFuzz, + sampleSeed, + -- * Helpers - , make - , pop - ) + make, + pop, + ) where -import Control.DeepSeq (force) -import Control.Exception.Lifted (finally) -import Control.Lens hiding ((<.>)) -import Control.Monad (forM, replicateM) -import Control.Monad.IO.Class -import Control.Monad.Reader -import Control.Monad.State.Strict -import Control.Monad.Trans.Control (MonadBaseControl) -import Data.ByteString (ByteString) -import Data.List (nubBy, sort) -import Data.Maybe (catMaybes, fromMaybe, isNothing) -import Data.Text (Text) -import qualified Data.Text as T -import Data.Time -import Data.Tuple (swap) -import Hedgehog (Gen) -import qualified Hedgehog.Internal.Gen as Hog -import Hedgehog.Internal.Seed (Seed) -import qualified Hedgehog.Internal.Seed as Hog -import qualified Hedgehog.Internal.Tree as Hog -import Prelude hiding (FilePath) -import Shelly hiding (get, sub) -import Shelly.Lifted (MonadSh, liftSh, sub) -import System.FilePath.Posix (takeBaseName) -import Verismith.Config -import Verismith.CounterEg (CounterEg (..)) -import Verismith.Internal -import Verismith.Reduce -import Verismith.Report -import Verismith.Result -import Verismith.Tool.Icarus -import Verismith.Tool.Internal -import Verismith.Tool.Yosys -import Verismith.Verilog.AST -import Verismith.Verilog.CodeGen +import Control.DeepSeq (force) +import Control.Exception.Lifted (finally) +import Control.Lens hiding ((<.>)) +import Control.Monad (forM, replicateM) +import Control.Monad.IO.Class +import Control.Monad.Reader +import Control.Monad.State.Strict +import Control.Monad.Trans.Control (MonadBaseControl) +import Data.ByteString (ByteString) +import Data.List (nubBy, sort) +import Data.Maybe (catMaybes, fromMaybe, isNothing) +import Data.Text (Text) +import qualified Data.Text as T +import Data.Time +import Data.Tuple (swap) +import Hedgehog (Gen) +import qualified Hedgehog.Internal.Gen as Hog +import Hedgehog.Internal.Seed (Seed) +import qualified Hedgehog.Internal.Seed as Hog +import qualified Hedgehog.Internal.Tree as Hog +import Shelly hiding (get, sub) +import Shelly.Lifted (MonadSh, liftSh, sub) +import System.FilePath.Posix (takeBaseName) +import Verismith.Config +import Verismith.CounterEg (CounterEg (..)) +import Verismith.Internal +import Verismith.Reduce +import Verismith.Report +import Verismith.Result +import Verismith.Tool.Icarus +import Verismith.Tool.Internal +import Verismith.Tool.Yosys import Verismith.Utils (generateByteString) - -data FuzzOpts = FuzzOpts { _fuzzOptsOutput :: !(Maybe FilePath) - , _fuzzOptsForced :: !Bool - , _fuzzOptsKeepAll :: !Bool - , _fuzzOptsIterations :: {-# UNPACK #-} !Int - , _fuzzOptsNoSim :: !Bool - , _fuzzOptsNoEquiv :: !Bool - , _fuzzOptsNoReduction :: !Bool - , _fuzzOptsConfig :: {-# UNPACK #-} !Config - , _fuzzDataDir :: !FilePath - , _fuzzOptsCrossCheck :: !Bool - , _fuzzOptsChecker :: !(Maybe Text) - } - deriving (Show, Eq) +import Verismith.Verilog.AST +import Verismith.Verilog.CodeGen +import Prelude hiding (FilePath) + +data FuzzOpts + = FuzzOpts + { _fuzzOptsOutput :: !(Maybe FilePath), + _fuzzOptsForced :: !Bool, + _fuzzOptsKeepAll :: !Bool, + _fuzzOptsIterations :: {-# UNPACK #-} !Int, + _fuzzOptsNoSim :: !Bool, + _fuzzOptsNoEquiv :: !Bool, + _fuzzOptsNoReduction :: !Bool, + _fuzzOptsConfig :: {-# UNPACK #-} !Config, + _fuzzDataDir :: !FilePath, + _fuzzOptsCrossCheck :: !Bool, + _fuzzOptsChecker :: !(Maybe Text) + } + deriving (Show, Eq) $(makeLenses ''FuzzOpts) defaultFuzzOpts :: FuzzOpts -defaultFuzzOpts = FuzzOpts { _fuzzOptsOutput = Nothing - , _fuzzOptsForced = False - , _fuzzOptsKeepAll = False - , _fuzzOptsIterations = 1 - , _fuzzOptsNoSim = False - , _fuzzOptsNoEquiv = False - , _fuzzOptsNoReduction = False - , _fuzzOptsConfig = defaultConfig - , _fuzzDataDir = fromText "." - , _fuzzOptsCrossCheck = False - , _fuzzOptsChecker = Nothing - } - -data FuzzEnv = FuzzEnv { _getSynthesisers :: ![SynthTool] - , _getSimulators :: ![SimTool] - , _yosysInstance :: {-# UNPACK #-} !Yosys - , _fuzzEnvOpts :: {-# UNPACK #-} !FuzzOpts - } - deriving (Eq, Show) +defaultFuzzOpts = + FuzzOpts + { _fuzzOptsOutput = Nothing, + _fuzzOptsForced = False, + _fuzzOptsKeepAll = False, + _fuzzOptsIterations = 1, + _fuzzOptsNoSim = False, + _fuzzOptsNoEquiv = False, + _fuzzOptsNoReduction = False, + _fuzzOptsConfig = defaultConfig, + _fuzzDataDir = fromText ".", + _fuzzOptsCrossCheck = False, + _fuzzOptsChecker = Nothing + } + +data FuzzEnv + = FuzzEnv + { _getSynthesisers :: ![SynthTool], + _getSimulators :: ![SimTool], + _yosysInstance :: {-# UNPACK #-} !Yosys, + _fuzzEnvOpts :: {-# UNPACK #-} !FuzzOpts + } + deriving (Eq, Show) $(makeLenses ''FuzzEnv) -data FuzzState = FuzzState { _fuzzSynthResults :: ![SynthResult] - , _fuzzSimResults :: ![SimResult] - , _fuzzSynthStatus :: ![SynthStatus] - } - deriving (Eq, Show) +data FuzzState + = FuzzState + { _fuzzSynthResults :: ![SynthResult], + _fuzzSimResults :: ![SimResult], + _fuzzSynthStatus :: ![SynthStatus] + } + deriving (Eq, Show) $(makeLenses ''FuzzState) @@ -124,16 +131,19 @@ runFuzz :: MonadIO m => FuzzOpts -> Yosys -> Fuzz Sh a -> m a runFuzz fo yos m = shelly $ runFuzz' fo yos m runFuzz' :: Monad m => FuzzOpts -> Yosys -> Fuzz m b -> m b -runFuzz' fo yos m = runReaderT +runFuzz' fo yos m = + runReaderT (evalStateT m (FuzzState [] [] [])) - (FuzzEnv { _getSynthesisers = ( force - $ defaultIdentitySynth - : (descriptionToSynth <$> conf ^. configSynthesisers) - ) - , _getSimulators = (force $ descriptionToSim <$> conf ^. configSimulators) - , _yosysInstance = yos - , _fuzzEnvOpts = fo - } + ( FuzzEnv + { _getSynthesisers = + ( force $ + defaultIdentitySynth + : (descriptionToSynth <$> conf ^. configSynthesisers) + ), + _getSimulators = (force $ descriptionToSim <$> conf ^. configSimulators), + _yosysInstance = yos, + _fuzzEnvOpts = fo + } ) where conf = _fuzzOptsConfig fo @@ -145,42 +155,42 @@ askOpts :: Monad m => Fuzz m FuzzOpts askOpts = asks _fuzzEnvOpts genMethod conf seed gen = - case T.toLower $ conf ^. configProperty . propSampleMethod of - "hat" -> do - logT "Using the hat function" - sv hatFreqs - "mean" -> do - logT "Using the mean function" - sv meanFreqs - "median" -> do - logT "Using the median function" - sv medianFreqs - _ -> do - logT "Using first seed" - sampleSeed seed gen + case T.toLower $ conf ^. configProperty . propSampleMethod of + "hat" -> do + logT "Using the hat function" + sv hatFreqs + "mean" -> do + logT "Using the mean function" + sv meanFreqs + "median" -> do + logT "Using the median function" + sv medianFreqs + _ -> do + logT "Using first seed" + sampleSeed seed gen where sv a = sampleVerilog a (conf ^. configProperty . propSampleSize) seed gen relativeFuzzReport :: (MonadSh m) => FuzzReport -> m FuzzReport relativeFuzzReport fr@(FuzzReport dir _ _ _ _ _ _ _) = liftSh $ do - newPath <- relPath dir - return $ (fuzzDir .~ newPath) fr + newPath <- relPath dir + return $ (fuzzDir .~ newPath) fr filterSynth :: SynthResult -> Bool filterSynth (SynthResult _ _ (Pass _) _) = True -filterSynth _ = False +filterSynth _ = False filterSim :: SimResult -> Bool filterSim (SimResult _ _ _ (Pass _) _) = True -filterSim _ = False +filterSim _ = False filterSynthStat :: SynthStatus -> Bool filterSynthStat (SynthStatus _ (Pass _) _) = True -filterSynthStat _ = False +filterSynthStat _ = False passedFuzz :: FuzzReport -> Bool passedFuzz (FuzzReport _ synth sim synthstat _ _ _ _) = - (passedSynth + passedSim + passedSynthStat) == 0 + (passedSynth + passedSim + passedSynthStat) == 0 where passedSynth = length $ filter (not . filterSynth) synth passedSim = length $ filter (not . filterSim) sim @@ -193,42 +203,42 @@ synthesisers = lift $ asks _getSynthesisers --simulators = lift $ asks getSimulators combinations :: [a] -> [b] -> [(a, b)] -combinations l1 l2 = [ (x, y) | x <- l1, y <- l2 ] +combinations l1 l2 = [(x, y) | x <- l1, y <- l2] logT :: MonadSh m => Text -> m () logT = liftSh . logger timeit :: (MonadIO m, MonadSh m) => m a -> m (NominalDiffTime, a) timeit a = do - start <- liftIO getCurrentTime - result <- a - end <- liftIO getCurrentTime - return (diffUTCTime end start, result) + start <- liftIO getCurrentTime + result <- a + end <- liftIO getCurrentTime + return (diffUTCTime end start, result) synthesis :: (MonadBaseControl IO m, MonadSh m, Show ann) => (SourceInfo ann) -> Fuzz m () synthesis src = do - synth <- synthesisers - resTimes <- liftSh $ mapM exec synth - fuzzSynthStatus - .= applyList (uncurry . SynthStatus <$> synth) (fmap swap resTimes) - liftSh $ inspect resTimes + synth <- synthesisers + resTimes <- liftSh $ mapM exec synth + fuzzSynthStatus + .= applyList (uncurry . SynthStatus <$> synth) (fmap swap resTimes) + liftSh $ inspect resTimes where exec a = toolRun ("synthesis with " <> toText a) . runResultT $ do - liftSh . mkdir_p . fromText $ toText a - pop (fromText $ toText a) $ runSynth a src + liftSh . mkdir_p . fromText $ toText a + pop (fromText $ toText a) $ runSynth a src passedSynthesis :: MonadSh m => Fuzz m [SynthTool] passedSynthesis = fmap toSynth . filter passed . _fuzzSynthStatus <$> get where passed (SynthStatus _ (Pass _) _) = True - passed _ = False + passed _ = False toSynth (SynthStatus s _ _) = s failedSynthesis :: MonadSh m => Fuzz m [SynthTool] failedSynthesis = fmap toSynth . filter failed . _fuzzSynthStatus <$> get where failed (SynthStatus _ (Fail SynthFail) _) = True - failed _ = False + failed _ = False toSynth (SynthStatus s _ _) = s make :: MonadSh m => FilePath -> m () @@ -236,8 +246,8 @@ make f = liftSh $ mkdir_p f pop :: (MonadBaseControl IO m, MonadSh m) => FilePath -> m a -> m a pop f a = do - dir <- liftSh pwd - finally (liftSh (cd f) >> a) . liftSh $ cd dir + dir <- liftSh pwd + finally (liftSh (cd f) >> a) . liftSh $ cd dir applyList :: [a -> b] -> [a] -> [b] applyList a b = apply' <$> zip a b where apply' (a', b') = a' b' @@ -245,156 +255,169 @@ applyList a b = apply' <$> zip a b where apply' (a', b') = a' b' applyLots :: (a -> b -> c -> d -> e) -> [(a, b)] -> [(c, d)] -> [e] applyLots func a b = applyList (uncurry . uncurry func <$> a) b -toSynthResult :: [(SynthTool, SynthTool)] - -> [(NominalDiffTime, Result Failed ())] - -> [SynthResult] +toSynthResult :: + [(SynthTool, SynthTool)] -> + [(NominalDiffTime, Result Failed ())] -> + [SynthResult] toSynthResult a b = applyLots SynthResult a $ fmap swap b -toSimResult :: SimTool - -> [ByteString] - -> [SynthTool] - -> [(NominalDiffTime, Result Failed ByteString)] - -> [SimResult] +toSimResult :: + SimTool -> + [ByteString] -> + [SynthTool] -> + [(NominalDiffTime, Result Failed ByteString)] -> + [SimResult] toSimResult sima bs as b = - applyList (applyList (repeat uncurry) - (applyList (applyList (SimResult <$> as) (repeat sima)) (repeat bs))) + applyList + ( applyList + (repeat uncurry) + (applyList (applyList (SimResult <$> as) (repeat sima)) (repeat bs)) + ) $ fmap swap b toolRun :: (MonadIO m, MonadSh m, Show a) => Text -> m a -> m (NominalDiffTime, a) toolRun t m = do - logT $ "Running " <> t - s <- timeit m - logT $ "Finished " <> t <> " " <> showT s - return s + logT $ "Running " <> t + s <- timeit m + logT $ "Finished " <> t <> " " <> showT s + return s equivalence :: (MonadBaseControl IO m, MonadSh m, Show ann) => (SourceInfo ann) -> Fuzz m () equivalence src = do - doCrossCheck <- fmap _fuzzOptsCrossCheck askOpts - datadir <- fmap _fuzzDataDir askOpts - checker <- fmap _fuzzOptsChecker askOpts - synth <- passedSynthesis - conf <- fmap _fuzzOptsConfig askOpts - let synthComb = - if doCrossCheck - then nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth - else nubBy tupEq . filter (uncurry (/=)) $ (,) defaultIdentitySynth <$> synth - resTimes <- liftSh $ mapM (uncurry (equiv (conf ^. configProperty . propDefaultYosys) checker datadir)) synthComb - fuzzSynthResults .= toSynthResult synthComb resTimes - liftSh $ inspect resTimes + doCrossCheck <- fmap _fuzzOptsCrossCheck askOpts + datadir <- fmap _fuzzDataDir askOpts + checker <- fmap _fuzzOptsChecker askOpts + synth <- passedSynthesis + conf <- fmap _fuzzOptsConfig askOpts + let synthComb = + if doCrossCheck + then nubBy tupEq . filter (uncurry (/=)) $ combinations synth synth + else nubBy tupEq . filter (uncurry (/=)) $ (,) defaultIdentitySynth <$> synth + resTimes <- liftSh $ mapM (uncurry (equiv (conf ^. configProperty . propDefaultYosys) checker datadir)) synthComb + fuzzSynthResults .= toSynthResult synthComb resTimes + liftSh $ inspect resTimes where tupEq (a, b) (a', b') = (a == a' && b == b') || (a == b' && b == a') equiv yosysloc checker datadir a b = - toolRun ("equivalence check for " <> toText a <> " and " <> toText b) - . runResultT - $ do make dir - pop dir $ do - liftSh $ do - cp ( fromText ".." - </> fromText (toText a) - </> synthOutput a - ) $ synthOutput a - cp ( fromText ".." - </> fromText (toText b) - </> synthOutput b - ) $ synthOutput b - writefile "rtl.v" $ genSource src - sub $ do - maybe (return ()) (liftSh . prependToPath . fromText) yosysloc - runEquiv checker datadir a b src - where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b + toolRun ("equivalence check for " <> toText a <> " and " <> toText b) + . runResultT + $ do + make dir + pop dir $ do + liftSh $ do + cp + ( fromText ".." + </> fromText (toText a) + </> synthOutput a + ) + $ synthOutput a + cp + ( fromText ".." + </> fromText (toText b) + </> synthOutput b + ) + $ synthOutput b + writefile "rtl.v" $ genSource src + sub $ do + maybe (return ()) (liftSh . prependToPath . fromText) yosysloc + runEquiv checker datadir a b src + where + dir = fromText $ "equiv_" <> toText a <> "_" <> toText b simulation :: (MonadIO m, MonadSh m, Show ann) => (SourceInfo ann) -> Fuzz m () simulation src = do - datadir <- fmap _fuzzDataDir askOpts - synth <- passedSynthesis - counterEgs <- failEquivWithIdentityCE - vals <- liftIO $ generateByteString Nothing 32 20 - ident <- liftSh $ sim datadir vals Nothing defaultIdentitySynth - resTimes <- liftSh $ mapM (sim datadir vals (justPass $ snd ident)) synth - resTimes2 <- liftSh $ mapM (simCounterEg datadir) counterEgs - fuzzSimResults .= toSimResult defaultIcarusSim vals synth resTimes - liftSh - . inspect - $ (\(_, r) -> bimap show (T.unpack . T.take 10 . showBS) r) - <$> (ident : resTimes) + datadir <- fmap _fuzzDataDir askOpts + synth <- passedSynthesis + counterEgs <- failEquivWithIdentityCE + vals <- liftIO $ generateByteString Nothing 32 20 + ident <- liftSh $ sim datadir vals Nothing defaultIdentitySynth + resTimes <- liftSh $ mapM (sim datadir vals (justPass $ snd ident)) synth + resTimes2 <- liftSh $ mapM (simCounterEg datadir) counterEgs + fuzzSimResults .= toSimResult defaultIcarusSim vals synth resTimes + liftSh + . inspect + $ (\(_, r) -> bimap show (T.unpack . T.take 10 . showBS) r) + <$> (ident : resTimes) where sim datadir b i a = toolRun ("simulation for " <> toText a) . runResultT $ do - make dir - pop dir $ do - liftSh $ do - cp (fromText ".." </> fromText (toText a) </> synthOutput a) - $ synthOutput a - writefile "rtl.v" $ genSource src - runSimIc datadir defaultIcarus a src b i - where dir = fromText $ "simulation_" <> toText a + make dir + pop dir $ do + liftSh $ do + cp (fromText ".." </> fromText (toText a) </> synthOutput a) $ + synthOutput a + writefile "rtl.v" $ genSource src + runSimIc datadir defaultIcarus a src b i + where + dir = fromText $ "simulation_" <> toText a simCounterEg datadir (a, Nothing) = toolRun ("counter-example simulation for " <> toText a) . return $ Fail EmptyFail simCounterEg datadir (a, Just b) = toolRun ("counter-example simulation for " <> toText a) . runResultT $ do - make dir - pop dir $ do - liftSh $ do - cp (fromText ".." </> fromText (toText a) </> synthOutput a) $ synthOutput a - writefile "syn_identity.v" $ genSource src - ident <- runSimIcEC datadir defaultIcarus defaultIdentitySynth src b Nothing - runSimIcEC datadir defaultIcarus a src b (Just ident) - where dir = fromText $ "countereg_sim_" <> toText a + make dir + pop dir $ do + liftSh $ do + cp (fromText ".." </> fromText (toText a) </> synthOutput a) $ synthOutput a + writefile "syn_identity.v" $ genSource src + ident <- runSimIcEC datadir defaultIcarus defaultIdentitySynth src b Nothing + runSimIcEC datadir defaultIcarus a src b (Just ident) + where + dir = fromText $ "countereg_sim_" <> toText a failEquivWithIdentity :: (MonadSh m) => Fuzz m [SynthResult] failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get where withIdentity (SynthResult (IdentitySynth _) _ (Fail (EquivFail _)) _) = True withIdentity (SynthResult _ (IdentitySynth _) (Fail (EquivFail _)) _) = True - withIdentity _ = False + withIdentity _ = False failEquivWithIdentityCE :: (MonadSh m) => Fuzz m [(SynthTool, Maybe CounterEg)] failEquivWithIdentityCE = catMaybes . fmap withIdentity . _fuzzSynthResults <$> get where withIdentity (SynthResult (IdentitySynth _) s (Fail (EquivFail c)) _) = Just (s, c) withIdentity (SynthResult s (IdentitySynth _) (Fail (EquivFail c)) _) = Just (s, c) - withIdentity _ = Nothing + withIdentity _ = Nothing failedSimulations :: (MonadSh m) => Fuzz m [SimResult] failedSimulations = filter failedSim . _fuzzSimResults <$> get where failedSim (SimResult _ _ _ (Fail (SimFail _)) _) = True - failedSim _ = False + failedSim _ = False passEquiv :: (MonadSh m) => Fuzz m [SynthResult] passEquiv = filter withIdentity . _fuzzSynthResults <$> get where withIdentity (SynthResult _ _ (Pass _) _) = True - withIdentity _ = False + withIdentity _ = False -- | Always reduces with respect to 'Identity'. reduction :: (MonadSh m) => SourceInfo ann -> Fuzz m () reduction rsrc = do - datadir <- fmap _fuzzDataDir askOpts - checker <- fmap _fuzzOptsChecker askOpts - fails <- failEquivWithIdentity - synthFails <- failedSynthesis - simFails <- failedSimulations - _ <- liftSh $ mapM (red checker datadir) fails - _ <- liftSh $ mapM redSynth synthFails - _ <- liftSh $ mapM (redSim datadir) simFails - return () + datadir <- fmap _fuzzDataDir askOpts + checker <- fmap _fuzzOptsChecker askOpts + fails <- failEquivWithIdentity + synthFails <- failedSynthesis + simFails <- failedSimulations + _ <- liftSh $ mapM (red checker datadir) fails + _ <- liftSh $ mapM redSynth synthFails + _ <- liftSh $ mapM (redSim datadir) simFails + return () where red checker datadir (SynthResult a b _ _) = do - r <- reduceSynth checker datadir a b src - writefile (fromText $ "reduce_" <> toText a <> "_" <> toText b <> ".v") $ genSource r + r <- reduceSynth checker datadir a b src + writefile (fromText $ "reduce_" <> toText a <> "_" <> toText b <> ".v") $ genSource r redSynth a = do - r <- reduceSynthesis a src - writefile (fromText $ "reduce_" <> toText a <> ".v") $ genSource r + r <- reduceSynthesis a src + writefile (fromText $ "reduce_" <> toText a <> ".v") $ genSource r redSim datadir (SimResult t _ bs _ _) = do - r <- reduceSimIc datadir bs t src - writefile (fromText $ "reduce_sim_" <> toText t <> ".v") $ genSource r + r <- reduceSimIc datadir bs t src + writefile (fromText $ "reduce_sim_" <> toText t <> ".v") $ genSource r src = clearAnn rsrc -titleRun - :: (MonadIO m, MonadSh m) => Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a) +titleRun :: + (MonadIO m, MonadSh m) => Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a) titleRun t f = do - logT $ "### Starting " <> t <> " ###" - (diff, res) <- timeit f - logT $ "### Finished " <> t <> " (" <> showT diff <> ") ###" - return (diff, res) + logT $ "### Starting " <> t <> " ###" + (diff, res) <- timeit f + logT $ "### Finished " <> t <> " (" <> showT diff <> ") ###" + return (diff, res) whenMaybe :: Applicative m => Bool -> m a -> m (Maybe a) whenMaybe b x = if b then Just <$> x else pure Nothing @@ -402,39 +425,40 @@ whenMaybe b x = if b then Just <$> x else pure Nothing getTime :: (Num n) => Maybe (n, a) -> n getTime = maybe 0 fst -generateSample - :: (MonadIO m, MonadSh m, Show ann) - => Fuzz m (Seed, (SourceInfo ann)) - -> Fuzz m (Seed, (SourceInfo ann)) +generateSample :: + (MonadIO m, MonadSh m, Show ann) => + Fuzz m (Seed, (SourceInfo ann)) -> + Fuzz m (Seed, (SourceInfo ann)) generateSample f = do - logT "Sampling Verilog from generator" - (t, v@(s, _)) <- timeit f - logT $ "Chose " <> showT s - logT $ "Generated Verilog (" <> showT t <> ")" - return v + logT "Sampling Verilog from generator" + (t, v@(s, _)) <- timeit f + logT $ "Chose " <> showT s + logT $ "Generated Verilog (" <> showT t <> ")" + return v verilogSize :: (Source a) => a -> Int verilogSize = length . lines . T.unpack . genSource -sampleVerilog - :: (MonadSh m, MonadIO m, Source a, Ord a) - => Frequency a - -> Int - -> Maybe Seed - -> Gen a - -> m (Seed, a) -sampleVerilog _ _ seed@(Just _) gen = sampleSeed seed gen -sampleVerilog freq n Nothing gen = do - res <- replicateM n $ sampleSeed Nothing gen - let sizes = fmap getSize res - let samples = fmap snd . sort $ zip sizes res - liftIO $ Hog.sample . Hog.frequency $ freq samples - where getSize (_, s) = verilogSize s +sampleVerilog :: + (MonadSh m, MonadIO m, Source a, Ord a) => + Frequency a -> + Int -> + Maybe Seed -> + Gen a -> + m (Seed, a) +sampleVerilog _ _ seed@(Just _) gen = sampleSeed seed gen +sampleVerilog freq n Nothing gen = do + res <- replicateM n $ sampleSeed Nothing gen + let sizes = fmap getSize res + let samples = fmap snd . sort $ zip sizes res + liftIO $ Hog.sample . Hog.frequency $ freq samples + where + getSize (_, s) = verilogSize s hatFreqs :: Frequency a hatFreqs l = zip hat (return <$> l) where - h = length l `div` 2 + h = length l `div` 2 hat = (+ h) . negate . abs . (h -) <$> [1 .. length l] meanFreqs :: Source a => Frequency a @@ -442,115 +466,127 @@ meanFreqs l = zip hat (return <$> l) where hat = calc <$> sizes calc i = if abs (mean - i) == min_ then 1 else 0 - mean = sum sizes `div` length l - min_ = minimum $ abs . (mean -) <$> sizes + mean = sum sizes `div` length l + min_ = minimum $ abs . (mean -) <$> sizes sizes = verilogSize . snd <$> l medianFreqs :: Frequency a medianFreqs l = zip hat (return <$> l) where - h = length l `div` 2 + h = length l `div` 2 hat = set_ <$> [1 .. length l] set_ n = if n == h then 1 else 0 fuzz :: (MonadFuzz m, Ord ann, Show ann) => Gen (SourceInfo ann) -> Fuzz m FuzzReport fuzz gen = do - conf <- askConfig - opts <- askOpts - let seed = conf ^. configProperty . propSeed - (seed', src) <- generateSample $ genMethod conf seed gen - let size = length . lines . T.unpack $ genSource src - liftSh - . writefile "config.toml" - . encodeConfig - $ conf - & configProperty - . propSeed - ?~ seed' - (tsynth, _) <- titleRun "Synthesis" $ synthesis src - (tequiv, _) <- if (_fuzzOptsNoEquiv opts) - then return (0, mempty) - else titleRun "Equivalence Check" $ equivalence src - (_ , _) <- if (_fuzzOptsNoSim opts) - then return (0, mempty) - else titleRun "Simulation" $ simulation src - fails <- failEquivWithIdentity - failedSim <- failedSimulations - synthFails <- failedSynthesis - redResult <- - whenMaybe (not (null failedSim && null fails && null synthFails) - && not (_fuzzOptsNoReduction opts)) - . titleRun "Reduction" - $ reduction src - state_ <- get - currdir <- liftSh pwd - let vi = flip view state_ - let report = FuzzReport currdir - (vi fuzzSynthResults) - (vi fuzzSimResults) - (vi fuzzSynthStatus) - size - tsynth - tequiv - (getTime redResult) - return report + conf <- askConfig + opts <- askOpts + let seed = conf ^. configProperty . propSeed + (seed', src) <- generateSample $ genMethod conf seed gen + let size = length . lines . T.unpack $ genSource src + liftSh + . writefile "config.toml" + . encodeConfig + $ conf + & configProperty + . propSeed + ?~ seed' + (tsynth, _) <- titleRun "Synthesis" $ synthesis src + (tequiv, _) <- + if (_fuzzOptsNoEquiv opts) + then return (0, mempty) + else titleRun "Equivalence Check" $ equivalence src + (_, _) <- + if (_fuzzOptsNoSim opts) + then return (0, mempty) + else titleRun "Simulation" $ simulation src + fails <- failEquivWithIdentity + failedSim <- failedSimulations + synthFails <- failedSynthesis + redResult <- + whenMaybe + ( not (null failedSim && null fails && null synthFails) + && not (_fuzzOptsNoReduction opts) + ) + . titleRun "Reduction" + $ reduction src + state_ <- get + currdir <- liftSh pwd + let vi = flip view state_ + let report = + FuzzReport + currdir + (vi fuzzSynthResults) + (vi fuzzSimResults) + (vi fuzzSynthStatus) + size + tsynth + tequiv + (getTime redResult) + return report fuzzInDir :: (MonadFuzz m, Ord ann, Show ann) => Gen (SourceInfo ann) -> Fuzz m FuzzReport fuzzInDir src = do - fuzzOpts <- askOpts - let fp = fromMaybe "fuzz" $ _fuzzOptsOutput fuzzOpts - make fp - res <- pop fp $ fuzz src - liftSh $ do - writefile (fp <.> "html") $ printResultReport (bname fp) res - when (passedFuzz res && not (_fuzzOptsKeepAll fuzzOpts)) $ rm_rf fp - relativeFuzzReport res + fuzzOpts <- askOpts + let fp = fromMaybe "fuzz" $ _fuzzOptsOutput fuzzOpts + make fp + res <- pop fp $ fuzz src + liftSh $ do + writefile (fp <.> "html") $ printResultReport (bname fp) res + when (passedFuzz res && not (_fuzzOptsKeepAll fuzzOpts)) $ rm_rf fp + relativeFuzzReport res where bname = T.pack . takeBaseName . T.unpack . toTextIgnore -fuzzMultiple - :: (MonadFuzz m, Ord ann, Show ann) - => Gen (SourceInfo ann) - -> Fuzz m [FuzzReport] +fuzzMultiple :: + (MonadFuzz m, Ord ann, Show ann) => + Gen (SourceInfo ann) -> + Fuzz m [FuzzReport] fuzzMultiple src = do - fuzzOpts <- askOpts - let seed = (_fuzzOptsConfig fuzzOpts) ^. configProperty . propSeed - x <- case _fuzzOptsOutput fuzzOpts of - Nothing -> do - ct <- liftIO getZonedTime - return - . fromText - . T.pack - $ "output_" - <> formatTime defaultTimeLocale "%Y-%m-%d_%H-%M-%S" ct - Just f -> return f - make x - pop x $ do - results <- if isNothing seed - then forM [1 .. (_fuzzOptsIterations fuzzOpts)] fuzzDir' - else (: []) <$> fuzzDir' (1 :: Int) - liftSh . writefile (fromText "index" <.> "html") $ printSummary - "Fuzz Summary" - results - return results + fuzzOpts <- askOpts + let seed = (_fuzzOptsConfig fuzzOpts) ^. configProperty . propSeed + x <- case _fuzzOptsOutput fuzzOpts of + Nothing -> do + ct <- liftIO getZonedTime + return + . fromText + . T.pack + $ "output_" + <> formatTime defaultTimeLocale "%Y-%m-%d_%H-%M-%S" ct + Just f -> return f + make x + pop x $ do + results <- + if isNothing seed + then forM [1 .. (_fuzzOptsIterations fuzzOpts)] fuzzDir' + else (: []) <$> fuzzDir' (1 :: Int) + liftSh . writefile (fromText "index" <.> "html") $ + printSummary + "Fuzz Summary" + results + return results where fuzzDir' :: (Show a, MonadFuzz m) => a -> Fuzz m FuzzReport - fuzzDir' n' = local (fuzzEnvOpts . fuzzOptsOutput .~ - (Just . fromText $ "fuzz_" <> showT n')) - $ fuzzInDir src + fuzzDir' n' = + local + ( fuzzEnvOpts . fuzzOptsOutput + .~ (Just . fromText $ "fuzz_" <> showT n') + ) + $ fuzzInDir src sampleSeed :: MonadSh m => Maybe Seed -> Gen a -> m (Seed, a) sampleSeed s gen = - liftSh - $ let loop n = if n <= 0 - then - error - "Hedgehog.Gen.sample: too many discards, could not generate a sample" - else do - seed <- maybe Hog.random return s - case Hog.evalGen 30 seed gen of - Nothing -> - loop (n - 1) - Just x -> - pure (seed, Hog.treeValue x) - in loop (100 :: Int) + liftSh $ + let loop n = + if n <= 0 + then + error + "Hedgehog.Gen.sample: too many discards, could not generate a sample" + else do + seed <- maybe Hog.random return s + case Hog.evalGen 30 seed gen of + Nothing -> + loop (n - 1) + Just x -> + pure (seed, Hog.treeValue x) + in loop (100 :: Int) |