{-# Language NamedFieldPuns #-}
module Crux.SVCOMP.Witness
( Witness(..), WitnessNode(..), WitnessEdge(..)
, WitnessType(..), SourceCodeLang(..), Control(..), GraphMLAttrType(..)
, mkNode, mkNodeId, mkEdge
, ppWitness
) where
import Data.ByteString (ByteString)
import qualified Data.ByteString.Char8 as B (unpack)
import qualified Data.List as L (intercalate)
import Data.Maybe (catMaybes)
import Data.Time.Format.ISO8601 (iso8601Show)
import Data.Time.LocalTime (LocalTime(..), TimeOfDay(..), ZonedTime(..))
import Text.XML.Light
import Crux.SVCOMP (Arch(..))
data Witness = Witness
{ Witness -> WitnessType
witnessType :: WitnessType
, Witness -> SourceCodeLang
witnessSourceCodeLang :: SourceCodeLang
, Witness -> String
witnessProducer :: String
, Witness -> String
witnessSpecification :: String
, Witness -> String
witnessProgramFile :: FilePath
, Witness -> ByteString
witnessProgramHash :: ByteString
, Witness -> Arch
witnessArchitecture :: Arch
, Witness -> ZonedTime
witnessCreationTime :: ZonedTime
, Witness -> [WitnessNode]
witnessNodes :: [WitnessNode]
, Witness -> [WitnessEdge]
witnessEdges :: [WitnessEdge]
}
deriving Int -> Witness -> ShowS
[Witness] -> ShowS
Witness -> String
(Int -> Witness -> ShowS)
-> (Witness -> String) -> ([Witness] -> ShowS) -> Show Witness
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Witness -> ShowS
showsPrec :: Int -> Witness -> ShowS
$cshow :: Witness -> String
show :: Witness -> String
$cshowList :: [Witness] -> ShowS
showList :: [Witness] -> ShowS
Show
data WitnessNode = WitnessNode
{ WitnessNode -> String
nodeId :: Id
, WitnessNode -> Maybe Bool
nodeEntry :: Maybe Bool
, WitnessNode -> Maybe Bool
nodeSink :: Maybe Bool
, WitnessNode -> Maybe Bool
nodeViolation :: Maybe Bool
, WitnessNode -> Maybe String
nodeInvariant :: Maybe String
, WitnessNode -> Maybe String
nodeInvariantScope :: Maybe String
}
deriving Int -> WitnessNode -> ShowS
[WitnessNode] -> ShowS
WitnessNode -> String
(Int -> WitnessNode -> ShowS)
-> (WitnessNode -> String)
-> ([WitnessNode] -> ShowS)
-> Show WitnessNode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WitnessNode -> ShowS
showsPrec :: Int -> WitnessNode -> ShowS
$cshow :: WitnessNode -> String
show :: WitnessNode -> String
$cshowList :: [WitnessNode] -> ShowS
showList :: [WitnessNode] -> ShowS
Show
mkNode :: Int -> WitnessNode
mkNode :: Int -> WitnessNode
mkNode Int
i = WitnessNode
{ nodeId :: String
nodeId = Int -> String
mkNodeId Int
i
, nodeEntry :: Maybe Bool
nodeEntry = Maybe Bool
forall a. Maybe a
Nothing
, nodeSink :: Maybe Bool
nodeSink = Maybe Bool
forall a. Maybe a
Nothing
, nodeViolation :: Maybe Bool
nodeViolation = Maybe Bool
forall a. Maybe a
Nothing
, nodeInvariant :: Maybe String
nodeInvariant = Maybe String
forall a. Maybe a
Nothing
, nodeInvariantScope :: Maybe String
nodeInvariantScope = Maybe String
forall a. Maybe a
Nothing
}
mkNodeId :: Int -> Id
mkNodeId :: Int -> String
mkNodeId Int
i = String
"N" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
data WitnessEdge = WitnessEdge
{ WitnessEdge -> String
edgeSource :: Id
, WitnessEdge -> String
edgeTarget :: Id
, WitnessEdge -> Maybe Assumption
edgeAssumption :: Maybe Assumption
, WitnessEdge -> Maybe String
edgeAssumptionScope :: Maybe String
, WitnessEdge -> Maybe String
edgeAssumptionResultFunction :: Maybe String
, WitnessEdge -> Maybe Control
edgeControl :: Maybe Control
, WitnessEdge -> Maybe Int
edgeStartLine :: Maybe Int
, WitnessEdge -> Maybe Int
edgeEndLine :: Maybe Int
, WitnessEdge -> Maybe Int
edgeStartOffset :: Maybe Int
, WitnessEdge -> Maybe Int
edgeEndOffset :: Maybe Int
, WitnessEdge -> Maybe Bool
edgeEnterLoopHead :: Maybe Bool
, WitnessEdge -> Maybe String
edgeEnterFunction :: Maybe String
, WitnessEdge -> Maybe String
edgeReturnFromFunction :: Maybe String
, WitnessEdge -> Maybe String
edgeThreadId :: Maybe String
, WitnessEdge -> Maybe String
edgeCreateThread :: Maybe String
, WitnessEdge -> Maybe Int
edgeStartColumn :: Maybe Int
}
deriving Int -> WitnessEdge -> ShowS
[WitnessEdge] -> ShowS
WitnessEdge -> String
(Int -> WitnessEdge -> ShowS)
-> (WitnessEdge -> String)
-> ([WitnessEdge] -> ShowS)
-> Show WitnessEdge
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WitnessEdge -> ShowS
showsPrec :: Int -> WitnessEdge -> ShowS
$cshow :: WitnessEdge -> String
show :: WitnessEdge -> String
$cshowList :: [WitnessEdge] -> ShowS
showList :: [WitnessEdge] -> ShowS
Show
mkEdge :: Int -> Int -> WitnessEdge
mkEdge :: Int -> Int -> WitnessEdge
mkEdge Int
source Int
target = WitnessEdge
{ edgeSource :: String
edgeSource = Int -> String
mkNodeId Int
source
, edgeTarget :: String
edgeTarget = Int -> String
mkNodeId Int
target
, edgeAssumption :: Maybe Assumption
edgeAssumption = Maybe Assumption
forall a. Maybe a
Nothing
, edgeAssumptionScope :: Maybe String
edgeAssumptionScope = Maybe String
forall a. Maybe a
Nothing
, edgeAssumptionResultFunction :: Maybe String
edgeAssumptionResultFunction = Maybe String
forall a. Maybe a
Nothing
, edgeControl :: Maybe Control
edgeControl = Maybe Control
forall a. Maybe a
Nothing
, edgeStartLine :: Maybe Int
edgeStartLine = Maybe Int
forall a. Maybe a
Nothing
, edgeEndLine :: Maybe Int
edgeEndLine = Maybe Int
forall a. Maybe a
Nothing
, edgeStartOffset :: Maybe Int
edgeStartOffset = Maybe Int
forall a. Maybe a
Nothing
, edgeEndOffset :: Maybe Int
edgeEndOffset = Maybe Int
forall a. Maybe a
Nothing
, edgeEnterLoopHead :: Maybe Bool
edgeEnterLoopHead = Maybe Bool
forall a. Maybe a
Nothing
, edgeEnterFunction :: Maybe String
edgeEnterFunction = Maybe String
forall a. Maybe a
Nothing
, edgeReturnFromFunction :: Maybe String
edgeReturnFromFunction = Maybe String
forall a. Maybe a
Nothing
, edgeThreadId :: Maybe String
edgeThreadId = Maybe String
forall a. Maybe a
Nothing
, edgeCreateThread :: Maybe String
edgeCreateThread = Maybe String
forall a. Maybe a
Nothing
, edgeStartColumn :: Maybe Int
edgeStartColumn = Maybe Int
forall a. Maybe a
Nothing
}
data WitnessType
= CorrectnessWitness
| ViolationWitness
deriving Int -> WitnessType -> ShowS
[WitnessType] -> ShowS
WitnessType -> String
(Int -> WitnessType -> ShowS)
-> (WitnessType -> String)
-> ([WitnessType] -> ShowS)
-> Show WitnessType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WitnessType -> ShowS
showsPrec :: Int -> WitnessType -> ShowS
$cshow :: WitnessType -> String
show :: WitnessType -> String
$cshowList :: [WitnessType] -> ShowS
showList :: [WitnessType] -> ShowS
Show
ppWitnessType :: WitnessType -> String
ppWitnessType :: WitnessType -> String
ppWitnessType WitnessType
witnessType =
case WitnessType
witnessType of
WitnessType
CorrectnessWitness -> String
"correctness_witness"
WitnessType
ViolationWitness -> String
"violation_witness"
data SourceCodeLang
= C
| Java
deriving Int -> SourceCodeLang -> ShowS
[SourceCodeLang] -> ShowS
SourceCodeLang -> String
(Int -> SourceCodeLang -> ShowS)
-> (SourceCodeLang -> String)
-> ([SourceCodeLang] -> ShowS)
-> Show SourceCodeLang
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SourceCodeLang -> ShowS
showsPrec :: Int -> SourceCodeLang -> ShowS
$cshow :: SourceCodeLang -> String
show :: SourceCodeLang -> String
$cshowList :: [SourceCodeLang] -> ShowS
showList :: [SourceCodeLang] -> ShowS
Show
ppSourceCodeLang :: SourceCodeLang -> String
ppSourceCodeLang :: SourceCodeLang -> String
ppSourceCodeLang SourceCodeLang
sourceCodeLang =
case SourceCodeLang
sourceCodeLang of
SourceCodeLang
C -> String
"C"
SourceCodeLang
Java -> String
"Java"
ppArch :: Arch -> String
ppArch :: Arch -> String
ppArch Arch
arch =
case Arch
arch of
Arch
Arch32 -> String
"32bit"
Arch
Arch64 -> String
"64bit"
newtype Assumption = Assumption [String]
deriving Int -> Assumption -> ShowS
[Assumption] -> ShowS
Assumption -> String
(Int -> Assumption -> ShowS)
-> (Assumption -> String)
-> ([Assumption] -> ShowS)
-> Show Assumption
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Assumption -> ShowS
showsPrec :: Int -> Assumption -> ShowS
$cshow :: Assumption -> String
show :: Assumption -> String
$cshowList :: [Assumption] -> ShowS
showList :: [Assumption] -> ShowS
Show
ppAssumption :: Assumption -> String
ppAssumption :: Assumption -> String
ppAssumption (Assumption [String]
exprs) =
String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
";" [String]
exprs
data Control
= ConditionTrue
| ConditionFalse
deriving Int -> Control -> ShowS
[Control] -> ShowS
Control -> String
(Int -> Control -> ShowS)
-> (Control -> String) -> ([Control] -> ShowS) -> Show Control
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Control -> ShowS
showsPrec :: Int -> Control -> ShowS
$cshow :: Control -> String
show :: Control -> String
$cshowList :: [Control] -> ShowS
showList :: [Control] -> ShowS
Show
ppControl :: Control -> String
ppControl :: Control -> String
ppControl Control
control =
case Control
control of
Control
ConditionTrue -> String
"condition-true"
Control
ConditionFalse -> String
"condition-false"
data GraphMLAttrType
= Boolean
| Int
| Long
| Float
| Double
| String
deriving Int -> GraphMLAttrType -> ShowS
[GraphMLAttrType] -> ShowS
GraphMLAttrType -> String
(Int -> GraphMLAttrType -> ShowS)
-> (GraphMLAttrType -> String)
-> ([GraphMLAttrType] -> ShowS)
-> Show GraphMLAttrType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GraphMLAttrType -> ShowS
showsPrec :: Int -> GraphMLAttrType -> ShowS
$cshow :: GraphMLAttrType -> String
show :: GraphMLAttrType -> String
$cshowList :: [GraphMLAttrType] -> ShowS
showList :: [GraphMLAttrType] -> ShowS
Show
ppGraphMLAttrType :: GraphMLAttrType -> String
ppGraphMLAttrType :: GraphMLAttrType -> String
ppGraphMLAttrType GraphMLAttrType
ty =
case GraphMLAttrType
ty of
GraphMLAttrType
Boolean -> String
"boolean"
GraphMLAttrType
Int -> String
"int"
GraphMLAttrType
Long -> String
"long"
GraphMLAttrType
Float -> String
"float"
GraphMLAttrType
Double -> String
"double"
GraphMLAttrType
String -> String
"string"
data GraphMLAttrDomain
= Graph
| Node
| Edge
| All
deriving Int -> GraphMLAttrDomain -> ShowS
[GraphMLAttrDomain] -> ShowS
GraphMLAttrDomain -> String
(Int -> GraphMLAttrDomain -> ShowS)
-> (GraphMLAttrDomain -> String)
-> ([GraphMLAttrDomain] -> ShowS)
-> Show GraphMLAttrDomain
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GraphMLAttrDomain -> ShowS
showsPrec :: Int -> GraphMLAttrDomain -> ShowS
$cshow :: GraphMLAttrDomain -> String
show :: GraphMLAttrDomain -> String
$cshowList :: [GraphMLAttrDomain] -> ShowS
showList :: [GraphMLAttrDomain] -> ShowS
Show
ppGraphMLAttrDomain :: GraphMLAttrDomain -> String
ppGraphMLAttrDomain :: GraphMLAttrDomain -> String
ppGraphMLAttrDomain GraphMLAttrDomain
domain =
case GraphMLAttrDomain
domain of
GraphMLAttrDomain
Graph -> String
"graph"
GraphMLAttrDomain
Node -> String
"node"
GraphMLAttrDomain
Edge -> String
"edge"
GraphMLAttrDomain
All -> String
"all"
ppBool :: Bool -> String
ppBool :: Bool -> String
ppBool Bool
b =
case Bool
b of
Bool
False -> String
"false"
Bool
True -> String
"true"
ppByteString :: ByteString -> String
ppByteString :: ByteString -> String
ppByteString = ByteString -> String
B.unpack
ppInt :: Int -> String
ppInt :: Int -> String
ppInt = Int -> String
forall a. Show a => a -> String
show
ppString :: String -> String
ppString :: ShowS
ppString = ShowS
forall a. a -> a
id
ppZonedTime :: ZonedTime -> String
ppZonedTime :: ZonedTime -> String
ppZonedTime = ZonedTime -> String
forall t. ISO8601 t => t -> String
iso8601Show (ZonedTime -> String)
-> (ZonedTime -> ZonedTime) -> ZonedTime -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ZonedTime -> ZonedTime
roundNearestSecond
where
roundNearestSecond :: ZonedTime -> ZonedTime
roundNearestSecond :: ZonedTime -> ZonedTime
roundNearestSecond zt :: ZonedTime
zt@ZonedTime{ zonedTimeToLocalTime :: ZonedTime -> LocalTime
zonedTimeToLocalTime =
lt :: LocalTime
lt@LocalTime{ localTimeOfDay :: LocalTime -> TimeOfDay
localTimeOfDay =
tod :: TimeOfDay
tod@TimeOfDay{ todSec :: TimeOfDay -> Pico
todSec = Pico
sec }}} =
ZonedTime
zt{ zonedTimeToLocalTime =
lt{ localTimeOfDay =
tod{ todSec = fromInteger (round sec) }}}
type Id = String
dataNode :: String -> (a -> String) -> a -> Element
dataNode :: forall a. String -> (a -> String) -> a -> Element
dataNode String
keyVal a -> String
ppThing a
thing =
Attr -> Element -> Element
add_attr (Attr{attrKey :: QName
attrKey = String -> QName
unqual String
"key", attrVal :: String
attrVal = String
keyVal}) (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$
String -> String -> Element
forall t. Node t => String -> t -> Element
unode String
"data" (String -> Element) -> String -> Element
forall a b. (a -> b) -> a -> b
$
a -> String
ppThing a
thing
ppWitness :: Witness -> String
ppWitness :: Witness -> String
ppWitness Witness
witness =
[String] -> String
unlines [ String
"<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, Element -> String
ppElement (Element -> String) -> Element -> String
forall a b. (a -> b) -> a -> b
$ String -> Witness -> Element
forall t. Node t => String -> t -> Element
unode String
"graph" Witness
witness
]
instance Node Witness where
node :: QName -> Witness -> Element
node QName
n Witness{ WitnessType
witnessType :: Witness -> WitnessType
witnessType :: WitnessType
witnessType, SourceCodeLang
witnessSourceCodeLang :: Witness -> SourceCodeLang
witnessSourceCodeLang :: SourceCodeLang
witnessSourceCodeLang, String
witnessProducer :: Witness -> String
witnessProducer :: String
witnessProducer
, String
witnessSpecification :: Witness -> String
witnessSpecification :: String
witnessSpecification, String
witnessProgramFile :: Witness -> String
witnessProgramFile :: String
witnessProgramFile, ByteString
witnessProgramHash :: Witness -> ByteString
witnessProgramHash :: ByteString
witnessProgramHash
, Arch
witnessArchitecture :: Witness -> Arch
witnessArchitecture :: Arch
witnessArchitecture, ZonedTime
witnessCreationTime :: Witness -> ZonedTime
witnessCreationTime :: ZonedTime
witnessCreationTime
, [WitnessNode]
witnessNodes :: Witness -> [WitnessNode]
witnessNodes :: [WitnessNode]
witnessNodes, [WitnessEdge]
witnessEdges :: Witness -> [WitnessEdge]
witnessEdges :: [WitnessEdge]
witnessEdges
} =
[Attr] -> Element -> Element
add_attrs [ Attr{ attrKey :: QName
attrKey = String -> QName
unqual String
"xmlns"
, attrVal :: String
attrVal = String
"http://graphml.graphdrawing.org/xmlns"
}
, Attr{ attrKey :: QName
attrKey = String -> QName
unqual String
"xmlns:xsi"
, attrVal :: String
attrVal = String
"http://www.w3.org/2001/XMLSchema-instance"
}
, Attr{ attrKey :: QName
attrKey = String -> QName
unqual String
"xsi:schemaLocation"
, attrVal :: String
attrVal = String
"http://graphml.graphdrawing.org/xmlns http://graphml.graphdrawing.org/xmlns/1.0/graphml.xsd"
}
] (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$
String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode String
"graphml" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$
[ String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"witness-type" GraphMLAttrType
String GraphMLAttrDomain
Graph
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"sourcecodelang" GraphMLAttrType
String GraphMLAttrDomain
Graph
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"producer" GraphMLAttrType
String GraphMLAttrDomain
Graph
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"specification" GraphMLAttrType
String GraphMLAttrDomain
Graph
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"programfile" GraphMLAttrType
String GraphMLAttrDomain
Graph
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"programhash" GraphMLAttrType
String GraphMLAttrDomain
Graph
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"architecture" GraphMLAttrType
String GraphMLAttrDomain
Graph
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"creationtime" GraphMLAttrType
String GraphMLAttrDomain
Graph
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"entry" GraphMLAttrType
Boolean GraphMLAttrDomain
Node
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"sink" GraphMLAttrType
Boolean GraphMLAttrDomain
Node
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"violation" GraphMLAttrType
Boolean GraphMLAttrDomain
Node
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"invariant" GraphMLAttrType
String GraphMLAttrDomain
Node
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"invariant.scope" GraphMLAttrType
String GraphMLAttrDomain
Node
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"assumption" GraphMLAttrType
String GraphMLAttrDomain
Edge
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"assumption.scope" GraphMLAttrType
String GraphMLAttrDomain
Edge
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"assumption.resultfunction" GraphMLAttrType
String GraphMLAttrDomain
Edge
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"control" GraphMLAttrType
String GraphMLAttrDomain
Edge
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"startline" GraphMLAttrType
Int GraphMLAttrDomain
Edge
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"endline" GraphMLAttrType
Int GraphMLAttrDomain
Edge
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"startoffset" GraphMLAttrType
Int GraphMLAttrDomain
Edge
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"endoffset" GraphMLAttrType
Int GraphMLAttrDomain
Edge
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"enterLoopHead" GraphMLAttrType
Boolean GraphMLAttrDomain
Edge
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"enterFunction" GraphMLAttrType
String GraphMLAttrDomain
Edge
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"returnFromFunction" GraphMLAttrType
String GraphMLAttrDomain
Edge
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"threadId" GraphMLAttrType
String GraphMLAttrDomain
Edge
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"createThread" GraphMLAttrType
String GraphMLAttrDomain
Edge
, String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
"startcolumn" GraphMLAttrType
Int GraphMLAttrDomain
Edge
, Attr -> Element -> Element
add_attr (Attr{attrKey :: QName
attrKey = String -> QName
unqual String
"edgedefault", attrVal :: String
attrVal = String
"directed"}) (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$
QName -> [Element] -> Element
forall t. Node t => QName -> t -> Element
node QName
n ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$
[ String -> (WitnessType -> String) -> WitnessType -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"witness-type" WitnessType -> String
ppWitnessType WitnessType
witnessType
, String -> (SourceCodeLang -> String) -> SourceCodeLang -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"sourcecodelang" SourceCodeLang -> String
ppSourceCodeLang SourceCodeLang
witnessSourceCodeLang
, String -> ShowS -> String -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"producer" ShowS
ppString String
witnessProducer
, String -> ShowS -> String -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"specification" ShowS
ppString String
witnessSpecification
, String -> ShowS -> String -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"programfile" ShowS
ppString String
witnessProgramFile
, String -> (ByteString -> String) -> ByteString -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"programhash" ByteString -> String
ppByteString ByteString
witnessProgramHash
, String -> (Arch -> String) -> Arch -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"architecture" Arch -> String
ppArch Arch
witnessArchitecture
, String -> (ZonedTime -> String) -> ZonedTime -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"creationtime" ZonedTime -> String
ppZonedTime ZonedTime
witnessCreationTime
] [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ (WitnessNode -> Element) -> [WitnessNode] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (String -> WitnessNode -> Element
forall t. Node t => String -> t -> Element
unode String
"node") [WitnessNode]
witnessNodes
[Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ (WitnessEdge -> Element) -> [WitnessEdge] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (String -> WitnessEdge -> Element
forall t. Node t => String -> t -> Element
unode String
"edge") [WitnessEdge]
witnessEdges
]
where
keyNode :: Id -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode :: String -> GraphMLAttrType -> GraphMLAttrDomain -> Element
keyNode String
name GraphMLAttrType
ty GraphMLAttrDomain
domain =
[Attr] -> Element -> Element
add_attrs [ Attr{attrKey :: QName
attrKey = String -> QName
unqual String
"id", attrVal :: String
attrVal = String
name}
, Attr{attrKey :: QName
attrKey = String -> QName
unqual String
"attr.name", attrVal :: String
attrVal = String
name}
, Attr{attrKey :: QName
attrKey = String -> QName
unqual String
"attr.type", attrVal :: String
attrVal = GraphMLAttrType -> String
ppGraphMLAttrType GraphMLAttrType
ty}
, Attr{attrKey :: QName
attrKey = String -> QName
unqual String
"for", attrVal :: String
attrVal = GraphMLAttrDomain -> String
ppGraphMLAttrDomain GraphMLAttrDomain
domain}
] (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$
case GraphMLAttrType
ty of
GraphMLAttrType
Boolean -> String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode String
"key" [String -> String -> Element
forall t. Node t => String -> t -> Element
unode String
"default" (Bool -> String
ppBool Bool
False)]
GraphMLAttrType
_ -> String -> () -> Element
forall t. Node t => String -> t -> Element
unode String
"key" ()
instance Node WitnessNode where
node :: QName -> WitnessNode -> Element
node QName
n WitnessNode{ String
nodeId :: WitnessNode -> String
nodeId :: String
nodeId, Maybe Bool
nodeEntry :: WitnessNode -> Maybe Bool
nodeEntry :: Maybe Bool
nodeEntry, Maybe Bool
nodeSink :: WitnessNode -> Maybe Bool
nodeSink :: Maybe Bool
nodeSink
, Maybe Bool
nodeViolation :: WitnessNode -> Maybe Bool
nodeViolation :: Maybe Bool
nodeViolation, Maybe String
nodeInvariant :: WitnessNode -> Maybe String
nodeInvariant :: Maybe String
nodeInvariant, Maybe String
nodeInvariantScope :: WitnessNode -> Maybe String
nodeInvariantScope :: Maybe String
nodeInvariantScope
} =
Attr -> Element -> Element
add_attr (Attr{attrKey :: QName
attrKey = String -> QName
unqual String
"id", attrVal :: String
attrVal = String
nodeId}) (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$
QName -> [Element] -> Element
forall t. Node t => QName -> t -> Element
node QName
n ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ [Maybe Element] -> [Element]
forall a. [Maybe a] -> [a]
catMaybes
[ String -> (Bool -> String) -> Bool -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"entry" Bool -> String
ppBool (Bool -> Element) -> Maybe Bool -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Bool
nodeEntry
, String -> (Bool -> String) -> Bool -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"sink" Bool -> String
ppBool (Bool -> Element) -> Maybe Bool -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Bool
nodeSink
, String -> (Bool -> String) -> Bool -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"violation" Bool -> String
ppBool (Bool -> Element) -> Maybe Bool -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Bool
nodeViolation
, String -> ShowS -> String -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"invariant" ShowS
ppString (String -> Element) -> Maybe String -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
nodeInvariant
, String -> ShowS -> String -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"invariant.scope" ShowS
ppString (String -> Element) -> Maybe String -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
nodeInvariantScope
]
instance Node WitnessEdge where
node :: QName -> WitnessEdge -> Element
node QName
n WitnessEdge{ String
edgeSource :: WitnessEdge -> String
edgeSource :: String
edgeSource, String
edgeTarget :: WitnessEdge -> String
edgeTarget :: String
edgeTarget
, Maybe Assumption
edgeAssumption :: WitnessEdge -> Maybe Assumption
edgeAssumption :: Maybe Assumption
edgeAssumption, Maybe String
edgeAssumptionScope :: WitnessEdge -> Maybe String
edgeAssumptionScope :: Maybe String
edgeAssumptionScope, Maybe String
edgeAssumptionResultFunction :: WitnessEdge -> Maybe String
edgeAssumptionResultFunction :: Maybe String
edgeAssumptionResultFunction
, Maybe Control
edgeControl :: WitnessEdge -> Maybe Control
edgeControl :: Maybe Control
edgeControl, Maybe Int
edgeStartLine :: WitnessEdge -> Maybe Int
edgeStartLine :: Maybe Int
edgeStartLine, Maybe Int
edgeEndLine :: WitnessEdge -> Maybe Int
edgeEndLine :: Maybe Int
edgeEndLine, Maybe Int
edgeStartOffset :: WitnessEdge -> Maybe Int
edgeStartOffset :: Maybe Int
edgeStartOffset, Maybe Int
edgeEndOffset :: WitnessEdge -> Maybe Int
edgeEndOffset :: Maybe Int
edgeEndOffset
, Maybe Bool
edgeEnterLoopHead :: WitnessEdge -> Maybe Bool
edgeEnterLoopHead :: Maybe Bool
edgeEnterLoopHead, Maybe String
edgeEnterFunction :: WitnessEdge -> Maybe String
edgeEnterFunction :: Maybe String
edgeEnterFunction, Maybe String
edgeReturnFromFunction :: WitnessEdge -> Maybe String
edgeReturnFromFunction :: Maybe String
edgeReturnFromFunction
, Maybe String
edgeThreadId :: WitnessEdge -> Maybe String
edgeThreadId :: Maybe String
edgeThreadId, Maybe String
edgeCreateThread :: WitnessEdge -> Maybe String
edgeCreateThread :: Maybe String
edgeCreateThread
, Maybe Int
edgeStartColumn :: WitnessEdge -> Maybe Int
edgeStartColumn :: Maybe Int
edgeStartColumn
} =
[Attr] -> Element -> Element
add_attrs [ Attr{attrKey :: QName
attrKey = String -> QName
unqual String
"source", attrVal :: String
attrVal = String
edgeSource}
, Attr{attrKey :: QName
attrKey = String -> QName
unqual String
"target", attrVal :: String
attrVal = String
edgeTarget}
] (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$
QName -> [Element] -> Element
forall t. Node t => QName -> t -> Element
node QName
n ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ [Maybe Element] -> [Element]
forall a. [Maybe a] -> [a]
catMaybes
[ String -> (Assumption -> String) -> Assumption -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"assumption" Assumption -> String
ppAssumption (Assumption -> Element) -> Maybe Assumption -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Assumption
edgeAssumption
, String -> ShowS -> String -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"assumption.scope" ShowS
ppString (String -> Element) -> Maybe String -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
edgeAssumptionScope
, String -> ShowS -> String -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"assumption.resultfunction" ShowS
ppString (String -> Element) -> Maybe String -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
edgeAssumptionResultFunction
, String -> (Control -> String) -> Control -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"control" Control -> String
ppControl (Control -> Element) -> Maybe Control -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Control
edgeControl
, String -> (Int -> String) -> Int -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"startline" Int -> String
ppInt (Int -> Element) -> Maybe Int -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
edgeStartLine
, String -> (Int -> String) -> Int -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"endline" Int -> String
ppInt (Int -> Element) -> Maybe Int -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
edgeEndLine
, String -> (Int -> String) -> Int -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"startoffset" Int -> String
ppInt (Int -> Element) -> Maybe Int -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
edgeStartOffset
, String -> (Int -> String) -> Int -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"endoffset" Int -> String
ppInt (Int -> Element) -> Maybe Int -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
edgeEndOffset
, String -> (Bool -> String) -> Bool -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"enterLoopHead" Bool -> String
ppBool (Bool -> Element) -> Maybe Bool -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Bool
edgeEnterLoopHead
, String -> ShowS -> String -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"enterFunction" ShowS
ppString (String -> Element) -> Maybe String -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
edgeEnterFunction
, String -> ShowS -> String -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"returnFromFunction" ShowS
ppString (String -> Element) -> Maybe String -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
edgeReturnFromFunction
, String -> ShowS -> String -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"threadId" ShowS
ppString (String -> Element) -> Maybe String -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
edgeThreadId
, String -> ShowS -> String -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"createThread" ShowS
ppString (String -> Element) -> Maybe String -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
edgeCreateThread
, String -> (Int -> String) -> Int -> Element
forall a. String -> (a -> String) -> a -> Element
dataNode String
"startcolumn" Int -> String
ppInt (Int -> Element) -> Maybe Int -> Maybe Element
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
edgeStartColumn
]