From c31961da322d9700fd6604541cbce5a4042f9b24 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 5 May 2019 16:54:27 +0100 Subject: Add seeds for reproducible runs --- app/Main.hs | 4 +-- src/VeriFuzz.hs | 44 +++++++++++++++++------------ src/VeriFuzz/Config.hs | 20 ++++++++------ src/VeriFuzz/Fuzz.hs | 61 ++++++++++++++++++++++++++++++----------- src/VeriFuzz/Verilog/CodeGen.hs | 2 +- 5 files changed, 85 insertions(+), 46 deletions(-) diff --git a/app/Main.hs b/app/Main.hs index 277533c..18173ba 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -209,8 +209,8 @@ handleOpts :: Opts -> IO () handleOpts (Fuzz out configF _ _ n) = do config <- getConfig configF _ <- V.runFuzz config - V.defaultYosys - (V.fuzzMultiple n Nothing (V.proceduralSrc "top" config)) + V.defaultYosys + (V.fuzzMultiple n Nothing (V.proceduralSrc "top" config)) return () handleOpts (Generate f c) = do config <- getConfig c diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs index f2fb90b..489ac01 100644 --- a/src/VeriFuzz.hs +++ b/src/VeriFuzz.hs @@ -24,21 +24,28 @@ module VeriFuzz where import Control.Lens -import qualified Crypto.Random.DRBG as C -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.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 Prelude hiding (FilePath) +import Control.Monad.IO.Class (MonadIO) +import Control.Monad.Trans.Maybe (runMaybeT) +import qualified Crypto.Random.DRBG as C +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 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 -import Shelly.Lifted (liftSh) +import Shelly.Lifted (liftSh) import VeriFuzz.Circuit import VeriFuzz.Config import VeriFuzz.Fuzz @@ -128,14 +135,15 @@ checkEquivalence src dir = shellyFailDir $ do -- | Run a fuzz run and check if all of the simulators passed by checking if the -- generated Verilog files are equivalent. runEquivalence - :: Gen Verilog -- ^ Generator for the Verilog file. + :: 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 gm t d k i = do - m <- Hog.sample gm +runEquivalence seed gm t d k i = do + m <- sampleSeed seed gm let srcInfo = SourceInfo "top" m rand <- generateByteString 20 shellyFailDir $ do @@ -162,7 +170,7 @@ runEquivalence gm t d k i = do $ onFailure n cd ".." unless k . rm_rf $ fromText n - when (i < 5) (runEquivalence gm t d k $ i + 1) + when (i < 5 && isNothing seed) (runEquivalence seed gm t d k $ i + 1) where n = t <> "_" <> T.pack (show i) runReduce :: SourceInfo -> IO SourceInfo diff --git a/src/VeriFuzz/Config.hs b/src/VeriFuzz/Config.hs index 8a3d422..9961667 100644 --- a/src/VeriFuzz/Config.hs +++ b/src/VeriFuzz/Config.hs @@ -74,13 +74,15 @@ module VeriFuzz.Config ) where -import Control.Applicative (Alternative, (<|>)) -import Control.Lens hiding ((.=)) -import Data.List.NonEmpty (NonEmpty (..)) -import Data.Maybe (fromMaybe) -import Data.Text (Text) -import qualified Data.Text.IO as T -import Toml (TomlCodec, (.=)) +import Control.Applicative (Alternative, (<|>)) +import Control.Lens hiding ((.=)) +import Data.List.NonEmpty (NonEmpty (..)) +import Data.Maybe (fromMaybe) +import Data.Text (Text) +import qualified Data.Text.IO as T +import Hedgehog.Internal.Seed (Seed) +import qualified Hedgehog.Internal.Seed as Seed +import Toml (TomlCodec, (.=)) import qualified Toml -- $conf @@ -224,7 +226,7 @@ data Probability = Probability { _probModItem :: {-# UNPACK #-} !ProbModItem deriving (Eq, Show) data Property = Property { _propSize :: {-# UNPACK #-} !Int - , _propSeed :: !(Maybe Int) + , _propSeed :: !(Maybe Seed) , _propStmntDepth :: {-# UNPACK #-} !Int , _propModDepth :: {-# UNPACK #-} !Int , _propMaxModules :: {-# UNPACK #-} !Int @@ -363,7 +365,7 @@ propCodec = Property <$> defaultValue (defProp propSize) (Toml.int "size") .= _propSize - <*> Toml.dioptional (Toml.int "seed") + <*> Toml.dioptional (Toml.read "seed") .= _propSeed <*> defaultValue (defProp propStmntDepth) (int "statement" "depth") .= _propStmntDepth diff --git a/src/VeriFuzz/Fuzz.hs b/src/VeriFuzz/Fuzz.hs index c0e6117..52e7e61 100644 --- a/src/VeriFuzz/Fuzz.hs +++ b/src/VeriFuzz/Fuzz.hs @@ -20,6 +20,7 @@ module VeriFuzz.Fuzz , fuzzInDir , fuzzMultiple , runFuzz + , sampleSeed ) where @@ -29,15 +30,23 @@ import Control.Monad (forM, void) import Control.Monad.IO.Class import Control.Monad.Trans.Class (lift) import Control.Monad.Trans.Control (MonadBaseControl) +import Control.Monad.Trans.Maybe (runMaybeT) import Control.Monad.Trans.Reader hiding (local) import Control.Monad.Trans.State.Strict import Data.ByteString (ByteString) import Data.List (nubBy) +import Data.Maybe (isNothing) import Data.Text (Text) import qualified Data.Text as T import Data.Time import Hedgehog (Gen) +import Hedgehog (Gen) +import qualified Hedgehog.Gen as Hog import qualified Hedgehog.Gen as Hog +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) import Shelly.Lifted (MonadSh, liftSh) @@ -66,12 +75,12 @@ type Fuzz m = StateT FuzzReport (ReaderT FuzzEnv m) type MonadFuzz m = (MonadBaseControl IO m, MonadIO m, MonadSh m) -runFuzz :: MonadIO m => Config -> Yosys -> Fuzz Sh a -> m a +runFuzz :: MonadIO m => Config -> Yosys -> (Maybe Seed -> Fuzz Sh a) -> m a runFuzz conf yos m = shelly $ runFuzz' conf yos m -runFuzz' :: Monad m => Config -> Yosys -> Fuzz m b -> m b +runFuzz' :: Monad m => Config -> Yosys -> (Maybe Seed -> Fuzz m b) -> m b runFuzz' conf yos m = runReaderT - (evalStateT m (FuzzReport [] [] [])) + (evalStateT (m (conf ^. configProperty . propSeed)) (FuzzReport [] [] [])) (FuzzEnv (descriptionToSynth <$> conf ^. configSynthesisers) (descriptionToSim <$> conf ^. configSimulators) yos @@ -107,10 +116,10 @@ synthesis src = do liftSh . mkdir_p . fromText $ toText a pop (fromText $ toText a) $ runSynth a src -generateSample :: (MonadIO m, MonadSh m) => Gen SourceInfo -> Fuzz m SourceInfo -generateSample gen = do +generateSample :: (MonadIO m, MonadSh m) => Maybe Seed -> Gen SourceInfo -> Fuzz m SourceInfo +generateSample seed gen = do logT "Sampling Verilog from generator" - (t, src) <- timeit $ Hog.sample gen + (t, src) <- timeit $ sampleSeed seed gen logT $ "Generated Verilog (" <> showT t <> ")" return src @@ -153,25 +162,26 @@ equivalence src = do runEquiv yos a (Just b) src where dir = fromText $ "equiv_" <> toText a <> "_" <> toText b -fuzz :: MonadFuzz m => Gen SourceInfo -> Fuzz m FuzzReport -fuzz gen = do - src <- generateSample gen +fuzz :: MonadFuzz m => Gen SourceInfo -> Maybe Seed -> Fuzz m FuzzReport +fuzz gen seed = do + src <- generateSample seed gen synthesis src equivalence src return mempty -fuzzInDir :: MonadFuzz m => FilePath -> Gen SourceInfo -> Fuzz m FuzzReport -fuzzInDir fp src = do +fuzzInDir :: MonadFuzz m => FilePath -> Gen SourceInfo -> Maybe Seed -> Fuzz m FuzzReport +fuzzInDir fp src seed = do make fp - pop fp $ fuzz src + pop fp $ fuzz src seed fuzzMultiple :: MonadFuzz m => Int - -> (Maybe FilePath) + -> Maybe FilePath -> Gen SourceInfo + -> Maybe Seed -> Fuzz m FuzzReport -fuzzMultiple n fp src = do +fuzzMultiple n fp src seed = do x <- case fp of Nothing -> do ct <- liftIO getZonedTime @@ -182,6 +192,25 @@ fuzzMultiple n fp src = do <> formatTime defaultTimeLocale "%Y-%m-%d_%H-%M-%S" ct Just f -> return f make x - void . pop x $ forM [1 .. n] fuzzDir + when (isNothing seed) . void . pop x . forM [1 .. n] $ fuzzDir + unless (isNothing seed) . void . pop x $ fuzzDir (1 :: Int) return mempty - where fuzzDir n' = fuzzInDir (fromText $ "fuzz_" <> showT n') src + where fuzzDir n' = fuzzInDir (fromText $ "fuzz_" <> showT n') src seed + +sampleSeed :: MonadIO m => Maybe Seed -> Gen a -> m a +sampleSeed s gen = + liftIO $ + 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 runIdentity . runMaybeT . Hog.runTree $ Hog.runGenT 30 seed gen of + Nothing -> + loop (n - 1) + Just x -> do + liftIO . putStrLn $ "VeriFuzz: Chosen seed was '" <> show seed <> "'" + pure $ Hog.nodeValue x + in + loop (100 :: Int) diff --git a/src/VeriFuzz/Verilog/CodeGen.hs b/src/VeriFuzz/Verilog/CodeGen.hs index 2cd2b13..af255a2 100644 --- a/src/VeriFuzz/Verilog/CodeGen.hs +++ b/src/VeriFuzz/Verilog/CodeGen.hs @@ -138,7 +138,7 @@ expr (BinOp eRhs bin eLhs) = "(" <> expr eRhs <> binaryOp bin <> expr eLhs <> ")" expr (Number b ) = showNum b expr (Id i ) = getIdentifier i -expr (VecSelect i e) = getIdentifier i <> "[" <> genExpr e <> "]" +expr (VecSelect i e) = getIdentifier i <> "[" <> expr e <> "]" expr (RangeSelect i r) = getIdentifier i <> range r expr (Concat c ) = "{" <> comma (expr <$> c) <> "}" expr (UnOp u e ) = "(" <> unaryOp u <> expr e <> ")" -- cgit