From 1bdaf7b5d9e0cf9516253c002a2437ad74579bd1 Mon Sep 17 00:00:00 2001 From: ccremers Date: Tue, 7 Jun 2005 15:02:27 +0000 Subject: [PATCH] - Large rewrite of switch code. Instead of having switch parameters in the (monstrously large) system structure, there is now a global 'switchdata' structure originating in switches.c. This makes it much easier to see what's happening. * Note: although this code has been tested, there might be some hiccups, because doing multiple search&replace actions over all files is bound to cause some problems. --- src/arachne.c | 138 ++++++++++++++++++++++---------------------- src/binding.c | 4 +- src/compiler.c | 7 ++- src/main-switches.c | 122 +++++++++++++++++++-------------------- src/main.c | 56 +++++++++--------- src/match_basic.c | 5 +- src/match_clp.c | 3 +- src/mgu.c | 4 +- src/modelchecker.c | 67 ++++++++++----------- src/output.c | 11 ++-- src/report.c | 9 +-- src/switches.c | 118 +++++++++++++++++++++++++++++-------- src/switches.h | 64 +++++++++++++++++++- src/system.c | 64 +++++++------------- src/system.h | 45 +-------------- src/type.c | 3 +- src/xmlout.c | 5 +- 17 files changed, 400 insertions(+), 325 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 8fc058a..bca2c86 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -31,6 +31,7 @@ #include "warshall.h" #include "timer.h" #include "type.h" +#include "switches.h" extern Term CLAIM_Secret; extern Term CLAIM_Nisynch; @@ -170,7 +171,7 @@ arachneDone () void indentPrefixPrint (const int annotate, const int jumps) { - if (sys->output == ATTACK && globalError == 0) + if (switches.output == ATTACK && globalError == 0) { // Arachne, attack, not an error // We assume that means DOT output @@ -409,7 +410,7 @@ add_read_goals (const int run, const int old, const int new) { if (rd->type == READ) { - if (sys->output == PROOF) + if (switches.output == PROOF) { if (count == 0) { @@ -427,7 +428,7 @@ add_read_goals (const int run, const int old, const int new) rd = rd->next; i++; } - if ((count > 0) && sys->output == PROOF) + if ((count > 0) && switches.output == PROOF) { eprintf ("\n"); } @@ -522,7 +523,7 @@ role_name_print (const int run) void proof_suppose_run (const int run, const int oldlength, const int newlength) { - if (sys->output == PROOF) + if (switches.output == PROOF) { int reallength; @@ -553,7 +554,7 @@ proof_suppose_run (const int run, const int oldlength, const int newlength) void proof_select_goal (Binding b) { - if (sys->output == PROOF) + if (switches.output == PROOF) { Roledef rd; @@ -573,7 +574,7 @@ proof_select_goal (Binding b) void proof_cannot_bind (const Binding b, const int run, const int index) { - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf @@ -586,7 +587,7 @@ proof_cannot_bind (const Binding b, const int run, const int index) void proof_suppose_binding (Binding b) { - if (sys->output == PROOF) + if (switches.output == PROOF) { Roledef rd; @@ -785,7 +786,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index) printf ("\n"); } #endif - if (cryptlist != NULL && sys->output == PROOF) + if (cryptlist != NULL && switches.output == PROOF) { indentPrint (); eprintf @@ -925,7 +926,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index) flag = termMguSubTerm (b->term, rd->message, subterm_iterate, sys->know->inverses, NULL); // Did it work? - if (found == 0 && sys->output == PROOF) + if (found == 0 && switches.output == PROOF) { indentPrint (); eprintf ("Cannot bind "); @@ -954,7 +955,7 @@ bind_existing_run (const Binding b, const Protocol p, const Role r, if (sys->runs[run].protocol == p && sys->runs[run].role == r) { found++; - if (sys->output == PROOF) + if (switches.output == PROOF) { if (found == 1) { @@ -973,7 +974,7 @@ bind_existing_run (const Binding b, const Protocol p, const Role r, indentDepth--; } } - if (sys->output == PROOF && found == 0) + if (switches.output == PROOF && found == 0) { indentPrint (); eprintf ("There is no existing run for "); @@ -2033,10 +2034,10 @@ select_goal () int mode; // mode bits local storage - mode = sys->switchGoalSelectMethod; + mode = switches.arachneSelector; // Find the most constrained goal - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Listing open goals that might be chosen: "); @@ -2103,7 +2104,7 @@ select_goal () buf_constrain = 0; buf_weight = 0; - if (sys->output == PROOF && best != NULL) + if (switches.output == PROOF && best != NULL) eprintf (", "); // We will shift this mode variable @@ -2129,10 +2130,10 @@ select_goal () { min_constrain = buf_constrain; best = b; - if (sys->output == PROOF) + if (switches.output == PROOF) eprintf ("*"); } - if (sys->output == PROOF) + if (switches.output == PROOF) { termPrint (b->term); if (mode & 2) @@ -2145,7 +2146,7 @@ select_goal () } bl = bl->next; } - if (sys->output == PROOF) + if (switches.output == PROOF) { if (best == NULL) eprintf ("none"); @@ -2219,7 +2220,7 @@ bind_goal_new_m0 (const Binding b) { found++; proof_suppose_binding (b); - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("* I.e. retrieving "); @@ -2245,7 +2246,7 @@ bind_goal_new_m0 (const Binding b) tl = tl->next; } - if (found == 0 && sys->output == PROOF) + if (found == 0 && switches.output == PROOF) { indentPrint (); eprintf ("Term "); @@ -2302,7 +2303,7 @@ bind_goal_new_encrypt (const Binding b) rd->next->next->message = termDuplicateUV (term); index = 2; proof_suppose_run (run, 0, index + 1); - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("* Encrypting "); @@ -2334,7 +2335,7 @@ bind_goal_new_encrypt (const Binding b) if (!can_be_encrypted) { - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Term "); @@ -2357,7 +2358,7 @@ bind_goal_new_intruder_run (const Binding b) { int flag; - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Can we bind "); @@ -2419,7 +2420,7 @@ bind_goal_regular_run (const Binding b) // A good candidate found++; - if (sys->output == PROOF && found == 1) + if (switches.output == PROOF && found == 1) { indentPrint (); eprintf ("The term ", found); @@ -2427,7 +2428,7 @@ bind_goal_regular_run (const Binding b) eprintf (" matches patterns from the role definitions. Investigate.\n"); } - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("%i. It matches the pattern ", found); @@ -2458,7 +2459,7 @@ bind_goal_regular_run (const Binding b) // Bind to all possible sends of regular runs found = 0; flag = iterate_role_sends (bind_this_role_send); - if (sys->output == PROOF && found == 0) + if (switches.output == PROOF && found == 0) { indentPrint (); eprintf ("The term "); @@ -2493,7 +2494,7 @@ bind_goal_old_intruder_run (Binding b) if (rd->type == SEND) { found++; - if (sys->output == PROOF && found == 1) + if (switches.output == PROOF && found == 1) { indentPrint (); eprintf @@ -2508,7 +2509,7 @@ bind_goal_old_intruder_run (Binding b) } } } - if (sys->output == PROOF && found == 0) + if (switches.output == PROOF && found == 0) { indentPrint (); eprintf ("No existing intruder runs to match to.\n"); @@ -2538,7 +2539,7 @@ bind_goal (const Binding b) // if (1 == 0) if (bind_old_goal (b)) { - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Goal for term "); @@ -2567,7 +2568,7 @@ bind_goal (const Binding b) if (!inKnowledge (sys->know, function)) { // Prune because we didn't know it before, and it is never subterm-sent - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("* Because "); @@ -2582,7 +2583,7 @@ bind_goal (const Binding b) // Keylevel lemmas: improves on the previous one if (!isPossiblySent (b->term)) { - if (sys->output == PROOF) + if (switches.output == PROOF) { eprintf ("Rejecting a term as a regular bind because key levels are off: "); @@ -2654,7 +2655,7 @@ prune_theorems () // Check all types of the local agents according to the matching type if (!checkTypeLocals (sys)) { - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf @@ -2695,7 +2696,7 @@ prune_theorems () } else { // real leaf - if (sys->match == 0 || !isTermVariable (agent)) + if (switches.match == 0 || !isTermVariable (agent)) { // either strict matching, or not a variable, so we should check matching types if (agent->stype == NULL) { // Too generic @@ -2713,7 +2714,7 @@ prune_theorems () if (!sensibleagent) { - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Pruned because the agent "); @@ -2738,7 +2739,7 @@ prune_theorems () agent = deVar (tl->term); if (!realTermVariable (agent) && inTermlist (sys->untrusted, agent)) { - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf @@ -2770,7 +2771,7 @@ prune_theorems () } if (inTermlist (sys->untrusted, actor)) { - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf @@ -2805,7 +2806,7 @@ prune_theorems () { if (!bindings_c_minimal ()) { - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Pruned because this is not <=c-minimal.\n"); @@ -2828,7 +2829,7 @@ prune_theorems () if (termInTerm (b->term, TERM_Hidden)) { // Prune the state: we can never meet this - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Pruned because intruder can never construnct "); @@ -2840,12 +2841,12 @@ prune_theorems () // Check for encryption levels /* - * if (sys->match < 2 + * if (switches.match < 2 */ if (term_encryption_level (b->term) > max_encryption_level) { // Prune: we do not need to construct such terms - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Pruned because the encryption level of "); @@ -2863,7 +2864,7 @@ prune_theorems () if (!inKnowledge (sys->know, b->term)) { // Not in initial knowledge of the intruder - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Pruned because the function "); @@ -2894,7 +2895,7 @@ prune_bounds () if (passed_time_limit ()) { // Oh no, we ran out of time! - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Pruned: ran out of allowed time (-T %i switch)\n", @@ -2906,20 +2907,20 @@ prune_bounds () } /* prune for proof depth */ - if (proofDepth > sys->switch_maxproofdepth) + if (proofDepth > switches.maxproofdepth) { // Hardcoded limit on proof tree depth - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Pruned: proof tree too deep: %i (-d %i switch)\n", - proofDepth, sys->switch_maxproofdepth); + proofDepth, switches.maxproofdepth); } return 1; } /* prune for trace length */ - if (sys->switch_maxtracelength < INT_MAX) + if (switches.maxtracelength < INT_MAX) { int tracelength; int run; @@ -2937,23 +2938,23 @@ prune_bounds () run++; } /* test */ - if (tracelength > sys->switch_maxtracelength) + if (tracelength > switches.maxtracelength) { // Hardcoded limit on proof tree depth - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Pruned: trace too long: %i (-l %i switch)\n", - tracelength, sys->switch_maxtracelength); + tracelength, switches.maxtracelength); } return 1; } } - if (num_regular_runs > sys->switchRuns) + if (num_regular_runs > switches.runs) { // Hardcoded limit on runs - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Pruned: too many regular runs (%i).\n", num_regular_runs); @@ -2963,12 +2964,12 @@ prune_bounds () // This needs some foundation. Probably * 2^max_encryption_level //!@todo Fix this bound - if ((sys->match < 2) + if ((switches.match < 2) && (num_intruder_runs > - ((double) sys->switchRuns * max_encryption_level * 8))) + ((double) switches.runs * max_encryption_level * 8))) { // Hardcoded limit on iterations - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf @@ -2979,9 +2980,9 @@ prune_bounds () } // Limit on exceeding any attack length - if (sys->prune == 2 && get_semitrace_length () >= attack_length) + if (switches.prune == 2 && get_semitrace_length () >= attack_length) { - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf @@ -3010,7 +3011,7 @@ prune_claim_specifics () { sys->current_claim->count = statesIncrease (sys->current_claim->count); - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf @@ -3025,7 +3026,7 @@ prune_claim_specifics () { sys->current_claim->count = statesIncrease (sys->current_claim->count); - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf @@ -3045,7 +3046,7 @@ add_claim_specifics (const Claimlist cl, const Roledef rd) /** * Secrecy claim */ - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("* To verify the secrecy claim, we add the term "); @@ -3093,15 +3094,15 @@ property_check () * By the way the claim is handled, this automatically means a flaw. */ count_false (); - if (sys->output == ATTACK) + if (switches.output == ATTACK) { - if (sys->switchXMLoutput) + if (switches.xml) { xmlOutSemitrace (sys); } else { - if (sys->latex == 1) + if (switches.latex == 1) { latexSemiState (); } @@ -3117,7 +3118,7 @@ property_check () { // Shortest attack attack_length = attack_this; - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("New shortest attack found with trace length %i.\n", @@ -3157,7 +3158,7 @@ iterate () count = goal_add (b->term, b->run_to, b->ev_to, b->level); // Show this in output - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Expanding tuple goal "); @@ -3193,7 +3194,7 @@ iterate () /* * all goals bound, check for property */ - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("All goals are now bound.\n"); @@ -3275,7 +3276,7 @@ arachne () * set up claim role(s) */ - if (sys->switchRuns == 0) + if (switches.runs == 0) { // No real checking. return; @@ -3311,8 +3312,7 @@ arachne () Protocol p; Role r; - if (sys->switchClaimToCheck == NULL - || sys->switchClaimToCheck == cl->type) + if (switches.filterClaim == NULL || switches.filterClaim == cl->type) { int run; @@ -3322,7 +3322,7 @@ arachne () p = (Protocol) cl->protocol; r = (Role) cl->role; - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Testing Claim "); @@ -3365,7 +3365,7 @@ arachne () //! Indent back indentDepth--; - if (sys->output == PROOF) + if (switches.output == PROOF) { indentPrint (); eprintf ("Proof complete for this claim.\n"); diff --git a/src/binding.c b/src/binding.c index 366397b..e9f4f85 100644 --- a/src/binding.c +++ b/src/binding.c @@ -13,6 +13,7 @@ #include "term.h" #include "termmap.h" #include "arachne.h" +#include "switches.h" #include static System sys; @@ -295,7 +296,8 @@ goal_graph_create () else { // It doesn't occur first in a READ, which shouldn't be happening - if (sys->output == + if (switches. + output == PROOF) { eprintf diff --git a/src/compiler.c b/src/compiler.c index 1e9a153..90474b3 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -10,6 +10,7 @@ #include "symbol.h" #include "substitution.h" #include "compiler.h" +#include "switches.h" /* Simple sys pointer as a global. Yields cleaner code although it's against programming standards. @@ -481,7 +482,7 @@ commEvent (int event, Tac tc) torole = claim; /* check for ignored claim types */ - if (sys->switchClaimToCheck != NULL && sys->switchClaimToCheck != claim) + if (switches.filterClaim != NULL && switches.filterClaim != claim) { /* abort the construction of the node */ return; @@ -796,7 +797,7 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles) Term rolename; Role r; - if (sys->engine == ARACHNE_ENGINE) + if (switches.engine == ARACHNE_ENGINE) { rolename = levelVar (tcroles->t1.sym); rolename->stype = termlistAdd (NULL, TERM_Agent); @@ -1426,7 +1427,7 @@ compute_prec_sets (const System sys) #ifdef DEBUG // Porparam = 100 (weirdness) [x][cc][debug] can turn of the synchronising label sets (override). - if (sys->porparam == 100) + if (switches.switchP == 100) { termlistDelete (sys->synchronising_labels); sys->synchronising_labels = NULL; diff --git a/src/main-switches.c b/src/main-switches.c index acebb29..952969f 100644 --- a/src/main-switches.c +++ b/src/main-switches.c @@ -363,15 +363,15 @@ main (int argc, char **argv) sys = systemInit (); if (switch_arachne->count > 0) { - sys->engine = ARACHNE_ENGINE; + switches.engine = ARACHNE_ENGINE; bindingInit (sys); } /* init compiler for this system */ compilerInit (sys); /* transfer command line */ - sys->argc = argc; - sys->argv = argv; + switches.argc = argc; + switches.argv = argv; if (switch_echo->count > 0) { @@ -383,64 +383,64 @@ main (int argc, char **argv) /* handle switches */ - sys->switchRuns = switch_maximum_runs->ival[0]; /* maximum number of runs */ + switches.runs = switch_maximum_runs->ival[0]; /* maximum number of runs */ if (switch_implicit_choose->count > 0) /* allow implicit chooses */ - sys->switchForceChoose = 0; + switches.forceChoose = 0; if (switch_choose_first->count > 0) - sys->switchChooseFirst = 1; /* priority to chooses */ + switches.chooseFirst = 1; /* priority to chooses */ if (switch_enable_read_symmetries->count > 0) { if (switch_enable_symmetry_order->count > 0) error ("--read-symm and --symm-order cannot be used at the same time."); - sys->switchReadSymm = 1; + switches.readSymmetries = 1; } if (switch_enable_symmetry_order->count > 0) - sys->switchSymmOrder = 1; /* enable symmetry order */ + switches.orderSymmetries = 1; /* enable symmetry order */ if (switch_disable_agent_symmetries->count > 0) - sys->switchAgentSymm = 0; /* disable agent symmetry order */ + switches.agentSymmetries = 0; /* disable agent symmetry order */ if (switch_disable_noclaims_reductions->count > 0) - sys->switchNomoreClaims = 0; /* disable no more claims cutter */ + switches.pruneNomoreClaims = 0; /* disable no more claims cutter */ if (switch_disable_endgame_reductions->count > 0) - sys->switchReduceEndgame = 0; /* disable endgame cutter */ + switches.reduceEndgame = 0; /* disable endgame cutter */ if (switch_disable_claim_symmetry->count > 0) - sys->switchReduceClaims = 0; /* disable claim symmetry cutter */ + switches.reduceClaims = 0; /* disable claim symmetry cutter */ if (switch_summary->count > 0) - sys->output = SUMMARY; /* report summary on stdout */ + switches.output = SUMMARY; /* report summary on stdout */ if (switch_proof->count > 0) - sys->output = PROOF; /* report proof on stdout (for arachne only) */ + switches.output = PROOF; /* report proof on stdout (for arachne only) */ /* * The scenario selector has an important side effect; when it is non-null, * any scenario traversing selects chooses first. */ - sys->switchScenario = switch_scenario->ival[0]; /* scenario selector */ - sys->switchScenarioSize = switch_scenario_size->ival[0]; /* scenario size */ - if (sys->switchScenario == 0 && sys->switchScenarioSize > 0) + switches.scenario = switch_scenario->ival[0]; /* scenario selector */ + switches.scenarioSize = switch_scenario_size->ival[0]; /* scenario size */ + if (switches.scenario == 0 && switches.scenarioSize > 0) { /* no scenario, but a size is set. so override */ #ifdef DEBUG warning ("Scanning scenarios."); #endif - sys->switchScenario = -1; + switches.scenario = -1; } - if (sys->switchScenario < 0) + if (switches.scenario < 0) { - sys->output = SCENARIOS; + switches.output = SCENARIOS; } - if (sys->switchScenario != 0 && sys->switchScenarioSize == 0) + if (switches.scenario != 0 && switches.scenarioSize == 0) { #ifdef DEBUG warning ("Scenario selection without trace prefix length implies --choose-first."); #endif - sys->switchChooseFirst = 1; + switches.chooseFirst = 1; } #ifdef DEBUG - sys->porparam = switch_por_parameter->ival[0]; + switches.switchP = switch_por_parameter->ival[0]; #endif - sys->latex = switch_latex_output->count; + switches.latex = switch_latex_output->count; sys->know = emptyKnowledge (); @@ -463,7 +463,7 @@ main (int argc, char **argv) if (claim == NULL) error ("Unknown claim type to check."); if (inTermlist (claim->stype, TERM_Claim)) - sys->switchClaimToCheck = claim; + switches.filterClaim = claim; else error ("Claim type to check is not a claim."); } @@ -478,7 +478,7 @@ main (int argc, char **argv) /* compile */ - if (sys->engine != ARACHNE_ENGINE) + if (switches.engine != ARACHNE_ENGINE) { // Compile as many runs as possible compile (spdltac, switch_maximum_runs->ival[0]); @@ -518,42 +518,42 @@ main (int argc, char **argv) /* add parameters to system */ - sys->clp = (switch_clp->count > 0 ? 1 : 0); + switches.clp = (switch_clp->count > 0 ? 1 : 0); - sys->traverse = switch_traversal_method->ival[0]; - sys->match = switch_match_method->ival[0]; - mgu_match = sys->match; - sys->prune = switch_pruning_method->ival[0]; + switches.traverse = switch_traversal_method->ival[0]; + switches.match = switch_match_method->ival[0]; + mgu_match = switches.match; + switches.prune = switch_pruning_method->ival[0]; time_limit_seconds = switch_timer->ival[0]; set_time_limit (switch_timer->ival[0]); if (switch_progress_bar->count > 0) /* enable progress display */ - sys->switchS = 50000; + switches.reportStates = 50000; else /* disable progress display */ - sys->switchS = 0; + switches.reportStates = 0; if (switch_state_space_graph->count > 0) { /* enable state space graph output */ - sys->output = STATESPACE; //!< New method + switches.output = STATESPACE; //!< New method } if (switch_empty->count > 0) - sys->output = EMPTY; + switches.output = EMPTY; if (switch_prune_proof_depth->ival[0] >= 0) - sys->switch_maxproofdepth = switch_prune_proof_depth->ival[0]; + switches.maxproofdepth = switch_prune_proof_depth->ival[0]; if (switch_prune_trace_length->ival[0] >= 0) - sys->switch_maxtracelength = switch_prune_trace_length->ival[0]; + switches.maxtracelength = switch_prune_trace_length->ival[0]; if (switch_goal_select_method->ival[0] >= 0) - sys->switchGoalSelectMethod = switch_goal_select_method->ival[0]; + switches.arachneSelector = switch_goal_select_method->ival[0]; #ifdef DEBUG /* in debugging mode, some extra switches */ if (switch_debug_indent->count > 0) indentActivate (); if (DEBUGL (1)) - printf ("Using traversal method %i.\n", sys->traverse); + printf ("Using traversal method %i.\n", switches.traverse); #else /* non-debug defaults */ - sys->switchM = 0; + switches.reportMemory = 0; #endif /* @@ -563,7 +563,7 @@ main (int argc, char **argv) */ /* Latex only makes sense for attacks */ - if (sys->latex && sys->output != ATTACK) + if (switches.latex && switches.output != ATTACK) { error ("Scyther can only generate LaTeX output for attacks."); } @@ -571,7 +571,7 @@ main (int argc, char **argv) if (switch_incremental_runs->count > 0 || switch_incremental_trace_length->count > 0) { - if (sys->output != ATTACK && sys->output != EMPTY) + if (switches.output != ATTACK && switches.output != EMPTY) { error ("Incremental traversal only for empty or attack output."); } @@ -579,11 +579,11 @@ main (int argc, char **argv) #ifdef DEBUG if (DEBUGL (4)) { - warning ("Selected output method is %i", sys->output); + warning ("Selected output method is %i", switches.output); } #endif - if (sys->engine == ARACHNE_ENGINE) + if (switches.engine == ARACHNE_ENGINE) { arachneInit (sys); } @@ -594,7 +594,7 @@ main (int argc, char **argv) */ /* latex header? */ - if (sys->latex) + if (switches.latex) latexInit (sys, argc, argv); /* model check system */ @@ -628,7 +628,7 @@ main (int argc, char **argv) if (sys->attack != NULL && sys->attack->length != 0) { - if (sys->output == ATTACK) + if (switches.output == ATTACK) { attackDisplay (sys); } @@ -654,12 +654,12 @@ main (int argc, char **argv) } /* latex closeup */ - if (sys->latex) + if (switches.latex) latexDone (sys); /* Transfer any scenario counting to the exit code, * assuming that there is no error. */ - if (exitcode != EXIT_ERROR && sys->switchScenario < 0) + if (exitcode != EXIT_ERROR && switches.scenario < 0) { exitcode = sys->countScenario; } @@ -668,7 +668,7 @@ main (int argc, char **argv) * Now we clean up any memory that was allocated. */ - if (sys->engine == ARACHNE_ENGINE) + if (switches.engine == ARACHNE_ENGINE) { arachneDone (); bindingDone (); @@ -710,7 +710,7 @@ timersPrint (const System sys) // #define NOTIMERS /* display stats */ - if (sys->output != SUMMARY) + if (switches.output != SUMMARY) { globalError++; } @@ -723,7 +723,7 @@ timersPrint (const System sys) /* scenario info */ - if (sys->switchScenario > 0) + if (switches.scenario > 0) { eprintf ("scen_st\t"); statesFormat (sys->statesScenario); @@ -845,7 +845,7 @@ timersPrint (const System sys) } /* reset globalError */ - if (sys->output != SUMMARY) + if (switches.output != SUMMARY) { globalError--; } @@ -885,7 +885,7 @@ MC_incRuns (const System sys) * the whole space, then we just continue. However, if * we're looking to prune, ``the buck stops here''. */ - if (sys->prune != 0) + if (switches.prune != 0) { flag = 0; } @@ -942,7 +942,7 @@ MC_incTraces (const System sys) * the whole space, then we just continue. However, if * we're looking to prune, ``the buck stops here''. */ - if (sys->prune != 0) + if (switches.prune != 0) { flag = 0; } @@ -980,13 +980,13 @@ MC_single (const System sys) int modelCheck (const System sys) { - if (sys->output == STATESPACE) + if (switches.output == STATESPACE) { graphInit (sys); } /* modelcheck the system */ - switch (sys->engine) + switch (switches.engine) { case POR_ENGINE: traverse (sys); @@ -995,25 +995,25 @@ modelCheck (const System sys) arachne (); break; default: - error ("Unknown engine type %i.", sys->engine); + error ("Unknown engine type %i.", switches.engine); } /* clean up any states display */ - if (sys->switchS > 0) + if (switches.reportStates > 0) { // States: 1.000e+06 fprintf (stderr, " \r"); } timersPrint (sys); - if (sys->output == STATESPACE) + if (switches.output == STATESPACE) { graphDone (sys); } - if (sys->switchScenario > 0) + if (switches.scenario > 0) { /* Traversing a scenario. Maybe we ran out. */ - if (sys->switchScenario > sys->countScenario) + if (switches.scenario > sys->countScenario) { /* Signal as error */ exit (1); diff --git a/src/main.c b/src/main.c index 92d3962..0c938cf 100644 --- a/src/main.c +++ b/src/main.c @@ -100,11 +100,11 @@ main (int argc, char **argv) * ------------------------------------------------ */ - sys = systemInit (); - sys->argc = argc; - sys->argv = argv; + /* process any command-line switches */ + switchesInit (argc, argv); - process_switches (sys); + /* start system */ + sys = systemInit (); /* init compiler for this system */ compilerInit (sys); @@ -122,10 +122,10 @@ main (int argc, char **argv) /* compile */ - if (sys->engine != ARACHNE_ENGINE) + if (switches.engine != ARACHNE_ENGINE) { // Compile as many runs as possible - compile (spdltac, sys->switchRuns); + compile (spdltac, switches.runs); } else { @@ -170,18 +170,18 @@ main (int argc, char **argv) */ /* Latex only makes sense for attacks */ - if (sys->latex && sys->output != ATTACK) + if (switches.latex && switches.output != ATTACK) { error ("Scyther can only generate LaTeX output for attacks."); } #ifdef DEBUG if (DEBUGL (4)) { - warning ("Selected output method is %i", sys->output); + warning ("Selected output method is %i", switches.output); } #endif - if (sys->engine == ARACHNE_ENGINE) + if (switches.engine == ARACHNE_ENGINE) { arachneInit (sys); } @@ -192,11 +192,11 @@ main (int argc, char **argv) */ /* xml init */ - if (sys->switchXMLoutput) + if (switches.xml) xmlOutInit (); /* latex header? */ - if (sys->latex) + if (switches.latex) latexInit (sys, argc, argv); /* model check system */ @@ -216,7 +216,7 @@ main (int argc, char **argv) if (sys->attack != NULL && sys->attack->length != 0) { - if (sys->output == ATTACK) + if (switches.output == ATTACK) { attackDisplay (sys); } @@ -242,16 +242,16 @@ main (int argc, char **argv) } /* latex closeup */ - if (sys->latex) + if (switches.latex) latexDone (sys); /* xml closeup */ - if (sys->switchXMLoutput) + if (switches.xml) xmlOutDone (); /* Transfer any scenario counting to the exit code, * assuming that there is no error. */ - if (exitcode != EXIT_ERROR && sys->switchScenario < 0) + if (exitcode != EXIT_ERROR && switches.scenario < 0) { exitcode = sys->countScenario; } @@ -260,7 +260,7 @@ main (int argc, char **argv) * Now we clean up any memory that was allocated. */ - if (sys->engine == ARACHNE_ENGINE) + if (switches.engine == ARACHNE_ENGINE) { arachneDone (); bindingDone (); @@ -299,7 +299,7 @@ timersPrint (const System sys) // #define NOTIMERS /* display stats */ - if (sys->output != SUMMARY) + if (switches.output != SUMMARY) { globalError++; } @@ -312,7 +312,7 @@ timersPrint (const System sys) /* scenario info */ - if (sys->switchScenario > 0) + if (switches.scenario > 0) { eprintf ("scen_st\t"); statesFormat (sys->statesScenario); @@ -434,7 +434,7 @@ timersPrint (const System sys) } /* reset globalError */ - if (sys->output != SUMMARY) + if (switches.output != SUMMARY) { globalError--; } @@ -474,7 +474,7 @@ MC_incRuns (const System sys) * the whole space, then we just continue. However, if * we're looking to prune, ``the buck stops here''. */ - if (sys->prune != 0) + if (switches.prune != 0) { flag = 0; } @@ -531,7 +531,7 @@ MC_incTraces (const System sys) * the whole space, then we just continue. However, if * we're looking to prune, ``the buck stops here''. */ - if (sys->prune != 0) + if (switches.prune != 0) { flag = 0; } @@ -569,13 +569,13 @@ MC_single (const System sys) int modelCheck (const System sys) { - if (sys->output == STATESPACE) + if (switches.output == STATESPACE) { graphInit (sys); } /* modelcheck the system */ - switch (sys->engine) + switch (switches.engine) { case POR_ENGINE: if (sys->maxruns > 0) @@ -587,25 +587,25 @@ modelCheck (const System sys) arachne (); break; default: - error ("Unknown engine type %i.", sys->engine); + error ("Unknown engine type %i.", switches.engine); } /* clean up any states display */ - if (sys->switchS > 0) + if (switches.reportStates > 0) { // States: 1.000e+06 fprintf (stderr, " \r"); } timersPrint (sys); - if (sys->output == STATESPACE) + if (switches.output == STATESPACE) { graphDone (sys); } - if (sys->switchScenario > 0) + if (switches.scenario > 0) { /* Traversing a scenario. Maybe we ran out. */ - if (sys->switchScenario > sys->countScenario) + if (switches.scenario > sys->countScenario) { /* Signal as error */ exit (1); diff --git a/src/match_basic.c b/src/match_basic.c index 47a0dd9..af79bc5 100644 --- a/src/match_basic.c +++ b/src/match_basic.c @@ -12,6 +12,7 @@ #include "system.h" #include "modelchecker.h" #include "match_basic.h" +#include "switches.h" //! Get the candidates list for typeless basic stuff __inline__ Termlist @@ -132,7 +133,7 @@ fixVariablelist (const struct fvpass fp, const Knowledge know, { /* substitute */ varlist->term->subst = tlscan->term; - if (validSubst (fp.sys->match, varlist->term)) + if (validSubst (switches.match, varlist->term)) { #ifdef DEBUG if (DEBUGL (5)) @@ -191,7 +192,7 @@ matchRead_basic (const System sys, const int run, /* remove variable linkages */ newterm = termDuplicateUV (fp.roledef->message); /* a candidate, but if this is a t4 traversal, is it also an old one? */ - if (fp.sys->traverse < 4 || + if (switches.traverse < 4 || fp.roledef->forbidden == NULL || enabled_basic (fp.sys, fp.roledef->forbidden, newterm)) { diff --git a/src/match_clp.c b/src/match_clp.c index 7f38db8..d1502b7 100644 --- a/src/match_clp.c +++ b/src/match_clp.c @@ -18,6 +18,7 @@ #include "debug.h" #include "match_clp.h" #include "modelchecker.h" +#include "switches.h" struct solvepass { @@ -94,7 +95,7 @@ solve (const struct solvepass sp, Constraintlist solvecons) tlscan = tlres; while (tlscan != NULL && tlres != MGUFAIL) { - if (validSubst (sp.sys->match, tlscan->term)) + if (validSubst (switches.match, tlscan->term)) { tlscan = tlscan->next; } diff --git a/src/mgu.c b/src/mgu.c index 46691b1..2641c1a 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -17,7 +17,7 @@ //! Internal constant. If true, typed checking /** - * Analoguous to sys->match + * Analoguous to switches.match * 0 typed * 1 basic typeflaws * 2 all typeflaws @@ -26,7 +26,7 @@ static int mgu_match = 0; extern Term TERM_Hidden; -//! Set mgu mode (basically sys->match) +//! Set mgu mode (basically switches.match) void setMguMode (const int match) { diff --git a/src/modelchecker.c b/src/modelchecker.c index 5c21d58..f674188 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -20,6 +20,7 @@ #include "tracebuf.h" #include "attackminimize.h" #include "claim.h" +#include "switches.h" /* @@ -107,14 +108,14 @@ int traverse (const System sys) { /* maybe chooses have precedence over _all_ methods */ - if (sys->switchChooseFirst) + if (switches.chooseFirst) { if (traverse_chooses_first (sys)) return 1; } /* branch for traversal methods */ - switch (sys->traverse) + switch (switches.traverse) { case 1: return traverseSimple (sys); @@ -125,7 +126,7 @@ traverse (const System sys) case 5: case 6: case 7: - error ("%i is an obsolete traversal method.", sys->traverse); + error ("%i is an obsolete traversal method.", switches.traverse); case 8: return traversePOR4 (sys); case 9: @@ -137,7 +138,7 @@ traverse (const System sys) case 12: return traversePOR8 (sys); default: - error ("%i is NOT an existing traversal method.", sys->traverse); + error ("%i is NOT an existing traversal method.", switches.traverse); } } @@ -203,18 +204,18 @@ executeStep (const System sys, const int run) sys->states = statesIncrease (sys->states); /* what about scenario exploration? */ - if (sys->switchScenario && sys->step + 1 > sys->switchScenarioSize) + if (switches.scenario && sys->step + 1 > switches.scenarioSize) { /* count states within scenario */ sys->statesScenario = statesIncrease (sys->statesScenario); } /* show progression */ - if (sys->switchS > 0) + if (switches.reportStates > 0) { sys->interval = statesIncrease (sys->interval); if (!statesSmallerThan - (sys->interval, (unsigned long int) sys->switchS)) + (sys->interval, (unsigned long int) switches.reportStates)) { globalError++; sys->interval = STATES0; @@ -228,7 +229,7 @@ executeStep (const System sys, const int run) /* 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 (sys->output == STATESPACE + if (switches.output == STATESPACE && statesSmallerThan (sys->states, MAX_GRAPH_STATES)) { /* display graph */ @@ -375,7 +376,7 @@ explorify (const System sys, const int run) * further traversal. */ //!@todo This implementation relies on the fact that there are only secrecy, synchr and agreement properties. - if (sys->switchNomoreClaims && sys->secrets == NULL) + if (switches.pruneNomoreClaims && sys->secrets == NULL) { /* there are no remaining secrecy claims to be checked */ Roledef rdscan; int validclaim; @@ -416,7 +417,7 @@ explorify (const System sys, const int run) * If the run we depend upon has already been activated (otherwise warn!) check for instance ordering */ - if (sys->switchAgentSymm && sys->runs[run].prevSymmRun != -1) + if (switches.agentSymmetries && sys->runs[run].prevSymmRun != -1) { /* there is such a run on which we depend */ int ridSymm; @@ -442,7 +443,7 @@ explorify (const System sys, const int run) /* we only explore the other half */ return 0; } - if (order == 0 && sys->switchReduceClaims) + 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 */ @@ -454,7 +455,7 @@ explorify (const System sys, const int run) /* Special check 3: if after choosing, this run is untrusted and ends on (read|skippedclaim)*, we can remove that part already. */ - if (sys->switchReduceEndgame && roleCap == NULL) + 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, @@ -479,7 +480,7 @@ explorify (const System sys, const int run) * Special check b1: symmetry reduction part II on similar read events for equal roles. */ - if (sys->switchReadSymm) + if (switches.readSymmetries) { if (sys->runs[run].firstNonAgentRead == myStep) { @@ -539,7 +540,7 @@ explorify (const System sys, const int run) * Depends on prevSymm, skipping chooses even. */ - if (sys->switchSymmOrder && myStep == sys->runs[run].firstReal) + if (switches.orderSymmetries && myStep == sys->runs[run].firstReal) { if (sys->runs[run].prevSymmRun != -1) { @@ -571,10 +572,10 @@ explorify (const System sys, const int run) * Note: any choose selection after this would result in empty scenarios, so this * should be the last special check. */ - if (sys->switchScenario != 0) + if (switches.scenario != 0) { /* two variants. If scenario size is 0, we operate on the old method involving chooses */ - if (sys->switchScenarioSize == 0) + if (switches.scenarioSize == 0) { /* only after chooses */ if (myStep == 0 && rd->type == READ) @@ -588,18 +589,18 @@ explorify (const System sys, const int run) sys->countScenario++; } /* If we are displaying scenarios, print it */ - if (sys->output == SCENARIOS) + if (switches.output == SCENARIOS) { printf ("%i\t", sys->countScenario); scenarioPrint (sys); printf ("\n"); } /* If it is not the selected one, abort */ - if (sys->switchScenario != sys->countScenario) + if (switches.scenario != sys->countScenario) { /* this branch is not interesting */ /* unfortunately, it is also not drawn in the state graph because of this */ - if (sys->output == STATESPACE) + if (switches.output == STATESPACE) { graphScenario (sys, run, rd); } @@ -614,20 +615,20 @@ explorify (const System sys, const int run) /* 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 == sys->switchScenarioSize) + if (sys->step + 1 == switches.scenarioSize) { /* Now, the prefix has been set. Count it */ if (sys->countScenario < INT_MAX) { sys->countScenario++; } - if (sys->output == SCENARIOS) + if (switches.output == SCENARIOS) { /* apparently we want the output */ int index; eprintf ("%i\t", sys->countScenario); index = 0; - while (index < sys->switchScenarioSize) + while (index < switches.scenarioSize) { roledefPrint (sys->traceEvent[index]); eprintf ("#%i; ", sys->traceRun[index]); @@ -636,10 +637,10 @@ explorify (const System sys, const int run) eprintf ("\n"); } /* Is this the selected one? */ - if (sys->switchScenario != sys->countScenario) + if (switches.scenario != sys->countScenario) { /* unfortunately, it is also not drawn in the state graph because of this */ - if (sys->output == STATESPACE) + if (switches.output == STATESPACE) { graphScenario (sys, run, rd); } @@ -796,7 +797,7 @@ tryChoiceSend (const System sys, const int run, const Roledef rd) /* It will possibly be unblocked by a corresponding read event, * the actual code would be in explorify, post instantiation of the read event. */ - if (sys->clp) + if (switches.clp) { block_clp (sys, run); } @@ -837,7 +838,7 @@ tryChoiceRead (const System sys, const int run, const Roledef rd) int stackKnowPhase = rd->knowPhase; rd->knowPhase = sys->knowPhase; - if (sys->clp) + if (switches.clp) { block_clp (sys, run); } @@ -913,8 +914,8 @@ lastActiveRun (const System sys) { /* there was a previous action, start scan from there */ #ifdef DEBUG - if (sys->porparam < 100) - return sys->traceRun[sys->step - 1] + sys->porparam; + if (switches.switchP < 100) + return sys->traceRun[sys->step - 1] + switches.switchP; #endif return sys->traceRun[sys->step - 1]; } @@ -1113,7 +1114,7 @@ propertyCheck (const System sys) int isTermSecret (const System sys, const Term t) { - switch (sys->clp) + switch (switches.clp) { case 0: /* test for simple inclusion */ @@ -1245,7 +1246,7 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt) 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 (sys->output == STATESPACE) + if (switches.output == STATESPACE) { graphPath (sys, length); } @@ -1260,7 +1261,7 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt) /* maybe there is some new pruning going on */ flag = 0; - switch (sys->prune) + switch (switches.prune) { case 0: flag = 1; @@ -1310,14 +1311,14 @@ executeTry (const System sys, int run) #endif if (runPoint->type == READ) { - if (sys->clp) + if (switches.clp) return matchRead_clp (sys, run, explorify); else return matchRead_basic (sys, run, explorify); } if (runPoint->type == SEND) { - if (sys->clp) + if (switches.clp) flag = send_clp (sys, run); else flag = send_basic (sys, run); diff --git a/src/output.c b/src/output.c index 0a0954d..45003b4 100644 --- a/src/output.c +++ b/src/output.c @@ -10,6 +10,7 @@ #include #include "system.h" #include "latex.h" +#include "switches.h" void @@ -220,7 +221,7 @@ tracePrint (const System sys) printf ("\n"); } - if (sys->latex) + if (switches.latex) { //latexTracePrint(sys); return; @@ -331,7 +332,7 @@ tracePrint (const System sys) printf ("\n"); } - switch (sys->clp) + switch (switches.clp) { case 1: indent (); @@ -481,7 +482,7 @@ attackDisplayAscii (const System sys) void attackDisplay (const System sys) { - if (sys->latex) + if (switches.latex) { attackDisplayLatex (sys); } @@ -507,7 +508,7 @@ graphInit (const System sys) /* label */ printf ("\tcomment = \"$"); - commandlinePrint (stdout, sys); + commandlinePrint (stdout); printf ("\";\n"); /* fit stuff onto the page */ @@ -579,7 +580,7 @@ graphNode (const System sys) else { /* no added knowledge */ - if (sys->switchScenario != 0 && + if (switches.scenario != 0 && rd != NULL && rd == sys->runs[run].start && rd->type == READ && run == sys->lastChooseRun) diff --git a/src/report.c b/src/report.c index de701d8..0c8a4b1 100644 --- a/src/report.c +++ b/src/report.c @@ -4,6 +4,7 @@ #include "system.h" #include "debug.h" #include "output.h" +#include "switches.h" extern int globalLatex; @@ -12,7 +13,7 @@ void reportQuit (const System sys) { /* determine quit or not */ - if (sys->prune >= 3) + if (switches.prune >= 3) { indent (); printf ("Quitting after %li claims, at the first violated claim.\n", @@ -24,7 +25,7 @@ reportQuit (const System sys) void reportStart (const System sys) { - if (!sys->latex) + if (!switches.latex) { indent (); printf ("\n"); @@ -47,7 +48,7 @@ reportMid (const System sys) void reportEnd (const System sys) { - if (!sys->latex) + if (!switches.latex) { indent (); printf ("\n"); @@ -58,7 +59,7 @@ reportEnd (const System sys) void reportSecrecy (const System sys, Term t) { - if (sys->output != ATTACK) + if (switches.output != ATTACK) { reportQuit (sys); return; diff --git a/src/switches.c b/src/switches.c index 79c02e3..fbbefac 100644 --- a/src/switches.c +++ b/src/switches.c @@ -10,8 +10,10 @@ #include "debug.h" #include "version.h" #include "timer.h" +#include "switches.h" +#include -extern System sys; +struct switchdata switches; extern struct tacnode *spdltac; extern Term TERM_Claim; @@ -19,6 +21,73 @@ extern Term TERM_Claim; const char *progname = "scyther"; const char *releasetag = SVNVERSION; +// Forward declarations +void process_switches (); + +//! Init switches +/** + * Set them all to the default settings. + */ +void +switchesInit (int argc, char **argv) +{ + // Command-line + switches.argc = argc; + switches.argv = argv; + + // Methods + switches.engine = POR_ENGINE; // default is partial ordering engine + switches.match = 0; // default matching + switches.clp = 0; + + // Pruning and Bounding + switches.prune = 2; // default pruning method + switches.maxproofdepth = INT_MAX; + switches.maxtracelength = INT_MAX; + switches.runs = INT_MAX; + switches.filterClaim = NULL; // default check all claims + + // 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.arachneSelector = 3; // default goal selection method + + // Misc + switches.switchP = 0; // multi-purpose parameter + + // Output + switches.output = ATTACK; // default is to show the attacks + switches.report = 0; + switches.reportClaims = 0; // default don't report on claims + switches.xml = 0; // default no xml output + switches.human = false; // not human friendly by default + switches.reportMemory; + switches.reportTime; + switches.reportStates; + // Obsolete + switches.latex = 0; // latex output? + + process_switches (); +} + +//! Exit +void +switchesDone (void) +{ +} + //! Process a single switch or generate help text /** * When process is false, we just generate the help text. @@ -29,7 +98,7 @@ const char *releasetag = SVNVERSION; * The index steps through 1..argc-1. */ int -switcher (const int process, const System sys, int index) +switcher (const int process, int index) { char *this_arg; // just a shortcut int this_arg_length; // same here @@ -166,8 +235,8 @@ switcher (const int process, const System sys, int index) if (process) { - argc = sys->argc; - argv = sys->argv; + argc = switches.argc; + argv = switches.argv; #ifdef DEBUG // Check range for debug; we trust the non-debug version :) if (index < 1 || index >= argc) @@ -203,8 +272,7 @@ switcher (const int process, const System sys, int index) else { // Select arachne engine - sys->engine = ARACHNE_ENGINE; - bindingInit (sys); + switches.engine = ARACHNE_ENGINE; return index; } } @@ -217,7 +285,7 @@ switcher (const int process, const System sys, int index) } else { - sys->switchXMLoutput = 1; + switches.xml = 1; return index; } } @@ -230,7 +298,7 @@ switcher (const int process, const System sys, int index) } else { - sys->match = integer_argument (); + switches.match = integer_argument (); return index; } } @@ -259,7 +327,7 @@ switcher (const int process, const System sys, int index) } else { - sys->switchRuns = integer_argument (); + switches.runs = integer_argument (); return index; } } @@ -273,7 +341,7 @@ switcher (const int process, const System sys, int index) } else { - sys->switch_maxtracelength = integer_argument (); + switches.maxtracelength = integer_argument (); return index; } } @@ -288,7 +356,7 @@ switcher (const int process, const System sys, int index) } else { - sys->prune = integer_argument (); + switches.prune = integer_argument (); return index; } } @@ -302,7 +370,7 @@ switcher (const int process, const System sys, int index) } else { - sys->switchHuman = true; + switches.human = true; return index; } } @@ -323,7 +391,7 @@ switcher (const int process, const System sys, int index) } else { - sys->latex = 1; + switches.latex = 1; return index; } } @@ -337,7 +405,7 @@ switcher (const int process, const System sys, int index) } else { - sys->output = STATESPACE; + switches.output = STATESPACE; return index; } } @@ -362,7 +430,7 @@ switcher (const int process, const System sys, int index) } else { - sys->switchGoalSelectMethod = integer_argument (); + switches.arachneSelector = integer_argument (); return index; } } @@ -376,7 +444,7 @@ switcher (const int process, const System sys, int index) else { // Proof - sys->output = PROOF; + switches.output = PROOF; return index; } } @@ -399,7 +467,7 @@ switcher (const int process, const System sys, int index) { /* print command line */ fprintf (stdout, "command\t"); - commandlinePrint (stdout, sys); + commandlinePrint (stdout); fprintf (stdout, "\n"); return index; } @@ -413,7 +481,7 @@ switcher (const int process, const System sys, int index) } else { - sys->output = SUMMARY; + switches.output = SUMMARY; return index; } } @@ -428,7 +496,7 @@ switcher (const int process, const System sys, int index) } else { - sys->switchS = 50000; + switches.reportStates = 50000; return index; } } @@ -443,7 +511,7 @@ switcher (const int process, const System sys, int index) } else { - sys->output = EMPTY; + switches.output = EMPTY; return index; } } @@ -480,7 +548,7 @@ switcher (const int process, const System sys, int index) { printf ("Usage:\n"); printf (" %s [switches] [FILE]\nSwitches:\n", progname); - switcher (0, NULL, 0); + switcher (0, 0); exit (0); } } @@ -557,11 +625,11 @@ switcher (const int process, const System sys, int index) //! Process switches void -process_switches (const System sys) +process_switches () { int index; - if (sys->argc == 1) + if (switches.argc == 1) { printf ("Try '%s --help' for more information, or visit:\n", progname); printf (" http://www.win.tue.nl/~ccremers/scyther/index.html\n"); @@ -569,8 +637,8 @@ process_switches (const System sys) } index = 1; - while (index < sys->argc && index > 0) + while (index < switches.argc && index > 0) { - index = switcher (1, sys, index); + index = switcher (1, index); } } diff --git a/src/switches.h b/src/switches.h index 8adca3d..76402c1 100644 --- a/src/switches.h +++ b/src/switches.h @@ -1,6 +1,68 @@ #ifndef SWITCHES #define SWITCHES -void process_switches (const System sys); +#include "term.h" +#include "system.h" + +void switchesInit (); +void switchesDone (); + +//! Command-line switches structure +struct switchdata +{ + // Command-line + int argc; + char **argv; + + // Methods + int engine; //!< Engine type (POR_ENGINE,ARACHNE_ENGINE) + int match; //!< Matching type. + int clp; //!< Do we use clp? + + // Pruning and Bounding + int prune; //!< Type of pruning. + int maxproofdepth; //!< Maximum proof depth + int maxtracelength; //!< Maximum trace length allowed + int runs; //!< The number of runs as in the switch + Term filterClaim; //!< Which claim should be checked? + + // 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 arachneSelector; //!< Goal selection method for Arachne engine + + // Misc + int switchP; //!< A multi-purpose integer parameter, passed to the partial order reduction method selected. + + // Output + int output; //!< From enum outputs: what should be produced. Default ATTACK. + int report; + int reportClaims; //!< Enable claims report + int xml; //!< xml output + int human; //!< human readable + int reportMemory; //!< Memory display switch. + int reportTime; //!< Time display switch. + int reportStates; //!< Progress display switch. (traversed states) + //! Latex output switch. + /** + * Obsolete. Use globalLatex instead. + *\sa globalLatex + */ + int latex; +}; + +extern struct switchdata switches; #endif diff --git a/src/system.c b/src/system.c index 40f8c7e..62da118 100644 --- a/src/system.c +++ b/src/system.c @@ -16,6 +16,8 @@ #include "tracebuf.h" #include "role.h" #include "mgu.h" +#include "switches.h" +#include "binding.h" /* from compiler.o */ extern Term TERM_Type; @@ -57,32 +59,6 @@ systemInit () sys->step = 0; sys->shortestattack = INT_MAX; sys->attack = tracebufInit (); - - /* switches */ - sys->engine = POR_ENGINE; // default is partial ordering engine - sys->output = ATTACK; // default is to show the attacks - sys->porparam = 0; // multi-purpose parameter - sys->latex = 0; // latex output? - sys->switchRuns = INT_MAX; - sys->switchScenario = 0; - sys->switchScenarioSize = 0; - sys->switchForceChoose = 1; // force explicit chooses by default - sys->switchChooseFirst = 0; // no priority to chooses by default - sys->switchReadSymm = 0; // don't force read symmetries by default - sys->switchAgentSymm = 1; // default enable agent symmetry - sys->switchSymmOrder = 0; // don't force symmetry order reduction by default - sys->switchNomoreClaims = 1; // default cutter when there are no more claims - sys->switchReduceEndgame = 1; // default cutter of last events in a trace - sys->switchReduceClaims = 1; // default remove claims from duplicate instance choosers - sys->switchClaims = 0; // default don't report on claims - sys->switchClaimToCheck = NULL; // default check all claims - sys->switchXMLoutput = 0; // default no xml output - sys->switchHuman = false; // not human friendly by default - sys->switchGoalSelectMethod = 3; // default goal selection method - sys->traverse = 12; // default traversal method - - sys->switch_maxproofdepth = INT_MAX; - sys->switch_maxtracelength = INT_MAX; sys->maxtracelength = INT_MAX; /* init rundefs */ @@ -97,19 +73,21 @@ systemInit () sys->secrets = NULL; // list of claimed secrets sys->synchronising_labels = NULL; sys->attack = NULL; - sys->prune = 2; // default pruning method /* no protocols => no protocol preprocessed */ sys->rolecount = 0; sys->roleeventmax = 0; sys->claimlist = NULL; sys->labellist = NULL; - sys->match = 0; // default matching 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); + } sys->bindings = NULL; sys->current_claim = NULL; @@ -151,7 +129,7 @@ systemReset (const System sys) sys->secrets = NULL; // list of claimed secrets /* transfer switches */ - sys->maxtracelength = sys->switch_maxtracelength; + sys->maxtracelength = switches.maxtracelength; /* POR init */ sys->PORphase = -1; @@ -160,11 +138,11 @@ systemReset (const System sys) /* global latex switch: ugly, but otherwise I must carry it into every * single subprocedure such as termPrint */ - globalLatex = sys->latex; + globalLatex = switches.latex; /* propagate mgu_mode */ - setMguMode (sys->match); + setMguMode (switches.match); } //! Initialize runtime system (according to cut traces, limited runs) @@ -186,7 +164,7 @@ systemRuns (const System sys) } } #ifdef DEBUG - if (sys->switchScenario < 0) + if (switches.scenario < 0) { warning ("Last run with a choose: %i", sys->lastChooseRun); } @@ -294,7 +272,7 @@ ensureValidRun (const System sys, int run) myrun.artefacts = NULL; myrun.substitutions = NULL; - if (sys->engine == POR_ENGINE) + if (switches.engine == POR_ENGINE) { myrun.know = knowledgeDuplicate (sys->know); } @@ -378,7 +356,7 @@ not_read_first (const Roledef rdstart, const Term t) Term agentOfRunRole (const System sys, const int run, const Term role) { - if (sys->engine != ARACHNE_ENGINE) + if (switches.engine != ARACHNE_ENGINE) { // Non-arachne Termlist roles; @@ -762,7 +740,7 @@ roleInstanceArachne (const System sys, const Protocol protocol, * TODO currently disabled: something weird was goind on causing weird prunes, * for match=2. Investigate later. */ - if (0 && not_read_first (rd, oldt) && sys->match == 2) + if (0 && not_read_first (rd, oldt) && switches.match == 2) { /* this term is forced as a choose, or it does not occur in the (first) read event */ if (extterm == NULL) @@ -898,7 +876,7 @@ roleInstanceModelchecker (const System sys, const Protocol protocol, /* newvar is apparently new, but it might occur * in the first event if it's a read, in which * case we forget it */ - if (sys->switchForceChoose || not_read_first (rd, scanfrom->term)) + 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) @@ -964,7 +942,7 @@ roleInstanceModelchecker (const System sys, const Protocol protocol, /* erase any substitutions in the role definition, as they are now copied */ termlistSubstReset (role->variables); - if (sys->engine == POR_ENGINE) + if (switches.engine == POR_ENGINE) { /* Determine symmetric run */ runs[rid].prevSymmRun = staticRunSymmetry (sys, rid); // symmetry reduction static analysis @@ -986,7 +964,7 @@ void roleInstance (const System sys, const Protocol protocol, const Role role, const Termlist paramlist, Termlist substlist) { - if (sys->engine == ARACHNE_ENGINE) + if (switches.engine == ARACHNE_ENGINE) { roleInstanceArachne (sys, protocol, role, paramlist, substlist); } @@ -1020,7 +998,7 @@ 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 (sys->engine == ARACHNE_ENGINE) + if (switches.engine == ARACHNE_ENGINE) { Termlist artefacts; // Remove artefacts @@ -1250,7 +1228,7 @@ untrustedAgent (const System sys, Termlist agents) { if (isTermVariable (agents->term)) { - if (sys->clp) + if (switches.clp) { /* clp: variables are difficult */ /* TODO Add as constraint that they're @@ -1360,13 +1338,13 @@ attackLength (struct tracebuf *tb) } void -commandlinePrint (FILE * stream, const System sys) +commandlinePrint (FILE * stream) { /* print command line */ int i; - for (i = 0; i < sys->argc; i++) - fprintf (stream, " %s", sys->argv[i]); + for (i = 0; i < switches.argc; i++) + fprintf (stream, " %s", switches.argv[i]); } //! Get the number of roles in the system. diff --git a/src/system.h b/src/system.h index ea01969..1908d0d 100644 --- a/src/system.h +++ b/src/system.h @@ -103,7 +103,6 @@ struct tracebuf //! The main state structure. struct system { - int engine; //!< Engine type (POR_ENGINE,ARACHNE_ENGINE) int step; //!< Step in trace during exploration. Can be managed globally Knowledge know; //!< Knowledge in currect step of system. struct parameters *parameters; // misc @@ -117,41 +116,7 @@ struct system Termlist secrets; //!< Integrate secrets list into system. Termlist synchronising_labels; //!< List of labels that might synchronise. int shortestattack; //!< Length of shortest attack trace. - - /* switches */ - int output; //!< From enum outputs: what should be produced. Default ATTACK. - int report; - int prune; //!< Type of pruning. - int switch_maxproofdepth; //!< Maximum proof depth - int switch_maxtracelength; //!< Maximum trace length allowed int maxtracelength; //!< helps to remember the length of the last trace. - int switchM; //!< Memory display switch. - int switchT; //!< Time display switch. - int switchS; //!< Progress display switch. (traversed states) - int porparam; //!< A multi-purpose integer parameter, passed to the partial order reduction method selected. - int switchRuns; //!< The number of runs as in the switch - int switchScenario; //!< -1 to count, 0 for disable, 1-n to select the choose scenario - int switchScenarioSize; //!< Scenario size, also called fixed trace prefix length - int switchForceChoose; //!< Force chooses for each run, even if involved in first read - int switchChooseFirst; //!< Priority to chooses, implicit and explicit - int switchReadSymm; //!< Enable read symmetry reduction - int switchAgentSymm; //!< Enable agent symmetry reduction - int switchSymmOrder; //!< Enable symmetry order reduction - int switchNomoreClaims; //!< Enable no more claims cutter - int switchReduceEndgame; //!< Enable endgame cutter - int switchReduceClaims; //!< Symmetry reduction on claims (only works when switchAgentSymm is true) - int switchClaims; //!< Enable clails report - int switchGoalSelectMethod; //!< Goal selection method for Arachne engine - Term switchClaimToCheck; //!< Which claim should be checked? - int switchXMLoutput; //!< xml output - int switchHuman; //!< human readable - - //! Latex output switch. - /** - * Obsolete. Use globalLatex instead. - *\sa globalLatex - */ - int latex; /* traversal */ int traverse; //!< Traversal method. @@ -166,10 +131,6 @@ struct system int attackid; //!< Global counter of attacks (used for assigning identifiers) within this Scyther call. int countScenario; //!< Number of scenarios skipped. - /* matching */ - int match; //!< Matching type. - int clp; //!< Do we use clp? - /* protocol definition */ Protocol protocols; //!< List of protocols in the system Termlist locals; //!< List of local terms @@ -201,10 +162,6 @@ struct system //! Shortest attack storage. struct tracebuf *attack; - - //! Command line arguments - int argc; - char **argv; }; typedef struct system *System; @@ -239,7 +196,7 @@ 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, const System sys); +void commandlinePrint (FILE * stream); int compute_rolecount (const System sys); int compute_roleeventmax (const System sys); diff --git a/src/type.c b/src/type.c index 5497d95..3667ffc 100644 --- a/src/type.c +++ b/src/type.c @@ -10,6 +10,7 @@ #include "termlist.h" #include "system.h" #include "debug.h" +#include "switches.h" /* * Special term definitions from compiler.c @@ -142,7 +143,7 @@ checkTypeLocals (const System sys) { if (sys->runs[run].protocol != INTRUDER) { - if (!checkTypeTermlist (sys->match, sys->runs[run].locals)) + if (!checkTypeTermlist (switches.match, sys->runs[run].locals)) return false; } run++; diff --git a/src/xmlout.c b/src/xmlout.c index 87fee45..5192e46 100644 --- a/src/xmlout.c +++ b/src/xmlout.c @@ -17,6 +17,7 @@ #include "system.h" #include "binding.h" #include "arachne.h" // for get_semitrace_length +#include "switches.h" #include "xmlout.h" @@ -411,7 +412,7 @@ isProtocolInvolved (const System sys, const Protocol p) int isEventInteresting (const System sys, const Roledef rd) { - if (sys->switchHuman) + if (switches.human) { if (rd->type != CLAIM) { @@ -624,7 +625,7 @@ xmlOutSysInfo (const System sys) xmlPrint (""); xmlindent++; - xmlOutInteger ("match", sys->match); + xmlOutInteger ("match", switches.match); xmlInitialKnowledge (sys); xmlInvolvedProtocolRoles (sys);