- Split roleInstance into two more managable parts.

src/system.c

@@ -327,7 +327,8 @@ runsPrint (const System sys)
 }
 
 //! Determine whether a term is sent or claimed, but not read first in a roledef
-int not_read_first (const Roledef rdstart, const Term t)
+int
+not_read_first (const Roledef rdstart, const Term t)
 {
   Roledef rd;
 
@@ -377,7 +378,9 @@ agentOfRunRole (const System sys, const int run, const Term role)
     }
   else
     {
-      error ("Agent list for run %i is empty, so agentOfRunRole is not usable.", run);
+      error
+	("Agent list for run %i is empty, so agentOfRunRole is not usable.",
+	 run);
     }
   return NULL;
 }
@@ -512,7 +515,105 @@ firstNonAgentRead (const System sys, int rid)
 }
 
 
-//! Instantiate a role by making a new run.
+/*************************************************
+ *
+ * Support code for roleInstance
+ *
+*************************************************/
+
+//! Prefix a read before a given run.
+/**
+ * Maybe this simply needs integration in the role definitions. However, in practice it
+ * depends on the specific scenario. For Arachne it can thus depend on the roledef.
+ *
+ * Stores the (new) rd pointer in start and index
+ */
+void
+run_prefix_read (const System sys, const int run, Roledef rd,
+		 const Term extterm)
+{
+  /* prefix a read for such reads. TODO: this should also cover any external stuff */
+  if (extterm != NULL)
+    {
+      Roledef rdnew;
+
+      rdnew = roledefInit (READ, NULL, NULL, NULL, extterm, NULL);
+      /* this is an internal action! */
+      rdnew->internal = 1;
+      /* Store this new pointer */
+      rdnew->next = rd;
+      rd = rdnew;
+      /* mark the first real action */
+      sys->runs[run].firstReal++;
+    }
+  /* possibly shifted rd */
+  sys->runs[run].start = rd;
+  sys->runs[run].index = rd;
+}
+
+
+//! Create a new local
+/**
+ * Given a term, construct a new local term. Returns NULL if no such term was constructed.
+ */
+Term
+create_new_local (const Term t, const int rid)
+{
+  if (t != NULL && realTermLeaf (t))
+    {
+      Term newt;
+
+      newt = makeTermType (t->type, t->left.symb, rid);
+      newt->stype = t->stype;
+
+      return newt;
+    }
+  else
+    {
+      return NULL;
+    }
+}
+
+//! Localize run
+/**
+ * Takes a run roledef list and substitutes fromlist into tolist terms.
+ * Furthermore, localizes all substitutions occurring in this, which termLocal
+ * does not. Any localized substitutions are stored as well in a list.
+ */
+void
+run_localize (const System sys, const int rid, Termlist fromlist,
+	      Termlist tolist, Termlist substlist)
+{
+  Roledef rd;
+
+  rd = sys->runs[rid].start;
+  while (rd != NULL)
+    {
+      rd->from = termLocal (rd->from, fromlist, tolist, rid);
+      rd->to = termLocal (rd->to, fromlist, tolist, rid);
+      rd->message = termLocal (rd->message, fromlist, tolist, rid);
+      rd = rd->next;
+    }
+
+  sys->runs[rid].substitutions = NULL;
+  while (substlist != NULL)
+    {
+      Term t;
+
+      t = substlist->term;
+      if (t->subst != NULL)
+	{
+	  t->subst = termLocal (t->subst, fromlist, tolist, rid);
+	  sys->runs[rid].substitutions =
+	    termlistAdd (sys->runs[rid].substitutions, t);
+	}
+      substlist = substlist->next;
+    }
+}
+
+
+
+//! Instantiate a role by making a new run for Arachne
 /**
  * This involves creation of a new run(id).
  * Copy & subst of Roledef, Agent knowledge.
@@ -520,8 +621,9 @@ firstNonAgentRead (const System sys, int rid)
 */
 
 void
-roleInstance (const System sys, const Protocol protocol, const Role role,
+roleInstanceArachne (const System sys, const Protocol protocol,
-	      const Termlist paramlist, Termlist substlist)
+		     const Role role, const Termlist paramlist,
+		     Termlist substlist)
 {
   int rid;
   Run runs;
@@ -549,66 +651,10 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
 
   /* scan for types in agent list */
   /* scanners */
-  if (sys->engine != ARACHNE_ENGINE)
-    {
-      // Default engine adheres to scenario
-      scanfrom = protocol->rolenames;
-      scanto = paramlist;
-      while (scanfrom != NULL && scanto != NULL)
-	{
-	  fromlist = termlistAdd (fromlist, scanfrom->term);
-	  if (scanto->term->stype != NULL &&
-	      inTermlist (scanto->term->stype, TERM_Type))
-	    {
-	      Term newvar;
-
-	      /* There is a TYPE constant in the parameter list.
-	       * Generate a new local variable for this run, with this type */
-	      newvar =
-		makeTermType (VARIABLE, scanfrom->term->left.symb, rid);
-	      artefacts = termlistAdd (artefacts, newvar);
-	      sys->variables = termlistAdd (sys->variables, newvar);
-	      newvar->stype = termlistAdd (NULL, scanto->term);
-	      tolist = termlistAdd (tolist, newvar);
-	      /* newvar is apparently new, but it might occur
-	       * in the first event if it's a read, in which
-	       * case we forget it */
-	      if (sys->switchForceChoose || not_read_first (rd, scanfrom->term))
-		{
-		  /* this term is forced as a choose, or it does not occur in the (first) read event */
-		  if (extterm == NULL)
-		    {
-		      extterm = newvar;
-		    }
-		  else
-		    {
-		      extterm = makeTermTuple (newvar, extterm);
-		      artefacts = termlistAdd (artefacts, extterm);
-		    }
-		}
-	    }
-	  else
-	    {
-	      /* not a type constant, add to list */
-	      tolist = termlistAdd (tolist, scanto->term);
-	    }
-	  scanfrom = scanfrom->next;
-	  scanto = scanto->next;
-	}
-
-      /* set agent list */
-      runs[rid].agents = termlistDuplicate (tolist);
-
-    }
-  else
-    {
-      // For the Arachne engine, we need to copy all these roles to new variables
   /**
    * Because of pre-instantiation unification, some variables might already have been filled in.
    * Ignore agent list; instead rely on role->variables.
    */
-      Termlist scanfrom;
-
   runs[rid].agents = NULL;
 
   scanfrom = role->variables;
@@ -667,25 +713,8 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
 
       scanfrom = scanfrom->next;
     }
-    }
 
-  /* prefix a read for such reads. TODO: this should also cover any external stuff */
+  run_prefix_read (sys, rid, rd, extterm);
-  if (extterm != NULL)
-    {
-      Roledef rdnew;
-
-      rdnew = roledefInit (READ, NULL, NULL, NULL, extterm, NULL);
-      /* this is an internal action! */
-      rdnew->internal = 1;
-      rdnew->next = rd;
-      rd = rdnew;
-      /* mark the first real action */
-      runs[rid].firstReal++;
-    }
-
-  /* possibly shifted rd */
-  runs[rid].start = rd;
-  runs[rid].index = rd;
 
   /* duplicate all locals form this run */
   scanto = role->locals;
@@ -694,15 +723,16 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
       Term t = scanto->term;
       if (!inTermlist (fromlist, t))
 	{
-	  if (realTermLeaf (t))
+	  Term newt;
+
+	  newt = create_new_local (t, rid);
+	  if (newt != NULL)
 	    {
-	      Term newt = makeTermType (t->type, t->left.symb, rid);
 	      artefacts = termlistAdd (artefacts, newt);
 	      if (realTermVariable (newt))
 		{
 		  sys->variables = termlistAdd (sys->variables, newt);
 		}
-	      newt->stype = t->stype;
 	      fromlist = termlistAdd (fromlist, t);
 	      tolist = termlistAdd (tolist, newt);
 	    }
@@ -712,39 +742,139 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
 
   /* TODO this is not what we want yet, also local knowledge. The local
    * knowledge (list?) also needs to be substituted on invocation. */
-  if (sys->engine == ARACHNE_ENGINE)
-    {
   runs[rid].know = NULL;
+
+  /* now adjust the local run copy */
+  run_localize (sys, rid, fromlist, tolist, substlist);
+
+  termlistDelete (fromlist);
+  runs[rid].locals = tolist;
+  runs[rid].artefacts = artefacts;
+
+  /* erase any substitutions in the role definition, as they are now copied */
+  termlistSubstReset (role->variables);
+}
+
+
+
+//! Instantiate a role by making a new run for the Modelchecker
+/**
+ * This involves creation of a new run(id).
+ * Copy & subst of Roledef, Agent knowledge.
+ * Tolist might contain type constants.
+*/
+
+void
+roleInstanceModelchecker (const System sys, const Protocol protocol,
+			  const Role role, const Termlist paramlist,
+			  Termlist substlist)
+{
+  int rid;
+  Run runs;
+  Roledef rd;
+  Termlist scanfrom, scanto;
+  Termlist fromlist = NULL;
+  Termlist tolist = NULL;
+  Termlist artefacts = NULL;
+  Term extterm = NULL;
+
+  /* claim runid, allocate space */
+  rid = sys->maxruns;
+  ensureValidRun (sys, rid);
+  runs = sys->runs;
+
+  /* duplicate roledef in buffer rd */
+  rd = roledefDuplicate (role->roledef);
+
+  /* set parameters */
+  /* generic setup */
+  runs[rid].protocol = protocol;
+  runs[rid].role = role;
+  runs[rid].step = 0;
+  runs[rid].firstReal = 0;
+
+  /* scan for types in agent list */
+  /* scanners */
+  // Default engine adheres to scenario
+  scanfrom = protocol->rolenames;
+  scanto = paramlist;
+  while (scanfrom != NULL && scanto != NULL)
+    {
+      fromlist = termlistAdd (fromlist, scanfrom->term);
+      if (scanto->term->stype != NULL &&
+	  inTermlist (scanto->term->stype, TERM_Type))
+	{
+	  Term newvar;
+
+	  /* There is a TYPE constant in the parameter list.
+	   * Generate a new local variable for this run, with this type */
+	  newvar = makeTermType (VARIABLE, scanfrom->term->left.symb, rid);
+	  artefacts = termlistAdd (artefacts, newvar);
+	  sys->variables = termlistAdd (sys->variables, newvar);
+	  newvar->stype = termlistAdd (NULL, scanto->term);
+	  tolist = termlistAdd (tolist, newvar);
+	  /* newvar is apparently new, but it might occur
+	   * in the first event if it's a read, in which
+	   * case we forget it */
+	  if (sys->switchForceChoose || not_read_first (rd, scanfrom->term))
+	    {
+	      /* this term is forced as a choose, or it does not occur in the (first) read event */
+	      if (extterm == NULL)
+		{
+		  extterm = newvar;
 		}
 	      else
 		{
-      runs[rid].know = knowledgeDuplicate (sys->know);
+		  extterm = makeTermTuple (newvar, extterm);
+		  artefacts = termlistAdd (artefacts, extterm);
 		}
+	    }
+	}
+      else
+	{
+	  /* not a type constant, add to list */
+	  tolist = termlistAdd (tolist, scanto->term);
+	}
+      scanfrom = scanfrom->next;
+      scanto = scanto->next;
+    }
+
+  /* set agent list */
+  runs[rid].agents = termlistDuplicate (tolist);
+
+  run_prefix_read (sys, rid, rd, extterm);
+
+  /* duplicate all locals form this run */
+  scanto = role->locals;
+  while (scanto != NULL)
+    {
+      Term t = scanto->term;
+      if (!inTermlist (fromlist, t))
+	{
+	  Term newt;
+
+	  newt = create_new_local (t, rid);
+	  if (newt != NULL)
+	    {
+	      artefacts = termlistAdd (artefacts, newt);
+	      if (realTermVariable (newt))
+		{
+		  sys->variables = termlistAdd (sys->variables, newt);
+		}
+	      fromlist = termlistAdd (fromlist, t);
+	      tolist = termlistAdd (tolist, newt);
+	    }
+	}
+      scanto = scanto->next;
+    }
+
+  /* TODO this is not what we want yet, also local knowledge. The local
+   * knowledge (list?) also needs to be substituted on invocation. */
+  runs[rid].know = knowledgeDuplicate (sys->know);
 
   /* now adjust the local run copy */
+  run_localize (sys, rid, fromlist, tolist, substlist);
 
-  rd = runs[rid].start;
-  while (rd != NULL)
-    {
-      rd->from = termLocal (rd->from, fromlist, tolist, rid);
-      rd->to = termLocal (rd->to, fromlist, tolist, rid);
-      rd->message = termLocal (rd->message, fromlist, tolist, rid);
-      rd = rd->next;
-    }
-
-  runs[rid].substitutions = NULL;
-  while (substlist != NULL)
-    {
-      Term t;
-
-      t = substlist->term;
-      if (t->subst != NULL)
-	{
-	  t->subst = termLocal (t->subst, fromlist, tolist, rid);
-	  runs[rid].substitutions = termlistAdd (runs[rid].substitutions, t);
-	}
-      substlist = substlist->next;
-    }
   termlistDelete (fromlist);
   runs[rid].locals = tolist;
   runs[rid].artefacts = artefacts;
@@ -762,6 +892,27 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
     }
 }
 
+//! Instantiate a role by making a new run
+/**
+ * Generic splitter. Splits into the arachne version, or the modelchecker version.
+ *
+ * This involves creation of a new run(id).
+ * Copy & subst of Roledef, Agent knowledge.
+ * Tolist might contain type constants.
+*/
+void
+roleInstance (const System sys, const Protocol protocol, const Role role,
+	      const Termlist paramlist, Termlist substlist)
+{
+  if (sys->engine == ARACHNE_ENGINE)
+    {
+      roleInstanceArachne (sys, protocol, role, paramlist, substlist);
+    }
+  else
+    {
+      roleInstanceModelchecker (sys, protocol, role, paramlist, substlist);
+    }
+}
 
 //! Destroy roleInstance
 /**

src/termlist.c

@@ -134,7 +134,8 @@ inTermlist (Termlist tl, const Term term)
 }
 
 //! Determine whether a term is an element of a termlist: yield pointer
-__inline__ Termlist termlistFind (Termlist tl, const Term term)
+__inline__ Termlist
+termlistFind (Termlist tl, const Term term)
 {
 #ifdef DEBUG
   if (term == NULL)
@@ -614,6 +615,9 @@ inverseKey (Termlist inverses, Term key)
 /*
  * We assume that at this point, no variables have been instantiated yet that occur in this term.
  * We also assume that fromlist, tolist only hold real leaves.
+ *
+ * variable instantiations are not followed through.
+ *
  *\sa termlistLocal()
  */
 Term
@@ -622,7 +626,6 @@ termLocal (Term t, Termlist fromlist, Termlist tolist, const int runid)
   if (t == NULL)
     return NULL;
 
-  // deVar (t);                 // remove any instantiated variables from the term.
   if (realTermLeaf (t))
     {
       while (fromlist != NULL && tolist != NULL)
@@ -813,7 +816,8 @@ termlist_iterate (Termlist tl, int (*func) ())
 }
 
 //! Create a tuple term from a termlist
-Term termlist_to_tuple (Termlist tl)
+Term
+termlist_to_tuple (Termlist tl)
 {
   int width;
 
@@ -843,7 +847,8 @@ Term termlist_to_tuple (Termlist tl)
 	  tl = tl->next;
 	  i++;
 	}
-      tresult = makeTermTuple (termlist_to_tuple (tl1), termlist_to_tuple (tl2));
+      tresult =
+	makeTermTuple (termlist_to_tuple (tl1), termlist_to_tuple (tl2));
       termlistDelete (tl1);
       termlistDelete (tl2);
       return tresult;

src/todo.txt

@@ -1,9 +1,5 @@
 - For secrecy, one trusted agent and one untrusted agent suffices.
   Implement this in the modelchecker.
-- Possible bug in Arachne: AV->BV->AV mappings cause loops. This can
-  occur normally, but typically in type flaw stuff. It should be covered
-  by the unification procedure, but I haven't verified it myself that
-  this covers all cased in such a system.
 - Rewrite for untrusted roles, redesign this.
 - Add switch for arachne to prune encryption levels when using -m2.
 - Rewrite termMguTerm such that it iterates and adapt all functions