diff --git a/osek-verification.cabal b/osek-verification.cabal index 75e14afe89e85e50686cbcc17387906dfefafb23..41c47077eea7a21630647f0de871ad79dfdfff0c 100644 --- a/osek-verification.cabal +++ b/osek-verification.cabal @@ -33,6 +33,7 @@ library , Compare.Compare , Compare.Matching , Compare.Preprocess + , Compare.SSEGraph hs-source-dirs: src build-depends: base >=4.9 && <4.10 , megaparsec >= 5 && <5.3 @@ -47,6 +48,8 @@ library , fgl >= 5.5 && < 5.6 , microlens >= 0.4 && < 0.5 , microlens-th >= 0.4 && < 0.5 + , unordered-containers >= 0.2 && <0.3 + , hashable >= 1.2 && < 1.3 default-language: Haskell2010 ghc-options: -Wall -fno-warn-name-shadowing @@ -94,5 +97,6 @@ test-suite spec , fgl >= 5.5 && < 5.6 , microlens >= 0.4 && < 0.5 , microlens-aeson >= 2.2 && <2.3 + , unordered-containers >= 0.2 && <0.3 default-language: Haskell2010 ghc-options: -Wall -fno-warn-name-shadowing diff --git a/src/Compare/JSON.hs b/src/Compare/JSON.hs index 0ff4d7c91dc0a1986b84b553cbf76fd9692c9afa..05ce68fc36b1132b7bbf373f0c60d98727388792 100644 --- a/src/Compare/JSON.hs +++ b/src/Compare/JSON.hs @@ -1,58 +1,69 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE TupleSections #-} {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -Wno-orphans #-} module Compare.JSON ( parseFile - , NodeLabel - , EdgeLabel + , FromJSONNode(..) + , ToJSONNode(..) ) where import Data.Aeson -import Data.Aeson.Types (typeMismatch) +import Data.Aeson.Types (typeMismatch, Parser) import qualified Data.ByteString.Lazy as BS import qualified Data.Graph.Inductive as G import Data.Text (Text) -import qualified Data.Text as T import Lens.Micro import Compare.Types +import Compare.Types.Lenses -parseFile :: BS.ByteString -> Either String (Graph NodeLabel EdgeLabel) -parseFile input = eitherDecode' input & _Right . _graph %~ G.emap stripArgument +parseFile :: FromJSON (Graph n e) => BS.ByteString -> Either String (Graph n e) +parseFile input = eitherDecode' input -type NodeLabel = Text -type EdgeLabel = Text +class FromJSONNode a where + parseJSONNode :: Value -> Parser a + +class ToJSONNode a where + toJSONNode :: a -> Value -newtype N n = N { unN :: n } newtype E n e = E { unE :: (n, n, e) } -instance (FromJSON n, Ord n, FromJSON e) => FromJSON (Graph n e) where +instance (FromJSONNode n, HasNodeId n, FromJSON (NodeId n), FromJSON e) => FromJSON (Graph n e) where parseJSON (Object v) = mkGraph - <$> (map unN <$> v .: "nodes") - <*> (map unE <$> v .: "edges") + <$> ((v .: "nodes") >>= mapM parseJSONNode) + <*> (map unE <$> (v .: "edges")) <*> v .: "entry" parseJSON invalid = typeMismatch "Graph" invalid -instance (ToJSON n, ToJSON e) => ToJSON (Graph n e) where +instance (ToJSONNode n, HasNodeId n, ToJSON (NodeId n), ToJSON e) => ToJSON (Graph n e) where toJSON g = object - [ "nodes" .= ((g^._graph) & G.labNodes & map snd & map N) - , "edges" .= ((g^._graph) & G.labEdges & map (toE g)) - , "entry" .= (G.lab (g^._graph) (g^._point) ^?! _Just) + [ "nodes" .= (g ^. _graph & G.labNodes & map snd & map toJSONNode) + , "edges" .= (g ^. _graph & G.labEdges & map (toE g)) + , "entry" .= (g ^?! node (g ^. _point) . to nodeId) ] -toE :: Graph n e -> G.LEdge e -> E n e -toE g (from, to, lab) = E ( G.lab (g^._graph) from ^?! _Just - , G.lab (g^._graph) to ^?! _Just - , lab) +instance FromJSONNode Text where + parseJSONNode (Object v) = v .: "id" + parseJSONNode invalid = typeMismatch "NodeLabel" invalid + +instance FromJSONNode Int where + parseJSONNode (Object v) = v .: "id" + parseJSONNode invalid = typeMismatch "NodeLabel" invalid -instance FromJSON n => FromJSON (N n) where - parseJSON (Object v) = N <$> v .: "id" - parseJSON invalid = typeMismatch "Node" invalid +instance ToJSONNode Text where + toJSONNode x = object [ "id" .= toJSON x] -instance ToJSON n => ToJSON (N n) where - toJSON (N n) = object ["id" .= n] +instance ToJSONNode Int where + toJSONNode x = object [ "id" .= toJSON x] + +toE :: HasNodeId n => Graph n e -> G.LEdge e -> E (NodeId n) e +toE g (from, to', lab) = E ( G.lab (g^._graph) from ^?! _Just . to nodeId + , G.lab (g^._graph) to' ^?! _Just . to nodeId + , lab) instance (FromJSON n, FromJSON e) => FromJSON (E n e) where parseJSON (Object v) = @@ -65,7 +76,3 @@ instance (ToJSON n, ToJSON e) => ToJSON (E n e) where , "to" .= to , "label" .= label ] - --- | Strip the part inside parenthesis from edge labels -stripArgument :: Text -> Text -stripArgument = fst . T.breakOn "(" diff --git a/src/Compare/Preprocess.hs b/src/Compare/Preprocess.hs index 5b26363e304ef3ec7b4921a27939971d390c4308..5c3c8b35f863e481fd0ae146c06fc86cbbb02495 100644 --- a/src/Compare/Preprocess.hs +++ b/src/Compare/Preprocess.hs @@ -14,7 +14,7 @@ import Compare.Types import Compare.Types.Lenses preprocess :: Graph Text Text -> Graph Text Text -preprocess g = g & _graph %~ (G.emap (renameIdle . renameStartOS)) +preprocess g = g & _graph %~ (G.emap (renameIdle . renameStartOS . stripArgument)) & renameIdleKickoff -- | Rename the startOSEdge from "ABBx/StartOS" to "StartOS" @@ -44,3 +44,7 @@ renameIdleKickoff g = case find ((=="Idle") . G.edgeLabel) (g ^. _graph . to G.l idleThreadNode = idleLoop ^. edgeFrom in g & inn idleThreadNode . edgeLabel . filtered (/= "Idle") .~ "IdleKickoff" + +-- | Strip the part inside parenthesis from edge labels +stripArgument :: Text -> Text +stripArgument = fst . T.breakOn "(" diff --git a/src/Compare/SSEGraph.hs b/src/Compare/SSEGraph.hs new file mode 100644 index 0000000000000000000000000000000000000000..e8cdec5c043a0a68d4e1d997c8a53586f82dfdf8 --- /dev/null +++ b/src/Compare/SSEGraph.hs @@ -0,0 +1,61 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE OverloadedStrings #-} + +-- | JSON parsing/printing for the whole SSE-Graph from dOSEK with all +-- additional metadata. +-- +-- This is similar to "Compare.JSON" but retains all metadata +module Compare.SSEGraph + ( NodeLabelMeta(..) + , nodeMetaId + , nodeMetaData + , SSEEdgeLabel(..) + , unSSEEdgeLabel + ) where + +import Data.Aeson +import Data.Aeson.Types (typeMismatch) +import Data.Text (Text) +import qualified Data.Text as T +import Lens.Micro.TH +import qualified Data.HashMap.Lazy as HM + +import Compare.JSON +import Compare.Types +import Search.Types + +-- | A node that retains all metadata additionally to the node id from the json +-- file. +data NodeLabelMeta = NodeLabelMeta + { _nodeMetaId :: Text + , _nodeMetaData :: (HM.HashMap Text Value) + } + +makeLenses ''NodeLabelMeta + +instance HasNodeId NodeLabelMeta where + type NodeId NodeLabelMeta = Text + nodeId = _nodeMetaId + +instance FromJSONNode NodeLabelMeta where + parseJSONNode (Object v) = NodeLabelMeta <$> (v .: "id") <*> (pure v) + parseJSONNode invalid = typeMismatch "NodeLabelMeta" invalid + +instance ToJSONNode NodeLabelMeta where + toJSONNode (NodeLabelMeta i h) = Object (HM.insert "id" (String i) h) + +newtype SSEEdgeLabel = SSEEdgeLabel { _unSSEEdgeLabel :: Text } + deriving (Show, Eq, Ord) + +makeLenses ''SSEEdgeLabel + +instance FromJSON SSEEdgeLabel where + parseJSON v = SSEEdgeLabel <$> parseJSON v + +instance ToJSON SSEEdgeLabel where + toJSON (SSEEdgeLabel t) = toJSON t + +instance IsEpsilon SSEEdgeLabel where + -- epsilon edges in SSE graph differentiate themselves by not having a slash + isEpsilon (SSEEdgeLabel t) = not $ "/" `T.isInfixOf` t diff --git a/src/Compare/Types.hs b/src/Compare/Types.hs index 0c6c75d74024a7d3e3cd98ef87febbf10d7f9144..706c2d26cb5599ca4220baf4b2eb9011e81d4572 100644 --- a/src/Compare/Types.hs +++ b/src/Compare/Types.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TemplateHaskell #-} module Compare.Types @@ -6,15 +8,19 @@ module Compare.Types , _point , singletonGraph , insEdges' + , HasNodeId(..) , mkGraph ) where import Data.Foldable -import Data.Tuple +import Data.Bifunctor import qualified Data.Graph.Inductive as G -import qualified Data.Map as M +import qualified Data.HashMap.Lazy as HM +import Data.Hashable import qualified Data.Set as S +import Data.Text (Text) +import Lens.Micro import Lens.Micro.TH -- | Pointed graph @@ -25,6 +31,9 @@ data Graph node edge = Graph makeLensesFor [("graph", "_graph"), ("point", "_point")] ''Graph +instance Bifunctor Graph where + bimap fn fe g = g & _graph %~ bimap fn fe + -- | Create 'Graph' with just a single node, which is also the 'point'. singletonGraph :: G.Node -> node -> Graph node edge singletonGraph n label = Graph (G.insNode (n, label) G.empty) n @@ -44,18 +53,30 @@ insEdges' edges g = foldl' (flip insEdge) g edges (Nothing, _) -> g (Just (pr, _, la, su), g') -> (pr, v, la, S.toList $ S.insert (l,w) (S.fromList su)) G.& g' +class (Eq (NodeId a), Hashable (NodeId a)) => HasNodeId a where + type NodeId a + nodeId :: a -> NodeId a + +instance HasNodeId Text where + type NodeId Text = Text + nodeId = id + +instance HasNodeId Int where + type NodeId Int = Int + nodeId = id + -- TODO Make more robust against input errors -- E.g unknown notes in edges -- | Create a graph from node and edge labels -mkGraph :: Ord n +mkGraph :: HasNodeId n => [n] -- ^ nodes - -> [(n, n, e)] -- ^ edges - -> n -- ^ point + -> [(NodeId n, NodeId n, e)] -- ^ edges + -> NodeId n -- ^ point -> Graph n e mkGraph nodes labels entry = let labNodes = zip [0..] nodes - nodeMap = M.fromList $ map swap labNodes - labEdges = map (\(from, to, label) -> (nodeMap M.! from, nodeMap M.! to, label)) labels + nodeMap = HM.fromList $ map (\(i,l) -> (nodeId l, i)) labNodes + labEdges = map (\(from, to, label) -> (nodeMap HM.! from, nodeMap HM.! to, label)) labels in - Graph (G.mkGraph labNodes labEdges) (nodeMap M.! entry) + Graph (G.mkGraph labNodes labEdges) (nodeMap HM.! entry) diff --git a/src/main/Main.hs b/src/main/Main.hs index b24762bb818ab3606075ab2e2ab473a176e648d1..f9b5ec9aa3a5c3a57c3d34b8ce0fe9eecac6c868 100644 --- a/src/main/Main.hs +++ b/src/main/Main.hs @@ -8,9 +8,10 @@ import System.Exit import System.IO import qualified Data.ByteString.Lazy as BS +import Data.Text (Text) import qualified Data.Text.IO as T -import Options.Applicative import Lens.Micro +import Options.Applicative import CFG.Types import qualified CFG.Parser as P @@ -115,7 +116,7 @@ main = do case (,) <$> JSON.parseFile sseJSON <*> JSON.parseFile searchJSON of Left err -> hPrint stderr err Right (sseGraph, searchGraph) -> - case isIsomorphic (preprocess sseGraph) searchGraph of + case isIsomorphic (preprocess sseGraph) (searchGraph :: Graph Text Text) of Isomorphic -> putStrLn "Graphs are isomorphic!" NotIsomorphic reason -> do putStrLn "Graphs are not isomorphic :(" diff --git a/test/Compare/JSONSpec.hs b/test/Compare/JSONSpec.hs index 85530504c435ebfe92ee3d950624d3e4b2dbec00..88896f72678f38d6bf25720c036e907b1d4c7890 100644 --- a/test/Compare/JSONSpec.hs +++ b/test/Compare/JSONSpec.hs @@ -12,14 +12,19 @@ import qualified Data.Set as S import Data.Text (Text) import Lens.Micro import Lens.Micro.Aeson +import qualified Data.HashMap.Lazy as HM import Compare.JSON +import Compare.SSEGraph import Compare.Types +import Search.Types (isEpsilon) spec :: Spec spec = do describe "parseFile" parseFileSpec describe "toJSON implementation for Graph" toJSONSpec + describe "NodeLabelMeta" metaSpec + describe "EdgeLabel" edgeLabelSpec exampleJson :: BS.ByteString exampleJson = BS.pack $ UTF8.encode $ unlines @@ -81,3 +86,58 @@ toJSONSpec = do it "convertes the point correctly" $ g ^?! key "entry" . _Integer `shouldBe` 0 + +metaSpec :: Spec +metaSpec = do + it "retains metadata from the original json" $ + case parseFile exampleJson :: Either String (Graph NodeLabelMeta Text) of + Left err -> expectationFailure err + Right g -> + let + nodes = g ^.. _graph . to G.labNodes . each . _2 + in + (nodes ^.. each . nodeMetaData . ix "runnable" . _String) + `shouldMatchList` + ["TaskA", "TaskB"] + + let + nodes = [ NodeLabelMeta "a" (HM.fromList [("runnable", "TaskA")]) + , NodeLabelMeta "b" (HM.fromList [("runnable", "TaskB")]) + ] + edges = [("a", "b", "foo")] :: [(Text, Text, Text)] + g = encode (mkGraph nodes edges "a" :: Graph NodeLabelMeta Text) + + it "writes metadata back out to json" $ + (g ^.. key "nodes" . values . key "runnable" . _String) + `shouldMatchList` ["TaskA", "TaskB"] + + it "also writes its id to json" $ + (g ^.. key "nodes" . values . key "id" . _String) + `shouldMatchList` ["a", "b"] + + +edgeLabelSpec :: Spec +edgeLabelSpec = do + it "serializes correctly" $ + case parseFile exampleJson :: Either String (Graph Text SSEEdgeLabel) of + Left err -> expectationFailure err + Right g -> + let + edges = g ^.. _graph . to G.labEdges . each . _3 + in + (edges ^.. each . unSSEEdgeLabel) `shouldMatchList` ["syscall_a"] + + let nodes = [0,1] :: [Int] + edges = [ (0, 1, SSEEdgeLabel "foo") + , (0, 1, SSEEdgeLabel "bar") + , (1, 0, SSEEdgeLabel "foo") + ] + g = encode (mkGraph nodes edges 0 :: Graph Int SSEEdgeLabel) + + it "deserializes correctly" $ + g ^.. key "edges" . values . key "label" . _String + `shouldMatchList` ["foo", "foo", "bar"] + + it "has a correct IsEpsilon instance" $ do + isEpsilon (SSEEdgeLabel "foo/bar") `shouldBe` False + isEpsilon (SSEEdgeLabel "ABB4()") `shouldBe` True