- Added xml output switch (-x, check scyther --help). It's not complete

yet, to be finished tomorrow.

src/arachne.c

@@ -437,7 +437,7 @@ determine_unification_run (Termlist tl)
 
 //! Determine trace length
 int
-get_trace_length ()
+get_semitrace_length ()
 {
   int run;
   int length;
@@ -608,16 +608,16 @@ int
 iterate_role_sends (int (*func) ())
 {
   int send_wrapper (Protocol p, Role r, Roledef rd, int i)
-    {
+  {
-      if (rd->type == SEND)
+    if (rd->type == SEND)
-	{
+      {
-	  return func (p,r,rd,i);
+	return func (p, r, rd, i);
-	}
+      }
-      else
+    else
-	{
+      {
-	  return 1;
+	return 1;
-	}
+      }
-    }
+  }
 
   return iterate_role_events (send_wrapper);
 }
@@ -1571,7 +1571,7 @@ printSemiState ()
   indentPrint ();
   eprintf ("!!\n");
   indentPrint ();
-  eprintf ("!! Trace length: %i\n", get_trace_length ());
+  eprintf ("!! Trace length: %i\n", get_semitrace_length ());
   open = 0;
   for (run = 0; run < sys->maxruns; run++)
     {
@@ -1718,7 +1718,8 @@ isOpenNonceVar (Term t)
 //! Count unique open variables in term
 /**
  */
-int count_open_variables (const Term t)
+int
+count_open_variables (const Term t)
 {
   Termlist tl;
   int n;
@@ -1758,7 +1759,7 @@ term_noncevariables_level (const Term t)
     }
   else
     {
-      return 1 - (onv/enough);
+      return 1 - (onv / enough);
     }
 }
 
@@ -1880,13 +1881,13 @@ select_goal ()
 	      }
 
 	      void erode (const int w, const float fl)
-		{
+	      {
-		  if (smode & 1)
+		if (smode & 1)
-		    {
+		  {
-		      adapt (w,fl);
+		    adapt (w, fl);
-		    }
+		  }
-		  smode = smode / 2;
+		smode = smode / 2;
-		}
+	      }
 
 	      // buf_constrain is the addition of the factors before division by weight
 	      buf_constrain = 0;
@@ -1900,15 +1901,15 @@ select_goal ()
 
 	      // Determine buf_constrain levels
 	      // Bit 0: 1 constrain level
-		erode (1, term_constrain_level (b->term));
+	      erode (1, term_constrain_level (b->term));
 	      // Bit 1: 2 key level (inverted)
-		erode (1, 0.5 * (1 - b->level));
+	      erode (1, 0.5 * (1 - b->level));
 	      // Bit 2: 4 consequence level
-		erode (1, termBindConsequences (b->term));
+	      erode (1, termBindConsequences (b->term));
 	      // Bit 3: 8 single variables first
-		erode (1, 1 - isTermVariable (b->term));
+	      erode (1, 1 - isTermVariable (b->term));
 	      // Bit 4: 16 nonce variables level (Cf. what I think is in Athena)
-	        erode (1, term_noncevariables_level (b->term));
+	      erode (1, term_noncevariables_level (b->term));
 	      // Define legal range
 	      if (smode > 0)
 		error ("--goal-select mode %i is illegal", mode);
@@ -2725,7 +2726,7 @@ prune_bounds ()
     }
 
   // Limit on exceeding any attack length
-  if (sys->prune == 2 && get_trace_length () >= attack_length)
+  if (sys->prune == 2 && get_semitrace_length () >= attack_length)
     {
       if (sys->output == PROOF)
 	{
@@ -2835,17 +2836,24 @@ property_check ()
   count_false ();
   if (sys->output == ATTACK)
     {
-      if (sys->latex == 1)
+      if (sys->switchXMLoutput)
 	{
-	  latexSemiState ();
+	  xmlOutSemitrace (sys);
 	}
       else
 	{
-	  dotSemiState ();
+	  if (sys->latex == 1)
+	    {
+	      latexSemiState ();
+	    }
+	  else
+	    {
+	      dotSemiState ();
+	    }
 	}
     }
   // Store attack length if shorter
-  attack_this = get_trace_length ();
+  attack_this = get_semitrace_length ();
   if (attack_this < attack_length)
     {
       // Shortest attack
@@ -2992,7 +3000,7 @@ arachne ()
 
     tlevel = term_encryption_level (rd->message);
 #ifdef DEBUG
-    if (DEBUGL(3))
+    if (DEBUGL (3))
       {
 	eprintf ("Encryption level %i found for term ", tlevel);
 	termPrint (rd->message);

src/arachne.h

@@ -6,5 +6,6 @@
 void arachneInit (const System sys);
 void arachneDone ();
 int arachne ();
+int get_semitrace_length ();
 
 #endif

src/switches.c

@@ -114,7 +114,7 @@ switcher (const int process, const System sys, int index)
 		// It's the right thing
 		if (optlength + 3 < this_arg_length)
 		  {
-	            arg_pointer = this_arg + 2 + optlength + 1;
+		    arg_pointer = this_arg + 2 + optlength + 1;
 		  }
 		else
 		  {
@@ -177,7 +177,7 @@ switcher (const int process, const System sys, int index)
 	}
 #endif
       this_arg = argv[index];
-      this_arg_length = strlen(this_arg);
+      this_arg_length = strlen (this_arg);
     }
   else
     {
@@ -210,6 +210,19 @@ switcher (const int process, const System sys, int index)
 	}
     }
 
+  if (detect ('x', "xml-output", 0))
+    {
+      if (!process)
+	{
+	  helptext ("-x,--xml-output", "show attack output in XML format");
+	}
+      else
+	{
+	  sys->switchXMLoutput = 1;
+	  return index;
+	}
+    }
+
   if (detect ('m', "match", 1))
     {
       if (!process)
@@ -517,9 +530,10 @@ switcher (const int process, const System sys, int index)
 		{
 		  fprintf (stderr, "Unknown switch '%s'.\n", this_arg);
 		}
-		  else
+	      else
 		{
-		  fprintf (stderr, "Could not open input file '%s'.\n", this_arg);
+		  fprintf (stderr, "Could not open input file '%s'.\n",
+			   this_arg);
 		}
 	      exit (1);
 	    }

src/system.c

@@ -75,8 +75,9 @@ systemInit ()
   sys->switchReduceClaims = 1;	// default remove claims from duplicate instance choosers
   sys->switchClaims = 0;	// default don't report on claims
   sys->switchClaimToCheck = NULL;	// default check all claims
+  sys->switchXMLoutput = 0;	// default no xml output
   sys->switchGoalSelectMethod = 3;	// default goal selection method
-  sys->traverse = 12;			// default traversal method
+  sys->traverse = 12;		// default traversal method
 
   sys->switch_maxproofdepth = INT_MAX;
   sys->switch_maxtracelength = INT_MAX;
@@ -262,7 +263,8 @@ ensureValidRun (const System sys, int run)
   /* update size parameter */
   oldsize = sys->maxruns;
   sys->maxruns = run + 1;
-  sys->runs = (Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns));
+  sys->runs =
+    (Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns));
 
   /* create runs, set the new pointer(s) to NULL */
   for (i = oldsize; i < sys->maxruns; i++)
@@ -408,7 +410,7 @@ agentOfRunRole (const System sys, const int run, const Term role)
 	  Term agent;
 
 	  agent = agents->term;
-	  if (TermSymb(role) == TermSymb(agent))
+	  if (TermSymb (role) == TermSymb (agent))
 	    {
 	      return agent;
 	    }
@@ -671,15 +673,15 @@ roleInstanceArachne (const System sys, const Protocol protocol,
   Run runs;
   Roledef rd;
   Termlist scanfrom, scanto;
-  Termlist fromlist = NULL;		// deleted at the end
+  Termlist fromlist = NULL;	// deleted at the end
-  Termlist tolist = NULL;		// -> .locals
+  Termlist tolist = NULL;	// -> .locals
-  Termlist artefacts = NULL;		// -> .artefacts
+  Termlist artefacts = NULL;	// -> .artefacts
-  Term extterm = NULL;			// construction thing (will go to artefacts)
+  Term extterm = NULL;		// construction thing (will go to artefacts)
 
   /* claim runid, allocate space */
   rid = sys->maxruns;
-  ensureValidRun (sys, rid);		// creates a new block
+  ensureValidRun (sys, rid);	// creates a new block
-  runs = sys->runs;			// simple structure pointer transfer (shortcut)
+  runs = sys->runs;		// simple structure pointer transfer (shortcut)
 
   /* duplicate roledef in buffer rd */
   /* Notice that it is not stored (yet) in the run structure,
@@ -712,7 +714,7 @@ roleInstanceArachne (const System sys, const Protocol protocol,
        * of it again.
        */
       oldt = scanfrom->term;
-      newt = deVar(oldt);
+      newt = deVar (oldt);
       if (realTermVariable (newt))
 	{
 	  /* This is a variable of the role, that is not instantiated yet.
@@ -1035,31 +1037,31 @@ roleInstanceDestroy (const System sys)
 	    }
 	  substlist = substlist->next;
 	}
-      termlistDelete(myrun.substitutions);
+      termlistDelete (myrun.substitutions);
 
       // sys->variables might contain locals from the run: remove them
-        {
+      {
-	  Termlist tl;
+	Termlist tl;
 
-	  tl = sys->variables;
+	tl = sys->variables;
-	  while (tl != NULL)
+	while (tl != NULL)
-	    {
+	  {
-	      Term t;
+	    Term t;
 
-	      t = tl->term;
+	    t = tl->term;
-	      if (realTermLeaf(t) && TermRunid(t) == runid)
+	    if (realTermLeaf (t) && TermRunid (t) == runid)
-		{
+	      {
-		  // remove from list; return pointer to head
+		// remove from list; return pointer to head
-		  sys->variables = termlistDelTerm (tl);
+		sys->variables = termlistDelTerm (tl);
-		  tl = sys->variables;
+		tl = sys->variables;
-		}
+	      }
-	      else
+	    else
-		{
+	      {
-		  // proceed
+		// proceed
-	          tl = tl->next;
+		tl = tl->next;
-		}
+	      }
-	    }
+	  }
-	}
+      }
 
       // remove lists
       termlistDelete (myrun.artefacts);
@@ -1069,7 +1071,8 @@ roleInstanceDestroy (const System sys)
       // Destroy run struct allocation in array using realloc
       // Reduce run count
       sys->maxruns = sys->maxruns - 1;
-      sys->runs = (Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns));
+      sys->runs =
+	(Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns));
     }
 }
 

src/system.h

@@ -143,6 +143,7 @@ struct system
   int switchClaims;		//!< Enable clails report
   int switchGoalSelectMethod;	//!< Goal selection method for Arachne engine
   Term switchClaimToCheck;	//!< Which claim should be checked?
+  int switchXMLoutput;		//!< xml output
 
   //! Latex output switch.
   /**

src/xmlout.c

@@ -0,0 +1,336 @@
+/*
+ * xmlout.c
+ *
+ * XML output for Scyther
+ *
+ * Module to output detailed Scyther information in XML format, for easier
+ * interaction with external programs. Originally developed for attack output
+ * details.
+ */
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <stdarg.h>
+
+#include "term.h"
+#include "termlist.h"
+#include "system.h"
+#include "binding.h"
+#include "arachne.h"		// for get_semitrace_length
+
+#include "xmlout.h"
+
+/*
+ * Global/static stuff.
+ */
+static int xmlindent;		// indent level for xml elements in output
+
+/*
+ * Default external interface: init/done
+ */
+
+//! Init this module
+void
+xmlOutInit (void)
+{
+  xmlindent = 0;
+}
+
+//! Close up
+void
+xmlOutDone (void)
+{
+}
+
+/*
+ * Local code, needed for any further real code.
+ */
+
+//! Indent code
+void
+xmlIndentPrint ()
+{
+  int i;
+
+  i = xmlindent;
+  while (i > 0)
+    {
+      printf ("   ");
+      i--;
+    }
+}
+
+//! XML print
+/**
+ * Input is comparable to printf, but indents (according to xmlindent) and adds
+ * a newline.
+ */
+void
+xmlPrint (char *fmt, ...)
+{
+  va_list args;
+
+  xmlIndentPrint ();
+  va_start (args, fmt);
+  vfprintf (stdout, fmt, args);
+  va_end (args);
+  printf ("\n");
+}
+
+//! Print a simple integer value element
+void
+xmlOutInteger (const char *tag, const int value)
+{
+  xmlPrint ("<%s>%i</%s>", tag, value, tag);
+}
+
+//! Print a term for an element
+void
+xmlOutTerm (const char *tag, const Term term)
+{
+  if (term != NULL)
+    {
+      xmlIndentPrint ();
+      printf ("<%s>", tag);
+      termPrint (term);
+      printf ("</%s>\n", tag);
+    }
+}
+
+//! Attribute term
+void
+xmlAttrTerm (const char *tag, const Term term)
+{
+  if (term != NULL)
+    {
+      printf (" %s=\"", tag);
+      termPrint (term);
+      printf ("\"");
+    }
+}
+
+//! Global system info
+/**
+ * To be used by concrete trace as well as semitrace output
+ */
+void
+xmlOutSysInfo (const System sys)
+{
+  xmlPrint ("<system>");
+  xmlindent++;
+
+  {
+    Protocol p;
+
+    p = sys->protocols;
+    while (p != NULL)
+      {
+	xmlOutTerm ("protocol", p->nameterm);
+	p = p->next;
+      }
+  }
+
+  xmlOutInteger ("match", sys->match);
+
+  xmlindent--;
+  xmlPrint ("</system>");
+}
+
+//! 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)
+{
+  Role r;
+  Term oldagent;
+
+  xmlOutInteger ("runid", run);
+  xmlOutTerm ("protocol", sys->runs[run].protocol->nameterm);
+  r = sys->runs[run].role;
+
+  /* undo substitution temporarily to retrieve role name */
+  /* Note that this is fairly tailored towards the Arachne method, TODO: make
+   * more generic. */
+  oldagent = r->nameterm->subst;
+  r->nameterm->subst = NULL;
+  xmlOutTerm ("role", r->nameterm);
+  /* reinstate substitution */
+  r->nameterm->subst = oldagent;
+  if (oldagent != NULL)
+    {
+      xmlOutTerm ("agent", r->nameterm);
+    }
+}
+
+//! Show a single event from a run
+/**
+ * run and index will only be output if they are nonnegative.
+ */
+void
+xmlOutEvent (const System sys, Roledef rd, const int run, const int index)
+{
+  xmlIndentPrint ();
+
+  printf ("<");
+  switch (rd->type)
+    {
+      /* Read or send types are fairly similar.
+       * Currently, choose events are not distinguished yet. TODO
+       */
+    case READ:
+      printf ("read");
+      break;
+    case SEND:
+      printf ("send");
+      break;
+    case CLAIM:
+      printf ("claim");
+      break;
+    default:
+      printf ("unknown code=\"%i\"", rd->type);
+      break;
+    }
+
+  xmlAttrTerm ("label", rd->label);
+  if (rd->type != CLAIM)
+    {
+      /* read or send */
+      xmlAttrTerm ("from", rd->from);
+      xmlAttrTerm ("to", rd->to);
+      xmlAttrTerm ("message", rd->message);
+    }
+  else
+    {
+      /* claim */
+      xmlAttrTerm ("role", rd->from);
+      xmlAttrTerm ("type", rd->to);
+      xmlAttrTerm ("argument", rd->message);
+    }
+
+  if (run >= 0)
+    {
+      printf (" run=\"%i\"", run);
+    }
+  if (index >= 0)
+    {
+      printf (" index=\"%i\"", index);
+    }
+  printf (" />\n");
+}
+
+//! Display runs
+void
+xmlOutRuns (const System sys)
+{
+  int run;
+
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      xmlPrint ("<run>");
+      xmlindent++;
+
+      xmlRunInfo (sys, run);
+
+      xmlPrint ("<eventlist>");
+      xmlindent++;
+      {
+	Roledef rd;
+	int index;
+
+	index = 0;
+	rd = sys->runs[run].start;
+	while (rd != NULL)
+	  {
+	    xmlOutEvent (sys, rd, -1, index);
+	    index++;
+	    rd = rd->next;
+	  }
+      }
+      xmlindent--;
+      xmlPrint ("</eventlist>");
+      xmlindent--;
+      xmlPrint ("</run>");
+    }
+}
+
+
+//! Output list of bindings
+void
+xmlOutBindings (const System sys)
+{
+  int xmlBindingState (void *dt)
+  {
+    Binding b;
+    void xmlRunIndex (char *desc, const int run, const int index)
+    {
+      xmlPrint ("<%s run=\"%i\" index=\"%i\" />", desc, run, index);
+    }
+
+    b = (Binding) dt;
+    xmlIndentPrint ();
+    printf ("<binding term=\"");
+    termPrint (b->term);
+    printf ("\" />\n");
+    xmlindent++;
+    if (b->done)
+      xmlRunIndex ("from", b->run_from, b->ev_from);
+    else
+      xmlPrint ("<unbound />");
+    xmlRunIndex ("to", b->run_to, b->ev_to);
+    if (b->blocked)
+      printf ("<blocked />");
+    xmlindent--;
+    xmlPrint ("</binding>");
+    return 1;
+  }
+
+  xmlPrint ("<bindinglist>");
+  xmlindent++;
+  if (sys->bindings != NULL)
+    {
+      list_iterate (sys->bindings, xmlBindingState);
+    }
+  xmlindent--;
+  xmlPrint ("</bindinglist>");
+}
+
+/*
+ * -----------------------------------------------------------------------------------
+ * Publicly available functions
+ */
+
+//! Output for a concrete trace (from modelchecker)
+void
+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.
+ */
+void
+xmlOutSemitrace (const System sys)
+{
+  xmlIndentPrint ();
+  printf ("<attack");
+  /* add trace length attribute */
+  printf (" tracelength=\"%i\"", get_semitrace_length ());
+  printf (">\n");
+  xmlindent++;
+  /* any global information about the system */
+  xmlOutSysInfo (sys);
+  xmlPrint ("<semitrace>");
+  xmlindent++;
+  xmlOutRuns (sys);
+  xmlOutBindings (sys);
+  xmlindent--;
+  xmlPrint ("</semitrace>");
+  xmlindent--;
+  xmlPrint ("</attack>");
+}

src/xmlout.h

@@ -0,0 +1,12 @@
+#ifndef XMLOUT
+#define XMLOUT
+
+#include "system.h"
+
+void xmlOutInit (void);
+void xmlOutDone (void);
+
+void xmlOutSemitrace (const System sys);
+void xmlOutTrace (const System sys);
+
+#endif