- Rollback of commit r674, because stuff was pretty broken. Work at that
in phases.
This commit is contained in:
ccremers
parent
570933612f
commit
ca975ed970
|
|
@ -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, synchr and agreement properties.
|
||||
*@todo "What is interesting" relies on the fact that there are only secrecy, sychnr and agreement properties.
|
||||
*/
|
||||
Roledef removeIrrelevant (const System sys, const int run, Roledef rd)
|
||||
{
|
||||
|
|
@ -237,25 +237,21 @@ 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 myRid)
|
||||
explorify (const System sys, const int run)
|
||||
{
|
||||
Roledef myRp;
|
||||
Roledef rd;
|
||||
int flag;
|
||||
int myStep;
|
||||
Run runs;
|
||||
Roledef roleCap, roleCapPart;
|
||||
|
||||
runs = sys->runs;
|
||||
myRp = runs[myRid].index;
|
||||
myStep = runs[myRid].step;
|
||||
rd = runPointerGet (sys, run);
|
||||
myStep = sys->runs[run].step;
|
||||
roleCap = NULL;
|
||||
|
||||
if (myRp == NULL)
|
||||
if (rd == NULL)
|
||||
{
|
||||
fprintf (stderr, "ERROR: trying to progress completed run!\n");
|
||||
exit (1);
|
||||
|
|
@ -266,40 +262,36 @@ explorify (const System sys, const int myRid)
|
|||
/*
|
||||
* Special checks after (implicit) choose events; always first in run reads.
|
||||
*/
|
||||
if (myStep == 0 && myRp->type == READ)
|
||||
if (myStep == 0 && rd->type == READ)
|
||||
{
|
||||
/*---------------------------------------------------------------------------*/
|
||||
/* special check 0: after choosing, terminate any runs by the intruder */
|
||||
/*---------------------------------------------------------------------------*/
|
||||
if (inTermlist (sys->untrusted, agentOfRun (sys, myRid)))
|
||||
int rid;
|
||||
|
||||
if (inTermlist (sys->untrusted, agentOfRun (sys, run)))
|
||||
{
|
||||
/* 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;
|
||||
|
||||
ridscan = 0;
|
||||
rid = 0;
|
||||
validclaim = 0;
|
||||
/* check for each run */
|
||||
while (ridscan < sys->maxruns)
|
||||
while (rid < sys->maxruns)
|
||||
{
|
||||
/* are claims in this run evaluated anyway? */
|
||||
if (trustedClaims (sys, ridscan))
|
||||
if (!untrustedAgent (sys, sys->runs[rid].agents))
|
||||
{ /* possibly claims to be checked in this run */
|
||||
rdscan = runPointerGet(sys, ridscan);
|
||||
rdscan = runPointerGet(sys, rid);
|
||||
while (rdscan != NULL)
|
||||
{
|
||||
if (rdscan->type == CLAIM)
|
||||
|
|
@ -307,7 +299,7 @@ explorify (const System sys, const int myRid)
|
|||
/* force abort of loop */
|
||||
validclaim = 1;
|
||||
rdscan = NULL;
|
||||
ridscan = sys->maxruns;
|
||||
rid = sys->maxruns;
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -315,39 +307,36 @@ explorify (const System sys, const int myRid)
|
|||
}
|
||||
}
|
||||
}
|
||||
ridscan++;
|
||||
rid++;
|
||||
}
|
||||
if (!validclaim)
|
||||
if (validclaim == 0)
|
||||
{ /* no valid claims, abort */
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
/*---------------------------------------------------------------------------*/
|
||||
/* Special check 2: Symmetry reduction on agent instances
|
||||
/* Special check 2: Symmetry reduction.
|
||||
* If the run we depend upon has already been activated (otherwise warn!) check for instance ordering
|
||||
*/
|
||||
/*---------------------------------------------------------------------------*/
|
||||
|
||||
if (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;
|
||||
if (runs[ridSymm].step == 0)
|
||||
ridSymm = sys->runs[run].prevSymmRun;
|
||||
if (sys->runs[ridSymm].step == 0)
|
||||
{
|
||||
/*
|
||||
* 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.
|
||||
* dependency run was not chosen yet, so we can't do anything now
|
||||
*/
|
||||
return 0;
|
||||
// warning ("Symmetrical run dependency #%i (for run #%i) has not chosen yet!", ridSymm, run);
|
||||
}
|
||||
else
|
||||
{
|
||||
/* dependent run has chosen, so we can compare */
|
||||
if (termlistOrder (runs[myRid].agents,
|
||||
runs[ridSymm].agents) < 0)
|
||||
if (termlistOrder (sys->runs[run].agents,
|
||||
sys->runs[ridSymm].agents) < 0)
|
||||
{
|
||||
/* we only explore the other half */
|
||||
return 0;
|
||||
|
|
@ -355,19 +344,15 @@ explorify (const System sys, const int myRid)
|
|||
}
|
||||
}
|
||||
|
||||
/*---------------------------------------------------------------------------*/
|
||||
/* Special check 3: if after choosing, this run ends on (read|skippedclaim)*, we can remove that part already.
|
||||
*/
|
||||
/*---------------------------------------------------------------------------*/
|
||||
|
||||
roleCap = removeIrrelevant (sys, myRid, myRp);
|
||||
roleCap = removeIrrelevant (sys, run, rd);
|
||||
|
||||
|
||||
/*---------------------------------------------------------------------------*/
|
||||
/* 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.
|
||||
|
||||
|
|
@ -375,7 +360,7 @@ explorify (const System sys, const int myRid)
|
|||
rid = 0;
|
||||
while (rid < sys->maxruns)
|
||||
{
|
||||
if (!untrustedAgent (sys, runs[rid].agents))
|
||||
if (!untrustedAgent (sys, sys->runs[rid].agents))
|
||||
{
|
||||
}
|
||||
rid++;
|
||||
|
|
@ -383,40 +368,36 @@ explorify (const System sys, const int myRid)
|
|||
*/
|
||||
}
|
||||
|
||||
/*---------------------------------------------------------------------------*/
|
||||
/*
|
||||
* 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 (runs[myRid].firstNonAgentRead == myStep)
|
||||
if (sys->runs[run].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 (myRp->type != READ)
|
||||
if (rd->type != READ)
|
||||
{
|
||||
error ("firstNonAgentRead is not a read?!");
|
||||
}
|
||||
ridSymm = runs[myRid].prevSymmRun;
|
||||
if (isTermlistEqual (runs[myRid].agents, runs[ridSymm].agents))
|
||||
ridSymm = sys->runs[run].prevSymmRun;
|
||||
if (isTermlistEqual (sys->runs[run].agents, sys->runs[ridSymm].agents))
|
||||
{
|
||||
/* same agents, so relevant */
|
||||
if (myStep > 0 && runs[ridSymm].step < myStep)
|
||||
if (myStep > 0 && sys->runs[ridSymm].step < myStep)
|
||||
{
|
||||
// warning ("Symmetrical firstread dependency #%i (for run #%i) has not chosen yet!", ridSymm, myRid);
|
||||
// warning ("Symmetrical firstread dependency #%i (for run #%i) has not chosen yet!", ridSymm, run);
|
||||
}
|
||||
else
|
||||
{
|
||||
if (runs[ridSymm].step <= myStep)
|
||||
if (sys->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, myRid, myStep, 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, run, myStep, sys->runs[ridSymm].step);
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -424,7 +405,7 @@ explorify (const System sys, const int myRid)
|
|||
int i;
|
||||
Roledef rdSymm;
|
||||
|
||||
rdSymm = runs[ridSymm].start;
|
||||
rdSymm = sys->runs[ridSymm].start;
|
||||
i = myStep;
|
||||
while (i > 0)
|
||||
{
|
||||
|
|
@ -432,7 +413,7 @@ explorify (const System sys, const int myRid)
|
|||
i--;
|
||||
}
|
||||
/* rdSymm now points to the instance of the symmetrical read */
|
||||
i = termOrder (rdSymm->message, myRp->message);
|
||||
i = termOrder (rdSymm->message, rd->message);
|
||||
if (i < 0)
|
||||
{
|
||||
/* only explore symmetrical variant */
|
||||
|
|
@ -444,33 +425,32 @@ explorify (const System sys, const int myRid)
|
|||
}
|
||||
}
|
||||
|
||||
/*---------------------------------------------------------------------------*/
|
||||
/* 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 == runs[myRid].firstReal && runs[myRid].prevSymmRun != -1)
|
||||
if (sys->switchSymmOrder && myStep == sys->runs[run].firstReal)
|
||||
{
|
||||
/* 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))
|
||||
if (sys->runs[run].prevSymmRun != -1)
|
||||
{
|
||||
/* so, we have an identical partner */
|
||||
/* is our partner there already? */
|
||||
if (runs[ridSymm].step <= myStep)
|
||||
/* 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))
|
||||
{
|
||||
/* not yet there, this is not a valid exploration */
|
||||
/* verify !! */
|
||||
return 0;
|
||||
/* 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;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -482,29 +462,15 @@ explorify (const System sys, const int myRid)
|
|||
roleCapPart = roleCap->next;
|
||||
roleCap->next = NULL;
|
||||
}
|
||||
if (executeStep (sys, myRid))
|
||||
if (executeStep (sys, run))
|
||||
{
|
||||
/* 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;
|
||||
|
|
@ -512,12 +478,6 @@ explorify (const System sys, const int myRid)
|
|||
return flag;
|
||||
}
|
||||
|
||||
|
||||
//! The simplest form of traversal.
|
||||
/**
|
||||
* All options are explored, and no partial order reduction is applied.
|
||||
*/
|
||||
|
||||
int
|
||||
traverseSimple (const System sys)
|
||||
{
|
||||
|
|
@ -1086,8 +1046,7 @@ 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. */
|
||||
i = 0;
|
||||
while (i < sys->maxruns && !flag)
|
||||
for (i = 0; i < sys->maxruns && !flag; i++)
|
||||
{
|
||||
run = (i + offset) % sys->maxruns;
|
||||
rd = runPointerGet (sys, run);
|
||||
|
|
@ -1099,7 +1058,8 @@ traversePOR4 (const System sys)
|
|||
case CLAIM:
|
||||
case SEND:
|
||||
executeTry (sys, run);
|
||||
return 1;
|
||||
flag = 1;
|
||||
break;
|
||||
|
||||
case READ:
|
||||
/* the sendsdone check only prevent
|
||||
|
|
@ -1139,7 +1099,6 @@ traversePOR4 (const System sys)
|
|||
exit (1);
|
||||
}
|
||||
}
|
||||
i++;
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
|
|
@ -1173,23 +1132,6 @@ 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 */
|
||||
|
|
@ -1197,23 +1139,41 @@ traversePOR5 (const System sys)
|
|||
}
|
||||
else
|
||||
{
|
||||
if (sys->traceEvent[sys->step-1]->internal &&
|
||||
sys->traceEvent[sys->step-1]->type == READ)
|
||||
/* 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)
|
||||
{
|
||||
/* 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;
|
||||
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);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/* 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. */
|
||||
i = 0;
|
||||
while (i < sys->maxruns && !flag)
|
||||
for (i = 0; i < sys->maxruns && !flag; i++)
|
||||
{
|
||||
run = (i + offset) % sys->maxruns;
|
||||
rd = runPointerGet (sys, run);
|
||||
|
|
@ -1233,7 +1193,7 @@ traversePOR5 (const System sys)
|
|||
* some unneccessary inKnowledge tests,
|
||||
* and branch tests, still improves
|
||||
* about 15% */
|
||||
if (!rd->internal && sys->knowPhase > rd->knowPhase)
|
||||
if (sys->knowPhase > rd->knowPhase)
|
||||
{
|
||||
/* apparently there has been a new knowledge item since the
|
||||
* previous check */
|
||||
|
|
@ -1266,7 +1226,6 @@ traversePOR5 (const System sys)
|
|||
exit (1);
|
||||
}
|
||||
}
|
||||
i++;
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -562,15 +562,14 @@ 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\"", sys->traceRun[index]);
|
||||
printf ("Skip claim in #%i\"", sys->traceRun[index]);
|
||||
}
|
||||
else
|
||||
{
|
||||
roledefPrint (rd);
|
||||
printf ("\"");
|
||||
printf ("#%i\"", sys->traceRun[index]);
|
||||
if (rd->type == CLAIM)
|
||||
{
|
||||
printf (",shape=house,color=green");
|
||||
|
|
|
|||
15
src/runs.c
15
src/runs.c
|
|
@ -515,9 +515,7 @@ 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;
|
||||
}
|
||||
}
|
||||
|
|
@ -549,9 +547,7 @@ 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 */
|
||||
|
|
@ -950,7 +946,7 @@ rolesPrint (Role r)
|
|||
*@return True iff any agent in the list is untrusted.
|
||||
*/
|
||||
int
|
||||
untrustedAgent (const System sys, Termlist agents)
|
||||
untrustedAgent (System sys, Termlist agents)
|
||||
{
|
||||
while (agents != NULL)
|
||||
{
|
||||
|
|
@ -978,15 +974,6 @@ untrustedAgent (const 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)
|
||||
|
|
|
|||
|
|
@ -296,8 +296,7 @@ void protocolPrint (Protocol p);
|
|||
void protocolsPrint (Protocol p);
|
||||
void rolePrint (Role r);
|
||||
void rolesPrint (Role r);
|
||||
int untrustedAgent (const System sys, Termlist agents);
|
||||
int trustedClaims (const System sys, const int run);
|
||||
int untrustedAgent (System sys, Termlist agents);
|
||||
int getMaxTraceLength (const System sys);
|
||||
void agentsOfRunPrint (const System sys, const int run);
|
||||
void violatedClaimPrint (const System sys, int i);
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user