From 15c76ebe58bfedbd727ef731963868b7948a0a96 Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hpd@hpdeifel.de>
Date: Thu, 15 Dec 2016 19:26:41 +0100
Subject: [PATCH] Implement a new protocol for mockup/search communication
Based on JSON and defined in a single place. This should make it much
easier to change the format.
---
files/mockup_prelude.cc | 11 +++--
osek-verification.cabal | 1 +
src/CFG/C.hs | 29 ++++++++++--
src/CFG/IR.hs | 5 +-
src/Protocol.hs | 100 ++++++++++++++++++++++++++++++++++++++++
src/Search/Search.hs | 40 +++++++++-------
6 files changed, 159 insertions(+), 27 deletions(-)
create mode 100644 src/Protocol.hs
diff --git a/files/mockup_prelude.cc b/files/mockup_prelude.cc
index ed85350..4f4b7c9 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 a8c8e0e..e79a8f2 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 6bde31c..61c4550 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 ae8f503..c7a2c7a 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 0000000..6588f1e
--- /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 9e1e14e..6c02467 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
--
GitLab