diff --git a/osek-verification.cabal b/osek-verification.cabal index d091c7e94157e30bfe3b7be1cfe7f8939143aa6f..e18a4e7cc541e1915b829b64488bc59a5ecd48d9 100644 --- a/osek-verification.cabal +++ b/osek-verification.cabal @@ -21,6 +21,7 @@ library , CFG.C , CFG.Types , CFG.Sanitize + , CFG.DecisionTree , Search.Search , Search.Types , Search.EpsilonElimination diff --git a/src/CFG/C.hs b/src/CFG/C.hs index f600d5165ca444769ef5964f33ba07e23f4bfc33..2a859c1563c982ba9a52b245df08786b70beb968 100644 --- a/src/CFG/C.hs +++ b/src/CFG/C.hs @@ -1,4 +1,5 @@ {-# LANGUAGE OverloadedStrings #-} + module CFG.C ( instrsToC , compileToC @@ -14,6 +15,7 @@ module CFG.C import Control.Arrow import Control.Comonad import Control.Monad.State +import Control.Monad.Writer hiding ((<>)) import Data.IntSet (IntSet) import qualified Data.IntSet as S import Data.List @@ -21,7 +23,11 @@ import Data.Maybe import Data.Semigroup import Data.Text (Text) import qualified Data.Text as T +import qualified Data.Text.Lazy.Builder as TB +import qualified Data.Text.Lazy.Builder.Int as TB +import qualified Data.Text.Lazy as TL +import CFG.DecisionTree import CFG.IR import CFG.Types import Protocol @@ -42,8 +48,6 @@ compileToCAll interrupts funs = flip evalState 0 $ do <> (T.strip funs') <> "\n" -type DecisionM = State Int - include :: Text include = "#include <mockup_prelude.cc>\n\n" @@ -88,38 +92,45 @@ declareExtern funs = mconcat $ triggerInterrupts :: Maybe IntSet -> Text -> Int -> DecisionM Text triggerInterrupts Nothing _ _ = return "" triggerInterrupts (Just ints) ident abb = do - triggerCode <- mconcat <$> mapM triggerInterrupt (S.toList ints) + dtree <- mkDTree (-1:S.toList ints) - return $ - "while (1) {\n" - <> " int _triggeredSomeInterrupt = 0;\n" - <> triggerCode - <> " if (_triggeredSomeInterrupt == 0) break;\n" - <> "}\n" + return $ TL.toStrict $ TB.toLazyText $ execWriter $ do + tell "while (1) {\n" + mkDecision dtree + tell "}\n" - where triggerInterrupt int = do - decision <- decisionNumber + where + mkDecision :: DTree -> Writer TB.Builder () + mkDecision (Decision i) + | i == -1 = tell "break;\n" + | otherwise = triggerInterrupt i + mkDecision (Question q left right) = do + tell $ "if (" <> TB.fromText (decisionMaker q) <> ") {\n" + mkDecision left + tell "} else {" + mkDecision right + tell "}" + + triggerInterrupt :: Int -> Writer TB.Builder () + triggerInterrupt int = do + -- decision <- decisionNumber let interrupt_name = "trigger_interrupt_" <> T.pack (show int) - return $ - " if (" <> decisionMaker decision <> ") {\n" - <> " _syscall_prolog(" <> T.pack (show abb) <> ");\n" - <> " if (" <> doTriggerInterrupt interrupt_name (ident <> "_" <> interrupt_name) int <> ") {\n" - <> " _syscall_prolog(0);\n" - <> " " <> printOSState AtBasicBlockType ident "__func__" <> ";\n" - <> " _triggeredSomeInterrupt = 1;\n" - <> " }\n" - <> " _syscall_prolog(0);\n" - <> " }\n" - - doTriggerInterrupt ident payload int = T.pack $ + tell $ " _syscall_prolog(" <> TB.fromString (show abb) <> ");\n" + tell $ " if (" <> doTriggerInterrupt interrupt_name (ident <> "_" <> interrupt_name) int <> ") {\n" + tell $ " _syscall_prolog(0);\n" + tell $ " " <> TB.fromText (printOSState AtBasicBlockType ident "__func__") <> ";\n" + tell $ " }\n" + tell $ " _syscall_prolog(0);\n" + + doTriggerInterrupt ident payload int = "_do_trigger_interrupt(" - <> show int + <> TB.decimal int <> ", " - <> show (generateCFormatString BeforeSyscallType) + <> TB.fromString (show (generateCFormatString BeforeSyscallType)) <> ", " - <> show ident + <> TB.fromString (show ident) <> ", " - <> show payload + <> TB.fromString (show payload) <> ")" instrsToC :: Maybe IntSet -> [Instr] -> DecisionM Text @@ -155,12 +166,6 @@ instrToC _ (PrintInformation (CurrentNodeIs ident)) = indent :: Text -> Text indent = T.unlines . map (" " <>) . T.lines -decisionNumber :: DecisionM Int -decisionNumber = do - n <- get - put (n+1) - return n - -- | Generate a call to the decisionMaker function -- diff --git a/src/CFG/DecisionTree.hs b/src/CFG/DecisionTree.hs new file mode 100644 index 0000000000000000000000000000000000000000..c4e2e29478edc2f2b1c3b3b3fa24230d2cf1ea28 --- /dev/null +++ b/src/CFG/DecisionTree.hs @@ -0,0 +1,26 @@ +module CFG.DecisionTree where + +import Control.Monad.State + +type DecisionM = State Int + +decisionNumber :: DecisionM Int +decisionNumber = do + n <- get + put (n+1) + return n + + +data DTree = Question Int DTree DTree | Decision Int + deriving (Show, Eq) + +mkDTree :: [Int] -> DecisionM DTree +mkDTree [] = error "trying to create empty decision tree" +mkDTree [a] = return $ Decision a +mkDTree ls = + let + half = length ls `div` 2 + in + Question <$> decisionNumber + <*> mkDTree (take half ls) + <*> mkDTree (drop half ls)