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->maxexecutions = 10;
  24         params->traceminsize = 0;
  25         params->checkthreshold = 500000;
  26         params->removevisible = false;
  27         params->nofork = false;
  28 }
  29
  30 static void print_usage(struct model_params *params)
  31 {
  32         ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
  33         /* Reset defaults before printing */
  34         param_defaults(params);
  35
  36         model_print(
  37                 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
  38                 "Distributed under the GPLv2\n"
  39                 "Written by Brian Norris and Brian Demsky\n"
  40                 "\n"
  41                 "Usage: C11TESTER=[MODEL-CHECKER OPTIONS]\n"
  42                 "\n"
  43                 "MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n"
  44                 "provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n"
  45                 "\n"
  46                 "Model-checker options:\n"
  47                 "-h, --help                  Display this help message and exit\n"
  48                 "-v[NUM], --verbose[=NUM]    Print verbose execution information. NUM is optional:\n"
  49                 "                              0 is quiet; 1 shows valid executions; 2 is noisy;\n"
  50                 "                              3 is noisier.\n"
  51                 "                              Default: %d\n"
  52                 "-t, --analysis=NAME         Use Analysis Plugin.\n"
  53                 "-o, --options=NAME          Option for previous analysis plugin.  \n"
  54                 "-x, --maxexec=NUM           Maximum number of executions.\n"
  55                 "                            Default: %u\n"
  56                 "                            -o help for a list of options\n"
  57                 "-n                          No fork\n"
  58                 "-m, --minsize=NUM           Minimum number of actions to keep\n"
  59                 "                            Default: %u\n"
  60                 "-f, --freqfree=NUM          Frequency to free actions\n"
  61                 "                            Default: %u\n"
  62                 "-r, --removevisible         Free visible writes\n",
  63                 params->verbose,
  64                 params->maxexecutions,
  65                 params->traceminsize,
  66                 params->checkthreshold);
  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 = "hrnt:o:x:v:m:f::";
  92         const struct option longopts[] = {
  93                 {"help", no_argument, NULL, 'h'},
  94                 {"verbose", optional_argument, NULL, 'v'},
  95                 {"analysis", required_argument, NULL, 't'},
  96                 {"options", required_argument, NULL, 'o'},
  97                 {"maxexecutions", required_argument, NULL, 'x'},
  98                 {"minsize", required_argument, NULL, 'm'},
  99                 {"freqfree", required_argument, NULL, 'f'},
 100                 {"removevisible", no_argument, NULL, 'r'},
 101                 {0, 0, 0, 0}    /* Terminator */
 102         };
 103         int opt, longindex;
 104         int tmpoptind = optind;
 105         bool error = false;
 106         char * options = getenv("C11TESTER");
 107
 108         if (options == NULL)
 109                 return;
 110         int argc = 1;
 111         int index;
 112         for(index = 0;options[index]!=0;index++) {
 113                 if (options[index] == ' ')
 114                         argc++;
 115         }
 116         argc++; //first parameter is executable name
 117         char optcpy[index + 1];
 118         memcpy(optcpy, options, index+1);
 119         char * argv[argc + 1];
 120         argv[0] = NULL;
 121         argv[1] = optcpy;
 122         int count = 2;
 123         for(index = 0;optcpy[index]!=0;index++) {
 124                 if (optcpy[index] == ' ') {
 125                         argv[count++] = &optcpy[index+1];
 126                         optcpy[index] = 0;
 127                 }
 128         }
 129
 130         while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
 131                 switch (opt) {
 132                 case 'h':
 133                         print_usage(params);
 134                         break;
 135                 case 'n':
 136                         params->nofork = true;
 137                         break;
 138                 case 'x':
 139                         params->maxexecutions = atoi(optarg);
 140                         break;
 141                 case 'v':
 142                         params->verbose = optarg ? atoi(optarg) : 1;
 143                         break;
 144                 case 't':
 145                         if (install_plugin(optarg))
 146                                 error = true;
 147                         break;
 148                 case 'm':
 149                         params->traceminsize = atoi(optarg);
 150                         break;
 151                 case 'f':
 152                         params->checkthreshold = atoi(optarg);
 153                         break;
 154                 case 'r':
 155                         params->removevisible = true;
 156                         break;
 157                 case 'o':
 158                 {
 159                         ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
 160                         if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
 161                                 error = true;
 162                 }
 163                 break;
 164                 default:        /* '?' */
 165                         error = true;
 166                         break;
 167                 }
 168         }
 169
 170         /* Restore (global) optind for potential use by user program */
 171         optind = tmpoptind;
 172
 173         if (error)
 174                 print_usage(params);
 175 }
 176
 177 void install_trace_analyses(ModelExecution *execution) {
 178         ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
 179         for(unsigned int i=0;i<installedanalysis->size();i++) {
 180                 TraceAnalysis * ta=(*installedanalysis)[i];
 181                 ta->setExecution(execution);
 182                 model->add_trace_analysis(ta);
 183                 /** Call the installation event for each installed plugin */
 184                 ta->actionAtInstallation();
 185         }
 186 }