ogma-language-jsonspec (empty) → 1.2.0
raw patch · 5 files changed
+284/−0 lines, 5 filesdep +aesondep +basedep +bytestringsetup-changedbinary-added
Dependencies added: aeson, base, bytestring, jsonpath, megaparsec, ogma-spec, text
Files
- CHANGELOG.md +6/−0
- LICENSE.pdf binary
- Setup.hs +2/−0
- ogma-language-jsonspec.cabal +82/−0
- src/Language/JSONSpec/Parser.hs +194/−0
+ CHANGELOG.md view
@@ -0,0 +1,6 @@+# Revision history for ogma-language-jsonspec++## [1.2.0] - 2024-01-21++* Version bump 1.2.0 (#117).+* Initial release (#115).
+ LICENSE.pdf view
binary file changed (absent → 117991 bytes)
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ogma-language-jsonspec.cabal view
@@ -0,0 +1,82 @@+-- 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-jsonspec+version: 1.2.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: JSON Frontend++description: Ogma is a tool to facilitate the integration of safe runtime monitors into+ other systems. Ogma extends+ <https://github.com/Copilot-Language/copilot Copilot>, a high-level runtime+ verification framework that generates hard real-time C99 code.+ .+ This library contains a frontend to read specifications from JSON 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.JSONSpec.Parser++ build-depends:+ base >= 4.11.0.0 && < 5+ , aeson >= 2.0.0.0 && < 2.2+ , jsonpath >= 0.3 && < 0.4+ , text+ , megaparsec+ , bytestring++ , ogma-spec >= 1.2.0 && < 1.3++ hs-source-dirs:+ src++ default-language:+ Haskell2010++ ghc-options:+ -Wall
+ src/Language/JSONSpec/Parser.hs view
@@ -0,0 +1,194 @@+-- 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.+--++-- | Parser for Ogma specs stored in JSON files.+module Language.JSONSpec.Parser where++-- External imports+import Data.Aeson (FromJSON (..), Value (..), decode, (.:))+import Data.Aeson.Key (toString)+import qualified Data.Aeson.KeyMap as M+import Data.Aeson.Types (prependFailure, typeMismatch)+import Data.Bifunctor (first)+import Data.ByteString.Lazy (fromStrict)+import Data.JSONPath.Execute+import Data.JSONPath.Parser+import Data.JSONPath.Types+import Data.Text (pack, unpack)+import qualified Data.Text as T+import qualified Data.Text.Encoding as T+import qualified Data.Text.IO as T+import Text.Megaparsec (eof, errorBundlePretty, parse)++-- External imports: ogma-spec+import Data.OgmaSpec++data JSONFormat = JSONFormat+ { specInternalVars :: String+ , specInternalVarId :: String+ , specInternalVarExpr :: String+ , specInternalVarType :: String+ , specExternalVars :: String+ , specExternalVarId :: String+ , specExternalVarType :: String+ , specRequirements :: String+ , specRequirementId :: String+ , specRequirementDesc :: String+ , specRequirementExpr :: String+ }++data JSONFormatInternal = JSONFormatInternal+ { jfiInternalVars :: [JSONPathElement]+ , jfiInternalVarId :: [JSONPathElement]+ , jfiInternalVarExpr :: [JSONPathElement]+ , jfiInternalVarType :: [JSONPathElement]+ , jfiExternalVars :: [JSONPathElement]+ , jfiExternalVarId :: [JSONPathElement]+ , jfiExternalVarType :: [JSONPathElement]+ , jfiRequirements :: [JSONPathElement]+ , jfiRequirementId :: [JSONPathElement]+ , jfiRequirementDesc :: [JSONPathElement]+ , jfiRequirementExpr :: [JSONPathElement]+ }++parseJSONFormat :: JSONFormat -> Either String JSONFormatInternal+parseJSONFormat jsonFormat = do+ jfi2 <- showErrors $ parseJSONPath (pack (specInternalVars jsonFormat))+ jfi3 <- showErrors $ parseJSONPath (pack (specInternalVarId jsonFormat))+ jfi4 <- showErrors $ parseJSONPath (pack (specInternalVarExpr jsonFormat))+ jfi5 <- showErrors $ parseJSONPath (pack (specInternalVarType jsonFormat))+ jfi6 <- showErrors $ parseJSONPath (pack (specExternalVars jsonFormat))+ jfi7 <- showErrors $ parseJSONPath (pack (specExternalVarId jsonFormat))+ jfi8 <- showErrors $ parseJSONPath (pack (specExternalVarType jsonFormat))+ jfi9 <- showErrors $ parseJSONPath (pack (specRequirements jsonFormat))+ jfi10 <- showErrors $ parseJSONPath (pack (specRequirementId jsonFormat))+ jfi11 <- showErrors $ parseJSONPath (pack (specRequirementDesc jsonFormat))+ jfi12 <- showErrors $ parseJSONPath (pack (specRequirementExpr jsonFormat))+ return $ JSONFormatInternal+ { jfiInternalVars = jfi2+ , jfiInternalVarId = jfi3+ , jfiInternalVarExpr = jfi4+ , jfiInternalVarType = jfi5+ , jfiExternalVars = jfi6+ , jfiExternalVarId = jfi7+ , jfiExternalVarType = jfi8+ , jfiRequirements = jfi9+ , jfiRequirementId = jfi10+ , jfiRequirementDesc = jfi11+ , jfiRequirementExpr = jfi12+ }++parseJSONSpec :: (String -> Either String a) -> JSONFormat -> Value -> Either String (Spec a)+parseJSONSpec parseExpr jsonFormat value = do+ jsonFormatInternal <- parseJSONFormat jsonFormat++ let values :: [Value]+ values = executeJSONPath (jfiInternalVars jsonFormatInternal) value++ internalVarDef :: Value -> Either String InternalVariableDef+ internalVarDef value = do+ let msg = "internal variable name"+ varId <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiInternalVarId jsonFormatInternal) value))++ let msg = "internal variable type"+ varType <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiInternalVarType jsonFormatInternal) value))++ let msg = "internal variable expr"+ varExpr <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiInternalVarExpr jsonFormatInternal) value))++ return $ InternalVariableDef+ { internalVariableName = varId+ , internalVariableType = varType+ , internalVariableExpr = varExpr+ }++ internalVariableDefs <- mapM internalVarDef values++ let values :: [Value]+ values = executeJSONPath (jfiExternalVars jsonFormatInternal) value++ externalVarDef :: Value -> Either String ExternalVariableDef+ externalVarDef value = do++ let msg = "external variable name"+ varId <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiExternalVarId jsonFormatInternal) value))++ let msg = "external variable type"+ varType <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiExternalVarType jsonFormatInternal) value))++ return $ ExternalVariableDef+ { externalVariableName = varId+ , externalVariableType = varType+ }++ externalVariableDefs <- mapM externalVarDef values++ let values :: [Value]+ values = executeJSONPath (jfiRequirements jsonFormatInternal) value++ -- requirementDef :: Value -> Either String (Requirement a)+ requirementDef value = do+ let msg = "Requirement name"+ reqId <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementId jsonFormatInternal) value))++ let msg = "Requirement expression"+ reqExpr <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementExpr jsonFormatInternal) value))+ reqExpr' <- parseExpr reqExpr++ let msg = "Requirement description"+ reqDesc <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementDesc jsonFormatInternal) value))++ return $ Requirement+ { requirementName = reqId+ , requirementExpr = reqExpr'+ , requirementDescription = reqDesc+ }++ requirements <- mapM requirementDef values++ return $ Spec internalVariableDefs externalVariableDefs requirements++valueToString :: String -> Value -> Either String String+valueToString msg (String x) = Right $ unpack x+valueToString msg _ = Left $ "The JSON value provided for " ++ msg ++ " does not contain a string"++listToEither :: String -> [a] -> Either String a+listToEither _ [x] = Right x+listToEither msg [] = Left $ "Failed to find a value for " ++ msg+listToEither msg _ = Left $ "Unexpectedly found multiple values for " ++ msg++-- | Parse a JSONPath expression, returning its element components.+parseJSONPath :: T.Text -> Either String [JSONPathElement]+parseJSONPath = first errorBundlePretty . parse (jsonPath eof) ""++showErrors :: Show a => Either a b -> Either String b+showErrors (Left s) = Left (show s)+showErrors (Right x) = Right x