2 * @brief Entry point for the model checker.
14 /* global "model" object */
17 #include "snapshot-interface.h"
20 static void param_defaults(struct model_params *params)
22 params->enabledcount = 1;
24 params->verbose = !!DBG_ENABLED();
25 params->uninitvalue = 0;
26 params->maxexecutions = 0;
29 static void print_usage(const char *program_name, struct model_params *params)
31 ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
32 /* Reset defaults before printing */
33 param_defaults(params);
36 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
37 "Distributed under the GPLv2\n"
38 "Written by Brian Norris and Brian Demsky\n"
40 "Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n"
42 "MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n"
43 "provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n"
45 "Model-checker options:\n"
46 "-h, --help Display this help message and exit\n"
47 "-e, --enabled=COUNT Enabled count.\n"
49 "-b, --bound=MAX Upper length bound.\n"
51 "-v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:\n"
52 " 0 is quiet; 1 shows valid executions; 2 is noisy;\n"
55 "-u, --uninitialized=VALUE Return VALUE any load which may read from an\n"
56 " uninitialized atomic.\n"
58 "-t, --analysis=NAME Use Analysis Plugin.\n"
59 "-o, --options=NAME Option for previous analysis plugin. \n"
60 "-x, --maxexec=NUM Maximum number of executions.\n"
62 " -o help for a list of options\n"
63 " -- Program arguments follow.\n\n",
69 params->maxexecutions);
70 model_print("Analysis plugins:\n");
71 for(unsigned int i=0;i<registeredanalysis->size();i++) {
72 TraceAnalysis * analysis=(*registeredanalysis)[i];
73 model_print("%s\n", analysis->name());
78 bool install_plugin(char * name) {
79 ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
80 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
82 for(unsigned int i=0;i<registeredanalysis->size();i++) {
83 TraceAnalysis * analysis=(*registeredanalysis)[i];
84 if (strcmp(name, analysis->name())==0) {
85 installedanalysis->push_back(analysis);
89 model_print("Analysis %s Not Found\n", name);
93 static void parse_options(struct model_params *params, int argc, char **argv)
95 const char *shortopts = "ht:o:e:b:u:x:v::";
96 const struct option longopts[] = {
97 {"help", no_argument, NULL, 'h'},
98 {"enabled", required_argument, NULL, 'e'},
99 {"bound", required_argument, NULL, 'b'},
100 {"verbose", optional_argument, NULL, 'v'},
101 {"uninitialized", required_argument, NULL, 'u'},
102 {"analysis", required_argument, NULL, 't'},
103 {"options", required_argument, NULL, 'o'},
104 {"maxexecutions", required_argument, NULL, 'x'},
105 {0, 0, 0, 0} /* Terminator */
109 while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
112 print_usage(argv[0], params);
115 params->maxexecutions = atoi(optarg);
118 params->enabledcount = atoi(optarg);
121 params->bound = atoi(optarg);
124 params->verbose = optarg ? atoi(optarg) : 1;
127 params->uninitvalue = atoi(optarg);
130 if (install_plugin(optarg))
135 ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
136 if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
146 /* Pass remaining arguments to user program */
147 params->argc = argc - (optind - 1);
148 params->argv = argv + (optind - 1);
150 /* Reset program name */
151 params->argv[0] = argv[0];
153 /* Reset (global) optind for potential use by user program */
157 print_usage(argv[0], params);
163 static void install_trace_analyses(ModelExecution *execution)
165 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
166 for(unsigned int i=0;i<installedanalysis->size();i++) {
167 TraceAnalysis * ta=(*installedanalysis)[i];
168 ta->setExecution(execution);
169 model->add_trace_analysis(ta);
170 /** Call the installation event for each installed plugin */
171 ta->actionAtInstallation();
175 /** The model_main function contains the main model checking loop. */
176 static void model_main()
178 struct model_params params;
180 param_defaults(¶ms);
183 parse_options(¶ms, main_argc, main_argv);
185 //Initialize race detector
188 snapshot_stack_init();
190 model = new ModelChecker(params);
191 install_trace_analyses(model->get_execution());
201 * Main function. Just initializes snapshotting library and the
202 * snapshotting library calls the model_main function.
204 int main(int argc, char **argv)
210 * If this printf statement is removed, CDSChecker will fail on an
211 * assert on some versions of glibc. The first time printf is
212 * called, it allocated internal buffers. We can't easily snapshot
213 * libc since we also use it.
216 printf("CDSChecker\n"
217 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
218 "Distributed under the GPLv2\n"
219 "Written by Brian Norris and Brian Demsky\n\n");
221 /* Configure output redirection for the model-checker */
224 /* Let's jump in quickly and start running stuff */
225 snapshot_system_init(10000, 1024, 1024, 4000, &model_main);