X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=main.cc;h=d489d96eb459b5263d6d8a4032e31f39c28127c9;hp=0ca78b97a8ced2e2cd9e9188386415f0d6192997;hb=2d0d4ac38e05905a6633b3f2d5112ccadd45c27f;hpb=85d19a94bbe42390e82837ba75df5c39211a26f5 diff --git a/main.cc b/main.cc index 0ca78b9..d489d96 100644 --- a/main.cc +++ b/main.cc @@ -4,6 +4,7 @@ #include #include +#include #include "common.h" #include "output.h" @@ -15,6 +16,7 @@ #include "params.h" #include "snapshot-interface.h" #include "scanalysis.h" +#include "plugins.h" static void param_defaults(struct model_params *params) { @@ -23,7 +25,6 @@ static void param_defaults(struct model_params *params) params->fairwindow = 0; params->yieldon = false; params->yieldblock = false; - params->sc_trace_analysis = false; params->enabledcount = 1; params->bound = 0; params->maxfuturevalues = 0; @@ -34,6 +35,7 @@ static void param_defaults(struct model_params *params) static void print_usage(const char *program_name, struct model_params *params) { + ModelVector * registeredanalysis=getRegisteredTraceAnalysis(); /* Reset defaults before printing */ param_defaults(params); @@ -44,7 +46,7 @@ static void print_usage(const char *program_name, struct model_params *params) "\n" "Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n" "\n" -"MODLE-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n" +"MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n" "provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n" "\n" "Model-checker options:\n" @@ -61,7 +63,8 @@ static void print_usage(const char *program_name, struct model_params *params) " Default: %d\n" "-S, --fvslop=NUM Future value expiration sloppiness.\n" " Default: %u\n" -"-y, --yield Enable CHESS-like yield-based fairness support.\n" +"-y, --yield Enable CHESS-like yield-based fairness support\n" +" (requires thrd_yield() in test program).\n" " Default: %s\n" "-Y, --yieldblock Prohibit an execution from running a yield.\n" " Default: %s\n" @@ -73,11 +76,15 @@ static void print_usage(const char *program_name, struct model_params *params) " Default: %d\n" "-b, --bound=MAX Upper length bound.\n" " Default: %d\n" -"-v, --verbose Print verbose execution information.\n" +"-v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:\n" +" 0 is quiet; 1 is noisy; 2 is noisier.\n" +" Default: %d\n" "-u, --uninitialized=VALUE Return VALUE any load which may read from an\n" " uninitialized atomic.\n" " Default: %u\n" -"-c, --analysis Use SC Trace Analysis.\n" +"-t, --analysis=NAME Use Analysis Plugin.\n" +"-o, --options=NAME Option for previous analysis plugin. \n" +" -o help for a list of options\n" " -- Program arguments follow.\n\n", program_name, params->maxreads, @@ -89,13 +96,34 @@ static void print_usage(const char *program_name, struct model_params *params) params->fairwindow, params->enabledcount, params->bound, + params->verbose, params->uninitvalue); + model_print("Analysis plugins:\n"); + for(unsigned int i=0;isize();i++) { + TraceAnalysis * analysis=(*registeredanalysis)[i]; + model_print("%s\n", analysis->name()); + } exit(EXIT_SUCCESS); } +bool install_plugin(char * name) { + ModelVector * registeredanalysis=getRegisteredTraceAnalysis(); + ModelVector * installedanalysis=getInstalledTraceAnalysis(); + + for(unsigned int i=0;isize();i++) { + TraceAnalysis * analysis=(*registeredanalysis)[i]; + if (strcmp(name, analysis->name())==0) { + installedanalysis->push_back(analysis); + return false; + } + } + model_print("Analysis %s Not Found\n", name); + return true; +} + static void parse_options(struct model_params *params, int argc, char **argv) { - const char *shortopts = "hyYcm:M:s:S:f:e:b:u:v::"; + const char *shortopts = "hyYt:o:m:M:s:S:f:e:b:u:v::"; const struct option longopts[] = { {"help", no_argument, NULL, 'h'}, {"liveness", required_argument, NULL, 'm'}, @@ -109,7 +137,8 @@ static void parse_options(struct model_params *params, int argc, char **argv) {"bound", required_argument, NULL, 'b'}, {"verbose", optional_argument, NULL, 'v'}, {"uninitialized", optional_argument, NULL, 'u'}, - {"analysis", optional_argument, NULL, 'c'}, + {"analysis", optional_argument, NULL, 't'}, + {"options", optional_argument, NULL, 'o'}, {0, 0, 0, 0} /* Terminator */ }; int opt, longindex; @@ -146,12 +175,20 @@ static void parse_options(struct model_params *params, int argc, char **argv) case 'u': params->uninitvalue = atoi(optarg); break; - case 'c': - params->sc_trace_analysis = true; - break; case 'y': params->yieldon = true; break; + case 't': + if (install_plugin(optarg)) + error = true; + break; + case 'o': + { + ModelVector * analyses = getInstalledTraceAnalysis(); + if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg)) + error = true; + } + break; case 'Y': params->yieldblock = true; break; @@ -178,10 +215,14 @@ static void parse_options(struct model_params *params, int argc, char **argv) int main_argc; char **main_argv; -static void install_trace_analyses(const ModelExecution *execution) +static void install_trace_analyses(ModelExecution *execution) { - if (model->params.sc_trace_analysis) - model->add_trace_analysis(new SCAnalysis(execution)); + ModelVector * installedanalysis=getInstalledTraceAnalysis(); + for(unsigned int i=0;isize();i++) { + TraceAnalysis * ta=(*installedanalysis)[i]; + ta->setExecution(execution); + model->add_trace_analysis(ta); + } } /** The model_main function contains the main model checking loop. */ @@ -190,6 +231,7 @@ static void model_main() struct model_params params; param_defaults(¶ms); + register_plugins(); parse_options(¶ms, main_argc, main_argv);