diff --git a/osek-verification.cabal b/osek-verification.cabal index 1d573839733aa811750fe3816a882a8c1c3e2780..041b826f8a21b2699d0748857996d6d22bf4b684 100644 --- a/osek-verification.cabal +++ b/osek-verification.cabal @@ -55,6 +55,7 @@ executable mockup_generator , bytestring >= 0.10 && <0.11 , osek-verification , optparse-applicative >= 0.12 && <0.13 + , microlens >= 0.4 && < 0.5 hs-source-dirs: src/main default-language: Haskell2010 ghc-options: -Wall -fdefer-typed-holes -fno-warn-name-shadowing diff --git a/src/main/Main.hs b/src/main/Main.hs index 9245342908416fdb06e6c9d78005f6543bd55f52..6b3eddc6f2c0f34fd368dbcc8b5d5f04acf93209 100644 --- a/src/main/Main.hs +++ b/src/main/Main.hs @@ -3,10 +3,13 @@ module Main where import Control.Monad +import System.IO +import System.Exit import qualified Data.ByteString.Lazy as BS import qualified Data.Text.IO as T import Options.Applicative +import Lens.Micro import CFG.Types import qualified CFG.Parser as P @@ -15,6 +18,9 @@ import CFG.IR import CFG.C import CFG.Sanitize import Search.Search +import qualified Compare.JSON as JSON +import Compare.Compare +import Compare.Types data Command = Mockup MockupOpts | Search SearchOpts @@ -27,12 +33,14 @@ optParser = subparser data SearchOpts = SearchOpts { mockupExecutable :: FilePath + , sseGraphJsonFile :: Maybe FilePath , eliminateEpsilons :: Bool } searchOptParser :: Parser SearchOpts searchOptParser = SearchOpts <$> argument str (metavar "EXECUTABLE") + <*> optional (argument str (metavar "SSE-JSON")) <*> (not <$> switch ( long "no-epsilon-elimination" <> help "Don't do epsilon elimination on the search graph" )) @@ -53,7 +61,20 @@ main = do ( fullDesc <> progDesc "dOSEK verification tool" ) case cmd of (Search opts) -> do - void (driver (eliminateEpsilons opts) (mockupExecutable opts)) + json <- traverse BS.readFile (sseGraphJsonFile opts) + case JSON.parseFile <$> json of + -- Don't do any comparision between graphs + Nothing -> void (driver (eliminateEpsilons opts) (mockupExecutable opts)) + Just (Left e) -> do + hPutStrLn stderr $ "Could not parse sse graph json: " <> e + exitFailure + Just (Right graph1) -> do + graph2 <- driver (eliminateEpsilons opts) (mockupExecutable opts) + if (not (isDeterministic (graph1^._graph)) || not (isDeterministic (graph2^._graph))) then do + hPutStrLn stderr $ "One of the graphs is not deterministic" + exitFailure + else + hPrint stderr (isIsomorphic graph1 graph2) Mockup opts -> do cntnt <- BS.getContents case P.parseFile cntnt of