From 0540b744e2afc92ff42165693a4cabe4c94e5a7b Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 19 May 2005 14:43:32 +0000 Subject: [PATCH] - Repaired a pruning method that still needed a lemma. It was a bit overzealous and killed a woolam-mutual attack. --- src/arachne.c | 122 +++++++++++++++++++++++++++++++++++++++++--------- src/arachne.h | 1 + src/binding.c | 15 +++++++ 3 files changed, 116 insertions(+), 22 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index db3527a..209c008 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -52,6 +52,8 @@ Role I_RRS; Role I_RRSD; static int indentDepth; +static int prevIndentDepth; +static int indentDepthChanges; static int proofDepth; static int max_encryption_level; static int num_regular_runs; @@ -136,6 +138,10 @@ arachneInit (const System mysys) num_intruder_runs = 0; max_encryption_level = 0; + indentDepth = 0; + prevIndentDepth = 0; + indentDepthChanges = 0; + return; } @@ -159,22 +165,23 @@ arachneDone () #define isBound(rd) (rd->bound) #define length step -//! Indent print +//! Indent prefix print void -indentPrint () +indentPrefixPrint (const int annotate, const int jumps) { if (sys->output == ATTACK && globalError == 0) { // Arachne, attack, not an error // We assume that means DOT output - eprintf ("// "); + eprintf ("// %i\t", annotate); } else { // If it is not to stdout, or it is not an attack... int i; - for (i = 0; i < indentDepth; i++) + eprintf ("%i\t", annotate); + for (i = 0; i < jumps; i++) { if (i % 3 == 0) eprintf ("|"); @@ -185,6 +192,35 @@ indentPrint () } } +//! Indent print +/** + * More subtle than before. Indentlevel changes now cause a counter to be increased, which is printed. Nice to find stuff in attacks. + */ +void +indentPrint () +{ + if (indentDepth != prevIndentDepth) + { + indentDepthChanges++; + while (indentDepth != prevIndentDepth) + { + if (prevIndentDepth < indentDepth) + { + indentPrefixPrint (indentDepthChanges, prevIndentDepth); + eprintf ("{\n"); + prevIndentDepth++; + } + else + { + prevIndentDepth--; + indentPrefixPrint (indentDepthChanges, prevIndentDepth); + eprintf ("}\n"); + } + } + } + indentPrefixPrint (indentDepthChanges, indentDepth); +} + //! Print indented binding void binding_indent_print (const Binding b, const int flag) @@ -733,6 +769,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index) newruns = 0; // New runs introduced smalltermbinding = b; // Start off with destination binding + indentDepth++; #ifdef DEBUG if (DEBUGL (4)) { @@ -751,7 +788,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index) { indentPrint (); eprintf - ("This introduces the obligation to decrypted the following encrypted subterms: "); + ("This introduces the obligation to decrypt the following encrypted subterms: "); termlistPrint (cryptlist); eprintf ("\n"); } @@ -866,6 +903,8 @@ bind_existing_to_goal (const Binding b, const int run, const int index) newruns--; } goal_unbind (b); + + indentDepth--; return flag; } @@ -2399,12 +2438,12 @@ bind_goal_regular_run (const Binding b) eprintf (", at %i\n", index); } indentDepth++; + // Bind to existing run sflag = bind_existing_run (b, p, r, index); // bind to new run - { - sflag = sflag && bind_new_run (b, p, r, index); - } + sflag = sflag && bind_new_run (b, p, r, index); + indentDepth--; return sflag; } @@ -2627,20 +2666,51 @@ prune_theorems () { error ("Agent of run %i is NULL", run); } - if (!realTermLeaf (agent) - || agent->stype == NULL - || (agent->stype != NULL - && !inTermlist (agent->stype, TERM_Agent))) - { - if (sys->output == PROOF) - { - indentPrint (); - eprintf ("Pruned because the agent "); - termPrint (agent); - eprintf (" of run %i is not of a compatible type.\n", run); - } - return 1; - } + /** + * Check whether the agent of the run is of a sensible type. + * + * @TODO Note that this still needs a lemma. + */ + { + int sensibleagent; + + sensibleagent = true; + + if (!realTermLeaf (agent)) + { // not a leaf + sensibleagent = false; + } + else + { // real leaf + if (sys->match == 0 || !isTermVariable (agent)) + { // either strict matching, or not a variable, so we should check matching types + if (agent->stype == NULL) + { // Too generic + sensibleagent = false; + } + else + { // Has a type + if (!inTermlist (agent->stype, TERM_Agent)) + { // but not the right type + sensibleagent = false; + } + } + } + } + + if (!sensibleagent) + { + if (sys->output == PROOF) + { + indentPrint (); + eprintf ("Pruned because the agent "); + termPrint (agent); + eprintf (" of run %i is not of a compatible type.\n", + run); + } + return 1; + } + } agl = agl->next; } run++; @@ -3274,7 +3344,15 @@ arachne () { semiRunDestroy (); } + + //! Indent back indentDepth--; + + if (sys->output == PROOF) + { + indentPrint (); + eprintf ("Proof complete for this claim.\n"); + } } // next cl = cl->next; diff --git a/src/arachne.h b/src/arachne.h index a00791c..3783a69 100644 --- a/src/arachne.h +++ b/src/arachne.h @@ -7,5 +7,6 @@ void arachneInit (const System sys); void arachneDone (); int arachne (); int get_semitrace_length (); +void indentPrint (); #endif diff --git a/src/binding.c b/src/binding.c index 08dd76a..366397b 100644 --- a/src/binding.c +++ b/src/binding.c @@ -12,6 +12,7 @@ #include "debug.h" #include "term.h" #include "termmap.h" +#include "arachne.h" #include static System sys; @@ -771,6 +772,20 @@ bindings_c_minimal () 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 0; } }