diff --git a/ogma-core/.hlint.yaml b/ogma-core/.hlint.yaml index 22e1ee4..cabbf1d 100644 --- a/ogma-core/.hlint.yaml +++ b/ogma-core/.hlint.yaml @@ -6,7 +6,5 @@ # We use data instead of newtype for uniformity. - ignore: { name: Use newtype instead of data - , within: [ Command.FRETReqsDB2Copilot - , Language.Trans.FRETReqsDB2Copilot - ] + , within: [ Command.FRETReqsDB2Copilot ] } diff --git a/ogma-core/ogma-core.cabal b/ogma-core/ogma-core.cabal index 5dc9ac1..7ba687b 100644 --- a/ogma-core/ogma-core.cabal +++ b/ogma-core/ogma-core.cabal @@ -92,7 +92,6 @@ library Language.Trans.CStruct2CopilotStruct Language.Trans.CStructs2Copilot Language.Trans.CStructs2MsgHandlers - Language.Trans.FRETReqsDB2Copilot Language.Trans.Spec2Copilot Language.Trans.SMV2Copilot @@ -114,7 +113,6 @@ library , ogma-language-c >= 1.2.0 && < 1.3 , ogma-language-cocospec >= 1.2.0 && < 1.3 , ogma-language-copilot >= 1.2.0 && < 1.3 - , ogma-language-fret-reqs >= 1.2.0 && < 1.3 , ogma-language-jsonspec >= 1.2.0 && < 1.3 , ogma-language-smv >= 1.2.0 && < 1.3 , ogma-spec >= 1.2.0 && < 1.3 diff --git a/ogma-core/src/Command/FRETReqsDB2Copilot.hs b/ogma-core/src/Command/FRETReqsDB2Copilot.hs index daa8c97..ee6d100 100644 --- a/ogma-core/src/Command/FRETReqsDB2Copilot.hs +++ b/ogma-core/src/Command/FRETReqsDB2Copilot.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE ExistentialQuantification #-} -- Copyright 2020 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- @@ -30,9 +31,6 @@ -- -- | 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(..) @@ -43,21 +41,31 @@ module Command.FRETReqsDB2Copilot -- External imports import Control.Monad.IfElse ( awhen ) import Data.Aeson ( eitherDecode ) +import Data.List ( nub, (\\) ) -- 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) - ) +-- Internal imports: Generic specification, parser. +import Data.OgmaSpec (ExternalVariableDef (..), + InternalVariableDef (..), Requirement (..), + Spec (..)) +import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec) + +-- Internal imports: language ASTs, transformers +import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec (myLexer, pBoolSpec) +import qualified Language.SMV.ParSMV as SMV (myLexer, pBoolSpec) +import Language.SMV.Substitution (substituteBoolExpr) + +import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec (boolSpec2Copilot, + boolSpecNames) +import Language.Trans.SMV2Copilot as SMV (boolSpec2Copilot, + boolSpecNames) +import Language.Trans.Spec2Copilot (spec2Copilot, specAnalyze) -- | Print the contents of a Copilot module that implements the Past-time TL -- formula in a FRET file. @@ -71,24 +79,50 @@ fretReqsDB2Copilot :: FilePath -- ^ Path to a file containing a FRET -> 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 +fretReqsDB2Copilot fp options = do - -- Extract internal command options from external command options - let internalOptions = fretReqsDB2CopilotOptions useCoCoSpec + let functions = fretExprPair (fretReqsDB2CopilotUseCoCoSpec options) - let copilot = T.fret2CopilotModule internalOptions =<< headEither =<< fret + copilot <- fretReqsDB2Copilot' fp options functions let (mOutput, result) = - fretReqsDB2CopilotResult useCoCoSpec fp copilot + fretReqsDB2CopilotResult options fp copilot awhen mOutput putStrLn return result +-- | Print the contents of a Copilot module that implements the Past-time TL +-- formula in a FRET file, using a subexpression handler. +-- +-- 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 + -> FRETReqsDB2CopilotOptions + -> FRETExprPair + -> IO (Either String String) +fretReqsDB2Copilot' fp options (FRETExprPair parse replace showExpr ids) = do + let name = fretReqsDB2CopilotFilename options + useCoCoSpec = fretReqsDB2CopilotUseCoCoSpec options + typeMaps = [("", "_")] + + -- 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. + content <- B.safeReadFile fp + res <- case content of + Left s -> return $ Left s + Right b -> return $ parseJSONSpec parse (fretFormat useCoCoSpec) =<< eitherDecode b + + -- Complement the specification with any missing/implicit definitions + let res' = fmap (addMissingIdentifiers ids) res + + let copilot = + spec2Copilot name typeMaps replace showExpr =<< specAnalyze =<< res' + + return copilot + -- | Options used to customize the conversion of FRET Requirements Database -- to Copilot code. data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions @@ -96,17 +130,6 @@ data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions , fretReqsDB2CopilotFilename :: String } --- | 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. @@ -119,17 +142,6 @@ type ErrorCode = Int 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) - (fretReqsDB2CopilotFilename options) - -- * Result -- | Process the result of the transformation function. @@ -137,6 +149,65 @@ fretReqsDB2CopilotResult :: FRETReqsDB2CopilotOptions -> FilePath -> Either String String -> (Maybe String, Result ErrorCode) -fretReqsDB2CopilotResult options fp result = case result of +fretReqsDB2CopilotResult _options fp result = case result of Left msg -> (Nothing, Error ecFretReqsDBError msg (LocationFile fp)) Right t -> (Just t, Success) + +-- * Parser + +-- | JSONPath selectors for a FRET file +fretFormat :: Bool -> JSONFormat +fretFormat useCoCoSpec = JSONFormat + { specInternalVars = Nothing + , specInternalVarId = "" + , specInternalVarExpr = "" + , specInternalVarType = Nothing + , specExternalVars = Just ".semantics.variables..*.*" + , specExternalVarId = "" + , specExternalVarType = Nothing + , specRequirements = "$[:]" + , specRequirementId = ".reqid" + , specRequirementDesc = Just ".fulltext" + , specRequirementExpr = if useCoCoSpec then ".semantics.CoCoSpecCode" else ".semantics.ptExpanded" + } + +-- * Handler for boolean expressions + +-- | Handler for boolean expressions that knows how to parse them, replace +-- variables in them, and convert them to Copilot. +data FRETExprPair = forall a . FRETExprPair + { exprParse :: String -> Either String a + , exprReplace :: [(String, String)] -> a -> a + , exprPrint :: a -> String + , exprIdents :: a -> [String] + } + +-- | Return a handler depending on whether it should be for CoCoSpec boolean +-- expressions or for SMV boolean expressions. +fretExprPair :: Bool -> FRETExprPair +fretExprPair True = FRETExprPair (CoCoSpec.pBoolSpec . CoCoSpec.myLexer) + (\_ -> id) + (CoCoSpec.boolSpec2Copilot) + (CoCoSpec.boolSpecNames) +fretExprPair False = FRETExprPair (SMV.pBoolSpec . SMV.myLexer) + (substituteBoolExpr) + (SMV.boolSpec2Copilot) + (SMV.boolSpecNames) + +-- | Add to a spec external variables for all identifiers mentioned in +-- expressions that are not defined anywhere. +addMissingIdentifiers :: (a -> [String]) -> Spec a -> Spec a +addMissingIdentifiers f s = s { externalVariables = vars' } + where + vars' = externalVariables s ++ newVars + newVars = map (\n -> ExternalVariableDef n "") newVarNames + + -- Names that are not defined anywhere + newVarNames = identifiers \\ existingNames + + -- Identifiers being mentioned in the requirements. + identifiers = nub $ concatMap (f . requirementExpr) (requirements s) + + -- Names that are defined in variables. + existingNames = map externalVariableName (externalVariables s) + ++ map internalVariableName (internalVariables s) diff --git a/ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs b/ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs deleted file mode 100644 index 4de2650..0000000 --- a/ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs +++ /dev/null @@ -1,169 +0,0 @@ --- 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 - , fretReqsDB2CopilotFilename :: String - } - --- | 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, tpre, spec - , main' - ] - - | otherwise - = [ imports, propDef, externs, clock, ftp, tpre, 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 qualified Copilot.Library.MTL as MTL" - , "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" - ] - - tpre = [ "" - , "tpre :: Stream Bool -> Stream Bool" - , "tpre = ([True] ++)" - ] - - 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 \"" - ++ fretReqsDB2CopilotFilename prefs ++ "\"" - ]