andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Removing a collection of fairly simple remaining nested function calls.

Browse Source
This commit is contained in:
Cas Cremers 2019-01-04 17:16:27 +01:00
parent d25445538e
commit d4ec0004d6
9 changed files with 558 additions and 528 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

50
src/binding.c
View File

@ -300,6 +300,28 @@ goal_remove_last (int n)
} }
} }
//! Get index of run
int
get_index (const int run, const Term label)
{
Roledef rd;
int i;
i = 0;
rd = sys->runs[run].start;
while (rd != NULL && !isTermEqual (rd->label, label))
{
rd = rd->next;
i++;
}
#ifdef DEBUG
if (rd == NULL)
error
("Could not locate send or recv for label, after niagree holds, to test for order.");
#endif
return i;
}
//! Determine whether some label set is ordered w.r.t. send/recv order. //! Determine whether some label set is ordered w.r.t. send/recv order.
/** /**
* Assumes all these labels exist in the system, within length etc, and that the run mappings are valid. * Assumes all these labels exist in the system, within length etc, and that the run mappings are valid.
@ -312,34 +334,16 @@ labels_ordered (Termmap runs, Termlist labels)
// Given this label, and the mapping of runs, we want to know if the order is okay. Thus, we need to know sendrole and recvrole // Given this label, and the mapping of runs, we want to know if the order is okay. Thus, we need to know sendrole and recvrole
Labelinfo linfo; Labelinfo linfo;
int send_run, send_ev, recv_run, recv_ev; int send_run, send_ev, recv_run, recv_ev;
Term label;
int get_index (const int run) label = labels->term;
{ linfo = label_find (sys->labellist, label);
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 recv for label, after niagree holds, to test for order.");
#endif
return i;
}
linfo = label_find (sys->labellist, labels->term);
if (!linfo->ignore) if (!linfo->ignore)
{ {
send_run = termmapGet (runs, linfo->sendrole); send_run = termmapGet (runs, linfo->sendrole);
recv_run = termmapGet (runs, linfo->recvrole); recv_run = termmapGet (runs, linfo->recvrole);
send_ev = get_index (send_run); send_ev = get_index (send_run, label);
recv_ev = get_index (recv_run); recv_ev = get_index (recv_run, label);
if (!isDependEvent (send_run, send_ev, recv_run, recv_ev)) if (!isDependEvent (send_run, send_ev, recv_run, recv_ev))
{ {
// Not ordered; false // Not ordered; false

109
src/claim.c
View File

@ -514,7 +514,59 @@ check_claim_niagree (const System sys, const int i)
return result; return result;
} }
//! Get label event
Roledef
get_label_event (const System sys, const Labelinfo linfo, const Term role,
const Term label, const Termmap runs)
{
Roledef rd, rd_res;
int i;
int run;
run = termmapGet (runs, role);
if (run != -1)
{
#ifdef DEBUG
if (run < 0 || run >= sys->maxruns)
{
globalError++;
eprintf ("Run mapping %i out of bounds for role ", run);
termPrint (role);
eprintf (" and label ");
termPrint (label);
eprintf ("\n");
eprintf ("This label has sendrole ");
termPrint (linfo->sendrole);
eprintf (" and recvrole ");
termPrint (linfo->recvrole);
eprintf ("\n");
globalError--;
error ("Run mapping is out of bounds.");
}
#endif
rd = sys->runs[run].start;
rd_res = NULL;
i = 0;
while (i < sys->runs[run].step && rd != NULL)
{
if (isTermEqual (rd->label, label))
{
rd_res = rd;
rd = NULL;
}
else
{
rd = rd->next;
}
i++;
}
return rd_res;
}
else
{
return NULL;
}
}
//! Check generic agree claim for a given set of runs, arachne style //! Check generic agree claim for a given set of runs, arachne style
int int
@ -541,63 +593,14 @@ arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs)
Roledef rd_send, rd_recv; Roledef rd_send, rd_recv;
Labelinfo linfo; Labelinfo linfo;
Roledef get_label_event (const Term role, const Term label)
{
Roledef rd, rd_res;
int i;
int run;
run = termmapGet (runs, role);
if (run != -1)
{
#ifdef DEBUG
if (run < 0 || run >= sys->maxruns)
{
globalError++;
eprintf ("Run mapping %i out of bounds for role ", run);
termPrint (role);
eprintf (" and label ");
termPrint (label);
eprintf ("\n");
eprintf ("This label has sendrole ");
termPrint (linfo->sendrole);
eprintf (" and recvrole ");
termPrint (linfo->recvrole);
eprintf ("\n");
globalError--;
error ("Run mapping is out of bounds.");
}
#endif
rd = sys->runs[run].start;
rd_res = NULL;
i = 0;
while (i < sys->runs[run].step && rd != NULL)
{
if (isTermEqual (rd->label, label))
{
rd_res = rd;
rd = NULL;
}
else
{
rd = rd->next;
}
i++;
}
return rd_res;
}
else
{
return NULL;
}
}
// Main // Main
linfo = label_find (sys->labellist, labels->term); linfo = label_find (sys->labellist, labels->term);
if (!linfo->ignore) if (!linfo->ignore)
{ {
rd_send = get_label_event (linfo->sendrole, labels->term); rd_send =
rd_recv = get_label_event (linfo->recvrole, labels->term); get_label_event (sys, linfo, linfo->sendrole, labels->term, runs);
rd_recv =
get_label_event (sys, linfo, linfo->recvrole, labels->term, runs);
if (rd_send == NULL || rd_recv == NULL) if (rd_send == NULL || rd_recv == NULL)
{ {

302
src/compiler.c
View File

@ -1183,31 +1183,33 @@ normalDeclaration (Tac tc)
return 1; return 1;
} }
/* first: secrecy claims for all locally declared things */
void
addSecrecyList (const System sys, const Protocol protocol, const Role role,
Termlist tl)
{
while (tl != NULL)
{
Term t;
t = deVar (tl->term);
if (realTermLeaf (t))
{
// Add a secrecy claim
claimCreate (sys, protocol, role, CLAIM_Secret, NULL, t, -1);
}
tl = tl->next;
}
}
//! Add all sorts of claims to this role //! Add all sorts of claims to this role
void void
claimAddAll (const System sys, const Protocol protocol, const Role role) claimAddAll (const System sys, const Protocol protocol, const Role role)
{ {
/* first: secrecy claims for all locally declared things */
void addSecrecyList (Termlist tl)
{
while (tl != NULL)
{
Term t;
t = deVar (tl->term);
if (realTermLeaf (t))
{
// Add a secrecy claim
claimCreate (sys, protocol, role, CLAIM_Secret, NULL, t, -1);
}
tl = tl->next;
}
}
if (!isHelperProtocol (protocol)) if (!isHelperProtocol (protocol))
{ {
addSecrecyList (role->declaredconsts); addSecrecyList (sys, protocol, role, role->declaredconsts);
addSecrecyList (role->declaredvars); addSecrecyList (sys, protocol, role, role->declaredvars);
/* full non-injective agreement and ni-synch */ /* full non-injective agreement and ni-synch */
claimCreate (sys, protocol, role, CLAIM_Alive, NULL, NULL, -1); claimCreate (sys, protocol, role, CLAIM_Alive, NULL, NULL, -1);
@ -1699,6 +1701,26 @@ compute_label_roles (Termlist labels)
return roles; return roles;
} }
// This function checks whether the newrole can connect to the connectedrole, and whether they fulfil their requirements.
int
roles_test (const Termlist roles_ordered, const Termlist roles_remaining,
const Term connectedrole, const Term newrole)
{
if (inTermlist (roles_ordered, connectedrole) &&
inTermlist (roles_remaining, newrole))
{
#ifdef DEBUG
if (DEBUGL (4))
{
eprintf (" ");
termPrint (newrole);
}
#endif
return true;
}
return false;
}
//! Order the label roles for a given claim //! Order the label roles for a given claim
void void
order_label_roles (const Claimlist cl) order_label_roles (const Claimlist cl)
@ -1749,30 +1771,28 @@ order_label_roles (const Claimlist cl)
{ {
// If it's not the same protocol, the labels can't match // 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. if (roles_test
void roles_test (const Term connectedrole, (roles_ordered, roles_remaining, linfo->sendrole,
const Term newrole) linfo->recvrole))
{ {
if (inTermlist (roles_ordered, connectedrole) && roles_ordered =
inTermlist (roles_remaining, newrole)) termlistAppend (roles_ordered, linfo->recvrole);
{ roles_remaining =
#ifdef DEBUG termlistDelTerm (termlistFind
if (DEBUGL (4)) (roles_remaining,
{ linfo->recvrole));
eprintf (" "); }
termPrint (newrole); if (roles_test
} (roles_ordered, roles_remaining, linfo->recvrole,
#endif linfo->sendrole))
roles_ordered = {
termlistAppend (roles_ordered, newrole); roles_ordered =
roles_remaining = termlistAppend (roles_ordered, linfo->sendrole);
termlistDelTerm (termlistFind roles_remaining =
(roles_remaining, newrole)); termlistDelTerm (termlistFind
} (roles_remaining,
} linfo->sendrole));
}
roles_test (linfo->sendrole, linfo->recvrole);
roles_test (linfo->recvrole, linfo->sendrole);
} }
} }
} }
@ -1788,6 +1808,84 @@ order_label_roles (const Claimlist cl)
#endif #endif
} }
// Assist: compute m_index from role, lev
int
m_index (const System sys, const int r, const int lev)
{
return r * sys->roleeventmax + lev;
}
// Assist: yield roledef from r, lev
Roledef
roledef_re (const System sys, int r, int lev)
{
Protocol pr;
Role ro;
Roledef rd;
pr = sys->protocols;
ro = pr->roles;
while (r > 0 && ro != NULL)
{
ro = ro->next;
if (ro == NULL)
{
pr = pr->next;
if (pr != NULL)
{
ro = pr->roles;
}
else
{
ro = NULL;
}
}
r--;
}
if (ro != NULL)
{
rd = ro->roledef;
while (lev > 0 && rd != NULL)
{
rd = rd->next;
lev--;
}
return rd;
}
else
{
return NULL;
}
}
//! Assist: print matrix
void
show_matrix (const System sys, const int rowsize, const unsigned int *prec)
{
int r1, r2, ev1, ev2;
for (r1 = 0; r1 < sys->rolecount; r1++)
{
for (ev1 = 0; ev1 < sys->roleeventmax; ev1++)
{
eprintf ("prec %i,%i: ", r1, ev1);
for (r2 = 0; r2 < sys->rolecount; r2++)
{
for (ev2 = 0; ev2 < sys->roleeventmax; ev2++)
{
eprintf ("%i ",
BIT (prec + rowsize * m_index (sys, r2, ev2),
m_index (sys, r1, ev1)));
}
eprintf (" ");
}
eprintf ("\n");
}
eprintf ("\n");
}
eprintf ("\n");
}
//! Compute prec() sets for each claim. //! Compute prec() sets for each claim.
/** /**
* Generates two auxiliary structures. First, a table that contains * Generates two auxiliary structures. First, a table that contains
@ -1808,89 +1906,6 @@ compute_prec_sets (const System sys)
int r1, r2, ev1, ev2; // some counters int r1, r2, ev1, ev2; // some counters
Claimlist cl; Claimlist cl;
// Assist: compute index from role, lev
int index (int r, int lev)
{
return r * sys->roleeventmax + lev;
}
// Assist: yield roledef from r, lev
Roledef roledef_re (int r, int lev)
{
Protocol pr;
Role ro;
Roledef rd;
pr = sys->protocols;
ro = pr->roles;
while (r > 0 && ro != NULL)
{
ro = ro->next;
if (ro == NULL)
{
pr = pr->next;
if (pr != NULL)
{
ro = pr->roles;
}
else
{
ro = NULL;
}
}
r--;
}
if (ro != NULL)
{
rd = ro->roledef;
while (lev > 0 && rd != NULL)
{
rd = rd->next;
lev--;
}
return rd;
}
else
{
return NULL;
}
}
// Assist: print matrix
void show_matrix (void)
{
int r1, r2, ev1, ev2;
r1 = 0;
while (r1 < sys->rolecount)
{
ev1 = 0;
while (ev1 < sys->roleeventmax)
{
eprintf ("prec %i,%i: ", r1, ev1);
r2 = 0;
while (r2 < sys->rolecount)
{
ev2 = 0;
while (ev2 < sys->roleeventmax)
{
eprintf ("%i ",
BIT (prec + rowsize * index (r2, ev2),
index (r1, ev1)));
ev2++;
}
eprintf (" ");
r2++;
}
eprintf ("\n");
ev1++;
}
eprintf ("\n");
r1++;
}
eprintf ("\n");
}
/* /*
* Phase 1: Allocate structures and map to labels * Phase 1: Allocate structures and map to labels
*/ */
@ -1907,10 +1922,10 @@ compute_prec_sets (const System sys)
Roledef rd; Roledef rd;
ev1 = 0; ev1 = 0;
rd = roledef_re (r1, ev1); rd = roledef_re (sys, r1, ev1);
while (rd != NULL) while (rd != NULL)
{ {
eventlabels[index (r1, ev1)] = rd->label; eventlabels[m_index (sys, r1, ev1)] = rd->label;
//termPrint (rd->label); //termPrint (rd->label);
//eprintf ("\t"); //eprintf ("\t");
ev1++; ev1++;
@ -1918,7 +1933,7 @@ compute_prec_sets (const System sys)
} }
while (ev1 < sys->roleeventmax) while (ev1 < sys->roleeventmax)
{ {
eventlabels[index (r1, ev1)] = NULL; eventlabels[m_index (sys, r1, ev1)] = NULL;
ev1++; ev1++;
} }
//eprintf ("\n"); //eprintf ("\n");
@ -1931,7 +1946,8 @@ compute_prec_sets (const System sys)
ev1 = 1; ev1 = 1;
while (ev1 < (sys->roleeventmax)) while (ev1 < (sys->roleeventmax))
{ {
SETBIT (prec + rowsize * index (r1, ev1 - 1), index (r1, ev1)); SETBIT (prec + rowsize * m_index (sys, r1, ev1 - 1),
m_index (sys, r1, ev1));
ev1++; ev1++;
} }
r1++; r1++;
@ -1945,7 +1961,7 @@ compute_prec_sets (const System sys)
{ {
Roledef rd1; Roledef rd1;
rd1 = roledef_re (r1, ev1); rd1 = roledef_re (sys, r1, ev1);
if (rd1 != NULL && rd1->type == SEND) if (rd1 != NULL && rd1->type == SEND)
{ {
r2 = 0; r2 = 0;
@ -1956,12 +1972,12 @@ compute_prec_sets (const System sys)
{ {
Roledef rd2; Roledef rd2;
rd2 = roledef_re (r2, ev2); rd2 = roledef_re (sys, r2, ev2);
if (rd2 != NULL && rd2->type == RECV if (rd2 != NULL && rd2->type == RECV
&& isTermEqual (rd1->label, rd2->label)) && isTermEqual (rd1->label, rd2->label))
{ {
SETBIT (prec + rowsize * index (r1, ev1), SETBIT (prec + rowsize * m_index (sys, r1, ev1),
index (r2, ev2)); m_index (sys, r2, ev2));
} }
ev2++; ev2++;
} }
@ -1976,7 +1992,7 @@ compute_prec_sets (const System sys)
#ifdef DEBUG #ifdef DEBUG
if (DEBUGL (5)) if (DEBUGL (5))
{ {
show_matrix (); show_matrix (sys, rowsize, prec);
} }
#endif #endif
@ -1988,7 +2004,7 @@ compute_prec_sets (const System sys)
#ifdef DEBUG #ifdef DEBUG
if (DEBUGL (5)) if (DEBUGL (5))
{ {
show_matrix (); show_matrix (sys, rowsize, prec);
} }
#endif #endif
@ -2016,14 +2032,14 @@ compute_prec_sets (const System sys)
} }
} }
while (r1 < sys->rolecount while (r1 < sys->rolecount
&& !isTermEqual (label, eventlabels[index (r1, ev1)])); && !isTermEqual (label, eventlabels[m_index (sys, r1, ev1)]));
if (r1 == sys->rolecount) if (r1 == sys->rolecount)
{ {
error error
("Prec() setup: Could not find the event corresponding to a claim label."); ("Prec() setup: Could not find the event corresponding to a claim label.");
} }
rd = roledef_re (r1, ev1); rd = roledef_re (sys, r1, ev1);
if (rd->type != CLAIM) if (rd->type != CLAIM)
{ {
error error
@ -2039,15 +2055,15 @@ compute_prec_sets (const System sys)
* Now we compute the preceding label set * Now we compute the preceding label set
*/ */
cl->prec = NULL; // clear first cl->prec = NULL; // clear first
claim_index = index (r1, ev1); claim_index = m_index (sys, r1, ev1);
r2 = 0; r2 = 0;
while (r2 < sys->rolecount) while (r2 < sys->rolecount)
{ {
ev2 = 0; ev2 = 0;
rd = roledef_re (r2, ev2); rd = roledef_re (sys, r2, ev2);
while (rd != NULL) while (rd != NULL)
{ {
if (BIT (prec + rowsize * index (r2, ev2), claim_index)) if (BIT (prec + rowsize * m_index (sys, r2, ev2), claim_index))
{ {
// This event precedes the claim // This event precedes the claim
@ -2118,12 +2134,12 @@ compute_prec_sets (const System sys)
{ {
// if this event preceds the claim, replace the label term // if this event preceds the claim, replace the label term
if (BIT if (BIT
(prec + rowsize * index (r_scan, ev_scan), (prec + rowsize * m_index (sys, r_scan, ev_scan),
claim_index)) claim_index))
{ {
Roledef rd; Roledef rd;
rd = roledef_re (r_scan, ev_scan); rd = roledef_re (sys, r_scan, ev_scan);
if (rd->label != NULL) if (rd->label != NULL)
{ {
t_buf = rd->label; t_buf = rd->label;

137
src/dotout.c
View File

@ -263,30 +263,31 @@ redirNode (const System sys, Binding b)
node (sys, b->run_to, b->ev_to); node (sys, b->run_to, b->ev_to);
} }
void
optlabel (const Roledef rd)
{
Term label;
label = rd->label;
if (label != NULL)
{
if (realTermTuple (label))
{
label = TermOp2 (label);
}
eprintf ("_");
termPrintRemap (label);
}
}
//! Roledef draw //! Roledef draw
void void
roledefDraw (Roledef rd) roledefDraw (Roledef rd)
{ {
void optlabel (void)
{
Term label;
label = rd->label;
if (label != NULL)
{
if (realTermTuple (label))
{
label = TermOp2 (label);
}
eprintf ("_");
termPrintRemap (label);
}
}
if (rd->type == RECV) if (rd->type == RECV)
{ {
eprintf ("recv"); eprintf ("recv");
optlabel (); optlabel (rd);
eprintf (" from "); eprintf (" from ");
termPrintRemap (rd->from); termPrintRemap (rd->from);
eprintf ("\\n"); eprintf ("\\n");
@ -295,7 +296,7 @@ roledefDraw (Roledef rd)
if (rd->type == SEND) if (rd->type == SEND)
{ {
eprintf ("send"); eprintf ("send");
optlabel (); optlabel (rd);
eprintf (" to "); eprintf (" to ");
termPrintRemap (rd->to); termPrintRemap (rd->to);
eprintf ("\\n"); eprintf ("\\n");
@ -304,7 +305,7 @@ roledefDraw (Roledef rd)
if (rd->type == CLAIM) if (rd->type == CLAIM)
{ {
eprintf ("claim"); eprintf ("claim");
optlabel (); optlabel (rd);
eprintf ("\\n"); eprintf ("\\n");
termPrintRemap (rd->to); termPrintRemap (rd->to);
if (rd->message != NULL) if (rd->message != NULL)
@ -348,25 +349,26 @@ hlsValue (double n1, double n2, double hue)
return n1; return n1;
} }
int
bytedouble (double d)
{
double x;
x = 255.0 * d;
if (x <= 0)
return 0;
else if (x >= 255.0)
return 255;
else
return (int) x;
}
//! hls to rgb conversion //! hls to rgb conversion
void void
hlsrgbreal (int *r, int *g, int *b, double h, double l, double s) hlsrgbreal (int *r, int *g, int *b, double h, double l, double s)
{ {
double m1, m2; double m1, m2;
int bytedouble (double d)
{
double x;
x = 255.0 * d;
if (x <= 0)
return 0;
else if (x >= 255.0)
return 255;
else
return (int) x;
}
while (h >= 360.0) while (h >= 360.0)
h -= 360.0; h -= 360.0;
while (h < 0) while (h < 0)
@ -385,6 +387,12 @@ hlsrgbreal (int *r, int *g, int *b, double h, double l, double s)
} }
} }
double
closer (double l, double factor)
{
return l + ((1.0 - l) * factor);
}
//! hls to rgb conversion //! hls to rgb conversion
/** /**
* Secretly takes the monochrome switch into account * Secretly takes the monochrome switch into account
@ -392,11 +400,6 @@ hlsrgbreal (int *r, int *g, int *b, double h, double l, double s)
void void
hlsrgb (int *r, int *g, int *b, double h, double l, double s) hlsrgb (int *r, int *g, int *b, double h, double l, double s)
{ {
double closer (double l, double factor)
{
return l + ((1.0 - l) * factor);
}
if (switches.monochrome) if (switches.monochrome)
{ {
// No colors // No colors
@ -432,6 +435,14 @@ printColor (double h, double l, double s)
eprintf ("#%02x%02x%02x", r, g, b); eprintf ("#%02x%02x%02x", r, g, b);
} }
// help function: contract roleoffset, roledelta with a factor (<= 1.0)
void
contract (double roledelta, double roleoffset, double factor)
{
roledelta = roledelta * factor;
roleoffset = (roleoffset * factor) + ((1.0 - factor) / 2.0);
}
//! Set local buffer with the correct color for this run. //! Set local buffer with the correct color for this run.
/** /**
@ -453,13 +464,6 @@ setRunColorBuf (const System sys, int run, char *colorbuf)
double h, l, s; double h, l, s;
int r, g, b; int r, g, b;
// help function: contract roleoffset, roledelta with a factor (<= 1.0)
void contract (double factor)
{
roledelta = roledelta * factor;
roleoffset = (roleoffset * factor) + ((1.0 - factor) / 2.0);
}
// determine #protocol, resulting in two colors // determine #protocol, resulting in two colors
{ {
Termlist protocols; Termlist protocols;
@ -547,12 +551,13 @@ setRunColorBuf (const System sys, int run, char *colorbuf)
// Now this can result in a delta that is too high (depending on protocolrange) // Now this can result in a delta that is too high (depending on protocolrange)
if (protrange * roledelta > RUNCOLORDELTA) if (protrange * roledelta > RUNCOLORDELTA)
{ {
contract (RUNCOLORDELTA / (protrange * roledelta)); contract (roledelta, roleoffset,
RUNCOLORDELTA / (protrange * roledelta));
} }
} }
// We slightly contract the colors (taking them away from protocol edges) // We slightly contract the colors (taking them away from protocol edges)
contract (RUNCOLORCONTRACT); contract (roledelta, roleoffset, RUNCOLORCONTRACT);
// Now we can convert this to a color // Now we can convert this to a color
color = protoffset + (protrange * roleoffset); color = protoffset + (protrange * roleoffset);
@ -1061,27 +1066,29 @@ regularModifiedLabel (Binding b)
} }
} }
void
myarrow (const System sys, const int m0_from, const Binding b)
{
if (m0_from)
{
eprintf ("\t");
intruderNodeM0 ();
eprintf (" -> ");
node (sys, b->run_to, b->ev_to);
}
else
{
arrow (sys, b);
}
}
//! Draw a single binding //! Draw a single binding
void void
drawBinding (const System sys, Binding b) drawBinding (const System sys, Binding b)
{ {
int intr_to, intr_from, m0_from; int intr_to, intr_from, m0_from;
void myarrow (const Binding b)
{
if (m0_from)
{
eprintf ("\t");
intruderNodeM0 ();
eprintf (" -> ");
node (sys, b->run_to, b->ev_to);
}
else
{
arrow (sys, b);
}
}
intr_from = (sys->runs[b->run_from].protocol == INTRUDER); intr_from = (sys->runs[b->run_from].protocol == INTRUDER);
intr_to = (sys->runs[b->run_to].protocol == INTRUDER); intr_to = (sys->runs[b->run_to].protocol == INTRUDER);
@ -1121,7 +1128,7 @@ drawBinding (const System sys, Binding b)
{ {
// intr->intr // intr->intr
eprintf ("\t"); eprintf ("\t");
myarrow (b); myarrow (sys, m0_from, b);
eprintf (" [label=\""); eprintf (" [label=\"");
termPrintRemap (b->term); termPrintRemap (b->term);
eprintf ("\""); eprintf ("\"");
@ -1136,7 +1143,7 @@ drawBinding (const System sys, Binding b)
{ {
// intr->regular // intr->regular
eprintf ("\t"); eprintf ("\t");
myarrow (b); myarrow (sys, m0_from, b);
if (m0_from) if (m0_from)
{ {
eprintf ("[weight=\"0.5\"]"); eprintf ("[weight=\"0.5\"]");
@ -1151,7 +1158,7 @@ drawBinding (const System sys, Binding b)
{ {
// regular->intr // regular->intr
eprintf ("\t"); eprintf ("\t");
myarrow (b); myarrow (sys, m0_from, b);
eprintf (";\n"); eprintf (";\n");
} }
else else
@ -1163,7 +1170,7 @@ drawBinding (const System sys, Binding b)
if (isCommunicationExact (sys, b)) if (isCommunicationExact (sys, b))
{ {
eprintf ("\t"); eprintf ("\t");
myarrow (b); myarrow (sys, m0_from, b);
eprintf (" [style=bold,color=\"%s\"]", GOODCOMMCOLOR); eprintf (" [style=bold,color=\"%s\"]", GOODCOMMCOLOR);
eprintf (";\n"); eprintf (";\n");
} }

31
src/intruderknowledge.c
View File

@ -56,36 +56,25 @@ addEnumTerm (const System sys, Term t, Term actor, Termlist todo,
{ {
if (termSubTerm (t, todo->term)) if (termSubTerm (t, todo->term))
{ {
// Occurs, we have to iterate Termlist tl;
void iterateThis (Term to)
{
tolist = termlistPrepend (tolist, to);
addEnumTerm (sys, t, actor, todo->next, fromlist, tolist);
tolist = termlistDelTerm (tolist);
}
fromlist = termlistPrepend (fromlist, todo->term); fromlist = termlistPrepend (fromlist, todo->term);
if (isTermEqual (todo->term, actor)) if (isTermEqual (todo->term, actor))
{ {
// Untrusted agents only // Untrusted agents only
Termlist tl; tl = sys->untrusted;
for (tl = sys->untrusted; tl != NULL; tl = tl->next)
{
iterateThis (tl->term);
}
} }
else else
{ {
// any agents // any agents
Termlist tl; tl = sys->agentnames;
}
for (tl = sys->agentnames; tl != NULL; tl = tl->next) while (tl != NULL)
{ {
iterateThis (tl->term); tolist = termlistPrepend (tolist, tl->term);
} addEnumTerm (sys, t, actor, todo->next, fromlist, tolist);
tolist = termlistDelTerm (tolist);
tl = tl->next;
} }
fromlist = termlistDelTerm (fromlist); fromlist = termlistDelTerm (fromlist);
} }

16
src/knowledge.c
View File

@ -430,6 +430,14 @@ isKnowledgePublicFunction (const Knowledge know, const Term f)
return inTermlist (know->publicfunctions, f); return inTermlist (know->publicfunctions, f);
} }
Term
funKey (Term orig, Term f)
{
/* in: f'{op}, f
* out: f{op'} */
return makeTermFcall (termDuplicate (TermOp (orig)), termDuplicate (f));
}
//! Give the inverse key term of a term. //! Give the inverse key term of a term.
/** /**
* Gives a duplicate of the inverse Key of some term (which is used to encrypt something), as is defined * Gives a duplicate of the inverse Key of some term (which is used to encrypt something), as is defined
@ -452,14 +460,6 @@ inverseKey (Knowledge know, Term key)
{ {
Termlist tl; Termlist tl;
Term funKey (Term orig, Term f)
{
/* in: f'{op}, f
* out: f{op'} */
return makeTermFcall (termDuplicate (TermOp (orig)),
termDuplicate (f));
}
tl = know->inversekeyfunctions; tl = know->inversekeyfunctions;
while (tl != NULL && tl->next != NULL) while (tl != NULL && tl->next != NULL)
{ {

37
src/mgu.c
View File

@ -146,6 +146,22 @@ unify_callback_wrapper (Termlist tl, struct state_mgu_tmp *ptr_tmpstate)
ptr_tmpstate->oldcallback, ptr_tmpstate->oldstate); ptr_tmpstate->oldcallback, ptr_tmpstate->oldstate);
} }
int
callsubst (int (*callback) (), void *state, Termlist tl, Term t, Term tsubst)
{
int proceed;
t->subst = tsubst;
#ifdef DEBUG
showSubst (t);
#endif
tl = termlistAdd (tl, t);
proceed = callback (tl, state);
tl = termlistDelTerm (tl);
t->subst = NULL;
return proceed;
}
//! Most general unifier iteration //! Most general unifier iteration
/** /**
* Try to determine the most general unifier of two terms, if so calls function. * Try to determine the most general unifier of two terms, if so calls function.
@ -161,21 +177,6 @@ unify_callback_wrapper (Termlist tl, struct state_mgu_tmp *ptr_tmpstate)
int int
unify (Term t1, Term t2, Termlist tl, int (*callback) (), void *state) unify (Term t1, Term t2, Termlist tl, int (*callback) (), void *state)
{ {
int callsubst (Termlist tl, Term t, Term tsubst)
{
int proceed;
t->subst = tsubst;
#ifdef DEBUG
showSubst (t);
#endif
tl = termlistAdd (tl, t);
proceed = callback (tl, state);
tl = termlistDelTerm (tl);
t->subst = NULL;
return proceed;
}
/* added for speed */ /* added for speed */
t1 = deVar (t1); t1 = deVar (t1);
t2 = deVar (t2); t2 = deVar (t2);
@ -223,7 +224,7 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (), void *state)
t1 = t2; t1 = t2;
t2 = t3; t2 = t3;
} }
return callsubst (tl, t1, t2); return callsubst (callback, state, tl, t1, t2);
} }
/* symmetrical tests for single variable. /* symmetrical tests for single variable.
@ -235,7 +236,7 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (), void *state)
return true; return true;
else else
{ {
return callsubst (tl, t2, t1); return callsubst (callback, state, tl, t2, t1);
} }
} }
if (realTermVariable (t1)) if (realTermVariable (t1))
@ -244,7 +245,7 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (), void *state)
return true; return true;
else else
{ {
return callsubst (tl, t1, t2); return callsubst (callback, state, tl, t1, t2);
} }
} }

272
src/term.c
View File

@ -1188,6 +1188,53 @@ term_rolelocals_are_variables ()
rolelocal_variable = 1; rolelocal_variable = 1;
} }
//! Helper for counting encryption level of a term
int
iter_maxencrypt (Term baseterm, Term t)
{
if (isTicketTerm (t))
{
return 0;
}
t = deVar (t);
if (t == NULL)
{
#ifdef DEBUG
if (DEBUGL (2))
{
eprintf ("Warning: Term encryption level finds a NULL for term ");
termPrint (baseterm);
eprintf ("\n");
}
#endif
return 0;
}
if (realTermLeaf (t))
{
return 0;
}
else
{
int l, r;
if (realTermTuple (t))
{
l = iter_maxencrypt (baseterm, TermOp1 (t));
r = iter_maxencrypt (baseterm, TermOp2 (t));
}
else
{
// encrypt
l = 1 + iter_maxencrypt (baseterm, TermOp (t));
r = iter_maxencrypt (baseterm, TermKey (t));
}
if (l > r)
return l;
else
return r;
}
}
//! Count the encryption level of a term //! Count the encryption level of a term
/** /**
* Note that this stops at any variable that is of ticket type. * Note that this stops at any variable that is of ticket type.
@ -1195,52 +1242,38 @@ term_rolelocals_are_variables ()
int int
term_encryption_level (const Term term) term_encryption_level (const Term term)
{ {
int iter_maxencrypt (Term t) return iter_maxencrypt (term, term);
{ }
if (isTicketTerm (t))
{
return 0;
}
t = deVar (t);
if (t == NULL)
{
#ifdef DEBUG
if (DEBUGL (2))
{
eprintf ("Warning: Term encryption level finds a NULL for term ");
termPrint (term);
eprintf ("\n");
}
#endif
return 0;
}
if (realTermLeaf (t))
{
return 0;
}
else
{
int l, r;
if (realTermTuple (t)) struct ti_data
{ {
l = iter_maxencrypt (TermOp1 (t)); int vars;
r = iter_maxencrypt (TermOp2 (t)); int structure;
} };
else
{
// encrypt
l = 1 + iter_maxencrypt (TermOp (t));
r = iter_maxencrypt (TermKey (t));
}
if (l > r)
return l;
else
return r;
}
}
return iter_maxencrypt (term); void
tcl_iterate (struct ti_data *p_data, Term t)
{
t = deVar (t);
(p_data->structure)++;
if (realTermLeaf (t))
{
if (realTermVariable (t))
(p_data->vars)++;
}
else
{
if (realTermTuple (t))
{
tcl_iterate (p_data, TermOp1 (t));
tcl_iterate (p_data, TermOp2 (t));
}
else
{
tcl_iterate (p_data, TermOp (t));
tcl_iterate (p_data, TermKey (t));
}
}
} }
//! Determine 'constrained factor' of a term //! Determine 'constrained factor' of a term
@ -1252,40 +1285,61 @@ term_encryption_level (const Term term)
float float
term_constrain_level (const Term term) term_constrain_level (const Term term)
{ {
int vars; struct ti_data data;
int structure;
void tcl_iterate (Term t)
{
t = deVar (t);
structure++;
if (realTermLeaf (t))
{
if (realTermVariable (t))
vars++;
}
else
{
if (realTermTuple (t))
{
tcl_iterate (TermOp1 (t));
tcl_iterate (TermOp2 (t));
}
else
{
tcl_iterate (TermOp (t));
tcl_iterate (TermKey (t));
}
}
}
if (term == NULL) if (term == NULL)
error ("Cannot determine constrain level of empty term."); error ("Cannot determine constrain level of empty term.");
vars = 0; data.vars = 0;
structure = 0; data.structure = 0;
tcl_iterate (term); tcl_iterate (&data, term);
return ((float) vars / (float) structure); return ((float) data.vars / (float) data.structure);
}
void
scan_levels (int level, Term t)
{
#ifdef DEBUG
if (DEBUGL (5))
{
int c;
c = 0;
while (c < level)
{
eprintf (" ");
c++;
}
eprintf ("Scanning keylevel %i for term ", level);
termPrint (t);
eprintf ("\n");
}
#endif
if (realTermLeaf (t))
{
Symbol sym;
// So, it occurs at 'level' as key. If that is less than known, store.
sym = TermSymb (t);
if (level < sym->keylevel)
{
// New minimum level
sym->keylevel = level;
}
}
else
{
if (realTermTuple (t))
{
scan_levels (level, TermOp1 (t));
scan_levels (level, TermOp2 (t));
}
else
{
scan_levels (level, TermOp (t));
scan_levels ((level + 1), TermKey (t));
}
}
} }
//! Adjust the keylevels of the symbols in a term. //! Adjust the keylevels of the symbols in a term.
@ -1295,54 +1349,22 @@ term_constrain_level (const Term term)
void void
term_set_keylevels (const Term term) term_set_keylevels (const Term term)
{ {
void scan_levels (int level, Term t)
{
#ifdef DEBUG
if (DEBUGL (5))
{
int c;
c = 0;
while (c < level)
{
eprintf (" ");
c++;
}
eprintf ("Scanning keylevel %i for term ", level);
termPrint (t);
eprintf ("\n");
}
#endif
if (realTermLeaf (t))
{
Symbol sym;
// So, it occurs at 'level' as key. If that is less than known, store.
sym = TermSymb (t);
if (level < sym->keylevel)
{
// New minimum level
sym->keylevel = level;
}
}
else
{
if (realTermTuple (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 (0, term); scan_levels (0, term);
} }
void
termFromTo (Term t1, Term t2)
{
t1 = deVar (t1);
t2 = deVar (t2);
eprintf (" [");
termPrint (t1);
eprintf ("]->[");
termPrint (t2);
eprintf ("] ");
}
//! Print the term diff of two terms //! Print the term diff of two terms
/** /**
* This is not correct yet. We need to add function application and correct tuple handing. * This is not correct yet. We need to add function application and correct tuple handing.
@ -1350,18 +1372,6 @@ term_set_keylevels (const Term term)
void void
termPrintDiff (Term t1, Term t2) termPrintDiff (Term t1, Term t2)
{ {
void termFromTo (Term t1, Term t2)
{
t1 = deVar (t1);
t2 = deVar (t2);
eprintf (" [");
termPrint (t1);
eprintf ("]->[");
termPrint (t2);
eprintf ("] ");
}
t1 = deVar (t1); t1 = deVar (t1);
t2 = deVar (t2); t2 = deVar (t2);

132
src/xmlout.c
View File

@ -843,6 +843,71 @@ xmlRunInfo (const System sys, const int run)
xmlRunVariables (sys, run); xmlRunVariables (sys, run);
} }
//! Test whether to display this event
/**
* Could be integrated into a single line on the while loop,
* but that makes it rather hard to understand.
*/
int
showthis (const System sys, const int run, const Roledef rd, const int index)
{
if (rd != NULL)
{
if (index < sys->runs[run].step)
{
return true;
}
else
{
if (switches.extendTrivial || switches.extendNonRecvs)
{
if (rd->type != RECV)
{
return true;
}
else
{
if (switches.extendTrivial)
{
/* This is a recv, and we don't know whether to
* include it. Default behaviour would be to jump
* out of the conditions, and return false.
* Instead, we check whether it can be trivially
* satisfied by the knowledge from the preceding
* events.
*/
if (isTriviallyKnownAtArachne (sys,
rd->message, run, index))
{
return true;
}
else
{
/* We cannot extend it trivially, based on
* the preceding events, but maybe we can
* base it on another (*all*) event. That
* would in fact introduce another implicit
* binding. Currently, we do not explicitly
* introduce this binding, but just allow
* displaying the event.
*
* TODO consider what it means to leave out
* this binding.
*/
if (isTriviallyKnownAfterArachne
(sys, rd->message, run, index))
{
return true;
}
}
}
}
}
}
}
return false;
}
//! Display runs //! Display runs
void void
xmlOutRuns (const System sys) xmlOutRuns (const System sys)
@ -862,74 +927,9 @@ xmlOutRuns (const System sys)
Roledef rd; Roledef rd;
int index; int index;
//! Test whether to display this event
/**
* Could be integrated into a single line on the while loop,
* but that makes it rather hard to understand.
*/
int showthis (void)
{
if (rd != NULL)
{
if (index < sys->runs[run].step)
{
return true;
}
else
{
if (switches.extendTrivial || switches.extendNonRecvs)
{
if (rd->type != RECV)
{
return true;
}
else
{
if (switches.extendTrivial)
{
/* This is a recv, and we don't know whether to
* include it. Default behaviour would be to jump
* out of the conditions, and return false.
* Instead, we check whether it can be trivially
* satisfied by the knowledge from the preceding
* events.
*/
if (isTriviallyKnownAtArachne (sys,
rd->message,
run, index))
{
return true;
}
else
{
/* We cannot extend it trivially, based on
* the preceding events, but maybe we can
* base it on another (*all*) event. That
* would in fact introduce another implicit
* binding. Currently, we do not explicitly
* introduce this binding, but just allow
* displaying the event.
*
* TODO consider what it means to leave out
* this binding.
*/
if (isTriviallyKnownAfterArachne
(sys, rd->message, run, index))
{
return true;
}
}
}
}
}
}
}
return false;
}
index = 0; index = 0;
rd = sys->runs[run].start; rd = sys->runs[run].start;
while (showthis ()) while (showthis (sys, run, rd, index))
{ {
xmlOutEvent (sys, rd, run, index); xmlOutEvent (sys, rd, run, index);
index++; index++;