diff --git a/src/arachne.c b/src/arachne.c index 934843f..f0ea864 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -43,34 +43,34 @@ extern int *graph; extern int nodes; extern int graph_uordblks; -static System sys; +static System sys; //!< local buffer for the system pointer -int attack_length; -int attack_leastcost; +int attack_length; //!< length of the attack +int attack_leastcost; //!< cost of the best attack sofar \sa cost.c -Protocol INTRUDER; // Pointers, to be set by the Init -Role I_M; // Same here. -Role I_RRS; -Role I_RRSD; +Protocol INTRUDER; //!< intruder protocol +Role I_M; //!< Initial knowledge role of the intruder +Role I_RRS; //!< Encrypt role of the intruder +Role I_RRSD; //!< Decrypt role of the intruder -int proofDepth; -int max_encryption_level; -int num_regular_runs; -int num_intruder_runs; +int proofDepth; //!< Current depth of the proof +int max_encryption_level; //!< Maximum encryption level of any term +int num_regular_runs; //!< Current number of regular runs +int num_intruder_runs; //!< Current number of intruder runs static int indentDepth; static int prevIndentDepth; static int indentDepthChanges; static FILE *attack_stream; -/** +/* * Forward declarations */ int iterate (); void printSemiState (); -/** +/* * Program code */ @@ -151,14 +151,12 @@ arachneDone () // Detail //------------------------------------------------------------------------ -/* - * runs[rid].step is now the number of 'valid' events within the run, but we - * call it 'length' here. - */ +//! Just a defined integer for invalid #define INVALID -1 +//! can this roledef constitute a read Goal? #define isGoal(rd) (rd->type == READ && !rd->internal) +//! is this roledef already bound? #define isBound(rd) (rd->bound) -#define length step //! Indent prefix print void @@ -303,7 +301,7 @@ semiRunCreate (const Protocol p, const Role r) num_regular_runs++; roleInstance (sys, p, r, NULL, NULL); run = sys->maxruns - 1; - sys->runs[run].length = 0; + sys->runs[run].height = 0; return run; } @@ -359,7 +357,7 @@ fixAgentKeylevels (void) //! After a role instance, or an extension of a run, we might need to add some goals /** - * From old to new. Sets the new length to new. + * From old to new. Sets the new height to new. *@returns The number of goals added (for destructions) */ int @@ -369,7 +367,7 @@ add_read_goals (const int run, const int old, const int new) int i; Roledef rd; - sys->runs[run].length = new; + sys->runs[run].height = new; i = old; rd = roledef_shift (sys->runs[run].start, i); count = 0; @@ -465,7 +463,7 @@ get_semitrace_length () { // Non-intruder run: count length // Subtract 'firstReal' to ignore chooses. - length = length + sys->runs[run].length - sys->runs[run].firstReal; + length = length + sys->runs[run].height - sys->runs[run].firstReal; } run++; } @@ -674,6 +672,7 @@ iterate_role_sends (int (*func) ()) * Note that this does not add any bindings for the reads. * *@param term The term to be decrypted (implies decryption key) + *@param key The key that is needed to decrypt the term * *@returns The run id of the decryptor instance */ @@ -691,7 +690,7 @@ create_decryptor (const Term term, const Term key) rd->message = termDuplicateUV (term); rd->next->message = termDuplicateUV (key); rd->next->next->message = termDuplicateUV (TermOp (term)); - sys->runs[run].step = 3; + sys->runs[run].height = 3; proof_suppose_run (run, 0, 3); return run; @@ -739,7 +738,9 @@ getPriorityOfNeededKey (const System sys, const Term keyneeded) * needed keys, but simply the path throught the term. This would enable * reconstruction of the keys anyway. TODO * - *@param subterm determines whether it is a subterm unification or not. + *@param b binding to fix (bind), destination filled in + *@param run run of binding start + *@param index index in run of binding start */ int bind_existing_to_goal (const Binding b, const int run, const int index) @@ -914,7 +915,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index) rd = roledef_shift (sys->runs[run].start, index); // Fix length - old_length = sys->runs[run].length; + old_length = sys->runs[run].height; if ((index + 1) > old_length) newgoals = add_read_goals (run, old_length, index + 1); else @@ -935,7 +936,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index) } // Reset length goal_remove_last (newgoals); - sys->runs[run].length = old_length; + sys->runs[run].height = old_length; return flag; } @@ -1055,7 +1056,7 @@ printSemiState () index = 0; rd = sys->runs[run].start; - while (index < sys->runs[run].length) + while (index < sys->runs[run].height) { indentPrint (); eprintf ("!! %i ", index); @@ -1110,7 +1111,6 @@ bind_old_goal (const Binding b_new) } //! Create a new intruder run to generate knowledge from m0 - int bind_goal_new_m0 (const Binding b) { @@ -1137,7 +1137,7 @@ bind_goal_new_m0 (const Binding b) I_M->roledef->message = m0t; run = semiRunCreate (INTRUDER, I_M); proof_suppose_run (run, 0, 1); - sys->runs[run].length = 1; + sys->runs[run].height = 1; { indentDepth++; if (goal_bind (b, run, 0)) @@ -1394,7 +1394,7 @@ bind_goal_regular_run (const Binding b) } -// Bind to all possible sends of intruder runs +//! Bind to all possible sends of intruder runs int bind_goal_old_intruder_run (Binding b) { @@ -1413,7 +1413,7 @@ bind_goal_old_intruder_run (Binding b) rd = sys->runs[run].start; ev = 0; - while (ev < sys->runs[run].length) + while (ev < sys->runs[run].height) { if (rd->type == SEND) { @@ -2207,19 +2207,19 @@ knowledgeAtArachne (const System sys, const int myrun, const int myindex, while (run < sys->maxruns) { int index; - int maxstep; + int maxheight; Roledef rd; index = 0; rd = sys->runs[run].start; - maxstep = sys->runs[run].step; - if (run == myrun && myindex > maxstep) + maxheight = sys->runs[run].height; + if (run == myrun && myindex > maxheight) { // local run index can override real step - maxstep = myindex; + maxheight = myindex; } - while (rd != NULL && index < maxstep) + while (rd != NULL && index < maxheight) { // Check whether this event precedes myevent if (aftercomplete || isOrderedBefore (run, index, myrun, myindex)) diff --git a/src/arachne.h b/src/arachne.h index f6ae052..1474d4a 100644 --- a/src/arachne.h +++ b/src/arachne.h @@ -13,13 +13,17 @@ int isTriviallyKnownAtArachne (const System sys, const Term t, const int run, int isTriviallyKnownAfterArachne (const System sys, const Term t, const int run, const int index); +//! Goal structure +/** + * Signals a read event or claim event to which a term has to be bound. + */ struct goalstruct { - int run; - int index; - Roledef rd; + int run; //!< run of goal + int index; //!< index of goal in the run + Roledef rd; //!< pointer to the role definition }; -typedef struct goalstruct Goal; +typedef struct goalstruct Goal; //!< pointer to goal structure #endif diff --git a/src/binding.c b/src/binding.c index 08aae3e..a8fa0a3 100644 --- a/src/binding.c +++ b/src/binding.c @@ -16,13 +16,13 @@ #include "switches.h" #include -static System sys; -int *graph = NULL; -int nodes = 0; +static System sys; //!< local storage of system pointer +int *graph = NULL; //!< graph data +int nodes = 0; //!< number of nodes in the graph int graph_uordblks = 0; -extern Protocol INTRUDER; // The intruder protocol -extern Role I_M; // special role; precedes all other events always +extern Protocol INTRUDER; //!< The intruder protocol +extern Role I_M; //!< special role; precedes all other events always /* * Forward declarations diff --git a/src/binding.h b/src/binding.h index d031c9e..ace1863 100644 --- a/src/binding.h +++ b/src/binding.h @@ -5,6 +5,7 @@ #include "termmap.h" #include "system.h" +//! Binding structure /* * Idea is the ev_from *has to* precede the ev_to */ @@ -13,20 +14,17 @@ struct binding int done; //!< Iff true, it is bound int blocked; //!< Iff true, ignore it - int run_from; - int ev_from; + int run_from; //!< origination run + int ev_from; //!< step in origination run - int run_to; - int ev_to; + int run_to; //!< destination run + int ev_to; //!< step in destination run - int *graph; - int nodes; - - Term term; - int level; + Term term; //!< Binding term + int level; //!< ??? }; -typedef struct binding *Binding; +typedef struct binding *Binding; //!< pointer to binding structure void bindingInit (const System mysys); diff --git a/src/claim.c b/src/claim.c index a3157d6..025df48 100644 --- a/src/claim.c +++ b/src/claim.c @@ -19,12 +19,18 @@ #include "switches.h" #include "memory.h" +//! When none of the runs match #define MATCH_NONE 0 +//! When the order matches #define MATCH_ORDER 1 +//! When the order is reversed #define MATCH_REVERSE 2 +//! When the content matches #define MATCH_CONTENT 3 +//! This label is fixed #define LABEL_GOOD -3 +//! This label still needs to be done #define LABEL_TODO -2 extern int globalError; diff --git a/src/color.c b/src/color.c index 7eca4cf..6eb56a8 100644 --- a/src/color.c +++ b/src/color.c @@ -8,12 +8,18 @@ #include #include "switches.h" +//! Substitution string for --plain output char *empty = ""; +//! Reset colors char *COLOR_Reset = ""; +//! Red char *COLOR_Red = ""; +//! Green char *COLOR_Green = ""; +//! Bold char *COLOR_Bold = ""; +//! Init colors void colorInit (void) { @@ -26,6 +32,7 @@ colorInit (void) } } +//! Exit colors void colorDone (void) { diff --git a/src/cost.c b/src/cost.c index 27e3da6..d287560 100644 --- a/src/cost.c +++ b/src/cost.c @@ -12,6 +12,7 @@ // Private methods //************************************************************************ +//! determine whether a run is a so-called self-initiator int selfInitiator (const System sys, const int run) { diff --git a/src/error.c b/src/error.c index 7b29ef8..58c126b 100644 --- a/src/error.c +++ b/src/error.c @@ -6,7 +6,7 @@ void error_die (void) { - exit (1); + exit (EXIT_ERROR); } //! Print error message header @@ -34,7 +34,7 @@ error_post (char *fmt, ...) vfprintf (stderr, fmt, args); fprintf (stderr, "\n"); va_end (args); - exit (1); + exit (EXIT_ERROR); } //! Print error message and die. diff --git a/src/error.h b/src/error.h index 7218a6f..31facbc 100644 --- a/src/error.h +++ b/src/error.h @@ -1,6 +1,10 @@ #ifndef ERROR #define ERROR +//! Types of exit codes +enum exittypes +{ EXIT_NOATTACK = 0, EXIT_ERROR = 1, EXIT_NOCLAIM = 2, EXIT_ATTACK = 3 }; + void error_die (void); void error_pre (void); void error_post (char *fmt, ...); diff --git a/src/heuristic.c b/src/heuristic.c index b5172eb..2923092 100644 --- a/src/heuristic.c +++ b/src/heuristic.c @@ -13,8 +13,6 @@ #include "specialterm.h" #include "switches.h" -#define length step - //! Check whether a binding (goal) is selectable int is_goal_selectable (const Binding b) @@ -99,7 +97,7 @@ termBindConsequences (const System sys, Term t) rd = sys->runs[run].start; step = 0; - while (step < sys->runs[run].length) + while (step < sys->runs[run].height) { Termlist tl; diff --git a/src/knowledge.h b/src/knowledge.h index 11fb186..6353c71 100644 --- a/src/knowledge.h +++ b/src/knowledge.h @@ -14,6 +14,7 @@ struct knowledge Termlist basic; //! A list of terms encrypted, such that the inverse is not in the knowledge set. Termlist encrypt; + //! List of inverse pairs (thus length of list is even) Termlist inverses; //! List of open variables in the knowledge set. /** diff --git a/src/list.h b/src/list.h index 1631b01..e612e26 100644 --- a/src/list.h +++ b/src/list.h @@ -1,14 +1,15 @@ #ifndef GENERICLIST #define GENERICLIST +//! generic list structure node struct list_struct { - struct list_struct *next; - struct list_struct *prev; - void *data; + struct list_struct *next; //!< pointer to next node + struct list_struct *prev; //!< pointer to previous node + void *data; //!< pointer to the actual data element (should be typecast) }; -typedef struct list_struct *List; +typedef struct list_struct *List; //!< pointer to generic list node List list_create (const void *data); List list_rewind (List list); diff --git a/src/main.c b/src/main.c index 38a2687..7902cf9 100644 --- a/src/main.c +++ b/src/main.c @@ -37,9 +37,6 @@ * be done for any style using the GNU indent program. */ -enum exittypes -{ EXIT_NOATTACK = 0, EXIT_ERROR = 1, EXIT_NOCLAIM = 2, EXIT_ATTACK = 3 }; - #include #include #include @@ -61,11 +58,14 @@ enum exittypes #include "switches.h" #include "specialterm.h" #include "color.h" +#include "error.h" -// The global system state +//! The global system state pointer System sys; +//! Pointer to the tac node container extern struct tacnode *spdltac; +//! Match mode extern int mgu_match; void scanner_cleanup (void); diff --git a/src/role.c b/src/role.c index 9caed03..3bd3c48 100644 --- a/src/role.c +++ b/src/role.c @@ -1,5 +1,5 @@ /** - * @file roles.c + * @file role.c * \brief role related logic. */ #include @@ -108,12 +108,14 @@ roledefPrintGeneric (Roledef rd, int print_actor) eprintf ("$"); } +//! Print a roledef void roledefPrint (Roledef rd) { roledefPrintGeneric (rd, 1); } +//! Print a roledef, but shorten it void roledefPrintShort (Roledef rd) { diff --git a/src/role.h b/src/role.h index 11675ed..cb7b25e 100644 --- a/src/role.h +++ b/src/role.h @@ -103,7 +103,7 @@ struct roledef /* * Bindings for Arachne engine */ - int bound; + int bound; //!< determines whether it is already bound /* evt runid for synchronisation, but that is implied in the base array */ diff --git a/src/substitution.h b/src/substitution.h index c134ff4..9657fb5 100644 --- a/src/substitution.h +++ b/src/substitution.h @@ -5,21 +5,23 @@ #include "knowledge.h" #include "system.h" +//! substitution structure struct substitution { Term from; Term to; }; -typedef struct substitution *Substitution; +typedef struct substitution *Substitution; //!< substitution structure +//! substitution list struct substitutionlist { Substitution subst; struct substitutionlist *next; }; -typedef struct substitutionlist *Substitutionlist; +typedef struct substitutionlist *Substitutionlist; //!< substitution list structure Substitution makeSubstitution (Term from, Term to); diff --git a/src/switches.h b/src/switches.h index 59eac5e..53e93d6 100644 --- a/src/switches.h +++ b/src/switches.h @@ -79,6 +79,6 @@ struct switchdata int latex; }; -extern struct switchdata switches; +extern struct switchdata switches; //!< pointer to switchdata structure #endif diff --git a/src/symbol.h b/src/symbol.h index 1503cc8..d727cd3 100644 --- a/src/symbol.h +++ b/src/symbol.h @@ -13,6 +13,7 @@ enum symboltypes #define EOS 0 +//! Symbol structure struct symbol { //! Type of symbol. @@ -32,7 +33,7 @@ struct symbol struct symbol *allocnext; }; -typedef struct symbol *Symbol; +typedef struct symbol *Symbol; //!< pointer to symbol structure void symbolsInit (void); void symbolsDone (void); diff --git a/src/system.h b/src/system.h index f81d04e..09e051b 100644 --- a/src/system.h +++ b/src/system.h @@ -207,4 +207,11 @@ int isAgentTrusted (const System sys, Term agent); int isAgentlistTrusted (const System sys, Termlist agents); int isRunTrusted (const System sys, const int run); +//! Equality for run structure naming +/** + * For the modelchecker, there was an index called step. In Strand Space + * terminology, something like that is the height of the strand. + */ +#define height step + #endif diff --git a/src/tac.h b/src/tac.h index 99e42fe..606d4fa 100644 --- a/src/tac.h +++ b/src/tac.h @@ -31,13 +31,14 @@ enum tactypes TAC_USERTYPE }; +//! Structure to hold the compilation tree nodes struct tacnode { - struct tacnode *next; - struct tacnode *prev; + struct tacnode *next; //!< pointer to previous node + struct tacnode *prev; //!< pointer to next node struct tacnode *allnext; - int op; - int lineno; + int op; //!< operator for this node + int lineno; //!< line number of parser location in the input file union { Symbol sym; diff --git a/src/term.c b/src/term.c index cb77890..942f892 100644 --- a/src/term.c +++ b/src/term.c @@ -1,4 +1,4 @@ -/** @file terms.c \brief Term related base functions. +/** @file term.c \brief Term related base functions. * * Intended to be a standalone file, however during development it turned out * that a termlist structure was needed to define term types, so there is now a @@ -7,7 +7,7 @@ * Until now, symbols were unique and never deleted. The same holds for basic * terms; leaves are equal when their pointers are equal. We are looking to * extend this to whole terms. At that point, term equality is be reduced to - * pointer comparison, which is what we want. However, for comparison of terms + * pointer comparison, which is what we want. */ #include @@ -34,6 +34,7 @@ void indent (void); /* useful macros */ +//! Undefined run identifier in a term #define RID_UNDEF MIN_INT /* main code */ @@ -507,7 +508,6 @@ termDuplicateDeep (const Term term) * Remove all instantiated variables on the way down. *\sa termDuplicate() */ - Term termDuplicateUV (Term term) { @@ -534,14 +534,7 @@ termDuplicateUV (Term term) return newterm; } -/* - -realTermDuplicate - -make a deep copy of a term, also of leaves. - -*/ - +//! Make a deep copy of a term, also of leaves Term realTermDuplicate (const Term term) { @@ -1149,7 +1142,7 @@ term_encryption_level (const Term term) //! Determine 'constrained factor' of a term /** - * Actually this is (#vars/structure). + * Actually this is (number of vars/structure). * Thus, 0 means very constrained, no variables. * Everything else has higher float, but always <=1. In fact, only a single variable has a level 1. */ diff --git a/src/term.h b/src/term.h index 0428ba1..4c58f7b 100644 --- a/src/term.h +++ b/src/term.h @@ -30,7 +30,7 @@ struct term //! Data Type termlist (e.g. agent or nonce) /** Only for leaves. */ void *stype; // list of types - int roleVar; // only for leaf, arachne engine: role variable flag + int roleVar; //!< only for leaf, arachne engine: role variable flag //! Substitution term. /** @@ -41,15 +41,17 @@ struct term union { + //! Pointer to the symbol for leaves Symbol symb; //! Encrypted subterm. struct term *op; //! Left-hand side of tuple pair. struct term *op1; - struct term *next; // for alternative memory management + struct term *next; //!< for alternative memory management } left; union { + //! run identifier for leaves int runid; //! Key used to encrypt subterm. struct term *key; diff --git a/src/termlist.c b/src/termlist.c index ee1279e..b10b574 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -5,14 +5,14 @@ #include "debug.h" #include "memory.h" -/** +/* * Shared stuff */ //! Termlist error thing (for global use) Termlist TERMLISTERROR; -/** +/* * Forward declarations */ diff --git a/src/warshall.c b/src/warshall.c index e131e0f..d181a1c 100644 --- a/src/warshall.c +++ b/src/warshall.c @@ -1,11 +1,16 @@ /** + *@file warshall.c + * * Warshall's algorithm for transitive closure computation. + * + * Currently this is the slow integer-instead-of-bit olde slowe version. */ #include #include "warshall.h" #include "debug.h" +//! fill the graph with some value void graph_fill (int *graph, int nodes, int value) {