From f00392ac3e3fb5cb9fb4bf21adb8f7ed15e8b55f Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Thu, 27 Jul 2006 10:44:12 +0000
Subject: [PATCH] - Added functional 'knows' keyword.

---
 src/compiler.c | 24 ++++++++++++++++++++++++
 src/parser.y   | 10 ++++++++++
 src/role.c     |  1 +
 src/role.h     |  2 ++
 src/system.c   | 25 +++++++++++++++++++++++++
 src/system.h   |  1 +
 src/tac.h      |  1 +
 7 files changed, 64 insertions(+)

diff --git a/src/compiler.c b/src/compiler.c
index a3ba904..50e4545 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -44,6 +44,7 @@ Term tacTerm (Tac tc);
 Termlist tacTermlist (Tac tc);
 Term levelDeclare (Symbol s, int isVar, int level);
 void compute_role_variables (const System sys, Protocol p, Role r);
+void roleKnows (Tac tc);
 
 /*
  * Global stuff
@@ -828,6 +829,9 @@ roleCompile (Term nameterm, Tac tc)
 	  case TAC_CLAIM:
 	    commEvent (CLAIM, tc);
 	    break;
+	  case TAC_KNOWS:
+	    roleKnows (tc);
+	    break;
 	  default:
 	    if (!normalDeclaration (tc))
 	      {
@@ -859,6 +863,13 @@ roleCompile (Term nameterm, Tac tc)
   levelDone ();
 }
 
+//! Initial role knowledge declaration
+void
+roleKnows (Tac tc)
+{
+  thisRole->knows = termlistConcat (thisRole->knows, tacTermlist (tc->t1.tac));
+}
+
 void
 runInstanceCreate (Tac tc)
 {
@@ -1801,4 +1812,17 @@ preprocess (const System sys)
    * compute hidelevels
    */
   hidelevelCompute (sys);
+  /*
+   * display initial role knowledge
+   */
+
+  int showRK (Protocol p, Role r)
+  {
+    eprintf ("Role ");
+    termPrint (r->nameterm);
+    eprintf (" knows ");
+    termlistPrint (r->knows);
+    eprintf ("\n");
+  }
+  iterateRoles (sys,showRK);
 }
diff --git a/src/parser.y b/src/parser.y
index 2d1c28b..964cbf1 100644
--- a/src/parser.y
+++ b/src/parser.y
@@ -54,6 +54,7 @@ int yylex(void);
 %type	<tac>	basictermlist
 %type	<tac>	key
 %type	<tac>	roleref
+%type	<tac>	knowsdecl
 
 %type   <value>	singular
 
@@ -145,6 +146,8 @@ roledef		: /* empty */
 		  {	$$ = tacCat($1,$2); }
 		| declaration roledef
 		  {	$$ = tacCat($1,$2); }
+		| knowsdecl roledef
+		  {	$$ = tacCat($1,$2); }
 		;
 
 event		: READT label '(' termlist ')' ';'
@@ -178,6 +181,13 @@ roleref		: ID '.' ID
 		  }
 		;
 
+knowsdecl	: KNOWS termlist ';'
+		  {	Tac t = tacCreate(TAC_KNOWS);
+		  	t->t1.tac = $2;
+			$$ = t;
+		  }
+		;
+
 declaration	: secretpref CONST basictermlist typeinfo1 ';'
 		  {	Tac t = tacCreate(TAC_CONST);
 		  	t->t1.tac = $3;
diff --git a/src/role.c b/src/role.c
index 207034b..ec5c9de 100644
--- a/src/role.c
+++ b/src/role.c
@@ -229,6 +229,7 @@ roleCreate (Term name)
   r->initiator = 1;		//! Will be determined later, if a read is the first action (in compiler.c)
   r->singular = false;		// by default, a role is not singular
   r->next = NULL;
+  r->knows = NULL;
   return r;
 }
 
diff --git a/src/role.h b/src/role.h
index 2e7acf1..3498b89 100644
--- a/src/role.h
+++ b/src/role.h
@@ -134,6 +134,8 @@ struct role
   Termlist declaredconsts;
   //! Declared variables for this role
   Termlist declaredvars;
+  //! Initial role knowledge
+  Termlist knows;
   //! Flag for initiator roles
   int initiator;
   //! Flag for singular roles
diff --git a/src/system.c b/src/system.c
index 8c13b2a..32a1c44 100644
--- a/src/system.c
+++ b/src/system.c
@@ -1381,6 +1381,31 @@ iterateLocalToOther (const System sys, const int myrun,
   return flag;
 }
 
+//! Iterate over all roles
+int
+iterateRoles (const System sys, int (*callback) (Protocol p, Role r))
+{
+  Protocol p;
+
+  p = sys->protocols;
+  while (p != NULL)
+    {
+      Role r;
+
+      r = p->roles;
+      while (r != NULL)
+	{
+	  if (!callback (p, r))
+	    {
+	      return false;
+	    }
+	  r = r->next;
+	}
+      p = p->next;
+    }
+  return true;
+}
+
 //! Get first read/send occurrence (event index) of term t in run r
 int
 firstOccurrence (const System sys, const int r, Term t, int evtype)
diff --git a/src/system.h b/src/system.h
index 5ab319a..53d9652 100644
--- a/src/system.h
+++ b/src/system.h
@@ -203,6 +203,7 @@ int iterateEventsType (const System sys, const int run, const int evtype,
 		       int (*callback) (Roledef rd, int ev));
 int iterateLocalToOther (const System sys, const int myrun,
 			 int (*callback) (Term t));
+int iterateRoles (const System sys, int (*callback) (Protocol p, Role r));
 int firstOccurrence (const System sys, const int r, Term t, int evtype);
 Roledef eventRoledef (const System sys, const int run, const int ev);
 int countInitiators (const System sys);
diff --git a/src/tac.h b/src/tac.h
index 606d4fa..8eceda1 100644
--- a/src/tac.h
+++ b/src/tac.h
@@ -22,6 +22,7 @@ enum tactypes
   TAC_STRING,
   TAC_ROLE,
   TAC_PROTOCOL,
+  TAC_KNOWS,
   TAC_RUN,
   TAC_ROLEREF,
   TAC_SECRET,