tamarin-prover 0.4.0.0 → 0.4.1.0
raw patch · 11 files changed
+124/−51 lines, 11 filesdep ~tamarin-prover-termdep ~tamarin-prover-utils
Dependency ranges changed: tamarin-prover-term, tamarin-prover-utils
Files
- data/CHANGES +11/−0
- interactive-only-src/Paths_tamarin_prover.hs +1/−1
- src/Main/Console.hs +1/−1
- src/Main/Environment.hs +21/−13
- src/Main/Mode/Interactive.hs +40/−15
- src/Theory/IntruderRules.hs +1/−1
- src/Web/Dispatch.hs +7/−2
- src/Web/Handler.hs +6/−3
- src/Web/Theory.hs +14/−12
- src/Web/Types.hs +19/−0
- tamarin-prover.cabal +3/−3
data/CHANGES view
@@ -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:
interactive-only-src/Paths_tamarin_prover.hs view
@@ -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 = "./"
src/Main/Console.hs view
@@ -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
src/Main/Environment.hs view
@@ -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." ]
src/Main/Mode/Interactive.hs view
@@ -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."
src/Theory/IntruderRules.hs view
@@ -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 _) (_:_) =
src/Web/Dispatch.hs view
@@ -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
src/Web/Handler.hs view
@@ -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
src/Web/Theory.hs view
@@ -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
src/Web/Types.hs view
@@ -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 }
tamarin-prover.cabal view
@@ -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: