aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-05-12 13:16:15 +0100
committerYann Herklotz <git@yannherklotz.com>2020-05-12 13:16:15 +0100
commitbc2fd5f80e235a1bd00c58e29554aea91afcf4d8 (patch)
treeb85ba6c8d5ffc6f49350b9d11753ca7076db8510
parent7124a4f00e536b4d5323a7488c1f65469dddb102 (diff)
downloadverismith-bc2fd5f80e235a1bd00c58e29554aea91afcf4d8.tar.gz
verismith-bc2fd5f80e235a1bd00c58e29554aea91afcf4d8.zip
Add debug to reduction
-rw-r--r--src/Verismith/Fuzz.hs4
-rw-r--r--src/Verismith/Reduce.hs14
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