From 8861567898a9c922bfe2dfeb700f1fe3370e482a Mon Sep 17 00:00:00 2001 From: ValentinYuri <135957879+ValentinYuri@users.noreply.github.com> Date: Fri, 23 Jun 2023 10:40:39 +0200 Subject: [PATCH] Adding Maude version to --version option of Tamarin (#550) * Adding Maude version to --version option of Tamarin * Removing useless comments and moving others comments --- src/Main/Console.hs | 125 ++++++++++++++++++++++++++++++++++++++- src/Main/Environment.hs | 110 ---------------------------------- src/Main/TheoryLoader.hs | 1 + 3 files changed, 123 insertions(+), 113 deletions(-) diff --git a/src/Main/Console.hs b/src/Main/Console.hs index 0b9b2f18d..9a7afa09a 100644 --- a/src/Main/Console.hs +++ b/src/Main/Console.hs @@ -22,6 +22,13 @@ module Main.Console ( , helpAndExit + -- * Maude Version + , maudePath + , ensureMaude + , ensureMaudeAndGetVersion + , testProcess + , commandLine + -- * Argument parsing , Arguments , ArgKey @@ -52,13 +59,19 @@ module Main.Console ( import Data.Maybe import Data.Version (showVersion) import Data.Time +import Data.List +import Data.Char (isSpace, toLower) import Safe import Control.Monad +import Control.Exception as E import System.Console.CmdArgs.Explicit import System.Console.CmdArgs.Text import System.Exit +import System.FilePath +import System.IO +import System.Process import qualified Text.PrettyPrint.Class as PP @@ -67,6 +80,112 @@ import Paths_tamarin_prover (version) import Language.Haskell.TH import Development.GitRev +------------------------------------------------------------------------------ +-- Maude version functions - previously in Environment.hs +------------------------------------------------------------------------------ + +-- | Path to maude tool +maudePath :: Arguments -> FilePath +maudePath = fromMaybe "maude" . findArg "withMaude" + +getVersionIO :: String -> IO String +getVersionIO maudeVersion = do + let tamarinVersion = showVersion version + let versionExport = "Generated from:\nTamarin version " ++ tamarinVersion + ++ "\nMaude version " ++ maudeVersion ++ gitVersion + ++ "\n" ++ compileTime + return versionExport + +commandLine :: String -> [String] -> String +commandLine prog args = unwords $ prog : args + +testProcess + :: (String -> String -> Either String String) + -- ^ Analysis of stdout, stderr. Use 'Left' to report error. + -> String -- ^ Default error message to display to the user. + -> String -- ^ Test description to display. + -> FilePath -- ^ Process to start + -> [String] -- ^ Arguments + -> String -- ^ Stdin + -> Bool -- ^ Whether to ignore ExitFailure + -> Bool -- ^ Whether Maude is being tested - hard fail for exceptions on Maude. + -> IO (Maybe String) -- ^ String with the process output, if test was successful +testProcess check defaultMsg testName prog args inp ignoreExitCode maudeTest = do + putStr testName + hFlush stdout + handle handler $ do + (exitCode, out, err) <- readProcessWithExitCode prog args inp + let errMsg reason = do + putStrLn reason + putStrLn $ "Detailed results from testing '" ++ prog ++ "'" + putStrLn $ " command: " ++ commandLine prog args + putStrLn $ " stdin: " ++ inp + putStrLn $ " stdout: " ++ out + putStrLn $ " stderr: " ++ err + return Nothing + + let check' = case check out err of + Left msg -> errMsg msg + Right msg -> do putStrLn msg + return (Just out) + + if not ignoreExitCode + then case exitCode of + ExitFailure code -> errMsg $ + "failed with exit code " ++ show code ++ "\n\n" ++ defaultMsg + ExitSuccess -> check' + else check' + + where + handler :: IOException -> IO (Maybe String) + handler _ = do putStrLn "caught exception while executing:" + putStrLn $ commandLine prog args + putStrLn $ "with input: " ++ inp + if maudeTest then + error "Maude is not installed. Ensure Maude is available and on the path." + else putStrLn "" + return Nothing + +ensureMaude :: Arguments -> IO (Maybe String) +ensureMaude as = do + putStrLn $ "maude tool: '" ++ maude ++ "'" + t1 <- testProcess checkVersion errMsg' " checking version: " maude ["--version"] "" False True + t2 <- testProcess checkInstall errMsg' " checking installation: " maude [] "quit\n" False True + return (if isNothing t1 || isNothing t2 then Nothing else t1) + where + maude = maudePath as + checkVersion out _ + | strip out `elem` supportedVersions = Right (strip out ++ ". OK.") + | otherwise = Left $ errMsg $ + " 'maude --version' returned unsupported version '" ++ strip out ++ "'" + + strip = reverse . dropWhile isSpace . reverse + + checkInstall _ [] = Right "OK." + checkInstall _ err = Left $ errMsg err + +-- Maude versions prior to 2.7.1 are no longer supported, +-- because the 'get variants' command is incompatible. + supportedVersions = ["2.7.1", "3.0", "3.1", "3.2.1", "3.2.2"] + + errMsg' = errMsg $ "'" ++ maude ++ "' executable not found / does not work" + + errMsg reason = unlines + [ "WARNING:" + , "" + , reason + , " Please install one of the following versions of Maude: " ++ intercalate ", " supportedVersions + ] + +-- Maude Version +ensureMaudeAndGetVersion :: Arguments -> IO String +ensureMaudeAndGetVersion as = do + -- Ensure Maude version and get Maude version + maybeMaudeVersion <- ensureMaude as + let maudeVersion = fromMaybe "Nothing" maybeMaudeVersion + -- Get String for version and put it in the arguments __version__ + getVersionIO maudeVersion + ------------------------------------------------------------------------------ -- Static constants for the tamarin-prover ------------------------------------------------------------------------------ @@ -103,8 +222,6 @@ versionStr = unlines , showVersion version , ", (C) David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, Benedikt Schmidt, ETH Zurich 2010-2020" ] - , gitVersion - , compileTime , "" , "This program comes with ABSOLUTELY NO WARRANTY. It is free software, and you" , "are welcome to redistribute it according to its LICENSE, see" @@ -205,7 +322,9 @@ tamarinMode name help adaptMode run0 = TamarinMode where run thisMode as | argExists "help" as = helpAndExit thisMode Nothing - | argExists "version" as = putStrLn versionStr + | argExists "version" as = do putStrLn versionStr + versionMaude <- ensureMaudeAndGetVersion as + putStrLn versionMaude | otherwise = run0 thisMode as -- | Disply help message of a tamarin mode and exit. diff --git a/src/Main/Environment.hs b/src/Main/Environment.hs index c3e3a47b6..185fb9b7c 100644 --- a/src/Main/Environment.hs +++ b/src/Main/Environment.hs @@ -27,27 +27,6 @@ import Main.Console import Data.Version (showVersion) import Paths_tamarin_prover (version) ------------------------------------------------------------------------------- --- Versions String ------------------------------------------------------------------------------- - --- | Get Version String by adding maude version -getVersionIO :: String -> IO String -getVersionIO maudeVersion = do - let tamarinVersion = showVersion version - let versionExport = "Generated from:\nTamarin version " ++ tamarinVersion - ++ "\nMaude version " ++ maudeVersion ++ gitVersion - ++ "\n" ++ compileTime - return versionExport - -ensureMaudeAndGetVersion :: Arguments -> IO String -ensureMaudeAndGetVersion as = do - -- Ensure Maude version and get Maude version - maybeMaudeVersion <- ensureMaude as - let maudeVersion = fromMaybe "Nothing" maybeMaudeVersion - -- Get String for version and put it in the arguments __version__ - getVersionIO maudeVersion - ------------------------------------------------------------------------------ -- Retrieving the paths to required tools. ------------------------------------------------------------------------------ @@ -60,10 +39,6 @@ toolFlags = , flagOpt "maude" ["with-maude"] (updateArg "withMaude") "FILE" "Path to 'maude' rewriting tool" ] --- | Path to maude tool -maudePath :: Arguments -> FilePath -maudePath = fromMaybe "maude" . findArg "withMaude" - -- | Path to dot tool dotPath :: Arguments -> FilePath dotPath = fromMaybe "dot" . findArg "withDot" @@ -99,59 +74,6 @@ getCpuModel = handler :: IOException -> IO String handler _ = return errMsg --- | Build the command line corresponding to a program arguments tuple. -commandLine :: String -> [String] -> String -commandLine prog args = unwords $ prog : args - --- | Test if a process is executable and check its response. This is used to --- determine the versions and capabilities of tools that we depend on. -testProcess - :: (String -> String -> Either String String) - -- ^ Analysis of stdout, stderr. Use 'Left' to report error. - -> String -- ^ Default error message to display to the user. - -> String -- ^ Test description to display. - -> FilePath -- ^ Process to start - -> [String] -- ^ Arguments - -> String -- ^ Stdin - -> Bool -- ^ Whether to ignore ExitFailure - -> Bool -- ^ Whether Maude is being tested - hard fail for exceptions on Maude. - -> IO (Maybe String) -- ^ String with the process output, if test was successful -testProcess check defaultMsg testName prog args inp ignoreExitCode maudeTest = do - putStr testName - hFlush stdout - handle handler $ do - (exitCode, out, err) <- readProcessWithExitCode prog args inp - let errMsg reason = do - putStrLn reason - putStrLn $ "Detailed results from testing '" ++ prog ++ "'" - putStrLn $ " command: " ++ commandLine prog args - putStrLn $ " stdin: " ++ inp - putStrLn $ " stdout: " ++ out - putStrLn $ " stderr: " ++ err - return Nothing - - let check' = case check out err of - Left msg -> errMsg msg - Right msg -> do putStrLn msg - return (Just out) - - if not ignoreExitCode - then case exitCode of - ExitFailure code -> errMsg $ - "failed with exit code " ++ show code ++ "\n\n" ++ defaultMsg - ExitSuccess -> check' - else check' - - where - handler :: IOException -> IO (Maybe String) - handler _ = do putStrLn "caught exception while executing:" - putStrLn $ commandLine prog args - putStrLn $ "with input: " ++ inp - if maudeTest then - error "Maude is not installed. Ensure Maude is available and on the path." - else putStrLn "" - return Nothing - -- | Ensure a suitable version of the Graphviz dot tool is installed. ensureGraphVizDot :: Arguments -> IO (Maybe String) ensureGraphVizDot as = do @@ -196,35 +118,3 @@ ensureGraphCommand as = do | otherwise = Left $ errMsg errMsg = unlines [ "Command not found" ] - --- | Ensure a suitable version of Maude is installed. If it is the case, send back the version otherwise Nothing. -ensureMaude :: Arguments -> IO (Maybe String) -ensureMaude as = do - putStrLn $ "maude tool: '" ++ maude ++ "'" - t1 <- testProcess checkVersion errMsg' " checking version: " maude ["--version"] "" False True - t2 <- testProcess checkInstall errMsg' " checking installation: " maude [] "quit\n" False True - return (if isNothing t1 || isNothing t2 then Nothing else t1) - where - maude = maudePath as - checkVersion out _ - | strip out `elem` supportedVersions = Right (strip out ++ ". OK.") - | otherwise = Left $ errMsg $ - " 'maude --version' returned unsupported version '" ++ strip out ++ "'" - - strip = reverse . dropWhile isSpace . reverse - - checkInstall _ [] = Right "OK." - checkInstall _ err = Left $ errMsg err - --- Maude versions prior to 2.7.1 are no longer supported, --- because the 'get variants' command is incompatible. - supportedVersions = ["2.7.1", "3.0", "3.1", "3.2.1", "3.2.2"] - - errMsg' = errMsg $ "'" ++ maude ++ "' executable not found / does not work" - - errMsg reason = unlines - [ "WARNING:" - , "" - , reason - , " Please install one of the following versions of Maude: " ++ intercalate ", " supportedVersions - ] diff --git a/src/Main/TheoryLoader.hs b/src/Main/TheoryLoader.hs index 417860785..f450ead9a 100644 --- a/src/Main/TheoryLoader.hs +++ b/src/Main/TheoryLoader.hs @@ -66,6 +66,7 @@ import qualified Sapic as Sapic import Main.Console (argExists, findArg, addEmptyArg, updateArg, Arguments) import Main.Environment +import Main.Console import Text.Parsec hiding ((<|>),try,parse) import Safe