diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,37 @@ +# Revision history for ogma-cli + +## [1.0.6] - 2022-11-21 + +* Version bump 1.0.6 (#64). +* Update license in cabal file to OtherLicense (#62). +* Add empty file to keep directory structure in distributable package (#65). + +## [1.0.5] - 2022-09-21 + +* Version bump 1.0.5 (#60). +* Update README to reflect that GHC 9.2 is supported (#55). + +## [1.0.4] - 2022-07-21 + +* Version bump 1.0.4 (#53). +* Address all hlint suggestions (#51). + +## [1.0.3] - 2022-05-21 + +* Version bump 1.0.3 (#49). +* Enable CI (#47). +* Conformance with style guide (partial) (#45). + +## [1.0.2] - 2022-03-21 + +* Version bump 1.0.2 (#43). +* Address HLint warning (#41). + +## [1.0.1] - 2022-01-21 + +* Version bump 1.0.1 (#39). +* Merge imports (#33). + +## [1.0.0] - 2021-11-22 + +* Initial release. diff --git a/LICENSE.pdf b/LICENSE.pdf new file mode 100644 Binary files /dev/null and b/LICENSE.pdf differ diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ogma-cli.cabal b/ogma-cli.cabal new file mode 100644 --- /dev/null +++ b/ogma-cli.cabal @@ -0,0 +1,153 @@ +-- 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. + +cabal-version: 2.0 +build-type: Simple + +name: ogma-cli +version: 1.0.6 +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: Helper tool to interoperate between Copilot and other languages. + +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. + . + Some use cases supported by Ogma include: + . + - Translating requirements defined in + + into corresponding monitors in Copilot. + . + - Generating the glue code necessary to work with C + structs in Copilot. + . + - Generating + + applications that use Copilot for monitoring data + received from the message bus. + . + - Generating message handlers for NASA Core Flight System + applications to make external data in structs available + to a Copilot monitor. + . + The main invocation with @--help@ lists sub-commands available. + . + >$ ogma --help + >ogma - an anything-to-Copilot application generator + > + >Usage: ogma COMMAND + > Generate complete or partial Copilot applications from multiple languages + > + >Available options: + > -h,--help Show this help text + > + >Available commands: + > structs Generate Copilot structs from C structs + > handlers Generate message handlers from C structs + > cfs Generate a complete CFS/Copilot application + > fret-component-spec Generate a Copilot file from a FRET Component + > Specification + > fret-reqs-db Generate a Copilot file from a FRET Requirements + > Database + . + For further information, see: + . + - . + . + - . + . + - . + . + - . + . + - , Perez, Dedden and Goodloe. 2020. + . + - , Dutle et al. 2020. + +executable ogma + + main-is: + Main.hs + + other-modules: + CLI.CommandCFSApp + CLI.CommandCStructs2Copilot + CLI.CommandCStructs2MsgHandlers + CLI.CommandFretComponentSpec2Copilot + CLI.CommandFretReqsDB2Copilot + CLI.CommandTop + CLI.Result + + build-depends: + base >= 4.11.0.0 && < 5 + , optparse-applicative + , ogma-core >= 1.0.0 && < 1.1 + + hs-source-dirs: + src + + default-language: + Haskell2010 + + ghc-options: + -Wall + +test-suite test-ogma + type: + exitcode-stdio-1.0 + + main-is: + Main.hs + + build-depends: + base + , HUnit + , process + , test-framework + , test-framework-hunit + , unix + + hs-source-dirs: + tests + + default-language: + Haskell2010 + + ghc-options: + -Wall diff --git a/src/CLI/CommandCFSApp.hs b/src/CLI/CommandCFSApp.hs new file mode 100644 --- /dev/null +++ b/src/CLI/CommandCFSApp.hs @@ -0,0 +1,117 @@ +-- 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. +-- +-- | CLI interface to the CFSApp subcommand. +module CLI.CommandCFSApp + ( + -- * Direct command access + command + , CommandOpts + , ErrorCode + + -- * CLI + , commandDesc + , commandOptsParser + ) + where + +-- External imports +import Options.Applicative ( Parser, help, long, metavar, optional, showDefault, + strOption, value ) + +-- External imports: command results +import Command.Result ( Result ) + +-- External imports: actions or commands supported +import Command.CFSApp ( ErrorCode, cFSApp ) + +-- * Command + +-- | Options needed to generate the cFS application. +data CommandOpts = CommandOpts + { cFSAppTarget :: String + , cFSAppVarNames :: String + , cFSAppVarDB :: Maybe String + } + +-- | Create (cFS) +-- applications that subscribe to the communication bus and call Copilot when +-- new messages arrive. +-- +-- This is just an uncurried version of "Command.CFSApp". +command :: CommandOpts -> IO (Result ErrorCode) +command c = + cFSApp (cFSAppTarget c) (cFSAppVarNames c) (cFSAppVarDB c) + +-- * CLI + +-- | cFS command description +commandDesc :: String +commandDesc = "Generate a complete cFS/Copilot application" + +-- | Subparser for the @cfs@ command, used to generate a NASA Core Flight +-- System application connected to Copilot monitors. +commandOptsParser :: Parser CommandOpts +commandOptsParser = CommandOpts + <$> strOption + ( long "app-target-dir" + <> metavar "DIR" + <> showDefault + <> value "copilot-cfs-demo" + <> help strCFSAppDirArgDesc + ) + <*> strOption + ( long "variable-file" + <> metavar "FILENAME" + <> showDefault + <> value "variables" + <> help strCFSAppVarListArgDesc + ) + <*> optional + ( strOption + ( long "variable-db" + <> metavar "FILENAME" + <> help strCFSAppVarDBArgDesc + ) + ) + +-- | Argument target directory to cFS app generation command +strCFSAppDirArgDesc :: String +strCFSAppDirArgDesc = "Target directory" + +-- | Argument variable list to cFS app generation command +strCFSAppVarListArgDesc :: String +strCFSAppVarListArgDesc = + "File containing list of cFS/ICAROUS variables to make accessible" + +-- | Argument variable database to cFS app generation command +strCFSAppVarDBArgDesc :: String +strCFSAppVarDBArgDesc = + "File containing a DB of known cFS/ICAROUS variables" diff --git a/src/CLI/CommandCStructs2Copilot.hs b/src/CLI/CommandCStructs2Copilot.hs new file mode 100644 --- /dev/null +++ b/src/CLI/CommandCStructs2Copilot.hs @@ -0,0 +1,86 @@ +-- 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. +-- +-- | CLI interface to the CStructs2Copilot subcommand +module CLI.CommandCStructs2Copilot + ( + -- * Direct command access + command + , CommandOpts + , ErrorCode + + -- * CLI + , commandDesc + , commandOptsParser + ) + where + +-- External imports +import Options.Applicative ( Parser, help, long, metavar, strOption ) + +-- External imports: command results +import Command.Result ( Result ) + +-- External imports: actions or commands supported +import Command.CStructs2Copilot ( ErrorCode, cstructs2Copilot ) + +-- * Command + +-- | A Copilot correspondence for a C struct can be generated by providing +-- the path to the file that declares the struct. +newtype CommandOpts = CommandOpts + { cstructsFileName :: FilePath } + +-- | Generate Copilot struct definitions and instances from structs defined in +-- a C header file. +-- +-- This is just an uncurried version of "Command.CStructs2Copilot". +command :: CommandOpts -> IO (Result ErrorCode) +command c = cstructs2Copilot (cstructsFileName c) + +-- * CLI + +-- | Command description for CLI help. +commandDesc :: String +commandDesc = "Generate Copilot structs from C structs" + +-- | Subparser for the @structs@ command, used to generate Copilot declarations +-- from C structs. +commandOptsParser :: Parser CommandOpts +commandOptsParser = CommandOpts + <$> strOption + ( long "header-file-name" + <> metavar "FILENAME" + <> help strStructsHeaderArgDesc + ) + +-- | Argument C header file to struct conversion command +strStructsHeaderArgDesc :: String +strStructsHeaderArgDesc = "C header file with struct definitions" diff --git a/src/CLI/CommandCStructs2MsgHandlers.hs b/src/CLI/CommandCStructs2MsgHandlers.hs new file mode 100644 --- /dev/null +++ b/src/CLI/CommandCStructs2MsgHandlers.hs @@ -0,0 +1,85 @@ +-- 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. +-- +-- | CLI interface to the CStructs2Copilot subcommand +module CLI.CommandCStructs2MsgHandlers + ( + -- * Direct command access + command + , CommandOpts + , ErrorCode + + -- * CLI + , commandDesc + , commandOptsParser + ) + where + +-- External imports +import Options.Applicative ( Parser, help, long, metavar, strOption ) + +-- External imports: command results +import Command.Result ( Result ) + +-- External imports: actions or commands supported +import Command.CStructs2MsgHandlers ( ErrorCode, cstructs2MsgHandlers ) + +-- * Command + +-- | Options to generate message handlers from C struct definitions. +newtype CommandOpts = CommandOpts + { msgHandlersFileName :: FilePath } + +-- | Generate C methods that process NASA Core Flight System messages dealing +-- with the structs defined in a header file. +-- +-- This is just an uncurried version of "Command.CStructs2MsgHandlers". +command :: CommandOpts -> IO (Result ErrorCode) +command c = cstructs2MsgHandlers (msgHandlersFileName c) + +-- * CLI + +-- | Command description for CLI help. +commandDesc :: String +commandDesc = "Generate message handlers from C structs" + +-- | Subparser for the @handlers@ command, used to generate message handers +-- from C structs. +commandOptsParser :: Parser CommandOpts +commandOptsParser = CommandOpts + <$> strOption + ( long "header-file-name" + <> metavar "FILENAME" + <> help strMsgHandlersHeaderArgDesc + ) + +-- | Argument C header file to handler generation command +strMsgHandlersHeaderArgDesc :: String +strMsgHandlersHeaderArgDesc = "C header file with struct definitions" diff --git a/src/CLI/CommandFretComponentSpec2Copilot.hs b/src/CLI/CommandFretComponentSpec2Copilot.hs new file mode 100644 --- /dev/null +++ b/src/CLI/CommandFretComponentSpec2Copilot.hs @@ -0,0 +1,136 @@ +-- 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. +-- +-- | CLI interface to the FRET CS 2 Copilot subcommand +module CLI.CommandFretComponentSpec2Copilot + ( + -- * Direct command access + command + , CommandOpts + , ErrorCode + + -- * CLI + , commandDesc + , commandOptsParser + ) + where + +-- External imports +import Options.Applicative (Parser, help, long, metavar, short, showDefault, + strOption, switch, value) + +-- External imports: command results +import Command.Result ( Result ) + +-- External imports: actions or commands supported +import Command.FRETComponentSpec2Copilot ( ErrorCode, + FRETComponentSpec2CopilotOptions(..), + fretComponentSpec2Copilot ) + +-- * Command + +-- | Options to generate Copilot from FRET Component Specifications. +data CommandOpts = CommandOpts + { fretComponentSpecFileName :: FilePath + , fretComponentSpecCoCoSpec :: Bool + , fretComponentSpecIntType :: String + , fretComponentSpecRealType :: String + } + +-- | Transform a FRET component specification into a Copilot specification. +-- +-- This is just an uncurried version of "Command.FRETComponentSpec2Copilot". +command :: CommandOpts -> IO (Result ErrorCode) +command c = + fretComponentSpec2Copilot + (fretComponentSpecFileName c) + internalCommandOpts + + where + + internalCommandOpts :: FRETComponentSpec2CopilotOptions + internalCommandOpts = FRETComponentSpec2CopilotOptions + { fretCS2CopilotUseCoCoSpec = fretComponentSpecCoCoSpec c + , fretCS2CopilotIntType = fretComponentSpecIntType c + , fretCS2CopilotRealType = fretComponentSpecRealType c + } + +-- * CLI + +-- | Command description for CLI help. +commandDesc :: String +commandDesc = + "Generate a Copilot file from a FRET Component Specification" + +-- | Subparser for the @fret-component-spec@ command, used to generate a +-- Copilot specification from a FRET component specification file. +commandOptsParser :: Parser CommandOpts +commandOptsParser = CommandOpts + <$> strOption + ( long "fret-file-name" + <> metavar "FILENAME" + <> help strFretArgDesc + ) + <*> switch + ( long "cocospec" + <> help strFretCoCoDesc + ) + <*> strOption + ( long "map-int-to" + <> short 'i' + <> metavar "TYPE_NAME" + <> help strFretIntTypeDesc + <> showDefault + <> value "Int64" + ) + <*> strOption + ( long "map-real-to" + <> short 'r' + <> metavar "TYPE_NAME" + <> help strFretRealTypeDesc + <> showDefault + <> value "Float" + ) + +-- | Argument FRET command description +strFretArgDesc :: String +strFretArgDesc = "FRET file with requirements." + +-- | CoCoSpec flag description +strFretCoCoDesc :: String +strFretCoCoDesc = "Use CoCoSpec variant of TL properties" + +-- | Int type mapping flag description. +strFretIntTypeDesc :: String +strFretIntTypeDesc = "Map integer variables to the given type" + +-- | Real type mapping flag description. +strFretRealTypeDesc :: String +strFretRealTypeDesc = "Map real variables to the given type" diff --git a/src/CLI/CommandFretReqsDB2Copilot.hs b/src/CLI/CommandFretReqsDB2Copilot.hs new file mode 100644 --- /dev/null +++ b/src/CLI/CommandFretReqsDB2Copilot.hs @@ -0,0 +1,107 @@ +-- 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. +-- +-- | CLI interface to the CStructs2Copilot subcommand +module CLI.CommandFretReqsDB2Copilot + ( + -- * Direct command access + command + , CommandOpts + , ErrorCode + + -- * CLI + , commandDesc + , commandOptsParser + ) + where + +-- External imports +import Options.Applicative ( Parser, help, long, metavar, strOption, switch ) + +-- External imports: command results +import Command.Result ( Result ) + +-- External imports: actions or commands supported +import Command.FRETReqsDB2Copilot ( ErrorCode, FRETReqsDB2CopilotOptions (..), + fretReqsDB2Copilot ) + +-- * Command + +-- | Options to generate Copilot from FRET Requirements Databases. +data CommandOpts = CommandOpts + { fretReqsDBFileName :: FilePath + , fretReqsDBCoCoSpec :: Bool + } + +-- | Transform a FRET requirements database containing a temporal logic +-- specification into a Copilot specification. +-- +-- This is just an uncurried version of "Command.FRETReqsDB2Copilot". +command :: CommandOpts -> IO (Result ErrorCode) +command c = + fretReqsDB2Copilot + (fretReqsDBFileName c) + internalCommandOpts + + where + + internalCommandOpts :: FRETReqsDB2CopilotOptions + internalCommandOpts = FRETReqsDB2CopilotOptions + { fretReqsDB2CopilotUseCoCoSpec = fretReqsDBCoCoSpec c + } + +-- * CLI + +-- | Command description for CLI help. +commandDesc :: String +commandDesc = + "Generate a Copilot file from a FRET Requirements Database" + +-- | Subparser for the @fret-reqs-db@ command, used to generate a Copilot +-- specification from a FRET file containing requirements only. +commandOptsParser :: Parser CommandOpts +commandOptsParser = CommandOpts + <$> strOption + ( long "fret-file-name" + <> metavar "FILENAME" + <> help strFretArgDesc + ) + <*> switch + ( long "cocospec" + <> help strFretCoCoDesc + ) + +-- | Argument FRET command description +strFretArgDesc :: String +strFretArgDesc = "FRET file with requirements." + +-- | CoCoSpec flag description +strFretCoCoDesc :: String +strFretCoCoDesc = "Use CoCoSpec variant of TL properties" diff --git a/src/CLI/CommandTop.hs b/src/CLI/CommandTop.hs new file mode 100644 --- /dev/null +++ b/src/CLI/CommandTop.hs @@ -0,0 +1,234 @@ +-- 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. +-- +-- | CLI parsing, handling, and execution. +-- +-- The full module CLI is just a sum of all the subcommands with their +-- respective CLI options. +-- +-- This module defines: +-- +-- - A 'CommandOpts' type that represents all options to the program, +-- the subcommand executed, and any options for that subcommand. +-- +-- - A 'commandOptsParser' parser for the subcommands and their arguments, +-- delegating the argument parsing to each subcommand's own CLI parser. +-- +-- - A 'command' function that dispatcher processing of the execution to the +-- appropriate subcommand. +-- +-- - An 'ErrorCode' type that represents reasons why the program may have +-- failed. +-- +-- Each of the subcommands is defined using the same standard interface. + +-- This module is merely a sum of all subcommands: +-- +-- - The type 'CommandOpts' is the sum of all respective subcommand options +-- (whose types all share the same name but have different representations). +-- +-- - The parser is a sum of all subparsers, each attached to a specific +-- command name defined in this module. +-- +-- - The command function is merely a dispatcher that detects the subcommand +-- that must be executed, extracts the input, runs it, and translates the +-- subcommands result into a top-level command result. +-- +-- - The error code is a plain representation that collapses the local +-- subcommand error codes into a few possible values. + +module CLI.CommandTop + ( + -- * Direct command access + CommandOpts + , command + , ErrorCode + + -- * CLI + , commandDesc + , commandOptsParser + ) + where + +-- External imports +import Options.Applicative ( CommandFields, Mod, Parser, helper, info, + progDesc, subparser, (<**>) ) +import qualified Options.Applicative as OptParse + +-- External imports: command results +import Command.Result ( Result ) + +-- Internal imports: subcommands +import qualified CLI.CommandCFSApp +import qualified CLI.CommandCStructs2Copilot +import qualified CLI.CommandCStructs2MsgHandlers +import qualified CLI.CommandFretComponentSpec2Copilot +import qualified CLI.CommandFretReqsDB2Copilot + +-- * Command + +-- | Commands supported by Ogma and their arguments. + +-- All subcommands use the same interface, so they all use the type name +-- @CommandOpts@ to capture their respective arguments. These types are +-- different for each subcommand. +data CommandOpts = + CommandOptsCFSApp CLI.CommandCFSApp.CommandOpts + | CommandOptsCStructs2Copilot CLI.CommandCStructs2Copilot.CommandOpts + | CommandOptsCStructs2MsgHandlers CLI.CommandCStructs2MsgHandlers.CommandOpts + | CommandOptsFretComponentSpec2Copilot CLI.CommandFretComponentSpec2Copilot.CommandOpts + | CommandOptsFretReqsDB2Copilot CLI.CommandFretReqsDB2Copilot.CommandOpts + +-- * CLI + +-- | Command description for CLI help. +commandDesc :: String +commandDesc = + "Generate complete or partial Copilot applications from multiple languages" + +-- | Subparser for multiple subcommands. +commandOptsParser :: Parser CommandOpts +commandOptsParser = subparser + ( subcommandCStructs + <> subcommandMsgHandlers + <> subcommandCFSApp + <> subcommandFretComponentSpec + <> subcommandFretReqs + ) + +-- | Modifier for the CStruct to Copilot Struct generation subcommand, linking +-- the subcommand options and description to the command @structs@ at top +-- level. +subcommandCStructs :: Mod CommandFields CommandOpts +subcommandCStructs = + subcommand + "structs" + (CommandOptsCStructs2Copilot + <$> CLI.CommandCStructs2Copilot.commandOptsParser) + CLI.CommandCStructs2Copilot.commandDesc + +-- | Modifier for the msg handler generation subcommand, linking the subcommand +-- options and description to the command @handlers@ at top level. +subcommandMsgHandlers :: Mod CommandFields CommandOpts +subcommandMsgHandlers = + subcommand + "handlers" + (CommandOptsCStructs2MsgHandlers + <$> CLI.CommandCStructs2MsgHandlers.commandOptsParser) + CLI.CommandCStructs2MsgHandlers.commandDesc + +-- | Modifier for the CFS app expansion subcommand, linking the subcommand +-- options and description to the command @cfs@ at top level. +subcommandCFSApp :: Mod CommandFields CommandOpts +subcommandCFSApp = + subcommand + "cfs" + (CommandOptsCFSApp <$> CLI.CommandCFSApp.commandOptsParser) + CLI.CommandCFSApp.commandDesc + +-- | Modifier for the FRET component spec to copilot subcommand, linking the +-- subcommand options and description to the command @fret-component-spec@ at +-- top level. +subcommandFretComponentSpec :: Mod CommandFields CommandOpts +subcommandFretComponentSpec = + subcommand + "fret-component-spec" + (CommandOptsFretComponentSpec2Copilot + <$> CLI.CommandFretComponentSpec2Copilot.commandOptsParser) + CLI.CommandFretComponentSpec2Copilot.commandDesc + +-- | Modifier for the FRET requirements DB to copilot subcommand, linking the +-- subcommand options and description to the command @fret-reqs-db@ at top +-- level. +subcommandFretReqs :: Mod CommandFields CommandOpts +subcommandFretReqs = + subcommand + "fret-reqs-db" + (CommandOptsFretReqsDB2Copilot + <$> CLI.CommandFretReqsDB2Copilot.commandOptsParser) + CLI.CommandFretReqsDB2Copilot.commandDesc + +-- * Command dispatcher + +-- | Command dispatcher that obtains the parameters from the command line and +-- passes them as arguments to the actual function that will process them, +-- transforming the local result into a global program result. + +-- This function is implemented as a combination of three processes or +-- functions: one that adapts the input to the inner function (down), the +-- actual function implementing the command, and a translation of the local +-- result into a global result that can be reported to users (up). In this +-- case, the commands are all using the same (and compatible) exit codes, but +-- they might not do so. This is captured by the fmap of the function id on +-- each processing command. +-- +-- The function that adapts the inputs simply passes the arguments obtained +-- from the command line one by one. Composition with this function uncurries +-- the next function to work over the product as defined by the record that +-- accompanies each command definition in the type OgmaCLICommand. +-- +-- Neither this nor the internal commands not know, and need to know, that they +-- run in CLI. +command :: CommandOpts -> IO (Result ErrorCode) +command (CommandOptsCFSApp c) = + id <$> CLI.CommandCFSApp.command c +command (CommandOptsCStructs2Copilot c) = + id <$> CLI.CommandCStructs2Copilot.command c +command (CommandOptsCStructs2MsgHandlers c) = + id <$> CLI.CommandCStructs2MsgHandlers.command c +command (CommandOptsFretComponentSpec2Copilot c) = + id <$> CLI.CommandFretComponentSpec2Copilot.command c +command (CommandOptsFretReqsDB2Copilot c) = + id <$> CLI.CommandFretReqsDB2Copilot.command c + +-- We indicate to HLint that the use of (id <$>) above should not trigger a +-- warning. Conceptually, there is a transformation taking place, but no change +-- is required because the types used by the internal functions and the +-- top-level command to represent results are the same, and the error codes are +-- non-overlapping. +{-# ANN command "HLint: ignore Functor law" #-} + +-- * Error codes + +-- | Encoding of reasons why the command can fail. +-- +-- The error code used is 1 for user error, 2 for internal bug. +type ErrorCode = Int + +-- * Auxiliary defs + +-- | Build a subcommand modifier from a command name, option parser and command +-- description. +subcommand :: String + -> Parser CommandOpts + -> String + -> Mod CommandFields CommandOpts +subcommand entry parser desc = + OptParse.command entry (info (parser <**> helper) (progDesc desc)) diff --git a/src/CLI/Result.hs b/src/CLI/Result.hs new file mode 100644 --- /dev/null +++ b/src/CLI/Result.hs @@ -0,0 +1,57 @@ +-- 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. +-- +-- | Process a result of a command in a way suitable for command-line +-- interaction. +module CLI.Result where + +-- External imports +import System.Exit ( ExitCode (ExitFailure, ExitSuccess), exitWith ) +import System.IO ( hPutStrLn, stderr ) + +-- External imports: command results +import Command.Result ( Result (Error, Success) ) +import Data.Location ( Location (..) ) + +{- HLINT ignore "Use exitSuccess" -} +-- | Process a result, report any pending messages, and exit with an error code +-- if necessary. +processResult :: Result Int -> IO () +processResult Success = exitWith ExitSuccess +processResult (Error ec msg loc) = do + hPutStrLn stderr $ showLocation loc ++ "error: " ++ msg + exitWith (ExitFailure ec) + where + -- | Show locations in a standard way in user messages. + showLocation :: Location -> String + showLocation LocationNothing = ": " + showLocation (LocationFile f) = f ++ ": " + showLocation (LocationFileLine f l) = f ++ ":" ++ show l ++ ": " + showLocation (LocationFileLC f l c) = f ++ ":" ++ show l ++ ":" ++ show c ++ ": " diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,81 @@ +-- 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. +-- +-- | Ogma: Tool to interoperate between +-- and other languages. +-- +-- Ogma is a tool to facilitate integration of safe runtime monitors into other +-- systems. It takes information from a system created in a language (e.g., +-- CoCoSpec ) and produces specifications for the runtime verification +-- framework . Currently, features +-- supported are: +-- +-- * Translation of ptLTL and Cocospec properties defined in a +-- file into corresponding +-- expressions in Copilot. +-- +-- * Translation of C headers declaring structs into the corresponding Copilot +-- Struct definitions. +-- +-- * Translation of C headers declaring structs into CFS message handlers that +-- copy data in global variables. +-- +-- * Generate NASA core Flight System (cFS) applications for runtime monitoring +-- using Copilot. +-- +-- More information can be obtained by calling ogma with the argument @--help@. +module Main + ( main ) + where + +-- External imports +import Options.Applicative (ParserInfo, execParser, fullDesc, header, helper, + info, progDesc, (<**>)) + +-- Internal imports: CLI parsing, handling, and processing of results. +import CLI.CommandTop ( CommandOpts, command, commandDesc, commandOptsParser ) +import CLI.Result ( processResult ) + +-- | Ogma: Helper tool to interoperate between Copilot and other languages. +main :: IO () +main = execParser fullCLIOpts >>= command >>= processResult + +-- | Full program options. +fullCLIOpts :: ParserInfo CommandOpts +fullCLIOpts = info (commandOptsParser <**> helper) + ( fullDesc + <> progDesc commandDesc + <> header strProgramSummary + ) + +-- | Short program description +strProgramSummary :: String +strProgramSummary = + "ogma - an anything-to-Copilot application generator" diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -0,0 +1,188 @@ +-- | Test Ogma +module Main where + +import Data.List ( intercalate ) +import Data.Monoid ( mempty ) +import System.Exit ( ExitCode (ExitSuccess) ) +import System.Process ( readProcessWithExitCode ) +import Test.Framework ( Test, defaultMainWithOpts ) +import Test.Framework.Providers.HUnit ( testCase ) +import Test.HUnit ( assertBool ) + +-- | Run all unit tests on Ogma. +main :: IO () +main = + defaultMainWithOpts tests mempty + +-- | All unit tests for Ogma +tests :: [Test.Framework.Test] +tests = + [ + testCase "cli-main-ok" (runErrorCode ["--help" ] True) + -- Should pass + + , testCase "cli-main-fail" (runErrorCode ["hfdsafdkajdfaskl"] False) + -- Should fail due to arguments being incorrect + + , testCase "cli-cmd-structs" (runErrorCode ["structs", "--help" ] True) + -- Should pass + + , testCase "cli-cmd-structs-fail" (runErrorCode ["structs", "--incorrect-argument"] False) + -- Should fail due to arguments being incorrect + + , testCase "cli-cmd-handlers" (runErrorCode ["handlers", "--help" ] True) + -- Should pass + + , testCase "cli-cmd-handlers-fail" (runErrorCode ["handlers", "--incorrect-argument"] False) + -- Should fail due to arguments being incorrect + + , testCase "cli-cmd-cfs" (runErrorCode ["cfs", "--help" ] True) + -- Should pass + + , testCase "cli-cmd-cfs-fail" (runErrorCode ["cfs", "--incorrect-argument"] False) + -- Should fail due to arguments being incorrect + + , testCase "cli-cmd-fret-component-spec" (runErrorCode ["fret-component-spec", "--help" ] True) + -- Should pass + + , testCase "cli-cmd-fret-component-spec-fail" (runErrorCode ["fret-component-spec", "--incorrect-argument"] False) + -- Should fail due to arguments being incorrect + + , testCase "cli-cmd-fret-reqs-db" (runErrorCode ["fret-reqs-db", "--help" ] True) + -- Should pass + + , testCase "cli-cmd-fret-reqs-db-fail" (runErrorCode ["fret-reqs-db", "--incorrect-argument"] False) + -- Should fail due to arguments being incorrect + + , testCase "fret-cmd-fret-parse-ok" (parseFretCopilot "examples/fret.json" True) + -- Should pass + + , testCase "fret-cmd-fret-file-not-found" (parseFretCopilot "tests/file-invalid.json" False) + -- Should fail because the file does not exist + + , testCase "fret-cmd-fret-parse-fail-1" (parseFretCopilot "tests/commands-fret-error-parsing-failed-1.json" False) + -- Should fail because the opening bracket is [ and not { + + , testCase "fret-cmd-fret-parse-fail-2" (parseFretCopilot "tests/commands-fret-error-parsing-failed-2.json" False) + -- Should fail because a field is missing in an external variable + + , testCase "fret-cmd-fret-parse-fail-3" (parseFretCopilot "tests/commands-fret-error-parsing-failed-3.json" False) + -- Should fail because a field is missing in an internal variable + + , testCase "fret-test2" (parseFretCoCoSpec "tests/fret-example1.json") + -- Should pass + + , testCase "structs-parse-ok" (testCStructs2Copilot "tests/reduced_geofence_msgs.h" True) + -- Should pass + + , testCase "structs-parse-fail-1" (testCStructs2Copilot "tests/reduced_geofence_msgs_bad.h" False) + -- Should fail because a keyword is incorrect + ] + +-- | Test C struct parser for a particular file. +-- +-- This test uses the Copilot backend for C header files, so it generates +-- Copilot types and instances. It may be convenient to run this action in a +-- temporary directory. +-- +-- This IO action fails if any of the following are true: +-- * Ogma cannot be found in the current PATH. +-- * Ogma cannot be executed. +-- * The given file is not found or accessible. +-- * The format in the given file is incorrect. +-- * Ogma fails due to an internal error or bug. +-- * The output file cannot be created due to lack of space or permissions. +-- +testCStructs2Copilot :: FilePath -- ^ Path to a C header file with structs + -> Bool + -> IO () +testCStructs2Copilot file success = do + (ec, _out, _err) <- readProcessWithExitCode "ogma" args "" + + -- True if success is expected and detected, or niether expected nor + -- detected. + let testPass = success == (ec == ExitSuccess) + + assertBool errorMsg testPass + where + args = ["structs", "--header-file-name", file] + errorMsg = "Result of processing file " ++ file ++ " failed" + +-- | Test FRET parser for a particular file. +-- +-- This test uses the Copilot backend for FRET files, so it generates a Copilot +-- file. It may be convenient to run this action in a temporary directory. +-- +-- This IO action fails if any of the following are true: +-- * Ogma cannot be found in the current PATH. +-- * Ogma cannot be executed. +-- * The given file is not found or accessible. +-- * The format in the given file is incorrect. +-- * Ogma fails due to an internal error or bug. +-- * The output file cannot be created due to lack of space or permissions. +-- +parseFretCopilot :: FilePath -- ^ Path to a FRET/JSON requirements file + -> Bool + -> IO () +parseFretCopilot file success = do + (ec, _out, _err) <- readProcessWithExitCode "ogma" args "" + + -- True if success is expected and detected, or niether expected nor + -- detected. + let testPass = success == (ec == ExitSuccess) + + assertBool errorMsg testPass + where + args = ["fret-component-spec", "--fret-file-name", file] + errorMsg = "Parsing file " ++ file ++ " result unexpected." + +-- | Test FRET CoCoSpec-based parser for a particular file. +-- +-- This test uses the Copilot backend for FRET files, so it generates a Copilot +-- file. It may be convenient to run this action in a temporary directory. +-- +-- This IO action fails if any of the following are true: +-- * Ogma cannot be found in the current PATH. +-- * Ogma cannot be executed. +-- * The given file is not found or accessible. +-- * The format in the given file is incorrect. +-- * Ogma fails due to an internal error or bug. +-- * The output file cannot be created due to lack of space or permissions. +-- +parseFretCoCoSpec :: FilePath -- ^ Path to a FRET/JSON requirements file + -> IO () +parseFretCoCoSpec file = do + (ec, _out, _err) <- readProcessWithExitCode "ogma" args "" + assertBool errorMsg (ec == ExitSuccess) + where + args = ["fret-reqs-db", "--fret-file-name", file, "--cocospec"] + errorMsg = "Parsing file " ++ file ++ " failed" + +-- | Test ogma by running it and checking the error code. +-- +-- This tests just whether ogma finishes with an error code or not. If files +-- may be generated for the command being tested, it may be convenient to run +-- this action in a temporary directory. +-- +-- This IO action fails if any of the following are true: +-- * Ogma cannot be found in the current PATH. +-- * Ogma cannot be executed. +-- * The given command is not valid. +-- * Ogma fails due to an internal error or bug. +-- * Output files cannot be created due to lack of space or permissions. +-- +runErrorCode :: [String] -- ^ Arguments to pass to ogma + -> Bool + -> IO () +runErrorCode args success = do + (ec, _out, _err) <- readProcessWithExitCode "ogma" args "" + + -- True if success is expected and detected, or niether expected nor + -- detected. + let testPass = success == (ec == ExitSuccess) + + assertBool errorMsg testPass + where + errorMsg = "Testing ogma's CLI parser with arguments " + ++ intercalate "," args + ++ " failed"