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 basictermlist %type key %type roleref +%type knowsdecl %type 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,