0abc80b7e766063c5b3304be14d3a86dbc049045
[c11tester.git] / main.cc
1 /** @file main.cc
2  *  @brief Entry point for the model checker.
3  */
4
5 #include <unistd.h>
6 #include <getopt.h>
7 #include <string.h>
8
9 #include "common.h"
10 #include "output.h"
11
12 #include "datarace.h"
13
14 /* global "model" object */
15 #include "model.h"
16 #include "params.h"
17 #include "snapshot-interface.h"
18 #include "plugins.h"
19
20 static void param_defaults(struct model_params *params)
21 {
22         params->verbose = !!DBG_ENABLED();
23         params->uninitvalue = 0;
24         params->maxexecutions = 10;
25         params->nofork = false;
26 }
27
28 static void print_usage(const char *program_name, struct model_params *params)
29 {
30         ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
31         /* Reset defaults before printing */
32         param_defaults(params);
33
34         model_print(
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"
38                 "\n"
39                 "Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n"
40                 "\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"
43                 "\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"
48                 "                              3 is noisier.\n"
49                 "                              Default: %d\n"
50                 "-u, --uninitialized=VALUE   Return VALUE any load which may read from an\n"
51                 "                              uninitialized atomic.\n"
52                 "                              Default: %u\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"
56                 "                            Default: %u\n"
57                 "                            -o help for a list of options\n"
58                 "-n                          No fork\n"
59                 " --                         Program arguments follow.\n\n",
60                 program_name,
61                 params->verbose,
62                 params->uninitvalue,
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());
68         }
69         exit(EXIT_SUCCESS);
70 }
71
72 bool install_plugin(char * name) {
73         ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
74         ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
75
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);
80                         return false;
81                 }
82         }
83         model_print("Analysis %s Not Found\n", name);
84         return true;
85 }
86
87 static void parse_options(struct model_params *params, int argc, char **argv)
88 {
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 */
98         };
99         int opt, longindex;
100         bool error = false;
101         while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
102                 switch (opt) {
103                 case 'h':
104                         print_usage(argv[0], params);
105                         break;
106                 case 'n':
107                         params->nofork = true;
108                         break;
109                 case 'x':
110                         params->maxexecutions = atoi(optarg);
111                         break;
112                 case 'v':
113                         params->verbose = optarg ? atoi(optarg) : 1;
114                         break;
115                 case 'u':
116                         params->uninitvalue = atoi(optarg);
117                         break;
118                 case 't':
119                         if (install_plugin(optarg))
120                                 error = true;
121                         break;
122                 case 'o':
123                 {
124                         ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
125                         if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
126                                 error = true;
127                 }
128                 break;
129                 default:        /* '?' */
130                         error = true;
131                         break;
132                 }
133         }
134
135         /* Pass remaining arguments to user program */
136         params->argc = argc - (optind - 1);
137         params->argv = argv + (optind - 1);
138
139         /* Reset program name */
140         params->argv[0] = argv[0];
141
142         /* Reset (global) optind for potential use by user program */
143         optind = 1;
144
145         if (error)
146                 print_usage(argv[0], params);
147 }
148
149 int main_argc;
150 char **main_argv;
151
152 static void install_trace_analyses(ModelExecution *execution)
153 {
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();
161         }
162 }
163
164 /** The model_main function contains the main model checking loop. */
165 static void model_main()
166 {
167         struct model_params params;
168
169         param_defaults(&params);
170         register_plugins();
171
172         parse_options(&params, main_argc, main_argv);
173
174         //Initialize race detector
175         initRaceDetector();
176
177         snapshot_stack_init();
178
179         if (!model)
180                 model = new ModelChecker();
181         model->setParams(params);
182         install_trace_analyses(model->get_execution());
183
184         snapshot_record(0);
185         model->run();
186         delete model;
187
188         DEBUG("Exiting\n");
189 }
190
191 /**
192  * Main function.  Just initializes snapshotting library and the
193  * snapshotting library calls the model_main function.
194  */
195 int main(int argc, char **argv)
196 {
197         main_argc = argc;
198         main_argv = argv;
199
200         /*
201          * If this printf statement is removed, CDSChecker will fail on an
202          * assert on some versions of glibc.  The first time printf is
203          * called, it allocated internal buffers.  We can't easily snapshot
204          * libc since we also use it.
205          */
206
207         printf("CDSChecker\n"
208                                  "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
209                                  "Distributed under the GPLv2\n"
210                                  "Written by Brian Norris and Brian Demsky\n\n");
211
212         /* Configure output redirection for the model-checker */
213         redirect_output();
214
215         /* Let's jump in quickly and start running stuff */
216         snapshot_system_init(10000, 1024, 1024, 40000, &model_main);
217 }