From 4d1362cb1be2b503fc315c8a837e12bfc4cbc92a Mon Sep 17 00:00:00 2001 From: ccremers Date: Mon, 9 Aug 2004 09:42:58 +0000 Subject: [PATCH] - Implemented --check=Secret switch, which allows checking of specific properties. - Fixed a bug in the symbol table, where symbols were never inserted into the hash table. --- src/compiler.c | 51 ++++++++++++++++++++++++++++++++++++---------- src/compiler.h | 6 +++++- src/main.c | 33 +++++++++++++++++++++++++++++- src/modelchecker.c | 1 + src/symbol.c | 41 +++++++++++++++++++++++++++++++------ src/symbol.h | 13 ++++++------ src/system.c | 1 + src/system.h | 1 + src/term.c | 6 +++--- src/todo.txt | 2 -- 10 files changed, 125 insertions(+), 30 deletions(-) diff --git a/src/compiler.c b/src/compiler.c index f027a36..2f29d50 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -18,6 +18,7 @@ */ static System sys; +static Tac tac_root; /* Forward declarations. @@ -67,20 +68,12 @@ static int maxruns; static Protocol thisProtocol; static Role thisRole; -/* ------------------------------------------------------------------- */ - -//! Compile the tac into the system -/** - *@todo Currently, the semantics assume all labels are globally unique, but this is not enforced yet. There should be some automatic renaming when compositing protocols. - *\sa oki_nisynch - */ +//! Init terms and such void -compile (const System mysys, Tac tc, int maxrunsset) +compilerInit (const System mysys) { int i; - /* Init globals */ - maxruns = maxrunsset; /* transfer to global static variable */ sys = mysys; /* init levels */ @@ -105,9 +98,30 @@ compile (const System mysys, Tac tc, int maxrunsset) langcons (CLAIM_Secret, "Secret", TERM_Claim); langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim); langcons (CLAIM_Niagree, "Niagree", TERM_Claim); +} +//! Clean up afterwards +void +compilerDone (void) +{ + return; +} + +/* ------------------------------------------------------------------- */ + +//! Compile the tac into the system +/** + *@todo Currently, the semantics assume all labels are globally unique, but this is not enforced yet. There should be some automatic renaming when compositing protocols. + *\sa oki_nisynch + */ +void +compile (Tac tc, int maxrunsset) +{ + /* Init globals */ + maxruns = maxrunsset; + tac_root = tc; /* process the tac */ - tacProcess (tc); + tacProcess (tac_root); /* cleanup */ levelDone (); @@ -228,6 +242,12 @@ symbolFind (Symbol s) return NULL; } +//! Yield a basic global constant term (we suppose it exists) or NULL, given a string +Term findGlobalConstant (const char *s) +{ + return levelFind (lookup (s), 0); +} + void defineUsertype (Tac tcdu) { @@ -372,6 +392,15 @@ commEvent (int event, Tac tc) /* check for several types */ claim = tupleProject (claimbig, 0); torole = claim; + + /* check for ignored claim types */ + if (sys->switchClaimToCheck != NULL && + sys->switchClaimToCheck != claim) + { + /* abort the construction of the node */ + return; + } + /* check for obvious flaws */ if (claim == NULL) { diff --git a/src/compiler.h b/src/compiler.h index b2668aa..62e85a1 100644 --- a/src/compiler.h +++ b/src/compiler.h @@ -1,7 +1,11 @@ #ifndef COMPILER #define COMPILER -void compile (const System sys, Tac tc, int maxruns); +void compilerInit (const System sys); +void compilerDone (void); + +void compile (Tac tc, int maxruns); void preprocess (const System sys); +Term findGlobalConstant (const char *s); #endif diff --git a/src/main.c b/src/main.c index a2aff51..2f4fbfe 100644 --- a/src/main.c +++ b/src/main.c @@ -57,6 +57,7 @@ #include "argtable2.h" extern struct tacnode *spdltac; +extern Term TERM_Claim; void scanner_cleanup (void); void strings_cleanup (void); int yyparse (void); @@ -83,6 +84,7 @@ main (int argc, char **argv) struct arg_file *infile = arg_file0(NULL,NULL,"FILE", "input file ('-' for stdin)"); struct arg_file *outfile = arg_file0("o","output","FILE", "output file (default is stdout)"); + struct arg_str *switch_check = arg_str0(NULL,"check","CLAIM","claim type to check (default is all)"); struct arg_int *switch_scenario = arg_int0 ("s", "scenario", NULL, "select a scenario instance 1-n (-1 to count)"); struct arg_int *switch_scenario_size = @@ -140,6 +142,7 @@ main (int argc, char **argv) switch_echo, switch_progress_bar, + switch_check, switch_traversal_method, switch_match_method, switch_clp, @@ -300,6 +303,8 @@ main (int argc, char **argv) */ sys = systemInit (); + /* init compiler for this system */ + compilerInit (sys); /* transfer command line */ sys->argc = argc; @@ -369,6 +374,31 @@ main (int argc, char **argv) sys->latex = switch_latex_output->count; sys->know = emptyKnowledge (); + + /* parse compiler-dependant switches */ + if (switch_check->count > 0) + { + Term claim; + +#ifdef DEBUG + if (lookup(switch_check->sval[0]) == NULL) + { + globalError++; + warning ("Could not find this string at all in:"); + symbolPrintAll (); + eprintf ("\n"); + globalError--; + } +#endif + claim = findGlobalConstant (switch_check->sval[0]); + if (claim == NULL) + error ("Unknown claim type to check."); + if (inTermlist (claim->stype, TERM_Claim)) + sys->switchClaimToCheck = claim; + else + error ("Claim type to check is not a claim."); + } + /* parse input */ yyparse (); @@ -379,7 +409,7 @@ main (int argc, char **argv) /* compile */ - compile (sys, spdltac, switch_maximum_runs->ival[0]); + compile (spdltac, switch_maximum_runs->ival[0]); scanner_cleanup (); /* preprocess */ @@ -548,6 +578,7 @@ main (int argc, char **argv) knowledgeDestroy (sys->know); systemDone (sys); + compilerDone (); /* done symbols */ tacDone (); diff --git a/src/modelchecker.c b/src/modelchecker.c index 025213a..d37acdd 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -1037,6 +1037,7 @@ traversePOR8 (const System sys) //! Check for the properties that have lasting effects throughout the trace. /** * Currently, only functions for secrecy. + *@returns 1 (true) iff everything is okay, and no attack is found. 0 (false) if an attack is found. */ int diff --git a/src/symbol.c b/src/symbol.c index 939a8da..98a18cb 100644 --- a/src/symbol.c +++ b/src/symbol.c @@ -84,7 +84,7 @@ get_symb (void) //! Declare a symbol to be freed. void -free_symb (Symbol s) +free_symb (const Symbol s) { if (s == NULL) return; @@ -94,7 +94,7 @@ free_symb (Symbol s) //! Return the index in the hash table for the string. int -hash (char *s) +hash (const char *s) { int hv = 0; int i; @@ -110,7 +110,7 @@ hash (char *s) //! Insert a string into the hash table. void -insert (Symbol s) +insert (const Symbol s) { int hv; @@ -124,7 +124,7 @@ insert (Symbol s) //! Find a string in the hash table. Symbol -lookup (char *s) +lookup (const char *s) { int hv; Symbol t; @@ -147,7 +147,7 @@ lookup (char *s) //! Print a symbol. void -symbolPrint (Symbol s) +symbolPrint (const Symbol s) { if (s == NULL) return; @@ -156,13 +156,41 @@ symbolPrint (Symbol s) eprintf ("%s", s->text); } +//! Print all symbols +void +symbolPrintAll (void) +{ + int i, count; + + eprintf ("List of all symbols\n"); + count = 0; + for (i = 0; i < HASHSIZE; i++) + { + Symbol sym; + + sym = symbtab[i]; + if (sym != NULL) + { + eprintf ("H%i:\t", i); + while (sym != NULL) + { + count++; + eprintf ("[%s]\t", sym->text); + sym = sym->next; + } + eprintf ("\n"); + } + } + eprintf ("Total:\t%i\n", count); +} + //! Insert a string into the symbol table, if it wasn't there yet. /** * Also sets line numbers and type. *\sa T_SYSCONST */ Symbol -symbolSysConst (char *str) +symbolSysConst (const char *str) { Symbol symb; @@ -173,6 +201,7 @@ symbolSysConst (char *str) symb->lineno = yylineno; symb->type = T_SYSCONST; symb->text = str; + insert (symb); } return symb; } diff --git a/src/symbol.h b/src/symbol.h index c992324..88bb505 100644 --- a/src/symbol.h +++ b/src/symbol.h @@ -20,7 +20,7 @@ struct symbol //! Line number at which it occurred. int lineno; //! Ascii string with name of the symbol. - char *text; + const char *text; //! Possible next pointer. struct symbol *next; //! Used for linking all symbol blocks, freed or in use. @@ -33,12 +33,13 @@ void symbolsInit (void); void symbolsDone (void); Symbol get_symb (void); -void free_symb (Symbol s); +void free_symb (const Symbol s); -void insert (Symbol s); -Symbol lookup (char *s); -void symbolPrint (Symbol s); -Symbol symbolSysConst (char *str); +void insert (const Symbol s); +Symbol lookup (const char *s); +void symbolPrint (const Symbol s); +void symbolPrintAll (void); +Symbol symbolSysConst (const char *str); void eprintf (char *fmt, ... ); diff --git a/src/system.c b/src/system.c index c87e212..92c5622 100644 --- a/src/system.c +++ b/src/system.c @@ -67,6 +67,7 @@ systemInit () sys->switchNomoreClaims = 1; // default cutter when there are no more claims sys->switchReduceEndgame = 1; // default cutter of last events in a trace sys->switchClaims = 0; // default don't report on claims + sys->switchClaimToCheck = NULL; // default check all claims /* set illegal traversal by default, to make sure it is set later */ diff --git a/src/system.h b/src/system.h index cd39c24..95827a4 100644 --- a/src/system.h +++ b/src/system.h @@ -130,6 +130,7 @@ struct system int switchNomoreClaims; //!< Enable no more claims cutter int switchReduceEndgame; //!< Enable endgame cutter int switchClaims; //!< Enable clails report + Term switchClaimToCheck; //!< Which claim should be checked? //! Latex output switch. /** diff --git a/src/term.c b/src/term.c index 2d0927a..5c0da7b 100644 --- a/src/term.c +++ b/src/term.c @@ -832,9 +832,9 @@ int termOrder (Term t1, Term t2) /* compare names */ int comp; - name1 = t1->left.symb->text; - name2 = t2->left.symb->text; - comp = strcmp (name1,name2); + comp = strcmp (t1->left.symb->text, + t2->left.symb->text + ); if (comp != 0) { /* names differ */ diff --git a/src/todo.txt b/src/todo.txt index 6d0adb1..592ac73 100644 --- a/src/todo.txt +++ b/src/todo.txt @@ -7,8 +7,6 @@ - Intruder should at least have one copy of each type that an agent can construct, I think in any case. Proof needed for single identifier need. Furthermore reduction if type flaw testing; only one constant needed. -- Make filter switch, allowing maybe for some claims only to be evaluated. - --check=Secret, --check-all as default. - Make --with-argtabledir= something switch, replacing README/galious-configure.sh constructs. - Move initial intruder knowledge maybe into the title of the MSC.