- Added debug code for dot output.
- Push/pop goals are counted now, making the child parameter obsolete.
This commit is contained in:
ccremers
parent
4b10c7f151
commit
94b3ac7c96
@ -67,6 +67,7 @@ typedef struct goalstruct Goal;
|
||||
*/
|
||||
|
||||
int iterate ();
|
||||
void printSemiState ();
|
||||
|
||||
/**
|
||||
* Program code
|
||||
@ -148,15 +149,25 @@ arachneDone ()
|
||||
void
|
||||
indentPrint ()
|
||||
{
|
||||
int i;
|
||||
|
||||
for (i = 0; i < indentDepth; i++)
|
||||
if (sys->output == ATTACK && globalError == 0)
|
||||
{
|
||||
if (i % 3 == 0)
|
||||
eprintf ("|");
|
||||
else
|
||||
eprintf (" ");
|
||||
eprintf (" ");
|
||||
// Arachne, attack, not an error
|
||||
// We assume that means DOT output
|
||||
eprintf ("// ");
|
||||
}
|
||||
else
|
||||
{
|
||||
// If it is not to stdout, or it is not an attack...
|
||||
int i;
|
||||
|
||||
for (i = 0; i < indentDepth; i++)
|
||||
{
|
||||
if (i % 3 == 0)
|
||||
eprintf ("|");
|
||||
else
|
||||
eprintf (" ");
|
||||
eprintf (" ");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -265,8 +276,7 @@ add_read_goals (const int run, const int old, const int new)
|
||||
}
|
||||
termPrint (rd->message);
|
||||
}
|
||||
goal_add (rd->message, run, i, 0);
|
||||
count++;
|
||||
count = count + goal_add (rd->message, run, i, 0);
|
||||
}
|
||||
rd = rd->next;
|
||||
i++;
|
||||
@ -278,17 +288,6 @@ add_read_goals (const int run, const int old, const int new)
|
||||
return count;
|
||||
}
|
||||
|
||||
//! Remove n goals
|
||||
void
|
||||
remove_read_goals (int n)
|
||||
{
|
||||
while (n > 0)
|
||||
{
|
||||
goal_remove_last ();
|
||||
n--;
|
||||
}
|
||||
}
|
||||
|
||||
//! Determine the run that follows from a substitution.
|
||||
/**
|
||||
* After an Arachne unification, stuff might go wrong w.r.t. nonce instantiation.
|
||||
@ -529,7 +528,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
|
||||
*/
|
||||
if (goal_bind (b, run, index))
|
||||
{
|
||||
int keycount;
|
||||
int newgoals;
|
||||
Termlist tl;
|
||||
|
||||
proof_suppose_binding (b);
|
||||
@ -541,7 +540,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
|
||||
termlistPrint (keylist);
|
||||
eprintf ("\n");
|
||||
}
|
||||
keycount = 0;
|
||||
newgoals = 0;
|
||||
tl = keylist;
|
||||
while (tl != NULL)
|
||||
{
|
||||
@ -561,20 +560,15 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
|
||||
}
|
||||
}
|
||||
/* add the key as a goal */
|
||||
goal_add (tl->term, b->run_to, b->ev_to, prioritylevel);
|
||||
newgoals = newgoals + goal_add (tl->term, b->run_to, b->ev_to, prioritylevel);
|
||||
tl = tl->next;
|
||||
keycount++;
|
||||
}
|
||||
|
||||
indentDepth++;
|
||||
flag = flag && iterate ();
|
||||
indentDepth--;
|
||||
|
||||
while (keycount > 0)
|
||||
{
|
||||
goal_remove_last ();
|
||||
keycount--;
|
||||
}
|
||||
goal_remove_last (newgoals);
|
||||
}
|
||||
else
|
||||
{
|
||||
@ -609,7 +603,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
|
||||
run, index);
|
||||
}
|
||||
// Reset length
|
||||
remove_read_goals (newgoals);
|
||||
goal_remove_last (newgoals);
|
||||
sys->runs[run].length = old_length;
|
||||
return flag;
|
||||
}
|
||||
@ -675,7 +669,7 @@ bind_new_run (const Binding b, const Protocol p, const Role r,
|
||||
indentDepth++;
|
||||
flag = bind_existing_to_goal (b, run, index);
|
||||
indentDepth--;
|
||||
remove_read_goals (newgoals);
|
||||
goal_remove_last (newgoals);
|
||||
semiRunDestroy ();
|
||||
return flag;
|
||||
}
|
||||
@ -719,6 +713,15 @@ dotSemiState ()
|
||||
termPrint (current_claim->type);
|
||||
eprintf ("\";\n");
|
||||
|
||||
// Needed for the bindings later on: create graph
|
||||
goal_graph_create (); // create graph
|
||||
warshall (graph, nodes); // determine closure
|
||||
|
||||
#ifdef DEBUG
|
||||
// For debugging purposes, we also display an ASCII version of some stuff in the comments
|
||||
printSemiState ();
|
||||
#endif
|
||||
|
||||
// Draw graph
|
||||
// First, all simple runs
|
||||
run = 0;
|
||||
@ -838,8 +841,6 @@ dotSemiState ()
|
||||
|
||||
// Second, all bindings.
|
||||
// We now determine them ourselves between existing runs
|
||||
goal_graph_create (); // create graph
|
||||
warshall (graph, nodes); // determine closure
|
||||
run = 0;
|
||||
while (run < sys->maxruns)
|
||||
{
|
||||
@ -1227,7 +1228,7 @@ bind_goal_new_encrypt (const Binding b)
|
||||
}
|
||||
goal_unbind (b);
|
||||
indentDepth--;
|
||||
remove_read_goals (newgoals);
|
||||
goal_remove_last (newgoals);
|
||||
semiRunDestroy ();
|
||||
}
|
||||
}
|
||||
@ -2017,7 +2018,7 @@ arachne ()
|
||||
//! Destroy
|
||||
while (sys->bindings != NULL)
|
||||
{
|
||||
remove_read_goals (1);
|
||||
goal_remove_last (1);
|
||||
}
|
||||
while (sys->maxruns > 0)
|
||||
{
|
||||
|
||||
@ -379,9 +379,12 @@ binding_print (const Binding b)
|
||||
* The int parameter 'level' is just to store additional info. Here, it stores priorities for a goal.
|
||||
* Higher level goals will be selected first. Typically, a normal goal is level 0, a key is 1.
|
||||
*/
|
||||
void
|
||||
int
|
||||
goal_add (Term term, const int run, const int ev, const int level)
|
||||
{
|
||||
int sum;
|
||||
|
||||
sum = 0;
|
||||
term = deVar (term);
|
||||
#ifdef DEBUG
|
||||
if (term == NULL)
|
||||
@ -403,7 +406,7 @@ goal_add (Term term, const int run, const int ev, const int level)
|
||||
i = 0;
|
||||
while (i < width)
|
||||
{
|
||||
goal_add (tupleProject (term, i), run, ev, level);
|
||||
sum = sum + goal_add (tupleProject (term, i), run, ev, level);
|
||||
if (i > 0)
|
||||
{
|
||||
Binding b;
|
||||
@ -416,28 +419,52 @@ goal_add (Term term, const int run, const int ev, const int level)
|
||||
}
|
||||
else
|
||||
{
|
||||
Binding b;
|
||||
// Determine whether we already had it
|
||||
int nope;
|
||||
|
||||
b = binding_create (term, run, ev);
|
||||
b->level = level;
|
||||
sys->bindings = list_insert (sys->bindings, b);
|
||||
int testSame (void *data)
|
||||
{
|
||||
Binding b;
|
||||
|
||||
b = (Binding) data;
|
||||
if (isTermEqual (b->term, term) &&
|
||||
run == b->run_to &&
|
||||
ev == b->ev_to)
|
||||
{ // abort scan, report
|
||||
return 0;
|
||||
}
|
||||
else
|
||||
{ // proceed with scan
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
nope = list_iterate (sys->bindings, testSame);
|
||||
if (nope)
|
||||
{
|
||||
// Add a new binding
|
||||
Binding b;
|
||||
b = binding_create (term, run, ev);
|
||||
b->level = level;
|
||||
sys->bindings = list_insert (sys->bindings, b);
|
||||
sum = sum + 1;
|
||||
}
|
||||
}
|
||||
return sum;
|
||||
}
|
||||
|
||||
//! Remove a goal
|
||||
void
|
||||
goal_remove_last ()
|
||||
goal_remove_last (int n)
|
||||
{
|
||||
Binding b;
|
||||
int child;
|
||||
|
||||
child = 1;
|
||||
while (child && (sys->bindings != NULL))
|
||||
while (n > 0 && (sys->bindings != NULL))
|
||||
{
|
||||
Binding b;
|
||||
|
||||
b = (Binding) sys->bindings->data;
|
||||
child = b->child;
|
||||
binding_destroy (b);
|
||||
sys->bindings = list_delete (sys->bindings);
|
||||
n--;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@ -41,8 +41,8 @@ void goal_graph_create ();
|
||||
|
||||
int binding_print (Binding b);
|
||||
|
||||
void goal_add (Term term, const int run, const int ev, const int level);
|
||||
void goal_remove_last ();
|
||||
int goal_add (Term term, const int run, const int ev, const int level);
|
||||
void goal_remove_last (int n);
|
||||
int goal_bind (const Binding b, const int run, const int ev);
|
||||
void goal_unbind (const Binding b);
|
||||
int labels_ordered (Termmap runs, Termlist labels);
|
||||
|
||||
Loading…
Reference in New Issue
Block a user