tamarin-prover 0.8.4.0 → 0.8.5.0
raw patch · 10 files changed
+136/−188 lines, 10 filesdep ~aesondep ~arraydep ~blaze-builder
Dependency ranges changed: aeson, array, blaze-builder, blaze-html, bytestring, conduit, containers, deepseq, directory, dlist, filepath, hamlet, http-types, lifted-base, monad-control, mtl, old-locale, safe, syb, tamarin-prover-term, tamarin-prover-theory, tamarin-prover-utils, threads, time, transformers, wai, warp, yesod-core, yesod-json, yesod-static
Files
- data/CHANGES +6/−0
- data/examples/ake/dh/client_session_key.aes +0/−1
- src/Main/Console.hs +1/−1
- src/Main/Mode/Interactive.hs +1/−1
- src/Main/TheoryLoader.hs +29/−79
- src/Web/Dispatch.hs +13/−10
- src/Web/Hamlet.hs +12/−9
- src/Web/Handler.hs +9/−8
- src/Web/Types.hs +33/−46
- tamarin-prover.cabal +32/−33
data/CHANGES view
@@ -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
− data/examples/ake/dh/client_session_key.aes
@@ -1,1 +0,0 @@-ÔZÀ[d'ám]ÌNÞÜælÎDùª-vóÃ]§ödTòDÿM}zSÒÕÈS>u¯·ëðU? kdmrõâg@cV42üújâ3kÉõ]PS
src/Main/Console.hs view
@@ -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"
src/Main/Mode/Interactive.hs view
@@ -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)
src/Main/TheoryLoader.hs view
@@ -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--}
src/Web/Dispatch.hs view
@@ -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
src/Web/Hamlet.hs view
@@ -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
src/Web/Handler.hs view
@@ -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
src/Web/Types.hs view
@@ -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
tamarin-prover.cabal view
@@ -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 <benedikt.schmidt@inf.ethz.ch>, Simon Meier <simon.meier@inf.ethz.ch> maintainer: Simon Meier <simon.meier@inf.ethz.ch>-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: