From 0505aaacd6fde192546c919c60e293e600c0d90e Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 28 Dec 2005 11:50:17 +0000 Subject: [PATCH] - New claim: CLAIM_Reachable - Added new switches: -G,--generate-statespace -C,--generate-claims - Claims are now allowed to have no label (they will be generated automatically) - Output summary shows parameter of claims - Internally, new symbols can now be generated by symbolNextFree(prefixsymbol) --- src/compiler.c | 278 ++++++++++++++++++++++++++++++---------------- src/main.c | 103 +++++++++++++---- src/parser.y | 11 +- src/role.c | 1 + src/role.h | 4 + src/specialterm.c | 2 + src/specialterm.h | 1 + src/switches.c | 33 ++++++ src/switches.h | 2 + src/symbol.c | 54 +++++++++ src/symbol.h | 1 + src/term.c | 16 +++ src/term.h | 1 + 13 files changed, 389 insertions(+), 118 deletions(-) diff --git a/src/compiler.c b/src/compiler.c index edba420..ed13dcb 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -355,15 +355,130 @@ levelTacDeclaration (Tac tc, int isVar) /* declare this variable/constant with the previously derived type list */ t = symbolDeclare (tscan->t1.sym, isVar); t->stype = typetl; - if (isVar && level == 2) + /* local to the role? */ + if (level == 2) { - /* it is a role variable, so add it to the nicely declared variables */ - thisRole->declaredvars = termlistAdd (thisRole->declaredvars, t); + if (isVar) + { + /* it is a role variable, so add it to the nicely declared variables */ + thisRole->declaredvars = + termlistAdd (thisRole->declaredvars, t); + } + else + { + /* it is a role constant, so add it to the nicely declared constants */ + thisRole->declaredconsts = + termlistAdd (thisRole->declaredconsts, t); + } } tscan = tscan->next; } } +//! Check whether a claim label already occurs +int +isClaimlabelUsed (const System sys, const Term label) +{ + Claimlist cl; + + if (label == NULL) + { + /* we assign this 'occurs' because it is an invalid label */ + return true; + } + cl = sys->claimlist; + while (cl != NULL) + { + if (isTermEqual (cl->label, label)) + { + return true; + } + cl = cl->next; + } + return false; +} + +//! Generate a fresh claim label +Term +generateFreshClaimlabel (const System sys, const Role role, const Term claim) +{ + /* Simply use the role as a prefix */ + return freshTermPrefix (role->nameterm); +} + +//! Create a claim and add it to the claims list, and add the role event. +Claimlist +claimCreate (const System sys, const Protocol protocol, const Role role, + const Term claim, Term label, const Term msg) +{ + Claimlist cl; + Term labeltuple; + + /* check for ignored claim types */ + if (switches.filterClaim != NULL && switches.filterClaim != claim) + { + /* abort the construction of the node */ + return; + } + + /* generate full unique label */ + /* is the label empty or used? */ + if (label == NULL || isClaimlabelUsed (sys, label)) + { + /* simply generate a fresh one */ + label = generateFreshClaimlabel (sys, role, claim); + } + + // Assert: label is unique, add claimlist info + cl = memAlloc (sizeof (struct claimlist)); + cl->type = claim; + cl->label = label; + cl->parameter = msg; + cl->protocol = thisProtocol; + cl->rolename = role->nameterm; + cl->role = role; + cl->roledef = NULL; + cl->count = 0; + cl->complete = 0; + cl->timebound = 0; + cl->failed = 0; + cl->prec = NULL; + cl->roles = NULL; + cl->alwaystrue = false; + cl->warnings = false; + cl->next = sys->claimlist; + sys->claimlist = cl; + + /* add the role event */ + role->roledef = roledefAdd (role->roledef, CLAIM, label, + role->nameterm, claim, msg, cl); + + /* possible special handlers for each claim */ + + if (claim == CLAIM_Secret) + { + Termlist claimvars; + Termlist readvars; + + /* now check whether the claim contains variables that can actually be influenced by the intruder */ + + claimvars = termlistAddVariables (NULL, msg); + readvars = compute_read_variables (thisRole); + while (claimvars != NULL) + { + if (!inTermlist (readvars, claimvars->term)) + { + /* this claimvar does not occur in the reads? */ + /* then we should ignore it later */ + cl->alwaystrue = true; + cl->warnings = true; + } + claimvars = claimvars->next; + } + } +} + +//! Parse a communication event tc of type event, and add a role definition event for it. void commEvent (int event, Tac tc) { @@ -382,7 +497,12 @@ commEvent (int event, Tac tc) /* Construct label, if any */ if (tc->t1.sym == NULL) { - label = NULL; + /* right, now this should not be NULL anyway, if so we construct a fresh one. + * 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. + */ + warning ("Generated fresh label for line %i.", tc->lineno); + label = freshTermPrefix (thisRole->nameterm); } else { @@ -398,21 +518,10 @@ commEvent (int event, Tac tc) } else { - /* we already had this label constant */ /* leaves a garbage tuple. dunnoh what to do with it */ label = makeTermTuple (thisProtocol->nameterm, label); } } - /** - * We now know the label. Find the corresponding labelinfo bit or make a new one - */ - linfo = label_find (sys->labellist, label); - if (linfo == NULL) - { - /* Not found, make a new one */ - linfo = label_create (label, thisProtocol); - sys->labellist = list_append (sys->labellist, linfo); - } /** * Parse the specific event type @@ -422,6 +531,17 @@ commEvent (int event, Tac tc) { case READ: case SEND: + /** + * We know the label. Find the corresponding labelinfo bit or make a new one + */ + linfo = label_find (sys->labellist, label); + if (linfo == NULL) + { + /* Not found, make a new one */ + linfo = label_create (label, thisProtocol); + sys->labellist = list_append (sys->labellist, linfo); + } + /* now parse triplet info */ if (trip == NULL || trip->next == NULL || trip->next->next == NULL) { @@ -461,8 +581,13 @@ commEvent (int event, Tac tc) linfo->readrole = torole; } + /* and make that read/send event */ + thisRole->roledef = roledefAdd (thisRole->roledef, event, label, + fromrole, torole, msg, cl); break; + case CLAIM: + /* switch can be used to remove all *parsed* claims */ if (!switches.removeclaims) { /* now parse tuple info */ @@ -477,13 +602,6 @@ commEvent (int event, Tac tc) claim = tupleProject (claimbig, 0); torole = claim; - /* check for ignored claim types */ - if (switches.filterClaim != NULL && switches.filterClaim != claim) - { - /* abort the construction of the node */ - return; - } - /* check for obvious flaws */ if (claim == NULL) { @@ -491,7 +609,7 @@ commEvent (int event, Tac tc) } if (!inTermlist (claim->stype, TERM_Claim)) { - printf ("error: unknown claim type "); + printf ("error: claim term is not of claim type "); termPrint (claim); errorTac (trip->next->lineno); } @@ -514,50 +632,21 @@ commEvent (int event, Tac tc) } } - /* store claim in claim list */ + // check whether label is unique - if (label == NULL) + if (isClaimlabelUsed (sys, label)) { - error ("Claim should have label on line %i.", - trip->next->lineno); + warning + ("Claim label is not unique at line %i, generating fresh label.", + tc->lineno); } - // First check whether label is unique - cl = sys->claimlist; - while (cl != NULL) - { - if (isTermEqual (cl->label, label)) - { - /** - *@todo This should not error exit, but automatically generate a fresh claim label. - */ - error ("Claim label is not unique at line %i.", tc->lineno); - } - cl = cl->next; - } - // Assert: label is unique, add claimlist info - cl = memAlloc (sizeof (struct claimlist)); - cl->type = claim; - cl->label = label; - cl->protocol = thisProtocol; - cl->rolename = fromrole; - cl->role = thisRole; + if (!isTermEqual (fromrole, thisRole->nameterm)) error ("Claim role does not correspond to execution role at line %i.", tc->lineno); - cl->roledef = NULL; - cl->count = 0; - cl->complete = 0; - cl->timebound = 0; - cl->failed = 0; - cl->prec = NULL; - cl->roles = NULL; - cl->alwaystrue = false; - cl->warnings = false; - cl->next = sys->claimlist; - sys->claimlist = cl; - /* handles all claim types differently */ + /* handles claim types with different syntactic claims */ if (claim == CLAIM_Secret) { @@ -573,26 +662,6 @@ commEvent (int event, Tac tc) ("Secrecy claim on line %i should not contain tuples (for Arachne) until it is officially supported.", trip->next->lineno); } - /* now check whether the claim contains variables that can actually be influenced by the intruder */ - { - Termlist claimvars; - Termlist readvars; - - claimvars = termlistAddVariables (NULL, msg); - readvars = compute_read_variables (thisRole); - while (claimvars != NULL) - { - if (!inTermlist (readvars, claimvars->term)) - { - /* this claimvar does not occur in the reads? */ - /* then we should ignore it later */ - cl->alwaystrue = true; - cl->warnings = true; - } - claimvars = claimvars->next; - } - } - break; } if (claim == CLAIM_Nisynch) { @@ -601,7 +670,6 @@ commEvent (int event, Tac tc) error ("NISYNCH claim requires no parameters at line %i.", trip->next->lineno); } - break; } if (claim == CLAIM_Niagree) { @@ -610,25 +678,14 @@ commEvent (int event, Tac tc) error ("NIAGREE claim requires no parameters at line %i.", trip->next->lineno); } - break; - } - if (claim == CLAIM_Empty) - { - break; } - /* hmm, no handler yet */ + /* create the event */ - printf ("error: No know handler for this claim type: "); - termPrint (claim); - printf (" "); - errorTac (trip->next->lineno); + cl = claimCreate (sys, thisProtocol, thisRole, claim, label, msg); } break; } - /* and make that event */ - thisRole->roledef = roledefAdd (thisRole->roledef, event, label, - fromrole, torole, msg, cl); } int @@ -663,6 +720,28 @@ normalDeclaration (Tac tc) return 1; } +//! Add all sorts of claims to this role +void +claimAddAll (const System sys, const Protocol protocol, const Role role) +{ + /* first: secrecy claims for all locally declared things */ + void addSecrecyList (Termlist tl) + { + while (tl != NULL) + { + claimCreate (sys, protocol, role, CLAIM_Secret, NULL, tl->term); + tl = tl->next; + } + } + + addSecrecyList (role->declaredconsts); + addSecrecyList (role->declaredvars); + + /* full non-injective agreement and ni-synch */ + claimCreate (sys, protocol, role, CLAIM_Niagree, NULL, NULL); + claimCreate (sys, protocol, role, CLAIM_Nisynch, NULL, NULL); +} + void roleCompile (Term nameterm, Tac tc) { @@ -726,6 +805,19 @@ roleCompile (Term nameterm, Tac tc) tc = tc->next; } } + + /* add any claims according to the switches */ + + if (switches.addreachableclaim) + { + claimCreate (sys, thisProtocol, thisRole, CLAIM_Reachable, NULL, NULL); + } + if (switches.addallclaims) + { + claimAddAll (sys, thisProtocol, thisRole); + } + + /* last bits */ compute_role_variables (sys, thisProtocol, thisRole); levelDone (); } diff --git a/src/main.c b/src/main.c index 878e606..9a730dd 100644 --- a/src/main.c +++ b/src/main.c @@ -370,47 +370,104 @@ timersPrint (const System sys) /* Note that if the output is set to empty, the claim output is redirected to stdout (for e.g. processing) */ cl_scan = sys->claimlist; - anyclaims = 0; + anyclaims = false; while (cl_scan != NULL) { if (!isTermEqual (cl_scan->type, CLAIM_Empty)) { - anyclaims = 1; + Protocol protocol; + Term pname; + Term rname; + Termlist labellist; + + anyclaims = true; eprintf ("claim\t"); - /* claim label is tuple */ - if (realTermTuple (cl_scan->label)) + protocol = (Protocol) cl_scan->protocol; + pname = protocol->nameterm; + rname = cl_scan->rolename; + + labellist = tuple_to_termlist (cl_scan->label); + + /* maybe the label contains duplicate info: if so, we remove it here */ + { + Termlist tl; + tl = labellist; + while (tl != NULL) + { + if (isTermEqual (tl->term, pname) + || isTermEqual (tl->term, rname)) + { + tl = termlistDelTerm (tl); + labellist = tl; + } + else + { + tl = tl->next; + } + } + } + + termPrint (pname); + eprintf (","); + termPrint (rname); + eprintf ("\t"); + /* second print event_label */ + termPrint (cl_scan->type); + + eprintf ("_"); + if (labellist != NULL) { - /* modern version: claim label is tuple (protocname, label) */ - /* first print protocol.role */ - termPrint (TermOp1 (cl_scan->label)); - eprintf (","); - termPrint (cl_scan->rolename); - eprintf ("\t"); - /* second print event_label */ - termPrint (cl_scan->type); - eprintf ("_"); - termPrint (TermOp2 (cl_scan->label)); - eprintf ("\t"); + Termlist tl; + + tl = labellist; + while (tl != NULL) + { + termPrint (tl->term); + tl = tl->next; + if (tl != NULL) + { + eprintf (","); + } + } + /* clean up */ + termlistDelete (labellist); + labellist = NULL; } else { - /* old-fashioned output */ - termPrint (cl_scan->type); - eprintf ("\t"); - termPrint (cl_scan->rolename); - eprintf (" ("); - termPrint (cl_scan->label); - eprintf (")\t"); + eprintf ("?"); + } + /* add parameter */ + eprintf ("\t"); + if (cl_scan->parameter != NULL) + { + termPrint (cl_scan->parameter); + } + else + { + eprintf ("-"); } /* now report the status */ + eprintf ("\t"); eprintf ("attacks: "); if (cl_scan->count > 0 && cl_scan->failed > 0) { /* there is an attack */ - eprintf ("yes\t(at least %i)", cl_scan->failed); + eprintf ("yes\t"); + /* are these all attacks? */ + eprintf ("("); + if (cl_scan->complete) + { + eprintf ("exactly"); + } + else + { + eprintf ("at least"); + } + eprintf (" %i)", cl_scan->failed); } else { diff --git a/src/parser.y b/src/parser.y index 3a7ccff..88f72da 100644 --- a/src/parser.y +++ b/src/parser.y @@ -48,6 +48,7 @@ int yylex(void); %type roleref %type label +%type optlabel %start spdlcomplete @@ -142,7 +143,7 @@ event : READT label '(' termlist ')' ';' t->t2.tac = $4; $$ = t; } - | CLAIMT label '(' termlist ')' ';' + | CLAIMT optlabel '(' termlist ')' ';' /* TODO maybe claims should be in the syntax */ { Tac t = tacCreate(TAC_CLAIM); t->t1.sym = $2; @@ -226,11 +227,17 @@ typeinfoN : /* empty */ } ; -/* Previously, the label could be omitted. It is now required. */ label : '_' ID { $$ = $2; } ; +optlabel : /* empty */ + { $$ = NULL; } + | label + { } + ; + + term : ID { Tac t = tacCreate(TAC_STRING); diff --git a/src/role.c b/src/role.c index 2a6a9c5..3a16b87 100644 --- a/src/role.c +++ b/src/role.c @@ -241,6 +241,7 @@ roleCreate (Term name) r->locals = NULL; r->variables = NULL; r->declaredvars = NULL; + r->declaredconsts = NULL; r->initiator = 1; //! Will be determined later, if a read is the first action (in compiler.c) r->next = NULL; return r; diff --git a/src/role.h b/src/role.h index 5cafa6c..af09507 100644 --- a/src/role.h +++ b/src/role.h @@ -18,6 +18,8 @@ struct claimlist Term type; //! The term element for this node. Term label; + //! Any parameters + Term parameter; //! The pointer to the protocol (not defined typically, because //! at compile time of the claim the protocol structure is not known yet.) void *protocol; @@ -124,6 +126,8 @@ struct role Termlist locals; //! Local variables for this role. Termlist variables; + //! Declared constants for this role + Termlist declaredconsts; //! Declared variables for this role Termlist declaredvars; //! Flag for initiator roles diff --git a/src/specialterm.c b/src/specialterm.c index 34c0f44..aa16b14 100644 --- a/src/specialterm.c +++ b/src/specialterm.c @@ -26,6 +26,7 @@ Term CLAIM_Secret; Term CLAIM_Nisynch; Term CLAIM_Niagree; Term CLAIM_Empty; +Term CLAIM_Reachable; //! Init special terms /** @@ -50,4 +51,5 @@ specialTermInit (const System sys) langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim); langcons (CLAIM_Niagree, "Niagree", TERM_Claim); langcons (CLAIM_Empty, "Empty", TERM_Claim); + langcons (CLAIM_Reachable, "Reachable", TERM_Claim); } diff --git a/src/specialterm.h b/src/specialterm.h index 62e801b..de0f9b3 100644 --- a/src/specialterm.h +++ b/src/specialterm.h @@ -18,5 +18,6 @@ extern Term CLAIM_Secret; extern Term CLAIM_Nisynch; extern Term CLAIM_Niagree; extern Term CLAIM_Empty; +extern Term CLAIM_Reachable; #endif diff --git a/src/switches.c b/src/switches.c index d4a9d22..a73bc5e 100644 --- a/src/switches.c +++ b/src/switches.c @@ -75,6 +75,8 @@ switchesInit (int argc, char **argv) switches.switchP = 0; // multi-purpose parameter switches.experimental = 0; // experimental stuff defaults to 0, whatever that means. switches.removeclaims = false; // default: leave claims from spdl file + switches.addreachableclaim = false; // add 'reachable' claims + switches.addallclaims = false; // add all sorts of claims // Output switches.output = SUMMARY; // default is to show a summary @@ -395,6 +397,37 @@ switcher (const int process, int index) } } + if (detect ('C', "generate-claims", 0)) + { + if (!process) + { + helptext ("-C,--generate-claims", + "ignore any existing claims and automatically generate new claims"); + } + else + { + switches.removeclaims = true; + switches.addallclaims = true; + return index; + } + } + + if (detect ('G', "generate-semibundles", 0)) + { + if (!process) + { + helptext ("-G,--generate-statespace", + "ignore any existing claims and add 'reachable' claims to generate the full state space"); + } + else + { + switches.removeclaims = true; // remove parsed claims + switches.addreachableclaim = true; // add reachability claims + switches.prune = 0; // do not prune anything + return index; + } + } + /* ================== * Bounding options */ diff --git a/src/switches.h b/src/switches.h index e95415b..606660b 100644 --- a/src/switches.h +++ b/src/switches.h @@ -54,6 +54,8 @@ struct switchdata int switchP; //!< A multi-purpose integer parameter, passed to the partial order reduction method selected. int experimental; //!< Experimental stuff goes here until it moves into main stuff. int removeclaims; //!< Remove any claims in the spdl file + int addreachableclaim; //!< Adds 'reachable' claims to each role + int addallclaims; //!< Adds all sorts of claims to the roles // Output int output; //!< From enum outputs: what should be produced. Default ATTACK. diff --git a/src/symbol.c b/src/symbol.c index 745f0be..17f30df 100644 --- a/src/symbol.c +++ b/src/symbol.c @@ -211,6 +211,60 @@ symbolSysConst (const char *str) return symb; } +//! Generate the first fresh free number symbol, prefixed by a certain symbol's string. +/** + * Note that there is an upper limit to this, to avoid some problems with buffer overflows etc. + */ +Symbol +symbolNextFree (Symbol prefixsymbol) +{ + char *prefixstr; + int n; + int len; + + if (prefixsymbol != NULL) + { + prefixstr = (char *) prefixsymbol->text; + } + else + { + prefixstr = ""; + } + + len = strlen (prefixstr); + n = 1; + while (n <= 9999) + { + 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); + 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 *) memAlloc (slen + 1); + memcpy (newstring, buffer, slen + 1); + + /* This persistent string can be used to return a fresh symbol */ + + return symbolSysConst (newstring); + } + + // Try next one + n++; + } + error ("We ran out of numbers (%i) when trying to generate a fresh symbol.", + n); +} + //! Fix all the unset keylevels void symbol_fix_keylevels (void) diff --git a/src/symbol.h b/src/symbol.h index 5baf533..949765a 100644 --- a/src/symbol.h +++ b/src/symbol.h @@ -44,6 +44,7 @@ void symbolPrint (const Symbol s); void symbolPrintAll (void); Symbol symbolSysConst (const char *str); void symbol_fix_keylevels (void); +Symbol symbolNextFree (Symbol prefixsymbol); void eprintf (char *fmt, ...); diff --git a/src/term.c b/src/term.c index 69ad56a..c170358 100644 --- a/src/term.c +++ b/src/term.c @@ -1336,3 +1336,19 @@ isLeafNameEqual (Term t1, Term t2) { return (TermSymb (t1) == TermSymb (t2)); } + +//! Generate a fresh term, that does not occur yet, prefixed with the string of the given term. +Term +freshTermPrefix (Term prefixterm) +{ + Symbol prefixsymbol; + Symbol freshsymbol; + + prefixsymbol = NULL; + if (prefixterm != NULL && realTermLeaf (prefixterm)) + { + prefixsymbol = TermSymb (prefixterm); + } + freshsymbol = symbolNextFree (prefixsymbol); + return makeTermType (GLOBAL, freshsymbol, -1); +} diff --git a/src/term.h b/src/term.h index c11ce7b..f12fcb2 100644 --- a/src/term.h +++ b/src/term.h @@ -196,5 +196,6 @@ float term_constrain_level (const Term term); void term_set_keylevels (const Term term); void termPrintDiff (Term t1, Term t2); int isLeafNameEqual (Term t1, Term t2); +Term freshTermPrefix (Term prefixterm); #endif