- [[[ Broken commit ]]]

More work on the arachne multiple-decryptor. Horrific.

src/arachne.c

@@ -764,48 +764,48 @@ getPriorityOfNeededKey (const System sys, const Term keyneeded)
  *
  * The key goals are bound to the goal. Iterates on success.
  */
-int
+void
 bind_existing_to_goal (const Binding b, const int run, const int index)
 {
   int old_length;
-  int flag;
   int newgoals;
+  Term goalterm;
 
-  int subterm_unification_needs (const Binding bt, Term tbig)
+  int subterm_unification_needs (Term tbig, const int r, const int e)
   {
     Term t;
-    int flag;
 
-    int bind_iterate (Termlist tl)
+    void bind_iterate (Termlist tl)
     {
-      if (goal_bind (bt, run, index))
+      if (goal_bind (b, r, e))
 	{
-	  int flag;
+	  if (switches.output == PROOF)
-
+	    {
-	  flag = iterate ();
+	      indentPrint ();
-	  goal_unbind (bt);
+	      eprintf ("Iterating for ");
-	  return flag;
+	      termPrint (b->term);
+	      eprintf (" to occur first in ");
+	      termPrint (roledef_shift (sys->runs[run].start, index)->
+			 message);
+	      eprintf ("\n");
+	    }
+	  iterate ();
+	  goal_unbind (b);
 	}
-      return false;
     }
 
-    if (bt == NULL)
+    t = deVar (b->term);
-      {
-	return false;
-      }
-    flag = false;
-    t = deVar (bt->term);
     tbig = deVar (tbig);
 
     // First check whether it unifies in a simple way
-    flag = flag || unify (t, tbig, NULL, bind_iterate);
+    unify (t, tbig, NULL, bind_iterate);
 
     // The other options are unification on subparts
     if (realTermTuple (tbig))
       {
 	// Either one will do
-	return (subterm_unification_needs (bt, TermOp1 (tbig)) ||
+	subterm_unification_needs (TermOp1 (tbig), r, e);
-		subterm_unification_needs (bt, TermOp1 (tbig)));
+	subterm_unification_needs (TermOp1 (tbig), r, e);
       }
     if (realTermEncrypt (tbig))
       {
@@ -816,6 +816,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
 	int newgoals;
 	Binding bnew;
 
+	indentDepth++;
 	// Maybe we can bind to the inner thing. Try.
 	// Add decryptor run
 	keyneeded = inverseKey (sys->know->inverses, TermKey (tbig));
@@ -823,6 +824,17 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
 	smallrun = create_decryptor (tbig, keyneeded);
 	rddecrypt = sys->runs[smallrun].start;
 
+	if (switches.output == PROOF)
+	  {
+	    indentPrint ();
+	    eprintf
+	      ("This introduces the obligation to decrypt the following subterm: ");
+	    termPrint (tbig);
+	    eprintf (" to be decrypted using ");
+	    termPrint (keyneeded);
+	    eprintf ("\n");
+	  }
+
 	/*
 	 * 2. Add goal bindings
 	 */
@@ -850,14 +862,31 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
 
 	newgoals += goal_add (rddecrypt->next->message, smallrun, 1,
 			      prioritylevel);
-	/*
+	if (switches.output == PROOF)
-	 * 3. Bind open goal to decryptor
-	 */
-	if (goal_bind (bt, smallrun, 2))
 	  {
-	    // Allright, good binding, proceed with next
+	    indentPrint ();
-	    flag = flag || subterm_unification_needs (bnew, TermOp (tbig));
+	    eprintf
-	    goal_unbind (bt);
+	      ("To this end, we added two new goals and one new send: ");
+	    termPrint (rddecrypt->message);
+	    eprintf (",");
+	    termPrint (rddecrypt->next->message);
+	    eprintf (",");
+	    termPrint (rddecrypt->next->next->message);
+	    eprintf ("\n");
+	  }
+
+	/*
+	 * 3. Bind open goal to decryptor? 
+	 */
+	if (goal_bind (bnew, r, e))
+	  {
+	    if (switches.output == PROOF)
+	      {
+		indentPrint ();
+		eprintf ("Bound: trying new subterm_unfication_needs.\n");
+	      }
+	    subterm_unification_needs (TermOp (tbig), smallrun, 2);
+	    goal_unbind (bnew);
 	  }
 	/*
 	 * clean up
@@ -865,14 +894,12 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
 	termDelete (keyneeded);
 	goal_remove_last (newgoals);
 	semiRunDestroy ();
-
+	indentDepth--;
-	return flag;
       }
-    return false;
   }
 
   old_length = sys->runs[run].height;
-  if ((index + 1) > old_length)
+  if (index >= old_length)
     {
       newgoals = add_read_goals (run, old_length, index + 1);
     }
@@ -880,16 +907,13 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
     {
       newgoals = 0;
     }
-  flag =
+  goalterm = roledef_shift (sys->runs[run].start, index)->message;
-    subterm_unification_needs (b,
+  subterm_unification_needs (goalterm, run, index);
-			       roledef_shift (sys->runs[run].start,
-					      index)->message);
   if (newgoals > 0)
     {
       goal_remove_last (newgoals);
     }
   sys->runs[run].height = old_length;
-  return flag;
 }
 
 //! Try to bind a specific existing run to a goal.
@@ -1135,7 +1159,7 @@ bind_existing_run (const Binding b, const Protocol p, const Role r,
 	      eprintf ("%i. Can we bind it to run %i?\n", found, run);
 	    }
 	  indentDepth++;
-	  flag = flag && bind_existing_to_goal (b, run, index);
+	  bind_existing_to_goal (b, run, index);
 	  indentDepth--;
 	}
     }
@@ -1157,7 +1181,6 @@ bind_new_run (const Binding b, const Protocol p, const Role r,
 	      const int index)
 {
   int run;
-  int flag;
   int newgoals;
 
   run = semiRunCreate (p, r);
@@ -1165,12 +1188,12 @@ bind_new_run (const Binding b, const Protocol p, const Role r,
   {
     newgoals = add_read_goals (run, 0, index + 1);
     indentDepth++;
-    flag = bind_existing_to_goal (b, run, index);
+    bind_existing_to_goal (b, run, index);
     indentDepth--;
     goal_remove_last (newgoals);
   }
   semiRunDestroy ();
-  return flag;
+  return true;
 }
 
 //! Print the current semistate
@@ -1596,7 +1619,7 @@ bind_goal_old_intruder_run (Binding b)
 			("Suppose it is from an existing intruder run.\n");
 		    }
 		  indentDepth++;
-		  flag = flag && bind_existing_to_goal (b, run, ev);
+		  bind_existing_to_goal (b, run, ev);
 		  indentDepth--;
 		}
 	      rd = rd->next;

src/mgu.c

@@ -115,41 +115,47 @@ termlistSubstReset (Termlist tl)
  * Try to determine the most general unifier of two terms, if so calls function.
  *
  * The callback receives a list of variables, that were previously open, but are now closed
- * in such a way that the two terms unify. Returns result of iteration, or false if not.
+ * in such a way that the two terms unify. 
+ *
  */
-int
+void
-unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
+unify (Term t1, Term t2, Termlist tl, void (*callback) (Termlist))
 {
   /* added for speed */
   t1 = deVar (t1);
   t2 = deVar (t2);
   if (t1 == t2)
-    return callback (tl);
+    {
+      callback (tl);
+      return;
+    }
 
   int callsubst (Termlist tl, Term t, Term tsubst)
   {
-    int flag;
-
     t->subst = tsubst;
 #ifdef DEBUG
     showSubst (t);
 #endif
     tl = termlistAdd (tl, t);
-    flag = callback (tl);
+    callback (tl);
     tl = termlistDelTerm (tl);
     t->subst = NULL;
-    return flag;
+    return;
   }
 
   if (!(hasTermVariable (t1) || hasTermVariable (t2)))
     {
+      // None has a variable
       if (isTermEqual (t1, t2))
 	{
-	  return callback (tl);
+	  // Equal!
+	  callback (tl);
+	  return;
 	}
       else
 	{
-	  return false;
+	  // Can never be fixed, no variables
+	  return;
 	}
     }
 
@@ -177,7 +183,8 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
 	  t1 = t2;
 	  t2 = t3;
 	}
-      return callsubst (tl, t1, t2);
+      callsubst (tl, t1, t2);
+      return;
     }
 
   /* symmetrical tests for single variable.
@@ -186,55 +193,61 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
   if (realTermVariable (t2))
     {
       if (termSubTerm (t1, t2) || !goodsubst (t2, t1))
-	return false;
+	return;
       else
 	{
-	  return callsubst (tl, t2, t1);
+	  callsubst (tl, t2, t1);
+	  return;
 	}
     }
   if (realTermVariable (t1))
     {
       if (termSubTerm (t2, t1) || !goodsubst (t1, t2))
-	return false;
+	return;
       else
 	{
-	  return callsubst (tl, t1, t2);
+	  callsubst (tl, t1, t2);
+	  return;
 	}
     }
 
   /* left & right are compounds with variables */
   if (t1->type != t2->type)
-    return false;
+    return;
 
   /* identical compound types */
 
   /* encryption first */
   if (realTermEncrypt (t1))
     {
-      int unify_combined_enc (Termlist tl)
+      void unify_combined_enc (Termlist tl)
       {
 	// now the keys are unified (subst in this tl)
 	// and we try the inner terms
-	return unify (TermOp (t1), TermOp (t2), tl, callback);
+	unify (TermOp (t1), TermOp (t2), tl, callback);
+	return;
       }
 
-      return unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc);
+      unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc);
+      return;
     }
 
   /* tupling second
      non-associative version ! TODO other version */
   if (isTermTuple (t1))
     {
-      int unify_combined_tup (Termlist tl)
+      void unify_combined_tup (Termlist tl)
       {
 	// now the keys are unified (subst in this tl)
 	// and we try the inner terms
-	return unify (TermOp2 (t1), TermOp2 (t2), tl, callback);
+	unify (TermOp2 (t1), TermOp2 (t2), tl, callback);
+	return;
+      }
+      unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup);
+      return;
     }
 
-      return unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup);
+  return;
-    }
-  return false;
 }
 
 

src/mgu.h

@@ -20,6 +20,6 @@ int termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist));
 int termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
 		    Termlist inverses, Termlist keylist);
 void termlistSubstReset (Termlist tl);
-int unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist));
+void unify (Term t1, Term t2, Termlist tl, void (*callback) (Termlist));
 
 #endif