diff --git a/data/CHANGES b/data/CHANGES --- a/data/CHANGES +++ b/data/CHANGES @@ -1,3 +1,14 @@ +* 0.4.1.0 + - core prover: + - detect maude errors earlier + + - GUI + - support for SVG output + - the network interface for the webserver is configurable now + + - bugfixes: + - fix unit-test executed by 'test' mode + * 0.4.0.0 The version we used for our CSF'12 paper - core prover: diff --git a/interactive-only-src/Paths_tamarin_prover.hs b/interactive-only-src/Paths_tamarin_prover.hs --- a/interactive-only-src/Paths_tamarin_prover.hs +++ b/interactive-only-src/Paths_tamarin_prover.hs @@ -12,7 +12,7 @@ version :: Version -version = Version {versionBranch = [0,4,0,0], versionTags = []} +version = Version {versionBranch = [0,4,1,0], versionTags = []} bindir, libdir, datadir, libexecdir :: FilePath bindir = "./" diff --git a/src/Main/Console.hs b/src/Main/Console.hs --- a/src/Main/Console.hs +++ b/src/Main/Console.hs @@ -186,7 +186,7 @@ -- output example info when (tmIsMainMode tmode) $ do examplePath <- getDataFileName "examples" - manualPath <- getDataFileName "doc/MANUAL" + manualPath <- getDataFileName ("doc" "MANUAL") let tutorialPath = examplePath "stable" "Tutorial.spthy" csf12Path = examplePath "csf12" "*.spthy" csf12Cmd = programName ++ " --prove -Ocase-studies +RTS -N -RTS " ++ csf12Path diff --git a/src/Main/Environment.hs b/src/Main/Environment.hs --- a/src/Main/Environment.hs +++ b/src/Main/Environment.hs @@ -79,14 +79,16 @@ -- | 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, String) - -- ^ Analysis of stdout, stderr. Use 'Left' to report error. - -> String -- ^ Test description to display. - -> FilePath -- ^ Process to start - -> [String] -- ^ Arguments - -> String -- ^ Stdin - -> IO Bool -- ^ True, if test was successful -testProcess (check, defaultMsg) testName prog args inp = do +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 + -> IO Bool -- ^ True, if test was successful +testProcess check defaultMsg testName prog args inp = do putStr testName hFlush stdout handle handler $ do @@ -96,8 +98,8 @@ putStrLn $ "Detailed results from testing '" ++ prog ++ "'" putStrLn $ " command: " ++ commandLine prog args putStrLn $ " stdin: " ++ inp - putStrLn $ " stdout: " ++ out - putStrLn $ " stderr: " ++ err + putStrLn $ " stdout:\n" ++ out + putStrLn $ " stderr:\n" ++ err return False case exitCode of @@ -119,7 +121,7 @@ ensureGraphVizDot :: Arguments -> IO Bool ensureGraphVizDot as = do putStrLn $ "GraphViz tool: '" ++ dot ++ "'" - testProcess (check, errMsg) " checking version: " dot ["-V"] "" + testProcess check errMsg " checking version: " dot ["-V"] "" where dot = dotPath as check _ err @@ -138,14 +140,19 @@ ensureMaude :: Arguments -> IO Bool ensureMaude as = do putStrLn $ "maude tool: '" ++ maude ++ "'" - testProcess (check, errMsg') " checking version: " maude ["--version"] "" + t1 <- testProcess checkVersion errMsg' " checking version: " maude ["--version"] "" + t2 <- testProcess checkInstall errMsg' " checking installation: " maude [] "quit\n" + return (t1 && t2) where maude = maudePath as - check out _ + checkVersion out _ | filter (not . isSpace) out == "2.6" = Right "2.6. OK." | otherwise = Left $ errMsg $ " 'maude --version' returned wrong verison '" ++ out ++ "'" + checkInstall _ [] = Right "OK." + checkInstall _ err = Left $ errMsg err + errMsg' = errMsg $ "'" ++ maude ++ "' executable not found / does not work" errMsg reason = unlines [ "WARNING:" @@ -154,4 +161,5 @@ , " " ++ programName ++ " will likely not work." , " Please download 'Core Maude 2.6' from:" , " http://maude.cs.uiuc.edu/download/" + , " Note that 'prelude.maude' must be in the same directory as the 'maude' executable." ] diff --git a/src/Main/Mode/Interactive.hs b/src/Main/Mode/Interactive.hs --- a/src/Main/Mode/Interactive.hs +++ b/src/Main/Mode/Interactive.hs @@ -13,7 +13,10 @@ import Data.List import Data.Maybe +import Data.String (fromString) +import Data.Char (toLower) import Control.Basics +import Control.Exception (handle, IOException) import System.Console.CmdArgs.Explicit as CmdArgs import System.FilePath import System.Directory (doesFileExist, doesDirectoryExist) @@ -47,7 +50,9 @@ interactiveFlags = [ flagOpt "" ["port","p"] (updateArg "port") "PORT" "Port to listen on" - -- , flagOpt "" ["datadir"] (updateArg "datadir") "DATADIR" "Directory with data" + , flagOpt "" ["interface","i"] (updateArg "interface") "INTERFACE" + "Interface to listen on (use '*4' for all IPv4 interfaces)" + , flagOpt "" ["image-format"] (updateArg "image-format") "PNG|SVG" "image format used for graphs" , flagNone ["debug"] (addEmptyArg "debug") "Show server debugging output" -- , flagNone ["autosave"] (addEmptyArg "autosave") "Automatically save proof state" -- , flagNone ["loadstate"] (addEmptyArg "loadstate") "Load proof state if present" @@ -75,31 +80,24 @@ _ <- ensureMaude as putStrLn "" port <- readPort - dataDir <- readDataDir - let serverUrl = "http://127.0.0.1:" ++ show port + dataDir <- getDataDir + let webUrl = serverUrl (fromString interface) port putStrLn $ intercalate "\n" [ "The server is starting up on port " ++ show port ++ "." - , "Browse to " ++ serverUrl ++ " once the server is ready." + , "Browse to " ++ webUrl ++ " once the server is ready." , "" , "Loading the security protocol theories '" ++ workDir "*.spthy" ++ "' ..." ] withWebUI - ("Finished loading theories ... server ready at \n\n " ++ serverUrl ++ "\n") + ("Finished loading theories ... server ready at \n\n " ++ webUrl ++ "\n") workDir (argExists "loadstate" as) (argExists "autosave" as) (loadClosedWfThy as) (loadClosedThyString as) (closeThy as) - (argExists "debug" as) dataDir - (Warp.runSettings - (defaultSettings { settingsHost = Host "127.0.0.1", - settingsPort = port})) + (argExists "debug" as) dataDir (dotPath as) readImageFormat + (runWarp port) else helpAndExit thisMode (Just $ "directory '" ++ workDir ++ "' does not exist.") where - -- Datadir argument - readDataDir = - case findArg "datadir" as of - [d] -> return d - _ -> getDataDir -- Port argument ---------------- @@ -108,5 +106,32 @@ when (argExists "port" as && isNothing port) (putStrLn $ "Unable to read port from argument `" - ++fromMaybe "" (findArg "port" as)++"'. Using default.") + ++ fromMaybe "" (findArg "port" as) ++ "'. Using default.") return $ fromMaybe Web.Settings.defaultPort port + + -- Interface argument, we use 127.0.0.1 as default + -------------------------------------------------- + interface = fromMaybe "127.0.0.1" $ findArg "interface" as + + readImageFormat = case map toLower <$> findArg "image-format" as of + Just "svg" -> SVG + Just "png" -> PNG + Nothing -> PNG + _ -> error "image-format must be one of PNG|SVG" + + serverUrl host port = "http://" ++ hostString ++ ":" ++ show port + where + hostString = case host of + Host s -> s + _ -> "127.0.0.1" -- 127.0.0.1 should work for HostAny.. + + runWarp port wapp = + handle (\e -> err (e::IOException)) + (Warp.runSettings + (defaultSettings { settingsHost = fromString interface + , settingsPort = port}) + wapp) + + err e = error $ "Starting the webserver on "++interface++" failed: \n" + ++ show e + ++ "\nNote that you can use '--interface=\"*4\"' for binding to all interfaces." diff --git a/src/Theory/IntruderRules.hs b/src/Theory/IntruderRules.hs --- a/src/Theory/IntruderRules.hs +++ b/src/Theory/IntruderRules.hs @@ -111,7 +111,7 @@ then (`evalFresh` avoid ([rhs,t']++uprems')) $ do dfact <- kdFact Nothing t' ufacts <- mapM (kuFact Nothing) uprems' - concfact <- kdFact Nothing rhs + concfact <- kdFact (Just CanExp) rhs return [ Rule (DestrRule (BC.unpack f)) (dfact:ufacts) [concfact] [] ] else [] go _ (viewTerm -> Lit _) (_:_) = diff --git a/src/Web/Dispatch.hs b/src/Web/Dispatch.hs --- a/src/Web/Dispatch.hs +++ b/src/Web/Dispatch.hs @@ -16,7 +16,8 @@ {-# OPTIONS_GHC -fno-warn-name-shadowing #-} module Web.Dispatch - ( withWebUI + ( withWebUI + , ImageFormat(..) ) where @@ -72,9 +73,11 @@ -> (OpenTheory -> IO ClosedTheory) -- ^ Theory closer. -> Bool -- ^ Show debugging messages? -> FilePath -- ^ Path to static content directory + -> FilePath -- ^ Path to dot binary + -> ImageFormat -- ^ The preferred image format -> (Application -> IO b) -- ^ Function to execute -> IO b -withWebUI readyMsg thDir loadState autosave thLoader thParser thCloser debug' stPath f = do +withWebUI readyMsg thDir loadState autosave thLoader thParser thCloser debug' stPath dotCmd' imgFormat' f = do thy <- getTheos thrVar <- newMVar M.empty thyVar <- newMVar thy @@ -89,6 +92,8 @@ , theoryVar = thyVar , threadVar = thrVar , autosaveProofstate = autosave + , dotCmd = dotCmd' + , imageFormat = imgFormat' , debug = debug' } where diff --git a/src/Web/Handler.hs b/src/Web/Handler.hs --- a/src/Web/Handler.hs +++ b/src/Web/Handler.hs @@ -67,6 +67,7 @@ import Data.Maybe import Data.Aeson import Data.Label +import Data.String (fromString) -- import Data.Traversable (traverse) import qualified Data.Map as M @@ -453,12 +454,14 @@ yesod <- getYesod compact <- isNothing <$> lookupGetParam "uncompact" compress <- isNothing <$> lookupGetParam "uncompress" - png <- liftIO $ traceExceptions "getTheoryGraphR" $ - pngThyPath + img <- liftIO $ traceExceptions "getTheoryGraphR" $ + imgThyPath + (imageFormat yesod) + (dotCmd yesod) (workDir yesod) (graphStyle compact compress) (tiTheory ti) path - sendFile "image/png" png + sendFile (fromString . imageFormatMIME $ imageFormat yesod) img where graphStyle d c = dotStyle d . compression c dotStyle True = dotSequentCompact CompactBoringNodes diff --git a/src/Web/Theory.hs b/src/Web/Theory.hs --- a/src/Web/Theory.hs +++ b/src/Web/Theory.hs @@ -14,7 +14,7 @@ module Web.Theory ( htmlThyPath -- , htmlThyDbgPath - , pngThyPath + , imgThyPath , titleThyPath , theoryIndex , nextThyPath @@ -382,9 +382,9 @@ -} -- | Render the image corresponding to the given theory path. -pngThyPath :: FilePath -> (Sequent -> D.Dot ()) -> ClosedTheory +imgThyPath :: ImageFormat -> FilePath -> FilePath -> (Sequent -> D.Dot ()) -> ClosedTheory -> TheoryPath -> IO FilePath -pngThyPath dir compact thy path = go path +imgThyPath imgFormat dotCommand dir compact thy path = go path where go (TheoryCaseDist k i j) = renderDotCode (casesDotCode k i j) go (TheoryProof l p) = renderDotCode (proofPathDotCode l p) @@ -406,20 +406,22 @@ -- Render a piece of dot code renderDotCode code = do let dotPath = dir getDotPath code - pngPath = addExtension dotPath "png" + imgPath = addExtension dotPath (show imgFormat) - pngGenerated <- - firstSuccess [ doesFileExist pngPath - , writeFile dotPath code >> dotToPng "dot" dotPath pngPath - , dotToPng "fdp" dotPath pngPath ] - return (if pngGenerated then pngPath else imageDir ++ "/img/delete.png") + imgGenerated <- + firstSuccess [ doesFileExist imgPath + , writeFile dotPath code >> dotToImg "dot" dotPath imgPath + , dotToImg "fdp" dotPath imgPath ] + return (if imgGenerated then imgPath else imageDir ++ "/img/delete.png") - dotToPng dotCmd dotFile pngFile = do - (ecode,_out,err) <- readProcessWithExitCode dotCmd ["-Tpng","-o",pngFile,dotFile] "" + dotToImg dotMode dotFile imgFile = do + (ecode,_out,err) <- readProcessWithExitCode dotCommand + [ "-T"++show imgFormat, "-K"++dotMode, "-o",imgFile, dotFile] + "" case ecode of ExitSuccess -> return True ExitFailure i -> do - putStrLn $ "dotToPng: "++dotCmd++" failed with code " + putStrLn $ "dotToImg: "++dotCommand++" failed with code " ++show i++" for file "++dotFile++":\n"++err return False diff --git a/src/Web/Types.hs b/src/Web/Types.hs --- a/src/Web/Types.hs +++ b/src/Web/Types.hs @@ -33,6 +33,9 @@ , RenderUrl -- , GenericWidget , Widget + -- Image rendering + , ImageFormat(..) + , imageFormatMIME ) where @@ -77,6 +80,18 @@ -- | Type synonym representing a map of threads. type ThreadMap = M.Map T.Text ThreadId +-- | The image format used for rendering graphs. +data ImageFormat = PNG | SVG + +instance Show ImageFormat where + show PNG = "png" + show SVG = "svg" + +-- | convert image format to MIME type. +imageFormatMIME :: ImageFormat -> String +imageFormatMIME PNG = "image/png" +imageFormatMIME SVG = "image/svg+xml" + -- | The so-called site argument for our application, which can hold various -- information that can use to keep info that needs to be available to the -- handler functions. @@ -96,6 +111,10 @@ -- ^ MVar that holds the thread map , autosaveProofstate :: Bool -- ^ Automatically store theory map + , dotCmd :: FilePath + -- ^ The dot command + , imageFormat :: ImageFormat + -- ^ The image-format used for rendering graphs , debug :: Bool -- ^ Output debug messages } diff --git a/tamarin-prover.cabal b/tamarin-prover.cabal --- a/tamarin-prover.cabal +++ b/tamarin-prover.cabal @@ -1,7 +1,7 @@ cabal-version: >= 1.8 build-type: Simple name: tamarin-prover -version: 0.4.0.0 +version: 0.4.1.0 license: GPL license-file: LICENSE category: Theorem Provers @@ -195,8 +195,8 @@ , parallel == 3.2.* , HUnit == 1.2.* - , tamarin-prover-utils == 0.4.* - , tamarin-prover-term == 0.4.* + , tamarin-prover-utils == 0.4.1.* + , tamarin-prover-term == 0.4.1.* other-modules: