diff --git a/src/main-switches.c b/src/main-switches.c new file mode 100644 index 0000000..acebb29 --- /dev/null +++ b/src/main-switches.c @@ -0,0 +1,1023 @@ +/** + * OBSOLETE SWITCH HANDLING + * + * However, there are some switches here that are not yet found in switches.c + */ + +/** + * \mainpage + * + * \section intro Introduction + * + * Scyther is a model checker for security protocols. + * + * \section install Installation + * + * How to install Scyther. + * + * \section exit Exit codes + * + * 0 Okay No attack found, claims encountered + * + * 1 Error Something went wrong (error) E.g. switch error, or scenario ran out. + * + * 2 Okay No attack found (because) no claims encountered + * + * 3 Okay Attack found + * + * However, if the --scenario=-1 switch is used, the exit code is used to return the number of scenarios. + * + * \section coding Coding conventions + * + * Usually, each source file except main.c has an myfileInit() and myfileDone() function + * available. These allow any initialisation and destruction of required structures. + * + * GNU indent rules are used, but K&R derivatives are allowed as well. Conversion can + * be done for any style using the GNU indent program. + */ + +enum exittypes +{ EXIT_NOATTACK = 0, EXIT_ERROR = 1, EXIT_NOCLAIM = 2, EXIT_ATTACK = 3 }; + +#include +#include +#include +#include +#include "system.h" +#include "debug.h" +#include "modelchecker.h" +#include "memory.h" +#include "symbol.h" +#include "pheading.h" +#include "symbol.h" +#include "parser.h" +#include "tac.h" +#include "timer.h" +#include "compiler.h" +#include "latex.h" +#include "output.h" +#include "binding.h" +#include "version.h" + +#include "argtable2.h" + +// The global system state +System sys; + +extern struct tacnode *spdltac; +extern Term TERM_Claim; +extern int mgu_match; + +void scanner_cleanup (void); +void strings_cleanup (void); +int yyparse (void); + +void MC_incRuns (const System sys); +void MC_incTraces (const System sys); +void MC_single (const System sys); +int modelCheck (const System sys); + +//! The name of this program. +const char *progname = "scyther"; +//! Release tag name. +/** + * Note that this is only referenced in the help output of the commandline program. + * \todo Come up with a useful solution for release names. + */ +const char *releasetag = SVNVERSION; + +//! The number of seconds a test is allowed to run +static int time_limit_seconds; + +//! The main body, as called by the environment. +int +main (int argc, char **argv) +{ + struct arg_file *infile = + arg_file0 (NULL, NULL, "FILE", "input file ('-' for stdin)"); + struct arg_file *outfile = arg_file0 ("o", "output", "FILE", + "output file (default is stdout)"); + struct arg_lit *switch_arachne = + arg_lit0 ("a", "arachne", "use Arachne engine"); + struct arg_lit *switch_proof = + arg_lit0 ("P", "proof", "generate proof output"); + struct arg_str *switch_check = arg_str0 (NULL, "check", "CLAIM", + "claim type to check (default is all)"); + struct arg_int *switch_scenario = arg_int0 ("s", "scenario", NULL, + "select a scenario instance 1-n (-1 to count)"); + struct arg_int *switch_scenario_size = arg_int0 ("S", "scenario-size", NULL, + "scenario size (fixed trace prefix length)"); + struct arg_int *switch_traversal_method = arg_int0 ("t", "traverse", NULL, + "set traversal method, partial order reduction (default is 12)"); + struct arg_int *switch_match_method = + arg_int0 ("m", "match", NULL, "matching method (default is 0)"); + struct arg_lit *switch_clp = + arg_lit0 ("c", "cl", "use constraint logic, non-associative"); + struct arg_int *switch_pruning_method = arg_int0 ("p", "prune", NULL, + "pruning method (default is 2)"); + struct arg_int *switch_prune_trace_length = + arg_int0 ("l", "max-length", NULL, + "prune traces longer than events."); + struct arg_int *switch_prune_proof_depth = arg_int0 ("d", "max-depth", NULL, + "prune proof deeper than splits."); + struct arg_lit *switch_incremental_trace_length = + arg_lit0 (NULL, "increment-traces", + "incremental search using the length of the traces."); + struct arg_int *switch_maximum_runs = + arg_int0 ("r", "max-runs", NULL, "create at most runs"); + struct arg_lit *switch_incremental_runs = arg_lit0 (NULL, "increment-runs", + "incremental search using the number of runs"); + struct arg_int *switch_goal_select_method = + arg_int0 (NULL, "goal-select", NULL, + "use goal selection method (default 3)"); + struct arg_lit *switch_latex_output = + arg_lit0 (NULL, "latex", "output attacks in LaTeX format"); + struct arg_lit *switch_empty = + arg_lit0 ("e", "empty", "do not generate output"); + struct arg_lit *switch_progress_bar = + arg_lit0 ("b", "progress-bar", "show progress bar"); + struct arg_lit *switch_state_space_graph = + arg_lit0 (NULL, "state-space", "output state space graph"); + struct arg_lit *switch_implicit_choose = arg_lit0 (NULL, "implicit-choose", + "allow implicit choose events (useful for few runs)"); + struct arg_lit *switch_choose_first = + arg_lit0 (NULL, "choose-first", "priority to any choose events"); + struct arg_lit *switch_enable_read_symmetries = + arg_lit0 (NULL, "read-symm", "enable read symmetry reductions"); + struct arg_lit *switch_disable_agent_symmetries = + arg_lit0 (NULL, "no-agent-symm", + "disable agent symmetry reductions"); + struct arg_lit *switch_enable_symmetry_order = arg_lit0 (NULL, "symm-order", + "enable ordering symmetry reductions"); + struct arg_lit *switch_disable_noclaims_reductions = + arg_lit0 (NULL, "no-noclaims-red", + "disable no more claims reductions"); + struct arg_lit *switch_disable_endgame_reductions = + arg_lit0 (NULL, "no-endgame-red", "disable endgame reductions"); + struct arg_lit *switch_disable_claim_symmetry = + arg_lit0 (NULL, "no-claimsymmetry-red", + "disable claim symmetry reductions"); + struct arg_lit *switch_summary = arg_lit0 (NULL, "summary", + "show summary on stdout instead of stderr"); + struct arg_lit *switch_echo = + arg_lit0 ("E", "echo", "echo command line to stdout"); + struct arg_int *switch_timer = + arg_int0 ("T", "timer", NULL, "maximum time in seconds"); +#ifdef DEBUG + struct arg_int *switch_por_parameter = + arg_int0 (NULL, "pp", NULL, "POR parameter"); + struct arg_lit *switch_debug_indent = arg_lit0 ("I", "debug-indent", + "indent the debug output using trace length"); + struct arg_int *switch_debug_level = + arg_int0 ("D", "debug", NULL, "set debug level (default is 0)"); +#endif + struct arg_lit *help = arg_lit0 (NULL, "help", "print this help and exit"); + struct arg_lit *version = + arg_lit0 (NULL, "version", "print version information and exit"); + struct arg_end *end = arg_end (30); + void *argtable[] = { + infile, + outfile, + switch_empty, + switch_proof, + switch_state_space_graph, + switch_scenario, + switch_scenario_size, + switch_latex_output, + switch_summary, + switch_echo, + switch_progress_bar, + + switch_arachne, + switch_check, + switch_traversal_method, + switch_match_method, + switch_clp, + switch_timer, + switch_pruning_method, + switch_prune_proof_depth, + switch_prune_trace_length, switch_incremental_trace_length, + switch_maximum_runs, switch_incremental_runs, + switch_goal_select_method, + + switch_implicit_choose, + switch_choose_first, + switch_enable_read_symmetries, + switch_enable_symmetry_order, + switch_disable_agent_symmetries, + switch_disable_noclaims_reductions, + switch_disable_endgame_reductions, + switch_disable_claim_symmetry, +#ifdef DEBUG + switch_por_parameter, + switch_debug_indent, + switch_debug_level, +#endif + help, version, + end + }; + int nerrors; + int exitcode = EXIT_NOATTACK; + + /* verify the argtable[] entries were allocated sucessfully */ + if (arg_nullcheck (argtable) != 0) + { + /* NULL entries were detected, some allocations must have failed */ + fprintf (stderr, "%s: insufficient memory\n", progname); + exitcode = EXIT_ERROR; + goto exit; + } + + /* defaults + * set any command line default values prior to parsing */ +#ifdef DEBUG + switch_debug_level->ival[0] = 0; + switch_por_parameter->ival[0] = 0; +#endif + switch_scenario->ival[0] = 0; + switch_scenario_size->ival[0] = 0; + switch_traversal_method->ival[0] = 12; + switch_match_method->ival[0] = 0; + switch_prune_trace_length->ival[0] = -1; + switch_prune_proof_depth->ival[0] = -1; + switch_maximum_runs->ival[0] = INT_MAX; + switch_pruning_method->ival[0] = 2; + switch_goal_select_method->ival[0] = -1; + switch_timer->ival[0] = 0; + + /* Parse the command line as defined by argtable[] */ + nerrors = arg_parse (argc, argv, argtable); + + /* special case: '--help' takes precedence over error reporting */ + if (help->count > 0) + { + printf ("Usage: %s ", progname); + arg_print_syntax (stdout, argtable, "\n"); + printf + ("This program can model check security protocols for various\n"); + printf ("properties, given a finite scenario.\n\n"); + arg_print_glossary (stdout, argtable, " %-25s %s\n"); + exitcode = 0; + goto exit; + } + + /* special case: '--version' takes precedence error reporting */ + if (version->count > 0) + { + printf ("'%s' model checker for security protocols.\n", progname); +#ifdef DEBUG + printf ("Revision %s, compiled with debugging support.\n", releasetag); +#else + printf ("Revision %s\n", releasetag); +#endif + printf ("December 2003--, Cas Cremers\n"); + exitcode = 0; + goto exit; + } + + /* If the parser returned any errors then display them and exit */ + if (nerrors > 0) + { + /* Display the error details contained in the arg_end struct. */ + arg_print_errors (stdout, end, progname); + printf ("Try '%s --help' for more information.\n", progname); + exitcode = EXIT_ERROR; + goto exit; + } + + /* special case: uname with no command line options induces brief help */ + if (argc == 1) + { + printf ("Try '%s --help' for more information.\n", progname); + exitcode = 0; + goto exit; + } + + /* + * Arguments have been parsed by argtable, + * continue with main code. + */ + + /* Lutger-tries-to-test-with-broken-methods detector */ + if (switch_clp->count > 0) + { + fprintf (stderr, + "For the time being, this method is not supported, \n"); + fprintf (stderr, "as too many changes have been made to the normal \n"); + fprintf (stderr, + "matching logic, and CL simply isn't reliable in \nmany "); + fprintf (stderr, "ways. Try again in a few weeks.\n"); + exit (0); + } + + /* redirect in- and output according to supplied filenames */ + /* output */ + if (outfile->count > 0) + { + /* try to open */ + if (!freopen (outfile->filename[0], "w", stdout)) + { + fprintf (stderr, "Could not create output file '%s'.\n", + outfile->filename[0]); + exit (1); + } + } + /* input */ + if (infile->count > 0) + { + /* check for the single dash */ + if (strcmp (infile->filename[0], "-")) + { + if (!freopen (infile->filename[0], "r", stdin)) + { + fprintf (stderr, "Could not open input file '%s'.\n", + infile->filename[0]); + exit (1); + } + } + } + + /* handle debug level */ +#ifdef DEBUG + debugSet (switch_debug_level->ival[0]); +#else + debugSet (0); +#endif + /* Initialize memory routines */ + memInit (); + + /* initialize symbols */ + termsInit (); + termmapsInit (); + termlistsInit (); + knowledgeInit (); + symbolsInit (); + tacInit (); + + /* + * ------------------------------------------------ + * generate system + * ------------------------------------------------ + */ + + sys = systemInit (); + if (switch_arachne->count > 0) + { + sys->engine = ARACHNE_ENGINE; + bindingInit (sys); + } + /* init compiler for this system */ + compilerInit (sys); + + /* transfer command line */ + sys->argc = argc; + sys->argv = argv; + + if (switch_echo->count > 0) + { + /* print command line */ + fprintf (stdout, "command\t"); + commandlinePrint (stdout, sys); + fprintf (stdout, "\n"); + } + + /* handle switches */ + + sys->switchRuns = switch_maximum_runs->ival[0]; /* maximum number of runs */ + if (switch_implicit_choose->count > 0) + /* allow implicit chooses */ + sys->switchForceChoose = 0; + if (switch_choose_first->count > 0) + sys->switchChooseFirst = 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; + } + if (switch_enable_symmetry_order->count > 0) + sys->switchSymmOrder = 1; /* enable symmetry order */ + if (switch_disable_agent_symmetries->count > 0) + sys->switchAgentSymm = 0; /* disable agent symmetry order */ + if (switch_disable_noclaims_reductions->count > 0) + sys->switchNomoreClaims = 0; /* disable no more claims cutter */ + if (switch_disable_endgame_reductions->count > 0) + sys->switchReduceEndgame = 0; /* disable endgame cutter */ + if (switch_disable_claim_symmetry->count > 0) + sys->switchReduceClaims = 0; /* disable claim symmetry cutter */ + if (switch_summary->count > 0) + sys->output = SUMMARY; /* report summary on stdout */ + if (switch_proof->count > 0) + sys->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) + { + /* no scenario, but a size is set. so override */ +#ifdef DEBUG + warning ("Scanning scenarios."); +#endif + sys->switchScenario = -1; + } + if (sys->switchScenario < 0) + { + sys->output = SCENARIOS; + } + if (sys->switchScenario != 0 && sys->switchScenarioSize == 0) + { +#ifdef DEBUG + warning + ("Scenario selection without trace prefix length implies --choose-first."); +#endif + sys->switchChooseFirst = 1; + } +#ifdef DEBUG + sys->porparam = switch_por_parameter->ival[0]; +#endif + sys->latex = switch_latex_output->count; + sys->know = emptyKnowledge (); + + + /* parse compiler-dependant switches */ + if (switch_check->count > 0) + { + Term claim; + +#ifdef DEBUG + if (lookup (switch_check->sval[0]) == NULL) + { + globalError++; + warning ("Could not find this string at all in:"); + symbolPrintAll (); + eprintf ("\n"); + globalError--; + } +#endif + claim = findGlobalConstant (switch_check->sval[0]); + if (claim == NULL) + error ("Unknown claim type to check."); + if (inTermlist (claim->stype, TERM_Claim)) + sys->switchClaimToCheck = claim; + else + error ("Claim type to check is not a claim."); + } + + /* parse input */ + + yyparse (); +#ifdef DEBUG + if (DEBUGL (1)) + tacPrint (spdltac); +#endif + + /* compile */ + + if (sys->engine != ARACHNE_ENGINE) + { + // Compile as many runs as possible + compile (spdltac, switch_maximum_runs->ival[0]); + } + else + { + // Compile no runs for Arachne + compile (spdltac, 0); + } + scanner_cleanup (); + + /* preprocess */ + preprocess (sys); + +#ifdef DEBUG + if (DEBUGL (1)) + { + printf ("\nCompilation yields:\n\n"); + printf ("untrusted agents: "); + termlistPrint (sys->untrusted); + printf ("\n"); + knowledgePrint (sys->know); + printf ("inverses: "); + knowledgeInversesPrint (sys->know); + printf ("\n"); + locVarPrint (sys->locals); + protocolsPrint (sys->protocols); + + printf ("\nInstantiated runs:\n\n"); + runsPrint (sys); + } +#endif + + /* allocate memory for traces, based on runs */ + systemStart (sys); + sys->traceKnow[0] = sys->know; // store initial knowledge + + /* add parameters to system */ + + sys->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]; + 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; + else + /* disable progress display */ + sys->switchS = 0; + if (switch_state_space_graph->count > 0) + { + /* enable state space graph output */ + sys->output = STATESPACE; //!< New method + } + if (switch_empty->count > 0) + sys->output = EMPTY; + if (switch_prune_proof_depth->ival[0] >= 0) + sys->switch_maxproofdepth = switch_prune_proof_depth->ival[0]; + if (switch_prune_trace_length->ival[0] >= 0) + sys->switch_maxtracelength = switch_prune_trace_length->ival[0]; + if (switch_goal_select_method->ival[0] >= 0) + sys->switchGoalSelectMethod = 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); +#else + /* non-debug defaults */ + sys->switchM = 0; +#endif + + /* + * --------------------------------------- + * Switches consistency checking. + * --------------------------------------- + */ + + /* Latex only makes sense for attacks */ + if (sys->latex && sys->output != ATTACK) + { + error ("Scyther can only generate LaTeX output for attacks."); + } + /* Incremental stuff only works for attack locating */ + if (switch_incremental_runs->count > 0 || + switch_incremental_trace_length->count > 0) + { + if (sys->output != ATTACK && sys->output != EMPTY) + { + error ("Incremental traversal only for empty or attack output."); + } + } +#ifdef DEBUG + if (DEBUGL (4)) + { + warning ("Selected output method is %i", sys->output); + } +#endif + + if (sys->engine == ARACHNE_ENGINE) + { + arachneInit (sys); + } + /* + * --------------------------------------- + * Start real stuff + * --------------------------------------- + */ + + /* latex header? */ + if (sys->latex) + latexInit (sys, argc, argv); + + /* model check system */ +#ifdef DEBUG + if (DEBUGL (1)) + warning ("Start modelchecking system."); +#endif + if (switch_incremental_runs->count > 0) + { + MC_incRuns (sys); + } + else + { + if (switch_incremental_trace_length->count > 0) + { + MC_incTraces (sys); + } + else + { + MC_single (sys); + } + } + + /* + * --------------------------------------- + * After checking the system, results + * --------------------------------------- + */ + + /* Display shortest attack, if any */ + + if (sys->attack != NULL && sys->attack->length != 0) + { + if (sys->output == ATTACK) + { + attackDisplay (sys); + } + /* mark exit code */ + exitcode = EXIT_ATTACK; + } + else + { + /* check if there is a claim type that was never reached */ + Claimlist cl_scan; + + cl_scan = sys->claimlist; + while (cl_scan != NULL) + { + if (cl_scan->failed == STATES0) + { + /* mark exit code */ + exitcode = EXIT_NOCLAIM; + } + cl_scan = cl_scan->next; + } + + } + + /* latex closeup */ + if (sys->latex) + latexDone (sys); + + /* Transfer any scenario counting to the exit code, + * assuming that there is no error. */ + if (exitcode != EXIT_ERROR && sys->switchScenario < 0) + { + exitcode = sys->countScenario; + } + + /* + * Now we clean up any memory that was allocated. + */ + + if (sys->engine == ARACHNE_ENGINE) + { + arachneDone (); + bindingDone (); + } + knowledgeDestroy (sys->know); + systemDone (sys); + compilerDone (); + + /* done symbols */ + tacDone (); + symbolsDone (); + knowledgeDone (); + termlistsDone (); + termmapsDone (); + termsDone (); + + /* memory clean up? */ + strings_cleanup (); + memDone (); + +exit: + /* deallocate each non-null entry in argtable[] */ + arg_free (argtable); + + return exitcode; +} + +//! Display time and state space size information using ASCII. +/** + * Displays also whether an attack was found or not. + */ + +void +timersPrint (const System sys) +{ + Claimlist cl_scan; + int anyclaims; + +// #define NOTIMERS + + /* display stats */ + if (sys->output != SUMMARY) + { + globalError++; + } + + /* states traversed */ + + eprintf ("states\t"); + statesPrintShort (sys); + eprintf ("\n"); + + /* scenario info */ + + if (sys->switchScenario > 0) + { + eprintf ("scen_st\t"); + statesFormat (sys->statesScenario); + eprintf ("\n"); + } + + /* flag + * + * L n Attack of length + * None failed claim + * NoClaim no claims + */ + + eprintf ("attack\t"); + if (sys->claims == STATES0) + { + eprintf ("NoClaim\n"); + } + else + { + if (sys->failed != STATES0) + eprintf ("L:%i\n", attackLength (sys->attack)); + else + eprintf ("None\n"); + } + +#ifndef NOTIMERS + /* print time */ + + double seconds; + seconds = (double) clock () / CLOCKS_PER_SEC; + eprintf ("time\t%.3e\n", seconds); + + /* states per second */ + + eprintf ("st/sec\t"); + if (seconds > 0) + { + eprintf ("%.3e\n", statesDouble (sys->states) / seconds); + } + else + { + eprintf ("\n"); + } +#endif + + /* Print also individual claims */ + /* Note that if the output is set to empty, the claim output is redirected to stdout (for e.g. processing) + */ + cl_scan = sys->claimlist; + anyclaims = 0; + while (cl_scan != NULL) + { + anyclaims = 1; + + eprintf ("claim\t"); + + /* claim label is tuple */ + if (realTermTuple (cl_scan->label)) + { + /* modern version: claim label is tuple (protocname, label) */ + /* first print protocol.role */ + termPrint (TermOp1 (cl_scan->label)); + eprintf ("\t"); + termPrint (cl_scan->rolename); + eprintf ("\t"); + /* second print event_label */ + termPrint (cl_scan->type); + eprintf ("_"); + termPrint (TermOp2 (cl_scan->label)); + eprintf ("\t"); + } + else + { + /* old-fashioned output */ + termPrint (cl_scan->type); + eprintf ("\t"); + termPrint (cl_scan->rolename); + eprintf (" ("); + termPrint (cl_scan->label); + eprintf (")\t"); + } + /* print counts etc. */ + eprintf ("found:\t"); + statesFormat (cl_scan->count); + if (cl_scan->count > 0) + { + if (cl_scan->failed > 0) + { + eprintf ("\t"); + eprintf ("failed:\t"); + statesFormat (cl_scan->failed); + } + else + { + eprintf ("\tcorrect: "); + if (cl_scan->complete) + { + eprintf ("complete_proof"); + } + else + { + eprintf ("bounded_proof"); + if (cl_scan->timebound) + eprintf ("\ttime=%i", time_limit_seconds); + } + } + } + else + { + eprintf ("\tcorrect: does_not_occur"); + } + eprintf ("\n"); + cl_scan = cl_scan->next; + } + if (!anyclaims) + { + warning ("No claims in system."); + } + + /* reset globalError */ + if (sys->output != SUMMARY) + { + globalError--; + } +} + +//! Analyse the model by incremental runs. +/* + * This procedure considers mainly incremental searches, and settings + * parameters for that. The real work is handled by modelCheck. + */ + +void +MC_incRuns (const System sys) +{ + /* + * incremental runs check + * + * note: we assume that at least one run needs to be checked. + */ + int maxruns = sys->maxruns; + int runs = 1; + int flag = 1; + int res; + + do + { + systemReset (sys); + sys->maxruns = runs; + systemRuns (sys); + fprintf (stderr, "%i of %i runs in incremental runs search.\n", + runs, maxruns); + res = modelCheck (sys); + fprintf (stderr, "\n"); + if (res) + { + /* Apparently a violation occurred. If we are searching + * the whole space, then we just continue. However, if + * we're looking to prune, ``the buck stops here''. */ + + if (sys->prune != 0) + { + flag = 0; + } + } + runs++; + } + while (flag && runs <= maxruns); + sys->maxruns = maxruns; +} + +//! Analyse the model by incremental trace lengths. +/* + * This procedure considers mainly incremental searches, and settings + * parameters for that. The real work is handled by modelCheck. + */ + +void +MC_incTraces (const System sys) +{ + /* + * incremental traces check + * + * note: we assume that at least one run needs to be checked. + */ + int maxtracelen; + int tracelen; + int tracestep; + int flag; + int res; + + tracestep = 3; /* what is a sensible stepping size? */ + flag = 1; + + maxtracelen = getMaxTraceLength (sys); + tracelen = maxtracelen - tracestep; + while (tracelen > 6) /* what is a reasonable minimum? */ + tracelen -= tracestep; + + flag = 1; + + do + { + systemReset (sys); + sys->maxtracelength = tracelen; + systemRuns (sys); + fprintf (stderr, + "%i of %i trace length in incremental trace length search.\n", + tracelen, maxtracelen); + res = modelCheck (sys); + fprintf (stderr, "\n"); + if (res) + { + /* Apparently a violation occurred. If we are searching + * the whole space, then we just continue. However, if + * we're looking to prune, ``the buck stops here''. */ + + if (sys->prune != 0) + { + flag = 0; + } + } + tracelen += tracestep; + } + while (flag && tracelen <= maxtracelen); +} + +//! Analyse the model with a fixed scenario. +/** + * Traditional handywork. + */ + +void +MC_single (const System sys) +{ + /* + * simple one-time check + */ + + systemReset (sys); // reset any globals + systemRuns (sys); // init runs data + modelCheck (sys); +} + +//! Model check the system, given all parameters. +/* + * Precondition: the system was reset with the corresponding parameters. + * Reports time and states traversed. + * Note that the return values doubles as the number of failed claims. + *@return True iff any claim failed, and thus an attack was found. + */ + +int +modelCheck (const System sys) +{ + if (sys->output == STATESPACE) + { + graphInit (sys); + } + + /* modelcheck the system */ + switch (sys->engine) + { + case POR_ENGINE: + traverse (sys); + break; + case ARACHNE_ENGINE: + arachne (); + break; + default: + error ("Unknown engine type %i.", sys->engine); + } + + /* clean up any states display */ + if (sys->switchS > 0) + { + // States: 1.000e+06 + fprintf (stderr, " \r"); + } + + timersPrint (sys); + if (sys->output == STATESPACE) + { + graphDone (sys); + } + if (sys->switchScenario > 0) + { + /* Traversing a scenario. Maybe we ran out. */ + if (sys->switchScenario > sys->countScenario) + { + /* Signal as error */ + exit (1); + } + } + return (sys->failed != STATES0); +} diff --git a/src/main.c b/src/main.c index 7047e96..6e5846c 100644 --- a/src/main.c +++ b/src/main.c @@ -58,7 +58,7 @@ enum exittypes #include "latex.h" #include "output.h" #include "binding.h" -#include "version.h" +#include "switches.h" #include "argtable2.h" @@ -78,272 +78,13 @@ void MC_incTraces (const System sys); void MC_single (const System sys); int modelCheck (const System sys); -//! The name of this program. -const char *progname = "scyther"; -//! Release tag name. -/** - * Note that this is only referenced in the help output of the commandline program. - * \todo Come up with a useful solution for release names. - */ -const char *releasetag = SVNVERSION; - -//! The number of seconds a test is allowed to run -static int time_limit_seconds; - //! The main body, as called by the environment. int main (int argc, char **argv) { - struct arg_file *infile = - arg_file0 (NULL, NULL, "FILE", "input file ('-' for stdin)"); - struct arg_file *outfile = arg_file0 ("o", "output", "FILE", - "output file (default is stdout)"); - struct arg_lit *switch_arachne = - arg_lit0 ("a", "arachne", "use Arachne engine"); - struct arg_lit *switch_proof = - arg_lit0 ("P", "proof", "generate proof output"); - struct arg_str *switch_check = arg_str0 (NULL, "check", "CLAIM", - "claim type to check (default is all)"); - struct arg_int *switch_scenario = arg_int0 ("s", "scenario", NULL, - "select a scenario instance 1-n (-1 to count)"); - struct arg_int *switch_scenario_size = arg_int0 ("S", "scenario-size", NULL, - "scenario size (fixed trace prefix length)"); - struct arg_int *switch_traversal_method = arg_int0 ("t", "traverse", NULL, - "set traversal method, partial order reduction (default is 12)"); - struct arg_int *switch_match_method = - arg_int0 ("m", "match", NULL, "matching method (default is 0)"); - struct arg_lit *switch_clp = - arg_lit0 ("c", "cl", "use constraint logic, non-associative"); - struct arg_int *switch_pruning_method = arg_int0 ("p", "prune", NULL, - "pruning method (default is 2)"); - struct arg_int *switch_prune_trace_length = - arg_int0 ("l", "max-length", NULL, - "prune traces longer than events."); - struct arg_int *switch_prune_proof_depth = arg_int0 ("d", "max-depth", NULL, - "prune proof deeper than splits."); - struct arg_lit *switch_incremental_trace_length = - arg_lit0 (NULL, "increment-traces", - "incremental search using the length of the traces."); - struct arg_int *switch_maximum_runs = - arg_int0 ("r", "max-runs", NULL, "create at most runs"); - struct arg_lit *switch_incremental_runs = arg_lit0 (NULL, "increment-runs", - "incremental search using the number of runs"); - struct arg_int *switch_goal_select_method = - arg_int0 (NULL, "goal-select", NULL, - "use goal selection method (default 3)"); - struct arg_lit *switch_latex_output = - arg_lit0 (NULL, "latex", "output attacks in LaTeX format"); - struct arg_lit *switch_empty = - arg_lit0 ("e", "empty", "do not generate output"); - struct arg_lit *switch_progress_bar = - arg_lit0 ("b", "progress-bar", "show progress bar"); - struct arg_lit *switch_state_space_graph = - arg_lit0 (NULL, "state-space", "output state space graph"); - struct arg_lit *switch_implicit_choose = arg_lit0 (NULL, "implicit-choose", - "allow implicit choose events (useful for few runs)"); - struct arg_lit *switch_choose_first = - arg_lit0 (NULL, "choose-first", "priority to any choose events"); - struct arg_lit *switch_enable_read_symmetries = - arg_lit0 (NULL, "read-symm", "enable read symmetry reductions"); - struct arg_lit *switch_disable_agent_symmetries = - arg_lit0 (NULL, "no-agent-symm", - "disable agent symmetry reductions"); - struct arg_lit *switch_enable_symmetry_order = arg_lit0 (NULL, "symm-order", - "enable ordering symmetry reductions"); - struct arg_lit *switch_disable_noclaims_reductions = - arg_lit0 (NULL, "no-noclaims-red", - "disable no more claims reductions"); - struct arg_lit *switch_disable_endgame_reductions = - arg_lit0 (NULL, "no-endgame-red", "disable endgame reductions"); - struct arg_lit *switch_disable_claim_symmetry = - arg_lit0 (NULL, "no-claimsymmetry-red", - "disable claim symmetry reductions"); - struct arg_lit *switch_summary = arg_lit0 (NULL, "summary", - "show summary on stdout instead of stderr"); - struct arg_lit *switch_echo = - arg_lit0 ("E", "echo", "echo command line to stdout"); - struct arg_int *switch_timer = - arg_int0 ("T", "timer", NULL, "maximum time in seconds"); -#ifdef DEBUG - struct arg_int *switch_por_parameter = - arg_int0 (NULL, "pp", NULL, "POR parameter"); - struct arg_lit *switch_debug_indent = arg_lit0 ("I", "debug-indent", - "indent the debug output using trace length"); - struct arg_int *switch_debug_level = - arg_int0 ("D", "debug", NULL, "set debug level (default is 0)"); -#endif - struct arg_lit *help = arg_lit0 (NULL, "help", "print this help and exit"); - struct arg_lit *version = - arg_lit0 (NULL, "version", "print version information and exit"); - struct arg_end *end = arg_end (30); - void *argtable[] = { - infile, - outfile, - switch_empty, - switch_proof, - switch_state_space_graph, - switch_scenario, - switch_scenario_size, - switch_latex_output, - switch_summary, - switch_echo, - switch_progress_bar, - - switch_arachne, - switch_check, - switch_traversal_method, - switch_match_method, - switch_clp, - switch_timer, - switch_pruning_method, - switch_prune_proof_depth, - switch_prune_trace_length, switch_incremental_trace_length, - switch_maximum_runs, switch_incremental_runs, - switch_goal_select_method, - - switch_implicit_choose, - switch_choose_first, - switch_enable_read_symmetries, - switch_enable_symmetry_order, - switch_disable_agent_symmetries, - switch_disable_noclaims_reductions, - switch_disable_endgame_reductions, - switch_disable_claim_symmetry, -#ifdef DEBUG - switch_por_parameter, - switch_debug_indent, - switch_debug_level, -#endif - help, version, - end - }; int nerrors; int exitcode = EXIT_NOATTACK; - /* verify the argtable[] entries were allocated sucessfully */ - if (arg_nullcheck (argtable) != 0) - { - /* NULL entries were detected, some allocations must have failed */ - fprintf (stderr, "%s: insufficient memory\n", progname); - exitcode = EXIT_ERROR; - goto exit; - } - - /* defaults - * set any command line default values prior to parsing */ -#ifdef DEBUG - switch_debug_level->ival[0] = 0; - switch_por_parameter->ival[0] = 0; -#endif - switch_scenario->ival[0] = 0; - switch_scenario_size->ival[0] = 0; - switch_traversal_method->ival[0] = 12; - switch_match_method->ival[0] = 0; - switch_prune_trace_length->ival[0] = -1; - switch_prune_proof_depth->ival[0] = -1; - switch_maximum_runs->ival[0] = INT_MAX; - switch_pruning_method->ival[0] = 2; - switch_goal_select_method->ival[0] = -1; - switch_timer->ival[0] = 0; - - /* Parse the command line as defined by argtable[] */ - nerrors = arg_parse (argc, argv, argtable); - - /* special case: '--help' takes precedence over error reporting */ - if (help->count > 0) - { - printf ("Usage: %s ", progname); - arg_print_syntax (stdout, argtable, "\n"); - printf - ("This program can model check security protocols for various\n"); - printf ("properties, given a finite scenario.\n\n"); - arg_print_glossary (stdout, argtable, " %-25s %s\n"); - exitcode = 0; - goto exit; - } - - /* special case: '--version' takes precedence error reporting */ - if (version->count > 0) - { - printf ("'%s' model checker for security protocols.\n", progname); -#ifdef DEBUG - printf ("Revision %s, compiled with debugging support.\n", releasetag); -#else - printf ("Revision %s\n", releasetag); -#endif - printf ("December 2003--, Cas Cremers\n"); - exitcode = 0; - goto exit; - } - - /* If the parser returned any errors then display them and exit */ - if (nerrors > 0) - { - /* Display the error details contained in the arg_end struct. */ - arg_print_errors (stdout, end, progname); - printf ("Try '%s --help' for more information.\n", progname); - exitcode = EXIT_ERROR; - goto exit; - } - - /* special case: uname with no command line options induces brief help */ - if (argc == 1) - { - printf ("Try '%s --help' for more information.\n", progname); - exitcode = 0; - goto exit; - } - - /* - * Arguments have been parsed by argtable, - * continue with main code. - */ - - /* Lutger-tries-to-test-with-broken-methods detector */ - if (switch_clp->count > 0) - { - fprintf (stderr, - "For the time being, this method is not supported, \n"); - fprintf (stderr, "as too many changes have been made to the normal \n"); - fprintf (stderr, - "matching logic, and CL simply isn't reliable in \nmany "); - fprintf (stderr, "ways. Try again in a few weeks.\n"); - exit (0); - } - - /* redirect in- and output according to supplied filenames */ - /* output */ - if (outfile->count > 0) - { - /* try to open */ - if (!freopen (outfile->filename[0], "w", stdout)) - { - fprintf (stderr, "Could not create output file '%s'.\n", - outfile->filename[0]); - exit (1); - } - } - /* input */ - if (infile->count > 0) - { - /* check for the single dash */ - if (strcmp (infile->filename[0], "-")) - { - if (!freopen (infile->filename[0], "r", stdin)) - { - fprintf (stderr, "Could not open input file '%s'.\n", - infile->filename[0]); - exit (1); - } - } - } - - /* handle debug level */ -#ifdef DEBUG - debugSet (switch_debug_level->ival[0]); -#else - debugSet (0); -#endif /* Initialize memory routines */ memInit (); @@ -362,113 +103,18 @@ main (int argc, char **argv) */ sys = systemInit (); - if (switch_arachne->count > 0) - { - sys->engine = ARACHNE_ENGINE; - bindingInit (sys); - } - /* init compiler for this system */ - compilerInit (sys); - - /* transfer command line */ sys->argc = argc; sys->argv = argv; - if (switch_echo->count > 0) - { - /* print command line */ - fprintf (stdout, "command\t"); - commandlinePrint (stdout, sys); - fprintf (stdout, "\n"); - } + process_switches(sys); + // exit (0); // TODO FIX weghalen [x][cc] - /* handle switches */ + /* init compiler for this system */ + compilerInit (sys); - sys->switchRuns = switch_maximum_runs->ival[0]; /* maximum number of runs */ - if (switch_implicit_choose->count > 0) - /* allow implicit chooses */ - sys->switchForceChoose = 0; - if (switch_choose_first->count > 0) - sys->switchChooseFirst = 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; - } - if (switch_enable_symmetry_order->count > 0) - sys->switchSymmOrder = 1; /* enable symmetry order */ - if (switch_disable_agent_symmetries->count > 0) - sys->switchAgentSymm = 0; /* disable agent symmetry order */ - if (switch_disable_noclaims_reductions->count > 0) - sys->switchNomoreClaims = 0; /* disable no more claims cutter */ - if (switch_disable_endgame_reductions->count > 0) - sys->switchReduceEndgame = 0; /* disable endgame cutter */ - if (switch_disable_claim_symmetry->count > 0) - sys->switchReduceClaims = 0; /* disable claim symmetry cutter */ - if (switch_summary->count > 0) - sys->output = SUMMARY; /* report summary on stdout */ - if (switch_proof->count > 0) - sys->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) - { - /* no scenario, but a size is set. so override */ -#ifdef DEBUG - warning ("Scanning scenarios."); -#endif - sys->switchScenario = -1; - } - if (sys->switchScenario < 0) - { - sys->output = SCENARIOS; - } - if (sys->switchScenario != 0 && sys->switchScenarioSize == 0) - { -#ifdef DEBUG - warning - ("Scenario selection without trace prefix length implies --choose-first."); -#endif - sys->switchChooseFirst = 1; - } -#ifdef DEBUG - sys->porparam = switch_por_parameter->ival[0]; -#endif - sys->latex = switch_latex_output->count; sys->know = emptyKnowledge (); - /* parse compiler-dependant switches */ - if (switch_check->count > 0) - { - Term claim; - -#ifdef DEBUG - if (lookup (switch_check->sval[0]) == NULL) - { - globalError++; - warning ("Could not find this string at all in:"); - symbolPrintAll (); - eprintf ("\n"); - globalError--; - } -#endif - claim = findGlobalConstant (switch_check->sval[0]); - if (claim == NULL) - error ("Unknown claim type to check."); - if (inTermlist (claim->stype, TERM_Claim)) - sys->switchClaimToCheck = claim; - else - error ("Claim type to check is not a claim."); - } - /* parse input */ yyparse (); @@ -482,7 +128,7 @@ main (int argc, char **argv) if (sys->engine != ARACHNE_ENGINE) { // Compile as many runs as possible - compile (spdltac, switch_maximum_runs->ival[0]); + compile (spdltac, sys->switchRuns); } else { @@ -519,43 +165,6 @@ main (int argc, char **argv) /* add parameters to system */ - sys->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]; - 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; - else - /* disable progress display */ - sys->switchS = 0; - if (switch_state_space_graph->count > 0) - { - /* enable state space graph output */ - sys->output = STATESPACE; //!< New method - } - if (switch_empty->count > 0) - sys->output = EMPTY; - if (switch_prune_proof_depth->ival[0] >= 0) - sys->switch_maxproofdepth = switch_prune_proof_depth->ival[0]; - if (switch_prune_trace_length->ival[0] >= 0) - sys->switch_maxtracelength = switch_prune_trace_length->ival[0]; - if (switch_goal_select_method->ival[0] >= 0) - sys->switchGoalSelectMethod = 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); -#else - /* non-debug defaults */ - sys->switchM = 0; -#endif /* * --------------------------------------- @@ -568,15 +177,6 @@ main (int argc, char **argv) { error ("Scyther can only generate LaTeX output for attacks."); } - /* Incremental stuff only works for attack locating */ - if (switch_incremental_runs->count > 0 || - switch_incremental_trace_length->count > 0) - { - if (sys->output != ATTACK && sys->output != EMPTY) - { - error ("Incremental traversal only for empty or attack output."); - } - } #ifdef DEBUG if (DEBUGL (4)) { @@ -603,21 +203,7 @@ main (int argc, char **argv) if (DEBUGL (1)) warning ("Start modelchecking system."); #endif - if (switch_incremental_runs->count > 0) - { - MC_incRuns (sys); - } - else - { - if (switch_incremental_trace_length->count > 0) - { - MC_incTraces (sys); - } - else - { - MC_single (sys); - } - } + MC_single (sys); /* * --------------------------------------- @@ -692,7 +278,6 @@ main (int argc, char **argv) exit: /* deallocate each non-null entry in argtable[] */ - arg_free (argtable); return exitcode; } @@ -829,7 +414,7 @@ timersPrint (const System sys) { eprintf ("bounded_proof"); if (cl_scan->timebound) - eprintf ("\ttime=%i", time_limit_seconds); + eprintf ("\ttime=%i", get_time_limit()); } } } diff --git a/src/switches.c b/src/switches.c new file mode 100644 index 0000000..0a2a019 --- /dev/null +++ b/src/switches.c @@ -0,0 +1,477 @@ +/** + *@file switches.c + * \brief Handle command-line options + * + * Contains the main switch handling. + */ + +#include "string.h" +#include "system.h" +#include "debug.h" +#include "version.h" +#include "timer.h" + +extern System sys; + +extern struct tacnode *spdltac; +extern Term TERM_Claim; +extern int mgu_match; + +const char *progname = "scyther"; +const char *releasetag = SVNVERSION; + +//! Process a single switch or generate help text +/** + * When process is false, we just generate the help text. + * + * Yields new index, or -1 when an error occurred. + * When the new index > argc, it should not be called anymore. + * By convention, argc = the number of arguments + 1 + * The index steps through 1..argc-1. + */ +int +switcher (const int process, const System sys, int index) +{ + char *this_arg; // just a shortcut + int argc; + char **argv; + + char *arg_pointer; + int arg_index; + + //! Check whether there are still n options left + int enough_arguments_left (const int n, char shortopt, char *longopt) + { + if (index + n > argc) + { + error ("Option %c [%s] needs at least %i arguments.", shortopt, + longopt, n); + } + return 1; + } + + // Skip over (processed) argument + void arg_next (void) + { + index++; + arg_pointer = argv[index]; + } + + //! Parse an argument into an integer + int integer_argument (void) + { + int result; + + if (arg_pointer == NULL) + { + error ("(Integer) argument expected."); + } + result = 0; + if (sscanf (arg_pointer, "%i", &result) != 1) + { + error ("Could not parse expected integer argument."); + } + arg_next (); + return result; + } + + //! Detect whether this confirms to this option. + /** + * set arg_pointer and index + */ + int detect (char shortopt, char *longopt, int args) + { + arg_pointer = NULL; + + if (!process) + { + // If we are not processing, we always yield true. + return 1; + } + // Is it this option anyway? + if (strlen (this_arg) < 2 || this_arg[0] != '-') + { + // No option + return 0; + } + // Compare + if (this_arg[1] == '-') + { + int optlength; + + // Long variant + optlength = strlen (longopt); + if (strncmp (this_arg + 2, longopt, optlength)) + return 0; + if ((optlength + 2 < strlen (this_arg)) && + this_arg[2 + optlength] == '=') + { + // This has an additional thing! + arg_pointer = this_arg + 2 + optlength + 1; + } + else + { + // arg = next + index++; + arg_pointer = argv[index]; + } + } + else + { + // Short variant + if (strlen (this_arg) < 2 || this_arg[1] != shortopt) + return 0; + if (strlen (this_arg) > 2) + { + // This has an additional thing! + arg_pointer = this_arg + 2; + } + else + { + // arg = next + index++; + arg_pointer = argv[index]; + } + } + // Allright, this is the right option +#ifdef DEBUG + // [x] TODO remove + printf ("%% Detected switch: [%c] %s\n", shortopt, longopt); +#endif + // Enough arguments left? + return enough_arguments_left (args, shortopt, longopt); + } + + //! Align columns + void helptext (const char *left, const char *right) + { + printf (" %-25s %s\n", left, right); + } + + if (process) + { + argc = sys->argc; + argv = sys->argv; +#ifdef DEBUG + // Check range for debug; we trust the non-debug version :) + if (index < 1 || index >= argc) + { + error ("Bad index number %i for argc %i", index, argc); + } +#endif + this_arg = argv[index]; + } + else + { + // Just doing help + this_arg = NULL; + } + + /* + * ------------------------------------------------------------- + * Process the options, one by one + * ------------------------------------------------------------- + */ + + if (detect ('o', "output", 1)) + { + if (!process) + { + helptext ("-o,--output=", "output file [stdout]"); + } + else + { + // Set output file name + /* try to open */ + if (!freopen (arg_pointer, "w", stdout)) + { + fprintf (stderr, "Could not create output file '%s'.\n", + arg_pointer); + exit (1); + } + arg_next (); + return index; + } + } + + if (detect ('T', "timer", 1)) + { + if (!process) + { + helptext ("-T,--timer=", + "maximum time in seconds"); + } + else + { + set_time_limit (integer_argument ()); + return index; + } + } + + if (detect ('r', "max-runs", 1)) + { + if (!process) + { + helptext ("-r,--max-runs=", + "Maximum number of runs in the system"); + } + else + { + sys->switchRuns = integer_argument (); + return index; + } + } + + if (detect ('E', "echo", 0)) + { + if (!process) + { + helptext ("-E,--echo", "echo command line to stdout"); + } + else + { + /* print command line */ + fprintf (stdout, "command\t"); + commandlinePrint (stdout, sys); + fprintf (stdout, "\n"); + return index; + } + } + + if (detect (' ', "summary", 0)) + { + if (!process) + { + helptext ("--summary", "show summary on stdout"); + } + else + { + sys->output = SUMMARY; + return index; + } + } + + if (detect (' ', "state-space", 0)) + { + if (!process) + { + helptext ("--state-space", "output state space graph (modelchecker)"); + } + else + { + sys->output = STATESPACE; + return index; + } + } + + if (detect ('b', "progress-bar", 0)) + { + if (!process) + { + helptext ("-b,--progress-bar", "show progress bar"); + } + else + { + sys->switchS = 50000; + return index; + } + } + + if (detect ('e', "empty", 0)) + { + if (!process) + { + helptext ("-e,--empty", "do not generate output"); + } + else + { + sys->output = EMPTY; + return index; + } + } + + if (detect ('L', "latex", 0)) + { + if (!process) + { + helptext ("-L,--latex", "output attacks in LaTeX format"); + } + else + { + sys->latex = 1; + return index; + } + } + + if (detect ('G', "goal-select", 1)) + { + if (!process) + { + helptext ("-G,--goal-select=", "use goal selection method (default is 3)"); + } + else + { + sys->switchGoalSelectMethod = integer_argument (); + return index; + } + } + + if (detect ('l', "max-length", 1)) + { + if (!process) + { + helptext ("-l,--max-length=", "prune traces longer than events."); + } + else + { + sys->switch_maxtracelength = integer_argument (); + return index; + } + } + + if (detect ('p', "prune", 1)) + { + if (!process) + { + helptext ("-p,--prune", "pruning method"); + } + else + { + sys->prune = integer_argument (); + return index; + } + } + + if (detect ('m', "match", 1)) + { + if (!process) + { + helptext ("-m,--match", "matching method"); + } + else + { + sys->match = integer_argument (); + return index; + } + } + + if (detect ('P', "proof", 0)) + { + if (!process) + { + helptext ("-P,--proof", "construct explicit proof"); + } + else + { + // Proof + sys->output = PROOF; + return index; + } + } + + if (detect ('a', "arachne", 0)) + { + if (!process) + { + helptext ("-a,--arachne", "select Arachne engine"); + } + else + { + // Select arachne engine + sys->engine = ARACHNE_ENGINE; + bindingInit (sys); + return index; + } + } + + if (detect ('v', "version", 0)) + { + if (!process) + helptext ("-v,--version", "version information"); + else + { + printf ("'%s' model checker for security protocols.\n", progname); +#ifdef DEBUG + printf ("Revision %s, compiled with debugging support.\n", + SVNVERSION); +#else + printf ("Revision %s\n", SVNVERSION); +#endif + printf ("December 2003--, Cas Cremers\n"); + exit (0); + } + } + + if (detect ('h', "help", 0)) + { + if (!process) + { + helptext ("-h,--help", "show this help"); + } + else + { + printf ("Usage:\n"); + printf (" %s [switches] [FILE]\nSwitches:\n", progname); + switcher (0, NULL, 0); + exit (0); + } + } + +#ifdef DEBUG + if (detect ('D', "debug", 1)) + { + if (!process) + { + helptext ("-D,--debug=", "set debug (verbosity) level."); + } + else + { + debugSet (integer_argument ()); + return index; + } + } +#endif + + // If the option is not recognized, it means a file name. + if (!process) + { + helptext ("FILE", "input file ('-' for stdin)"); + } + else + { + if (!strcmp (this_arg, "-")) + { + // '-' input: Leave input to stdin + } + else + { + // not '-' input: change stdin to come from this file + if (!freopen (this_arg, "r", stdin)) + { + fprintf (stderr, "Could not open input file '%s'.\n", this_arg); + exit (1); + } + return index + 1; + } + } + return 0; +} + +//! Process switches +void +process_switches (const System sys) +{ + int index; + + if (sys->argc == 1) + { + printf ("Try '%s --help' for more information.\n", progname); + exit (0); + } + + index = 1; + while (index < sys->argc && index > 0) + { + index = switcher (1, sys, index); + } +} diff --git a/src/switches.h b/src/switches.h new file mode 100644 index 0000000..8adca3d --- /dev/null +++ b/src/switches.h @@ -0,0 +1,6 @@ +#ifndef SWITCHES +#define SWITCHES + +void process_switches (const System sys); + +#endif diff --git a/src/system.c b/src/system.c index 127eeda..ec05230 100644 --- a/src/system.c +++ b/src/system.c @@ -76,10 +76,8 @@ systemInit () sys->switchClaims = 0; // default don't report on claims sys->switchClaimToCheck = NULL; // default check all claims sys->switchGoalSelectMethod = 3; // default goal selection method + sys->traverse = 12; // default traversal method - /* set illegal traversal by default, to make sure it is set - later */ - sys->traverse = 0; sys->switch_maxproofdepth = INT_MAX; sys->switch_maxtracelength = INT_MAX; sys->maxtracelength = INT_MAX;