diff --git a/ogma-cli/CHANGELOG.md b/ogma-cli/CHANGELOG.md index f005cbe..dbd0af8 100644 --- a/ogma-cli/CHANGELOG.md +++ b/ogma-cli/CHANGELOG.md @@ -1,9 +1,10 @@ # Revision history for ogma-cli -## [1.X.Y] - 2024-11-26 +## [1.X.Y] - 2024-12-23 * Update contribution guidelines (#161). * Provide ability to customize template in fprime command (#185). +* Provide ability to customize template in standalone command (#189). ## [1.5.0] - 2024-11-21 diff --git a/ogma-cli/src/CLI/CommandStandalone.hs b/ogma-cli/src/CLI/CommandStandalone.hs index b4cd737..108e4a6 100644 --- a/ogma-cli/src/CLI/CommandStandalone.hs +++ b/ogma-cli/src/CLI/CommandStandalone.hs @@ -43,7 +43,7 @@ module CLI.CommandStandalone where -- External imports -import Options.Applicative (Parser, help, long, metavar, many, short, +import Options.Applicative (Parser, help, long, many, metavar, optional, short, showDefault, strOption, switch, value) -- External imports: command results @@ -58,11 +58,13 @@ import qualified Command.Standalone -- | Options to generate Copilot from specification. data CommandOpts = CommandOpts - { standaloneFileName :: FilePath - , standaloneFormat :: String - , standalonePropFormat :: String - , standaloneTypes :: [String] - , standaloneTarget :: String + { standaloneTargetDir :: FilePath + , standaloneTemplateDir :: Maybe FilePath + , standaloneFileName :: FilePath + , standaloneFormat :: String + , standalonePropFormat :: String + , standaloneTypes :: [String] + , standaloneTarget :: String } -- | Transform an input specification into a Copilot specification. @@ -71,7 +73,9 @@ command c = standalone (standaloneFileName c) internalCommandOpts where internalCommandOpts :: Command.Standalone.StandaloneOptions internalCommandOpts = Command.Standalone.StandaloneOptions - { Command.Standalone.standaloneFormat = standaloneFormat c + { Command.Standalone.standaloneTargetDir = standaloneTargetDir c + , Command.Standalone.standaloneTemplateDir = standaloneTemplateDir c + , Command.Standalone.standaloneFormat = standaloneFormat c , Command.Standalone.standalonePropFormat = standalonePropFormat c , Command.Standalone.standaloneTypeMapping = types , Command.Standalone.standaloneFilename = standaloneTarget c @@ -98,6 +102,20 @@ commandDesc = commandOptsParser :: Parser CommandOpts commandOptsParser = CommandOpts <$> strOption + ( long "target-dir" + <> metavar "DIR" + <> showDefault + <> value "copilot" + <> help strStandaloneTargetDirDesc + ) + <*> optional + ( strOption + ( long "template-dir" + <> metavar "DIR" + <> help strStandaloneTemplateDirArgDesc + ) + ) + <*> strOption ( long "file-name" <> metavar "FILENAME" <> help strStandaloneFilenameDesc @@ -133,6 +151,14 @@ commandOptsParser = CommandOpts <> value "monitor" ) +-- | Target dir flag description. +strStandaloneTargetDirDesc :: String +strStandaloneTargetDirDesc = "Target directory" + +-- | Template dir flag description. +strStandaloneTemplateDirArgDesc :: String +strStandaloneTemplateDirArgDesc = "Directory holding standalone source template" + -- | Filename flag description. strStandaloneFilenameDesc :: String strStandaloneFilenameDesc = "File with properties or requirements" diff --git a/ogma-core/CHANGELOG.md b/ogma-core/CHANGELOG.md index cd51e53..7417feb 100644 --- a/ogma-core/CHANGELOG.md +++ b/ogma-core/CHANGELOG.md @@ -1,9 +1,10 @@ # Revision history for ogma-core -## [1.X.Y] - 2024-12-04 +## [1.X.Y] - 2024-12-23 * Replace queueSize with QUEUE_SIZE in FPP file (#186). * Use template expansion system to generate F' monitoring component (#185). +* Use template expansion system to generate standalone Copilot monitor (#189). ## [1.5.0] - 2024-11-21 diff --git a/ogma-core/ogma-core.cabal b/ogma-core/ogma-core.cabal index e493068..54c0108 100644 --- a/ogma-core/ogma-core.cabal +++ b/ogma-core/ogma-core.cabal @@ -71,6 +71,7 @@ data-files: templates/copilot-cfs/CMakeLists.txt templates/fprime/Copilot.hpp templates/fprime/Dockerfile templates/fprime/instance-copilot + templates/standalone/Copilot.hs data/formats/fcs_smv data/formats/fcs_cocospec data/formats/fdb_smv @@ -143,6 +144,7 @@ test-suite unit-tests build-depends: base + , directory , HUnit , QuickCheck , test-framework diff --git a/ogma-core/src/Command/Standalone.hs b/ogma-core/src/Command/Standalone.hs index 5d96314..f727433 100644 --- a/ogma-core/src/Command/Standalone.hs +++ b/ogma-core/src/Command/Standalone.hs @@ -1,4 +1,5 @@ {-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE OverloadedStrings #-} -- Copyright 2020 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- @@ -38,15 +39,18 @@ module Command.Standalone where -- External imports -import Data.Aeson (decode, eitherDecode) -import Data.ByteString.Lazy (fromStrict, pack) +import Control.Exception as E +import Data.Aeson (decode, eitherDecode, object, (.=)) +import Data.ByteString.Lazy (fromStrict) import Data.Foldable (for_) import Data.List (nub, (\\)) import Data.Maybe (fromMaybe) import System.FilePath (()) +import Data.Text.Lazy (pack) -- External imports: auxiliary -import Data.ByteString.Extra as B ( safeReadFile ) +import Data.ByteString.Extra as B ( safeReadFile ) +import System.Directory.Extra ( copyTemplate ) -- Internal imports: auxiliary import Command.Result (Result (..)) @@ -73,38 +77,61 @@ import Language.Trans.SMV2Copilot as SMV (boolSpec2Copilot, boolSpecNames) import Language.Trans.Spec2Copilot (spec2Copilot, specAnalyze) --- | Print the contents of a Copilot module that implements the spec in an +-- | Generate a new standalone Copilot monitor that implements the spec in an -- input file. -- -- PRE: The file given is readable, contains a valid file with recognizable -- format, the formulas in the file do not use any identifiers that exist in -- Copilot, or any of @prop@, @clock@, @ftp@, @notPreviousNot@. All identifiers --- used are valid C99 identifiers. +-- used are valid C99 identifiers. The template, if provided, exists and uses +-- the variables needed by the standalone application generator. The target +-- directory is writable and there's enough disk space to copy the files over. standalone :: FilePath -- ^ Path to a file containing a specification -> StandaloneOptions -- ^ Customization options -> IO (Result ErrorCode) standalone fp options = do + E.handle (return . standaloneTemplateError options fp) $ do + -- Obtain template dir + templateDir <- case standaloneTemplateDir options of + Just x -> return x + Nothing -> do + dataDir <- getDataDir + return $ dataDir "templates" "standalone" - let functions = exprPair (standalonePropFormat options) + let functions = exprPair (standalonePropFormat options) - copilot <- standalone' fp options functions + copilot <- standalone' fp options functions - let (mOutput, result) = standaloneResult options fp copilot + let (mOutput, result) = standaloneResult options fp copilot - for_ mOutput putStrLn - return result + for_ mOutput $ \(externs, internals, reqs, triggers, specName) -> do + let subst = object $ + [ "externs" .= pack externs + , "internals" .= pack internals + , "reqs" .= pack reqs + , "triggers" .= pack triggers + , "specName" .= pack specName + ] --- | Print the contents of a Copilot module that implements the spec in an + let targetDir = standaloneTargetDir options + + copyTemplate templateDir subst targetDir + + return result + +-- | Generate a new standalone Copilot monitor that implements the spec in an -- input file, using a subexpression handler. -- -- PRE: The file given is readable, contains a valid file with recognizable -- format, the formulas in the file do not use any identifiers that exist in -- Copilot, or any of @prop@, @clock@, @ftp@, @notPreviousNot@. All identifiers --- used are valid C99 identifiers. +-- used are valid C99 identifiers. The template, if provided, exists and uses +-- the variables needed by the standalone application generator. The target +-- directory is writable and there's enough disk space to copy the files over. standalone' :: FilePath -> StandaloneOptions -> ExprPair - -> IO (Either String String) + -> IO (Either String (String, String, String, String, String)) standalone' fp options (ExprPair parse replace print ids) = do let name = standaloneFilename options typeMaps = typeToCopilotTypeMapping options @@ -135,7 +162,9 @@ standalone' fp options (ExprPair parse replace print ids) = do -- | Options used to customize the conversion of specifications to Copilot -- code. data StandaloneOptions = StandaloneOptions - { standaloneFormat :: String + { standaloneTargetDir :: FilePath + , standaloneTemplateDir :: Maybe FilePath + , standaloneFormat :: String , standalonePropFormat :: String , standaloneTypeMapping :: [(String, String)] , standaloneFilename :: String @@ -153,17 +182,36 @@ type ErrorCode = Int ecStandaloneError :: ErrorCode ecStandaloneError = 1 +-- | Error: standalone component generation failed during the copy/write +-- process. +ecStandaloneTemplateError :: ErrorCode +ecStandaloneTemplateError = 2 + -- * Result -- | Process the result of the transformation function. standaloneResult :: StandaloneOptions -> FilePath - -> Either String String - -> (Maybe String, Result ErrorCode) + -> Either String a + -> (Maybe a, Result ErrorCode) standaloneResult options fp result = case result of Left msg -> (Nothing, Error ecStandaloneError msg (LocationFile fp)) Right t -> (Just t, Success) +-- | Report an error when trying to open or copy the template +standaloneTemplateError :: StandaloneOptions + -> FilePath + -> E.SomeException + -> Result ErrorCode +standaloneTemplateError options fp exception = + Error ecStandaloneTemplateError msg (LocationFile fp) + where + msg = + "Standlone monitor 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. " + ++ show exception + -- * Mapping of types from input format to Copilot typeToCopilotTypeMapping :: StandaloneOptions -> [(String, String)] typeToCopilotTypeMapping options = diff --git a/ogma-core/src/Language/Trans/Spec2Copilot.hs b/ogma-core/src/Language/Trans/Spec2Copilot.hs index 8a75ca6..57254e0 100644 --- a/ogma-core/src/Language/Trans/Spec2Copilot.hs +++ b/ogma-core/src/Language/Trans/Spec2Copilot.hs @@ -1,4 +1,5 @@ -- Copyright 2024 United States Government as represented by the Administrator +-- Copyright 2024 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- -- Disclaimers @@ -36,7 +37,7 @@ module Language.Trans.Spec2Copilot where -- External imports -import Data.List ( intersect, lookup, union ) +import Data.List ( intercalate, intersect, lookup, union ) import Data.Maybe ( fromMaybe ) -- External imports: auxiliary @@ -56,46 +57,17 @@ spec2Copilot :: String -- Spec / target file name -> ([(String, String)] -> a -> a) -- Expr subsitution function -> (a -> String) -- Expr show function -> Spec a -- Specification - -> Either String String + -> Either String (String, String, String, String, String) spec2Copilot specName typeMaps exprTransform showExpr spec = - pure $ unlines $ concat - [ imports - , externs - , internals - , reqs - , clock - , ftp - , pre - , tpre - , notPreviousNot - , copilotSpec - , main' - ] + pure (externs, internals, reqs, triggers, specName) where - -- Import header block - imports :: [String] - imports = - [ "import Copilot.Compile.C99" - , "import Copilot.Language hiding (prop)" - , "import Copilot.Language.Prelude" - , "import Copilot.Library.LTL (next)" - , "import Copilot.Library.MTL hiding (since," - ++ " alwaysBeen, trigger)" - , "import Copilot.Library.PTLTL (since, previous," - ++ " alwaysBeen)" - , "import qualified Copilot.Library.PTLTL as PTLTL" - , "import qualified Copilot.Library.MTL as MTL" - , "import Language.Copilot (reify)" - , "import Prelude hiding ((&&), (||), (++)," - ++ " (<=), (>=), (<), (>), (==), (/=), not)" - , "" - ] - -- Extern streams - externs = concatMap externVarToDecl - (externalVariables spec) + externs = unlines' + $ intercalate [""] + $ map externVarToDecl + (externalVariables spec) where externVarToDecl i = [ propName ++ " :: Stream " @@ -110,14 +82,15 @@ spec2Copilot specName typeMaps exprTransform showExpr spec = ++ show (externalVariableName i) ++ " " ++ "Nothing" - , "" ] where propName = safeMap nameSubstitutions (externalVariableName i) -- Internal stream definitions - internals = concatMap internalVarToDecl - (internalVariables spec) + internals = unlines' + $ intercalate [""] + $ map internalVarToDecl + (internalVariables spec) where internalVarToDecl i = (\implem -> [ propName @@ -129,20 +102,19 @@ spec2Copilot specName typeMaps exprTransform showExpr spec = , propName ++ " = " ++ implem - - , "" ]) implementation where propName = safeMap nameSubstitutions (internalVariableName i) implementation = (internalVariableExpr i) -- Encoding of requirements as boolean streams - reqs :: [String] - reqs = concatMap reqToDecl (requirements spec) + reqs :: String + reqs = unlines' + $ intercalate [""] + $ map reqToDecl (requirements spec) where reqToDecl i = [ reqComment, reqSignature , reqBody nameSubstitutions - , "" ] where reqName = safeMap nameSubstitutions (requirementName i) @@ -165,58 +137,10 @@ spec2Copilot specName typeMaps exprTransform showExpr spec = (showExpr (exprTransform subs (requirementExpr i))) - -- Auxiliary streams: clock - clock :: [String] - clock = [ "" - , "-- | Clock that increases in one-unit steps." - , "clock :: Stream Int64" - , "clock = [0] ++ (clock + 1)" - , "" - ] - - -- Auxiliary streams: first time point - ftp :: [String] - ftp = [ "" - , "-- | First Time Point" - , "ftp :: Stream Bool" - , "ftp = [True] ++ false" - , "" - ] - - -- Auxiliary streams: pre - pre = [ "" - , "pre :: Stream Bool -> Stream Bool" - , "pre = ([False] ++)" - ] - - -- Auxiliary streams: tpre - tpre = [ "" - , "tpre :: Stream Bool -> Stream Bool" - , "tpre = ([True] ++)" - ] - - -- Auxiliary streams: notPreviousNot - notPreviousNot :: [String] - notPreviousNot = [ "" - , "notPreviousNot :: Stream Bool -> Stream Bool" - , "notPreviousNot = not . PTLTL.previous . not" - ] - - -- Main specification - copilotSpec :: [String] - copilotSpec = [ "" - , "-- | Complete specification. Calls C handler functions" - ++ " when" - , "-- properties are violated." - , "spec :: Spec" - , "spec = do" - ] - ++ triggers - ++ [ "" ] + -- Main specification triggers + triggers :: String + triggers = unlines' $ fmap reqTrigger (requirements spec) where - triggers :: [String] - triggers = fmap reqTrigger (requirements spec) - reqTrigger :: Requirement a -> String reqTrigger r = " trigger " ++ show handlerName ++ " (not " ++ propName ++ ") " ++ "[]" @@ -224,14 +148,6 @@ spec2Copilot specName typeMaps exprTransform showExpr spec = handlerName = "handler" ++ sanitizeUCIdentifier (requirementName r) propName = safeMap nameSubstitutions (requirementName r) - -- Main program that compiles specification to C in two files (code and - -- header). - main' :: [String] - main' = [ "" - , "main :: IO ()" - , "main = reify spec >>= compile \"" ++ specName ++ "\"" - ] - -- Map from a variable name to its desired identifier in the code -- generated. internalVariableMap = @@ -318,3 +234,9 @@ specAnalyze spec -- substitution table. safeMap :: [(String, String)] -> String -> String safeMap ls k = fromMaybe k $ lookup k ls + +-- | Create a string from a list of strings, inserting new line characters +-- between them. Unlike 'Prelude.unlines', this function does not insert +-- an end of line character at the end of the last string. +unlines' :: [String] -> String +unlines' = intercalate "\n" diff --git a/ogma-core/templates/standalone/Copilot.hs b/ogma-core/templates/standalone/Copilot.hs new file mode 100644 index 0000000..69329c9 --- /dev/null +++ b/ogma-core/templates/standalone/Copilot.hs @@ -0,0 +1,40 @@ +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) + +{{{externs}}} +{{{internals}}} +{{{reqs}}} + +-- | Clock that increases in one-unit steps. +clock :: Stream Int64 +clock = [0] ++ (clock + 1) + +-- | First Time Point +ftp :: Stream Bool +ftp = [True] ++ false + +pre :: Stream Bool -> Stream Bool +pre = ([False] ++) + +tpre :: Stream Bool -> Stream Bool +tpre = ([True] ++) + +notPreviousNot :: Stream Bool -> Stream Bool +notPreviousNot = not . PTLTL.previous . not + +-- | Complete specification. Calls C handler functions when properties are +-- violated. +spec :: Spec +spec = do +{{{triggers}}} + +main :: IO () +main = reify spec >>= compile "{{{specName}}}" diff --git a/ogma-core/tests/Main.hs b/ogma-core/tests/Main.hs index 4565d21..716d635 100644 --- a/ogma-core/tests/Main.hs +++ b/ogma-core/tests/Main.hs @@ -5,6 +5,7 @@ import Data.Monoid ( mempty ) import Test.Framework ( Test, defaultMainWithOpts ) import Test.Framework.Providers.HUnit ( testCase ) import Test.HUnit ( assertBool ) +import System.Directory ( getTemporaryDirectory ) -- Internal imports import Command.CStructs2Copilot (cstructs2Copilot) @@ -101,11 +102,14 @@ testFretComponentSpec2Copilot :: FilePath -- ^ Path to a FRET/JSON requirements -> Bool -> IO () testFretComponentSpec2Copilot file success = do + targetDir <- getTemporaryDirectory let opts = StandaloneOptions { standaloneFormat = "fcs" , standalonePropFormat = "smv" , standaloneTypeMapping = [("int", "Int64"), ("real", "Float")] , standaloneFilename = "fret" + , standaloneTargetDir = targetDir + , standaloneTemplateDir = Nothing } result <- standalone file opts @@ -133,11 +137,14 @@ testFretReqsDBCoCoSpec2Copilot :: FilePath -- ^ Path to a FRET/JSON -> Bool -> IO () testFretReqsDBCoCoSpec2Copilot file success = do + targetDir <- getTemporaryDirectory let opts = StandaloneOptions { standaloneFormat = "fdb" , standalonePropFormat = "cocospec" , standaloneTypeMapping = [] , standaloneFilename = "fret" + , standaloneTargetDir = targetDir + , standaloneTemplateDir = Nothing } result <- standalone file opts