search: Remove hack to identify states with different syscalls

Right now, the next syscall is part of the identity of a state. There
was a hack in place that allowed to temporarily ignore this piece of
information for the comparison.

While the feature may have been useful, it was implemented as a rather
crude hack and should be redone properly.

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

src/main/Main.hs

@@ -5,6 +5,8 @@ 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 qualified CFG.Parser as P
@@ -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