From 01124e21048dc1816b7ba1775442b7f87213bcae Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 2 Jun 2005 08:25:45 +0000 Subject: [PATCH] - Modified a number of things related to the attack analysis tools. * removed wrappers * added wrappers * removed construct, now R constructs. * added section. * variable substitutions are followed through in runs. Thus, only unbound variables occur in the semitrace. * added the untested claims back in, so that all events in a role/semitrace are now shown. Note that they can be disabled again by using the new '-H' switch. --- src/switches.c | 14 +++++ src/system.c | 1 + src/system.h | 1 + src/xmlout.c | 164 +++++++++++++++++++++++++++++++++++++++++-------- 4 files changed, 155 insertions(+), 25 deletions(-) diff --git a/src/switches.c b/src/switches.c index 1f56337..d972ae1 100644 --- a/src/switches.c +++ b/src/switches.c @@ -295,6 +295,20 @@ switcher (const int process, const System sys, int index) } } + if (detect ('H', "human-readable", 0)) + { + if (!process) + { + helptext ("-H,--human-readable", + "try to make the output human-friendly (e.g. in XML)"); + } + else + { + sys->switchHuman = true; + return index; + } + } + /* ================== * Modelchecker only */ diff --git a/src/system.c b/src/system.c index 3567085..46d933f 100644 --- a/src/system.c +++ b/src/system.c @@ -76,6 +76,7 @@ systemInit () sys->switchClaims = 0; // default don't report on claims sys->switchClaimToCheck = NULL; // default check all claims sys->switchXMLoutput = 0; // default no xml output + sys->switchHuman = false; // not human friendly by default sys->switchGoalSelectMethod = 3; // default goal selection method sys->traverse = 12; // default traversal method diff --git a/src/system.h b/src/system.h index 2e03671..91552e6 100644 --- a/src/system.h +++ b/src/system.h @@ -144,6 +144,7 @@ struct system int switchGoalSelectMethod; //!< Goal selection method for Arachne engine Term switchClaimToCheck; //!< Which claim should be checked? int switchXMLoutput; //!< xml output + int switchHuman; //!< human readable //! Latex output switch. /** diff --git a/src/xmlout.c b/src/xmlout.c index ec6c63c..fbecbae 100644 --- a/src/xmlout.c +++ b/src/xmlout.c @@ -31,6 +31,7 @@ extern Term TERM_Function; // from termlist.c */ static int xmlindent; // indent level for xml elements in output static Term only_claim_label; // if NULL, show all claims in xml event lists. Otherwise, only this one. +static int show_substitution_path; // is only set to true for variable printing, normally false. /* * Default external interface: init/done @@ -43,6 +44,7 @@ xmlOutInit (void) printf ("\n"); xmlindent = 1; only_claim_label = NULL; + show_substitution_path = false; } //! Close up @@ -96,10 +98,18 @@ xmlOutInteger (const char *tag, const int value) //! Print a term in XML form (iteration inner) void -xmlTermPrintInner (const Term term) +xmlTermPrintInner (Term term) { if (term != NULL) { + if (!show_substitution_path) + { + /* In a normal situation, variables are immediately substituted, and + * only the result is output. + */ + term = deVar (term); + } + if (realTermLeaf (term)) { // Variable? @@ -129,7 +139,9 @@ xmlTermPrintInner (const Term term) else { // Constant + printf (""); termPrint (term); // Must be a normal termPrint + printf (""); } } else @@ -170,12 +182,17 @@ xmlTermPrintInner (const Term term) } //! Print a term in XML form (wrapper) +/** + * In the original setupt, a wrapper was added. It is disabled for now. + * If this turns out to be the preferred situation, xmlTermPrintInner can be + * renamed to xmlTermPrint and all will be well. + */ void xmlTermPrint (const Term term) { - printf (""); + // printf (""); xmlTermPrintInner (term); - printf (""); + // printf (""); } //! Print a termlist in XML form @@ -240,11 +257,98 @@ roleTermPrint (const Term t) typebuffer = t->type; t->type = GLOBAL; - xmlTermPrint (t); + termPrint (t); t->type = typebuffer; } } +//! Print a role term with tag and indenting etc. +void +xmlRoleTermPrint (const Term t) +{ + xmlIndentPrint (); + printf (""); + roleTermPrint (t); + printf ("\n"); +} + +//! Show a single variable instantiation, depth one +void +xmlVariableDepthOne (const Term variable) +{ + /* + * To print a variable, we would wish to see only the first substitution. + * Therefore, we temporarily undo any further substitutions, and reset + * them at the end. + */ + Term varsubst; // substitution shortcut + Term nextsubst; // temporary buffer + + varsubst = variable->subst; + if (varsubst != NULL && realTermVariable (varsubst)) + { + nextsubst = varsubst->subst; + varsubst->subst = NULL; + } + else + { + nextsubst = NULL; + } + + // Print the actual term + xmlIndentPrint (); + xmlTermPrint (variable); + printf ("\n"); + + if (nextsubst != NULL) + { + varsubst->subst = nextsubst; + } + +} + +//! Show variable instantiations +/** + * Show the instantiations of all variables. Maybe we need to restrict this, + * and scan only for those variables that actually occur in the semitrace. + */ +void +xmlVariables (const System sys) +{ + int prev_mode; // buffer for show mode + int run; // for loop + + prev_mode = show_substitution_path; + show_substitution_path = true; + xmlPrint (""); + xmlindent++; + run = 0; + while (run < sys->maxruns) + { + if (sys->runs[run].protocol != INTRUDER) + { + Termlist varlist; + + varlist = sys->runs[run].locals; + while (varlist != NULL) + { + if (realTermVariable (varlist->term)) + { + // xmlVariableDepthOne (varlist->term); + xmlIndentPrint (); + xmlTermPrint (varlist->term); + printf ("\n"); + } + varlist = varlist->next; + } + } + run++; + } + xmlindent--; + xmlPrint (""); + show_substitution_path = prev_mode; +} + //! Show inverses void xmlInverses (const System sys) @@ -305,28 +409,35 @@ isProtocolInvolved (const System sys, const Protocol p) //! Determine whether to show an event int -isEventInteresting (const Roledef rd) +isEventInteresting (const System sys, const Roledef rd) { - if (rd->type != CLAIM) + if (sys->switchHuman) { - return 1; - } - else - { - // A claim - if (only_claim_label == NULL) + if (rd->type != CLAIM) { return 1; } else { - if (isTermEqual (only_claim_label, rd->label)) + // A claim + if (only_claim_label == NULL) { return 1; } + else + { + if (isTermEqual (only_claim_label, rd->label)) + { + return 1; + } + } } + return 0; + } + else + { + return 1; } - return 0; } //! Show a single event from a run @@ -340,7 +451,7 @@ isEventInteresting (const Roledef rd) void xmlOutEvent (const System sys, Roledef rd, const int run, const int index) { - if (!isEventInteresting (rd)) + if (!isEventInteresting (sys, rd)) { return; } @@ -457,12 +568,16 @@ xmlOutEvent (const System sys, Roledef rd, const int run, const int index) void xmlRoleEventlist (const System sys, Roledef rd, int index) { + xmlPrint (""); + xmlindent++; while (rd != NULL) { xmlOutEvent (sys, rd, -1, index); index++; rd = rd->next; } + xmlindent--; + xmlPrint (""); } //! Show all protocol roles that are in the attack. @@ -486,7 +601,7 @@ xmlInvolvedProtocolRoles (const System sys) { xmlPrint (""); xmlindent++; - xmlOutTerm ("name", r->nameterm); + xmlRoleTermPrint (r->nameterm); xmlRoleEventlist (sys, r->roledef, 0); xmlindent--; xmlPrint (""); @@ -530,8 +645,10 @@ xmlAgentsOfRunPrint (const System sys, const int run) while (roles != NULL) { xmlPrint (""); - xmlOutTerm ("name", roles->term); + xmlindent++; + xmlRoleTermPrint (roles->term); xmlOutTerm ("agent", deVar (agentOfRunRole (sys, run, roles->term))); + xmlindent--; xmlPrint (""); roles = roles->next; } @@ -564,10 +681,7 @@ xmlRunInfo (const System sys, const int run) * more generic. */ oldagent = r->nameterm->subst; r->nameterm->subst = NULL; - xmlIndentPrint (); - printf (""); - roleTermPrint (r->nameterm); - printf ("\n"); + xmlRoleTermPrint (r->nameterm); /* reinstate substitution */ r->nameterm->subst = oldagent; if (oldagent != NULL) @@ -643,6 +757,7 @@ xmlOutSemitrace (const System sys) /* mention the broken claim */ buffer_only_claim_label = only_claim_label; + only_claim_label = NULL; if (sys->current_claim != NULL) { xmlPrint (""); @@ -653,12 +768,11 @@ xmlOutSemitrace (const System sys) xmlPrint (""); only_claim_label = sys->current_claim->label; } - else - { - only_claim_label = NULL; - } + /* any global information about the system */ xmlOutSysInfo (sys); + /* instantiations of the variables */ + xmlVariables (sys); /* semitrace */ xmlPrint (""); xmlindent++;