From 131ee69f1d25b74d09d93f511a528628d414b700 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Sun, 4 Nov 2018 23:06:24 +0100 Subject: [PATCH] Removed another straightforward trampoline with one nested call only. --- src/TODO-trampolines.txt | 2 - src/prune_theorems.c | 102 ++++++++++++++++++++------------------- src/system.c | 9 +++- src/system.h | 3 +- 4 files changed, 61 insertions(+), 55 deletions(-) diff --git a/src/TODO-trampolines.txt b/src/TODO-trampolines.txt index e34f389..06a961b 100644 --- a/src/TODO-trampolines.txt +++ b/src/TODO-trampolines.txt @@ -2,7 +2,6 @@ 1 subtermUnify arachne.c +961 1 term_iterate_open_leaves dotout.c +1790 // Could be replaced by term_iterate_leaves 3 unify mgu.c +233 ; mgu.c +247 ; mgu.c +281 -1 iterateLocalToOther prune_theorems.c +108 term_iterate_leaves term_iterate_state_leaves @@ -13,5 +12,4 @@ iterateTermOther is called using makeDepend and addOther subtermUnify is called using unifiesWithKeys term_iterate_open_leaves is called using addsubterms unify is called using unify_combine_enc and unify_combined_tup, and a callback using the keys list? (which propagates back to subtermunify data) -iterateLocalToOther is called using checkTerm diff --git a/src/prune_theorems.c b/src/prune_theorems.c index 546f45d..54852d8 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -41,6 +41,58 @@ extern Protocol INTRUDER; extern int proofDepth; extern int max_encryption_level; +//! checkTerm is a helper for the next function +int +checkTerm (const System sys, const Term t, const int r1) +{ + if (!isTermVariable (t)) + { + int r2; + int e1, e2; + + // t is a term from r2 that occurs in r1 + r2 = TermRunid (t); + e1 = firstOccurrence (sys, r1, t, ANYEVENT); + if (e1 >= 0) + { + if (roledef_shift (sys->runs[r1].start, e1)->type == RECV) + { + e2 = firstOccurrence (sys, r2, t, SEND); + if (e2 >= 0) + { + // thus, it should not be the case that e1 occurs before e2 + if (isDependEvent (r1, e1, r2, e2)) + { + // That's not good! + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned because ordering for term "); + termSubstPrint (t); + eprintf + (" cannot be correct: the first send r%ii%i occurs after the receive r%ii%i.\n", + r2, e2, r1, e1); + } + return false; + } + } + } + } + else + { + globalError++; + eprintf ("error: term "); + termSubstPrint (t); + eprintf + (" from run %i should occur in run %i, but it doesn't.\n", r2, + r1); + globalError--; + error ("Abort"); + } + } + return true; +} + //! Check locals occurrence /* @@ -51,56 +103,6 @@ correctLocalOrder (const System sys) { int r1; - int checkTerm (Term t) - { - if (!isTermVariable (t)) - { - int r2; - int e1, e2; - - // t is a term from r2 that occurs in r1 - r2 = TermRunid (t); - e1 = firstOccurrence (sys, r1, t, ANYEVENT); - if (e1 >= 0) - { - if (roledef_shift (sys->runs[r1].start, e1)->type == RECV) - { - e2 = firstOccurrence (sys, r2, t, SEND); - if (e2 >= 0) - { - // thus, it should not be the case that e1 occurs before e2 - if (isDependEvent (r1, e1, r2, e2)) - { - // That's not good! - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Pruned because ordering for term "); - termSubstPrint (t); - eprintf - (" cannot be correct: the first send r%ii%i occurs after the receive r%ii%i.\n", - r2, e2, r1, e1); - } - return false; - } - } - } - } - else - { - globalError++; - eprintf ("error: term "); - termSubstPrint (t); - eprintf - (" from run %i should occur in run %i, but it doesn't.\n", r2, - r1); - globalError--; - error ("Abort"); - } - } - return true; - } - for (r1 = 0; r1 < sys->maxruns; r1++) { if (sys->runs[r1].protocol != INTRUDER) diff --git a/src/system.c b/src/system.c index 4fa2742..0632d48 100644 --- a/src/system.c +++ b/src/system.c @@ -1129,9 +1129,14 @@ iterateEventsType (const System sys, const int run, const int evtype, } // Iterate over all 'others': local variables of a run that are instantiated and contain some term of another run. +/** + * Now incorporates "checkterm" required argument of myrun to the callback: + * + * It's now callback(conts Term,const int); + */ int iterateLocalToOther (const System sys, const int myrun, - int (*callback) (Term tlocal)) + int (*callback) (const System, const Term, const int)) { Termlist tlo, tls; int flag; @@ -1158,7 +1163,7 @@ iterateLocalToOther (const System sys, const int myrun, // now iterate over all of them for (tls = tlo; flag && (tls != NULL); tls = tls->next) { - if (!callback (tls->term)) + if (!callback (sys, tls->term, myrun)) { flag = false; } diff --git a/src/system.h b/src/system.h index 8e75bbb..4a6f708 100644 --- a/src/system.h +++ b/src/system.h @@ -199,7 +199,8 @@ int iterateAllEvents (const System sys, int iterateEventsType (const System sys, const int run, const int evtype, int (*callback) (Roledef rd, int ev)); int iterateLocalToOther (const System sys, const int myrun, - int (*callback) (Term t)); + int (*callback) (const System sys, const Term t, + const int myrun)); int iterateRoles (const System sys, int (*callback) (Protocol p, Role r)); int firstOccurrence (const System sys, const int r, Term t, int evtype); Roledef eventRoledef (const System sys, const int run, const int ev);