diff --git a/src/arachne.c b/src/arachne.c index 32b4270..d97bd81 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -10,6 +10,7 @@ #include #include #include +#include #ifdef DEBUG #include #endif @@ -23,7 +24,6 @@ #include "states.h" #include "mgu.h" #include "arachne.h" -#include "memory.h" #include "error.h" #include "claim.h" #include "debug.h" @@ -167,11 +167,8 @@ indentPrefixPrint (const int annotate, const int jumps) { void counterPrint () { - if (switches.engine == ARACHNE_ENGINE) - { - statesFormat (sys->current_claim->states); - eprintf ("\t"); - } + statesFormat (sys->current_claim->states); + eprintf ("\t"); eprintf ("%i", annotate); eprintf ("\t"); } @@ -1770,7 +1767,7 @@ createNewTermGeneric (Termlist tl, Term t) } /* Make a new term with the free number */ - newterm = (Term) memAlloc (sizeof (struct term)); + newterm = (Term) malloc (sizeof (struct term)); memcpy (newterm, t, sizeof (struct term)); TermRunid (newterm) = freenumber; @@ -1839,7 +1836,7 @@ deleteNewTerm (Term t) /* if it has a positive runid, it did not come from the intruder * knowledge, so it must have been constructed. */ - memFree (t, sizeof (struct term)); + free (t); } } diff --git a/src/attackminimize.c b/src/attackminimize.c deleted file mode 100644 index bd186df..0000000 --- a/src/attackminimize.c +++ /dev/null @@ -1,142 +0,0 @@ -#include -#include -#include "system.h" -#include "tracebuf.h" - -//! Help counter for the number of unknowns. -int cUnk = 0; -//! Help counter for the number of todos. -int cTod = 0; - -//! Mark all events of the same run before the event as required. -/** - *@param sys The system. - *@param tb The attack buffer. - *@param ev The reference event index. - */ -void -markback (const System sys, struct tracebuf *tb, int ev) -{ - int run = tb->run[ev]; - - while (ev >= 0) - { - if (tb->run[ev] == run) - { - switch (tb->event[ev]->type) - { - case READ: - switch (tb->status[ev]) - { - case S_UNK: - cUnk--; - case S_RED: - tb->status[ev] = S_TOD; - cTod++; - break; - case S_TOD: - case S_OKE: - break; - } - break; - case SEND: - case CLAIM: - if (tb->status[ev] == S_UNK) - { - cUnk--; - } - tb->status[ev] = S_OKE; - break; - } - } - ev--; - } -} - -//! Minimize the attack. -void -attackMinimize (const System sys, struct tracebuf *tb) -{ - int i; - int j; - - cUnk = 0; - cTod = 0; - - for (i = 0; i < tb->length; i++) - { - switch (tb->status[i]) - { - case S_UNK: - cUnk++; - break; - case S_TOD: - cTod++; - break; - default: - break; - } - } - - markback (sys, tb, tb->violatedclaim); - - while (cUnk + cTod > 0) - { - while (cTod > 0) - { - for (i = 0; i < tb->length; i++) - // kies een i; laten we de eerste maar pakken - { - if (tb->status[i] == S_TOD) - break; - } - if (i == tb->length) - { - eprintf ("Some step error.\n"); - exit (1); - } - - j = i; - while (j >= 0 && inKnowledge (tb->know[j], tb->event[i]->message)) - { - // zoek waar m in de kennis komt - j--; - } - tb->status[i] = S_OKE; - cTod--; - if (j >= 0) - { - markback (sys, tb, j); - } - } - while (cTod == 0 && cUnk > 0) - { - for (i = tb->length - 1; i >= 0; i--) - // pak laatste i - { - if (tb->status[i] == S_UNK) - break; - } - if (i < 0) - { - eprintf ("Some i<0 error.\n"); - exit (1); - } - - tb->status[i] = S_RED; - cUnk--; - tb->reallength--; - - j = tracebufRebuildKnow (tb); - if (j > -1) - { - tb->reallength++; - markback (sys, tb, i); - if (j < tb->length) - { - tb->link[j] = (tb->link[j] > i ? tb->link[j] : i); - } - } - } - } -} diff --git a/src/attackminimize.h b/src/attackminimize.h deleted file mode 100644 index 79fa64a..0000000 --- a/src/attackminimize.h +++ /dev/null @@ -1 +0,0 @@ -void attackMinimize (const System sys, struct tracebuf *tb); diff --git a/src/binding.c b/src/binding.c index 96fa42f..8842773 100644 --- a/src/binding.c +++ b/src/binding.c @@ -8,7 +8,6 @@ #include "system.h" #include "binding.h" #include "warshall.h" -#include "memory.h" #include "debug.h" #include "term.h" #include "termmap.h" @@ -34,7 +33,7 @@ binding_create (Term term, int run_to, int ev_to) { Binding b; - b = memAlloc (sizeof (struct binding)); + b = malloc (sizeof (struct binding)); b->done = false; b->blocked = false; b->run_from = -1; @@ -54,7 +53,7 @@ binding_destroy (Binding b) { goal_unbind (b); } - memFree (b, sizeof (struct binding)); + free (b); } /* diff --git a/src/claim.c b/src/claim.c index 21d3dcf..57701c2 100644 --- a/src/claim.c +++ b/src/claim.c @@ -17,7 +17,6 @@ #include "arachne.h" #include "specialterm.h" #include "switches.h" -#include "memory.h" //! When none of the runs match #define MATCH_NONE 0 diff --git a/src/compiler.c b/src/compiler.c index 4e179ac..a8e7581 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -5,7 +5,6 @@ #include "term.h" #include "termlist.h" #include "label.h" -#include "memory.h" #include "system.h" #include "knowledge.h" #include "symbol.h" @@ -438,7 +437,7 @@ claimCreate (const System sys, const Protocol protocol, const Role role, } // Assert: label is unique, add claimlist info - cl = memAlloc (sizeof (struct claimlist)); + cl = malloc (sizeof (struct claimlist)); cl->type = claim; cl->label = label; cl->parameter = msg; @@ -1003,15 +1002,9 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles) Term rolename; Role r; - if (switches.engine == ARACHNE_ENGINE) - { - rolename = levelVar (tcroles->t1.sym); - rolename->stype = termlistAdd (NULL, TERM_Agent); - } - else - { - rolename = levelConst (tcroles->t1.sym); - } + rolename = levelVar (tcroles->t1.sym); + rolename->stype = termlistAdd (NULL, TERM_Agent); + /* add name to list of role names */ pr->rolenames = termlistAppend (pr->rolenames, rolename); /* make new (empty) current protocol with name */ @@ -1402,7 +1395,7 @@ compute_prec_sets (const System sys) //eprintf ("Maxevent : %i\n", sys->roleeventmax); size = sys->rolecount * sys->roleeventmax; rowsize = WORDSIZE (size); - eventlabels = memAlloc (size * sizeof (Term)); + eventlabels = malloc (size * sizeof (Term)); prec = (unsigned int *) CALLOC (1, rowsize * size * sizeof (unsigned int)); // Assign labels r1 = 0; @@ -1703,7 +1696,7 @@ compute_prec_sets (const System sys) /* * Cleanup */ - memFree (eventlabels, size * sizeof (Term)); + free (eventlabels); FREE (prec); #ifdef DEBUG diff --git a/src/constraint.c b/src/constraint.c deleted file mode 100644 index ec407fe..0000000 --- a/src/constraint.c +++ /dev/null @@ -1,336 +0,0 @@ -#include -#include "memory.h" -#include "constraint.h" -#include "debug.h" -#include "system.h" - - - -/* constraints currently are shallow copies */ - -Constraint -makeConstraint (Term term, Knowledge know) -{ - /* maybe knowDup can just be a link, but then it needs to be moved from destroy as well */ - Constraint co = memAlloc (sizeof (struct constraint)); - co->term = term; - //co->know = knowledgeDuplicate(know); - co->know = know; - return co; -} - - -Constraint -constraintDuplicate (Constraint co) -{ - return makeConstraint (co->term, co->know); -} - - -void -constraintDestroy (Constraint cons) -{ - //knowledgeDelete(cons->know); - if (cons != NULL) - memFree (cons, sizeof (struct constraint)); -} - -/* constraints are typically added at the end, to maintain the order in which they were added */ - -Constraintlist -constraintlistAdd (Constraintlist cl, Constraint co) -{ - Constraintlist clnew = memAlloc (sizeof (struct constraintlist)); - - clnew->constraint = co; - clnew->next = NULL; - if (cl == NULL) - { - clnew->prev = NULL; - return clnew; - } - else - { - Constraintlist scan; - - scan = cl; - while (scan->next != NULL) - scan = scan->next; - scan->next = clnew; - clnew->prev = scan; - return cl; - } -} - -Constraintlist -constraintlistConcat (Constraintlist cl1, Constraintlist cl2) -{ - Constraintlist scan; - - if (cl1 == NULL) - return cl2; - scan = cl1; - while (scan->next != NULL) - scan = scan->next; - scan->next = cl2; - return cl1; -} - -Constraintlist -constraintlistRewind (Constraintlist cl) -{ - if (cl == NULL) - return NULL; - while (cl->prev != NULL) - cl = cl->prev; - return cl; -} - - -Constraintlist -constraintlistInsert (Constraintlist cl, Term term, Knowledge know) -{ - Constraintlist clnew = memAlloc (sizeof (struct constraintlist)); - - clnew->constraint = makeConstraint (term, know); - if (cl != NULL) - { - if (cl->next != NULL) - { - clnew->next = cl->next; - cl->next->prev = cl; - } - else - { - clnew->next = NULL; - } - clnew->prev = cl; - cl->next = clnew; - return constraintlistRewind (cl); - } - else - { - clnew->next = NULL; - clnew->prev = NULL; - return clnew; - } -} - -/* unlink a single constraint */ - -Constraintlist -constraintlistUnlink (Constraintlist cl) -{ - Constraintlist clnext, clprev; - - if (cl == NULL) - return NULL; - clprev = cl->prev; - clnext = cl->next; - - if (clnext != NULL) - { - clnext->prev = clprev; - cl->next = NULL; - } - if (clprev != NULL) - { - clprev->next = clnext; - cl->prev = NULL; - return constraintlistRewind (clprev); - } - else - { - return clnext; - } -} - - -/* remove a single constraint */ - -Constraintlist -constraintlistRemove (Constraintlist cl) -{ - Constraintlist clnew; - - clnew = constraintlistUnlink (cl); - memFree (cl, sizeof (struct constraintlist)); - return clnew; -} - -/* remove all constraints from this point onwards */ - -void -constraintlistDelete (Constraintlist cl) -{ - Constraintlist cldel; - - /* no empty cl */ - if (cl == NULL) - return; - - /* cut off previous */ - if (cl->prev != NULL) - { - /* TODO maybe this should cause a warning? */ - eprintf ("WARNING: clDelete with non-empty prev\n"); - cl->prev->next = NULL; - } - while (cl != NULL) - { - cldel = cl; - cl = cl->next; - memFree (cldel, sizeof (struct constraintlist)); - } - return; -} - -void -constraintlistDestroy (Constraintlist cl) -{ - Constraintlist cldel; - - /* no empty cl */ - if (cl == NULL) - return; - - /* cut off previous */ - if (cl->prev != NULL) - { - /* TODO maybe this should cause a warning? */ - eprintf ("WARNING: clDestroy with non-empty prev\n"); - cl->prev = NULL; - } - while (cl != NULL) - { - cldel = cl; - cl = cl->next; - constraintDestroy (cldel->constraint); - memFree (cldel, sizeof (struct constraintlist)); - } -} - - -Constraintlist -constraintlistDuplicate (Constraintlist oldcl) -{ - Constraintlist newcl = NULL; - - while (oldcl != NULL) - { - newcl = - constraintlistAdd (newcl, constraintDuplicate (oldcl->constraint)); - oldcl = oldcl->next; - } - return newcl; -} - -Constraintlist -constraintlistShallow (Constraintlist oldcl) -{ - Constraintlist newcl = NULL; - - while (oldcl != NULL) - { - newcl = constraintlistAdd (newcl, oldcl->constraint); - oldcl = oldcl->next; - } - return newcl; -} - -/* ---------------------------------------------------------- - - Print stuff - ----------------------------------------------------------- */ - -void -constraintPrint (Constraint co) -{ - indent (); - eprintf ("Constraint "); - if (co == NULL) - { - eprintf ("[empty]\n"); - return; - } - termPrint (co->term); - eprintf (" :\n"); - knowledgePrint (co->know); -} - -void -constraintlistPrint (Constraintlist cl) -{ - if (cl == NULL) - { - indent (); - eprintf ("[empty constraintlist]\n"); - return; - } - while (cl != NULL) - { - constraintPrint (cl->constraint); - cl = cl->next; - } -} - - -/* ---------------------------------------------------------- - - Now some real logic for the constraints - ----------------------------------------------------------- */ - -/* eliminate all standalone variables */ - -void -msElim (Constraint co) -{ - Termlist tl; - - /* simple variables can only exist in basic */ - if (co->know == NULL) - { -#ifdef DEBUG - debug (5, "Exiting because co->know is empty."); -#endif - } - else - { - tl = co->know->basic; - while (tl != NULL) - { - if (isTermVariable (tl->term)) - { - tl = termlistDelTerm (tl); - co->know->basic = tl; - } - else - tl = tl->next; - } - } -} - - -/* find the first constraint such that m is not a variable */ -/* also, apply standalone elimination to it */ - -Constraintlist -firstNonVariable (Constraintlist cl) -{ - while (cl != NULL && isTermVariable (cl->constraint->term)) - { - cl = cl->next; - } - if (cl != NULL) - { - msElim (cl->constraint); - cl->constraint->term = deVar (cl->constraint->term); - return cl; - } - else - { - return NULL; - } -} diff --git a/src/constraint.h b/src/constraint.h deleted file mode 100644 index 5464cc9..0000000 --- a/src/constraint.h +++ /dev/null @@ -1,42 +0,0 @@ -#ifndef CONSTRAINTS -#define CONSTRAINTS -#include "term.h" -#include "knowledge.h" - -struct constraint -{ - Term term; - Knowledge know; -}; - -typedef struct constraint *Constraint; - -struct constraintlist -{ - Constraint constraint; - struct constraintlist *next; - struct constraintlist *prev; -}; - -typedef struct constraintlist *Constraintlist; - -Constraint makeConstraint (Term term, Knowledge know); -Constraint constraintDuplicate (Constraint co); -void constraintDestroy (Constraint cons); -Constraintlist constraintlistAdd (Constraintlist cl, Constraint co); -Constraintlist constraintlistConcat (Constraintlist cl1, Constraintlist cl2); -Constraintlist constraintlistRewind (Constraintlist cl); -Constraintlist constraintlistInsert (Constraintlist cl, Term term, - Knowledge know); -Constraintlist constraintlistUnlink (Constraintlist cl); -Constraintlist constraintlistRemove (Constraintlist cl); -void constraintlistDestroy (Constraintlist cl); -void constraintlistDelete (Constraintlist cl); -Constraintlist constraintlistShallow (Constraintlist oldcl); -Constraintlist constraintlistDuplicate (Constraintlist oldcl); -void constraintPrint (Constraint co); -void constraintlistPrint (Constraintlist cl); - -Constraintlist firstNonVariable (Constraintlist cl); - -#endif diff --git a/src/depend.c b/src/depend.c index 9ad949b..572332e 100644 --- a/src/depend.c +++ b/src/depend.c @@ -4,6 +4,8 @@ * */ +#include +#include #include "depend.h" #include "term.h" #include "system.h" diff --git a/src/dotout.c b/src/dotout.c index 7c59772..b44f7d4 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -1,9 +1,9 @@ +#include +#include #include "system.h" #include "switches.h" -#include "memory.h" #include "arachne.h" #include "depend.h" -#include extern Protocol INTRUDER; // Pointers, to be set by the Init of arachne.c extern Role I_M; // Same here. @@ -238,8 +238,7 @@ iterate_outgoing_arrows (const System sys, void (*func) (), const int run, //! Display the current semistate using dot output format. /** - * This is not as nice as we would like it. Furthermore, the function is too big, and needs to be split into functional parts that - * will allow the generation of LaTeX code as well. + * This is not as nice as we would like it. Furthermore, the function is too big. */ void dotSemiState (const System sys) @@ -288,7 +287,7 @@ dotSemiState (const System sys) // Needed for the bindings later on: create graph nodes = nodeCount (); - ranks = memAlloc (nodes * sizeof (int)); + ranks = malloc (nodes * sizeof (int)); maxrank = graph_ranks (ranks, nodes); // determine ranks #ifdef DEBUG @@ -669,7 +668,7 @@ dotSemiState (const System sys) #endif // clean memory - memFree (ranks, nodes * sizeof (int)); // ranks + free (ranks); // ranks // close graph eprintf ("};\n\n"); diff --git a/src/error.c b/src/error.c index 58c126b..2377513 100644 --- a/src/error.c +++ b/src/error.c @@ -1,3 +1,4 @@ +#include #include #include #include "error.h" diff --git a/src/hidelevel.c b/src/hidelevel.c index bad454b..58e23a4 100644 --- a/src/hidelevel.c +++ b/src/hidelevel.c @@ -4,10 +4,10 @@ * instead of fully recomputing the required data each time again. */ +#include #include #include "hidelevel.h" #include "system.h" -#include "memory.h" extern Term TERM_Hidden; @@ -115,7 +115,7 @@ hidelevelCompute (const System sys) { Hiddenterm ht; - ht = (Hiddenterm) memAlloc (sizeof (struct hiddenterm)); + ht = (Hiddenterm) malloc (sizeof (struct hiddenterm)); ht->term = tl->term; ht->hideminimum = l; ht->hideprotocol = l2; diff --git a/src/knowledge.c b/src/knowledge.c index ede0c1a..69a15ff 100644 --- a/src/knowledge.c +++ b/src/knowledge.c @@ -8,7 +8,6 @@ #include #include "termlist.h" #include "knowledge.h" -#include "memory.h" #include "system.h" #include "debug.h" @@ -47,7 +46,7 @@ knowledgeDone (void) Knowledge makeKnowledge () { - return (Knowledge) memAlloc (sizeof (struct knowledge)); + return (Knowledge) malloc (sizeof (struct knowledge)); } //! Create a new empty knowledge structure. @@ -107,7 +106,7 @@ knowledgeDelete (Knowledge know) termlistDelete (know->basic); termlistDelete (know->encrypt); termlistDelete (know->vars); - memFree (know, sizeof (struct knowledge)); + free (know); } } @@ -126,7 +125,7 @@ knowledgeDestroy (Knowledge know) termlistDestroy (know->encrypt); termlistDestroy (know->vars); // termlistDestroy(know->inverses); - memFree (know, sizeof (struct knowledge)); + free (know); } } diff --git a/src/label.c b/src/label.c index 3358b3d..7d5d5cf 100644 --- a/src/label.c +++ b/src/label.c @@ -2,7 +2,7 @@ * Label info */ -#include "memory.h" +#include #include "term.h" #include "label.h" #include "list.h" @@ -14,7 +14,7 @@ label_create (const Term label, const Protocol protocol) { Labelinfo li; - li = (Labelinfo) memAlloc (sizeof (struct labelinfo)); + li = (Labelinfo) malloc (sizeof (struct labelinfo)); li->label = label; li->protocol = protocol; li->sendrole = NULL; @@ -26,7 +26,7 @@ label_create (const Term label, const Protocol protocol) void label_destroy (Labelinfo linfo) { - memFree (linfo, sizeof (struct labelinfo)); + free (linfo); } //! Given a list of label infos, yield the correct one or NULL diff --git a/src/latex.c b/src/latex.c deleted file mode 100644 index 7cb9ce6..0000000 --- a/src/latex.c +++ /dev/null @@ -1,1123 +0,0 @@ -/* - * LaTeX output component - */ - -#include -#include -#include -#include -#include "system.h" -#include "memory.h" -#include "modelchecker.h" -#include "tracebuf.h" -#include "varbuf.h" -#include "output.h" -#include "latex.h" -#include "specialterm.h" - -//! Multiplication factor for distance between events in an MSC diagram. -#define EVENTSPACE 1 -//! Similarity factor required for connecting arrows. Ranges from 0 to 1. -#define LINKTHRESHOLD 0.95 - -extern const char *progname; -extern const char *releasetag; -extern int globalLatex; - -/*! Additional information for an events. */ -struct traceinfo -{ - int match; - int position; -}; - -/* global variables for this module */ - -//! Additional information for each event in the trace. -struct traceinfo *tinfo; -//! The maximum run number involved, plus 1. -int width; -//! Landscape/portrait switch. Currently not used. -int landscape = 0; - -//! Phase of MSC production. -/** - * In pass 1, the widths of the boxes are determined. - * In pass 2 the actual MSC is constructed. - */ -int pass; - -/* code */ - -//! Start the latex output. -/** Prints some headers, and - * the command line that was used, as comments. - *@param sys The system buffer. - *@param argv The command line arguments as they were passed to the tool. - *@param argc The number of arguments. - */ - -void -latexInit (const System sys, int argc, char **argv) -{ - int i; - - eprintf ("%%\n"); - eprintf ("%% LaTeX output generated by %s\n", progname); - eprintf ("%% Input:\n"); - - /* print command line */ - eprintf ("%% $"); - for (i = 0; i < argc; i++) - eprintf (" %s", argv[i]); - eprintf ("\n"); - - eprintf ("%%\n"); - - /* comment macro (used for debugging) */ - eprintf ("\\newcommand{\\comment}[1]{}\n"); -} - -//! Close up any LaTeX output. -/** - *@param sys The system state. - */ - -void -latexDone (const System sys) -{ - /* closing of the document */ -} - -//! Print a term using LaTeX and highlighting. -/** - * Basically a recode of termPrint, now specific using latex codes and with a - * highlighting feature. There is still some obsolete code to show variable mappings in a term. - *@param term a term to be printed. - *@param highlight a list of terms to be highlighted. - */ - -void -latexTermPrint (Term term, Termlist highlight) -{ - if (term == NULL) - { - eprintf ("Empty term"); - return; - } -#ifdef DEBUG - if (!DEBUGL (1)) - { - term = deVar (term); - } -#else - term = deVar (term); -#endif - if (realTermLeaf (term)) - { - if (inTermlist (highlight, term)) - eprintf ("\\mathbf{"); - symbolPrint (TermSymb (term)); - if (realTermVariable (term)) - eprintf ("V"); - if (TermRunid (term) >= 0) - { - eprintf ("\\sharp%i", TermRunid (term)); - } - if (term->subst != NULL) - { - eprintf ("\\rightarrow"); - latexTermPrint (term->subst, highlight); - } - if (inTermlist (highlight, term)) - eprintf ("}"); - } - if (realTermTuple (term)) - { - eprintf ("("); - latexTermTuplePrint (term, highlight); - eprintf (")"); - return; - } - if (realTermEncrypt (term)) - { - if (isTermLeaf (TermKey (term)) - && inTermlist (TermKey (term)->stype, TERM_Function)) - { - /* function application */ - latexTermPrint (TermKey (term), highlight); - eprintf ("("); - latexTermTuplePrint (TermOp (term), highlight); - eprintf (")"); - } - else - { - /* normal encryption */ - eprintf ("\\{"); - latexTermTuplePrint (TermOp (term), highlight); - eprintf ("\\}_{"); - latexTermPrint (TermKey (term), highlight); - eprintf ("}"); - } - } -} - -//! Print an inner (tuple) term using LaTeX, without brackets. -/** - * The tuple printing only works correctly for normalized terms. - * If not, they might are displayed as "((x,y),z)". Maybe that is even - * desirable to distinguish them. - */ -void -latexTermTuplePrint (Term term, Termlist hl) -{ - if (term == NULL) - { - eprintf ("Empty term"); - return; - } - term = deVar (term); - while (realTermTuple (term)) - { - // To remove any brackets, change this into latexTermTuplePrint. - latexTermPrint (TermOp1 (term), hl); - eprintf (","); - term = deVar (TermOp2 (term)); - } - latexTermPrint (term, hl); - return; -} - -//! Print a termlist in LaTeX using highlighting. -/** - * Extending LaTeX term printing to term list printing, again with highlight - * list parameter. - *@param tl A term list to print. - *@param highlight Any terms to be highlighted. - */ - -void -latexTermlistPrint (Termlist tl, Termlist highlight) -{ - if (tl == NULL) - { - eprintf ("\\emptyset"); - return; - } - while (tl != NULL) - { - latexTermPrint (tl->term, highlight); - tl = tl->next; - if (tl != NULL) - eprintf (", "); - } -} - -//! Display the timers and states traversed using LaTeX. -/** - * Obsolete: we will now only print timers on stderr. - */ - -void -latexTimers (const System sys) -{ -} - -//! Start drawing MSC environment. -/** - * Includes printing title. - *@param protocolnames A termlist with protocol name terms. - */ - -void -latexMSCStart (Termlist protocolnames) -{ - if (landscape) - eprintf ("\\begin{landscape}\n"); - - eprintf ("\\begin{msc}{attack on $"); - termlistPrint (protocolnames); - eprintf ("$}\n"); -} - -//! Close drawing MSC - -void -latexMSCEnd () -{ - eprintf ("\\end{msc}\n"); - - if (landscape) - eprintf ("\\end{landscape}\n"); - -} - -/** - * Declare the MSC stick for a single instance of a run participating in an - * attack. - * This involves layout of the partners roles, and the agent etc. - *@param sys System state. - *@param run The run to be declared. - */ - -void -latexDeclInst (const System sys, int run) -{ - Term myAgent; - Term myRole; - Termlist roles; - int first; - - myAgent = agentOfRun (sys, run); - myRole = sys->runs[run].role->nameterm; - if (pass == 1) - { - eprintf ("\\maxlength{\\maxmscinst}{"); - } - else - { - eprintf ("\\declinst{run%i}{", run); - } - - /* display above assumptions */ - roles = sys->runs[run].protocol->rolenames; - if (pass == 2) - { - eprintf ("assumes $"); - first = 1; - while (roles != NULL) - { - if (!isTermEqual (myRole, roles->term)) - { - if (!first) - eprintf (", "); - else - first = 0; - termPrint (agentOfRunRole (sys, run, roles->term)); - eprintf (": "); - termPrint (roles->term); - } - roles = roles->next; - } - eprintf ("$}{"); - } - - /* display agent and role */ - eprintf ("$\\mathbf{"); - termPrint (myAgent); - eprintf ("}: "); - termPrint (myRole); - - eprintf ("$}\n"); - - /* cleanup */ - termDelete (myAgent); -} - -//! Add vertical space in MSC diagrams. -/** - * Make some space in the diagram by nextlevels. - * TODO: can be incorporated in nextlevel[param] without loop. - *@param amount the line integer. - */ - -void -latexEventSpace (int amount) -{ - int i; - - if (pass < 2) - { - /* not printing */ - return; - } - - //eprintf("%% number of newlines: %d\n",amount); - for (i = 0; i < EVENTSPACE * amount; i++) - eprintf ("\\nextlevel\n"); -} - -//! MSC message print. -/** - * Print an arrow with message from event i to event j, as defined in the - * tracebuffer. If either i or j are -1, the intruder is meant. - */ - -void -latexMessagePrint (struct tracebuf *tb, int from, int to) -{ - - Term sendTerm = NULL; - Term readTerm = NULL; - - if (pass < 2) - { - /* no measurement of messages yet */ - return; - } - - if (from == -1 && to == -1) - { - return; - } - if (from != -1) - { - sendTerm = tb->event[from]->message; - } - if (to != -1) - { - readTerm = tb->event[to]->message; - } - if (from == -1 && to != -1) - { - /* message from intruder into system */ - eprintf ("\\mess{$"); - termPrint (readTerm); - eprintf ("$}{eve}{run%d}\n", tb->run[to]); - } - else if (from != -1 && to == -1) - { - /* message from system to intruder */ - eprintf ("\\mess{$"); - termPrint (sendTerm); - eprintf ("$}{run%d}{eve}\n", tb->run[from]); - } - else if (from != -1 && to != -1) - { - /* message from one agent to another, possibly transformed */ - - eprintf ("\\mess{$"); - - termPrint (sendTerm); - - if (!isTermEqual (sendTerm, readTerm)) - { - eprintf ("\\rightarrow"); - termPrint (readTerm); - } - - eprintf ("$}{run%d", tb->run[from]); - eprintf ("}{run%d}[%d]", tb->run[to], - EVENTSPACE * (tinfo[to].position - tinfo[from].position)); - - eprintf ("\n"); - } -} - -/** - * hmm? TODO apparently, some other variant used, with duplicate handling of - * lost and found ??? But only using lost... weirdness. - */ - -void -latexMessagePrintHighlight (struct tracebuf *tb, int from, int to, - Termlist highlight) -{ - - Term sendTerm = NULL; - Term readTerm = NULL; - - if (pass < 2) - { - /* no measurements on message width yet */ - return; - } - - if (from == -1 && to == -1) - { - return; - } - if (from != -1) - { - sendTerm = tb->event[from]->message; - } - if (to != -1) - { - readTerm = tb->event[to]->message; - } - if (from == -1 && to != -1) - { - /* TODO redundant */ - eprintf ("\\found{$"); - latexTermPrint (readTerm, highlight); - eprintf ("$}{}{run%d}\n", tb->run[to]); - } - else if (from != -1 && to == -1) - { - eprintf ("\\mess{$"); - latexTermPrint (sendTerm, highlight); - eprintf ("$}{run%d}{eve}\n", tb->run[from]); - } - else if (from != -1 && to != -1) - { - - eprintf ("\\mess{$"); - - latexTermPrint (sendTerm, highlight); - - if (!isTermEqual (sendTerm, readTerm)) - { - eprintf ("\\rightarrow"); - latexTermPrint (readTerm, highlight); - } - - eprintf ("$}{run%d", tb->run[from]); - eprintf ("}{run%d}[%d]", tb->run[to], - EVENTSPACE * (tinfo[to].position - tinfo[from].position)); - - eprintf ("\n"); - } -} - -//! Display claim violation. -/** - * For now, only secrecy: TODO - */ - -void -latexClaim (struct tracebuf *tb, int run, Termlist tl) -{ - if (pass == 1) - { - eprintf ("\\maxlength{\\maxmsccondition}{"); - } - else - { - eprintf ("\\condition{"); - } - eprintf ("$\\neg secret "); - termlistPrint (tl); - eprintf ("$}"); - if (pass == 1) - { - eprintf ("\n"); - } - else - { - eprintf ("{run%d}\n", run); - } -} - -//! Determine matching send event. -/** - * Given a read event, tries to find a corresponding send event in the trace - * buffer. Currently unused. - */ - -int -latexCorrespondingSend (struct tracebuf *tb, int rd) -{ - - int labelMatch = 0; - int toMatch = 0; - int fromMatch = 0; - int tofromMatch = 0; - int messageMatch = 0; - int nMatches = 0; - int maxNMatches = 0; - - int readEvent = rd; - int sendEvent = -1; - int bestSendEvent = -1; - - for (sendEvent = readEvent; sendEvent >= 0; sendEvent--) - { - if (tb->event[sendEvent]->type == SEND) - { - /* do all the different kind of matchings first */ - - labelMatch = - isTermEqual (tb->event[sendEvent]->label, - tb->event[readEvent]->label); - toMatch = - isTermEqual (tb->event[sendEvent]->to, tb->event[readEvent]->to); - fromMatch = - isTermEqual (tb->event[sendEvent]->from, - tb->event[readEvent]->from); - tofromMatch = toMatch || fromMatch; - messageMatch = - isTermEqual (tb->event[sendEvent]->message, - tb->event[readEvent]->message); - - /* calculate the score */ - - nMatches = labelMatch + tofromMatch + messageMatch; - - if (nMatches == 3) - { - /* bingo! success on all matches */ - - //eprintf("Found perfect match: %d\n", s); - bestSendEvent = sendEvent; - break; - } - if (nMatches > maxNMatches) - { - if (labelMatch && messageMatch) - { - /* strongest restriction: message and label should match */ - - maxNMatches = nMatches; - bestSendEvent = sendEvent; - - } - else if (messageMatch) - { - /* if label AND message don't match: */ - /* at least message should match */ - - maxNMatches = nMatches; - bestSendEvent = sendEvent; - } - else if (labelMatch) - { - /* if message doesn't match */ - /* the label should matches */ - - maxNMatches = nMatches; - bestSendEvent = sendEvent; - } - } - } - } - - //bestSendEvent = NULL; - if (bestSendEvent == -1) - { - - int u; - - for (u = 0; u < rd; u++) - { - if (tb->event[u]->type == SEND) - { - //knowledgePrint(sys->traceKnow[u]); - if (inKnowledge - (tb->know[u + 1], tb->event[readEvent]->message)) - { - bestSendEvent = u; - break; - } - } - } - } - - if (bestSendEvent == -1) - { - eprintf ("%% Could not find a matching SEND\n"); - } - return bestSendEvent; -} - -//! Determine matching send event. -/** - * Simplified variant of finding the matching send event. - * However, if it is introduced at a non-send event, things start to break - * done. REVIEW later. - */ - -int -latexCorrespondingSend2 (struct tracebuf *tb, int readEvent) -{ - int u; - - for (u = tb->length - 1; u >= 0; u--) - { - if (tb->event[u]->type == SEND) - { - if (!inKnowledge (tb->know[u], tb->event[readEvent]->message)) - { - /* - eprintf("%% term["); - eprintf("]#%d is introduced at traceEvent[%d] ",readEvent,u); - eprintf("\n"); - */ - return u; - } - } - } - - return -1; - -} - -//! Display knowledge in LaTeX. - -void -knowledgePrintLatex (Knowledge know) -{ - Termlist tl; - - if (know == NULL) - { - eprintf ("\\emptyset"); - } - else - { - tl = knowledgeSet (know); - latexTermlistPrint (tl, NULL); - termlistDelete (tl); - } -} - -//! Display the attack in the systems attack buffer using LaTeX. - -void -attackDisplayLatex (const System sys) -{ - int i; - struct tracebuf *tb; - int *runPosition; - int currRun; - int position; - int eventSize; - Termlist tl; - Termlist newtl; - Termlist claimDetails; - Termlist highlights = NULL; - int cKnowledge; - int bestSend; - - tb = sys->attack; - if (tb == NULL) - { - eprintf ("Attack pointer empty: nothing to display.\n"); - exit (1); - } - /* set variables */ - varbufSet (sys, tb->variables); - - /* Rebuild knowledge. Strange, this ought to be good. - * Maybe reconstruct dependencies as well. */ - tracebufRebuildKnow (tb); - - /* Make a comment in which the trace is displayed, for debugging etc. */ - eprintf ("\n\\comment{ TRACE\n\n"); - eprintf ("Length: %i\n", tb->length); - eprintf ("Reallength: %i\n", tb->reallength); - eprintf ("\n"); - i = 0; - while (i <= tb->length) - { - eprintf ("Knowledge %i:\n", i); - knowledgePrint (tb->know[i]); - eprintf (" [Inverses]: "); - knowledgeInversesPrint (tb->know[i]); - eprintf ("\n\n"); - if (i < tb->length) - { - eprintf ("Event %i\t[", i); - switch (tb->status[i]) - { - case S_UNK: - eprintf ("?"); - break; - case S_RED: - eprintf ("redundant"); - break; - case S_TOD: - eprintf ("to do"); - break; - case S_OKE: - eprintf ("okay"); - break; - default: - eprintf ("illegal status code"); - break; - } - eprintf ("]\t"); - termPrint (tb->event[i]->message); - eprintf ("\t#%i", tb->run[i]); - eprintf ("\n"); - roledefPrint (tb->event[i]); - eprintf ("\n\n"); - } - i++; - } - eprintf ("}\n\n"); - - tinfo = - (struct traceinfo *) memAlloc ((tb->length + 1) * - sizeof (struct traceinfo)); - - /* - * Determine width, which is the 1+max(runid involved in the attack) - */ - - width = 1; - for (i = 0; i < tb->length; i++) - { - // TODO: I would expect here a redundancy test - if (tb->run[i] >= width) - width = tb->run[i] + 1; - } - - /* - * Initialise tinfo arrays. - */ - - for (i = 0; i < tb->length; i++) - { - tb->link[i] = -1; - tinfo[i].match = -1; - tinfo[i].position = i; - } - tinfo[i].match = -1; - tinfo[i].position = i; - - /* - * Init array of positions (ordering) of the MSC lines. - */ - - runPosition = (int *) memAlloc (width * sizeof (int)); - for (i = 0; i < width; i++) - { - runPosition[i] = 0; - } - - /* - * Determine corresponding sends and thus links - */ - - for (i = tb->length - 1; i >= 0; i--) - { - if (tb->status[i] != S_RED) - { - if (tb->event[i]->type == READ && !tb->event[i]->internal) - { - bestSend = latexCorrespondingSend2 (tb, i); - eprintf ("%% match: %d <-> %d\n", i, bestSend); - if (bestSend == -1) - continue; // TODO major ugliness - - tb->link[i] = bestSend; - tb->link[bestSend] = i; - } - if (tb->event[i]->type == CLAIM) - { - claimDetails = - claimViolationDetails (sys, tb->run[i], tb->event[i], - tb->know[i]); - } - } - } - eprintf ("\\comment{ claimDetails :\n"); - termlistPrint (claimDetails); - eprintf ("\n}\n"); - - // landscape = (width > 4); // not for the time being - - /* - * Apparently unlinks things that do not meet the threshold. - */ - - position = 0; - currRun = 0; - eventSize = 0; - for (i = 0; i < tb->length; i++) - { - if (tb->status[i] != S_RED) - { - tinfo[i].position = position; - eventSize = 1; - currRun = tb->run[i]; - - switch (tb->event[i]->type) - { - case SEND: - position++; - tinfo[i].position++; - break; - case READ: - if (tb->link[i] != -1) - { - if (termDistance - (tb->event[i]->message, - tb->event[tb->link[i]]->message) < LINKTHRESHOLD) - { - /* disconnect read-send */ - tb->link[tb->link[i]] = -1; - tb->link[i] = -1; - } - else - { - if (runPosition[currRun] <= tinfo[tb->link[i]].position - && currRun != tb->run[tb->link[i]]) - { - eprintf ("\\comment{\n"); - termPrint (tb->event[i]->message); - eprintf ("\n"); - termPrint (tb->event[tb->link[i]]->message); - eprintf ("\n"); - eprintf ("%% termDistance: %f\n", - termDistance (tb->event[i]->message, - tb->event[tb->link[i]]-> - message)); - eprintf ("}\n"); - tinfo[i].position = tinfo[tb->link[i]].position; - eventSize = 0; - } - } - } - if (tb->event[i]->internal) - { - eventSize = 0; - } - break; - case CLAIM: - if (claimDetails != NULL && claimDetails != (Termlist) - 1) - { - eventSize = 2; - } - else - { - eventSize = 0; - } - break; - default: - break; - } - if (!(tb->event[i]->type == READ && tb->event[i]->internal)) - runPosition[currRun] = tinfo[i].position + eventSize; - /* eprintf("%% Event %d at %d\n", i, position); */ - position += eventSize; - } - } - - /* ------------------------------------------------------ - * - * Start of MSC creation (2-phase) - * - * - * ------------------------------------------------------ - */ - - /* 2 pass for widths */ - - for (pass = 1; pass <= 2; pass++) - { - eprintf ("%% Pass %i\n\n", pass); - - if (pass == 1) - { - eprintf ("\\maxlength{\\maxmscaction}{knows}\n"); - eprintf ("\\maxlength{\\maxmscaction}{creates}\n"); - } - else - { - Termlist protocolnames; - Term pname; - - /* slightly stretch measurements */ - eprintf ("\\addtolength{\\maxmscall}{2\\mscspacer}\n"); - eprintf ("\\addtolength{\\maxmscaction}{\\mscspacer}\n"); - eprintf ("\\addtolength{\\maxmscinst}{\\mscspacer}\n"); - eprintf ("\\addtolength{\\maxmsccondition}{\\mscspacer}\n"); - - /* put out computed widths */ - - eprintf ("\\setlength{\\envinstdist}{0.7\\maxmscall}\n"); - eprintf ("\\setlength{\\instdist}{\\maxmscall}\n"); - eprintf ("\\setlength{\\actionwidth}{\\maxmscaction}\n"); - eprintf ("\\setlength{\\instwidth}{\\maxmscinst}\n"); - eprintf ("\\setlength{\\conditionoverlap}{0.5\\maxmsccondition}\n"); - - /* create MSC title, involving protocol names and such. */ - - protocolnames = NULL; - for (i = 0; i < width; i++) - { - if (runPosition[i] > 0) - { - pname = sys->runs[i].protocol->nameterm; - if (!inTermlist (protocolnames, pname)) - { - protocolnames = termlistAppend (protocolnames, pname); - } - } - } - latexMSCStart (protocolnames); - termlistDelete (protocolnames); - } - - /* declare instances */ - - for (i = 0; i < width; i++) - { - if (runPosition[i] > 0) - latexDeclInst (sys, i); - } - /* Add the intruder instance */ - if (pass == 2) - eprintf ("\\declinst{eve}{}{"); - else - eprintf ("\\maxlength{\\maxmscinst}{"); - eprintf ("{\\bf Eve}: Intruder}\n\n"); - - /* Print the local constants for each instance */ - - for (i = 0; i < width; i++) - { - if (runPosition[i] > 0) - { - Termlist tl = sys->runs[i].locals; - int first = 1; - while (tl != NULL) - { - /* detect whether it's really local to this run */ - Term t = deVar (tl->term); - if (isTermLeaf (t) && TermRunid (t) == i) - { - if (first) - { - if (pass == 1) - eprintf ("\\maxlength{\\maxmscaction}{$"); - else - eprintf ("\\ActionBox{creates \\\\\n$"); - first = 0; - } - else - { - eprintf (", "); - } - termPrint (tl->term); - } - tl = tl->next; - } - if (!first) - { - if (pass == 1) - eprintf ("$}\n"); - else - eprintf ("$}{run%i}\n", i); - } - } - } - - /* Print the initial intruder knowledge */ - - if (pass == 2) - { - eprintf ("\\ActionBox{"); - eprintf ("knows \\\\\n$"); - knowledgePrintLatex (tb->know[0]); - eprintf ("$}"); - eprintf ("{eve}\n"); - eprintf ("\\nextlevel[3]\n"); - eprintf ("\n"); - } - - /* print the events in the attack */ - - //for (j=-1; j<=sys->step; j++) - position = 0; - cKnowledge = 0; - for (i = 0; i < tb->length; i++) - { - if (tb->status[i] != S_RED) - { - latexEventSpace (tinfo[i].position - position); - if (tinfo[i].position >= position) - { - position = tinfo[i].position; - } - switch (tb->event[i]->type) - { - case SEND: - newtl = knowledgeNew (tb->know[i], tb->know[i + 1]); - highlights = NULL; - /* Build a Termlist of terms that from the claimViolationDetails, - that appear in the knowledge */ - if (newtl != NULL) - { - tl = claimDetails; - while (tl != NULL) - { - if (inTermlist (newtl, tl->term)) - { - highlights = termlistAdd (highlights, tl->term); - } - tl = tl->next; - } - - } - - if (tb->link[i] != -1 && i < tb->length) - { - latexMessagePrintHighlight (tb, i, tb->link[i], - highlights); - } - else - { - latexMessagePrintHighlight (tb, i, -1, highlights); //lost message - } - - /* maybe extra knowledge? */ - if (newtl != NULL) - { - /* print what was learned */ - - if (pass == 1) - { - eprintf ("\\maxlength{\\maxmscaction}{"); - } - else - { - eprintf ("\\nextlevel[1]\n"); - eprintf ("\\ActionBox{learns \\\\\n"); - } - eprintf ("$"); - cKnowledge++; - latexTermlistPrint (newtl, highlights); - eprintf ("$}"); - if (pass == 1) - { - eprintf ("\n"); - } - else - { - eprintf ("{eve}\n"); - eprintf ("\\nextlevel[2]\n"); - } - } - - termlistDelete (highlights); - - break; - case READ: - if (tb->event[i]->internal) - { - } - else if (tb->link[i] == -1) - { - latexMessagePrint (tb, -1, i); //found message - } - break; - case CLAIM: - if (claimDetails != NULL && claimDetails != (Termlist) - 1) - { - latexClaim (tb, tb->run[i], claimDetails); - } - break; - default: - break; //kannie! - } - } - } - } - - /* - * close up diagrams - */ - - - latexEventSpace (2); - latexMSCEnd (); - - /* - * free used memory - */ - - memFree (runPosition, width * sizeof (int)); - memFree (tinfo, (tb->length + 1) * sizeof (struct traceinfo)); -} diff --git a/src/latex.h b/src/latex.h deleted file mode 100644 index 413acb9..0000000 --- a/src/latex.h +++ /dev/null @@ -1,21 +0,0 @@ -/* - * LaTeX output component header - */ - -#ifndef LATEX -#define LATEX - -#include "system.h" - -void latexInit (const System sys, int argc, char **argv); -void latexDone (const System sys); -void latexTimers (const System sys); -void latexMSCStart (); -void latexMSCEnd (); -void latexLearnComment (const System sys, Termlist tl); -void latexTracePrint (const System sys); -void attackDisplayLatex (const System sys); -void latexTermPrint (Term term, Termlist hl); -void latexTermTuplePrint (Term term, Termlist hl); - -#endif diff --git a/src/main-switches.c b/src/main-switches.c index 634c43b..0d1a043 100644 --- a/src/main-switches.c +++ b/src/main-switches.c @@ -46,7 +46,6 @@ enum exittypes #include "system.h" #include "debug.h" #include "modelchecker.h" -#include "memory.h" #include "symbol.h" #include "pheading.h" #include "symbol.h" @@ -54,8 +53,6 @@ enum exittypes #include "tac.h" #include "timer.h" #include "compiler.h" -#include "latex.h" -#include "output.h" #include "binding.h" #include "version.h" #include "specialterm.h" @@ -130,8 +127,6 @@ main (int argc, char **argv) struct arg_int *switch_goal_select_method = arg_int0 (NULL, "goal-select", NULL, "use goal selection method (default 3)"); - struct arg_lit *switch_latex_output = - arg_lit0 (NULL, "latex", "output attacks in LaTeX format"); struct arg_lit *switch_empty = arg_lit0 ("e", "empty", "do not generate output"); struct arg_lit *switch_progress_bar = @@ -343,8 +338,6 @@ main (int argc, char **argv) #else debugSet (0); #endif - /* Initialize memory routines */ - memInit (); /* initialize symbols */ termsInit (); @@ -668,11 +661,8 @@ main (int argc, char **argv) * Now we clean up any memory that was allocated. */ - if (switches.engine == ARACHNE_ENGINE) - { - arachneDone (); - bindingDone (); - } + arachneDone (); + bindingDone (); knowledgeDestroy (sys->know); systemDone (sys); compilerDone (); @@ -687,7 +677,6 @@ main (int argc, char **argv) /* memory clean up? */ strings_cleanup (); - memDone (); exit: /* deallocate each non-null entry in argtable[] */ diff --git a/src/main.c b/src/main.c index 0404c07..d7f2725 100644 --- a/src/main.c +++ b/src/main.c @@ -26,8 +26,6 @@ * * 3 Okay Attack found * - * However, if the --scenario=-1 switch is used, the exit code is used to return the number of scenarios. - * * \section coding Coding conventions * * Usually, each source file except main.c has an myfileInit() and myfileDone() function @@ -43,8 +41,6 @@ #include #include "system.h" #include "debug.h" -#include "modelchecker.h" -#include "memory.h" #include "symbol.h" #include "pheading.h" #include "symbol.h" @@ -52,8 +48,6 @@ #include "tac.h" #include "timer.h" #include "compiler.h" -#include "latex.h" -#include "output.h" #include "binding.h" #include "switches.h" #include "specialterm.h" @@ -84,9 +78,6 @@ main (int argc, char **argv) int nerrors; int exitcode = EXIT_NOATTACK; - /* Initialize memory routines */ - memInit (); - /* initialize symbols */ termsInit (); termmapsInit (); @@ -126,16 +117,8 @@ main (int argc, char **argv) /* compile */ - if (switches.engine != ARACHNE_ENGINE) - { - // Compile as many runs as possible - compile (spdltac, switches.runs); - } - else - { - // Compile no runs for Arachne - compile (spdltac, 0); - } + // Compile no runs for Arachne + compile (spdltac, 0); scanner_cleanup (); /* preprocess */ @@ -173,11 +156,6 @@ main (int argc, char **argv) * --------------------------------------- */ - /* Latex only makes sense for attacks */ - if (switches.latex && switches.output != ATTACK) - { - error ("Scyther can only generate LaTeX output for attacks."); - } #ifdef DEBUG if (DEBUGL (4)) { @@ -185,10 +163,8 @@ main (int argc, char **argv) } #endif - if (switches.engine == ARACHNE_ENGINE) - { - arachneInit (sys); - } + arachneInit (sys); + /* * --------------------------------------- * Start real stuff @@ -199,10 +175,6 @@ main (int argc, char **argv) if (switches.xml) xmlOutInit (); - /* latex header? */ - if (switches.latex) - latexInit (sys, argc, argv); - /* model check system */ #ifdef DEBUG if (DEBUGL (1)) @@ -216,58 +188,19 @@ main (int argc, char **argv) * --------------------------------------- */ - /* Display shortest attack, if any */ + /* Exitcodes are *not* correct anymore */ - if (sys->attack != NULL && sys->attack->length != 0) - { - if (switches.output == ATTACK) - { - attackDisplay (sys); - } - /* mark exit code */ - exitcode = EXIT_ATTACK; - } - else - { - /* check if there is a claim type that was never reached */ - Claimlist cl_scan; - - cl_scan = sys->claimlist; - while (cl_scan != NULL) - { - if (cl_scan->failed == STATES0) - { - /* mark exit code */ - exitcode = EXIT_NOCLAIM; - } - cl_scan = cl_scan->next; - } - - } - - /* latex closeup */ - if (switches.latex) - latexDone (sys); + exitcode = EXIT_ATTACK; /* xml closeup */ if (switches.xml) xmlOutDone (); - /* Transfer any scenario counting to the exit code, - * assuming that there is no error. */ - if (exitcode != EXIT_ERROR && switches.scenario < 0) - { - exitcode = sys->countScenario; - } - /* * Now we clean up any memory that was allocated. */ - if (switches.engine == ARACHNE_ENGINE) - { - arachneDone (); - } + arachneDone (); knowledgeDestroy (sys->know); systemDone (sys); colorDone (); @@ -283,7 +216,6 @@ main (int argc, char **argv) /* memory clean up? */ strings_cleanup (); - memDone (); exit: return exitcode; @@ -341,66 +273,6 @@ timersPrint (const System sys) //********************************************************************** - /* states traversed */ - - if (switches.engine == POR_ENGINE) - { - eprintf ("states\t"); - statesPrintShort (sys); - eprintf ("\n"); - - /* scenario info */ - - if (switches.scenario > 0) - { - eprintf ("scen_st\t"); - statesFormat (sys->statesScenario); - eprintf ("\n"); - } - - /* flag - * - * L n Attack of length - * None failed claim - * NoClaim no claims - */ - - eprintf ("attack\t"); - if (sys->claims == STATES0) - { - eprintf ("NoClaim\n"); - } - else - { - if (sys->failed != STATES0) - eprintf ("L:%i\n", attackLength (sys->attack)); - else - eprintf ("None\n"); - } - -#ifndef NOTIMERS - /* print time */ - - double seconds; - seconds = (double) clock () / CLOCKS_PER_SEC; - eprintf ("time\t%.3e\n", seconds); - - /* states per second */ - - eprintf ("st/sec\t"); - if (seconds > 0) - { - eprintf ("%.3e\n", statesDouble (sys->states) / seconds); - } - else - { - eprintf ("\n"); - } -#endif - } - - //********************************************************************** - /* Print also individual claims */ /* Note that if the output is set to empty, the claim output is redirected to stdout (for e.g. processing) */ @@ -559,13 +431,10 @@ timersPrint (const System sys) } /* states (if asked) */ - if (switches.engine == ARACHNE_ENGINE) + if (switches.countStates) { - if (switches.countStates) - { - eprintf ("\tstates="); - statesFormat (cl_scan->states); - } + eprintf ("\tstates="); + statesFormat (cl_scan->states); } /* any warnings */ @@ -591,108 +460,7 @@ timersPrint (const System sys) } } -//! Analyse the model by incremental runs. -/* - * This procedure considers mainly incremental searches, and settings - * parameters for that. The real work is handled by modelCheck. - */ - -void -MC_incRuns (const System sys) -{ - /* - * incremental runs check - * - * note: we assume that at least one run needs to be checked. - */ - int maxruns = sys->maxruns; - int runs = 1; - int flag = 1; - int res; - - do - { - systemReset (sys); - sys->maxruns = runs; - systemRuns (sys); - fprintf (stderr, "%i of %i runs in incremental runs search.\n", - runs, maxruns); - res = modelCheck (sys); - fprintf (stderr, "\n"); - if (res) - { - /* Apparently a violation occurred. If we are searching - * the whole space, then we just continue. However, if - * we're looking to prune, ``the buck stops here''. */ - - if (switches.prune != 0) - { - flag = 0; - } - } - runs++; - } - while (flag && runs <= maxruns); - sys->maxruns = maxruns; -} - -//! Analyse the model by incremental trace lengths. -/* - * This procedure considers mainly incremental searches, and settings - * parameters for that. The real work is handled by modelCheck. - */ - -void -MC_incTraces (const System sys) -{ - /* - * incremental traces check - * - * note: we assume that at least one run needs to be checked. - */ - int maxtracelen; - int tracelen; - int tracestep; - int flag; - int res; - - tracestep = 3; /* what is a sensible stepping size? */ - flag = 1; - - maxtracelen = getMaxTraceLength (sys); - tracelen = maxtracelen - tracestep; - while (tracelen > 6) /* what is a reasonable minimum? */ - tracelen -= tracestep; - - flag = 1; - - do - { - systemReset (sys); - sys->maxtracelength = tracelen; - systemRuns (sys); - fprintf (stderr, - "%i of %i trace length in incremental trace length search.\n", - tracelen, maxtracelen); - res = modelCheck (sys); - fprintf (stderr, "\n"); - if (res) - { - /* Apparently a violation occurred. If we are searching - * the whole space, then we just continue. However, if - * we're looking to prune, ``the buck stops here''. */ - - if (switches.prune != 0) - { - flag = 0; - } - } - tracelen += tracestep; - } - while (flag && tracelen <= maxtracelen); -} - -//! Analyse the model with a fixed scenario. +//! Analyse the model /** * Traditional handywork. */ @@ -720,26 +488,8 @@ MC_single (const System sys) int modelCheck (const System sys) { - if (switches.output == STATESPACE) - { - graphInit (sys); - } - /* modelcheck the system */ - switch (switches.engine) - { - case POR_ENGINE: - if (sys->maxruns > 0) - traverse (sys); - else - warning ("Model checking system with empty scenario."); - break; - case ARACHNE_ENGINE: - arachne (); - break; - default: - error ("Unknown engine type %i.", switches.engine); - } + arachne (); /* clean up any states display */ if (switches.reportStates > 0) @@ -749,18 +499,5 @@ modelCheck (const System sys) } timersPrint (sys); - if (switches.output == STATESPACE) - { - graphDone (sys); - } - if (switches.scenario > 0) - { - /* Traversing a scenario. Maybe we ran out. */ - if (switches.scenario > sys->countScenario) - { - /* Signal as error */ - exit (1); - } - } return (sys->failed != STATES0); } diff --git a/src/match_basic.c b/src/match_basic.c deleted file mode 100644 index af79bc5..0000000 --- a/src/match_basic.c +++ /dev/null @@ -1,308 +0,0 @@ -/*!\file match_basic.c - *\brief Implements the match function. - * - * The match function here is integrated here with an enabled() function. - * It is also the basic match, so not suited for Constraint Logic Programming. - */ - -#include -#include -#include "memory.h" -#include "substitution.h" -#include "system.h" -#include "modelchecker.h" -#include "match_basic.h" -#include "switches.h" - -//! Get the candidates list for typeless basic stuff -__inline__ Termlist -candidates (const Knowledge know) -{ - return knowledgeGetBasics (know); -} - -struct fvpass -{ - int (*solution) (); - - System sys; - int run; - Roledef roledef; - int (*proceed) (System, int); -}; - -//! Fix variables in a message, and check whether it can be accepted. -/** - * fp.sys is only accessed for the matching type. - *@returns 1 (true) if there exists a message that can be accepted, fvpass returns 1 on it. - */ -int -fixVariablelist (const struct fvpass fp, const Knowledge know, - Termlist varlist, const Term message) -{ - int flag = 0; - - Termlist tlscan; - Termlist candlist; - - if (varlist != NULL) - { - if (!isTermVariable (varlist->term)) - { - while (varlist != NULL && !isTermVariable (varlist->term)) - { - varlist = varlist->next; - } - } - } - - /* cond: varlist == NULL || isTermvariable(varlist->term) */ - - if (varlist == NULL) - { - /* there are no (more) variables to be fixed. */ - /* actually trigger it if possible */ - - int copied; - Knowledge tempknow; - - /* first we propagate the substitutions in the knowledge */ - /* TODO this must also be done for all agent knowledge!! */ - - if (knowledgeSubstNeeded (know)) - { - copied = 1; - tempknow = knowledgeSubstDo (know); - } - else - { - copied = 0; - tempknow = know; - } - - if (inKnowledge (tempknow, message)) - { - if (fp.solution != NULL) - { - flag = fp.solution (fp, tempknow); - } - else - { - /* signal that it was enabled, now we omit the pruning */ - flag = 1; - } - } - else - { - /* not enabled */ - flag = 0; - } - - /* restore state */ - if (copied) - { - knowledgeDelete (tempknow); - knowledgeSubstUndo (know); - } - return flag; - } - - /* cond: isTermvariable(varlist->term) */ - varlist->term = deVar (varlist->term); - /* cond: realTermvariable(varlist->term) */ - candlist = candidates (know); -#ifdef DEBUG - if (DEBUGL (5)) - { - indent (); - printf ("Set "); - termPrint (varlist->term); - printf (" with type "); - termlistPrint (varlist->term->stype); - printf (" from candidates "); - termlistPrint (candlist); - printf ("\n"); - } -#endif - - /* Now check all candidates. Do they work as candidates? */ - tlscan = candlist; - while (tlscan != NULL && !(flag && fp.solution == NULL)) - { - if (!isTermEqual (varlist->term, tlscan->term)) - { - /* substitute */ - varlist->term->subst = tlscan->term; - if (validSubst (switches.match, varlist->term)) - { -#ifdef DEBUG - if (DEBUGL (5)) - { - indent (); - printf ("Substituting "); - termPrint (varlist->term); - printf ("\n"); - } -#endif - /* now we may need to substitute more */ - flag = fixVariablelist (fp, know, varlist->next, message) - || flag; - } - } - tlscan = tlscan->next; - } - /* restore state: variable is not instantiated. */ - varlist->term->subst = NULL; - - /* garbage collect */ - termlistDelete (candlist); - - return flag; -} - -/* - * check whether a roledef, given some newer knowledge substitutions, can survive - */ - -#define enabled_basic(sys,know,newterm) !inKnowledge(know,newterm) - -//! Try to execute a read event. -/** - * Try to execute a read event. It must be able to be construct it from the - * current intruder knowledge (Inject), but not from the forbidden knowledge - * set, which we tried earlier. - * - *@returns 0 if it is not enabled, 1 if it was enabled (and routes explored) - *\sa explorify() - */ -int -matchRead_basic (const System sys, const int run, - int (*proceed) (System, int)) -{ - Roledef rd; - int flag = 0; - struct fvpass fp; - Termlist varlist; - - int solution (struct fvpass fp, Knowledge know) - { - Knowledge oldknow; - Term newterm; - - /* remove variable linkages */ - newterm = termDuplicateUV (fp.roledef->message); - /* a candidate, but if this is a t4 traversal, is it also an old one? */ - if (switches.traverse < 4 || - fp.roledef->forbidden == NULL || - enabled_basic (fp.sys, fp.roledef->forbidden, newterm)) - { - /* it is possibly enabled, i.e. not forbidden */ - int enabled; - - oldknow = fp.sys->know; - fp.sys->know = know; -#ifdef DEBUG - if (DEBUGL (5)) - { - printf ("+"); - } -#endif - enabled = fp.proceed (fp.sys, fp.run); // flag determines the enabled status now - fp.sys->know = oldknow; - termDelete (newterm); - return enabled; - } - else - { - /* blocked */ -#ifdef DEBUG - if (DEBUGL (5)) - { - printf ("-"); - } -#endif - termDelete (newterm); - return 0; - } - } - - rd = runPointerGet (sys, run); - varlist = termlistAddVariables (NULL, rd->message); - - fp.sys = sys; - fp.run = run; - fp.roledef = rd; - fp.proceed = proceed; - fp.solution = solution; - -#ifdef DEBUG - if (DEBUGL (5)) - { - indent (); - printf ("{\n"); - } -#endif - - flag = fixVariablelist (fp, sys->know, varlist, rd->message); - termlistDelete (varlist); - -#ifdef DEBUG - if (DEBUGL (5)) - { - indent (); - printf ("} with flag %i\n", flag); - } -#endif - return flag; -} - -//! Skip an event -/** - * Skips over an event. Because the intruder knowledge is incremental, we can - * just overwrite the old value of forbidden. - *@returns 1 - */ -int -block_basic (const System sys, const int run) -{ - Knowledge pushKnow; - Roledef rd; - - rd = runPointerGet (sys, run); - pushKnow = rd->forbidden; - rd->forbidden = sys->know; - traverse (sys); - rd->forbidden = pushKnow; - return 1; -} - -//! Execute a send -/** - *@returns 1 - */ -int -send_basic (const System sys, const int run) -{ - Roledef rd = runPointerGet (sys, run); - /* execute send, push knowledge? */ - if (inKnowledge (sys->know, rd->message)) - { - /* no new knowledge, so this remains */ - explorify (sys, run); - } - else - { - /* new knowledge, must store old state */ - Knowledge oldknow = sys->know; - sys->know = knowledgeDuplicate (sys->know); - - sys->knowPhase++; - knowledgeAddTerm (sys->know, rd->message); - explorify (sys, run); - sys->knowPhase--; - - knowledgeDelete (sys->know); - sys->know = oldknow; - } - return 1; -} diff --git a/src/match_basic.h b/src/match_basic.h deleted file mode 100644 index 88b5d58..0000000 --- a/src/match_basic.h +++ /dev/null @@ -1,11 +0,0 @@ -#ifndef MATCHBASIC -#define MATCHBASIC - -int matchRead_basic (const System sys, const int run, - int (*proceed) (System, int)); -int enabled_basic (const System sys, const Knowledge know, - const Term newterm); -int block_basic (const System sys, const int run); -int send_basic (const System sys, const int run); - -#endif diff --git a/src/match_clp.c b/src/match_clp.c index d1502b7..959fa3e 100644 --- a/src/match_clp.c +++ b/src/match_clp.c @@ -11,7 +11,6 @@ #include #include "match_clp.h" #include "system.h" -#include "memory.h" #include "constraint.h" #include "mgu.h" #include "memory.h" diff --git a/src/memory.c b/src/memory.c deleted file mode 100644 index 6894576..0000000 --- a/src/memory.c +++ /dev/null @@ -1,63 +0,0 @@ -/** - *@file - * \brief Memory functions - * - * These are not really used anymore, so maybe they should be removed. - * - * \par Performance - * Tests showed that memory pooling was actually much less efficient than - * having \c malloc() trying to fit stuff into the memory caches. - */ - -/* my own memory functions (not yet) */ - -#include -#include -#include -#ifdef DEBUG -#include -#endif -#include "memory.h" -#include "debug.h" - -/* for displaying the sizes */ - -#include "term.h" -#include "termlist.h" -#include "knowledge.h" -#include "substitution.h" -#include "system.h" - -//! Open memory code. -void -memInit () -{ -#ifdef DEBUG - if (DEBUGL (5)) - { - void sp (char *txt, int size) - { - printf ("Size of %s : %i\n", txt, size); - } - printf ("Data structure size.\n\n"); - sp ("pointer", sizeof (Term)); - sp ("term node", sizeof (struct term)); - sp ("termlist node", sizeof (struct termlist)); - sp ("knowledge node", sizeof (struct knowledge)); - sp ("substituition node", sizeof (struct substitution)); - sp ("substlist node", sizeof (struct substitutionlist)); - sp ("roledef node", sizeof (struct roledef)); - sp ("system node", sizeof (struct system)); - printf ("\n"); - } - mtrace (); -#endif - return; -} - -//! Close memory code. -void -memDone (int sw) -{ - return; -} diff --git a/src/memory.h b/src/memory.h deleted file mode 100644 index 6ff766c..0000000 --- a/src/memory.h +++ /dev/null @@ -1,35 +0,0 @@ -#ifndef MEMORY -#define MEMORY - -#include "string.h" -#include "debug.h" -#include - -void memInit (); -void memDone (); -#define memAlloc(t) malloc(t) -#define memFree(p,t) free(p) -#define memRealloc(p,t) realloc(p,t); - -#ifdef DEBUG -#define findLoserBegin(ign) int mem_before; \ - int mem_diff; \ - static int mem_errorcount = 0; \ - struct mallinfo mi; \ - mi = mallinfo(); \ - mem_before = mi.uordblks - ign; -#define findLoserEnd(ign,t) mi = mallinfo(); \ - mem_diff = mi.uordblks - ign - mem_before; \ - if (mem_diff != 0) \ - { \ - warning ("Memory leak in [%s] of %i", t, mem_diff); \ - mem_errorcount++; \ - if (mem_errorcount >= 1) \ - error ("More than enough leaks."); \ - } -#else -#define findLoserBegin(ign) ; -#define findLoserEnd(ign,t) ; -#endif - -#endif diff --git a/src/mgu.c b/src/mgu.c index ad27d25..d857b70 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -4,7 +4,6 @@ #include "termlist.h" #include "substitution.h" #include "mgu.h" -#include "memory.h" #include "type.h" #include "specialterm.h" diff --git a/src/modelchecker.c b/src/modelchecker.c deleted file mode 100644 index d77f478..0000000 --- a/src/modelchecker.c +++ /dev/null @@ -1,1458 +0,0 @@ -/*!\file modelchecker.c - * \brief The main procedures guiding the (optimized) traversal of the state space. - * - * This file implements various traversal methods through the state space. - */ - -#include -#include -#include -#include "substitution.h" -#include "knowledge.h" -#include "system.h" -#include "debug.h" -#include "modelchecker.h" -#include "report.h" -#include "memory.h" -#include "match_basic.h" -#include "match_clp.h" -#include "output.h" -#include "tracebuf.h" -#include "attackminimize.h" -#include "claim.h" -#include "switches.h" -#include "specialterm.h" - -/* - - A model checker. Really. -*/ - -/* - Some forward declarations. -*/ - -int traverseSimple (const System oldsys); -int traverseNonReads (const System oldsys); -int traversePOR4 (const System oldsys); -int traversePOR5 (const System oldsys); -int traversePOR6 (const System oldsys); -int traversePOR7 (const System oldsys); -int traversePOR8 (const System oldsys); -int propertyCheck (const System sys); -int executeTry (const System sys, int run); -int claimSecrecy (const System sys, const Term t); -int violateClaim (const System sys, int length, int claimev, Termlist reqt); -Termlist secrecyUnfolding (Term t, const Knowledge know); - -/* - Main code. -*/ - -void -statePrint (const System sys) -{ - int i, s; - Roledef rd; - - indent (); - printf ("state %i: ", sys->step); - for (i = 0; i < sys->maxruns; i++) - { - s = 0; - rd = runPointerGet (sys, i); - while (rd != NULL) - { - rd = rd->next; - s++; - } - printf ("%i ", s); - } - printf (" - phase %i, done %i", sys->PORphase, sys->PORdone); - printf ("\n"); -} - -//! Scenario selection makes sure implicit and explicit chooses are selected first. -/** - * This help function traverses any chooses first. - */ -__inline__ int -traverse_chooses_first (const System sys) -{ - int run_scan; - - for (run_scan = 0; run_scan < sys->maxruns; run_scan++) - { - Roledef rd_scan; - - rd_scan = runPointerGet (sys, run_scan); - if (rd_scan != NULL && // Not empty run - rd_scan == sys->runs[run_scan].start && // First event - rd_scan->type == READ) // Read - { - if (executeTry (sys, run_scan)) - return 1; - } - } - return 0; -} - -//! Main traversal call. -/** - * Branches into submethods. - */ -int -traverse (const System sys) -{ - /* maybe chooses have precedence over _all_ methods */ - if (switches.chooseFirst) - { - if (traverse_chooses_first (sys)) - return 1; - } - - /* branch for traversal methods */ - switch (switches.traverse) - { - case 1: - return traverseSimple (sys); - case 2: - return traverseNonReads (sys); - case 3: - case 4: - case 5: - case 6: - case 7: - error ("%i is an obsolete traversal method.", switches.traverse); - case 8: - return traversePOR4 (sys); - case 9: - return traversePOR5 (sys); - case 10: - return traversePOR6 (sys); - case 11: - return traversePOR7 (sys); - case 12: - return traversePOR8 (sys); - default: - error ("%i is NOT an existing traversal method.", switches.traverse); - } -} - -//! Progress counters to next step. -/** - * Does not really execute anything, it's just bookkeeping, progressing - * counters and such. - * - *@returns If it returns TRUE, explore. If false, don't traverse. - */ - -int -executeStep (const System sys, const int run) -{ - Roledef runPoint; - runPoint = runPointerGet (sys, run); -#ifdef DEBUG - if (DEBUGL (3)) - { - indent (); - printf ("exec: "); - roledefPrint (runPoint); - printf ("#%i\n", run); - } -#endif - sys->runs[run].step++; - runPointerSet (sys, run, runPoint->next); - - /* store knowledge for this step */ - (sys->step)++; - sys->traceKnow[sys->step] = sys->know; - - /* check for properties */ - propertyCheck (sys); - - /* set indent for printing */ - indentSet (sys->step); - /* hmmm, but what should it return if not exploring? */ - if (!sys->explore) - return 0; - - /* prune (exit) if enough attacks found */ - if (enoughAttacks (sys)) - return 0; - - /* we want to explore it, but are we allowed by pruning? */ - if (sys->step >= sys->maxtracelength) - { - /* cut off traces that are too long */ -#ifdef DEBUG - if (DEBUGL (4)) - { - indent (); - printf ("trace cut off.\n"); - if (DEBUGL (5)) - { - (sys->step)--; - tracePrint (sys); - (sys->step)++; - } - } -#endif - return 0; - } - - /* we will explore this state, so count it. */ - sys->states = statesIncrease (sys->states); - - /* what about scenario exploration? */ - if (switches.scenario && sys->step + 1 > switches.scenarioSize) - { - /* count states within scenario */ - sys->statesScenario = statesIncrease (sys->statesScenario); - } - - /* show progression */ - if (switches.reportStates > 0) - { - sys->interval = statesIncrease (sys->interval); - if (!statesSmallerThan - (sys->interval, (unsigned long int) switches.reportStates)) - { - globalError++; - sys->interval = STATES0; - eprintf ("States "); - statesFormat (sys->states); - eprintf (" \r"); - globalError--; - } - } - - /* store new node numbder */ - sys->traceNode[sys->step] = sys->states; - /* the construction below always assumes MAX_GRAPH_STATES to be smaller than the unsigned long it, which seems realistic. */ - if (switches.output == STATESPACE - && statesSmallerThan (sys->states, MAX_GRAPH_STATES)) - { - /* display graph */ - graphNode (sys); - } - return 1; -} - -//! Determine end of run after removing end reads, and optionally claims. -Roledef -removeDangling (Roledef rd, const int killclaims) -{ - Roledef rdkill; - - rdkill = rd; - while (rd != NULL) - { - if (rd->type == SEND || (!killclaims && rd->type == CLAIM)) - rdkill = rd; - rd = rd->next; - } - /* remove after rdkill */ - return rdkill; -} - -/** - * Determine for a roledef that is instantiated, the uninteresting ends bits. - * - *@todo "What is interesting" relies on the fact that there are only secrecy, sychnr and agreement properties. - */ -Roledef -removeIrrelevant (const System sys, const int run, Roledef rd) -{ - if (!isRunTrusted (sys, run)) - { - // untrusted, so also remove claims - return removeDangling (rd, 1); - } - else - { - // trusted, so only remove reads - return removeDangling (rd, 0); - } -} - - -//! Unblock any waiting sends of my type. -/** - * Note that the caller must ensure that rd->forbidden is restored afterwards. - *\sa tryChoiceSend() - */ -void -unblock_synchronising_labels (const System sys, const int run, - const Roledef rd) -{ - if (rd->type != READ || rd->internal) - return; - if (!inTermlist (sys->synchronising_labels, rd->label)) - return; - - // This read possibly unblocks other sends - int run_scan; - - for (run_scan = 0; run_scan < sys->maxruns; run_scan++) - { - if (run_scan != run) - { - Roledef rd_scan; - - rd_scan = sys->runs[run_scan].index; - if (rd_scan != NULL && - rd_scan->type == SEND && - rd_scan->forbidden != NULL && - isTermEqual (rd_scan->label, rd->label) && - isTermEqual (rd_scan->message, rd->message) && - isTermEqual (rd_scan->from, rd->from) && - isTermEqual (rd_scan->to, rd->to)) - { - rd_scan->forbidden = NULL; - } - } - } - return; -} - -//! Explores the system state given by the next step of a run. -/** Grandiose naming scheme (c) sjors dubya. - * - * After an event was instantiated, this function is called to explore the - * remainder of the system. - * - * Note that some additional pruning is done, so this function - * also determines the enabledness of the event that was just instantiated. - * - *@returns 1 (true) if the event was enabled. - *\sa match_basic(),executeTry() - */ - -int -explorify (const System sys, const int run) -{ - Roledef rd; - int flag; - int myStep; - Roledef roleCap, roleCapPart; - Knowledge forbiddenBuffer; - - rd = runPointerGet (sys, run); - myStep = sys->runs[run].step; - roleCap = NULL; - - if (rd == NULL) - { - error ("Trying to progress completed run!\n"); - } - - flag = 0; - - /** - * -------------------------------------------- - * Is the event really enabled? - * Typically, a read event is only instantiated - * at this point, so we can only now do some - * instantiation related determinings. - * -------------------------------------------- - */ - - /* - * Special checks after (implicit) choose events; always first in run reads. - */ - if (myStep == 0 && rd->type == READ) - { - int rid; - - if (inTermlist (sys->untrusted, agentOfRun (sys, run))) - { - /* this run is executed by an untrusted agent, do not explore */ - return 0; - } - /* executed by trusted agent */ - - /* Special check 1: if agents have been instantiated in such a way that no more claims in any run - * need to be evaluated, then we can skip - * further traversal. - */ - //!@todo This implementation relies on the fact that there are only secrecy, synchr and agreement properties. - if (switches.pruneNomoreClaims && sys->secrets == NULL) - { /* there are no remaining secrecy claims to be checked */ - Roledef rdscan; - int validclaim; - - rid = 0; - validclaim = 0; - /* check for each run */ - while (rid < sys->maxruns) - { - /* are claims in this run evaluated anyway? */ - if (isRunTrusted (sys, rid)) - { /* possibly claims to be checked in this run */ - rdscan = runPointerGet (sys, rid); - while (rdscan != NULL) - { - if (rdscan->type == CLAIM) - { - /* force abort of loop */ - validclaim = 1; - rdscan = NULL; - rid = sys->maxruns; - } - else - { - rdscan = rdscan->next; - } - } - } - rid++; - } - if (validclaim == 0) - { /* no valid claims, abort */ - return 0; - } - } - - /* Special check 2: Symmetry reduction on chooses. - * If the run we depend upon has already been activated (otherwise warn!) check for instance ordering - */ - - if (switches.agentSymmetries && sys->runs[run].prevSymmRun != -1) - { - /* there is such a run on which we depend */ - int ridSymm; - - ridSymm = sys->runs[run].prevSymmRun; - if (sys->runs[ridSymm].step == 0) - { - /* - * dependency run was not chosen yet, so we can't do anything now - */ - // warning ("Symmetrical run dependency #%i (for run #%i) has not chosen yet!", ridSymm, run); - } - else - { - /* dependent run has chosen, so we can compare */ - int order; - - order = - termlistOrder (sys->runs[run].agents, - sys->runs[ridSymm].agents); - if (order < 0) - { - /* we only explore the other half */ - return 0; - } - if (order == 0 && switches.reduceClaims) - { - /* identical run; only the first would be checked for a claim */ - /* so we cut off this run, including claims, turning it into a dummy run */ - roleCap = removeDangling (rd, 1); - } - } - } - - /* Special check 3: if after choosing, this run is untrusted and ends on (read|skippedclaim)*, we can remove that part already. - */ - - if (switches.reduceEndgame && roleCap == NULL) - roleCap = removeIrrelevant (sys, run, rd); - - /* Special check x: if all agents in each run send only encrypted stuff, and all agents are trusted, - * there is no way for the intruder to learn anything else than encrypted terms, so secrecy claims will not - * be violated anymore if they contain no terms that are encrypted with such keys */ - - //!@todo For now, there is no check that the runs only send publicly encrypted stuff! Just an assumption to be made true using static analysis. - - /* - rid = 0; - while (rid < sys->maxruns) - { - if (!isRunTrusted (sys, rid)) - { - } - rid++; - } - */ - } - - /* - * Special check b1: symmetry reduction part II on similar read events for equal roles. - */ - - if (switches.readSymmetries) - { - if (sys->runs[run].firstNonAgentRead == myStep) - { - /* Apparently, we have a possible ordering with our symmetrical friend. - * Check if it has progressed enough, and has the same agents. - */ - int ridSymm; - - if (rd->type != READ) - { - error ("firstNonAgentRead is not a read?!"); - } - ridSymm = sys->runs[run].prevSymmRun; - if (isTermlistEqual - (sys->runs[run].agents, sys->runs[ridSymm].agents)) - { - /* same agents, so relevant */ - if (myStep > 0 && sys->runs[ridSymm].step < myStep) - { - // warning ("Symmetrical firstread dependency #%i (for run #%i) has not chosen yet!", ridSymm, run); - } - else - { - if (sys->runs[ridSymm].step <= myStep) - { - // warning ("Symmetrical firstread dependency #%i (for run #%i) has not read it's firstNonAgentRead %i yet, as it is only at %i!", ridSymm, run, myStep, sys->runs[ridSymm].step); - } - else - { - /* read was done, so we can compare them */ - int i; - Roledef rdSymm; - - rdSymm = sys->runs[ridSymm].start; - i = myStep; - while (i > 0) - { - rdSymm = rdSymm->next; - i--; - } - /* rdSymm now points to the instance of the symmetrical read */ - i = termOrder (rdSymm->message, rd->message); - if (i < 0) - { - /* only explore symmetrical variant */ - return 0; - } - } - } - } - } - } - - /* Special check b2: symmetry order reduction. - * - * Concept: when there are two identical runs w.r.t. agents, we can make sure one goes before the other. - * Depends on prevSymm, skipping chooses even. - */ - - if (switches.orderSymmetries && myStep == sys->runs[run].firstReal) - { - if (sys->runs[run].prevSymmRun != -1) - { - /* there is such a run on which we depend */ - int ridSymm; - - ridSymm = sys->runs[run].prevSymmRun; - /* equal runs? */ - - if (isTermlistEqual - (sys->runs[run].agents, sys->runs[ridSymm].agents)) - { - /* so, we have an identical partner */ - /* is our partner there already? */ - if (sys->runs[ridSymm].step <= myStep) - { - /* not yet there, this is not a valid exploration */ - /* verify !! */ - return 0; - } - } - } - } - - /** - * Final special check; we must be sure that chooses have been done. Only - * necessary for scenario != 0. - * - * Note: any choose selection after this would result in empty scenarios, so this - * should be the last special check. - */ - if (switches.scenario != 0) - { - /* two variants. If scenario size is 0, we operate on the old method involving chooses */ - if (switches.scenarioSize == 0) - { - /* only after chooses */ - if (myStep == 0 && rd->type == READ) - { - if (run == sys->lastChooseRun) - { - /* We are just after the last choose instance */ - /* count this instance */ - if (sys->countScenario < INT_MAX) - { - sys->countScenario++; - } - /* If we are displaying scenarios, print it */ - if (switches.output == SCENARIOS) - { - printf ("%i\t", sys->countScenario); - scenarioPrint (sys); - printf ("\n"); - } - /* If it is not the selected one, abort */ - if (switches.scenario != sys->countScenario) - { - /* this branch is not interesting */ - /* unfortunately, it is also not drawn in the state graph because of this */ - if (switches.output == STATESPACE) - { - graphScenario (sys, run, rd); - } - /* act as if executed, but don't really explore it. */ - return 1; - } - } - } - } - else - { - /* scenario size is not zero */ - - //!@todo Optimization: if the good scenario is already traversed, other trace prefixes need not be explored any further. - if (sys->step + 1 == switches.scenarioSize) - { - /* Now, the prefix has been set. Count it */ - if (sys->countScenario < INT_MAX) - { - sys->countScenario++; - } - if (switches.output == SCENARIOS) - { - /* apparently we want the output */ - int index; - eprintf ("%i\t", sys->countScenario); - index = 0; - while (index < switches.scenarioSize) - { - roledefPrint (sys->traceEvent[index]); - eprintf ("#%i; ", sys->traceRun[index]); - index++; - } - eprintf ("\n"); - } - /* Is this the selected one? */ - if (switches.scenario != sys->countScenario) - { - /* unfortunately, it is also not drawn in the state graph because of this */ - if (switches.output == STATESPACE) - { - graphScenario (sys, run, rd); - } - /* act as if executed, but don't really explore it. */ - return 1; - } - } - } - } - - /** - * -------------------------------------------- - * Now we assume the event is indeed enabled ! - * -------------------------------------------- - */ - - /* (Possibly) do some local damage */ - // Unblock any sends - forbiddenBuffer = rd->forbidden; - if (sys->synchronising_labels != NULL) - { - unblock_synchronising_labels (sys, run, rd); - } - // Cap roles - if (roleCap != NULL) - { - roleCapPart = roleCap->next; - roleCap->next = NULL; - } - - /* And explore the resulting system */ - if (executeStep (sys, run)) - { - /* traverse the system after the step */ - flag = traverse (sys); - } - /* restore executeStep "damage" */ - runPointerSet (sys, run, rd); // reset rd pointer - sys->runs[run].step = myStep; // reset local index - sys->step--; - indentSet (sys->step); - - /* restore local damage */ - rd->forbidden = forbiddenBuffer; - if (roleCap != NULL) - { - roleCap->next = roleCapPart; - } - return 1; // The event was indeed enabled (irrespective of traverse!) -} - - - -//! Simple nondeterministic traversal. - -__inline__ int -traverseSimple (const System sys) -{ - int run; - int flag = 0; - - for (run = 0; run < (sys->maxruns); run++) - { - if (runPointerGet (sys, run) != NULL) - { - flag = 1; - executeTry (sys, run); - } - } - if (!flag) - { - /* trace was not succesful */ - } - return flag; -} - -/** - * ----------------------------------------------------- - * - * Traversal Methods - * - * ----------------------------------------------------- - */ - -/* - * Some assistance macros - */ -#define predRead(sys,rd) ( rd->type == READ && !rd->internal ) -#define isRead(sys,rd) ( rd != NULL && predRead(sys,rd) ) -#define nonRead(sys,rd) ( rd != NULL && !predRead(sys,rd) ) - -/* - * nonReads - * - * Do a certain type of action first, i.e. that which satisfies nonRead(System, - * Roledef). Use the inverse of this predicate to detect the other type of - * event. - */ - -__inline__ int -nonReads (const System sys) -{ - /* all sends first, then simple nondeterministic traversal */ - - int run; - Roledef rd; - - /* check for existence of executable sends */ - for (run = 0; run < (sys->maxruns); run++) - { - rd = runPointerGet (sys, run); - if (nonRead (sys, rd)) - { - return executeTry (sys, run); - } - } - return 0; -} - -/* - * First traverse any non-reads, then non-deterministically the reads. - */ - -__inline__ int -traverseNonReads (const System sys) -{ - if (nonReads (sys)) - return 1; - else - return traverseSimple (sys); -} - -//! Execute a send -/** - *\sa unblock_synchronising_labels() - */ - -__inline__ int -tryChoiceSend (const System sys, const int run, const Roledef rd) -{ - int flag; - - flag = 0; - if (rd->forbidden == NULL) - { - /* this is allowed. So we either try it, or we try it later (if blocking) */ - /* Note that a send in executetry will always succeed. */ - /* 1. Simply try */ - flag = executeTry (sys, run); - /* 2. Postpone if synchonisable */ - if (flag && inTermlist (sys->synchronising_labels, rd->label)) - { - /* This is supposed to be blocked, so we do so */ - /* It will possibly be unblocked by a corresponding read event, - * the actual code would be in explorify, post instantiation of the read event. - */ - if (switches.clp) - { - block_clp (sys, run); - } - else - { - block_basic (sys, run); - } - } - } - return flag; -} - -//! Execute a read in the knowledge postponing way, on which the partial order reduction for secrecy depends. - -__inline__ int -tryChoiceRead (const System sys, const int run, const Roledef rd) -{ - int flag; - - flag = 0; - - /* the sendsdone check only prevent - * some unneccessary inKnowledge tests, - * and branch tests, still improves - * about 15% */ - if (sys->knowPhase > rd->knowPhase) - { - /* apparently there has been a new knowledge item since the - * previous check */ - - /* implicit check for enabledness */ - flag = executeTry (sys, run); - - /* if it was enabled (flag) we postpone it if it makes sense - * to do so (hasVariable, non internal) */ - if (flag && hasTermVariable (rd->message) && !rd->internal) - { - int stackKnowPhase = rd->knowPhase; - - rd->knowPhase = sys->knowPhase; - if (switches.clp) - { - block_clp (sys, run); - } - else - { - block_basic (sys, run); - } - rd->knowPhase = stackKnowPhase; - } - } - return flag; -} - -//! Try to execute the event at the roledef. Returns true iff it was enabled, and thus explored. -/** - * Note that rd should not be NULL - */ -__inline__ int -tryChoiceRoledef (const System sys, const int run, const Roledef rd) -{ - int flag; - -#ifdef DEBUG - if (rd == NULL) - error ("tryChoiceRoledef should not be called with a NULL rd pointer"); -#endif - - flag = 0; - switch (rd->type) - { - case CLAIM: - flag = executeTry (sys, run); - break; - - case SEND: - flag = tryChoiceSend (sys, run, rd); - break; - - case READ: - flag = tryChoiceRead (sys, run, rd); - break; - - default: - fprintf (stderr, "Encountered unknown event type %i.\n", rd->type); - exit (1); - } - return flag; -} - -//! Try to execute the event in a given run -__inline__ int -tryChoiceRun (const System sys, const int run) -{ - Roledef rd; - - rd = runPointerGet (sys, run); - if (rd != NULL) - return tryChoiceRoledef (sys, run, rd); - else - return 0; -} - -//! Yield the last active run in the partial trace, or 0 if there is none. -__inline__ int -lastActiveRun (const System sys) -{ - if (sys->step == 0) - { - /* first step, start at 0 */ - return 0; - } - else - { - /* there was a previous action, start scan from there */ -#ifdef DEBUG - if (switches.switchP < 100) - return sys->traceRun[sys->step - 1] + switches.switchP; -#endif - return sys->traceRun[sys->step - 1]; - } -} - -//! Determine whether a roleevent is a choose event -__inline__ int -isChooseRoledef (const System sys, const int run, const Roledef rd) -{ - return (rd == sys->runs[run].start && rd->type == READ && rd->internal); -} - -//! Explore possible chooses first -__inline__ int -tryChoosesFirst (const System sys) -{ - int flag; - int run; - Roledef rd; - - flag = 0; - for (run = 0; run < sys->maxruns && !flag; run++) - { - rd = runPointerGet (sys, run); - if (isChooseRoledef (sys, run, rd)) - flag = tryChoiceRoledef (sys, run, rd); - } - return flag; -} - -//! Explore left-to-right (from an offset) -__inline__ int -tryEventsOffset (const System sys, const int offset) -{ - int flag; - int run; - int i; - - flag = 0; - for (i = 0; i < sys->maxruns && !flag; i++) - { - run = (i + offset) % sys->maxruns; - flag = tryChoiceRun (sys, run); - } - return flag; -} - -/* - * POR4 - * - * This is the simplified version of the algorithm, to be compared with - * the -t7 version. - * - * Based on some new considerations. - */ - -__inline__ int -traversePOR4 (const System sys) -{ - return tryEventsOffset (sys, lastActiveRun (sys)); -} - -/* - * POR5 - * - * POR4 but does chooses first. - */ - -__inline__ int -traversePOR5 (const System sys) -{ - if (tryChoosesFirst (sys)) - return 1; - return tryEventsOffset (sys, lastActiveRun (sys)); -} - -/* - * POR6 - * - * POR5 but has a left-oriented scan instead of working from the current run. - */ - -__inline__ int -traversePOR6 (const System sys) -{ - return tryEventsOffset (sys, 0); -} - -/* - * POR7 - * - * Left-oriented scan, to ensure reductions. However, first does all initial actions. - */ - -__inline__ int -traversePOR7 (const System sys) -{ - if (tryChoosesFirst (sys)) - return 1; - tryEventsOffset (sys, 0); -} - -/* - * POR8 - * - * POR6, but tries to continue on the current run first. This turned out to be highly more efficient. - */ - -__inline__ int -traversePOR8 (const System sys) -{ - int flag; - int run; - int last; - - last = lastActiveRun (sys); - flag = tryChoiceRun (sys, last); - for (run = 0; run < sys->maxruns && !flag; run++) - { - if (run != last) - flag = tryChoiceRun (sys, run); - } - return flag; -} - - -//! 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 -propertyCheck (const System sys) -{ - int flag = 1; // default: properties are true, no attack - - /* for now, we only check secrecy */ - if (sys->secrets != NULL) - { - Termlist scan; - scan = sys->secrets; - while (scan != NULL) - { - if (!claimSecrecy (sys, scan->term)) - { - /* apparently, secrecy of this term was violated */ - /* find the violated claim event */ - - Termlist tl = NULL; - int claimev = -1; - int i = 0; - - while (claimev == -1 && i <= sys->step) - { - if (sys->traceEvent[i]->type == CLAIM && - sys->traceEvent[i]->to == CLAIM_Secret) - { - Termlist tl = secrecyUnfolding (scan->term, sys->know); - if (tl != NULL) - { - /* This was indeed a violated claim */ - claimev = i; - } - } - i++; - } - /* do we have it? */ - if (claimev == -1) - { - /* weird, should not occur */ - fprintf (stderr, "Violation, but cannot locate claim.\n"); - printf - ("A secrecy claim was supposed to be violated on term "); - termPrint (scan->term); - printf (" but we couldn't find the corresponding claim.\n"); - exit (1); - } - else - { - /* fine. so it's violated */ - violateClaim (sys, sys->step, claimev, tl); - termlistDelete (tl); - flag = 0; - } - } - scan = scan->next; - } - - } - return flag; -} - -/* true iff the term is secret */ - -int -isTermSecret (const System sys, const Term t) -{ - switch (switches.clp) - { - case 0: - /* test for simple inclusion */ - if (inKnowledge (sys->know, t)) - return 0; - if (isTermVariable (t)) - { - /* it's a variable! */ - - /* TODO that does not necessarily mean we can choose it, does - * it? NO: the rule should be: there is at least one message - * in knowledge. We don't check it currently.*/ - - return 0; - } - return 1; - case 1: - /* CLP stuff */ - return secret_clp (sys, t); - default: - return 0; - } -} - -/* true iff the claim is valid */ - -int -claimSecrecy (const System sys, const Term t) -{ - int csScan (Term t) - { - t = deVar (t); - if (isTermTuple (t)) - return csScan (TermOp1 (t)) && csScan (TermOp2 (t)); - else - return isTermSecret (sys, t); - } - - if (csScan (t)) - return 1; - else - { - /* Not reported anymore here, but only at the end */ - // reportSecrecy (sys, t); - return 0; - } -} - -/* - * Unfold the secrecy tuple and construct a list of terms that violate it. - */ - -Termlist -secrecyUnfolding (Term t, const Knowledge know) -{ - t = deVar (t); - if (isTermTuple (t)) - return termlistConcat (secrecyUnfolding (TermOp1 (t), know), - secrecyUnfolding (TermOp2 (t), know)); - else - { - if (inKnowledge (know, t)) - return termlistAdd (NULL, t); - else - return NULL; - } -} - -/* - * for reporting we need a more detailed output of the claims. - * Output is a termlist pointer, or -1. - * - * in: claim roledef, knowledge for which it is violated - * - * -1 : claim was ignored - * NULL : claim is fulfilled (true) - * Termlist: claim was violated, termlist terms are know to the intruder. - */ - -Termlist -claimViolationDetails (const System sys, const int run, const Roledef rd, - const Knowledge know) -{ - if (rd->type != CLAIM) - { - fprintf (stderr, - "Trying to determine details of something other than a claim!\n"); - exit (-1); - } - - /* cases */ - if (rd->to == CLAIM_Secret) - { - /* secrecy claim */ - - if (!isRunTrusted (sys, run)) - { - /* claim was skipped */ - return (Termlist) - 1; - } - else - { - /* construct violating subterms list */ - return secrecyUnfolding (rd->message, know); - } - } - return NULL; -} - -//! A claim was violated. -/** - * This happens when we violate a claim. - * Lots of administration. - *@returns True iff explorify is in order. - */ -int -violateClaim (const System sys, int length, int claimev, Termlist reqt) -{ - int flag; - Claimlist clinfo; - - /* default = no adaption of pruning, continue search */ - flag = 1; - - /* enough? */ - if (enoughAttacks (sys)) - return flag; - - /* Count the violations */ - sys->attackid++; - sys->failed = statesIncrease (sys->failed); - clinfo = sys->traceEvent[claimev]->claiminfo; - clinfo->failed = statesIncrease (clinfo->failed); // note: for modelchecking secrecy, this can lead to more fails (at further events in branches of the tree) than claim encounters - - /* mark the path in the state graph? */ - if (switches.output == STATESPACE) - { - graphPath (sys, length); - } - - /* Copy the current trace to the buffer, if the new one is shorter than the previous one. */ - if (sys->attack == NULL || length < sys->attack->reallength) - { - tracebufDone (sys->attack); - sys->attack = tracebufSet (sys, length, claimev); - attackMinimize (sys, sys->attack); - sys->shortestattack = sys->attack->reallength; - - /* maybe there is some new pruning going on */ - flag = 0; - switch (switches.prune) - { - case 0: - flag = 1; - break; - case 1: - break; - case 2: - sys->maxtracelength = sys->shortestattack - 1; - break; - } - } - return flag; -} - -//! Try to execute the next event in a run. -/** - * One of the core functions of the system. - *@returns 0 (false) if the event was not enabled. 1 (true) if there was an enabled instantiation of this event. - */ -int -executeTry (const System sys, int run) -{ - Roledef runPoint; - int flag = 0; - - runPoint = runPointerGet (sys, run); - sys->traceEvent[sys->step] = runPoint; // store for later usage, problem: variables are substituted later... - sys->traceRun[sys->step] = run; // same - - if (runPoint == NULL) - { -#ifdef DEBUG - /* warning, ought not to occur */ - debug (2, "Trying to activate completed run"); -#endif - } - else - { -#ifdef DEBUG - if (DEBUGL (4)) - { - indent (); - printf ("try: "); - roledefPrint (runPoint); - printf ("#%i\n", run); - } -#endif - if (runPoint->type == READ) - { - if (switches.clp) - return matchRead_clp (sys, run, explorify); - else - return matchRead_basic (sys, run, explorify); - } - if (runPoint->type == SEND) - { - if (switches.clp) - flag = send_clp (sys, run); - else - flag = send_basic (sys, run); - return flag; - } - - /* - * Execute claim event - */ - if (runPoint->type == CLAIM) - { - /* first we might dynamically determine whether the claim is valid */ - if (!isRunTrusted (sys, run)) - { - /* for untrusted agents we check no claim violations at all - * so: we know it's okay. */ - /* TODO for CLP this doesn't work and call for branching, if the - * agent is a variable */ -#ifdef DEBUG - if (DEBUGL (3)) - { - indent (); - printf ("Skipped claim in untrusted run with agents "); - termlistPrint (sys->runs[run].agents); - printf ("\n"); - } -#endif - explorify (sys, run); - return 1; - } - - /* determine type of claim, and parameters */ -#ifdef DEBUG - if (DEBUGL (2)) - { - indent (); - printf ("claim: "); - roledefPrint (runPoint); - printf ("#%i\n", run); - } -#endif - /* - * update claim counters - */ - sys->claims = statesIncrease (sys->claims); - - /* - * distinguish claim types - */ - if (runPoint->to == CLAIM_Secret) - { - /* - * SECRECY - */ - /* TODO claims now have their own type, test for that */ - /* TODO for now it is secrecy of the message */ - - Termlist oldsecrets = sys->secrets; - /* TODO this can be more efficient, by filtering out double occurrences */ - sys->secrets = - termlistAdd (termlistShallow (oldsecrets), runPoint->message); - flag = claimSecrecy (sys, runPoint->message); - runPoint->claiminfo->count++; - - /* now check whether the claim failed for further actions */ - if (!flag) - { - /* violation */ - Termlist tl; - - tl = claimViolationDetails (sys, run, runPoint, sys->know); - if (violateClaim (sys, sys->step + 1, sys->step, tl)) - flag = explorify (sys, run); - termlistDelete (tl); - } - else - { - /* no violation */ - flag = explorify (sys, run); - } - - /* reset secrets list */ - termlistDelete (sys->secrets); - sys->secrets = oldsecrets; - } - else if (runPoint->to == CLAIM_Nisynch) - { - /* - * NISYNCH - */ - flag = check_claim_nisynch (sys, sys->step); - if (!flag) - { - /* violation */ - if (violateClaim (sys, sys->step + 1, sys->step, NULL)) - flag = explorify (sys, run); - } - else - { - /* no violation */ - flag = explorify (sys, run); - } - } - else if (runPoint->to == CLAIM_Niagree) - { - /* - * NIAGREE - */ - flag = check_claim_niagree (sys, sys->step); - if (!flag) - { - /* violation */ - if (violateClaim (sys, sys->step + 1, sys->step, NULL)) - flag = explorify (sys, run); - } - else - { - /* no violation */ - flag = explorify (sys, run); - } - } - else // if (runPoint->to == CLAIM_Empty) - { - // Skip other claim types - flag = explorify (sys, run); - } - } - /* a claim always succeeds */ - flag = 1; - } - return flag; -} diff --git a/src/modelchecker.h b/src/modelchecker.h deleted file mode 100644 index d2fb81d..0000000 --- a/src/modelchecker.h +++ /dev/null @@ -1,7 +0,0 @@ -#define MAX_GRAPH_STATES 1000 //!< Maximum number of state space nodes drawn -int traverse (const System oldsys); -int explorify (const System sys, const int run); -int executeStep (const System sys, const int run); -int propertyCheck (const System sys); -Termlist claimViolationDetails (const System sys, const int run, const Roledef - rd, const Knowledge know); diff --git a/src/output.c b/src/output.c deleted file mode 100644 index 94457f0..0000000 --- a/src/output.c +++ /dev/null @@ -1,703 +0,0 @@ -/* - * output.c - * - * Outputs an attack. - * Currently, every attack is printed. - */ - -#include -#include -#include "system.h" -#include "latex.h" -#include "switches.h" - - -void -linePrint (int i) -{ - indent (); - while (i > 0) - { - printf ("--------"); - i--; - } - printf ("\n"); -} - -int -correspondingSend (const System sys, int rd) -{ - - int labelMatch = 0; - int toMatch = 0; - int fromMatch = 0; - int tofromMatch = 0; - int messageMatch = 0; - int nMatches = 0; - int maxNMatches = 0; - - int readEvent = rd; - int sendEvent = -1; - int bestSendEvent = -1; - - for (sendEvent = readEvent; sendEvent >= 0; sendEvent--) - { - if (sys->traceEvent[sendEvent]->type == SEND) - { - /* do all the different kind of matchings first */ - - labelMatch = - isTermEqualFn (sys->traceEvent[sendEvent]->label, - sys->traceEvent[readEvent]->label); - toMatch = - isTermEqualFn (sys->traceEvent[sendEvent]->to, - sys->traceEvent[readEvent]->to); - fromMatch = - isTermEqualFn (sys->traceEvent[sendEvent]->from, - sys->traceEvent[readEvent]->from); - tofromMatch = toMatch || fromMatch; - messageMatch = - isTermEqualFn (sys->traceEvent[sendEvent]->message, - sys->traceEvent[readEvent]->message); - - /* calculate the score */ - - nMatches = labelMatch + tofromMatch + messageMatch; - - if (nMatches == 3) - { - /* bingo! success on all matches */ - - //printf("Found perfect match: %d\n", s); - bestSendEvent = sendEvent; - break; - } - if (nMatches > maxNMatches) - { - /* if we found a better candidate than we already had, we'll update */ - - //printf("Comparing SEND #%d: ",s); - //if (labelMatch) printf("label "); - //if (toMatch) printf("to "); - //if (fromMatch) printf("from "); - //if (messageMatch) printf("message "); - //printf("\n"); - - /* however, we first want to be sure that at least some matches are successful */ - - if (labelMatch && messageMatch) - { - /* strongest restriction: message and label should match */ - - maxNMatches = nMatches; - bestSendEvent = sendEvent; - - } - else if (messageMatch) - { - /* if label AND message don't match: */ - /* at least message should match */ - - maxNMatches = nMatches; - bestSendEvent = sendEvent; - } - else if (labelMatch) - { - /* if message doesn't match */ - /* the label should matches */ - - maxNMatches = nMatches; - bestSendEvent = sendEvent; - } - //printf("Best match: %d maxNMatches: %d\n", s, maxNMatches); - } - } - } - - //bestSendEvent = NULL; - if (bestSendEvent == -1) - { - /*Termlist tl; - Term t; - - //newtl = knowledgeNew(sys->traceKnow[i],sys->traceKnow[i+1]); - - for (tl = sys->traceKnow[rd]->basic; tl != NULL; tl = tl->next) - { - t = tl->term; - termPrint(t); - printf(" - "); - } - printf("\n"); - for (tl = sys->traceKnow[rd]->encrypt; tl != NULL; tl = tl->next) - { - t = tl->term; - termPrint(t); - printf(" - "); - } - printf("\n"); - for (tl = sys->traceKnow[rd]->inverses; tl != NULL; tl = tl->next) - { - t = tl->term; - termPrint(t); - printf(" - "); - } - printf("\n"); */ - - int u; - - for (u = 0; u < rd; u++) - { - if (sys->traceEvent[u]->type == SEND) - { - - - //termPrint(readEvent->message); - //printf("\n"); - knowledgePrint (sys->traceKnow[u]); - //printf("Is received message in knowledge after SEND %d? %d\n", u, inKnowledge(sys->traceKnow[u+1],readEvent->message)); - if (inKnowledge - (sys->traceKnow[u + 1], - sys->traceEvent[readEvent]->message)) - { - bestSendEvent = u; - break; - } - } - } - } - - if (bestSendEvent == -1) - { - printf ("!! Could not find a matching SEND\n"); - } - else - { - //latexMessagePrint(sys, bestSendEvent, readEvent); - //printf("Latex: "); - //termPrint(bestSendEvent->from); - //printf(" -> "); - if (!isTermEqualFn - (sys->traceEvent[bestSendEvent]->to, - sys->traceEvent[readEvent]->to)) - { - //termPrint(bestSendEvent->to); - //printf(" -> "); - } - if (!isTermEqualFn - (sys->traceEvent[bestSendEvent]->from, - sys->traceEvent[readEvent]->from)) - { - //termPrint(readEvent->from); - //printf(" -> "); - } - //termPrint(readEvent->to); - //printf("\n"); - } - return bestSendEvent; -} - -void -tracePrint (const System sys) -{ - int i, j; - int lastrid; - int width; - Termlist newtl; - - void sticks (int i) - { - while (i > 0) - { - printf ("|\t"); - i--; - } - } - - void sticksLine (void) - { - sticks (width); - printf ("\n"); - } - - if (switches.latex) - { - //latexTracePrint(sys); - return; - } - - /* fix the 'next' knowledge, this is required because sometimes - * when calling this function, the next knowledge is not stored - * yet, but required for the general form of the output . */ - - sys->traceKnow[sys->step + 1] = sys->know; - - - /* how wide is the trace? */ - width = 0; - for (i = 0; i <= sys->step; i++) - { - if (sys->traceRun[i] >= width) - width = sys->traceRun[i] + 1; - } - - linePrint (width); - indent (); - printf ("Dumping trace:\n"); - linePrint (width); - - /* first some parameter issues */ - - knowledgePrint (sys->traceKnow[0]); - /* also print inverses */ - indent (); - printf ("Inverses: "); - knowledgeInversesPrint (sys->traceKnow[0]); - printf ("\n"); - - /* Trace columns header. First the run identifier and role. On the - * second line we have the perceived agents for each partner role. - * These are printed in the same order as the role specification in the - * protocol. */ - - linePrint (width); - indent (); - - for (i = 0; i < width; i++) - { - termPrint (sys->runs[i].role->nameterm); - printf ("#%i\t", i); - } - printf ("\n"); - for (i = 0; i < width; i++) - { - termPrint (agentOfRun (sys, i)); - printf ("\t"); - } - printf ("\n"); - - for (i = 0; i < width; i++) - { - agentsOfRunPrint (sys, i); - printf ("\t"); - } - printf ("\n"); - - /* now we print the actual trace */ - - linePrint (width); - lastrid = -1; - for (i = 0; i <= sys->step; i++) - { - /* yields extra newlines between switching of runs */ - - j = sys->traceRun[i]; - if (j != lastrid) - { - sticksLine (); - lastrid = j; - } - - /* print the actual event */ - - indent (); - sticks (j); - roledefPrint (sys->traceEvent[i]); - - //if (sys->traceEvent[i]->type == READ && !sys->traceEvent[i]->internal) - //{ - /* calls routine to find the best SEND-candidate */ - /* the result is not yet being used */ - - // printf("\n"); - // correspondingSend(sys, i); - //} - - /* have we learnt anything new? */ - newtl = knowledgeNew (sys->traceKnow[i], sys->traceKnow[i + 1]); - if (newtl != NULL) - { - printf ("\n"); - sticksLine (); - sticks (width); - printf ("/* Intruder learns "); - termlistPrint (newtl); - termlistDelete (newtl); - printf (" */"); - lastrid = -1; - } - - /* new line */ - printf ("\n"); - } - - switch (switches.clp) - { - case 1: - indent (); - printf ("---[ constraints ]-----\n"); - constraintlistPrint (sys->constraints); - break; - default: - break; - } - linePrint (width); -} - - - -void -attackDisplayAscii (const System sys) -{ - int i, j; - int length; - int lastrid; - int width; - Termlist newtl; - struct tracebuf *tb; - - void sticks (int i) - { - while (i > 0) - { - printf ("|\t"); - i--; - } - } - - void sticksLine (void) - { - sticks (width); - printf ("\n"); - } - - /* attack trace buffer */ - tb = sys->attack; - length = sys->attack->length; - - /* set variables */ - varbufSet (sys, tb->variables); - - /* how wide is the trace? */ - width = 0; - for (i = 0; i < length; i++) - { - if (tb->run[i] >= width) - width = tb->run[i] + 1; - } - - linePrint (width); - indent (); - printf ("Dumping trace:\n"); - linePrint (width); - - /* first some parameter issues */ - - knowledgePrint (tb->know[0]); - printf ("Variables: "); - termlistPrint (sys->variables); - printf ("\n"); - - /* Trace columns header. First the run identifier and role. On the - * second line we have the perceived agents for each partner role. - * These are printed in the same order as the role specification in the - * protocol. */ - - linePrint (width); - indent (); - - for (i = 0; i < width; i++) - { - termPrint (sys->runs[i].role->nameterm); - printf ("#%i\t", i); - } - printf ("\n"); - for (i = 0; i < width; i++) - { - termPrint (agentOfRun (sys, i)); - printf ("\t"); - } - printf ("\n"); - - for (i = 0; i < width; i++) - { - agentsOfRunPrint (sys, i); - printf ("\t"); - } - printf ("\n"); - - /* now we print the actual trace */ - - linePrint (width); - lastrid = -1; - for (i = 0; i < length; i++) - { - /* yields extra newlines between switching of runs */ - - j = tb->run[i]; - if (j != lastrid) - { - sticksLine (); - lastrid = j; - } - - /* print the actual event */ - - indent (); - sticks (j); - roledefPrint (tb->event[i]); - - //if (sys->traceEvent[i]->type == READ && !sys->traceEvent[i]->internal) - //{ - /* calls routine to find the best SEND-candidate */ - /* the result is not yet being used */ - - // printf("\n"); - // correspondingSend(sys, i); - //} - - /* have we learnt anything new? */ - newtl = knowledgeNew (tb->know[i], tb->know[i + 1]); - if (newtl != NULL) - { - printf ("\n"); - sticksLine (); - sticks (width); - printf ("/* Intruder learns "); - termlistPrint (newtl); - termlistDelete (newtl); - printf (" */"); - lastrid = -1; - } - - /* new line */ - printf ("\n"); - } - - linePrint (width); -} - - -void -attackDisplay (const System sys) -{ - if (switches.latex) - { - attackDisplayLatex (sys); - } - else - { - attackDisplayAscii (sys); - } -} - -/* - *------------------------------------------- - * state space graph section - *------------------------------------------- - */ - -void -graphInit (const System sys) -{ - Termlist tl; - - /* drawing state space. */ - printf ("digraph Statespace {\n"); - - /* label */ - printf ("\tcomment = \"$"); - commandlinePrint (stdout); - printf ("\";\n"); - - /* fit stuff onto the page */ - printf ("\trankdir=LR;\n"); - printf ("\tsize=\"8.5,11\";\n"); - //printf ("\tpage=\"8.5,11\";\n"); - printf ("\tfontsize=\"6\";\n"); - printf ("\tfontname=\"Helvetica\";\n"); - printf ("\tmargin=0.5;\n"); - printf ("\tnodesep=0.06;\n"); - printf ("\tranksep=0.01;\n"); - printf ("\torientation=landscape;\n"); - printf ("\tcenter=true;\n"); - // printf ("\tlabeljust=\"r\";\n"); - printf ("\tconcentrate=true;\n"); - - /* node/edge defaults */ - printf - ("\tnode [shape=\"point\",fontsize=\"4\",fontname=\"Helvetica\"];\n"); - printf ("\tedge [fontsize=\"4\",fontname=\"Helvetica\"];\n"); - - /* start with initial node 0 */ - printf ("\tn"); - statesFormat (STATES0); - printf (" [shape=box,height=0.2,label=\"M0: "); - tl = knowledgeSet (sys->know); - termlistPrint (tl); - termlistDelete (tl); - printf ("\"];\n"); -} - -void -graphDone (const System sys) -{ - /* drawing state space. close up. */ - printf ("}\n"); -} - -void -graphNode (const System sys) -{ - Termlist newtl; - states_t thisNode, parentNode; - int index; - int run; - Roledef rd; - - /* determine node numbers */ - index = sys->step - 1; - parentNode = sys->traceNode[index]; - thisNode = sys->states; - rd = sys->traceEvent[index]; - run = sys->traceRun[index]; - - /* add node */ - printf ("\tn"); - statesFormat (thisNode); - printf (" ["); - - newtl = knowledgeNew (sys->traceKnow[index], sys->traceKnow[index + 1]); - if (newtl != NULL) - { - /* knowledge added */ - printf ("shape=box,height=0.2,label=\"M + "); - termlistPrint (newtl); - termlistDelete (newtl); - printf ("\""); - } - else - { - /* no added knowledge */ - if (switches.scenario != 0 && - rd != NULL && - rd == sys->runs[run].start && - rd->type == READ && run == sys->lastChooseRun) - { - /* last choose; scenario selected */ - printf ("shape=box,height=0.2,label=\"Scenario %i: ", - sys->countScenario); - scenarioPrint (sys); - printf ("\""); - } - else - { - printf ("label=\"\""); - } - } - printf ("];\n"); - - /* add edge */ - printf ("\tn"); - statesFormat (parentNode); - printf (" -> n"); - statesFormat (thisNode); - /* add label */ - printf (" [label=\""); - - // Print step - printf ("%i:", sys->runs[run].step - 1); - - if (rd->type == CLAIM && (!isRunTrusted (sys, run))) - { - printf ("Skip claim in #%i\"", run); - } - else - { - // Print event - roledefPrint (rd); - printf ("#%i\"", run); - if (rd->type == CLAIM) - { - printf (",shape=house,color=green"); - } - } - /* a choose? */ - if (rd->type == READ && rd->internal) - { - printf (",color=blue"); - //printf (",style=dotted"); - } - printf ("]"); - printf (";\n"); -} - -void -graphNodePath (const System sys, const int length, const char *nodepar) -{ - int i; - states_t thisNode; - - i = 0; - while (i < length) - { - /* determine node number */ - thisNode = sys->traceNode[i]; - - /* color node */ - printf ("\tn"); - statesFormat (thisNode); - printf (" [%s];\n", nodepar); - i++; - } -} - -void -graphEdgePath (const System sys, const int length, const char *edgepar) -{ - int i; - states_t thisNode, prevNode; - - i = 0; - prevNode = sys->traceNode[i]; - while (i < length) - { - /* determine node number */ - thisNode = sys->traceNode[i + 1]; - - /* color edge */ - printf ("\tn"); - statesFormat (prevNode); - printf (" -> n"); - statesFormat (thisNode); - printf (" [%s];\n", edgepar); - prevNode = thisNode; - i++; - } -} - -void -graphPath (const System sys, int length) -{ - graphNodePath (sys, length, "style=bold,color=red"); - graphEdgePath (sys, length - 1, "style=bold,color=red"); -} - -//! Scenario for graph; bit of a hack -void -graphScenario (const System sys, const int run, const Roledef rd) -{ - /* Add scenario node */ - printf ("\ts%i [shape=box,height=0.2,label=\"Scenario %i: ", - sys->countScenario, sys->countScenario); - scenarioPrint (sys); - printf ("\"];\n"); - - /* draw edge */ - printf ("\tn%i -> s%i", sys->traceNode[sys->step], sys->countScenario); - printf (" [color=blue,label=\""); - printf ("%i:", sys->runs[run].step); - roledefPrint (rd); - printf ("#%i", run); - printf ("\"];\n"); -} diff --git a/src/output.h b/src/output.h deleted file mode 100644 index 7864492..0000000 --- a/src/output.h +++ /dev/null @@ -1,16 +0,0 @@ -#ifndef OUTPUT -#define OUTPUT - -#include "system.h" - -void tracePrint (const System sys); -void attackDisplay (const System sys); -void graphInit (const System sys); -void graphDone (const System sys); -void graphNode (const System sys); -void graphNodePath (const System sys, const int length, const char *nodepar); -void graphEdgePath (const System sys, const int length, const char *edgepar); -void graphPath (const System sys, int length); -void graphScenario (const System sys, const int run, const Roledef rd); - -#endif diff --git a/src/report.c b/src/report.c deleted file mode 100644 index 0c8a4b1..0000000 --- a/src/report.c +++ /dev/null @@ -1,76 +0,0 @@ -#include -#include -#include "term.h" -#include "system.h" -#include "debug.h" -#include "output.h" -#include "switches.h" - -extern int globalLatex; - -/* reportQuit is called after each violation, because it might need to abort the process */ -void -reportQuit (const System sys) -{ - /* determine quit or not */ - if (switches.prune >= 3) - { - indent (); - printf ("Quitting after %li claims, at the first violated claim.\n", - sys->claims); - sys->maxtracelength = 0; - } -} - -void -reportStart (const System sys) -{ - if (!switches.latex) - { - indent (); - printf ("\n"); - indent (); - } - statesPrint (sys); -} - -void -reportMid (const System sys) -{ - indent (); - printf ("Trace length %i.\n", 1 + sys->step); - if (globalLatex) - printf ("\n"); - tracePrint (sys); -} - - -void -reportEnd (const System sys) -{ - if (!switches.latex) - { - indent (); - printf ("\n"); - } - reportQuit (sys); -} - -void -reportSecrecy (const System sys, Term t) -{ - if (switches.output != ATTACK) - { - reportQuit (sys); - return; - } - reportStart (sys); - indent (); - printf ("Secrecy violation of $"); - termPrint (t); - printf ("$\n"); - if (globalLatex) - printf ("\n"); - reportMid (sys); - reportEnd (sys); -} diff --git a/src/report.h b/src/report.h deleted file mode 100644 index 232ce4c..0000000 --- a/src/report.h +++ /dev/null @@ -1,6 +0,0 @@ -#ifndef REPORT -#define REPORT - -void reportSecrecy (const System sys, Term t); - -#endif diff --git a/src/role.c b/src/role.c index 3bd3c48..f8ba952 100644 --- a/src/role.c +++ b/src/role.c @@ -4,26 +4,22 @@ */ #include #include +#include #include #include "term.h" #include "termlist.h" #include "knowledge.h" #include "system.h" -#include "memory.h" -#include "constraint.h" #include "debug.h" -#include "output.h" -#include "tracebuf.h" #include "role.h" -extern int globalLatex; // from system.c extern int protocolCount; // from system.c //! Allocate memory the size of a roledef struct. Roledef makeRoledef () { - return (Roledef) memAlloc (sizeof (struct roledef)); + return (Roledef) malloc (sizeof (struct roledef)); } //! Print a role event. @@ -71,21 +67,9 @@ roledefPrintGeneric (Roledef rd, int print_actor) label = TermOp2 (label); } - //! Print latex/normal - if (globalLatex) - { - eprintf ("$_{"); - termPrint (label); - eprintf ("}$"); - } - else - { - eprintf ("_"); - termPrint (label); - } + eprintf ("_"); + termPrint (label); } - if (globalLatex) - eprintf ("$"); eprintf ("("); if (!(rd->from == NULL && rd->to == NULL)) { @@ -104,8 +88,6 @@ roledefPrintGeneric (Roledef rd, int print_actor) } termPrint (rd->message); eprintf (" )"); - if (globalLatex) - eprintf ("$"); } //! Print a roledef @@ -166,7 +148,7 @@ roledefDelete (Roledef rd) if (rd == NULL) return; roledefDelete (rd->next); - memFree (rd, sizeof (struct roledef)); + free (rd); return; } @@ -180,7 +162,7 @@ roledefDestroy (Roledef rd) termDelete (rd->from); termDelete (rd->to); termDelete (rd->message); - memFree (rd, sizeof (struct roledef)); + free (rd); return; } @@ -237,7 +219,7 @@ roleCreate (Term name) { Role r; - r = memAlloc (sizeof (struct role)); + r = malloc (sizeof (struct role)); r->nameterm = name; r->roledef = NULL; r->locals = NULL; diff --git a/src/role.h b/src/role.h index 8e3036e..c92d6a3 100644 --- a/src/role.h +++ b/src/role.h @@ -5,7 +5,6 @@ #include "termmap.h" #include "termlist.h" #include "knowledge.h" -#include "constraint.h" #include "states.h" enum eventtype diff --git a/src/scanner.l b/src/scanner.l index 840952f..2f5b6db 100644 --- a/src/scanner.l +++ b/src/scanner.l @@ -122,8 +122,8 @@ Symbol mkstring(char *name) } // make new name len = strlen(name); - s = (char *)memAlloc(len+1); - sl = (Stringlist) memAlloc(sizeof(struct stringlist)); + s = (char *)malloc(len+1); + sl = (Stringlist) malloc(sizeof(struct stringlist)); strncpy(s,name,len); sl->next = allocatedStrings; allocatedStrings = sl; @@ -151,8 +151,8 @@ void strings_cleanup(void) { sl = allocatedStrings; allocatedStrings = sl->next; - memFree(sl->string, strlen(sl->string)+1); - memFree(sl, sizeof(struct stringlist)); + free(sl->string); + free(sl); } } diff --git a/src/switches.c b/src/switches.c index 44a0bd2..546ea6f 100644 --- a/src/switches.c +++ b/src/switches.c @@ -5,18 +5,16 @@ * Contains the main switch handling. */ -#include "string.h" +#include +#include +#include #include "system.h" #include "debug.h" #include "version.h" #include "timer.h" #include "switches.h" #include "error.h" -#include "string.h" #include "specialterm.h" -#include "memory.h" -#include -#include struct switchdata switches; @@ -37,9 +35,7 @@ void switchesInit (int argc, char **argv) { // Methods - switches.engine = ARACHNE_ENGINE; // default is arachne engine switches.match = 0; // default matching - switches.clp = 0; switches.tupling = 0; // Pruning and Bounding @@ -50,20 +46,6 @@ switchesInit (int argc, char **argv) switches.filterClaim = NULL; // default check all claims switches.maxAttacks = 0; // no maximum default - // Modelchecker - switches.traverse = 12; // default traversal method - switches.forceChoose = 1; // force explicit chooses by default - switches.chooseFirst = 0; // no priority to chooses by default - switches.readSymmetries = 0; // don't force read symmetries by default - switches.agentSymmetries = 1; // default enable agent symmetry - switches.orderSymmetries = 0; // don't force symmetry order reduction by default - switches.pruneNomoreClaims = 1; // default cutter when there are no more claims - switches.reduceEndgame = 1; // default cutter of last events in a trace - switches.reduceClaims = 1; // default remove claims from duplicate instance choosers - // Parallellism - switches.scenario = 0; - switches.scenarioSize = 0; - // Arachne switches.heuristic = 3; // default goal selection method switches.maxIntruderActions = INT_MAX; // max number of encrypt/decrypt events @@ -95,9 +77,6 @@ switchesInit (int argc, char **argv) switches.extendTrivial = 0; // default off switches.plain = false; // default colors - // Obsolete - switches.latex = 0; // latex output? - // Process the environment variable SCYTHERFLAGS process_environment (); // Process the command-line switches @@ -147,7 +126,7 @@ openFileStdin (char *filename) nameindex++; } - buffer = (char *) memAlloc (buflen); + buffer = (char *) malloc (buflen); memcpy (buffer, prefix, prefixlen); memcpy (buffer + nameindex, filename, namelen); buffer[buflen - 1] = '\0'; @@ -164,7 +143,7 @@ openFileStdin (char *filename) result = true; } - memFree (buffer, buflen); + free (buffer); return result; } @@ -379,41 +358,6 @@ switcher (const int process, int index, int commandline) /* ================== * Generic options */ - if (detect (' ', "arachne", 0)) - { - if (!process) - { - /* - * Obsolete switch, as it is now the default behaviour. - */ - } - else - { - // Select arachne engine - switches.engine = ARACHNE_ENGINE; - return index; - } - } - - if (detect (' ', "modelchecker", 0)) - { - if (!process) - { - /* - * Discourage - * - helptext (" --modelchecker", - "select Model checking engine [Arachne]"); - */ - } - else - { - // Select arachne engine - switches.engine = POR_ENGINE; - return index; - } - } - if (detect ('d', "dot-output", 0)) { if (!process) @@ -786,19 +730,6 @@ switcher (const int process, int index, int commandline) /* obsolete, worked for modelchecker * - if (detect (' ', "latex", 0)) - { - if (!process) - { - helptext (" --latex", "output attacks in LaTeX format [ASCII]"); - } - else - { - switches.latex = 1; - return index; - } - } - if (detect (' ', "state-space", 0)) { if (!process) @@ -1225,7 +1156,7 @@ process_environment (void) char *argn; /* make a safe copy */ - args = (char *) memAlloc (slen + 1); + args = (char *) malloc (slen + 1); memcpy (args, flags, slen + 1); /* warning */ diff --git a/src/switches.h b/src/switches.h index 748ff96..520cb6e 100644 --- a/src/switches.h +++ b/src/switches.h @@ -15,9 +15,7 @@ struct switchdata char **argv; // Methods - int engine; //!< Engine type (POR_ENGINE,ARACHNE_ENGINE) int match; //!< Matching type. - int clp; //!< Do we use clp? int tupling; //!< Tupling is by default 0: right-associative, optionally 1: left-associative. // Pruning and Bounding @@ -28,20 +26,6 @@ struct switchdata Term filterClaim; //!< Which claim should be checked? int maxAttacks; //!< When not 0, maximum number of attacks - // Modelchecker - int traverse; //!< Traversal method - int forceChoose; //!< Force chooses for each run, even if involved in first read - int chooseFirst; //!< Priority to chooses, implicit and explicit - int readSymmetries; //!< Enable read symmetry reduction - int agentSymmetries; //!< Enable agent symmetry reduction - int orderSymmetries; //!< Enable symmetry order reduction - int pruneNomoreClaims; //!< Enable no more claims cutter - int reduceEndgame; //!< Enable endgame cutter - int reduceClaims; //!< Symmetry reduction on claims (only works when switchAgentSymm is true) - // Parallellism - int scenario; //!< -1 to count, 0 for disable, 1-n to select the choose scenario - int scenarioSize; //!< Scenario size, also called fixed trace prefix length - // Arachne int heuristic; //!< Goal selection method for Arachne engine int maxIntruderActions; //!< Maximum number of intruder actions in the semitrace (encrypt/decrypt) @@ -72,13 +56,6 @@ struct switchdata int extendNonReads; //!< Show further events in arachne xml output. int extendTrivial; //!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension) int plain; //!< Disable color output - - //! Latex output switch. - /** - * Obsolete. Use globalLatex instead. - *\sa globalLatex - */ - int latex; }; extern struct switchdata switches; //!< pointer to switchdata structure diff --git a/src/symbol.c b/src/symbol.c index 08954a1..b4c6b1d 100644 --- a/src/symbol.c +++ b/src/symbol.c @@ -1,11 +1,11 @@ #include #include #include +#include #include #include "symbol.h" #include "debug.h" -#include "memory.h" /* Symbol processor. @@ -59,7 +59,7 @@ symbolsDone (void) { s = symb_alloc; symb_alloc = s->allocnext; - memFree (s, sizeof (struct symbol)); + free (s); } } @@ -79,7 +79,7 @@ get_symb (void) } else { - t = (Symbol) memAlloc (sizeof (struct symbol)); + t = (Symbol) malloc (sizeof (struct symbol)); t->allocnext = symb_alloc; symb_alloc = t; } @@ -225,13 +225,14 @@ symbolNextFree (Symbol prefixsymbol) if (prefixsymbol != NULL) { prefixstr = (char *) prefixsymbol->text; + len = strlen (prefixstr); } else { prefixstr = ""; + len = 0; } - len = strlen (prefixstr); n = 1; while (n <= 9999) { @@ -250,7 +251,7 @@ symbolNextFree (Symbol prefixsymbol) * Thus, some precaution is necessary. * [x][CC] */ - newstring = (char *) memAlloc (slen + 1); + newstring = (char *) malloc (slen + 1); memcpy (newstring, buffer, slen + 1); /* This persistent string can be used to return a fresh symbol */ diff --git a/src/system.c b/src/system.c index 008202e..6a94e75 100644 --- a/src/system.c +++ b/src/system.c @@ -9,11 +9,7 @@ #include "termlist.h" #include "knowledge.h" #include "system.h" -#include "memory.h" -#include "constraint.h" #include "debug.h" -#include "output.h" -#include "tracebuf.h" #include "role.h" #include "mgu.h" #include "switches.h" @@ -21,12 +17,6 @@ #include "depend.h" #include "specialterm.h" -//! Global flag that signals LaTeX output. -/** - * True iff LaTeX output is desired. - */ -int globalLatex; - //! Global count of protocols int protocolCount; @@ -42,7 +32,7 @@ static int indentDepth = 0; Run makeRun () { - return (Run) memAlloc (sizeof (struct run)); + return (Run) malloc (sizeof (struct run)); } @@ -54,12 +44,11 @@ makeRun () System systemInit () { - System sys = (System) memAlloc (sizeof (struct system)); + System sys = (System) malloc (sizeof (struct system)); /* initially, no trace ofcourse */ sys->step = 0; sys->shortestattack = INT_MAX; - sys->attack = tracebufInit (); sys->maxtracelength = INT_MAX; /* init rundefs */ @@ -75,7 +64,6 @@ systemInit () sys->hidden = NULL; sys->secrets = NULL; // list of claimed secrets sys->synchronising_labels = NULL; - sys->attack = NULL; // clash with prev. attack declaration TODO /* no protocols => no protocol preprocessed */ sys->rolecount = 0; sys->roleeventmax = 0; @@ -83,14 +71,7 @@ systemInit () sys->labellist = NULL; sys->attackid = 0; // First attack will have id 1, because the counter is increased before any attacks are displayed. - /* matching CLP */ - sys->constraints = NULL; // no initial constraints - - /* Arachne assist */ - if (switches.engine == ARACHNE_ENGINE) - { - bindingInit (sys); - } + bindingInit (sys); sys->bindings = NULL; sys->current_claim = NULL; @@ -126,23 +107,12 @@ systemReset (const System sys) cl = cl->next; } - sys->knowPhase = 0; // knowledge transition id - termlistDestroy (sys->secrets); // remove old secrets list sys->secrets = NULL; // list of claimed secrets /* transfer switches */ sys->maxtracelength = switches.maxtracelength; - /* POR init */ - sys->PORphase = -1; - sys->PORdone = 1; // mark as 'something done' with previous reads - - /* global latex switch: ugly, but otherwise I must carry it into every - * single subprocedure such as termPrint */ - - globalLatex = switches.latex; - /* propagate mgu_mode */ setMguMode (switches.match); @@ -188,10 +158,10 @@ systemDone (const System sys) /* clear globals, which were defined in systemStart */ s = sys->maxtracelength + 1; - memFree (sys->traceEvent, s * sizeof (Roledef)); - memFree (sys->traceRun, s * sizeof (int)); - memFree (sys->traceKnow, s * sizeof (Knowledge)); - memFree (sys->traceNode, s * sizeof (states_t)); + free (sys->traceEvent); + free (sys->traceRun); + free (sys->traceKnow); + free (sys->traceNode); /* clear roledefs */ while (sys->maxruns > 0) @@ -201,10 +171,7 @@ systemDone (const System sys) /* undo bindings (for arachne) */ - if (switches.engine == ARACHNE_ENGINE) - { - bindingDone (); - } + bindingDone (); /* clear substructures */ termlistDestroy (sys->secrets); @@ -226,8 +193,6 @@ statesPrint (const System sys) { statesFormat (sys->states); eprintf (" states traversed.\n"); - if (globalLatex) - eprintf ("\n"); } //! Destroy a system memory block and system::runs @@ -238,8 +203,8 @@ statesPrint (const System sys) void systemDestroy (const System sys) { - memFree (sys->runs, sys->maxruns * sizeof (struct run)); - memFree (sys, sizeof (struct system)); + free (sys->runs); + free (sys); } //! Ensures that a run can be added to the system. @@ -263,8 +228,7 @@ ensureValidRun (const System sys, int run) /* update size parameter */ oldsize = sys->maxruns; sys->maxruns = run + 1; - sys->runs = - (Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns)); + sys->runs = (Run) realloc (sys->runs, sizeof (struct run) * (sys->maxruns)); /* create runs, set the new pointer(s) to NULL */ for (i = oldsize; i < sys->maxruns; i++) @@ -282,15 +246,7 @@ ensureValidRun (const System sys, int run) myrun.artefacts = NULL; myrun.substitutions = NULL; - if (switches.engine == POR_ENGINE) - { - myrun.know = knowledgeDuplicate (sys->know); - } - else - { - // Arachne etc. - myrun.know = NULL; - } + myrun.know = NULL; myrun.prevSymmRun = -1; myrun.firstNonAgentRead = -1; @@ -366,61 +322,26 @@ not_read_first (const Roledef rdstart, const Term t) Term agentOfRunRole (const System sys, const int run, const Term role) { - if (switches.engine != ARACHNE_ENGINE) + Termlist agents; + + // Agent variables have the same symbol as the role names, so + // we can scan for this. + agents = sys->runs[run].agents; + while (agents != NULL) { - // Non-arachne - Termlist roles; - Termlist agents; + Term agent; - roles = sys->runs[run].protocol->rolenames; - agents = sys->runs[run].agents; - - /* TODO stupid reversed order, lose that soon */ - if (agents != NULL) + agent = agents->term; + if (TermSymb (role) == TermSymb (agent)) { - agents = termlistForward (agents); - while (agents != NULL && roles != NULL) - { - if (isTermEqual (roles->term, role)) - { - return agents->term; - } - agents = agents->prev; - roles = roles->next; - } + return agent; } else { - error - ("Agent list for run %i is empty, so agentOfRunRole is not usable.", - run); + agents = agents->next; } - return NULL; - } - else - { - // Arachne engine - Termlist agents; - - // Agent variables have the same symbol as the role names, so - // we can scan for this. - agents = sys->runs[run].agents; - while (agents != NULL) - { - Term agent; - - agent = agents->term; - if (TermSymb (role) == TermSymb (agent)) - { - return agent; - } - else - { - agents = agents->next; - } - } - return NULL; } + return NULL; } //! Yield the actor agent of a run in the system. @@ -837,148 +758,9 @@ roleInstanceArachne (const System sys, const Protocol protocol, } - -//! Instantiate a role by making a new run for the Modelchecker -/** - * This involves creation of a new run(id). - * Copy & subst of Roledef, Agent knowledge. - * Tolist might contain type constants. -*/ - -void -roleInstanceModelchecker (const System sys, const Protocol protocol, - const Role role, const Termlist paramlist, - Termlist substlist) -{ - int rid; - Run runs; - Roledef rd; - Termlist scanfrom, scanto; - Termlist fromlist = NULL; - Termlist tolist = NULL; - Termlist artefacts = NULL; - Term extterm = NULL; - - /* claim runid, allocate space */ - rid = sys->maxruns; - ensureValidRun (sys, rid); - runs = sys->runs; - - /* duplicate roledef in buffer rd */ - rd = roledefDuplicate (role->roledef); - - /* set parameters */ - /* generic setup */ - runs[rid].protocol = protocol; - runs[rid].role = role; - runs[rid].step = 0; - runs[rid].firstReal = 0; - - /* scan for types in agent list */ - /* scanners */ - // Default engine adheres to scenario - scanfrom = protocol->rolenames; - scanto = paramlist; - while (scanfrom != NULL && scanto != NULL) - { - fromlist = termlistAdd (fromlist, scanfrom->term); - if (scanto->term->stype != NULL && - inTermlist (scanto->term->stype, TERM_Type)) - { - Term newvar; - - /* There is a TYPE constant in the parameter list. - * Generate a new local variable for this run, with this type */ - newvar = makeTermType (VARIABLE, TermSymb (scanfrom->term), rid); - artefacts = termlistAdd (artefacts, newvar); - sys->variables = termlistAdd (sys->variables, newvar); - newvar->stype = termlistAdd (NULL, scanto->term); - tolist = termlistAdd (tolist, newvar); - /* newvar is apparently new, but it might occur - * in the first event if it's a read, in which - * case we forget it */ - if (switches.forceChoose || not_read_first (rd, scanfrom->term)) - { - /* this term is forced as a choose, or it does not occur in the (first) read event */ - if (extterm == NULL) - { - extterm = newvar; - } - else - { - extterm = makeTermTuple (newvar, extterm); - artefacts = termlistAdd (artefacts, extterm); - } - } - } - else - { - /* not a type constant, add to list */ - tolist = termlistAdd (tolist, scanto->term); - } - scanfrom = scanfrom->next; - scanto = scanto->next; - } - - /* set agent list */ - runs[rid].agents = termlistDuplicate (tolist); - - run_prefix_read (sys, rid, rd, extterm); - - /* duplicate all locals form this run */ - scanto = role->locals; - while (scanto != NULL) - { - Term t = scanto->term; - if (!inTermlist (fromlist, t)) - { - Term newt; - - newt = create_new_local (t, rid); - if (newt != NULL) - { - artefacts = termlistAdd (artefacts, newt); - if (realTermVariable (newt)) - { - sys->variables = termlistAdd (sys->variables, newt); - } - fromlist = termlistAdd (fromlist, t); - tolist = termlistAdd (tolist, newt); - } - } - scanto = scanto->next; - } - - /* TODO this is not what we want yet, also local knowledge. The local - * knowledge (list?) also needs to be substituted on invocation. */ - runs[rid].know = knowledgeDuplicate (sys->know); - - /* now adjust the local run copy */ - run_localize (sys, rid, fromlist, tolist, substlist); - - termlistDelete (fromlist); - runs[rid].locals = tolist; - runs[rid].artefacts = artefacts; - - /* erase any substitutions in the role definition, as they are now copied */ - termlistSubstReset (role->variables); - - if (switches.engine == POR_ENGINE) - { - /* Determine symmetric run */ - runs[rid].prevSymmRun = staticRunSymmetry (sys, rid); // symmetry reduction static analysis - - /* Determine first read with variables besides agents */ - runs[rid].firstNonAgentRead = firstNonAgentRead (sys, rid); // symmetry reduction type II - } - - /* length */ - runs[rid].rolelength = roledef_length (runs[rid].start); -} - //! Instantiate a role by making a new run /** - * Generic splitter. Splits into the arachne version, or the modelchecker version. + * Just forwards to Arachne version. * * This involves creation of a new run(id). * Copy & subst of Roledef, Agent knowledge. @@ -988,14 +770,7 @@ void roleInstance (const System sys, const Protocol protocol, const Role role, const Termlist paramlist, Termlist substlist) { - if (switches.engine == ARACHNE_ENGINE) - { - roleInstanceArachne (sys, protocol, role, paramlist, substlist); - } - else - { - roleInstanceModelchecker (sys, protocol, role, paramlist, substlist); - } + roleInstanceArachne (sys, protocol, role, paramlist, substlist); } //! Destroy roleInstance @@ -1015,10 +790,7 @@ roleInstanceDestroy (const System sys) myrun = sys->runs[runid]; // Reset graph - if (switches.engine == ARACHNE_ENGINE) - { - dependPopRun (); - } + dependPopRun (); // Destroy roledef roledefDestroy (myrun.start); @@ -1056,16 +828,13 @@ roleInstanceDestroy (const System sys) * Arachne does real-time reduction of memory, POR does not * Artefact removal can only be done if knowledge sets are empty, as with Arachne */ - if (switches.engine == ARACHNE_ENGINE) + Termlist artefacts; + // Remove artefacts + artefacts = myrun.artefacts; + while (artefacts != NULL) { - Termlist artefacts; - // Remove artefacts - artefacts = myrun.artefacts; - while (artefacts != NULL) - { - memFree (artefacts->term, sizeof (struct term)); - artefacts = artefacts->next; - } + free (artefacts->term); + artefacts = artefacts->next; } /** @@ -1096,7 +865,7 @@ roleInstanceDestroy (const System sys) // Reduce run count sys->maxruns = sys->maxruns - 1; sys->runs = - (Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns)); + (Run) realloc (sys->runs, sizeof (struct run) * (sys->maxruns)); } } @@ -1132,10 +901,10 @@ systemStart (const System sys) s = sys->maxtracelength + 1; /* freed in systemDone */ - sys->traceEvent = memAlloc (s * sizeof (Roledef)); - sys->traceRun = memAlloc (s * sizeof (int)); - sys->traceKnow = memAlloc (s * sizeof (Knowledge)); - sys->traceNode = memAlloc (s * sizeof (states_t)); + sys->traceEvent = malloc (s * sizeof (Roledef)); + sys->traceRun = malloc (s * sizeof (int)); + sys->traceKnow = malloc (s * sizeof (Knowledge)); + sys->traceNode = malloc (s * sizeof (states_t)); /* clear, for niceties */ for (i = 0; i < s; i++) @@ -1182,7 +951,7 @@ protocolCreate (Term name) { Protocol p; - p = memAlloc (sizeof (struct protocol)); + p = malloc (sizeof (struct protocol)); p->nameterm = name; p->roles = NULL; p->rolenames = NULL; @@ -1358,35 +1127,6 @@ violatedClaimPrint (const System sys, const int i) eprintf ("Claim stuk"); } -//! Yield the real length of an attack. -/** - * AttackLength yields the real (user friendly) length of an attack by omitting - * the redundant events but also the choose events. - */ - -int -attackLength (struct tracebuf *tb) -{ - int len, i; - - len = 0; - i = 0; - while (i < tb->length) - { - if (tb->status[i] != S_RED) - { - /* apparently not redundant */ - if (!(tb->event[i]->type == READ && tb->event[i]->internal)) - { - /* and no internal read, so it counts */ - len++; - } - } - i++; - } - return len; -} - void commandlinePrint (FILE * stream) { diff --git a/src/system.h b/src/system.h index eeeb491..068e1be 100644 --- a/src/system.h +++ b/src/system.h @@ -5,7 +5,6 @@ #include "termmap.h" #include "termlist.h" #include "knowledge.h" -#include "constraint.h" #include "states.h" #include "role.h" #include "list.h" @@ -73,34 +72,6 @@ struct varbuf //! Shorthand for varbuf pointer. typedef struct varbuf *Varbuf; -//! Trace buffer. -struct tracebuf -{ - //! Length of trace. - int length; - //! Length of trace minus the redundant events. - int reallength; - //! Array of events. - Roledef *event; - //! Array of run identifiers for each event. - int *run; - //! Array of status flags for each event. - /** - *\sa S_OKE, S_RED, S_TOD, S_UNK - */ - int *status; - //! Array for matching sends to reads. - int *link; - //! Index of violated claim in trace. - int violatedclaim; - //! Array of knowledge sets for each event. - Knowledge *know; - //! List of terms required to be in the final knowledge. - Termlist requiredterms; - //! List of variables in the system. - Varbuf variables; -}; - //! Structure for information on special terms (cacheing) struct hiddenterm { @@ -166,18 +137,9 @@ struct system Knowledge *traceKnow; //!< Trace intruder knowledge: Maxruns * maxRoledef states_t *traceNode; //!< Trace node traversal: Maxruns * maxRoledef - /* POR reduction assistance */ - int PORphase; //!< -1: init (all sends), 0...: recurse reads - int PORdone; //!< Simple bit to denote something was done. - int knowPhase; //!< Which knowPhase have we already explored? - Constraintlist constraints; //!< Only needed for CLP match - /* Arachne assistance */ List bindings; //!< List of bindings Claimlist current_claim; //!< The claim under current investigation - - //! Shortest attack storage. - struct tracebuf *attack; }; typedef struct system *System; @@ -212,7 +174,6 @@ int untrustedAgent (const System sys, Termlist agents); int getMaxTraceLength (const System sys); void agentsOfRunPrint (const System sys, const int run); void violatedClaimPrint (const System sys, int i); -int attackLength (struct tracebuf *tb); void commandlinePrint (FILE * stream); int compute_rolecount (const System sys); diff --git a/src/tac.c b/src/tac.c index c04d42b..62cb3c9 100644 --- a/src/tac.c +++ b/src/tac.c @@ -27,7 +27,7 @@ tacDone (void) tf = ts; ts = ts->allnext; - memFree (tf, sizeof (struct tacnode)); + free (tf); } } @@ -37,7 +37,7 @@ tacCreate (int op) { /* maybe even store in scrapping list, so we could delete them * all later */ - Tac t = memAlloc (sizeof (struct tacnode)); + Tac t = malloc (sizeof (struct tacnode)); t->allnext = allocatedTacs; allocatedTacs = t; t->lineno = yylineno; diff --git a/src/term.c b/src/term.c index ba2c317..4f827fa 100644 --- a/src/term.c +++ b/src/term.c @@ -10,13 +10,12 @@ * pointer comparison, which is what we want. */ -#include #include #include #include +#include #include "term.h" #include "debug.h" -#include "memory.h" #include "ctype.h" #include "specialterm.h" @@ -26,7 +25,6 @@ int rolelocal_variable; /* external definitions */ extern int inTermlist (); // suppresses a warning, but at what cost? -extern int globalLatex; /* forward declarations */ @@ -63,7 +61,7 @@ termsDone (void) Term makeTerm () { - return (Term) memAlloc (sizeof (struct term)); + return (Term) malloc (sizeof (struct term)); } //! Create a fresh encrypted term from two existing terms. @@ -335,17 +333,11 @@ termPrint (Term term) eprintf ("V"); if (TermRunid (term) >= 0) { - if (globalLatex && globalError == 0) - eprintf ("\\sharp%i", TermRunid (term)); - else - eprintf ("#%i", TermRunid (term)); + eprintf ("#%i", TermRunid (term)); } if (term->subst != NULL) { - if (globalLatex) - eprintf ("\\rightarrow"); - else - eprintf ("->"); + eprintf ("->"); termPrint (term->subst); } } @@ -370,21 +362,10 @@ termPrint (Term term) else { /* normal encryption */ - if (globalLatex) - { - eprintf ("\\{"); - termTuplePrint (TermOp (term)); - eprintf ("\\}_{"); - termPrint (TermKey (term)); - eprintf ("}"); - } - else - { - eprintf ("{"); - termTuplePrint (TermOp (term)); - eprintf ("}"); - termPrint (TermKey (term)); - } + eprintf ("{"); + termTuplePrint (TermOp (term)); + eprintf ("}"); + termPrint (TermKey (term)); } } } @@ -432,7 +413,7 @@ termDuplicate (const Term term) if (realTermLeaf (term)) return term; - newterm = (Term) memAlloc (sizeof (struct term)); + newterm = (Term) malloc (sizeof (struct term)); memcpy (newterm, term, sizeof (struct term)); if (realTermEncrypt (term)) { @@ -464,7 +445,7 @@ termNodeDuplicate (const Term term) if (realTermLeaf (term)) return term; - newterm = (Term) memAlloc (sizeof (struct term)); + newterm = (Term) malloc (sizeof (struct term)); memcpy (newterm, term, sizeof (struct term)); return newterm; } @@ -485,7 +466,7 @@ termDuplicateDeep (const Term term) if (term == NULL) return NULL; - newterm = (Term) memAlloc (sizeof (struct term)); + newterm = (Term) malloc (sizeof (struct term)); memcpy (newterm, term, sizeof (struct term)); if (!realTermLeaf (term)) { @@ -519,7 +500,7 @@ termDuplicateUV (Term term) if (realTermLeaf (term)) return term; - newterm = (Term) memAlloc (sizeof (struct term)); + newterm = (Term) malloc (sizeof (struct term)); memcpy (newterm, term, sizeof (struct term)); if (realTermEncrypt (term)) { @@ -543,7 +524,7 @@ realTermDuplicate (const Term term) if (term == NULL) return NULL; - newterm = (Term) memAlloc (sizeof (struct term)); + newterm = (Term) malloc (sizeof (struct term)); if (realTermLeaf (term)) { memcpy (newterm, term, sizeof (struct term)); @@ -587,7 +568,7 @@ termDelete (const Term term) termDelete (TermOp1 (term)); termDelete (TermOp2 (term)); } - memFree (term, sizeof (struct term)); + free (term); } } diff --git a/src/termlist.c b/src/termlist.c index 6699fec..7812a20 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -3,7 +3,6 @@ #include "termlist.h" #include "specialterm.h" #include "debug.h" -#include "memory.h" /* * Shared stuff @@ -45,7 +44,7 @@ Termlist makeTermlist () { /* inline candidate */ - return (Termlist) memAlloc (sizeof (struct termlist)); + return (Termlist) malloc (sizeof (struct termlist)); } //! Duplicate a termlist. @@ -113,7 +112,7 @@ termlistDelete (Termlist tl) } #endif termlistDelete (tl->next); - memFree (tl, sizeof (struct termlist)); + free (tl); } @@ -129,7 +128,7 @@ termlistDestroy (Termlist tl) return; termlistDestroy (tl->next); termDelete (tl->term); - memFree (tl, sizeof (struct termlist)); + free (tl); } //! Determine whether a term is an element of a termlist. @@ -345,7 +344,7 @@ termlistDelTerm (Termlist tl) } if (tl->next != NULL) (tl->next)->prev = tl->prev; - memFree (tl, sizeof (struct termlist)); + free (tl); return newhead; } diff --git a/src/termmap.c b/src/termmap.c index d5ca93e..17897a7 100644 --- a/src/termmap.c +++ b/src/termmap.c @@ -2,7 +2,6 @@ #include #include "termmap.h" #include "debug.h" -#include "memory.h" //! Open termmaps code. void @@ -26,7 +25,7 @@ Termmap makeTermmap (void) { /* inline candidate */ - return (Termmap) memAlloc (sizeof (struct termmap)); + return (Termmap) malloc (sizeof (struct termmap)); } //! Get function result @@ -102,7 +101,7 @@ termmapDelete (const Termmap f) if (f != NULL) { termmapDelete (f->next); - memFree (f, sizeof (struct termmap)); + free (f); } } diff --git a/src/tracebuf.c b/src/tracebuf.c deleted file mode 100644 index f3ad697..0000000 --- a/src/tracebuf.c +++ /dev/null @@ -1,202 +0,0 @@ -/* - * tracebuf.c - * - * trace buffer operations - */ - -#include -#include -#include "system.h" -#include "memory.h" -#include "tracebuf.h" -#include "varbuf.h" - -/* reconstruct the knowledge sequence, -1 if it can be done, event nr of last depending read otherwise. - * There is one exception: if it returns tb->length, the required terms are not in the last knowledge - */ - -int -tracebufRebuildKnow (struct tracebuf *tb) -{ - Knowledge k; - Roledef rd; - int i; - int flag; - Termlist tl; - - if (tb == NULL || tb->length == 0) - { - /* stupid, but true */ - return -1; - } - - flag = -1; - k = knowledgeDuplicate (tb->know[0]); - i = 0; - while (i < tb->length) - { - rd = tb->event[i]; - if (tb->status[i] != S_RED) - { - /* simulate execution of the event */ - switch (rd->type) - { - case READ: - if (!inKnowledge (k, rd->message)) - { - flag = i; - } - break; - case SEND: - knowledgeAddTerm (k, rd->message); - break; - case CLAIM: - /* TODO parse term requirements ? */ - /* Probably not needed */ - break; - default: - /* Anything else */ - break; - } - } - /* write the new knowledge, overwriting old stuff */ - knowledgeDelete (tb->know[i + 1]); - tb->know[i + 1] = knowledgeDuplicate (k); - - i++; - } - tl = tb->requiredterms; - while (tl != NULL) - { - if (!inKnowledge (k, tl->term)) - { - flag = tb->length; - } - tl = tl->next; - } - knowledgeDelete (k); - return flag; -} - -/* - * traceBufInit - * - * initializes the trace buffer. - */ - -struct tracebuf * -tracebufInit (void) -{ - struct tracebuf *tb = - (struct tracebuf *) memAlloc (sizeof (struct tracebuf)); - tb->length = 0; - tb->reallength = 0; - tb->event = NULL; - tb->know = NULL; - tb->run = NULL; - tb->status = NULL; - tb->link = NULL; - tb->requiredterms = NULL; - tb->violatedclaim = 0; - tb->variables = NULL; - return tb; -} - -void -tracebufDone (struct tracebuf *tb) -{ - Roledef rd; - - if (tb == NULL) - { - return; - } - - varbufDone (tb->variables); - if (tb->length > 0) - { - int i; - - i = 0; - /* note: knowledge domain is length+1 */ - knowledgeDelete (tb->know[0]); - while (i < tb->length) - { - rd = tb->event[i]; - termDelete (rd->from); - termDelete (rd->to); - termDelete (rd->message); - roledefDelete (rd); - knowledgeDelete (tb->know[i + 1]); - i++; - } - - memFree (tb->know, (i + 1) * sizeof (struct knowledge *)); - memFree (tb->event, i * sizeof (struct roledef *)); - memFree (tb->run, i * sizeof (int)); - memFree (tb->status, i * sizeof (int)); - memFree (tb->link, i * sizeof (int)); - } - memFree (tb, sizeof (tracebuf)); -} - -struct tracebuf * -tracebufSet (const System sys, int length, int claimev) -{ - struct tracebuf *tb; - int i; - Roledef rd; - - /* TODO For the constraint logic approach, we would simply insert - * any constant from the constraint for a variable. - */ - - tb = tracebufInit (); - if (length == 0) - { - return tb; - } - tb->length = length; - tb->reallength = length; - tb->variables = (Varbuf) varbufInit (sys); - tb->event = (Roledef *) memAlloc (length * sizeof (struct roledef *)); - tb->status = (int *) memAlloc (length * sizeof (int)); - tb->link = (int *) memAlloc (length * sizeof (int)); - tb->run = (int *) memAlloc (length * sizeof (int)); - tb->know = - (Knowledge *) memAlloc ((length + 1) * sizeof (struct knowledge *)); - - /* when duplicating the knowledge, we want to instantiate the variables as well - */ - - tb->know[0] = knowledgeSubstDo (sys->traceKnow[0]); - - i = 0; - while (i < length) - { - rd = roledefDuplicate1 (sys->traceEvent[i]); - if (rd == NULL) - { - printf ("Empty event in trace at %i of %i?\n", i, length); - exit (1); - } - - /* make a copy without variables */ - rd->to = termDuplicateUV (rd->to); - rd->from = termDuplicateUV (rd->from); - rd->message = termDuplicateUV (rd->message); - - tb->event[i] = rd; - tb->link[i] = -1; - tb->status[i] = S_UNK; - tb->run[i] = sys->traceRun[i]; - tb->know[i + 1] = NULL; - i++; - } - - /* mark claim */ - tb->violatedclaim = claimev; - tb->status[claimev] = S_OKE; - tracebufRebuildKnow (tb); - return tb; -} diff --git a/src/tracebuf.h b/src/tracebuf.h deleted file mode 100644 index a057076..0000000 --- a/src/tracebuf.h +++ /dev/null @@ -1,29 +0,0 @@ -#ifndef TRACEBUF -#define TRACEBUF - -#include "term.h" -#include "termlist.h" -#include "knowledge.h" -#include "system.h" - -/* STATUS symbols */ -enum statussymbols -{ - S_UNK, // UNKnown : unprocessed. - S_OKE, // OKE : done, but required for the attack. - S_RED, // REDundant : is not needed for attack, we're sure. - S_TOD // TODo : The previous suggestion REQ was too similar to RED. This is reserved for reads. -}; - - -/* - * tracebuf struct is defined in system.h to avoid loops. - */ - -int tracebufRebuildKnow (struct tracebuf *tb); -struct tracebuf *tracebufInit (void); -void tracebufDone (struct tracebuf *tb); -struct tracebuf *tracebufSet (const System sys, int length, int claimev); - - -#endif diff --git a/src/varbuf.c b/src/varbuf.c deleted file mode 100644 index ee8fa0c..0000000 --- a/src/varbuf.c +++ /dev/null @@ -1,92 +0,0 @@ -/* - * varbuf.c - * - * Operations on a variable substitutions buffer. - * The type is actually defined in system.h - */ - -#include "memory.h" -#include "system.h" - -/* - * create a new varbuffer from the current state of the system - */ - -Varbuf -varbufInit (const System sys) -{ - Varbuf vb; - Termlist tl; - Term termfrom, termto; - - vb = (Varbuf) memAlloc (sizeof (struct varbuf)); - vb->from = NULL; - vb->to = NULL; - vb->empty = NULL; - tl = sys->variables; - while (tl != NULL) - { - if (realTermVariable (tl->term)) - { - /* this is actually a variable */ - if (tl->term->subst == NULL) - { - /* non-instantiated */ - vb->empty = termlistAdd (vb->empty, tl->term); - } - else - { - /* store instantiation */ - termfrom = tl->term; - termto = termfrom->subst; - termfrom->subst = NULL; // temp disable - vb->from = termlistAdd (vb->from, termfrom); - vb->to = termlistAdd (vb->to, termto); - termfrom->subst = termto; // restore - } - } - tl = tl->next; - } - return vb; -} - -/* - * copy the variable state back into the system - */ - -void -varbufSet (const System sys, Varbuf vb) -{ - Termlist tl1, tl2; - - tl1 = vb->from; - tl2 = vb->to; - while (tl1 != NULL && tl2 != NULL) - { - tl1->term->subst = tl2->term; - tl1 = tl1->next; - tl2 = tl2->next; - } - tl1 = vb->empty; - while (tl1 != NULL) - { - tl1->term->subst = NULL; - tl1 = tl1->next; - } -} - -/* - * cleanup - */ - -void -varbufDone (Varbuf vb) -{ - if (vb != NULL) - { - termlistDelete (vb->from); - termlistDelete (vb->to); - termlistDelete (vb->empty); - memFree (vb, sizeof (struct varbuf)); - } -} diff --git a/src/varbuf.h b/src/varbuf.h deleted file mode 100644 index 9467e82..0000000 --- a/src/varbuf.h +++ /dev/null @@ -1,10 +0,0 @@ -#ifndef VARBUF -#define VARBUF - -#include "system.h" - -Varbuf varbufInit (const System sys); -void varbufSet (const System sys, Varbuf vb); -void varbufDone (Varbuf vb); - -#endif