diff --git a/files/mockup_prelude.cc b/files/mockup_prelude.cc index ed85350f287a86cddb3e890d8b881772e5310275..4f4b7c9c99b793ab9e0e85f8c3a0452e600c680e 100644 --- a/files/mockup_prelude.cc +++ b/files/mockup_prelude.cc @@ -99,9 +99,9 @@ uint32_t hash_os_state() { return first_hash ^ second_hash; } -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; +void _print_os_state(const char *format, const char *syscall, const char *func) { + printf(format, hash_os_state(), syscall, func); + printf("\n"); fflush(stdout); } @@ -109,8 +109,9 @@ void os_main(void) { StartOS(0); } -int _decisionMaker(int i) { - printf("Decision %d\n", i); +int _decisionMaker(const char *format, int i) { + printf(format, i); + printf("\n"); fflush(stdout); int res = (getchar() == '0') ? 0 : 1; diff --git a/osek-verification.cabal b/osek-verification.cabal index a8c8e0ef92aa775165dd0399a066014af4bc966e..e79a8f248b33d26449333961f86392b66270fbb2 100644 --- a/osek-verification.cabal +++ b/osek-verification.cabal @@ -23,6 +23,7 @@ library , CFG.Sanitize , Search.States2Dot , Search.Search + , Protocol hs-source-dirs: src build-depends: base >=4.9 && <4.10 , megaparsec >= 5 && <5.1 diff --git a/src/CFG/C.hs b/src/CFG/C.hs index 6bde31c8f4ae2717cdf7397f9e4f7b67e72775e9..61c45502e1a21852a9af66495f9b94003bf9d513 100644 --- a/src/CFG/C.hs +++ b/src/CFG/C.hs @@ -22,6 +22,7 @@ import qualified Data.Text as T import CFG.IR import CFG.Types +import Protocol -- | Compile multiple functions to C, inckluding declarations compileToCAll :: Maybe IntSet -- ^ All possible interrupt numbers @@ -97,8 +98,8 @@ triggerInterrupts (Just ints) = do where triggerInterrupt int = do decision <- decisionNumber return $ - " if (_decisionMaker("<> T.pack (show decision) <> ")) {\n" - <> " _print_os_state(\"IRQ" <> T.pack (show int) <> "\", __func__);\n" + " if (" <> decisionMaker decision <> ") {\n" + <> " " <> printState ("IRQ" <> T.pack (show int)) <> ";\n" <> " Machine::trigger_interrupt_from_user(" <> T.pack (show int) <> ");\n" <> " _triggeredSomeInterrupt = 1;\n" <> " }\n" @@ -120,7 +121,7 @@ instrToC _ (Label ident) = return $ ident <> ":" instrToC _ (IfThanElse left right) = do decision <- decisionNumber return $ - "if (_decisionMaker(" <> T.pack (show decision) <> "))\n" <> + "if (" <> decisionMaker decision <> "))\n" <> " goto " <> left <> ";\n" <> "else\n" <> " goto " <> right <> ";" @@ -128,7 +129,7 @@ instrToC _ (Call ident) = return $ ident <> "();" instrToC _ Return = return "return;" instrToC interrupts TriggerAllInterrupts = triggerInterrupts interrupts instrToC _ (PrintInformation (NextSyscallIs ident)) = - return $ "_print_os_state(\"" <> ident <> "\", __func__);" + return $ printState ident <> ";" indent :: Text -> Text indent = T.unlines . map (" " <>) . T.lines @@ -138,3 +139,23 @@ decisionNumber = do n <- get put (n+1) return n + + +-- Generates something like: _decisionMaker("%d", 5) +decisionMaker :: Int -> Text +decisionMaker decision = T.pack $ + "_decisionMaker(" + <> show (generateCFormatString DecisionRequestType) + <> ", " + <> show decision + <> ")" + +printState :: Text -> Text +printState ident = T.pack $ + "_print_os_state(" + <> show (generateCFormatString BeforeSyscallType) + <> ", " + <> show ident + <> ", " + <> "__func__" + <> ")" diff --git a/src/CFG/IR.hs b/src/CFG/IR.hs index ae8f5033b5731d881959b6847aee317f1e6a981e..c7a2c7a5758b451f726f2af28c26ec71380ca88b 100644 --- a/src/CFG/IR.hs +++ b/src/CFG/IR.hs @@ -95,8 +95,9 @@ preIdleHook = Function , funEntryNode = "" -- ignored by C code , funBlocks = [] -- ignored by C code , funAnnotation = - [ TriggerAllInterrupts - , PrintInformation (NextSyscallIs "ShutdownMachine") + [ PrintInformation (NextSyscallIs "PreIdleHook") + , TriggerAllInterrupts + -- , PrintInformation (NextSyscallIs "ShutdownMachine") , Call "ShutdownMachine" ] } diff --git a/src/Protocol.hs b/src/Protocol.hs new file mode 100644 index 0000000000000000000000000000000000000000..6588f1eec076f8d29efb0d874d47eb6577a14014 --- /dev/null +++ b/src/Protocol.hs @@ -0,0 +1,100 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE OverloadedStrings, DeriveGeneric #-} + +-- | This is the protocol with which the mockup and search program can +-- communicate. +-- +-- The generated C program sends values of type "StateOutput" and the search +-- procedure responds with values of type "DecisionInput". +-- +-- The on-the-wire format is JSON, used through the provided instances (and +-- 'generateCFormatString'). +module Protocol + ( -- * Data Types + DecisionInput(..) + , StateHash + , StateOutput(..) + , StateOutputType(..) + -- * JSON generation from C + , generateCFormatString + , formatDecision + ) where + +import Data.Aeson +import Data.Aeson.Types +import Data.Text (Text) + +import GHC.Generics + +-- | Values provided by the search procedure to select the left or right branch +-- of a condition. +newtype DecisionInput = DecisionInput Bool + deriving (Eq, Show, Generic) + +-- | Type synonym for state hashes (e.g "0xbadfood"). +type StateHash = Text + +-- | Values send by the mockup program to the search algorithm. +data StateOutput = + -- | Request a decision from the search algorithm + DecisionRequest Int + -- | Tell the search that we are about to make a syscall + -- + -- The first 'Text' argument represents the name of this syscall, the other is + -- arbitrary metadata (e.g the current function's name) + | BeforeSyscall StateHash Text Text + +-- | Constructors of StateOutput. Used for generateCFormatString. +data StateOutputType = DecisionRequestType | BeforeSyscallType + deriving (Show, Eq) + + +----------------- +-- Json instances +----------------- + +instance ToJSON StateOutput where + toJSON (DecisionRequest num) = + object [ "type" .= ("decision" :: Text), "number" .= num ] + + toJSON (BeforeSyscall state syscall payload) = + object [ "type" .= ("syscall" :: Text) + , "state" .= state + , "syscall" .= syscall + , "payload" .= payload + ] + +instance FromJSON StateOutput where + parseJSON (Object v) = do + (typ :: String) <- v .: "type" + case typ of + "decision" -> + DecisionRequest <$> v .: "number" + "syscall" -> + BeforeSyscall <$> v .: "state" <*> v .: "syscall" <*> v .: "payload" + _ -> fail $ "type of StateOutput must be \"decision\" or \"syscall\"" + + parseJSON invalid = typeMismatch "StateOutput" invalid + +----------------------------- +-- C format string generation +----------------------------- + +-- | Generate a suitable C format string to print a value of the given type in JSON. +-- +-- The order of format directives are: +-- +-- * DecisionRequest: number +-- * BeforeSyscall: state, syscall, payload +generateCFormatString :: StateOutputType -> Text +generateCFormatString soType = case soType of + DecisionRequestType -> + "{ \"type\": \"decision\", \"number\": %d }" + BeforeSyscallType -> + "{ \"type\": \"syscall\", \"state\": \"0x%x\", \"syscall\": \"%s\", \"payload\": \"%s\" }" + +-- | Generate a byte of text for our decition number in for format that the C +-- code expects. +formatDecision :: DecisionInput -> Text +formatDecision (DecisionInput True) = "1" +formatDecision (DecisionInput False) = "0" diff --git a/src/Search/Search.hs b/src/Search/Search.hs index 9e1e14ead3ac7b45e01b24ec4e16e855a78b11a9..6c02467306a48a4389ee6138a3de7743fb7c53e9 100644 --- a/src/Search/Search.hs +++ b/src/Search/Search.hs @@ -3,21 +3,27 @@ module Search.Search (driver) where -import Data.Map (Map) +import Control.Monad +import qualified Data.ByteString.Lazy as BS +import Data.Foldable +import Data.IORef +import Data.Map (Map) import qualified Data.Map as M -import Data.Set (Set) +import Data.Maybe +import Data.Monoid +import Data.Set (Set) import qualified Data.Set as S -import Data.Text (Text) +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 -import Data.Foldable +import qualified Data.Text.Encoding as T +import System.Exit +import System.IO +import System.Process + +import Data.Aeson + +import Protocol data Metadata = Metadata { metaFunc :: Text -- ^ Function Name @@ -134,7 +140,7 @@ 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" + T.hPutStrLn pstdin $ formatDecision $ DecisionInput decision hFlush pstdin modifyIORef state (\s -> s { curTrace = decision : curTrace s}) hPutStrLn stderr $ "deciding " ++ show decision @@ -151,10 +157,12 @@ parseLine handle = do 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) - ["Function",func,"before","syscall",call,"in","state",state] - -> return $ NewState $ Vertex state (Metadata func call) + case decodeStrict (T.encodeUtf8 line) of + Nothing -> error $ "Parser error in line " <> T.unpack line + Just (DecisionRequest num) -> + return $ Decision num + Just (BeforeSyscall state call func) -> + return $ NewState $ Vertex state (Metadata func call) handleLine :: Handle -> IORef State -> IO LineOut handleLine pstdin state = parseLine pstdin >>= \case