module Main_vcdcheck(main) where import Version import FileNameUtil(hasDotSuf, vcdSuffix) import Position import Error(internalError, EMsg, ErrMsg(..), showErrorList) import Util(separate) import IOUtil(getEnvDef) import TopUtils(dfltBluespecDir) import VCD import System.Environment(getArgs) import System.Console.GetOpt import System.IO import System.Exit import Control.Exception(bracket) import Control.Monad(when, msum) import Data.List(intercalate, partition, isPrefixOf) import Data.Maybe(fromMaybe, isJust, isNothing, fromJust) import Data.Bits(shiftL, xor, (.|.), shiftR) import qualified Data.Map as M import qualified Data.Set as S import qualified Data.ByteString.Lazy.Char8 as C import Text.Regex import Numeric(readDec, readHex, readSigned) -- import Debug.Trace -- Version string (matches main BSC version numbering) versionString :: String versionString = versionStr True (bluespec ++ " vcdcheck utility") -- ------------------------------------------------------------------- -- Option processing -- Structure which holds all option settings data Options = Options { optShowVersion :: Bool , optShowHelp :: Bool , optVCD1 :: Maybe FilePath , optVCD2 :: Maybe FilePath , optCheckStrings :: [String] , optLimitString :: String , optCheckCmds :: [CheckCmd] , optLimit :: Integer } deriving (Show) -- Default settings defaultOptions :: Options defaultOptions = Options { optShowVersion = False , optShowHelp = False , optVCD1 = Nothing , optVCD2 = Nothing , optCheckStrings = [] , optLimitString = "" , optCheckCmds = [] , optLimit = 1000 } -- Description of command-line options options :: [OptDescr (Options -> Options)] options = [ Option ['V'] ["version"] (NoArg (\opts -> opts { optShowVersion = True })) "show version information and exit" , Option ['c'] ["check"] (ReqArg (\s opts -> opts { optCheckStrings = (optCheckStrings opts) ++ [s] }) "CHECK") "check the given assertion" , Option ['h','?'] ["help"] (NoArg (\opts -> opts { optShowHelp = True })) "print usage information and exit" , Option ['l'] ["limit"] (ReqArg (\s opts -> opts { optLimitString = s }) "LIMIT") "limit the number of errors displayed (default = 1000)" , Option ['q'] ["quiet"] (NoArg (\opts -> opts { optLimitString = "0" })) "do not print errors, only set exit status" ] -- Header used in usage message usage_header :: String usage_header = "Usage: vcdcheck [OPTIONS] \n" ++ " vcdcheck [OPTIONS] " -- Parse the command line to produce the option structure, etc. parseOpts :: [String] -> String -> (Options, [String], [EMsg]) parseOpts argv bluespecdir = let (opts,args0,errs) = getOpt Permute options argv options0 = foldl (flip id) defaultOptions opts (vcds,args1) = partition (hasDotSuf vcdSuffix) args0 emsgs0 = map toEMsg errs (options1,emsgs1) = checkVCDs vcds (options0,emsgs0) emsgs2 = if (null args1) then emsgs1 else emsgs1 ++ [(noPosition, EUnrecognizedCmdLineText (unwords args1))] (options2,emsgs3) = if (null (optLimitString options1)) then (options1,emsgs2) else case (readSigned readDec (optLimitString options1)) of [(n,"")] | n >= 0 -> (options1 { optLimit = n }, emsgs2) otherwise -> (options1, emsgs2 ++ [(noPosition, EBadArgFlag "--limit" (optLimitString options1) ["non-negative integers"])]) (options3,emsgs4) = parseCheckCmds (options2, emsgs3) in (options3, [], emsgs4) where checkVCDs fs (os,es) = case fs of [vcd1] -> (os { optVCD1 = Just vcd1 }, es) [vcd1,vcd2] -> (os { optVCD1 = Just vcd1, optVCD2 = Just vcd2 }, es) [] -> (os,es ++ [(noPosition, EGeneric "no VCD files given")]) _ -> (os,es ++ [(noPosition, EGeneric "too many VCD files given")]) parseCheckCmds (os,es) = let ss = optCheckStrings os (bad,cmds) = separate (concatMap (parseCheckCmd os) ss) errs = [ (noPosition, EGeneric ("invalid check command: " ++ s)) | s <- bad ] in (os { optCheckCmds = cmds }, es ++ errs) -- Produce a standard EMsg value from an option parser error string toEMsg :: String -> EMsg toEMsg s = fromMaybe (noPosition, EGeneric s) $ msum [f s | f <- [ bad_option , missing_arg ]] where bad_option_regex = mkRegex "unrecognized option `(.*)'" bad_option x = do [opt] <- matchRegex bad_option_regex s return (noPosition, EUnknownFlag opt) missing_arg_regex = mkRegex "option `(.*)' requires an argument .*" missing_arg x = do [opt] <- matchRegex missing_arg_regex s return (noPosition, EOneArgFlag opt) -- Validate command-line and process help requests checkCmdLine :: Options -> [String] -> [EMsg] -> IO () checkCmdLine opts args errs = do when (optShowVersion opts) $ do hPutStrLn stdout versionString hPutStrLn stdout copyright when (optShowHelp opts) $ hPutStrLn stdout (usageInfo usage_header options) when ((optShowVersion opts) || (optShowHelp opts)) $ exitWith ExitSuccess when (not (null errs)) $ do hPutStr stderr (showErrorList errs) hPutStrLn stderr (usageInfo usage_header options) exitWith (ExitFailure 1) -- ------------------------------------------------------------------- -- Description of checker commands -- Identify which file the command applies to type FileNum = Int file1, file2 :: FileNum file1 = 1 file2 = 2 -- String describing which signals a command applies to -- For now this is just a name, but may become a regex in the future type SigSpec = String -- Description of what time period a command applies to. data TimeSpec = Initially | At Integer | Earlier Integer | Later Integer | Sometime deriving (Eq, Show) -- increment time incrTime :: Integer -> TimeSpec -> TimeSpec incrTime t (At x) = At (t+x) incrTime _ x = x -- check the timespec against the current time timeOK :: TimeSpec -> Integer -> Bool timeOK Initially 0 = True timeOK (At t) n = t == n timeOK (Earlier t) n = n < t timeOK (Later t) n = n > t timeOK Sometime _ = True timeOK _ _ = False -- These are the supported checker commands data CheckCmd = Exists SigSpec FileNum | Toggles SigSpec FileNum TimeSpec | Stable SigSpec FileNum TimeSpec | Value SigSpec Integer FileNum TimeSpec | IsX SigSpec FileNum TimeSpec | IsZ SigSpec FileNum TimeSpec | Matches SigSpec SigSpec TimeSpec | HasTimescale Integer Integer FileNum | GoesTo Integer FileNum | Sequence SeqCmd deriving (Show) data SeqState = Waiting | Running | Finished deriving(Show, Eq) -- Sequence to track a data SeqCmd = CRCCmd {sc_fileNum :: FileNum ,sc_signal :: SigSpec ,sc_width :: Integer ,sc_startVal :: Integer ,sc_nextTime :: TimeSpec ,sc_timeIncr :: TimeSpec ,sc_count :: Integer ,sc_currentCount :: Integer ,sc_state :: SeqState ,sc_crcfunction :: Integer -> Integer } -- Show is used in properties -- only invariants are shown instance Show SeqCmd where show c = "CRC: " ++ (sc_signal c) ++ " starting " ++ (show $ sc_startVal c) ++ " every " ++ (show $ sc_timeIncr c) ++ " for " ++ (show $ sc_count c) -- Command parsing routines data Target = IntVal Integer | XVal | ZVal deriving (Eq) parseValue :: String -> Maybe Target parseValue "false" = Just (IntVal 0) parseValue "true" = Just (IntVal 1) parseValue "x" = Just XVal parseValue s | "'h" `isPrefixOf` s = case (readHex (drop 2 s)) of [(n,"")] -> Just (IntVal n) _ -> Nothing parseValue s = case (readDec s) of [(n,"")] -> Just (IntVal n) _ -> Nothing parseTimeSpec :: String -> Maybe TimeSpec parseTimeSpec "initially" = Just Initially parseTimeSpec "sometime" = Just Sometime parseTimeSpec ('@':s) = case (readDec s) of [(t,"")] -> Just (At t) _ -> Nothing parseTimeSpec ('<':s) = case (readDec s) of [(t,"")] -> Just (Earlier t) _ -> Nothing parseTimeSpec ('>':s) = case (readDec s) of [(t,"")] -> Just (Later t) _ -> Nothing parseTimeSpec _ = Nothing parseInteger :: String -> Maybe Integer parseInteger s = case (readDec s) of [(n,"")] -> Just n _ -> Nothing parseCheckCmd :: Options -> String -> [Either String CheckCmd] parseCheckCmd opts s = parse (words s) where parse :: [String] -> [Either String CheckCmd] parse [sig,"exists"] = [ Right (Exists sig f) | f <- getFNums opts ] parse [sig,"toggles"] = [ Right (Toggles sig f Sometime) | f <- getFNums opts ] parse [sig,"toggles", t] = case (parseTimeSpec t) of (Just ts) -> [ Right (Toggles sig f ts) | f <- getFNums opts ] _ -> [Left s] parse [sig,"stable", t] = case (parseTimeSpec t) of (Just ts) -> [ Right (Stable sig f ts) | f <- getFNums opts ] _ -> [Left s] parse [sig,"equals",val,t] = case (parseValue val, parseTimeSpec t) of (Just v, Just ts) -> case v of (IntVal n) -> [ Right (Value sig n f ts) | f <- getFNums opts ] XVal -> [ Right (IsX sig f ts) | f <- getFNums opts ] ZVal -> [ Right (IsZ sig f ts) | f <- getFNums opts ] _ -> [Left s] parse [sig,"becomes",val,t] = case (parseValue val, parseTimeSpec t) of (Just v, Just ts) -> [ Right (Toggles sig f ts) | f <- getFNums opts ] ++ case v of (IntVal n) -> [ Right (Value sig n f ts) | f <- getFNums opts ] XVal -> [ Right (IsX sig f ts) | f <- getFNums opts ] ZVal -> [ Right (IsZ sig f ts) | f <- getFNums opts ] _ -> [Left s] parse [sig,"remains",val,t] = case (parseValue val, parseTimeSpec t) of (Just v, Just ts) -> [ Right (Stable sig f ts) | f <- getFNums opts ] ++ case v of (IntVal n) -> [ Right (Value sig n f ts) | f <- getFNums opts ] XVal -> [ Right (IsX sig f ts) | f <- getFNums opts ] ZVal -> [ Right (IsZ sig f ts) | f <- getFNums opts ] _ -> [Left s] parse ["CRC", sig, startv, every, for] = case (parseValue startv, parseTimeSpec every, parseInteger for) of (Just (IntVal sv), Just et, Just fr) -> let cmd = CRCCmd {sc_fileNum=0 ,sc_signal=sig ,sc_width=0 ,sc_startVal=sv ,sc_nextTime=Sometime ,sc_timeIncr=et ,sc_count=fr ,sc_currentCount = 0 ,sc_state = Waiting ,sc_crcfunction = id} in [Right (Sequence cmd{sc_fileNum=f}) | f <- getFNums opts] (Nothing, _, _) -> [Left $ "Error in scanning CRC command -- start value " ++ startv] (_, Nothing, _) -> [Left $ "Error in scanning CRC command -- every time " ++ every] (_, _, Nothing) -> [Left $ "Error in scanning CRC command -- sequence length " ++ for] _ -> [Left $ "Error in scanning CRC command " ++ s] parse ("CRC":_) = [Left $"CRC command expects 4 arguments " ++ s] parse _ = [Left s] -- Routines for converting checker commands into checker functions getFNums :: Options -> [FileNum] getFNums opts = (if (isJust (optVCD1 opts)) then [file1] else []) ++ (if (isJust (optVCD2 opts)) then [file2] else []) getFile :: CheckerState -> FileNum -> FilePath getFile cs 1 = name (state1 cs) getFile cs 2 = name (state2 cs) getFile _ n = internalError $ "Bad file number: " ++ (show n) cmdToCheckers :: CheckCmd -> [Checker] cmdToCheckers cmd@(Exists sig fnum) = let prop = show cmd mkMsg cs = sig ++ " not found in " ++ (getFile cs fnum) in [ \_ -> OnDef fnum sig (const [set_prop prop]) , \cs -> EndDef fnum (require_prop prop (mkMsg cs)) ] cmdToCheckers cmd@(Toggles sig fnum Sometime) = let prop_aux = show (Exists sig fnum) mkMsg_aux cs = sig ++ " not found in " ++ (getFile cs fnum) prop = show cmd mkMsg cs = sig ++ " never toggled in " ++ (getFile cs fnum) setup_checkers (code,_) = [ \_ -> Watch fnum code (set_prop_if_changed code fnum prop) , \cs -> EndVCD fnum (require_prop prop (mkMsg cs)) ] in [ \_ -> OnDef fnum sig setup_checkers , \_ -> OnDef fnum sig (const [set_prop prop_aux]) , \cs -> EndDef fnum (require_prop prop_aux (mkMsg_aux cs)) ] cmdToCheckers cmd@(Toggles sig fnum (At t)) = let prop_aux = show (Exists sig fnum) mkMsg_aux cs = sig ++ " not found in " ++ (getFile cs fnum) mkMsg cs = sig ++ " did not toggle at " ++ (show t) ++ " in " ++ (getFile cs fnum) setup_checkers (code,_) = [ \cs -> Wait t (check_toggle code fnum t (mkMsg cs)) ] in [ \_ -> OnDef fnum sig setup_checkers , \_ -> OnDef fnum sig (const [set_prop prop_aux]) , \cs -> EndDef fnum (require_prop prop_aux (mkMsg_aux cs)) ] cmdToCheckers cmd@(Stable sig fnum (At t)) = let prop_aux = show (Exists sig fnum) mkMsg_aux cs = sig ++ " not found in " ++ (getFile cs fnum) mkMsg cs = sig ++ " is not stable at " ++ (show t) ++ " in " ++ (getFile cs fnum) setup_checkers (code,_) = [ \cs -> Wait t (check_stable code fnum t (mkMsg cs)) ] in [ \_ -> OnDef fnum sig setup_checkers , \_ -> OnDef fnum sig (const [set_prop prop_aux]) , \cs -> EndDef fnum (require_prop prop_aux (mkMsg_aux cs)) ] cmdToCheckers cmd@(Value sig val fnum (At t)) = let prop_aux = show (Exists sig fnum) mkMsg_aux cs = sig ++ " not found in " ++ (getFile cs fnum) mkMsg cs = sig ++ " != " ++ (show val) ++ " at " ++ (show t) ++ " in " ++ (getFile cs fnum) setup_checkers (code,_) = [ \cs -> Wait t (check_value code fnum t val (mkMsg cs)) ] in [ \_ -> OnDef fnum sig setup_checkers , \_ -> OnDef fnum sig (const [set_prop prop_aux]) , \cs -> EndDef fnum (require_prop prop_aux (mkMsg_aux cs)) ] cmdToCheckers cmd@(IsX sig fnum (At t)) = let prop_aux = show (Exists sig fnum) mkMsg_aux cs = sig ++ " not found in " ++ (getFile cs fnum) mkMsg cs = sig ++ " != X at " ++ (show t) ++ " in " ++ (getFile cs fnum) setup_checkers (code,_) = [ \cs -> Wait t (check_X code fnum t (mkMsg cs)) ] in [ \_ -> OnDef fnum sig setup_checkers , \_ -> OnDef fnum sig (const [set_prop prop_aux]) , \cs -> EndDef fnum (require_prop prop_aux (mkMsg_aux cs)) ] cmdToCheckers cmd@(IsZ sig fnum (At t)) = let prop_aux = show (Exists sig fnum) mkMsg_aux cs = sig ++ " not found in " ++ (getFile cs fnum) mkMsg cs = sig ++ " != Z at " ++ (show t) ++ " in " ++ (getFile cs fnum) setup_checkers (code,_) = [ \cs -> Wait t (check_Z code fnum t (mkMsg cs)) ] in [ \_ -> OnDef fnum sig setup_checkers , \_ -> OnDef fnum sig (const [set_prop prop_aux]) , \cs -> EndDef fnum (require_prop prop_aux (mkMsg_aux cs)) ] cmdToCheckers (Sequence cmd) = let fnum = sc_fileNum cmd sig = sc_signal cmd prop_exists = show (Exists sig fnum) mkMsg_exists cs = sig ++ " not found in " ++ (getFile cs fnum) -- prop_started = show cmd ++ " Started" prop_complete = show cmd ++ " Completed" failed a = (show cmd) ++ " failed to " ++ a setup_checkers (code,width) = let cmd' = cmd {sc_width = width ,sc_crcfunction = (crcFunction width)} in [ \cs -> EndDef fnum (setup_crc code fnum cmd') ,\cs -> Watch fnum code (check_crc code fnum) ,\cs -> EndVCD fnum (require_prop prop_started (failed "start")) ,\cs -> EndVCD fnum (require_prop prop_complete (failed "complete")) ] in [ \_ -> OnDef fnum sig setup_checkers , \_ -> OnDef fnum sig (const [set_prop prop_exists]) , \cs -> EndDef fnum (require_prop prop_exists (mkMsg_exists cs)) ] cmdToCheckers cmd = [ failure $ "Not implemented: " ++ (show cmd)] -- ------------------------------------------------------------------- -- Facility for managing checkers type ValueMap = M.Map Code VCDValue type Checker = CheckerState -> Action type Property = String data Action = Succeed | Fail String | SetProperty Property Checker | OnDef FileNum String ( (Code,Integer) -> [Checker]) | EndDef FileNum Checker | Wait Integer Checker | Watch FileNum Code Checker | EndVCD FileNum Checker | UpdateCS Code FileNum SeqCmd Checker data CheckerState = CS { props :: S.Set Property , waiting :: M.Map Integer [Checker] , user :: M.Map (FileNum,Code) SeqCmd , state1 :: FileState , state2 :: FileState } data FileState = FS { name :: FilePath , scope :: [String] , stable :: ValueMap , changing :: ValueMap , ondefs :: M.Map String [ (Code,Integer) -> [Checker]] , enddefs :: [Checker] , watching :: M.Map Code [Checker] , endvcd :: [Checker] , now :: Integer } getFS :: FileNum -> CheckerState -> FileState getFS 1 = state1 getFS 2 = state2 getFS n = internalError $ "Bad file number: " ++ (show n) setFS :: FileNum -> FileState -> CheckerState -> CheckerState setFS 1 fs cs = cs { state1 = fs } setFS 2 fs cs = cs { state2 = fs } setFS n _ _ = internalError $ "Bad file number: " ++ (show n) -- basic checkers success :: Checker success = const Succeed failure :: String -> Checker failure msg = const (Fail msg) set_prop :: Property -> Checker set_prop p = const $ SetProperty p success require_prop :: Property -> String -> Checker require_prop p msg = \cs -> if (p `S.member` (props cs)) then Succeed else Fail msg set_prop_if_changed :: Code -> FileNum -> Property -> Checker set_prop_if_changed code fnum prop = \cs -> let fs = getFS fnum cs stable_val = M.lookup code (stable fs) changed_val = M.lookup code (changing fs) ok = (isJust changed_val) && (isJust stable_val) && (changed_val /= stable_val) in if ok then SetProperty prop success else Succeed -- try again on next change check_value :: Code -> FileNum -> Integer -> Integer -> String -> Checker check_value code fnum t val msg = \cs -> let fs = getFS fnum cs stable_val = M.lookup code (stable fs) changed_val = M.lookup code (changing fs) stable_ok = maybe False (\v -> vcd_to_integer v == (Just val)) stable_val no_change = isNothing changed_val change_ok = maybe False (\v -> vcd_to_integer v == (Just val)) changed_val ok = if (now fs < t) then stable_ok else (stable_ok && no_change) || change_ok in if ok then Succeed else Fail msg check_toggle :: Code -> FileNum -> Integer -> String -> Checker check_toggle code fnum t msg = \cs -> let fs = getFS fnum cs stable_val = M.lookup code (stable fs) changed_val = M.lookup code (changing fs) ok = (now fs == t) && (isJust changed_val) && (changed_val /= stable_val) in if ok then Succeed else Fail msg check_stable :: Code -> FileNum -> Integer -> String -> Checker check_stable code fnum t msg = \cs -> let fs = getFS fnum cs stable_val = M.lookup code (stable fs) changed_val = M.lookup code (changing fs) ok = (now fs == t) && ((isNothing changed_val) || (changed_val == stable_val)) in if ok then Succeed else Fail msg check_X :: Code -> FileNum -> Integer -> String -> Checker check_X code fnum t msg = \cs -> let fs = getFS fnum cs stable_val = M.lookup code (stable fs) changed_val = M.lookup code (changing fs) stable_ok = maybe False vcd_is_x stable_val no_change = isNothing changed_val change_ok = maybe False vcd_is_x changed_val ok = if (now fs < t) then stable_ok else (stable_ok && no_change) || change_ok in if ok then Succeed else Fail msg check_Z :: Code -> FileNum -> Integer -> String -> Checker check_Z code fnum t msg = \cs -> let fs = getFS fnum cs stable_val = M.lookup code (stable fs) changed_val = M.lookup code (changing fs) stable_ok = maybe False vcd_is_z stable_val no_change = isNothing changed_val change_ok = maybe False vcd_is_z changed_val ok = if (now fs < t) then stable_ok else (stable_ok && no_change) || change_ok in if ok then Succeed else Fail msg setup_crc :: Code -> FileNum -> SeqCmd -> Checker setup_crc code fnum seqcmd = \cs -> UpdateCS code fnum seqcmd success check_crc :: Code -> FileNum -> Checker check_crc code fnum = \cs -> let err = error $ "Could not find " ++ show code ++ " in checker state" cmd = M.findWithDefault err (fnum,code) (user cs) fs = getFS fnum cs changed_val =fromMaybe (0-1) $ (M.lookup code (changing fs)) >>= vcd_to_integer stable_val = fromMaybe (0-1) $ M.lookup code (stable fs) >>= vcd_to_integer time = now fs -- timeok = timeOK (sc_nextTime cmd) time valueok = changed_val == (sc_crcfunction cmd) stable_val vnow = to_VCDValue (sc_width cmd) changed_val vexpected = to_VCDValue (sc_width cmd) $ (sc_crcfunction cmd) stable_val -- doWaiting = let prop = show cmd ++ " Started" ok = (sc_startVal cmd) == changed_val cmd' = cmd {sc_state = Running ,sc_nextTime = incrTime time (sc_timeIncr cmd) } in if (ok) then SetProperty prop (\cs -> UpdateCS code fnum cmd' success) else Succeed -- doRunning = let prop = show cmd ++ " Completed" completed = (sc_count cmd) == 1 + (sc_currentCount cmd) cmd' = cmd {sc_currentCount = 1+ (sc_currentCount cmd) ,sc_nextTime = incrTime time (sc_timeIncr cmd) ,sc_state = if (completed) then Finished else Running} errMsg = "at time: " ++ show time ++ "\n Expected: " ++ show vexpected ++ "\n Got: " ++ show vnow ++ "\n " ++ show cmd -- in case (completed, timeok, valueok) of (True, True, True) -> UpdateCS code fnum cmd' (set_prop prop) (False, True, True) -> UpdateCS code fnum cmd' success (_, True, False) -> UpdateCS code fnum cmd' $ failure $ "Incorrect Value: " ++ errMsg (_, False, True) -> UpdateCS code fnum cmd' $ failure $ "Incorrect Time: " ++ errMsg (_, False, False) -> UpdateCS code fnum cmd' $ failure $ "Incorrect Time and Value: " ++ errMsg -- doFinished = Fail $ "Signal " ++ sc_signal cmd ++ " changed at " ++ (show time) ++ " after completion. " ++ show cmd in case (sc_state cmd) of Waiting -> doWaiting Running -> doRunning Finished -> doFinished -- This crc function is derivied from an BSV function in -- testsuite/bsc.bluetcl/verific/probeinsetion/perftest/Flooder.bsv nextData crcFunction :: (Integral a) => a -> Integer -> Integer crcFunction width din = dout `rem` (1 `shiftL` w) where w = fromIntegral width dout = (din `xor` sh) + 1 sh = (din `shiftL` 5) .|. (din `shiftR` (w-5)) -- Compiles CheckCmds into a CheckerState containing all of -- the desired checkers. initState :: Options -> CheckerState initState opts = let cmds = optCheckCmds opts checkers = concatMap cmdToCheckers cmds initFS nm = FS { name = fromMaybe "" nm , scope = [] , stable = M.empty , changing = M.empty , ondefs = M.empty , enddefs = [] , watching = M.empty , endvcd = [] , now = 0 } cs = CS { props = S.empty , waiting = M.empty , user = M.empty , state1 = initFS (optVCD1 opts) , state2 = initFS (optVCD2 opts) } (init_cs,msgs) = foldl execChecker (cs,[]) checkers in if (null msgs) then init_cs else internalError $ "Failures when initializing checkers:\n" ++ (unlines msgs) -- Execute a checker and update the CheckerState and Fail messages execChecker :: (CheckerState,[String]) -> Checker -> (CheckerState,[String]) execChecker (cs,msgs) chk = case (chk cs) of Succeed -> (cs,msgs) (Fail msg) -> (cs,msgs ++ [msg]) (SetProperty prop nxt) -> let props' = S.insert prop (props cs) in execChecker (cs { props = props' },msgs) nxt (OnDef fnum name nxt_fn) -> let fs = getFS fnum cs ondefs' = M.insertWith (++) name [nxt_fn] (ondefs fs) in (setFS fnum (fs { ondefs = ondefs' }) cs,msgs) (EndDef fnum nxt) -> let fs = getFS fnum cs enddefs' = nxt:(enddefs fs) in (setFS fnum (fs { enddefs = enddefs' }) cs,msgs) (Wait t nxt) -> let waiting' = M.insertWith (++) t [nxt] (waiting cs) in (cs { waiting = waiting' },msgs) (Watch fnum code nxt) -> let fs = getFS fnum cs watching' = M.insertWith (++) code [nxt] (watching fs) in (setFS fnum (fs { watching = watching' }) cs,msgs) (EndVCD fnum nxt) -> let fs = getFS fnum cs endvcd' = nxt:(endvcd fs) in (setFS fnum (fs { endvcd = endvcd' }) cs,msgs) (UpdateCS code fnum scmd nxt) -> let user' = M.insert (fnum,code) scmd (user cs) in execChecker (cs {user=user'}, msgs) nxt -- Process a VCD command and update the checker state handleCmd :: (CheckerState,[String]) -> (FileNum,VCDCmd) -> (CheckerState,[String]) handleCmd (cs,msgs) (fnum, (Scope _ s)) = let fs = getFS fnum cs fs' = fs { scope = s:(scope fs) } in (setFS fnum fs' cs,msgs) handleCmd (cs,msgs) (fnum, UpScope) = let fs = getFS fnum cs fs' = fs { scope = tail (scope fs) } in (setFS fnum fs' cs,msgs) handleCmd (cs,msgs) (fnum, (Var _ width code s)) = let fs = getFS fnum cs stripped = takeWhile (/='[') s varname = intercalate "." $ reverse (stripped:(scope fs)) activated = M.findWithDefault [] varname (ondefs fs) cs' = setFS fnum (fs { ondefs = (M.delete varname (ondefs fs)) }) cs in foldl execChecker (cs',msgs) (concatMap (\f -> f (code,width)) activated) handleCmd (cs,msgs) (fnum, EndDefs) = let fs = getFS fnum cs activated = enddefs fs cs' = setFS fnum (fs { ondefs = M.empty, enddefs = [] }) cs in foldl execChecker (cs',msgs) activated handleCmd (cs,msgs) (fnum, (Timestamp t)) = let (cs',msgs') = flushWaiting (cs,msgs) t fs = getFS fnum cs' stable' = M.union (changing fs) (stable fs) fs' = if (stable' == stable') -- force thunks then fs { stable = stable', changing = M.empty, now = t } else error "not good" cs_new_time = setFS fnum fs' cs' in (cs_new_time,msgs') handleCmd (cs,msgs) (fnum, (Task "dumpvars" chs)) = foldl handleCmd (cs,msgs) (zip (repeat fnum) (map Change chs)) handleCmd (cs,msgs) (fnum, (Task _ _)) = (cs,msgs) handleCmd (cs,msgs) (fnum, (Change chg)) = let fs = getFS fnum cs code = signal_code chg value = new_value chg activated = M.findWithDefault [] code (watching fs) changing' = M.insert code value (changing fs) cs' = if (changing' == changing') -- force thunks then setFS fnum (fs { changing = changing' }) cs else error "not good" in foldl execChecker (cs',msgs) activated handleCmd (cs,msgs) (fnum,(VCDErr msg text)) = let fs = getFS fnum cs in (cs, msgs ++ [(name fs) ++ ": " ++ msg ++ " in `" ++ text ++ "'"]) handleCmd (cs,msgs) _ = (cs,msgs) -- Flush commands waiting at a particular time flushWaiting :: (CheckerState,[String]) -> Integer -> (CheckerState,[String]) flushWaiting (cs,msgs) t = let (before,at,later) = M.splitLookup t (waiting cs) cs' = cs { waiting = case (at) of (Just chks) -> M.insert t chks later Nothing -> later } activated = concat (M.elems before) in foldl execChecker (cs',msgs) activated -- A left fold for commands which exits early once all non-end checkers -- have been dispatched foldCmds :: ((CheckerState,[String]) -> (FileNum,VCDCmd) -> (CheckerState,[String])) -> (CheckerState,[String]) -> [(FileNum,VCDCmd)] -> (CheckerState,[String]) foldCmds handler state [] = state foldCmds handler state@(cs,msgs) (cmd:rest) = let fs1 = getFS 1 cs fs2 = getFS 2 cs quiescent1 = M.null (waiting cs) && M.null (ondefs fs1) && null (enddefs fs1) && M.null (watching fs1) quiescent2 = M.null (waiting cs) && M.null (ondefs fs2) && null (enddefs fs2) && M.null (watching fs2) in if (quiescent1 && quiescent2) then state else foldCmds handler (handler state cmd) rest -- ------------------------------------------------------------------- -- Main program routine main :: IO () main = do -- parse command line arguments argv <- getArgs bluespecdir <- getEnvDef "BLUESPECDIR" dfltBluespecDir let (opts, args, emsgs) = parseOpts argv bluespecdir -- handle errors and/or request for help and version info checkCmdLine opts args emsgs ok <- if (isJust (optVCD2 opts)) then compareTwoVCDs opts else checkOneVCD opts exitWith (if ok then ExitSuccess else (ExitFailure 2)) checkOneVCD :: Options -> IO Bool checkOneVCD opts = do let vcd_in = fromJust (optVCD1 opts) bracket (openFile vcd_in ReadMode) (\hIn -> do { hClose hIn; return False }) (\hIn -> do txt <- C.hGetContents hIn let cmds = map (\x -> (file1,x)) (parseVCD txt) cs0 = initState opts (cs1,msgs1) = foldCmds handleCmd (cs0,[]) cmds (cs2,msgs2) = flushWaiting (cs1,msgs1) (now (state1 cs1) + 1) (cs3,msgs3) = foldl execChecker (cs2,msgs2) (endvcd (state1 cs2)) stranded = waiting cs3 smsgs = if (M.null stranded) then [] else [ intercalate "\n" $ [ vcd_in ++ " ends before checkers at time: " ] ++ [ " " ++ (show t) | t <- M.keys stranded ] ] msgs = msgs3 ++ smsgs when (not (null msgs)) $ mapM_ putStrLn msgs return (null msgs) ) compareTwoVCDs :: Options -> IO Bool compareTwoVCDs opts = do putStrLn $ "Checking " ++ (fromJust (optVCD1 opts)) ++ " against " ++ (fromJust (optVCD2 opts)) return True