From 472aedf5daeb1cb0d095a63eacf259b798f56586 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 16 Mar 2020 13:12:30 +0000 Subject: WIP changes to the AST types --- src/Verismith/Verilog/AST.hs | 4 ++-- src/Verismith/Verilog/CodeGen.hs | 30 +++++++++++++------------- src/Verismith/Verilog/Internal.hs | 18 ++++++++-------- src/Verismith/Verilog/Mutate.hs | 42 ++++++++++++++++++------------------- src/Verismith/Verilog/Parser.hs | 44 +++++++++++++++++++-------------------- src/Verismith/Verilog/Quote.hs | 3 ++- 6 files changed, 71 insertions(+), 70 deletions(-) (limited to 'src/Verismith/Verilog') diff --git a/src/Verismith/Verilog/AST.hs b/src/Verismith/Verilog/AST.hs index 9a71022..74c3cfb 100644 --- a/src/Verismith/Verilog/AST.hs +++ b/src/Verismith/Verilog/AST.hs @@ -364,7 +364,7 @@ instance Num Range where -- cumbersome than useful, as a lot of ports can be declared without input and -- output port. -- --- This is now implemented inside 'ModDecl' itself, which uses a list of output +-- This is now implemented inside '(ModDecl ann)' itself, which uses a list of output -- and input ports. data Port = Port { _portType :: !PortType @@ -547,7 +547,7 @@ traverseModConn :: (Applicative f) => (Expr -> f Expr) -> ModConn -> f ModConn traverseModConn f (ModConn e ) = ModConn <$> f e traverseModConn f (ModConnNamed a e) = ModConnNamed a <$> f e -traverseModItem :: (Applicative f) => (Expr -> f Expr) -> ModItem a -> f (ModItem a) +traverseModItem :: (Applicative f) => (Expr -> f Expr) -> (ModItem ann) -> f (ModItem ann) traverseModItem f (ModCA (ContAssign a e)) = ModCA . ContAssign a <$> f e traverseModItem f (ModInst a b e) = ModInst a b <$> sequenceA (traverseModConn f <$> e) diff --git a/src/Verismith/Verilog/CodeGen.hs b/src/Verismith/Verilog/CodeGen.hs index 8dd8f28..f8fce80 100644 --- a/src/Verismith/Verilog/CodeGen.hs +++ b/src/Verismith/Verilog/CodeGen.hs @@ -38,17 +38,17 @@ import Verismith.Verilog.BitVec class Source a where genSource :: a -> Text --- | Map a 'Maybe Statement' to 'Text'. If it is 'Just statement', the generated +-- | Map a 'Maybe (Statement ann)' to 'Text'. If it is 'Just statement', the generated -- statements are returned. If it is 'Nothing', then @;\n@ is returned. -defMap :: Maybe Statement -> Doc a +defMap :: Maybe (Statement ann) -> Doc a defMap = maybe semi statement --- | Convert the 'Verilog' type to 'Text' so that it can be rendered. -verilogSrc :: Verilog -> Doc a +-- | Convert the 'Verilog ann' type to 'Text' so that it can be rendered. +verilogSrc :: (Verilog ann) -> Doc a verilogSrc (Verilog modules) = vsep . punctuate line $ moduleDecl <$> modules --- | Generate the 'ModDecl' for a module and convert it to 'Text'. -moduleDecl :: ModDecl -> Doc a +-- | Generate the 'ModDecl ann' for a module and convert it to 'Text'. +moduleDecl :: ModDecl ann -> Doc a moduleDecl (ModDecl i outP inP items ps) = vsep [ sep ["module" <+> identifier i, params ps, ports <> semi] , indent 2 modI @@ -110,8 +110,8 @@ portDir PortIn = "input" portDir PortOut = "output" portDir PortInOut = "inout" --- | Generate a 'ModItem'. -moduleItem :: ModItem -> Doc a +-- | Generate a '(ModItem ann)'. +moduleItem :: (ModItem ann) -> Doc a moduleItem (ModCA ca ) = contAssign ca moduleItem (ModInst i name conn) = (<> semi) $ hsep [ identifier i @@ -248,11 +248,11 @@ caseType CaseStandard = "case" caseType CaseX = "casex" caseType CaseZ = "casez" -casePair :: CasePair -> Doc a +casePair :: (CasePair ann) -> Doc a casePair (CasePair e s) = vsep [hsep [expr e, colon], indent 2 $ statement s] -statement :: Statement -> Doc a +statement :: Statement ann -> Doc a statement (TimeCtrl d stat) = hsep [delay d, defMap stat] statement (EventCtrl e stat) = hsep [event e, defMap stat] statement (SeqBlock s) = @@ -302,7 +302,7 @@ instance Source Identifier where instance Source Task where genSource = showT . task -instance Source Statement where +instance Source (Statement ann) where genSource = showT . statement instance Source PortType where @@ -329,7 +329,7 @@ instance Source Expr where instance Source ContAssign where genSource = showT . contAssign -instance Source ModItem where +instance Source (ModItem ann) where genSource = showT . moduleItem instance Source PortDir where @@ -338,13 +338,13 @@ instance Source PortDir where instance Source Port where genSource = showT . port -instance Source ModDecl where +instance Source (ModDecl ann) where genSource = showT . moduleDecl -instance Source Verilog where +instance Source (Verilog ann) where genSource = showT . verilogSrc -instance Source SourceInfo where +instance Source (SourceInfo ann) where genSource (SourceInfo _ src) = genSource src newtype GenVerilog a = GenVerilog { unGenVerilog :: a } diff --git a/src/Verismith/Verilog/Internal.hs b/src/Verismith/Verilog/Internal.hs index 0644d95..0ebc626 100644 --- a/src/Verismith/Verilog/Internal.hs +++ b/src/Verismith/Verilog/Internal.hs @@ -32,28 +32,28 @@ import Control.Lens import Data.Text (Text) import Verismith.Verilog.AST -regDecl :: Identifier -> ModItem +regDecl :: Identifier -> (ModItem ann) regDecl i = Decl Nothing (Port Reg False (Range 1 0) i) Nothing -wireDecl :: Identifier -> ModItem +wireDecl :: Identifier -> (ModItem ann) wireDecl i = Decl Nothing (Port Wire False (Range 1 0) i) Nothing -- | Create an empty module. -emptyMod :: ModDecl +emptyMod :: (ModDecl ann) emptyMod = ModDecl "" [] [] [] [] -- | Set a module name for a module declaration. -setModName :: Text -> ModDecl -> ModDecl +setModName :: Text -> (ModDecl ann) -> (ModDecl ann) setModName str = modId .~ Identifier str -- | Add a input port to the module declaration. -addModPort :: Port -> ModDecl -> ModDecl +addModPort :: Port -> (ModDecl ann) -> (ModDecl ann) addModPort port = modInPorts %~ (:) port -addModDecl :: ModDecl -> Verilog -> Verilog +addModDecl :: (ModDecl ann) -> (Verilog ann) -> (Verilog ann) addModDecl desc = _Wrapped %~ (:) desc -testBench :: ModDecl +testBench :: (ModDecl ann) testBench = ModDecl "main" [] @@ -71,7 +71,7 @@ testBench = ModDecl ] [] -addTestBench :: Verilog -> Verilog +addTestBench :: (Verilog ann) -> (Verilog ann) addTestBench = addModDecl testBench defaultPort :: Identifier -> Port @@ -80,7 +80,7 @@ defaultPort = Port Wire False (Range 1 0) portToExpr :: Port -> Expr portToExpr (Port _ _ _ i) = Id i -modName :: ModDecl -> Text +modName :: (ModDecl ann) -> Text modName = getIdentifier . view modId yPort :: Identifier -> Port diff --git a/src/Verismith/Verilog/Mutate.hs b/src/Verismith/Verilog/Mutate.hs index e80437f..260d759 100644 --- a/src/Verismith/Verilog/Mutate.hs +++ b/src/Verismith/Verilog/Mutate.hs @@ -106,7 +106,7 @@ instance Mutate Assign where instance Mutate ContAssign where mutExpr f (ContAssign a e) = ContAssign a $ f e -instance Mutate Statement where +instance Mutate (Statement ann) where mutExpr f (TimeCtrl d s) = TimeCtrl d $ mutExpr f <$> s mutExpr f (EventCtrl e s) = EventCtrl e $ mutExpr f <$> s mutExpr f (SeqBlock s) = SeqBlock $ mutExpr f <$> s @@ -123,7 +123,7 @@ instance Mutate Parameter where instance Mutate LocalParam where mutExpr _ = id -instance Mutate ModItem where +instance Mutate (ModItem ann) where mutExpr f (ModCA (ContAssign a e)) = ModCA . ContAssign a $ f e mutExpr f (ModInst a b conns) = ModInst a b $ mutExpr f conns mutExpr f (Initial s) = Initial $ mutExpr f s @@ -132,13 +132,13 @@ instance Mutate ModItem where mutExpr _ p@ParamDecl{} = p mutExpr _ l@LocalParamDecl{} = l -instance Mutate ModDecl where +instance Mutate (ModDecl ann) where mutExpr f (ModDecl a b c d e) = ModDecl (mutExpr f a) (mutExpr f b) (mutExpr f c) (mutExpr f d) (mutExpr f e) -instance Mutate Verilog where +instance Mutate (Verilog ann) where mutExpr f (Verilog a) = Verilog $ mutExpr f a -instance Mutate SourceInfo where +instance Mutate (SourceInfo ann) where mutExpr f (SourceInfo a b) = SourceInfo a $ mutExpr f b instance Mutate a => Mutate [a] where @@ -150,8 +150,8 @@ instance Mutate a => Mutate (Maybe a) where instance Mutate a => Mutate (GenVerilog a) where mutExpr f (GenVerilog a) = GenVerilog $ mutExpr f a --- | Return if the 'Identifier' is in a 'ModDecl'. -inPort :: Identifier -> ModDecl -> Bool +-- | Return if the 'Identifier' is in a '(ModDecl ann)'. +inPort :: Identifier -> (ModDecl ann) -> Bool inPort i m = inInput where inInput = @@ -159,7 +159,7 @@ inPort i m = inInput -- | Find the last assignment of a specific wire/reg to an expression, and -- returns that expression. -findAssign :: Identifier -> [ModItem] -> Maybe Expr +findAssign :: Identifier -> [ModItem ann] -> Maybe Expr findAssign i items = safe last . catMaybes $ isAssign <$> items where isAssign (ModCA (ContAssign val expr)) | val == i = Just expr @@ -184,7 +184,7 @@ replace = (transform .) . idTrans -- This could be improved by instead of only using the last assignment to the -- wire that one finds, to use the assignment to the wire before the current -- expression. This would require a different approach though. -nestId :: Identifier -> ModDecl -> ModDecl +nestId :: Identifier -> (ModDecl ann) -> (ModDecl ann) nestId i m | not $ inPort i m = let expr = fromMaybe def . findAssign i $ m ^. modItems @@ -196,15 +196,15 @@ nestId i m def = Id i -- | Replaces an identifier by a expression in all the module declaration. -nestSource :: Identifier -> Verilog -> Verilog +nestSource :: Identifier -> (Verilog ann) -> (Verilog ann) nestSource i src = src & getModule %~ nestId i -- | Nest variables in the format @w[0-9]*@ up to a certain number. -nestUpTo :: Int -> Verilog -> Verilog +nestUpTo :: Int -> (Verilog ann) -> (Verilog ann) nestUpTo i src = foldl (flip nestSource) src $ Identifier . fromNode <$> [1 .. i] -allVars :: ModDecl -> [Identifier] +allVars :: (ModDecl ann) -> [Identifier] allVars m = (m ^.. modOutPorts . traverse . portName) <> (m ^.. modInPorts . traverse . portName) @@ -226,7 +226,7 @@ allVars m = -- endmodule -- -- -instantiateMod :: ModDecl -> ModDecl -> ModDecl +instantiateMod :: (ModDecl ann) -> (ModDecl ann) -> (ModDecl ann) instantiateMod m main = main & modItems %~ ((out ++ regIn ++ [inst]) ++) where out = Decl Nothing <$> m ^. modOutPorts <*> pure Nothing @@ -252,7 +252,7 @@ instantiateMod m main = main & modItems %~ ((out ++ regIn ++ [inst]) ++) -- >>> GenVerilog $ instantiateMod_ m -- m m(y, x); -- -instantiateMod_ :: ModDecl -> ModItem +instantiateMod_ :: (ModDecl ann) -> (ModItem ann) instantiateMod_ m = ModInst (m ^. modId) (m ^. modId) conns where conns = @@ -267,7 +267,7 @@ instantiateMod_ m = ModInst (m ^. modId) (m ^. modId) conns -- >>> GenVerilog $ instantiateModSpec_ "_" m -- m m(.y(y), .x(x)); -- -instantiateModSpec_ :: Text -> ModDecl -> ModItem +instantiateModSpec_ :: Text -> (ModDecl ann) -> (ModItem ann) instantiateModSpec_ outChar m = ModInst (m ^. modId) (m ^. modId) conns where conns = zipWith ModConnNamed ids (Id <$> instIds) @@ -288,7 +288,7 @@ filterChar t ids = -- endmodule -- -- -initMod :: ModDecl -> ModDecl +initMod :: (ModDecl ann) -> (ModDecl ann) initMod m = m & modItems %~ ((out ++ inp) ++) where out = Decl (Just PortOut) <$> (m ^. modOutPorts) <*> pure Nothing @@ -301,7 +301,7 @@ makeIdFrom a i = (i <>) . Identifier . ("_" <>) $ showT a -- | Make top level module for equivalence verification. Also takes in how many -- modules to instantiate. -makeTop :: Int -> ModDecl -> ModDecl +makeTop :: Int -> (ModDecl ann) -> (ModDecl ann) makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt [] where ys = yPort . flip makeIdFrom "y" <$> [1 .. i] @@ -311,7 +311,7 @@ makeTop i m = ModDecl (m ^. modId) ys (m ^. modInPorts) modIt [] -- | Make a top module with an assert that requires @y_1@ to always be equal to -- @y_2@, which can then be proven using a formal verification tool. -makeTopAssert :: ModDecl -> ModDecl +makeTopAssert :: (ModDecl ann) -> (ModDecl ann) makeTopAssert = (modItems %~ (++ [assert])) . makeTop 2 where assert = Always . EventCtrl e . Just $ SeqBlock @@ -320,7 +320,7 @@ makeTopAssert = (modItems %~ (++ [assert])) . makeTop 2 -- | Provide declarations for all the ports that are passed to it. If they are -- registers, it should assign them to 0. -declareMod :: [Port] -> ModDecl -> ModDecl +declareMod :: [Port] -> (ModDecl ann) -> (ModDecl ann) declareMod ports = initMod . (modItems %~ (fmap decl ports ++)) where decl p@(Port Reg _ _ _) = Decl Nothing p (Just 0) @@ -374,7 +374,7 @@ removeId i = transform trans | otherwise = Id ident trans e = e -combineAssigns :: Port -> [ModItem] -> [ModItem] +combineAssigns :: Port -> [ModItem ann] -> [ModItem ann] combineAssigns p a = a <> [ ModCA @@ -386,7 +386,7 @@ combineAssigns p a = ] where assigns = a ^.. traverse . modContAssign . contAssignNetLVal -combineAssigns_ :: Bool -> Port -> [Port] -> ModItem +combineAssigns_ :: Bool -> Port -> [Port] -> (ModItem ann) combineAssigns_ comb p ps = ModCA . ContAssign (p ^. portName) diff --git a/src/Verismith/Verilog/Parser.hs b/src/Verismith/Verilog/Parser.hs index a6eaf24..70dc973 100644 --- a/src/Verismith/Verilog/Parser.hs +++ b/src/Verismith/Verilog/Parser.hs @@ -283,7 +283,7 @@ strId = satisfy' matchId identifier :: Parser Identifier identifier = Identifier . T.pack <$> strId -parseNetDecl :: Maybe PortDir -> Parser ModItem +parseNetDecl :: Maybe PortDir -> Parser (ModItem ann) parseNetDecl pd = do t <- option Wire type_ sign <- option False (tok KWSigned $> True) @@ -303,10 +303,10 @@ parsePortDir = <|> tok KWInout $> PortInOut -parseDecl :: Parser ModItem +parseDecl :: Parser (ModItem ann) parseDecl = (Just <$> parsePortDir >>= parseNetDecl) <|> parseNetDecl Nothing -parseConditional :: Parser Statement +parseConditional :: Parser (Statement ann) parseConditional = do expr <- tok' KWIf *> parens parseExpr true <- maybeEmptyStatement @@ -336,7 +336,7 @@ parseAssign t = do expr <- parseExpr return $ Assign lval delay expr -parseLoop :: Parser Statement +parseLoop :: Parser (Statement ann) parseLoop = do a <- tok' KWFor *> tok' SymParenL *> parseAssign SymEq expr <- tok' SymSemi *> parseExpr @@ -373,37 +373,37 @@ parseEvent' = <|> try (fmap EId identifier) <|> try (fmap EExpr parseExpr) -parseEventCtrl :: Parser Statement +parseEventCtrl :: Parser (Statement ann) parseEventCtrl = do event <- parseEvent statement <- option Nothing maybeEmptyStatement return $ EventCtrl event statement -parseDelayCtrl :: Parser Statement +parseDelayCtrl :: Parser (Statement ann) parseDelayCtrl = do delay <- parseDelay statement <- option Nothing maybeEmptyStatement return $ TimeCtrl delay statement -parseBlocking :: Parser Statement +parseBlocking :: Parser (Statement ann) parseBlocking = do a <- parseAssign SymEq tok' SymSemi return $ BlockAssign a -parseNonBlocking :: Parser Statement +parseNonBlocking :: Parser (Statement ann) parseNonBlocking = do a <- parseAssign SymLtEq tok' SymSemi return $ NonBlockAssign a -parseSeq :: Parser Statement +parseSeq :: Parser (Statement ann) parseSeq = do seq' <- tok' KWBegin *> many parseStatement tok' KWEnd return $ SeqBlock seq' -parseStatement :: Parser Statement +parseStatement :: Parser (Statement ann) parseStatement = parseSeq <|> parseConditional @@ -413,14 +413,14 @@ parseStatement = <|> try parseBlocking <|> parseNonBlocking -maybeEmptyStatement :: Parser (Maybe Statement) +maybeEmptyStatement :: Parser (Maybe (Statement ann)) maybeEmptyStatement = (tok' SymSemi >> return Nothing) <|> (Just <$> parseStatement) -parseAlways :: Parser ModItem +parseAlways :: Parser (ModItem ann) parseAlways = tok' KWAlways *> (Always <$> parseStatement) -parseInitial :: Parser ModItem +parseInitial :: Parser (ModItem ann) parseInitial = tok' KWInitial *> (Initial <$> parseStatement) namedModConn :: Parser ModConn @@ -432,7 +432,7 @@ namedModConn = do parseModConn :: Parser ModConn parseModConn = try (fmap ModConn parseExpr) <|> namedModConn -parseModInst :: Parser ModItem +parseModInst :: Parser (ModItem ann) parseModInst = do m <- identifier name <- identifier @@ -440,7 +440,7 @@ parseModInst = do tok' SymSemi return $ ModInst m name modconns -parseModItem :: Parser ModItem +parseModItem :: Parser (ModItem ann) parseModItem = try (ModCA <$> parseContAssign) <|> try parseDecl @@ -451,11 +451,11 @@ parseModItem = parseModList :: Parser [Identifier] parseModList = list <|> return [] where list = parens $ commaSep identifier -filterDecl :: PortDir -> ModItem -> Bool +filterDecl :: PortDir -> (ModItem ann) -> Bool filterDecl p (Decl (Just p') _ _) = p == p' filterDecl _ _ = False -modPorts :: PortDir -> [ModItem] -> [Port] +modPorts :: PortDir -> [ModItem ann] -> [Port] modPorts p mis = filter (filterDecl p) mis ^.. traverse . declPort parseParam :: Parser Parameter @@ -467,7 +467,7 @@ parseParam = do parseParams :: Parser [Parameter] parseParams = tok' SymPound *> parens (commaSep parseParam) -parseModDecl :: Parser ModDecl +parseModDecl :: Parser (ModDecl ann) parseModDecl = do name <- tok KWModule *> identifier paramList <- option [] $ try parseParams @@ -483,7 +483,7 @@ parseModDecl = do -- | Parses a 'String' into 'Verilog' by skipping any beginning whitespace -- and then parsing multiple Verilog source. -parseVerilogSrc :: Parser Verilog +parseVerilogSrc :: Parser (Verilog ann) parseVerilogSrc = Verilog <$> many parseModDecl -- | Parse a 'String' containing verilog code. The parser currently only supports @@ -491,7 +491,7 @@ parseVerilogSrc = Verilog <$> many parseModDecl parseVerilog :: Text -- ^ Name of parsed object. -> Text -- ^ Content to be parsed. - -> Either Text Verilog -- ^ Returns 'String' with error + -> Either Text (Verilog ann) -- ^ Returns 'String' with error -- message if parse fails. parseVerilog s = bimap showT id @@ -500,12 +500,12 @@ parseVerilog s = . preprocess [] (T.unpack s) . T.unpack -parseVerilogFile :: Text -> IO Verilog +parseVerilogFile :: Text -> IO (Verilog ann) parseVerilogFile file = do src <- T.readFile $ T.unpack file case parseVerilog file src of Left s -> error $ T.unpack s Right r -> return r -parseSourceInfoFile :: Text -> Text -> IO SourceInfo +parseSourceInfoFile :: Text -> Text -> IO (SourceInfo ann) parseSourceInfoFile top = fmap (SourceInfo top) . parseVerilogFile diff --git a/src/Verismith/Verilog/Quote.hs b/src/Verismith/Verilog/Quote.hs index 879b8fd..5e1e5dc 100644 --- a/src/Verismith/Verilog/Quote.hs +++ b/src/Verismith/Verilog/Quote.hs @@ -23,6 +23,7 @@ import qualified Language.Haskell.TH as TH import Language.Haskell.TH.Quote import Language.Haskell.TH.Syntax import Verismith.Verilog.Parser +import Verismith.Verilog.AST (Verilog) liftDataWithText :: Data a => a -> Q Exp liftDataWithText = dataToExpQ $ fmap liftText . cast @@ -47,4 +48,4 @@ quoteVerilog s = do v <- case parseVerilog pos (T.pack s) of Right e -> return e Left e -> fail $ show e - liftDataWithText v + liftDataWithText (v :: Verilog ()) -- cgit