From 3fbb87fe5c5058ecb2a2bdc30a999835aaced8af Mon Sep 17 00:00:00 2001 From: Yann Herklotz Grave Date: Sun, 3 Mar 2019 18:57:07 +0000 Subject: Add transformers and procedural generation --- src/VeriFuzz/AST.hs | 2 ++ src/VeriFuzz/Gen.hs | 95 ++++++++++++++++++++++++++++++++++++++++++++------ src/VeriFuzz/Mutate.hs | 3 +- src/VeriFuzz/Reduce.hs | 24 ++++++------- verifuzz.cabal | 3 +- 5 files changed, 102 insertions(+), 25 deletions(-) diff --git a/src/VeriFuzz/AST.hs b/src/VeriFuzz/AST.hs index b468c2f..a2ebb32 100644 --- a/src/VeriFuzz/AST.hs +++ b/src/VeriFuzz/AST.hs @@ -112,6 +112,8 @@ module VeriFuzz.AST , modConn , modConnName , modExpr + -- * Useful functions + , positiveArb -- * Useful Lenses and Traversals , getModule , getSourceId diff --git a/src/VeriFuzz/Gen.hs b/src/VeriFuzz/Gen.hs index 1e83888..1a64344 100644 --- a/src/VeriFuzz/Gen.hs +++ b/src/VeriFuzz/Gen.hs @@ -10,19 +10,44 @@ Portability : POSIX Various useful generators. -} +{-# LANGUAGE TemplateHaskell #-} + module VeriFuzz.Gen where -import Control.Lens -import Data.Foldable (fold) -import qualified Data.Text as T -import Test.QuickCheck (Gen) -import qualified Test.QuickCheck as QC +import Control.Lens hiding (Context) +import Control.Monad (replicateM) +import Control.Monad.Trans.Class (lift) +import Control.Monad.Trans.Reader hiding (local) +import Control.Monad.Trans.State.Lazy +import Data.Foldable (fold) +import qualified Data.Text as T +import Test.QuickCheck (Gen) +import qualified Test.QuickCheck as QC import VeriFuzz.AST import VeriFuzz.ASTGen +import VeriFuzz.CodeGen import VeriFuzz.Internal import VeriFuzz.Mutate import VeriFuzz.Random +data Context = Context { _variables :: [Port] + , _modules :: [ModDecl] + } + +makeLenses ''Context + +data ProbModItem = ProbModItem { _probAssign :: {-# UNPACK #-} !Int + , _probAlways :: {-# UNPACK #-} !Int + } + +makeLenses ''ProbModItem + +data Probabilities = Probabilities { _probModItem :: {-# UNPACK #-} !ProbModItem } + +makeLenses ''Probabilities + +type StateGen = StateT Context (ReaderT Probabilities Gen) + toId :: Int -> Identifier toId = Identifier . ("w" <>) . T.pack . show @@ -54,12 +79,7 @@ randomMod inps total = do let other = drop inps ident let y = ModCA . ContAssign "y" . fold $ Id <$> drop inps ids let yport = [wire (sumSize other) "y"] - return - . initMod - . declareMod other - . ModDecl "test_module" yport inputs_ - $ x - ++ [y] + return . declareMod other . ModDecl "test_module" yport inputs_ $ x ++ [y] where ids = toId <$> [1 .. total] end = drop inps ids @@ -75,3 +95,56 @@ fromGraph = do ^.. getVerilogSrc . traverse . getDescription + +gen :: Gen a -> StateGen a +gen = lift . lift + +proceduralContAssign :: StateGen ContAssign +proceduralContAssign = do + name <- gen QC.arbitrary + size <- gen positiveArb + signed <- gen QC.arbitrary + context <- get + variables %= (Port Wire signed size name :) + ContAssign name + <$> ( gen + . QC.sized + . exprWithContext + $ context + ^.. variables + . traverse + . portName + ) + +proceduralModItem :: StateGen ModItem +proceduralModItem = ModCA <$> proceduralContAssign + +proceduralPorts :: StateGen [Port] +proceduralPorts = do + portList <- gen $ QC.listOf1 QC.arbitrary + variables %= (<> portList) + return portList + +proceduralMod :: Bool -> StateGen ModDecl +proceduralMod top = do + name <- if top then return "top" else gen QC.arbitrary + portList <- proceduralPorts + amount <- gen positiveArb + mi <- replicateM amount proceduralModItem + context <- get + let local = filter (\p -> notElem p portList) $ context ^. variables + let size = sum $ local ^.. traverse . portSize + let yport = Port Wire False size "y" + return . declareMod local . ModDecl name [yport] portList $ combineAssigns + yport + mi + +procedural :: Gen VerilogSrc +procedural = + VerilogSrc + . (: []) + . Description + <$> runReaderT (evalStateT (proceduralMod True) context) config + where + config = Probabilities (ProbModItem 5 1) + context = Context [] [] diff --git a/src/VeriFuzz/Mutate.hs b/src/VeriFuzz/Mutate.hs index b851d8d..e8b510f 100644 --- a/src/VeriFuzz/Mutate.hs +++ b/src/VeriFuzz/Mutate.hs @@ -191,7 +191,8 @@ makeTopAssert = (modItems %~ (++ [assert])) . (modInPorts %~ addClk) . makeTop -- | Provide declarations for all the ports that are passed to it. declareMod :: [Port] -> ModDecl -> ModDecl -declareMod ports = modItems %~ (decl ++) where decl = Decl Nothing <$> ports +declareMod ports = initMod . (modItems %~ (decl ++)) + where decl = Decl Nothing <$> ports -- | Simplify an 'Expr' by using constants to remove 'BinaryOperator' and -- simplify expressions. To make this work effectively, it should be run until diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs index 3cecbe4..b09055e 100644 --- a/src/VeriFuzz/Reduce.hs +++ b/src/VeriFuzz/Reduce.hs @@ -108,12 +108,12 @@ halveAssigns :: SourceInfo -> Replacement SourceInfo halveAssigns = combine mainModule halveModAssign halveIndExpr :: Expr -> Replacement Expr -halveIndExpr (Concat l) = Concat <$> halve l -halveIndExpr (BinOp e1 _ e2 ) = Dual e1 e2 -halveIndExpr (Cond _ e1 e2 ) = Dual e1 e2 -halveIndExpr (UnOp _ e ) = Single e -halveIndExpr (Func _ e ) = Single e -halveIndExpr e = Single e +halveIndExpr (Concat l ) = Concat <$> halve l +halveIndExpr (BinOp e1 _ e2) = Dual e1 e2 +halveIndExpr (Cond _ e1 e2) = Dual e1 e2 +halveIndExpr (UnOp _ e ) = Single e +halveIndExpr (Func _ e ) = Single e +halveIndExpr e = Single e halveModExpr :: ModItem -> Replacement ModItem halveModExpr (ModCA ca) = ModCA <$> combine contAssignExpr halveIndExpr ca @@ -121,9 +121,9 @@ halveModExpr a = Single a halveExpr :: SourceInfo -> Replacement SourceInfo halveExpr = combine contexpr $ traverse halveModExpr - where - contexpr :: Lens' SourceInfo [ModItem] - contexpr = mainModule . modItems + where + contexpr :: Lens' SourceInfo [ModItem] + contexpr = mainModule . modItems reduce_ :: (SourceInfo -> Replacement SourceInfo) @@ -136,10 +136,10 @@ reduce_ repl eval src = do (Single s, Single False) -> do putStrLn "########## 1 ##########" runIf s - (Dual _ l, Dual True False ) -> do + (Dual _ l, Dual True False) -> do putStrLn "########## 2 ##########" runIf l - (Dual r _, Dual False True ) -> do + (Dual r _, Dual False True) -> do putStrLn "########## 3 ##########" runIf r (Dual r l, Dual False False) -> do @@ -152,7 +152,7 @@ reduce_ repl eval src = do (None, None) -> do putStrLn "########## 5 ##########" return src - _ -> do + _ -> do putStrLn "########## 6 ##########" return src where diff --git a/verifuzz.cabal b/verifuzz.cabal index 5bcf0ef..118406a 100644 --- a/verifuzz.cabal +++ b/verifuzz.cabal @@ -59,7 +59,8 @@ library , cryptonite >=0.25 && <0.26 , memory >=0.14 && <0.15 , DRBG >=0.5 && <0.6 - , parsec >= 3.1 && < 3.2 + , parsec >=3.1 && <3.2 + , transformers >=0.5 && <0.6 default-extensions: OverloadedStrings executable verifuzz -- cgit