From 2191d80885bfdf102ae87127e49e1fb722312136 Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 11 Aug 2004 14:09:12 +0000 Subject: [PATCH] - Lots of stuff starts to take shape. Nice. --- src/arachne.c | 209 +++++++++++++++++++++++++++++++++++++++++++++----- src/arachne.h | 4 +- src/main.c | 4 +- src/mgu.c | 39 ++++++---- src/mgu.h | 7 +- 5 files changed, 223 insertions(+), 40 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 1819e16..0555d31 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -7,24 +7,41 @@ */ #include "term.h" +#include "termlist.h" #include "role.h" #include "system.h" +#include "states.h" +#include "mgu.h" #include "arachne.h" -Term INTRUDER_ROLE; +static System sys; +static Protocol INTRUDER; // Pointers, to be set by the Init +static Role I_GOAL; // Same here. struct goalstruct { int run; int index; + Roledef rd; }; typedef struct goalstruct Goal; +/** + * Forward declarations + */ + +int iterate (); + +/** + * Program code + */ + //! Init Arachne engine void -arachneInit (const System sys) +arachneInit (const System mysys) { + sys = mysys; // make sys available for this module as a global /* * Add intruder protocol roles */ @@ -33,7 +50,7 @@ arachneInit (const System sys) //! Close Arachne engine void -arachneDone (const System sys) +arachneDone () { return; } @@ -47,14 +64,73 @@ arachneDone (const System sys) * call it 'length' here. */ #define INVALID -1 -#define isGoal(rd) (rd->type == READ) +#define isGoal(rd) (rd->type == READ && !rd->internal) #define isBound(rd) (rd->bind_run != INVALID) #define length step +//! Iterate but discard the info of the termlist +int +mgu_iterate (const Termlist tl) +{ + return iterate (); +} + + //------------------------------------------------------------------------ // Sub //------------------------------------------------------------------------ +//! Iterate over all send types in the roles (including the intruder ones) +/** + * Function is called with (protocol pointer, role pointer, roledef pointer, index) + * and returns an integer. If it is false, iteration aborts. + */ +int +iterate_role_sends (int (*func) ()) +{ + Protocol p; + + p = sys->protocols; + while (p != NULL) + { + Role r; + + r = p->roles; + while (r != NULL) + { + Roledef rd; + int index; + + rd = r->roledef; + index = 0; + while (rd != NULL) + { + if (rd->type == SEND) + { + int flag; + + flag = func (p, r, rd, index); + if (!flag) + return 0; + } + index++; + rd = rd->next; + } + r = r->next; + } + p = p->next; + } + return 1; +} + +//! Generates a new intruder goal, yields runid +int +add_intruder_goal (Term t) +{ + roleInstance (sys, INTRUDER, I_GOAL, NULL); + return (sys->maxruns - 1); +} + //------------------------------------------------------------------------ // Larger logical componentents //------------------------------------------------------------------------ @@ -64,19 +140,20 @@ arachneDone (const System sys) * Should be ordered to prefer most constrained; for now, it is simply the first one encountered. */ Goal -select_goal (const System sys) +select_goal () { Goal goal; int run; goal.run = INVALID; + goal.rd = NULL; for (run = 0; run < sys->maxruns; run++) { Roledef rd; int index; index = 0; - rd = runPointerGet (sys, run); + rd = sys->runs[run].start; while (rd != NULL && index < sys->runs[run].length) { if (isGoal (rd) && !isBound (rd)) @@ -84,6 +161,7 @@ select_goal (const System sys) // Return this goal goal.run = run; goal.index = index; + goal.rd = rd; return goal; } index++; @@ -93,29 +171,114 @@ select_goal (const System sys) return goal; } +//! Bind a goal to an existing regular run, if possible +int +bind_existing_run (const Goal goal, const Protocol p, const Role r, + const int index) +{ + int run, flag; + + flag = 1; + for (run = 0; run < sys->maxruns; run++) + { + if (sys->runs[run].protocol == p && sys->runs[run].role == r) + { + int i; + int old_length; + Roledef rd; + + // find roledef entry + rd = sys->runs[run].start; + for (i = 0; i < index; i++) + rd = rd->next; + + // mgu and iterate + old_length = sys->runs[run].length; + if (index >= old_length) + sys->runs[run].length = index + 1; + flag = + flag & termMguInTerm (goal.rd->message, rd->message, mgu_iterate); + sys->runs[run].length = old_length; + } + } + return flag; +} + +//! Bind a goal to a new run +int +bind_new_run (const Goal goal, const Protocol p, const Role r, + const int index) +{ +} + //! Bind a regular goal int -bind_goal_regular (const System sys, const Goal goal) +bind_goal_regular (const Goal goal) { + int flag; + + /* + * This is a local function so we have access to goal + */ + int bind_this (Protocol p, Role r, Roledef rd, int index) + { + int element_f1 (Termlist substlist) + { + /** + * Two options; as this, it is from an existing run, + * or from a new one. + */ + int flag; + + termlistSubstReset (substlist); // undo, we don't really need that + flag = bind_existing_run (goal, p, r, index); + if (flag) + { + flag = bind_new_run (goal, p, r, index); + } + return flag; + } + + // Test for interm unification + return termMguInTerm (goal.rd->message, rd->message, element_f1); + } + + // Bind to all possible sends? + flag = iterate_role_sends (bind_this); + // Bind to an intruder node? + if (flag) + { + int run; + + goal.rd->bind_run = add_intruder_goal (goal.rd->message); // creates a new run + goal.rd->bind_index = 0; // such a run only has a simple read; + + flag = iterate (); + + roleInstanceDestroy (sys); // destroy the created run + goal.rd->bind_run = INVALID; + } + return flag; } //! Bind an intruder goal int -bind_goal_intruder (const System sys, const Goal goal) +bind_goal_intruder (const Goal goal) { + //!@todo Fix intruder goal stuff } //! Bind a goal in all possible ways int -bind_goal (const System sys, const Goal goal) +bind_goal (const Goal goal) { - if (isTermEqual (sys->runs[goal.run].protocol->nameterm, INTRUDER_ROLE)) + if (sys->runs[goal.run].protocol == INTRUDER) { - return bind_goal_intruder (sys, goal); + return bind_goal_intruder (goal); } else { - return bind_goal_regular (sys, goal); + return bind_goal_regular (goal); } } @@ -124,7 +287,7 @@ bind_goal (const System sys, const Goal goal) *@returns true iff this state is invalid for some reason */ int -prune (const System sys) +prune () { return 0; } @@ -135,7 +298,7 @@ prune (const System sys) //! Main recursive procedure for Arachne int -iterate (const System sys) +iterate () { Goal goal; @@ -143,14 +306,20 @@ iterate (const System sys) * Possibly prune this state */ - if (prune (sys)) + if (prune ()) return 0; /** - * If not pruned, check whether its a final state (i.e. all goals bound) + * Not pruned: count */ - goal = select_goal (sys); + sys->states = statesIncrease (sys->states); + + /** + * Check whether its a final state (i.e. all goals bound) + */ + + goal = select_goal (); if (goal.run == INVALID) { /* @@ -163,7 +332,7 @@ iterate (const System sys) /* * bind this goal in all possible ways and iterate */ - return bind_goal (sys, goal); + return bind_goal (goal); } } @@ -172,7 +341,7 @@ iterate (const System sys) * For this test, we manually set up some stuff. */ int -arachne (const System sys) +arachne () { /* * set up claim role(s) @@ -181,5 +350,5 @@ arachne (const System sys) /* * iterate */ - iterate (sys); + iterate (); } diff --git a/src/arachne.h b/src/arachne.h index 52a1c10..1d9a403 100644 --- a/src/arachne.h +++ b/src/arachne.h @@ -4,7 +4,7 @@ #include "system.h" void arachneInit (const System sys); -void arachneDone (const System sys); -int arachne (const System sys); +void arachneDone (); +int arachne (); #endif diff --git a/src/main.c b/src/main.c index 7db70cd..5f62a69 100644 --- a/src/main.c +++ b/src/main.c @@ -542,7 +542,7 @@ main (int argc, char **argv) if (sys->engine == ARACHNE_ENGINE) { - arachneInit (); + arachneInit (sys); } /* * --------------------------------------- @@ -912,7 +912,7 @@ modelCheck (const System sys) traverse (sys); break; case ARACHNE_ENGINE: - arachne (sys); + arachne (); break; default: error ("Unknown engine type %i.", sys->engine); diff --git a/src/mgu.c b/src/mgu.c index 2e83201..6004c53 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -163,49 +163,59 @@ termMguTerm (Term t1, Term t2) //! Most general interm unifiers of t1 interm t2 /** * Try to determine the most general interm unifiers of two terms. - *@returns Nothing. Iteration gets void. + *@returns Nothing. Iteration gets termlist of substitutions. */ -void -termMguInTerm (Term t1, Term t2, void (*iterator) ()) +int +termMguInTerm (Term t1, Term t2, int (*iterator) ()) { Termlist tl; + int flag; + flag = 1; t2 = deVar (t2); if (t2 != NULL && isTermTuple (t2)) { // t2 is a tuple, consider interm options as well. - termMguInTerm (t1, t2->left.op1, iterator); - termMguInTerm (t1, t2->right.op2, iterator); + flag = flag & termMguInTerm (t1, t2->left.op1, iterator); + flag = flag & termMguInTerm (t1, t2->right.op2, iterator); } // simple clause or combined tl = termMguTerm (t1, t2); if (tl != MGUFAIL) { // Iterate - iterator (); + flag = flag & iterator (tl); // Reset variables termlistSubstReset (tl); } + return flag; } //! Most general subterm unifiers of t1 subterm t2 /** * Try to determine the most general subterm unifiers of two terms. - *@returns Nothing. Iteration gets list of keys needed to decrypt. + *@returns Nothing. Iteration gets termlist of subst, and list of keys needed to decrypt. */ -void -termMguSubTerm (Term t1, Term t2, void (*iterator) (), +int +termMguSubTerm (Term t1, Term t2, int (*iterator) (), const Termlist inverses, Termlist keylist) { + int flag; Termlist tl; + + flag = 1; t2 = deVar (t2); if (t2 != NULL && !isTermLeaf (t2)) { if (isTermTuple (t2)) { // 'simple' tuple - termMguSubTerm (t1, t2->left.op1, iterator, inverses, keylist); - termMguSubTerm (t1, t2->right.op2, iterator, inverses, keylist); + flag = + flag & termMguSubTerm (t1, t2->left.op1, iterator, inverses, + keylist); + flag = + flag & termMguSubTerm (t1, t2->right.op2, iterator, inverses, + keylist); } else { @@ -219,7 +229,9 @@ termMguSubTerm (Term t1, Term t2, void (*iterator) (), keylist_new = termlistAdd (keylist_new, newkey); // Recurse - termMguSubTerm (t1, t2->left.op, iterator, inverses, keylist_new); + flag = + flag & termMguSubTerm (t1, t2->left.op, iterator, inverses, + keylist_new); termlistDelete (keylist_new); termDelete (newkey); @@ -230,8 +242,9 @@ termMguSubTerm (Term t1, Term t2, void (*iterator) (), if (tl != MGUFAIL) { // Iterate - iterator (keylist); + flag = flag & iterator (tl, keylist); // Reset variables termlistSubstReset (tl); } + return flag; } diff --git a/src/mgu.h b/src/mgu.h index 0cb636b..c9d03e5 100644 --- a/src/mgu.h +++ b/src/mgu.h @@ -15,8 +15,9 @@ #define MGUFAIL (Termlist) -1 Termlist termMguTerm (Term t1, Term t2); -void termMguInTerm (Term t1, Term t2, void (*iterator) ()); -void termMguSubTerm (Term t1, Term t2, void (*iterator) (), - const Termlist inverses, Termlist keylist); +int termMguInTerm (Term t1, Term t2, int (*iterator) ()); +int termMguSubTerm (Term t1, Term t2, int (*iterator) (), + const Termlist inverses, Termlist keylist); +void termlistSubstReset (Termlist tl); #endif