From 0fb7e9e24edb3bf9431fbf3179abfde6c9c8fccd Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Thu, 22 Nov 2012 12:30:00 +0100
Subject: [PATCH] Added support for macro definitions.

It is now possible to declare syntactic macros at the global level.

  macro ID = TERM;

After this definition, every occurrence of ID will be replaced by TERM.
For example, this can be used to avoid duplicating message definitions
among roles:

  macro M1 = { nI, I}pk(R) ;

  protocol X(I,R) {
    role I {
      send (I,R, M1);
    }
    role R {
      recv (I,R, M1);
    }
  }
---
 src/ns3.spdl  |  51 +++++++++++++++++++++++++
 src/parser.y  | 104 ++++++++++++++++++++++++++++++++++++++++++++++----
 src/scanner.l |   1 +
 src/tac.h     |   3 +-
 4 files changed, 150 insertions(+), 9 deletions(-)
 create mode 100644 src/ns3.spdl

diff --git a/src/ns3.spdl b/src/ns3.spdl
new file mode 100644
index 0000000..d488561
--- /dev/null
+++ b/src/ns3.spdl
@@ -0,0 +1,51 @@
+/* 
+ * Needham-Schroeder protocol
+ */
+
+// The protocol description
+
+macro m1 = {ni,I}pk(R);
+macro m2 = {ni,nr}pk(I);
+macro m3 = {nr}pk(R);
+
+protocol ns3(I,R)
+{
+	role I
+	{
+		fresh ni: Nonce;
+		var nr: Nonce;
+
+		send_1(I,R, m1 );
+		recv_2(R,I, m2 );
+		claim(I,Running,R,ni,nr);
+		send_3(I,R, m3 );
+
+		claim(I,Secret,ni);
+		claim(I,Secret,nr);
+		claim(I,Alive);
+		claim(I,Weakagree);
+		claim(I,Commit,R,ni,nr);
+		claim(I,Niagree);
+		claim(I,Nisynch);
+	}	
+	
+	role R
+	{
+		var ni: Nonce;
+		fresh nr: Nonce;
+
+		recv_1(I,R, m1 );
+		claim(R,Running,I,ni,nr);
+		send_2(R,I, m2 );
+		recv_3(I,R, m3 );
+
+		claim(R,Secret,ni);
+		claim(R,Secret,nr);
+		claim(R,Alive);
+		claim(R,Weakagree);
+		claim(R,Commit,I,ni,nr);
+		claim(R,Niagree);
+		claim(R,Nisynch);
+	}
+}
+
diff --git a/src/parser.y b/src/parser.y
index fb7027b..ca4e8cc 100644
--- a/src/parser.y
+++ b/src/parser.y
@@ -21,12 +21,41 @@
 #include "pheading.h"
 #include "tac.h"
 #include "error.h"
+#include "list.h"
 
 struct tacnode*	spdltac;
 
 int yyerror(char *s);
 int yylex(void);
 
+List macrolist=NULL;
+
+List findMacroDefinition(Symbol s)
+{
+	List l;
+
+	if (s == NULL)
+	  {
+	     return NULL;
+	  }
+	/* Now check if it is in the list
+	 * already */
+	for (l = list_rewind(macrolist); l != NULL; l = l->next)
+	  {
+	    Tac tmacro;
+	    Symbol sl;
+	    Tac tl;
+		
+	    tmacro = (Tac) l->data;
+	    sl = (tmacro->t1.tac)->t1.sym;	// The symbol
+	    if (strcmp (sl->text, s->text) == 0)
+	      {
+	        return l;
+	      }
+	  }
+	return NULL;
+}
+
 %}
 
 %union{
@@ -59,6 +88,7 @@ int yylex(void);
 %token		TRUSTED
 %token 		MATCH
 %token 		NOT
+%token 		MACRO
 
 %type	<tac>	spdlcomplete
 %type	<tac>	spdlrep
@@ -73,11 +103,13 @@ int yylex(void);
 %type	<tac>	typeinfoN
 %type	<tac>	term
 %type	<tac>	basicterm
+%type	<tac>	basicormacro
 %type	<tac>	termlist
 %type	<tac>	basictermlist
 %type	<tac>	key
 %type	<tac>	roleref
 %type	<tac>	knowsdecl
+%type	<tac>	macrodecl
 
 %type   <value>	singular
 
@@ -130,6 +162,10 @@ spdl		: UNTRUSTED termlist ';'
 		  {
 		  	$$ = $1;
 		  }
+		| macrodecl 
+		  {	
+		  	$$ = $1;
+		  }
 		;
 
 roles		: /* empty */
@@ -242,6 +278,33 @@ knowsdecl	: KNOWS termlist ';'
 		  }
 		;
 
+macrodecl	: MACRO basicterm '=' termlist ';'
+		  {	
+			List l;
+
+			l = findMacroDefinition($2->t1.sym);
+			if (l == NULL)
+			  {
+		  	    Tac t;
+		  	    /* Add to macro declaration list.
+			     * TAC_MACRO doesn't show up in the compiler though.  */
+			    t = tacCreate(TAC_MACRO);
+			    t->t1.tac = $2;
+			    t->t2.tac = tacTuple($4);
+			    macrolist = list_append(macrolist, t);
+			  }
+			else
+			  {
+			    /* Already defined. We can consider this
+			     * a bug or we can define it to
+			     * overwrite.
+			     */
+			    //yyerror("macro symbol already defined earlier.");
+			  }
+			$$ = NULL;
+		  }
+		;
+
 declaration	: secretpref CONST basictermlist typeinfo1 ';'
 		  {	Tac t = tacCreate(TAC_CONST);
 		  	t->t1.tac = $3; // names
@@ -304,10 +367,9 @@ typeinfo1	: /* empty */
 		  	Tac t = tacCreate(TAC_UNDEF);
 			$$ = t;
 		  }
-		| ':' ID
-		  {	Tac t = tacCreate(TAC_STRING);
-		  	t->t1.sym = $2;
-			$$ = t;
+		| ':' basicterm
+		  {	
+			$$ = $2;
 		  }
 		;
 
@@ -335,15 +397,39 @@ optlabel        : /* empty */
 
 basicterm	: ID
 		  {
-		  	Tac t = tacCreate(TAC_STRING);
+			Tac t;
+
+			t = tacCreate(TAC_STRING);
 			t->t1.sym = $1;
 			$$ = t;
 		  }
 		;
 
-term  		: basicterm
-	          { }
-		| ID '(' termlist ')'
+basicormacro	: ID
+		  {
+			List l;
+			Tac t;
+
+			/* check if it is in the list
+			 * already */
+			l = findMacroDefinition($1);
+			if (l == NULL)
+			  {
+			    t = tacCreate(TAC_STRING);
+			    t->t1.sym = $1;
+			  }
+			else
+			  {
+			    Tac macrotac;
+
+			    macrotac = (Tac) l->data;
+			    t = macrotac->t2.tac;
+			  }
+			$$ = t;
+		  }
+		;
+
+term  		: ID '(' termlist ')'
 		  {
 		  	Tac t = tacCreate(TAC_STRING);
 			t->t1.sym = $1;
@@ -357,6 +443,8 @@ term  		: basicterm
 		  { 
 		  	$$ = tacTuple($2);
 		  }
+		| basicormacro
+		  { }
 		;
 
 termlist	: term
diff --git a/src/scanner.l b/src/scanner.l
index 600421f..71ab075 100644
--- a/src/scanner.l
+++ b/src/scanner.l
@@ -162,6 +162,7 @@ recv		{ return RECVT; }
 send		{ return SENDT; }
 match		{ return MATCH; }
 not		{ return NOT; }
+macro		{ return MACRO; }
 var		{ return VAR; }
 const		{ return CONST; }
 fresh		{ return FRESH; }
diff --git a/src/tac.h b/src/tac.h
index 0ff1599..093a2db 100644
--- a/src/tac.h
+++ b/src/tac.h
@@ -51,7 +51,8 @@ enum tactypes
   TAC_UNTRUSTED,
   TAC_COMPROMISED,
   TAC_USERTYPE,
-  TAC_MATCH
+  TAC_MATCH,
+  TAC_MACRO
 };
 
 //! Structure to hold the compilation tree nodes