diff --git a/src/Search/Search.hs b/src/Search/Search.hs index 2f415d46d7d51f13ea941477454ce32ff38b15c0..35713be3991878fc874687982cffa1950d14bddc 100644 --- a/src/Search/Search.hs +++ b/src/Search/Search.hs @@ -1,7 +1,4 @@ {-# LANGUAGE LambdaCase, OverloadedStrings #-} -{-# LANGUAGE KindSignatures, DataKinds #-} -{-# LANGUAGE FlexibleInstances, FlexibleContexts #-} -{-# LANGUAGE ScopedTypeVariables #-} module Search.Search (driver) where @@ -20,53 +17,38 @@ import System.Exit import System.Process import System.IO import Data.Foldable -import Data.Function - -data Compare = OnlyState | StateAndSyscall -- | (Syscall, Statehash) -newtype Vertex (a :: Compare) = Vertex { unVertex :: (Text, Text) } - -instance Eq (Vertex 'OnlyState) where - (==) = (==) `on` (snd . unVertex) - -instance Eq (Vertex 'StateAndSyscall) where - (==) = (==) `on` unVertex +type Vertex = (Text, Text) -instance Ord (Vertex 'OnlyState) where - compare = compare `on` (snd . unVertex) - -instance Ord (Vertex 'StateAndSyscall) where - compare = compare `on` unVertex - -type Graph a = Map (Vertex a) (Set (Vertex a)) +type Graph = Map Vertex (Set Vertex) type DecisionNumber = Int -type Decision a = (Vertex a, DecisionNumber) +type Decision = (Vertex, DecisionNumber) data DecisionState = Half [Bool] -- Trace | Full -data State a = State - { graph :: Graph a - , currentVertex :: Maybe (Vertex a) - , decisions :: Map (Decision a) DecisionState +data State = State + { graph :: Graph + , currentVertex :: Maybe Vertex + , decisions :: Map Decision DecisionState , curTrace :: [Bool] } -addVertex :: Ord (Vertex a) => Vertex a -> State a -> State a -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 - } +addVertex :: (Text, 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 :: Ord (Vertex a) => DecisionNumber -> [Bool] -> State a -> (NextStep, State a) +handleDecision :: DecisionNumber -> [Bool] -> State -> (NextStep, State) handleDecision decision trace s = let curSystemState = fromJust (currentVertex s) -- FIXME fromJust decisionState = M.lookup (curSystemState, decision) (decisions s) @@ -75,7 +57,7 @@ handleDecision decision trace s = Just (Half _) -> (Continue False, s { decisions = M.insert (curSystemState, decision) Full (decisions s) }) Just Full -> (Restart, s) -findOpenDecision :: State a -> Maybe [Bool] +findOpenDecision :: State -> Maybe [Bool] findOpenDecision = listToMaybe . mapMaybe isHalf . M.elems . decisions where isHalf (Half trace) = Just trace @@ -86,10 +68,10 @@ findOpenDecision = listToMaybe . mapMaybe isHalf . M.elems . decisions driver :: FilePath -> Bool -- ^ Identify states on different locations? -> IO () -driver prog identStates = driver' prog identStates (Vertex ("", "start") :: Vertex 'StateAndSyscall) +driver prog identStates = driver' prog identStates ("", "start") --driver prog True = driver' prog (Vertex ("", "start") :: Vertex 'OnlyState) -driver' :: Ord (Vertex a) => FilePath -> Bool -> Vertex a -> IO () +driver' :: FilePath -> Bool -> Vertex -> IO () driver' prog identStates startVertex = do state <- newIORef (State M.empty (Just startVertex) M.empty []) oneProgRun prog state Nothing @@ -104,7 +86,7 @@ driver' prog identStates startVertex = do Just trace -> oneProgRun prog state (Just $ reverse trace) -oneProgRun :: Ord (Vertex a) => FilePath -> IORef (State a) -> Maybe [Bool] -> IO () +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 @@ -118,8 +100,8 @@ oneProgRun prog state trace = do writeIORef state s' case next of Restart -> terminateProcess handle >> mapM_ hClose [pstdin, pstdout] - Continue x' -> do - makeDecision pstdin state x' + Continue x -> do + makeDecision pstdin state x loop EOF -> terminateProcess handle >> mapM_ hClose [pstdin, pstdout] @@ -128,28 +110,28 @@ oneProgRun prog state trace = do loop -tracePath :: Ord (Vertex a) => Handle -> Handle -> IORef (State a) -> [Bool] -> IO () -tracePath _ _ _ [] = return () -tracePath pstdin pstdout state (decision:ds) = +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 _ -> do + Decision x -> do makeDecision pstdin state decision tracePath pstdin pstdout state ds NewState _ -> tracePath pstdin pstdout state (decision:ds) -makeDecision :: Handle -> IORef (State a) -> Bool -> IO () +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 a = NewState (Vertex a) - | Decision DecisionNumber - | EOF +data LineOut = NewState Vertex + | Decision DecisionNumber + | EOF -parseLine :: Handle -> IO (LineOut a) +parseLine :: Handle -> IO LineOut parseLine handle = do eof <- hIsEOF handle if eof @@ -160,14 +142,14 @@ parseLine handle = do case T.words line of ("Decision":num:_) -> return $ Decision (read $ T.unpack num) ["Line",linum,"before","syscall",call,"in","state",state] - -> return $ NewState $ Vertex (call, state) + -> return $ NewState (call, state) -handleLine :: Ord (Vertex a) => Handle -> IORef (State a) -> IO (LineOut a) +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 :: Ord (Vertex a) => Bool -> Graph a -> Text +graph2Dot :: Bool -> Graph -> Text graph2Dot is graph = "digraph gcfg {\n" <> dotNodes is graph @@ -177,21 +159,21 @@ graph2Dot is graph = where nodeStr from tos = mconcat $ map (arrow from) $ S.toList tos arrow from to = " " <> nodeId is from <> " -> " - <> nodeId is to <> " [label=\"" <> edgeLabel (fst $ unVertex from) <> "\"];\n" + <> nodeId is to <> " [label=\"" <> edgeLabel (fst from) <> "\"];\n" edgeLabel txt = T.dropEnd 1 $ T.dropWhileEnd (/='_') $ T.drop (T.length "OSEKOS_") txt -dotNodes :: Ord (Vertex a) => Bool -> Graph a -> Text +dotNodes :: Bool -> Graph -> Text dotNodes is = foldMap formatNode . allNotes where allNotes m = M.keysSet m `S.union` fold m - formatNode (Vertex (call, state)) = nodeId is (Vertex (call,state)) + formatNode (call, state) = nodeId is (call,state) <> " [label=\"" <> "State: " <> state <> (if not is then "\\nSyscall: " <> call else mempty) <> "\", shape=box];\n" -nodeId :: Bool -> Vertex a -> Text -nodeId False (Vertex (call, state)) = "node" <> state <> "_" <> call -nodeId True (Vertex (_, state)) = "node" <> state +nodeId :: Bool -> Vertex -> Text +nodeId False (call, state) = "node" <> state <> "_" <> call +nodeId True (_, state) = "node" <> state