From e2f6a008feb304fd4e6497bfc41a4a32740e2adf Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 10 Nov 2019 21:13:06 +0000 Subject: Add counter example parsing --- src/Verismith.hs | 34 ++++++------- src/Verismith/CounterEg.hs | 112 +++++++++++++++++++++++++++++++++++++++++ src/Verismith/Fuzz.hs | 4 +- src/Verismith/Reduce.hs | 6 +-- src/Verismith/Report.hs | 14 +++--- src/Verismith/Tool/Internal.hs | 3 +- src/Verismith/Tool/Yosys.hs | 38 +++++++------- verismith.cabal | 1 + 8 files changed, 165 insertions(+), 47 deletions(-) create mode 100644 src/Verismith/CounterEg.hs diff --git a/src/Verismith.hs b/src/Verismith.hs index 19237ae..48f851e 100644 --- a/src/Verismith.hs +++ b/src/Verismith.hs @@ -72,6 +72,19 @@ import Verismith.Tool.Internal import Verismith.Verilog import Verismith.Verilog.Parser (parseSourceInfoFile) +-- | Generate a specific number of random bytestrings of size 256. +randomByteString :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString] +randomByteString gen n bytes + | n == 0 = ranBytes : bytes + | otherwise = randomByteString newGen (n - 1) $ ranBytes : bytes + where Right (ranBytes, newGen) = C.genBytes 32 gen + +-- | generates the specific number of bytestring with a random seed. +generateByteString :: Int -> IO [ByteString] +generateByteString n = do + gen <- C.newGenIO :: IO C.CtrDRBG + return $ randomByteString gen n [] + toFP :: String -> FilePath toFP = fromText . T.pack @@ -196,10 +209,10 @@ handleOpts (Reduce f t _ ls' True) = do runSynth b src runEquiv (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" + 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" @@ -218,19 +231,6 @@ defaultMain = do optsparsed <- execParser opts handleOpts optsparsed --- | Generate a specific number of random bytestrings of size 256. -randomByteString :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString] -randomByteString gen n bytes - | n == 0 = ranBytes : bytes - | otherwise = randomByteString newGen (n - 1) $ ranBytes : bytes - where Right (ranBytes, newGen) = C.genBytes 32 gen - --- | generates the specific number of bytestring with a random seed. -generateByteString :: Int -> IO [ByteString] -generateByteString n = do - gen <- C.newGenIO :: IO C.CtrDRBG - return $ randomByteString gen n [] - makeSrcInfo :: ModDecl -> SourceInfo makeSrcInfo m = SourceInfo (getIdentifier $ m ^. modId) (Verilog [m]) diff --git a/src/Verismith/CounterEg.hs b/src/Verismith/CounterEg.hs new file mode 100644 index 0000000..f5547ed --- /dev/null +++ b/src/Verismith/CounterEg.hs @@ -0,0 +1,112 @@ +{-| +Module : Verismith.CounterEg +Description : Counter example parser to load the counter example +Copyright : (c) 2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX +-} + +module Verismith.CounterEg + ( CounterEg(..) + , parseCounterEg + ) +where + +import Control.Applicative ((<|>)) +import Data.Bifunctor (bimap) +import Data.Binary (encode) +import Data.Bits (shiftL, (.|.)) +import Data.ByteString (ByteString) +import qualified Data.ByteString as B +import qualified Data.ByteString.Lazy as L +import Data.Char (digitToInt) +import Data.Functor (($>)) +import Data.Maybe (listToMaybe) +import Data.Text (Text) +import qualified Data.Text as T +import Numeric (readInt) +import qualified Text.Parsec as P + +data CounterEg = CounterEg { _counterEgInitial :: ![(Text, Int)] + , _counterEgStates :: ![[(Text, Int)]] + } + deriving (Eq, Show) + +instance Semigroup CounterEg where + CounterEg a b <> CounterEg c d = CounterEg (a <> c) (b <> d) + +instance Monoid CounterEg where + mempty = CounterEg mempty mempty + +type Parser = P.Parsec String () + +fromBytes :: ByteString -> Int +fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b + +convert :: String -> ByteString +convert = + L.toStrict + . (encode :: Integer -> L.ByteString) + . maybe 0 fst + . listToMaybe + . readInt 2 (`elem` ("01" :: String)) digitToInt + +convertBinary :: String -> Int +convertBinary = fromBytes . convert + +lexme :: Parser a -> Parser a +lexme f = do { a <- f; _ <- P.spaces; return a } + +nameChar :: Parser Char +nameChar = P.alphaNum + <|> P.oneOf "$.:_" + +parens :: Parser a -> Parser a +parens = lexme . P.between (P.char '(') (P.char ')') + +brackets :: Parser a -> Parser a +brackets = lexme . P.between (P.char '[') (P.char ']') + +trueOrFalse :: Parser String +trueOrFalse = lexme $ (P.string "true" $> "1") <|> (P.string "false" $> "0") + +assumeBody :: Parser (String, String) +assumeBody = lexme $ do + name <- P.char '=' *> P.spaces *> brackets (P.many1 nameChar) + num <- P.spaces *> ((P.string "#b" *> P.many1 P.digit) <|> trueOrFalse) + return (name, num) + +parseAssume :: Parser (String, String) +parseAssume = lexme $ P.string "assume" *> P.spaces *> parens assumeBody + +parseInitial :: Parser [(String, String)] +parseInitial = lexme $ do + _ <- lexme $ P.string "initial" + P.many parseAssume + +parseState :: Parser (String, [(String, String)]) +parseState = lexme $ do + n <- lexme $ P.string "state" *> P.spaces *> P.many1 P.digit + assumes <- P.many parseAssume + return (n, assumes) + +parseCE :: Parser [[(String, String)]] +parseCE = lexme $ do + i <- parseInitial + other <- fmap snd <$> P.many parseState + return (i : other) + +cEtoCounterEg :: [[(String, String)]] -> CounterEg +cEtoCounterEg [] = mempty +cEtoCounterEg (i : is) = CounterEg (bimap T.pack convertBinary <$> i) + (fmap (bimap T.pack convertBinary) <$> is) + +parseCounterEg' :: Parser CounterEg +parseCounterEg' = lexme $ do + _ <- P.spaces + cEtoCounterEg <$> parseCE + +parseCounterEg :: Text -> Either String CounterEg +parseCounterEg = bimap show id . P.parse parseCounterEg' "" . T.unpack diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs index d14e74b..b600d68 100644 --- a/src/Verismith/Fuzz.hs +++ b/src/Verismith/Fuzz.hs @@ -325,8 +325,8 @@ generateByteString n = do failEquivWithIdentity :: (MonadSh m) => Fuzz m [SynthResult] failEquivWithIdentity = filter withIdentity . _fuzzSynthResults <$> get where - withIdentity (SynthResult (IdentitySynth _) _ (Fail EquivFail) _) = True - withIdentity (SynthResult _ (IdentitySynth _) (Fail EquivFail) _) = True + withIdentity (SynthResult (IdentitySynth _) _ (Fail (EquivFail _)) _) = True + withIdentity (SynthResult _ (IdentitySynth _) (Fail (EquivFail _)) _) = True withIdentity _ = False passEquiv :: (MonadSh m) => Fuzz m [SynthResult] diff --git a/src/Verismith/Reduce.hs b/src/Verismith/Reduce.hs index cff61ed..69b5e17 100644 --- a/src/Verismith/Reduce.hs +++ b/src/Verismith/Reduce.hs @@ -613,9 +613,9 @@ reduceSynth datadir a b = reduce synth runSynth b src' runEquiv datadir a b src' return $ case r of - Fail EquivFail -> True - Fail _ -> False - Pass _ -> False + Fail (EquivFail _) -> True + Fail _ -> False + Pass _ -> False reduceSynthesis :: (Synthesiser a, MonadSh m) => a -> SourceInfo -> m SourceInfo reduceSynthesis a = reduce synth diff --git a/src/Verismith/Report.hs b/src/Verismith/Report.hs index 196e891..743240d 100644 --- a/src/Verismith/Report.hs +++ b/src/Verismith/Report.hs @@ -236,13 +236,13 @@ descriptionToSynth s = error $ "Could not find implementation for synthesiser '" <> show s <> "'" status :: Result Failed () -> Html -status (Pass _ ) = H.td ! A.class_ "is-success" $ "Passed" -status (Fail EmptyFail ) = H.td ! A.class_ "is-danger" $ "Failed" -status (Fail EquivFail ) = H.td ! A.class_ "is-danger" $ "Equivalence failed" -status (Fail SimFail ) = H.td ! A.class_ "is-danger" $ "Simulation failed" -status (Fail SynthFail ) = H.td ! A.class_ "is-danger" $ "Synthesis failed" -status (Fail EquivError ) = H.td ! A.class_ "is-danger" $ "Equivalence error" -status (Fail TimeoutError) = H.td ! A.class_ "is-warning" $ "Time out" +status (Pass _ ) = H.td ! A.class_ "is-success" $ "Passed" +status (Fail EmptyFail ) = H.td ! A.class_ "is-danger" $ "Failed" +status (Fail (EquivFail _)) = H.td ! A.class_ "is-danger" $ "Equivalence failed" +status (Fail SimFail ) = H.td ! A.class_ "is-danger" $ "Simulation failed" +status (Fail SynthFail ) = H.td ! A.class_ "is-danger" $ "Synthesis failed" +status (Fail EquivError ) = H.td ! A.class_ "is-danger" $ "Equivalence error" +status (Fail TimeoutError) = H.td ! A.class_ "is-warning" $ "Time out" synthStatusHtml :: SynthStatus -> Html synthStatusHtml (SynthStatus synth res diff) = H.tr $ do diff --git a/src/Verismith/Tool/Internal.hs b/src/Verismith/Tool/Internal.hs index c2e3a0c..ee31c4e 100644 --- a/src/Verismith/Tool/Internal.hs +++ b/src/Verismith/Tool/Internal.hs @@ -54,6 +54,7 @@ import Prelude hiding (FilePath) import Shelly import Shelly.Lifted (MonadSh, liftSh) import System.FilePath.Posix (takeBaseName) +import Verismith.CounterEg (CounterEg) import Verismith.Internal import Verismith.Result import Verismith.Verilog.AST @@ -74,7 +75,7 @@ class Tool a => Simulator a where -> ResultSh ByteString data Failed = EmptyFail - | EquivFail + | EquivFail CounterEg | EquivError | SimFail | SynthFail diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs index afbffe9..67f8536 100644 --- a/src/Verismith/Tool/Yosys.hs +++ b/src/Verismith/Tool/Yosys.hs @@ -23,11 +23,14 @@ where import Control.DeepSeq (NFData, rnf, rwhnf) import Control.Lens import Control.Monad (void) +import Data.Either (fromRight) import Data.Text (Text, unpack) import Prelude hiding (FilePath) -import Shelly -import Shelly.Lifted (liftSh) +import Shelly (FilePath, ()) +import qualified Shelly as S +import Shelly.Lifted (liftSh, readfile) import Text.Shakespeare.Text (st) +import Verismith.CounterEg (parseCounterEg) import Verismith.Result import Verismith.Tool.Internal import Verismith.Tool.Template @@ -59,13 +62,13 @@ defaultYosys :: Yosys defaultYosys = Yosys Nothing "yosys" "syn_yosys.v" yosysPath :: Yosys -> FilePath -yosysPath sim = maybe (fromText "yosys") ( fromText "yosys") $ yosysBin sim +yosysPath sim = maybe (S.fromText "yosys") ( S.fromText "yosys") $ yosysBin sim runSynthYosys :: Yosys -> SourceInfo -> ResultSh () runSynthYosys sim (SourceInfo _ src) = do dir <- liftSh $ do - dir' <- pwd - writefile inpf $ genSource src + dir' <- S.pwd + S.writefile inpf $ genSource src return dir' execute_ SynthFail @@ -77,8 +80,8 @@ runSynthYosys sim (SourceInfo _ src) = do ] where inpf = "rtl.v" - inp = toTextIgnore inpf - out = toTextIgnore $ synthOutput sim + inp = S.toTextIgnore inpf + out = S.toTextIgnore $ synthOutput sim runEquivYosys :: (Synthesiser a, Synthesiser b) @@ -89,24 +92,24 @@ runEquivYosys -> ResultSh () runEquivYosys yosys sim1 sim2 srcInfo = do liftSh $ do - writefile "top.v" + S.writefile "top.v" . genSource . initMod . makeTop 2 $ srcInfo ^. mainModule - writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo + S.writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo runSynth sim1 srcInfo runSynth sim2 srcInfo - liftSh $ run_ (yosysPath yosys) [toTextIgnore checkFile] - where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|] + liftSh $ S.run_ (yosysPath yosys) [S.toTextIgnore checkFile] + where checkFile = S.fromText [st|test.#{toText sim1}.#{toText sim2}.ys|] runEquiv :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> ResultSh () runEquiv datadir sim1 sim2 srcInfo = do - dir <- liftSh pwd + dir <- liftSh S.pwd liftSh $ do - writefile "top.v" + S.writefile "top.v" . genSource . initMod . makeTopAssert @@ -114,14 +117,15 @@ runEquiv datadir sim1 sim2 srcInfo = do ^. mainModule replaceMods (synthOutput sim1) "_1" srcInfo replaceMods (synthOutput sim2) "_2" srcInfo - writefile "proof.sby" $ sbyConfig datadir sim1 sim2 srcInfo + S.writefile "proof.sby" $ sbyConfig datadir sim1 sim2 srcInfo e <- liftSh $ do exe dir "symbiyosys" "sby" ["-f", "proof.sby"] - lastExitCode + S.lastExitCode case e of 0 -> ResultT . return $ Pass () - 2 -> ResultT . return $ Fail EquivFail + 2 -> ResultT $ Fail . EquivFail . fromRight mempty + . parseCounterEg <$> readfile "proof/engine_0/trace.smtc" 124 -> ResultT . return $ Fail TimeoutError _ -> ResultT . return $ Fail EquivError where - exe dir name e = void . errExit False . logCommand dir name . timeout e + exe dir name e = void . S.errExit False . logCommand dir name . timeout e diff --git a/verismith.cabal b/verismith.cabal index 61fd087..b54e522 100644 --- a/verismith.cabal +++ b/verismith.cabal @@ -47,6 +47,7 @@ library , Verismith.Circuit.Internal , Verismith.Circuit.Random , Verismith.Config + , Verismith.CounterEg , Verismith.Fuzz , Verismith.Generate , Verismith.Internal -- cgit