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(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: [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                 params->verbose,
  65                 params->uninitvalue,
  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());
  71         }
  72         exit(EXIT_SUCCESS);
  73 }
  74
  75 bool install_plugin(char * name) {
  76         ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
  77         ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
  78
  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);
  83                         return false;
  84                 }
  85         }
  86         model_print("Analysis %s Not Found\n", name);
  87         return true;
  88 }
  89
  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 */
 100         };
 101         int opt, longindex;
 102         int tmpoptind = optind;
 103         bool error = false;
 104         char * options = getenv("C11TESTER");
 105
 106         if (options == NULL)
 107                 return;
 108         int argc = 1;
 109         for(int index = 0;options[index]!=0;index++) {
 110                 if (options[index] == ' ')
 111                         argc++;
 112         }
 113         argc++; //first parameter is executable name
 114         char * argv[argc + 1];
 115         argv[0] = NULL;
 116         argv[1] = options;
 117         for(int index = 0, count = 2;options[index]!=0;index++) {
 118                 if (options[index]==' ')
 119                         argv[count++] = &options[index];
 120         }
 121
 122         while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
 123                 switch (opt) {
 124                 case 'h':
 125                         print_usage(params);
 126                         break;
 127                 case 'd':
 128                         params->threadsnocleanup = true;
 129                         break;
 130                 case 'n':
 131                         params->nofork = true;
 132                         break;
 133                 case 'x':
 134                         params->maxexecutions = atoi(optarg);
 135                         break;
 136                 case 'v':
 137                         params->verbose = optarg ? atoi(optarg) : 1;
 138                         break;
 139                 case 'u':
 140                         params->uninitvalue = atoi(optarg);
 141                         break;
 142                 case 't':
 143                         if (install_plugin(optarg))
 144                                 error = true;
 145                         break;
 146                 case 'o':
 147                 {
 148                         ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
 149                         if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
 150                                 error = true;
 151                 }
 152                 break;
 153                 default:        /* '?' */
 154                         error = true;
 155                         break;
 156                 }
 157         }
 158
 159         /* Restore (global) optind for potential use by user program */
 160         optind = tmpoptind;
 161
 162         if (error)
 163                 print_usage(params);
 164 }
 165
 166 static void install_trace_analyses(ModelExecution *execution)
 167 {
 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();
 175         }
 176 }
 177
 178 /**
 179  * Main function.  Just initializes snapshotting library and the
 180  * snapshotting library calls the model_main function.
 181  */
 182 int main(int argc, char **argv)
 183 {
 184         /*
 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.
 189          */
 190
 191         printf("C11Tester\n"
 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");
 195
 196
 197         //Initialize snapshotting library and model checker object
 198         if (!model) {
 199                 snapshot_system_init(10000, 1024, 1024, 40000);
 200                 model = new ModelChecker();
 201                 model->startChecker();
 202         }
 203
 204         /* Configure output redirection for the model-checker */
 205         redirect_output();
 206         register_plugins();
 207
 208         //Stash command line options
 209         model_params *params = model->getParams();
 210         params->argc = argc;
 211         params->argv = argv;
 212
 213         install_trace_analyses(model->get_execution());
 214
 215         model->startMainThread();
 216         DEBUG("Exiting\n");
 217 }