From 71558706a6af96a3e87ac17a824a5aab119575a7 Mon Sep 17 00:00:00 2001 From: ccremers Date: Mon, 2 May 2005 13:38:45 +0000 Subject: [PATCH] - XML output should be workable now. --- src/arachne.c | 39 ++++++++++++++--------------- src/system.c | 4 +++ src/system.h | 1 + src/xmlout.c | 68 +++++++++++++++++++++++++++++++++++++++++++++------ 4 files changed, 84 insertions(+), 28 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 25e7151..a26929f 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -43,7 +43,6 @@ extern int nodes; extern int graph_uordblks; static System sys; -static Claimlist current_claim; static int attack_length; Protocol INTRUDER; // Pointers, to be set by the Init @@ -1042,12 +1041,12 @@ latexSemiState () // Open graph attack_number++; eprintf ("\\begin{msc}{Attack on "); - p = (Protocol) current_claim->protocol; + p = (Protocol) sys->current_claim->protocol; termPrint (p->nameterm); eprintf (", role "); - termPrint (current_claim->rolename); + termPrint (sys->current_claim->rolename); eprintf (", claim type "); - termPrint (current_claim->type); + termPrint (sys->current_claim->type); eprintf ("}\n%% Attack number %i\n", attack_number); eprintf ("\n"); @@ -1218,12 +1217,12 @@ dotSemiState () attack_number++; eprintf ("digraph semiState%i {\n", attack_number); eprintf ("\tlabel = \"Protocol "); - p = (Protocol) current_claim->protocol; + p = (Protocol) sys->current_claim->protocol; termPrint (p->nameterm); eprintf (", role "); - termPrint (current_claim->rolename); + termPrint (sys->current_claim->rolename); eprintf (", claim type "); - termPrint (current_claim->type); + termPrint (sys->current_claim->type); eprintf ("\";\n"); // Needed for the bindings later on: create graph @@ -1334,7 +1333,7 @@ dotSemiState () eprintf ("\t\t"); node (run, index); eprintf (" ["); - if (run == 0 && index == current_claim->ev) + if (run == 0 && index == sys->current_claim->ev) { eprintf ("style=filled,fillcolor=mistyrose,color=salmon,shape=doubleoctagon,"); @@ -2648,7 +2647,7 @@ prune_bounds () get_time_limit ()); } // Pruned because of time bound! - current_claim->timebound = 1; + sys->current_claim->timebound = 1; return 1; } @@ -2751,11 +2750,11 @@ prune_bounds () int prune_claim_specifics () { - if (current_claim->type == CLAIM_Niagree) + if (sys->current_claim->type == CLAIM_Niagree) { - if (arachne_claim_niagree (sys, 0, current_claim->ev)) + if (arachne_claim_niagree (sys, 0, sys->current_claim->ev)) { - current_claim->count = statesIncrease (current_claim->count); + sys->current_claim->count = statesIncrease (sys->current_claim->count); if (sys->output == PROOF) { indentPrint (); @@ -2765,11 +2764,11 @@ prune_claim_specifics () return 1; } } - if (current_claim->type == CLAIM_Nisynch) + if (sys->current_claim->type == CLAIM_Nisynch) { - if (arachne_claim_nisynch (sys, 0, current_claim->ev)) + if (arachne_claim_nisynch (sys, 0, sys->current_claim->ev)) { - current_claim->count = statesIncrease (current_claim->count); + sys->current_claim->count = statesIncrease (sys->current_claim->count); if (sys->output == PROOF) { indentPrint (); @@ -2814,7 +2813,7 @@ add_claim_specifics (const Claimlist cl, const Roledef rd) void count_false () { - current_claim->failed = statesIncrease (current_claim->failed); + sys->current_claim->failed = statesIncrease (sys->current_claim->failed); } //------------------------------------------------------------------------ @@ -2940,8 +2939,8 @@ iterate () eprintf ("All goals are now bound.\n"); } sys->claims = statesIncrease (sys->claims); - current_claim->count = - statesIncrease (current_claim->count); + sys->current_claim->count = + statesIncrease (sys->current_claim->count); flag = property_check (); } else @@ -2956,7 +2955,7 @@ iterate () else { // Pruned because of bound! - current_claim->complete = 0; + sys->current_claim->complete = 0; } } } @@ -3057,7 +3056,7 @@ arachne () { int run; - current_claim = cl; + sys->current_claim = cl; attack_length = INT_MAX; cl->complete = 1; p = (Protocol) cl->protocol; diff --git a/src/system.c b/src/system.c index ad0a6b8..4e33c28 100644 --- a/src/system.c +++ b/src/system.c @@ -104,6 +104,10 @@ systemInit () /* matching CLP */ sys->constraints = NULL; // no initial constraints + /* Arachne assist */ + sys->bindings = NULL; + sys->current_claim = NULL; + /* reset global counters */ systemReset (sys); diff --git a/src/system.h b/src/system.h index 2e07857..2e03671 100644 --- a/src/system.h +++ b/src/system.h @@ -195,6 +195,7 @@ struct system /* Arachne assistance */ List bindings; //!< List of bindings + Claimlist current_claim; //!< The claim under current investigation //! Shortest attack storage. struct tracebuf *attack; diff --git a/src/xmlout.c b/src/xmlout.c index b46a189..9fed897 100644 --- a/src/xmlout.c +++ b/src/xmlout.c @@ -109,6 +109,25 @@ xmlAttrTerm (const char *tag, const Term term) } } +//! Print a term, known to be a role name +/** + * Arachne turns all role names into variables for convenience. Here we + * temporarily undo it for pretty-printing. + */ +void +roleTermPrint (const Term t) +{ + if (t != NULL) + { + int typebuffer; + + typebuffer = t->type; + t->type = GLOBAL; + termPrint (t); + t->type = typebuffer; + } +} + //! Global system info /** * To be used by concrete trace as well as semitrace output @@ -136,10 +155,34 @@ xmlOutSysInfo (const System sys) xmlPrint (""); } +//! Nicely format the role and agents we think we're talking to. +void +xmlAgentsOfRunPrint (const System sys, const int run) +{ + Termlist roles; + + xmlPrint (""); + xmlindent++; + + roles = sys->runs[run].protocol->rolenames; + while (roles != NULL) + { + xmlIndentPrint (); + printf ("<"); + roleTermPrint (roles->term); + printf (">"); + termPrint (agentOfRunRole (sys, run, roles->term)); + printf ("term); + printf (">\n"); + roles = roles->next; + } + + xmlindent--; + xmlPrint (""); +} + //! Static information about a run -/** - * TODO: Does not output any sigma info yet (role->agent mappings), which is very important. - */ void xmlRunInfo (const System sys, const int run) { @@ -155,13 +198,17 @@ xmlRunInfo (const System sys, const int run) * more generic. */ oldagent = r->nameterm->subst; r->nameterm->subst = NULL; - xmlOutTerm ("role", r->nameterm); + xmlIndentPrint (); + printf (""); + roleTermPrint (r->nameterm); + printf ("\n"); /* reinstate substitution */ r->nameterm->subst = oldagent; if (oldagent != NULL) { xmlOutTerm ("agent", r->nameterm); } + xmlAgentsOfRunPrint (sys, run); } //! Show a single event from a run @@ -309,22 +356,27 @@ xmlOutTrace (const System sys) //! Output for a semitrace (from arachne method) /** - * Note: Uses get_trace_length(), which is defined for the arachne method only. - * - * TODO does not show violated claim yet, this must now be guessed by the - * reader. + * Note: Uses get_trace_length(), which is defined for the arachne method + * only. */ void xmlOutSemitrace (const System sys) { xmlIndentPrint (); printf ("current_claim != NULL) + { + xmlAttrTerm ("claim", sys->current_claim->type); + xmlAttrTerm ("label", sys->current_claim->label); + } /* add trace length attribute */ printf (" tracelength=\"%i\"", get_semitrace_length ()); printf (">\n"); xmlindent++; /* any global information about the system */ xmlOutSysInfo (sys); + /* semitrace */ xmlPrint (""); xmlindent++; xmlOutRuns (sys);