From 1e7ef8f11dac8912076112600b939a249ef5e6d0 Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 16 Jul 2004 13:09:46 +0000 Subject: [PATCH] - Lots of rewrites and code cleanups. --- src/modelchecker.c | 225 +++++++++++++++++++++++++++------------------ src/output.c | 5 +- src/runs.c | 15 ++- src/runs.h | 3 +- 4 files changed, 152 insertions(+), 96 deletions(-) diff --git a/src/modelchecker.c b/src/modelchecker.c index 36f03de..67a54ae 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -195,7 +195,7 @@ executeStep (const System sys, const int run) /** * Determine for a roledef that is instantiated, the uninteresting ends bits. * - *@todo "What is interesting" relies on the fact that there are only secrecy, sychnr and agreement properties. + *@todo "What is interesting" relies on the fact that there are only secrecy, synchr and agreement properties. */ Roledef removeIrrelevant (const System sys, const int run, Roledef rd) { @@ -237,21 +237,25 @@ Roledef removeIrrelevant (const System sys, const int run, Roledef rd) //! Explores the system state given by the next step of a run. /** * grandiose naming scheme (c) sjors dubya. + * + * Fairly complex as it also handles pruning of traces according to symmetry reductions and such. */ int -explorify (const System sys, const int run) +explorify (const System sys, const int myRid) { - Roledef rd; + Roledef myRp; int flag; int myStep; + Run runs; Roledef roleCap, roleCapPart; - rd = runPointerGet (sys, run); - myStep = sys->runs[run].step; + runs = sys->runs; + myRp = runs[myRid].index; + myStep = runs[myRid].step; roleCap = NULL; - if (rd == NULL) + if (myRp == NULL) { fprintf (stderr, "ERROR: trying to progress completed run!\n"); exit (1); @@ -262,36 +266,40 @@ explorify (const System sys, const int run) /* * Special checks after (implicit) choose events; always first in run reads. */ - if (myStep == 0 && rd->type == READ) + if (myStep == 0 && myRp->type == READ) { - int rid; - - if (inTermlist (sys->untrusted, agentOfRun (sys, run))) + /*---------------------------------------------------------------------------*/ + /* special check 0: after choosing, terminate any runs by the intruder */ + /*---------------------------------------------------------------------------*/ + if (inTermlist (sys->untrusted, agentOfRun (sys, myRid))) { /* this run is executed by an untrusted agent, do not explore */ return 0; } /* executed by trusted agent */ + /*---------------------------------------------------------------------------*/ /* Special check 1: if agents have been instantiated in such a way that no more claims in any run * need to be evaluated, then we can skip * further traversal. */ //!@todo This implementation relies on the fact that there are only secrecy, sychnr and agreement properties. + /*---------------------------------------------------------------------------*/ if (sys->secrets == NULL) { /* there are no remaining secrecy claims to be checked */ Roledef rdscan; int validclaim; + int ridscan; - rid = 0; + ridscan = 0; validclaim = 0; /* check for each run */ - while (rid < sys->maxruns) + while (ridscan < sys->maxruns) { /* are claims in this run evaluated anyway? */ - if (!untrustedAgent (sys, sys->runs[rid].agents)) + if (trustedClaims (sys, ridscan)) { /* possibly claims to be checked in this run */ - rdscan = runPointerGet(sys, rid); + rdscan = runPointerGet(sys, ridscan); while (rdscan != NULL) { if (rdscan->type == CLAIM) @@ -299,7 +307,7 @@ explorify (const System sys, const int run) /* force abort of loop */ validclaim = 1; rdscan = NULL; - rid = sys->maxruns; + ridscan = sys->maxruns; } else { @@ -307,36 +315,39 @@ explorify (const System sys, const int run) } } } - rid++; + ridscan++; } - if (validclaim == 0) + if (!validclaim) { /* no valid claims, abort */ return 0; } } - /* Special check 2: Symmetry reduction. + /*---------------------------------------------------------------------------*/ + /* Special check 2: Symmetry reduction on agent instances * If the run we depend upon has already been activated (otherwise warn!) check for instance ordering */ + /*---------------------------------------------------------------------------*/ - if (sys->runs[run].prevSymmRun != -1) + if (runs[myRid].prevSymmRun != -1) { /* there is such a run on which we depend */ int ridSymm; - ridSymm = sys->runs[run].prevSymmRun; - if (sys->runs[ridSymm].step == 0) + ridSymm = runs[myRid].prevSymmRun; + if (runs[ridSymm].step == 0) { /* - * dependency run was not chosen yet, so we can't do anything now + * Dependency run was not chosen yet, so we can't do anything now. + * This is typically caused by any possibly delayed first reads with other stuff in it than agents. */ - // warning ("Symmetrical run dependency #%i (for run #%i) has not chosen yet!", ridSymm, run); + return 0; } else { /* dependent run has chosen, so we can compare */ - if (termlistOrder (sys->runs[run].agents, - sys->runs[ridSymm].agents) < 0) + if (termlistOrder (runs[myRid].agents, + runs[ridSymm].agents) < 0) { /* we only explore the other half */ return 0; @@ -344,15 +355,19 @@ explorify (const System sys, const int run) } } + /*---------------------------------------------------------------------------*/ /* Special check 3: if after choosing, this run ends on (read|skippedclaim)*, we can remove that part already. */ + /*---------------------------------------------------------------------------*/ - roleCap = removeIrrelevant (sys, run, rd); + roleCap = removeIrrelevant (sys, myRid, myRp); + /*---------------------------------------------------------------------------*/ /* Special check x: if all agents in each run send only encrypted stuff, and all agents are trusted, * there is no way for the intruder to learn anything else than encrypted terms, so secrecy claims will not * be violated anymore if they contain no terms that are encrypted with such keys */ + /*---------------------------------------------------------------------------*/ //!@todo For now, there is no check that the runs only send publicly encrypted stuff! Just an assumption to be made true using static analysis. @@ -360,7 +375,7 @@ explorify (const System sys, const int run) rid = 0; while (rid < sys->maxruns) { - if (!untrustedAgent (sys, sys->runs[rid].agents)) + if (!untrustedAgent (sys, runs[rid].agents)) { } rid++; @@ -368,36 +383,40 @@ explorify (const System sys, const int run) */ } + /*---------------------------------------------------------------------------*/ /* * Special check b1: symmetry reduction part II on similar read events for equal roles. + * + * This assumes a left-right traversal of these first real events. */ + /*---------------------------------------------------------------------------*/ if (sys->switchReadSymm) { - if (sys->runs[run].firstNonAgentRead == myStep) + if (runs[myRid].firstNonAgentRead == myStep) { /* Apparently, we have a possible ordering with our symmetrical friend. * Check if it has progressed enough, and has the same agents. */ int ridSymm; - if (rd->type != READ) + if (myRp->type != READ) { error ("firstNonAgentRead is not a read?!"); } - ridSymm = sys->runs[run].prevSymmRun; - if (isTermlistEqual (sys->runs[run].agents, sys->runs[ridSymm].agents)) + ridSymm = runs[myRid].prevSymmRun; + if (isTermlistEqual (runs[myRid].agents, runs[ridSymm].agents)) { /* same agents, so relevant */ - if (myStep > 0 && sys->runs[ridSymm].step < myStep) + if (myStep > 0 && runs[ridSymm].step < myStep) { - // warning ("Symmetrical firstread dependency #%i (for run #%i) has not chosen yet!", ridSymm, run); + // warning ("Symmetrical firstread dependency #%i (for run #%i) has not chosen yet!", ridSymm, myRid); } else { - if (sys->runs[ridSymm].step <= myStep) + if (runs[ridSymm].step <= myStep) { - // warning ("Symmetrical firstread dependency #%i (for run #%i) has not read it's firstNonAgentRead %i yet, as it is only at %i!", ridSymm, run, myStep, sys->runs[ridSymm].step); + // warning ("Symmetrical firstread dependency #%i (for run #%i) has not read it's firstNonAgentRead %i yet, as it is only at %i!", ridSymm, myRid, myStep, runs[ridSymm].step); } else { @@ -405,7 +424,7 @@ explorify (const System sys, const int run) int i; Roledef rdSymm; - rdSymm = sys->runs[ridSymm].start; + rdSymm = runs[ridSymm].start; i = myStep; while (i > 0) { @@ -413,7 +432,7 @@ explorify (const System sys, const int run) i--; } /* rdSymm now points to the instance of the symmetrical read */ - i = termOrder (rdSymm->message, rd->message); + i = termOrder (rdSymm->message, myRp->message); if (i < 0) { /* only explore symmetrical variant */ @@ -425,32 +444,33 @@ explorify (const System sys, const int run) } } + /*---------------------------------------------------------------------------*/ /* Special check b2: symmetry order reduction. * * Concept: when there are two identical runs w.r.t. agents, we can make sure one goes before the other. * Depends on prevSymm, skipping chooses even. + * + * This assumes a left-right traversal of these first real events. Therefore, some --pp values will cause problems, e.g. -1 */ + /*---------------------------------------------------------------------------*/ - if (sys->switchSymmOrder && myStep == sys->runs[run].firstReal) + if (sys->switchSymmOrder && myStep == runs[myRid].firstReal && runs[myRid].prevSymmRun != -1) { - if (sys->runs[run].prevSymmRun != -1) + /* there is such a run on which we depend */ + int ridSymm; + + ridSymm = runs[myRid].prevSymmRun; + /* equal runs? */ + + if (isTermlistEqual (runs[myRid].agents, runs[ridSymm].agents)) { - /* there is such a run on which we depend */ - int ridSymm; - - ridSymm = sys->runs[run].prevSymmRun; - /* equal runs? */ - - if (isTermlistEqual (sys->runs[run].agents, sys->runs[ridSymm].agents)) + /* so, we have an identical partner */ + /* is our partner there already? */ + if (runs[ridSymm].step <= myStep) { - /* so, we have an identical partner */ - /* is our partner there already? */ - if (sys->runs[ridSymm].step <= myStep) - { - /* not yet there, this is not a valid exploration */ - /* verify !! */ - return 0; - } + /* not yet there, this is not a valid exploration */ + /* verify !! */ + return 0; } } } @@ -462,15 +482,29 @@ explorify (const System sys, const int run) roleCapPart = roleCap->next; roleCap->next = NULL; } - if (executeStep (sys, run)) + if (executeStep (sys, myRid)) { /* traverse the system after the step */ flag = traverse (sys); - runPointerSet (sys, run, rd); // reset rd pointer - sys->runs[run].step = myStep; // reset local index - sys->step--; - indentSet (sys->step); } + runPointerSet (sys, myRid, myRp); // reset myRp pointer + runs[myRid].step = myStep; // reset local index + sys->step--; + + /* reset state */ + /* first restore executeStep damage */ +#ifdef DEBUG + if (sys->step < 0) + { + error ("Global step counter has fallen below 0."); + } + if (runs[myRid].step < 0) + { + error ("Local step counter has fallen below 0."); + } +#endif + indentSet (sys->step); + /* restore roleCap damage */ if (roleCap != NULL) { roleCap->next = roleCapPart; @@ -478,6 +512,12 @@ explorify (const System sys, const int run) return flag; } + +//! The simplest form of traversal. +/** + * All options are explored, and no partial order reduction is applied. + */ + int traverseSimple (const System sys) { @@ -1046,7 +1086,8 @@ traversePOR4 (const System sys) /* Try all events (implicitly we only handle enabled ones) starting with our * first choice. If one was chosen, flag is set, and the loop aborts. */ - for (i = 0; i < sys->maxruns && !flag; i++) + i = 0; + while (i < sys->maxruns && !flag) { run = (i + offset) % sys->maxruns; rd = runPointerGet (sys, run); @@ -1058,8 +1099,7 @@ traversePOR4 (const System sys) case CLAIM: case SEND: executeTry (sys, run); - flag = 1; - break; + return 1; case READ: /* the sendsdone check only prevent @@ -1099,6 +1139,7 @@ traversePOR4 (const System sys) exit (1); } } + i++; } return flag; } @@ -1132,6 +1173,23 @@ traversePOR5 (const System sys) * and where lastrun is the runid of the previous event * in the trace, or 0 if there was none. */ + + /* First pick out any choose events */ + run = 0; + while (run < sys->maxruns && !flag) + { + rd = runPointerGet (sys, run); + + if (rd != NULL && rd->type == READ && rd->internal) + { + if (executeTry (sys, run)) + { + return 1; + } + } + run++; + } + if (sys->step == 0) { /* first step, start at 0 */ @@ -1139,41 +1197,23 @@ traversePOR5 (const System sys) } else { - /* there was a previous action, start scan from there */ - offset = sys->traceRun[sys->step - 1] + sys->porparam; - } - - /* First pick out any choose events */ - for (i = 0; i < sys->maxruns && !flag; i++) - { - run = (i + offset) % sys->maxruns; - rd = runPointerGet (sys, run); - - if (rd != NULL) + if (sys->traceEvent[sys->step-1]->internal && + sys->traceEvent[sys->step-1]->type == READ) { - switch (rd->type) - { - case CLAIM: - case SEND: - break; - - case READ: - if (rd->internal) - { - flag = executeTry (sys, run); - } - break; - - default: - fprintf (stderr, "Encountered unknown event type %i.\n", rd->type); - exit (1); - } + /* we just finished off the previous round of chooses */ + offset = 0; + } + else + { + /* there was a previous action, start scan from there */ + offset = sys->traceRun[sys->step - 1] + sys->porparam; } } /* Try all events (implicitly we only handle enabled ones) starting with our * first choice. If one was chosen, flag is set, and the loop aborts. */ - for (i = 0; i < sys->maxruns && !flag; i++) + i = 0; + while (i < sys->maxruns && !flag) { run = (i + offset) % sys->maxruns; rd = runPointerGet (sys, run); @@ -1193,7 +1233,7 @@ traversePOR5 (const System sys) * some unneccessary inKnowledge tests, * and branch tests, still improves * about 15% */ - if (sys->knowPhase > rd->knowPhase) + if (!rd->internal && sys->knowPhase > rd->knowPhase) { /* apparently there has been a new knowledge item since the * previous check */ @@ -1226,6 +1266,7 @@ traversePOR5 (const System sys) exit (1); } } + i++; } return flag; } diff --git a/src/output.c b/src/output.c index f5c3206..bce9577 100644 --- a/src/output.c +++ b/src/output.c @@ -562,14 +562,15 @@ void graphNode (const System sys) printf ("\tn%li -> n%li ", parentNode, thisNode); /* add label */ printf ("[label=\""); + printf ("%i:%i ", sys->traceRun[index], sys->runs[sys->traceRun[index]].step-1); if (rd->type == CLAIM && untrustedAgent (sys, sys->runs[sys->traceRun[index]].agents)) { - printf ("Skip claim in #%i\"", sys->traceRun[index]); + printf ("Skip claim\"", sys->traceRun[index]); } else { roledefPrint (rd); - printf ("#%i\"", sys->traceRun[index]); + printf ("\""); if (rd->type == CLAIM) { printf (",shape=house,color=green"); diff --git a/src/runs.c b/src/runs.c index 7e3559f..e8c3cdf 100644 --- a/src/runs.c +++ b/src/runs.c @@ -515,7 +515,9 @@ int staticRunSymmetry (const System sys,const int rid) if (al == NULL && isEqual) { /* this candidate is allright */ +#ifdef DEBUG warning ("Symmetry detection. #%i can depend on #%i.",rid,ridSymm); +#endif return ridSymm; } } @@ -547,7 +549,9 @@ int firstNonAgentRead (const System sys, int rid) } if (rd != NULL && !rd->internal && rd->type == READ) // assumes lazy LR eval { +#ifdef DEBUG warning ("First read %i with dependency on symmetrical found in run %i.", step, rid); +#endif return step; } /* no such read */ @@ -946,7 +950,7 @@ rolesPrint (Role r) *@return True iff any agent in the list is untrusted. */ int -untrustedAgent (System sys, Termlist agents) +untrustedAgent (const System sys, Termlist agents) { while (agents != NULL) { @@ -974,6 +978,15 @@ untrustedAgent (System sys, Termlist agents) return 0; } +//! Determine for a run whether the claims are trusted +/** + * Nice inline candidate. + */ +int trustedClaims (const System sys, const int run) +{ + return (!untrustedAgent (sys, sys->runs[run].agents)); +} + //! Yield the maximum length of a trace by analysing the runs in the system. int getMaxTraceLength (const System sys) diff --git a/src/runs.h b/src/runs.h index bdceb51..4a253aa 100644 --- a/src/runs.h +++ b/src/runs.h @@ -296,7 +296,8 @@ void protocolPrint (Protocol p); void protocolsPrint (Protocol p); void rolePrint (Role r); void rolesPrint (Role r); -int untrustedAgent (System sys, Termlist agents); +int untrustedAgent (const System sys, Termlist agents); +int trustedClaims (const System sys, const int run); int getMaxTraceLength (const System sys); void agentsOfRunPrint (const System sys, const int run); void violatedClaimPrint (const System sys, int i);