-- | This module defines a data type for SV-COMP witness automatons, as
--   specified in https://github.com/sosy-lab/sv-witnesses.

{-# 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(..))

-- | A witness automaton. Adheres to the format specified in
-- https://github.com/sosy-lab/sv-witnesses/tree/a592b52c4034423d42bed2059addbc6d8f1fa443#data-elements.
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

    -- crux-llvm–specific extensions
  , WitnessEdge -> Maybe Int
edgeStartColumn              :: Maybe Int
      -- Not to be confused with startoffset, which records the total number
      -- of characters from the very start of the program. This, on the other
      -- hand, simply records the number of characters from the start of the
      -- current line, which I find to be a nice debugging tool.
  }
  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

    -- crux-llvm–specific extensions
  , 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
    -- Round to the nearest second to ensure that we do not print out seconds
    -- with a decimal component. This is an unforunate hack to work around
    -- https://github.com/sosy-lab/sv-witnesses/issues/40.
    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
        -- crux-llvm–specific extensions
      , 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
                      -- crux-llvm–specific extensions
                    , 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
      ]