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(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 /**
 165  * Main function.  Just initializes snapshotting library and the
 166  * snapshotting library calls the model_main function.
 167  */
 168 int main(int argc, char **argv)
 169 {
 170         main_argc = argc;
 171         main_argv = argv;
 172
 173         /*
 174          * If this printf statement is removed, CDSChecker will fail on an
 175          * assert on some versions of glibc.  The first time printf is
 176          * called, it allocated internal buffers.  We can't easily snapshot
 177          * libc since we also use it.
 178          */
 179
 180         printf("CDSChecker\n"
 181                                  "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
 182                                  "Distributed under the GPLv2\n"
 183                                  "Written by Brian Norris and Brian Demsky\n\n");
 184
 185         /* Configure output redirection for the model-checker */
 186         redirect_output();
 187
 188         //Initialize snapshotting library and model checker object
 189         if (!model) {
 190                 snapshot_system_init(10000, 1024, 1024, 40000);
 191                 model = new ModelChecker();
 192                 model->startChecker();
 193         }
 194
 195         register_plugins();
 196
 197         //Parse command line options
 198         model_params *params = model->getParams();
 199         parse_options(params, main_argc, main_argv);
 200
 201
 202         snapshot_stack_init();
 203         install_trace_analyses(model->get_execution());
 204
 205         snapshot_record(0);
 206         model->startMainThread();
 207         DEBUG("Exiting\n");
 208 }