Skip to content

Commit

Permalink
ogma-core: Use template expansion to generate standalone monitoring c…
Browse files Browse the repository at this point in the history 
…omponent. Refs nasa#189.

The standlone backend uses a fixed template to generate the Copilot
monitor. That template does not fit all use cases, so we are finding
users heavily modifying the output (which is hard to keep up with when
there are changes), and or not using ogma altogether for that reason.

This commit modifies the ogma-core standalone command to use mustache to
generate the Copilot monitor via a template and variable expansion. We
introduce a new template that uses variables, and we modify the cabal
file to include the new files as data files that are copied over during
installation.

To be able to generate the files, we need to introduce a target
directory option for the standalone command.
  • Loading branch information
@ivanperez-keera
ivanperez-keera committed Dec 11, 2024
1 parent c4060bf commit c984144
Show file tree
Hide file tree
Showing 4 changed files with 117 additions and 115 deletions.
1 change: 1 addition & 0 deletions ogma-core/ogma-core.cabal
View file
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
64 changes: 52 additions & 12 deletions ogma-core/src/Command/Standalone.hs
View file
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 Down Expand Up @@ -84,15 +88,31 @@ 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
dataDir <- getDataDir
let templateDir = 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
]

let targetDir = standaloneTargetDir options

copyTemplate templateDir subst targetDir

return result

-- | Print the contents of a Copilot module that implements the spec in an
-- input file, using a subexpression handler.
Expand All @@ -104,7 +124,7 @@ standalone fp options = do
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 +155,8 @@ 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
, standaloneFormat :: String
, standalonePropFormat :: String
, standaloneTypeMapping :: [(String, String)]
, standaloneFilename :: String
Expand All @@ -153,17 +174,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
127 changes: 24 additions & 103 deletions ogma-core/src/Language/Trans/Spec2Copilot.hs
View file
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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 "
Expand All @@ -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
Expand All @@ -129,20 +102,18 @@ 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)
Expand All @@ -165,73 +136,17 @@ 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 ++ ") " ++ "[]"
where
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 =
Expand Down Expand Up @@ -318,3 +233,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"
40 changes: 40 additions & 0 deletions ogma-core/templates/standalone/Copilot.hs
View file
Original file line number Diff line number Diff line change
@@ -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}}}"

0 comments on commit c984144

Please sign in to comment.