diff --git a/files/mockup_prelude.cc b/files/mockup_prelude.cc index b8fe886a3a876c0efad95a36604c26f3a1d64647..ed85350f287a86cddb3e890d8b881772e5310275 100644 --- a/files/mockup_prelude.cc +++ b/files/mockup_prelude.cc @@ -99,8 +99,8 @@ uint32_t hash_os_state() { return first_hash ^ second_hash; } -void _print_os_state(const char *syscall, int line) { - kout << "Line " << line << " before syscall " << syscall << " in state "; +void _print_os_state(const char *syscall, const char *func) { + kout << "Function " << func << " before syscall " << syscall << " in state "; kout << "0x" << hex << hash_os_state() << dec << endl; fflush(stdout); } diff --git a/src/CFG/C.hs b/src/CFG/C.hs index bc87ec4d24c125dc76931afa0dff4bf716dbe1bd..f0af83b01f7a720e9a0633f5470d62069ad39f19 100644 --- a/src/CFG/C.hs +++ b/src/CFG/C.hs @@ -86,7 +86,7 @@ preIdleHook interrupts = do return $ "void PreIdleHook() {\n" - <> " _print_os_state(\"PreIdleHook\", __LINE__);\n" + <> " _print_os_state(\"PreIdleHook\", __func__);\n" <> triggerCode <> " ShutdownMachine();\n" <> "}\n" @@ -107,7 +107,7 @@ triggerInterrupts (Just ints) = do decision <- decisionNumber return $ " if (_decisionMaker("<> T.pack (show decision) <> ")) {\n" - <> " _print_os_state(\"IRQ" <> T.pack (show int) <> "\", __LINE__);\n" + <> " _print_os_state(\"IRQ" <> T.pack (show int) <> "\", __func__);\n" <> " Machine::trigger_interrupt_from_user(" <> T.pack (show int) <> ");\n" <> " }\n" @@ -132,7 +132,7 @@ instrToC interrupts kind (Call ident True) = do else return mempty return $ ints - <> "_print_os_state(\"" <> ident <> "\", __LINE__);\n" + <> "_print_os_state(\"" <> ident <> "\", __func__);\n" <> ident <> "();" instrToC _ _ Return = return "return;" diff --git a/src/Search/Search.hs b/src/Search/Search.hs index 49ea4212c5c67f126bc81d55390ecf78af3b9125..4b1b64d99849f2cf89ea4b9306232ba300c67eb9 100644 --- a/src/Search/Search.hs +++ b/src/Search/Search.hs @@ -19,8 +19,22 @@ import System.Process import System.IO import Data.Foldable --- | (Syscall, Statehash) -type Vertex = (Text, Text) +data Metadata = Metadata + { metaFunc :: Text -- | Function Name + , metaSyscall :: Text -- | Next Syscall + } + +-- | (Statehash, Metadata) +data Vertex = Vertex + { vertState :: Text + , vertMeta :: Metadata + } + +instance Eq Vertex where + Vertex x meta1 == Vertex y meta2 = (x, metaSyscall meta1) == (x, metaSyscall meta2) + +instance Ord Vertex where + compare (Vertex x meta1) (Vertex y meta2) = compare (x, metaSyscall meta1) (y, metaSyscall meta2) type Graph = Map Vertex (Set Vertex) @@ -36,7 +50,7 @@ data State = State , curTrace :: [Bool] } -addVertex :: (Text, Text ) -> State -> State +addVertex :: Vertex -> State -> State addVertex vert s = s { graph = case currentVertex s of Just old @@ -69,7 +83,7 @@ findOpenDecision = listToMaybe . mapMaybe isHalf . M.elems . decisions driver :: FilePath -> Bool -- ^ Identify states on different locations? -> IO () -driver prog identStates = driver' prog identStates ("", "start") +driver prog identStates = driver' prog identStates (Vertex "start" (Metadata "" "")) --driver prog True = driver' prog (Vertex ("", "start") :: Vertex 'OnlyState) driver' :: FilePath -> Bool -> Vertex -> IO () @@ -142,8 +156,8 @@ parseLine handle = do T.hPutStrLn stderr $ "Found line: " <> line case T.words line of ("Decision":num:_) -> return $ Decision (read $ T.unpack num) - ["Line",linum,"before","syscall",call,"in","state",state] - -> return $ NewState (call, state) + ["Function",func,"before","syscall",call,"in","state",state] + -> return $ NewState $ Vertex state (Metadata func call) handleLine :: Handle -> IORef State -> IO LineOut handleLine pstdin state = parseLine pstdin >>= \case @@ -160,7 +174,7 @@ 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 from) <> "\"];\n" + <> nodeId is to <> " [label=\"" <> edgeLabel (metaSyscall $ vertMeta from) <> "\"];\n" -- | Generate readable edge label from syscall name -- @@ -176,12 +190,17 @@ dotNodes :: Bool -> Graph -> Text dotNodes is = foldMap formatNode . allNotes where allNotes m = M.keysSet m `S.union` fold m - formatNode (call, state) = nodeId is (call,state) - <> " [label=\"" - <> "State: " <> state - <> "\", shape=box];\n" + formatNode vert = nodeId is vert + <> " [label=\"" + <> "State: " <> vertState vert + <> "\\nFunction: " <> stripPrefix' "OSEKOS_" (metaFunc (vertMeta vert)) + <> "\", shape=box];\n" nodeId :: Bool -> Vertex -> Text -nodeId False (call, state) = "node" <> state <> "_" <> call -nodeId True (_, state) = "node" <> state +nodeId False vert = "node" <> vertState vert <> "_" <> metaSyscall (vertMeta vert) +nodeId True vert = "node" <> vertState vert +-- | Strip prefix but return original string if it doesn't begin with the prefix +stripPrefix' :: Text -> Text -> Text +stripPrefix' pref (T.stripPrefix pref -> Just txt) = txt +stripPrefix' _ txt = txt