From 2280187b32c2b60d78e07b0123a3df8a13c7e9ca Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 8 Mar 2006 15:12:58 +0000 Subject: [PATCH] - Improved dot class output. --- src/depend.c | 26 +++ src/depend.h | 2 + src/dotout.c | 609 +++++++++++++++++++++++++++++++-------------------- src/role.c | 15 ++ src/role.h | 1 + src/system.c | 7 + src/system.h | 1 + src/term.c | 4 +- src/term.h | 2 + 9 files changed, 434 insertions(+), 233 deletions(-) diff --git a/src/depend.c b/src/depend.c index 572332e..f0cc106 100644 --- a/src/depend.c +++ b/src/depend.c @@ -542,3 +542,29 @@ eventNode (const int r, const int e) { return eventtonode (currentdepgraph, r, e); } + +//! Iterate over any preceding events +int +iteratePrecedingEvents (const System sys, int (*func) (int run, int ev), + const int run, const int ev) +{ + int run2; + + for (run2 = 0; run2 < sys->maxruns; run2++) + { + int ev2; + + for (ev2 = 0; ev2 < sys->runs[run2].step; ev2++) + { + if (isDependEvent (run2, ev2, run, ev)) + { + if (!func (run2, ev2)) + { + return false; + } + break; + } + } + } + return true; +} diff --git a/src/depend.h b/src/depend.h index 4204631..d7ebfab 100644 --- a/src/depend.h +++ b/src/depend.h @@ -38,5 +38,7 @@ void setDependEvent (const int r1, const int e1, const int r2, const int e2); int hasCycle (); int eventNode (const int r, const int e); int nodeCount (void); +int iteratePrecedingEvents (const System sys, int (*func) (int run, int ev), + const int run, const int ev); #endif diff --git a/src/dotout.c b/src/dotout.c index b44f7d4..3ff423e 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -3,6 +3,7 @@ #include "system.h" #include "switches.h" #include "arachne.h" +#include "binding.h" #include "depend.h" extern Protocol INTRUDER; // Pointers, to be set by the Init of arachne.c @@ -16,6 +17,28 @@ extern Role I_RRSD; #define length step +//! Draw node +void +node (const System sys, const int run, const int index) +{ + if (sys->runs[run].protocol == INTRUDER) + { + if (sys->runs[run].role == I_M) + { + eprintf ("m0"); + } + else + { + eprintf ("i%i", run); + } + } + else + { + eprintf ("r%ii%i", run, index); + } +} + + //! Determine ranks for all nodes /** * Some crude algorithm I sketched on the blackboard. @@ -78,6 +101,40 @@ graph_ranks (int *ranks, int nodes) } +//! Iterate over events (in non-intruder runs) in which some value term occurs first. +// Function should return true for iteration to continue. +int +iterate_first_regular_occurrences (const System sys, + int (*func) (int run, int ev), + const Term t) +{ + int run; + + for (run = 0; run < sys->maxruns; run++) + { + if (sys->runs[run].protocol != INTRUDER) + { + int ev; + Roledef rd; + + rd = sys->runs[run].start; + for (ev = 0; ev < sys->runs[run].step; ev++) + { + if (termSubTerm (rd->from, t) || + termSubTerm (rd->to, t) || termSubTerm (rd->message, t)) + { + // Allright, t occurs here in this run first + if (!func (run, ev)) + { + return false; + } + break; + } + } + } + } + return true; +} //! Iterate over all events that have an incoming arrow to the current one (forgetting the intruder for a moment) void @@ -236,6 +293,320 @@ iterate_outgoing_arrows (const System sys, void (*func) (), const int run, } } + +//! Draw the dependencies (returns from_intruder_count) +int +drawBindings (const System sys) +{ + int run; + int from_intruder_count; + + // We now determine them ourselves between existing runs + run = 0; + from_intruder_count = 0; + while (run < sys->maxruns) + { + if (sys->runs[run].protocol != INTRUDER) + { + int ev; + + ev = 0; + while (ev < sys->runs[run].length) + { + int incoming_arrow_count; + + void incoming_arrow (int run2, int ev2) + { + Roledef rd, rd2; + + incoming_arrow_count++; + /* + * We have decided to draw this binding, + * from run2,ev2 to run,ev + * However, me might need to decide some colouring for this node. + */ + eprintf ("\t"); + node (sys, run2, ev2); + eprintf (" -> "); + node (sys, run, ev); + eprintf (" "); + // decide color + rd = roledef_shift (sys->runs[run].start, ev); + rd2 = roledef_shift (sys->runs[run2].start, ev2); + if (rd->type == CLAIM) + { + // Towards a claim, so only indirect dependency + eprintf ("[color=cornflowerblue]"); + } + else + { + // Not towards claim should imply towards read, + // but we check it to comply with future stuff. + if (rd->type == READ && rd2->type == SEND) + { + // We want to distinguish where it is from a 'broken' send + if (isTermEqual (rd->message, rd2->message)) + { + if (isTermEqual + (rd->from, rd2->from) + && isTermEqual (rd->to, rd2->to)) + { + // Wow, a perfect match. Leave the arrow as-is :) + eprintf ("[color=darkgreen]"); + } + else + { + // Same message, different people + eprintf + ("[label=\"redirect\",color=darkorange2]"); + } + } + else + { + // Not even the same message, intruder construction + eprintf ("[label=\"construct\",color=red]"); + } + } + } + // close up + eprintf (";\n"); + } + + incoming_arrow_count = 0; + iterate_incoming_arrows (sys, incoming_arrow, run, ev); + + ev++; + } + } + run++; + } + return from_intruder_count; +} + + +//! Draw simple runs +void +drawSimpleRuns (const System sys) +{ + int run; + + // Draw graph + // First, all simple runs + run = 0; + while (run < sys->maxruns) + { + Roledef rd; + int index; + + index = 0; + rd = sys->runs[run].start; + if (sys->runs[run].protocol != INTRUDER && sys->runs[run].length > 0) + { + // Regular run + + /* DISABLED subgraphs + eprintf ("\tsubgraph cluster_run%i {\n", run); + eprintf ("\t\tlabel = \""); + eprintf ("#%i: ", run); + termPrint (sys->runs[run].protocol->nameterm); + eprintf (", "); + agentsOfRunPrint (sys, run); + eprintf ("\";\n", run); + if (run == 0) + { + eprintf ("\t\tcolor = red;\n"); + } + else + { + eprintf ("\t\tcolor = blue;\n"); + } + */ + + + // Display the respective events + while (index < sys->runs[run].length) + { + // Print node itself + eprintf ("\t\t"); + node (sys, run, index); + eprintf (" ["); + if (run == 0 && index == sys->current_claim->ev) + { + eprintf + ("style=filled,fillcolor=mistyrose,color=salmon,shape=doubleoctagon,"); + } + else + { + eprintf ("shape=box,"); + } + eprintf ("label=\""); + roledefPrintShort (rd); + eprintf ("\"]"); + eprintf (";\n"); + + // Print binding to previous node + if (index > sys->runs[run].firstReal) + { + // index > 0 + eprintf ("\t\t"); + node (sys, run, index - 1); + eprintf (" -> "); + node (sys, run, index); + eprintf (" [style=\"bold\", weight=\"10.0\"]"); + eprintf (";\n"); + } + else + { + // index <= firstReal + if (index == sys->runs[run].firstReal) + { + // index == firstReal + Roledef rd; + int send_before_read; + int done; + + // Determine if it is an active role or note + /** + *@todo note that this will probably become a standard function call for role.h + */ + rd = + roledef_shift (sys->runs[run].start, + sys->runs[run].firstReal); + done = 0; + send_before_read = 0; + while (!done && rd != NULL) + { + if (rd->type == READ) + { + done = 1; + } + if (rd->type == SEND) + { + done = 1; + send_before_read = 1; + } + rd = rd->next; + } + // Draw the first box + // This used to be drawn only if done && send_before_read, now we always draw it. + eprintf ("\t\ts%i [label=\"Run %i: ", run, run); + termPrint (sys->runs[run].protocol->nameterm); + eprintf (", "); + termPrint (sys->runs[run].role->nameterm); + eprintf ("\\n"); + agentsOfRunPrint (sys, run); + eprintf ("\", shape=diamond];\n"); + eprintf ("\t\ts%i -> ", run); + node (sys, run, index); + eprintf (" [weight=\"10.0\"];\n"); + } + } + index++; + rd = rd->next; + } + /* DISABLED subgraphs + eprintf ("\t}\n"); + */ + } + run++; + } +} + +//! Choose term node +void +chooseTermNode (const Term t) +{ + eprintf ("CHOOSE"); + { + char *rsbuf; + + rsbuf = RUNSEP; + RUNSEP = "x"; + termPrint (t); + RUNSEP = rsbuf; + } +} + +//! Show intruder choices +void +drawIntruderChoices (const System sys) +{ + Termlist shown; + List bl; + + shown = NULL; + for (bl = sys->bindings; bl != NULL; bl = bl->next) + { + Binding b; + + b = (Binding) bl->data; + if ((!b->blocked) && (!b->done) && isTermVariable (b->term)) + { + /* + * If the binding is not blocked, but also not done, + * the intruder can apparently satisfy it at will. + */ + + if (!inTermlist (shown, b->term)) + { + int firsthere (int run, int ev) + { + /** + * @todo This is not very efficient, + * but maybe that is not really + * needed here. + */ + int notearlier (int run2, int ev2) + { + if (sys->runs[run2].protocol != INTRUDER) + { + return (!roledefSubTerm + (eventRoledef (sys, run2, ev2), b->term)); + } + else + { + return true; + } + } + + if (iteratePrecedingEvents (sys, notearlier, run, ev)) + { + eprintf ("\t"); + chooseTermNode (b->term); + eprintf (" -> "); + node (sys, run, ev); + eprintf (" [color=\"darkgreen\"];\n"); + } + return true; + } + + // If the first then we add a header + if (shown == NULL) + { + eprintf ("// Showing intruder choices.\n"); + } + // Not in the list, show new node + shown = termlistAdd (shown, b->term); + eprintf ("\t"); + chooseTermNode (b->term); + eprintf (" [label=\"Class: any "); + termPrint (b->term); + eprintf ("\",color=\"darkgreen\"];\n"); + + iterate_first_regular_occurrences (sys, firsthere, b->term); + } + } + + } + + if (shown != NULL) + { + eprintf ("\n"); + } + termlistDelete (shown); +} + + //! Display the current semistate using dot output format. /** * This is not as nice as we would like it. Furthermore, the function is too big. @@ -251,25 +622,6 @@ dotSemiState (const System sys) int from_intruder_count; int nodes; - void node (const int run, const int index) - { - if (sys->runs[run].protocol == INTRUDER) - { - if (sys->runs[run].role == I_M) - { - eprintf ("m0"); - } - else - { - eprintf ("i%i", run); - } - } - else - { - eprintf ("r%ii%i", run, index); - } - } - // Open graph attack_number++; eprintf ("digraph semiState%i {\n", attack_number); @@ -282,8 +634,6 @@ dotSemiState (const System sys) termPrint (sys->current_claim->type); eprintf ("\";\n"); - from_intruder_count = 0; // number of terms that can come from the initial knowledge - // Needed for the bindings later on: create graph nodes = nodeCount (); @@ -347,218 +697,10 @@ dotSemiState (const System sys) } #endif - // Draw graph - // First, all simple runs - run = 0; - while (run < sys->maxruns) - { - Roledef rd; - int index; - - index = 0; - rd = sys->runs[run].start; - if (sys->runs[run].protocol != INTRUDER && sys->runs[run].length > 0) - { - // Regular run - - /* DISABLED subgraphs - eprintf ("\tsubgraph cluster_run%i {\n", run); - eprintf ("\t\tlabel = \""); - eprintf ("#%i: ", run); - termPrint (sys->runs[run].protocol->nameterm); - eprintf (", "); - agentsOfRunPrint (sys, run); - eprintf ("\";\n", run); - if (run == 0) - { - eprintf ("\t\tcolor = red;\n"); - } - else - { - eprintf ("\t\tcolor = blue;\n"); - } - */ - - - // Display the respective events - while (index < sys->runs[run].length) - { - // Print node itself - eprintf ("\t\t"); - node (run, index); - eprintf (" ["); - if (run == 0 && index == sys->current_claim->ev) - { - eprintf - ("style=filled,fillcolor=mistyrose,color=salmon,shape=doubleoctagon,"); - } - else - { - eprintf ("shape=box,"); - } - eprintf ("label=\""); - roledefPrintShort (rd); - eprintf ("\"]"); - eprintf (";\n"); - - // Print binding to previous node - if (index > sys->runs[run].firstReal) - { - // index > 0 - eprintf ("\t\t"); - node (run, index - 1); - eprintf (" -> "); - node (run, index); - eprintf (" [style=\"bold\", weight=\"10.0\"]"); - eprintf (";\n"); - } - else - { - // index <= firstReal - if (index == sys->runs[run].firstReal) - { - // index == firstReal - Roledef rd; - int send_before_read; - int done; - - // Determine if it is an active role or note - /** - *@todo note that this will probably become a standard function call for role.h - */ - rd = - roledef_shift (sys->runs[run].start, - sys->runs[run].firstReal); - done = 0; - send_before_read = 0; - while (!done && rd != NULL) - { - if (rd->type == READ) - { - done = 1; - } - if (rd->type == SEND) - { - done = 1; - send_before_read = 1; - } - rd = rd->next; - } - // Draw the first box - // This used to be drawn only if done && send_before_read, now we always draw it. - eprintf ("\t\ts%i [label=\"Run %i: ", run, run); - termPrint (sys->runs[run].protocol->nameterm); - eprintf (", "); - termPrint (sys->runs[run].role->nameterm); - eprintf ("\\n"); - agentsOfRunPrint (sys, run); - eprintf ("\", shape=diamond];\n"); - eprintf ("\t\ts%i -> ", run); - node (run, index); - eprintf (" [weight=\"10.0\"];\n"); - } - } - index++; - rd = rd->next; - } - /* DISABLED subgraphs - eprintf ("\t}\n"); - */ - } - run++; - } - + // First, simple runs + drawSimpleRuns (sys); // Second, all bindings. - // We now determine them ourselves between existing runs - run = 0; - while (run < sys->maxruns) - { - if (sys->runs[run].protocol != INTRUDER) - { - int ev; - - ev = 0; - while (ev < sys->runs[run].length) - { - int incoming_arrow_count; - - void incoming_arrow (int run2, int ev2) - { - Roledef rd, rd2; - - incoming_arrow_count++; - /* - * We have decided to draw this binding, - * from run2,ev2 to run,ev - * However, me might need to decide some colouring for this node. - */ - eprintf ("\t"); - node (run2, ev2); - eprintf (" -> "); - node (run, ev); - eprintf (" "); - // decide color - rd = roledef_shift (sys->runs[run].start, ev); - rd2 = roledef_shift (sys->runs[run2].start, ev2); - if (rd->type == CLAIM) - { - // Towards a claim, so only indirect dependency - eprintf ("[color=cornflowerblue]"); - } - else - { - // Not towards claim should imply towards read, - // but we check it to comply with future stuff. - if (rd->type == READ && rd2->type == SEND) - { - // We want to distinguish where it is from a 'broken' send - if (isTermEqual (rd->message, rd2->message)) - { - if (isTermEqual - (rd->from, rd2->from) - && isTermEqual (rd->to, rd2->to)) - { - // Wow, a perfect match. Leave the arrow as-is :) - eprintf ("[color=forestgreen]"); - } - else - { - // Same message, different people - eprintf - ("[label=\"redirect\",color=darkorange2]"); - } - } - else - { - // Not even the same message, intruder construction - eprintf ("[label=\"construct\",color=red]"); - } - } - } - // close up - eprintf (";\n"); - } - - incoming_arrow_count = 0; - iterate_incoming_arrows (sys, incoming_arrow, run, ev); - /* - * Currently disabled: generates too much garbage - */ - if (false && incoming_arrow_count == 0) - { - // No incoming arrows: can be generated from initial intruder knowledge - - from_intruder_count++; - eprintf ("\tintruder -> "); - node (run, ev); - eprintf (";\n"); - } - - ev++; - } - } - run++; - } + from_intruder_count = drawBindings (sys); // Third, the intruder node (if needed) if (from_intruder_count > 0) @@ -659,6 +801,9 @@ dotSemiState (const System sys) } } + // Intruder choices + drawIntruderChoices (sys); + #ifdef DEBUG // Debug: print dependencies if (DEBUGL (3)) diff --git a/src/role.c b/src/role.c index f8ba952..207034b 100644 --- a/src/role.c +++ b/src/role.c @@ -319,3 +319,18 @@ roledef_shift (Roledef rd, int i) } return rd; } + +// Check whether a term is a subterm of a roledef +int +roledefSubTerm (Roledef rd, Term tsub) +{ + if (rd == NULL) + { + return false; + } + else + { + return (termSubTerm (rd->from, tsub) || + termSubTerm (rd->to, tsub) || termSubTerm (rd->message, tsub)); + } +} diff --git a/src/role.h b/src/role.h index c92d6a3..2e7acf1 100644 --- a/src/role.h +++ b/src/role.h @@ -161,5 +161,6 @@ void rolesPrint (Role r); int roledef_iterate_events (Roledef rd, int (*func) ()); int roledef_length (const Roledef rd); Roledef roledef_shift (Roledef rd, int i); +int roledefSubTerm (Roledef rd, Term tsub); #endif diff --git a/src/system.c b/src/system.c index 6a94e75..c30518b 100644 --- a/src/system.c +++ b/src/system.c @@ -1413,3 +1413,10 @@ firstOccurrence (const System sys, const int r, Term t, int evtype) #endif return firste; } + +//! Get the roledef of an event +Roledef +eventRoledef (const System sys, const int run, const int ev) +{ + return roledef_shift (sys->runs[run].start, ev); +} diff --git a/src/system.h b/src/system.h index 068e1be..ef6645a 100644 --- a/src/system.h +++ b/src/system.h @@ -194,6 +194,7 @@ int iterateEventsType (const System sys, const int run, const int evtype, int iterateLocalToOther (const System sys, const int myrun, int (*callback) (Term t)); int firstOccurrence (const System sys, const int r, Term t, int evtype); +Roledef eventRoledef (const System sys, const int run, const int ev); //! Equality for run structure naming diff --git a/src/term.c b/src/term.c index 4f827fa..c900489 100644 --- a/src/term.c +++ b/src/term.c @@ -21,6 +21,7 @@ /* public flag */ int rolelocal_variable; +char *RUNSEP; /* external definitions */ @@ -44,6 +45,7 @@ void termsInit (void) { rolelocal_variable = 0; + RUNSEP = "#"; return; } @@ -333,7 +335,7 @@ termPrint (Term term) eprintf ("V"); if (TermRunid (term) >= 0) { - eprintf ("#%i", TermRunid (term)); + eprintf ("%s%i", RUNSEP, TermRunid (term)); } if (term->subst != NULL) { diff --git a/src/term.h b/src/term.h index 646eb51..e072ef6 100644 --- a/src/term.h +++ b/src/term.h @@ -208,4 +208,6 @@ void termSubstPrint (Term t); int iterateTermOther (const int myrun, Term t, int (*callback) (Term t)); +extern char *RUNSEP; // by default, set to "#" + #endif