diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-05-12 13:16:15 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-12 13:16:15 +0100 |
commit | bc2fd5f80e235a1bd00c58e29554aea91afcf4d8 (patch) | |
tree | b85ba6c8d5ffc6f49350b9d11753ca7076db8510 | |
parent | 7124a4f00e536b4d5323a7488c1f65469dddb102 (diff) | |
download | verismith-bc2fd5f80e235a1bd00c58e29554aea91afcf4d8.tar.gz verismith-bc2fd5f80e235a1bd00c58e29554aea91afcf4d8.zip |
Add debug to reduction
-rw-r--r-- | src/Verismith/Fuzz.hs | 4 | ||||
-rw-r--r-- | src/Verismith/Reduce.hs | 14 |
2 files changed, 14 insertions, 4 deletions
diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs index 2fb9f00..278879d 100644 --- a/src/Verismith/Fuzz.hs +++ b/src/Verismith/Fuzz.hs @@ -397,7 +397,7 @@ reduction rsrc = do simFails <- failedSimulations _ <- liftSh $ mapM (red checker datadir) fails _ <- liftSh $ mapM redSynth synthFails - _ <- liftSh $ mapM (redSim datadir) simFails + -- _ <- liftSh $ mapM (redSim datadir) simFails return () where red checker datadir (SynthResult a b _ _) = do @@ -490,7 +490,7 @@ fuzz gen = do $ conf & configProperty . propSeed - ?~ seed' + ?~ seed' (tsynth, _) <- titleRun "Synthesis" $ synthesis src (tequiv, _) <- if (_fuzzOptsNoEquiv opts) diff --git a/src/Verismith/Reduce.hs b/src/Verismith/Reduce.hs index 8a5bbbd..956722e 100644 --- a/src/Verismith/Reduce.hs +++ b/src/Verismith/Reduce.hs @@ -44,6 +44,7 @@ import Control.Monad (void) import Control.Monad.IO.Class (MonadIO, liftIO) import Data.ByteString (ByteString) import Data.Foldable (foldrM) +import Data.IORef (newIORef, readIORef, writeIORef) import Data.List (nub) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NonEmpty @@ -681,16 +682,25 @@ reduceSynth :: b -> (SourceInfo ()) -> m (SourceInfo ()) -reduceSynth mt datadir a b = reduce (fromText $ "reduce_" <> toText a <> "_" <> toText b <> ".v") synth +reduceSynth mt datadir a b src = do + counter <- liftSh . liftIO $ newIORef (0 :: Int) + reduce (fromText $ prefix <> ".v") (synth counter) src where - synth src' = liftSh $ do + synth counter src' = liftSh $ do + count <- liftIO $ readIORef counter + liftIO $ writeIORef counter (count + 1) + Shelly.mkdir (fromText $ prefix <> "_" <> showT count) + current_dir <- Shelly.pwd + Shelly.cd (fromText $ prefix <> "_" <> showT count) r <- runResultT $ do runSynth a src' runSynth b src' runEquiv mt datadir a b src' + Shelly.cd current_dir return $ case r of Fail (EquivFail _) -> True _ -> False + prefix = "reduce_" <> toText a <> "_" <> toText b reduceSynthesis :: (Synthesiser a, MonadSh m) => a -> SourceInfo () -> m (SourceInfo ()) reduceSynthesis a = reduce (fromText $ "reduce_" <> toText a <> ".v") synth |