- Added '--remove-claims' switch to cut off all existing claims.
This commit is contained in:
ccremers
parent
ca4c5674ac
commit
ccc4c34823
317
src/compiler.c
317
src/compiler.c
@ -463,162 +463,167 @@ commEvent (int event, Tac tc)
|
|||||||
|
|
||||||
break;
|
break;
|
||||||
case CLAIM:
|
case CLAIM:
|
||||||
/* now parse tuple info */
|
if (!switches.removeclaims)
|
||||||
if (trip == NULL || trip->next == NULL)
|
|
||||||
{
|
{
|
||||||
error ("Problem with claim %i event on line %i.", event,
|
/* now parse tuple info */
|
||||||
tc->lineno);
|
if (trip == NULL || trip->next == NULL)
|
||||||
}
|
{
|
||||||
fromrole = tacTerm (trip);
|
error ("Problem with claim %i event on line %i.", event,
|
||||||
claimbig = tacTerm (tacTuple ((trip->next)));
|
tc->lineno);
|
||||||
/* check for several types */
|
}
|
||||||
claim = tupleProject (claimbig, 0);
|
fromrole = tacTerm (trip);
|
||||||
torole = claim;
|
claimbig = tacTerm (tacTuple ((trip->next)));
|
||||||
|
/* check for several types */
|
||||||
|
claim = tupleProject (claimbig, 0);
|
||||||
|
torole = claim;
|
||||||
|
|
||||||
/* check for ignored claim types */
|
/* check for ignored claim types */
|
||||||
if (switches.filterClaim != NULL && switches.filterClaim != claim)
|
if (switches.filterClaim != NULL && switches.filterClaim != claim)
|
||||||
{
|
{
|
||||||
/* abort the construction of the node */
|
/* abort the construction of the node */
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
/* check for obvious flaws */
|
/* check for obvious flaws */
|
||||||
if (claim == NULL)
|
if (claim == NULL)
|
||||||
{
|
{
|
||||||
error ("Invalid claim specification on line %i.", tc->lineno);
|
error ("Invalid claim specification on line %i.", tc->lineno);
|
||||||
}
|
}
|
||||||
if (!inTermlist (claim->stype, TERM_Claim))
|
if (!inTermlist (claim->stype, TERM_Claim))
|
||||||
{
|
{
|
||||||
printf ("ERROR: unknown claim type ");
|
printf ("error: unknown claim type ");
|
||||||
|
termPrint (claim);
|
||||||
|
errorTac (trip->next->lineno);
|
||||||
|
}
|
||||||
|
/* unfold parameters to msg */
|
||||||
|
msg = NULL;
|
||||||
|
n = tupleCount (claimbig) - 1;
|
||||||
|
if (n < 1)
|
||||||
|
{
|
||||||
|
/* no parameters */
|
||||||
|
n = 0;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
/* n parameters */
|
||||||
|
msg = TermOp2 (deVar (claimbig));
|
||||||
|
if (tupleCount (msg) != n)
|
||||||
|
{
|
||||||
|
error ("Problem with claim tuple unfolding at line %i.",
|
||||||
|
trip->next->lineno);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/* store claim in claim list */
|
||||||
|
|
||||||
|
if (label == NULL)
|
||||||
|
{
|
||||||
|
error ("Claim should have label on line %i.",
|
||||||
|
trip->next->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 */
|
||||||
|
|
||||||
|
if (claim == CLAIM_Secret)
|
||||||
|
{
|
||||||
|
if (n == 0)
|
||||||
|
{
|
||||||
|
error
|
||||||
|
("Secrecy claim requires a list of terms to be secret on line %i.",
|
||||||
|
trip->next->lineno);
|
||||||
|
}
|
||||||
|
if (n > 1)
|
||||||
|
{
|
||||||
|
error
|
||||||
|
("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)
|
||||||
|
{
|
||||||
|
if (n != 0)
|
||||||
|
{
|
||||||
|
error ("NISYNCH claim requires no parameters at line %i.",
|
||||||
|
trip->next->lineno);
|
||||||
|
}
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
if (claim == CLAIM_Niagree)
|
||||||
|
{
|
||||||
|
if (n != 0)
|
||||||
|
{
|
||||||
|
error ("NIAGREE claim requires no parameters at line %i.",
|
||||||
|
trip->next->lineno);
|
||||||
|
}
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
if (claim == CLAIM_Empty)
|
||||||
|
{
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
|
||||||
|
/* hmm, no handler yet */
|
||||||
|
|
||||||
|
printf ("error: No know handler for this claim type: ");
|
||||||
termPrint (claim);
|
termPrint (claim);
|
||||||
|
printf (" ");
|
||||||
errorTac (trip->next->lineno);
|
errorTac (trip->next->lineno);
|
||||||
}
|
}
|
||||||
/* unfold parameters to msg */
|
|
||||||
msg = NULL;
|
|
||||||
n = tupleCount (claimbig) - 1;
|
|
||||||
if (n < 1)
|
|
||||||
{
|
|
||||||
/* no parameters */
|
|
||||||
n = 0;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
/* n parameters */
|
|
||||||
msg = TermOp2 (deVar (claimbig));
|
|
||||||
if (tupleCount (msg) != n)
|
|
||||||
{
|
|
||||||
error ("Problem with claim tuple unfolding at line %i.",
|
|
||||||
trip->next->lineno);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/* store claim in claim list */
|
|
||||||
|
|
||||||
if (label == NULL)
|
|
||||||
{
|
|
||||||
error ("Claim should have label on line %i.", trip->next->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 */
|
|
||||||
|
|
||||||
if (claim == CLAIM_Secret)
|
|
||||||
{
|
|
||||||
if (n == 0)
|
|
||||||
{
|
|
||||||
error
|
|
||||||
("Secrecy claim requires a list of terms to be secret on line %i.",
|
|
||||||
trip->next->lineno);
|
|
||||||
}
|
|
||||||
if (n > 1)
|
|
||||||
{
|
|
||||||
error
|
|
||||||
("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)
|
|
||||||
{
|
|
||||||
if (n != 0)
|
|
||||||
{
|
|
||||||
error ("NISYNCH claim requires no parameters at line %i.",
|
|
||||||
trip->next->lineno);
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
if (claim == CLAIM_Niagree)
|
|
||||||
{
|
|
||||||
if (n != 0)
|
|
||||||
{
|
|
||||||
error ("NIAGREE claim requires no parameters at line %i.",
|
|
||||||
trip->next->lineno);
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
if (claim == CLAIM_Empty)
|
|
||||||
{
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
|
|
||||||
/* hmm, no handler yet */
|
|
||||||
|
|
||||||
printf ("ERROR: No know handler for this claim type: ");
|
|
||||||
termPrint (claim);
|
|
||||||
printf (" ");
|
|
||||||
errorTac (trip->next->lineno);
|
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
/* and make that event */
|
/* and make that event */
|
||||||
@ -670,7 +675,7 @@ roleCompile (Term nameterm, Tac tc)
|
|||||||
}
|
}
|
||||||
if (thisRole == NULL)
|
if (thisRole == NULL)
|
||||||
{
|
{
|
||||||
printf ("ERROR: undeclared role name ");
|
printf ("error: undeclared role name ");
|
||||||
termPrint (nameterm);
|
termPrint (nameterm);
|
||||||
printf (" in line ");
|
printf (" in line ");
|
||||||
errorTac (tc->lineno);
|
errorTac (tc->lineno);
|
||||||
@ -710,7 +715,7 @@ roleCompile (Term nameterm, Tac tc)
|
|||||||
default:
|
default:
|
||||||
if (!normalDeclaration (tc))
|
if (!normalDeclaration (tc))
|
||||||
{
|
{
|
||||||
printf ("ERROR: illegal command %i in role ", tc->op);
|
printf ("error: illegal command %i in role ", tc->op);
|
||||||
termPrint (thisRole->nameterm);
|
termPrint (thisRole->nameterm);
|
||||||
printf (" ");
|
printf (" ");
|
||||||
errorTac (tc->lineno);
|
errorTac (tc->lineno);
|
||||||
@ -812,7 +817,7 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles)
|
|||||||
|
|
||||||
if (levelFind (prots, level) != NULL)
|
if (levelFind (prots, level) != NULL)
|
||||||
{
|
{
|
||||||
printf ("ERROR: Double declaration of protocol ");
|
printf ("error: Double declaration of protocol ");
|
||||||
symbolPrint (prots);
|
symbolPrint (prots);
|
||||||
printf (" ");
|
printf (" ");
|
||||||
errorTac (tc->lineno);
|
errorTac (tc->lineno);
|
||||||
@ -871,7 +876,7 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles)
|
|||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
printf ("ERROR: undeclared role ");
|
printf ("error: undeclared role ");
|
||||||
symbolPrint (tc->t1.sym);
|
symbolPrint (tc->t1.sym);
|
||||||
printf (" in protocol ");
|
printf (" in protocol ");
|
||||||
termPrint (pr->nameterm);
|
termPrint (pr->nameterm);
|
||||||
@ -881,7 +886,7 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles)
|
|||||||
default:
|
default:
|
||||||
if (!normalDeclaration (tc))
|
if (!normalDeclaration (tc))
|
||||||
{
|
{
|
||||||
printf ("ERROR: illegal command %i in protocol ", tc->op);
|
printf ("error: illegal command %i in protocol ", tc->op);
|
||||||
termPrint (thisProtocol->nameterm);
|
termPrint (thisProtocol->nameterm);
|
||||||
errorTac (tc->lineno);
|
errorTac (tc->lineno);
|
||||||
}
|
}
|
||||||
@ -915,7 +920,7 @@ tacProcess (Tac tc)
|
|||||||
default:
|
default:
|
||||||
if (!normalDeclaration (tc))
|
if (!normalDeclaration (tc))
|
||||||
{
|
{
|
||||||
printf ("ERROR: illegal command %i at the global level.\n",
|
printf ("error: illegal command %i at the global level.\n",
|
||||||
tc->op);
|
tc->op);
|
||||||
errorTac (tc->lineno);
|
errorTac (tc->lineno);
|
||||||
}
|
}
|
||||||
|
|||||||
@ -74,6 +74,7 @@ switchesInit (int argc, char **argv)
|
|||||||
// Misc
|
// Misc
|
||||||
switches.switchP = 0; // multi-purpose parameter
|
switches.switchP = 0; // multi-purpose parameter
|
||||||
switches.experimental = 0; // experimental stuff defaults to 0, whatever that means.
|
switches.experimental = 0; // experimental stuff defaults to 0, whatever that means.
|
||||||
|
switches.removeclaims = false; // default: leave claims from spdl file
|
||||||
|
|
||||||
// Output
|
// Output
|
||||||
switches.output = SUMMARY; // default is to show a summary
|
switches.output = SUMMARY; // default is to show a summary
|
||||||
@ -378,6 +379,22 @@ switcher (const int process, int index)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if (detect (' ', "remove-claims", 0))
|
||||||
|
{
|
||||||
|
if (!process)
|
||||||
|
{
|
||||||
|
/* discourage:
|
||||||
|
*
|
||||||
|
* Causes all existing claims in the specification to be skipped.
|
||||||
|
*/
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
switches.removeclaims = true;
|
||||||
|
return index;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
/* ==================
|
/* ==================
|
||||||
* Bounding options
|
* Bounding options
|
||||||
*/
|
*/
|
||||||
|
|||||||
@ -53,6 +53,7 @@ struct switchdata
|
|||||||
// Misc
|
// Misc
|
||||||
int switchP; //!< A multi-purpose integer parameter, passed to the partial order reduction method selected.
|
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 experimental; //!< Experimental stuff goes here until it moves into main stuff.
|
||||||
|
int removeclaims; //!< Remove any claims in the spdl file
|
||||||
|
|
||||||
// Output
|
// Output
|
||||||
int output; //!< From enum outputs: what should be produced. Default ATTACK.
|
int output; //!< From enum outputs: what should be produced. Default ATTACK.
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user