From 6fabb3b1b4e8808853f43155b16dc008297049da Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Tue, 1 May 2012 16:37:18 +0200 Subject: [PATCH] Improved checking of required parameters for various claims with informative error reporting. --- src/compiler.c | 148 ++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 135 insertions(+), 13 deletions(-) diff --git a/src/compiler.c b/src/compiler.c index 4180f45..c33b81c 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -483,6 +483,105 @@ isStringEqual (const char *s1, const char *s2) return (strcmp (s1, s2) == 0); } +//! Check sanity of the parameters occurring in a claim +/** + * Check if all variables have been received before. + * If not, aborts with error. + */ +void +checkParameterGround (Claimlist cl) +{ + Termlist claimvars; + Termlist recvvars; + Termlist cli; + + /* Compute received variables and those occurring in the claim parameter */ + claimvars = termlistAddVariables (NULL, cl->parameter); + recvvars = compute_recv_variables (thisRole); + + cli = claimvars; + while (cli != NULL) + { + if (!inTermlist (thisProtocol->rolenames, cli->term)) + { + /* only if it is not a role */ + if (!inTermlist (recvvars, cli->term)) + { + /* this claimvar does not occur in the recvs? */ + /* abort with error */ + error_pre (); + globalError++; + eprintf ("Claim of role "); + termPrint (cl->rolename); + eprintf (" contains a variable "); + termPrint (cli->term); + eprintf + (" which is not initialized before (i.e., not received), on line %i.", + cl->lineno); + globalError--; + error_post (""); + } + } + cli = cli->next; + } + termlistDelete (claimvars); + termlistDelete (recvvars); + return; +} + +//! Check if claim is of certain type, then check if meets parameter range, if not abort with error +void +checkParameterRange (const Claimlist cl, const Term claimtype, int minargs, + int maxargs) +{ + Termlist params; + int num; + + if (cl->type != claimtype) + { + return; + } + + params = tuple_to_termlist (cl->parameter); + num = termlistLength (params); + + if (minargs == -1) + { + minargs = num - 1; + } + if (maxargs == -1) + { + maxargs = num + 1; + } + + if ((num < minargs) || (num > maxargs)) + { + error_pre (); + globalError++; + termPrint (cl->type); + eprintf (" claim of role "); + termPrint (cl->rolename); + eprintf (" on line %i", cl->lineno); + if (maxargs == 0) + { + error_post (" does not require any arguments."); + } + else + { + if (num < minargs) + { + eprintf (" requires at least"); + } + else + { + eprintf (" requires at most"); + } + error_post (" %i arguments.", maxargs); + } + } + termlistDelete (params); +} + //! 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, @@ -546,21 +645,23 @@ claimCreate (const System sys, const Protocol protocol, const Role role, /* possible special handlers for each claim */ - if (claim == CLAIM_Secret) + if ((claim == CLAIM_Secret) || (claim == CLAIM_SKR)) { Termlist claimvars; Termlist recvvars; + Termlist cli; /* now check whether the claim contains variables that can actually be influenced by the intruder */ - claimvars = termlistAddVariables (NULL, msg); + claimvars = termlistAddVariables (NULL, cl->parameter); recvvars = compute_recv_variables (thisRole); - while (claimvars != NULL) + cli = claimvars; + while (cli != NULL) { - if (!inTermlist (protocol->rolenames, claimvars->term)) + if (!inTermlist (thisProtocol->rolenames, cli->term)) { /* only if it is not a role */ - if (!inTermlist (recvvars, claimvars->term)) + if (!inTermlist (recvvars, cli->term)) { /* this claimvar does not occur in the recvs? */ /* then we should ignore it later */ @@ -569,20 +670,26 @@ claimCreate (const System sys, const Protocol protocol, const Role role, /* show a warning for this */ globalError++; - eprintf ("warning: secrecy claim of role "); + warning_pre (); + eprintf ("Secrecy claim of role "); termPrint (cl->rolename); eprintf (" contains a variable "); - termPrint (claimvars->term); + termPrint (cli->term); eprintf - (" which is never recv; therefore the claim will be true.\n"); + (" which is never received; therefore the claim will be true.\n"); globalError--; } } - claimvars = claimvars->next; + cli = cli->next; } termlistDelete (claimvars); termlistDelete (recvvars); } + else + { + /* If it is NOT a SECRET claim, then check parameters are ground */ + checkParameterGround (cl); + } if ((claim == CLAIM_Commit) || (claim == CLAIM_Running)) { @@ -596,14 +703,17 @@ claimCreate (const System sys, const Protocol protocol, const Role role, { /* yield error */ globalError++; - eprintf ("warning: "); + warning_pre (); termPrint (claim); eprintf (" claim of role "); termPrint (cl->rolename); eprintf (" requires four arguments. Please specify both the target role and the data to agree on, as in:\n"); + warning_pre (); eprintf (" claim(R, Commit, R', data )\n"); + warning_pre (); eprintf ("and\n"); + warning_pre (); eprintf (" claim(R', Running, R, data ).\n"); globalError--; error @@ -620,16 +730,20 @@ claimCreate (const System sys, const Protocol protocol, const Role role, { /* yield error */ globalError++; - eprintf ("warning: "); + warning_pre (); termPrint (claim); eprintf (" claim of role "); termPrint (cl->rolename); eprintf (" specifies the target role to be '"); termPrint (targetrole); eprintf ("', which is not a role name.\n"); + warning_pre (); eprintf ("Please use:\n"); + warning_pre (); eprintf (" claim(R, Commit, R', data )\n"); + warning_pre (); eprintf ("and\n"); + warning_pre (); eprintf (" claim(R', Running, R, data ).\n"); globalError--; error @@ -637,8 +751,16 @@ claimCreate (const System sys, const Protocol protocol, const Role role, lineno); } } - } + checkParameterRange (cl, CLAIM_Secret, 1, -1); + checkParameterRange (cl, CLAIM_SKR, 1, -1); + checkParameterRange (cl, CLAIM_Alive, 0, 0); + checkParameterRange (cl, CLAIM_Weakagree, 0, 0); + checkParameterRange (cl, CLAIM_Nisynch, 0, 0); + checkParameterRange (cl, CLAIM_Niagree, 0, 0); + checkParameterRange (cl, CLAIM_Empty, 0, 0); + checkParameterRange (cl, CLAIM_Reachable, 0, 0); + checkParameterRange (cl, CLAIM_SID, 1, -1); return cl; } @@ -831,7 +953,7 @@ commEvent (int event, Tac tc) /* handles claim types with different syntactic claims */ - if (claim == CLAIM_Secret) + if ((claim == CLAIM_Secret) || (claim == CLAIM_SKR)) { if (n == 0) {