diff --git a/ogma-core/CHANGELOG.md b/ogma-core/CHANGELOG.md index d70f88d6..d6a4569e 100644 --- a/ogma-core/CHANGELOG.md +++ b/ogma-core/CHANGELOG.md @@ -10,6 +10,7 @@ * Add command to transform state diagrams into monitors (#194). * Extend standalone command to use external process to parse properties (#197). * Enable using user-provided file as format definition spec (#200). +* Add support for XML files to standalone backend (#202). ## [1.5.0] - 2024-11-21 diff --git a/ogma-core/data/formats/xml-md_cocospec b/ogma-core/data/formats/xml-md_cocospec new file mode 100644 index 00000000..9f838f31 --- /dev/null +++ b/ogma-core/data/formats/xml-md_cocospec @@ -0,0 +1,13 @@ +XMLFormat + { XML.specInternalVars = Nothing + , XML.specInternalVarId = ("//*", Nothing) + , XML.specInternalVarExpr = ("//*", Nothing) + , XML.specInternalVarType = Nothing + , XML.specExternalVars = Nothing + , XML.specExternalVarId = ("//*", Nothing) + , XML.specExternalVarType = Nothing + , XML.specRequirements = ("//sysml:Requirement", Nothing) + , XML.specRequirementId = ("//sysml:Requirement/@Id/text()", Nothing) + , XML.specRequirementDesc = Just ("//sysml:Requirement/@Id/text()", Nothing) + , XML.specRequirementExpr = ("//sysml:Requirement/@Text/text()", Nothing) + } diff --git a/ogma-core/data/formats/xml-md_smv b/ogma-core/data/formats/xml-md_smv new file mode 100644 index 00000000..9f838f31 --- /dev/null +++ b/ogma-core/data/formats/xml-md_smv @@ -0,0 +1,13 @@ +XMLFormat + { XML.specInternalVars = Nothing + , XML.specInternalVarId = ("//*", Nothing) + , XML.specInternalVarExpr = ("//*", Nothing) + , XML.specInternalVarType = Nothing + , XML.specExternalVars = Nothing + , XML.specExternalVarId = ("//*", Nothing) + , XML.specExternalVarType = Nothing + , XML.specRequirements = ("//sysml:Requirement", Nothing) + , XML.specRequirementId = ("//sysml:Requirement/@Id/text()", Nothing) + , XML.specRequirementDesc = Just ("//sysml:Requirement/@Id/text()", Nothing) + , XML.specRequirementExpr = ("//sysml:Requirement/@Text/text()", Nothing) + } diff --git a/ogma-core/data/formats/xml-reqif_cocospec b/ogma-core/data/formats/xml-reqif_cocospec new file mode 100644 index 00000000..d838f8a4 --- /dev/null +++ b/ogma-core/data/formats/xml-reqif_cocospec @@ -0,0 +1,13 @@ +XMLFormat + { specInternalVars = Nothing + , specInternalVarId = ("//*", Nothing) + , specInternalVarExpr = ("//*", Nothing) + , specInternalVarType = Nothing + , specExternalVars = Nothing + , specExternalVarId = ("//*", Nothing) + , specExternalVarType = Nothing + , specRequirements = ("//SPEC-OBJECTS/SPEC-OBJECT/TYPE/SPEC-OBJECT-TYPE-REF[contains(text(),\"KEY\")]/../..", Just ("KEY", "//SPEC-OBJECT-TYPE[contains(@LONG-NAME, \"Requirement\")]/@IDENTIFIER/text()")) + , specRequirementId = ("//SPEC-OBJECT/@IDENTIFIER/text()", Nothing) + , specRequirementDesc = Just ("//ATTRIBUTE-VALUE-XHTML/DEFINITION/ATTRIBUTE-DEFINITION-XHTML-REF[contains(text(),'KEY')]/../../THE-VALUE/div/*", Just ("KEY", "//ATTRIBUTE-DEFINITION-XHTML[contains(@LONG-NAME, \"ReqIF.Name\")]/@IDENTIFIER/text()")) + , specRequirementExpr = ("//ATTRIBUTE-VALUE-XHTML/DEFINITION/ATTRIBUTE-DEFINITION-XHTML-REF[contains(text(),'KEY')]/../../THE-VALUE/div/*", Just ("KEY", "//ATTRIBUTE-DEFINITION-XHTML[contains(@LONG-NAME, \"ReqIF.Text\")]/@IDENTIFIER/text()")) + } diff --git a/ogma-core/data/formats/xml-reqif_smv b/ogma-core/data/formats/xml-reqif_smv new file mode 100644 index 00000000..d838f8a4 --- /dev/null +++ b/ogma-core/data/formats/xml-reqif_smv @@ -0,0 +1,13 @@ +XMLFormat + { specInternalVars = Nothing + , specInternalVarId = ("//*", Nothing) + , specInternalVarExpr = ("//*", Nothing) + , specInternalVarType = Nothing + , specExternalVars = Nothing + , specExternalVarId = ("//*", Nothing) + , specExternalVarType = Nothing + , specRequirements = ("//SPEC-OBJECTS/SPEC-OBJECT/TYPE/SPEC-OBJECT-TYPE-REF[contains(text(),\"KEY\")]/../..", Just ("KEY", "//SPEC-OBJECT-TYPE[contains(@LONG-NAME, \"Requirement\")]/@IDENTIFIER/text()")) + , specRequirementId = ("//SPEC-OBJECT/@IDENTIFIER/text()", Nothing) + , specRequirementDesc = Just ("//ATTRIBUTE-VALUE-XHTML/DEFINITION/ATTRIBUTE-DEFINITION-XHTML-REF[contains(text(),'KEY')]/../../THE-VALUE/div/*", Just ("KEY", "//ATTRIBUTE-DEFINITION-XHTML[contains(@LONG-NAME, \"ReqIF.Name\")]/@IDENTIFIER/text()")) + , specRequirementExpr = ("//ATTRIBUTE-VALUE-XHTML/DEFINITION/ATTRIBUTE-DEFINITION-XHTML-REF[contains(text(),'KEY')]/../../THE-VALUE/div/*", Just ("KEY", "//ATTRIBUTE-DEFINITION-XHTML[contains(@LONG-NAME, \"ReqIF.Text\")]/@IDENTIFIER/text()")) + } diff --git a/ogma-core/ogma-core.cabal b/ogma-core/ogma-core.cabal index 18c3d0e4..1159754f 100644 --- a/ogma-core/ogma-core.cabal +++ b/ogma-core/ogma-core.cabal @@ -78,6 +78,10 @@ data-files: templates/copilot-cfs/CMakeLists.txt data/formats/fcs_cocospec data/formats/fdb_smv data/formats/fdb_cocospec + data/formats/xml-md_cocospec + data/formats/xml-md_smv + data/formats/xml-reqif_cocospec + data/formats/xml-reqif_smv -- Ogma packages should be uncurated so that only the official maintainers make -- changes. @@ -137,6 +141,7 @@ library , ogma-language-copilot >= 1.5.0 && < 1.6 , ogma-language-jsonspec >= 1.5.0 && < 1.6 , ogma-language-smv >= 1.5.0 && < 1.6 + , ogma-language-xmlspec >= 1.5.0 && < 1.6 , ogma-spec >= 1.5.0 && < 1.6 hs-source-dirs: diff --git a/ogma-core/src/Command/Standalone.hs b/ogma-core/src/Command/Standalone.hs index b7d9f712..9532c58f 100644 --- a/ogma-core/src/Command/Standalone.hs +++ b/ogma-core/src/Command/Standalone.hs @@ -1,4 +1,5 @@ {-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} -- Copyright 2020 United States Government as represented by the Administrator @@ -44,7 +45,7 @@ import Control.Exception as E import Data.Aeson (decode, eitherDecode, object, (.=)) import Data.ByteString.Lazy (fromStrict) import Data.Foldable (for_) -import Data.List (isInfixOf, nub, (\\)) +import Data.List (isInfixOf, isPrefixOf, nub, (\\)) import Data.Maybe (fromMaybe) import System.Directory (doesFileExist) import System.Process (readProcess) @@ -64,6 +65,7 @@ import Paths_ogma_core (getDataDir) import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..), Requirement (..), Spec (..)) import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec) +import Language.XMLSpec.Parser (parseXMLSpec) -- Internal imports: language ASTs, transformers import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec @@ -135,7 +137,7 @@ standalone' :: FilePath -> StandaloneOptions -> ExprPair -> IO (Either String (String, String, String, String, String)) -standalone' fp options (ExprPair parse replace print ids) = do +standalone' fp options (ExprPair parse replace print ids def) = do let name = standaloneFilename options typeMaps = typeToCopilotTypeMapping options @@ -160,19 +162,25 @@ standalone' fp options (ExprPair parse replace print ids) = do if formatMissing then return $ Left $ standaloneIncorrectFormatSpec formatFile else do - format <- read <$> readFile formatFile + format <- readFile formatFile let wrapper = wrapVia (standalonePropVia options) parse - -- All of the following operations use Either to return error messages. -- The use of the monadic bind to pass arguments from one function to the -- next will cause the program to stop at the earliest error. - content <- B.safeReadFile fp - res <- case content of - Left s -> return $ Left s - Right b -> do case eitherDecode b of - Left e -> return $ Left e - Right v -> parseJSONSpec wrapper format v + res <- + if | isPrefixOf "XMLFormat" format + -> do let xmlFormat = read format + content <- readFile fp + parseXMLSpec wrapper def xmlFormat content + | otherwise + -> do let jsonFormat = read format + content <- B.safeReadFile fp + case content of + Left s -> return $ Left s + Right b -> do case eitherDecode b of + Left e -> return $ Left e + Right v -> parseJSONSpec wrapper jsonFormat v -- Complement the specification with any missing/implicit definitions let res' = fmap (addMissingIdentifiers ids) res @@ -276,11 +284,15 @@ typeToCopilotTypeMapping options = -- | Handler for boolean expressions that knows how to parse them, replace -- variables in them, and convert them to Copilot. +-- +-- It also contains a default value to be used whenever an expression cannot be +-- found in the input file. data ExprPair = forall a . ExprPair { exprParse :: String -> Either String a , exprReplace :: [(String, String)] -> a -> a , exprPrint :: a -> String , exprIdents :: a -> [String] + , exprUnknown :: a } -- | Return a handler depending on whether it should be for CoCoSpec boolean @@ -291,10 +303,12 @@ exprPair "cocospec" = ExprPair (CoCoSpec.pBoolSpec . CoCoSpec.myLexer) (\_ -> id) (CoCoSpec.boolSpec2Copilot) (CoCoSpec.boolSpecNames) + (CoCoSpec.BoolSpecSignal (CoCoSpec.Ident "undefined")) exprPair _ = ExprPair (SMV.pBoolSpec . SMV.myLexer) (substituteBoolExpr) (SMV.boolSpec2Copilot) (SMV.boolSpecNames) + (SMV.BoolSpecSignal (SMV.Ident "undefined")) -- | Add to a spec external variables for all identifiers mentioned in -- expressions that are not defined anywhere. diff --git a/ogma-language-xmlspec/CHANGELOG.md b/ogma-language-xmlspec/CHANGELOG.md new file mode 100644 index 00000000..eb5096af --- /dev/null +++ b/ogma-language-xmlspec/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for ogma-language-xmlspec + +## [1.X.Y] - 2024-01-27 + +* Initial release (#202). diff --git a/ogma-language-xmlspec/LICENSE.pdf b/ogma-language-xmlspec/LICENSE.pdf new file mode 100644 index 00000000..d4333fb2 Binary files /dev/null and b/ogma-language-xmlspec/LICENSE.pdf differ diff --git a/ogma-language-xmlspec/Setup.hs b/ogma-language-xmlspec/Setup.hs new file mode 100644 index 00000000..9a994af6 --- /dev/null +++ b/ogma-language-xmlspec/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ogma-language-xmlspec/ogma-language-xmlspec.cabal b/ogma-language-xmlspec/ogma-language-xmlspec.cabal new file mode 100644 index 00000000..cd3848a4 --- /dev/null +++ b/ogma-language-xmlspec/ogma-language-xmlspec.cabal @@ -0,0 +1,83 @@ +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY +-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT +-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO +-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A +-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE +-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF +-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN +-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR +-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR +-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER, +-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING +-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES +-- IT "AS IS."
 +-- +-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST +-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS +-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN +-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE, +-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S +-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE +-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY +-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY +-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS +-- AGREEMENT. + +cabal-version: 2.0 +build-type: Simple + +name: ogma-language-xmlspec +version: 1.5.0 +homepage: http://nasa.gov +license: OtherLicense +license-file: LICENSE.pdf +author: Ivan Perez, Alwyn Goodloe +maintainer: ivan.perezdominguez@nasa.gov +category: Aerospace +extra-source-files: CHANGELOG.md + +synopsis: Ogma: Runtime Monitor translator: XML Frontend + +description: Ogma is a tool to facilitate the integration of safe runtime monitors into + other systems. Ogma extends + , a high-level runtime + verification framework that generates hard real-time C99 code. + . + This library contains a frontend to read specifications from XML files. + +-- Ogma packages should be uncurated so that only the official maintainers make +-- changes. +-- +-- Because this is a NASA project, we want to make sure that users obtain +-- exactly what we publish, unmodified by anyone external to our project. +x-curation: uncurated + +library + + exposed-modules: + Language.XMLSpec.Parser + Language.XMLSpec.PrintTrees + + build-depends: + base >= 4.11.0.0 && < 5 + , mtl >= 2.2.2 && < 2.4 + , hxt >= 9.3.1.4 && < 9.4 + , hxt-regex-xmlschema >= 9.0 && < 9.3 + , hxt-xpath >= 8.5 && < 9.2 + , pretty >= 1.1 && < 1.2 + + , ogma-spec >= 1.5.0 && < 1.6 + + hs-source-dirs: + src + + default-language: + Haskell2010 + + ghc-options: + -Wall diff --git a/ogma-language-xmlspec/src/Language/XMLSpec/Parser.hs b/ogma-language-xmlspec/src/Language/XMLSpec/Parser.hs new file mode 100644 index 00000000..eac9087b --- /dev/null +++ b/ogma-language-xmlspec/src/Language/XMLSpec/Parser.hs @@ -0,0 +1,362 @@ +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY +-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT +-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO +-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A +-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE +-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF +-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN +-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR +-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR +-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER, +-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING +-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES +-- IT "AS IS." +-- +-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST +-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS +-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN +-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE, +-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S +-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE +-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY +-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY +-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS +-- AGREEMENT. + +-- | Parser for Ogma specs stored in XML files. +module Language.XMLSpec.Parser where + +-- External imports +import Control.Monad.Except (ExceptT (..), liftEither, throwError, runExceptT) +import Control.Monad.IO.Class (liftIO) +import Data.List (isPrefixOf) +import Data.Maybe (fromMaybe, listToMaybe) +import Text.XML.HXT.Core (configSysVars, no, readString, runX, + withCanonicalize, withOutputPLAIN, withRedirect, + withRemoveWS, withSubstDTDEntities, + withSubstHTMLEntities, withValidate, yes, (>>>)) +import Text.XML.HXT.XPath (getXPathTrees, parseXPathExpr) + +-- External imports: ogma-spec +import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..), + Requirement (..), Spec (Spec)) + +-- Internal imports +import Language.XMLSpec.PrintTrees (pretty, flattenDoc) + +-- | List of XPath routes to the elements we need to parse. +-- +-- The optional paths denote elements that may not exist. If they are nothing, +-- those elements are not parsed in the input file. +-- +-- The subfields are applied on each string matching the parent element. That +-- is, the internal var ID XPath will be a applied to the strings returned when +-- applying the internal vars XPath (if it exists). Paths whose names are +-- plural denote expected lists of elements. +-- +-- The components of a tuple (String, Maybe (String, String)) mean the +-- following: if a string is present but the second component is Nothing, then +-- the string is the XPath expression to be used. If a Just value is present, +-- the first element of its inner tuple represents a key, and the second +-- element represents an XPath expression that will produce a value when +-- evaluated globally in the file. After evaluating that expression, the key +-- must be found in the first string of the three and replaced with the result +-- of evaluating the expression. +data XMLFormat = XMLFormat + { specInternalVars :: Maybe String + , specInternalVarId :: (String, Maybe (String, String)) + , specInternalVarExpr :: (String, Maybe (String, String)) + , specInternalVarType :: Maybe (String, Maybe (String, String)) + , specExternalVars :: Maybe String + , specExternalVarId :: (String, Maybe (String, String)) + , specExternalVarType :: Maybe (String, Maybe (String, String)) + , specRequirements :: (String, Maybe (String, String)) + , specRequirementId :: (String, Maybe (String, String)) + , specRequirementDesc :: Maybe (String, Maybe (String, String)) + , specRequirementExpr :: (String, Maybe (String, String)) + } + deriving (Show, Read) + +-- | Parse an XML file and extract a Spec from it. +-- +-- An auxiliary function must be provided to parse the requirement expressions. +-- +-- Fails if any of the XPaths in the argument XMLFormat are not valid +-- expressions, of the XML is malformed, or if the elements are not found with +-- the frequency expected (e.g., an external variable id is not found even +-- though external variables are found). +parseXMLSpec :: (String -> IO (Either String a)) -- ^ Parser for expressions. + -> a + -> XMLFormat -- ^ XPaths for spec locations. + -> String -- ^ String containing XML + -> IO (Either String (Spec a)) +parseXMLSpec parseExpr defA xmlFormat value = runExceptT $ do + xmlFormatInternal <- parseXMLFormat xmlFormat value + + -- Internal variables + + -- intVarStrings :: [String] + intVarStrings <- liftIO $ maybe + (return []) + (`executeXPath` value) + (xfiInternalVars xmlFormatInternal) + + let internalVarDef :: String -> ExceptT String IO InternalVariableDef + internalVarDef def = do + let msgI = "internal variable name" + varId <- ExceptT $ + listToEither msgI <$> + executeXPath (xfiInternalVarId xmlFormatInternal) def + + let msgT = "internal variable type" + varType <- maybe + (liftEither $ Right "") + (\e -> ExceptT $ listToEither msgT <$> executeXPath e def) + (xfiInternalVarType xmlFormatInternal) + + let msgE = "internal variable expr" + varExpr <- ExceptT $ + listToEither msgE <$> + executeXPath (xfiInternalVarExpr xmlFormatInternal) def + + return $ InternalVariableDef + { internalVariableName = varId + , internalVariableType = varType + , internalVariableExpr = varExpr + } + + internalVariableDefs <- mapM internalVarDef intVarStrings + + -- External variables + + -- extVarStrings :: [String] + extVarStrings <- liftIO $ maybe + (return []) + (`executeXPath` value) + (xfiExternalVars xmlFormatInternal) + + let externalVarDef :: String -> ExceptT String IO ExternalVariableDef + externalVarDef def = do + + let msgI = "external variable name" + varId <- ExceptT $ + listToEither msgI <$> + executeXPath (xfiExternalVarId xmlFormatInternal) def + + let msgT = "external variable type" + varType <- maybe + (liftEither $ Right "") + (\e -> ExceptT $ listToEither msgT <$> executeXPath e def) + (xfiExternalVarType xmlFormatInternal) + + return $ ExternalVariableDef + { externalVariableName = varId + , externalVariableType = varType + } + + externalVariableDefs <- mapM externalVarDef extVarStrings + + -- Requirements + + -- reqStrings :: [String] + reqStrings <- liftIO $ executeXPath (xfiRequirements xmlFormatInternal) value + + let -- requirementDef :: String -> ExceptT String (Requirement a) + requirementDef def = do + -- let msgI = "Requirement name: " ++ take 160 def + reqId <- liftIO $ fromMaybe "" . listToMaybe <$> + executeXPath (xfiRequirementId xmlFormatInternal) def + + -- let msgE = "Requirement expression: " ++ take 160 def + reqExpr <- liftIO $ + listToMaybe <$> + concatMapM (`executeXPath` def) (xfiRequirementExpr xmlFormatInternal) + + reqExpr' <- maybe (return defA) + (ExceptT . parseExpr . textUnescape) + reqExpr + + -- let msgD = "Requirement description" + reqDesc <- maybe + (liftEither $ Right "") + (\e -> liftIO $ fromMaybe "" . listToMaybe <$> executeXPath e def) + (xfiRequirementDesc xmlFormatInternal) + + return $ Requirement + { requirementName = reqId + , requirementExpr = reqExpr' + , requirementDescription = reqDesc + } + + requirements <- mapM requirementDef reqStrings + + -- Complete spec + return $ Spec internalVariableDefs externalVariableDefs requirements + +-- | Internal representation of an XML Format specification. +data XMLFormatInternal = XMLFormatInternal + { xfiInternalVars :: Maybe XPathExpr + , xfiInternalVarId :: XPathExpr + , xfiInternalVarExpr :: XPathExpr + , xfiInternalVarType :: Maybe XPathExpr + , xfiExternalVars :: Maybe XPathExpr + , xfiExternalVarId :: XPathExpr + , xfiExternalVarType :: Maybe XPathExpr + , xfiRequirements :: XPathExpr + , xfiRequirementId :: XPathExpr + , xfiRequirementDesc :: Maybe XPathExpr + , xfiRequirementExpr :: [XPathExpr] + } + +-- | Internal representation of an XPath expression. +type XPathExpr = String + +-- | Resolve an indirect XPath query, returning an XPath expression. +resolveIndirectly :: String + -> (String, Maybe (String, String)) + -> ExceptT String IO XPathExpr +resolveIndirectly _ (query, Nothing) = + liftEither $ checkXPathExpr query + +resolveIndirectly xml (query, Just (key, val)) = do + -- Check that the given query string parses correctly. + _ <- liftEither $ checkXPathExpr val + + v <- liftIO $ executeXPath val xml + case v of + (f:_) -> do let query' = replace query key f + liftEither $ checkXPathExpr query' + _ -> throwError $ + "Substitution path " ++ show val ++ " not found in file." + +-- | Resolve an indirect XPath query, returning a list of XPath expressions. +resolveIndirectly' :: String + -> (String, Maybe (String, String)) + -> ExceptT String IO [XPathExpr] +resolveIndirectly' _ (query, Nothing) = + fmap (:[]) $ liftEither $ checkXPathExpr query + +resolveIndirectly' xml (query, Just (key, val)) = do + -- Check that the given query string parses correctly. + _ <- liftEither $ checkXPathExpr val + + v <- liftIO $ executeXPath val xml + case v of + [] -> throwError $ "Substitution path " ++ show val ++ " not found in file." + fs -> do let queries = map (replace query key) fs + liftEither $ mapM checkXPathExpr queries + +-- | Check that an XPath expression is syntactically correct. +checkXPathExpr :: String -> Either String XPathExpr +checkXPathExpr s = s <$ parseXPathExpr s + +-- | Check an XMLFormat and return an internal representation. +-- +-- Fails with an error message if any of the given expressions are not a valid +-- XPath expression. +parseXMLFormat :: XMLFormat -> String -> ExceptT String IO XMLFormatInternal +parseXMLFormat xmlFormat file = do + xfi2 <- liftEither $ swapMaybeEither + $ checkXPathExpr <$> specInternalVars xmlFormat + + xfi3 <- resolveIndirectly file $ specInternalVarId xmlFormat + + xfi4 <- resolveIndirectly file $ specInternalVarExpr xmlFormat + + xfi5 <- swapMaybeExceptT $ + resolveIndirectly file <$> specInternalVarType xmlFormat + + xfi6 <- liftEither $ + swapMaybeEither $ checkXPathExpr <$> specExternalVars xmlFormat + + xfi7 <- resolveIndirectly file $ specExternalVarId xmlFormat + + xfi8 <- swapMaybeExceptT $ + resolveIndirectly file <$> specExternalVarType xmlFormat + + xfi9 <- resolveIndirectly file $ specRequirements xmlFormat + + xfi10 <- resolveIndirectly file $ specRequirementId xmlFormat + + xfi11 <- swapMaybeExceptT $ + resolveIndirectly file <$> specRequirementDesc xmlFormat + + xfi12 <- resolveIndirectly' file $ specRequirementExpr xmlFormat + + return $ XMLFormatInternal + { xfiInternalVars = xfi2 + , xfiInternalVarId = xfi3 + , xfiInternalVarExpr = xfi4 + , xfiInternalVarType = xfi5 + , xfiExternalVars = xfi6 + , xfiExternalVarId = xfi7 + , xfiExternalVarType = xfi8 + , xfiRequirements = xfi9 + , xfiRequirementId = xfi10 + , xfiRequirementDesc = xfi11 + , xfiRequirementExpr = xfi12 + } + +-- | Execute an XPath query in an XML string, returning the list of strings +-- that match the path. +executeXPath :: String -> String -> IO [String] +executeXPath query string = do + let config = [ withValidate no + , withRedirect no + , withCanonicalize no + , withRemoveWS yes + , withSubstDTDEntities no + , withOutputPLAIN + , withSubstHTMLEntities no + ] + v <- runX $ configSysVars config + >>> (readString config string >>> getXPathTrees query) + + let u = map (flattenDoc . pretty . (:[])) v + + return u + +-- * Auxiliary + +-- | Unescape @'<'@, @'>'@ and @'&'@ in a string. +textUnescape :: String -> String +textUnescape ('&':'l':'t':';':xs) = '<' : textUnescape xs +textUnescape ('&':'g':'t':';':xs) = '>' : textUnescape xs +textUnescape ('&':'a':'m': 'p' : ';':xs) = '&' : textUnescape xs +textUnescape (x:xs) = x : textUnescape xs +textUnescape [] = [] + +-- | Swap the Maybe and Either layers of a value. +swapMaybeEither :: Maybe (Either a b) -> Either a (Maybe b) +swapMaybeEither Nothing = Right Nothing +swapMaybeEither (Just (Left s)) = Left s +swapMaybeEither (Just (Right x)) = Right $ Just x + +-- | Swap the Maybe and Either layers of a value. +swapMaybeExceptT :: Monad m => Maybe (ExceptT a m b) -> ExceptT a m (Maybe b) +swapMaybeExceptT Nothing = return Nothing +swapMaybeExceptT (Just e) = Just <$> e + +-- | Convert a list to an Either, failing if the list provided does not have +-- exactly one value. +listToEither :: String -> [String] -> Either String String +listToEither _ [x] = Right x +listToEither msg [] = Left $ "Failed to find a value for " ++ msg +listToEither msg _ = Left $ "Unexpectedly found multiple values for " ++ msg + +-- | Replace a string by another string +replace :: String -> String -> String -> String +replace [] _k _v = [] +replace string@(h:t) key value + | key `isPrefixOf` string + = value ++ replace (drop (length key) string) key value + | otherwise + = h : replace t key value + +-- | Map a monadic action over the elements of a container and concatenate the +-- resulting lists. +concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b] +concatMapM f = fmap concat . mapM f diff --git a/ogma-language-xmlspec/src/Language/XMLSpec/PrintTrees.hs b/ogma-language-xmlspec/src/Language/XMLSpec/PrintTrees.hs new file mode 100644 index 00000000..28f90953 --- /dev/null +++ b/ogma-language-xmlspec/src/Language/XMLSpec/PrintTrees.hs @@ -0,0 +1,352 @@ +{-# LANGUAGE FlexibleInstances #-} +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY +-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT +-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO +-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A +-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE +-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF +-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN +-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR +-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR +-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER, +-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING +-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES +-- IT "AS IS." +-- +-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST +-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS +-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN +-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE, +-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S +-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE +-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY +-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY +-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS +-- AGREEMENT. + +-- | Print XML trees. +-- +-- This variant of the function to show XML trees available in HXT is needed +-- because of issues with values being quoted by HXT's default function. +-- +-- It's based on the same ideas, but it's been implemented using the +-- pretty-library instead of using plain string functions. +module Language.XMLSpec.PrintTrees where + +-- External imports +import Data.Maybe (fromMaybe, isNothing) +import Data.Tree.NTree.TypeDefs (NTree (NTree)) +import Prelude hiding (quot, (<>)) +import Text.PrettyPrint.HughesPJ (Doc, Mode (..), Style (..), brackets, char, + colon, doubleQuotes, empty, equals, hcat, + int, isEmpty, parens, renderStyle, space, + text, vcat, (<+>), (<>)) +import Text.Regex.XMLSchema.Generic (sed) +import Text.XML.HXT.Core hiding (getDTDAttrl, getNode, mkDTDElem, + xshow, (<+>), txt) +import Text.XML.HXT.DOM.ShowXml (xshow) +import Text.XML.HXT.DOM.XmlNode (getDTDAttrl, getNode, mkDTDElem) + +-- | Render a document into a string. +flattenDoc :: Doc -> String +flattenDoc = renderStyle (Style LeftMode 0 0) + +-- | Class for values that can be converted into a document. +class Pretty x where + pretty :: x -> Doc + +instance Pretty [XmlTree] where + pretty = hcat . map pretty + +instance Pretty XmlTree where + pretty (NTree (XText s) _) = + text (textEscapeXml' s) + where + -- | Auxiliary function to escape certain XML characters + textEscapeXml' :: String -> String + textEscapeXml' = concatMap textEscapeChar + where + textEscapeChar '<' = "<" + textEscapeChar '>' = ">" + textEscapeChar '&' = "&" + textEscapeChar x = [x] + + pretty (NTree (XBlob blob) _) = + text (blobToString blob) + + pretty (NTree (XCharRef ref) _) = + text "&#" <> int ref <> char ';' + + pretty (NTree (XEntityRef ref) _) = + text "&" <> text ref <> char ';' + + pretty (NTree (XCmt comment) _) = + text "" + + pretty (NTree (XCdata txt) _) = + text " text txt' <> text "]]>" + where + -- Escape "]]>" if present in the data contents + txt' = sed (const "]]>") "\\]\\]>" txt + + pretty (NTree (XPi iName attributes) _) = + text " pretty iName + <> hcat (map prettyPIAttr attributes) + <> text "?>" + where + -- Print an attribute of a processing instruction. + prettyPIAttr :: XmlTree -> Doc + prettyPIAttr attrs + | (NTree (XAttr attrQName) children) <- attrs + , qualifiedName attrQName == a_value + = space <> pretty children + + -- + | otherwise + = pretty attrs + + pretty (NTree (XTag tagQName attributeList) []) = + angles (pretty tagQName <> pretty attributeList <> slash) + + pretty (NTree (XTag tagQName attributeList) children) = + angles (pretty tagQName <> pretty attributeList) <> pretty children + <> angles (slash <> pretty tagQName) + + pretty (NTree (XDTD dtdElem attributeList) children) = + pretty (dtdElem, attributeList, children) + + pretty (NTree (XAttr attrQName) children) = + space <> pretty attrQName <> equals <> doubleQuotes (pretty children) + + pretty (NTree (XError level txt) _) = + text "" + +instance Pretty (DTDElem, Attributes, XmlTrees) where + pretty (DOCTYPE, attributeList, children) = + text " pretty (a_name, attributeList) + <> prettyExternalId attributeList + <+> prettyInternalDTD children + <> text ">" + where + prettyInternalDTD [] = empty + prettyInternalDTD ds = brackets $ nl <> vcat (map pretty ds) + + pretty (ELEMENT, attributeList, children) = + text " pretty (a_name, attributeList) + <+> prettyElemType (lookup1 a_type attributeList) children + <> text " >" + + pretty (CONTENT, attributeList, children) = + prettyContent (mkDTDElem CONTENT attributeList children) + + pretty (ATTLIST, attributeList, children) = + text " ( if isNothing (lookup a_name attributeList) + then pretty children + else pretty (a_name, attributeList) + <+> prettyValue attributeList children + ) + <> text " >" + + pretty (ENTITY, attributeList, children) = + prettyEntity "" attributeList children + + pretty (PENTITY, attributeList, children) = + prettyEntity "% " attributeList children + + pretty (NOTATION, attributeList, _children) = + text " pretty (a_name, attributeList) + <> prettyExternalId attributeList + <> text " >" + + pretty (CONDSECT, _, child:children) = + text " pretty child + <> text " [\n" + <> pretty children + <> text "]]>" + + pretty (CONDSECT, _, []) = + empty + + pretty (NAME, attributeList, _children) = + pretty (a_name, attributeList) + + pretty (PEREF, attributeList, _children) = + prettyPEAttr attributeList + +instance Pretty QName where + pretty = text . qualifiedName + +instance Pretty (String, Attributes) where + pretty (k, attributeList) = text (lookup1 k attributeList) + +-- * Auxiliary functions related to pretty printing XML trees. + +-- | Pretty print an attribute followed by its value. +prettyAttr :: String -> Attributes -> Doc +prettyAttr k attributeList + | Just v <- lookup k attributeList + = text k <+> text v + | otherwise + = empty + +-- | Pretty print a content element. +prettyContent :: XmlTree -> Doc +prettyContent (NTree (XDTD NAME attributeList) _) = + pretty (a_name, attributeList) +prettyContent (NTree (XDTD PEREF attributeList) _) = + prettyPEAttr attributeList +prettyContent (NTree (XDTD CONTENT attributeList) children) = + parens (sepBy separator (map prettyContent children)) + <> pretty (a_modifier, attributeList) + where + separator = text (if a_kind == v_seq then ", " else " | ") +prettyContent (NTree (XDTD n _) _) = + error $ "prettyContent " ++ show n ++ " is undefined" +prettyContent tree = pretty tree + +-- | Pretty print the type of an element. +prettyElemType :: String -> XmlTrees -> Doc +prettyElemType elemType children + | elemType == v_pcdata + = parens (text v_pcdata) + + | elemType == v_mixed && not (null children) + , let [NTree (XDTD CONTENT attributeList') children'] = children + = parens + ( sepBy + (text " | ") + ( text v_pcdata + : map (prettyEnum . treeElemAttributes. getNode) children' + ) + ) + <> pretty (a_modifier, attributeList') + + | elemType == v_mixed -- incorrect tree + = parens empty + + | elemType == v_children && not (null children) + = prettyContent (head children) + + | elemType == v_children + = parens empty + + | elemType == k_peref + = hcat $ map prettyContent children + + | otherwise + = text elemType + + where + treeElemAttributes (XDTD _ attributeList') = attributeList' + treeElemAttributes (XText txt) = [(a_name, txt)] + treeElemAttributes _ = [] + +-- | Pretty print an entity. +prettyEntity :: String -> Attributes -> XmlTrees -> Doc +prettyEntity kind attributeList children = + text " text kind + <> pretty (a_name, attributeList) + <> prettyExternalId attributeList + <+> prettyAttr k_ndata attributeList + <+> prettyLiteralTrees children + <> text " >" + +-- | Pretty print trees as text, quoting them. +prettyLiteralTrees :: XmlTrees -> Doc +prettyLiteralTrees [] = empty +prettyLiteralTrees children = doubleQuotes $ text $ xshow children + +-- | Pretty print an external ID. +prettyExternalId :: Attributes -> Doc +prettyExternalId attributeList = + case (lookup k_system attributeList, lookup k_public attributeList) of + (Nothing, Nothing) -> empty + (Just s, Nothing) -> text k_system <+> doubleQuotes (text s) + (Nothing, Just p ) -> space <> text k_public <+> doubleQuotes (text p) + (Just s, Just p ) -> space <> text k_public <+> doubleQuotes (text p) + <+> doubleQuotes (text s) + +-- | Pretty print a Parameter Entity Reference. +prettyPEAttr :: Attributes -> Doc +prettyPEAttr = maybe empty (\pe -> char '%' <> text pe <> char ';') + . lookup a_peref + +-- | Given a list of attributes, pretty print the value in them. +prettyValue :: Attributes -> XmlTrees -> Doc +prettyValue attributeList children + | Just aValue <- lookup a_value attributeList + = text aValue + <+> prettyAttrType (lookup1 a_type attributeList) + <+> prettyAttrKind (lookup1 a_kind attributeList) + + | otherwise + = prettyPEAttr $ fromMaybe [] $ getDTDAttrl $ head children + where + + prettyAttrType attrType + | attrType == k_peref = prettyPEAttr attributeList + | attrType == k_enumeration = prettyAttrEnum + | attrType == k_notation = text k_notation <+> prettyAttrEnum + | otherwise = text attrType + + prettyAttrEnum = + parens $ sepBy (text " | ") $ + map (prettyEnum . fromMaybe [] . getDTDAttrl) children + where + + prettyAttrKind kind + | kind == k_default + = doubleQuotes (text (lookup1 a_default attributeList)) + + | kind == k_fixed + = text k_fixed + <+> doubleQuotes (text (lookup1 a_default attributeList)) + + | otherwise + = text kind + +-- Pretty print the name of an attribute, followed by the PE Reference. +prettyEnum :: Attributes -> Doc +prettyEnum attributes = pretty (a_name, attributes) <> prettyPEAttr attributes + +-- ** Generic document constructors + +-- | Forward slash character. +slash :: Doc +slash = char '/' + +-- | New line character. +nl :: Doc +nl = char '\n' + +-- | Enclose document in angle brackets. +angles :: Doc -> Doc +angles s = char '<' <> s <> char '>' + +-- | Compose two documents, separating them by a new line. +-- +-- The new line is not inserted if either document is empty. +(<|>) :: Doc -> Doc -> Doc +(<|>) x y + | isEmpty x = y + | isEmpty y = x + | otherwise = x <> nl <> y + +-- | Concatenate a list od documents, separating them by a given separator. +sepBy :: Doc -- ^ Separator + -> [Doc] -- ^ List of documents + -> Doc +sepBy _ [] = empty +sepBy _ [x] = x +sepBy sep (x:xs) = x <> sep <> sepBy sep xs