diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,24 @@ -2010-03-11 John D. Ramsdell +2010-03-30 John D. Ramsdell + * cpsa.cabal (Version): Tagged as version 2.0.3. + + * src/CPSA/Lib/Cohort.hs (useEncryptionFirstOrder): Added switch + to determine critical message search order. + + * src/CPSA/Lib/Strand.hs (skelNons, skelUniques): Use inheritRnon, + and inheritRunique for inherited origination assumptions. + +2010-03-27 John D. Ramsdell + + * src/pp.pl: Added an SWI-Prolog version of the pretty printer in + CPSA.Lib.Pretty. + + * src/cpsa.pl: Added an SWI-Prolog version of the CPSA specific + pretty printer in CPSA.Lib.Printer and support for skeleton + transformations. + +2010-03-11 John D. Ramsdell + * cpsa.cabal (Version): Tagged as version 2.0.2. * src/CPSA/Graph/Loader.hs (itrace): When computing the trace of @@ -9,6 +28,10 @@ * cpsa.cabal (Version): Tagged as version 2.0.1. +2010-03-10 John D. Ramsdell + + * src/cpsa.el: Added Emacs support for skeleton transformations. + 2010-03-07 John D. Ramsdell * src/CPSA/Basic/Algebra.hs (rootName): Improved renaming @@ -211,7 +234,7 @@ Two functions were added for printing terms is the operation field. These functions extend the display context as needed. -2009-08-05 John D. Ramsdell +2009-08-05 John D. Ramsdell * cpsa.cabal (Version): Tagged as version 1.4.8. diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -1,5 +1,19 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.0.3 + +** Generalization bug fixed +A bug associated with origination assumption forgetting has been +fixed. + +** SWI Prolog tools added +Tools that allows CPSA to be manipulated in Prolog are in the src +directory. The tools include a pretty printer that uses the same +algorithm as is used in the Haskell pretty printer. + +** Cabal description improved +An expanded description of CPSA has been added to its cabal file. + * Changes in version 2.0.2 ** Better message terms in graphs diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -1,19 +1,42 @@ Name: cpsa -Version: 2.0.2 +Version: 2.0.3 Maintainer: ramsdell@mitre.org Cabal-Version: >= 1.2 License: BSD3 License-File: license.txt Synopsis: Symbolic cryptographic protocol analyzer -Description: The Cryptographic Protocol Shapes Analyzer - (CPSA) attempts to enumerate all essentially - different executions possible for a - cryptographic protocol. We call them the - shapes of the protocol. Naturally occurring - protocols have only finitely many, indeed very - few shapes. Authentication and secrecy - properties are easy to determine from them, as - are attacks and anomalies. +Description: + The Cryptographic Protocol Shapes Analyzer (CPSA) attempts to + enumerate all essentially different executions possible for a + cryptographic protocol. We call them the shapes of the protocol. + Naturally occurring protocols have only finitely many, indeed very + few shapes. Authentication and secrecy properties are easy to + determine from them, as are attacks and anomalies. + . + For each input problem, the CPSA program is given some initial + behavior, and it discovers what shapes are compatible with it. + Normally, the initial behavior is from the point of view of one + participant. The analysis reveals what the other participants must + have done, given the participant's view. + . + We are working towards a version of CPSA with the property that + whenever it successfully terminates, every possible execution is + described by its output. However, the current implementation + occasionally fails to find some executions. + . + The package contains a set of programs used to perform and display + the analysis. Program documentation is in the doc directory in the + source distribution, and installed in the package's data directory. + You can locate the package's data directory by searching for the + file cpsauser.html. New users should study the documentation and + the sample inputs in the data directory. The source distribution + includes a test suite with an expanded set of input files and + program design documentation. + . + The theory and algorithm used by CPSA was developed with the help of + Joshua D. Guttman, John D. Ramsdell, Jon C. Herzog, Shaddin + F. Doghmi, F. Javier Thayer, and Paul D. Rowe. John D. Ramsdell + implemented the algorithm in Haskell. Category: Cryptography Build-Type: Simple Data-Files: @@ -26,24 +49,23 @@ -- ffgg.scm ns.scm or.scm woolam.scm yahalom.scm -- Data-Dir: doc Extra-Source-Files: - Makefile ChangeLog README NEWS ghci cpsatst doc/README - doc/Makefile doc/macros.tex doc/cpsaprimer.tex doc/bcasyntax.tex - doc/cpsaspec.tex doc/cpsadesign.tex doc/cpsaoverview.tex - doc/cpsadiagrams.mp doc/strands.mp doc/cmstrands.mp doc/carriers.mp - doc/termtree.mp doc/cpsa.bib doc/SDAG.lhs src/index.html - src/cpsacgi src/cpsacgi.py src/cpsa2svg src/cpsa.el - src/httpd_allow_execmem.te src/cpsaops.scm src/preskel - src/sexpr.pl tst/README tst/Makefile tst/Make.hs tst/checktst - tst/cpsagraphall tst/cpsashapesall tst/dass.lisp - tst/completeness-test.scm tst/completeness-test.tst - tst/missing-contraction.scm tst/missing-contraction.tst - tst/dass-mod.lisp tst/dass_simple.scm tst/dass_simple.tst - tst/denning-sacco.scm tst/denning-sacco.tst tst/dh.sch tst/dh.tst - tst/ds-short.lisp tst/dy.lsp tst/dy.tst tst/epmo_acctnum.lsp - tst/epmo_acctnum.tst tst/epmo.scm tst/encsig.scm tst/encsig.tst - tst/epmo.tst tst/ffgg.scm tst/ffgg.tst tst/isoreject.scm - tst/isoreject.tst tst/kelly1.scm tst/kelly1.tst tst/kelly64.lisp - tst/kerb5.lisp tst/kerberos.scm tst/kerberos.tst + Makefile ChangeLog README NEWS ghci cpsatst doc/README doc/Makefile + doc/macros.tex doc/cpsaprimer.tex doc/bcasyntax.tex doc/cpsaspec.tex + doc/cpsadesign.tex doc/cpsaoverview.tex doc/cpsadiagrams.mp + doc/strands.mp doc/cmstrands.mp doc/carriers.mp doc/termtree.mp + doc/cpsa.bib doc/SDAG.lhs src/index.html src/cpsacgi src/cpsacgi.py + src/cpsa2svg src/cpsa.el src/httpd_allow_execmem.te src/cpsaops.scm + src/preskel src/cpsa.pl src/pp.pl src/sexpr.pl + tst/README tst/Makefile tst/Make.hs tst/checktst tst/cpsagraphall + tst/cpsashapesall tst/dass.lisp tst/completeness-test.scm + tst/completeness-test.tst tst/missing-contraction.scm + tst/missing-contraction.tst tst/dass-mod.lisp tst/dass_simple.scm + tst/dass_simple.tst tst/denning-sacco.scm tst/denning-sacco.tst + tst/dh.sch tst/dh.tst tst/ds-short.lisp tst/dy.lsp tst/dy.tst + tst/epmo_acctnum.lsp tst/epmo_acctnum.tst tst/epmo.scm + tst/encsig.scm tst/encsig.tst tst/epmo.tst tst/ffgg.scm tst/ffgg.tst + tst/isoreject.scm tst/isoreject.tst tst/kelly1.scm tst/kelly1.tst + tst/kelly64.lisp tst/kerb5.lisp tst/kerberos.scm tst/kerberos.tst tst/neuman-stubblebine-alt.lisp tst/neuman-stubblebine-reauth.lisp tst/neuman-stubblebine-reauth.lsp tst/neuman-stubblebine-reauth.tst tst/neuman-stubblebine.scm tst/neuman-stubblebine.tst tst/nsl3.scm diff --git a/doc/cpsaoverview.pdf b/doc/cpsaoverview.pdf Binary files a/doc/cpsaoverview.pdf and b/doc/cpsaoverview.pdf differ diff --git a/doc/cpsaprimer.pdf b/doc/cpsaprimer.pdf Binary files a/doc/cpsaprimer.pdf and b/doc/cpsaprimer.pdf differ diff --git a/doc/cpsauser.html b/doc/cpsauser.html --- a/doc/cpsauser.html +++ b/doc/cpsauser.html @@ -23,7 +23,7 @@ are easy to determine from them, as are attacks and anomalies.

For each input problem, the CPSA program is given some initial behavior, and -it descovers what shapes are compatible with it. Normally, the initial behavior +it discovers what shapes are compatible with it. Normally, the initial behavior is from the point of view of one participant. The analysis reveals what the other participants must have done, given the participant's view. The search is based on a high-level algorithm shown to be complete, i.e. every shape can in @@ -50,7 +50,7 @@ href="#cpsapp">cpsapp program pretty prints its input using the CPSA specific algorithm.

-

The input syntax is essentially the same as the output systax. A Lisp aware +

The input syntax is essentially the same as the output syntax. A Lisp aware editor will pretty print input, and the output is pretty printed. We use Emacs' Scheme mode to prepare input. This document describes the syntax, but provides little assistance for its interpretation. See the CPSA Tutorial document for @@ -258,7 +258,7 @@ option +RTS -M512m -RTS limits memory usage to 512m.

For long running problems, SMP parallelism is available. For example, on a -quad-core machine, we would prrobably use +RTS -N4 -RTS.

+quad-core machine, we would probably use +RTS -N4 -RTS.

When run with isomorphism checks disabled (--noisochk), CPSA searches for realized skeletons, not shapes. It attempts to speed up analysis diff --git a/doc/macros.tex b/doc/macros.tex --- a/doc/macros.tex +++ b/doc/macros.tex @@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}} -\newcommand{\version}{2.0.1} +\newcommand{\version}{2.0.3} \newcommand{\cpsacopying}{\begingroup \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2009 The MITRE Corporation. Permission to copy without fee all or part of diff --git a/src/CPSA/Lib/Cohort.hs b/src/CPSA/Lib/Cohort.hs --- a/src/CPSA/Lib/Cohort.hs +++ b/src/CPSA/Lib/Cohort.hs @@ -191,6 +191,9 @@ else Just $ testNode k u ts der (graphNode n) t +useEncryptionFirstOrder :: Bool +useEncryptionFirstOrder = True + -- Look for a critical term that makes this node a test node. testNode :: Algebra t p g s e c => Preskel t p g s e c -> [t] -> Set t -> (t -> Bool) -> Node -> t -> @@ -207,8 +210,13 @@ loop cts else solveNode k ct ek n t escape - cts = map g (filter h (encryptions t)) ++ - map f (filter (flip carriedBy t) u) + cts = + if useEncryptionFirstOrder then + map g (filter h (encryptions t)) ++ + map f (filter (flip carriedBy t) u) + else + map f (filter (flip carriedBy t) u) ++ + map g (filter h (encryptions t)) f ct = (ct, Nothing) g (ct, ek) = (ct, Just ek) h (_, ek) = not (derivable ek) diff --git a/src/CPSA/Lib/Strand.hs b/src/CPSA/Lib/Strand.hs --- a/src/CPSA/Lib/Strand.hs +++ b/src/CPSA/Lib/Strand.hs @@ -1431,11 +1431,7 @@ skelNons k = filter (flip notElem ru) (knon k) where - ru = [u | i <- insts k, u <- roleNons i] - -roleNons :: Algebra t p g s e c => Instance t p g s e c -> [t] -roleNons i = - map (instantiate (env i) . snd) (rnon (role i)) + ru = [u | i <- insts k, u <- inheritRnon i] -- Uniquely-originating terms @@ -1452,11 +1448,7 @@ skelUniques k = filter (flip notElem ru) (kunique k) where - ru = [u | i <- insts k, u <- roleUniques i] - -roleUniques :: Algebra t p g s e c => Instance t p g s e c -> [t] -roleUniques i = - map (instantiate (env i)) (runique (role i)) + ru = [u | i <- insts k, u <- inheritRunique i] -- Variable separation diff --git a/src/CPSA/Lib/Utilities.hs b/src/CPSA/Lib/Utilities.hs --- a/src/CPSA/Lib/Utilities.hs +++ b/src/CPSA/Lib/Utilities.hs @@ -9,6 +9,7 @@ module CPSA.Lib.Utilities where import qualified Data.Set as S +import Data.List (foldl') adjoin :: Eq a => a -> [a] -> [a] adjoin x xs @@ -52,8 +53,8 @@ numbering = dfs adj (S.toList start) -- Remove nodes that have non-zero indegree start = S.difference (S.fromList nodes) (S.map fst edges) - edges = foldl f S.empty nodes - f edges src = foldl (g src) edges (adj src) + edges = foldl' f S.empty nodes + f edges src = foldl' (g src) edges (adj src) g src edges dst = S.insert (dst, src) edges -- Compute a depth first search numbering of nodes using postorder. @@ -63,14 +64,14 @@ dfs adj nodes = alist where - (_, alist, _) = foldl po (0, [], S.empty) nodes + (_, alist, _) = foldl' po (0, [], S.empty) nodes po a@(num, alist, seen) node | S.member node seen = a | otherwise = (num' + 1, (node, num') : alist', seen'') where -- Search is postorder because nodes at the end of (num', alist', seen'') = -- edges are explored before - foldl po (num, alist, seen') nodes' -- the node + foldl' po (num, alist, seen') nodes' -- the node seen' = S.insert node seen -- Insert node as soon as nodes' = adj node -- it's seen diff --git a/src/cpsa.pl b/src/cpsa.pl new file mode 100644 --- /dev/null +++ b/src/cpsa.pl @@ -0,0 +1,227 @@ +% -*- mode: prolog -*- + +%% CPSA tools in Prolog + +%% This module contains a Prolog implementation of the CPSA specific +%% S-expression pretty printer algorithm used in the Haskell program. +%% It also contains a translator between an S-expression and an +%% internal representation that eases transformations on CPSA data +%% structures. + +%% Known to work in SWI-Prolog, but not with GNU Prolog. + +%% Copyright (c) 2009 The MITRE Corporation +%% +%% This program is free software: you can redistribute it and/or +%% modify it under the terms of the BSD License as published by the +%% University of California. + +:- module(cpsa, [cpsa_sexprs_pp/2, cpsa/2, sexprs_to_cpsas/2, + cpsas_to_sexprs/2]). + +:- use_module(pp). +:- use_module(sexpr). + +%% cpsa_sexprs_pp(+Out, +Sexprs) +%% Pretty print a list of S-expressions to stream Out. +cpsa_sexprs_pp(_, []). +cpsa_sexprs_pp(Out, [Sexpr|Sexprs]) :- + cpsa_sexpr_pp(Out, Sexpr), + nl(Out), + cpsa_sexprs_pp(Out, Sexprs). + +cpsa_sexpr_pp(Out, Sexpr) :- + cpsa_sexpr_to_pretty(Sexpr, Pretty), + pp:pr(Out, 72, Pretty), + nl(Out). + +%% Create a pretty printing tree for each top-level CPSA form. +cpsa_sexpr_to_pretty([comment|X], Pretty) :- + sexpr:sexpr_to_pretty([comment|X], Pretty). +cpsa_sexpr_to_pretty([defskeleton|X], Pretty) :- + sexpr_to_cpsa_pretty([defskeleton|X], Pretty). +cpsa_sexpr_to_pretty([defprotocol, Name, Alg|Roles], Pretty) :- + pp:atm(defprotocol, X), + pp:atm(Name, Y), + pp:atm(Alg, Z), + pp:atm('(', P), + pp:atm(' ', S), + sexpr_to_role_pretty(Roles, Pretties), + pp:grp(2, [P, X, S, Y, S, Z, S|Pretties], Pretty). + +%% CPSA role specific pretty printing support. +sexpr_to_role_pretty([[defrole|X]|Roles], [Space, Pretty|Pretties]) :- + !, + pp:brk(1, Space), + sexpr_to_cpsa_pretty([defrole|X], Pretty), + sexpr_to_role_pretty(Roles, Pretties). +sexpr_to_role_pretty(Sexprs, Pretties) :- + sexprs_to_pretty(Sexprs, Pretties). + +%% Creates a group in which breaks are allowed only before lists. +sexpr_to_cpsa_pretty(Thing, Pretty) :- + atomic(Thing), + !, + sexpr:atom_to_pretty(Thing, Pretty). +sexpr_to_cpsa_pretty([Sexpr|Sexprs], Pretty) :- + pp:atm('(', First), + sexpr:sexpr_to_pretty(Sexpr, Second), + sexprs_to_cpsa_pretty(Sexprs, Rest), + pp:grp(2, [First, Second|Rest], Pretty). + +sexprs_to_cpsa_pretty([], [Pretty]) :- + pp:atm(')', Pretty). +sexprs_to_cpsa_pretty([Sexpr|Sexprs], [Space, Pretty|Pretties]) :- + atomic(Sexpr), + !, + pp:atm(' ', Space), + sexpr:sexpr_to_pretty(Sexpr, Pretty), + sexprs_to_cpsa_pretty(Sexprs, Pretties). +sexprs_to_cpsa_pretty([Sexpr|Sexprs], [Space, Pretty|Pretties]) :- + pp:brk(1, Space), + sexpr:sexpr_to_pretty(Sexpr, Pretty), + sexprs_to_cpsa_pretty(Sexprs, Pretties). + +%% Translate between S-expressions and an internal form. + +%% Currently, you have to read the code or look at output to +%% understand the internal form. + +cpsa(File, Cpsas) :- + sexpr:read_sexpr_list(File, Sexprs), + sexprs_to_cpsas(Sexprs, Cpsas). + +sexprs_to_cpsas([], []). +sexprs_to_cpsas([Sexpr|Sexprs], [Cpsa|Cpsas]) :- + sexpr_to_cpsa(Sexpr, Cpsa), + sexprs_to_cpsas(Sexprs, Cpsas). + +sexpr_to_cpsa([comment|X], c(X)). +sexpr_to_cpsa([defprotocol, Name, Alg|Rest], + p(Name, Alg, Roles)) :- + atom(Name), atom(Alg), + sexpr_to_roles(Rest, Roles). +sexpr_to_cpsa([defskeleton, Prot, [vars|Vars]|Rest], + k(Prot, Decls, Strands, Precedes, Nons, Uniqs)) :- + atom(Prot), + decls(Vars, Decls), + sexpr_to_strands(Rest, Strands, Alist), + lookup(precedes, Alist, Values), + edges(Values, Precedes), + lookup('non-orig', Alist, Nons), + lookup('uniq-orig', Alist, Uniqs). + +sexpr_to_roles([[defrole|Sexpr]|Rest], [Role|Roles]) :- + !, + sexpr_to_role(Sexpr, Role), + sexpr_to_roles(Rest, Roles). +sexpr_to_roles(_, []). + +sexpr_to_role([Name, [vars|Vars], [trace|Trace]|Alist], + r(Name, Decls, Trace, Nons, Uniqs)) :- + decls(Vars, Decls), + lookup('non-orig', Alist, Nons), + lookup('uniq-orig', Alist, Uniqs). + +sexpr_to_strands([[defstrand|Sexpr]|Rest], [Strand|Strands], Alist) :- + !, + sexpr_to_strand([defstrand|Sexpr], Strand), + sexpr_to_strands(Rest, Strands, Alist). +sexpr_to_strands([[deflistener|Sexpr]|Rest], [Strand|Strands], Alist) :- + !, + sexpr_to_strand([deflistener|Sexpr], Strand), + sexpr_to_strands(Rest, Strands, Alist). +sexpr_to_strands(Alist, [], Alist). + +sexpr_to_strand([defstrand, Role, Height|Sexprs], s(Role, Height, Map)) :- + atom(Role), + integer(Height), + maplets(Sexprs, Map). +sexpr_to_strand([deflistener, Term], l(Term)). + +decls([], []). +decls([Sexpr|Sexprs], [Decl|Decls]) :- + decl(Sexpr, Decl), + decls(Sexprs, Decls). + +decl(Sexprs, d(Type, Vars)) :- + decl_vars(Sexprs, Type, Vars). + +decl_vars([Type], Type, []) :- + !, + atom(Type). +decl_vars([Var|Decl], Type, [Var|Vars]) :- + atom(Var), + decl_vars(Decl, Type, Vars). + +maplets([], []). +maplets([[Key, Value]|Sexprs], [[Key|Value]|Map]) :- + maplets(Sexprs, Map). + +lookup(_, [], []). +lookup(Key, [[Key|Value]|Alist], Values) :- + !, + append(Value, Rest, Values), + lookup(Key, Alist, Rest). +lookup(Key, [[_|_]|Alist], Values) :- + lookup(Key, Alist, Values). + +edges([], []). +edges([Sexpr|Sexprs], [Edge|Edges]) :- + edge(Sexpr, Edge), + edges(Sexprs, Edges). + +edge([S0, S1], [N0|N1]) :- + node(S0, N0), + node(S1, N1). + +node([S, P], [S|P]) :- + integer(S), + integer(P). + +%% Translate the internal form to an S-expression. + +cpsas_to_sexprs([], []). +cpsas_to_sexprs([Cpsa|Cpsas], [Sexpr|Sexprs]) :- + cpsa_to_sexpr(Cpsa, Sexpr), + cpsas_to_sexprs(Cpsas, Sexprs). + +cpsa_to_sexpr(c(X), [comment|X]). +cpsa_to_sexpr(p(Name, Alg, Roles), [defprotocol, Name, Alg|Rest]) :- + roles_to_sexprs(Roles, Rest). +cpsa_to_sexpr(k(Prot, Decls, Strands, Precedes, Nons, Uniqs), + [defskeleton, Prot, [vars|Vars]|Rest]) :- + decls(Vars, Decls), + preds(Precedes, Nons, Uniqs, Alist), + strands_to_sexprs(Strands, Alist, Rest). + +preds([], Nons, Uniqs, Alist) :- + !, + origs(Nons, Uniqs, Alist). +preds(Precedes, Nons, Uniqs, [[precedes|Sexprs]|Alist]) :- + edges(Sexprs, Precedes), + origs(Nons, Uniqs, Alist). + +strands_to_sexprs([], Alist, Alist). +strands_to_sexprs([Strand|Strands], Alist, [Sexpr|Sexprs]) :- + sexpr_to_strand(Sexpr, Strand), + strands_to_sexprs(Strands, Alist, Sexprs). + +roles_to_sexprs([], []). +roles_to_sexprs([Role|Roles], [Sexpr|Sexprs]) :- + role_to_sexpr(Role, Sexpr), + roles_to_sexprs(Roles, Sexprs). + +role_to_sexpr(r(Name, Decls, Trace, Nons, Uniqs), + [defrole, Name, [vars|Vars], [trace|Trace]|Alist]) :- + decls(Vars, Decls), + origs(Nons, Uniqs, Alist). + +origs([], Uniqs, Alist) :- + !, + uniq_origs(Uniqs, Alist). +origs(Nons, Uniqs, [['non-orig'|Nons]|Alist]) :- + uniq_origs(Uniqs, Alist). + +uniq_origs([], []) :- !. +uniq_origs(Uniqs, [['uniq-orig'|Uniqs]]). diff --git a/src/pp.pl b/src/pp.pl new file mode 100644 --- /dev/null +++ b/src/pp.pl @@ -0,0 +1,176 @@ +% -*- mode: prolog -*- + +%% A simple pretty printer + +%% Construct a pretty printer tree using the tree constructors atm, +%% brk, blo, and grb, and then print it with pr. + +%% The alogithm is by Lawrence C. Paulson, who simplified an algorithm +%% by Derek C. Oppen. + +%% Derek C. Oppen, Prettyprinting, ACM Transactions on Programming +%% Languages and Systems, Vol 2, No. 4, October 1980, Pages 465-483. + +%% Copyright (c) 2009 The MITRE Corporation +%% +%% This program is free software: you can redistribute it and/or +%% modify it under the terms of the BSD License as published by the +%% University of California. + +%% A pretty printer based on ML programs with the following copyright + +%% (**** ML Programs from Chapter 8 of + +%% ML for the Working Programmer, 2nd edition +%% by Lawrence C. Paulson, Computer Laboratory, University of Cambridge. +%% (Cambridge University Press, 1996) + +%% Copyright (C) 1996 by Cambridge University Press. +%% Permission to copy without fee is granted provided that this copyright +%% notice and the DISCLAIMER OF WARRANTY are included in any copy. + +%% DISCLAIMER OF WARRANTY. These programs are provided `as is' without +%% warranty of any kind. We make no warranties, express or implied, that the +%% programs are free of error, or are consistent with any particular standard +%% of merchantability, or that they will meet your requirements for any +%% particular application. They should not be relied upon for solving a +%% problem whose incorrect solution could result in injury to a person or loss +%% of property. If you do use the programs or functions in such a manner, it +%% is at your own risk. The author and publisher disclaim all liability for +%% direct, incidental or consequential damages resulting from your use of +%% these programs or functions. +%% ****) + +% Known to work in SWI-Prolog, but not with GNU Prolog. + +:- module(pp, [atm/2, brk/2, blo/3, grp/3, pr/2, pr/3]). + +%% Pretty printer tree constructors + +%% Atoms (Strings str in the original code) +%% atm(+Atom, -Pretty) +atm(Atom, atm(Codes)) :- + atomic(Atom), + !, + atom_codes(Atom, Codes). +atm(Codes, atm(Codes)). + +%% Break points, where Len is the number of spaces to print when the +%% break is not turned into a newline break. +%% brk(+Len, -Pretty) +brk(Len, brk(Len)) :- + integer(Len). + +%% Indentation blocks (any number of breaks may be turned into a +%% newline break). +%% blk(+Indent, +Pretties, -Pretty) +blo(Indent, Pretties, blo(Pretties, Indent, Len)) :- + len(Pretties, Len). + +%% Indentation groups (all or none of the breaks are turned into +%% newline breaks) +%% grp(+Indent, +Pretties, -Pretty) +grp(Indent, Pretties, grp(Pretties, Indent, Len)) :- + len(Pretties, Len). + +% Compute the unbroken length of a list of pretty printing trees. +len(Pretties, Len) :- + len(Pretties, 0, Len). + +len([], Len, Len). +len([Pretty|Pretties], Start, Out) :- + size(Pretty, Len), + End is Start + Len, + len(Pretties, End, Out). + +size(atm(Codes), Len) :- + length(Codes, Len). +size(brk(Len), Len). +size(blo(_, _, Len), Len). +size(grp(_, _, Len), Len). + +%% After generating a pretty printing tree, print it + +%% pr(+Margin, +Pretty) +pr(Margin, Pretty) :- + current_output(Stream), + pr(Stream, Margin, Pretty). + +%% pr(+Stream, +Margin, +Pretty) +pr(Stream, Margin, Pretty) :- + printing(Stream, Margin, [Pretty], Margin, 0, false, Margin, _). + +%% Pretty print lists of trees +printing(_, _, [], _, _, _, Space, Space). +printing(Stream, Margin, [Pretty|Pretties], + Blockspace, After, Force, Start, End) :- + pretty_print(Stream, Margin, Pretty, Pretties, + Blockspace, After, Force, Start, Mid), + printing(Stream, Margin, Pretties, + Blockspace, After, Force, Mid, End). + +%% Print a string +pretty_print(Stream, _, atm(Codes), _, _, + _, _, Start, End) :- + put_codes(Stream, Codes), + length(Codes, Len), + End is Start - Len. +%% Print a break point without a newline break +pretty_print(Stream, _, brk(Len), Pretties, _, + After, false, Start, End) :- + break_dist(Pretties, After, Dist), + Len + Dist =< Start, + !, + put_blanks(Stream, Len), + End is Start - Len. +%% Print a break point with a newline break +pretty_print(Stream, Margin, brk(_), _, Blockspace, + _, _, _, Blockspace) :- + nl(Stream), + End is Margin - Blockspace, + put_blanks(Stream, End). +%% Print a block +pretty_print(Stream, Margin, blo(Body, Indent, _), Pretties, _, + After, _, Start, End) :- + New is Start - Indent, + break_dist(Pretties, After, Dist), + printing(Stream, Margin, Body, New, Dist, false, Start, End). +%% Print a group +pretty_print(Stream, Margin, grp(Body, Indent, Len), Pretties, _, + After, _, Start, End) :- + New is Start - Indent, + break_dist(Pretties, After, Dist), + (Len + Dist > Start -> Force = true; Force = false), + printing(Stream, Margin, Body, New, Dist, Force, Start, End). + +%% Find the distance to the next break point +break_dist([], After, After). +break_dist([atm(Codes)|Pretties], After, Dist) :- + break_dist(Pretties, After, Mid), + length(Codes, Len), + Dist is Mid + Len. +break_dist([brk(_)|_], _, 0). +break_dist([blo(_, _, Len)|Pretties], After, Dist) :- + break_dist(Pretties, After, Mid), + Dist is Mid + Len. +break_dist([grp(_, _, Len)|Pretties], After, Dist) :- + break_dist(Pretties, After, Mid), + Dist is Mid + Len. + +%% Printing primitives +put_blanks(Stream, Len) :- + 0 < Len, + !, + put_blank(Stream), + Next is Len - 1, + put_blanks(Stream, Next). +put_blanks(_, _). + +put_blank(Stream) :- + atom_codes(' ', Codes), + put_codes(Stream, Codes). + +put_codes(_, []). +put_codes(Stream, [Code|Codes]) :- + put_code(Stream, Code), + put_codes(Stream, Codes). diff --git a/src/sexpr.pl b/src/sexpr.pl --- a/src/sexpr.pl +++ b/src/sexpr.pl @@ -1,13 +1,27 @@ % -*- mode: prolog -*- -% Converts lists of character codes to Prolog style S-Expressions. +%% Converts lists of character codes to Prolog style S-Expressions and +%% generates pretty printer trees for S-expressions for use with the +%% exports of the pretty printer module pp. -% Known to work in SWI-Prolog, but not with GNU Prolog. +%% Known to work in SWI-Prolog, but not with GNU Prolog. The program +%% makes use of the non-standard atomic data type string to represent +%% strings in S-expressions. Atoms and integers in S-expressions are +%% mapped to Prolog standard atoms and numbers. -:- module(sexpr, - [codes_sexpr/2, codes_sexpr_list/2, sexpr_term/2, - read_sexpr_list/2, read_sexpr_term_list/2]). +%% Copyright (c) 2009 The MITRE Corporation +%% +%% This program is free software: you can redistribute it and/or +%% modify it under the terms of the BSD License as published by the +%% University of California. +:- module(sexpr, [codes_sexpr/2, codes_sexpr_list/2, sexpr_term/2, + read_sexpr_list/2, read_sexpr_term_list/2, atom_to_pretty/2, + sexpr_to_pretty/2, sexprs_to_pretty/2, + sexpr_to_group_pretty/2]). + +:- use_module(pp). + % codes_sexpr(+Codes, -Sexpr) % Convert a list of character codes to a Prolog style S-Expression. @@ -280,6 +294,7 @@ % Intrepret the character codes from a file as a list of S-Expressions. +%% read_sexpr_list(+Name, -Sexprs) read_sexpr_list(Name, Sexprs) :- read_file(Name, Codes), codes_sexpr_list(Codes, Sexprs). @@ -290,6 +305,57 @@ % in which lists that start with an atom have been converted to a % function application. +%% read_sexpr_list(+Name, -Terms) read_sexpr_term_list(Name, Terms) :- read_sexpr_list(Name, Sexprs), sexpr_term_list(Sexprs, Terms). + +%% Generates pretty printer trees for S-expressions. + +%% atom_to_pretty(+Sexpr, -Pretty) +atom_to_pretty([], Pretty) :- + !, + pp:atm('()', Pretty). +atom_to_pretty(Thing, Pretty) :- + string(Thing), + !, + atom_codes('"', Quote), + string_to_list(Thing, Codes), + append(Quote, Codes, X), + append(X, Quote, String), + pp:atm(String, Pretty). +atom_to_pretty(Thing, Pretty) :- + atomic(Thing), + pp:atm(Thing, Pretty). + +%% Creates blocks for all lists +%% sexpr_to_pretty(+Sexpr, -Pretty) +sexpr_to_pretty(Thing, Pretty) :- + atomic(Thing), + !, + atom_to_pretty(Thing, Pretty). +sexpr_to_pretty([Sexpr|Sexprs], Pretty) :- + pp:atm('(', First), + sexpr_to_pretty(Sexpr, Second), + sexprs_to_pretty(Sexprs, Rest), + pp:blo(2, [First, Second|Rest], Pretty). + +%% sexprs_to_pretty(+Sexprs, -Pretties) +sexprs_to_pretty([], [Pretty]) :- + pp:atm(')', Pretty). +sexprs_to_pretty([Sexpr|Sexprs], [Space, Pretty|Pretties]) :- + pp:brk(1, Space), + sexpr_to_pretty(Sexpr, Pretty), + sexprs_to_pretty(Sexprs, Pretties). + +%% Creates a group for the top-level list, and then blocks for all +%% interior lists. +%% sexpr_to_group_pretty(+Sexpr, -Pretty) +sexpr_to_group_pretty([Sexpr|Sexprs], Pretty) :- + !, + pp:atm('(', First), + sexpr_to_pretty(Sexpr, Second), + sexprs_to_pretty(Sexprs, Rest), + pp:grp(2, [First, Second|Rest], Pretty). +sexpr_to_group_pretty(Sexpr, Pretty) :- + sexpr_to_pretty(Sexpr, Pretty). diff --git a/tst/completeness-test.tst b/tst/completeness-test.tst --- a/tst/completeness-test.tst +++ b/tst/completeness-test.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol completeness-test basic diff --git a/tst/dass_simple.tst b/tst/dass_simple.tst --- a/tst/dass_simple.tst +++ b/tst/dass_simple.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol dass basic diff --git a/tst/denning-sacco.tst b/tst/denning-sacco.tst --- a/tst/denning-sacco.tst +++ b/tst/denning-sacco.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol denning-sacco basic diff --git a/tst/dh.tst b/tst/dh.tst --- a/tst/dh.tst +++ b/tst/dh.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol dhke diffie-hellman diff --git a/tst/dy.tst b/tst/dy.tst --- a/tst/dy.tst +++ b/tst/dy.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol dy basic diff --git a/tst/encsig.tst b/tst/encsig.tst --- a/tst/encsig.tst +++ b/tst/encsig.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol mult-keys-enc-sig basic diff --git a/tst/epmo.tst b/tst/epmo.tst --- a/tst/epmo.tst +++ b/tst/epmo.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol epmo basic diff --git a/tst/epmo_acctnum.tst b/tst/epmo_acctnum.tst --- a/tst/epmo_acctnum.tst +++ b/tst/epmo_acctnum.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol epmo_acctnum basic diff --git a/tst/ffgg.tst b/tst/ffgg.tst --- a/tst/ffgg.tst +++ b/tst/ffgg.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol ffgg basic diff --git a/tst/isoreject.tst b/tst/isoreject.tst --- a/tst/isoreject.tst +++ b/tst/isoreject.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol isoreject basic diff --git a/tst/kelly1.tst b/tst/kelly1.tst --- a/tst/kelly1.tst +++ b/tst/kelly1.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol kelly1 basic diff --git a/tst/kerberos.tst b/tst/kerberos.tst --- a/tst/kerberos.tst +++ b/tst/kerberos.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol kerberos basic diff --git a/tst/missing-contraction.tst b/tst/missing-contraction.tst --- a/tst/missing-contraction.tst +++ b/tst/missing-contraction.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol missing-contraction basic diff --git a/tst/neuman-stubblebine-reauth.tst b/tst/neuman-stubblebine-reauth.tst --- a/tst/neuman-stubblebine-reauth.tst +++ b/tst/neuman-stubblebine-reauth.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol neuman-stubblebine basic diff --git a/tst/neuman-stubblebine.tst b/tst/neuman-stubblebine.tst --- a/tst/neuman-stubblebine.tst +++ b/tst/neuman-stubblebine.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol neuman-stubblebine basic diff --git a/tst/ns.tst b/tst/ns.tst --- a/tst/ns.tst +++ b/tst/ns.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol ns basic diff --git a/tst/nsl3.tst b/tst/nsl3.tst --- a/tst/nsl3.tst +++ b/tst/nsl3.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol nsl3 basic diff --git a/tst/nsl4cm1.tst b/tst/nsl4cm1.tst --- a/tst/nsl4cm1.tst +++ b/tst/nsl4cm1.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol nsl4cm basic diff --git a/tst/nslsk.tst b/tst/nslsk.tst --- a/tst/nslsk.tst +++ b/tst/nslsk.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol nslsk basic diff --git a/tst/or.tst b/tst/or.tst --- a/tst/or.tst +++ b/tst/or.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol or basic diff --git a/tst/pca.tst b/tst/pca.tst --- a/tst/pca.tst +++ b/tst/pca.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol aic basic diff --git a/tst/sigenc.tst b/tst/sigenc.tst --- a/tst/sigenc.tst +++ b/tst/sigenc.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol mult-keys-sig-enc basic diff --git a/tst/sorted_epmo_acctnum.tst b/tst/sorted_epmo_acctnum.tst --- a/tst/sorted_epmo_acctnum.tst +++ b/tst/sorted_epmo_acctnum.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol epmo_acctnum basic diff --git a/tst/weird.tst b/tst/weird.tst --- a/tst/weird.tst +++ b/tst/weird.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol wierd basic diff --git a/tst/wmf.tst b/tst/wmf.tst --- a/tst/wmf.tst +++ b/tst/wmf.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol wide-mouth-frog basic diff --git a/tst/woolam.tst b/tst/woolam.tst --- a/tst/woolam.tst +++ b/tst/woolam.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol woolam basic diff --git a/tst/yahalom.tst b/tst/yahalom.tst --- a/tst/yahalom.tst +++ b/tst/yahalom.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.0.2") +(comment "CPSA 2.0.3") (comment "All input read") (defprotocol yahalom basic