diff --git a/src/Search/Search.hs b/src/Search/Search.hs index e173e24cbde07a58dbe9bb650241ff5b01aed9b3..84cface256a62b8803c780464d96c6fb4c117445 100644 --- a/src/Search/Search.hs +++ b/src/Search/Search.hs @@ -80,14 +80,11 @@ findOpenDecision = listToMaybe . mapMaybe isHalf . M.elems . decisions -driver :: FilePath - -> Bool -- ^ Identify states on different locations? - -> IO () -driver prog identStates = driver' prog identStates (Vertex "start" (Metadata "" "")) ---driver prog True = driver' prog (Vertex ("", "start") :: Vertex 'OnlyState) - -driver' :: FilePath -> Bool -> Vertex -> IO () -driver' prog identStates startVertex = do +driver :: FilePath -> IO () +driver prog = driver' prog (Vertex "start" (Metadata "" "")) + +driver' :: FilePath -> Vertex -> IO () +driver' prog startVertex = do state <- newIORef (State M.empty (Just startVertex) M.empty []) oneProgRun prog state Nothing @@ -96,7 +93,7 @@ driver' prog identStates startVertex = do findOpenDecision <$> readIORef state >>= \case Nothing -> do s <- readIORef state - T.putStrLn (graph2Dot identStates (graph s)) + T.putStrLn (graph2Dot (graph s)) exitSuccess Just trace -> oneProgRun prog state (Just $ reverse trace) @@ -164,17 +161,17 @@ handleLine pstdin state = parseLine pstdin >>= \case NewState vert -> modifyIORef state (addVertex vert) >> return (NewState vert) other -> return other -graph2Dot :: Bool -> Graph -> Text -graph2Dot is graph = +graph2Dot :: Graph -> Text +graph2Dot graph = "digraph gcfg {\n" - <> dotNodes is graph + <> dotNodes graph <> M.foldMapWithKey nodeStr graph <> "}" where nodeStr from tos = mconcat $ map (arrow from) $ S.toList tos - arrow from to = " " <> nodeId is from <> " -> " - <> nodeId is to <> " [label=\"" <> edgeLabel (metaSyscall $ vertMeta from) <> "\"];\n" + arrow from to = " " <> nodeId from <> " -> " + <> nodeId to <> " [label=\"" <> edgeLabel (metaSyscall $ vertMeta from) <> "\"];\n" -- | Generate readable edge label from syscall name -- @@ -186,19 +183,18 @@ edgeLabel (T.stripPrefix "OSEKOS_" -> Just txt) = in derscore call <> "(" <> derscore argument <> ")" edgeLabel txt = txt -- There are "syscalls" that don't begin with OSEKOS_. E.g ISRs -dotNodes :: Bool -> Graph -> Text -dotNodes is = foldMap formatNode . allNotes +dotNodes :: Graph -> Text +dotNodes = foldMap formatNode . allNotes where allNotes m = M.keysSet m `S.union` fold m - formatNode vert = nodeId is vert + formatNode vert = nodeId vert <> " [label=\"" <> "State: " <> vertState vert <> "\\nFunction: " <> stripPrefix' "OSEKOS_" (metaFunc (vertMeta vert)) <> "\", shape=box];\n" -nodeId :: Bool -> Vertex -> Text -nodeId False vert = "node" <> vertState vert <> "_" <> metaSyscall (vertMeta vert) -nodeId True vert = "node" <> vertState vert +nodeId :: Vertex -> Text +nodeId vert = "node" <> vertState vert <> "_" <> metaSyscall (vertMeta vert) -- | Strip prefix but return original string if it doesn't begin with the prefix stripPrefix' :: Text -> Text -> Text diff --git a/src/main/Main.hs b/src/main/Main.hs index 3ac905d32d9b5257378dc087fe5d0837b578fafd..e0bf9940fbfa5b21f898c80914aadf1c920fcf9e 100644 --- a/src/main/Main.hs +++ b/src/main/Main.hs @@ -5,14 +5,16 @@ module Main where import qualified Data.ByteString.Lazy as BS import qualified Data.Text.IO as T import Options.Applicative +import System.Exit +import System.IO -import CFG.Types +import CFG.Types import qualified CFG.Parser as P -import CFG.Graph -import CFG.IR -import CFG.C -import CFG.Sanitize -import Search.Search +import CFG.Graph +import CFG.IR +import CFG.C +import CFG.Sanitize +import Search.Search data Command = Mockup MockupOpts | Search SearchOpts @@ -50,7 +52,12 @@ main = do cmd <- execParser $ info (helper <*> optParser) ( fullDesc <> progDesc "dOSEK verification tool" ) case cmd of - (Search opts) -> driver (mockupExecutable opts) (identifyStates opts) + (Search opts) -> do + if (identifyStates opts) then do + hPutStrLn stderr "--identify-states is currently not implemented, sorry" + exitFailure + else + driver (mockupExecutable opts) Mockup opts -> do cntnt <- BS.getContents case P.parseFile cntnt of