Skip to content
Browse files

test: prover and parsing of proofs

  • Loading branch information...
1 parent 320965c commit d90d1a3b46d5e5efa40788a2b8517eb6a6c96233 @meiersi meiersi committed
View
2 src/Main/Mode/Intruder.hs
@@ -18,11 +18,11 @@ import System.Console.CmdArgs.Explicit as CmdArgs
import System.FilePath
import Theory
+import Theory.Text.Parser (intruderVariantsFile)
import Theory.Tools.IntruderRules
import Main.Console
import Main.Environment
-import Main.TheoryLoader (intruderVariantsFile)
import Main.Utils
View
32 src/Main/Mode/Test.hs
@@ -12,7 +12,6 @@ module Main.Mode.Test (
testMode
) where
-import Control.Applicative
import System.Console.CmdArgs.Explicit as CmdArgs
import System.Exit
import Test.HUnit (Counts(..), Test(..), runTestTT)
@@ -23,7 +22,8 @@ import Main.Console
import Main.Environment
import qualified Term.UnitTests as Term (tests)
-import qualified Theory.Text.Parser.UnitTests as Parser (testParseDirectory)
+import Theory
+import qualified Theory.Text.Parser.UnitTests as Parser
-- | Self-test mode.
@@ -55,19 +55,41 @@ run _thisMode as = do
#else
let successGraphVizDot = True
#endif
+ --------------------------------------------------------------------------
nextTopic "Testing the parser on our examples"
examplePath <- getDataFileName "examples"
- parseTests <- TestList <$> Parser.testParseDirectory 2 examplePath
- successParser <- runUnitTest parseTests
+ let mkParseTest = Parser.testParseFile Nothing
+ parseTests <- Parser.testParseDirectory mkParseTest 2 examplePath
+ successParser <- runUnitTest $ TestList parseTests
+ --------------------------------------------------------------------------
+ nextTopic "Testing the prover on some of our examples"
+
+ let heuristic = roundRobinHeuristic [SmartRanking False]
+ autoProver = AutoProver heuristic Nothing CutDFS
+ prover = Just ( maudePath as
+ , replaceSorryProver $ runAutoProver autoProver
+ )
+ mkProverTest file = do
+ fullFile <- getDataFileName file
+ return $ Parser.testParseFile prover fullFile
+
+ nslEx <- mkProverTest "examples/classic/NSLPK3.spthy"
+ loopEx <- mkProverTest "examples/loops/Minimal_Loop_Example.spthy"
+ diffieEx <- mkProverTest "examples/csf12/JKL_TS1_2008_KI.spthy"
+
+ successProver <- runUnitTest $ TestList [ nslEx, loopEx, diffieEx ]
+
+ --------------------------------------------------------------------------
nextTopic "Testing the unification infrastructure"
successTerm <- runUnitTest =<< Term.tests (maudePath as)
+ --------------------------------------------------------------------------
-- FIXME: Implement regression testing.
--
nextTopic "TEST SUMMARY"
let success = and [ successMaude, successGraphVizDot
- , successTerm, successParser ]
+ , successTerm, successParser, successProver ]
if success
then do putStrLn $ "All tests successful."
putStrLn $ "The " ++ programName ++ " should work as intended."
View
32 src/Main/TheoryLoader.hs
@@ -9,8 +9,7 @@
-- Theory loading infrastructure.
module Main.TheoryLoader (
-- * Static theory loading settings
- intruderVariantsFile
- , theoryLoadFlags
+ theoryLoadFlags
-- ** Loading open theories
, loadOpenThy
@@ -30,7 +29,6 @@ module Main.TheoryLoader (
import Prelude hiding (id, (.))
import Data.Char (toLower)
-import Data.Label
import Data.Monoid
import Control.Basics
@@ -38,31 +36,21 @@ import Control.Category
import Control.DeepSeq (rnf)
import System.Console.CmdArgs.Explicit
-import System.Directory
-
-import Extension.Prelude
import Theory
import Theory.Text.Parser
import Theory.Text.Pretty
import Theory.Tools.AbstractInterpretation (EvaluationStyle(..))
-import Theory.Tools.IntruderRules
import Theory.Tools.Wellformedness
import Main.Console
import Main.Environment
-import Paths_tamarin_prover (getDataFileName)
-
------------------------------------------------------------------------------
-- Theory loading: shared between interactive and batch mode
------------------------------------------------------------------------------
--- | The name of the intruder variants file.
-intruderVariantsFile :: FilePath
-intruderVariantsFile = "intruder_variants_dh.spthy"
-
-- | Flags for loading a theory.
theoryLoadFlags :: [Flag Arguments]
@@ -134,23 +122,7 @@ loadGenericThy :: (a -> IO OpenTheory)
-> Arguments
-> (a -> IO OpenTheory, OpenTheory -> IO ClosedTheory)
loadGenericThy loader as =
- (loader, (closeThy as) <=< tryAddIntrVariants)
- where
- -- intruder variants
- --------------------
- tryAddIntrVariants :: OpenTheory -> IO OpenTheory
- tryAddIntrVariants thy0 = do
- let msig = get (sigpMaudeSig . thySignature) thy0
- thy = addIntrRuleACs (subtermIntruderRules msig ++ specialIntruderRules) thy0
- if (enableDH msig) then
- do variantsFile <- getDataFileName intruderVariantsFile
- ifM (doesFileExist variantsFile)
- (do intrVariants <- parseIntruderRulesDH variantsFile
- return $ addIntrRuleACs intrVariants thy
- )
- (error $ "could not find intruder message deduction theory '"
- ++ variantsFile ++ "'")
- else return thy
+ (loader, (closeThy as) <=< addMessageDeductionRuleVariants)
-- | Close a theory according to arguments.
closeThy :: Arguments -> OpenTheory -> IO ClosedTheory
View
43 src/Theory.hs
@@ -1,5 +1,9 @@
-{-# LANGUAGE TemplateHaskell, TupleSections, DeriveFunctor #-}
-{-# LANGUAGE StandaloneDeriving, TypeSynonymInstances, FlexibleInstances #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeSynonymInstances #-}
-- |
-- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier
-- License : GPL v3 (see LICENSE)
@@ -42,8 +46,9 @@ module Theory (
, OpenTheory
, defaultOpenTheory
, addProtoRule
- , addIntrRuleACs
, applyPartialEvaluation
+ , addIntrRuleACs
+ , normalizeTheory
-- ** Closed theories
, ClosedTheory
@@ -88,7 +93,7 @@ module Theory (
) where
-import Prelude hiding ( (.), id )
+import Prelude hiding (id, (.))
import Data.Binary
import Data.DeriveTH
@@ -113,10 +118,9 @@ import Theory.Model
import Theory.Proof
import Theory.Text.Pretty
import Theory.Tools.AbstractInterpretation
+import Theory.Tools.InjectiveFactInstances
import Theory.Tools.LoopBreakers
import Theory.Tools.RuleVariants
-import Theory.Tools.InjectiveFactInstances
-
------------------------------------------------------------------------------
-- Specific proof types
@@ -439,6 +443,31 @@ addProtoRule ruE thy = do
addIntrRuleACs :: [IntrRuleAC] -> OpenTheory -> OpenTheory
addIntrRuleACs rs' = modify (thyCache) (\rs -> nub $ rs ++ rs')
+-- | Normalize the theory representation such that they remain semantically
+-- equivalent. Use this function when you want to compare two theories (quite
+-- strictly) for semantic equality; e.g., when testing the parser.
+normalizeTheory :: OpenTheory -> OpenTheory
+normalizeTheory =
+ L.modify thyCache sort
+ . L.modify thyItems (\items -> do
+ item <- items
+ return $ case item of
+ LemmaItem lem ->
+ LemmaItem $
+ L.set lFormulaAC Nothing $
+ L.modify lProof stripProofAnnotations $ lem
+ RuleItem _ -> item
+ TextItem _ -> item)
+ where
+ stripProofAnnotations :: ProofSkeleton -> ProofSkeleton
+ stripProofAnnotations = fmap stripProofStepAnnotations
+ stripProofStepAnnotations (ProofStep method ()) =
+ ProofStep (case method of
+ Sorry _ -> Sorry Nothing
+ Contradiction _ -> Contradiction Nothing
+ _ -> method)
+ ()
+
------------------------------------------------------------------------------
-- Closed theory querying / construction / modification
@@ -518,7 +547,7 @@ closeTheoryWithMaude sig thy0 = do
proveTheory checkProof $ Theory (L.get thyName thy0) sig cache items
where
cache = closeRuleCache typAsms sig rules $ L.get thyCache thy0
- checkProof = checkAndExtendProver (sorryProver "not yet proven")
+ checkProof = checkAndExtendProver (sorryProver Nothing)
-- Maude / Signature handle
hnd = L.get sigmMaudeHandle sig
View
5 src/Theory/Constraint/Solver/ProofMethod.hs
@@ -92,7 +92,7 @@ type CaseName = String
-- | Sound transformations of sequents.
data ProofMethod =
- Sorry String -- ^ Proof was not completed
+ Sorry (Maybe String) -- ^ Proof was not completed
| Solved -- ^ An attack was fond
| Simplify -- ^ A simplification step.
| SolveGoal Goal -- ^ A goal that was solved.
@@ -384,7 +384,8 @@ prettyProofMethod :: HighlightDocument d => ProofMethod -> d
prettyProofMethod method = case method of
Solved -> keyword_ "SOLVED" <-> lineComment_ "trace found"
Induction -> keyword_ "induction"
- Sorry reason -> fsep [keyword_ "sorry", lineComment_ reason]
+ Sorry reason ->
+ fsep [keyword_ "sorry", maybe emptyDoc lineComment_ reason]
SolveGoal goal ->
keyword_ "solve(" <-> prettyGoal goal <-> keyword_ ")"
Simplify -> keyword_ "simplify"
View
16 src/Theory/Proof.hs
@@ -181,12 +181,12 @@ type Proof a = LTree CaseName (ProofStep a)
--------------------
-- | A proof using the 'sorry' proof method.
-sorry :: String -> a -> Proof a
+sorry :: Maybe String -> a -> Proof a
sorry reason ann = LNode (ProofStep (Sorry reason) ann) M.empty
-- | A proof denoting an unproven part of the proof.
unproven :: a -> Proof a
-unproven = sorry "not yet proven"
+unproven = sorry Nothing
-- Paths in proofs
@@ -235,7 +235,7 @@ boundProofDepth bound =
where
go n (LNode ps@(ProofStep _ info) cs)
| 0 < n = LNode ps $ M.map (go (pred n)) cs
- | otherwise = sorry ("bound " ++ show bound ++ " hit") info
+ | otherwise = sorry (Just $ "bound " ++ show bound ++ " hit") info
-- | Fold a proof.
foldProof :: Monoid m => (ProofStep a -> m) -> Proof a -> m
@@ -324,7 +324,8 @@ checkProof ctxt prover d sys prf@(LNode (ProofStep method info) cs) =
(Sorry reason, _ ) -> sorryNode reason cs
(_ , Just cases) -> node method $ checkChildren cases
(_ , Nothing ) ->
- sorryNode "invalid proof step encountered" (M.singleton "" prf)
+ sorryNode (Just "invalid proof step encountered")
+ (M.singleton "" prf)
where
node m = LNode (ProofStep m (Just info, Just sys))
sorryNode reason cases = node (Sorry reason) (M.map noSystemPrf cases)
@@ -408,7 +409,7 @@ oneStepProver method = Prover $ \ctxt _ se _ -> do
return $ LNode (ProofStep method (Just se)) (M.map (unproven . Just) cases)
-- | Replace the current proof with a sorry step and the given reason.
-sorryProver :: String -> Prover
+sorryProver :: Maybe String -> Prover
sorryProver reason = Prover $ \_ _ se _ -> return $ sorry reason (Just se)
-- | Apply a prover only to a sub-proof, fails if the subproof doesn't exist.
@@ -427,7 +428,7 @@ checkAndExtendProver :: Prover -> Prover
checkAndExtendProver prover0 = Prover $ \ctxt d se prf ->
return $ mapProofInfo snd $ checkProof ctxt (prover ctxt) d se prf
where
- unhandledCase = sorry "unhandled case" Nothing
+ unhandledCase = sorry (Just "unhandled case") Nothing
prover ctxt d se =
fromMaybe unhandledCase $ runProver prover0 ctxt d se unhandledCase
@@ -462,7 +463,6 @@ contradictionProver = Prover $ \ctxt d sys prf ->
data SolutionExtractor = CutDFS | CutBFS | CutNothing
deriving( Eq, Ord, Show, Read )
-
data AutoProver = AutoProver
{ apHeuristic :: Heuristic
, apBound :: Maybe Int
@@ -566,7 +566,7 @@ cutOnSolvedBFS =
msg <- case st of
TraceFound -> return $ "ignored (attack exists)"
_ -> S.put IncompleteProof >> return "bound reached"
- return $ LNode (ProofStep (Sorry msg) x) M.empty
+ return $ LNode (ProofStep (Sorry (Just msg)) x) M.empty
checkLevel l prf@(LNode step cs)
| isNothing (psInfo step) = return prf
| otherwise = LNode step <$> traverse (checkLevel (l-1)) cs
View
63 src/Theory/Text/Parser.hs
@@ -11,29 +11,42 @@ module Theory.Text.Parser (
, parseOpenTheoryString
, parseLemma
, parseIntruderRulesDH
+
+ -- * Cached Message Deduction Rule Variants
+ , intruderVariantsFile
+ , addMessageDeductionRuleVariants
) where
-import Prelude hiding (id, (.))
+import Prelude hiding (id, (.))
-import qualified Data.ByteString.Char8 as BC
-import Data.Char (isUpper, toUpper)
-import Data.Foldable (asum)
+import qualified Data.ByteString.Char8 as BC
+import Data.Char (isUpper, toUpper)
+import Data.Foldable (asum)
import Data.Label
-import qualified Data.Map as M
-import Data.Monoid hiding (Last)
-import qualified Data.Set as S
+import qualified Data.Map as M
+import Data.Monoid hiding (Last)
+import qualified Data.Set as S
-import Control.Applicative hiding (empty, many, optional)
+import Control.Applicative hiding (empty, many, optional)
import Control.Category
import Control.Monad
-import Text.Parsec hiding ((<|>))
-import Text.PrettyPrint.Class (render)
+import Extension.Prelude (ifM)
+
+import Text.Parsec hiding ((<|>))
+import Text.PrettyPrint.Class (render)
+
+import Paths_tamarin_prover
+import System.Directory
import Term.Substitution
import Term.SubtermRule
import Theory
import Theory.Text.Parser.Token
+import Theory.Tools.IntruderRules
+
+
+
@@ -508,7 +521,7 @@ goal = asum
-- | Parse a proof method.
proofMethod :: Parser ProofMethod
proofMethod = asum
- [ symbol "sorry" *> pure (Sorry "not yet proven")
+ [ symbol "sorry" *> pure (Sorry Nothing)
, symbol "simplify" *> pure Simplify
, symbol "solve" *> (SolveGoal <$> parens goal)
, symbol "contradiction" *> pure (Contradiction Nothing)
@@ -648,3 +661,31 @@ theory flags0 = do
liftedAddLemma thy l = case addLemma l thy of
Just thy' -> return thy'
Nothing -> fail $ "duplicate lemma: " ++ get lName l
+
+
+------------------------------------------------------------------------------
+-- 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
View
52 src/Theory/Text/Parser/UnitTests.hs
@@ -18,25 +18,48 @@ import Control.Basics
import System.Directory
import System.FilePath
-import Theory (prettyOpenTheory)
+import Theory
import Theory.Text.Parser
import Theory.Text.Pretty (render)
-- | Test wether a given file exists, can be parsed, and can still be parsed
-- after being pretty printed.
-testParseFile :: FilePath -> Test
-testParseFile inpFile = TestLabel inpFile $ TestCase $ do
+testParseFile :: Maybe (FilePath, Prover)
+ -- ^ Path to maude and prover for testing whether proof parsing
+ -- works properly.
+ -> FilePath
+ -- ^ File on which to test parsing (and proving)
+ -> Test
+testParseFile optionalProver inpFile = TestLabel inpFile $ TestCase $ do
thyString <- readFile inpFile
- thy <- parse "original file:" thyString
- thy' <- parse "pretty printed theory:" (render $ prettyOpenTheory thy)
- assertEqual "parse . pretty" thy thy'
+ thy0 <- parse "original file:" thyString
+ -- add proofs and pretty print closed theory, if desired
+ (thy, thyPretty) <- case optionalProver of
+ Nothing ->
+ return (thy0, prettyOpenTheory thy0)
+ Just (maudePath, prover) -> do
+ closedThy <- proveTheory prover <$> closeTheory maudePath thy0
+ return $ ( normalizeTheory $ openTheory closedThy
+ , prettyClosedTheory closedThy)
+ thy' <- parse "pretty printed theory:" (render thyPretty)
+ unless (thy == thy') $ do
+ let (diff1, diff2) =
+ unzip $ dropWhile (uncurry (==)) $ zip (show thy) (show thy')
+ assertFailure $ unlines
+ [ "Original theory", "", render (prettyOpenTheory thy), ""
+ , "Pretty printed and parsed" , "", render (prettyOpenTheory thy'), ""
+ , "Original theory (diff)", "", indent diff1, ""
+ , "Pretty printed and parsed (diff)" , "", indent diff2, "", "DIFFER"
+ ]
+ return ()
where
+ indent = unlines . map (' ' :) . lines
+
parse msg str = case parseOpenTheoryString [] str of
Left err -> do assertFailure $ withLineNumbers $ indent $ show err
- return (error "testParseFile: not used")
- Right thy -> do return thy
+ return (error "testParseFile: dead code")
+ Right thy -> normalizeTheory <$> addMessageDeductionRuleVariants thy
where
- indent = unlines . map (' ' :) . lines
withLineNumbers err =
unlines $ zipWith (\i l -> nr (show i) ++ l) [(1::Int)..] ls
++ ["", "Parse error when parsing the " ++ msg, err]
@@ -47,8 +70,11 @@ testParseFile inpFile = TestLabel inpFile $ TestCase $ do
-- | Create the test whether 'testParseFile' succeeds on all @*.spthy@ files
-- in a given directory and all its subdirectories of depth n.
-testParseDirectory :: Int -> FilePath -> IO [Test]
-testParseDirectory n dir
+testParseDirectory :: (FilePath -> Test) -- ^ Test creation function.
+ -> Int -- ^ Maximal depth of traversal.
+ -> FilePath -- ^ Starting directory.
+ -> IO [Test]
+testParseDirectory mkTest n dir
| n < 0 = return []
| otherwise = do
rawContents <- getDirectoryContents dir
@@ -56,10 +82,10 @@ testParseDirectory n dir
| content <- rawContents
, content /= ".", content /= ".." ]
subDirs <- filterM doesDirectoryExist contents
- innerTests <- mapM (testParseDirectory (n - 1)) subDirs
+ innerTests <- mapM (testParseDirectory mkTest (n - 1)) subDirs
let tests = [ file
| file <- contents, takeExtension file == ".spthy" ]
mapM_ (putStrLn . (" peparing: " ++)) tests
- return $ map testParseFile tests ++ map TestList innerTests
+ return $ map mkTest tests ++ map TestList innerTests
View
2 src/Web/Handler.hs
@@ -641,7 +641,7 @@ getDeleteStepR idx path = do
go (TheoryProof lemma proofPath) ti = modifyTheory ti
(\thy -> return $
- applyProverAtPath thy lemma proofPath (sorryProver "removed"))
+ applyProverAtPath thy lemma proofPath (sorryProver (Just "removed")))
(const path)
(JsonAlert "Sorry, but removing the selected proof step failed!")
View
6 src/Web/Theory.hs
@@ -21,7 +21,6 @@ module Web.Theory
, prevThyPath
, nextSmartThyPath
, prevSmartThyPath
- , checkProofs
, applyMethodAtPath
, applyProverAtPath
)
@@ -67,11 +66,6 @@ import Web.Types
-- Various other functions
------------------------------------------------------------------------------
-checkProofs :: ClosedTheory -> ClosedTheory
-checkProofs = proveTheory checkedProver
- where
- checkedProver = checkAndExtendProver (sorryProver "not yet proven")
-
applyMethodAtPath :: ClosedTheory -> String -> ProofPath
-> Heuristic -- ^ How to extract/order the proof methods.
-> Int -- What proof method to use.

0 comments on commit d90d1a3

Please sign in to comment.
Something went wrong with that request. Please try again.