-- | 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 [ "" , 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 ]