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->enabledcount = 1;
  23         params->bound = 0;
  24         params->verbose = !!DBG_ENABLED();
  25         params->uninitvalue = 0;
  26         params->maxexecutions = 0;
  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 "-e, --enabled=COUNT         Enabled count.\n"
  48 "                              Default: %d\n"
  49 "-b, --bound=MAX             Upper length bound.\n"
  50 "                              Default: %d\n"
  51 "-v[NUM], --verbose[=NUM]    Print verbose execution information. NUM is optional:\n"
  52 "                              0 is quiet; 1 shows valid executions; 2 is noisy;\n"
  53 "                              3 is noisier.\n"
  54 "                              Default: %d\n"
  55 "-u, --uninitialized=VALUE   Return VALUE any load which may read from an\n"
  56 "                              uninitialized atomic.\n"
  57 "                              Default: %u\n"
  58 "-t, --analysis=NAME         Use Analysis Plugin.\n"
  59 "-o, --options=NAME          Option for previous analysis plugin.  \n"
  60 "-x, --maxexec=NUM           Maximum number of executions.\n"
  61 "                            Default: %u\n"
  62 "                            -o help for a list of options\n"
  63 " --                         Program arguments follow.\n\n",
  64                 program_name,
  65                 params->enabledcount,
  66                 params->bound,
  67                 params->verbose,
  68                 params->uninitvalue,
  69                 params->maxexecutions);
  70         model_print("Analysis plugins:\n");
  71         for(unsigned int i=0;i<registeredanalysis->size();i++) {
  72                 TraceAnalysis * analysis=(*registeredanalysis)[i];
  73                 model_print("%s\n", analysis->name());
  74         }
  75         exit(EXIT_SUCCESS);
  76 }
  77
  78 bool install_plugin(char * name) {
  79         ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
  80         ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
  81
  82         for(unsigned int i=0;i<registeredanalysis->size();i++) {
  83                 TraceAnalysis * analysis=(*registeredanalysis)[i];
  84                 if (strcmp(name, analysis->name())==0) {
  85                         installedanalysis->push_back(analysis);
  86                         return false;
  87                 }
  88         }
  89         model_print("Analysis %s Not Found\n", name);
  90         return true;
  91 }
  92
  93 static void parse_options(struct model_params *params, int argc, char **argv)
  94 {
  95         const char *shortopts = "ht:o:e:b:u:x:v::";
  96         const struct option longopts[] = {
  97                 {"help", no_argument, NULL, 'h'},
  98                 {"enabled", required_argument, NULL, 'e'},
  99                 {"bound", required_argument, NULL, 'b'},
 100                 {"verbose", optional_argument, NULL, 'v'},
 101                 {"uninitialized", required_argument, NULL, 'u'},
 102                 {"analysis", required_argument, NULL, 't'},
 103                 {"options", required_argument, NULL, 'o'},
 104                 {"maxexecutions", required_argument, NULL, 'x'},
 105                 {0, 0, 0, 0} /* Terminator */
 106         };
 107         int opt, longindex;
 108         bool error = false;
 109         while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
 110                 switch (opt) {
 111                 case 'h':
 112                         print_usage(argv[0], params);
 113                         break;
 114                 case 'x':
 115                         params->maxexecutions = atoi(optarg);
 116                         break;
 117                 case 'e':
 118                         params->enabledcount = atoi(optarg);
 119                         break;
 120                 case 'b':
 121                         params->bound = atoi(optarg);
 122                         break;
 123                 case 'v':
 124                         params->verbose = optarg ? atoi(optarg) : 1;
 125                         break;
 126                 case 'u':
 127                         params->uninitvalue = atoi(optarg);
 128                         break;
 129                 case 't':
 130                         if (install_plugin(optarg))
 131                                 error = true;
 132                         break;
 133                 case 'o':
 134                         {
 135                                 ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
 136                                 if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
 137                                         error = true;
 138                         }
 139                         break;
 140                 default: /* '?' */
 141                         error = true;
 142                         break;
 143                 }
 144         }
 145
 146         /* Pass remaining arguments to user program */
 147         params->argc = argc - (optind - 1);
 148         params->argv = argv + (optind - 1);
 149
 150         /* Reset program name */
 151         params->argv[0] = argv[0];
 152
 153         /* Reset (global) optind for potential use by user program */
 154         optind = 1;
 155
 156         if (error)
 157                 print_usage(argv[0], params);
 158 }
 159
 160 int main_argc;
 161 char **main_argv;
 162
 163 static void install_trace_analyses(ModelExecution *execution)
 164 {
 165         ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
 166         for(unsigned int i=0;i<installedanalysis->size();i++) {
 167                 TraceAnalysis * ta=(*installedanalysis)[i];
 168                 ta->setExecution(execution);
 169                 model->add_trace_analysis(ta);
 170                 /** Call the installation event for each installed plugin */
 171                 ta->actionAtInstallation();
 172         }
 173 }
 174
 175 /** The model_main function contains the main model checking loop. */
 176 static void model_main()
 177 {
 178         struct model_params params;
 179
 180         param_defaults(&params);
 181         register_plugins();
 182
 183         parse_options(&params, main_argc, main_argv);
 184
 185         //Initialize race detector
 186         initRaceDetector();
 187
 188         snapshot_stack_init();
 189
 190         model = new ModelChecker(params);
 191         install_trace_analyses(model->get_execution());
 192
 193         snapshot_record(0);
 194         model->run();
 195         delete model;
 196
 197         DEBUG("Exiting\n");
 198 }
 199
 200 /**
 201  * Main function.  Just initializes snapshotting library and the
 202  * snapshotting library calls the model_main function.
 203  */
 204 int main(int argc, char **argv)
 205 {
 206         main_argc = argc;
 207         main_argv = argv;
 208
 209         /*
 210          * If this printf statement is removed, CDSChecker will fail on an
 211          * assert on some versions of glibc.  The first time printf is
 212          * called, it allocated internal buffers.  We can't easily snapshot
 213          * libc since we also use it.
 214          */
 215
 216         printf("CDSChecker\n"
 217                                  "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
 218                                  "Distributed under the GPLv2\n"
 219                                  "Written by Brian Norris and Brian Demsky\n\n");
 220
 221         /* Configure output redirection for the model-checker */
 222         redirect_output();
 223
 224         /* Let's jump in quickly and start running stuff */
 225         snapshot_system_init(10000, 1024, 1024, 4000, &model_main);
 226 }