diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,10 @@ # Revision history for ogma-core +## [1.2.0] - 2024-01-21 + +* Version bump 1.2.0 (#117). +* Generalize JSON parser (#115). + ## [1.1.0] - 2023-11-21 * Version bump 1.1.0 (#112). diff --git a/ogma-core.cabal b/ogma-core.cabal --- a/ogma-core.cabal +++ b/ogma-core.cabal @@ -32,7 +32,7 @@ build-type: Simple name: ogma-core -version: 1.1.0 +version: 1.2.0 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf @@ -92,8 +92,8 @@ Language.Trans.CStruct2CopilotStruct Language.Trans.CStructs2Copilot Language.Trans.CStructs2MsgHandlers - Language.Trans.FRETComponentSpec2Copilot Language.Trans.FRETReqsDB2Copilot + Language.Trans.Spec2Copilot Language.Trans.SMV2Copilot other-modules: @@ -105,17 +105,19 @@ build-depends: base >= 4.11.0.0 && < 5 , aeson >= 2.0.0.0 && < 2.2 + , bytestring , filepath , IfElse , mtl - , ogma-extra >= 1.1.0 && < 1.2 - , 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-smv >= 1.1.0 && < 1.2 + , ogma-extra >= 1.2.0 && < 1.3 + , ogma-language-c >= 1.2.0 && < 1.3 + , ogma-language-cocospec >= 1.2.0 && < 1.3 + , ogma-language-copilot >= 1.2.0 && < 1.3 + , ogma-language-fret-reqs >= 1.2.0 && < 1.3 + , ogma-language-jsonspec >= 1.2.0 && < 1.3 + , ogma-language-smv >= 1.2.0 && < 1.3 + , ogma-spec >= 1.2.0 && < 1.3 hs-source-dirs: src diff --git a/src/Command/FPrimeApp.hs b/src/Command/FPrimeApp.hs --- a/src/Command/FPrimeApp.hs +++ b/src/Command/FPrimeApp.hs @@ -53,13 +53,14 @@ 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 @@ -- | 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 @@ -- -- 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 @@ -- | 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 @@ -- 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/src/Command/FRETComponentSpec2Copilot.hs b/src/Command/FRETComponentSpec2Copilot.hs --- a/src/Command/FRETComponentSpec2Copilot.hs +++ b/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 @@ -- 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,13 +52,23 @@ 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,15 +84,9 @@ -> 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 - - -- Extract internal command options from external command options - let internalOptions = fretComponentSpec2CopilotOptions options + let functions = fretExprPair (fretCS2CopilotUseCoCoSpec options) - let copilot = T.fretComponentSpec2Copilot internalOptions =<< fret + copilot <- fretComponentSpec2Copilot' fp options functions let (mOutput, result) = fretComponentSpec2CopilotResult options fp copilot @@ -88,6 +94,34 @@ 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 @@ , 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 @@ 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 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) diff --git a/src/Command/ROSApp.hs b/src/Command/ROSApp.hs --- a/src/Command/ROSApp.hs +++ b/src/Command/ROSApp.hs @@ -56,13 +56,14 @@ 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 ) @@ -157,14 +158,13 @@ -- | 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 @@ -223,7 +223,7 @@ -- -- 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 String) -> Maybe [String] -> Maybe [String] -> Either ErrorTriplet () @@ -236,19 +236,19 @@ -- | Extract the variables from a FRET component specification, and sanitize -- them to be used in ROS. -fretCSExtractExternalVariables :: Maybe FRETComponentSpec -> [String] +fretCSExtractExternalVariables :: Maybe (Spec String) -> [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 String) -> [String] fretCSExtractHandlers Nothing = [] fretCSExtractHandlers (Just cs) = map handlerNameF - $ map fretRequirementName - $ fretRequirements cs + $ map requirementName + $ requirements cs where handlerNameF = ("handlerprop" ++) . sanitizeUCIdentifier @@ -712,3 +712,19 @@ -- 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/src/Language/Trans/FRETComponentSpec2Copilot.hs b/src/Language/Trans/FRETComponentSpec2Copilot.hs deleted file mode 100644 --- a/src/Language/Trans/FRETComponentSpec2Copilot.hs +++ /dev/null @@ -1,336 +0,0 @@ --- Copyright 2020 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. --- -{-# LANGUAGE OverloadedStrings #-} - --- | Transform a FRET Component Specification into a Copilot specification. --- --- Normally, this module would be implemented as a conversion between ASTs, but --- we want to add comments to the generated code, which are not representable --- in the abstract syntax tree. -module Language.Trans.FRETComponentSpec2Copilot where - --- External imports -import Data.List ( intersect, union ) -import Data.Maybe ( fromMaybe ) - --- External imports: auxiliary -import Data.String.Extra ( sanitizeLCIdentifier, sanitizeUCIdentifier ) - --- Internal imports: language ASTs, transformers -import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec ( myLexer, - pBoolSpec ) -import Language.FRETComponentSpec.AST as FRET -import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec ( boolSpec2Copilot ) -import Language.Trans.SMV2Copilot as SMV ( boolSpec2Copilot ) - --- | Options used to customize the conversion of FRET Component Specifications --- to Copilot code. -data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions - { fretCS2CopilotUseCoCoSpec :: Bool - , fretCS2CopilotIntType :: String - , fretCS2CopilotRealType :: String - , fretCS2CopilotFilename :: String - } - --- | Transform a FRET TL specification into a Copilot specification. --- --- This function may fail with a 'Left' value if the resulting Copilot --- specification would contain name clashes or other errors. -fretComponentSpec2Copilot :: FRETComponentSpec2CopilotOptions - -> FRETComponentSpec - -> Either String String -fretComponentSpec2Copilot prefs parseResult = - fretComponentSpec2Copilot' prefs =<< fret2CopilotAnalyze parseResult - --- | For a given FRET file, return the corresponding Copilot file, or an error --- message if such file cannot be generated. --- --- PRE: there are no name clashes between the variables and names used in the --- FRET specification and any definitions in Haskell's Prelude or in Copilot. -fretComponentSpec2Copilot' :: FRETComponentSpec2CopilotOptions - -> FRETComponentSpec - -> Either String String -fretComponentSpec2Copilot' prefs fretComponentSpec = - unlines . concat <$> sequence - [ pure imports - , pure externs - , internals - , reqs - , pure clock - , pure ftp - , pure pre - , pure tpre - , pure spec - , pure main' - ] - - where - - -- Import header block - imports :: [String] - imports = - [ "import Copilot.Compile.C99" - , "import Copilot.Language hiding (prop)" - , "import Copilot.Language.Prelude" - , "import Copilot.Library.LTL (next)" - , "import Copilot.Library.MTL hiding (since," - ++ " alwaysBeen, trigger)" - , "import Copilot.Library.PTLTL (since, previous," - ++ " alwaysBeen)" - , "import qualified Copilot.Library.PTLTL as PTLTL" - , "import qualified Copilot.Library.MTL as MTL" - , "import Language.Copilot (reify)" - , "import Prelude hiding ((&&), (||), (++)," - ++ " (<=), (>=), (<), (>), (==), (/=), not)" - , "" - ] - - -- Extern streams - externs = concatMap externVarToDecl - (FRET.fretExternalVariables fretComponentSpec) - where - externVarToDecl i = [ FRET.fretExternalVariableName i - ++ " :: Stream " - ++ "(" - ++ fretTypeToCopilotType - prefs - (FRET.fretExternalVariableType i) - ++ ")" - - , FRET.fretExternalVariableName i - ++ " = " - ++ "extern" - ++ " " - ++ show (FRET.fretExternalVariableName i) - ++ " " - ++ "Nothing" - , "" - ] - - -- Internal stream definitions - internals = concat - <$> mapM internalVarToDecl - (FRET.fretInternalVariables fretComponentSpec) - where - internalVarToDecl i = fmap (\implem -> - [ FRET.fretInternalVariableName i - ++ " :: Stream " - ++ "(" - ++ fretTypeToCopilotType - prefs - (FRET.fretInternalVariableType i) - ++ ")" - - , FRET.fretInternalVariableName i - ++ " = " - ++ implem - - , "" - ]) implementation - where - implementation = if null (FRET.fretInternalVariableCopilot i) - then CoCoSpec.boolSpec2Copilot - <$> CoCoSpec.pBoolSpec - ( CoCoSpec.myLexer - $ FRET.fretInternalVariableLustre i - ) - else pure (FRET.fretInternalVariableCopilot i) - - -- Encoding of requirements as boolean streams - reqs :: Either String [String] - reqs = concat <$> mapM reqToDecl (FRET.fretRequirements fretComponentSpec) - where - reqToDecl i = sequence - [ pure reqComment, pure reqSignature, reqBody, pure "" ] - where - -- Definition comment, which includes the requirement for - -- traceability purposes. - reqComment = "-- | " ++ FRET.fretRequirementName i ++ "\n" ++ - "-- @" ++ "\n" ++ - "-- " ++ FRET.fretRequirementFretish i ++ "\n" ++ - "-- @" - - -- Definition type signature. - reqSignature = FRET.fretRequirementName i - ++ " :: " ++ "Stream" ++ " " ++ "Bool" - - -- Definition implementation, either in SMV or in CoCoSpec - reqBody = if fretCS2CopilotUseCoCoSpec prefs - then reqBodyCoCo - else reqBodyPT - - reqBodyPT = fmap (\e -> FRET.fretRequirementName i ++ " = " - ++ SMV.boolSpec2Copilot e - ) - (fromMaybe (Left $ "No requirement for " ++ show i) - (FRET.fretRequirementPTExpanded i)) - - reqBodyCoCo = fmap - (\e -> FRET.fretRequirementName i ++ " = " - ++ CoCoSpec.boolSpec2Copilot e - ) - (fromMaybe (Left $ "No requirement for " ++ show i) - (FRET.fretRequirementCoCoSpec i)) - - -- Auxiliary streams: clock - clock :: [String] - clock = [ "" - , "-- | Clock that increases in one-unit steps." - , "clock :: Stream Int64" - , "clock = [0] ++ (clock + 1)" - , "" - ] - - -- Auxiliary streams: first time point - ftp :: [String] - ftp = [ "" - , "-- | First Time Point" - , "ftp :: Stream Bool" - , "ftp = [True] ++ false" - , "" - ] - - -- Auxiliary streams: pre - pre = [ "" - , "pre :: Stream Bool -> Stream Bool" - , "pre = ([False] ++)" - ] - - -- Auxiliary streams: tpre - tpre = [ "" - , "tpre :: Stream Bool -> Stream Bool" - , "tpre = ([True] ++)" - ] - - -- Main specification - spec :: [String] - spec = [ "" - , "-- | Complete specification. Calls the C function void " - ++ " handler(); when" - , "-- the property is violated." - , "spec :: Spec" - , "spec = do" - ] - ++ triggers - ++ [ "" ] - where - triggers :: [String] - triggers = fmap reqTrigger (FRET.fretRequirements fretComponentSpec) - - reqTrigger :: FRETRequirement -> String - reqTrigger r = " trigger " ++ show handlerName ++ " (not " - ++ propName ++ ") " ++ "[]" - where - handlerName = "handler" ++ FRET.fretRequirementName r - propName = FRET.fretRequirementName r - - -- Main program that compiles specification to C in two files (code and - -- header). - main' :: [String] - main' = [ "" - , "main :: IO ()" - , "main = reify spec >>= compile \"" - ++ fretCS2CopilotFilename prefs ++ "\"" - ] - --- | Return the corresponding type in Copilot matching a given FRET type. -fretTypeToCopilotType :: FRETComponentSpec2CopilotOptions -> String -> String -fretTypeToCopilotType _options "bool" = "Bool" -fretTypeToCopilotType options "int" = fretCS2CopilotIntType options -fretTypeToCopilotType options "integer" = fretCS2CopilotIntType options -fretTypeToCopilotType options "real" = fretCS2CopilotRealType options -fretTypeToCopilotType _options "string" = "String" -fretTypeToCopilotType _options x = x - --- | Analyze a FRET-Copilot file and determine if there will be any name --- clashes after the conversion to Copilot. --- --- This function does not compare against Haskell's prelude or Copilot's --- modules. It simply makes simple conversions to comply with Copilot/Haskell's --- grammar (e.g., variable/function names start with lowercase) and determines --- if the conversion would make two definitions in the given specification --- produce name clashes between them. -fret2CopilotAnalyze :: FRETComponentSpec -> Either String FRETComponentSpec -fret2CopilotAnalyze fretComponentSpec - | not (null evnClash) - = Left $ "Name clash detected: " ++ show evnClash - - | not (null ivnClash) - = Left $ "Name clash detected: " ++ show ivnClash - - | not (null reqClash) - = Left $ "Name clash detected: " ++ show reqClash - - | otherwise - = Right $ foldr applySubstitution fretComponentSpec nameSubstitutions - - where - - -- Sets containing name clashes - ivnClash = internalVariableNames' - `intersect` (externalVariableNames' `union` requirementNames') - - evnClash = externalVariableNames' - `intersect` (internalVariableNames' `union` requirementNames') - - reqClash = requirementNames' - `intersect` (internalVariableNames' - `union` externalVariableNames') - - -- Names used. - internalVariableNames' = map snd internalVariableMap - externalVariableNames' = map snd externalVariableMap - requirementNames' = map snd requirementNameMap - - -- Map from a variable name to its desired identifier in the code - -- generated. - internalVariableMap = - map (\x -> (x, sanitizeLCIdentifier x)) internalVariableNames - - externalVariableMap = - map (\x -> (x, sanitizeLCIdentifier x)) externalVariableNames - - requirementNameMap = - map (\x -> (x, "prop" ++ sanitizeUCIdentifier x)) requirementNames - - nameSubstitutions = internalVariableMap - ++ externalVariableMap - ++ requirementNameMap - - -- Variable/requirement names used in the component spec. - internalVariableNames = map fretInternalVariableName - $ fretInternalVariables fretComponentSpec - - externalVariableNames = map fretExternalVariableName - $ fretExternalVariables fretComponentSpec - - requirementNames = map fretRequirementName - $ fretRequirements fretComponentSpec diff --git a/src/Language/Trans/Spec2Copilot.hs b/src/Language/Trans/Spec2Copilot.hs new file mode 100644 --- /dev/null +++ b/src/Language/Trans/Spec2Copilot.hs @@ -0,0 +1,312 @@ +-- 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. + +-- | Transform an Ogma specification into a standalone Copilot specification. +-- +-- Normally, this module would be implemented as a conversion between ASTs, but +-- we want to add comments to the generated code, which are not representable +-- in the abstract syntax tree. +module Language.Trans.Spec2Copilot where + +-- External imports +import Data.List ( intersect, lookup, union ) +import Data.Maybe ( fromMaybe ) + +-- External imports: auxiliary +import Data.String.Extra ( sanitizeLCIdentifier, sanitizeUCIdentifier ) + +-- External imports: ogma-spec +import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..), + Requirement (..), Spec (..)) + +-- | For a given spec, return the corresponding Copilot file, or an error +-- message if such file cannot be generated. +-- +-- PRE: there are no name clashes between the variables and names used in the +-- specification and any definitions in Haskell's Prelude or in Copilot. +spec2Copilot :: String -- Spec / target file name + -> [(String, String)] -- Type substitution table + -> ([(String, String)] -> a -> a) -- Expr subsitution function + -> (a -> String) -- Expr show function + -> Spec a -- Specification + -> Either String String +spec2Copilot specName typeMaps exprTransform showExpr spec = + pure $ unlines $ concat + [ imports + , externs + , internals + , reqs + , clock + , ftp + , pre + , tpre + , copilotSpec + , main' + ] + + where + + -- Import header block + imports :: [String] + imports = + [ "import Copilot.Compile.C99" + , "import Copilot.Language hiding (prop)" + , "import Copilot.Language.Prelude" + , "import Copilot.Library.LTL (next)" + , "import Copilot.Library.MTL hiding (since," + ++ " alwaysBeen, trigger)" + , "import Copilot.Library.PTLTL (since, previous," + ++ " alwaysBeen)" + , "import qualified Copilot.Library.PTLTL as PTLTL" + , "import qualified Copilot.Library.MTL as MTL" + , "import Language.Copilot (reify)" + , "import Prelude hiding ((&&), (||), (++)," + ++ " (<=), (>=), (<), (>), (==), (/=), not)" + , "" + ] + + -- Extern streams + externs = concatMap externVarToDecl + (externalVariables spec) + where + externVarToDecl i = [ propName + ++ " :: Stream " + ++ "(" + ++ safeMap typeMaps (externalVariableType i) + ++ ")" + + , propName + ++ " = " + ++ "extern" + ++ " " + ++ show (externalVariableName i) + ++ " " + ++ "Nothing" + , "" + ] + where + propName = safeMap nameSubstitutions (externalVariableName i) + + -- Internal stream definitions + internals = concatMap internalVarToDecl + (internalVariables spec) + where + internalVarToDecl i = (\implem -> + [ propName + ++ " :: Stream " + ++ "(" + ++ safeMap typeMaps (internalVariableType i) + ++ ")" + + , propName + ++ " = " + ++ implem + + , "" + ]) implementation + where + propName = safeMap nameSubstitutions (internalVariableName i) + implementation = (internalVariableExpr i) + + -- Encoding of requirements as boolean streams + reqs :: [String] + reqs = concatMap reqToDecl (requirements spec) + where + reqToDecl i = [ reqComment, reqSignature + , reqBody nameSubstitutions + , "" + ] + where + reqName = safeMap nameSubstitutions (requirementName i) + + -- Definition comment, which includes the requirement for + -- traceability purposes. + reqComment = "-- | " ++ requirementName i ++ "\n" ++ + "-- @" ++ "\n" ++ + "-- " ++ requirementDescription i ++ "\n" ++ + "-- @" + + -- Definition type signature. + reqSignature = reqName + ++ " :: " ++ "Stream" ++ " " ++ "Bool" + + -- Definition implementation. We use an auxiliary function to + -- transform the implementation into Copilot, applying a + -- substitution. + reqBody subs = reqName ++ " = " ++ + (showExpr (exprTransform subs (requirementExpr i))) + + + -- Auxiliary streams: clock + clock :: [String] + clock = [ "" + , "-- | Clock that increases in one-unit steps." + , "clock :: Stream Int64" + , "clock = [0] ++ (clock + 1)" + , "" + ] + + -- Auxiliary streams: first time point + ftp :: [String] + ftp = [ "" + , "-- | First Time Point" + , "ftp :: Stream Bool" + , "ftp = [True] ++ false" + , "" + ] + + -- Auxiliary streams: pre + pre = [ "" + , "pre :: Stream Bool -> Stream Bool" + , "pre = ([False] ++)" + ] + + -- Auxiliary streams: tpre + tpre = [ "" + , "tpre :: Stream Bool -> Stream Bool" + , "tpre = ([True] ++)" + ] + + -- Main specification + copilotSpec :: [String] + copilotSpec = [ "" + , "-- | Complete specification. Calls the C function void " + ++ " handler(); when" + , "-- the property is violated." + , "spec :: Spec" + , "spec = do" + ] + ++ triggers + ++ [ "" ] + where + triggers :: [String] + triggers = fmap reqTrigger (requirements spec) + + reqTrigger :: Requirement a -> String + reqTrigger r = " trigger " ++ show handlerName ++ " (not " + ++ propName ++ ") " ++ "[]" + where + handlerName = "handler" ++ requirementName r + propName = requirementName r + + -- Main program that compiles specification to C in two files (code and + -- header). + main' :: [String] + main' = [ "" + , "main :: IO ()" + , "main = reify spec >>= compile \"" ++ specName ++ "\"" + ] + + -- Map from a variable name to its desired identifier in the code + -- generated. + internalVariableMap = + map (\x -> (x, sanitizeLCIdentifier x)) internalVariableNames + + externalVariableMap = + map (\x -> (x, sanitizeLCIdentifier x)) externalVariableNames + + requirementNameMap = + map (\x -> (x, "prop" ++ sanitizeUCIdentifier x)) requirementNames + + nameSubstitutions = internalVariableMap + ++ externalVariableMap + ++ requirementNameMap + + -- Variable/requirement names used in the component spec. + internalVariableNames = map internalVariableName + $ internalVariables spec + + externalVariableNames = map externalVariableName + $ externalVariables spec + + requirementNames = map requirementName + $ requirements spec + +specAnalyze :: Spec a -> Either String (Spec a) +specAnalyze spec + | not (null evnClash) + = Left $ "Name clash detected: " ++ show evnClash + + | not (null ivnClash) + = Left $ "Name clash detected: " ++ show ivnClash + + | not (null reqClash) + = Left $ "Name clash detected: " ++ show reqClash + + | otherwise + = Right spec + + where + + -- Sets containing name clashes + ivnClash = internalVariableNames' + `intersect` (externalVariableNames' `union` requirementNames') + + evnClash = externalVariableNames' + `intersect` (internalVariableNames' `union` requirementNames') + + reqClash = requirementNames' + `intersect` (internalVariableNames' + `union` externalVariableNames') + + -- Names used. + internalVariableNames' = map snd internalVariableMap + externalVariableNames' = map snd externalVariableMap + requirementNames' = map snd requirementNameMap + + -- Map from a variable name to its desired identifier in the code + -- generated. + internalVariableMap = + map (\x -> (x, sanitizeLCIdentifier x)) internalVariableNames + + externalVariableMap = + map (\x -> (x, sanitizeLCIdentifier x)) externalVariableNames + + requirementNameMap = + map (\x -> (x, "prop" ++ sanitizeUCIdentifier x)) requirementNames + + -- Variable/requirement names used in the component spec. + internalVariableNames = map internalVariableName + $ internalVariables spec + + externalVariableNames = map externalVariableName + $ externalVariables spec + + requirementNames = map requirementName + $ requirements spec + +-- * Auxiliary + +-- | Substitute a string based on a given substitution table. +-- +-- This function leaves the key unchanged if it cannot be found in the +-- substitution table. +safeMap :: [(String, String)] -> String -> String +safeMap ls k = fromMaybe k $ lookup k ls