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); } }
This commit is contained in:
parent
25da320128
commit
0fb7e9e24e
51
src/ns3.spdl
Normal file
51
src/ns3.spdl
Normal file
@ -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);
|
||||
}
|
||||
}
|
||||
|
104
src/parser.y
104
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
|
||||
|
@ -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; }
|
||||
|
Loading…
Reference in New Issue
Block a user