> {-# LANGUAGE CPP #-} > module Parser.BSV.CVParserCommon where #if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 804) > import Prelude hiding ((<>)) #endif > import Control.Monad.State > import Control.Monad.Except > import SystemVerilogTokens > import Flags(Flags, passThroughAssertions) > import Data.List > import Data.Maybe > import qualified Data.Set as S > import qualified Data.Map as M > import Debug.Trace(trace) > import Parsec hiding(getPosition) > import Error(internalError, EMsg, WMsg, ErrMsg(..), ErrorHandle) > import Position > import Id > import VModInfo > import SchedInfo > import CSyntax > import CFreeVars > import PreIds > import PreStrings > import PPrint(pparen) > import PVPrint > import CVPrint > import qualified SEMonad > import Pragma > import Util (headOrErr, set_insertMany, toMaybe, apRight) type of the BSV parser > data SV_Parser_State = SV_Parser_State > { errHandle :: ErrorHandle, > warnings :: [WMsg], -- warnings generated by parser, in reverse order > svaWarned :: Bool, -- "SV assertions have been warned about" > parserflags :: Flags -- Command-line flags > } > type SV_Parser result = GenParser SV_Token SV_Parser_State result struct field: identifier and qualified type > data ImperativeStatement = > ISNull > | ISDecl Position IdOrTuple (Maybe CType) [CPred] -- type #(params) variable; > | ISPatEq Position CPat CExpr -- match = > | ISPatBind Position CPat CExpr -- match <- > | ISEqual Position IdOrTuple CExpr -- var = expr; > -- XXX assign var = expr; > | ISUpdate Position CExpr CExpr -- expr.var = expr; expr[expr] = expr This is analogous to Haskell's "<-" in do notation, where we wish to do a something monadic and also get its output value. The canonical right-hand side is an ActionValue. > | ISUpdateBind Position [(Position,PProp)] CExpr CExpr -- expr[expr] <- expr; etc. > | ISUpdateReg Position CExpr CExpr -- expr[expr] <= expr; etc. > | ISRegWrite Position CExpr CExpr -- var <= expr; > | ISBind Position [(Position,PProp)] IdOrTuple CExpr -- var <- expr; > | ISReturn Position (Maybe CExpr) -- return expr; > | ISNakedExpr Position CExpr -- expr; > | ISInst Position -- type #(params) ifc(); > -- mkinst #(params) inst(ifc); > [(Position,PProp)] -- attributes > Id -- ifc name > Id -- instance name > (Maybe CType) -- ifc type > (Maybe CExpr) -- clocked_by expression > (Maybe CExpr) -- reset_by expression > (Maybe CExpr) -- powered_by expression > CExpr -- module expression > | ISFunction Position [Pragma] CDefl -- function .. endfunction > | ISRule Position Id [CSchedulePragma] CRule -- rule .. endrule > | ISMethod Position CDefl -- method .. endmethod > | ISFor Position [ImperativeStatement] -- for (ISs; bool; ISs) body > CExpr > [ImperativeStatement] > [ImperativeStatement] > | ISWhile Position CExpr [ImperativeStatement] > | ISBeginEnd Position [ImperativeStatement] -- interior nested blocks > | ISAction Position [ImperativeStatement] -- interior nested blocks > | ISActionValue Position [ImperativeStatement] -- interior nested blocks > -- if: conditions, consequent, alternative (alternative is Nothing > -- if there is no else branch) > | ISIf Position [CQual] [ImperativeStatement] (Maybe [ImperativeStatement]) > -- verilog-style case: subject, [(test, consequent)], default > | ISCase Position CExpr [ISCaseArm] (Maybe ISCaseDefault) > -- pattern-match case: subject, [(pattern, consequent)], default > | ISCaseTagged Position CExpr [ISCaseTaggedArm] (Maybe ISCaseTaggedDefault) StmtFSM (only) > | ISSeq Position [ImperativeStatement] -- nested sequential statements > | ISPar Position [ImperativeStatement] -- nested parallel statements > | ISAbtIf Position [CQual] [ImperativeStatement] (Maybe [ImperativeStatement]) > | ISRepeat Position CExpr [ImperativeStatement] -- repeat loop > | ISBreak Position -- break in loop > | ISContinue Position -- continue in loop > | ISGoto Position Id > | ISLabel Position Id > | ISNamed Position Id [ImperativeStatement] -- only 0 or 1 stmt Assertions > | ISSequence Position SVA_Sequence --sequence .. endsequence > | ISProperty Position SVA_Property --property .. endpropery > | ISAssertStmt Position SVA_Statement --assert, assume, cover, expect combined declaration/assignment > | ISTypedef Position [CDefn] > | ISModule Position Id (Maybe Pragma) CQType CClause > | ISForeignModule Position Id CQType CClause [Pragma] > -- def = CDef name modType [defClause] > | ISForeignFunction Position Id Id CQType > | ISInterface Position IdK [IfcPragma] [Id] CFields > -- interface #(params) name; methods; endinterface > -- return [Cstruct True SInterface name params methods []] > | ISTypeclass Position IdK [CPred] [([Id],[Id])] [Id] CFields > -- return [Cclass False context name params dependencies functions] > | ISTypeclassInstance Position CQType [CDefl] > | ISImport Position [Id] -- imported packages > | ISExport Position [CExport] -- exported identifiers > | ISBVI Position BVIStmt -- statement specific to import "BVI" modules classic definitions in BSV files > | ISClassicDefns Position [CDefn] -- classic definitions > deriving (Show) ISEqual and ISBind (and thus the ISDecl that gets created with them) are used in two situations: assigning to a single identifier or assigning to a tuple of identifiers. The following type is used represent both cases: Right for a single name, Left for a tuple. The tuple pattern can include a don't-care pattern (.*) so we use an Either to indicate which positions are ignored (Right for names, Left for ignored). The position of the don't-care is recorded in case it's necessary (although it might be sufficient to just include a single position for the start of the tuple). > type IdOrTuple = Either [Either Position Id] Id > mapIdOrTuple :: (Id -> Id) -> IdOrTuple -> IdOrTuple > mapIdOrTuple f (Right i) = Right (f i) > mapIdOrTuple f (Left mis) = Left (map (apRight f) mis) > mapIdOrTupleM :: (Monad m) => (Id -> m Id) -> IdOrTuple -> m IdOrTuple > mapIdOrTupleM f (Right i) = Right <$> f i > mapIdOrTupleM f (Left mis) = Left <$> mapM f' mis > where f' (Right i) = Right <$> f i > f' mi = return mi > mapIdOrTupleM_ :: (Monad m) => (Id -> m a) -> IdOrTuple -> m () > -- mapIdOrTupleM_ f vs = mapIdOrTupleM f vs >> return () > mapIdOrTupleM_ f (Right i) = f i >> return () > mapIdOrTupleM_ f (Left mis) = mapM_ f' mis >> return () > where f' (Right i) = f i >> return () > f' mi = return () > getIdOrTupleNames :: IdOrTuple -> [Id] > getIdOrTupleNames (Right i) = [i] > getIdOrTupleNames (Left mis) = [ i | (Right i) <- mis ] > getIdOrTuplePosition :: IdOrTuple -> Position > getIdOrTuplePosition (Right i) = getPosition i > getIdOrTuplePosition (Left (mi:_)) = > case mi of > Right i -> getPosition i > Left pos -> pos > getIdOrTuplePosition (Left []) = internalError "getIdOrTuplePosition" > mkIdOrTupleCPat :: Position -> IdOrTuple -> CPat > mkIdOrTupleCPat pos (Right i) = CPVar i > mkIdOrTupleCPat pos (Left mis) = pMkTuple pos $ map f mis > where f (Right i) = CPVar i > f (Left p) = CPAny p Note: the order of the clauses in the following declaration is important, as the list of statements is sorted in CVParserImperative, which then assumes that they will turn up in this order. > data BVIStmt = > BVI_default_clock Id > | BVI_default_reset Id > | BVI_input_clock InputClockInf > | BVI_output_clock OutputClockInf > | BVI_ancestor (Id, Id) > | BVI_family (Id, Id) > | BVI_input_reset ResetInf > | BVI_output_reset ResetInf > | BVI_arg (VArgInfo, CExpr, Bool) -- Bool says "bind, rather than eq" > | BVI_method (Id,VFieldInfo, Bool) > -- Id is short name; prefixed name is used in second component > -- Bool says "separate READY method required" > | BVI_interface (Id, Id, [ImperativeStatement]) -- Ids are name, type-constructor > -- stmts are all sub-interfaces, methods, output_clock, output_reset > | BVI_schedule ([Id], MethodConflictOp, [Id]) > | BVI_path (VName, VName) > | BVI_unsync [Id] -- for internal use only > deriving (Show) ========== ASSERTIONS > data SVA_SP = > SVA_SP_DelayU SVA_Delay [SVA_SP] SVA_SP --the backwards order plays nicer with parsec. > | SVA_SP_Delay SVA_Delay [SVA_SP] SVA_SP SVA_SP > | SVA_SP_Throughout SVA_SP SVA_SP > | SVA_SP_Within SVA_SP SVA_SP > | SVA_SP_Intersect SVA_SP SVA_SP > | SVA_SP_Not SVA_SP > | SVA_SP_And SVA_SP SVA_SP > | SVA_SP_Or SVA_SP SVA_SP > | SVA_SP_If CExpr SVA_SP (Maybe SVA_SP) > | SVA_SP_Implies SVA_SP SVA_SP > | SVA_SP_ImpliesD SVA_SP SVA_SP > -- Above are operators in descending binding order; below are primitives: > | SVA_SP_Expr CExpr SVA_REP > | SVA_SP_Parens SVA_SP SVA_REP > | SVA_SP_Match SVA_SP [[ImperativeStatement]] SVA_REP > | SVA_SP_FirstMatch SVA_SP [[ImperativeStatement]] SVA_REP > deriving (Show) > type SVA_Sequence = (Id, [(Maybe CType, Id)], [CPred], [[ImperativeStatement]], SVA_SP) > data SVA_SEQ = > SVA_SEQ_DelayU SVA_Delay [SVA_SEQ] SVA_SEQ --the backwards order plays nicer with parsec. > | SVA_SEQ_Delay SVA_Delay [SVA_SEQ] SVA_SEQ SVA_SEQ > | SVA_SEQ_Expr CExpr SVA_REP > | SVA_SEQ_Match SVA_SEQ [[ImperativeStatement]] SVA_REP > | SVA_SEQ_Or SVA_SEQ SVA_SEQ > | SVA_SEQ_And SVA_SEQ SVA_SEQ > | SVA_SEQ_Intersect SVA_SEQ SVA_SEQ > | SVA_SEQ_Within SVA_SEQ SVA_SEQ > | SVA_SEQ_Throughout SVA_SEQ SVA_SEQ > | SVA_SEQ_Parens SVA_SEQ SVA_REP > | SVA_SEQ_FirstMatch SVA_SEQ [[ImperativeStatement]] SVA_REP > deriving (Show) > type SVA_Property = (Id, [(Maybe CType, Id)], [CPred], [[ImperativeStatement]], SVA_SP) > -- name parameters provisos var decls body > data SVA_PROP = > SVA_PROP_Seq SVA_SEQ > | SVA_PROP_Not SVA_PROP > | SVA_PROP_Or SVA_PROP SVA_PROP > | SVA_PROP_And SVA_PROP SVA_PROP > | SVA_PROP_Implies SVA_SEQ SVA_PROP > | SVA_PROP_ImpliesD SVA_SEQ SVA_PROP > | SVA_PROP_If CExpr SVA_PROP (Maybe SVA_PROP) > deriving (Show) > data SVA_REP = > SVA_REP_None > | SVA_REP_Cons SVA_Delay > | SVA_REP_NonCons SVA_Delay > | SVA_REP_Goto SVA_Delay > deriving (Show) > instance HasPosition SVA_REP where > getPosition (SVA_REP_None) = noPosition > getPosition (SVA_REP_NonCons d) = getPosition d > getPosition (SVA_REP_Cons d) = getPosition d > getPosition (SVA_REP_Goto d)= getPosition d > data SVA_Delay = > SVA_Delay_Unbound CExpr > | SVA_Delay_Range CExpr CExpr > | SVA_Delay_Const CExpr > deriving (Show) > instance HasPosition SVA_Delay where > getPosition (SVA_Delay_Unbound e) = getPosition e > getPosition (SVA_Delay_Range e1 e2) = getPosition e1 > getPosition (SVA_Delay_Const e) = getPosition e > type SVA_Statement = (Bool, SVA_STMT) --False == initial, True == always > data SVA_STMT = > SVA_STMT_Assert (Maybe Id) SVA_SP [ImperativeStatement] [ImperativeStatement] > | SVA_STMT_Assume (Maybe Id) SVA_SP > | SVA_STMT_Cover (Maybe Id) SVA_SP [ImperativeStatement] > | SVA_STMT_Expect (Maybe Id) SVA_SP [ImperativeStatement] [ImperativeStatement] > deriving (Show) > instance PVPrint SVA_SEQ where > pvPrint d p (SVA_SEQ_DelayU del rest seq) = > text "##" <> > pvPrint d 0 del <+> > pvPrint d 0 seq <+> > sep (map (pvPrint d 0) rest) > pvPrint d p (SVA_SEQ_Delay del rest s1 s2) = > pvPrint d 0 s1 <+> > text "##" <> > pvPrint d 0 del <+> > pvPrint d 0 s2 <+> > sep (map (pvPrint d 0) rest) > pvPrint d p (SVA_SEQ_Expr exp rep) = > pvPrint d 0 exp <+> pvPrint d 0 rep > pvPrint d p (SVA_SEQ_Match seq asns rep) = > text "(" <> > pvPrint d 0 seq <> > text "," <+> > sep (map (pvPrint d 0) asns) <> > text ")" > pvPrint d p (SVA_SEQ_Or s1 s2) = > pparen (p > 0) $ > pvPrint d 0 s1 <+> > text "or" <+> > pvPrint d 1 s2 > pvPrint d p (SVA_SEQ_And s1 s2) = > pparen (p > 1) $ > pvPrint d 1 s1 <+> > text "and" <+> > pvPrint d 2 s2 > pvPrint d p (SVA_SEQ_Intersect s1 s2) = > pparen (p > 2) $ > pvPrint d 2 s1 <+> > text "intersect" <+> > pvPrint d 3 s2 > pvPrint d p (SVA_SEQ_Within s1 s2) = > pparen (p > 3) $ > pvPrint d 3 s1 <+> > text "within" <+> > pvPrint d 4 s2 > pvPrint d p (SVA_SEQ_Throughout s1 s2) = > pparen (p > 4) $ > pvPrint d 5 s1 <+> > text "throughout" <+> > pvPrint d 4 s2 > pvPrint d p (SVA_SEQ_FirstMatch seq [] rep) = > text "first_match(" <> > pvPrint d 0 seq <> > text ")" <+> > pvPrint d 0 rep > pvPrint d p (SVA_SEQ_FirstMatch seq asns rep) = > text "first_match(" <> > pvPrint d 0 seq <> > text "," <+> > sep (map (pvPrint d 0) asns) <> > text ")" <+> > pvPrint d 0 rep > pvPrint d p (SVA_SEQ_Parens seq rep) = > text "(" <> > pvPrint d 0 seq <> > text ")" <+> > pvPrint d 0 rep > instance PVPrint SVA_PROP where > pvPrint d p (SVA_PROP_Seq seq) = pparen (p > 0) $ pvPrint d p seq > pvPrint d p (SVA_PROP_Not prop) = > text "not" <+> pvPrint d 1 prop > pvPrint d p (SVA_PROP_And p1 p2) = > pparen (p > 3) $ sep [pvPrint d 3 p1, text "and", pvPrint d 4 p2] > pvPrint d p (SVA_PROP_Or p1 p2) = > pparen (p > 2) $ sep [pvPrint d 2 p1, text "or", pvPrint d 3 p2] > pvPrint d p (SVA_PROP_If e p1 Nothing) = > pparen (p > 1) $ sep [text "if", pvPrint d 1 p1] > pvPrint d p (SVA_PROP_If e p1 (Just p2)) = > pparen (p > 1) $ sep [text "if", pvPrint d 1 p1, pvPrint d 1 p1] > pvPrint d p (SVA_PROP_Implies p1 p2) = > pparen (p > 0) $ sep [pvPrint d 1 p1, text "|->", pvPrint d 0 p2] > pvPrint d p (SVA_PROP_ImpliesD p1 p2) = > pparen (p > 0) $ sep [pvPrint d 1 p1, text "|=>", pvPrint d 0 p2] > instance PVPrint SVA_SP where > pvPrint d p (SVA_SP_DelayU del rest seq) = > text "##" <> > pvPrint d 0 del <+> > pvPrint d 0 seq <+> > sep (map (pvPrint d 0) rest) > pvPrint d p (SVA_SP_Delay del rest s1 s2) = > pvPrint d 0 s1 <+> > text "##" <> > pvPrint d 0 del <+> > pvPrint d 0 s2 <+> > sep (map (pvPrint d 0) rest) > pvPrint d p (SVA_SP_Expr exp rep) = > pvPrint d 0 exp <+> pvPrint d 0 rep > pvPrint d p (SVA_SP_Match seq asns rep) = > text "(" <> > pvPrint d 0 seq <> > text "," <+> > sep (map (pvPrint d 0) asns) <> > text ")" > pvPrint d p (SVA_SP_Or s1 s2) = > pparen (p > 0) $ > pvPrint d 0 s1 <+> > text "or" <+> > pvPrint d 1 s2 > pvPrint d p (SVA_SP_And s1 s2) = > pparen (p > 1) $ > pvPrint d 1 s1 <+> > text "and" <+> > pvPrint d 2 s2 > pvPrint d p (SVA_SP_Intersect s1 s2) = > pparen (p > 2) $ > pvPrint d 2 s1 <+> > text "intersect" <+> > pvPrint d 3 s2 > pvPrint d p (SVA_SP_Within s1 s2) = > pparen (p > 3) $ > pvPrint d 3 s1 <+> > text "within" <+> > pvPrint d 4 s2 > pvPrint d p (SVA_SP_Throughout s1 s2) = > pparen (p > 4) $ > pvPrint d 5 s1 <+> > text "throughout" <+> > pvPrint d 4 s2 > pvPrint d p (SVA_SP_FirstMatch seq [] rep) = > text "first_match(" <> > pvPrint d 0 seq <> > text ")" <+> > pvPrint d 0 rep > pvPrint d p (SVA_SP_FirstMatch seq asns rep) = > text "first_match(" <> > pvPrint d 0 seq <> > text "," <+> > sep (map (pvPrint d 0) asns) <> > text ")" <+> > pvPrint d 0 rep > pvPrint d p (SVA_SP_Parens seq rep) = > text "(" <> > pvPrint d 0 seq <> > text ")" <+> > pvPrint d 0 rep > -- pvPrint d p (SVA_SP_Seq seq) = pparen (p > 0) $ pvPrint d p seq > pvPrint d p (SVA_SP_Not prop) = > text "not" <+> pvPrint d 1 prop > pvPrint d p (SVA_SP_If e p1 Nothing) = > pparen (p > 1) $ sep [text "if", pvPrint d 1 p1] > pvPrint d p (SVA_SP_If e p1 (Just p2)) = > pparen (p > 1) $ sep [text "if", pvPrint d 1 p1, pvPrint d 1 p1] > pvPrint d p (SVA_SP_Implies p1 p2) = > pparen (p > 0) $ sep [pvPrint d 1 p1, text "|->", pvPrint d 0 p2] > pvPrint d p (SVA_SP_ImpliesD p1 p2) = > pparen (p > 0) $ sep [pvPrint d 1 p1, text "|=>", pvPrint d 0 p2] > instance PVPrint SVA_REP where > pvPrint d p (SVA_REP_None) = empty > pvPrint d p (SVA_REP_Cons del) = > sep [text "[*", pvPrint d p del, text "]"] > pvPrint d p (SVA_REP_NonCons del) = > sep [text "[=", pvPrint d p del, text "]"] > pvPrint d p (SVA_REP_Goto del) = > sep [text "[->", pvPrint d p del, text "]"] > instance PVPrint SVA_Delay where > pvPrint d p (SVA_Delay_Unbound expr) = > pvPrint d p expr <> text ":$" > pvPrint d p (SVA_Delay_Range e1 e2) = > pvPrint d p e1 <> text ":" <> pvPrint d p e2 > pvPrint d p (SVA_Delay_Const expr) = > pvPrint d p expr > withId :: PDetail -> Maybe Id -> Doc > withId _ Nothing = empty > withId d (Just nm) = pvPrint d 0 nm <> text ": " > instance PVPrint SVA_STMT where > pvPrint d p (SVA_STMT_Assert mid prop [] []) = > pparen (p > 0) $ > sep [withId d mid <> text "assert property", parens (pvPrint d 0 prop)] > pvPrint d p (SVA_STMT_Assert Nothing prop pass []) = > pparen (p > 0) $ sep [text "assert property", parens (pvPrint d 0 prop), > nest 4 (pvBlock d 0 pass)] > pvPrint d p (SVA_STMT_Assert Nothing prop [] fail) = > pparen (p > 0) $ sep [text "assert property", parens (pvPrint d 0 prop), > text "else", nest 4 (pvBlock d 0 fail)] > pvPrint d p (SVA_STMT_Assert Nothing prop pass fail) = > pparen (p > 0) $ sep [text "assert property", parens (pvPrint d 0 prop), > nest 4 (pvBlock d 0 pass), > text "else", nest 4 (pvBlock d 0 fail)] > pvPrint d p (SVA_STMT_Assert (Just nm) prop pass []) = > pparen (p > 0) $ sep [pvPrint d 0 nm <> > text ": assert property", parens (pvPrint d 0 prop), > nest 4 (pvBlock d 0 pass)] > pvPrint d p (SVA_STMT_Assert (Just nm) prop [] fail) = > pparen (p > 0) $ sep [pvPrint d 0 nm <> > text ": assert property", parens (pvPrint d 0 prop), > text "else", nest 4 (pvBlock d 0 fail)] > pvPrint d p (SVA_STMT_Assert (Just nm) prop pass fail) = > pparen (p > 0) $ sep [pvPrint d 0 nm <> > text ": assert property", parens (pvPrint d 0 prop), > nest 4 (pvBlock d 0 pass), > text "else", nest 4 (pvBlock d 0 fail)] > pvPrint d p (SVA_STMT_Assume mid prop) = > pparen (p > 0) $ sep [withId d mid <> text "assume property", parens (pvPrint d 0 prop)] > pvPrint d p (SVA_STMT_Cover mid prop []) = > pparen (p > 0) $ sep [withId d mid <> text "cover property", parens (pvPrint d 0 prop)] > pvPrint d p (SVA_STMT_Cover mid prop pass) = > pparen (p > 0) $ sep [withId d mid <> text "cover property", parens (pvPrint d 0 prop), > nest 4 (pvBlock d 0 pass)] > pvPrint d p (SVA_STMT_Expect mid prop [] []) = > pparen (p > 0) $ sep [withId d mid <> text "expect" <+> parens (pvPrint d 0 prop)] > pvPrint d p (SVA_STMT_Expect mid prop pass []) = > pparen (p > 0) $ sep [withId d mid <> text "expect" <+> parens (pvPrint d 0 prop), > nest 4 (pvBlock d 0 pass)] > pvPrint d p (SVA_STMT_Expect mid prop [] fail) = > pparen (p > 0) $ sep [withId d mid <> text "expect" <+> parens (pvPrint d 0 prop), > text "else", nest 4 (pvBlock d 0 fail)] > pvPrint d p (SVA_STMT_Expect mid prop pass fail) = > pparen (p > 0) $ sep [withId d mid <> text "expect" <+> parens (pvPrint d 0 prop), > nest 4 (pvBlock d 0 pass), > text "else", nest 4 (pvBlock d 0 fail)] De-Sugaring The following functions convert from the full data-type to the temporal logic core. In this form the following data types will be used: > data SVA_CORE_SEQ = > SVA_CORE_SEQ_Expr CExpr > | SVA_CORE_SEQ_Asgn [ImperativeStatement] > | SVA_CORE_SEQ_Concat SVA_CORE_SEQ SVA_CORE_SEQ > | SVA_CORE_SEQ_Fuse SVA_CORE_SEQ SVA_CORE_SEQ > | SVA_CORE_SEQ_Or SVA_CORE_SEQ SVA_CORE_SEQ > | SVA_CORE_SEQ_Intersect SVA_CORE_SEQ SVA_CORE_SEQ > | SVA_CORE_SEQ_FirstMatch SVA_CORE_SEQ > | SVA_CORE_SEQ_Null SVA_CORE_SEQ > | SVA_CORE_SEQ_Unbound SVA_CORE_SEQ > | SVA_CORE_SEQ_Rep SVA_CORE_SEQ SVA_REP > | SVA_CORE_SEQ_Delay SVA_Delay [SVA_CORE_SEQ] SVA_CORE_SEQ SVA_CORE_SEQ > deriving (Show) > data SVA_CORE_PROP = > SVA_CORE_PROP_Seq SVA_CORE_SEQ > | SVA_CORE_PROP_Not SVA_CORE_PROP > | SVA_CORE_PROP_Or SVA_CORE_PROP SVA_CORE_PROP > | SVA_CORE_PROP_And SVA_CORE_PROP SVA_CORE_PROP > | SVA_CORE_PROP_Implies SVA_CORE_SEQ SVA_CORE_PROP > deriving (Show) > instance PVPrint SVA_CORE_SEQ where > pvPrint d p (SVA_CORE_SEQ_Concat s1 s2) = > pvPrint d 0 s1 <+> > text "##1 " <> > pvPrint d 0 s2 > pvPrint d p (SVA_CORE_SEQ_Fuse s1 s2) = > pvPrint d 0 s1 <+> > text "##0 " <> > pvPrint d 0 s2 > pvPrint d p (SVA_CORE_SEQ_Expr exp) = > pvPrint d 0 exp > pvPrint d p (SVA_CORE_SEQ_Asgn asns) = > text "(1, " <> > sep (map (pvPrint d 0) asns) <> > text ") " > pvPrint d p (SVA_CORE_SEQ_Or s1 s2) = > pparen (p > 0) $ > pvPrint d 0 s1 <+> > text "or" <+> > pvPrint d 1 s2 > pvPrint d p (SVA_CORE_SEQ_Intersect s1 s2) = > pparen (p > 2) $ > pvPrint d 2 s1 <+> > text "intersect" <+> > pvPrint d 3 s2 > pvPrint d p (SVA_CORE_SEQ_FirstMatch seq) = > text "first_match(" <> > pvPrint d 0 seq <> > text ") " > pvPrint d p (SVA_CORE_SEQ_Null seq) = > pvPrint d 0 seq <> > text " [*0] " > pvPrint d p (SVA_CORE_SEQ_Unbound seq) = > pvPrint d 0 seq <> > text " [*1:$] " > pvPrint d p (SVA_CORE_SEQ_Delay del rest s1 s2) = > pvPrint d 0 s1 <+> > text "##" <> > pvPrint d 0 del <+> > pvPrint d 0 s2 <+> > sep (map (pvPrint d 0) rest) > pvPrint d p (SVA_CORE_SEQ_Rep exp rep) = > pvPrint d 0 exp <+> pvPrint d 0 rep > instance PVPrint SVA_CORE_PROP where > pvPrint d p (SVA_CORE_PROP_Seq seq) = pparen (p > 0) $ pvPrint d p seq > pvPrint d p (SVA_CORE_PROP_Not prop) = > text "not" <+> pvPrint d 1 prop > pvPrint d p (SVA_CORE_PROP_And p1 p2) = > pparen (p > 3) $ sep [pvPrint d 3 p1, text "and", pvPrint d 4 p2] > pvPrint d p (SVA_CORE_PROP_Or p1 p2) = > pparen (p > 2) $ sep [pvPrint d 2 p1, text "or", pvPrint d 3 p2] > pvPrint d p (SVA_CORE_PROP_Implies p1 p2) = > pparen (p > 0) $ sep [pvPrint d 1 p1, text "|->", pvPrint d 0 p2] END ASSERTIONS > pvBlock :: PVPrint a => PDetail -> Int -> [a] -> Doc > pvBlock d p [] = text "" > pvBlock d p [stmt] = pvPrint d p stmt > pvBlock d p stmts = > pparen (p>0) $ > sep [text "begin", nest 4 (sep (map (pvPrint d 0) stmts)), text "end"] expressions are conditions for this arm > type ISCaseArm = (Position, [CExpr], [ImperativeStatement]) > type ISCaseDefault = (Position, [ImperativeStatement]) pattern guards this arm; expressions are additional conditions > type ISCaseTaggedArm = (Position, CPat, [CExpr], [ImperativeStatement]) > type ISCaseTaggedDefault = ISCaseDefault > instance PVPrint ImperativeStatement where > pvPrint d p ISNull = text"" > pvPrint d p (ISDecl _ var Nothing _) = > pparen (p > 0) $ text "let " <+> pvPrint d 0 var > pvPrint d p (ISDecl _ var (Just typ) []) = > pparen (p > 0) $ pvPrint d 0 typ <+> pvPrint d 0 var > pvPrint d p (ISDecl _ var (Just typ) ps) = > pparen (p > 0) $ pvPrint d 0 typ <+> pvPrint d 0 var $+$ pvPreds d ps > pvPrint d p (ISPatEq _ pat exp) = > pparen (p > 0) $ text "match" <+> pvPrint d 0 pat <+> text"=" <+> pvPrint d 0 exp > pvPrint d p (ISPatBind _ pat exp) = > pparen (p > 0) $ text "match" <+> pvPrint d 0 pat <+> text"<-" <+> pvPrint d 0 exp > pvPrint d p (ISEqual _ var expr) = > pparen (p > 0) $ pvPrint d 0 var <+> text "=" <+> pvPrint d 0 expr > pvPrint d p (ISUpdate _ e1 expr) = > pparen (p > 0) $ pvPrint d 0 e1 <> > text " =" <+> pvPrint d 0 expr > pvPrint d p (ISUpdateReg _ e1 expr) = > pparen (p > 0) $ pvPrint d 0 e1 <> > text " <=" <+> pvPrint d 0 expr > pvPrint d p (ISUpdateBind _ pprops e1 expr) = > pparen (p > 0) $ sep [pvPrint d 0 pprops, > pvPrint d 0 e1 <> > text " <-" <+> pvPrint d 0 expr] > pvPrint d p (ISRegWrite _ reg expr) = > pparen (p > 0) $ pvPrint d 0 reg <+> text "<=" <+> pvPrint d 0 expr > pvPrint d p (ISBind _ pprops var expr) = > pparen (p > 0) $ sep [pvPrint d 0 pprops, > pvPrint d 0 var <+> text "<-" <+> pvPrint d 0 expr] > pvPrint d p (ISReturn _ (Just expr)) = > pparen (p > 0) $ text "return" <+> pvPrint d p expr > pvPrint d p (ISReturn _ Nothing) = > pparen (p > 0) $ text "return" > pvPrint d p (ISNakedExpr _ expr) = pvPrint d p expr > pvPrint d p (ISInst _ pprops ifcName instName maybeTyp maybeCk maybeRt maybePr expr) = > pparen (p > 0) $ sep [pvPrint d 0 pprops, > if isNothing maybeTyp then text "let " > else pvPrint d 0 (fromJust maybeTyp) > <+> pvPrint d 0 ifcName <> text "();", > pvPrint d 0 expr <+> pvPrint d 0 instName <> text "(" <> > (if isNothing maybeCk > then empty > else (pvPrint d 0 (fromJust maybeCk) <> text ", ")) <> > (if isNothing maybeRt > then empty > else (pvPrint d 0 (fromJust maybeRt) <> text ", ")) <> > (if isNothing maybePr > then empty > else (pvPrint d 0 (fromJust maybePr) <> text ", ")) <> > pvPrint d 0 ifcName <> text ")"] > pvPrint d p (ISFunction pos pragmas def) = > -- XXX like ISModule and ISRule, we don't print pragmas > --sep (map pvPrint pragmas) $+$ > pvPrint d p def > pvPrint d p (ISRule _ _ [] rule) = > pvPrint d p rule > pvPrint d p (ISRule _ _ ps rule) = > pvPrint d p (Crules ps [rule]) > pvPrint d p (ISMethod _ def) = pvPrint d p def > pvPrint d p (ISRepeat _ e ss) = > pparen (p>0) $ sep (((text"repeat (" <> pvPrint d 0 e <> text") begin") > : (map (pvPrint d 0) ss)) ++ [text"end"]) > pvPrint d p (ISWhile _ e ss) = > pparen (p>0) $ sep (((text"while (" <> pvPrint d 0 e <> text") begin") > : (map (pvPrint d 0) ss)) ++ [text"end"]) > pvPrint d p (ISFor _ inis e incs ss) = > pparen (p>0) $ sep (((text"for (" <> > (sep (intersperse (text ",") (map (pvPrint d 0) inis))) <> text ";" <+> > (pvPrint d 0 e) <> text ";" <+> > (sep (intersperse (text ",") (map (pvPrint d 0) incs))) <> text") begin") > : (map (pvPrint d 0) ss)) ++ [text"end"]) > pvPrint d p (ISBeginEnd _ stmts) = > pparen (p>0) $ sep [text "begin", nest 4 (sep (map (pvPrint d 0) stmts)), text "end"] > pvPrint d p (ISSeq _ stmts) = > pparen (p>0) $ sep [text "seq", nest 4 (sep (map (pvPrint d 0) stmts)), text "endseq"] > pvPrint d p (ISPar _ stmts) = > pparen (p>0) $ sep [text "par", nest 4 (sep (map (pvPrint d 0) stmts)), text "endpar"] > pvPrint d p (ISGoto _ id) = > pparen (p>0) $ sep [text "goto " <> (pvPrint d 0 id)] > pvPrint d p (ISLabel _ id) = > pparen (p>0) $ sep [text "label " <> (pvPrint d 0 id)] > pvPrint d p (ISNamed _ id stmts) = > pparen (p>0) $ sep [text "named", nest 4 (sep (map (pvPrint d 0) stmts)), text "endnamed"] > pvPrint d p (ISAction _ stmts) = > pparen (p>0) $ sep [text "action", nest 4 (sep (map (pvPrint d 0) stmts)), text "endaction"] > pvPrint d p (ISActionValue _ stmts) = > pparen (p>0) $ sep [text "actionvalue", nest 4 (sep (map (pvPrint d 0) stmts)), text "endactionvalue"] > pvPrint d p (ISIf pos conds conseq Nothing) = > pparen (p>0) $ sep [text "if" <+> parens pConds, nest 4 (pvpStmts conseq)] > where pvpStmts [stmt] = pvPrint d 0 stmt > pvpStmts stmts = pvPrint d 0 (ISBeginEnd pos stmts) > pConds = sep (intersperse (text "&&") (map (pvPrint d 0) conds)) > pvPrint d p (ISIf pos conds conseq (Just alternative)) = > pparen (p>0) $ sep [text "if" <+> parens pConds, nest 4 (pvpStmts conseq), > text "else", nest 4 (pvpStmts alternative)] > where pvpStmts [stmt] = pvPrint d 0 stmt > pvpStmts stmts = pvPrint d 0 (ISBeginEnd pos stmts) > pConds = sep (intersperse (text "&&") (map (pvPrint d 0) conds)) > pvPrint d p (ISAbtIf pos conds conseq Nothing) = > pparen (p>0) $ sep [text "abortif" <+> parens pConds, nest 4 (pvpStmts conseq)] > where pvpStmts [stmt] = pvPrint d 0 stmt > pvpStmts stmts = pvPrint d 0 (ISBeginEnd pos stmts) > pConds = sep (intersperse (text "&&") (map (pvPrint d 0) conds)) > pvPrint d p (ISAbtIf pos conds conseq (Just alternative)) = > pparen (p>0) $ sep [text "abortif" <+> parens pConds, nest 4 (pvpStmts conseq), > text "with", nest 4 (pvpStmts alternative)] > where pvpStmts [stmt] = pvPrint d 0 stmt > pvpStmts stmts = pvPrint d 0 (ISBeginEnd pos stmts) > pConds = sep (intersperse (text "&&") (map (pvPrint d 0) conds)) > pvPrint d p (ISCase pos subject arms dflt) = > pparen (p>0) $ sep [text "case" <+> parens (pvPrint d 0 subject), > nest 4 pArms, > text "endcase"] > where pArm (pos, conds, stmts) = > sep [sep (intersperse (text "&&") [pvPrint d 0 cond | cond <- conds]) <> colon, > nest 4 (sep (map (pvPrint d 0) stmts))] > pDflt Nothing = empty > pDflt (Just (pos, stmts)) = sep [text "default" <> colon, > nest 4 (sep (map (pvPrint d 0) stmts))] > pArms = foldr ($+$) (pDflt dflt) (map pArm arms) > pvPrint d p (ISCaseTagged pos subject arms dflt) = > pparen (p>0) $ sep [text "case" <+> parens (pvPrint d 0 subject) <+> text "matches", > nest 4 pArms, > text "endcase"] > where pArm (pos, pat, [], stmts) = sep [pvPrint d 0 pat <> colon, > nest 4 (sep (map (pvPrint d 0) stmts))] > pArm (pos, pat, conds, stmts) = > sep [pvPrint d 0 pat <+> text "&&" <+> pvPrint d 0 conds <> colon, > nest 4 (sep (map (pvPrint d 0) stmts))] > pDflt Nothing = empty > pDflt (Just (pos, stmts)) = sep [text "default" <> colon, > nest 4 (sep (map (pvPrint d 0) stmts))] > pArms = foldr ($+$) (pDflt dflt) (map pArm arms) > pvPrint d p (ISModule pos nm prag typ clause) = > pparen (p>0) $ sep [text "module" <+> pvPrint d 0 nm <> text ";", nest 4 (pvPrint d 0 clause), text "endmodule"] > pvPrint d p (ISBreak _) = text "break" > pvPrint d p (ISContinue _) = text "continue" > pvPrint d p (ISSequence pos seq) = pvPrint d p seq > pvPrint d p (ISProperty pos prop) = pvPrint d p prop > pvPrint d p (ISAssertStmt pos as) = pvPrint d p as > pvPrint _ _ istmt = internalError $ "CVParserCommon.PVPrint(ImperativeStatement).pvPrint: " ++ show istmt > structVar :: CExpr -> Maybe Id > structVar (CVar v) = Just v > structVar (CSelect e _) = structVar e > structVar (CSub _ e _ ) = structVar e > structVar (CApply (CVar i) [e]) > | getIdString i == "primNoRead" = structVar e > structVar (CSub2 e _ _) = structVar e > structVar _ = Nothing > isISMethod :: ImperativeStatement -> Bool > isISMethod (ISMethod _ _) = True > isISMethod _ = False > isISRule :: ImperativeStatement -> Bool > isISRule (ISRule _ _ _ _) = True > isISRule _ = False > isISExport :: ImperativeStatement -> Bool > isISExport (ISExport _ _) = True > isISExport _ = False > isISImport :: ImperativeStatement -> Bool > isISImport (ISImport _ _) = True > isISImport _ = False one could be more clever about detecting same-register; one would then need to be careful about variable shadowing > data ISContext = ISCExpression | ISCAction | ISCActionValue | ISCModule CType | ISCIsModule > | ISCSequence | ISCToplevel | ISCInterface | ISCRules | ISCInstance | ISCBVI > deriving (Eq, Show) > instance PVPrint ISContext where > pvPrint d p ISCExpression = text "expression block" > pvPrint d p ISCAction = text "action" > pvPrint d p ISCActionValue = text "actionvalue" > pvPrint d p (ISCModule t) = text "module (" <> pvPrint d p t <> text ")" > pvPrint d p ISCIsModule = text "generic module" > pvPrint d p ISCSequence = text "sequence" > pvPrint d p ISCToplevel = text "toplevel" > pvPrint d p ISCInterface = text "interface" > pvPrint d p ISCRules = text "rules" > pvPrint d p ISCInstance = text "instance" > pvPrint d p ISCBVI = text "BVI" > isActionContext :: ISContext -> Bool > isActionContext ISCAction = True > isActionContext ISCActionValue = True > isActionContext _ = False > isMonadicContext :: ISContext -> Bool > isMonadicContext context = > case context of > ISCIsModule -> True > ISCModule _ -> True > ISCAction -> True > ISCActionValue -> True > _ -> False > isModuleContext :: ISContext -> Bool > isModuleContext ISCIsModule = True > isModuleContext (ISCModule _) = True > isModuleContext _ = False > data ImperativeFlags = ImperativeFlags { > functionNameArgs :: Maybe (Id, [(Maybe CType, Id)]), > stmtContext :: ISContext, > filestr :: Maybe CExpr, > ifcType :: Maybe CType, > -- endKeyword contains the block-terminating keyword if we're in a block; > -- it helps error messages suggest possible solutions > endKeyword :: Maybe String, > allowEq :: Bool, > allowBind :: Bool, > allowRegWrite :: Bool, > allowSubscriptAssign :: Bool, > allowFieldAssign :: Bool, > allowReturn :: Bool, > allowNakedExpr :: Bool, > allowLet :: Bool, > allowFunction :: Bool, > allowInst :: Bool, > allowRule :: Bool, > allowMethod :: Bool, > allowSubinterface :: Bool, > allowConditionals :: Bool, > allowLoops :: Bool, > allowModule :: Bool, > allowInterface :: Bool, > allowForeign :: Bool, > allowTypedef :: Bool, > allowTypeclass :: Bool, > allowInstanceDecl :: Bool, > allowExport :: Bool, > allowImport :: Bool, > allowArrayDecl :: Bool, > allowAssertVar :: Bool, > allowSequence :: Bool, > allowProperty :: Bool, > allowAssert :: Bool, > allowAssume :: Bool, > allowCover :: Bool, > allowExpect :: Bool > } deriving (Show) > nullImperativeFlags :: ImperativeFlags > nullImperativeFlags = ImperativeFlags { > functionNameArgs = Nothing, > stmtContext = ISCExpression, > filestr = Nothing, > ifcType = Nothing, > endKeyword = Nothing, > allowEq = False, > allowBind = False, > allowRegWrite = False, > allowSubscriptAssign = False, > allowFieldAssign = False, > allowReturn = False, > allowNakedExpr = False, > allowLet = False, > allowFunction = False, > allowInst = False, > allowRule = False, > allowMethod = False, > allowSubinterface = False, > allowConditionals = False, > allowLoops = False, > allowModule = False, > allowInterface = False, > allowForeign = False, > allowTypedef = False, > allowTypeclass = False, > allowInstanceDecl = False, > allowExport = False, > allowImport = False, > allowArrayDecl = False, > allowAssertVar = False, > allowSequence = False, > allowProperty = False, > allowAssert = False, > allowAssume = False, > allowCover = False, > allowExpect = False > } > type FreeVarSet = S.Set Id get free variables from statement or right-hand-side of assignment > -- XXX This is not used anywhere (might not be correct or up to date) > getFVIS :: ImperativeStatement -> FreeVarSet > getFVIS (ISNull) = S.empty > getFVIS (ISDecl pos name typ preds) = S.empty > getFVIS (ISPatEq pos pat exp) = snd $ getFVE exp > getFVIS (ISPatBind pos pat exp) = snd $ getFVE exp > getFVIS (ISEqual pos name expr) = snd $ getFVE expr > getFVIS (ISUpdate pos expr' expr) = snd (getFVE expr') `S.union` snd (getFVE expr) > -- XXX field name not treated as a FV: see CFreeVars.hs > getFVIS (ISUpdateReg pos expr' expr) = snd (getFVE expr') `S.union` snd (getFVE expr) > getFVIS (ISUpdateBind pos pprops expr' expr) = snd (getFVE expr') `S.union` snd (getFVE expr) > getFVIS (ISBind pos pprops name expr) = snd $ getFVE expr > getFVIS (ISRegWrite pos regExpr expr) = snd (getFVE regExpr) `S.union` snd (getFVE expr) > getFVIS (ISReturn pos (Just expr)) = snd $ getFVE expr > getFVIS (ISReturn pos Nothing) = S.empty > getFVIS (ISNakedExpr pos expr) = snd $ getFVE expr > getFVIS (ISInst pos pprops ifcName instName typ ck rt pr expr) = snd $ getFVE expr > getFVIS (ISRule pos name prags rule) = snd $ getFVR rule > getFVIS (ISMethod pos def) = snd $ getFVDl def > getFVIS (ISFunction pos prags def) = snd $ getFVDl def > getFVIS (ISExport pos exports) = S.empty > getFVIS (ISImport pos imports) = S.empty > getFVIS (ISTypeclassInstance pos classtype defs) = > S.unions [getFVIS (ISFunction pos [] def) | def <- defs] > getFVIS (ISTypeclass pos _ _ _ _ methods) = S.empty > getFVIS (ISInterface pos _ _ _ methods) = S.empty > getFVIS (ISForeignModule pos _ _ clause _) = snd $ getFVC clause > getFVIS (ISForeignFunction {}) = internalError "CVParserCommon.getFVIS ISForeignFunction" > getFVIS (ISModule pos _ _ _ clause) = snd $ getFVC clause > getFVIS (ISTypedef pos defns) = S.empty > getFVIS (ISBreak pos) = S.empty > getFVIS (ISContinue pos) = S.empty > getFVIS (ISCaseTagged pos subject arms dfltArm) = internalError "CVParserCommon.getFVIS ISCaseTagged" > getFVIS (ISCase pos subject arms dfltArm) = internalError "CVParserCommon.getFVIS ISCase" > getFVIS (ISIf pos test conseq altern) = internalError "CVParserCommon.getFVIS ISIf" > getFVIS (ISAbtIf pos test conseq altern) = internalError "CVParserCommon.getFVIS ISAbtIf" > getFVIS (ISAction pos body) = internalError "CVParserCommon.getFVIS ISAction" > getFVIS (ISActionValue pos body) = internalError "CVParserCommon.getFVIS ISActionValue" > getFVIS (ISBeginEnd pos body) = internalError "CVParserCommon.getFVIS ISBeginEnd" > getFVIS (ISRepeat pos test body) = internalError "CVParserCommon.getFVIS ISRepeat" > getFVIS (ISWhile pos test body) = internalError "CVParserCommon.getFVIS ISWhile" > getFVIS (ISFor pos init test incr body) = internalError "CVParserCommon.getFVIS ISFor" > getFVIS (ISSeq pos body) = internalError "CVParserCommon.getFVIS ISSeq" > getFVIS (ISPar pos body) = internalError "CVParserCommon.getFVIS ISPar" > getFVIS (ISGoto pos _) = S.empty > getFVIS (ISLabel pos _) = S.empty > getFVIS (ISNamed pos _ _) = internalError "CVParserCommon.getFVIS ISNamed" > getFVIS (ISSequence pos body) = internalError "CVParserCommon.getFVIS ISSequence" > getFVIS (ISProperty pos body) = internalError "CVParserCommon.getFVIS ISProperty" > getFVIS (ISAssertStmt pos body) = internalError "CVParserCommon.getFVIS ISAssertStmt" > getFVIS (ISBVI pos body) = internalError "CVParserCommon.getFVIS ISBVI" > getFVIS (ISClassicDefns pos body) = internalError "CVParserCommon.getFVIS ISClassicDefns" get free variables updated by a statement > getUFVIS :: ImperativeStatement -> FreeVarSet > getUFVIS (ISNull) = S.empty > getUFVIS (ISDecl pos name typ preds) = S.empty > getUFVIS (ISPatEq pos pat exp) = S.empty > getUFVIS (ISPatBind pos pat exp) = S.empty > getUFVIS (ISEqual pos vars expr) = S.fromList (getIdOrTupleNames vars) > getUFVIS (ISUpdate _ expr' _) = > case (structVar expr') of > Nothing -> S.empty > Just v -> S.singleton (v) > getUFVIS (ISUpdateBind _ _ expr' _) = > case (structVar expr') of > Nothing -> S.empty > Just v -> S.singleton (v) > getUFVIS (ISUpdateReg _ expr' _) = S.empty > getUFVIS (ISBind pos pprops vars expr) = S.fromList (getIdOrTupleNames vars) > getUFVIS (ISRegWrite pos regExpr expr) = S.empty > getUFVIS (ISReturn pos _) = S.empty > getUFVIS (ISNakedExpr pos expr) = S.empty > getUFVIS (ISInst pos pprops ifcName instName typ ck rt pr expr) = S.empty > getUFVIS (ISRule pos name prags rule) = S.empty > getUFVIS (ISMethod pos def) = S.empty > getUFVIS (ISFunction pos _ def) = S.empty > getUFVIS (ISRepeat pos cond body) = getUFVISs body > getUFVIS (ISWhile pos cond body) = getUFVISs body > getUFVIS (ISBeginEnd pos body) = getUFVISs body > getUFVIS (ISSeq pos body) = getUFVISs body > getUFVIS (ISPar pos body) = getUFVISs body > getUFVIS (ISGoto pos label) = S.empty > getUFVIS (ISLabel pos label) = S.empty > getUFVIS (ISNamed pos _ stmts) = getUFVISs stmts > getUFVIS (ISAction pos body) = getUFVISs body > getUFVIS (ISActionValue pos body) = getUFVISs body > getUFVIS (ISIf pos e s1s Nothing) = getUFVISs s1s > getUFVIS (ISIf pos e s1s (Just s2s)) = > (getUFVISs s1s) `S.union` (getUFVISs s2s) > getUFVIS (ISAbtIf pos e s1s Nothing) = getUFVISs s1s > getUFVIS (ISAbtIf pos e s1s (Just s2s)) = > (getUFVISs s1s) `S.union` (getUFVISs s2s) > getUFVIS (ISFor pos init cond incr body) = getUFVISs (init++body++incr) > getUFVIS (ISCase pos exp arms defq) = getUFVcase arms `S.union` getUFVdef defq > getUFVIS (ISCaseTagged pos exp arms defq) = getUFVtcase arms `S.union` getUFVdef defq > getUFVIS (ISExport _ _) = S.empty > getUFVIS (ISImport _ _) = S.empty > getUFVIS (ISTypeclassInstance _ _ defs) = S.empty > getUFVIS (ISTypeclass _ _ _ _ _ methods) = S.empty > getUFVIS (ISInterface _ _ _ _ methods) = S.empty > getUFVIS (ISForeignModule _ _ _ clause _) = S.empty > getUFVIS (ISForeignFunction {}) = S.empty > getUFVIS (ISModule _ _ _ _ clause) = S.empty > getUFVIS (ISTypedef _ defns) = S.empty > getUFVIS (ISSequence _ _) = S.empty > getUFVIS (ISProperty _ _) = S.empty > getUFVIS (ISAssertStmt _ _) = S.empty > getUFVIS (ISBVI _ _) = S.empty > getUFVIS (ISBreak pos) = S.empty > getUFVIS (ISContinue pos) = S.empty > getUFVIS (ISClassicDefns pos body) = internalError "CVParserCommon.getUFVIS ISClassicDefns" > getUFVdef :: Maybe (a, [ImperativeStatement]) -> S.Set Id > getUFVdef Nothing = S.empty > getUFVdef (Just (pos,ss)) = getUFVISs ss > getUFVcase :: [(a, b, [ImperativeStatement])] -> S.Set Id > getUFVcase as = S.unions (map (\ (x,y,z) -> getUFVISs z) as) > getUFVtcase :: [(a, b, c, [ImperativeStatement])] -> S.Set Id > getUFVtcase as = S.unions (map (\ (w,x,y,z) -> getUFVISs z) as) get free variables updated by a list of statements (i.e. omitting updates of variables declared earlier in the list) > getUFVISs :: [ImperativeStatement] -> FreeVarSet > getUFVISs = fst . foldl f (S.empty, S.empty) where > f (updates, decls) stmt = > case stmt of > ISDecl _ vars _ _ -> > let names = getIdOrTupleNames vars > in (updates, set_insertMany names decls) > ISPatEq _ pat _ -> (updates, S.union (getPV pat) decls) > ISPatBind _ pat _ -> (updates, S.union (getPV pat) decls) > _ -> (updates `S.union` (getUFVIS stmt `S.difference` decls), decls) > instance HasPosition ImperativeStatement where > getPosition (ISNull) = noPosition > getPosition (ISDecl pos name typ preds) = pos > getPosition (ISPatEq pos pat exp) = pos > getPosition (ISPatBind pos pat exp) = pos > getPosition (ISEqual pos name expr) = pos > getPosition (ISUpdate pos expr' expr) = pos > getPosition (ISUpdateBind pos pprops expr' expr) = pos > getPosition (ISUpdateReg pos expr' expr) = pos > getPosition (ISBind pos pprops name expr) = pos > getPosition (ISRegWrite pos regExpr expr) = pos > getPosition (ISReturn pos _) = pos > getPosition (ISNakedExpr pos expr) = pos > getPosition (ISInst pos pprops ifcName instName typ ck rt pr expr) = pos > getPosition (ISRule pos name prags rule) = pos > getPosition (ISMethod pos def) = pos > getPosition (ISFunction pos prags def) = pos > getPosition (ISRepeat pos _ _) = pos > getPosition (ISWhile pos _ _) = pos > getPosition (ISBeginEnd pos _) = pos > getPosition (ISSeq pos _) = pos > getPosition (ISPar pos _) = pos > getPosition (ISGoto pos _) = pos > getPosition (ISLabel pos _) = pos > getPosition (ISNamed pos _ _) = pos > getPosition (ISAction pos _) = pos > getPosition (ISActionValue pos _) = pos > getPosition (ISImport pos _) = pos > getPosition (ISExport pos _) = pos > getPosition (ISTypeclassInstance pos _ _) = pos > getPosition (ISTypeclass pos _ _ _ _ _) = pos > getPosition (ISInterface pos _ _ _ _) = pos > getPosition (ISForeignModule pos _ _ _ _) = pos > getPosition (ISForeignFunction pos _ _ _) = pos > getPosition (ISTypedef pos _) = pos > getPosition (ISModule pos _ _ _ _) = pos > getPosition (ISCaseTagged pos _ _ _) = pos > getPosition (ISCase pos _ _ _) = pos > getPosition (ISIf pos _ _ _) = pos > getPosition (ISAbtIf pos _ _ _) = pos > getPosition (ISFor pos _ _ _ _) = pos > getPosition (ISSequence pos _) = pos > getPosition (ISProperty pos _) = pos > getPosition (ISAssertStmt pos _) = pos > getPosition (ISBVI pos _) = pos > getPosition (ISClassicDefns pos _) = pos > getPosition (ISBreak pos) = pos > getPosition (ISContinue pos) = pos > {-# SPECIALIZE getListPosWithDefault :: [ImperativeStatement] -> Position -> Position #-} > getListPosWithDefault :: (HasPosition a) => [a] -> Position -> Position > getListPosWithDefault [] pos = pos > getListPosWithDefault (item:_) _ = getPosition item > emptyParserState :: ErrorHandle -> Flags -> SV_Parser_State > emptyParserState errh flags = > SV_Parser_State { errHandle = errh, > warnings = [], > svaWarned = False, > parserflags = flags } > parseWarn :: WMsg -> SV_Parser () > parseWarn warning = > let isSVAwarning = > case warning of > (_, WExperimental feature) -> (feature == "SV assertions") > _ -> False > in do > state <- getState > when (not (isSVAwarning && svaWarned state)) > (updateState (if isSVAwarning then addWarn2 else addWarn)) > return () > where addWarn state = state { warnings = (warning : warnings state)} > addWarn2 state = state { warnings = (warning : warnings state), > svaWarned = True} > getParseWarnings :: SV_Parser [WMsg] > getParseWarnings = warnings <$> getState > getParserFlags :: SV_Parser Flags > getParserFlags = parserflags <$> getState > getErrHandle :: SV_Parser ErrorHandle > getErrHandle = errHandle <$> getState given a list of guards and the consequent and alternative expressions, make either an if-then-else expression on an appropriate case expression > mkIf :: Position -- pos of the operator/keyword > -> [CQual] -- conditions -- must /= [] > -> CExpr -- consequent > -> CExpr -- alternative > -> CExpr -- resulting expression > mkIf _ [] _ _ = internalError "CVParserCommon.mkIfExpr with empty conditions" > mkIf pos conds@(cond1:_) consequent alternative > | all isCQFilter conds = -- turn into if-expression > let cond = joinWithAnd [e | CQFilter e <- conds] > in Cif pos cond consequent alternative > | otherwise = -- turn into case with pattern-matching guards > (Ccase pos (mkTuple (getPosition cond1) [] {- the unit -}) > [CCaseArm { cca_pattern = CPAny (getPosition consequent), > cca_filters = conds, > cca_consequent = consequent }, > CCaseArm { cca_pattern = CPAny (getPosition alternative), > cca_filters = [], > cca_consequent = alternative }]) > joinWithAnd :: [CExpr] -> CExpr > joinWithAnd = joinWithBinOpL idAndAt > joinWithBinOpL :: (Position -> Id) -- operator, parametrized on position > -> [CExpr] -- expressions to join (must /= []) > -> CExpr -- resulting expression > joinWithBinOpL _ [] = internalError "CVParserCommon.joinWithBinOpL: []" > joinWithBinOpL opAt exprs = foldl1 join exprs > where e1 `join` e2 = CBinOp e1 (opAt (getPosition e2)) e2 THE IMPERATIVE STATEMENT CONVERSION MONAD > type DeclarationInfo = (Position, [IdProp], Maybe CType, [CPred]) > type DeclaredVars = M.Map Id DeclarationInfo > data AssignmentType = ATUninitialized | ATNormal deriving (Show) > type AssignmentInfo = (Position, AssignmentType) > type AssignedVars = M.Map Id AssignmentInfo > type SequenceInfo = M.Map Id ImperativeStatement > type PropertyInfo = M.Map Id ImperativeStatement > type StmtChecker = ISContext -> [ImperativeStatement] -> ISConvMonad [ImperativeStatement] > type StmtConverter = (ISContext, Maybe CType, Maybe CExpr) -> Bool -> [ImperativeStatement] -> ISConvMonad [CStmt] > type ExprConverter = Position -- start of block > -> ImperativeFlags -- flags > -> Bool -- are we at end of block? > -> [ImperativeStatement] -- statements inside block > -> ISConvMonad CExpr -- resulting conversion computation > data ISConvState = ISConvState { > issFunction :: [Maybe (Id, [(Maybe CType, Id)])], -- Just function name/args > -- when a function is being parsed > -- so that assignment to > -- the function name can be converted > issDeclared :: [DeclaredVars], -- variables declared in this block > issAssigned :: [AssignedVars], -- variables assigned in this block > --ASSERTIONS > issPassThrough :: Bool, -- pass assertions to RTL, rather than synthesize > issSequences :: [SequenceInfo], -- sequences declared in this block > issProperties :: [PropertyInfo], -- properties declared in this block > issFile :: String, -- the file (package) name containing current assertion > issLine :: Int, -- the line number of the current assertion > issAssertNum :: Int, --A unique number to act as assertion identifier > issAssertSubNum :: Int, --A unique number per assertion > issAssertDecls :: [[ImperativeStatement]], --Assertion bind stack > issStmtChecker :: StmtChecker, --Assertion statement checker reference > issStmtConverter :: StmtConverter, --Assertion IStoCStmt converter reference > issExprConverter :: ExprConverter, --Assertion IStoCExpr converter reference > issWarnings :: [WMsg] -- warnings, in reverse order > } > instance Show ISConvState where > show (ISConvState fnm decls asgns pt seqs props > afile aline anum asub assdecls _ _ _ warns) = > (show fnm) ++ (unlines (map show decls)) ++ (unlines (map show asgns)) ++ > (show pt) ++ (unlines (map show seqs)) ++ (unlines (map show props )) ++ > (show afile) ++ (show aline) ++ > (show anum) ++ (show asub)++ (unlines (map show assdecls)) ++ (unlines (map show warns)) > type ISConvMonad result = SEMonad.SEM [EMsg] ISConvState result > emptyISConvState :: SV_Parser ISConvState > emptyISConvState = do > f <- getParserFlags > let s = ISConvState { issFunction = [Nothing], > issDeclared = [M.empty], > issAssigned = [M.empty], > issSequences = [M.empty], > issProperties = [M.empty], > issPassThrough = passThroughAssertions f, > issFile = "", > issLine = 0, > issAssertNum = 0, > issAssertSubNum = 0, > issAssertDecls = [[]], > issStmtChecker = \c x -> return x, > issStmtConverter = \a b c -> return [], > issExprConverter = \a b c d -> return (anyExprAt noPosition), > issWarnings = [] > } > return s > pushState :: ISConvMonad () > pushState = modify $ \state -> state > { -- issFunction = Nothing : issFunction state, > issDeclared = M.empty : issDeclared state, > issAssigned = M.empty : issAssigned state } > popState :: ISConvMonad () > popState = do > state <- get > if (null (issFunction state) > || null (issDeclared state) > || null (issAssigned state)) > then internalError "CVParserCommon.popState: non-existent state" > else > put $ state { -- issFunction = tail $ issFunction state, > issDeclared = tail $ issDeclared state, > issAssigned = tail $ issAssigned state } > > traceState :: ISConvMonad () > traceState = modify $ \ state -> trace (show state) state > getISCState :: ISConvMonad ISConvState > getISCState = get findDecl produces the info for a variable if declared, together with a flag saying whether or not the declaration is local > findDecl :: Id -> [DeclaredVars] -> (Maybe DeclarationInfo, Bool) > -- the Maybe says whether it's declared > findDecl var issDs = fd issDs True where > fd [] _ = (Nothing, False) > fd (d:ds) isTop = > case var `M.lookup` d of > Nothing -> fd ds False > x -> (x, isTop) > -- XXX error on duplicate declaration should permit declaring locals > declare :: Position -> Id -> (Maybe CType) -> [CPred] -> ISConvMonad () > declare pos var typ preds = do > state <- get > let decls = issDeclared state > nextState warns = > state { issDeclared = > (let d:ds = decls > declInfo = (pos, getIdProps var, typ, preds) > in (M.insert var declInfo d):ds), > issWarnings = reverse warns ++ issWarnings state } > in case findDecl var decls of > (Nothing,_) -> put $ nextState [] > (Just (prevPos, _, _, _), False) -> > put $ nextState [(pos, WShadowDecl (getIdString var) prevPos)] > (Just (prevPos, _, _, _), True) -> > throwError [(pos, EMultipleDecl (pvpString var) prevPos)] > isDeclared :: Id -> ISConvMonad Bool > isDeclared var = do > state <- get > return $ isJust $ fst $ findDecl var $ issDeclared state > isFunctionName :: Id -> ISConvMonad Bool > isFunctionName var = do > funcs <- gets issFunction > let func = head funcs > return $ isJust func && fst (fromJust func) == var > isFunctionNameIdOrTuple :: IdOrTuple -> ISConvMonad (Maybe Id) > isFunctionNameIdOrTuple vars = > let f var = do b <- isFunctionName var > return $ toMaybe b var > in case vars of > (Right var) -> f var > (Left [Right var]) -> f var -- XXX Is this branch needed/OK? > _ -> return Nothing > updateIdProps :: Id -> ISConvMonad Id > updateIdProps var = do > state <- get > isFunction <- isFunctionName var > if isFunction > then return var > else case findDecl var (issDeclared state) of > (Just (pos, props, _, _), _) -> return $ var `addIdProps` props > _ -> throwError [(getIdPosition var, EAssignBeforeDecl (pvpString var))] > getDeclInfo :: Id -> ISConvMonad (Maybe (Maybe CType, [CPred])) > -- the outer Maybe says whether it's declared > -- the inner Maybe says whether the type has been specified > getDeclInfo var = do > state <- get > let extract (Nothing, _) = Nothing > extract (Just (_, _, typ, preds), _) = Just (typ, preds) > return $ extract $ findDecl var $ issDeclared state > assign :: Position -> Id -> AssignmentType -> ISConvMonad () > assign pos var atype = modify > $ \state -> let a:as = issAssigned state > in state { issAssigned = (M.insert var (pos, atype) a):as} > isAssigned :: Id -> ISConvMonad Bool > isAssigned var = do > ass <- gets issAssigned > let isAssigned' [] = False > isAssigned' (a:as) = > maybe (isAssigned' as) (const True) (var `M.lookup` a) > return $ isAssigned' ass > isUninitialized :: Id -> ISConvMonad Bool > isUninitialized var = do > ass <- gets issAssigned > let isAssigned' [] = False > isAssigned' (a:as) = > maybe (isAssigned' as) hasUninit (var `M.lookup` a) > hasUninit (_, ATUninitialized) = True > hasUninit _ = False > return $ isAssigned' ass > getNormallyAssignedVars :: ISConvMonad (S.Set Id) > getNormallyAssignedVars = do > ass <- gets issAssigned > let assignedVars = headOrErr "CVParserCommon.getNormallyAssignedVars" ass > normallyAssignedVars = S.fromList > [v | (v, (pos, ATNormal)) <- M.toList assignedVars] > return normallyAssignedVars > getDeclaredVars :: ISConvMonad (S.Set Id) > getDeclaredVars = do > dss <- gets issDeclared > let declaredVars = headOrErr "CVParserCommon.getDeclaredVars" dss > return $ M.keysSet declaredVars > defaultModuleMonadInfo :: Position -> (CType, [CPred]) > defaultModuleMonadInfo pos = (mVar, [CPred (CTypeclass (idIsModuleAt pos)) [mVar, cVar]]) > where mVar = cTVar (idM pos) > cVar = cTVar (idC pos) > contextMonadInfo :: Position -> ISContext -> (CType, [CPred]) > contextMonadInfo pos ISCIsModule = defaultModuleMonadInfo pos > contextMonadInfo pos (ISCModule t) = (t, []) > contextMonadInfo pos ISCAction = (cTCon (idActionValueAt pos), []) > contextMonadInfo pos ISCActionValue = (cTCon (idActionValueAt pos), []) > contextMonadInfo pos _ = internalError ("CVParserCommon.convImperativeStmtsToCStmts: unknown monadic context (" ++ pvpString pos ++ ")") make a temporary id, appending accent acute, and removing keep attribute > mkAcute :: Id -> Id > mkAcute i = addIdProp (mkIdPost (rmKeepId i) fsAcute) IdPRenaming > csLetseq :: [CDefl] -> [CStmt] > csLetseq [] = [] > csLetseq defs = [CSletseq defs] > csLetrec :: [CDefl] -> [CStmt] > csLetrec [] = [] > csLetrec defs = [CSletrec defs] > cvtErr :: p -> e -> SEMonad.SEM [(p, e)] s a > cvtErr pos err = throwError [(pos, err)] > cvtErrs :: e -> SEMonad.SEM e s a > cvtErrs errs = throwError errs > cvtWarn :: Position -> ErrMsg -> ISConvMonad () > cvtWarn pos warning = modify $ \state -> state { issWarnings = (pos, warning) : issWarnings state } > cvtWarns :: [WMsg] -> ISConvMonad () > cvtWarns warnings = modify $ \state -> state { issWarnings = reverse warnings ++ issWarnings state } > semToParser :: ISConvState -> SEMonad.SEM [EMsg] ISConvState a -> SV_Parser a > semToParser initState monad = > case SEMonad.run monad initState of > Left errs -> failWithErrs errs > Right (result, finalState) -> > do mapM_ parseWarn (reverse (issWarnings finalState)) > return result > actionFlags :: ImperativeFlags > actionFlags = (nullImperativeFlags { stmtContext = ISCAction, > allowEq = True, > allowSubscriptAssign = True, > allowFieldAssign = True, > allowArrayDecl = True, > allowFunction = True, > allowBind = True, > allowLoops = True, > allowConditionals = True, > allowNakedExpr = True, > allowRegWrite = True, > allowLet = True }) > actionValueFlags :: ImperativeFlags > actionValueFlags = (nullImperativeFlags { stmtContext = ISCActionValue, > allowEq = True, > allowSubscriptAssign = True, > allowFieldAssign = True, > allowArrayDecl = True, > allowFunction = True, > allowBind = True, > allowLoops = True, > allowConditionals = True, > allowNakedExpr = True, > allowRegWrite = True, > allowReturn = True, > allowLet = True }) > expressionFlags :: ImperativeFlags > expressionFlags = (nullImperativeFlags { allowEq = True, > allowSubscriptAssign = True, > allowFieldAssign = True, > allowArrayDecl = True, > allowLoops = True, > allowConditionals = True, > allowFunction = True, > allowModule = True, > allowNakedExpr = True, > allowLet = True, > stmtContext = ISCExpression })