diff --git a/src/claims.c b/src/claims.c index 62a387a..307ef47 100644 --- a/src/claims.c +++ b/src/claims.c @@ -25,8 +25,10 @@ events_match (const System sys, const int i, const int j) rdi = sys->traceEvent[i]; rdj = sys->traceEvent[j]; - if (rdi->message == rdj->message && rdi->from == rdj->from && - rdi->to == rdj->to && rdi->label == rdj->label && + if (isTermEqual (rdi->message, rdj->message) && + isTermEqual (rdi->from, rdj->from) && + isTermEqual (rdi->to, rdj->to) && + isTermEqual (rdi->label, rdj->label) && !(rdi->internal || rdj->internal)) { if (rdi->type == SEND && rdj->type == READ) @@ -53,6 +55,7 @@ events_match (const System sys, const int i, const int j) * g maps all labels in prec to the event indices for things already found, * or to LABEL_TODO for things not found yet but in prec, and LABEL_GOOD for well linked messages (and that have thus defined a runid for the corresponding role). * All values not in prec map to -1. + *@returns 1 iff the claim is allright, 0 iff it is violated. */ int oki_nisynch (const System sys, const int i, const Termmap f, const Termmap g) @@ -129,19 +132,23 @@ oki_nisynch (const System sys, const int i, const Termmap f, const Termmap g) Term rolename; Termmap gscan; + /* + * Two options: it is either involved or not + */ + // 1. Assume that this run is not yet involved + result = oki_nisynch (sys, i-1, f, g); + // 2. It is involved. Then either already used for this role, or will be now. rolename = sys->runs[rid].role->nameterm; rid2 = termmapGet (f, rolename); - result = oki_nisynch (sys, i-1, f, g); - // Assume that this run is not yet involved - gscan = g; - while (gscan != NULL) + if (rid2 == -1 || rid2 == rid) { - // Ordered match needed - if (gscan->result > -1 && - events_match (sys, gscan->result, i) == 1) + // Was not involved yet in a registerd way, or was the correct rid + gscan = g; + while (!result && gscan != NULL) { - // Events match: but is the run a good candidate? - if (rid2 == -1 || rid2 == rid) + // Ordered match needed + if (gscan->result > -1 && + events_match (sys, gscan->result, i) == 1) { Termmap fbuf, gbuf; @@ -152,12 +159,12 @@ oki_nisynch (const System sys, const int i, const Termmap f, const Termmap g) fbuf = termmapSet (fbuf, rolename, rid); gbuf = termmapDuplicate (g); gbuf = termmapSet (gbuf, rd->label, -3); - result = oki_nisynch (sys, i-1, fbuf, gbuf); + result = oki_nisynch (sys, i-1, fbuf, gbuf) || result; termmapDelete (gbuf); termmapDelete (fbuf); } + gscan = gscan->next; } - gscan = gscan->next; } return result; } @@ -174,20 +181,46 @@ oki_nisynch (const System sys, const int i, const Termmap f, const Termmap g) */ //! Check validity of ni-synch claim at event i. +/** + *@returns 1 iff claim is true. + */ int check_claim_nisynch (const System sys, const int i) { + Roledef rd; int result; int rid; Termmap f,g; + Term label; + Claimlist cl; + Termlist tl; rid = sys->traceRun[i]; + rd = sys->traceEvent[i]; + cl = rd->claiminfo; + cl->count++; f = termmapSet (NULL, sys->runs[rid].role->nameterm, rid); - /** - *@todo g should map all labels in prec to LABEL_TODO + + // map all labels in prec to LABEL_TODO + g = NULL; + label = rd->label; + + tl = cl->prec; + while (tl != NULL) + { + g = termmapSet (g, tl->term, LABEL_TODO); + tl = tl->next; + } + /* + * Check claim */ - result = oki_nisynch(sys, i, f, NULL); + result = oki_nisynch(sys, i, f, g); + if (!result) + { + cl->failed++; + } termmapDelete (f); + termmapDelete (g); return result; } diff --git a/src/compiler.c b/src/compiler.c index da37128..f2fc26a 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -356,6 +356,7 @@ commEvent (int event, Tac tc) fromrole = tacTerm (trip); torole = tacTerm (trip->next); msg = tacTerm (tacTuple ((trip->next->next))); + cl = NULL; break; case CLAIM: @@ -452,7 +453,7 @@ commEvent (int event, Tac tc) } /* and make that event */ thisRole->roledef = roledefAdd (thisRole->roledef, event, label, - fromrole, torole, msg); + fromrole, torole, msg, cl); } int @@ -1055,7 +1056,13 @@ compute_prec_sets (const System sys) void preprocess (const System sys) { + /* + * init some counters + */ sys->rolecount = compute_rolecount(sys); sys->roleeventmax = compute_roleeventmax(sys); + /* + * compute preceding label sets + */ compute_prec_sets(sys); } diff --git a/src/modelchecker.c b/src/modelchecker.c index ade44a9..e968413 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -13,6 +13,7 @@ #include "output.h" #include "tracebuf.h" #include "attackminimize.h" +#include "claims.h" /* @@ -1012,11 +1013,12 @@ claimViolationDetails (const System sys, const int run, const Roledef rd, const return NULL; } -/* This happens when we violate a claim. +//! A claim was violated. +/** + * This happens when we violate a claim. * Lots of administration. - * Returns true iff explorify is in order. + *@returns True iff explorify is in order. */ - int violateClaim (const System sys, int length, int claimev, Termlist reqt) { @@ -1096,9 +1098,12 @@ executeTry (const System sys, int run) flag = send_basic (sys, run); return flag; } + + /* + * Execute claim event + */ if (runPoint->type == CLAIM) { - /* first we might dynamically determine whether the claim is valid */ if (untrustedAgent (sys, sys->runs[run].agents)) { @@ -1129,10 +1134,19 @@ executeTry (const System sys, int run) printf ("#%i\n", run); } #endif + /* + * update claim counters + */ sys->claims++; + /* + * distinguish claim types + */ if (runPoint->to == CLAIM_Secret) { + /* + * SECRECY + */ /* TODO claims now have their own type, test for that */ /* TODO for now it is secrecy of the message */ @@ -1141,6 +1155,7 @@ executeTry (const System sys, int run) sys->secrets = termlistAdd (termlistShallow (oldsecrets), runPoint->message); flag = claimSecrecy (sys, runPoint->message); + runPoint->claiminfo->count++; /* now check whether the claim failed for further actions */ if (!flag) @@ -1148,6 +1163,7 @@ executeTry (const System sys, int run) /* violation */ Termlist tl; + runPoint->claiminfo->failed++; tl = claimViolationDetails(sys,run,runPoint,sys->know); if (violateClaim (sys,sys->step+1, sys->step, tl )) flag = explorify (sys, run); @@ -1165,7 +1181,23 @@ executeTry (const System sys, int run) } if (runPoint->to == CLAIM_Nisynch) { - /* TODO nisynch implementation */ + /* + * NISYNCH + */ + //!@todo TODO nisynch implementation + + flag = check_claim_nisynch (sys, sys->step); + if (!flag) + { + /* violation */ + if (violateClaim (sys,sys->step+1, sys->step, NULL )) + flag = explorify (sys, run); + } + else + { + /* no violation */ + flag = explorify (sys, run); + } } } /* a claim always succeeds */ diff --git a/src/runs.c b/src/runs.c index db1886b..02fa1d2 100644 --- a/src/runs.c +++ b/src/runs.c @@ -253,40 +253,6 @@ ensureValidRun (System sys, int run) } } -//! Add a run event to the system -/** - *@param sys A system structure. - *@param run The run identifier. - *@param type The type of event. - *@param label The event label. - *@param from The sender. - *@param to The recipient. - *@param msg The message. - *\sa READ,SEND,CLAIM - */ -void -runAdd (System sys, int run, int type, Term label, Term from, Term to, - Term msg) -{ - Roledef newEvent; - Roledef scan; - - newEvent = roledefInit (type, label, from, to, msg); - ensureValidRun (sys, run); - if (runPointerGet (sys, run) == NULL) - { - sys->runs[run].start = newEvent; - runPointerSet (sys, run, newEvent); - } - else - { - scan = runPointerGet (sys, run); - while (scan->next != NULL) - scan = scan->next; - scan->next = newEvent; - } -} - //! Print a role event list. void roledefPrint (Roledef rd) @@ -543,7 +509,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role, { Roledef rdnew; - rdnew = roledefInit (READ, NULL, NULL, NULL, extterm); + rdnew = roledefInit (READ, NULL, NULL, NULL, extterm, NULL); /* this is an internal action! */ rdnew->internal = 1; rdnew->next = rd; @@ -603,7 +569,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role, *@return A pointer to a new role event with the given parameters. */ Roledef -roledefInit (int type, Term label, Term from, Term to, Term msg) +roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl) { Roledef newEvent; @@ -616,6 +582,7 @@ roledefInit (int type, Term label, Term from, Term to, Term msg) newEvent->message = msg; newEvent->forbidden = NULL; // no forbidden stuff newEvent->knowPhase = -1; // we haven't explored any knowledge yet + newEvent->claiminfo = cl; // only for claims newEvent->next = NULL; return newEvent; } @@ -625,17 +592,17 @@ roledefInit (int type, Term label, Term from, Term to, Term msg) *\sa roledefInit() */ Roledef -roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg) +roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg, Claimlist cl) { Roledef scan; if (rd == NULL) - return roledefInit (type, label, from, to, msg); + return roledefInit (type, label, from, to, msg, cl); scan = rd; while (scan->next != NULL) scan = scan->next; - scan->next = roledefInit (type, label, from, to, msg); + scan->next = roledefInit (type, label, from, to, msg, cl); return rd; } diff --git a/src/runs.h b/src/runs.h index ea7a489..93e3cfe 100644 --- a/src/runs.h +++ b/src/runs.h @@ -14,6 +14,28 @@ #define runPointerGet(sys,run) sys->runs[run].index #define runPointerSet(sys,run,newp) sys->runs[run].index = newp +//! The container for the claim info list +struct claimlist +{ + //! The term element for this node. + Term label; + //! The name of the role in which it occurs. + Term rolename; + //! Number of occurrences in system exploration. + int count; + //! Number of occurrences that failed. + int failed; + int r; //!< role number for mapping + int ev; //!< event index in role + //! Preceding label list + Termlist prec; + //! Next node pointer or NULL for the last element of the function. + struct claimlist *next; +}; + +//! Shorthand for claimlist pointers. +typedef struct claimlist *Claimlist; + //! Structure for a role event node or list. /** *\sa role @@ -42,11 +64,20 @@ struct roledef //! Pointer to next roledef node. struct roledef *next; + /* + * Substructure for reads + */ //! Illegal injections for this event. Knowledge forbidden; //! knowledge transitions counter. int knowPhase; + /* + * Substructure for claims + */ + //! Pointer to claim type info + Claimlist claiminfo; + /* evt runid for synchronisation, but that is implied in the base array */ }; @@ -155,28 +186,6 @@ struct tracebuf Varbuf variables; }; -//! The container for the claim info list -struct claimlist -{ - //! The term element for this node. - Term label; - //! The name of the role in which it occurs. - Term rolename; - //! Number of occurrences in system exploration. - int count; - //! Number of occurrences that failed. - int failed; - int r; //!< role number for mapping - int ev; //!< event index in role - //! Preceding label list - Termlist prec; - //! Next node pointer or NULL for the last element of the function. - struct claimlist *next; -}; - -//! Shorthand for claimlist pointers. -typedef struct claimlist *Claimlist; - //! The main state structure. struct system { @@ -259,8 +268,6 @@ void statesPrintShort (System sys); void systemDestroy (System sys); void systemDone (System sys); void ensureValidRun (System sys, int run); -void runAdd (System sys, int run, int type, Term label, Term from, Term to, - Term msg); void roledefPrint (Roledef rd); void runPrint (Roledef rd); void runsPrint (System sys); @@ -272,9 +279,8 @@ void roledefDelete (Roledef rd); void roledefDestroy (Roledef rd); void roleInstance (const System sys, const Protocol protocol, const Role role, const Termlist tolist); -Roledef roledefInit (int type, Term label, Term from, Term to, Term msg); -Roledef roledefAdd (Roledef rd, int type, Term label, Term from, Term to, - Term msg); +Roledef roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl); +Roledef roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg, Claimlist cl); void systemStart (System sys); void indentActivate (); void indentSet (int i);