From d4ec0004d66cff0395347276ed05555b24ff7d00 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Fri, 4 Jan 2019 17:16:27 +0100 Subject: [PATCH] Removing a collection of fairly simple remaining nested function calls. --- src/binding.c | 50 ++++--- src/claim.c | 109 ++++++++------- src/compiler.c | 302 +++++++++++++++++++++------------------- src/dotout.c | 137 +++++++++--------- src/intruderknowledge.c | 31 ++--- src/knowledge.c | 16 +-- src/mgu.c | 37 ++--- src/term.c | 272 +++++++++++++++++++----------------- src/xmlout.c | 132 +++++++++--------- 9 files changed, 558 insertions(+), 528 deletions(-) diff --git a/src/binding.c b/src/binding.c index da64e1c..cbe5294 100644 --- a/src/binding.c +++ b/src/binding.c @@ -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. /** * 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 Labelinfo linfo; int send_run, send_ev, recv_run, recv_ev; + Term label; - int get_index (const int run) - { - Roledef rd; - int i; - - i = 0; - rd = sys->runs[run].start; - while (rd != NULL && !isTermEqual (rd->label, labels->term)) - { - rd = rd->next; - i++; - } -#ifdef DEBUG - if (rd == NULL) - error - ("Could not locate send or recv for label, after niagree holds, to test for order."); -#endif - return i; - } - - linfo = label_find (sys->labellist, labels->term); + label = labels->term; + linfo = label_find (sys->labellist, label); if (!linfo->ignore) { send_run = termmapGet (runs, linfo->sendrole); recv_run = termmapGet (runs, linfo->recvrole); - send_ev = get_index (send_run); - recv_ev = get_index (recv_run); + send_ev = get_index (send_run, label); + recv_ev = get_index (recv_run, label); if (!isDependEvent (send_run, send_ev, recv_run, recv_ev)) { // Not ordered; false diff --git a/src/claim.c b/src/claim.c index e42fc00..644672d 100644 --- a/src/claim.c +++ b/src/claim.c @@ -514,7 +514,59 @@ check_claim_niagree (const System sys, const int i) 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 int @@ -541,63 +593,14 @@ arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs) Roledef rd_send, rd_recv; 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 linfo = label_find (sys->labellist, labels->term); if (!linfo->ignore) { - rd_send = get_label_event (linfo->sendrole, labels->term); - rd_recv = get_label_event (linfo->recvrole, labels->term); + rd_send = + 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) { diff --git a/src/compiler.c b/src/compiler.c index d4de5b3..a74bc4c 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -1183,31 +1183,33 @@ normalDeclaration (Tac tc) 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 void 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)) { - addSecrecyList (role->declaredconsts); - addSecrecyList (role->declaredvars); + addSecrecyList (sys, protocol, role, role->declaredconsts); + addSecrecyList (sys, protocol, role, role->declaredvars); /* full non-injective agreement and ni-synch */ claimCreate (sys, protocol, role, CLAIM_Alive, NULL, NULL, -1); @@ -1699,6 +1701,26 @@ compute_label_roles (Termlist labels) 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 void 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 - // 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)) - { -#ifdef DEBUG - 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->recvrole); - roles_test (linfo->recvrole, linfo->sendrole); + if (roles_test + (roles_ordered, roles_remaining, linfo->sendrole, + linfo->recvrole)) + { + roles_ordered = + termlistAppend (roles_ordered, linfo->recvrole); + roles_remaining = + termlistDelTerm (termlistFind + (roles_remaining, + linfo->recvrole)); + } + if (roles_test + (roles_ordered, roles_remaining, linfo->recvrole, + linfo->sendrole)) + { + roles_ordered = + termlistAppend (roles_ordered, linfo->sendrole); + roles_remaining = + termlistDelTerm (termlistFind + (roles_remaining, + linfo->sendrole)); + } } } } @@ -1788,6 +1808,84 @@ order_label_roles (const Claimlist cl) #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. /** * 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 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 */ @@ -1907,10 +1922,10 @@ compute_prec_sets (const System sys) Roledef rd; ev1 = 0; - rd = roledef_re (r1, ev1); + rd = roledef_re (sys, r1, ev1); while (rd != NULL) { - eventlabels[index (r1, ev1)] = rd->label; + eventlabels[m_index (sys, r1, ev1)] = rd->label; //termPrint (rd->label); //eprintf ("\t"); ev1++; @@ -1918,7 +1933,7 @@ compute_prec_sets (const System sys) } while (ev1 < sys->roleeventmax) { - eventlabels[index (r1, ev1)] = NULL; + eventlabels[m_index (sys, r1, ev1)] = NULL; ev1++; } //eprintf ("\n"); @@ -1931,7 +1946,8 @@ compute_prec_sets (const System sys) ev1 = 1; 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++; } r1++; @@ -1945,7 +1961,7 @@ compute_prec_sets (const System sys) { Roledef rd1; - rd1 = roledef_re (r1, ev1); + rd1 = roledef_re (sys, r1, ev1); if (rd1 != NULL && rd1->type == SEND) { r2 = 0; @@ -1956,12 +1972,12 @@ compute_prec_sets (const System sys) { Roledef rd2; - rd2 = roledef_re (r2, ev2); + rd2 = roledef_re (sys, r2, ev2); if (rd2 != NULL && rd2->type == RECV && isTermEqual (rd1->label, rd2->label)) { - SETBIT (prec + rowsize * index (r1, ev1), - index (r2, ev2)); + SETBIT (prec + rowsize * m_index (sys, r1, ev1), + m_index (sys, r2, ev2)); } ev2++; } @@ -1976,7 +1992,7 @@ compute_prec_sets (const System sys) #ifdef DEBUG if (DEBUGL (5)) { - show_matrix (); + show_matrix (sys, rowsize, prec); } #endif @@ -1988,7 +2004,7 @@ compute_prec_sets (const System sys) #ifdef DEBUG if (DEBUGL (5)) { - show_matrix (); + show_matrix (sys, rowsize, prec); } #endif @@ -2016,14 +2032,14 @@ compute_prec_sets (const System sys) } } while (r1 < sys->rolecount - && !isTermEqual (label, eventlabels[index (r1, ev1)])); + && !isTermEqual (label, eventlabels[m_index (sys, r1, ev1)])); if (r1 == sys->rolecount) { error ("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) { error @@ -2039,15 +2055,15 @@ compute_prec_sets (const System sys) * Now we compute the preceding label set */ cl->prec = NULL; // clear first - claim_index = index (r1, ev1); + claim_index = m_index (sys, r1, ev1); r2 = 0; while (r2 < sys->rolecount) { ev2 = 0; - rd = roledef_re (r2, ev2); + rd = roledef_re (sys, r2, ev2); 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 @@ -2118,12 +2134,12 @@ compute_prec_sets (const System sys) { // if this event preceds the claim, replace the label term if (BIT - (prec + rowsize * index (r_scan, ev_scan), + (prec + rowsize * m_index (sys, r_scan, ev_scan), claim_index)) { Roledef rd; - rd = roledef_re (r_scan, ev_scan); + rd = roledef_re (sys, r_scan, ev_scan); if (rd->label != NULL) { t_buf = rd->label; diff --git a/src/dotout.c b/src/dotout.c index 1f9cd76..5259fea 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -263,30 +263,31 @@ redirNode (const System sys, Binding b) 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 void 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) { eprintf ("recv"); - optlabel (); + optlabel (rd); eprintf (" from "); termPrintRemap (rd->from); eprintf ("\\n"); @@ -295,7 +296,7 @@ roledefDraw (Roledef rd) if (rd->type == SEND) { eprintf ("send"); - optlabel (); + optlabel (rd); eprintf (" to "); termPrintRemap (rd->to); eprintf ("\\n"); @@ -304,7 +305,7 @@ roledefDraw (Roledef rd) if (rd->type == CLAIM) { eprintf ("claim"); - optlabel (); + optlabel (rd); eprintf ("\\n"); termPrintRemap (rd->to); if (rd->message != NULL) @@ -348,25 +349,26 @@ hlsValue (double n1, double n2, double hue) 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 void hlsrgbreal (int *r, int *g, int *b, double h, double l, double s) { 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) h -= 360.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 /** * 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 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) { // No colors @@ -432,6 +435,14 @@ printColor (double h, double l, double s) 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. /** @@ -453,13 +464,6 @@ setRunColorBuf (const System sys, int run, char *colorbuf) double h, l, s; 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 { 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) 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) - contract (RUNCOLORCONTRACT); + contract (roledelta, roleoffset, RUNCOLORCONTRACT); // Now we can convert this to a color 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 void drawBinding (const System sys, Binding b) { 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_to = (sys->runs[b->run_to].protocol == INTRUDER); @@ -1121,7 +1128,7 @@ drawBinding (const System sys, Binding b) { // intr->intr eprintf ("\t"); - myarrow (b); + myarrow (sys, m0_from, b); eprintf (" [label=\""); termPrintRemap (b->term); eprintf ("\""); @@ -1136,7 +1143,7 @@ drawBinding (const System sys, Binding b) { // intr->regular eprintf ("\t"); - myarrow (b); + myarrow (sys, m0_from, b); if (m0_from) { eprintf ("[weight=\"0.5\"]"); @@ -1151,7 +1158,7 @@ drawBinding (const System sys, Binding b) { // regular->intr eprintf ("\t"); - myarrow (b); + myarrow (sys, m0_from, b); eprintf (";\n"); } else @@ -1163,7 +1170,7 @@ drawBinding (const System sys, Binding b) if (isCommunicationExact (sys, b)) { eprintf ("\t"); - myarrow (b); + myarrow (sys, m0_from, b); eprintf (" [style=bold,color=\"%s\"]", GOODCOMMCOLOR); eprintf (";\n"); } diff --git a/src/intruderknowledge.c b/src/intruderknowledge.c index 9b362db..1b7278d 100644 --- a/src/intruderknowledge.c +++ b/src/intruderknowledge.c @@ -56,36 +56,25 @@ addEnumTerm (const System sys, Term t, Term actor, Termlist todo, { if (termSubTerm (t, todo->term)) { - // Occurs, we have to iterate - void iterateThis (Term to) - { - tolist = termlistPrepend (tolist, to); - - addEnumTerm (sys, t, actor, todo->next, fromlist, tolist); - - tolist = termlistDelTerm (tolist); - } + Termlist tl; fromlist = termlistPrepend (fromlist, todo->term); if (isTermEqual (todo->term, actor)) { // Untrusted agents only - Termlist tl; - - for (tl = sys->untrusted; tl != NULL; tl = tl->next) - { - iterateThis (tl->term); - } + tl = sys->untrusted; } else { // any agents - Termlist tl; - - for (tl = sys->agentnames; tl != NULL; tl = tl->next) - { - iterateThis (tl->term); - } + tl = sys->agentnames; + } + while (tl != NULL) + { + tolist = termlistPrepend (tolist, tl->term); + addEnumTerm (sys, t, actor, todo->next, fromlist, tolist); + tolist = termlistDelTerm (tolist); + tl = tl->next; } fromlist = termlistDelTerm (fromlist); } diff --git a/src/knowledge.c b/src/knowledge.c index 255790b..300d61f 100644 --- a/src/knowledge.c +++ b/src/knowledge.c @@ -430,6 +430,14 @@ isKnowledgePublicFunction (const Knowledge know, const Term 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. /** * 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; - Term funKey (Term orig, Term f) - { - /* in: f'{op}, f - * out: f{op'} */ - return makeTermFcall (termDuplicate (TermOp (orig)), - termDuplicate (f)); - } - tl = know->inversekeyfunctions; while (tl != NULL && tl->next != NULL) { diff --git a/src/mgu.c b/src/mgu.c index 6dacb40..463b027 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -146,6 +146,22 @@ unify_callback_wrapper (Termlist tl, struct state_mgu_tmp *ptr_tmpstate) 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 /** * 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 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 */ t1 = deVar (t1); t2 = deVar (t2); @@ -223,7 +224,7 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (), void *state) t1 = t2; t2 = t3; } - return callsubst (tl, t1, t2); + return callsubst (callback, state, tl, t1, t2); } /* symmetrical tests for single variable. @@ -235,7 +236,7 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (), void *state) return true; else { - return callsubst (tl, t2, t1); + return callsubst (callback, state, tl, t2, t1); } } if (realTermVariable (t1)) @@ -244,7 +245,7 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (), void *state) return true; else { - return callsubst (tl, t1, t2); + return callsubst (callback, state, tl, t1, t2); } } diff --git a/src/term.c b/src/term.c index f39da5f..6bdd1b6 100644 --- a/src/term.c +++ b/src/term.c @@ -1188,6 +1188,53 @@ term_rolelocals_are_variables () 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 /** * Note that this stops at any variable that is of ticket type. @@ -1195,52 +1242,38 @@ term_rolelocals_are_variables () int term_encryption_level (const Term term) { - int iter_maxencrypt (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 (term); - eprintf ("\n"); - } -#endif - return 0; - } - if (realTermLeaf (t)) - { - return 0; - } - else - { - int l, r; + return iter_maxencrypt (term, term); +} - if (realTermTuple (t)) - { - l = iter_maxencrypt (TermOp1 (t)); - r = iter_maxencrypt (TermOp2 (t)); - } - else - { - // encrypt - l = 1 + iter_maxencrypt (TermOp (t)); - r = iter_maxencrypt (TermKey (t)); - } - if (l > r) - return l; - else - return r; - } - } +struct ti_data +{ + int vars; + int structure; +}; - 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 @@ -1252,40 +1285,61 @@ term_encryption_level (const Term term) float term_constrain_level (const Term term) { - int vars; - 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)); - } - } - } + struct ti_data data; if (term == NULL) error ("Cannot determine constrain level of empty term."); - vars = 0; - structure = 0; - tcl_iterate (term); - return ((float) vars / (float) structure); + data.vars = 0; + data.structure = 0; + tcl_iterate (&data, term); + 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. @@ -1295,54 +1349,22 @@ term_constrain_level (const Term term) void 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); } +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 /** * 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 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); t2 = deVar (t2); diff --git a/src/xmlout.c b/src/xmlout.c index a41a5fb..6b01062 100644 --- a/src/xmlout.c +++ b/src/xmlout.c @@ -843,6 +843,71 @@ xmlRunInfo (const System sys, const int 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 void xmlOutRuns (const System sys) @@ -862,74 +927,9 @@ xmlOutRuns (const System sys) Roledef rd; 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; rd = sys->runs[run].start; - while (showthis ()) + while (showthis (sys, run, rd, index)) { xmlOutEvent (sys, rd, run, index); index++;