Rough implementation of path search

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

src/Search/Search.hs

+{-# 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

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