From ec3be3d55bb17f3904f115cba2e40bed5d6df826 Mon Sep 17 00:00:00 2001 From: ccremers Date: Tue, 8 Aug 2006 12:30:29 +0000 Subject: [PATCH] - Implemented --claim=ns3,I switch to filter certain claims. --- src/arachne.c | 200 ++++++++++++++++++++++++------------------------- src/compiler.c | 61 +++++++++++---- src/switches.c | 41 +++++++++- src/switches.h | 3 +- src/todo.txt | 6 -- 5 files changed, 186 insertions(+), 125 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index e0ed4c3..7438df4 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -2238,129 +2238,125 @@ arachneClaim (Claimlist cl) // Skip the dummy claims if (!isTermEqual (cl->type, CLAIM_Empty)) { - // Any other claims might be filterered - if (switches.filterClaim == NULL || switches.filterClaim == cl->type) + // Some claims are always true! + if (!cl->alwaystrue) { - // Some claims are always true! - if (!cl->alwaystrue) + // others we simply test... + int run; + int newruns; + Protocol p; + Role r; + + newruns = 0; + sys->current_claim = cl; + attack_length = INT_MAX; + attack_leastcost = INT_MAX; + cl->complete = 1; + p = (Protocol) cl->protocol; + r = (Role) cl->role; + + if (switches.output == PROOF) { - // others we simply test... - int run; - int newruns; - Protocol p; - Role r; + indentPrint (); + eprintf ("Testing Claim "); + termPrint (cl->type); + eprintf (" from "); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf (" at index %i.\n", cl->ev); + } + indentDepth++; - newruns = 0; - sys->current_claim = cl; - attack_length = INT_MAX; - attack_leastcost = INT_MAX; - cl->complete = 1; - p = (Protocol) cl->protocol; - r = (Role) cl->role; + run = semiRunCreate (p, r); + newruns++; + { + int newgoals; - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Testing Claim "); - termPrint (cl->type); - eprintf (" from "); - termPrint (p->nameterm); - eprintf (", "); - termPrint (r->nameterm); - eprintf (" at index %i.\n", cl->ev); - } - indentDepth++; - - run = semiRunCreate (p, r); - newruns++; - { - int newgoals; - - int realStart (void) - { + int realStart (void) + { #ifdef DEBUG - if (DEBUGL (5)) - { - printSemiState (); - } -#endif - return iterate_buffer_attacks (); + if (DEBUGL (5)) + { + printSemiState (); } +#endif + return iterate_buffer_attacks (); + } - proof_suppose_run (run, 0, cl->ev + 1); - newgoals = add_read_goals (run, 0, cl->ev + 1); + proof_suppose_run (run, 0, cl->ev + 1); + newgoals = add_read_goals (run, 0, cl->ev + 1); /** * Add initial knowledge node */ - { - Termlist m0tl; - Term m0t; - int m0run; + { + Termlist m0tl; + Term m0t; + int m0run; - m0tl = knowledgeSet (sys->know); - m0t = termlist_to_tuple (m0tl); - // eprintf("Initial intruder knowledge node for "); - // termPrint(m0t); - // eprintf("\n"); - I_M->roledef->message = m0t; - m0run = semiRunCreate (INTRUDER, I_M); - newruns++; - proof_suppose_run (m0run, 0, 1); - sys->runs[m0run].height = 1; + m0tl = knowledgeSet (sys->know); + m0t = termlist_to_tuple (m0tl); + // eprintf("Initial intruder knowledge node for "); + // termPrint(m0t); + // eprintf("\n"); + I_M->roledef->message = m0t; + m0run = semiRunCreate (INTRUDER, I_M); + newruns++; + proof_suppose_run (m0run, 0, 1); + sys->runs[m0run].height = 1; - { + { /** * Add specific goal info and iterate algorithm */ - add_claim_specifics (sys, cl, - roledef_shift (sys->runs[run]. - start, cl->ev), - realStart); - } - - - // remove initial knowledge node - termDelete (m0t); - termlistDelete (m0tl); - semiRunDestroy (); - newruns--; - } - // remove claiming run goals - goal_remove_last (newgoals); - semiRunDestroy (); - newruns--; + add_claim_specifics (sys, cl, + roledef_shift (sys->runs[run]. + start, cl->ev), + realStart); } - //! Destroy - while (sys->maxruns > 0 && newruns > 0) - { - semiRunDestroy (); - newruns--; - } + + + // remove initial knowledge node + termDelete (m0t); + termlistDelete (m0tl); + semiRunDestroy (); + newruns--; + } + // remove claiming run goals + goal_remove_last (newgoals); + semiRunDestroy (); + newruns--; + } + //! Destroy + while (sys->maxruns > 0 && newruns > 0) + { + semiRunDestroy (); + newruns--; + } #ifdef DEBUG - if (sys->bindings != NULL) - { - error ("sys->bindings NOT empty after claim test."); - } - if (sys->maxruns != 0) - { - error ("%i undestroyed runs left after claim test.", - sys->maxruns); - } - if (newruns != 0) - { - error ("Lost %i runs after claim test.", newruns); - } + if (sys->bindings != NULL) + { + error ("sys->bindings NOT empty after claim test."); + } + if (sys->maxruns != 0) + { + error ("%i undestroyed runs left after claim test.", + sys->maxruns); + } + if (newruns != 0) + { + error ("Lost %i runs after claim test.", newruns); + } #endif - //! Indent back - indentDepth--; + //! Indent back + indentDepth--; - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Proof complete for this claim.\n"); - } + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Proof complete for this claim.\n"); } } claimStatusReport (sys, cl); diff --git a/src/compiler.c b/src/compiler.c index 3b25f06..6d9057c 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -1,6 +1,7 @@ #include #include #include +#include #include "tac.h" #include "term.h" #include "termlist.h" @@ -431,11 +432,31 @@ claimCreate (const System sys, const Protocol protocol, const Role role, Claimlist cl; Term labeltuple; - /* check for ignored claim types */ - if (switches.filterClaim != NULL && switches.filterClaim != claim) + if (switches.filterProtocol != NULL) { - /* abort the construction of the node */ - return; + // only this protocol + if (strcmp + (switches.filterProtocol, TermSymb (protocol->nameterm)->text) != 0) + { + // not this protocol; return + return NULL; + } + // and maybe also a specific label? + if (switches.filterLabel != NULL) + { + Term t; + + t = label; + while (isTermTuple (t)) + { + t = TermOp2 (t); + } + if (strcmp (switches.filterLabel, TermSymb (t)->text) != 0) + { + // not this label; return + return NULL; + } + } } /* generate full unique label */ @@ -556,16 +577,15 @@ commEvent (int event, Tac tc) /* effectively, labels are bound to the protocol */ level--; /* leaves a garbage tuple. dunnoh what to do with it */ - label = - makeTermTuple (thisProtocol->nameterm, levelConst (tc->t1.sym)); + label = levelConst (tc->t1.sym); level++; } else { /* leaves a garbage tuple. dunnoh what to do with it */ - label = makeTermTuple (thisProtocol->nameterm, label); } } + label = makeTermTuple (thisProtocol->nameterm, label); /** * Parse the specific event type @@ -1017,17 +1037,28 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles) Protocol pr; Term t; - if (levelFind (prots, level) != NULL) - { - globalError++; - eprintf ("error: Double declaration of protocol "); - symbolPrint (prots); - eprintf (" "); - errorTac (tc->lineno); - } /* make new (empty) current protocol with name */ pr = protocolCreate (levelConst (prots)); thisProtocol = pr; + { + // check for double name declarations + Protocol prold; + + prold = sys->protocols; + while (prold != NULL) + { + if (isTermEqual (pr->nameterm, prold->nameterm)) + { + globalError++; + eprintf ("error: Double declaration of protocol "); + symbolPrint (prots); + eprintf (" "); + errorTac (tc->lineno); + } + prold = prold->next; + } + } + /* add protocol to list */ pr->next = sys->protocols; sys->protocols = pr; diff --git a/src/switches.c b/src/switches.c index 14b86f9..42777e4 100644 --- a/src/switches.c +++ b/src/switches.c @@ -53,7 +53,8 @@ switchesInit (int argc, char **argv) switches.maxproofdepth = INT_MAX; switches.maxtracelength = INT_MAX; switches.runs = 5; // default is 5 for usability, but -r 0 or --maxruns=0 will set it back to INT_MAX - switches.filterClaim = NULL; // default check all claims + switches.filterProtocol = NULL; // default check all claims + switches.filterLabel = NULL; // default check all claims switches.maxAttacks = 0; // no maximum default // Arachne @@ -299,6 +300,20 @@ switcher (const int process, int index, int commandline) arg_pointer = argv[index]; } + //! Retrieve a (string) argument + char *string_argument (void) + { + char *result; + + if (arg_pointer == NULL) + { + error ("Argument expected."); + } + result = arg_pointer; + arg_next (); + return result; + } + //! Parse an argument into an integer int integer_argument (void) { @@ -480,6 +495,30 @@ switcher (const int process, int index, int commandline) } } + if (detect (' ', "claim", 1)) + { + if (!process) + { + helptext ("--claim=[,