path: root/src/Verismith.hs

{-|
Module      : Verismith
Description : Verismith
Copyright   : (c) 2018-2019, Yann Herklotz
License     : GPL-3
Maintainer  : yann [at] yannherklotz [dot] com
Stability   : experimental
Portability : POSIX
-}

{-# OPTIONS_GHC -Wno-unused-top-binds #-}

module Verismith
    ( defaultMain
    -- * Types
    , Opts(..)
    , SourceInfo(..)
    -- * Run functions
    , runEquivalence
    , runSimulation
    , runReduce
    , draw
    -- * Verilog generation functions
    , procedural
    , proceduralIO
    , proceduralSrc
    , proceduralSrcIO
    , randomMod
    -- * Extra modules
    , module Verismith.Verilog
    , module Verismith.Config
    , module Verismith.Circuit
    , module Verismith.Tool
    , module Verismith.Fuzz
    , module Verismith.Report
    )
where

import           Control.Concurrent
import           Control.Lens             hiding ((<.>))
import           Control.Monad.IO.Class   (liftIO)
import           Data.ByteString          (ByteString)
import           Data.ByteString.Builder  (byteStringHex, toLazyByteString)
import qualified Data.ByteString.Lazy     as L
import qualified Data.Graph.Inductive     as G
import qualified Data.Graph.Inductive.Dot as G
import           Data.Maybe               (isNothing)
import           Data.Text                (Text)
import qualified Data.Text                as T
import           Data.Text.Encoding       (decodeUtf8)
import qualified Data.Text.IO             as T
import           Hedgehog                 (Gen)
import qualified Hedgehog.Gen             as Hog
import           Hedgehog.Internal.Seed   (Seed)
import           Options.Applicative
import           Paths_verismith          (getDataDir)
import           Prelude                  hiding (FilePath)
import           Shelly                   hiding (command)
import           Shelly.Lifted            (liftSh)
import           System.Random            (randomIO)
import           Verismith.Circuit
import           Verismith.Config
import           Verismith.Fuzz
import           Verismith.Generate
import           Verismith.OptParser
import           Verismith.Reduce
import           Verismith.Report
import           Verismith.Result
import           Verismith.Tool
import           Verismith.Tool.Internal
import           Verismith.Verilog
import           Verismith.Verilog.Parser (parseSourceInfoFile)
import Verismith.Utils (generateByteString)

toFP :: String -> FilePath
toFP = fromText . T.pack

myForkIO :: IO () -> IO (MVar ())
myForkIO io = do
    mvar <- newEmptyMVar
    _    <- forkFinally io (\_ -> putMVar mvar ())
    return mvar

getConfig :: Maybe FilePath -> IO Config
getConfig s =
    maybe (return defaultConfig) parseConfigFile $ T.unpack . toTextIgnore <$> s

getGenerator :: Config -> Text -> Maybe FilePath -> IO (Gen (SourceInfo ()))
getGenerator config top s =
    maybe (return $ proceduralSrc top config) (fmap return . parseSourceInfoFile top)
    $ toTextIgnore <$> s

-- | Randomly remove an option by setting it to 0.
randDelete :: Int -> IO Int
randDelete i = do
    r <- randomIO
    return $ if r then i else 0

randomise :: Config -> IO Config
randomise config@(Config a _ c d e) = do
    mia  <- return $ cm ^. probModItemAssign
    misa <- return $ cm ^. probModItemSeqAlways
    mica <- return $ cm ^. probModItemCombAlways
    mii  <- return $ cm ^. probModItemInst
    ssb  <- return $ cs ^. probStmntBlock
    ssnb <- return $ cs ^. probStmntNonBlock
    ssc  <- return $ cs ^. probStmntCond
    ssf  <- return $ cs ^. probStmntFor
    en   <- return $ ce ^. probExprNum
    keep_out <- return $ cmo ^. probModDropOutput
    drop_out <- randDelete $ cmo ^. probModDropOutput
    ei   <- randDelete $ ce ^. probExprId
    ers  <- randDelete $ ce ^. probExprRangeSelect
    euo  <- randDelete $ ce ^. probExprUnOp
    ebo  <- randDelete $ ce ^. probExprBinOp
    ec   <- randDelete $ ce ^. probExprCond
    eco  <- randDelete $ ce ^. probExprConcat
    estr <- randDelete $ ce ^. probExprStr
    esgn <- randDelete $ ce ^. probExprSigned
    eus  <- randDelete $ ce ^. probExprUnsigned
    return $ Config
        a
        (Probability (ProbModItem mia misa mica mii)
                     (ProbStatement ssb ssnb ssc ssf)
                     (ProbExpr en ei ers euo ebo ec eco estr esgn eus)
                     (ProbMod drop_out keep_out)
        )
        c
        d
        e
  where
    cm = config ^. configProbability . probModItem
    cs = config ^. configProbability . probStmnt
    ce = config ^. configProbability . probExpr
    cmo = config ^. configProbability . probMod

handleOpts :: Opts -> IO ()
handleOpts (Fuzz o configF f k n nosim noequiv noreduction file top cc checker) = do
    config <- getConfig configF
    gen <- getGenerator config top file
    datadir <- getDataDir
    _      <- runFuzz
        (FuzzOpts (Just $ fromText o)
         f k n nosim noequiv noreduction config (toFP datadir) cc checker)
        defaultYosys
        (fuzzMultiple gen)
    return ()
handleOpts (Generate f c) = do
    config <- getConfig c
    source <- proceduralIO "top" config :: IO (Verilog ())
    maybe (T.putStrLn $ genSource source) (flip T.writeFile $ genSource source)
        $   T.unpack
        .   toTextIgnore
        <$> f
handleOpts (Parse f t o rc) = do
    verilogSrc <- T.readFile file
    case parseVerilog (T.pack file) verilogSrc of
        Left  l -> print l
        Right v ->
            case (o, GenVerilog
                     . mapply rc (takeReplace . removeConstInConcat)
                     $ SourceInfo t v) of
            (Nothing, a) -> print a
            (Just o', a) -> writeFile (T.unpack $ toTextIgnore o') $ show a
  where
    file = T.unpack . toTextIgnore $ f
    mapply i f = if i then f else id
handleOpts (Reduce f t _ ls' False) = do
    src <- parseSourceInfoFile t (toTextIgnore f)
    datadir <- getDataDir
    case descriptionToSynth <$> ls' of
        a : b : _ -> do
            putStrLn "Reduce with equivalence check"
            shelly $ do
                make dir
                pop dir $ do
                    src' <- reduceSynth Nothing (toFP datadir) a b src :: Sh (SourceInfo ())
                    writefile (fromText ".." </> dir <.> "v") $ genSource src'
        a : _ -> do
            putStrLn "Reduce with synthesis failure"
            shelly $ do
                make dir
                pop dir $ do
                    src' <- reduceSynthesis a src
                    writefile (fromText ".." </> dir <.> "v") $ genSource src'
        _ -> do
            putStrLn "Not reducing because no synthesiser was specified"
            return ()
    where dir = fromText "reduce"
handleOpts (Reduce f t _ ls' True) = do
    src <- parseSourceInfoFile t (toTextIgnore f) :: IO (SourceInfo ())
    datadir <- getDataDir
    case descriptionToSynth <$> ls' of
        a : b : _ -> do
            putStrLn "Starting equivalence check"
            res <- shelly . runResultT $ do
                make dir
                pop dir $ do
                    runSynth a src
                    runSynth b src
                    runEquiv Nothing (toFP datadir) a b src
            case res of
                Pass _             -> putStrLn "Equivalence check passed"
                Fail (EquivFail _) -> putStrLn "Equivalence check failed"
                Fail TimeoutError  -> putStrLn "Equivalence check timed out"
                Fail _             -> putStrLn "Equivalence check error"
            return ()
        as -> do
            putStrLn "Synthesis check"
            _ <- shelly . runResultT $ mapM (flip runSynth src) as
            return ()
    where dir = fromText "equiv"
handleOpts (ConfigOpt c conf r) = do
    config <- if r then getConfig conf >>= randomise else getConfig conf
    maybe (T.putStrLn . encodeConfig $ config) (`encodeConfigFile` config)
        $   T.unpack
        .   toTextIgnore
        <$> c

defaultMain :: IO ()
defaultMain = do
    optsparsed <- execParser opts
    handleOpts optsparsed

makeSrcInfo :: (ModDecl ann) -> (SourceInfo ann)
makeSrcInfo m = SourceInfo (getIdentifier $ m ^. modId) (Verilog [m])

-- | Draw a randomly generated DAG to a dot file and compile it to a png so it
-- can be seen.
draw :: IO ()
draw = do
    gr <- Hog.sample $ rDups . getCircuit <$> Hog.resize 10 randomDAG
    let dot = G.showDot . G.fglToDotString $ G.nemap show (const "") gr
    writeFile "file.dot" dot
    shelly $ run_ "dot" ["-Tpng", "-o", "file.png", "file.dot"]

-- | Function to show a bytestring in a hex format.
showBS :: ByteString -> Text
showBS = decodeUtf8 . L.toStrict . toLazyByteString . byteStringHex

-- | Run a simulation on a random DAG or a random module.
runSimulation :: IO ()
runSimulation = do
  -- gr <- Hog.generate $ rDups <$> Hog.resize 100 (randomDAG :: Gen (G.Gr Gate ()))
  -- let dot = G.showDot . G.fglToDotString $ G.nemap show (const "") gr
  -- writeFile "file.dot" dot
  -- shelly $ run_ "dot" ["-Tpng", "-o", "file.png", "file.dot"]
  -- let circ =
  --       head $ (nestUpTo 30 . generateAST $ Circuit gr) ^.. getVerilog . traverse . getDescription
    rand  <- generateByteString Nothing 32 20
    rand2 <- Hog.sample (randomMod 10 100) :: IO (ModDecl ())
    val   <- shelly . runResultT $ runSim defaultIcarus (makeSrcInfo rand2) rand
    case val of
        Pass a -> T.putStrLn $ showBS a
        _      -> T.putStrLn "Test failed"


-- | Code to be executed on a failure. Also checks if the failure was a timeout,
-- as the timeout command will return the 124 error code if that was the
-- case. In that case, the error will be moved to a different directory.
onFailure :: Text -> RunFailed -> Sh (Result Failed ())
onFailure t _ = do
    ex <- lastExitCode
    case ex of
        124 -> do
            logger "Test TIMEOUT"
            chdir ".." $ cp_r (fromText t) $ fromText (t <> "_timeout")
            return $ Fail EmptyFail
        _ -> do
            logger "Test FAIL"
            chdir ".." $ cp_r (fromText t) $ fromText (t <> "_failed")
            return $ Fail EmptyFail

checkEquivalence :: Show ann => SourceInfo ann -> Text -> IO Bool
checkEquivalence src dir = shellyFailDir $ do
    mkdir_p (fromText dir)
    curr <- toTextIgnore <$> pwd
    datadir <- liftIO getDataDir
    setenv "VERISMITH_ROOT" curr
    cd (fromText dir)
    catch_sh
        ((runResultT $ runEquiv Nothing (toFP datadir) defaultYosys defaultVivado src) >> return True)
        ((\_ -> return False) :: RunFailed -> Sh Bool)

-- | Run a fuzz run and check if all of the simulators passed by checking if the
-- generated Verilog files are equivalent.
runEquivalence
    :: Maybe Seed
    -> Gen (Verilog ()) -- ^ Generator for the Verilog file.
    -> Text        -- ^ Name of the folder on each thread.
    -> Text        -- ^ Name of the general folder being used.
    -> Bool        -- ^ Keep flag.
    -> Int         -- ^ Used to track the recursion.
    -> IO ()
runEquivalence seed gm t d k i = do
    (_, m) <- shelly $ sampleSeed seed gm
    let srcInfo = SourceInfo "top" m
    rand <- generateByteString Nothing 32 20
    datadir <- getDataDir
    shellyFailDir $ do
        mkdir_p (fromText d </> fromText n)
        curr <- toTextIgnore <$> pwd
        setenv "VERISMITH_ROOT" curr
        cd (fromText "output" </> fromText n)
        _ <-
            catch_sh
                    (  runResultT
                    $  runEquiv Nothing (toFP datadir) defaultYosys defaultVivado srcInfo
                    >> liftSh (logger "Test OK")
                    )
                $ onFailure n
        _ <-
            catch_sh
                    (   runResultT
                    $   runSim (Icarus "iverilog" "vvp") srcInfo rand
                    >>= (\b -> liftSh $ logger ("RTL Sim: " <> showBS b))
                    )
                $ onFailure n
        cd ".."
        unless k . rm_rf $ fromText n
    when (i < 5 && isNothing seed) (runEquivalence seed gm t d k $ i + 1)
    where n = t <> "_" <> T.pack (show i)

runReduce :: (SourceInfo ()) -> IO (SourceInfo ())
runReduce s =
    shelly $ reduce "reduce.v" (\s' -> not <$> liftIO (checkEquivalence s' "reduce")) s