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, C11Tester 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("C11Tester\n"
 181                                  "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n"
 182                                  "Distributed under the GPLv2\n"
 183                                  "Written by Weiyu Luo, 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 }