From 9271cc762480001e502de91b2aff73ae4583f2eb Mon Sep 17 00:00:00 2001 From: ccremers Date: Mon, 18 Apr 2005 05:51:25 +0000 Subject: [PATCH] - Matching method propagation was wrong in new switch code. - Some fixes for protocols that do not include matching send/read combo's. In particular, the max encryption level method ranged over the sends; now over all events. Maybe it can range over read events only? --- src/arachne.c | 52 +++++++++++++++++++++++++++++++++++++------------- src/switches.c | 3 ++- src/term.c | 26 ++++++++++++++++++------- src/termlist.c | 6 ++---- 4 files changed, 62 insertions(+), 25 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index dfd4f5c..7d8c2df 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -562,13 +562,13 @@ proof_suppose_binding (Binding b) // Sub //------------------------------------------------------------------------ -//! Iterate over all send types in the roles (including the intruder ones) +//! Iterate over all events in the roles (including the intruder ones) /** * Function is called with (protocol pointer, role pointer, roledef pointer, index) * and returns an integer. If it is false, iteration aborts. */ int -iterate_role_sends (int (*func) ()) +iterate_role_events (int (*func) ()) { Protocol p; @@ -587,11 +587,8 @@ iterate_role_sends (int (*func) ()) index = 0; while (rd != NULL) { - if (rd->type == SEND) - { - if (!func (p, r, rd, index)) - return 0; - } + if (!func (p, r, rd, index)) + return 0; index++; rd = rd->next; } @@ -602,6 +599,29 @@ iterate_role_sends (int (*func) ()) return 1; } +//! Iterate over all send types in the roles (including the intruder ones) +/** + * Function is called with (protocol pointer, role pointer, roledef pointer, index) + * and returns an integer. If it is false, iteration aborts. + */ +int +iterate_role_sends (int (*func) ()) +{ + int send_wrapper (Protocol p, Role r, Roledef rd, int i) + { + if (rd->type == SEND) + { + return func (p,r,rd,i); + } + else + { + return 1; + } + } + + return iterate_role_events (send_wrapper); +} + //! Try to bind a specific existing run to a goal. /** * The key goals are bound to the goal. @@ -2969,8 +2989,16 @@ arachne () int determine_encrypt_max (Protocol p, Role r, Roledef rd, int index) { int tlevel; - + tlevel = term_encryption_level (rd->message); +#ifdef DEBUG + if (DEBUGL(3)) + { + eprintf ("Encryption level %i found for term ", tlevel); + termPrint (rd->message); + eprintf ("\n"); + } +#endif if (tlevel > max_encryption_level) max_encryption_level = tlevel; return 1; @@ -2995,18 +3023,16 @@ arachne () num_intruder_runs = 0; max_encryption_level = 0; - iterate_role_sends (determine_encrypt_max); - - fixAgentKeylevels (); - + iterate_role_events (determine_encrypt_max); #ifdef DEBUG if (DEBUGL (1)) { eprintf ("Maximum encryption level: %i\n", max_encryption_level); - iterate_role_sends (print_send); } #endif + fixAgentKeylevels (); + indentDepth = 0; proofDepth = 0; cl = sys->claimlist; diff --git a/src/switches.c b/src/switches.c index df0200e..6b8f224 100644 --- a/src/switches.c +++ b/src/switches.c @@ -12,10 +12,10 @@ #include "timer.h" extern System sys; +extern int mgu_match; extern struct tacnode *spdltac; extern Term TERM_Claim; -extern int mgu_match; const char *progname = "scyther"; const char *releasetag = SVNVERSION; @@ -219,6 +219,7 @@ switcher (const int process, const System sys, int index) else { sys->match = integer_argument (); + mgu_match = sys->match; return index; } } diff --git a/src/term.c b/src/term.c index 4949539..ff60804 100644 --- a/src/term.c +++ b/src/term.c @@ -1079,21 +1079,33 @@ term_rolelocals_are_variables () int term_encryption_level (const Term term) { - int iter_maxencrypt (Term term) + int iter_maxencrypt (Term t) { - term = deVar (term); - if (realTermLeaf (term)) + t = deVar (t); + if (t == NULL) + { +#ifdef DEBUG + if (DEBUGL(2)) + { + eprintf ("Warning: Term encryption level finds a NULL for term "); + termPrint (term); + eprintf ("\n"); + } +#endif + return 0; + } + if (realTermLeaf (t)) { return 0; } else { - if (realTermTuple (term)) + if (realTermTuple (t)) { int l, r; - l = iter_maxencrypt (TermOp1 (term)); - r = iter_maxencrypt (TermOp2 (term)); + l = iter_maxencrypt (TermOp1 (t)); + r = iter_maxencrypt (TermOp2 (t)); if (l > r) return l; else @@ -1102,7 +1114,7 @@ term_encryption_level (const Term term) else { // encrypt - return 1 + iter_maxencrypt (TermOp (term)); + return 1 + iter_maxencrypt (TermOp (t)); } } } diff --git a/src/termlist.c b/src/termlist.c index 30a7b11..8ed23ce 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -109,19 +109,17 @@ termlistDestroy (Termlist tl) //! Determine whether a term is an element of a termlist. /** - * Term must be non-null. + * The NULL term is not an element of any list. (Not even of the NULL list) * *@return True iff the term is an element of the termlist. */ __inline__ int inTermlist (Termlist tl, const Term term) { -#ifdef DEBUG if (term == NULL) { - error ("Trying to do inTermlist for a NULL term."); + return 0; } -#endif while (tl != NULL) { if (isTermEqual (tl->term, term))