diff --git a/src/arachne.c b/src/arachne.c index 3c88c7e..2aa7515 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -17,6 +17,7 @@ #include "error.h" #include "claim.h" #include "debug.h" +#include "binding.h" extern CLAIM_Secret; extern CLAIM_Nisynch; @@ -121,7 +122,7 @@ arachneDone () */ #define INVALID -1 #define isGoal(rd) (rd->type == READ && !rd->internal) -#define isBound(rd) (rd->bind_run != INVALID) +#define isBound(rd) (rd->bound) #define length step //! Indent print @@ -132,7 +133,7 @@ indentPrint () int i; for (i = 0; i < indentDepth; i++) - eprintf ("%i ",i); + eprintf ("%i ", i); #else eprintf (">> "); #endif @@ -274,13 +275,17 @@ add_intruder_goal_iterate (Goal goal) int run; run = create_intruder_goal (goal.rd->message); - goal.rd->bind_run = run; - goal.rd->bind_index = 0; - - flag = iterate (); + if (binding_add (run, 0, goal.run, goal.index)) + { + flag = iterate (); + binding_remove_last (); + } + else + { + flag = 1; + } roleInstanceDestroy (sys); // destroy the created run - goal.rd->bind_run = INVALID; return flag; } @@ -305,7 +310,6 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r, } #endif flag = 1; - goal.rd->bind_index = index; for (run = 0; run < sys->maxruns; run++) { if (forced_run == -2 || forced_run == run) @@ -330,16 +334,17 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r, e_term1 = goal.rd->message; } #endif - goal.rd->bind_run = run; - - flag = (flag - && termMguInTerm (goal.rd->message, rd->message, - mgu_iterate)); + if (binding_add (run, index, goal.run, goal.index)) + { + flag = (flag + && termMguInTerm (goal.rd->message, rd->message, + mgu_iterate)); + binding_remove_last (); + } sys->runs[run].length = old_length; } } } - goal.rd->bind_run = -1; return flag; } @@ -354,28 +359,31 @@ bind_new_run (const Goal goal, const Protocol p, const Role r, int old_run; int old_index; + //!@todo if binding_add does not require the roleinstance to be done, move roleInstance into if of binding add (more efficient) roleInstance (sys, p, r, NULL); run = sys->maxruns - 1; sys->runs[run].length = index + 1; - old_run = goal.rd->bind_run; - old_index = goal.rd->bind_index; - goal.rd->bind_run = run; - goal.rd->bind_index = index; -#ifdef DEBUG - if (DEBUGL (3)) + if (binding_add (run, index, goal.run, goal.index)) { - explanation = "Bind new run"; - e_run = run; - e_term1 = r->nameterm; - rd = roledef_shift (sys->runs[run].start, index); - e_term2 = rd->message; - } +#ifdef DEBUG + if (DEBUGL (3)) + { + explanation = "Bind new run"; + e_run = run; + e_term1 = r->nameterm; + rd = roledef_shift (sys->runs[run].start, index); + e_term2 = rd->message; + } #endif - flag = iterate (); + flag = iterate (); - goal.rd->bind_run = old_run; - goal.rd->bind_index = old_index; + binding_remove_last (); + } + else + { + flag = 1; + } roleInstanceDestroy (sys); return flag; @@ -675,13 +683,24 @@ bind_goal_intruder (const Goal goal) int bind_goal (const Goal goal) { - if (sys->runs[goal.run].protocol == INTRUDER) + if (!goal.rd->bound) { - return bind_goal_intruder (goal); + int flag; + goal.rd->bound = 1; + if (sys->runs[goal.run].protocol == INTRUDER) + { + flag = bind_goal_intruder (goal); + } + else + { + flag = bind_goal_regular (goal); + } + goal.rd->bound = 0; + return flag; } else { - return bind_goal_regular (goal); + return 1; } } @@ -897,7 +916,7 @@ arachne () /** * Add specific goal info */ - add_claim_specifics (cl, roledef_shift(sys->runs[0].start, cl->ev)); + add_claim_specifics (cl, roledef_shift (sys->runs[0].start, cl->ev)); #ifdef DEBUG if (DEBUGL (5)) @@ -914,7 +933,7 @@ arachne () //! Destroy while (sys->maxruns > 0) { - roleInstanceDestroy (sys); + roleInstanceDestroy (sys); } // next diff --git a/src/binding.c b/src/binding.c index 46a465f..51927cd 100644 --- a/src/binding.c +++ b/src/binding.c @@ -7,6 +7,9 @@ #include "binding.h" #include "memory.h" +/* + * Idea is the ev_from *has to* precede the ev_to + */ struct binding { int run_from; @@ -112,14 +115,14 @@ binding_remove_last () manual = 0; list = sys->bindings; - while (!manual && list != NULL); - { - Binding b; + while (list != NULL && !manual) + { + Binding b; - b = (Binding) list->data; - manual = b->manual; - binding_destroy (b); - list = list_delete (list); - } + b = (Binding) list->data; + manual = b->manual; + binding_destroy (b); + list = list_delete (list); + } sys->bindings = list; } diff --git a/src/role.c b/src/role.c index b1b2952..9ceb355 100644 --- a/src/role.c +++ b/src/role.c @@ -157,8 +157,10 @@ roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl) newEvent->forbidden = NULL; // no forbidden stuff newEvent->knowPhase = -1; // we haven't explored any knowledge yet newEvent->claiminfo = cl; // only for claims - newEvent->bind_run = -1; // unbound goal - newEvent->bind_index = -1; // unbound goal + if (type == READ) + newEvent->bound = 0; // bound goal (Used for arachne only). Technically involves choose events as well. + else + newEvent->bound = 1; // other stuff does not need to be bound newEvent->next = NULL; return newEvent; } diff --git a/src/role.h b/src/role.h index 3d791b7..3a98388 100644 --- a/src/role.h +++ b/src/role.h @@ -89,8 +89,7 @@ struct roledef /* * Bindings for Arachne engine */ - int bind_run; //!< -1 for unbound - int bind_index; + int bound; /* evt runid for synchronisation, but that is implied in the base array */