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 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         params->threadsnocleanup = false;
  27 }
  28
  29 static void print_usage(const char *program_name, struct model_params *params)
  30 {
  31         ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
  32         /* Reset defaults before printing */
  33         param_defaults(params);
  34
  35         model_print(
  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"
  39                 "\n"
  40                 "Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n"
  41                 "\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"
  44                 "\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"
  49                 "                              3 is noisier.\n"
  50                 "                              Default: %d\n"
  51                 "-u, --uninitialized=VALUE   Return VALUE any load which may read from an\n"
  52                 "                              uninitialized atomic.\n"
  53                 "                              Default: %u\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"
  57                 "                            Default: %u\n"
  58                 "                            -o help for a list of options\n"
  59                 "-n                          No fork\n"
  60 #ifdef TLS
  61                 "-d                          Don't allow threads to cleanup\n"
  62 #endif
  63                 " --                         Program arguments follow.\n\n",
  64                 program_name,
  65                 params->verbose,
  66                 params->uninitvalue,
  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());
  72         }
  73         exit(EXIT_SUCCESS);
  74 }
  75
  76 bool install_plugin(char * name) {
  77         ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
  78         ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
  79
  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);
  84                         return false;
  85                 }
  86         }
  87         model_print("Analysis %s Not Found\n", name);
  88         return true;
  89 }
  90
  91 static void parse_options(struct model_params *params, int argc, char **argv)
  92 {
  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 */
 102         };
 103         int opt, longindex;
 104         bool error = false;
 105         while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
 106                 switch (opt) {
 107                 case 'h':
 108                         print_usage(argv[0], params);
 109                         break;
 110                 case 'd':
 111                         params->threadsnocleanup = true;
 112                         break;
 113                 case 'n':
 114                         params->nofork = true;
 115                         break;
 116                 case 'x':
 117                         params->maxexecutions = atoi(optarg);
 118                         break;
 119                 case 'v':
 120                         params->verbose = optarg ? atoi(optarg) : 1;
 121                         break;
 122                 case 'u':
 123                         params->uninitvalue = atoi(optarg);
 124                         break;
 125                 case 't':
 126                         if (install_plugin(optarg))
 127                                 error = true;
 128                         break;
 129                 case 'o':
 130                 {
 131                         ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
 132                         if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
 133                                 error = true;
 134                 }
 135                 break;
 136                 default:        /* '?' */
 137                         error = true;
 138                         break;
 139                 }
 140         }
 141
 142         /* Pass remaining arguments to user program */
 143         params->argc = argc - (optind - 1);
 144         params->argv = argv + (optind - 1);
 145
 146         /* Reset program name */
 147         params->argv[0] = argv[0];
 148
 149         /* Reset (global) optind for potential use by user program */
 150         optind = 1;
 151
 152         if (error)
 153                 print_usage(argv[0], params);
 154 }
 155
 156 int main_argc;
 157 char **main_argv;
 158
 159 static void install_trace_analyses(ModelExecution *execution)
 160 {
 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();
 168         }
 169 }
 170
 171 /**
 172  * Main function.  Just initializes snapshotting library and the
 173  * snapshotting library calls the model_main function.
 174  */
 175 int main(int argc, char **argv)
 176 {
 177         main_argc = argc;
 178         main_argv = argv;
 179
 180         /*
 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.
 185          */
 186
 187         printf("C11Tester\n"
 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");
 191
 192
 193         //Initialize snapshotting library and model checker object
 194         if (!model) {
 195                 snapshot_system_init(10000, 1024, 1024, 40000);
 196                 model = new ModelChecker();
 197                 model->startChecker();
 198         }
 199
 200         /* Configure output redirection for the model-checker */
 201         redirect_output();
 202
 203         register_plugins();
 204
 205         //Parse command line options
 206         model_params *params = model->getParams();
 207         parse_options(params, main_argc, main_argv);
 208
 209
 210         install_trace_analyses(model->get_execution());
 211
 212         model->startMainThread();
 213         DEBUG("Exiting\n");
 214 }