diff --git a/osek-verification.cabal b/osek-verification.cabal index b4a5ab9da3082cb91690ca5ef555e4505ac7f0aa..114370ca8dc06b69289fd0e733459ed480596f20 100644 --- a/osek-verification.cabal +++ b/osek-verification.cabal @@ -22,6 +22,7 @@ library , CFG.Types , CFG.Sanitize , Search.States2Dot + , Search.Search hs-source-dirs: src build-depends: base >=4.8 && <4.10 , megaparsec >= 5 && <5.1 @@ -32,6 +33,7 @@ library , aeson >= 1.0 && <1.1 , bytestring >= 0.10 && <0.11 , mtl >= 2.2 && <2.3 + , process >= 1.4 && <1.5 default-language: Haskell2010 executable mockup_generator diff --git a/src/Search/Search.hs b/src/Search/Search.hs new file mode 100644 index 0000000000000000000000000000000000000000..2e4c38589bb9a6491ea142b00b881803f7941d60 --- /dev/null +++ b/src/Search/Search.hs @@ -0,0 +1,151 @@ +{-# LANGUAGE LambdaCase, OverloadedStrings #-} + +module Search.Search (driver) where + +import Data.Map (Map) +import qualified Data.Map as M +import Data.Set (Set) +import qualified Data.Set as S +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.Text.IO as T +import Data.Maybe +import Data.Monoid +import Data.IORef +import Control.Monad +import System.Exit +import System.Process +import System.IO + +type Vertex = Text + +type Graph = Map Vertex (Set Vertex) + +type DecisionNumber = Int +type Decision = (Vertex, DecisionNumber) +data DecisionState = Half [Bool] -- Trace + | Full + +data State = State + { graph :: Graph + , currentVertex :: Maybe Vertex + , decisions :: Map Decision DecisionState + , curTrace :: [Bool] + } + +addVertex :: Text -> State -> State +addVertex vert s = s + { graph = case currentVertex s of + Just old + | old == vert -> graph s + | otherwise -> M.insertWith S.union old (S.singleton vert) (graph s) + Nothing -> graph s + , currentVertex = Just vert + } + +data NextStep = Restart + | Continue Bool + +handleDecision :: DecisionNumber -> [Bool] -> State -> (NextStep, State) +handleDecision decision trace s = + let curSystemState = fromJust (currentVertex s) -- FIXME fromJust + decisionState = M.lookup (curSystemState, decision) (decisions s) + in case decisionState of + Nothing -> (Continue True, s { decisions = M.insert (curSystemState, decision) (Half trace) (decisions s) }) + Just (Half _) -> (Continue False, s { decisions = M.insert (curSystemState, decision) Full (decisions s) }) + Just Full -> (Restart, s) + +findOpenDecision :: State -> Maybe [Bool] +findOpenDecision = listToMaybe . mapMaybe isHalf . M.elems . decisions + where + isHalf (Half trace) = Just trace + isHalf _ = Nothing + + +driver :: FilePath -> IO () +driver prog = do + state <- newIORef (State M.empty (Just "xstart") M.empty []) + oneProgRun prog state Nothing + + forever $ do + modifyIORef state $ \s -> s { curTrace = [], currentVertex = Just "xstart" } + findOpenDecision <$> readIORef state >>= \case + Nothing -> do + s <- readIORef state + T.putStrLn (graph2Dot (graph s)) + exitSuccess + Just trace -> do + oneProgRun prog state (Just $ reverse trace) + +oneProgRun :: FilePath -> IORef State -> Maybe [Bool] -> IO () +oneProgRun prog state trace = do + (Just pstdin, Just pstdout, _, handle) <- createProcess (proc prog []) { std_in = CreatePipe, std_out = CreatePipe } + case trace of + Just trace' -> tracePath pstdin pstdout state trace' + _ -> return () + + let loop = handleLine pstdout state >>= \case + Decision x -> do + s <- readIORef state + let (next, s') = handleDecision x (curTrace s) s + writeIORef state s' + case next of + Restart -> terminateProcess handle >> mapM_ hClose [pstdin, pstdout] + Continue x -> do + makeDecision pstdin state x + loop + + EOF -> terminateProcess handle >> mapM_ hClose [pstdin, pstdout] + NewState _ -> loop + + loop + + +tracePath :: Handle -> Handle -> IORef State -> [Bool] -> IO () +tracePath pstdin pstdout state [] = return () +tracePath pstdin pstdout state (decision:ds) = do + handleLine pstdout state >>= \case + EOF -> error "premature eof" -- FIXME + Decision x -> do + makeDecision pstdin state decision + tracePath pstdin pstdout state ds + NewState _ -> tracePath pstdin pstdout state (decision:ds) + +makeDecision :: Handle -> IORef State -> Bool -> IO () +makeDecision pstdin state decision = do + hPutStrLn pstdin $ if decision then "1" else "0" + hFlush pstdin + modifyIORef state (\s -> s { curTrace = decision : curTrace s}) + hPutStrLn stderr $ "deciding " ++ show decision + +data LineOut = NewState Text + | Decision DecisionNumber + | EOF + +parseLine :: Handle -> IO LineOut +parseLine handle = do + eof <- hIsEOF handle + if eof + then return EOF + else do + line <- T.hGetLine handle + T.hPutStrLn stderr $ "Found line: " <> line + case T.words line of + ("Decision":num:_) -> return $ Decision (read $ T.unpack num) + ("Line":rest) -> return $ NewState (last rest) + +handleLine :: Handle -> IORef State -> IO LineOut +handleLine pstdin state = parseLine pstdin >>= \case + NewState vert -> modifyIORef state (addVertex vert) >> return (NewState vert) + other -> return other + +graph2Dot :: Graph -> Text +graph2Dot graph = + "digraph gcfg {\n" + <> M.foldMapWithKey nodeStr graph + <> "}" + + where + nodeStr from tos = mconcat $ map (arrow from) $ S.toList tos + arrow from to = " " <> num2str from <> " -> " <> num2str to <> ";\n" + num2str = T.tail diff --git a/src/main/Main.hs b/src/main/Main.hs index d9e44700285145775a59ce03be9f73d38dbb6116..bc78bc570a657c7e7ca703fe2b33268194e80088 100644 --- a/src/main/Main.hs +++ b/src/main/Main.hs @@ -12,6 +12,7 @@ import CFG.IR import CFG.C import CFG.Sanitize import Search.States2Dot +import Search.Search main :: IO () main = do @@ -20,6 +21,9 @@ main = do cntnt <- T.getContents T.putStrLn $ states2Dot cntnt + ["search", prog] -> do + driver prog + _ -> do cntnt <- BS.getContents case P.parseFile cntnt of