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 }
  27
  28 static void print_usage(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: C11TESTER=[MODEL-CHECKER OPTIONS]\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\n"
  59                 params->verbose,
  60                 params->uninitvalue,
  61                 params->maxexecutions);
  62         model_print("Analysis plugins:\n");
  63         for(unsigned int i=0;i<registeredanalysis->size();i++) {
  64                 TraceAnalysis * analysis=(*registeredanalysis)[i];
  65                 model_print("%s\n", analysis->name());
  66         }
  67         exit(EXIT_SUCCESS);
  68 }
  69
  70 bool install_plugin(char * name) {
  71         ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
  72         ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
  73
  74         for(unsigned int i=0;i<registeredanalysis->size();i++) {
  75                 TraceAnalysis * analysis=(*registeredanalysis)[i];
  76                 if (strcmp(name, analysis->name())==0) {
  77                         installedanalysis->push_back(analysis);
  78                         return false;
  79                 }
  80         }
  81         model_print("Analysis %s Not Found\n", name);
  82         return true;
  83 }
  84
  85 void parse_options(struct model_params *params) {
  86         const char *shortopts = "hnt:o:u:x:v::";
  87         const struct option longopts[] = {
  88                 {"help", no_argument, NULL, 'h'},
  89                 {"verbose", optional_argument, NULL, 'v'},
  90                 {"uninitialized", required_argument, NULL, 'u'},
  91                 {"analysis", required_argument, NULL, 't'},
  92                 {"options", required_argument, NULL, 'o'},
  93                 {"maxexecutions", required_argument, NULL, 'x'},
  94                 {0, 0, 0, 0}    /* Terminator */
  95         };
  96         int opt, longindex;
  97         int tmpoptind = optind;
  98         bool error = false;
  99         char * options = getenv("C11TESTER");
 100
 101         if (options == NULL)
 102                 return;
 103         int argc = 1;
 104         for(int index = 0;options[index]!=0;index++) {
 105                 if (options[index] == ' ')
 106                         argc++;
 107         }
 108         argc++; //first parameter is executable name
 109         char * argv[argc + 1];
 110         argv[0] = NULL;
 111         argv[1] = options;
 112         for(int index = 0, count = 2;options[index]!=0;index++) {
 113                 if (options[index]==' ')
 114                         argv[count++] = &options[index];
 115         }
 116
 117         while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
 118                 switch (opt) {
 119                 case 'h':
 120                         print_usage(params);
 121                         break;
 122                 case 'n':
 123                         params->nofork = true;
 124                         break;
 125                 case 'x':
 126                         params->maxexecutions = atoi(optarg);
 127                         break;
 128                 case 'v':
 129                         params->verbose = optarg ? atoi(optarg) : 1;
 130                         break;
 131                 case 'u':
 132                         params->uninitvalue = atoi(optarg);
 133                         break;
 134                 case 't':
 135                         if (install_plugin(optarg))
 136                                 error = true;
 137                         break;
 138                 case 'o':
 139                 {
 140                         ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
 141                         if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
 142                                 error = true;
 143                 }
 144                 break;
 145                 default:        /* '?' */
 146                         error = true;
 147                         break;
 148                 }
 149         }
 150
 151         /* Restore (global) optind for potential use by user program */
 152         optind = tmpoptind;
 153
 154         if (error)
 155                 print_usage(params);
 156 }
 157
 158 static void install_trace_analyses(ModelExecution *execution)
 159 {
 160         ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
 161         for(unsigned int i=0;i<installedanalysis->size();i++) {
 162                 TraceAnalysis * ta=(*installedanalysis)[i];
 163                 ta->setExecution(execution);
 164                 model->add_trace_analysis(ta);
 165                 /** Call the installation event for each installed plugin */
 166                 ta->actionAtInstallation();
 167         }
 168 }
 169
 170 /**
 171  * Main function.  Just initializes snapshotting library and the
 172  * snapshotting library calls the model_main function.
 173  */
 174 int main(int argc, char **argv)
 175 {
 176         /*
 177          * If this printf statement is removed, C11Tester will fail on an
 178          * assert on some versions of glibc.  The first time printf is
 179          * called, it allocated internal buffers.  We can't easily snapshot
 180          * libc since we also use it.
 181          */
 182
 183         printf("C11Tester\n"
 184                                  "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n"
 185                                  "Distributed under the GPLv2\n"
 186                                  "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
 187
 188
 189         //Initialize snapshotting library and model checker object
 190         if (!model) {
 191                 snapshot_system_init(10000, 1024, 1024, 40000);
 192                 model = new ModelChecker();
 193                 model->startChecker();
 194         }
 195
 196         /* Configure output redirection for the model-checker */
 197         redirect_output();
 198         register_plugins();
 199
 200         //Stash command line options
 201         model_params *params = model->getParams();
 202         params->argc = argc;
 203         params->argv = argv;
 204
 205         install_trace_analyses(model->get_execution());
 206
 207         model->startMainThread();
 208         DEBUG("Exiting\n");
 209 }