Make JSON graph parsing more generic

This allows to parse arbitrary metadata instead of just the node id
and edges.

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

src/Compare/JSON.hs

+{-# 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 "("

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 "("

src/Compare/SSEGraph.hs

+{-# 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

src/Compare/Types.hs

+{-# 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)

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 :("

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