Add reduction for simulation failures

7 files changed, 176 insertions, 72 deletions

diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs
index b600d68..c38601a 100644
--- a/src/Verismith/Fuzz.hs
+++ b/src/Verismith/Fuzz.hs
@@ -39,7 +39,7 @@ import           Control.Monad.Trans.Control (MonadBaseControl)
 import qualified Crypto.Random.DRBG          as C
 import           Data.ByteString             (ByteString)
 import           Data.List                   (nubBy, sort)
-import           Data.Maybe                  (fromMaybe, isNothing)
+import           Data.Maybe                  (catMaybes, fromMaybe, isNothing)
 import           Data.Text                   (Text)
 import qualified Data.Text                   as T
 import           Data.Time
@@ -54,6 +54,7 @@ import           Shelly                      hiding (get)
 import           Shelly.Lifted               (MonadSh, liftSh)
 import           System.FilePath.Posix       (takeBaseName)
 import           Verismith.Config
+import           Verismith.CounterEg         (CounterEg (..))
 import           Verismith.Internal
 import           Verismith.Reduce
 import           Verismith.Report
@@ -166,8 +167,8 @@ filterSynth (SynthResult _ _ (Pass _) _) = True
 filterSynth _                            = False
 
 filterSim :: SimResult -> Bool
-filterSim (SimResult _ _ (Pass _) _) = True
-filterSim _                          = False
+filterSim (SimResult _ _ _ (Pass _) _) = True
+filterSim _                            = False
 
 filterSynthStat :: SynthStatus -> Bool
 filterSynthStat (SynthStatus _ (Pass _) _) = True
@@ -240,12 +241,19 @@ 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 sima bs as b =
+    applyList (applyList (repeat uncurry) (applyList (applyList (SimResult <$> as) (repeat sima)) (repeat bs))) $ fmap swap b
+
 toolRun :: (MonadIO m, MonadSh m) => Text -> m a -> m (NominalDiffTime, a)
 toolRun t m = do
     logT $ "Running " <> t
@@ -291,23 +299,35 @@ simulation :: (MonadIO m, MonadSh m) => SourceInfo -> Fuzz m ()
 simulation src = do
     datadir <- fmap _fuzzDataDir askOpts
     synth    <- passedSynthesis
+    counterEgs <- failEquivWithIdentityCE
     vals     <- liftIO $ generateByteString 20
-    ident    <- liftSh $ equiv datadir vals defaultIdentitySynth
-    resTimes <- liftSh $ mapM (equiv datadir vals) synth
+    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
-    equiv datadir b a = toolRun ("simulation for " <> toText a) . runResultT $ do
+    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
+            runSimIc datadir defaultIcarus a src b i
         where dir = fromText $ "simulation_" <> toText a
+    simCounterEg datadir (a, 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 "rtl.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
 
 -- | Generate a specific number of random bytestrings of size 256.
 randomByteString :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString]
@@ -329,6 +349,19 @@ failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get
     withIdentity (SynthResult _ (IdentitySynth _) (Fail (EquivFail _)) _) = True
     withIdentity _                                                    = False
 
+failEquivWithIdentityCE :: (MonadSh m) => Fuzz m [(SynthTool, 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
+
+failedSimulations :: (MonadSh m) => Fuzz m [SimResult]
+failedSimulations = filter failedSim . _fuzzSimResults <$> get
+  where
+    failedSim (SimResult _ _ _ (Fail (SimFail _)) _) = True
+    failedSim _                                      = False
+
 passEquiv :: (MonadSh m) => Fuzz m [SynthResult]
 passEquiv = filter withIdentity . _fuzzSynthResults <$> get
   where
@@ -341,8 +374,10 @@ reduction src = do
     datadir <- fmap _fuzzDataDir askOpts
     fails      <- failEquivWithIdentity
     synthFails <- failedSynthesis
+    simFails <- failedSimulations
     _          <- liftSh $ mapM (red datadir) fails
     _          <- liftSh $ mapM redSynth synthFails
+    _ <- liftSh $ mapM (redSim datadir) simFails
     return ()
   where
     red datadir (SynthResult a b _ _) = do
@@ -359,6 +394,13 @@ reduction src = do
             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
 
 titleRun
     :: (MonadIO m, MonadSh m) => Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a)
@@ -447,9 +489,10 @@ fuzz gen = do
         then return (0, mempty)
         else titleRun "Simulation" $ simulation src
     fails       <- failEquivWithIdentity
+    failedSim <- failedSimulations
     synthFails  <- failedSynthesis
     redResult   <-
-        whenMaybe (not (null fails && null synthFails)
+        whenMaybe (not (null failedSim && null fails && null synthFails)
                    && not (_fuzzOptsNoReduction opts))
         . titleRun "Reduction"
         $ reduction src
diff --git a/src/Verismith/Reduce.hs b/src/Verismith/Reduce.hs
index 69b5e17..e7614e6 100644
--- a/src/Verismith/Reduce.hs
+++ b/src/Verismith/Reduce.hs
@@ -18,6 +18,7 @@ module Verismith.Reduce
       reduceWithScript
     , reduceSynth
     , reduceSynthesis
+    , reduceSimIc
     , reduce
     , reduce_
     , Replacement(..)
@@ -40,6 +41,7 @@ where
 import           Control.Lens             hiding ((<.>))
 import           Control.Monad            (void)
 import           Control.Monad.IO.Class   (MonadIO, liftIO)
+import           Data.ByteString          (ByteString)
 import           Data.Foldable            (foldrM)
 import           Data.List                (nub)
 import           Data.List.NonEmpty       (NonEmpty (..))
@@ -48,10 +50,12 @@ import           Data.Maybe               (mapMaybe)
 import           Data.Text                (Text)
 import           Shelly                   ((<.>))
 import qualified Shelly
-import           Shelly.Lifted            (MonadSh, liftSh)
+import           Shelly.Lifted            (MonadSh, liftSh, rm_rf)
 import           Verismith.Internal
 import           Verismith.Result
 import           Verismith.Tool
+import           Verismith.Tool.Icarus
+import           Verismith.Tool.Identity
 import           Verismith.Tool.Internal
 import           Verismith.Verilog
 import           Verismith.Verilog.AST
@@ -614,8 +618,7 @@ reduceSynth datadir a b = reduce synth
             runEquiv datadir a b src'
         return $ case r of
             Fail (EquivFail _) -> True
-            Fail _             -> False
-            Pass _             -> False
+            _                  -> False
 
 reduceSynthesis :: (Synthesiser a, MonadSh m) => a -> SourceInfo -> m SourceInfo
 reduceSynthesis a = reduce synth
@@ -624,5 +627,25 @@ reduceSynthesis a = reduce synth
         r <- runResultT $ runSynth a src
         return $ case r of
             Fail SynthFail -> True
-            Fail _         -> False
-            Pass _         -> False
+            _              -> False
+
+runInTmp :: Shelly.Sh a -> Shelly.Sh a
+runInTmp a = Shelly.withTmpDir $ (\f -> do
+    dir <- Shelly.pwd
+    Shelly.cd f
+    r <- a
+    Shelly.cd dir
+    return r)
+
+reduceSimIc :: (Synthesiser a, MonadSh m) => Shelly.FilePath -> [ByteString] -> a -> SourceInfo -> m SourceInfo
+reduceSimIc fp bs a = reduce synth
+  where
+    synth src = liftSh . runInTmp $ do
+        r <- runResultT $ do
+            runSynth a src
+            runSynth defaultIdentity src
+            i <- runSimIc fp defaultIcarus defaultIdentity src bs Nothing
+            runSimIc fp defaultIcarus a src bs $ Just i
+        return $ case r of
+            Fail (SimFail _) -> True
+            _                -> False
diff --git a/src/Verismith/Report.hs b/src/Verismith/Report.hs
index 743240d..dbaf613 100644
--- a/src/Verismith/Report.hs
+++ b/src/Verismith/Report.hs
@@ -155,15 +155,15 @@ defaultIcarusSim = IcarusSim defaultIcarus
 
 -- | The results from running a tool through a simulator. It can either fail or
 -- return a result, which is most likely a 'ByteString'.
-data SimResult = SimResult !SynthTool !SimTool !BResult !NominalDiffTime
+data SimResult = SimResult !SynthTool !SimTool ![ByteString] !BResult !NominalDiffTime
                  deriving (Eq)
 
 instance Show SimResult where
-    show (SimResult synth sim r d) = show synth <> ", " <> show sim <> ": " <> show (bimap show (T.unpack . showBS) r) <> " (" <> show d <> ")"
+    show (SimResult synth sim _ r d) = show synth <> ", " <> show sim <> ": " <> show (bimap show (T.unpack . showBS) r) <> " (" <> show d <> ")"
 
 getSimResult :: SimResult -> UResult
-getSimResult (SimResult _ _ (Pass _) _) = Pass ()
-getSimResult (SimResult _ _ (Fail b) _) = Fail b
+getSimResult (SimResult _ _ _ (Pass _) _) = Pass ()
+getSimResult (SimResult _ _ _ (Fail b) _) = Fail b
 
 -- | The results of comparing the synthesised outputs of two files using a
 -- formal equivalence checker. This will either return a failure or an output
@@ -239,7 +239,7 @@ status :: Result Failed () -> Html
 status (Pass _           )  = H.td ! A.class_ "is-success" $ "Passed"
 status (Fail EmptyFail   )  = H.td ! A.class_ "is-danger" $ "Failed"
 status (Fail (EquivFail _)) = H.td ! A.class_ "is-danger" $ "Equivalence failed"
-status (Fail SimFail     )  = H.td ! A.class_ "is-danger" $ "Simulation failed"
+status (Fail (SimFail  _))  = H.td ! A.class_ "is-danger" $ "Simulation failed"
 status (Fail SynthFail   )  = H.td ! A.class_ "is-danger" $ "Synthesis failed"
 status (Fail EquivError  )  = H.td ! A.class_ "is-danger" $ "Equivalence error"
 status (Fail TimeoutError)  = H.td ! A.class_ "is-warning" $ "Time out"
diff --git a/src/Verismith/Result.hs b/src/Verismith/Result.hs
index d8efd2f..2ecb728 100644
--- a/src/Verismith/Result.hs
+++ b/src/Verismith/Result.hs
@@ -22,6 +22,8 @@ needed in "Verismith".
 module Verismith.Result
     ( Result(..)
     , ResultT(..)
+    , justPass
+    , justFail
     , (<?>)
     , annotate
     )
@@ -42,6 +44,14 @@ data Result a b = Fail a
                 | Pass b
                 deriving (Eq, Show)
 
+justPass :: Result a b -> Maybe b
+justPass (Fail _) = Nothing
+justPass (Pass a) = Just a
+
+justFail :: Result a b -> Maybe a
+justFail (Pass _) = Nothing
+justFail (Fail a) = Just a
+
 instance Semigroup (Result a b) where
     Pass _ <> a = a
     a <> _ = a
diff --git a/src/Verismith/Tool/Icarus.hs b/src/Verismith/Tool/Icarus.hs
index 9d4281f..68273a2 100644
--- a/src/Verismith/Tool/Icarus.hs
+++ b/src/Verismith/Tool/Icarus.hs
@@ -14,6 +14,7 @@ module Verismith.Tool.Icarus
     ( Icarus(..)
     , defaultIcarus
     , runSimIc
+    , runSimIcEC
     )
 where
 
@@ -39,6 +40,8 @@ import           Numeric                    (readInt)
 import           Prelude                    hiding (FilePath)
 import           Shelly
 import           Shelly.Lifted              (liftSh)
+import           Verismith.CounterEg        (CounterEg (..))
+import           Verismith.Result
 import           Verismith.Tool.Internal
 import           Verismith.Tool.Template
 import           Verismith.Verilog.AST
@@ -114,12 +117,12 @@ runSimIcarus sim rinfo bss = do
     let newtb     = instantiateMod m tb
     let modWithTb = Verilog [newtb, m]
     liftSh . writefile "main.v" $ genSource modWithTb
-    annotate SimFail $ runSimWithFile sim "main.v" bss
+    annotate (SimFail mempty) $ runSimWithFile sim "main.v" bss
     where m = rinfo ^. mainModule
 
 runSimIcarusWithFile
     :: Icarus -> FilePath -> [ByteString] -> ResultSh ByteString
-runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do
+runSimIcarusWithFile sim f _ = annotate (SimFail mempty) . liftSh $ do
     dir <- pwd
     logCommand_ dir "icarus"
         $ run (icarusPath sim) ["-o", "main", toTextIgnore f]
@@ -131,49 +134,46 @@ runSimIcarusWithFile sim f _ = annotate SimFail . liftSh $ do
 fromBytes :: ByteString -> Integer
 fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b
 
-runSimIc
-    :: (Synthesiser b)
-    => FilePath
-    -> Icarus
-    -> b
-    -> SourceInfo
-    -> [ByteString]
-    -> ResultSh ByteString
-runSimIc datadir sim1 synth1 srcInfo bss = do
-    dir <- liftSh pwd
-    let top      = srcInfo ^. mainModule
-    let inConcat = (RegConcat . filter filterClk $ (Id . fromPort <$> (top ^. modInPorts)))
-    let
-        tb = instantiateMod top $ ModDecl
-            "testbench"
-            []
-            []
-            [ Initial
-            $  fold
-                   [ BlockAssign (Assign "clk" Nothing 0)
-                   , BlockAssign (Assign inConcat Nothing 0)
-                   ]
-            <> fold
-                   (   (\r -> TimeCtrl
-                           10
-                           (Just $ BlockAssign (Assign inConcat Nothing r))
-                       )
-                   .   fromInteger
-                   .   fromBytes
-                   <$> bss
-                   )
-            <> (SysTaskEnable $ Task "finish" [])
-            , Always . TimeCtrl 5 . Just $ BlockAssign
+tbModule :: [ByteString] -> ModDecl -> Verilog
+tbModule bss top =
+    Verilog [ instantiateMod top $ ModDecl "testbench" [] []
+              [ Initial
+                $  fold [ BlockAssign (Assign "clk" Nothing 0)
+                        , BlockAssign (Assign inConcat Nothing 0)
+                        ]
+                <> fold ((\r -> TimeCtrl 10
+                             (Just $ BlockAssign (Assign inConcat Nothing r)))
+                         . fromInteger . fromBytes <$> bss)
+                <> (SysTaskEnable $ Task "finish" [])
+              , Always . TimeCtrl 5 . Just $ BlockAssign
                 (Assign "clk" Nothing (UnOp UnNot (Id "clk")))
-            , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable $ Task
-                "strobe"
-                ["%b", Id "y"]
+              , Always . EventCtrl (EPosEdge "clk") . Just . SysTaskEnable
+                $ Task "strobe" ["%b", Id "y"]
+              ] []
             ]
-            []
+  where
+    inConcat = (RegConcat . filter (/= (Id "clk")) $ (Id . fromPort <$> (top ^. modInPorts)))
 
-    liftSh . writefile "testbench.v" $ icarusTestbench datadir (Verilog [tb]) synth1
-    liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"]
-    liftSh
+counterTestBench :: CounterEg -> ModDecl -> Verilog
+counterTestBench (CounterEg _ states) m = tbModule filtered m
+  where
+    filtered = convert . fold . fmap snd . filter ((/= "clk") . fst) <$> states
+
+runSimIc' :: (Synthesiser b) => ([ByteString] -> ModDecl -> Verilog)
+          -> FilePath
+          -> Icarus
+          -> b
+          -> SourceInfo
+          -> [ByteString]
+          -> Maybe ByteString
+          -> ResultSh ByteString
+runSimIc' fun datadir sim1 synth1 srcInfo bss bs = do
+    dir <- liftSh pwd
+    let top      = srcInfo ^. mainModule
+    let tb = fun bss top
+    liftSh . writefile tbname $ icarusTestbench datadir tb synth1
+    liftSh $ exe dir "icarus" "iverilog" ["-o", exename, toTextIgnore tbname]
+    s <- liftSh
         $   B.take 8
         .   BA.convert
         .   (hash :: ByteString -> Digest SHA256)
@@ -183,9 +183,29 @@ runSimIc datadir sim1 synth1 srcInfo bss = do
                 (runFoldLines (mempty :: ByteString)
                               callback
                               (vvpPath sim1)
-                              ["main"]
-                )
+                              [exename])
+    case (bs, s) of
+        (Nothing, s') -> ResultT . return $ Pass s'
+        (Just bs', s') -> if bs' == s'
+                    then ResultT . return $ Pass s'
+                    else ResultT . return $ Fail (SimFail s')
   where
     exe dir name e = void . errExit False . logCommand dir name . timeout e
-    filterClk (Id "clk") = False
-    filterClk (Id _)     = True
+    tbname = fromText $ toText synth1 <> "_testbench.v"
+    exename = toText synth1 <> "_main"
+
+runSimIc :: (Synthesiser b)
+         => FilePath         -- ^ Data directory.
+         -> Icarus           -- ^ Icarus simulator.
+         -> b                -- ^ Synthesis tool to be tested.
+         -> SourceInfo       -- ^ Original generated program to test.
+         -> [ByteString]     -- ^ Test vectors to be passed as inputs to the generated Verilog.
+         -> Maybe ByteString -- ^ What the correct output should be. If
+                             -- 'Nothing' is passed, then just return 'Pass
+                             -- ByteString' with the answer.
+         -> ResultSh ByteString
+runSimIc = runSimIc' tbModule
+
+runSimIcEC :: (Synthesiser b) => FilePath -> Icarus -> b
+           -> SourceInfo -> CounterEg -> Maybe ByteString -> ResultSh ByteString
+runSimIcEC a b c d e = runSimIc' (const $ counterTestBench e) a b c d []
diff --git a/src/Verismith/Tool/Internal.hs b/src/Verismith/Tool/Internal.hs
index ee31c4e..b97c2f1 100644
--- a/src/Verismith/Tool/Internal.hs
+++ b/src/Verismith/Tool/Internal.hs
@@ -77,10 +77,18 @@ class Tool a => Simulator a where
 data Failed = EmptyFail
             | EquivFail CounterEg
             | EquivError
-            | SimFail
+            | SimFail ByteString
             | SynthFail
             | TimeoutError
-            deriving (Eq, Show)
+            deriving (Eq)
+
+instance Show Failed where
+    show EmptyFail     = "EmptyFail"
+    show (EquivFail _) = "EquivFail"
+    show EquivError    = "EquivError"
+    show (SimFail bs)  = "SimFail " <> T.unpack (T.take 10 $ showBS bs)
+    show SynthFail     = "SynthFail"
+    show TimeoutError  = "TimeoutError"
 
 instance Semigroup Failed where
     EmptyFail <> a = a
diff --git a/verismith.cabal b/verismith.cabal
index b54e522..76fc97b 100644
--- a/verismith.cabal
+++ b/verismith.cabal
@@ -1,5 +1,5 @@
 name: verismith
-version: 0.4.0.1
+version: 0.4.1.0
 synopsis: Random verilog generation and simulator testing.
 description:
   Verismith provides random verilog generation modules
@@ -27,7 +27,7 @@ source-repository head
 source-repository this
   type:     git
   location: https://github.com/ymherklotz/verismith
-  tag:      v0.4.0.1
+  tag:      v0.4.1.0
 
 custom-setup
   setup-depends: