Add counter example parsing

8 files changed, 165 insertions, 47 deletions

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