andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Large rewrite of switch code. Instead of having switch parameters in

Browse Source 
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.
This commit is contained in:
ccremers 2005-06-07 15:02:27 +00:00
parent c4fad31f25
commit 1bdaf7b5d9
17 changed files with 400 additions and 325 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

138
src/arachne.c
View File

@ -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");

4
src/binding.c
View File

@ -13,6 +13,7 @@
#include "term.h"
#include "termmap.h"
#include "arachne.h"
#include "switches.h"
#include <malloc.h>
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

7
src/compiler.c
View File

@ -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;

122
src/main-switches.c
View File

@ -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);

56
src/main.c
View File

@ -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);

5
src/match_basic.c
View File

@ -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))
{

3
src/match_clp.c
View File

@ -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;
}

4
src/mgu.c
View File

@ -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)
{

67
src/modelchecker.c
View File

@ -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);

11
src/output.c
View File

@ -10,6 +10,7 @@
#include <stdio.h>
#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)

9
src/report.c
View File

@ -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 ("<REPORT>\n");
@ -47,7 +48,7 @@ reportMid (const System sys)
void
reportEnd (const System sys)
{
if (!sys->latex)
if (!switches.latex)
{
indent ();
printf ("<REPORT>\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;

118
src/switches.c
View File

@ -10,8 +10,10 @@
#include "debug.h"
#include "version.h"
#include "timer.h"
#include "switches.h"
#include <limits.h>
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);
}
}

64
src/switches.h
View File

@ -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

64
src/system.c
View File

@ -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.

45
src/system.h
View File

@ -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);

3
src/type.c
View File

@ -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++;

5
src/xmlout.c
View File

@ -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 ("<system>");
xmlindent++;
xmlOutInteger ("match", sys->match);
xmlOutInteger ("match", switches.match);
xmlInitialKnowledge (sys);
xmlInvolvedProtocolRoles (sys);