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;
26 params->threadsnocleanup = false;
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 "-v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:\n"
48 " 0 is quiet; 1 shows valid executions; 2 is noisy;\n"
51 "-u, --uninitialized=VALUE Return VALUE any load which may read from an\n"
52 " uninitialized atomic.\n"
54 "-t, --analysis=NAME Use Analysis Plugin.\n"
55 "-o, --options=NAME Option for previous analysis plugin. \n"
56 "-x, --maxexec=NUM Maximum number of executions.\n"
58 " -o help for a list of options\n"
61 "-d Don't allow threads to cleanup\n"
63 " -- Program arguments follow.\n\n",
67 params->maxexecutions);
68 model_print("Analysis plugins:\n");
69 for(unsigned int i=0;i<registeredanalysis->size();i++) {
70 TraceAnalysis * analysis=(*registeredanalysis)[i];
71 model_print("%s\n", analysis->name());
76 bool install_plugin(char * name) {
77 ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
78 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
80 for(unsigned int i=0;i<registeredanalysis->size();i++) {
81 TraceAnalysis * analysis=(*registeredanalysis)[i];
82 if (strcmp(name, analysis->name())==0) {
83 installedanalysis->push_back(analysis);
87 model_print("Analysis %s Not Found\n", name);
91 static void parse_options(struct model_params *params, int argc, char **argv)
93 const char *shortopts = "hdnt:o:u:x:v::";
94 const struct option longopts[] = {
95 {"help", no_argument, NULL, 'h'},
96 {"verbose", optional_argument, NULL, 'v'},
97 {"uninitialized", required_argument, NULL, 'u'},
98 {"analysis", required_argument, NULL, 't'},
99 {"options", required_argument, NULL, 'o'},
100 {"maxexecutions", required_argument, NULL, 'x'},
101 {0, 0, 0, 0} /* Terminator */
105 while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
108 print_usage(argv[0], params);
111 params->threadsnocleanup = true;
114 params->nofork = true;
117 params->maxexecutions = atoi(optarg);
120 params->verbose = optarg ? atoi(optarg) : 1;
123 params->uninitvalue = atoi(optarg);
126 if (install_plugin(optarg))
131 ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
132 if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
142 /* Pass remaining arguments to user program */
143 params->argc = argc - (optind - 1);
144 params->argv = argv + (optind - 1);
146 /* Reset program name */
147 params->argv[0] = argv[0];
149 /* Reset (global) optind for potential use by user program */
153 print_usage(argv[0], params);
159 static void install_trace_analyses(ModelExecution *execution)
161 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
162 for(unsigned int i=0;i<installedanalysis->size();i++) {
163 TraceAnalysis * ta=(*installedanalysis)[i];
164 ta->setExecution(execution);
165 model->add_trace_analysis(ta);
166 /** Call the installation event for each installed plugin */
167 ta->actionAtInstallation();
172 * Main function. Just initializes snapshotting library and the
173 * snapshotting library calls the model_main function.
175 int main(int argc, char **argv)
181 * If this printf statement is removed, C11Tester will fail on an
182 * assert on some versions of glibc. The first time printf is
183 * called, it allocated internal buffers. We can't easily snapshot
184 * libc since we also use it.
188 "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n"
189 "Distributed under the GPLv2\n"
190 "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
193 //Initialize snapshotting library and model checker object
195 snapshot_system_init(10000, 1024, 1024, 40000);
196 model = new ModelChecker();
197 model->startChecker();
200 /* Configure output redirection for the model-checker */
205 //Parse command line options
206 model_params *params = model->getParams();
207 parse_options(params, main_argc, main_argv);
210 install_trace_analyses(model->get_execution());
212 model->startMainThread();