- Fixed error in error reporting :-\

- Added intruder construction nodes.
- Several cleanups.

src/arachne.c

@@ -374,18 +374,12 @@ bind_goal_regular (const Goal goal)
        *
        * Note that we only bind to regular runs here
        */
-      int flag;
-
       if (p == INTRUDER)
 	{
 	  return 1;		// don't abort scans
 	}
-      flag = bind_existing_run (goal, p, r, index);
+      return (bind_existing_run (goal, p, r, index)
-      if (flag)
+	      && bind_new_run (goal, p, r, index));
-	{
-	  flag = bind_new_run (goal, p, r, index);
-	}
-      return flag;
     }
 
     // Test for interm unification
@@ -397,49 +391,38 @@ bind_goal_regular (const Goal goal)
 }
 
 //! Bind an intruder goal to a regular run
+/**
+ * A bit of a problem child, this one.
+ */
 int
-bind_intruder_to_regular (const Goal goal)
+bind_intruder_to_regular (Goal goal)
 {
-  int bind_this_f2 (Protocol p, Role r, Roledef rd, int index)
+  int bind_this_roleevent (Protocol p, Role r, Roledef rd, int index)
   {
-    int element_f2 (Termlist substlist, Termlist keylist)
+    int bind_this_unification (Termlist substlist, Termlist keylist)
     {
       int flag;
-
-      /**
-       * Note that we only bind to regular runs here
-       */
-      if (p == INTRUDER)
-	{
-	  return 1;		// don't abort scans
-	}
-      else
-	{
       int keygoals;
+      Termlist tl;
 
       /**
-	   * In any case, the list of keys is added as a new goal.
+       * the list of keys is added as a new goal.
        */
-	  int add_key_goal (Term t)
+      keygoals = 0;
+      tl = keylist;
+      while (tl != NULL)
 	{
 	  keygoals++;
-	    create_intruder_goal (t);
+	  create_intruder_goal (tl->term);
 	  //!@todo This needs a mapping Pi relation as well.
-	    return 1;
-	  }
 
-	  keygoals = 0;
+	  tl = tl->next;
-	  termlist_iterate (keylist, add_key_goal);
+	}
       /**
        * Two options; as this, it is from an existing run,
        * or from a new one.
        */
 
-	  /**
-	   * This code has a major bug (memory destruction)
-	   * in both branches
-	   *@todo FIX!!
-	   */
       flag = (bind_existing_run (goal, p, r, index)
 	      && bind_new_run (goal, p, r, index));
 
@@ -454,21 +437,63 @@ bind_intruder_to_regular (const Goal goal)
 
       return flag;
     }
-    }
 
-    // Test for subterm unification
+  /**
-    return termMguSubTerm (goal.rd->message, rd->message, element_f2,
+   * Note that we only bind to regular runs here
-			   sys->traceKnow[0]->inverses, NULL);
+   */
+    if (p == INTRUDER)
+      {
+	return 1;		// don't abort scans
+      }
+    else
+      {				// Test for subterm unification
+	return termMguSubTerm (goal.rd->message, rd->message,
+			       bind_this_unification, sys->know->inverses,
+			       NULL);
+      }
   }
 
   // Bind to all possible sends?
-  return iterate_role_sends (bind_this_f2);
+  return iterate_role_sends (bind_this_roleevent);
 }
 
 //! Bind an intruder goal by intruder construction
 int
 bind_intruder_to_construct (const Goal goal)
 {
+  Term term;
+
+  term = goal.rd->message;
+  if (!realTermLeaf (term))
+    {
+      Term t1, t2;
+      int flag;
+
+      if (realTermTuple (term))
+	{
+	  // tuple construction
+	  t1 = term->left.op1;
+	  t2 = term->right.op2;
+	}
+      else
+	{
+	  // must be encryption
+	  t1 = term->left.op;
+	  t2 = term->right.key;
+	}
+      create_intruder_goal (t1);
+      create_intruder_goal (t2);
+
+      flag = iterate ();
+
+      roleInstanceDestroy (sys);
+      roleInstanceDestroy (sys);
+      return flag;
+    }
+  else
+    {
+      return 1;
+    }
 }
 
 
@@ -504,7 +529,7 @@ bind_goal (const Goal goal)
 int
 prune ()
 {
-  if (indentDepth > 2)
+  if (indentDepth > 10)
     {
       // Hardcoded limit on iterations
 #ifdef DEBUG
@@ -569,11 +594,6 @@ iterate ()
 	      eprintf (" ");
 	    }
 	  eprintf ("\n");
-	  explanation = NULL;
-	  e_run = INVALID;
-	  e_term1 = NULL;
-	  e_term2 = NULL;
-	  e_term3 = NULL;
 	}
 #endif
 
@@ -605,6 +625,13 @@ iterate ()
 	  flag = bind_goal (goal);
 	}
     }
+#ifdef DEBUG
+  explanation = NULL;
+  e_run = INVALID;
+  e_term1 = NULL;
+  e_term2 = NULL;
+  e_term3 = NULL;
+#endif
   indentDepth--;
   return flag;
 }

src/mgu.c

@@ -73,7 +73,7 @@ termMguTerm (Term t1, Term t2)
     }
 
   /* symmetrical tests for single variable */
-  if (isTermVariable (t1))
+  if (realTermVariable (t1))
     {
       if (termOccurs (t2, t1))
 	return MGUFAIL;
@@ -86,7 +86,7 @@ termMguTerm (Term t1, Term t2)
 	  return termlistAdd (NULL, t1);
 	}
     }
-  if (isTermVariable (t2))
+  if (realTermVariable (t2))
     {
       if (termOccurs (t1, t2))
 	return MGUFAIL;
@@ -106,7 +106,7 @@ termMguTerm (Term t1, Term t2)
 
   /* identical compounds */
   /* encryption first */
-  if (isTermEncrypt (t1))
+  if (realTermEncrypt (t1))
     {
       Termlist tl1, tl2;
 
@@ -175,7 +175,7 @@ termMguInTerm (Term t1, Term t2, int (*iterator) ())
   t2 = deVar (t2);
   if (t2 != NULL)
     {
-      if (isTermTuple (t2))
+      if (realTermTuple (t2))
 	{
 	  // t2 is a tuple, consider interm options as well.
 	  flag = flag && termMguInTerm (t1, t2->left.op1, iterator);
@@ -210,9 +210,9 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (),
   t2 = deVar (t2);
   if (t2 != NULL)
     {
-      if (!isTermLeaf (t2))
+      if (!realTermLeaf (t2))
 	{
-	  if (isTermTuple (t2))
+	  if (realTermTuple (t2))
 	    {
 	      // 'simple' tuple
 	      flag =

src/system.c

@@ -596,8 +596,9 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
 	    {
 	      // Make new var for this run
 	      newt = makeTermType (VARIABLE, newt->left.symb, rid);
-	      newt->subst = oldt->subst;
 	      artefacts = termlistAdd (artefacts, newt);
+	      // Copy substitution
+	      newt->subst = oldt->subst;
 	    }
 	  // Add to agent list, possibly
 	  if (inTermlist (protocol->rolenames, oldt))

src/termlist.c

@@ -601,7 +601,7 @@ termLocal (Term t, Termlist fromlist, Termlist tolist, const int runid)
   if (t == NULL)
     return NULL;
 
-  deVar (t);			// remove any instantiated variables from the term.
+  // deVar (t);                 // remove any instantiated variables from the term.
   if (realTermLeaf (t))
     {
       while (fromlist != NULL && tolist != NULL)