2 * @brief Entry point for the model checker.
14 /* global "model" object */
17 #include "snapshot-interface.h"
20 void param_defaults(struct model_params *params)
22 params->verbose = !!DBG_ENABLED();
23 params->uninitvalue = 0;
24 params->maxexecutions = 10;
25 params->nofork = false;
28 static void print_usage(const char *program_name, struct model_params *params)
30 ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
31 /* Reset defaults before printing */
32 param_defaults(params);
35 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
36 "Distributed under the GPLv2\n"
37 "Written by Brian Norris and Brian Demsky\n"
39 "Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n"
41 "MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n"
42 "provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n"
44 "Model-checker options:\n"
45 "-h, --help Display this help message and exit\n"
46 "-v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:\n"
47 " 0 is quiet; 1 shows valid executions; 2 is noisy;\n"
50 "-u, --uninitialized=VALUE Return VALUE any load which may read from an\n"
51 " uninitialized atomic.\n"
53 "-t, --analysis=NAME Use Analysis Plugin.\n"
54 "-o, --options=NAME Option for previous analysis plugin. \n"
55 "-x, --maxexec=NUM Maximum number of executions.\n"
57 " -o help for a list of options\n"
59 " -- Program arguments follow.\n\n",
63 params->maxexecutions);
64 model_print("Analysis plugins:\n");
65 for(unsigned int i=0;i<registeredanalysis->size();i++) {
66 TraceAnalysis * analysis=(*registeredanalysis)[i];
67 model_print("%s\n", analysis->name());
72 bool install_plugin(char * name) {
73 ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
74 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
76 for(unsigned int i=0;i<registeredanalysis->size();i++) {
77 TraceAnalysis * analysis=(*registeredanalysis)[i];
78 if (strcmp(name, analysis->name())==0) {
79 installedanalysis->push_back(analysis);
83 model_print("Analysis %s Not Found\n", name);
87 static void parse_options(struct model_params *params, int argc, char **argv)
89 const char *shortopts = "hnt:o:u:x:v::";
90 const struct option longopts[] = {
91 {"help", no_argument, NULL, 'h'},
92 {"verbose", optional_argument, NULL, 'v'},
93 {"uninitialized", required_argument, NULL, 'u'},
94 {"analysis", required_argument, NULL, 't'},
95 {"options", required_argument, NULL, 'o'},
96 {"maxexecutions", required_argument, NULL, 'x'},
97 {0, 0, 0, 0} /* Terminator */
101 while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
104 print_usage(argv[0], params);
107 params->nofork = true;
110 params->maxexecutions = atoi(optarg);
113 params->verbose = optarg ? atoi(optarg) : 1;
116 params->uninitvalue = atoi(optarg);
119 if (install_plugin(optarg))
124 ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
125 if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
135 /* Pass remaining arguments to user program */
136 params->argc = argc - (optind - 1);
137 params->argv = argv + (optind - 1);
139 /* Reset program name */
140 params->argv[0] = argv[0];
142 /* Reset (global) optind for potential use by user program */
146 print_usage(argv[0], params);
152 static void install_trace_analyses(ModelExecution *execution)
154 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
155 for(unsigned int i=0;i<installedanalysis->size();i++) {
156 TraceAnalysis * ta=(*installedanalysis)[i];
157 ta->setExecution(execution);
158 model->add_trace_analysis(ta);
159 /** Call the installation event for each installed plugin */
160 ta->actionAtInstallation();
164 /** The model_main function contains the main model checking loop. */
165 static void model_main()
175 * Main function. Just initializes snapshotting library and the
176 * snapshotting library calls the model_main function.
178 int main(int argc, char **argv)
184 * If this printf statement is removed, CDSChecker will fail on an
185 * assert on some versions of glibc. The first time printf is
186 * called, it allocated internal buffers. We can't easily snapshot
187 * libc since we also use it.
190 printf("CDSChecker\n"
191 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
192 "Distributed under the GPLv2\n"
193 "Written by Brian Norris and Brian Demsky\n\n");
195 /* Configure output redirection for the model-checker */
198 //Initialize snapshotting library and model checker object
200 snapshot_system_init(10000, 1024, 1024, 40000);
201 model = new ModelChecker();
206 //Parse command line options
207 model_params *params = model->getParams();
208 parse_options(params, main_argc, main_argv);
210 //Initialize race detector
213 snapshot_stack_init();
214 install_trace_analyses(model->get_execution());
216 //Start everything up
217 modelchecker_started = true;
218 startExecution(&model_main);