diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,39 @@ +# Revision history for ogma-core + +## [1.0.6] - 2022-11-21 + +* Version bump 1.0.6 (#64). +* Update license in cabal file to OtherLicense (#62). + +## [1.0.5] - 2022-09-21 + +* Version bump 1.0.5 (#60). +* Bump version bounds of Aeson (#55). +* Support floating point numbers in SMV expressions (#58). + +## [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). +* Conformance with style guide (partial) (#45). + +## [1.0.2] - 2022-03-21 + +* Version bump 1.0.2 (#43). +* Fix compilation error in unit tests (#42). +* Remove reduntant parenthesis (#40). + +## [1.0.1] - 2022-01-21 + +* Version bump 1.0.1 (#39). +* Align definitions consistently (#35). +* Indent ogma-core:Language.Trans.CStruct2CopilotStruct.buildCField (#36). +* Indent ogma-core:Command.Result module declaration (#37). + +## [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-core.cabal b/ogma-core.cabal new file mode 100644 --- /dev/null +++ b/ogma-core.cabal @@ -0,0 +1,137 @@ +-- 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-core +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. + . + This package implements the internal commands of ogma. + +data-files: templates/copilot-cfs/CMakeLists.txt + templates/copilot-cfs/fsw/for_build/Makefile + templates/copilot-cfs/fsw/mission_inc/copilot_cfs_perfids.h + templates/copilot-cfs/fsw/platform_inc/copilot_cfs_msgids.h + templates/copilot-cfs/fsw/src/Properties.hs + templates/copilot-cfs/fsw/src/copilot_cfs_msg.h + templates/copilot-cfs/fsw/src/copilot_cfs.c + templates/copilot-cfs/fsw/src/copilot_cfs_version.h + templates/copilot-cfs/fsw/src/copilot_cfs.h + templates/copilot-cfs/fsw/src/copilot_cfs_events.h + +library + + exposed-modules: + Command.CFSApp + Command.CStructs2Copilot + Command.CStructs2MsgHandlers + Command.FRETComponentSpec2Copilot + Command.FRETReqsDB2Copilot + Command.Result + + Data.Location + + Language.Trans.CoCoSpec2Copilot + Language.Trans.CStruct2CopilotStruct + Language.Trans.CStructs2Copilot + Language.Trans.CStructs2MsgHandlers + Language.Trans.FRETComponentSpec2Copilot + Language.Trans.FRETReqsDB2Copilot + Language.Trans.SMV2Copilot + + other-modules: + Paths_ogma_core + + autogen-modules: + Paths_ogma_core + + build-depends: + base >= 4.11.0.0 && < 5 + , aeson >= 2.0.0.0 && < 2.2 + , filepath + , IfElse + + , ogma-extra >= 1.0.0 && < 1.1 + , ogma-language-c >= 1.0.0 && < 1.1 + , ogma-language-cocospec >= 1.0.0 && < 1.1 + , ogma-language-copilot >= 1.0.0 && < 1.1 + , ogma-language-fret-cs >= 1.0.0 && < 1.1 + , ogma-language-fret-reqs >= 1.0.0 && < 1.1 + , ogma-language-smv >= 1.0.0 && < 1.1 + + hs-source-dirs: + src + + default-language: + Haskell2010 + + ghc-options: + -Wall + +test-suite unit-tests + type: + exitcode-stdio-1.0 + + main-is: + Main.hs + + build-depends: + base + , HUnit + , QuickCheck + , test-framework + , test-framework-hunit + , test-framework-quickcheck2 + + , ogma-core + + hs-source-dirs: + tests + + default-language: + Haskell2010 + + ghc-options: + -Wall diff --git a/src/Command/CFSApp.hs b/src/Command/CFSApp.hs new file mode 100644 --- /dev/null +++ b/src/Command/CFSApp.hs @@ -0,0 +1,431 @@ +-- 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. +-- +-- | Create (CFS) +-- applications that subscribe to the communication bus and call Copilot when +-- new messages arrive. +-- +-- The applications are created ready to be extracted in the application +-- directory in CFS, and they subscribe to a generic monitor. It is the user's +-- responsibility to modify the generated Copilot and C code to deal with the +-- monitors they'd like to implement, and the data they must manipulate. + +{- HLINT ignore "Functor law" -} +module Command.CFSApp + ( cFSApp + , ErrorCode + ) + where + +-- External imports +import qualified Control.Exception as E +import Data.List ( find ) +import System.FilePath ( () ) + +-- External imports: auxiliary +import System.Directory.Extra ( copyDirectoryRecursive ) + +-- Internal imports: auxiliary +import Command.Result ( Result (..) ) +import Data.Location ( Location (..) ) + +-- Internal imports +import Paths_ogma_core ( getDataDir ) + +-- | Generate a new CFS application connected to Copilot. +cFSApp :: FilePath -- ^ Target directory where the application + -- should be created. + -> FilePath -- ^ File containing a list of variables to make + -- available to Copilot. + -> Maybe FilePath -- ^ File containing a list of known variables + -- with their types and the message IDs they + -- can be obtained from. + -> IO (Result ErrorCode) +cFSApp targetDir varNameFile varDBFile = do + + -- We first try to open the two files we need to fill in details in the CFS + -- app template. + -- + -- The variable DB is optional, so this check only fails if the filename + -- provided does not exist or if the file cannot be opened or parsed (wrong + -- format). + varDBE <- E.try $ + case varDBFile of + Nothing -> return knownVars + Just fn -> fmap read <$> lines <$> readFile fn + + case varDBE of + Left e -> return $ cannotOpenDB varDBFile e + Right varDB -> do + + -- The variable list is mandatory. This check fails if the filename + -- provided does not exist or if the file cannot be opened. The condition + -- on the result also checks that the list of variables in the file is + -- not empty (otherwise, we do not know when to call Copilot). + varNamesE <- E.try $ lines <$> readFile varNameFile + + case varNamesE of + Left e -> return $ cannotOpenVarFile varNameFile e + Right [] -> return $ cannotEmptyVarList varNameFile + Right varNames -> do + + -- Obtain template dir + dataDir <- getDataDir + let templateDir = dataDir "templates" "copilot-cfs" + + E.handle (return . cannotCopyTemplate) $ do + -- Expand template + copyDirectoryRecursive templateDir targetDir + + let f n o@(oVars, oIds, oInfos, oDatas) = + case variableMap varDB n of + Nothing -> o + Just (vars, ids, infos, datas) -> + (vars : oVars, ids : oIds, infos : oInfos, datas : oDatas) + + -- This is a Data.List.unzip4 + let (vars, ids, infos, datas) = foldr f ([], [], [], []) varNames + + let cfsFileName = targetDir "fsw" "src" "copilot_cfs.c" + cfsFileContents = unlines $ fileContents vars ids infos datas + + writeFile cfsFileName cfsFileContents + return Success + +-- | Predefined list of Icarous variables that are known to Ogma +knownVars :: [(String, String, String, String)] +knownVars = + [ ("position", "position_t", "ICAROUS_POSITION_MID", "IcarousPosition") ] + +-- | Return the variable information needed to generate declarations +-- and subscriptions for a given variable name and variable database. +variableMap :: [(String, String, String, String)] + -> String + -> Maybe (VarDecl, MsgInfoId, MsgInfo, MsgData) +variableMap varDB varName = + csvToVarMap <$> find (sameName varName) varDB + + where + + -- True if the given variable and db entry have the same name + sameName :: String + -> (String, String, String, String) + -> Bool + sameName n (vn, _, _, _) = n == vn + + -- Convert a DB row into Variable info needed to generate the CFS file + csvToVarMap :: (String, String, String, String) + -> (VarDecl, String, MsgInfo, MsgData) + csvToVarMap (nm, ty, mid, mn) = + (VarDecl nm ty, mid, MsgInfo mid mn, MsgData mn nm ty) + +-- | The declaration of a variable in C, with a given type and name. +data VarDecl = VarDecl + { varDeclName :: String + , varDeclType :: String + } + +-- | The message ID to subscribe to. +type MsgInfoId = String + +-- | A message ID to subscribe to and the name associated to it. The name is +-- used to generate a suitable name for the message handler. +data MsgInfo = MsgInfo + { msgInfoId :: MsgInfoId + , msgInfoDesc :: String + } + +-- | Information on the data provided by a message with a given description, +-- and the type of the data it carries. +data MsgData = MsgData + { msgDataDesc :: String + , msgDataVarName :: String + , msgDataVarType :: String + } + +-- | Return the contents of the main CFS application. +fileContents :: [VarDecl] -> [MsgInfoId] -> [MsgInfo] -> [MsgData] -> [String] +fileContents variables msgIds msgNames msgDatas = cfsFileContents + where + variablesS = unlines $ map toVarDecl variables + toVarDecl varDecl = varDeclType varDecl ++ " " ++ varDeclName varDecl ++ ";" + + msgSubscriptionS = unlines $ map toMsgSubscription msgIds + toMsgSubscription nm = + " CFE_SB_Subscribe(" ++ nm ++ ", COPILOT_CommandPipe);" + + msgCasesS = unlines $ map toMsgCase msgNames + toMsgCase msgInfo = unlines + [ " case " ++ msgInfoId msgInfo ++ ":" + , " COPILOT_Process" ++ msgInfoDesc msgInfo ++ "();" + , " break;" + ] + + msgHandlerS = unlines $ map toMsgHandler msgDatas + toMsgHandler msgData = + unlines [ "/**" + , "* Make ICAROUS data available to Copilot and run monitors." + , "*/" + , "void COPILOT_Process" ++ msgDataDesc msgData ++ "(void)" + , "{" + , " " ++ msgDataVarType msgData ++ "* msg;" + , " msg = (" ++ msgDataVarType msgData ++ "*) COPILOTMsgPtr;" + , " " ++ msgDataVarName msgData ++ " = *msg;" + , "" + , " // Run all copilot monitors." + , " step();" + , "}" + ] + + cfsFileContents = + [ "/********************************************************************" + , "** File: copilot_cfs.c" + , "**" + , "** Purpose:" + , "** This file contains the source code for the Sample App." + , "**" + , "*********************************************************************/" + , "" + , "/*" + , "** Include Files:" + , "*/" + , "" + , "#include \"copilot_cfs.h\"" + , "#include \"copilot_cfs_perfids.h\"" + , "#include \"copilot_cfs_msgids.h\"" + , "#include \"copilot_cfs_msg.h\"" + , "#include \"copilot_cfs_events.h\"" + , "#include \"copilot_cfs_version.h\"" + , "#include \"Icarous_msgids.h\"" + , "#include \"Icarous_msg.h\"" + , "" + , variablesS + , "void split(void);" + , "void step(void);" + , "" + , "/*" + , "** global data" + , "*/" + , "" + , "copilot_hk_tlm_t COPILOT_HkTelemetryPkt;" + , "CFE_SB_PipeId_t COPILOT_CommandPipe;" + , "CFE_SB_MsgPtr_t COPILOTMsgPtr;" + , "" + , "static CFE_EVS_BinFilter_t COPILOT_EventFilters[] =" + , " { /* Event ID mask */" + , " {COPILOT_STARTUP_INF_EID, 0x0000}," + , " {COPILOT_COMMAND_ERR_EID, 0x0000}," + , " {COPILOT_COMMANDCPVIOL_INF_EID, 0x0000}," + , " };" + , "" + , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" + , "/* COPILOT_AppMain() -- App entry point and main process loop */" + , "/* */" + , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" + , "void COPILOT_AppMain( void )" + , "{" + , " int32 status;" + , " uint32 RunStatus = CFE_ES_APP_RUN;" + , "" + , " CFE_ES_PerfLogEntry(COPILOT_CFS_PERF_ID);" + , "" + , " COPILOT_AppInit();" + , "" + , " /*" + , " ** COPILOT Runloop" + , " */" + , " while (CFE_ES_RunLoop(&RunStatus) == TRUE)" + , " {" + , " CFE_ES_PerfLogExit(COPILOT_CFS_PERF_ID);" + , "" + , " // Pend on receipt of command packet" + , " // (timeout set to 500 millisecs)" + , " status = CFE_SB_RcvMsg (&COPILOTMsgPtr," + , " COPILOT_CommandPipe," + , " 500);" + , " " + , " CFE_ES_PerfLogEntry(COPILOT_CFS_PERF_ID);" + , "" + , " if (status == CFE_SUCCESS)" + , " {" + , " COPILOT_ProcessCommandPacket();" + , " }" + , "" + , " }" + , "" + , " CFE_ES_ExitApp(RunStatus);" + , "" + , "} /* End of COPILOT_AppMain() */" + , "" + , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" + , "/* */" + , "/* COPILOT_AppInit() -- initialization */" + , "/* */" + , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" + , "void COPILOT_AppInit(void)" + , "{" + , " // Register the app with Executive services" + , " CFE_ES_RegisterApp();" + , "" + , " // Register the events" + , " CFE_EVS_Register(COPILOT_EventFilters," + , " sizeof(COPILOT_EventFilters) / " + ++ "sizeof(CFE_EVS_BinFilter_t)," + , " CFE_EVS_BINARY_FILTER);" + , "" + , " // Create the Software Bus command pipe and subscribe to " + , " // housekeeping messages" + , " CFE_SB_CreatePipe(&COPILOT_CommandPipe, COPILOT_PIPE_DEPTH," + ++ "\"COPILOT_CMD_PIPE\");" + , msgSubscriptionS + , "" + , " CFE_EVS_SendEvent (COPILOT_STARTUP_INF_EID," + , " CFE_EVS_INFORMATION," + , " \"COPILOT App Initialized. Ver %d.%d.%d.%d\"," + , " COPILOT_CFS_MAJOR_VERSION," + , " COPILOT_CFS_MINOR_VERSION, " + , " COPILOT_CFS_REVISION, " + , " COPILOT_CFS_MISSION_REV);" + , "" + , "} /* End of COPILOT_AppInit() */" + , "" + , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" + , "/* Name: COPILOT_ProcessCommandPacket */" + , "/* */" + , "/* Purpose: */" + , "/* This routine will process any packet that is received */" + , "/* on the COPILOT command pipe. */" + , "/* */" + , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" + , "void COPILOT_ProcessCommandPacket(void)" + , "{" + , " CFE_SB_MsgId_t MsgId;" + , "" + , " MsgId = CFE_SB_GetMsgId(COPILOTMsgPtr);" + , "" + , " switch (MsgId)" + , " {" + , msgCasesS + , " default:" + , " COPILOT_HkTelemetryPkt.copilot_command_error_count++;" + , " CFE_EVS_SendEvent(COPILOT_COMMAND_ERR_EID,CFE_EVS_ERROR," + , " " + ++ "\"COPILOT: invalid command packet,MID = 0x%x\"," + , " MsgId);" + , " break;" + , " }" + , "" + , " return;" + , "" + , "} /* End COPILOT_ProcessCommandPacket */" + , "" + , msgHandlerS + , "" + , "/**" + , " * Report copilot property violations." + , " */" + , "void split(void) {" + , " CFE_EVS_SendEvent(COPILOT_COMMANDCPVIOL_INF_EID, CFE_EVS_ERROR," + , " \"COPILOT: violation\");" + , "}" + ] + +-- * Exception handlers + +-- | Exception handler to deal with the case in which the variable DB cannot be +-- opened. +cannotOpenDB :: Maybe FilePath -> E.SomeException -> Result ErrorCode +cannotOpenDB Nothing _e = + Error ecCannotOpenDBCritical msg LocationNothing + where + msg = + "cannotOpenDB: this is a bug. Please notify the developers" +cannotOpenDB (Just file) _e = + Error ecCannotOpenDBUser msg (LocationFile file) + where + msg = + "cannot open variable DB file " ++ file + +-- | Exception handler to deal with the case in which the variable file +-- provided by the user cannot be opened. +cannotOpenVarFile :: FilePath -> E.SomeException -> Result ErrorCode +cannotOpenVarFile file _e = + Error ecCannotOpenVarFile msg (LocationFile file) + where + msg = + "cannot open variable list file " ++ file + +-- | Exception handler to deal with the case of the variable file provided +-- containing an empty list. +cannotEmptyVarList :: FilePath -> Result ErrorCode +cannotEmptyVarList file = + Error ecCannotEmptyVarList msg (LocationFile file) + where + msg = + "variable list in file " ++ file ++ " is empty" + +-- | Exception handler to deal with the case of files that cannot be +-- copied/generated due lack of space or permissions or some I/O error. +cannotCopyTemplate :: E.SomeException -> Result ErrorCode +cannotCopyTemplate _e = + Error ecCannotCopyTemplate msg LocationNothing + where + msg = + "CFS app generation failed during copy/write operation. Check that" + ++ " there's free space in the disk and that you have the necessary" + ++ " permissions to write in the destination directory." + +-- * Error codes + +-- | Encoding of reasons why the command can fail. +-- +-- The error codes used are 1 for user error, and 2 for internal bug. +type ErrorCode = Int + +-- | Internal error: Variable DB cannot be opened. +ecCannotOpenDBCritical :: ErrorCode +ecCannotOpenDBCritical = 2 + +-- | Error: the variable DB provided by the user cannot be opened. +ecCannotOpenDBUser :: ErrorCode +ecCannotOpenDBUser = 1 + +-- | Error: the variable file provided by the user cannot be opened. +ecCannotOpenVarFile :: ErrorCode +ecCannotOpenVarFile = 1 + +-- | Error: the variable file provided contains an empty list. +ecCannotEmptyVarList :: ErrorCode +ecCannotEmptyVarList = 1 + +-- | Error: the files cannot be copied/generated due lack of space or +-- permissions or some I/O error. +ecCannotCopyTemplate :: ErrorCode +ecCannotCopyTemplate = 1 diff --git a/src/Command/CStructs2Copilot.hs b/src/Command/CStructs2Copilot.hs new file mode 100644 --- /dev/null +++ b/src/Command/CStructs2Copilot.hs @@ -0,0 +1,98 @@ +-- 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. +-- +-- | Generate Copilot struct definitions and instances from structs defined in +-- a C header file. +-- +-- Working with Copilot structs requires three definitions: the datatype, a +-- @Struct@ instance, and a @Typed@ instance. +-- +-- This module converts the C structs into 'Language.Copilot.CStruct.CStruct's, +-- and then converts those 'Language.Copilot.CStruct.CStruct's into Copilot +-- (i.e., Haskell) data type declarations and instance declarations. The result +-- is then printed to a file. This module makes use of +-- "Language.Trans.CStructs2Copilot", which does most of the work. +module Command.CStructs2Copilot + ( cstructs2Copilot + , ErrorCode + ) + where + +-- External imports: auxiliary +import Data.String.Extra as S ( safeReadFile ) + +-- Internal imports: auxiliary +import Command.Result ( Result (..) ) +import Data.Location ( Location (..) ) + +-- Internal imports: C parsing and AST +import qualified Language.C.AbsC as C ( TranslationUnit ) +import qualified Language.C.ParC as C ( myLexer, pTranslationUnit ) + +-- Internal imports: transformation of C structs to Copilot structs +import Language.Trans.CStructs2Copilot ( cstructs2CopilotDecls ) + +-- | Generate Copilot struct definitions and instances from structs defined in +-- a C header file. +cstructs2Copilot :: FilePath -- ^ Path to a readable, valid C header file + -- containing struct definitions. + -> IO (Result ErrorCode) +cstructs2Copilot fp = do + source <- parseCFile fp + + case cstructs2CopilotDecls =<< source of + Right decls -> printDecls decls >> return Success + Left msg -> return $ Error ecCStructError msg (LocationFile fp) + + where + + -- Parse a C file, returning 'Left' with some message when there is a parse + -- error. + -- + parseCFile :: FilePath -> IO (Either String C.TranslationUnit) + parseCFile fp' = do + content <- S.safeReadFile fp' + return $ C.pTranslationUnit . C.myLexer =<< content + + -- Print several Haskell declarations to standard output. + printDecls :: [ String ] -> IO () + printDecls = putStrLn . unlines + +-- * Error codes + +-- | Encoding of reasons why the command can fail. +-- +-- The error code used is 1 for user error. +type ErrorCode = Int + +-- | Error: the C header file cannot be read due to the file being unreadable +-- or the format being incorrect. +ecCStructError :: ErrorCode +ecCStructError = 1 diff --git a/src/Command/CStructs2MsgHandlers.hs b/src/Command/CStructs2MsgHandlers.hs new file mode 100644 --- /dev/null +++ b/src/Command/CStructs2MsgHandlers.hs @@ -0,0 +1,88 @@ +-- 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. +-- +-- | Generate C methods that process NASA Core Flight System messages dealing +-- with the structs defined in a header file. +-- +-- This module makes use of "Language.Trans.CStructs2MsgHandlers", which does +-- most of the work. +module Command.CStructs2MsgHandlers + ( cstructs2MsgHandlers + , ErrorCode + ) + where + +-- External imports: auxiliary +import Data.String.Extra as S ( safeReadFile ) + +-- Internal imports: auxiliary +import Command.Result ( Result (..) ) +import Data.Location ( Location (..) ) + +-- Internal imports: C parsing and AST +import qualified Language.C.AbsC as C ( TranslationUnit ) +import qualified Language.C.ParC as C ( myLexer, pTranslationUnit ) + +-- Internal imports: transformation of C structs to handling methods. +import qualified Language.Trans.CStructs2MsgHandlers as T ( cstructs2MsgHandlers ) + +-- | Print message handlers that copy data and make it available to Copilot. +cstructs2MsgHandlers :: FilePath -- ^ Path to a readable, valid C header file + -- containing struct definitions. + -> IO (Result ErrorCode) +cstructs2MsgHandlers fp = do + result <- parseCFile fp + + case T.cstructs2MsgHandlers =<< result of + Right content -> putStrLn content >> return Success + + Left msg -> return $ Error ecCStructError msg (LocationFile fp) + + where + + -- Parse a C file, returning 'Left' with some message when there is a parse + -- error. + -- + parseCFile :: FilePath -> IO (Either String C.TranslationUnit) + parseCFile fp' = do + content <- S.safeReadFile fp' + return $ C.pTranslationUnit . C.myLexer =<< content + +-- * Error codes + +-- | Encoding of reasons why the command can fail. +-- +-- The error code used is 1 for user error. +type ErrorCode = Int + +-- | Error: the C header file cannot be read due to the file being unreadable +-- or the format being incorrect. +ecCStructError :: ErrorCode +ecCStructError = 1 diff --git a/src/Command/FRETComponentSpec2Copilot.hs b/src/Command/FRETComponentSpec2Copilot.hs new file mode 100644 --- /dev/null +++ b/src/Command/FRETComponentSpec2Copilot.hs @@ -0,0 +1,143 @@ +-- 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. +-- +-- | Transform a FRET component specification into a Copilot specification. +-- +-- This module makes use of +-- "Language.Trans.FRETComponentSpec2Copilot", which does most of the work. +module Command.FRETComponentSpec2Copilot + ( fretComponentSpec2Copilot + , FRETComponentSpec2CopilotOptions(..) + , ErrorCode + ) + where + +-- External imports +import Control.Monad.IfElse ( awhen ) +import Data.Aeson ( eitherDecode ) + +-- External imports: auxiliary +import Data.ByteString.Extra as B ( safeReadFile ) + +-- Internal imports: auxiliary +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) + ) + +-- | Print the contents of a Copilot module that implements the Past-time TL +-- formula in a FRET file. +-- +-- 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 -- ^ Path to a file containing a FRET + -- Component Specification + -> FRETComponentSpec2CopilotOptions + -- ^ Customization options + -- formula + -> 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 copilot = T.fretComponentSpec2Copilot internalOptions =<< fret + + let (mOutput, result) = + fretComponentSpec2CopilotResult options fp copilot + + awhen mOutput putStrLn + return result + +-- | Options used to customize the conversion of FRET Component Specifications +-- to Copilot code. +data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions + { fretCS2CopilotUseCoCoSpec :: Bool + , fretCS2CopilotIntType :: String + , fretCS2CopilotRealType :: 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. +-- +-- The error code used is 1 for user error. +type ErrorCode = Int + +-- | Error: the FRET Component Spec file cannot be read due to the file being +-- unreadable or the format being incorrect. +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) + +-- * Result + +-- | Process the result of the transformation function. +fretComponentSpec2CopilotResult :: FRETComponentSpec2CopilotOptions + -> FilePath + -> Either String String + -> (Maybe String, Result ErrorCode) +fretComponentSpec2CopilotResult options fp result = case result of + Left msg -> (Nothing, Error ecFretCSError msg (LocationFile fp)) + Right t -> (Just t, Success) diff --git a/src/Command/FRETReqsDB2Copilot.hs b/src/Command/FRETReqsDB2Copilot.hs new file mode 100644 --- /dev/null +++ b/src/Command/FRETReqsDB2Copilot.hs @@ -0,0 +1,140 @@ +-- 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. +-- +-- | Transform a FRET requirements database containing a temporal logic +-- specification into a Copilot specification. +-- +-- This module makes use of +-- "Language.Trans.FRETReqsDB2Copilot", which does most of the work. +module Command.FRETReqsDB2Copilot + ( fretReqsDB2Copilot + , FRETReqsDB2CopilotOptions(..) + , ErrorCode + ) + where + +-- External imports +import Control.Monad.IfElse ( awhen ) +import Data.Aeson ( eitherDecode ) + +-- External imports: auxiliary +import Data.ByteString.Extra as B ( safeReadFile ) +import Data.List.Extra ( headEither ) + +-- Internal imports: auxiliary +import Command.Result ( Result (..) ) +import Data.Location ( Location (..) ) + +-- Internal imports: FRET files and conversion to Copilot +import qualified Language.FRETReqsDB.AST as FRET ( FRETReqsDB ) +import qualified Language.Trans.FRETReqsDB2Copilot as T + ( fret2CopilotModule + , FRETReqsDB2CopilotOptions(FRETReqsDB2CopilotOptions) + ) + +-- | Print the contents of a Copilot module that implements the Past-time TL +-- formula in a FRET file. +-- +-- 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. +fretReqsDB2Copilot :: FilePath -- ^ Path to a file containing a FRET + -- Requirements Database + -> FRETReqsDB2CopilotOptions + -- ^ Customization options formula + -> IO (Result ErrorCode) +fretReqsDB2Copilot fp useCoCoSpec = 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 <- parseFret fp + + -- Extract internal command options from external command options + let internalOptions = fretReqsDB2CopilotOptions useCoCoSpec + + let copilot = T.fret2CopilotModule internalOptions =<< headEither =<< fret + + let (mOutput, result) = + fretReqsDB2CopilotResult useCoCoSpec fp copilot + + awhen mOutput putStrLn + return result + +-- | Options used to customize the conversion of FRET Requirements Database +-- to Copilot code. +data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions + { fretReqsDB2CopilotUseCoCoSpec :: Bool + } + +-- | Parse a JSON file containing a FRET requirement database. +-- +-- 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. +parseFret :: FilePath -> IO (Either String [FRET.FRETReqsDB]) +parseFret fp = do + content <- B.safeReadFile fp + return $ eitherDecode =<< content + +-- * Error codes + +-- | Encoding of reasons why the command can fail. +-- +-- The error code used is 1 for user error. +type ErrorCode = Int + +-- | Error: the FRET Requirements DB file cannot be read due to the file being +-- unreadable or the format being incorrect. +ecFretReqsDBError :: ErrorCode +ecFretReqsDBError = 1 + +-- * Input arguments + +-- | Convert command input argument options to internal transformation function +-- input arguments. +fretReqsDB2CopilotOptions :: FRETReqsDB2CopilotOptions + -> T.FRETReqsDB2CopilotOptions +fretReqsDB2CopilotOptions options = + T.FRETReqsDB2CopilotOptions + (fretReqsDB2CopilotUseCoCoSpec options) + +-- * Result + +-- | Process the result of the transformation function. +fretReqsDB2CopilotResult :: FRETReqsDB2CopilotOptions + -> FilePath + -> Either String String + -> (Maybe String, Result ErrorCode) +fretReqsDB2CopilotResult options fp result = case result of + Left msg -> (Nothing, Error ecFretReqsDBError msg (LocationFile fp)) + Right t -> (Just t, Success) diff --git a/src/Command/Result.hs b/src/Command/Result.hs new file mode 100644 --- /dev/null +++ b/src/Command/Result.hs @@ -0,0 +1,53 @@ +-- 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. +-- +-- | A datatype representing the type of the results of processing input files. +module Command.Result + ( Result (Success, Error) + , isSuccess + , isError + ) + where + +-- Internal imports +import Data.Location ( Location ) + +-- | Result of the global process +data Result a = Success + | Error a String Location + +-- | 'True' if the result is a success, 'False' otherwise. +isSuccess :: Result a -> Bool +isSuccess Success = True +isSuccess _ = False + +-- | 'True' if the result is an error, 'False' otherwise. +isError :: Result a -> Bool +isError = not . isSuccess diff --git a/src/Data/Location.hs b/src/Data/Location.hs new file mode 100644 --- /dev/null +++ b/src/Data/Location.hs @@ -0,0 +1,42 @@ +-- 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. +-- +-- | Locations where conditions take place (within a file, or outside). +module Data.Location + ( Location(..) + ) + where + +-- | Locations where conditions take place (within a file, or outside). +data Location = LocationNothing -- ^ No location info. + | LocationFile String -- ^ Within a file. + | LocationFileLine String Int -- ^ On a line within a file. + | LocationFileLC String Int Int -- ^ On a line and column + -- within a file. diff --git a/src/Language/Trans/CStruct2CopilotStruct.hs b/src/Language/Trans/CStruct2CopilotStruct.hs new file mode 100644 --- /dev/null +++ b/src/Language/Trans/CStruct2CopilotStruct.hs @@ -0,0 +1,166 @@ +-- 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. +-- +-- | Copilot's struct representation of C Structs and creation from C's AST. +module Language.Trans.CStruct2CopilotStruct + ( + -- * Constructors + mkCStruct + + -- * Convert C type names to valid Copilot names + , camelCaseTypeName + ) + where + +-- External imports +import Data.Char ( toUpper ) + +-- External imports: Copilot C Struct representation +import Language.Copilot.CStruct ( CField (CArray, CPlain), CStruct(..) ) + +-- Internal imports +import qualified Language.C.AbsC as C + +-- | Convert a top-level struct declaration into a CStruct +mkCStruct :: C.ExternalDeclaration -> Either String CStruct +mkCStruct (C.MkExternalDeclarationFunctionDefinition _) = Left "C files must contain struct definitions only." +mkCStruct (C.MkExternalDeclarationDeclaration (C.MkDeclaration specifiers initDecl)) = + case specifiers of + C.DeclarationSpecifiers (C.MkDeclarationSpecifierStorageClass C.MkStorageClassSpecifierTypedef) s -> + let [C.MkDeclarationSpecifierTypeSpecifier (C.MkTypeSpecifierStructOrUnion (C.MkStructOrUnionSpecifierWithFields C.MkStructOrUnionStruct _structName u))] = s + (C.MkInitDeclarationListOptJust [C.MkInitDeclaratorUninitialized (C.MkDeclarator C.MkPointerOptNothing (C.MkDirectDeclaratorIdentifier (C.Identifier t)))]) = initDecl + name = Right t + fields = mapM buildCField u + in CStruct <$> name <*> fields + _ -> Left "C files must contain struct definitions only." + +-- -- | Convert a declaration within a struct into a field declaration. +buildCField :: C.StructDeclaration -> Either String CField +buildCField (C.MkStructDeclaration field name) + | fieldLength > 0 = CArray <$> fieldType <*> fieldName <*> pure fieldLength + | otherwise = CPlain <$> fieldType <*> fieldName + where + fieldType = extractFieldType (head field) + fieldName = extractFieldName (head name) + fieldLength = extractFieldLength (head name) + +-- | Extract the type of a field from a type specification. +extractFieldType :: C.SpecifierQualifier -> Either String String +extractFieldType (C.MkSpecifierQualifierTypeSpecifier t) = Right $ showTypeSpecifier t +extractFieldType (C.MkSpecifierQualifierTypeQualifier _) = Left "type qualifiers." + +-- | String representing a known type. +showTypeSpecifier :: C.TypeSpecifier -> String +showTypeSpecifier C.MkTypeSpecifierFloat = "float" +showTypeSpecifier C.MkTypeSpecifierDouble = "double" +showTypeSpecifier C.MkTypeSpecifierUInt8 = "uint8_t" +showTypeSpecifier C.MkTypeSpecifierUInt16 = "uint16_t" +showTypeSpecifier C.MkTypeSpecifierUInt32 = "uint32_t" +showTypeSpecifier C.MkTypeSpecifierUInt64 = "uint64_t" +showTypeSpecifier C.MkTypeSpecifierInt8 = "int8_t" +showTypeSpecifier C.MkTypeSpecifierInt16 = "int16_t" +showTypeSpecifier C.MkTypeSpecifierInt32 = "int32_t" +showTypeSpecifier C.MkTypeSpecifierInt64 = "int64_t" +showTypeSpecifier C.MkTypeSpecifierInt = "int" + +-- -- | Extract the name of a field from a struct declarator. +extractFieldName :: Read n => C.StructDeclarator -> Either String n +extractFieldName (C.MkStructDeclaratorDeclarator (C.MkDeclarator C.MkPointerOptNothing (C.MkDirectDeclaratorIdentifier (C.Identifier d)))) = Right $ read $ show d +extractFieldName (C.MkStructDeclaratorDeclarator + (C.MkDeclarator + C.MkPointerOptNothing + (C.MkDirectDeclaratorConstantExpressionOpt + (C.MkDirectDeclaratorIdentifier (C.Identifier i)) + _arrayLength + ) + ) + ) = Right $ read $ show i +extractFieldName _ = Left $ "only struct declarations that are IDs without a" + ++ " pointer, or plain arrays without a pointer, are" + ++ " supported." +-- +-- -- | Extract the length of an array field from a struct declarator. +extractFieldLength :: C.StructDeclarator -> Integer +extractFieldLength (C.MkStructDeclaratorDeclarator + (C.MkDeclarator + C.MkPointerOptNothing + (C.MkDirectDeclaratorConstantExpressionOpt + _varIdent + (C.MkConditionalExpressionJust + (C.MkConstantExpression + (C.Expression12 + (C.MkCastExpression1 + (C.MkUnaryExpressionPostfix + (C.MkPostfixExpression1 + (C.MkPrimaryExpressionIdentifier (C.Identifier _n)) + ) + ) + ) + ) + ) + ) + ) + ) ) = 99 +extractFieldLength (C.MkStructDeclaratorDeclarator + (C.MkDeclarator + C.MkPointerOptNothing + (C.MkDirectDeclaratorConstantExpressionOpt + _varIdent + (C.MkConditionalExpressionJust + (C.MkConstantExpression + (C.Expression12 + (C.MkCastExpression1 + (C.MkUnaryExpressionPostfix + (C.MkPostfixExpression1 + (C.MkPrimaryExpressionConstant (C.MkConstantInteger (C.IntegerConstant i)) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) = read i +extractFieldLength _ = 0 + +-- +-- | Convert a 'String' to camel case, also eliminating the @_t@ at the end if +-- present. +camelCaseTypeName :: String -> String +camelCaseTypeName [] = [] +camelCaseTypeName (x:xs) = toUpper x : camelCaseTypeName' xs + where + camelCaseTypeName' :: String -> String + camelCaseTypeName' [] = [] + camelCaseTypeName' "_t" = [] + camelCaseTypeName' ('_':y:ys) = toUpper y : camelCaseTypeName' ys + camelCaseTypeName' (y:ys) = y : camelCaseTypeName' ys diff --git a/src/Language/Trans/CStructs2Copilot.hs b/src/Language/Trans/CStructs2Copilot.hs new file mode 100644 --- /dev/null +++ b/src/Language/Trans/CStructs2Copilot.hs @@ -0,0 +1,267 @@ +-- 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. +-- +-- | Generate Copilot struct definitions and instances from structs defined in +-- a C header file. +-- +-- Working with Copilot structs requires three definitions: the datatype, +-- a @Struct@ instance, and a @Typed@ instance. +-- +-- This module converts the C structs into 'CStruct's, and then converts +-- those 'CStruct's into Copilot (i.e., Haskell) data type declarations and +-- instance declarations represented as strings. +module Language.Trans.CStructs2Copilot where + +-- External imports +import Data.Char ( isUpper, toLower ) +import Data.List ( intercalate ) + +-- External imports: auxiliary +import Data.List.Extra ( toHead, toTail ) + +-- Internal imports: C AST +import qualified Language.C.AbsC as C +import Language.Copilot.CStruct ( CField (CArray, CPlain), + CStruct (..) ) + +-- Internal imports: Copilot's representation of C structs +import Language.Trans.CStruct2CopilotStruct ( camelCaseTypeName, mkCStruct ) + +-- | Convert all the 'CStruct's in a header file into the declarations needed +-- in Copilot to use it. +cstructs2CopilotDecls :: C.TranslationUnit -> Either String [ String ] +cstructs2CopilotDecls (C.MkTranslationUnit gs) = + concat <$> mapM (fmap cstruct2CopilotDecls . mkCStruct) gs + +-- | Convert a 'CStruct' into the declarations needed in Copilot to use it. +cstruct2CopilotDecls :: CStruct -> [ String ] +cstruct2CopilotDecls cstruct = [ cStructToCopilotStruct cstruct + , structInstance cstruct + , typedInstance cstruct + ] + +-- ** Individual conversions + +-- | Convert a 'CStruct' definition into a Copilot Struct declaration. +-- +-- For example, given the struct generated by the following definition: +-- +-- @ +-- struct { +-- uint8_t f1; +-- } a_struct_t; +-- @ +-- +-- the corresponding Haskell definition would be: +-- +-- @ +-- data AStruct = AStruct +-- { aSF1 :: Word8 } +-- @ +cStructToCopilotStruct :: CStruct -> String +cStructToCopilotStruct cstruct = + "data " + ++ datatype + ++ " = " + ++ constructor + where + + -- The name of the type (e.g., @AStruct@). + datatype = cStructName2Haskell (cStructName cstruct) + + -- The name of the constructor (e.g., @AStruct@). + constructor = cStructName2Haskell (cStructName cstruct) ++ "\n" ++ fields + + -- The fields in the struct (e.g., @aSF1 :: Word 8@), formated as record + -- fields: separated by commas, enclosed in curly brackets, and indented. + fields = unlines $ map (" " ++) + $ (++ ["}"]) + $ toTail (", " ++) + $ toHead ("{ " ++) + $ map (toField cstruct) (cStructFields cstruct) + + -- Convert a 'CStruct' field into a Copilot record field declaration. + -- + -- The second case (@CArray@) uses depedent types to promote the length of + -- the array to type level. + toField :: CStruct -> CField -> String + toField cstruct' (CPlain t n) = name ++ " :: " ++ ty + where + name = fieldName cstruct' n + ty = "Field" ++ " " ++ show n + ++ " " ++ cTypeName2HaskellType t + + toField cstruct' (CArray t n l) = name ++ " :: " ++ ty + where + name = fieldName cstruct' n + ty = "Field" ++ " " ++ show n + ++ " (" ++ "Array" + ++ " " ++ show l + ++ " " ++ cTypeName2HaskellType t + ++ ")" + +-- | Convert a 'CStruct' definition into a Copilot @Struct@ instance +-- declaration. For example, for the struct: +-- +-- @ +-- struct { +-- uint8_t f1; +-- } a_struct_t; +-- @ +-- +-- the corresponding @Struct@ instance would be: +-- +-- @ +-- instance Struct AStruct where +-- typename _ = "a_struct_t" +-- toValues v = [Value Word8 (aSF1 v)] +-- @ +structInstance :: CStruct -> String +structInstance cstruct = + "instance " ++ instanceHead ++ " where\n" ++ + unlines (map (" " ++ ) instanceBody) + where + instanceHead = "Struct" ++ " " ++ instanceName + instanceName = cStructName2Haskell $ cStructName cstruct + + instanceBody = [ instanceTypename, instanceToValues ] + + instanceTypename = "typename" ++ " " ++ "_" ++ " = " ++ show (cStructName cstruct) + + instanceToValues = + "toValues" ++ " " ++ "v" ++ " = " ++ "[ " ++ intercalate ", " valueDecls ++ " ]" + + valueDecls = map (toValueDecl cstruct) (cStructFields cstruct) + + toValueDecl :: CStruct -> CField -> String + toValueDecl c (CPlain t n) = + "Value" ++ " " ++ cTypeName2HaskellType t + ++ " (" ++ fieldName c n + ++ " " ++ "v" ++ ")" + + toValueDecl c (CArray t n _len) = + "Value" ++ " (" ++ "Array" + ++ " " ++ cTypeName2HaskellType t ++ ")" + ++ " " ++ "(" ++ fieldName c n + ++ " " ++ "v" ++ ")" + +-- | Convert a 'CStruct' definition to Copilot @Typed@ instance declaration. +-- For example, for the struct: +-- +-- @ +-- struct { +-- uint8_t f1; +-- } a_struct_t; +-- @ +-- +-- the corresponding @Typed@ instance could be: +-- +-- @ +-- instance Typed AStruct where +-- typeOf = Struct (Field 0) +-- @ +typedInstance :: CStruct -> String +typedInstance cstruct = + "instance " ++ instanceHead ++ " where\n" ++ + unlines (map (" " ++ ) instanceBody) + where + instanceHead = "Typed" ++ " " ++ instanceName + instanceName = cStructName2Haskell $ cStructName cstruct + + instanceBody = [ instanceTypeOf ] + + instanceTypeOf = "typeOf" ++ " = " ++ "Struct" ++ " " + ++ "(" ++ dataConstructorName ++ " " ++ unwords vs ++ ")" + + dataConstructorName = cStructName2Haskell $ cStructName cstruct + + vs = map ((\x -> "(" ++ "Field" ++ " " ++ x ++ ")") . defaultValue) + (cStructFields cstruct) + +-- * Auxiliary functions + +-- | Provide a suitable field name for a record field of a 'CStruct' in Haskell. +-- +-- For example, given the struct: +-- +-- @ +-- struct { +-- uint8_t f1; +-- } a_struct_t; +-- @ +-- +-- the field name in the Haskell record would be @aSF1@, where the @aS@ and +-- comes from @a_struct_t@ and the final @F1@ comes from @f1@. +fieldName :: CStruct -> String -> String +fieldName cstruct n = + summary (cStructName2Haskell (cStructName cstruct)) ++ cStructName2Haskell n + where + summary :: String -> String + summary = map toLower . filter isUpper + +-- | Convert a C struct name (e.g., @some_type_t@) to a Haskell type name +-- (e.g., @SomeType@). +cStructName2Haskell :: String -> String +cStructName2Haskell = camelCaseTypeName + +-- | Return the corresponding type in Copilot/Haskell for a given type. +cTypeName2HaskellType :: String -> String +cTypeName2HaskellType "float" = "Float" +cTypeName2HaskellType "double" = "Double" +cTypeName2HaskellType "int" = "Int" +cTypeName2HaskellType "uint8_t" = "Word8" +cTypeName2HaskellType "uint16_t" = "Word16" +cTypeName2HaskellType "uint32_t" = "Word32" +cTypeName2HaskellType "uint64_t" = "Word64" +cTypeName2HaskellType "int8_t" = "Int8" +cTypeName2HaskellType "int16_t" = "Int16" +cTypeName2HaskellType "int32_t" = "Int32" +cTypeName2HaskellType "int64_t" = "Int64" +cTypeName2HaskellType "bool" = "Bool" +cTypeName2HaskellType t = camelCaseTypeName t + +-- | Create a default value in Copilot for a field of a given type. +defaultValue :: CField -> String +defaultValue CArray {} = "(array [])" +defaultValue (CPlain t _) = defaultValueOfType t + where + defaultValueOfType "float" = "0" + defaultValueOfType "double" = "0" + defaultValueOfType "int" = "0" + defaultValueOfType "uint8_t" = "0" + defaultValueOfType "uint16_t" = "0" + defaultValueOfType "uint32_t" = "0" + defaultValueOfType "uint64_t" = "0" + defaultValueOfType "int8_t" = "0" + defaultValueOfType "int16_t" = "0" + defaultValueOfType "int32_t" = "0" + defaultValueOfType "int64_t" = "0" + defaultValueOfType "bool" = "True" + defaultValueOfType _t = "0" diff --git a/src/Language/Trans/CStructs2MsgHandlers.hs b/src/Language/Trans/CStructs2MsgHandlers.hs new file mode 100644 --- /dev/null +++ b/src/Language/Trans/CStructs2MsgHandlers.hs @@ -0,0 +1,76 @@ +-- 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. +-- +-- | Generate C methods that process message dealing with the structs +-- defined in a header file. +-- +-- This module contains the pure conversion from CStructs into C code. +-- Normally, this module would be implemented as a conversion between C ASTs, +-- but we want to add comments to the generated code, which are not +-- representable in the abstract syntax tree. +module Language.Trans.CStructs2MsgHandlers where + +-- Internal imports: C AST representation. +import qualified Language.C.AbsC as C ( TranslationUnit (MkTranslationUnit) ) + +-- Internal imports: Copilot's own CStruct representation. +import Language.Copilot.CStruct ( CStruct (cStructName) ) + +import Language.Trans.CStruct2CopilotStruct ( camelCaseTypeName, mkCStruct ) + +-- | Generate a C methods that process message dealing with the structs +-- defined in a header file. +cstructs2MsgHandlers :: C.TranslationUnit -> Either String String +cstructs2MsgHandlers (C.MkTranslationUnit gs) = + unlines <$> mapM (fmap cstruct2MsgHandler . mkCStruct) gs + +-- | Generate a C method that processes one message dealing with one +-- kind of struct. +cstruct2MsgHandler :: CStruct -> String +cstruct2MsgHandler cstruct = unlines + [ nameCStruct ++ " " ++ nameLocalVar ++ ";" + , "" + , "/**" + , "* Make ICAROUS data available to Copilot and run monitors." + , "*/" + , "void COPILOT_Process" ++ nameVar ++ "Monitor(void)" + , "{" + , " " ++ nameCStruct ++ "* msg;" + , " msg = (" ++ nameCStruct ++ "*) COPILOTMsgPtr;" + , " " ++ nameLocalVar ++ " = *msg;" + , "" + , " // Run all copilot monitors." + , " step();" + , "}" + ] + where + nameCStruct = cStructName cstruct + nameVar = camelCaseTypeName nameCStruct + nameLocalVar = 'm' : 'y' : camelCaseTypeName nameCStruct diff --git a/src/Language/Trans/CoCoSpec2Copilot.hs b/src/Language/Trans/CoCoSpec2Copilot.hs new file mode 100644 --- /dev/null +++ b/src/Language/Trans/CoCoSpec2Copilot.hs @@ -0,0 +1,199 @@ +-- 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. +-- +-- | Transform a CoCoSpec TL 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.CoCoSpec2Copilot (boolSpec2Copilot, boolSpecNames) where + +-- Internal imports +import Language.CoCoSpec.AbsCoCoSpec ( BoolConst (..), BoolNumOp (..), + BoolSpec (..), Ident (..), NumExpr (..), + NumOp2In (..), Op1Pre (..), Op2In (..), + Op2Pre (..) ) + +-- | Return the Copilot representation of a CoCoSpec 'BoolSpec'. +-- +-- This function returns the temporal property only. The string does not +-- contain any top-level names, any imports, or auxiliary definitions that +-- may be required. +boolSpec2Copilot :: BoolSpec -> String +boolSpec2Copilot b = case b of + BoolSpecPar bs -> "( " ++ boolSpec2Copilot bs ++ " )" + BoolSpecConstI bc -> show bc + BoolSpecConstD bc -> show bc + BoolSpecConstB bc -> const2Copilot bc + BoolSpecSignal i -> ident2Copilot i + BoolSpecOp1Pre op spec -> opOnePre2Copilot op ++ " (" ++ boolSpec2Copilot spec ++ ")" + + BoolSpecOp2In spec1 Op2InPre (BoolSpecOp1Pre Op1Pre spec2) + -> "[" ++ lit2Copilot spec1 ++ "] ++ " ++ boolSpec2Copilot spec2 + + BoolSpecOp2In spec1 Op2InPre spec2 + -> "mux ftp (constant " ++ lit2Copilot spec1 ++ ") (" ++ boolSpec2Copilot spec2 ++ ")" + + BoolSpecOp2In spec1 op2 spec2 -> "(" ++ boolSpec2Copilot spec1 + ++ " " ++ opTwoIn2Copilot op2 + ++ " " ++ boolSpec2Copilot spec2 + ++ ")" + + BoolSpecOp2Pre op2 spec1 spec2 -> opTwoPre2Copilot op2 ++ " " ++ boolSpec2Copilot spec1 + ++ " " ++ boolSpec2Copilot spec2 + + BoolSpecOp2HT num1 num2 spec -> "MTL.alwaysBeen" + ++ " " ++ numExpr2Copilot num2 + ++ " " ++ numExpr2Copilot num1 + ++ " clock 1" -- clock and min time distance + ++ " " ++ boolSpec2Copilot spec + + BoolSpecOp2OT num1 num2 spec -> "MTL.eventuallyPrev" + ++ " " ++ numExpr2Copilot num2 + ++ " " ++ numExpr2Copilot num1 + ++ " clock 1" -- clock and min time distance + ++ " " ++ boolSpec2Copilot spec + + BoolSpecOp2ST num1 num2 spec1 spec2 -> "MTL.since" + ++ " " ++ numExpr2Copilot num1 + ++ " " ++ numExpr2Copilot num2 + ++ " clock 1" -- clock and min time distance + ++ " " ++ boolSpec2Copilot spec1 + ++ " " ++ boolSpec2Copilot spec2 + +-- | Return the Copilot representation of a CoCoSpec numeric +-- expression. +-- +-- This function returns the expression only. The string does not contain any +-- top-level names, any imports, or auxiliary definitions that may be required. +numExpr2Copilot :: NumExpr -> String +numExpr2Copilot expr = case expr of + NumExprNum i -> show i + NumExprPar iExpr -> "(" ++ numExpr2Copilot iExpr ++ ")" + NumExprOp2In iExpr1 op iExpr2 -> "(" ++ numExpr2Copilot iExpr1 ++ " " + ++ numOpTwoIn2Copilot op ++ " " + ++ numExpr2Copilot iExpr2 ++ ")" + NumExprId i -> ident2Copilot i + +-- | Return the Copilot representation of a numeric CoCoSpec arithmetic +-- operator. +numOpTwoIn2Copilot :: NumOp2In -> String +numOpTwoIn2Copilot NumOp2Plus = "+" +numOpTwoIn2Copilot NumOp2Minus = "-" +numOpTwoIn2Copilot NumOp2Mult = "*" + +-- | Return the Copilot representation of a numeric CoCoSpec comparison +-- operator. +opTwoNum2Copilot :: BoolNumOp -> String +opTwoNum2Copilot BoolNumOp2Eq = "==" +opTwoNum2Copilot BoolNumOp2Le = "<=" +opTwoNum2Copilot BoolNumOp2Lt = "<" +opTwoNum2Copilot BoolNumOp2Gt = ">=" +opTwoNum2Copilot BoolNumOp2Ge = ">" + +-- | Return the Copilot representation of a CoCoSpec boolean +-- constant. +const2Copilot :: BoolConst -> String +const2Copilot BoolConstTrue = "true" +const2Copilot BoolConstFalse = "false" +const2Copilot BoolConstFTP = "ftp" + +-- | Return the Copilot representation of a CoCoSpec logical +-- operator. +opOnePre2Copilot :: Op1Pre -> String +opOnePre2Copilot Op1Pre = "pre" +opOnePre2Copilot Op1Once = "PTLTL.eventuallyPrev" +opOnePre2Copilot Op1Hist = "PTLTL.alwaysBeen" +opOnePre2Copilot Op1Y = "PTLTL.previous" +opOnePre2Copilot Op1Not = "not" +opOnePre2Copilot Op1Bang = "not" + +-- | Return the Copilot representation of a CoCoSpec logical +-- operator. +opTwoIn2Copilot :: Op2In -> String +opTwoIn2Copilot Op2Amp = "&&" +opTwoIn2Copilot Op2And = "&&" +opTwoIn2Copilot Op2Or = "||" +opTwoIn2Copilot Op2Impl = "==>" +opTwoIn2Copilot Op2InPre = "pre" +opTwoIn2Copilot (Op2NumOp n) = numOpTwoIn2Copilot n +opTwoIn2Copilot (Op2NumCmp n) = opTwoNum2Copilot n + +-- | Return the Copilot representation of a CoCoSpec logical +-- operator. +opTwoPre2Copilot :: Op2Pre -> String +opTwoPre2Copilot Op2SI = "since" +opTwoPre2Copilot Op2OT = "ot" + +-- | Return the Copilot representation of a CoCoSpec identifier. +ident2Copilot :: Ident -> String +ident2Copilot (Ident "FTP") = "ftp" +ident2Copilot (Ident s) = s + +-- | Return all identifiers used in a BoolSpec that are not reserved keywords. +boolSpecNames :: BoolSpec -> [String] +boolSpecNames (BoolSpecPar bs) = boolSpecNames bs +boolSpecNames (BoolSpecConstI _bc) = [] +boolSpecNames (BoolSpecConstD _bc) = [] +boolSpecNames (BoolSpecConstB _bc) = [] +boolSpecNames (BoolSpecSignal (Ident i)) = [i] +boolSpecNames (BoolSpecOp1Pre _op spec) = boolSpecNames spec +boolSpecNames (BoolSpecOp2In spec1 _op2 spec2) = boolSpecNames spec1 ++ boolSpecNames spec2 +boolSpecNames (BoolSpecOp2Pre _op2 spec1 spec2) = boolSpecNames spec1 ++ boolSpecNames spec2 +boolSpecNames (BoolSpecOp2HT num1 num2 spec) = + numExprNames num1 ++ numExprNames num2 ++ boolSpecNames spec +boolSpecNames (BoolSpecOp2OT num1 num2 spec) = + numExprNames num1 ++ numExprNames num2 ++ boolSpecNames spec +boolSpecNames (BoolSpecOp2ST num1 num2 spec1 spec2) = + numExprNames num1 ++ numExprNames num2 ++ boolSpecNames spec1 ++ boolSpecNames spec2 + +-- | Return all identifiers used in a NumExpr that are not reserved keywords. +numExprNames :: NumExpr -> [String] +numExprNames (NumExprNum _i) = [] +numExprNames (NumExprPar expr) = numExprNames expr +numExprNames (NumExprOp2In expr1 _op expr2) = + numExprNames expr1 ++ numExprNames expr2 +numExprNames (NumExprId (Ident i)) = [i] + +-- | Return the Copilot representation of a CoCoSpec literal. +lit2Copilot :: BoolSpec -> String +lit2Copilot b = case b of + BoolSpecConstI bc -> show bc + BoolSpecConstD bc -> show bc + BoolSpecConstB bc -> litConst2Copilot bc + BoolSpecSignal i -> ident2Copilot i + _ -> ":error converting literal:" + where + -- | Return the Copilot representation of a CoCoSpec boolean + -- constant. + litConst2Copilot :: BoolConst -> String + litConst2Copilot BoolConstTrue = "True" + litConst2Copilot BoolConstFalse = "False" + litConst2Copilot _ = ":error converting literal boolean:" diff --git a/src/Language/Trans/FRETComponentSpec2Copilot.hs b/src/Language/Trans/FRETComponentSpec2Copilot.hs new file mode 100644 --- /dev/null +++ b/src/Language/Trans/FRETComponentSpec2Copilot.hs @@ -0,0 +1,327 @@ +-- 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 + } + +-- | 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 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] ++)" + ] + + -- 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 \"fret\"" + ] + +-- | 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/FRETReqsDB2Copilot.hs b/src/Language/Trans/FRETReqsDB2Copilot.hs new file mode 100644 --- /dev/null +++ b/src/Language/Trans/FRETReqsDB2Copilot.hs @@ -0,0 +1,159 @@ +-- 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. +-- + +-- | Transform a FRET temporal logic specification contained in a requirements +-- database into a Copilot specification. +-- +-- Ideally, 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.FRETReqsDB2Copilot + ( FRETReqsDB2CopilotOptions(..) + , fret2CopilotModule + ) + where + +-- External imports +import Data.List ( nub, sort ) + +-- Internal imports: SMV +import qualified Language.SMV.AbsSMV as SMV ( BoolSpec (..) ) +import qualified Language.Trans.SMV2Copilot as SMV ( boolSpec2Copilot, + boolSpecNames ) + +-- Internal imports: CoCoSpec +import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec ( BoolSpec (..) ) +import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec ( boolSpec2Copilot, + boolSpecNames ) + +import qualified Language.FRETReqsDB.AST as FRET ( FRETReqsDB, semantics, + semanticsCoCoSpec, + semanticsFretish ) + +-- | Options used to customize the conversion of FRET Component Specifications +-- to Copilot code. +data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions + { fretReqsDB2CopilotUseCoCoSpec :: Bool + } + +-- | Return a string with the contents of the Copilot module that implements a +-- CoCoSpec BoolSpec. +-- +-- PRE: The BoolSpec does not use any identifiers that exist in Copilot, +-- or any of @prop@, @clock@, @ftp@, @ot@, @pre@. All identifiers used are +-- valid C99 identifiers. +fret2CopilotModule :: FRETReqsDB2CopilotOptions + -> FRET.FRETReqsDB + -> Either String String +fret2CopilotModule prefs x = do + cocoSpec <- FRET.semanticsCoCoSpec $ FRET.semantics x + smvSpec <- FRET.semanticsFretish $ FRET.semantics x + pure $ fret2CopilotModule' prefs smvSpec cocoSpec + +fret2CopilotModule' :: FRETReqsDB2CopilotOptions + -> SMV.BoolSpec + -> CoCoSpec.BoolSpec + -> String +fret2CopilotModule' prefs smvSpec cocoSpec = unlines $ concat sections + where + specS = if fretReqsDB2CopilotUseCoCoSpec prefs + then CoCoSpec.boolSpec2Copilot cocoSpec + else SMV.boolSpec2Copilot smvSpec + + idents = nub $ sort $ if fretReqsDB2CopilotUseCoCoSpec prefs + then CoCoSpec.boolSpecNames cocoSpec + else SMV.boolSpecNames smvSpec + + sections | fretReqsDB2CopilotUseCoCoSpec prefs + = [ imports, propDef, externs, clock, ftp, undef, spec, main' ] + + | otherwise + = [ imports, propDef, externs, clock, ftp, spec, main' ] + + 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 Language.Copilot (reify)" + , "import Prelude hiding ((&&), (||), (++), (<=), (>=)," + ++ " (<), (>), (==), not)" + , "" + ] + + propDef = [ "" + , "-- | Property to monitor." + , "prop :: Stream Bool" + , "prop = " ++ specS + , "" + ] + + externs = map (\i -> i ++ " = extern " ++ show i ++ " Nothing") idents + + clock = [ "" + , "-- | Clock that increases in one-unit steps." + , "clock :: Stream Int64" + , "clock = [0] ++ (clock + 1)" + , "" + ] + + ftp = [ "" + , "-- | First Time Point" + , "ftp :: Stream Bool" + , "ftp = [True] ++ false" + , "" + ] + + undef = [ "ot :: Int -> Int -> Stream Bool -> Stream Bool" + , "ot = undefined" + , "pre :: Stream Bool -> Stream Bool" + , "pre = undefined" + ] + + spec = [ "" + , "-- | Complete specification. Calls the C function void handler(); when" + , "-- the property is violated." + , "spec :: Spec" + , "spec = do" + , " trigger \"handler\" prop []" + , "" + ] + + main' = [ "" + , "main :: IO ()" + , "main = reify spec >>= compile \"fret\"" + ] diff --git a/src/Language/Trans/SMV2Copilot.hs b/src/Language/Trans/SMV2Copilot.hs new file mode 100644 --- /dev/null +++ b/src/Language/Trans/SMV2Copilot.hs @@ -0,0 +1,216 @@ +-- 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. +-- + +-- | Transform a FRET TL 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.SMV2Copilot where + +import Language.SMV.AbsSMV (AdditiveOp (..), BoolConst (..), BoolSpec (..), + Ident (..), MultOp (..), NumExpr (..), Number (..), + Op1Name (..), OpOne (..), OpTwo (..), OrdOp (..)) + +-- | Return the Copilot representation of a FRET BoolSpec. +-- +-- This function returns the temporal property only. The string does not +-- contain any top-level names, any imports, or auxiliary definitions that may +-- be required. +boolSpec2Copilot :: BoolSpec -> String +boolSpec2Copilot b = case b of + BoolSpecConst bc -> const2Copilot bc + + BoolSpecNum nc -> numExpr2Copilot nc + + BoolSpecSignal i -> ident2Copilot i + + BoolSpecCmp spec1 op2 spec2 -> "(" ++ boolSpec2Copilot spec1 + ++ " " ++ ordOp2Copilot op2 + ++ " " ++ boolSpec2Copilot spec2 + ++ ")" + + BoolSpecNeg spec -> "(" ++ "not" + ++ " " ++ boolSpec2Copilot spec + ++ ")" + + BoolSpecAnd spec1 spec2 -> "(" ++ boolSpec2Copilot spec1 + ++ " " ++ "&&" + ++ " " ++ boolSpec2Copilot spec2 + ++ ")" + + BoolSpecOr spec1 spec2 -> "(" ++ boolSpec2Copilot spec1 + ++ " " ++ "||" + ++ " " ++ boolSpec2Copilot spec2 + ++ ")" + + BoolSpecXor spec1 spec2 -> "(" ++ boolSpec2Copilot spec1 + ++ " " ++ "`xor`" + ++ " " ++ boolSpec2Copilot spec2 + ++ ")" + + BoolSpecImplies spec1 spec2 -> "(" ++ boolSpec2Copilot spec1 + ++ " " ++ "==>" + ++ " " ++ boolSpec2Copilot spec2 + ++ ")" + + BoolSpecEquivs spec1 spec2 -> "(" ++ boolSpec2Copilot spec1 + ++ " " ++ "<==>" + ++ " " ++ boolSpec2Copilot spec2 + ++ ")" + + BoolSpecOp1 op spec -> "(" ++ opOne2Copilot op + ++ " " ++ boolSpec2Copilot spec + ++ ")" + + BoolSpecOp2 spec1 op2 spec2 -> "(" ++ boolSpec2Copilot spec1 + ++ " " ++ opTwo2Copilot op2 + ++ " " ++ boolSpec2Copilot spec2 + ++ ")" + +-- | Return the Copilot representation of a FRET boolean constant. +const2Copilot :: BoolConst -> String +const2Copilot BoolConstTrue = "true" +const2Copilot BoolConstFalse = "false" +const2Copilot BoolConstFTP = "ftp" +const2Copilot BoolConstLAST = "last" + +-- | Return the Copilot representation of a numeric expression. +numExpr2Copilot :: NumExpr -> String +numExpr2Copilot (NumId i) = ident2Copilot i +numExpr2Copilot (NumConstI i) = show i +numExpr2Copilot (NumConstD i) = show i +numExpr2Copilot (NumAdd x op y) = "(" + ++ numExpr2Copilot x + ++ additiveOp2Copilot op + ++ numExpr2Copilot y + ++ ")" +numExpr2Copilot (NumMult x op y) = "(" + ++ numExpr2Copilot x + ++ multOp2Copilot op + ++ numExpr2Copilot y + ++ ")" + +-- | Return the Copilot representation of a FRET additive operator. +additiveOp2Copilot :: AdditiveOp -> String +additiveOp2Copilot OpPlus = "+" +additiveOp2Copilot OpMinus = "-" + +-- | Return the Copilot representation of a FRET multiplicative operator. +multOp2Copilot :: MultOp -> String +multOp2Copilot OpTimes = "*" +multOp2Copilot OpDiv = "/" + +-- | Return the Copilot representation of a FRET comparison operator. +ordOp2Copilot :: OrdOp -> String +ordOp2Copilot OrdOpLT = "<" +ordOp2Copilot OrdOpLE = "<=" +ordOp2Copilot OrdOpEQ = "==" +ordOp2Copilot OrdOpGT = ">" +ordOp2Copilot OrdOpGE = ">=" + +-- | Return the Copilot representation of a unary logical FRET operator. +opOne2Copilot :: OpOne -> String +opOne2Copilot (Op1Alone x) = opOneAlone2Copilot x +opOne2Copilot (Op1MTL x op v) = opOneMTL2Copilot x op v + +-- | Return the Copilot representation of a unary logical non-MTL FRET +-- operator. +opOneAlone2Copilot :: Op1Name -> String +opOneAlone2Copilot Op1Pre = "pre" +opOneAlone2Copilot Op1X = "next" +opOneAlone2Copilot Op1G = "always" +opOneAlone2Copilot Op1F = "eventually" +opOneAlone2Copilot Op1Y = "PTLTL.previous" +opOneAlone2Copilot Op1Z = "notPreviousNot" +opOneAlone2Copilot Op1Hist = "PTLTL.alwaysBeen" +opOneAlone2Copilot Op1O = "PTLTL.eventuallyPrev" + +-- | Return the Copilot representation of a unary logical MTL FRET operator. +opOneMTL2Copilot :: Op1Name -> OrdOp -> Number -> String +opOneMTL2Copilot operator _comparison number = + opOneMTL2Copilot' operator ++ " " ++ show (0 :: Int) + ++ " " ++ number2Copilot number + ++ " " ++ "clock" ++ " " + ++ show (1 :: Int) + +-- | Return the Copilot representation of a unary logical possibly MTL FRET +-- operator. +opOneMTL2Copilot' :: Op1Name -> String +opOneMTL2Copilot' Op1Pre = "pre" +opOneMTL2Copilot' Op1X = "next" +opOneMTL2Copilot' Op1G = "always" +opOneMTL2Copilot' Op1F = "eventually" +opOneMTL2Copilot' Op1Y = "MTL.previous" +opOneMTL2Copilot' Op1Z = "notPreviousNot" +opOneMTL2Copilot' Op1Hist = "MTL.alwaysBeen" +opOneMTL2Copilot' Op1O = "MTL.eventuallyPrev" + +-- | Return the Copilot representation of a FRET number. +number2Copilot :: Number -> String +number2Copilot (NumberInt n) = show n + +-- | Return the Copilot representation of a binary logical non-MTL FRET +-- operator. +opTwo2Copilot :: OpTwo -> String +opTwo2Copilot Op2S = "`since`" +opTwo2Copilot Op2T = "`triggers`" +opTwo2Copilot Op2V = "`releases`" +opTwo2Copilot Op2U = "`until`" + +-- | Return the Copilot representation of a FRET identifier. +ident2Copilot :: Ident -> String +ident2Copilot (Ident i) = i + +-- | Return all identifiers used in a BoolSpec that are not reserved keywords. +boolSpecNames :: BoolSpec -> [String] +boolSpecNames b = case b of + BoolSpecConst _bc -> [] + BoolSpecSignal (Ident i) -> [i] + BoolSpecNum e -> numExprNames e + BoolSpecCmp spec1 _op2 spec2 -> boolSpecNames spec1 ++ boolSpecNames spec2 + BoolSpecNeg spec -> boolSpecNames spec + BoolSpecAnd spec1 spec2 -> boolSpecNames spec1 ++ boolSpecNames spec2 + BoolSpecOr spec1 spec2 -> boolSpecNames spec1 ++ boolSpecNames spec2 + BoolSpecXor spec1 spec2 -> boolSpecNames spec1 ++ boolSpecNames spec2 + BoolSpecImplies spec1 spec2 -> boolSpecNames spec1 ++ boolSpecNames spec2 + BoolSpecEquivs spec1 spec2 -> boolSpecNames spec1 ++ boolSpecNames spec2 + BoolSpecOp1 _op spec -> boolSpecNames spec + BoolSpecOp2 spec1 _op2 spec2 -> boolSpecNames spec1 ++ boolSpecNames spec2 + +-- | Return all identifiers used in a numeric expression. +numExprNames :: NumExpr -> [String] +numExprNames numExpr = case numExpr of + NumId (Ident i) -> [i] + NumConstI _c -> [] + NumConstD _c -> [] + NumAdd expr1 _op expr2 -> numExprNames expr1 ++ numExprNames expr2 + NumMult expr1 _op expr2 -> numExprNames expr1 ++ numExprNames expr2 diff --git a/templates/copilot-cfs/CMakeLists.txt b/templates/copilot-cfs/CMakeLists.txt new file mode 100644 --- /dev/null +++ b/templates/copilot-cfs/CMakeLists.txt @@ -0,0 +1,16 @@ +cmake_minimum_required(VERSION 2.6.4) +project(CFE_SAMPLE_APP C) + +include_directories(../../Modules/Core/Interfaces) +include_directories(../Icarouslib/fsw/platform_inc) +include_directories(../inc) +include_directories(fsw/mission_inc) +include_directories(fsw/platform_inc) + +aux_source_directory(fsw/src APP_SRC_FILES) + +# Create the app module +add_cfe_app(copilot_cfs ${APP_SRC_FILES}) + +add_custom_target(HASKELL_COPILOT COMMAND cabal v1-sandbox init COMMAND cabal update COMMAND cabal v1-install copilot COMMAND cabal v1-exec "--" ghc --make Properties.hs COMMAND ./Properties WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/ SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/Properties.hs) +add_dependencies(copilot_cfs HASKELL_COPILOT) diff --git a/templates/copilot-cfs/fsw/for_build/Makefile b/templates/copilot-cfs/fsw/for_build/Makefile new file mode 100644 --- /dev/null +++ b/templates/copilot-cfs/fsw/for_build/Makefile @@ -0,0 +1,112 @@ +############################################################################### +# File: CFS Application Makefile +# +# $Id: Makefile 1.8 2009/07/09 12:25:54EDT rmcgraw Exp $ +# +# $Log: Makefile $ +# Revision 1.8 2009/07/09 12:25:54EDT rmcgraw +# DCR8291:1 Changed CFE_MISSION_INC to CFS_MISSION_INC and added log +# +############################################################################### +# +# Subsystem produced by this makefile. +# +APPTARGET = copilot_cfs + +# +# Entry Point for task +# +ENTRY_PT = COPILOT_CFSMain + +# +# Object files required to build subsystem. +# +OBJS = copilot_cfs.o + +# +# Source files required to build subsystem; used to generate dependencies. +# As long as there are no assembly files this can be automated. +# +SOURCES = $(OBJS:.o=.c) + + +## +## Specify extra C Flags needed to build this subsystem +## +LOCAL_COPTS = + + +## +## EXEDIR is defined here, just in case it needs to be different for a custom +## build +## +EXEDIR=../exe + +## +## Certain OSs and Application Loaders require the following option for +## Shared libraries. Currently only needed for vxWorks 5.5 and RTEMS. +## For each shared library that this app depends on, you need to have an +## entry like the following: +## -R../tst_lib/tst_lib.elf +## +SHARED_LIB_LINK = + +######################################################################## +# Should not have to change below this line, except for customized +# Mission and cFE directory structures +######################################################################## + +# +# Set build type to CFE_APP. This allows us to +# define different compiler flags for the cFE Core and Apps. +# +BUILD_TYPE = CFE_APP + +## +## Include all necessary cFE make rules +## Any of these can be copied to a local file and +## changed if needed. +## +## +## cfe-config.mak contains PSP and OS selection +## +include ../cfe/cfe-config.mak +## +## debug-opts.mak contains debug switches +## +include ../cfe/debug-opts.mak +## +## compiler-opts.mak contains compiler definitions and switches/defines +## +include $(CFE_PSP_SRC)/$(PSP)/make/compiler-opts.mak + +## +## Setup the include path for this subsystem +## The OS specific includes are in the build-rules.make file +## +## If this subsystem needs include files from another app, add the path here. +## +INCLUDE_PATH = \ +-I$(OSAL_SRC)/inc \ +-I$(CFE_CORE_SRC)/inc \ +-I$(CFE_PSP_SRC)/inc \ +-I$(CFE_PSP_SRC)/$(PSP)/inc \ +-I$(CFS_APP_SRC)/inc \ +-I$(CFS_APP_SRC)/$(APPTARGET)/fsw/src \ +-I$(CFS_MISSION_INC) \ +-I../cfe/inc \ +-I../inc + +## +## Define the VPATH make variable. +## This can be modified to include source from another directory. +## If there is no corresponding app in the cfs-apps directory, then this can be discarded, or +## if the mission chooses to put the src in another directory such as "src", then that can be +## added here as well. +## +VPATH = $(CFS_APP_SRC)/$(APPTARGET)/fsw/src + +## +## Include the common make rules for building a cFE Application +## +include $(CFE_CORE_SRC)/make/app-rules.mak diff --git a/templates/copilot-cfs/fsw/mission_inc/copilot_cfs_perfids.h b/templates/copilot-cfs/fsw/mission_inc/copilot_cfs_perfids.h new file mode 100644 --- /dev/null +++ b/templates/copilot-cfs/fsw/mission_inc/copilot_cfs_perfids.h @@ -0,0 +1,21 @@ +/************************************************************************ +** File: +** $Id: copilot_cfs_perfids.h $ +** +** Purpose: +** Define Sample App Performance IDs +** +** Notes: +** +*************************************************************************/ +#ifndef _copilot_cfs_perfids_h_ +#define _copilot_cfs_perfids_h_ + + +#define COPILOT_CFS_PERF_ID 91 + +#endif /* _copilot_cfs_perfids_h_ */ + +/************************/ +/* End of File Comment */ +/************************/ diff --git a/templates/copilot-cfs/fsw/platform_inc/copilot_cfs_msgids.h b/templates/copilot-cfs/fsw/platform_inc/copilot_cfs_msgids.h new file mode 100644 --- /dev/null +++ b/templates/copilot-cfs/fsw/platform_inc/copilot_cfs_msgids.h @@ -0,0 +1,23 @@ +/************************************************************************ +** File: +** $Id: copilot_cfs_msgids.h $ +** +** Purpose: +** Define Sample App Message IDs +** +** Notes: +** +** +*************************************************************************/ +#ifndef _copilot_cfs_msgids_h_ +#define _copilot_cfs_msgids_h_ + +#define COPILOT_CFS_CMD_MID 0x1882 +#define COPILOT_CFS_SEND_HK_MID 0x1883 +#define COPILOT_CFS_HK_TLM_MID 0x0883 + +#endif /* _copilot_cfs_msgids_h_ */ + +/************************/ +/* End of File Comment */ +/************************/ diff --git a/templates/copilot-cfs/fsw/src/Properties.hs b/templates/copilot-cfs/fsw/src/Properties.hs new file mode 100644 --- /dev/null +++ b/templates/copilot-cfs/fsw/src/Properties.hs @@ -0,0 +1,64 @@ +{-# LANGUAGE DataKinds #-} + +import Language.Copilot +import Copilot.Compile.C99 + +import Prelude hiding ((>), (<), div, (++)) + +position :: Stream Position +position = extern "my_position" Nothing + +-- | Position information received from cFS application. + +-- We hardcode 16 as the length of the array for the field TmlHeader because +-- the Haskell compiler does not accept using an identifier (e.g., +-- tmlHeaderSize) for array lengths. +data Position = Position + { tlmHeader :: Field "TlmHeader" (Array 16 Word8) + , aircraft_id :: Field "aircraft_id" Word32 + , time_gps :: Field "time_gps" Double + , time_boot :: Field "time_boot" Double + , latitute :: Field "latitude" Double + , longitude :: Field "longitude" Double + , altitude_abs :: Field "altitude_abs" Double + , altitude_rel :: Field "altitude_rel" Double + , vn :: Field "vn" Double + , ve :: Field "ve" Double + , vd :: Field "vd" Double + , hdg :: Field "hdg" Double + , hdop :: Field "hdop" Word16 + , vdop :: Field "vdop" Word16 + , numSats :: Field "numSats" Int64 + } + +instance Struct Position where + typename _ = "position_t" -- Name of the type in C + + -- Function to translate Vec to list of Value's, order should match struct. + toValues v = [ Value (Array Word8) (tlmHeader v) + , Value Word32 (aircraft_id v) + , Value Double (time_gps v) + , Value Double (time_boot v) + , Value Double (latitute v) + , Value Double (longitude v) + , Value Double (altitude_abs v) + , Value Double (altitude_rel v) + , Value Double (vn v) + , Value Double (ve v) + , Value Double (vd v) + , Value Double (hdg v) + , Value Word16 (hdop v) + , Value Word16 (vdop v) + , Value Int64 (numSats v) + ] + +-- We need to provide an instance to Typed with a bogus Vec +instance Typed Position where + typeOf = Struct (Position (Field $ array []) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0)) + +spec = do + -- Trigger that always executes, splits the vec into seperate args. + -- trigger "split" true [arg $ vecs # x, arg $ vecs # y] + trigger "split" (position # vn > 10) [] + +main = reify spec >>= compile "position" diff --git a/templates/copilot-cfs/fsw/src/copilot_cfs.c b/templates/copilot-cfs/fsw/src/copilot_cfs.c new file mode 100644 --- /dev/null +++ b/templates/copilot-cfs/fsw/src/copilot_cfs.c @@ -0,0 +1,161 @@ +/******************************************************************************* +** File: copilot_cfs.c +** +** Purpose: +** This file contains the source code for the Sample App. +** +*******************************************************************************/ + +/* +** Include Files: +*/ + +#include "copilot_cfs.h" +#include "copilot_cfs_perfids.h" +#include "copilot_cfs_msgids.h" +#include "copilot_cfs_msg.h" +#include "copilot_cfs_events.h" +#include "copilot_cfs_version.h" +#include "Icarous_msgids.h" +#include "Icarous_msg.h" + +position_t my_position; +void split(void); +void step(void); + +/* +** global data +*/ + +copilot_hk_tlm_t COPILOT_HkTelemetryPkt; +CFE_SB_PipeId_t COPILOT_CommandPipe; +CFE_SB_MsgPtr_t COPILOTMsgPtr; + +static CFE_EVS_BinFilter_t COPILOT_EventFilters[] = + { /* Event ID mask */ + {COPILOT_STARTUP_INF_EID, 0x0000}, + {COPILOT_COMMAND_ERR_EID, 0x0000}, + {COPILOT_COMMANDCPVIOL_INF_EID, 0x0000}, + }; + +/** * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */ +/* COPILOT_AppMain() -- Application entry point and main process loop */ +/* */ +/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * **/ +void COPILOT_AppMain( void ) +{ + int32 status; + uint32 RunStatus = CFE_ES_APP_RUN; + + CFE_ES_PerfLogEntry(COPILOT_CFS_PERF_ID); + + COPILOT_AppInit(); + + /* + ** COPILOT Runloop + */ + while (CFE_ES_RunLoop(&RunStatus) == TRUE) + { + CFE_ES_PerfLogExit(COPILOT_CFS_PERF_ID); + + /* Pend on receipt of command packet -- timeout set to 500 millisecs */ + status = CFE_SB_RcvMsg(&COPILOTMsgPtr, COPILOT_CommandPipe, 500); + + CFE_ES_PerfLogEntry(COPILOT_CFS_PERF_ID); + + if (status == CFE_SUCCESS) + { + COPILOT_ProcessCommandPacket(); + } + + } + + CFE_ES_ExitApp(RunStatus); + +} /* End of COPILOT_AppMain() */ + +/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */ +/* */ +/* COPILOT_AppInit() -- initialization */ +/* */ +/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * **/ +void COPILOT_AppInit(void) +{ + /* + ** Register the app with Executive services + */ + CFE_ES_RegisterApp() ; + + /* + ** Register the events + */ + CFE_EVS_Register(COPILOT_EventFilters, + sizeof(COPILOT_EventFilters)/sizeof(CFE_EVS_BinFilter_t), + CFE_EVS_BINARY_FILTER); + + /* + ** Create the Software Bus command pipe and subscribe to housekeeping + ** messages + */ + CFE_SB_CreatePipe(&COPILOT_CommandPipe, COPILOT_PIPE_DEPTH,"COPILOT_CMD_PIPE"); + CFE_SB_Subscribe(ICAROUS_POSITION_MID, COPILOT_CommandPipe); + + CFE_EVS_SendEvent (COPILOT_STARTUP_INF_EID, CFE_EVS_INFORMATION, + "COPILOT App Initialized. Version %d.%d.%d.%d", + COPILOT_CFS_MAJOR_VERSION, + COPILOT_CFS_MINOR_VERSION, + COPILOT_CFS_REVISION, + COPILOT_CFS_MISSION_REV); + +} /* End of COPILOT_AppInit() */ + +/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * **/ +/* Name: COPILOT_ProcessCommandPacket */ +/* */ +/* Purpose: */ +/* This routine will process any packet that is received on the COPILOT */ +/* command pipe. */ +/* */ +/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */ +void COPILOT_ProcessCommandPacket(void) +{ + CFE_SB_MsgId_t MsgId; + + MsgId = CFE_SB_GetMsgId(COPILOTMsgPtr); + + switch (MsgId) + { + case ICAROUS_POSITION_MID: + COPILOT_ProcessIcarousPosition(); + break; + default: + COPILOT_HkTelemetryPkt.copilot_command_error_count++; + CFE_EVS_SendEvent(COPILOT_COMMAND_ERR_EID,CFE_EVS_ERROR, + "COPILOT: invalid command packet,MID = 0x%x", MsgId); + break; + } + + return; + +} /* End COPILOT_ProcessCommandPacket */ + +/** + * Make ICAROUS data available to Copilot and run monitors. + */ +void COPILOT_ProcessIcarousPosition(void) +{ + position_t* msg; + msg = (position_t*) COPILOTMsgPtr; + my_position = *msg; + + // Run all copilot monitors. + step(); +} + +/** + * Report copilot property violations. + */ +void split(void) { + CFE_EVS_SendEvent(COPILOT_COMMANDCPVIOL_INF_EID, CFE_EVS_ERROR, + "COPILOT: violation"); +} diff --git a/templates/copilot-cfs/fsw/src/copilot_cfs.h b/templates/copilot-cfs/fsw/src/copilot_cfs.h new file mode 100644 --- /dev/null +++ b/templates/copilot-cfs/fsw/src/copilot_cfs.h @@ -0,0 +1,49 @@ +/******************************************************************************* +** File: copilot_app.h +** +** Purpose: +** This file is main hdr file for the COPILOT application. +** +** +*******************************************************************************/ + +#ifndef _copilot_app_h_ +#define _copilot_app_h_ + +/* +** Required header files. +*/ +#include "cfe.h" +#include "cfe_error.h" +#include "cfe_evs.h" +#include "cfe_sb.h" +#include "cfe_es.h" + +#include +#include +#include + +/***********************************************************************/ + +#define COPILOT_PIPE_DEPTH 32 + +/************************************************************************ +** Type Definitions +*************************************************************************/ + +/****************************************************************************/ +/* +** Local function prototypes. +** +** Note: Except for the entry point (COPILOT_AppMain), these +** functions are not called from any other source module. +*/ +void COPILOT_AppMain(void); +void COPILOT_AppInit(void); +void COPILOT_ProcessCommandPacket(void); +void COPILOT_ProcessIcarousPosition(void); +void COPILOT_ResetCounters(void); + +boolean COPILOT_VerifyCmdLength(CFE_SB_MsgPtr_t msg, uint16 ExpectedLength); + +#endif /* _copilot_app_h_ */ diff --git a/templates/copilot-cfs/fsw/src/copilot_cfs_events.h b/templates/copilot-cfs/fsw/src/copilot_cfs_events.h new file mode 100644 --- /dev/null +++ b/templates/copilot-cfs/fsw/src/copilot_cfs_events.h @@ -0,0 +1,27 @@ +/************************************************************************ +** File: +** copilot_app_events.h +** +** Purpose: +** Define COPILOT App Events IDs +** +** Notes: +** +** +*************************************************************************/ +#ifndef _copilot_app_events_h_ +#define _copilot_app_events_h_ + + +#define COPILOT_RESERVED_EID 0 +#define COPILOT_STARTUP_INF_EID 1 +#define COPILOT_COMMAND_ERR_EID 2 +#define COPILOT_COMMANDCPVIOL_INF_EID 3 +#define COPILOT_INVALID_MSGID_ERR_EID 4 +#define COPILOT_LEN_ERR_EID 5 + +#endif /* _copilot_app_events_h_ */ + +/************************/ +/* End of File Comment */ +/************************/ diff --git a/templates/copilot-cfs/fsw/src/copilot_cfs_msg.h b/templates/copilot-cfs/fsw/src/copilot_cfs_msg.h new file mode 100644 --- /dev/null +++ b/templates/copilot-cfs/fsw/src/copilot_cfs_msg.h @@ -0,0 +1,42 @@ +/******************************************************************************* +** File: +** copilot_cfs_msg.h +** +** Purpose: +** Define COPILOT App Messages and info +** +** Notes: +** +** +*******************************************************************************/ +#ifndef _copilot_cfs_msg_h_ +#define _copilot_cfs_msg_h_ + +/*************************************************************************/ +/* +** Type definition (generic "no arguments" command) +*/ +typedef struct +{ + uint8 CmdHeader[CFE_SB_CMD_HDR_SIZE]; + +} COPILOT_NoArgsCmd_t; + +/*************************************************************************/ +/* +** Type definition (COPILOT App housekeeping) +*/ +typedef struct +{ + uint8 TlmHeader[CFE_SB_TLM_HDR_SIZE]; + uint8 copilot_command_error_count; + uint8 copilot_command_count; + uint8 spare[2]; + +} OS_PACK copilot_hk_tlm_t ; + +#endif /* _copilot_cfs_msg_h_ */ + +/************************/ +/* End of File Comment */ +/************************/ diff --git a/templates/copilot-cfs/fsw/src/copilot_cfs_version.h b/templates/copilot-cfs/fsw/src/copilot_cfs_version.h new file mode 100644 --- /dev/null +++ b/templates/copilot-cfs/fsw/src/copilot_cfs_version.h @@ -0,0 +1,24 @@ +/************************************************************************ +** File: +** $Id: copilot_app_version.h $ +** +** Purpose: +** The Sample Application header file containing version number +** +** Notes: +** +** +*************************************************************************/ +#ifndef _copilot_app_version_h_ +#define _copilot_app_version_h_ + +#define COPILOT_CFS_MAJOR_VERSION 1 +#define COPILOT_CFS_MINOR_VERSION 0 +#define COPILOT_CFS_REVISION 0 +#define COPILOT_CFS_MISSION_REV 0 + +#endif /* _copilot_app_version_h_ */ + +/************************/ +/* End of File Comment */ +/************************/ diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -0,0 +1,152 @@ +-- | Test ogma-core +module Main where + +import Data.Monoid ( mempty ) +import Test.Framework ( Test, defaultMainWithOpts ) +import Test.Framework.Providers.HUnit ( testCase ) +import Test.HUnit ( assertBool ) + +-- Internal imports +import Command.CStructs2Copilot ( cstructs2Copilot ) +import Command.FRETComponentSpec2Copilot ( FRETComponentSpec2CopilotOptions (..) + , fretComponentSpec2Copilot + ) +import Command.FRETReqsDB2Copilot ( FRETReqsDB2CopilotOptions (..) + , fretReqsDB2Copilot + ) +import Command.Result ( isSuccess ) + +-- | Run all unit tests on ogma-core. +main :: IO () +main = + defaultMainWithOpts tests mempty + +-- | All unit tests for ogma-core. +tests :: [Test.Framework.Test] +tests = + [ + testCase "fret-cmd-fret-cs-ok" + (testFretComponentSpec2Copilot "tests/fret_good.json" True) + -- Should pass + + , testCase "fret-cmd-fret-file-not-found" + (testFretComponentSpec2Copilot "tests/file-invalid.json" False) + -- Should fail because the file does not exist + + , testCase "fret-cmd-fret-parse-fail-1" + (testFretComponentSpec2Copilot + "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" + (testFretComponentSpec2Copilot + "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" + (testFretComponentSpec2Copilot + "tests/commands-fret-error-parsing-failed-3.json" + False + ) + -- Should fail because a field is missing in an internal variable + + , testCase "fret-reqs-db-cocospec" + (testFretReqsDBCoCoSpec2Copilot "tests/fret-example1.json" True) + -- 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 and conversion to Copilot structs +-- for a particular file. +-- +-- This test uses the Copilot backend for C header files, so it generates +-- Copilot types and instances. +-- +-- This IO action fails if any of the following are true: +-- * 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. +-- +testCStructs2Copilot :: FilePath -- ^ Path to a C header file with structs + -> Bool + -> IO () +testCStructs2Copilot file success = do + result <- cstructs2Copilot file + + -- True if success is expected and detected, or niether expected nor + -- detected. + let testPass = success == isSuccess result + + assertBool errorMsg testPass + where + errorMsg = "The result of the transformation of the C header file " + ++ file ++ " to Copilot struct declarations was unexpected." + +-- | Test FRET Component Spec 2 Copilot transformation. +-- +-- This test uses the Copilot backend for FRET files, so it generates a Copilot +-- file. +-- +-- This IO action fails if any of the following are true: +-- * 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. +testFretComponentSpec2Copilot :: FilePath -- ^ Path to a FRET/JSON requirements file + -> Bool + -> IO () +testFretComponentSpec2Copilot file success = do + let opts = FRETComponentSpec2CopilotOptions + { fretCS2CopilotUseCoCoSpec = False + , fretCS2CopilotIntType = "Int64" + , fretCS2CopilotRealType = "Float" + } + result <- fretComponentSpec2Copilot file opts + + -- True if success is expected and detected, or niether expected nor + -- detected. + let testPass = success == isSuccess result + + assertBool errorMsg testPass + where + errorMsg = "The result of the transformation of FRET CS file " + ++ file ++ " to Copilot was unexpected." + +-- | Test FRET Component Spec 2 Copilot transformation. +-- +-- This test uses the Copilot backend for FRET files with the CoCoSpec +-- frontend. +-- +-- This IO action fails if any of the following are true: +-- * 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. +-- +testFretReqsDBCoCoSpec2Copilot :: FilePath -- ^ Path to a FRET/JSON + -- requirements file + -> Bool + -> IO () +testFretReqsDBCoCoSpec2Copilot file success = do + let opts = FRETReqsDB2CopilotOptions + { fretReqsDB2CopilotUseCoCoSpec = True + } + result <- fretReqsDB2Copilot file opts + + -- True if success is expected and detected, or niether expected nor + -- detected. + let testPass = success == isSuccess result + + assertBool errorMsg testPass + where + errorMsg = "The result of the transformation of FRET CS file " + ++ file ++ " to Copilot was unexpected."