scyther/src/binding.c

465 lines
8.9 KiB
C
Raw Normal View History

2004-08-15 12:55:22 +01:00
/**
* Handle bindings for Arache engine.
*/
#include "list.h"
2004-08-18 20:43:58 +01:00
#include "role.h"
#include "label.h"
2004-08-15 12:55:22 +01:00
#include "system.h"
#include "binding.h"
2004-08-15 15:57:50 +01:00
#include "warshall.h"
2004-08-15 12:55:22 +01:00
#include "memory.h"
2004-08-15 17:08:53 +01:00
#include "debug.h"
2004-08-17 12:03:18 +01:00
#include "term.h"
#include "termmap.h"
2004-08-15 12:55:22 +01:00
static System sys;
static int *graph;
2004-08-17 16:52:52 +01:00
static int nodes;
2004-08-15 12:55:22 +01:00
2004-08-18 20:43:58 +01:00
extern Protocol INTRUDER; // The intruder protocol
extern Role I_M; // special role; precedes all other events always
2004-08-15 12:55:22 +01:00
/*
*
* Assist stuff
*
*/
//! Create mem for binding
Binding
2004-08-17 16:52:52 +01:00
binding_create (Term term, int run_to, int ev_to)
2004-08-15 12:55:22 +01:00
{
Binding b;
b = memAlloc (sizeof (struct binding));
2004-08-17 16:52:52 +01:00
b->done = 0;
b->child = 0;
b->run_from = -1;
b->ev_from = -1;
2004-08-15 12:55:22 +01:00
b->run_to = run_to;
b->ev_to = ev_to;
2004-08-17 16:52:52 +01:00
graph = NULL;
nodes = 0;
2004-08-17 12:03:18 +01:00
b->term = term;
b->level = 0;
2004-08-15 12:55:22 +01:00
return b;
}
//! Remove mem for binding
void
binding_destroy (Binding b)
{
2004-08-17 16:52:52 +01:00
if (b->done)
{
goal_unbind (b);
}
2004-08-15 12:55:22 +01:00
memFree (b, sizeof (struct binding));
}
/*
*
* Main
*
*/
//! Init module
void
bindingInit (const System mysys)
{
sys = mysys;
sys->bindings = NULL;
}
//! Close up
void
bindingDone ()
{
int delete (Binding b)
{
binding_destroy (b);
return 1;
}
list_iterate (sys->bindings, delete);
list_destroy (sys->bindings);
}
//! Destroy graph
void
goal_graph_destroy ()
{
if (graph != NULL)
{
memFree (graph, (nodes * nodes) * sizeof (int));
graph = NULL;
}
}
2004-08-17 16:52:52 +01:00
//! Compute unclosed graph
void
goal_graph_create ()
2004-08-17 16:52:52 +01:00
{
int run, ev;
2004-08-18 20:43:58 +01:00
int last_m;
2004-08-17 16:52:52 +01:00
List bl;
goal_graph_destroy ();
2004-08-17 16:52:52 +01:00
// Setup graph
nodes = node_count ();
graph = memAlloc ((nodes * nodes) * sizeof (int));
graph_fill (graph, nodes, 0);
// Setup run order
run = 0;
2004-08-18 20:43:58 +01:00
last_m = -1; // last I_M run
2004-08-17 16:52:52 +01:00
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++;
}
2004-08-18 20:43:58 +01:00
// Enforce I_M ordering
if (sys->runs[run].protocol == INTRUDER && sys->runs[run].role == I_M)
{
if (last_m != -1)
{
graph[graph_nodes (nodes, last_m, 0, run, 0)] = 1;
}
last_m = run;
}
// Next
2004-08-17 16:52:52 +01:00
run++;
}
// Setup bindings order
bl = sys->bindings;
while (bl != NULL)
{
Binding b;
b = (Binding) bl->data;
if (b->done)
{
2004-08-17 16:52:52 +01:00
#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);
2004-08-17 16:52:52 +01:00
#endif
graph[graph_nodes
(nodes, b->run_from, b->ev_from, b->run_to, b->ev_to)] = 1;
}
2004-08-17 16:52:52 +01:00
bl = bl->next;
}
}
2004-08-15 12:55:22 +01:00
/**
*
* 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)
{
2004-08-15 15:57:50 +01:00
run--;
//!@todo This now reference to step, but we intend "length" as in Arachne.
node = node + sys->runs[run].step;
}
return node;
}
//! Yield graph index, given node1, node2 numbers
__inline__ int
2004-08-17 16:52:52 +01:00
graph_index (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);
#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
2004-08-17 16:52:52 +01:00
return graph_index (node1, node2);
}
2004-08-17 16:52:52 +01:00
//! Print a binding (given a binding list pointer)
int
binding_print (const Binding b)
{
if (b->done)
eprintf ("Binding (%i,%i) --( ", b->run_from, b->ev_from);
else
eprintf ("Unbound --( ");
termPrint (b->term);
eprintf (" )->> (%i,%i)", b->run_to, b->ev_to);
2004-08-17 16:52:52 +01:00
return 1;
}
2004-08-17 16:52:52 +01:00
//! Add a goal
/**
* 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.
*/
2004-08-17 16:52:52 +01:00
void
goal_add (Term term, const int run, const int ev, const int level)
2004-08-17 16:52:52 +01:00
{
term = deVar (term);
#ifdef DEBUG
if (term == NULL)
2004-08-18 20:43:58 +01:00
error ("Trying to add an emtpy goal term");
if (run >= sys->maxruns)
2004-08-18 20:43:58 +01:00
error ("Trying to add a goal for a run that does not exist.");
if (ev >= sys->runs[run].step)
2004-08-18 20:43:58 +01:00
error
("Trying to add a goal for an event that is not in the semistate yet.");
#endif
2004-08-17 16:52:52 +01:00
if (realTermTuple (term))
{
2004-08-17 16:52:52 +01:00
int width;
int flag;
int i;
flag = 1;
width = tupleCount (term);
i = 0;
while (i < width)
{
goal_add (tupleProject (term, i), run, ev, level);
2004-08-17 16:52:52 +01:00
if (i > 0)
{
Binding b;
b = (Binding) sys->bindings->data;
b->child = 1;
}
i++;
}
}
2004-08-17 16:52:52 +01:00
else
{
Binding b;
2004-08-17 16:52:52 +01:00
b = binding_create (term, run, ev);
b->level = level;
2004-08-17 16:52:52 +01:00
sys->bindings = list_insert (sys->bindings, b);
}
}
2004-08-17 16:52:52 +01:00
//! Remove a goal
void
goal_remove_last ()
{
Binding b;
2004-08-17 16:52:52 +01:00
int child;
2004-08-17 16:52:52 +01:00
child = 1;
while (child && (sys->bindings != NULL))
{
b = (Binding) sys->bindings->data;
child = b->child;
binding_destroy (b);
sys->bindings = list_delete (sys->bindings);
}
}
2004-08-17 16:52:52 +01:00
//! Bind a goal (0 if it must be pruned)
2004-08-15 12:55:22 +01:00
int
2004-08-17 16:52:52 +01:00
goal_bind (const Binding b, const int run, const int ev)
2004-08-15 12:55:22 +01:00
{
2004-08-17 16:52:52 +01:00
if (!b->done)
2004-08-15 17:08:53 +01:00
{
#ifdef DEBUG
if (run >= sys->maxruns || sys->runs[run].step <= ev)
error ("Trying to bind to something not yet in the semistate.");
#endif
2004-08-17 16:52:52 +01:00
b->done = 1;
b->run_from = run;
b->ev_from = ev;
goal_graph_create (b);
return warshall (graph, nodes);
2004-08-15 17:08:53 +01:00
}
2004-08-17 16:52:52 +01:00
else
{
error ("Trying to bind a bound goal again.");
}
}
2004-08-17 16:52:52 +01:00
//! Unbind a goal
void
goal_unbind (const Binding b)
{
if (b->done)
{
2004-08-17 16:52:52 +01:00
goal_graph_destroy (b);
b->done = 0;
}
else
{
error ("Trying to unbind an unbound goal again.");
}
2004-08-15 12:55:22 +01:00
}
//! Determine whether some label set is ordered w.r.t. send/read order.
/**
* Assumes all these labels exist in the system, within length etc, and that the run mappings are valid.
*/
int
labels_ordered (Termmap runs, Termlist labels)
{
goal_graph_create ();
while (labels != NULL)
{
// Given this label, and the mapping of runs, we want to know if the order is okay. Thus, we need to know sendrole and readrole
Labelinfo linfo;
int send_run, send_ev, read_run, read_ev;
int get_index (const int run)
{
Roledef rd;
int i;
i = 0;
rd = sys->runs[run].start;
while (rd != NULL && !isTermEqual (rd->label, labels->term))
{
rd = rd->next;
i++;
}
#ifdef DEBUG
if (rd == NULL)
error
("Could not locate send or read for label, after niagree holds, to test for order.");
#endif
return i;
}
linfo = label_find (sys->labellist, labels->term);
send_run = termmapGet (runs, linfo->sendrole);
read_run = termmapGet (runs, linfo->readrole);
send_ev = get_index (send_run);
read_ev = get_index (read_run);
if (graph[graph_nodes (nodes, send_run, send_ev, read_run, read_ev)] ==
0)
{
// Not ordered; false
return 0;
}
// Proceed
labels = labels->next;
}
return 1;
}
2004-08-17 16:52:52 +01:00
//! Prune invalid state w.r.t. <=C minimal requirement
2004-08-15 12:55:22 +01:00
/**
2004-08-17 16:52:52 +01:00
* Intuition says this can be done a lot more efficient. Luckily this is the prototype.
*
*@returns True, if it's okay. If false, it needs to be pruned.
2004-08-15 12:55:22 +01:00
*/
int
bindings_c_minimal ()
2004-08-15 12:55:22 +01:00
{
2004-08-17 16:52:52 +01:00
List bl;
2004-08-15 12:55:22 +01:00
2004-08-17 16:52:52 +01:00
// Ensure a state graph
if (graph == NULL)
{
goal_graph_create ();
// Recompute closure; does that work?
if (!warshall (graph, nodes))
{
// Hmm, cycle
error ("Detected a cycle when testing for c-minimality");
}
}
2004-08-17 16:52:52 +01:00
// For all goals
bl = sys->bindings;
while (bl != NULL)
{
2004-08-17 16:52:52 +01:00
Binding b;
b = (Binding) bl->data;
if (b->done)
2004-08-17 16:52:52 +01:00
{
int run;
int node_from;
2004-08-17 16:52:52 +01:00
node_from = node_number (b->run_from, b->ev_from);
// Find all preceding events
for (run = 0; run < sys->maxruns; run++)
2004-08-17 16:52:52 +01:00
{
int ev;
2004-08-17 16:52:52 +01:00
//!@todo hardcoded reference to step, should be length
for (ev = 0; ev < sys->runs[run].step; ev++)
2004-08-17 16:52:52 +01:00
{
int node_comp;
2004-08-17 16:52:52 +01:00
node_comp = node_number (run, ev);
if (graph[graph_index (node_comp, node_from)] > 0)
2004-08-17 16:52:52 +01:00
{
// this node is *before* the from node
Roledef rd;
rd = roledef_shift (sys->runs[run].start, ev);
if (termInTerm (rd->message, b->term))
{
// This term already occurs as interm in a previous node!
return 0;
}
2004-08-17 16:52:52 +01:00
}
}
}
}
bl = bl->next;
}
2004-08-17 16:52:52 +01:00
return 1;
2004-08-15 12:55:22 +01:00
}