From cf832ca1b1d24836150b40064592b30668c97692 Mon Sep 17 00:00:00 2001 From: ccremers Date: Mon, 27 Feb 2006 22:27:09 +0000 Subject: [PATCH] - Seems to work again, but further testing is needed. --- src/arachne.c | 98 ++++++++++++++++++++++++++++++++++++-------- src/binding.c | 86 +++++++++++++++++++++++++++++++++----- src/compiler.c | 6 +++ src/depend.c | 1 + src/prune_theorems.c | 7 +++- src/switches.c | 2 - src/system.c | 25 +++++++---- src/term.c | 21 ++++++++++ src/term.h | 1 + 9 files changed, 208 insertions(+), 39 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 43a76d7..d97ffaa 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -164,18 +164,30 @@ arachneDone () void indentPrefixPrint (const int annotate, const int jumps) { + void counterPrint () + { + if (switches.engine == ARACHNE_ENGINE) + { + statesFormat (sys->current_claim->states); + eprintf ("\t"); + } + eprintf ("%i", annotate); + eprintf ("\t"); + } + if (switches.output == ATTACK && globalError == 0) { // Arachne, attack, not an error // We assume that means DOT output - eprintf ("// %i\t", annotate); + eprintf ("// "); + counterPrint (); } else { // If it is not to stdout, or it is not an attack... int i; - eprintf ("%i\t", annotate); + counterPrint (); for (i = 0; i < jumps; i++) { if (i % 3 == 0) @@ -763,6 +775,25 @@ getPriorityOfNeededKey (const System sys, const Term keyneeded) return prioritylevel; } +//! Report failed binding +void +report_failed_binding (Binding b, int run, int index) +{ + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Failed to bind the binding at r%ii%i with term ", b->run_to, + b->ev_to); + termPrint (b->term); + eprintf (" to the source r%ii%i because of orderings.\n", run, index); +#ifdef DEBUG + if (DEBUGL (5)) + { + dependPrint (); + } +#endif + } +} //! Make a decryption chain from a binding to some run,index using the key list, and callback if this works. /** @@ -781,6 +812,10 @@ createDecryptionChain (const Binding b, const int run, const int index, goal_unbind (b); return; } + else + { + report_failed_binding (b, run, index); + } } else { @@ -858,6 +893,10 @@ createDecryptionChain (const Binding b, const int run, const int index, createDecryptionChain (bnew, run, index, keylist->next, callback); goal_unbind (b); } + else + { + report_failed_binding (b, smallrun, 2); + } /* * clean up */ @@ -908,32 +947,59 @@ bind_existing_to_goal (const Binding b, const int run, const int index) { int neworders; int allgood; + Term tvar; // the idea is, that a substitution in run x with // something containing should be wrapped; this // occurs for all subterms of other runs. - int makeDepend (Term t) + int makeDepend (Term tsmall) { - int r1, e1; + Term tsubst; - r1 = TermRunid (t); - e1 = firstOccurrence (sys, r1, t, SEND); - if (dependPushEvent (r1, e1, run, index)) + tsubst = deVar (tsmall); + if (!realTermVariable (tsubst)) { - neworders++; - return true; - } - else - { - allgood = false; - return false; + // Only for non-variables (i.e. local constants) + int r1, e1, r2, e2; + + r1 = TermRunid (tsubst); + e1 = firstOccurrence (sys, r1, tsubst, SEND); + if (e1 >= 0) + { + r2 = TermRunid (tvar); + e2 = firstOccurrence (sys, r2, tsubst, READ); + if (e2 >= 0) + { + + if (dependPushEvent (r1, e1, r2, e2)) + { + neworders++; + return true; + } + else + { + allgood = false; + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Substitution for "); + termSubstPrint (sl->term); + eprintf (" (subterm "); + termPrint (tsmall); + eprintf (") could not be safely bound.\n"); + } + return false; + } + } + } } + return true; } neworders = 0; allgood = true; - iterateTermOther (run, sl->term, makeDepend); - + tvar = sl->term; + iterateTermOther (run, tvar, makeDepend); if (allgood) { wrapSubst (sl->next); diff --git a/src/binding.c b/src/binding.c index 24e68f3..409515d 100644 --- a/src/binding.c +++ b/src/binding.c @@ -230,25 +230,28 @@ goal_add (Term term, const int run, const int ev, const int level) else { // Determine whether we already had it - int nope; + int createnew; int testSame (void *data) { Binding b; b = (Binding) data; - if (isTermEqual (b->term, term) && run == b->run_to && ev == b->ev_to) - { // abort scan, report - return false; - } - else - { // proceed with scan - return true; + if (isTermEqual (b->term, term)) + { + // binding of same term + if (run == b->run_to && ev == b->ev_to) + { + // identical binding + createnew = false; + } } + return true; } - nope = list_iterate (sys->bindings, testSame); - if (nope) + createnew = true; + list_iterate (sys->bindings, testSame); + if (createnew) { // Add a new binding Binding b; @@ -436,5 +439,66 @@ unique_origination () int bindings_c_minimal () { - return unique_origination (); + if (!unique_origination ()) + { + return false; + } + + { + List bl; + + // For all goals + bl = sys->bindings; + while (bl != NULL) + { + Binding b; + + b = (Binding) bl->data; + // Check for a valid binding; it has to be 'done' and sensibly bound (not as in tuple expanded stuff) + if (valid_binding (b)) + { + int run; + int node_from; + + // Find all preceding events + for (run = 0; run < sys->maxruns; run++) + { + int ev; + + //!@todo hardcoded reference to step, should be length + for (ev = 0; ev < sys->runs[run].step; ev++) + { + if (isDependEvent (run, ev, b->run_from, b->ev_from)) + { + // this node is *before* the from node + Roledef rd; + + rd = roledef_shift (sys->runs[run].start, ev); + if (termInTerm (rd->message, b->term)) + { + // This term already occurs as interm in a previous node! +#ifdef DEBUG + if (DEBUGL (4)) + { + // Report this + indentPrint (); + eprintf ("Binding for "); + termPrint (b->term); + eprintf + (" at r%i i%i is not c-minimal because it occurred before at r%i i%i in ", + b->run_from, b->ev_from, run, ev); + termPrint (rd->message); + eprintf ("\n"); + } +#endif + return false; + } + } + } + } + } + bl = bl->next; + } + } + return true; } diff --git a/src/compiler.c b/src/compiler.c index 1a5c4e5..4e179ac 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -1420,6 +1420,11 @@ compute_prec_sets (const System sys) ev1++; rd = rd->next; } + while (ev1 < sys->roleeventmax) + { + eventlabels[index (r1, ev1)] = NULL; + ev1++; + } //eprintf ("\n"); r1++; } @@ -1517,6 +1522,7 @@ compute_prec_sets (const System sys) } while (r1 < sys->rolecount && !isTermEqual (label, eventlabels[index (r1, ev1)])); + if (r1 == sys->rolecount) { error diff --git a/src/depend.c b/src/depend.c index ea475e3..9ad949b 100644 --- a/src/depend.c +++ b/src/depend.c @@ -98,6 +98,7 @@ dependPrint () r1 = 0; o1 = 0; eprintf ("Printing dependency graph.\n"); + eprintf ("Y axis nodes comes before X axis node.\n"); for (n1 = 0; n1 < nodeCount (); n1++) { int n2; diff --git a/src/prune_theorems.c b/src/prune_theorems.c index 06845cc..62040c1 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -47,7 +47,7 @@ correctLocalOrder (const System sys) { indentPrint (); eprintf ("Pruned because ordering for term "); - termPrint (t); + termSubstPrint (t); eprintf (" cannot be correct: the first send r%ii%i occurs after the read r%ii%i.\n", r2, e2, r1, e1); @@ -282,7 +282,10 @@ prune_theorems (const System sys) /* * Check for correct orderings involving local constants */ - correctLocalOrder (sys); + if (switches.experimental & 8 != 0) + { + correctLocalOrder (sys); + } /** * Check whether the bindings are valid diff --git a/src/switches.c b/src/switches.c index baa55e6..4103525 100644 --- a/src/switches.c +++ b/src/switches.c @@ -942,8 +942,6 @@ switcher (const int process, int index, int commandline) else { switches.experimental = integer_argument (); - eprintf ("Set experimental switch to %i.\n", switches.experimental); - eprintf ("And 4 mask: %i.\n", switches.experimental & 4); return index; } } diff --git a/src/system.c b/src/system.c index e451e25..cab837b 100644 --- a/src/system.c +++ b/src/system.c @@ -1595,7 +1595,7 @@ 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. int iterateLocalToOther (const System sys, const int myrun, - int (*callback) (Term t)) + int (*callback) (Term tlocal)) { Termlist tlo, tls; @@ -1642,14 +1642,23 @@ firstOccurrence (const System sys, const int r, Term t, int evtype) return true; } - if (iterateEventsType (sys, r, evtype, checkOccurs)) + firste = -1; + iterateEventsType (sys, r, evtype, checkOccurs); +#ifdef DEBUG + if (DEBUGL (3)) { - globalError++; - eprintf ("Desired term "); - termPrint (t); - eprintf (" does not occur.\n"); - globalError--; - error ("(in run %i in event type %i.)", r, evtype); + if (firste == -1) + { + globalError++; + eprintf ("Warning: Desired term "); + termPrint (t); + eprintf (" does not occur"); + eprintf (" in run %i in event type %i.\n", r, evtype); + runPrint (sys->runs[r].start); + eprintf ("\n"); + globalError--; + } } +#endif return firste; } diff --git a/src/term.c b/src/term.c index 6ef95bb..6d4c52d 100644 --- a/src/term.c +++ b/src/term.c @@ -1428,6 +1428,27 @@ termHidelevel (const Term tsmall, Term tbig) } } +//! Show a substitution of t +void +termSubstPrint (Term t) +{ + if (realTermVariable (t)) + { + Term tbuf; + + tbuf = t->subst; + t->subst = NULL; + termPrint (t); + t->subst = tbuf; + eprintf (":="); + termSubstPrint (t->subst); + } + else + { + termPrint (t); + } +} + // Iterate over subterm constants of other runs in a term // Callback should return true to progress. This is reported in the final thing. int diff --git a/src/term.h b/src/term.h index 2849eae..646eb51 100644 --- a/src/term.h +++ b/src/term.h @@ -204,6 +204,7 @@ Term freshTermPrefix (Term prefixterm); int isTermFunctionName (Term t); Term getTermFunction (Term t); unsigned int termHidelevel (const Term tsmall, Term tbig); +void termSubstPrint (Term t); int iterateTermOther (const int myrun, Term t, int (*callback) (Term t));