diff --git a/src/arachne.c b/src/arachne.c index 9cca093..672b386 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -310,23 +310,31 @@ bind_existing_to_goal (const Goal goal, const int index, const int run, { Roledef rd; int flag; + int old_length; int subterm_iterate (Termlist substlist, Termlist keylist) { int keycount; int flag; - int old_length; - old_length = sys->runs[run].length; - if (index >= old_length) - sys->runs[run].length = index + 1; +#ifdef DEBUG + if (DEBUGL (5)) + { + indentPrint (); + eprintf ("Adding key list : "); + termlistPrint (keylist); + eprintf ("\n"); + } +#endif flag = 1; keycount = 0; while (flag && keylist != NULL) { - create_intruder_goal (keylist->term); - if (!binding_add (sys->maxruns - 1, 0, goal.run, goal.index)) + int keyrun; + + keyrun = create_intruder_goal (keylist->term); + if (!binding_add (keyrun, 0, goal.run, goal.index)) flag = 0; keylist = keylist->next; keycount++; @@ -334,11 +342,11 @@ bind_existing_to_goal (const Goal goal, const int index, const int run, flag = flag && iterate (); while (keycount > 0) { - roleInstanceDestroy (sys); binding_remove_last (); + roleInstanceDestroy (sys); keycount--; } - sys->runs[run].length = old_length; + termlistDestroy (keylist); return flag; } @@ -347,9 +355,15 @@ bind_existing_to_goal (const Goal goal, const int index, const int run, iterate (); } + //---------------------------- // Roledef entry rd = roledef_shift (sys->runs[run].start, index); + // Fix length + old_length = sys->runs[run].length; + if ((index + 1) > old_length) + sys->runs[run].length = index + 1; + #ifdef DEBUG if (DEBUGL (3)) { @@ -363,12 +377,12 @@ bind_existing_to_goal (const Goal goal, const int index, const int run, { if (subterm) { - return termMguSubTerm (goal.rd->message, rd->message, + flag = termMguSubTerm (goal.rd->message, rd->message, subterm_iterate, sys->know->inverses, NULL); } else { - return termMguInTerm (goal.rd->message, rd->message, + flag = termMguInTerm (goal.rd->message, rd->message, interm_iterate); } } @@ -381,8 +395,11 @@ bind_existing_to_goal (const Goal goal, const int index, const int run, eprintf ("Aborted binding existing run because of cycle.\n"); } #endif - return 1; } + binding_remove_last (); + // Reset length + sys->runs[run].length = old_length; + return flag; } //! Bind a goal to an existing regular run, if possible @@ -402,13 +419,16 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r, termPrint (p->nameterm); eprintf (", "); termPrint (r->nameterm); - eprintf ("\n"); + eprintf (" (%i)\n", subterm); } #endif flag = 1; for (run = 0; run < sys->maxruns; run++) { - flag = flag && bind_existing_to_goal (goal, index, run, subterm); + if (sys->runs[run].protocol == p && sys->runs[run].role == r) + { + flag = flag && bind_existing_to_goal (goal, index, run, subterm); + } } return flag; } @@ -421,8 +441,22 @@ bind_new_run (const Goal goal, const Protocol p, const Role r, int run; int flag; +#ifdef DEBUG + if (DEBUGL (4)) + { + indentPrint (); + eprintf ("Trying to bind "); + termPrint (goal.rd->message); + eprintf (" to a new instance of "); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf (" (%i)\n", subterm); + } +#endif roleInstance (sys, p, r, NULL, NULL); - flag = bind_existing_to_goal (goal, index, sys->maxruns - 1, subterm); + run = sys->maxruns - 1; + flag = bind_existing_to_goal (goal, index, run, subterm); roleInstanceDestroy (sys); return flag; } @@ -547,8 +581,6 @@ bind_goal_regular (const Goal goal) */ int bind_this_role_send (Protocol p, Role r, Roledef rd, int index) { - int cannotUnify; - int test_unification (Termlist substlist) { // A unification exists; return the signal @@ -576,12 +608,8 @@ bind_goal_regular (const Goal goal) eprintf (", index %i\n", index); } #endif - cannotUnify = - termMguInTerm (goal.rd->message, rd->message, test_unification); - if (!cannotUnify) + if (!termMguInTerm (goal.rd->message, rd->message, test_unification)) { - int flag; - // A good candidate #ifdef DEBUG if (DEBUGL (5)) @@ -594,9 +622,8 @@ bind_goal_regular (const Goal goal) eprintf (", index %i\n", index); } #endif - flag = flag && bind_new_run (goal, p, r, index, 0); - flag = flag && bind_existing_run (goal, p, r, index, 0); - return flag; + return (bind_new_run (goal, p, r, index, 0) && + bind_existing_run (goal, p, r, index, 0)); } else { @@ -657,14 +684,11 @@ bind_intruder_to_regular (Goal goal) } else { - int flag; - /** * Either from an existing, or from a new run. */ - flag = flag && bind_new_run (goal, p, r, index, 1); - flag = flag && bind_existing_run (goal, p, r, index, 1); - return flag; + return (bind_new_run (goal, p, r, index, 1) + && bind_existing_run (goal, p, r, index, 1)); } } } @@ -784,7 +808,7 @@ prune () { Termlist tl; - if (indentDepth > 30) + if (indentDepth > 20) { // Hardcoded limit on iterations #ifdef DEBUG @@ -796,7 +820,7 @@ prune () #endif return 1; } - if (sys->maxruns > 10) + if (sys->maxruns > 4) { // Hardcoded limit on runs #ifdef DEBUG diff --git a/src/binding.c b/src/binding.c index 8785f33..7d92fd9 100644 --- a/src/binding.c +++ b/src/binding.c @@ -142,7 +142,17 @@ graph_nodes (const int nodes, const int run1, const int ev1, const int run2, int node2; node1 = node_number (run1, ev1); +#ifdef DEBUG + if (node1 < 0 || node1 >= nodes) + error ("node_number %i out of scope %i for %i,%i.", node1, nodes, run1, + ev1); +#endif node2 = node_number (run2, ev2); +#ifdef DEBUG + if (node2 < 0 || node2 >= nodes) + error ("node_number %i out of scope %i for %i,%i.", node2, nodes, run2, + ev2); +#endif return graph_index (nodes, node1, node2); } @@ -160,7 +170,7 @@ closure_graph (Binding b) // Setup graph nodes = node_count (); - graph = memAlloc (nodes * nodes * sizeof (int)); + graph = memAlloc ((nodes * nodes) * sizeof (int)); graph_fill (graph, nodes, 0); b->nodes = nodes; b->graph = graph; @@ -185,6 +195,12 @@ closure_graph (Binding b) Binding b; b = (Binding) bl->data; +#ifdef DEBUG + if (graph_nodes (nodes, b->run_from, b->ev_from, b->run_to, b->ev_to) >= + (nodes * nodes)) + error ("Node out of scope for %i,%i -> %i,%i.\n", b->run_from, + b->ev_from, b->run_to, b->ev_to); +#endif graph[graph_nodes (nodes, b->run_from, b->ev_from, b->run_to, b->ev_to)] = 1; bl = bl->next; @@ -213,21 +229,37 @@ int binding_add (int run_from, int ev_from, int run_to, int ev_to) { Binding b; + int flag; - b = binding_create (run_from, ev_from, run_to, ev_to); #ifdef DEBUG if (DEBUGL (5)) { eprintf ("Adding binding (%i,%i) --->> (%i,%i)\n", run_from, ev_from, run_to, ev_to); } + if (ev_from >= sys->runs[run_from].step) + error ("run_from event index too large for scenario."); + if (ev_to >= sys->runs[run_to].step) + error ("run_to event index too large for scenario."); + if (run_from < 0 || run_from >= sys->maxruns) + error ("run_from out of scope."); + if (run_to < 0 || run_to >= sys->maxruns) + error ("run_to out of scope."); #endif + b = binding_create (run_from, ev_from, run_to, ev_to); sys->bindings = list_insert (sys->bindings, b); /* * Compute closure graph etc. */ - return closure_graph (b); + flag = closure_graph (b); +#ifdef DEBUG + if (DEBUGL (5)) + { + eprintf ("Adding binding result %i\n", flag); + } +#endif + return flag; } //! Remove last additions, including last manual addition diff --git a/src/warshall.c b/src/warshall.c index 0f16838..3bf6ca1 100644 --- a/src/warshall.c +++ b/src/warshall.c @@ -8,11 +8,11 @@ graph_fill (int *graph, int nodes, int value) { int node; - node = (nodes * nodes); - while (node > 0) + node = 0; + while (node < (nodes * nodes)) { - node--; graph[node] = value; + node++; } }