Skip to content

Commit

Permalink
Adding Maude version to --version option of Tamarin (tamarin-prover#550)
Browse files Browse the repository at this point in the history 
* Adding Maude version to --version option of Tamarin

* Removing useless comments and moving others comments
  • Loading branch information
@ValentinYuri
ValentinYuri committed Jun 23, 2023
1 parent 6bb7704 commit 8861567
Show file tree
Hide file tree
Showing 3 changed files with 123 additions and 113 deletions.
125 changes: 122 additions & 3 deletions src/Main/Console.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,13 @@ module Main.Console (

, helpAndExit

-- * Maude Version
, maudePath
, ensureMaude
, ensureMaudeAndGetVersion
, testProcess
, commandLine

-- * Argument parsing
, Arguments
, ArgKey
Expand Down Expand Up @@ -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

Expand All @@ -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
------------------------------------------------------------------------------
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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.
Expand Down
110 changes: 0 additions & 110 deletions src/Main/Environment.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
------------------------------------------------------------------------------
Expand All @@ -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"
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
]
1 change: 1 addition & 0 deletions src/Main/TheoryLoader.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 8861567

Please sign in to comment.