- Re-indented the files.
This commit is contained in:
parent
a38925c9c2
commit
506e42f841
309
src/arachne.c
309
src/arachne.c
@ -188,7 +188,8 @@ int
|
||||
isTermFunctionName (Term t)
|
||||
{
|
||||
t = deVar (t);
|
||||
if (t != NULL && isTermLeaf(t) && t->stype != NULL && inTermlist (t->stype, TERM_Function))
|
||||
if (t != NULL && isTermLeaf (t) && t->stype != NULL
|
||||
&& inTermlist (t->stype, TERM_Function))
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
@ -200,9 +201,9 @@ getTermFunction (Term t)
|
||||
t = deVar (t);
|
||||
if (t != NULL)
|
||||
{
|
||||
if (realTermEncrypt (t) && isTermFunctionName (TermKey(t)))
|
||||
if (realTermEncrypt (t) && isTermFunctionName (TermKey (t)))
|
||||
{
|
||||
return TermKey(t);
|
||||
return TermKey (t);
|
||||
}
|
||||
}
|
||||
return NULL;
|
||||
@ -304,7 +305,7 @@ determine_unification_run (Termlist tl)
|
||||
while (tl != NULL)
|
||||
{
|
||||
//! Again, hardcoded reference to compiler.c. Level -3 means a local constant for a role.
|
||||
if (tl->term->type != VARIABLE && TermRunid(tl->term) == -3)
|
||||
if (tl->term->type != VARIABLE && TermRunid (tl->term) == -3)
|
||||
{
|
||||
Term t;
|
||||
|
||||
@ -320,12 +321,12 @@ determine_unification_run (Termlist tl)
|
||||
if (run == -2)
|
||||
{
|
||||
// Any run
|
||||
run = TermRunid(t);
|
||||
run = TermRunid (t);
|
||||
}
|
||||
else
|
||||
{
|
||||
// Specific run: compare
|
||||
if (run != TermRunid(t))
|
||||
if (run != TermRunid (t))
|
||||
{
|
||||
return -1;
|
||||
}
|
||||
@ -553,7 +554,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
|
||||
if (realTermEncrypt (tl->term))
|
||||
{
|
||||
/* the key is a construction itself */
|
||||
if (inKnowledge (sys->know, TermKey(tl->term)))
|
||||
if (inKnowledge (sys->know, TermKey (tl->term)))
|
||||
{
|
||||
/* the key is constructed by a public thing */
|
||||
/* typically, this is a public key, so we postpone it */
|
||||
@ -561,7 +562,9 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
|
||||
}
|
||||
}
|
||||
/* add the key as a goal */
|
||||
newgoals = newgoals + 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;
|
||||
}
|
||||
|
||||
@ -720,10 +723,11 @@ dotSemiState ()
|
||||
goal_graph_create (); // create graph
|
||||
if (warshall (graph, nodes) == 0) // determine closure
|
||||
{
|
||||
eprintf ("// This graph was not completely closed transitively because it contains a cycle!\n");
|
||||
eprintf
|
||||
("// This graph was not completely closed transitively because it contains a cycle!\n");
|
||||
}
|
||||
|
||||
ranks = memAlloc (nodes * sizeof(int));
|
||||
ranks = memAlloc (nodes * sizeof (int));
|
||||
maxrank = graph_ranks (graph, ranks, nodes); // determine ranks
|
||||
|
||||
#ifdef DEBUG
|
||||
@ -731,57 +735,56 @@ dotSemiState ()
|
||||
printSemiState ();
|
||||
// Even draw all dependencies for non-intruder runs
|
||||
// Real nice debugging :(
|
||||
{
|
||||
int run;
|
||||
{
|
||||
int run;
|
||||
|
||||
run = 0;
|
||||
while (run < sys->maxruns)
|
||||
{
|
||||
int ev;
|
||||
run = 0;
|
||||
while (run < sys->maxruns)
|
||||
{
|
||||
int ev;
|
||||
|
||||
ev = 0;
|
||||
while (ev < sys->runs[run].length)
|
||||
{
|
||||
int run2;
|
||||
int notfirstrun;
|
||||
ev = 0;
|
||||
while (ev < sys->runs[run].length)
|
||||
{
|
||||
int run2;
|
||||
int notfirstrun;
|
||||
|
||||
eprintf ("// precedence: r%ii%i <- ", run,ev);
|
||||
run2 = 0;
|
||||
notfirstrun = 0;
|
||||
while (run2 < sys->maxruns)
|
||||
{
|
||||
int notfirstev;
|
||||
int ev2;
|
||||
eprintf ("// precedence: r%ii%i <- ", run, ev);
|
||||
run2 = 0;
|
||||
notfirstrun = 0;
|
||||
while (run2 < sys->maxruns)
|
||||
{
|
||||
int notfirstev;
|
||||
int ev2;
|
||||
|
||||
notfirstev = 0;
|
||||
ev2 = 0;
|
||||
while (ev2 < sys->runs[run2].length)
|
||||
{
|
||||
if (graph[graph_nodes (nodes, run2, ev2, run, ev)]
|
||||
!= 0)
|
||||
{
|
||||
if (notfirstev)
|
||||
eprintf (",");
|
||||
else
|
||||
{
|
||||
if (notfirstrun)
|
||||
eprintf (" ");
|
||||
eprintf ("r%i:", run2);
|
||||
}
|
||||
eprintf ("%i", ev2);
|
||||
notfirstrun = 1;
|
||||
notfirstev = 1;
|
||||
}
|
||||
ev2++;
|
||||
}
|
||||
run2++;
|
||||
}
|
||||
eprintf ("\n");
|
||||
ev++;
|
||||
}
|
||||
run++;
|
||||
}
|
||||
}
|
||||
notfirstev = 0;
|
||||
ev2 = 0;
|
||||
while (ev2 < sys->runs[run2].length)
|
||||
{
|
||||
if (graph[graph_nodes (nodes, run2, ev2, run, ev)] != 0)
|
||||
{
|
||||
if (notfirstev)
|
||||
eprintf (",");
|
||||
else
|
||||
{
|
||||
if (notfirstrun)
|
||||
eprintf (" ");
|
||||
eprintf ("r%i:", run2);
|
||||
}
|
||||
eprintf ("%i", ev2);
|
||||
notfirstrun = 1;
|
||||
notfirstev = 1;
|
||||
}
|
||||
ev2++;
|
||||
}
|
||||
run2++;
|
||||
}
|
||||
eprintf ("\n");
|
||||
ev++;
|
||||
}
|
||||
run++;
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
// Draw graph
|
||||
@ -799,22 +802,22 @@ dotSemiState ()
|
||||
// Regular run
|
||||
|
||||
/* DISABLED subgraphs
|
||||
eprintf ("\tsubgraph cluster_run%i {\n", run);
|
||||
eprintf ("\t\tlabel = \"");
|
||||
eprintf ("#%i: ", run);
|
||||
termPrint (sys->runs[run].protocol->nameterm);
|
||||
eprintf (", ");
|
||||
agentsOfRunPrint (sys, run);
|
||||
eprintf ("\";\n", run);
|
||||
if (run == 0)
|
||||
{
|
||||
eprintf ("\t\tcolor = red;\n");
|
||||
}
|
||||
else
|
||||
{
|
||||
eprintf ("\t\tcolor = blue;\n");
|
||||
}
|
||||
*/
|
||||
eprintf ("\tsubgraph cluster_run%i {\n", run);
|
||||
eprintf ("\t\tlabel = \"");
|
||||
eprintf ("#%i: ", run);
|
||||
termPrint (sys->runs[run].protocol->nameterm);
|
||||
eprintf (", ");
|
||||
agentsOfRunPrint (sys, run);
|
||||
eprintf ("\";\n", run);
|
||||
if (run == 0)
|
||||
{
|
||||
eprintf ("\t\tcolor = red;\n");
|
||||
}
|
||||
else
|
||||
{
|
||||
eprintf ("\t\tcolor = blue;\n");
|
||||
}
|
||||
*/
|
||||
|
||||
|
||||
// Display the respective events
|
||||
@ -883,7 +886,7 @@ dotSemiState ()
|
||||
}
|
||||
// Draw the first box
|
||||
// This used to be drawn only if done && send_before_read, now we always draw it.
|
||||
eprintf ("\t\ts%i [label=\"Run %i\\n", run,run);
|
||||
eprintf ("\t\ts%i [label=\"Run %i\\n", run, run);
|
||||
agentsOfRunPrint (sys, run);
|
||||
eprintf ("\", shape=diamond];\n");
|
||||
eprintf ("\t\ts%i -> ", run);
|
||||
@ -895,8 +898,8 @@ dotSemiState ()
|
||||
rd = rd->next;
|
||||
}
|
||||
/* DISABLED subgraphs
|
||||
eprintf ("\t}\n");
|
||||
*/
|
||||
eprintf ("\t}\n");
|
||||
*/
|
||||
}
|
||||
run++;
|
||||
}
|
||||
@ -983,7 +986,7 @@ dotSemiState ()
|
||||
}
|
||||
if (other_route == 0)
|
||||
{
|
||||
Roledef rd,rd2;
|
||||
Roledef rd, rd2;
|
||||
/*
|
||||
* We have decided to draw this binding,
|
||||
* from run2,ev2 to run,ev
|
||||
@ -995,8 +998,9 @@ dotSemiState ()
|
||||
node (run, ev);
|
||||
eprintf (" ");
|
||||
// decide color
|
||||
rd = roledef_shift (sys->runs[run].start,ev);
|
||||
rd2 = roledef_shift (sys->runs[run2].start,ev2);
|
||||
rd = roledef_shift (sys->runs[run].start, ev);
|
||||
rd2 =
|
||||
roledef_shift (sys->runs[run2].start, ev2);
|
||||
if (rd->type == CLAIM)
|
||||
{
|
||||
// Towards a claim, so only indirect dependency
|
||||
@ -1009,9 +1013,13 @@ dotSemiState ()
|
||||
if (rd->type == READ && rd2->type == SEND)
|
||||
{
|
||||
// We want to distinguish where it is from a 'broken' send
|
||||
if (isTermEqual (rd->message, rd2->message))
|
||||
if (isTermEqual
|
||||
(rd->message, rd2->message))
|
||||
{
|
||||
if (isTermEqual (rd->from, rd2->from) && isTermEqual (rd->to, rd2->to))
|
||||
if (isTermEqual
|
||||
(rd->from, rd2->from)
|
||||
&& isTermEqual (rd->to,
|
||||
rd2->to))
|
||||
{
|
||||
// Wow, a perfect match. Leave the arrow as-is :)
|
||||
eprintf ("[color=forestgreen]");
|
||||
@ -1019,13 +1027,15 @@ dotSemiState ()
|
||||
else
|
||||
{
|
||||
// Same message, different people
|
||||
eprintf ("[label=\"redirect\",color=darkorange2]");
|
||||
eprintf
|
||||
("[label=\"redirect\",color=darkorange2]");
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// Not even the same message, intruder construction
|
||||
eprintf ("[label=\"construct\",color=red]");
|
||||
eprintf
|
||||
("[label=\"construct\",color=red]");
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -1039,8 +1049,9 @@ dotSemiState ()
|
||||
run3--;
|
||||
ev3--;
|
||||
|
||||
eprintf ("\t// HIDDEN r%ii%i -> r%ii%i because route through r%ii%i\n",
|
||||
run2, ev2, run, ev, run3, ev3);
|
||||
eprintf
|
||||
("\t// HIDDEN r%ii%i -> r%ii%i because route through r%ii%i\n",
|
||||
run2, ev2, run, ev, run3, ev3);
|
||||
|
||||
}
|
||||
#endif
|
||||
@ -1055,62 +1066,62 @@ dotSemiState ()
|
||||
}
|
||||
|
||||
// Third, all ranking info
|
||||
{
|
||||
int myrank;
|
||||
{
|
||||
int myrank;
|
||||
|
||||
#ifdef DEBUG
|
||||
{
|
||||
int n;
|
||||
|
||||
eprintf ("/* ranks: %i\n", maxrank);
|
||||
n = 0;
|
||||
while (n < nodes)
|
||||
{
|
||||
int n;
|
||||
|
||||
eprintf ("/* ranks: %i\n", maxrank);
|
||||
n = 0;
|
||||
while (n < nodes)
|
||||
{
|
||||
eprintf ("%i ", ranks[n]);
|
||||
n++;
|
||||
}
|
||||
eprintf ("\n*/\n\n");
|
||||
}
|
||||
#endif
|
||||
myrank = 0;
|
||||
while (myrank < maxrank)
|
||||
{
|
||||
int count;
|
||||
int run;
|
||||
int run1;
|
||||
int ev1;
|
||||
|
||||
count = 0;
|
||||
run = 0;
|
||||
while (run < sys->maxruns)
|
||||
{
|
||||
if (sys->runs[run].protocol != INTRUDER)
|
||||
{
|
||||
int ev;
|
||||
|
||||
ev = 0;
|
||||
while (ev < sys->runs[run].step)
|
||||
{
|
||||
if (myrank == ranks[node_number (run,ev)])
|
||||
{
|
||||
if (count == 0)
|
||||
eprintf ("\t{ rank = same; ");
|
||||
count++;
|
||||
eprintf ("r%ii%i; ",run,ev);
|
||||
}
|
||||
ev++;
|
||||
}
|
||||
}
|
||||
run++;
|
||||
}
|
||||
if (count > 0)
|
||||
eprintf ("}\t\t// rank %i\n", myrank);
|
||||
myrank++;
|
||||
eprintf ("%i ", ranks[n]);
|
||||
n++;
|
||||
}
|
||||
eprintf ("\n*/\n\n");
|
||||
}
|
||||
#endif
|
||||
myrank = 0;
|
||||
while (myrank < maxrank)
|
||||
{
|
||||
int count;
|
||||
int run;
|
||||
int run1;
|
||||
int ev1;
|
||||
|
||||
count = 0;
|
||||
run = 0;
|
||||
while (run < sys->maxruns)
|
||||
{
|
||||
if (sys->runs[run].protocol != INTRUDER)
|
||||
{
|
||||
int ev;
|
||||
|
||||
ev = 0;
|
||||
while (ev < sys->runs[run].step)
|
||||
{
|
||||
if (myrank == ranks[node_number (run, ev)])
|
||||
{
|
||||
if (count == 0)
|
||||
eprintf ("\t{ rank = same; ");
|
||||
count++;
|
||||
eprintf ("r%ii%i; ", run, ev);
|
||||
}
|
||||
ev++;
|
||||
}
|
||||
}
|
||||
run++;
|
||||
}
|
||||
if (count > 0)
|
||||
eprintf ("}\t\t// rank %i\n", myrank);
|
||||
myrank++;
|
||||
}
|
||||
}
|
||||
|
||||
// clean memory
|
||||
memFree (ranks, nodes * sizeof(int)); // ranks
|
||||
memFree (ranks, nodes * sizeof (int)); // ranks
|
||||
|
||||
// close graph
|
||||
eprintf ("};\n\n");
|
||||
@ -1225,8 +1236,8 @@ select_goal ()
|
||||
b = (Binding) bl->data;
|
||||
|
||||
// Ignore singular variables
|
||||
if (!b->done && !realTermVariable (deVar(b->term)) )
|
||||
//if (!b->done)
|
||||
if (!b->done && !realTermVariable (deVar (b->term)))
|
||||
//if (!b->done)
|
||||
{
|
||||
float cons;
|
||||
|
||||
@ -1361,8 +1372,8 @@ bind_goal_new_encrypt (const Binding b)
|
||||
}
|
||||
|
||||
// must be encryption
|
||||
t1 = TermOp(term);
|
||||
t2 = TermKey(term);
|
||||
t1 = TermOp (term);
|
||||
t2 = TermKey (term);
|
||||
|
||||
if (t2 != TERM_Hidden)
|
||||
{
|
||||
@ -1481,7 +1492,8 @@ bind_goal_regular_run (const Binding b)
|
||||
}
|
||||
#endif
|
||||
if (!termMguSubTerm
|
||||
(b->term, rd->message, test_sub_unification, sys->know->inverses, NULL))
|
||||
(b->term, rd->message, test_sub_unification, sys->know->inverses,
|
||||
NULL))
|
||||
{
|
||||
int sflag;
|
||||
|
||||
@ -1665,12 +1677,14 @@ prune_theorems ()
|
||||
{
|
||||
Term agent;
|
||||
|
||||
agent = deVar(agl->term);
|
||||
agent = deVar (agl->term);
|
||||
if (agent == NULL)
|
||||
{
|
||||
error ("Agent of run %i is NULL", run);
|
||||
}
|
||||
if (!realTermLeaf (agent) || (agent->stype != NULL && !inTermlist (agent->stype, TERM_Agent)))
|
||||
if (!realTermLeaf (agent)
|
||||
|| (agent->stype != NULL
|
||||
&& !inTermlist (agent->stype, TERM_Agent)))
|
||||
{
|
||||
if (sys->output == PROOF)
|
||||
{
|
||||
@ -1718,9 +1732,9 @@ prune_theorems ()
|
||||
{
|
||||
if (sys->runs[run].agents != NULL)
|
||||
{
|
||||
Term actor;
|
||||
Term actor;
|
||||
|
||||
actor = agentOfRun(sys, run);
|
||||
actor = agentOfRun (sys, run);
|
||||
if (actor == NULL)
|
||||
{
|
||||
error ("Agent of run %i is NULL", run);
|
||||
@ -1730,7 +1744,9 @@ prune_theorems ()
|
||||
if (sys->output == PROOF)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Pruned because the actor of run %i is untrusted.\n", run);
|
||||
eprintf
|
||||
("Pruned because the actor of run %i is untrusted.\n",
|
||||
run);
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
@ -1741,7 +1757,7 @@ prune_theorems ()
|
||||
|
||||
globalError++;
|
||||
eprintf ("Run %i: ", run);
|
||||
role_name_print (run);
|
||||
role_name_print (run);
|
||||
eprintf (" has an empty agents list.\n");
|
||||
eprintf ("protocol->rolenames: ");
|
||||
p = (Protocol) sys->runs[run].protocol;
|
||||
@ -1847,7 +1863,8 @@ prune_bounds ()
|
||||
if (sys->output == PROOF)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Pruned: proof tree too deep: %i (-l %i switch)\n", proofDepth, sys->switch_maxtracelength);
|
||||
eprintf ("Pruned: proof tree too deep: %i (-l %i switch)\n",
|
||||
proofDepth, sys->switch_maxtracelength);
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
@ -177,7 +177,7 @@ goal_graph_create ()
|
||||
Term t;
|
||||
|
||||
t = tl->term;
|
||||
if (t->type == VARIABLE && TermRunid(t) == run
|
||||
if (t->type == VARIABLE && TermRunid (t) == run
|
||||
&& t->subst != NULL)
|
||||
{
|
||||
// t is a variable of run
|
||||
@ -190,7 +190,7 @@ goal_graph_create ()
|
||||
|
||||
t2 = tl2->term;
|
||||
if (realTermLeaf (t2) && t2->type != VARIABLE
|
||||
&& TermRunid(t2) == run2)
|
||||
&& TermRunid (t2) == run2)
|
||||
{
|
||||
// t2 is a constant of run2
|
||||
if (isTermEqual (t, t2))
|
||||
@ -250,20 +250,28 @@ goal_graph_create ()
|
||||
else
|
||||
{
|
||||
// It doesn't occur first in a READ, which shouldn't be happening
|
||||
if (sys->output == PROOF)
|
||||
if (sys->output ==
|
||||
PROOF)
|
||||
{
|
||||
eprintf ("Term ");
|
||||
eprintf
|
||||
("Term ");
|
||||
termPrint (t2);
|
||||
eprintf (" from run %i occurs in run %i, term ",
|
||||
eprintf
|
||||
(" from run %i occurs in run %i, term ",
|
||||
run2, run);
|
||||
termPrint (t);
|
||||
eprintf (" before it is read?\n");
|
||||
eprintf
|
||||
(" before it is read?\n");
|
||||
}
|
||||
// Thus, we create an artificial loop
|
||||
if (sys->runs[0].step > 1)
|
||||
if (sys->runs[0].
|
||||
step > 1)
|
||||
{
|
||||
// This forces a loop, and thus prunes
|
||||
graph[graph_nodes (nodes, 0,1, 0,0)] = 1;
|
||||
graph
|
||||
[graph_nodes
|
||||
(nodes, 0, 1,
|
||||
0, 0)] = 1;
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -421,21 +429,19 @@ goal_add (Term term, const int run, const int ev, const int level)
|
||||
int nope;
|
||||
|
||||
int testSame (void *data)
|
||||
{
|
||||
Binding b;
|
||||
{
|
||||
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;
|
||||
}
|
||||
}
|
||||
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)
|
||||
|
@ -3,7 +3,9 @@
|
||||
|
||||
int check_claim_nisynch (const System sys, const int i);
|
||||
int check_claim_niagree (const System sys, const int i);
|
||||
int arachne_claim_niagree (const System sys, const int claim_run, const int claim_index);
|
||||
int arachne_claim_nisynch (const System sys, const int claim_run, const int claim_index);
|
||||
int arachne_claim_niagree (const System sys, const int claim_run,
|
||||
const int claim_index);
|
||||
int arachne_claim_nisynch (const System sys, const int claim_run,
|
||||
const int claim_index);
|
||||
|
||||
#endif
|
||||
|
@ -241,7 +241,7 @@ levelFind (Symbol s, int level)
|
||||
{
|
||||
if (isTermLeaf (tl->term))
|
||||
{
|
||||
if (TermSymb(tl->term) == s)
|
||||
if (TermSymb (tl->term) == s)
|
||||
{
|
||||
return tl->term;
|
||||
}
|
||||
@ -404,8 +404,7 @@ commEvent (int event, Tac tc)
|
||||
{
|
||||
/* we already had this label constant */
|
||||
/* leaves a garbage tuple. dunnoh what to do with it */
|
||||
label =
|
||||
makeTermTuple (thisProtocol->nameterm, label);
|
||||
label = makeTermTuple (thisProtocol->nameterm, label);
|
||||
}
|
||||
}
|
||||
/**
|
||||
@ -441,9 +440,11 @@ commEvent (int event, Tac tc)
|
||||
{
|
||||
/* set sendrole */
|
||||
if (!isTermEqual (fromrole, thisRole->nameterm))
|
||||
error ("Send role does not correspond to execution role at line %i.", tc->lineno);
|
||||
error
|
||||
("Send role does not correspond to execution role at line %i.",
|
||||
tc->lineno);
|
||||
if (linfo->sendrole != NULL)
|
||||
error ("Label defined twice for sendrole!");
|
||||
error ("Label defined twice for sendrole!");
|
||||
linfo->sendrole = fromrole;
|
||||
|
||||
/* set keylevels based on send events */
|
||||
@ -456,9 +457,11 @@ commEvent (int event, Tac tc)
|
||||
// READ
|
||||
/* set readrole */
|
||||
if (!isTermEqual (torole, thisRole->nameterm))
|
||||
error ("Read role does not correspond to execution role at line %i.", tc->lineno);
|
||||
error
|
||||
("Read role does not correspond to execution role at line %i.",
|
||||
tc->lineno);
|
||||
if (linfo->readrole != NULL)
|
||||
error ("Label defined twice for readrole!");
|
||||
error ("Label defined twice for readrole!");
|
||||
linfo->readrole = torole;
|
||||
}
|
||||
|
||||
@ -505,7 +508,7 @@ commEvent (int event, Tac tc)
|
||||
else
|
||||
{
|
||||
/* n parameters */
|
||||
msg = TermOp2(deVar (claimbig));
|
||||
msg = TermOp2 (deVar (claimbig));
|
||||
if (tupleCount (msg) != n)
|
||||
{
|
||||
error ("Problem with claim tuple unfolding at line %i.",
|
||||
@ -540,7 +543,8 @@ commEvent (int event, Tac tc)
|
||||
cl->rolename = fromrole;
|
||||
cl->role = thisRole;
|
||||
if (!isTermEqual (fromrole, thisRole->nameterm))
|
||||
error ("Claim role does not correspond to execution role at line %i.", tc->lineno);
|
||||
error ("Claim role does not correspond to execution role at line %i.",
|
||||
tc->lineno);
|
||||
cl->roledef = NULL;
|
||||
cl->count = 0;
|
||||
cl->complete = 0;
|
||||
@ -690,7 +694,7 @@ runInstanceCreate (Tac tc)
|
||||
/* first, locate the protocol */
|
||||
psym = tc->t1.tac->t1.sym;
|
||||
p = sys->protocols;
|
||||
while (p != NULL && TermSymb(p->nameterm) != psym)
|
||||
while (p != NULL && TermSymb (p->nameterm) != psym)
|
||||
p = p->next;
|
||||
if (p == NULL)
|
||||
{
|
||||
@ -703,7 +707,7 @@ runInstanceCreate (Tac tc)
|
||||
/* locate the role */
|
||||
rsym = tc->t1.tac->t2.sym;
|
||||
r = p->roles;
|
||||
while (r != NULL && TermSymb(r->nameterm) != rsym)
|
||||
while (r != NULL && TermSymb (r->nameterm) != rsym)
|
||||
r = r->next;
|
||||
if (r == NULL)
|
||||
{
|
||||
@ -948,7 +952,7 @@ compute_label_roles (Termlist labels)
|
||||
linfo = label_find (sys->labellist, labels->term);
|
||||
#ifdef DEBUG
|
||||
if (linfo == NULL)
|
||||
error ("Label in prec list not found in label info list");
|
||||
error ("Label in prec list not found in label info list");
|
||||
#endif
|
||||
roles = termlistAddNew (roles, linfo->sendrole);
|
||||
roles = termlistAddNew (roles, linfo->readrole);
|
||||
@ -977,7 +981,8 @@ order_label_roles (const Claimlist cl)
|
||||
#endif
|
||||
roles_remaining = termlistShallow (cl->roles);
|
||||
roles_ordered = termlistAdd (NULL, cl->rolename);
|
||||
roles_remaining = termlistDelTerm (termlistFind (roles_remaining, cl->rolename));
|
||||
roles_remaining =
|
||||
termlistDelTerm (termlistFind (roles_remaining, cl->rolename));
|
||||
|
||||
distance = 0;
|
||||
while (roles_remaining != NULL)
|
||||
@ -991,40 +996,42 @@ order_label_roles (const Claimlist cl)
|
||||
#endif
|
||||
|
||||
int scan_label (void *data)
|
||||
{
|
||||
Labelinfo linfo;
|
||||
{
|
||||
Labelinfo linfo;
|
||||
|
||||
linfo = (Labelinfo) data;
|
||||
if (inTermlist (cl->prec, linfo->label ))
|
||||
{
|
||||
if (linfo->protocol == cl->protocol)
|
||||
linfo = (Labelinfo) data;
|
||||
if (inTermlist (cl->prec, linfo->label))
|
||||
{
|
||||
if (linfo->protocol == cl->protocol)
|
||||
{
|
||||
// If it's not the same protocol, the labels can't match
|
||||
|
||||
// This function checks whether the newrole can connect to the connectedrole, and whether they fulfil their requirements.
|
||||
void roles_test (const Term connectedrole, const Term newrole)
|
||||
{
|
||||
// If it's not the same protocol, the labels can't match
|
||||
|
||||
// This function checks whether the newrole can connect to the connectedrole, and whether they fulfil their requirements.
|
||||
void roles_test (const Term connectedrole, const Term newrole)
|
||||
if (inTermlist (roles_ordered, connectedrole) &&
|
||||
inTermlist (roles_remaining, newrole))
|
||||
{
|
||||
if (inTermlist (roles_ordered, connectedrole) &&
|
||||
inTermlist (roles_remaining, newrole))
|
||||
{
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (4))
|
||||
{
|
||||
eprintf (" ");
|
||||
termPrint (newrole);
|
||||
}
|
||||
#endif
|
||||
roles_ordered = termlistAppend (roles_ordered, newrole);
|
||||
roles_remaining = termlistDelTerm (termlistFind (roles_remaining, newrole));
|
||||
if (DEBUGL (4))
|
||||
{
|
||||
eprintf (" ");
|
||||
termPrint (newrole);
|
||||
}
|
||||
#endif
|
||||
roles_ordered = termlistAppend (roles_ordered, newrole);
|
||||
roles_remaining =
|
||||
termlistDelTerm (termlistFind
|
||||
(roles_remaining, newrole));
|
||||
}
|
||||
|
||||
roles_test (linfo->sendrole, linfo->readrole);
|
||||
roles_test (linfo->readrole, linfo->sendrole);
|
||||
}
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
roles_test (linfo->sendrole, linfo->readrole);
|
||||
roles_test (linfo->readrole, linfo->sendrole);
|
||||
}
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
list_iterate (sys->labellist, scan_label);
|
||||
}
|
||||
@ -1417,7 +1424,7 @@ compute_prec_sets (const System sys)
|
||||
{
|
||||
Protocol p;
|
||||
|
||||
printf ("Preceding label set for r:%i, ev:%i = ", r1,ev1);
|
||||
printf ("Preceding label set for r:%i, ev:%i = ", r1, ev1);
|
||||
termlistPrint (cl->prec);
|
||||
printf (", involving roles ");
|
||||
termlistPrint (cl->roles);
|
||||
|
@ -154,8 +154,8 @@ knowledgeAddTerm (Knowledge know, Term term)
|
||||
{
|
||||
int status;
|
||||
|
||||
status = knowledgeAddTerm (know, TermOp1(term));
|
||||
return knowledgeAddTerm (know, TermOp2(term)) || status;
|
||||
status = knowledgeAddTerm (know, TermOp1 (term));
|
||||
return knowledgeAddTerm (know, TermOp2 (term)) || status;
|
||||
}
|
||||
|
||||
/* test whether we knew it before */
|
||||
@ -172,12 +172,12 @@ knowledgeAddTerm (Knowledge know, Term term)
|
||||
}
|
||||
if (term->type == ENCRYPT)
|
||||
{
|
||||
Term invkey = inverseKey (know->inverses, TermKey(term));
|
||||
Term invkey = inverseKey (know->inverses, TermKey (term));
|
||||
if (inKnowledge (know, invkey))
|
||||
{
|
||||
/* we can decrypt it */
|
||||
knowledgeAddTerm (know, TermOp(term));
|
||||
if (!inKnowledge (know, TermKey(term)))
|
||||
knowledgeAddTerm (know, TermOp (term));
|
||||
if (!inKnowledge (know, TermKey (term)))
|
||||
{
|
||||
/* we know the op now, but not the key, so add it anyway */
|
||||
know->encrypt = termlistAdd (know->encrypt, term);
|
||||
@ -208,9 +208,9 @@ knowledgeSimplify (Knowledge know, Term key)
|
||||
|
||||
while (scan != NULL)
|
||||
{
|
||||
if (isTermEqual (TermKey(scan->term), invkey))
|
||||
if (isTermEqual (TermKey (scan->term), invkey))
|
||||
{
|
||||
tldecrypts = termlistAdd (tldecrypts, TermOp(scan->term));
|
||||
tldecrypts = termlistAdd (tldecrypts, TermOp (scan->term));
|
||||
know->encrypt = termlistDelTerm (scan);
|
||||
scan = know->encrypt;
|
||||
}
|
||||
@ -285,14 +285,14 @@ inKnowledge (const Knowledge know, Term term)
|
||||
if (term->type == ENCRYPT)
|
||||
{
|
||||
return inTermlist (know->encrypt, term) ||
|
||||
(inKnowledge (know, TermKey(term))
|
||||
&& inKnowledge (know, TermOp(term)));
|
||||
(inKnowledge (know, TermKey (term))
|
||||
&& inKnowledge (know, TermOp (term)));
|
||||
}
|
||||
if (term->type == TUPLE)
|
||||
{
|
||||
return (inTermlist (know->encrypt, term) ||
|
||||
(inKnowledge (know, TermOp1(term)) &&
|
||||
inKnowledge (know, TermOp2(term))));
|
||||
(inKnowledge (know, TermOp1 (term)) &&
|
||||
inKnowledge (know, TermOp2 (term))));
|
||||
}
|
||||
return 0; /* unrecognized term type, weird */
|
||||
}
|
||||
|
36
src/label.c
36
src/label.c
@ -9,7 +9,8 @@
|
||||
#include "system.h"
|
||||
|
||||
//! Create a new labelinfo node
|
||||
Labelinfo label_create (const Term label, const Protocol protocol)
|
||||
Labelinfo
|
||||
label_create (const Term label, const Protocol protocol)
|
||||
{
|
||||
Labelinfo li;
|
||||
|
||||
@ -22,31 +23,33 @@ Labelinfo label_create (const Term label, const Protocol protocol)
|
||||
}
|
||||
|
||||
//! Destroy a labelinfo node
|
||||
void label_destroy (Labelinfo linfo)
|
||||
void
|
||||
label_destroy (Labelinfo linfo)
|
||||
{
|
||||
memFree (linfo, sizeof (struct labelinfo));
|
||||
}
|
||||
|
||||
//! Given a list of label infos, yield the correct one or NULL
|
||||
Labelinfo label_find (List labellist, const Term label)
|
||||
Labelinfo
|
||||
label_find (List labellist, const Term label)
|
||||
{
|
||||
Labelinfo linfo;
|
||||
|
||||
int label_find_scan (void *data)
|
||||
{
|
||||
Labelinfo linfo_scan;
|
||||
{
|
||||
Labelinfo linfo_scan;
|
||||
|
||||
linfo_scan = (Labelinfo) data;
|
||||
if (isTermEqual (label, linfo_scan->label))
|
||||
{
|
||||
linfo = linfo_scan;
|
||||
return 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
linfo_scan = (Labelinfo) data;
|
||||
if (isTermEqual (label, linfo_scan->label))
|
||||
{
|
||||
linfo = linfo_scan;
|
||||
return 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
linfo = NULL;
|
||||
if (label != NULL)
|
||||
@ -55,4 +58,3 @@ Labelinfo label_find (List labellist, const Term label)
|
||||
}
|
||||
return linfo;
|
||||
}
|
||||
|
||||
|
10
src/label.h
10
src/label.h
@ -10,13 +10,13 @@
|
||||
*/
|
||||
struct labelinfo
|
||||
{
|
||||
Term label;
|
||||
Protocol protocol;
|
||||
Term sendrole;
|
||||
Term readrole;
|
||||
Term label;
|
||||
Protocol protocol;
|
||||
Term sendrole;
|
||||
Term readrole;
|
||||
};
|
||||
|
||||
typedef struct labelinfo* Labelinfo;
|
||||
typedef struct labelinfo *Labelinfo;
|
||||
|
||||
Labelinfo label_create (const Term label, const Protocol protocol);
|
||||
void label_destroy (Labelinfo linfo);
|
||||
|
24
src/latex.c
24
src/latex.c
@ -117,12 +117,12 @@ latexTermPrint (Term term, Termlist highlight)
|
||||
{
|
||||
if (inTermlist (highlight, term))
|
||||
printf ("\\mathbf{");
|
||||
symbolPrint (TermSymb(term));
|
||||
symbolPrint (TermSymb (term));
|
||||
if (realTermVariable (term))
|
||||
printf ("V");
|
||||
if (TermRunid(term) >= 0)
|
||||
if (TermRunid (term) >= 0)
|
||||
{
|
||||
printf ("\\sharp%i", TermRunid(term));
|
||||
printf ("\\sharp%i", TermRunid (term));
|
||||
}
|
||||
if (term->subst != NULL)
|
||||
{
|
||||
@ -141,22 +141,22 @@ latexTermPrint (Term term, Termlist highlight)
|
||||
}
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
if (isTermLeaf (TermKey(term))
|
||||
&& inTermlist (TermKey(term)->stype, TERM_Function))
|
||||
if (isTermLeaf (TermKey (term))
|
||||
&& inTermlist (TermKey (term)->stype, TERM_Function))
|
||||
{
|
||||
/* function application */
|
||||
latexTermPrint (TermKey(term), highlight);
|
||||
latexTermPrint (TermKey (term), highlight);
|
||||
printf ("(");
|
||||
latexTermTuplePrint (TermOp(term), highlight);
|
||||
latexTermTuplePrint (TermOp (term), highlight);
|
||||
printf (")");
|
||||
}
|
||||
else
|
||||
{
|
||||
/* normal encryption */
|
||||
printf ("\\{");
|
||||
latexTermTuplePrint (TermOp(term), highlight);
|
||||
latexTermTuplePrint (TermOp (term), highlight);
|
||||
printf ("\\}_{");
|
||||
latexTermPrint (TermKey(term), highlight);
|
||||
latexTermPrint (TermKey (term), highlight);
|
||||
printf ("}");
|
||||
}
|
||||
}
|
||||
@ -180,9 +180,9 @@ latexTermTuplePrint (Term term, Termlist hl)
|
||||
while (realTermTuple (term))
|
||||
{
|
||||
// To remove any brackets, change this into latexTermTuplePrint.
|
||||
latexTermPrint (TermOp1(term), hl);
|
||||
latexTermPrint (TermOp1 (term), hl);
|
||||
printf (",");
|
||||
term = deVar (TermOp2(term));
|
||||
term = deVar (TermOp2 (term));
|
||||
}
|
||||
latexTermPrint (term, hl);
|
||||
return;
|
||||
@ -966,7 +966,7 @@ attackDisplayLatex (const System sys)
|
||||
{
|
||||
/* detect whether it's really local to this run */
|
||||
Term t = deVar (tl->term);
|
||||
if (isTermLeaf (t) && TermRunid(t) == i)
|
||||
if (isTermLeaf (t) && TermRunid (t) == i)
|
||||
{
|
||||
if (first)
|
||||
{
|
||||
|
@ -771,15 +771,15 @@ timersPrint (const System sys)
|
||||
if (realTermTuple (cl_scan->label))
|
||||
{
|
||||
/* modern version: claim label is tuple (protocname, label) */
|
||||
/* first print protocol.role */
|
||||
termPrint (TermOp1(cl_scan->label));
|
||||
/* first print protocol.role */
|
||||
termPrint (TermOp1 (cl_scan->label));
|
||||
eprintf ("\t");
|
||||
termPrint (cl_scan->rolename);
|
||||
eprintf ("\t");
|
||||
/* second print event_label */
|
||||
termPrint (cl_scan->type);
|
||||
eprintf ("_");
|
||||
termPrint (TermOp2(cl_scan->label));
|
||||
termPrint (TermOp2 (cl_scan->label));
|
||||
eprintf ("\t");
|
||||
}
|
||||
else
|
||||
@ -790,7 +790,7 @@ timersPrint (const System sys)
|
||||
termPrint (cl_scan->rolename);
|
||||
eprintf (" (");
|
||||
termPrint (cl_scan->label);
|
||||
eprintf (")\t");
|
||||
eprintf (")\t");
|
||||
}
|
||||
/* print counts etc. */
|
||||
eprintf ("found:\t");
|
||||
|
@ -60,11 +60,11 @@ solve (const struct solvepass sp, Constraintlist solvecons)
|
||||
cl = constraintlistDuplicate (solvecons);
|
||||
cl =
|
||||
constraintlistAdd (cl,
|
||||
makeConstraint (TermOp1(deVar (activeco->term)),
|
||||
makeConstraint (TermOp1 (deVar (activeco->term)),
|
||||
activeco->know));
|
||||
cl =
|
||||
constraintlistAdd (cl,
|
||||
makeConstraint (TermOp2(deVar (activeco->term)),
|
||||
makeConstraint (TermOp2 (deVar (activeco->term)),
|
||||
activeco->know));
|
||||
solvecons = cl;
|
||||
flag = solve (sp, solvecons) || flag;
|
||||
@ -192,11 +192,11 @@ solve (const struct solvepass sp, Constraintlist solvecons)
|
||||
cl = constraintlistDuplicate (oldcl);
|
||||
cl =
|
||||
constraintlistAdd (cl,
|
||||
makeConstraint (TermOp(activeco->term),
|
||||
makeConstraint (TermOp (activeco->term),
|
||||
activeco->know));
|
||||
cl =
|
||||
constraintlistAdd (cl,
|
||||
makeConstraint (TermKey(activeco->term),
|
||||
makeConstraint (TermKey (activeco->term),
|
||||
activeco->know));
|
||||
solvecons = cl;
|
||||
flag = solve (sp, solvecons) || flag;
|
||||
@ -368,8 +368,8 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
|
||||
{
|
||||
/* tuple */
|
||||
tl2 = termlistShallow (tl->next);
|
||||
tl2 = termlistAdd (tl2, TermOp1(t));
|
||||
tl2 = termlistAdd (tl2, TermOp2(t));
|
||||
tl2 = termlistAdd (tl2, TermOp1 (t));
|
||||
tl2 = termlistAdd (tl2, TermOp2 (t));
|
||||
sendAdd_clp (sys, run, tl2);
|
||||
termlistDelete (tl2);
|
||||
}
|
||||
@ -378,15 +378,15 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
|
||||
/* encrypt */
|
||||
Term invkey;
|
||||
|
||||
invkey = inverseKey (sys->know->inverses, TermKey(t));
|
||||
invkey = inverseKey (sys->know->inverses, TermKey (t));
|
||||
if (!hasTermVariable (invkey))
|
||||
{
|
||||
/* simple case: no variable inside */
|
||||
knowledgeAddTerm (sys->know, t);
|
||||
tl2 = termlistShallow (tl->next);
|
||||
if (inKnowledge (sys->know, invkey)
|
||||
&& hasTermVariable (TermOp(t)))
|
||||
tl2 = termlistAdd (tl2, TermOp(t));
|
||||
&& hasTermVariable (TermOp (t)))
|
||||
tl2 = termlistAdd (tl2, TermOp (t));
|
||||
sendAdd_clp (sys, run, tl2);
|
||||
termlistDelete (tl2);
|
||||
}
|
||||
@ -418,7 +418,7 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
|
||||
sys->constraints = constraintlistAdd (clbuf, co);
|
||||
/* we _could_ explore first if this is solveable */
|
||||
knowledgeAddTerm (sys->know, t);
|
||||
tl2 = termlistAdd (tl2, TermOp(t));
|
||||
tl2 = termlistAdd (tl2, TermOp (t));
|
||||
sendAdd_clp (sys, run, tl2);
|
||||
|
||||
termlistDelete (tl2);
|
||||
|
25
src/mgu.c
25
src/mgu.c
@ -183,14 +183,14 @@ termMguTerm (Term t1, Term t2)
|
||||
{
|
||||
Termlist tl1, tl2;
|
||||
|
||||
tl1 = termMguTerm (TermKey(t1), TermKey(t2));
|
||||
tl1 = termMguTerm (TermKey (t1), TermKey (t2));
|
||||
if (tl1 == MGUFAIL)
|
||||
{
|
||||
return MGUFAIL;
|
||||
}
|
||||
else
|
||||
{
|
||||
tl2 = termMguTerm (TermOp(t1), TermOp(t2));
|
||||
tl2 = termMguTerm (TermOp (t1), TermOp (t2));
|
||||
if (tl2 == MGUFAIL)
|
||||
{
|
||||
termlistSubstReset (tl1);
|
||||
@ -210,14 +210,14 @@ termMguTerm (Term t1, Term t2)
|
||||
{
|
||||
Termlist tl1, tl2;
|
||||
|
||||
tl1 = termMguTerm (TermOp1(t1), TermOp1(t2));
|
||||
tl1 = termMguTerm (TermOp1 (t1), TermOp1 (t2));
|
||||
if (tl1 == MGUFAIL)
|
||||
{
|
||||
return MGUFAIL;
|
||||
}
|
||||
else
|
||||
{
|
||||
tl2 = termMguTerm (TermOp2(t1), TermOp2(t2));
|
||||
tl2 = termMguTerm (TermOp2 (t1), TermOp2 (t2));
|
||||
if (tl2 == MGUFAIL)
|
||||
{
|
||||
termlistSubstReset (tl1);
|
||||
@ -251,8 +251,8 @@ termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist))
|
||||
if (realTermTuple (t2))
|
||||
{
|
||||
// t2 is a tuple, consider interm options as well.
|
||||
flag = flag && termMguInTerm (t1, TermOp1(t2), iterator);
|
||||
flag = flag && termMguInTerm (t1, TermOp2(t2), iterator);
|
||||
flag = flag && termMguInTerm (t1, TermOp1 (t2), iterator);
|
||||
flag = flag && termMguInTerm (t1, TermOp2 (t2), iterator);
|
||||
}
|
||||
// simple clause or combined
|
||||
tl = termMguTerm (t1, t2);
|
||||
@ -300,10 +300,10 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
|
||||
{
|
||||
// 'simple' tuple
|
||||
flag =
|
||||
flag && termMguSubTerm (t1, TermOp1(t2), iterator, inverses,
|
||||
flag && termMguSubTerm (t1, TermOp1 (t2), iterator, inverses,
|
||||
keylist);
|
||||
flag =
|
||||
flag && termMguSubTerm (t1, TermOp2(t2), iterator, inverses,
|
||||
flag && termMguSubTerm (t1, TermOp2 (t2), iterator, inverses,
|
||||
keylist);
|
||||
}
|
||||
else
|
||||
@ -312,19 +312,20 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
|
||||
// So, we need the key, and try to get the rest
|
||||
Term newkey;
|
||||
|
||||
newkey = inverseKey (inverses, TermKey(t2));
|
||||
newkey = inverseKey (inverses, TermKey (t2));
|
||||
// We can never produce the TERM_Hidden key, thus, this is not a valid iteration.
|
||||
if (!isTermEqual (newkey, TERM_Hidden))
|
||||
{
|
||||
Termlist keylist_new;
|
||||
Termlist keylist_new;
|
||||
|
||||
keylist_new = termlistShallow (keylist);
|
||||
keylist_new = termlistAdd (keylist_new, newkey);
|
||||
|
||||
// Recurse
|
||||
flag =
|
||||
flag && termMguSubTerm (t1, TermOp(t2), iterator, inverses,
|
||||
keylist_new);
|
||||
flag
|
||||
&& termMguSubTerm (t1, TermOp (t2), iterator, inverses,
|
||||
keylist_new);
|
||||
|
||||
termlistDelete (keylist_new);
|
||||
}
|
||||
|
@ -1147,7 +1147,7 @@ claimSecrecy (const System sys, const Term t)
|
||||
{
|
||||
t = deVar (t);
|
||||
if (isTermTuple (t))
|
||||
return csScan (TermOp1(t)) && csScan (TermOp2(t));
|
||||
return csScan (TermOp1 (t)) && csScan (TermOp2 (t));
|
||||
else
|
||||
return isTermSecret (sys, t);
|
||||
}
|
||||
@ -1171,8 +1171,8 @@ secrecyUnfolding (Term t, const Knowledge know)
|
||||
{
|
||||
t = deVar (t);
|
||||
if (isTermTuple (t))
|
||||
return termlistConcat (secrecyUnfolding (TermOp1(t), know),
|
||||
secrecyUnfolding (TermOp2(t), know));
|
||||
return termlistConcat (secrecyUnfolding (TermOp1 (t), know),
|
||||
secrecyUnfolding (TermOp2 (t), know));
|
||||
else
|
||||
{
|
||||
if (inKnowledge (know, t))
|
||||
|
@ -61,7 +61,7 @@ roledefPrintGeneric (Roledef rd, int print_actor)
|
||||
if (protocolCount < 2 && realTermTuple (label))
|
||||
{
|
||||
// Only one protocol, so we don't need to show the extra label info
|
||||
label = TermOp2(label);
|
||||
label = TermOp2 (label);
|
||||
}
|
||||
|
||||
//! Print latex/normal
|
||||
@ -84,8 +84,8 @@ roledefPrintGeneric (Roledef rd, int print_actor)
|
||||
{
|
||||
if (print_actor || rd->type == READ)
|
||||
{
|
||||
termPrint (rd->from);
|
||||
eprintf (",");
|
||||
termPrint (rd->from);
|
||||
eprintf (",");
|
||||
}
|
||||
if (rd->type == CLAIM)
|
||||
eprintf (" ");
|
||||
|
@ -64,14 +64,14 @@ termSubstitute (Term term, Substitution subs)
|
||||
{
|
||||
if (isTermEncrypt (term))
|
||||
{
|
||||
return makeTermEncrypt (termSubstitute (TermOp(term), subs),
|
||||
termSubstitute (TermKey(term), subs));
|
||||
return makeTermEncrypt (termSubstitute (TermOp (term), subs),
|
||||
termSubstitute (TermKey (term), subs));
|
||||
}
|
||||
else
|
||||
{
|
||||
return
|
||||
makeTermTuple (termSubstitute (TermOp1(term), subs),
|
||||
termSubstitute (TermOp2(term), subs));
|
||||
makeTermTuple (termSubstitute (TermOp1 (term), subs),
|
||||
termSubstitute (TermOp2 (term), subs));
|
||||
}
|
||||
}
|
||||
else
|
||||
|
@ -563,7 +563,7 @@ create_new_local (const Term t, const int rid)
|
||||
{
|
||||
Term newt;
|
||||
|
||||
newt = makeTermType (t->type, TermSymb(t), rid);
|
||||
newt = makeTermType (t->type, TermSymb (t), rid);
|
||||
newt->stype = t->stype;
|
||||
|
||||
return newt;
|
||||
@ -667,7 +667,7 @@ roleInstanceArachne (const System sys, const Protocol protocol,
|
||||
if (realTermVariable (newt))
|
||||
{
|
||||
// Make new var for this run
|
||||
newt = makeTermType (VARIABLE, TermSymb(newt), rid);
|
||||
newt = makeTermType (VARIABLE, TermSymb (newt), rid);
|
||||
artefacts = termlistAdd (artefacts, newt);
|
||||
newt->stype = oldt->stype;
|
||||
// Copy substitution
|
||||
@ -808,7 +808,7 @@ roleInstanceModelchecker (const System sys, const Protocol protocol,
|
||||
|
||||
/* There is a TYPE constant in the parameter list.
|
||||
* Generate a new local variable for this run, with this type */
|
||||
newvar = makeTermType (VARIABLE, TermSymb(scanfrom->term), rid);
|
||||
newvar = makeTermType (VARIABLE, TermSymb (scanfrom->term), rid);
|
||||
artefacts = termlistAdd (artefacts, newvar);
|
||||
sys->variables = termlistAdd (sys->variables, newvar);
|
||||
newvar->stype = termlistAdd (NULL, scanto->term);
|
||||
@ -1200,7 +1200,7 @@ agentsOfRunPrint (const System sys, const int run)
|
||||
if (!isTermEqual (role, roles->term))
|
||||
{
|
||||
if (notfirst)
|
||||
eprintf (", ");
|
||||
eprintf (", ");
|
||||
termPrint (roles->term);
|
||||
eprintf (":");
|
||||
termPrint (agentOfRunRole (sys, run, roles->term));
|
||||
|
312
src/term.c
312
src/term.c
@ -75,8 +75,8 @@ makeTermEncrypt (Term t1, Term t2)
|
||||
Term term = makeTerm ();
|
||||
term->type = ENCRYPT;
|
||||
term->stype = NULL;
|
||||
TermOp(term) = t1;
|
||||
TermKey(term) = t2;
|
||||
TermOp (term) = t1;
|
||||
TermKey (term) = t2;
|
||||
return term;
|
||||
}
|
||||
|
||||
@ -111,8 +111,8 @@ makeTermTuple (Term t1, Term t2)
|
||||
tt = makeTerm ();
|
||||
tt->type = TUPLE;
|
||||
tt->stype = NULL;
|
||||
TermOp1(tt) = t1;
|
||||
TermOp2(tt) = t2;
|
||||
TermOp1 (tt) = t1;
|
||||
TermOp2 (tt) = t2;
|
||||
return tt;
|
||||
}
|
||||
|
||||
@ -128,8 +128,8 @@ makeTermType (const int type, const Symbol symb, const int runid)
|
||||
term->type = type;
|
||||
term->stype = NULL;
|
||||
term->subst = NULL;
|
||||
TermSymb(term) = symb;
|
||||
TermRunid(term) = runid;
|
||||
TermSymb (term) = symb;
|
||||
TermRunid (term) = runid;
|
||||
return term;
|
||||
}
|
||||
|
||||
@ -163,11 +163,11 @@ hasTermVariable (Term term)
|
||||
else
|
||||
{
|
||||
if (realTermTuple (term))
|
||||
return (hasTermVariable (TermOp1(term))
|
||||
|| hasTermVariable (TermOp2(term)));
|
||||
return (hasTermVariable (TermOp1 (term))
|
||||
|| hasTermVariable (TermOp2 (term)));
|
||||
else
|
||||
return (hasTermVariable (TermOp(term))
|
||||
|| hasTermVariable (TermKey(term)));
|
||||
return (hasTermVariable (TermOp (term))
|
||||
|| hasTermVariable (TermKey (term)));
|
||||
}
|
||||
}
|
||||
|
||||
@ -206,8 +206,8 @@ isTermEqualFn (Term term1, Term term2)
|
||||
}
|
||||
if (realTermLeaf (term1))
|
||||
{
|
||||
return (TermSymb(term1) == TermSymb(term2)
|
||||
&& TermRunid(term1) == TermRunid(term2));
|
||||
return (TermSymb (term1) == TermSymb (term2)
|
||||
&& TermRunid (term1) == TermRunid (term2));
|
||||
}
|
||||
else
|
||||
{
|
||||
@ -218,15 +218,15 @@ isTermEqualFn (Term term1, Term term2)
|
||||
/* for optimization of encryption equality, we compare
|
||||
operator 2 first (we expect it to be a smaller term)
|
||||
*/
|
||||
return (isTermEqualFn (TermKey(term1), TermKey(term2)) &&
|
||||
isTermEqualFn (TermOp(term1), TermOp(term2)));
|
||||
return (isTermEqualFn (TermKey (term1), TermKey (term2)) &&
|
||||
isTermEqualFn (TermOp (term1), TermOp (term2)));
|
||||
}
|
||||
else
|
||||
{
|
||||
/* tuple */
|
||||
|
||||
return (isTermEqualFn (TermOp1(term1), TermOp1(term2)) &&
|
||||
isTermEqualFn (TermOp2(term1), TermOp2(term2)));
|
||||
return (isTermEqualFn (TermOp1 (term1), TermOp1 (term2)) &&
|
||||
isTermEqualFn (TermOp2 (term1), TermOp2 (term2)));
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -248,11 +248,11 @@ termSubTerm (Term t, Term tsub)
|
||||
if (realTermLeaf (t))
|
||||
return 0;
|
||||
if (realTermTuple (t))
|
||||
return (termSubTerm (TermOp1(t), tsub)
|
||||
|| termSubTerm (TermOp2(t), tsub));
|
||||
return (termSubTerm (TermOp1 (t), tsub)
|
||||
|| termSubTerm (TermOp2 (t), tsub));
|
||||
else
|
||||
return (termSubTerm (TermOp(t), tsub)
|
||||
|| termSubTerm (TermKey(t), tsub));
|
||||
return (termSubTerm (TermOp (t), tsub)
|
||||
|| termSubTerm (TermKey (t), tsub));
|
||||
}
|
||||
|
||||
//! See if a term is an interm of another.
|
||||
@ -272,8 +272,7 @@ termInTerm (Term t, Term tsub)
|
||||
if (realTermLeaf (t))
|
||||
return 0;
|
||||
if (realTermTuple (t))
|
||||
return (termInTerm (TermOp1(t), tsub)
|
||||
|| termInTerm (TermOp2(t), tsub));
|
||||
return (termInTerm (TermOp1 (t), tsub) || termInTerm (TermOp2 (t), tsub));
|
||||
else
|
||||
return 0;
|
||||
}
|
||||
@ -303,15 +302,15 @@ termPrint (Term term)
|
||||
#endif
|
||||
if (realTermLeaf (term))
|
||||
{
|
||||
symbolPrint (TermSymb(term));
|
||||
symbolPrint (TermSymb (term));
|
||||
if (term->type == VARIABLE)
|
||||
eprintf ("V");
|
||||
if (TermRunid(term) >= 0)
|
||||
if (TermRunid (term) >= 0)
|
||||
{
|
||||
if (globalLatex && globalError == 0)
|
||||
eprintf ("\\sharp%i", TermRunid(term));
|
||||
eprintf ("\\sharp%i", TermRunid (term));
|
||||
else
|
||||
eprintf ("#%i", TermRunid(term));
|
||||
eprintf ("#%i", TermRunid (term));
|
||||
}
|
||||
if (term->subst != NULL)
|
||||
{
|
||||
@ -331,13 +330,13 @@ termPrint (Term term)
|
||||
}
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
if (isTermLeaf (TermKey(term))
|
||||
&& inTermlist (TermKey(term)->stype, TERM_Function))
|
||||
if (isTermLeaf (TermKey (term))
|
||||
&& inTermlist (TermKey (term)->stype, TERM_Function))
|
||||
{
|
||||
/* function application */
|
||||
termPrint (TermKey(term));
|
||||
termPrint (TermKey (term));
|
||||
eprintf ("(");
|
||||
termTuplePrint (TermOp(term));
|
||||
termTuplePrint (TermOp (term));
|
||||
eprintf (")");
|
||||
}
|
||||
else
|
||||
@ -346,17 +345,17 @@ termPrint (Term term)
|
||||
if (globalLatex)
|
||||
{
|
||||
eprintf ("\\{");
|
||||
termTuplePrint (TermOp(term));
|
||||
termTuplePrint (TermOp (term));
|
||||
eprintf ("\\}_{");
|
||||
termPrint (TermKey(term));
|
||||
termPrint (TermKey (term));
|
||||
eprintf ("}");
|
||||
}
|
||||
else
|
||||
{
|
||||
eprintf ("{");
|
||||
termTuplePrint (TermOp(term));
|
||||
termTuplePrint (TermOp (term));
|
||||
eprintf ("}");
|
||||
termPrint (TermKey(term));
|
||||
termPrint (TermKey (term));
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -380,9 +379,9 @@ termTuplePrint (Term term)
|
||||
while (realTermTuple (term))
|
||||
{
|
||||
// To remove any brackets, change this into termTuplePrint.
|
||||
termPrint (TermOp1(term));
|
||||
termPrint (TermOp1 (term));
|
||||
eprintf (",");
|
||||
term = deVar (TermOp2(term));
|
||||
term = deVar (TermOp2 (term));
|
||||
}
|
||||
termPrint (term);
|
||||
return;
|
||||
@ -409,13 +408,13 @@ termDuplicate (const Term term)
|
||||
memcpy (newterm, term, sizeof (struct term));
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
TermOp(newterm) = termDuplicate (TermOp(term));
|
||||
TermKey(newterm) = termDuplicate (TermKey(term));
|
||||
TermOp (newterm) = termDuplicate (TermOp (term));
|
||||
TermKey (newterm) = termDuplicate (TermKey (term));
|
||||
}
|
||||
else
|
||||
{
|
||||
TermOp1(newterm) = termDuplicate (TermOp1(term));
|
||||
TermOp2(newterm) = termDuplicate (TermOp2(term));
|
||||
TermOp1 (newterm) = termDuplicate (TermOp1 (term));
|
||||
TermOp2 (newterm) = termDuplicate (TermOp2 (term));
|
||||
}
|
||||
return newterm;
|
||||
}
|
||||
@ -464,13 +463,13 @@ termDuplicateDeep (const Term term)
|
||||
{
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
TermOp(newterm) = termDuplicateDeep (TermOp(term));
|
||||
TermKey(newterm) = termDuplicateDeep (TermKey(term));
|
||||
TermOp (newterm) = termDuplicateDeep (TermOp (term));
|
||||
TermKey (newterm) = termDuplicateDeep (TermKey (term));
|
||||
}
|
||||
else
|
||||
{
|
||||
TermOp1(newterm) = termDuplicateDeep (TermOp1(term));
|
||||
TermOp2(newterm) = termDuplicateDeep (TermOp2(term));
|
||||
TermOp1 (newterm) = termDuplicateDeep (TermOp1 (term));
|
||||
TermOp2 (newterm) = termDuplicateDeep (TermOp2 (term));
|
||||
}
|
||||
}
|
||||
return newterm;
|
||||
@ -497,13 +496,13 @@ termDuplicateUV (Term term)
|
||||
memcpy (newterm, term, sizeof (struct term));
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
TermOp(newterm) = termDuplicateUV (TermOp(term));
|
||||
TermKey(newterm) = termDuplicateUV (TermKey(term));
|
||||
TermOp (newterm) = termDuplicateUV (TermOp (term));
|
||||
TermKey (newterm) = termDuplicateUV (TermKey (term));
|
||||
}
|
||||
else
|
||||
{
|
||||
TermOp1(newterm) = termDuplicateUV (TermOp1(term));
|
||||
TermOp2(newterm) = termDuplicateUV (TermOp2(term));
|
||||
TermOp1 (newterm) = termDuplicateUV (TermOp1 (term));
|
||||
TermOp2 (newterm) = termDuplicateUV (TermOp2 (term));
|
||||
}
|
||||
return newterm;
|
||||
}
|
||||
@ -534,13 +533,13 @@ realTermDuplicate (const Term term)
|
||||
newterm->type = term->type;
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
TermOp(newterm) = realTermDuplicate (TermOp(term));
|
||||
TermKey(newterm) = realTermDuplicate (TermKey(term));
|
||||
TermOp (newterm) = realTermDuplicate (TermOp (term));
|
||||
TermKey (newterm) = realTermDuplicate (TermKey (term));
|
||||
}
|
||||
else
|
||||
{
|
||||
TermOp1(newterm) = realTermDuplicate (TermOp1(term));
|
||||
TermOp2(newterm) = realTermDuplicate (TermOp2(term));
|
||||
TermOp1 (newterm) = realTermDuplicate (TermOp1 (term));
|
||||
TermOp2 (newterm) = realTermDuplicate (TermOp2 (term));
|
||||
}
|
||||
}
|
||||
return newterm;
|
||||
@ -560,13 +559,13 @@ termDelete (const Term term)
|
||||
{
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
termDelete (TermOp(term));
|
||||
termDelete (TermKey(term));
|
||||
termDelete (TermOp (term));
|
||||
termDelete (TermKey (term));
|
||||
}
|
||||
else
|
||||
{
|
||||
termDelete (TermOp1(term));
|
||||
termDelete (TermOp2(term));
|
||||
termDelete (TermOp1 (term));
|
||||
termDelete (TermOp2 (term));
|
||||
}
|
||||
memFree (term, sizeof (struct term));
|
||||
}
|
||||
@ -589,29 +588,29 @@ termNormalize (Term term)
|
||||
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
termNormalize (TermOp(term));
|
||||
termNormalize (TermKey(term));
|
||||
termNormalize (TermOp (term));
|
||||
termNormalize (TermKey (term));
|
||||
}
|
||||
else
|
||||
{
|
||||
/* normalize left hand first,both for tupling and for
|
||||
encryption */
|
||||
termNormalize (TermOp1(term));
|
||||
termNormalize (TermOp1 (term));
|
||||
/* check for ((x,y),z) construct */
|
||||
if (realTermTuple (TermOp1(term)))
|
||||
if (realTermTuple (TermOp1 (term)))
|
||||
{
|
||||
/* temporarily store the old terms */
|
||||
Term tx = TermOp1(TermOp1(term));
|
||||
Term ty = TermOp2(TermOp1(term));
|
||||
Term tz = TermOp2(term);
|
||||
Term tx = TermOp1 (TermOp1 (term));
|
||||
Term ty = TermOp2 (TermOp1 (term));
|
||||
Term tz = TermOp2 (term);
|
||||
/* move node */
|
||||
TermOp2(term) = TermOp1(term);
|
||||
TermOp2 (term) = TermOp1 (term);
|
||||
/* construct (x,(y,z)) version */
|
||||
TermOp1(term) = tx;
|
||||
TermOp1(TermOp2(term)) = ty;
|
||||
TermOp2(TermOp2(term)) = tz;
|
||||
TermOp1 (term) = tx;
|
||||
TermOp1 (TermOp2 (term)) = ty;
|
||||
TermOp2 (TermOp2 (term)) = tz;
|
||||
}
|
||||
termNormalize (TermOp2(term));
|
||||
termNormalize (TermOp2 (term));
|
||||
}
|
||||
}
|
||||
|
||||
@ -629,12 +628,12 @@ termRunid (Term term, int runid)
|
||||
if (realTermLeaf (term))
|
||||
{
|
||||
/* leaf */
|
||||
if (TermRunid(term) == runid)
|
||||
if (TermRunid (term) == runid)
|
||||
return term;
|
||||
else
|
||||
{
|
||||
Term newt = termDuplicate (term);
|
||||
TermRunid(newt) = runid;
|
||||
TermRunid (newt) = runid;
|
||||
return newt;
|
||||
}
|
||||
}
|
||||
@ -643,13 +642,13 @@ termRunid (Term term, int runid)
|
||||
/* anything else, recurse */
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
return makeTermEncrypt (termRunid (TermOp(term), runid),
|
||||
termRunid (TermKey(term), runid));
|
||||
return makeTermEncrypt (termRunid (TermOp (term), runid),
|
||||
termRunid (TermKey (term), runid));
|
||||
}
|
||||
else
|
||||
{
|
||||
return makeTermTuple (termRunid (TermOp1(term), runid),
|
||||
termRunid (TermOp2(term), runid));
|
||||
return makeTermTuple (termRunid (TermOp1 (term), runid),
|
||||
termRunid (TermOp2 (term), runid));
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -674,7 +673,7 @@ tupleCount (Term tt)
|
||||
}
|
||||
else
|
||||
{
|
||||
return (tupleCount (TermOp1(tt)) + tupleCount (TermOp2(tt)));
|
||||
return (tupleCount (TermOp1 (tt)) + tupleCount (TermOp2 (tt)));
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -710,16 +709,16 @@ tupleProject (Term tt, int n)
|
||||
else
|
||||
{
|
||||
/* there is a tuple to traverse */
|
||||
int left = tupleCount (TermOp1(tt));
|
||||
int left = tupleCount (TermOp1 (tt));
|
||||
if (n >= left)
|
||||
{
|
||||
/* it's in the right hand side */
|
||||
return tupleProject (TermOp2(tt), n - left);
|
||||
return tupleProject (TermOp2 (tt), n - left);
|
||||
}
|
||||
else
|
||||
{
|
||||
/* left hand side */
|
||||
return tupleProject (TermOp1(tt), n);
|
||||
return tupleProject (TermOp1 (tt), n);
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -749,11 +748,11 @@ termSize (Term t)
|
||||
{
|
||||
if (realTermEncrypt (t))
|
||||
{
|
||||
return 1 + termSize (TermOp(t)) + termSize (TermKey(t));
|
||||
return 1 + termSize (TermOp (t)) + termSize (TermKey (t));
|
||||
}
|
||||
else
|
||||
{
|
||||
return termSize (TermOp1(t)) + termSize (TermOp2(t));
|
||||
return termSize (TermOp1 (t)) + termSize (TermOp2 (t));
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -811,13 +810,13 @@ termDistance (Term t1, Term t2)
|
||||
if (isTermEncrypt (t1))
|
||||
{
|
||||
/* encryption */
|
||||
return (termDistance (TermOp(t1), TermOp(t2)) +
|
||||
termDistance (TermKey(t1), TermKey(t2))) / 2;
|
||||
return (termDistance (TermOp (t1), TermOp (t2)) +
|
||||
termDistance (TermKey (t1), TermKey (t2))) / 2;
|
||||
}
|
||||
else
|
||||
{
|
||||
return (termDistance (TermOp1(t1), TermOp1(t2)) +
|
||||
termDistance (TermOp2(t1), TermOp2(t2))) / 2;
|
||||
return (termDistance (TermOp1 (t1), TermOp1 (t2)) +
|
||||
termDistance (TermOp2 (t1), TermOp2 (t2))) / 2;
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -859,7 +858,7 @@ termOrder (Term t1, Term t2)
|
||||
/* compare names */
|
||||
int comp;
|
||||
|
||||
comp = strcmp (TermSymb(t1)->text, TermSymb(t2)->text);
|
||||
comp = strcmp (TermSymb (t1)->text, TermSymb (t2)->text);
|
||||
if (comp != 0)
|
||||
{
|
||||
/* names differ */
|
||||
@ -868,14 +867,14 @@ termOrder (Term t1, Term t2)
|
||||
else
|
||||
{
|
||||
/* equal names, compare run identifiers */
|
||||
if (TermRunid(t1) == TermRunid(t2))
|
||||
if (TermRunid (t1) == TermRunid (t2))
|
||||
{
|
||||
error
|
||||
("termOrder: two terms seem to be identical although local precondition says they aren't.");
|
||||
}
|
||||
else
|
||||
{
|
||||
if (TermRunid(t1) < TermRunid(t2))
|
||||
if (TermRunid (t1) < TermRunid (t2))
|
||||
return -1;
|
||||
else
|
||||
return 1;
|
||||
@ -889,13 +888,13 @@ termOrder (Term t1, Term t2)
|
||||
|
||||
if (isTermEncrypt (t1))
|
||||
{
|
||||
compL = termOrder (TermOp(t1), TermOp(t2));
|
||||
compR = termOrder (TermKey(t1), TermKey(t2));
|
||||
compL = termOrder (TermOp (t1), TermOp (t2));
|
||||
compR = termOrder (TermKey (t1), TermKey (t2));
|
||||
}
|
||||
else
|
||||
{
|
||||
compL = termOrder (TermOp1(t1), TermOp1(t2));
|
||||
compR = termOrder (TermOp2(t1), TermOp2(t2));
|
||||
compL = termOrder (TermOp1 (t1), TermOp1 (t2));
|
||||
compR = termOrder (TermOp2 (t1), TermOp2 (t2));
|
||||
}
|
||||
if (compL != 0)
|
||||
return compL;
|
||||
@ -931,10 +930,10 @@ term_iterate (const Term term, int (*leaf) (), int (*nodel) (),
|
||||
// Left part
|
||||
if (realTermTuple (term))
|
||||
flag = flag
|
||||
&& (term_iterate (TermOp1(term), leaf, nodel, nodem, noder));
|
||||
&& (term_iterate (TermOp1 (term), leaf, nodel, nodem, noder));
|
||||
else
|
||||
flag = flag
|
||||
&& (term_iterate (TermOp(term), leaf, nodel, nodem, noder));
|
||||
&& (term_iterate (TermOp (term), leaf, nodel, nodem, noder));
|
||||
|
||||
if (nodem != NULL)
|
||||
flag = flag && nodem (term);
|
||||
@ -942,10 +941,10 @@ term_iterate (const Term term, int (*leaf) (), int (*nodel) (),
|
||||
// Right part
|
||||
if (realTermTuple (term))
|
||||
flag = flag
|
||||
&& (term_iterate (TermOp2(term), leaf, nodel, nodem, noder));
|
||||
&& (term_iterate (TermOp2 (term), leaf, nodel, nodem, noder));
|
||||
else
|
||||
flag = flag
|
||||
&& (term_iterate (TermKey(term), leaf, nodel, nodem, noder));
|
||||
&& (term_iterate (TermKey (term), leaf, nodel, nodem, noder));
|
||||
|
||||
if (noder != NULL)
|
||||
flag = flag && noder (term);
|
||||
@ -990,11 +989,11 @@ term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
|
||||
flag = flag
|
||||
&&
|
||||
(term_iterate_deVar
|
||||
(TermOp1(term), leaf, nodel, nodem, noder));
|
||||
(TermOp1 (term), leaf, nodel, nodem, noder));
|
||||
else
|
||||
flag = flag
|
||||
&&
|
||||
(term_iterate_deVar (TermOp(term), leaf, nodel, nodem, noder));
|
||||
(term_iterate_deVar (TermOp (term), leaf, nodel, nodem, noder));
|
||||
|
||||
if (nodem != NULL)
|
||||
flag = flag && nodem (term);
|
||||
@ -1004,11 +1003,12 @@ term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
|
||||
flag = flag
|
||||
&&
|
||||
(term_iterate_deVar
|
||||
(TermOp2(term), leaf, nodel, nodem, noder));
|
||||
(TermOp2 (term), leaf, nodel, nodem, noder));
|
||||
else
|
||||
flag = flag
|
||||
&&
|
||||
(term_iterate_deVar (TermKey(term), leaf, nodel, nodem, noder));
|
||||
(term_iterate_deVar
|
||||
(TermKey (term), leaf, nodel, nodem, noder));
|
||||
|
||||
if (noder != NULL)
|
||||
flag = flag && noder (term);
|
||||
@ -1037,11 +1037,11 @@ term_iterate_leaves (const Term term, int (*func) ())
|
||||
else
|
||||
{
|
||||
if (realTermTuple (term))
|
||||
return (term_iterate_leaves (TermOp1(term), func)
|
||||
&& term_iterate_leaves (TermOp2(term), func));
|
||||
return (term_iterate_leaves (TermOp1 (term), func)
|
||||
&& term_iterate_leaves (TermOp2 (term), func));
|
||||
else
|
||||
return (term_iterate_leaves (TermOp(term), func)
|
||||
&& term_iterate_leaves (TermKey(term), func));
|
||||
return (term_iterate_leaves (TermOp (term), func)
|
||||
&& term_iterate_leaves (TermKey (term), func));
|
||||
}
|
||||
}
|
||||
return 1;
|
||||
@ -1078,32 +1078,32 @@ int
|
||||
term_encryption_level (const Term term)
|
||||
{
|
||||
int iter_maxencrypt (Term term)
|
||||
{
|
||||
term = deVar (term);
|
||||
if (realTermLeaf (term))
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (realTermTuple (term))
|
||||
{
|
||||
int l,r;
|
||||
{
|
||||
term = deVar (term);
|
||||
if (realTermLeaf (term))
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (realTermTuple (term))
|
||||
{
|
||||
int l, r;
|
||||
|
||||
l = iter_maxencrypt (TermOp1(term));
|
||||
r = iter_maxencrypt (TermOp2(term));
|
||||
if (l>r)
|
||||
return l;
|
||||
else
|
||||
return r;
|
||||
}
|
||||
else
|
||||
{
|
||||
// encrypt
|
||||
return 1+iter_maxencrypt (TermOp(term));
|
||||
}
|
||||
}
|
||||
}
|
||||
l = iter_maxencrypt (TermOp1 (term));
|
||||
r = iter_maxencrypt (TermOp2 (term));
|
||||
if (l > r)
|
||||
return l;
|
||||
else
|
||||
return r;
|
||||
}
|
||||
else
|
||||
{
|
||||
// encrypt
|
||||
return 1 + iter_maxencrypt (TermOp (term));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return iter_maxencrypt (term);
|
||||
}
|
||||
@ -1134,13 +1134,13 @@ term_constrain_level (const Term term)
|
||||
{
|
||||
if (realTermTuple (t))
|
||||
{
|
||||
tcl_iterate (TermOp1(t));
|
||||
tcl_iterate (TermOp2(t));
|
||||
tcl_iterate (TermOp1 (t));
|
||||
tcl_iterate (TermOp2 (t));
|
||||
}
|
||||
else
|
||||
{
|
||||
tcl_iterate (TermOp(t));
|
||||
tcl_iterate (TermKey(t));
|
||||
tcl_iterate (TermOp (t));
|
||||
tcl_iterate (TermKey (t));
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -1184,7 +1184,7 @@ term_set_keylevels (const Term term)
|
||||
Symbol sym;
|
||||
|
||||
// So, it occurs at 'level' as key. If that is less than known, store.
|
||||
sym = TermSymb(t);
|
||||
sym = TermSymb (t);
|
||||
if (level < sym->keylevel)
|
||||
{
|
||||
// New minimum level
|
||||
@ -1195,13 +1195,13 @@ term_set_keylevels (const Term term)
|
||||
{
|
||||
if (realTermTuple (t))
|
||||
{
|
||||
scan_levels (level, TermOp1(t));
|
||||
scan_levels (level, TermOp2(t));
|
||||
scan_levels (level, TermOp1 (t));
|
||||
scan_levels (level, TermOp2 (t));
|
||||
}
|
||||
else
|
||||
{
|
||||
scan_levels (level, TermOp(t));
|
||||
scan_levels ((level + 1), TermKey(t));
|
||||
scan_levels (level, TermOp (t));
|
||||
scan_levels ((level + 1), TermKey (t));
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -1220,16 +1220,16 @@ termPrintDiff (Term t1, Term t2)
|
||||
t2 = deVar (t2);
|
||||
|
||||
void termFromTo (Term t1, Term t2)
|
||||
{
|
||||
t1 = deVar (t1);
|
||||
t2 = deVar (t2);
|
||||
{
|
||||
t1 = deVar (t1);
|
||||
t2 = deVar (t2);
|
||||
|
||||
eprintf (" [");
|
||||
termPrint (t1);
|
||||
eprintf ("]->[");
|
||||
termPrint (t2);
|
||||
eprintf ("] ");
|
||||
}
|
||||
eprintf (" [");
|
||||
termPrint (t1);
|
||||
eprintf ("]->[");
|
||||
termPrint (t2);
|
||||
eprintf ("] ");
|
||||
}
|
||||
|
||||
if (isTermEqual (t1, t2))
|
||||
{
|
||||
@ -1241,7 +1241,7 @@ termPrintDiff (Term t1, Term t2)
|
||||
if (t1->type != t2->type)
|
||||
{
|
||||
// Different types
|
||||
termFromTo (t1,t2);
|
||||
termFromTo (t1, t2);
|
||||
}
|
||||
else
|
||||
{
|
||||
@ -1257,31 +1257,33 @@ termPrintDiff (Term t1, Term t2)
|
||||
if (realTermEncrypt (t1))
|
||||
{
|
||||
// Encryption
|
||||
if (isTermEqual (TermOp(t1), TermOp(t2)) || isTermEqual (TermKey(t1), TermKey(t2)))
|
||||
if (isTermEqual (TermOp (t1), TermOp (t2))
|
||||
|| isTermEqual (TermKey (t1), TermKey (t2)))
|
||||
{
|
||||
eprintf ("{");
|
||||
termPrintDiff (TermOp(t1), TermOp(t2));
|
||||
termPrintDiff (TermOp (t1), TermOp (t2));
|
||||
eprintf ("}");
|
||||
termPrintDiff (TermKey(t1), TermKey(t2));
|
||||
termPrintDiff (TermKey (t1), TermKey (t2));
|
||||
}
|
||||
else
|
||||
{
|
||||
termFromTo (t1,t2);
|
||||
termFromTo (t1, t2);
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// Tupling
|
||||
if (isTermEqual (TermOp1(t1), TermOp1(t2)) || isTermEqual (TermOp2(t1), TermOp2(t2)))
|
||||
if (isTermEqual (TermOp1 (t1), TermOp1 (t2))
|
||||
|| isTermEqual (TermOp2 (t1), TermOp2 (t2)))
|
||||
{
|
||||
eprintf ("(");
|
||||
termPrintDiff (TermOp1(t1), TermOp1(t2));
|
||||
termPrintDiff (TermOp1 (t1), TermOp1 (t2));
|
||||
eprintf (")");
|
||||
termPrintDiff (TermOp2(t1), TermOp2(t2));
|
||||
termPrintDiff (TermOp2 (t1), TermOp2 (t2));
|
||||
}
|
||||
else
|
||||
{
|
||||
termFromTo (t1,t2);
|
||||
termFromTo (t1, t2);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -412,12 +412,12 @@ termlistAddVariables (Termlist tl, Term t)
|
||||
else
|
||||
{
|
||||
if (isTermEncrypt (t))
|
||||
return termlistAddVariables (termlistAddVariables (tl, TermOp(t)),
|
||||
TermKey(t));
|
||||
return termlistAddVariables (termlistAddVariables (tl, TermOp (t)),
|
||||
TermKey (t));
|
||||
else
|
||||
return
|
||||
termlistAddVariables (termlistAddVariables (tl, TermOp1(t)),
|
||||
TermOp2(t));
|
||||
termlistAddVariables (termlistAddVariables (tl, TermOp1 (t)),
|
||||
TermOp2 (t));
|
||||
}
|
||||
}
|
||||
|
||||
@ -455,12 +455,12 @@ termlistAddRealVariables (Termlist tl, Term t)
|
||||
else
|
||||
{
|
||||
if (realTermEncrypt (t))
|
||||
return termlistAddVariables (termlistAddVariables (tl, TermOp(t)),
|
||||
TermKey(t));
|
||||
return termlistAddVariables (termlistAddVariables (tl, TermOp (t)),
|
||||
TermKey (t));
|
||||
else
|
||||
return
|
||||
termlistAddVariables (termlistAddVariables (tl, TermOp1(t)),
|
||||
TermOp2(t));
|
||||
termlistAddVariables (termlistAddVariables (tl, TermOp1 (t)),
|
||||
TermOp2 (t));
|
||||
}
|
||||
}
|
||||
|
||||
@ -479,11 +479,11 @@ termlistAddBasic (Termlist tl, Term t)
|
||||
if (!isTermLeaf (t))
|
||||
{
|
||||
if (isTermEncrypt (t))
|
||||
return termlistAddBasic (termlistAddBasic (tl, TermOp(t)),
|
||||
TermKey(t));
|
||||
return termlistAddBasic (termlistAddBasic (tl, TermOp (t)),
|
||||
TermKey (t));
|
||||
else
|
||||
return termlistAddBasic (termlistAddBasic (tl, TermOp1(t)),
|
||||
TermOp2(t));
|
||||
return termlistAddBasic (termlistAddBasic (tl, TermOp1 (t)),
|
||||
TermOp2 (t));
|
||||
}
|
||||
else
|
||||
{
|
||||
@ -571,8 +571,8 @@ inverseKey (Termlist inverses, Term key)
|
||||
return termDuplicate (TERM_Hidden);
|
||||
}
|
||||
/* check for the special case first: when it is effectively a function application */
|
||||
if (isTermEncrypt (key) && isTermLeaf (TermKey(key))
|
||||
&& inTermlist (deVar (TermKey(key))->stype, TERM_Function))
|
||||
if (isTermEncrypt (key) && isTermLeaf (TermKey (key))
|
||||
&& inTermlist (deVar (TermKey (key))->stype, TERM_Function))
|
||||
{
|
||||
/* we are scanning for functions */
|
||||
/* scan the list */
|
||||
@ -581,15 +581,15 @@ inverseKey (Termlist inverses, Term key)
|
||||
{
|
||||
/* in: {op}kk, nk
|
||||
* out: {op'}nk */
|
||||
return makeTermEncrypt (termDuplicate (TermOp(orig)),
|
||||
return makeTermEncrypt (termDuplicate (TermOp (orig)),
|
||||
termDuplicate (newk));
|
||||
}
|
||||
while (inverses != NULL && inverses->next != NULL)
|
||||
{
|
||||
|
||||
if (isTermEqual (TermKey(key), inverses->term))
|
||||
if (isTermEqual (TermKey (key), inverses->term))
|
||||
return funKey (key, inverses->next->term);
|
||||
if (isTermEqual (TermKey(key), inverses->next->term))
|
||||
if (isTermEqual (TermKey (key), inverses->next->term))
|
||||
return funKey (key, inverses->term);
|
||||
inverses = inverses->next->next;
|
||||
}
|
||||
@ -645,13 +645,13 @@ termLocal (Term t, Termlist fromlist, Termlist tolist, const int runid)
|
||||
Term newt = termNodeDuplicate (t);
|
||||
if (realTermTuple (t))
|
||||
{
|
||||
TermOp1(newt) = termLocal (TermOp1(t), fromlist, tolist, runid);
|
||||
TermOp2(newt) = termLocal (TermOp2(t), fromlist, tolist, runid);
|
||||
TermOp1 (newt) = termLocal (TermOp1 (t), fromlist, tolist, runid);
|
||||
TermOp2 (newt) = termLocal (TermOp2 (t), fromlist, tolist, runid);
|
||||
}
|
||||
else
|
||||
{
|
||||
TermOp(newt) = termLocal (TermOp(t), fromlist, tolist, runid);
|
||||
TermKey(newt) = termLocal (TermKey(t), fromlist, tolist, runid);
|
||||
TermOp (newt) = termLocal (TermOp (t), fromlist, tolist, runid);
|
||||
TermKey (newt) = termLocal (TermKey (t), fromlist, tolist, runid);
|
||||
}
|
||||
return newt;
|
||||
}
|
||||
|
@ -111,7 +111,8 @@ warshall (int *graph, int nodes)
|
||||
/**
|
||||
* Some crude algorithm I sketched on the blackboard.
|
||||
*/
|
||||
int graph_ranks (int *graph, int *ranks, int nodes)
|
||||
int
|
||||
graph_ranks (int *graph, int *ranks, int nodes)
|
||||
{
|
||||
int i;
|
||||
int todo;
|
||||
@ -142,10 +143,11 @@ int graph_ranks (int *graph, int *ranks, int nodes)
|
||||
refn = 0;
|
||||
while (refn < nodes)
|
||||
{
|
||||
if (ranks[refn] >= rank && graph[graph_index(refn, n)] != 0)
|
||||
refn = nodes+1;
|
||||
if (ranks[refn] >= rank
|
||||
&& graph[graph_index (refn, n)] != 0)
|
||||
refn = nodes + 1;
|
||||
else
|
||||
refn++;
|
||||
refn++;
|
||||
}
|
||||
if (refn == nodes)
|
||||
{
|
||||
|
Loading…
Reference in New Issue
Block a user