diff --git a/src/arachne.c b/src/arachne.c index 2aa7515..0f04952 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -19,9 +19,9 @@ #include "debug.h" #include "binding.h" -extern CLAIM_Secret; -extern CLAIM_Nisynch; -extern CLAIM_Niagree; +extern Term CLAIM_Secret; +extern Term CLAIM_Nisynch; +extern Term CLAIM_Niagree; static System sys; Protocol INTRUDER; // Pointers, to be set by the Init @@ -278,13 +278,14 @@ add_intruder_goal_iterate (Goal goal) if (binding_add (run, 0, goal.run, goal.index)) { flag = iterate (); - binding_remove_last (); } else { + indentPrint (); + eprintf ("Aborted adding intruder goal because of cycle.\n"); flag = 1; } - + binding_remove_last (); roleInstanceDestroy (sys); // destroy the created run return flag; } @@ -339,8 +340,14 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r, flag = (flag && termMguInTerm (goal.rd->message, rd->message, mgu_iterate)); - binding_remove_last (); } + else + { + indentPrint (); + eprintf + ("Aborted binding existing run because of cycle.\n"); + } + binding_remove_last (); sys->runs[run].length = old_length; } } @@ -359,7 +366,6 @@ 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; @@ -377,14 +383,14 @@ bind_new_run (const Goal goal, const Protocol p, const Role r, #endif flag = iterate (); - - binding_remove_last (); } else { + indentPrint (); + eprintf ("Aborted binding new run because of cycle.\n"); flag = 1; } - + binding_remove_last (); roleInstanceDestroy (sys); return flag; } @@ -741,7 +747,7 @@ prune () //! Setup system for specific claim test add_claim_specifics (Claimlist cl, Roledef rd) { - if (isTermEqual (cl->type, CLAIM_Secret)) + if (cl->type == CLAIM_Secret) { /** * Secrecy claim diff --git a/src/binding.c b/src/binding.c index 51927cd..dda0683 100644 --- a/src/binding.c +++ b/src/binding.c @@ -18,7 +18,8 @@ struct binding int run_to; int ev_to; - int manual; + int *graph; + int nodes; }; typedef struct binding *Binding; @@ -42,7 +43,8 @@ binding_create (int run_from, int ev_from, int run_to, int ev_to, int manual) b->ev_from = ev_from; b->run_to = run_to; b->ev_to = ev_to; - b->manual = manual; + b->graph = NULL; + b->nodes = 0; return b; } @@ -50,6 +52,10 @@ binding_create (int run_from, int ev_from, int run_to, int ev_to, int manual) void binding_destroy (Binding b) { + if (b->graph != NULL) + { + memFree (b->graph, (b->nodes * b->nodes) * sizeof (int)); + } memFree (b, sizeof (struct binding)); } @@ -80,17 +86,116 @@ bindingDone () list_destroy (sys->bindings); } - /** * * Externally available functions * */ +//! Yield node count +int +node_count () +{ + int count; + int run; + + count = 0; + for (run = 0; run < sys->maxruns; run++) + { + //!@todo This now reference to step, but we intend "length" as in Arachne. + count = count + sys->runs[run].step; + } + return count; +} + +//! Yield node number given run, ev +__inline__ int +node_number (int run, int ev) +{ + int node; + + node = ev; + while (run > 0) + { + //!@todo This now reference to step, but we intend "length" as in Arachne. + node = node + sys->runs[run].step; + run--; + } + return node; +} + +//! Yield graph index, given node1, node2 numbers +__inline__ int +graph_index (const int nodes, const int node1, const int node2) +{ + return ((node1 * nodes) + node2); +} + +//! Yield graph index, given (node1), (node2) tuples +__inline__ int +graph_nodes (const int nodes, const int run1, const int ev1, const int run2, + const int ev2) +{ + int node1; + int node2; + + node1 = node_number (run1, ev1); + node2 = node_number (run2, ev2); + return graph_index (nodes, node1, node2); +} + +//! Compute closure graph +/** + *@returns 0 iff there is a cycle, 1 otherwise + */ +int +closure_graph (Binding b) +{ + int nodes; + int *graph; + int run, ev; + List bl; + + // Setup graph + nodes = node_count (); + graph = memAlloc (nodes * nodes * sizeof (int)); + graph_fill (graph, nodes, 0); + b->nodes = nodes; + b->graph = graph; + + // Setup run order + run = 0; + while (run < sys->maxruns) + { + ev = 1; + //!@todo This now reference to step, but we intend "length" as in Arachne. + while (ev < sys->runs[run].step) + { + graph[graph_nodes (nodes, run, ev - 1, run, ev)] = 1; + ev++; + } + run++; + } + // Setup bindings order + bl = sys->bindings; + while (bl != NULL) + { + Binding b; + + b = (Binding) bl->data; + graph[graph_nodes (nodes, b->run_from, b->ev_from, b->run_to, b->ev_to)] + = 1; + bl = bl->next; + } + + return warshall (graph, nodes); +} + + //! Add a binding /** * Note that bindings are added to the head of the list. - *@returns True iff is a valid additional binding. False if not. If false, nothing needs to be destroyed. + *@returns True iff is a valid additional binding. False if not. */ int binding_add (int run_from, int ev_from, int run_to, int ev_to) @@ -99,7 +204,11 @@ binding_add (int run_from, int ev_from, int run_to, int ev_to) b = binding_create (run_from, ev_from, run_to, ev_to, 1); sys->bindings = list_insert (sys->bindings, b); - return 1; + + /* + * Compute closure graph etc. + */ + return closure_graph (b); } //! Remove last additions, including last manual addition @@ -109,20 +218,12 @@ binding_add (int run_from, int ev_from, int run_to, int ev_to) void binding_remove_last () { - List list; - int manual; + Binding b; - manual = 0; - list = sys->bindings; - - while (list != NULL && !manual) + if (sys->bindings != NULL) { - Binding b; - - b = (Binding) list->data; - manual = b->manual; + b = (Binding) sys->bindings->data; binding_destroy (b); - list = list_delete (list); + sys->bindings = list_delete (sys->bindings); } - sys->bindings = list; } diff --git a/src/binding.h b/src/binding.h index ece4204..025f03b 100644 --- a/src/binding.h +++ b/src/binding.h @@ -4,6 +4,8 @@ void bindingInit (const System mysys); void bindingDone (); +int node_count (); +int node_number (int run, int ev); int binding_add (int run_from, int ev_from, int run_to, int ev_to); void binding_remove_last (); diff --git a/src/compiler.c b/src/compiler.c index 6bd20f6..aa8840d 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -103,9 +103,10 @@ compilerInit (const System mysys) } //! Make a global constant -Term makeGlobalConstant (const char *s) +Term +makeGlobalConstant (const char *s) { - return levelDeclare (symbolSysConst(s), 0, 0); + return levelDeclare (symbolSysConst (s), 0, 0); } //! Clean up afterwards @@ -1045,33 +1046,9 @@ compute_prec_sets (const System sys) /* * Compute transitive closure (Warshall). - * If j