From 7e67a69693c4c0964f488d87dd94f64a2efe5409 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 24 May 2019 15:09:06 +0100 Subject: Reduction throws away path if it finds a passing one --- src/VeriFuzz/Reduce.hs | 35 ++++++++++++++++------------------- 1 file changed, 16 insertions(+), 19 deletions(-) (limited to 'src/VeriFuzz/Reduce.hs') diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index 33cb648..4875e7d 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -502,28 +502,25 @@ reduce_ title repl bot eval src = do (src ^.. infoSrc . _Wrapped . traverse . modItems . traverse) ) <> ")" - replAnswer <- sequenceA $ evalIfNotEmpty <$> replacement - case (replacement, replAnswer) of - (Single s, Single True ) -> runIf s - (Dual _ r, Dual False True) -> runIf r - (Dual l _, Dual True False) -> runIf l - (Dual l r, Dual True True ) -> check l r - _ -> return src + case repl src of + Single s -> do + red <- eval s + if red then runIf s else return s + Dual l r -> do + red <- eval l + if red && cond l + then reduce_ title repl bot eval l + else do + red' <- eval r + if red' && cond r + then reduce_ title repl bot eval r + else if l < r then return l else return r + None -> return src where - replacement = repl src - runIf s = if s /= src && not (bot s) + runIf s = if cond s then reduce_ title repl bot eval s else return s - evalIfNotEmpty = eval - check l r - | bot l = return l - | bot r = return r - | otherwise = do - lreduced <- runIf l - rreduced <- runIf r - if _infoSrc lreduced < _infoSrc rreduced - then return lreduced - else return rreduced + cond s = s /= src && not (bot s) -- | Reduce an input to a minimal representation. It follows the reduction -- strategy mentioned above. -- cgit From 14158fc4ef0809adbbf0b7fdd0c0d5e0fafc2435 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 24 May 2019 15:45:35 +0100 Subject: Fix used wire check for clk --- src/VeriFuzz/Reduce.hs | 35 ++++++++++++++++++++++------------- 1 file changed, 22 insertions(+), 13 deletions(-) (limited to 'src/VeriFuzz/Reduce.hs') diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index 4875e7d..fcc8e51 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -111,7 +111,7 @@ instance Traversable Replacement where -- | Split a list in two halves. halve :: Replace [a] -halve [] = None +halve [] = Single [] halve [_] = Single [] halve l = Dual a b where (a, b) = splitAt (length l `div` 2) l @@ -254,6 +254,12 @@ exprId (VecSelect i _) = Just i exprId (RangeSelect i _) = Just i exprId _ = Nothing +eventId :: Event -> Maybe Identifier +eventId (EId i) = Just i +eventId (EPosEdge i) = Just i +eventId (ENegEdge i) = Just i +eventId _ = Nothing + portToId :: Port -> Identifier portToId (Port _ _ _ i) = i @@ -396,16 +402,19 @@ toIds = nub . mapMaybe exprId . concatMap universe toIdsConst :: [ConstExpr] -> [Identifier] toIdsConst = toIds . fmap constToExpr +toIdsEvent :: [Event] -> [Identifier] +toIdsEvent = nub . mapMaybe eventId . concatMap universe + allStatIds' :: Statement -> [Identifier] -allStatIds' s = nub $ assignIds <> otherExpr +allStatIds' s = nub $ assignIds <> otherExpr <> eventProcessedIds where - assignIds = - toIds + assignIds = toIds $ (s ^.. stmntBA . assignExpr) <> (s ^.. stmntNBA . assignExpr) <> (s ^.. forAssign . assignExpr) <> (s ^.. forIncr . assignExpr) otherExpr = toIds $ (s ^.. forExpr) <> (s ^.. stmntCondExpr) + eventProcessedIds = toIdsEvent $ s ^.. statEvent allStatIds :: Statement -> [Identifier] allStatIds s = nub . concat $ allStatIds' <$> universe s @@ -505,22 +514,22 @@ reduce_ title repl bot eval src = do case repl src of Single s -> do red <- eval s - if red then runIf s else return s + if red + then if cond s then recReduction s else return s + else return src Dual l r -> do red <- eval l - if red && cond l - then reduce_ title repl bot eval l + if red + then if cond l then recReduction l else return l else do red' <- eval r - if red' && cond r - then reduce_ title repl bot eval r - else if l < r then return l else return r + if red' + then if cond r then recReduction r else return r + else return src None -> return src where - runIf s = if cond s - then reduce_ title repl bot eval s - else return s cond s = s /= src && not (bot s) + recReduction = reduce_ title repl bot eval -- | Reduce an input to a minimal representation. It follows the reduction -- strategy mentioned above. -- cgit From fe9084c9fe731ff8f7d94729a3280357cda6f259 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 24 May 2019 17:37:02 +0100 Subject: No expression reduction --- src/VeriFuzz/Reduce.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/VeriFuzz/Reduce.hs') diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index fcc8e51..bfc9a6e 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -543,7 +543,7 @@ reduce eval src = $ red "Modules" moduleBot halveModules src >>= redAll "Module Items" modItemBot halveModItems >>= redAll "Statements" (const defaultBot) halveStatements - >>= redAll "Expressions" (const defaultBot) halveExpr + -- >>= redAll "Expressions" (const defaultBot) halveExpr where red s bot a = reduce_ s a bot eval red' s bot a t = reduce_ s (a t) (bot t) eval -- cgit From 0a45b7d0cfa76e8a543bc2ddffe7d4e56aaae93a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 25 May 2019 21:18:24 +0100 Subject: Add reducesynthesis function --- src/VeriFuzz/Reduce.hs | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src/VeriFuzz/Reduce.hs') diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index bfc9a6e..0ecde3f 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -591,3 +591,16 @@ reduceSynth a b = reduce synth Fail EquivFail -> True Fail _ -> False Pass _ -> False + +reduceSynthesis :: (Synthesiser a, MonadSh m) + => a + -> SourceInfo + -> m SourceInfo +reduceSynthesis a = reduce synth + where + synth src = liftSh $ do + r <- runResultT $ runSynth a src + return $ case r of + Fail SynthFail -> True + Fail _ -> False + Pass _ -> False -- cgit From 4fba97ba3a19c725714b5d55721368657e41daa3 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 25 May 2019 21:20:51 +0100 Subject: Add synthesis fails to fuzzer --- src/VeriFuzz/Reduce.hs | 1 + 1 file changed, 1 insertion(+) (limited to 'src/VeriFuzz/Reduce.hs') diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index 0ecde3f..b025a42 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -17,6 +17,7 @@ module VeriFuzz.Reduce ( -- $strategy reduceWithScript , reduceSynth + , reduceSynthesis , reduce , reduce_ , Replacement(..) -- cgit From 11bd73faa516cde0af74e5359c36c8f1fa4e816a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 25 May 2019 23:26:27 +0100 Subject: Fix reduction for statements --- src/VeriFuzz/Reduce.hs | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) (limited to 'src/VeriFuzz/Reduce.hs') diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index b025a42..2f44c07 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -35,27 +35,28 @@ module VeriFuzz.Reduce ) where -import Control.Lens hiding ((<.>)) -import Control.Monad (void) -import Control.Monad.IO.Class (MonadIO, liftIO) -import Data.Foldable (foldrM) -import Data.List (nub) -import Data.List.NonEmpty (NonEmpty (..)) -import qualified Data.List.NonEmpty as NonEmpty -import Data.Maybe (mapMaybe) -import Data.Text (Text) -import Shelly ((<.>)) +import Control.Lens hiding ((<.>)) +import Control.Monad (void) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Data.Foldable (foldrM) +import Data.List (nub) +import Data.List.NonEmpty (NonEmpty (..)) +import qualified Data.List.NonEmpty as NonEmpty +import Data.Maybe (mapMaybe) +import Data.Text (Text) +import Shelly ((<.>)) import qualified Shelly -import Shelly.Lifted (MonadSh, liftSh) +import Shelly.Lifted (MonadSh, liftSh) import VeriFuzz.Internal import VeriFuzz.Result import VeriFuzz.Sim import VeriFuzz.Sim.Internal +import VeriFuzz.Verilog import VeriFuzz.Verilog.AST -import VeriFuzz.Verilog.CodeGen import VeriFuzz.Verilog.Mutate import VeriFuzz.Verilog.Parser + -- $strategy -- The reduction strategy has multiple different steps. 'reduce' will run these -- strategies one after another, starting at the most coarse grained one. The @@ -334,6 +335,7 @@ matchesModName :: Identifier -> ModDecl -> Bool matchesModName top (ModDecl i _ _ _ _) = top == i halveStatement :: Replace Statement +halveStatement (SeqBlock [s]) = halveStatement s halveStatement (SeqBlock s) = SeqBlock <$> halve s halveStatement (CondStmnt _ (Just s1) (Just s2)) = Dual s1 s2 halveStatement (CondStmnt _ (Just s1) Nothing) = Single s1 -- cgit From 43e074229c4ea859e66035c716d8bb4fcd037c90 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 2 Jun 2019 12:54:15 +0100 Subject: Add check for quicker reduction --- src/VeriFuzz/Reduce.hs | 36 +++++++++++++++++++----------------- 1 file changed, 19 insertions(+), 17 deletions(-) (limited to 'src/VeriFuzz/Reduce.hs') diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index 2f44c07..2a8b489 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -514,24 +514,26 @@ reduce_ title repl bot eval src = do (src ^.. infoSrc . _Wrapped . traverse . modItems . traverse) ) <> ")" - case repl src of - Single s -> do - red <- eval s - if red - then if cond s then recReduction s else return s - else return src - Dual l r -> do - red <- eval l - if red - then if cond l then recReduction l else return l - else do - red' <- eval r - if red' - then if cond r then recReduction r else return r - else return src - None -> return src + if bot src + then return src + else case repl src of + Single s -> do + red <- eval s + if red + then if cond s then recReduction s else return s + else return src + Dual l r -> do + red <- eval l + if red + then if cond l then recReduction l else return l + else do + red' <- eval r + if red' + then if cond r then recReduction r else return r + else return src + None -> return src where - cond s = s /= src && not (bot s) + cond s = s /= src recReduction = reduce_ title repl bot eval -- | Reduce an input to a minimal representation. It follows the reduction -- cgit From 720fa7a822a077458cf0b29e9dcdc754a881e8bd Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 5 Jun 2019 13:52:20 +0100 Subject: Format all files --- src/VeriFuzz/Reduce.hs | 56 ++++++++++++++++++++++++-------------------------- 1 file changed, 27 insertions(+), 29 deletions(-) (limited to 'src/VeriFuzz/Reduce.hs') diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index 2a8b489..7cee31c 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -257,7 +257,7 @@ exprId (RangeSelect i _) = Just i exprId _ = Nothing eventId :: Event -> Maybe Identifier -eventId (EId i) = Just i +eventId (EId i) = Just i eventId (EPosEdge i) = Just i eventId (ENegEdge i) = Just i eventId _ = Nothing @@ -411,12 +411,13 @@ toIdsEvent = nub . mapMaybe eventId . concatMap universe allStatIds' :: Statement -> [Identifier] allStatIds' s = nub $ assignIds <> otherExpr <> eventProcessedIds where - assignIds = toIds + assignIds = + toIds $ (s ^.. stmntBA . assignExpr) <> (s ^.. stmntNBA . assignExpr) <> (s ^.. forAssign . assignExpr) <> (s ^.. forIncr . assignExpr) - otherExpr = toIds $ (s ^.. forExpr) <> (s ^.. stmntCondExpr) + otherExpr = toIds $ (s ^.. forExpr) <> (s ^.. stmntCondExpr) eventProcessedIds = toIdsEvent $ s ^.. statEvent allStatIds :: Statement -> [Identifier] @@ -517,21 +518,21 @@ reduce_ title repl bot eval src = do if bot src then return src else case repl src of - Single s -> do - red <- eval s - if red - then if cond s then recReduction s else return s - else return src - Dual l r -> do - red <- eval l - if red - then if cond l then recReduction l else return l - else do - red' <- eval r - if red' - then if cond r then recReduction r else return r - else return src - None -> return src + Single s -> do + red <- eval s + if red + then if cond s then recReduction s else return s + else return src + Dual l r -> do + red <- eval l + if red + then if cond l then recReduction l else return l + else do + red' <- eval r + if red' + then if cond r then recReduction r else return r + else return src + None -> return src where cond s = s /= src recReduction = reduce_ title repl bot eval @@ -597,15 +598,12 @@ reduceSynth a b = reduce synth Fail _ -> False Pass _ -> False -reduceSynthesis :: (Synthesiser a, MonadSh m) - => a - -> SourceInfo - -> m SourceInfo +reduceSynthesis :: (Synthesiser a, MonadSh m) => a -> SourceInfo -> m SourceInfo reduceSynthesis a = reduce synth - where - synth src = liftSh $ do - r <- runResultT $ runSynth a src - return $ case r of - Fail SynthFail -> True - Fail _ -> False - Pass _ -> False + where + synth src = liftSh $ do + r <- runResultT $ runSynth a src + return $ case r of + Fail SynthFail -> True + Fail _ -> False + Pass _ -> False -- cgit From d32f4cc45bc8c0670fb788b1fcd4c2f2b15fa094 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 29 Jun 2019 20:33:59 +0100 Subject: Format files --- src/VeriFuzz/Reduce.hs | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) (limited to 'src/VeriFuzz/Reduce.hs') diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index 7cee31c..6bae371 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -35,18 +35,22 @@ module VeriFuzz.Reduce ) where -import Control.Lens hiding ((<.>)) -import Control.Monad (void) -import Control.Monad.IO.Class (MonadIO, liftIO) -import Data.Foldable (foldrM) -import Data.List (nub) -import Data.List.NonEmpty (NonEmpty (..)) -import qualified Data.List.NonEmpty as NonEmpty -import Data.Maybe (mapMaybe) -import Data.Text (Text) -import Shelly ((<.>)) +import Control.Lens hiding ( (<.>) ) +import Control.Monad ( void ) +import Control.Monad.IO.Class ( MonadIO + , liftIO + ) +import Data.Foldable ( foldrM ) +import Data.List ( nub ) +import Data.List.NonEmpty ( NonEmpty(..) ) +import qualified Data.List.NonEmpty as NonEmpty +import Data.Maybe ( mapMaybe ) +import Data.Text ( Text ) +import Shelly ( (<.>) ) import qualified Shelly -import Shelly.Lifted (MonadSh, liftSh) +import Shelly.Lifted ( MonadSh + , liftSh + ) import VeriFuzz.Internal import VeriFuzz.Result import VeriFuzz.Sim -- cgit