From 4a42604cb6dbc63835a66c9aee09a92f899a0a5d Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 2 Jun 2005 12:14:28 +0000 Subject: [PATCH] - Added Ticket basic term type. Note that this only has consequences for the Arachne type checking. The net result is that a variable of type 'Ticket' can always contain any term, even with -m0 or -m1 matching. --- src/arachne.c | 13 +++++ src/compiler.c | 2 + src/mgu.c | 88 ++++++---------------------- src/mgu.h | 1 + src/switches.c | 2 - src/system.c | 4 ++ src/type.c | 151 +++++++++++++++++++++++++++++++++++++++++++++++++ src/type.h | 11 ++++ 8 files changed, 200 insertions(+), 72 deletions(-) create mode 100644 src/type.c create mode 100644 src/type.h diff --git a/src/arachne.c b/src/arachne.c index 209c008..f8b3508 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -30,6 +30,7 @@ #include "binding.h" #include "warshall.h" #include "timer.h" +#include "type.h" extern Term CLAIM_Secret; extern Term CLAIM_Nisynch; @@ -2650,6 +2651,18 @@ prune_theorems () List bl; int run; + // Check all types of the local agents according to the matching type + if (!checkTypeLocals (sys)) + { + if (sys->output == PROOF) + { + indentPrint (); + eprintf + ("Pruned because some local variable was incorrectly subsituted.\n"); + } + return 1; + } + // Check if all agents are agents (!) run = 0; while (run < sys->maxruns) diff --git a/src/compiler.c b/src/compiler.c index 4a83c9a..1e9a153 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -57,6 +57,7 @@ Term TERM_Function; Term TERM_Hidden; Term TERM_Type; Term TERM_Nonce; +Term TERM_Ticket; Term TERM_Claim; Term CLAIM_Secret; @@ -101,6 +102,7 @@ compilerInit (const System mysys) langcons (TERM_Agent, "Agent", TERM_Type); langcons (TERM_Function, "Function", TERM_Type); langcons (TERM_Nonce, "Nonce", TERM_Type); + langcons (TERM_Ticket, "Ticket", TERM_Type); langcons (CLAIM_Secret, "Secret", TERM_Claim); langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim); diff --git a/src/mgu.c b/src/mgu.c index 3654fbe..46691b1 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -5,6 +5,7 @@ #include "substitution.h" #include "mgu.h" #include "memory.h" +#include "type.h" /* Most General Unifier @@ -14,17 +15,24 @@ New version yields a termlist with substituted variables, which can later be reset to NULL. */ -//! Global constant. If true, typed checking +//! Internal constant. If true, typed checking /** * Analoguous to sys->match * 0 typed * 1 basic typeflaws * 2 all typeflaws */ -int mgu_match = 0; +static int mgu_match = 0; extern Term TERM_Hidden; +//! Set mgu mode (basically sys->match) +void +setMguMode (const int match) +{ + mgu_match = match; +} + void showSubst (Term t) { @@ -58,76 +66,16 @@ showSubst (Term t) __inline__ int goodsubst (Term tvar, Term tsubst) { - // function to test compatibility - __inline__ int compatibleTypes () - { - if (tvar->stype == NULL) - { - // If the variable type is unspecified, anything goes - return 1; - } - else - { - // There are variable types. - // At least one of them should match a type of the constant. - Termlist tl; + Term tbuf; + int res; - tl = tvar->stype; - while (tl != NULL) - { - if (inTermlist (tsubst->stype, tl->term)) - { - // One type matches - return 1; - } - tl = tl->next; - } - // No matches - return 0; - } - } + tbuf = tvar->subst; + tvar->subst = tsubst; - if (mgu_match == 2) - { - return 1; - } - else - { - /** - * Check if each type of the substitution is allowed in the variable - */ - if (!realTermLeaf (tsubst)) - { - // Typed var cannot match with non-leaf - return 0; - } - else - { - // It's a leaf, but what type? - if (mgu_match == 1 || compatibleTypes ()) - { - return 1; - } - else - { -#ifdef DEBUG - if (DEBUGL (5)) - { - eprintf ("Substitution fails on "); - termPrint (tvar); - eprintf (" -/-> "); - termPrint (tsubst); - eprintf (", because type: \n"); - termlistPrint (tvar->stype); - eprintf (" does not contain "); - termlistPrint (tsubst->stype); - eprintf ("\n"); - } -#endif - return 0; - } - } - } + res = checkTypeTerm (mgu_match, tvar); + + tvar->subst = tbuf; + return res; } //! Undo all substitutions in a list of variables. diff --git a/src/mgu.h b/src/mgu.h index 3b2e04c..62ab659 100644 --- a/src/mgu.h +++ b/src/mgu.h @@ -14,6 +14,7 @@ */ #define MGUFAIL (Termlist) -1 +void setMguMode (const int mgu); Termlist termMguTerm (Term t1, Term t2); int termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist)); int termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist), diff --git a/src/switches.c b/src/switches.c index d972ae1..79c02e3 100644 --- a/src/switches.c +++ b/src/switches.c @@ -12,7 +12,6 @@ #include "timer.h" extern System sys; -extern int mgu_match; extern struct tacnode *spdltac; extern Term TERM_Claim; @@ -232,7 +231,6 @@ switcher (const int process, const System sys, int index) else { sys->match = integer_argument (); - mgu_match = sys->match; return index; } } diff --git a/src/system.c b/src/system.c index b65f4e4..3b21451 100644 --- a/src/system.c +++ b/src/system.c @@ -15,6 +15,7 @@ #include "output.h" #include "tracebuf.h" #include "role.h" +#include "mgu.h" /* from compiler.o */ extern Term TERM_Type; @@ -160,6 +161,9 @@ systemReset (const System sys) globalLatex = sys->latex; + /* propagate mgu_mode */ + + setMguMode (sys->match); } //! Initialize runtime system (according to cut traces, limited runs) diff --git a/src/type.c b/src/type.c new file mode 100644 index 0000000..5497d95 --- /dev/null +++ b/src/type.c @@ -0,0 +1,151 @@ +/* + * type.c + * + * Code to check the consistency of types, in the presence of type flaw stuff etc. + */ + +#include +#include +#include "term.h" +#include "termlist.h" +#include "system.h" +#include "debug.h" + +/* + * Special term definitions from compiler.c + */ +extern Term TERM_Agent; +extern Term TERM_Function; +extern Term TERM_Hidden; +extern Term TERM_Type; +extern Term TERM_Nonce; +extern Term TERM_Ticket; + +extern Protocol INTRUDER; + +//! Report a bad substitution, if needed +void +reportBadSubst (const Term tvar, const Term tsubst) +{ +#ifdef DEBUG + if (DEBUGL (5)) + { + Term tbuf; + + tbuf = tvar->subst; + tvar->subst = NULL; + + eprintf ("Substitution fails on "); + termPrint (tvar); + eprintf (" -/-> "); + termPrint (tsubst); + eprintf (", maybe because type: \n"); + termlistPrint (tvar->stype); + eprintf (" does not contain "); + termlistPrint (tsubst->stype); + eprintf ("\n"); + + tvar->subst = tbuf; + } +#endif +} + +//! Check whether a single variable term is instantiated correctly. +/** + * Check whether a single variable term is instantiated correctly in this + * system. This takes the matching parameter into account, and is aware of the + * 'ticket' type. + * + * Non-variables etc. imply true. + */ +int +checkTypeTerm (const int mgumode, const Term tvar) +{ + // Checks are only needed for mgumode < 2 etc. + if (mgumode < 2 && tvar != NULL && realTermVariable (tvar)) + { + // Non-instantiated terms are fine. + if (tvar->subst != NULL) + { + // NULL type is always fine + if (tvar->stype != NULL) + { + // Tickets are always fine too + if (!inTermlist (tvar->stype, TERM_Ticket)) + { + // So there is a specific (non-ticket) type, and the var is instantiated, match mode 0 or 1 + // Is it really a leaf? + Term tsubst; + + tsubst = deVar (tvar); + if (!realTermLeaf (tsubst)) + { + // Then it's definitively false + reportBadSubst (tvar, tsubst); + return false; + } + else + { + // It is a leaf + if (mgumode == 0) + { + /* Types must match exactly. Thus, one of the variable type should match a type of the constant. + */ + Termlist tl; + + tl = tvar->stype; + while (tl != NULL) + { + if (inTermlist (tsubst->stype, tl->term)) + { + // One type matches + return true; + } + tl = tl->next; + } + // No type matches. + reportBadSubst (tvar, tsubst); + return false; + } + } + } + } + } + } + return true; +} + +//! Check types of a list +/** + * Empty list implies true. + */ +int +checkTypeTermlist (const int mgumode, Termlist tl) +{ + while (tl != NULL) + { + if (!checkTypeTerm (mgumode, tl->term)) + return false; + tl = tl->next; + } + return true; +} + +//! Check whether all local variables are instantiated correctly. +int +checkTypeLocals (const System sys) +{ + int run; + + run = 0; + while (run < sys->maxruns) + { + if (sys->runs[run].protocol != INTRUDER) + { + if (!checkTypeTermlist (sys->match, sys->runs[run].locals)) + return false; + } + run++; + } + return true; +} diff --git a/src/type.h b/src/type.h new file mode 100644 index 0000000..4681c8b --- /dev/null +++ b/src/type.h @@ -0,0 +1,11 @@ +#ifndef TYPE +#define TYPE + +#include "term.h" +#include "system.h" + +int checkTypeTerm (const int mgumode, const Term t); +int checkTypeTermlist (const int mgumode, Termlist tl); +int checkTypeLocals (const System sys); + +#endif