diff --git a/data/CHANGES b/data/CHANGES --- a/data/CHANGES +++ b/data/CHANGES @@ -1,3 +1,9 @@ +* 0.8.5 Dropped support for GHC 7.0.x and GHC 7.2.x in favor of GHC 7.6.x + + - fix: faster and simpler variant computation + - fix: parse errors when loading files with non-ASCII characters from GUI + - fix: compiles with GHC 7.6.x + * 0.8.4 features: 1. irreducible function symbols are now allowed in formulas diff --git a/data/examples/ake/dh/client_session_key.aes b/data/examples/ake/dh/client_session_key.aes deleted file mode 100644 --- a/data/examples/ake/dh/client_session_key.aes +++ /dev/null @@ -1,1 +0,0 @@ -ÔZÀ[d'•ám]ÌNÞ܄ælΖDù›ª-vóÃ]§ödTòDÿM}zSÒÕÈS>u¯Ž·‘ëðU?…kdm”rõ⚆•šg@cV42üú†jâ3kÉõ]PS diff --git a/src/Main/Console.hs b/src/Main/Console.hs --- a/src/Main/Console.hs +++ b/src/Main/Console.hs @@ -73,7 +73,7 @@ [ programName , " " , showVersion version - , ", (C) Benedikt Schmidt, Simon Meier, ETH Zurich 2010-2012" + , ", (C) Benedikt Schmidt, Simon Meier, ETH Zurich 2010-2013" ] , "" , "This program comes with ABSOLUTELY NO WARRANTY. It is free software, and you" 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 @@ -94,7 +94,7 @@ ("Finished loading theories ... server ready at \n\n " ++ webUrl ++ "\n") cacheDir workDir (argExists "loadstate" as) (argExists "autosave" as) - (loadClosedWfThy as) (loadClosedThyString as) (closeThy as) + (loadClosedThyWfReport as) (loadClosedThyString as) (argExists "debug" as) dataDir (dotPath as) readImageFormat (constructAutoProver as) (runWarp port) diff --git a/src/Main/TheoryLoader.hs b/src/Main/TheoryLoader.hs --- a/src/Main/TheoryLoader.hs +++ b/src/Main/TheoryLoader.hs @@ -16,14 +16,12 @@ -- ** Loading and closing theories , loadClosedThy - , loadClosedWfThy + , loadClosedThyWfReport , loadClosedThyString -- ** Constructing automatic provers , constructAutoProver - , closeThy - -- ** Cached Message Deduction Rule Variants , dhIntruderVariantsFile , bpIntruderVariantsFile @@ -47,7 +45,7 @@ import System.Directory (doesFileExist) import Theory -import Theory.Text.Parser +import Theory.Text.Parser (parseIntruderRules, parseOpenTheory, parseOpenTheoryString) import Theory.Text.Pretty import Theory.Tools.AbstractInterpretation (EvaluationStyle(..)) import Theory.Tools.IntruderRules (specialIntruderRules, subtermIntruderRules @@ -87,21 +85,29 @@ "Define flags for pseudo-preprocessor." ] +-- | The defined pre-processor flags in the argument. +defines :: Arguments -> [String] +defines = findArg "defines" + +-- | Load an open theory from a file. loadOpenThy :: Arguments -> FilePath -> IO OpenTheory -loadOpenThy = fst . loadThy +loadOpenThy as = parseOpenTheory (defines as) +-- | Load a closed theory. loadClosedThy :: Arguments -> FilePath -> IO ClosedTheory -loadClosedThy = uncurry (>=>) . loadThy +loadClosedThy as inFile = loadOpenThy as inFile >>= closeThy as -loadClosedWfThy :: Arguments -> FilePath -> IO ClosedTheory -loadClosedWfThy as file = do - thy <- loadOpen file +-- | Load a close theory and report on well-formedness errors. +loadClosedThyWfReport :: Arguments -> FilePath -> IO ClosedTheory +loadClosedThyWfReport as inFile = do + thy <- loadOpenThy as inFile + -- report case checkWellformedness thy of - [] -> close thy + [] -> return () report -> do putStrLn "" putStrLn $ replicate 78 '-' - putStrLn $ "Theory file '" ++ file ++ "'" + putStrLn $ "Theory file '" ++ inFile ++ "'" putStrLn $ replicate 78 '-' putStrLn "" putStrLn $ "WARNING: ignoring the following wellformedness errors" @@ -109,55 +115,27 @@ putStrLn $ renderDoc $ prettyWfErrorReport report putStrLn $ replicate 78 '-' putStrLn "" - close thy - -- report -> error $ renderDoc $ prettyWfErrorReport report - where - (loadOpen, close) = loadThy as + -- return closed theory + closeThy as thy -loadClosedThyString :: Arguments -> String -> IO (Either String ClosedTheory) -loadClosedThyString as file = do - let (loader, closer) = loadThyString as - openThy <- loader file - case openThy of - Right thy -> Right <$> closer thy - Left err -> return $ Left err --- | Load an open/closed theory from a file. -loadThy :: Arguments -> (FilePath -> IO OpenTheory, OpenTheory -> IO ClosedTheory) -loadThy as = loadGenericThy (parseOpenTheory (defines as)) as - --- | Load an open/closed theory from a string. -loadThyString :: Arguments -> ( String -> IO (Either String OpenTheory) - , OpenTheory -> IO ClosedTheory) -loadThyString as = loadGenericThy loader as - where - loader str = - case parseOpenTheoryString (defines as) str of - Right thy -> return $ Right thy +loadClosedThyString :: Arguments -> String -> IO (Either String ClosedTheory) +loadClosedThyString as input = + case parseOpenTheoryString (defines as) input of Left err -> return $ Left $ "parse error: " ++ show err - --- | The defined pre-processor flags in the argument. -defines :: Arguments -> [String] -defines = findArg "defines" - --- FIXME: SM: This naming, tupling, blah is a mess and can be done more --- cleanly. DO IT! - --- | Load an open/closed theory given a loader function. -loadGenericThy :: a -> Arguments -> (a, OpenTheory -> IO ClosedTheory) -loadGenericThy loader as = - (loader, (closeThy as) <=< addMessageDeductionRuleVariants) + Right thy -> fmap Right $ closeThy as thy -- | Close a theory according to arguments. closeThy :: Arguments -> OpenTheory -> IO ClosedTheory -closeThy as = - fmap (proveTheory lemmaSelector prover . partialEvaluation) - . closeTheory (maudePath as) +closeThy as thy0 = do + thy1 <- addMessageDeductionRuleVariants thy0 -- FIXME: wf-check is at the wrong position here. Needs to be more -- fine-grained. - . wfCheck + let thy2 = wfCheck thy1 + -- close and prove + cthy <- closeTheory (maudePath as) thy2 + return $ proveTheory lemmaSelector prover $ partialEvaluation cthy where - -- apply partial application ---------------------------- partialEvaluation = case map toLower <$> findArg "partialEvaluation" as of @@ -257,31 +235,3 @@ (parseIntruderRules msig variantsFile) (error $ "could not find intruder message deduction theory '" ++ variantsFile ++ "'") -{- ------------------------------------------------------------------------------- --- Message deduction variants cached in files ------------------------------------------------------------------------------- - --- | The name of the intruder variants file. -intruderVariantsFile :: FilePath -intruderVariantsFile = "intruder_variants_dh.spthy" - --- | Add the variants of the message deduction rule. Uses the cached version --- of the @"intruder_variants_dh.spthy"@ file for the variants of the message --- deduction rules for Diffie-Hellman exponentiation. -addMessageDeductionRuleVariants :: OpenTheory -> IO OpenTheory -addMessageDeductionRuleVariants thy0 - | enableDH msig = do - variantsFile <- getDataFileName intruderVariantsFile - ifM (doesFileExist variantsFile) - (do dhVariants <- parseIntruderRulesDH variantsFile - return $ addIntrRuleACs dhVariants thy - ) - (error $ "could not find intruder message deduction theory '" - ++ variantsFile ++ "'") - | otherwise = return thy - where - msig = get (sigpMaudeSig . thySignature) thy0 - rules = subtermIntruderRules msig ++ specialIntruderRules - thy = addIntrRuleACs rules thy0 --} diff --git a/src/Web/Dispatch.hs b/src/Web/Dispatch.hs --- a/src/Web/Dispatch.hs +++ b/src/Web/Dispatch.hs @@ -1,3 +1,14 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TupleSections #-} + +-- FIXME: See how we can get rid of the Template Haskell induced warning, such +-- that we have the warning again for our code. +{-# OPTIONS_GHC -fno-warn-name-shadowing #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + {- | Module : Web.Dispatch Description : Yesod dispatch functions and default handlers. @@ -9,12 +20,6 @@ Portability : non-portable -} -{-# LANGUAGE MultiParamTypeClasses, OverloadedStrings, TemplateHaskell, TupleSections #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} --- FIXME: See how we can get rid of the Template Haskell induced warning, such --- that we have the warning again for our code. -{-# OPTIONS_GHC -fno-warn-name-shadowing #-} - module Web.Dispatch ( withWebUI , ImageFormat(..) @@ -39,7 +44,6 @@ import Control.Applicative import Control.Concurrent import Control.Monad -import Control.Monad.IO.Class import Data.List import Data.Maybe import Data.Time.LocalTime @@ -72,7 +76,7 @@ -> (FilePath -> IO ClosedTheory) -- ^ Theory loader (from file). -> (String -> IO (Either String ClosedTheory)) -- ^ Theory loader (from string). - -> (OpenTheory -> IO ClosedTheory) -- ^ Theory closer. + -- -> (OpenTheory -> IO ClosedTheory) -- ^ Theory closer. -> Bool -- ^ Show debugging messages? -> FilePath -- ^ Path to static content directory -> FilePath -- ^ Path to dot binary @@ -80,7 +84,7 @@ -> AutoProver -- ^ The default autoprover. -> (Application -> IO b) -- ^ Function to execute -> IO b -withWebUI readyMsg cacheDir_ thDir loadState autosave thLoader thParser thCloser debug' +withWebUI readyMsg cacheDir_ thDir loadState autosave thLoader thParser debug' stPath dotCmd' imgFormat' defaultAutoProver' f = do thy <- getTheos @@ -95,7 +99,6 @@ { workDir = thDir , cacheDir = cacheDir_ , parseThy = liftIO . thParser - , closeThy = thCloser , getStatic = st , theoryVar = thyVar , threadVar = thrVar diff --git a/src/Web/Hamlet.hs b/src/Web/Hamlet.hs --- a/src/Web/Hamlet.hs +++ b/src/Web/Hamlet.hs @@ -1,3 +1,12 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeSynonymInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + {- | Module : Web.Hamlet Description : Hamlet templates. @@ -9,11 +18,6 @@ Portability : non-portable -} -{-# LANGUAGE - TypeFamilies, QuasiQuotes, TypeSynonymInstances, - PatternGuards, FlexibleInstances, CPP #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} - module Web.Hamlet ( rootTpl , overviewTpl @@ -28,15 +32,14 @@ import Yesod.Core import Data.List -import qualified Data.Map as M +import qualified Data.Map as M import Data.Ord import Data.Time.Format -import Data.Version (showVersion) -import Text.Blaze.Html (preEscapedToMarkup) +import Data.Version (showVersion) import System.Locale -import Paths_tamarin_prover (version) +import Paths_tamarin_prover (version) -- -- Templates diff --git a/src/Web/Handler.hs b/src/Web/Handler.hs --- a/src/Web/Handler.hs +++ b/src/Web/Handler.hs @@ -57,7 +57,6 @@ import Yesod.Core import Yesod.Json() -import Data.Aeson import Data.Label import Data.Maybe import Data.String (fromString) @@ -70,11 +69,11 @@ import qualified Data.ByteString.Char8 as BS import qualified Data.Map as M import qualified Data.Text as T -import Data.Text.Encoding +import qualified Data.Text.Encoding as T (encodeUtf8, decodeUtf8) import qualified Data.Traversable as Tr import Network.HTTP.Types ( urlDecode ) -import Text.Blaze.Html5 (toHtml) + import Control.Applicative import Control.Concurrent import qualified Control.Concurrent.Thread as Thread ( forkIO ) @@ -82,8 +81,6 @@ import Control.Exception.Base import qualified Control.Exception.Lifted as E import Control.Monad -import Control.Monad.IO.Class -import Control.Monad.Trans.Control import qualified Data.Binary as Bin import Data.Time.LocalTime import System.Directory @@ -230,7 +227,7 @@ trace (info ++ ": exception `" ++ show e ++ "'") $ E.throwIO e -- | Helper functions for generating JSON reponses. -jsonResp :: JsonResponse -> GHandler m WebUI RepJson +jsonResp :: JsonResponse -> Handler RepJson jsonResp = return . RepJson . toContent . responseToJson responseToJson :: JsonResponse -> Value @@ -346,7 +343,7 @@ then setMessage "No theory file given." else do yesod <- getYesod - closedThy <- liftIO $ parseThy yesod (concatMap BS.unpack content) + closedThy <- liftIO $ parseThy yesod (T.unpack $ T.decodeUtf8 $ BS.concat content) case closedThy of Left err -> setMessage $ "Theory loading failed:\n" <> toHtml err Right thy -> do @@ -511,7 +508,7 @@ maybeKey <- lookupGetParam "path" case maybeKey of Just key0 -> do - let key = decodeUtf8 . urlDecode True . encodeUtf8 $ key0 + let key = T.decodeUtf8 . urlDecode True . T.encodeUtf8 $ key0 tryKillThread key return $ RepPlain $ toContent ("Canceled request!" :: T.Text) Nothing -> invalidArgs ["No path to kill specified!"] @@ -586,6 +583,8 @@ -} {- +SM: Path editing hs bitrotted. Re-enable/implement once we really need it. + -- | Get the add lemma page. getEditPathR :: TheoryIdx -> TheoryPath -> Handler RepJson getEditPathR = postEditPathR @@ -612,6 +611,8 @@ Nothing -> addLemma newLemma openThy Just _ -> removeLemma lemmaName openThy >>= addLemma newLemma + -- SM: Theory closing has to be implemented again. + -- Probably, the whole path editing has to be rethought. traverse (closeThy yesod) openThy') -- Error response (JsonAlert $ T.unwords diff --git a/src/Web/Types.hs b/src/Web/Types.hs --- a/src/Web/Types.hs +++ b/src/Web/Types.hs @@ -1,3 +1,12 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + {- | Module : Types.hs Description : Central data type and Yesod typeclass instances. @@ -9,10 +18,6 @@ Portability : non-portable -} -{-# LANGUAGE - OverloadedStrings, Rank2Types, QuasiQuotes, - TypeFamilies, TemplateHaskell, CPP #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} module Web.Types ( WebUI(..) @@ -37,37 +42,34 @@ ) where -import Theory -import Yesod.Core -import Yesod.Static - -import Text.Hamlet - +import Control.Applicative import Control.Concurrent import Data.Label +import qualified Data.Map as M import Data.Maybe (listToMaybe) import Data.Monoid (mconcat) import Data.Ord (comparing) +import qualified Data.Text as T import Data.Time.LocalTime -import qualified Data.Map as M -import qualified Data.Text as T +import Text.Hamlet +import Yesod.Core +import Yesod.Static --- import Control.Monad.IO.Class -import Control.Applicative +import Theory ------------------------------------------------------------------------------ -- Types ------------------------------------------------------------------------------ -- | Type synonym for a generic handler inside our site. --- type GenericHandler m = GHandler WebUI WebUI m --- type Handler a = GHandler WebUI WebUI a +-- type GenericHandler m = Handler WebUI WebUI m +-- type Handler a = Handler WebUI WebUI a -- | Type synonym for a generic widget inside our site. --- type GenericWidget m = GWidget WebUI (GenericHandler m) --- type Widget a = GWidget WebUI WebUI a +-- type GenericWidget m = Widget WebUI (GenericHandler m) +-- type Widget a = Widget WebUI WebUI a -- | Type synonym representing a numeric index for a theory. type TheoryIdx = Int @@ -94,30 +96,28 @@ -- information that can use to keep info that needs to be available to the -- handler functions. data WebUI = WebUI - { getStatic :: Static + { getStatic :: Static -- ^ Settings for static file serving. - , cacheDir :: FilePath + , cacheDir :: FilePath -- ^ The caching directory (for storing rendered graphs). - , workDir :: FilePath + , workDir :: FilePath -- ^ The working directory (for storing/loading theories). -- , parseThy :: MonadIO m => String -> GenericHandler m ClosedTheory - , parseThy :: String -> IO (Either String ClosedTheory) - -- ^ Parse a closed theory according to command-line arguments. - , closeThy :: OpenTheory -> IO ClosedTheory + , parseThy :: String -> IO (Either String ClosedTheory) -- ^ Close an open theory according to command-line arguments. - , theoryVar :: MVar TheoryMap + , theoryVar :: MVar TheoryMap -- ^ MVar that holds the theory map - , threadVar :: MVar ThreadMap + , threadVar :: MVar ThreadMap -- ^ MVar that holds the thread map , autosaveProofstate :: Bool -- ^ Automatically store theory map - , dotCmd :: FilePath + , dotCmd :: FilePath -- ^ The dot command - , imageFormat :: ImageFormat + , imageFormat :: ImageFormat -- ^ The image-format used for rendering graphs - , defaultAutoProver :: AutoProver + , defaultAutoProver :: AutoProver -- ^ The default prover to use for automatic proving. - , debug :: Bool + , debug :: Bool -- ^ Output debug messages } @@ -166,18 +166,6 @@ instance Ord TheoryInfo where compare = compareTI --- Adapted from the output of 'derive'. -instance Read CaseDistKind where - readsPrec p0 r - = readParen (p0 > 10) - (\ r0 -> - [(UntypedCaseDist, r1) | ("untyped", r1) <- lex r0]) - r - ++ - readParen (p0 > 10) - (\ r0 -> [(TypedCaseDist, r1) | ("typed", r1) <- lex r0]) - r - -- | Simple data type for specifying a path to a specific -- item within a theory. data TheoryPath @@ -339,10 +327,9 @@ -- Note: We define the default layout here even tough it doesn't really -- belong in the "types" module in order to avoid mutually recursive modules. -- defaultLayout' :: (Yesod master, Route master ~ WebUIRoute) --- => GWidget sub master () -- ^ Widget to embed in layout --- -> GHandler sub master RepHtml -defaultLayout' :: Yesod master => - GWidget sub master () -> GHandler sub master RepHtml +-- => Widget master () -- ^ Widget to embed in layout +-- -> Handler master RepHtml +defaultLayout' :: Widget -> Handler RepHtml defaultLayout' w = do page <- widgetToPageContent w message <- getMessage diff --git a/tamarin-prover.cabal b/tamarin-prover.cabal --- a/tamarin-prover.cabal +++ b/tamarin-prover.cabal @@ -1,14 +1,14 @@ cabal-version: >= 1.8 build-type: Simple name: tamarin-prover -version: 0.8.4.0 +version: 0.8.5.0 license: GPL license-file: LICENSE category: Theorem Provers author: Benedikt Schmidt , Simon Meier maintainer: Simon Meier -copyright: Benedikt Schmidt, Simon Meier, ETH Zurich, 2010-2012 +copyright: Benedikt Schmidt, Simon Meier, ETH Zurich, 2010-2013 synopsis: The Tamarin prover for security protocol analysis. description: @@ -82,7 +82,6 @@ examples/features/private_function_symbols/NAXOS_eCK_private.spthy -- newer AKE examples - examples/ake/dh/client_session_key.aes examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_keyreg_partially_matching.spthy examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching.spthy examples/ake/dh/NAXOS_eCK.spthy @@ -227,51 +226,51 @@ build-depends: bytestring >= 0.9 - , blaze-html == 0.5.* - , http-types == 0.7.* - , blaze-builder == 0.3.* - , yesod-core == 1.1.* - , yesod-json == 1.1.* - , yesod-static == 1.1.* - , conduit == 0.5.* + , blaze-html >= 0.5 + , http-types >= 0.7 + , blaze-builder >= 0.3 + , yesod-core >= 1.1 + , yesod-json >= 1.1 + , yesod-static >= 1.1 + , conduit >= 0.5 -- , yesod-form == 0.4.* -- required once we reactivate editing , text == 0.11.* - , wai == 1.3.* - , hamlet == 1.1.* - , warp == 1.3.* - , aeson == 0.6.* - , old-locale == 1.0.* - , monad-control == 0.3.* - , lifted-base == 0.1.* - , threads >= 0.4 && < 0.6 + , wai >= 1.3 + , hamlet >= 1.1 + , warp >= 1.3 + , aeson >= 0.6 + , old-locale == 1.* + , monad-control == 0.* + , lifted-base >= 0.2.0.5 + , threads >= 0.4 build-depends: base == 4.* - , bytestring == 0.9.* - , deepseq == 1.3.* - , array >= 0.3 && < 0.5 - , containers >= 0.4.2 && < 0.5 - , dlist == 0.5.* - , mtl == 2.0.* + , bytestring >= 0.9 + , deepseq >= 1.3 + , array >= 0.3 + , containers >= 0.4.2 + , dlist >= 0.5 + , mtl >= 2.1 , cmdargs == 0.10.* - , filepath >= 1.1 && < 1.4 - , directory >= 1.0 && < 1.2 + , filepath >= 1.1 + , directory >= 1.0 , process == 1.1.* , parsec == 3.1.* - , safe >= 0.2 && < 0.4 - , transformers == 0.2.* + , safe >= 0.2 + , transformers >= 0.3 , fclabels == 1.1.* , uniplate == 1.6.* - , syb == 0.3.* && >= 0.3.3 + , syb >= 0.3.3 , binary == 0.5.* , derive == 2.5.* - , time >= 1.2 && < 1.5 + , time >= 1.2 , parallel == 3.2.* , HUnit == 1.2.* - , tamarin-prover-utils >= 0.8.4 && < 0.9 - , tamarin-prover-term >= 0.8.4 && < 0.9 - , tamarin-prover-theory >= 0.8.4 && < 0.9 + , tamarin-prover-utils >= 0.8.5 && < 0.9 + , tamarin-prover-term >= 0.8.5 && < 0.9 + , tamarin-prover-theory >= 0.8.5 && < 0.9 other-modules: