From a38925c9c24817268499efc3fce61386028efe9b Mon Sep 17 00:00:00 2001 From: ccremers Date: Tue, 16 Nov 2004 12:06:36 +0000 Subject: [PATCH] - Added some useful macros to term.h to address subparts (e.g. TermOp1(t)). Renamed all uses. --- src/arachne.c | 16 +-- src/binding.c | 4 +- src/compiler.c | 8 +- src/knowledge.c | 22 ++--- src/latex.c | 24 ++--- src/main.c | 4 +- src/match_clp.c | 20 ++-- src/mgu.c | 20 ++-- src/modelchecker.c | 6 +- src/role.c | 2 +- src/substitution.c | 8 +- src/system.c | 6 +- src/term.c | 242 ++++++++++++++++++++++----------------------- src/term.h | 36 ++++--- src/termlist.c | 42 ++++---- 15 files changed, 235 insertions(+), 225 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index ed15b19..657684a 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -200,9 +200,9 @@ getTermFunction (Term t) t = deVar (t); if (t != NULL) { - if (realTermEncrypt (t) && isTermFunctionName (t->right.key)) + if (realTermEncrypt (t) && isTermFunctionName (TermKey(t))) { - return t->right.key; + return TermKey(t); } } return NULL; @@ -304,7 +304,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 && tl->term->right.runid == -3) + if (tl->term->type != VARIABLE && TermRunid(tl->term) == -3) { Term t; @@ -320,12 +320,12 @@ determine_unification_run (Termlist tl) if (run == -2) { // Any run - run = t->right.runid; + run = TermRunid(t); } else { // Specific run: compare - if (run != t->right.runid) + if (run != TermRunid(t)) { return -1; } @@ -553,7 +553,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, tl->term->right.key)) + 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 */ @@ -1361,8 +1361,8 @@ bind_goal_new_encrypt (const Binding b) } // must be encryption - t1 = term->left.op; - t2 = term->right.key; + t1 = TermOp(term); + t2 = TermKey(term); if (t2 != TERM_Hidden) { diff --git a/src/binding.c b/src/binding.c index 038f684..9792291 100644 --- a/src/binding.c +++ b/src/binding.c @@ -177,7 +177,7 @@ goal_graph_create () Term t; t = tl->term; - if (t->type == VARIABLE && t->right.runid == 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 - && t2->right.runid == run2) + && TermRunid(t2) == run2) { // t2 is a constant of run2 if (isTermEqual (t, t2)) diff --git a/src/compiler.c b/src/compiler.c index 36e7901..b5af343 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -241,7 +241,7 @@ levelFind (Symbol s, int level) { if (isTermLeaf (tl->term)) { - if (tl->term->left.symb == s) + if (TermSymb(tl->term) == s) { return tl->term; } @@ -505,7 +505,7 @@ commEvent (int event, Tac tc) else { /* n parameters */ - msg = deVar (claimbig)->right.op2; + msg = TermOp2(deVar (claimbig)); if (tupleCount (msg) != n) { error ("Problem with claim tuple unfolding at line %i.", @@ -690,7 +690,7 @@ runInstanceCreate (Tac tc) /* first, locate the protocol */ psym = tc->t1.tac->t1.sym; p = sys->protocols; - while (p != NULL && p->nameterm->left.symb != psym) + while (p != NULL && TermSymb(p->nameterm) != psym) p = p->next; if (p == NULL) { @@ -703,7 +703,7 @@ runInstanceCreate (Tac tc) /* locate the role */ rsym = tc->t1.tac->t2.sym; r = p->roles; - while (r != NULL && r->nameterm->left.symb != rsym) + while (r != NULL && TermSymb(r->nameterm) != rsym) r = r->next; if (r == NULL) { diff --git a/src/knowledge.c b/src/knowledge.c index fe3a2eb..4b2efdc 100644 --- a/src/knowledge.c +++ b/src/knowledge.c @@ -154,8 +154,8 @@ knowledgeAddTerm (Knowledge know, Term term) { int status; - status = knowledgeAddTerm (know, term->left.op1); - return knowledgeAddTerm (know, term->right.op2) || 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, term->right.key); + Term invkey = inverseKey (know->inverses, TermKey(term)); if (inKnowledge (know, invkey)) { /* we can decrypt it */ - knowledgeAddTerm (know, term->left.op); - if (!inKnowledge (know, term->right.key)) + 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 ((scan->term)->right.key, invkey)) + if (isTermEqual (TermKey(scan->term), invkey)) { - tldecrypts = termlistAdd (tldecrypts, (scan->term)->left.op); + 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, term->right.key) - && inKnowledge (know, term->left.op)); + (inKnowledge (know, TermKey(term)) + && inKnowledge (know, TermOp(term))); } if (term->type == TUPLE) { return (inTermlist (know->encrypt, term) || - (inKnowledge (know, term->left.op1) && - inKnowledge (know, term->right.op2))); + (inKnowledge (know, TermOp1(term)) && + inKnowledge (know, TermOp2(term)))); } return 0; /* unrecognized term type, weird */ } diff --git a/src/latex.c b/src/latex.c index ec03bee..486d208 100644 --- a/src/latex.c +++ b/src/latex.c @@ -117,12 +117,12 @@ latexTermPrint (Term term, Termlist highlight) { if (inTermlist (highlight, term)) printf ("\\mathbf{"); - symbolPrint (term->left.symb); + symbolPrint (TermSymb(term)); if (realTermVariable (term)) printf ("V"); - if (term->right.runid >= 0) + if (TermRunid(term) >= 0) { - printf ("\\sharp%i", term->right.runid); + printf ("\\sharp%i", TermRunid(term)); } if (term->subst != NULL) { @@ -141,22 +141,22 @@ latexTermPrint (Term term, Termlist highlight) } if (realTermEncrypt (term)) { - if (isTermLeaf (term->right.key) - && inTermlist (term->right.key->stype, TERM_Function)) + if (isTermLeaf (TermKey(term)) + && inTermlist (TermKey(term)->stype, TERM_Function)) { /* function application */ - latexTermPrint (term->right.key, highlight); + latexTermPrint (TermKey(term), highlight); printf ("("); - latexTermTuplePrint (term->left.op, highlight); + latexTermTuplePrint (TermOp(term), highlight); printf (")"); } else { /* normal encryption */ printf ("\\{"); - latexTermTuplePrint (term->left.op, highlight); + latexTermTuplePrint (TermOp(term), highlight); printf ("\\}_{"); - latexTermPrint (term->right.key, 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 (term->left.op1, hl); + latexTermPrint (TermOp1(term), hl); printf (","); - term = deVar (term->right.op2); + 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) && t->right.runid == i) + if (isTermLeaf (t) && TermRunid(t) == i) { if (first) { diff --git a/src/main.c b/src/main.c index 1c8b6ea..3b767b5 100644 --- a/src/main.c +++ b/src/main.c @@ -772,14 +772,14 @@ timersPrint (const System sys) { /* modern version: claim label is tuple (protocname, label) */ /* first print protocol.role */ - termPrint (cl_scan->label->left.op1); + termPrint (TermOp1(cl_scan->label)); eprintf ("\t"); termPrint (cl_scan->rolename); eprintf ("\t"); /* second print event_label */ termPrint (cl_scan->type); eprintf ("_"); - termPrint (cl_scan->label->right.op2); + termPrint (TermOp2(cl_scan->label)); eprintf ("\t"); } else diff --git a/src/match_clp.c b/src/match_clp.c index 36d183a..fc51f07 100644 --- a/src/match_clp.c +++ b/src/match_clp.c @@ -60,11 +60,11 @@ solve (const struct solvepass sp, Constraintlist solvecons) cl = constraintlistDuplicate (solvecons); cl = constraintlistAdd (cl, - makeConstraint (deVar (activeco->term)->left.op1, + makeConstraint (TermOp1(deVar (activeco->term)), activeco->know)); cl = constraintlistAdd (cl, - makeConstraint (deVar (activeco->term)->right.op2, + 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 (activeco->term->left.op, + makeConstraint (TermOp(activeco->term), activeco->know)); cl = constraintlistAdd (cl, - makeConstraint (activeco->term->right.key, + 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, t->left.op1); - tl2 = termlistAdd (tl2, t->right.op2); + 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, t->right.key); + 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 (t->left.op)) - tl2 = termlistAdd (tl2, t->left.op); + && 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, t->left.op); + tl2 = termlistAdd (tl2, TermOp(t)); sendAdd_clp (sys, run, tl2); termlistDelete (tl2); diff --git a/src/mgu.c b/src/mgu.c index ba51db2..a560741 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -183,14 +183,14 @@ termMguTerm (Term t1, Term t2) { Termlist tl1, tl2; - tl1 = termMguTerm (t1->right.key, t2->right.key); + tl1 = termMguTerm (TermKey(t1), TermKey(t2)); if (tl1 == MGUFAIL) { return MGUFAIL; } else { - tl2 = termMguTerm (t1->left.op, t2->left.op); + 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 (t1->left.op1, t2->left.op1); + tl1 = termMguTerm (TermOp1(t1), TermOp1(t2)); if (tl1 == MGUFAIL) { return MGUFAIL; } else { - tl2 = termMguTerm (t1->right.op2, t2->right.op2); + 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, t2->left.op1, iterator); - flag = flag && termMguInTerm (t1, t2->right.op2, 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, t2->left.op1, iterator, inverses, + flag && termMguSubTerm (t1, TermOp1(t2), iterator, inverses, keylist); flag = - flag && termMguSubTerm (t1, t2->right.op2, iterator, inverses, + flag && termMguSubTerm (t1, TermOp2(t2), iterator, inverses, keylist); } else @@ -312,7 +312,7 @@ 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, t2->right.key); + 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)) { @@ -323,7 +323,7 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist), // Recurse flag = - flag && termMguSubTerm (t1, t2->left.op, iterator, inverses, + flag && termMguSubTerm (t1, TermOp(t2), iterator, inverses, keylist_new); termlistDelete (keylist_new); diff --git a/src/modelchecker.c b/src/modelchecker.c index 1c12db9..798803d 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -1147,7 +1147,7 @@ claimSecrecy (const System sys, const Term t) { t = deVar (t); if (isTermTuple (t)) - return csScan (t->left.op1) && csScan (t->right.op2); + 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 (t->left.op1, know), - secrecyUnfolding (t->right.op2, know)); + return termlistConcat (secrecyUnfolding (TermOp1(t), know), + secrecyUnfolding (TermOp2(t), know)); else { if (inKnowledge (know, t)) diff --git a/src/role.c b/src/role.c index c946086..1592d3f 100644 --- a/src/role.c +++ b/src/role.c @@ -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 = label->right.op2; + label = TermOp2(label); } //! Print latex/normal diff --git a/src/substitution.c b/src/substitution.c index a24bb80..53035c9 100644 --- a/src/substitution.c +++ b/src/substitution.c @@ -64,14 +64,14 @@ termSubstitute (Term term, Substitution subs) { if (isTermEncrypt (term)) { - return makeTermEncrypt (termSubstitute (term->left.op, subs), - termSubstitute (term->right.key, subs)); + return makeTermEncrypt (termSubstitute (TermOp(term), subs), + termSubstitute (TermKey(term), subs)); } else { return - makeTermTuple (termSubstitute (term->left.op1, subs), - termSubstitute (term->right.op2, subs)); + makeTermTuple (termSubstitute (TermOp1(term), subs), + termSubstitute (TermOp2(term), subs)); } } else diff --git a/src/system.c b/src/system.c index 42ec3f7..4a23d78 100644 --- a/src/system.c +++ b/src/system.c @@ -563,7 +563,7 @@ create_new_local (const Term t, const int rid) { Term newt; - newt = makeTermType (t->type, t->left.symb, 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, newt->left.symb, 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, scanfrom->term->left.symb, rid); + newvar = makeTermType (VARIABLE, TermSymb(scanfrom->term), rid); artefacts = termlistAdd (artefacts, newvar); sys->variables = termlistAdd (sys->variables, newvar); newvar->stype = termlistAdd (NULL, scanto->term); diff --git a/src/term.c b/src/term.c index 8e2ffdb..28d1127 100644 --- a/src/term.c +++ b/src/term.c @@ -75,8 +75,8 @@ makeTermEncrypt (Term t1, Term t2) Term term = makeTerm (); term->type = ENCRYPT; term->stype = NULL; - term->left.op = t1; - term->right.key = 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; - tt->left.op1 = t1; - tt->right.op2 = 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; - term->left.symb = symb; - term->right.runid = runid; + TermSymb(term) = symb; + TermRunid(term) = runid; return term; } @@ -163,11 +163,11 @@ hasTermVariable (Term term) else { if (realTermTuple (term)) - return (hasTermVariable (term->left.op1) - || hasTermVariable (term->right.op2)); + return (hasTermVariable (TermOp1(term)) + || hasTermVariable (TermOp2(term))); else - return (hasTermVariable (term->left.op) - || hasTermVariable (term->right.key)); + return (hasTermVariable (TermOp(term)) + || hasTermVariable (TermKey(term))); } } @@ -206,8 +206,8 @@ isTermEqualFn (Term term1, Term term2) } if (realTermLeaf (term1)) { - return (term1->left.symb == term2->left.symb - && term1->right.runid == term2->right.runid); + 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 (term1->right.key, term2->right.key) && - isTermEqualFn (term1->left.op, term2->left.op)); + return (isTermEqualFn (TermKey(term1), TermKey(term2)) && + isTermEqualFn (TermOp(term1), TermOp(term2))); } else { /* tuple */ - return (isTermEqualFn (term1->left.op1, term2->left.op1) && - isTermEqualFn (term1->right.op2, term2->right.op2)); + 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 (t->left.op1, tsub) - || termSubTerm (t->right.op2, tsub)); + return (termSubTerm (TermOp1(t), tsub) + || termSubTerm (TermOp2(t), tsub)); else - return (termSubTerm (t->left.op, tsub) - || termSubTerm (t->right.key, tsub)); + return (termSubTerm (TermOp(t), tsub) + || termSubTerm (TermKey(t), tsub)); } //! See if a term is an interm of another. @@ -272,8 +272,8 @@ termInTerm (Term t, Term tsub) if (realTermLeaf (t)) return 0; if (realTermTuple (t)) - return (termInTerm (t->left.op1, tsub) - || termInTerm (t->right.op2, tsub)); + return (termInTerm (TermOp1(t), tsub) + || termInTerm (TermOp2(t), tsub)); else return 0; } @@ -303,15 +303,15 @@ termPrint (Term term) #endif if (realTermLeaf (term)) { - symbolPrint (term->left.symb); + symbolPrint (TermSymb(term)); if (term->type == VARIABLE) eprintf ("V"); - if (term->right.runid >= 0) + if (TermRunid(term) >= 0) { if (globalLatex && globalError == 0) - eprintf ("\\sharp%i", term->right.runid); + eprintf ("\\sharp%i", TermRunid(term)); else - eprintf ("#%i", term->right.runid); + eprintf ("#%i", TermRunid(term)); } if (term->subst != NULL) { @@ -331,13 +331,13 @@ termPrint (Term term) } if (realTermEncrypt (term)) { - if (isTermLeaf (term->right.key) - && inTermlist (term->right.key->stype, TERM_Function)) + if (isTermLeaf (TermKey(term)) + && inTermlist (TermKey(term)->stype, TERM_Function)) { /* function application */ - termPrint (term->right.key); + termPrint (TermKey(term)); eprintf ("("); - termTuplePrint (term->left.op); + termTuplePrint (TermOp(term)); eprintf (")"); } else @@ -346,17 +346,17 @@ termPrint (Term term) if (globalLatex) { eprintf ("\\{"); - termTuplePrint (term->left.op); + termTuplePrint (TermOp(term)); eprintf ("\\}_{"); - termPrint (term->right.key); + termPrint (TermKey(term)); eprintf ("}"); } else { eprintf ("{"); - termTuplePrint (term->left.op); + termTuplePrint (TermOp(term)); eprintf ("}"); - termPrint (term->right.key); + termPrint (TermKey(term)); } } } @@ -380,9 +380,9 @@ termTuplePrint (Term term) while (realTermTuple (term)) { // To remove any brackets, change this into termTuplePrint. - termPrint (term->left.op1); + termPrint (TermOp1(term)); eprintf (","); - term = deVar (term->right.op2); + term = deVar (TermOp2(term)); } termPrint (term); return; @@ -409,13 +409,13 @@ termDuplicate (const Term term) memcpy (newterm, term, sizeof (struct term)); if (realTermEncrypt (term)) { - newterm->left.op = termDuplicate (term->left.op); - newterm->right.key = termDuplicate (term->right.key); + TermOp(newterm) = termDuplicate (TermOp(term)); + TermKey(newterm) = termDuplicate (TermKey(term)); } else { - newterm->left.op1 = termDuplicate (term->left.op1); - newterm->right.op2 = termDuplicate (term->right.op2); + TermOp1(newterm) = termDuplicate (TermOp1(term)); + TermOp2(newterm) = termDuplicate (TermOp2(term)); } return newterm; } @@ -464,13 +464,13 @@ termDuplicateDeep (const Term term) { if (realTermEncrypt (term)) { - newterm->left.op = termDuplicateDeep (term->left.op); - newterm->right.key = termDuplicateDeep (term->right.key); + TermOp(newterm) = termDuplicateDeep (TermOp(term)); + TermKey(newterm) = termDuplicateDeep (TermKey(term)); } else { - newterm->left.op1 = termDuplicateDeep (term->left.op1); - newterm->right.op2 = termDuplicateDeep (term->right.op2); + TermOp1(newterm) = termDuplicateDeep (TermOp1(term)); + TermOp2(newterm) = termDuplicateDeep (TermOp2(term)); } } return newterm; @@ -497,13 +497,13 @@ termDuplicateUV (Term term) memcpy (newterm, term, sizeof (struct term)); if (realTermEncrypt (term)) { - newterm->left.op = termDuplicateUV (term->left.op); - newterm->right.key = termDuplicateUV (term->right.key); + TermOp(newterm) = termDuplicateUV (TermOp(term)); + TermKey(newterm) = termDuplicateUV (TermKey(term)); } else { - newterm->left.op1 = termDuplicateUV (term->left.op1); - newterm->right.op2 = termDuplicateUV (term->right.op2); + TermOp1(newterm) = termDuplicateUV (TermOp1(term)); + TermOp2(newterm) = termDuplicateUV (TermOp2(term)); } return newterm; } @@ -534,13 +534,13 @@ realTermDuplicate (const Term term) newterm->type = term->type; if (realTermEncrypt (term)) { - newterm->left.op = realTermDuplicate (term->left.op); - newterm->right.key = realTermDuplicate (term->right.key); + TermOp(newterm) = realTermDuplicate (TermOp(term)); + TermKey(newterm) = realTermDuplicate (TermKey(term)); } else { - newterm->left.op1 = realTermDuplicate (term->left.op1); - newterm->right.op2 = realTermDuplicate (term->right.op2); + TermOp1(newterm) = realTermDuplicate (TermOp1(term)); + TermOp2(newterm) = realTermDuplicate (TermOp2(term)); } } return newterm; @@ -560,13 +560,13 @@ termDelete (const Term term) { if (realTermEncrypt (term)) { - termDelete (term->left.op); - termDelete (term->right.key); + termDelete (TermOp(term)); + termDelete (TermKey(term)); } else { - termDelete (term->left.op1); - termDelete (term->right.op2); + termDelete (TermOp1(term)); + termDelete (TermOp2(term)); } memFree (term, sizeof (struct term)); } @@ -589,29 +589,29 @@ termNormalize (Term term) if (realTermEncrypt (term)) { - termNormalize (term->left.op); - termNormalize (term->right.key); + termNormalize (TermOp(term)); + termNormalize (TermKey(term)); } else { /* normalize left hand first,both for tupling and for encryption */ - termNormalize (term->left.op1); + termNormalize (TermOp1(term)); /* check for ((x,y),z) construct */ - if (realTermTuple (term->left.op1)) + if (realTermTuple (TermOp1(term))) { /* temporarily store the old terms */ - Term tx = (term->left.op1)->left.op1; - Term ty = (term->left.op1)->right.op2; - Term tz = term->right.op2; + Term tx = TermOp1(TermOp1(term)); + Term ty = TermOp2(TermOp1(term)); + Term tz = TermOp2(term); /* move node */ - term->right.op2 = term->left.op1; + TermOp2(term) = TermOp1(term); /* construct (x,(y,z)) version */ - term->left.op1 = tx; - (term->right.op2)->left.op1 = ty; - (term->right.op2)->right.op2 = tz; + TermOp1(term) = tx; + TermOp1(TermOp2(term)) = ty; + TermOp2(TermOp2(term)) = tz; } - termNormalize (term->right.op2); + termNormalize (TermOp2(term)); } } @@ -629,12 +629,12 @@ termRunid (Term term, int runid) if (realTermLeaf (term)) { /* leaf */ - if (term->right.runid == runid) + if (TermRunid(term) == runid) return term; else { Term newt = termDuplicate (term); - newt->right.runid = runid; + TermRunid(newt) = runid; return newt; } } @@ -643,13 +643,13 @@ termRunid (Term term, int runid) /* anything else, recurse */ if (realTermEncrypt (term)) { - return makeTermEncrypt (termRunid (term->left.op, runid), - termRunid (term->right.key, runid)); + return makeTermEncrypt (termRunid (TermOp(term), runid), + termRunid (TermKey(term), runid)); } else { - return makeTermTuple (termRunid (term->left.op1, runid), - termRunid (term->right.op2, runid)); + return makeTermTuple (termRunid (TermOp1(term), runid), + termRunid (TermOp2(term), runid)); } } } @@ -674,7 +674,7 @@ tupleCount (Term tt) } else { - return (tupleCount (tt->left.op1) + tupleCount (tt->right.op2)); + return (tupleCount (TermOp1(tt)) + tupleCount (TermOp2(tt))); } } } @@ -710,16 +710,16 @@ tupleProject (Term tt, int n) else { /* there is a tuple to traverse */ - int left = tupleCount (tt->left.op1); + int left = tupleCount (TermOp1(tt)); if (n >= left) { /* it's in the right hand side */ - return tupleProject (tt->right.op2, n - left); + return tupleProject (TermOp2(tt), n - left); } else { /* left hand side */ - return tupleProject (tt->left.op1, n); + return tupleProject (TermOp1(tt), n); } } } @@ -749,11 +749,11 @@ termSize (Term t) { if (realTermEncrypt (t)) { - return 1 + termSize (t->left.op) + termSize (t->right.key); + return 1 + termSize (TermOp(t)) + termSize (TermKey(t)); } else { - return termSize (t->left.op1) + termSize (t->right.op2); + return termSize (TermOp1(t)) + termSize (TermOp2(t)); } } } @@ -811,13 +811,13 @@ termDistance (Term t1, Term t2) if (isTermEncrypt (t1)) { /* encryption */ - return (termDistance (t1->left.op, t2->left.op) + - termDistance (t1->right.key, t2->right.key)) / 2; + return (termDistance (TermOp(t1), TermOp(t2)) + + termDistance (TermKey(t1), TermKey(t2))) / 2; } else { - return (termDistance (t1->left.op1, t2->left.op1) + - termDistance (t1->right.op2, t2->right.op2)) / 2; + return (termDistance (TermOp1(t1), TermOp1(t2)) + + termDistance (TermOp2(t1), TermOp2(t2))) / 2; } } } @@ -859,7 +859,7 @@ termOrder (Term t1, Term t2) /* compare names */ int comp; - comp = strcmp (t1->left.symb->text, t2->left.symb->text); + comp = strcmp (TermSymb(t1)->text, TermSymb(t2)->text); if (comp != 0) { /* names differ */ @@ -868,14 +868,14 @@ termOrder (Term t1, Term t2) else { /* equal names, compare run identifiers */ - if (t1->right.runid == t2->right.runid) + if (TermRunid(t1) == TermRunid(t2)) { error ("termOrder: two terms seem to be identical although local precondition says they aren't."); } else { - if (t1->right.runid < t2->right.runid) + if (TermRunid(t1) < TermRunid(t2)) return -1; else return 1; @@ -889,13 +889,13 @@ termOrder (Term t1, Term t2) if (isTermEncrypt (t1)) { - compL = termOrder (t1->left.op, t2->left.op); - compR = termOrder (t1->right.key, t2->right.key); + compL = termOrder (TermOp(t1), TermOp(t2)); + compR = termOrder (TermKey(t1), TermKey(t2)); } else { - compL = termOrder (t1->left.op1, t2->left.op1); - compR = termOrder (t1->right.op2, t2->right.op2); + compL = termOrder (TermOp1(t1), TermOp1(t2)); + compR = termOrder (TermOp2(t1), TermOp2(t2)); } if (compL != 0) return compL; @@ -931,10 +931,10 @@ term_iterate (const Term term, int (*leaf) (), int (*nodel) (), // Left part if (realTermTuple (term)) flag = flag - && (term_iterate (term->left.op1, leaf, nodel, nodem, noder)); + && (term_iterate (TermOp1(term), leaf, nodel, nodem, noder)); else flag = flag - && (term_iterate (term->left.op, leaf, nodel, nodem, noder)); + && (term_iterate (TermOp(term), leaf, nodel, nodem, noder)); if (nodem != NULL) flag = flag && nodem (term); @@ -942,10 +942,10 @@ term_iterate (const Term term, int (*leaf) (), int (*nodel) (), // Right part if (realTermTuple (term)) flag = flag - && (term_iterate (term->right.op2, leaf, nodel, nodem, noder)); + && (term_iterate (TermOp2(term), leaf, nodel, nodem, noder)); else flag = flag - && (term_iterate (term->right.key, leaf, nodel, nodem, noder)); + && (term_iterate (TermKey(term), leaf, nodel, nodem, noder)); if (noder != NULL) flag = flag && noder (term); @@ -990,11 +990,11 @@ term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (), flag = flag && (term_iterate_deVar - (term->left.op1, leaf, nodel, nodem, noder)); + (TermOp1(term), leaf, nodel, nodem, noder)); else flag = flag && - (term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder)); + (term_iterate_deVar (TermOp(term), leaf, nodel, nodem, noder)); if (nodem != NULL) flag = flag && nodem (term); @@ -1004,11 +1004,11 @@ term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (), flag = flag && (term_iterate_deVar - (term->right.op2, leaf, nodel, nodem, noder)); + (TermOp2(term), leaf, nodel, nodem, noder)); else flag = flag && - (term_iterate_deVar (term->right.key, 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 (term->left.op1, func) - && term_iterate_leaves (term->right.op2, func)); + return (term_iterate_leaves (TermOp1(term), func) + && term_iterate_leaves (TermOp2(term), func)); else - return (term_iterate_leaves (term->left.op, func) - && term_iterate_leaves (term->right.key, func)); + return (term_iterate_leaves (TermOp(term), func) + && term_iterate_leaves (TermKey(term), func)); } } return 1; @@ -1090,8 +1090,8 @@ term_encryption_level (const Term term) { int l,r; - l = iter_maxencrypt (term->left.op1); - r = iter_maxencrypt (term->right.op2); + l = iter_maxencrypt (TermOp1(term)); + r = iter_maxencrypt (TermOp2(term)); if (l>r) return l; else @@ -1100,7 +1100,7 @@ term_encryption_level (const Term term) else { // encrypt - return 1+iter_maxencrypt (term->left.op); + return 1+iter_maxencrypt (TermOp(term)); } } } @@ -1134,13 +1134,13 @@ term_constrain_level (const Term term) { if (realTermTuple (t)) { - tcl_iterate (t->left.op1); - tcl_iterate (t->right.op2); + tcl_iterate (TermOp1(t)); + tcl_iterate (TermOp2(t)); } else { - tcl_iterate (t->left.op); - tcl_iterate (t->right.key); + 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 = t->left.symb; + 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, t->left.op1); - scan_levels (level, t->right.op2); + scan_levels (level, TermOp1(t)); + scan_levels (level, TermOp2(t)); } else { - scan_levels (level, t->left.op); - scan_levels ((level + 1), t->right.key); + scan_levels (level, TermOp(t)); + scan_levels ((level + 1), TermKey(t)); } } } @@ -1257,12 +1257,12 @@ termPrintDiff (Term t1, Term t2) if (realTermEncrypt (t1)) { // Encryption - if (isTermEqual (t1->left.op, t2->left.op) || isTermEqual (t1->right.key, t2->right.key)) + if (isTermEqual (TermOp(t1), TermOp(t2)) || isTermEqual (TermKey(t1), TermKey(t2))) { eprintf ("{"); - termPrintDiff (t1->left.op, t2->left.op); + termPrintDiff (TermOp(t1), TermOp(t2)); eprintf ("}"); - termPrintDiff (t1->right.key, t2->right.key); + termPrintDiff (TermKey(t1), TermKey(t2)); } else { @@ -1272,12 +1272,12 @@ termPrintDiff (Term t1, Term t2) else { // Tupling - if (isTermEqual (t1->left.op1, t2->left.op1) || isTermEqual (t1->right.op2, t2->right.op2)) + if (isTermEqual (TermOp1(t1), TermOp1(t2)) || isTermEqual (TermOp2(t1), TermOp2(t2))) { eprintf ("("); - termPrintDiff (t1->left.op1, t2->left.op1); + termPrintDiff (TermOp1(t1), TermOp1(t2)); eprintf (")"); - termPrintDiff (t1->right.op2, t2->right.op2); + termPrintDiff (TermOp2(t1), TermOp2(t2)); } else { diff --git a/src/term.h b/src/term.h index e704c64..bb7d5da 100644 --- a/src/term.h +++ b/src/term.h @@ -53,6 +53,16 @@ struct term } right; }; +//! Component macros (left) +#define TermSymb(t) (t->left.symb) +#define TermOp1(t) (t->left.op1) +#define TermOp(t) (t->left.op) + +//! Component macros (right) +#define TermRunid(t) (t->right.runid) +#define TermOp2(t) (t->right.op2) +#define TermKey(t) (t->right.key) + //! Flag for term status extern int rolelocal_variable; @@ -68,7 +78,7 @@ __inline__ Term deVarScan (Term t); #define realTermLeaf(t) (t != NULL && t->type <= LEAF) #define realTermTuple(t) (t != NULL && t->type == TUPLE) #define realTermEncrypt(t) (t != NULL && t->type == ENCRYPT) -#define realTermVariable(t) (t != NULL && (t->type == VARIABLE || (t->type <= LEAF && rolelocal_variable && t->right.runid == -3))) +#define realTermVariable(t) (t != NULL && (t->type == VARIABLE || (t->type <= LEAF && rolelocal_variable && TermRunid(t) == -3))) #define substVar(t) ((realTermVariable (t) && t->subst != NULL) ? 1 : 0) #define deVar(t) ( substVar(t) ? deVarScan(t->subst) : t) #define isTermLeaf(t) realTermLeaf(deVar(t)) @@ -92,10 +102,10 @@ int isTermEqualDebug (Term t1, Term t2); ? isTermEqualFn(t1,t2) \ : ( \ realTermEncrypt(t2) \ - ? (isTermEqualFn(t1->right.key, t2->right.key) && \ - isTermEqualFn(t1->left.op, t2->left.op)) \ - : (isTermEqualFn(t1->left.op1, t2->left.op1) && \ - isTermEqualFn(t1->right.op2, t2->right.op2)) \ + ? (isTermEqualFn(TermKey(t1), TermKey(t2)) && \ + isTermEqualFn(TermOp(t1), TermOp(t2))) \ + : (isTermEqualFn(TermOp1(t1), TermOp1(t2)) && \ + isTermEqualFn(TermOp2(t1), TermOp2(t2))) \ ) \ ) \ ) \ @@ -115,10 +125,10 @@ int isTermEqualDebug (Term t1, Term t2); ? isTermEqualFn(t1,t2) \ : ( \ realTermEncrypt(t2) \ - ? (isTermEqual1(t1->right.key, t2->right.key) && \ - isTermEqual1(t1->left.op, t2->left.op)) \ - : (isTermEqual1(t1->left.op1, t2->left.op1) && \ - isTermEqual1(t1->right.op2, t2->right.op2)) \ + ? (isTermEqual1(TermKey(t1), TermKey(t2)) && \ + isTermEqual1(TermOp(t1), TermOp(t2))) \ + : (isTermEqual1(TermOp1(t1), TermOp1(t2)) && \ + isTermEqual1(TermOp2(t1), TermOp2(t2))) \ ) \ ) \ ) \ @@ -138,10 +148,10 @@ int isTermEqualDebug (Term t1, Term t2); ? isTermEqualFn(t1,t2) \ : ( \ realTermEncrypt(t2) \ - ? (isTermEqual2(t1->right.key, t2->right.key) && \ - isTermEqual2(t1->left.op, t2->left.op)) \ - : (isTermEqual2(t1->left.op1, t2->left.op1) && \ - isTermEqual2(t1->right.op2, t2->right.op2)) \ + ? (isTermEqual2(TermKey(t1), TermKey(t2)) && \ + isTermEqual2(TermOp(t1), TermOp(t2))) \ + : (isTermEqual2(TermOp1(t1), TermOp1(t2)) && \ + isTermEqual2(TermOp2(t1), TermOp2(t2))) \ ) \ ) \ ) \ diff --git a/src/termlist.c b/src/termlist.c index 943d5e2..c3b7069 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -412,12 +412,12 @@ termlistAddVariables (Termlist tl, Term t) else { if (isTermEncrypt (t)) - return termlistAddVariables (termlistAddVariables (tl, t->left.op), - t->right.key); + return termlistAddVariables (termlistAddVariables (tl, TermOp(t)), + TermKey(t)); else return - termlistAddVariables (termlistAddVariables (tl, t->left.op1), - t->right.op2); + termlistAddVariables (termlistAddVariables (tl, TermOp1(t)), + TermOp2(t)); } } @@ -455,12 +455,12 @@ termlistAddRealVariables (Termlist tl, Term t) else { if (realTermEncrypt (t)) - return termlistAddVariables (termlistAddVariables (tl, t->left.op), - t->right.key); + return termlistAddVariables (termlistAddVariables (tl, TermOp(t)), + TermKey(t)); else return - termlistAddVariables (termlistAddVariables (tl, t->left.op1), - t->right.op2); + 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, t->left.op), - t->right.key); + return termlistAddBasic (termlistAddBasic (tl, TermOp(t)), + TermKey(t)); else - return termlistAddBasic (termlistAddBasic (tl, t->left.op1), - t->right.op2); + 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 (key->right.key) - && inTermlist (deVar (key->right.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 (orig->left.op), + return makeTermEncrypt (termDuplicate (TermOp(orig)), termDuplicate (newk)); } while (inverses != NULL && inverses->next != NULL) { - if (isTermEqual (key->right.key, inverses->term)) + if (isTermEqual (TermKey(key), inverses->term)) return funKey (key, inverses->next->term); - if (isTermEqual (key->right.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)) { - newt->left.op1 = termLocal (t->left.op1, fromlist, tolist, runid); - newt->right.op2 = termLocal (t->right.op2, fromlist, tolist, runid); + TermOp1(newt) = termLocal (TermOp1(t), fromlist, tolist, runid); + TermOp2(newt) = termLocal (TermOp2(t), fromlist, tolist, runid); } else { - newt->left.op = termLocal (t->left.op, fromlist, tolist, runid); - newt->right.key = termLocal (t->right.key, fromlist, tolist, runid); + TermOp(newt) = termLocal (TermOp(t), fromlist, tolist, runid); + TermKey(newt) = termLocal (TermKey(t), fromlist, tolist, runid); } return newt; }