ogma-core: Use new JSON parsing interface. Refs #115.

The JSON parsing functions currently used by ogma-core are very specific to two formats supported, and cannot be easily generalized. This commit replaces the existing FRET component specficiation parser and converter by one that is based on the new generic parsing library.
nasa · Jan 22, 2024 · f41d795 · f41d795
1 parent a8b3dbc
commit f41d795
Show file tree

Hide file tree

Showing 5 changed files with 279 additions and 210 deletions.
diff --git a/ogma-core/ogma-core.cabal b/ogma-core/ogma-core.cabal
@@ -92,8 +92,8 @@ library
     Language.Trans.CStruct2CopilotStruct
     Language.Trans.CStructs2Copilot
     Language.Trans.CStructs2MsgHandlers
-    Language.Trans.FRETComponentSpec2Copilot
     Language.Trans.FRETReqsDB2Copilot
+    Language.Trans.Spec2Copilot
     Language.Trans.SMV2Copilot
 
   other-modules:
@@ -105,6 +105,7 @@ library
   build-depends:
       base                    >= 4.11.0.0 && < 5
     , aeson                   >= 2.0.0.0  && < 2.2
+    , bytestring
     , filepath
     , IfElse
     , mtl
@@ -113,9 +114,10 @@ library
     , ogma-language-c         >= 1.1.0 && < 1.2
     , ogma-language-cocospec  >= 1.1.0 && < 1.2
     , ogma-language-copilot   >= 1.1.0 && < 1.2
-    , ogma-language-fret-cs   >= 1.1.0 && < 1.2
     , ogma-language-fret-reqs >= 1.1.0 && < 1.2
+    , ogma-language-jsonspec  >= 1.1.0 && < 1.2
     , ogma-language-smv       >= 1.1.0 && < 1.2
+    , ogma-spec               >= 1.1.0 && < 1.2
 
   hs-source-dirs:
     src

diff --git a/ogma-core/src/Command/FPrimeApp.hs b/ogma-core/src/Command/FPrimeApp.hs
@@ -53,13 +53,14 @@ import Data.ByteString.Extra  as B ( safeReadFile )
 import Data.String.Extra      ( sanitizeLCIdentifier, sanitizeUCIdentifier )
 import System.Directory.Extra ( copyDirectoryRecursive )
 
+-- External imports: ogma
+import Data.OgmaSpec            (Spec, externalVariableName, externalVariables,
+                                 requirementName, requirements)
+import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec)
+
 -- Internal imports: auxiliary
 import Command.Result                 ( Result (..) )
 import Data.Location                  ( Location (..) )
-import Language.FRETComponentSpec.AST ( FRETComponentSpec,
-                                        fretExternalVariableName,
-                                        fretExternalVariables,
-                                        fretRequirementName, fretRequirements )
 
 -- Internal imports
 import Paths_ogma_core ( getDataDir )
@@ -153,14 +154,13 @@ fprimeApp' targetDir varNames varDB monitors =
 -- | Process FRET component spec, if available, and return its abstract
 -- representation.
 parseOptionalFRETCS :: Maybe FilePath
-                    -> ExceptT ErrorTriplet IO (Maybe FRETComponentSpec)
+                    -> ExceptT ErrorTriplet IO (Maybe (Spec String))
 parseOptionalFRETCS Nothing   = return Nothing
 parseOptionalFRETCS (Just fp) = do
   -- Throws an exception if the file cannot be read.
   content <- liftIO $ B.safeReadFile fp
-
-  let fretCS :: Either String FRETComponentSpec
-      fretCS = eitherDecode =<< content
+  let fretCS :: Either String (Spec String)
+      fretCS = parseJSONSpec return fretFormat =<< eitherDecode =<< content
 
   case fretCS of
     Left e   -> throwError $ cannotOpenFRETFile fp e
@@ -219,7 +219,7 @@ parseOptionalVarDBFile (Just fp) = do
 --
 -- If a FRET file is not provided, then the user must provide BOTH a variable
 -- list, and a list of handlers.
-checkArguments :: Maybe FRETComponentSpec
+checkArguments :: Maybe (Spec a)
                -> Maybe [String]
                -> Maybe [String]
                -> Either ErrorTriplet ()
@@ -232,19 +232,19 @@ checkArguments _       _         _         = Right ()
 
 -- | Extract the variables from a FRET component specification, and sanitize
 -- them to be used in FPrime.
-fretCSExtractExternalVariables :: Maybe FRETComponentSpec -> [String]
+fretCSExtractExternalVariables :: Maybe (Spec a) -> [String]
 fretCSExtractExternalVariables Nothing   = []
 fretCSExtractExternalVariables (Just cs) = map sanitizeLCIdentifier
-                                         $ map fretExternalVariableName
-                                         $ fretExternalVariables cs
+                                         $ map externalVariableName
+                                         $ externalVariables cs
 
 -- | Extract the requirements from a FRET component specification, and sanitize
 -- them to match the names of the handlers used by Copilot.
-fretCSExtractHandlers :: Maybe FRETComponentSpec -> [String]
+fretCSExtractHandlers :: Maybe (Spec a) -> [String]
 fretCSExtractHandlers Nothing   = []
 fretCSExtractHandlers (Just cs) = map handlerNameF
-                                $ map fretRequirementName
-                                $ fretRequirements cs
+                                $ map requirementName
+                                $ requirements cs
   where
     handlerNameF = ("handlerprop" ++) . sanitizeUCIdentifier
 
@@ -737,3 +737,19 @@ ecCannotOpenHandlersFile = 1
 -- permissions or some I/O error.
 ecCannotCopyTemplate :: ErrorCode
 ecCannotCopyTemplate = 1
+
+-- | JSONPath selectors for a FRET file
+fretFormat :: JSONFormat
+fretFormat = JSONFormat
+  { specInternalVars    = "..Internal_variables[*]"
+  , specInternalVarId   = ".name"
+  , specInternalVarExpr = ".assignmentCopilot"
+  , specInternalVarType = ".type"
+  , specExternalVars    = "..Other_variables[*]"
+  , specExternalVarId   = ".name"
+  , specExternalVarType = ".type"
+  , specRequirements    = "..Requirements[*]"
+  , specRequirementId   = ".name"
+  , specRequirementDesc = ".fretish"
+  , specRequirementExpr = ".ptLTL"
+  }
diff --git a/ogma-core/src/Command/FRETComponentSpec2Copilot.hs b/ogma-core/src/Command/FRETComponentSpec2Copilot.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ExistentialQuantification #-}
 -- Copyright 2020 United States Government as represented by the Administrator
 -- of the National Aeronautics and Space Administration. All Rights Reserved.
 --
@@ -41,7 +42,8 @@ module Command.FRETComponentSpec2Copilot
 
 -- External imports
 import Control.Monad.IfElse ( awhen )
-import Data.Aeson           ( eitherDecode )
+import Data.Aeson           ( eitherDecode, decode )
+import Data.ByteString.Lazy (fromStrict)
 
 -- External imports: auxiliary
 import Data.ByteString.Extra as B ( safeReadFile )
@@ -50,12 +52,22 @@ import Data.ByteString.Extra as B ( safeReadFile )
 import Command.Result ( Result (..) )
 import Data.Location  ( Location (..) )
 
--- Internal imports
-import           Language.FRETComponentSpec.AST           ( FRETComponentSpec )
-import qualified Language.Trans.FRETComponentSpec2Copilot as T
-  ( fretComponentSpec2Copilot
-  , FRETComponentSpec2CopilotOptions(FRETComponentSpec2CopilotOptions)
-  )
+-- Internal imports: language ASTs, transformers
+import Data.OgmaSpec (Spec)
+
+import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec
+import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec ( myLexer,
+                                                             pBoolSpec )
+
+import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec)
+
+import qualified Language.SMV.AbsSMV       as SMV
+import qualified Language.SMV.ParSMV       as SMV (myLexer, pBoolSpec)
+import           Language.SMV.Substitution (substituteBoolExpr)
+
+import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec (boolSpec2Copilot)
+import           Language.Trans.SMV2Copilot      as SMV (boolSpec2Copilot)
+import           Language.Trans.Spec2Copilot     (spec2Copilot, specAnalyze)
 
 -- | Print the contents of a Copilot module that implements the Past-time TL
 -- formula in a FRET file.
@@ -72,22 +84,44 @@ fretComponentSpec2Copilot :: FilePath -- ^ Path to a file containing a FRET
                           -> IO (Result ErrorCode)
 fretComponentSpec2Copilot fp options = do
 
-  -- 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.
-  fret <- parseFretComponentSpec fp
+  let functions = fretExprPair (fretCS2CopilotUseCoCoSpec options)
 
-  -- Extract internal command options from external command options
-  let internalOptions = fretComponentSpec2CopilotOptions options
-
-  let copilot = T.fretComponentSpec2Copilot internalOptions =<< fret
+  copilot <- fretComponentSpec2Copilot' fp options functions
 
   let (mOutput, result) =
         fretComponentSpec2CopilotResult options fp copilot
 
   awhen mOutput putStrLn
   return result
 
+-- | Print the contents of a Copilot module that implements the Past-time TL
+-- formula in a FRET file, using a subexpression handler.
+--
+-- PRE: The file given is readable, contains a valid FRET file with a PT
+-- formula in the @ptExpanded@ key, the formula does not use any identifiers
+-- that exist in Copilot, or any of @prop@, @clock@, @ftp@. All identifiers
+-- used are valid C99 identifiers.
+fretComponentSpec2Copilot' :: FilePath
+                           -> FRETComponentSpec2CopilotOptions
+                           -> FRETExprPair
+                           -> IO (Either String String)
+fretComponentSpec2Copilot' fp options (FRETExprPair parse replace print) = do
+  let name        = fretCS2CopilotFilename options
+      useCoCoSpec = fretCS2CopilotUseCoCoSpec options
+      typeMaps    = fretTypeToCopilotTypeMapping options
+
+  -- 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 -> return $ parseJSONSpec parse (fretFormat useCoCoSpec) =<< eitherDecode b
+
+  let copilot = spec2Copilot name typeMaps replace print =<< specAnalyze =<< res
+
+  return copilot
+
 -- | Options used to customize the conversion of FRET Component Specifications
 -- to Copilot code.
 data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions
@@ -97,17 +131,6 @@ data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions
   , fretCS2CopilotFilename    :: String
   }
 
--- | Parse a JSON file containing a FRET component specification.
---
--- Returns a 'Left' with an error message if the file does not have the correct
--- format.
---
--- Throws an exception if the file cannot be read.
-parseFretComponentSpec :: FilePath -> IO (Either String FRETComponentSpec)
-parseFretComponentSpec fp = do
-  content <- B.safeReadFile fp
-  return $ eitherDecode =<< content
-
 -- * Error codes
 
 -- | Encoding of reasons why the command can fail.
@@ -120,19 +143,6 @@ type ErrorCode = Int
 ecFretCSError :: ErrorCode
 ecFretCSError = 1
 
--- * Input arguments
-
--- | Convert command input argument options to internal transformation function
--- input arguments.
-fretComponentSpec2CopilotOptions :: FRETComponentSpec2CopilotOptions
-                                 -> T.FRETComponentSpec2CopilotOptions
-fretComponentSpec2CopilotOptions options =
-  T.FRETComponentSpec2CopilotOptions
-      (fretCS2CopilotUseCoCoSpec options)
-      (fretCS2CopilotIntType options)
-      (fretCS2CopilotRealType options)
-      (fretCS2CopilotFilename options)
-
 -- * Result
 
 -- | Process the result of the transformation function.
@@ -143,3 +153,52 @@ fretComponentSpec2CopilotResult :: FRETComponentSpec2CopilotOptions
 fretComponentSpec2CopilotResult options fp result = case result of
   Left msg -> (Nothing, Error ecFretCSError msg (LocationFile fp))
   Right t  -> (Just t, Success)
+
+-- * Parser
+
+-- | JSONPath selectors for a FRET file
+fretFormat :: Bool -> JSONFormat
+fretFormat useCoCoSpec = JSONFormat
+  { specInternalVars    = "..Internal_variables[*]"
+  , specInternalVarId   = ".name"
+  , specInternalVarExpr = ".assignmentCopilot"
+  , specInternalVarType = ".type"
+  , specExternalVars    = "..Other_variables[*]"
+  , specExternalVarId   = ".name"
+  , specExternalVarType = ".type"
+  , specRequirements    = "..Requirements[*]"
+  , specRequirementId   = ".name"
+  , specRequirementDesc = ".fretish"
+  , specRequirementExpr = if useCoCoSpec then ".CoCoSpecCode" else ".ptLTL"
+  }
+
+-- * Mapping of types from FRET to Copilot
+fretTypeToCopilotTypeMapping :: FRETComponentSpec2CopilotOptions
+                             -> [(String, String)]
+fretTypeToCopilotTypeMapping options =
+  [ ("bool",    "Bool")
+  , ("int",     fretCS2CopilotIntType options)
+  , ("integer", fretCS2CopilotIntType options)
+  , ("real",    fretCS2CopilotRealType options)
+  , ("string",  "String")
+  ]
+
+-- * Handler for boolean expressions
+
+-- | Handler for boolean expressions that knows how to parse them, replace
+-- variables in them, and convert them to Copilot.
+data FRETExprPair = forall a . FRETExprPair
+  { exprParse   :: String -> Either String a
+  , exprReplace :: [(String, String)] -> a -> a
+  , exprPrint   :: a -> String
+  }
+
+-- | Return a handler depending on whether it should be for CoCoSpec boolean
+-- expressions or for SMV boolean expressions.
+fretExprPair :: Bool -> FRETExprPair
+fretExprPair True  = FRETExprPair (CoCoSpec.pBoolSpec . CoCoSpec.myLexer)
+                                  (\_ -> id)
+                                  (CoCoSpec.boolSpec2Copilot)
+fretExprPair False = FRETExprPair (SMV.pBoolSpec . SMV.myLexer)
+                                  (substituteBoolExpr)
+                                  (SMV.boolSpec2Copilot)