Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ogma-cli: Allow customizing the standalone application template. Refs #189. #191

Merged
3 changes: 2 additions & 1 deletion ogma-cli/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -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

Expand Down
40 changes: 33 additions & 7 deletions ogma-cli/src/CLI/CommandStandalone.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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.
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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"
Expand Down
3 changes: 2 additions & 1 deletion ogma-core/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -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

Expand Down
2 changes: 2 additions & 0 deletions ogma-core/ogma-core.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -143,6 +144,7 @@ test-suite unit-tests

build-depends:
base
, directory
, HUnit
, QuickCheck
, test-framework
Expand Down
80 changes: 64 additions & 16 deletions ogma-core/src/Command/Standalone.hs
Original file line number Diff line number Diff line change
@@ -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.
--
Expand Down Expand Up @@ -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 (..))
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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 =
Expand Down
Loading
Loading