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(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: [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",
66 params->maxexecutions);
67 model_print("Analysis plugins:\n");
68 for(unsigned int i=0;i<registeredanalysis->size();i++) {
69 TraceAnalysis * analysis=(*registeredanalysis)[i];
70 model_print("%s\n", analysis->name());
75 bool install_plugin(char * name) {
76 ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
77 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
79 for(unsigned int i=0;i<registeredanalysis->size();i++) {
80 TraceAnalysis * analysis=(*registeredanalysis)[i];
81 if (strcmp(name, analysis->name())==0) {
82 installedanalysis->push_back(analysis);
86 model_print("Analysis %s Not Found\n", name);
90 void parse_options(struct model_params *params) {
91 const char *shortopts = "hdnt:o:u:x:v::";
92 const struct option longopts[] = {
93 {"help", no_argument, NULL, 'h'},
94 {"verbose", optional_argument, NULL, 'v'},
95 {"uninitialized", required_argument, NULL, 'u'},
96 {"analysis", required_argument, NULL, 't'},
97 {"options", required_argument, NULL, 'o'},
98 {"maxexecutions", required_argument, NULL, 'x'},
99 {0, 0, 0, 0} /* Terminator */
102 int tmpoptind = optind;
104 char * options = getenv("C11TESTER");
109 for(int index = 0;options[index]!=0;index++) {
110 if (options[index] == ' ')
113 argc++; //first parameter is executable name
114 char * argv[argc + 1];
117 for(int index = 0, count = 2;options[index]!=0;index++) {
118 if (options[index]==' ')
119 argv[count++] = &options[index];
122 while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
128 params->threadsnocleanup = true;
131 params->nofork = true;
134 params->maxexecutions = atoi(optarg);
137 params->verbose = optarg ? atoi(optarg) : 1;
140 params->uninitvalue = atoi(optarg);
143 if (install_plugin(optarg))
148 ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
149 if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
159 /* Restore (global) optind for potential use by user program */
166 static void install_trace_analyses(ModelExecution *execution)
168 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
169 for(unsigned int i=0;i<installedanalysis->size();i++) {
170 TraceAnalysis * ta=(*installedanalysis)[i];
171 ta->setExecution(execution);
172 model->add_trace_analysis(ta);
173 /** Call the installation event for each installed plugin */
174 ta->actionAtInstallation();
179 * Main function. Just initializes snapshotting library and the
180 * snapshotting library calls the model_main function.
182 int main(int argc, char **argv)
185 * If this printf statement is removed, C11Tester will fail on an
186 * assert on some versions of glibc. The first time printf is
187 * called, it allocated internal buffers. We can't easily snapshot
188 * libc since we also use it.
192 "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n"
193 "Distributed under the GPLv2\n"
194 "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
197 //Initialize snapshotting library and model checker object
199 snapshot_system_init(10000, 1024, 1024, 40000);
200 model = new ModelChecker();
201 model->startChecker();
204 /* Configure output redirection for the model-checker */
208 //Stash command line options
209 model_params *params = model->getParams();
213 install_trace_analyses(model->get_execution());
215 model->startMainThread();