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