aboutsummaryrefslogtreecommitdiffstats
path: root/src/Verismith.hs
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2019-11-10 21:13:06 +0000
committerYann Herklotz <git@yannherklotz.com>2019-11-10 21:13:06 +0000
commite2f6a008feb304fd4e6497bfc41a4a32740e2adf (patch)
tree3e5522243e32b4c7d9932ed329076f8f2cfb2ede /src/Verismith.hs
parent0438eb4999c3d03ec9a22afbc88b30e0fa131aa6 (diff)
downloadverismith-e2f6a008feb304fd4e6497bfc41a4a32740e2adf.tar.gz
verismith-e2f6a008feb304fd4e6497bfc41a4a32740e2adf.zip
Add counter example parsing
Diffstat (limited to 'src/Verismith.hs')
-rw-r--r--src/Verismith.hs34
1 files changed, 17 insertions, 17 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])