From a03f06ea412719e031a1e905be0a3b7be6d79eaf Mon Sep 17 00:00:00 2001
From: Cas Cremers <cremersc@brutus3.ethz.ch>
Date: Thu, 27 Jan 2011 14:12:51 +0100
Subject: [PATCH] BUGFIX: Auto-claim naming scheme was context dependent.

The automatic mechanism to assign labels to claims was dependent on the
context. In practice, a claim could get a different label when analyzed in
isolation compared to when analyzed in parallel with some other protocols. This
caused problems for the multi-protocol analysis.
---
 src/compiler.c | 20 ++++++++++++++++---
 src/symbol.c   | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++
 src/symbol.h   |  1 +
 src/term.c     | 16 +++++++++++++++
 src/term.h     |  1 +
 5 files changed, 89 insertions(+), 3 deletions(-)

diff --git a/src/compiler.c b/src/compiler.c
index 8f803ef..98d4296 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -466,7 +466,7 @@ isClaimlabelUsed (const System sys, const Term label)
 //! Generate a fresh claim label
 Term
 generateFreshClaimlabel (const System sys, const Protocol protocol,
-			 const Role role, const Term claim)
+			 const Role role, const Term claim, const int n)
 {
   Term label;
 
@@ -489,13 +489,16 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
 	     const Term claim, Term label, const Term msg, const int lineno)
 {
   Claimlist cl;
+  int len;
+
+  len = roledef_length (role->roledef);
 
   /* generate full unique label */
   /* is the label empty or used? */
   if (label == NULL || isClaimlabelUsed (sys, label))
     {
       /* simply generate a fresh one */
-      label = generateFreshClaimlabel (sys, protocol, role, claim);
+      label = generateFreshClaimlabel (sys, protocol, role, claim, len);
     }
 
   // Assert: label is unique, add claimlist info
@@ -606,7 +609,18 @@ commEvent (int event, Tac tc)
        * This can be a weird choice if it is a read or send, because in that case
        * we cannot chain them anymore and the send-read correspondence is lost.
        */
-      label = freshTermPrefix (thisRole->nameterm);
+      int n;
+      Roledef rd;
+
+      n = 1;
+      for (rd = thisRole->roledef; rd != NULL; rd = rd->next)
+	{
+	  if (rd->type == CLAIM)
+	    {
+	      n++;
+	    }
+	}
+      label = intTermPrefix (n, thisRole->nameterm);
     }
   else
     {
diff --git a/src/symbol.c b/src/symbol.c
index 53f4429..48ca4ac 100644
--- a/src/symbol.c
+++ b/src/symbol.c
@@ -291,6 +291,60 @@ symbolNextFree (Symbol prefixsymbol)
   return NULL;
 }
 
+//! Return symbol according to integer
+Symbol
+symbolFromInt (int n, Symbol prefixsymbol)
+{
+  char *prefixstr;
+  int len;
+
+  if (!(n <= 9999))
+    {
+      error ("Can only make symbol from int when smaller than 10000");
+    }
+
+  if (prefixsymbol != NULL)
+    {
+      prefixstr = (char *) prefixsymbol->text;
+      len = strlen (prefixstr);
+    }
+  else
+    {
+      prefixstr = "";
+      len = 0;
+    }
+
+  /*
+   * The construction below (variable buffer length) is not allowed in ISO C90
+   */
+  char buffer[len + 5];		// thus we must enforce a maximum of 9.999 (allowing for storage of \0 )
+  Symbol symb;
+  int slen;
+
+  slen = sprintf (buffer, "%s%i", prefixstr, n);
+  buffer[slen] = EOS;
+  symb = lookup (buffer);
+  if (symb == NULL)
+    {
+      char *newstring;
+      // Copy the buffer to something that will survive
+	  /**
+	   * Memory leak: although this routine should not be called recursively, it will never de-allocate this memory.
+	   * Thus, some precaution is necessary.
+	   * [x][CC]
+	   */
+      newstring = (char *) malloc (slen + 1);
+      memcpy (newstring, buffer, slen + 1);
+
+      /* This persistent string can be used to return a fresh symbol */
+
+      symb = symbolSysConst (newstring);
+    }
+
+  return symb;
+
+}
+
 //! Fix all the unset keylevels
 void
 symbol_fix_keylevels (void)
diff --git a/src/symbol.h b/src/symbol.h
index c71b943..09cbb8c 100644
--- a/src/symbol.h
+++ b/src/symbol.h
@@ -67,6 +67,7 @@ void symbolPrintAll (void);
 Symbol symbolSysConst (const char *str);
 void symbol_fix_keylevels (void);
 Symbol symbolNextFree (Symbol prefixsymbol);
+Symbol symbolFromInt (int n, Symbol prefixsymbol);
 
 void eprintf (char *fmt, ...);
 void veprintf (const char *fmt, va_list args);
diff --git a/src/term.c b/src/term.c
index 4590e4f..da02e9d 100644
--- a/src/term.c
+++ b/src/term.c
@@ -1386,6 +1386,22 @@ freshTermPrefix (Term prefixterm)
   return makeTermType (GLOBAL, freshsymbol, -1);
 }
 
+//! Generate a term from an int, prefixed with the string of the given term.
+Term
+intTermPrefix (const int n, Term prefixterm)
+{
+  Symbol prefixsymbol;
+  Symbol freshsymbol;
+
+  prefixsymbol = NULL;
+  if (prefixterm != NULL && realTermLeaf (prefixterm))
+    {
+      prefixsymbol = TermSymb (prefixterm);
+    }
+  freshsymbol = symbolFromInt (n, prefixsymbol);
+  return makeTermType (GLOBAL, freshsymbol, -1);
+}
+
 //! Determine whether a term is a functor
 int
 isTermFunctionName (Term t)
diff --git a/src/term.h b/src/term.h
index 0891842..377ad47 100644
--- a/src/term.h
+++ b/src/term.h
@@ -201,6 +201,7 @@ void term_set_keylevels (const Term term);
 void termPrintDiff (Term t1, Term t2);
 int isLeafNameEqual (Term t1, Term t2);
 Term freshTermPrefix (Term prefixterm);
+Term intTermPrefix (const int n, Term prefixterm);
 int isTermFunctionName (Term t);
 Term getTermFunction (Term t);
 unsigned int termHidelevel (const Term tsmall, Term tbig);