X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=main.cc;h=502f499eff9cb2de956256bb6f24b84080e600e0;hb=refs%2Fheads%2Fmaster;hp=0ca78b97a8ced2e2cd9e9188386415f0d6192997;hpb=85d19a94bbe42390e82837ba75df5c39211a26f5;p=model-checker.git diff --git a/main.cc b/main.cc index 0ca78b9..502f499 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,17 +25,18 @@ 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; params->expireslop = 4; params->verbose = !!DBG_ENABLED(); params->uninitvalue = 0; + params->maxexecutions = 0; } static void print_usage(const char *program_name, struct model_params *params) { + ModelVector * registeredanalysis=getRegisteredTraceAnalysis(); /* Reset defaults before printing */ param_defaults(params); @@ -44,7 +47,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 +64,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 +77,18 @@ 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 shows valid executions; 2 is noisy;\n" +" 3 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" +"-x, --maxexec=NUM Maximum number of executions.\n" +" Default: %u\n" +" -o help for a list of options\n" " -- Program arguments follow.\n\n", program_name, params->maxreads, @@ -89,13 +100,35 @@ static void print_usage(const char *program_name, struct model_params *params) params->fairwindow, params->enabledcount, params->bound, - params->uninitvalue); + params->verbose, + params->uninitvalue, + params->maxexecutions); + 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:x:v::"; const struct option longopts[] = { {"help", no_argument, NULL, 'h'}, {"liveness", required_argument, NULL, 'm'}, @@ -108,8 +141,10 @@ static void parse_options(struct model_params *params, int argc, char **argv) {"enabled", required_argument, NULL, 'e'}, {"bound", required_argument, NULL, 'b'}, {"verbose", optional_argument, NULL, 'v'}, - {"uninitialized", optional_argument, NULL, 'u'}, - {"analysis", optional_argument, NULL, 'c'}, + {"uninitialized", required_argument, NULL, 'u'}, + {"analysis", required_argument, NULL, 't'}, + {"options", required_argument, NULL, 'o'}, + {"maxexecutions", required_argument, NULL, 'x'}, {0, 0, 0, 0} /* Terminator */ }; int opt, longindex; @@ -119,6 +154,9 @@ static void parse_options(struct model_params *params, int argc, char **argv) case 'h': print_usage(argv[0], params); break; + case 'x': + params->maxexecutions = atoi(optarg); + break; case 's': params->maxfuturedelay = atoi(optarg); break; @@ -146,12 +184,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 +224,16 @@ 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); + /** Call the installation event for each installed plugin */ + ta->actionAtInstallation(); + } } /** The model_main function contains the main model checking loop. */ @@ -190,6 +242,7 @@ static void model_main() struct model_params params; param_defaults(¶ms); + register_plugins(); parse_options(¶ms, main_argc, main_argv); @@ -217,6 +270,18 @@ int main(int argc, char **argv) main_argc = argc; main_argv = argv; + /* + * If this printf statement is removed, CDSChecker will fail on an + * assert on some versions of glibc. The first time printf is + * called, it allocated internal buffers. We can't easily snapshot + * libc since we also use it. + */ + + printf("CDSChecker\n" + "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n" + "Distributed under the GPLv2\n" + "Written by Brian Norris and Brian Demsky\n\n"); + /* Configure output redirection for the model-checker */ redirect_output();