From 740d61ce91cca8666175d0559345cbcac7690ac6 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 24 Nov 2019 14:55:47 +0000 Subject: Add output of v file during reduction --- src/Verismith/Fuzz.hs | 26 ++++---------------------- src/Verismith/Reduce.hs | 29 ++++++++++++++++------------- 2 files changed, 20 insertions(+), 35 deletions(-) diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs index 82507a8..2db0b7b 100644 --- a/src/Verismith/Fuzz.hs +++ b/src/Verismith/Fuzz.hs @@ -262,7 +262,7 @@ toolRun :: (MonadIO m, MonadSh m, Show a) => Text -> m a -> m (NominalDiffTime, toolRun t m = do logT $ "Running " <> t s <- timeit m - logT $ "Finished " <> t <> " (" <> showT s <> ")" + logT $ "Finished " <> t <> " " <> showT s return s equivalence :: (MonadBaseControl IO m, MonadSh m) => SourceInfo -> Fuzz m () @@ -382,27 +382,9 @@ reduction src = do _ <- liftSh $ mapM (redSim datadir) simFails return () where - red datadir (SynthResult a b _ _) = do - make dir - pop dir $ do - s <- reduceSynth datadir a b src - writefile (fromText ".." dir <.> "v") $ genSource s - return s - where dir = fromText $ "reduce_" <> toText a <> "_" <> toText b - redSynth a = do - make dir - pop dir $ do - s <- reduceSynthesis a src - writefile (fromText ".." dir <.> "v") $ genSource s - return s - where dir = fromText $ "reduce_" <> toText a - redSim datadir (SimResult t _ bs _ _) = do - make dir - pop dir $ do - s <- reduceSimIc datadir bs t src - writefile (fromText ".." dir <.> "v") $ genSource s - return s - where dir = fromText $ "reduce_sim_" <> toText t + red datadir (SynthResult a b _ _) = reduceSynth datadir a b src + redSynth a = reduceSynthesis a src + redSim datadir (SimResult t _ bs _ _) = reduceSimIc datadir bs t src titleRun :: (MonadIO m, MonadSh m) => Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a) diff --git a/src/Verismith/Reduce.hs b/src/Verismith/Reduce.hs index e7614e6..f6e55dc 100644 --- a/src/Verismith/Reduce.hs +++ b/src/Verismith/Reduce.hs @@ -48,9 +48,9 @@ import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NonEmpty import Data.Maybe (mapMaybe) import Data.Text (Text) -import Shelly ((<.>)) +import Shelly (fromText, (<.>)) import qualified Shelly -import Shelly.Lifted (MonadSh, liftSh, rm_rf) +import Shelly.Lifted (MonadSh, liftSh, rm_rf, writefile) import Verismith.Internal import Verismith.Result import Verismith.Tool @@ -517,13 +517,15 @@ defaultBot = const False -- | Reduction using custom reduction strategies. reduce_ :: MonadSh m - => Text + => Shelly.FilePath + -> Text -> Replace SourceInfo -> (SourceInfo -> Bool) -> (SourceInfo -> m Bool) -> SourceInfo -> m SourceInfo -reduce_ title repl bot eval src = do +reduce_ out title repl bot eval src = do + writefile out $ genSource src liftSh . Shelly.echo $ "Reducing " @@ -556,16 +558,17 @@ reduce_ title repl bot eval src = do None -> return src where cond s = s /= src - recReduction = reduce_ title repl bot eval + recReduction = reduce_ out title repl bot eval -- | Reduce an input to a minimal representation. It follows the reduction -- strategy mentioned above. reduce :: MonadSh m - => (SourceInfo -> m Bool) -- ^ Failed or not. + => Shelly.FilePath -- ^ Filepath for temporary file. + -> (SourceInfo -> m Bool) -- ^ Failed or not. -> SourceInfo -- ^ Input verilog source to be reduced. -> m SourceInfo -- ^ Reduced output. -reduce eval src = +reduce fp eval src = fmap removeDecl $ red "Modules" moduleBot halveModules src >>= redAll "Module items" modItemBot halveModItems @@ -573,8 +576,8 @@ reduce eval src = -- >>= redAll "Expressions" (const defaultBot) halveExpr >>= red "Remove constants in concat" defaultBot removeConstInConcat where - red s bot a = reduce_ s a bot eval - red' s bot a t = reduce_ s (a t) (bot t) eval + red s bot a = reduce_ fp s a bot eval + red' s bot a t = reduce_ fp s (a t) (bot t) eval redAll s bot halve' src' = foldrM (\t -> red' (s <> " (" <> getIdentifier t <> ")") bot halve' t) src' @@ -599,7 +602,7 @@ reduceWithScript reduceWithScript top script file = do liftSh . Shelly.cp file $ file <.> "original" srcInfo <- liftIO . parseSourceInfoFile top $ Shelly.toTextIgnore file - void $ reduce (runScript script file) srcInfo + void $ reduce (fromText "reduce_script.v") (runScript script file) srcInfo -- | Reduce a 'SourceInfo' using two 'Synthesiser' that are passed to it. reduceSynth @@ -609,7 +612,7 @@ reduceSynth -> b -> SourceInfo -> m SourceInfo -reduceSynth datadir a b = reduce synth +reduceSynth datadir a b = reduce (fromText $ "reduce_" <> toText a <> "_" <> toText b <> ".v") synth where synth src' = liftSh $ do r <- runResultT $ do @@ -621,7 +624,7 @@ reduceSynth datadir a b = reduce synth _ -> False reduceSynthesis :: (Synthesiser a, MonadSh m) => a -> SourceInfo -> m SourceInfo -reduceSynthesis a = reduce synth +reduceSynthesis a = reduce (fromText $ "reduce_" <> toText a <> ".v") synth where synth src = liftSh $ do r <- runResultT $ runSynth a src @@ -638,7 +641,7 @@ runInTmp a = Shelly.withTmpDir $ (\f -> do return r) reduceSimIc :: (Synthesiser a, MonadSh m) => Shelly.FilePath -> [ByteString] -> a -> SourceInfo -> m SourceInfo -reduceSimIc fp bs a = reduce synth +reduceSimIc fp bs a = reduce (fromText $ "reduce_sim_" <> toText a) synth where synth src = liftSh . runInTmp $ do r <- runResultT $ do -- cgit