CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file main.cpp 00004 * \brief Main program for cvc3 00005 * 00006 * Author: Clark Barrett 00007 * 00008 * Created: Wed Dec 4 17:21:10 2002 00009 * 00010 * <hr> 00011 * 00012 * License to use, copy, modify, sell and/or distribute this software 00013 * and its documentation for any purpose is hereby granted without 00014 * royalty, subject to the terms and conditions defined in the \ref 00015 * LICENSE file provided with this distribution. 00016 * 00017 * <hr> 00018 * 00019 */ 00020 /*****************************************************************************/ 00021 00022 #include <signal.h> 00023 #include <fstream> 00024 #include <iomanip> 00025 00026 #include "os.h" 00027 #include "vc.h" 00028 #include "parser.h" 00029 #include "vc_cmd.h" 00030 #include "command_line_flags.h" 00031 #include "statistics.h" 00032 00033 #ifdef _MSC_VER 00034 #include <windows.h> 00035 #else 00036 #include <unistd.h> 00037 #endif 00038 00039 00040 using namespace std; 00041 using namespace CVC3; 00042 00043 00044 static void parse_args(int argc, char **argv, CLFlags &flags, 00045 string& fileName); 00046 static void printUsage(const CLFlags& flags, bool followDisplay); 00047 00048 // Our own name 00049 static string programName; 00050 00051 static ValidityChecker* vc = NULL; 00052 IF_DEBUG(static DebugTimer* pRuntime = NULL;) 00053 00054 #ifndef _MSC_VER 00055 void sighandler(int signum) { 00056 cerr << "\nInterrupted by signal " << signum; 00057 if(signum == SIGALRM) 00058 cerr << " (self-timeout)"; 00059 cerr << ". " << programName << " is aborting.\n"; 00060 // Print the debugging info 00061 IF_DEBUG(if (pRuntime != NULL) CVC3::debugger.setElapsed(*pRuntime);) 00062 IF_DEBUG(debugger.printAll();) 00063 if(vc != NULL && vc->getFlags()["stats"].getBool()) 00064 cout << vc->getStatistics() << endl; 00065 abort(); 00066 } 00067 #else 00068 DWORD WINAPI thread_timeout(PVOID timeout) { 00069 Sleep((int)timeout * 1000); 00070 cerr << "(self-timeout)." << endl; 00071 ExitProcess(1); 00072 } 00073 #endif 00074 00075 00076 int main(int argc, char **argv) 00077 { 00078 CLFlags flags(ValidityChecker::createFlags()); 00079 programName = string(argv[0]); 00080 IF_DEBUG(DebugTimer runtime(CVC3::debugger.timer("total runtime"));) 00081 IF_DEBUG(pRuntime = &runtime;) 00082 00083 #ifndef _MSC_VER 00084 signal(SIGINT, sighandler); 00085 signal(SIGTERM, sighandler); 00086 signal(SIGQUIT, sighandler); 00087 signal(SIGALRM, sighandler); 00088 #endif 00089 00090 string fileName(""); 00091 00092 try { 00093 parse_args(argc, argv, flags, fileName); 00094 } catch(Exception& e) { 00095 cerr << "*** " << e; 00096 cerr << "\n\nRun with -help option for usage information." << endl; 00097 exit(1); 00098 } 00099 00100 // Set the timeout, if given in the command line options 00101 int timeout = flags["timeout"].getInt(); 00102 if(timeout > 0) { 00103 #ifndef _MSC_VER 00104 alarm(timeout); 00105 #else 00106 // http://msdn2.microsoft.com/en-us/library/ms682453.aspx 00107 CreateThread(NULL, 0, thread_timeout, (PVOID)timeout, 0, NULL); 00108 #endif 00109 } 00110 00111 /* 00112 * Create and run the validity checker 00113 */ 00114 00115 // Debugging code may throw an exception 00116 try { 00117 vc = ValidityChecker::create(flags); 00118 } catch(Exception& e) { 00119 cerr << "*** Fatal exception: " << e << endl; 00120 exit(1); 00121 } 00122 00123 // -h flag sets "help" to false (+h would make it true, but that's 00124 // not what the user normally types in). 00125 if(!vc->getFlags()["help"].getBool()) { 00126 printUsage(vc->getFlags(), true); 00127 return 0; 00128 } 00129 if(!vc->getFlags()["unsupported"].getBool()) { 00130 printUsage(vc->getFlags(), false); 00131 return 0; 00132 } 00133 #ifndef VERSION 00134 #define VERSION "unknown" 00135 #endif 00136 // Similarly, -version sets the flag "version" to false 00137 if(!vc->getFlags()["version"].getBool()) { 00138 cout << "This is CVC3 version " << VERSION 00139 IF_DEBUG( << " (debug build)") 00140 << "\n\n"; 00141 cout << 00142 "Copyright (C) 2003-2009 by the Board of Trustees of Leland Stanford Junior\n" 00143 "University, New York University, and the University of Iowa.\n\n" 00144 "THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. " 00145 "USE IT AT YOUR OWN RISK.\n" 00146 << endl; 00147 return 0; 00148 } 00149 00150 try { 00151 // Test if the output language is correctly specified; if not, an 00152 // exception will be thrown 00153 vc->getEM()->getOutputLang(); 00154 // Set the timer 00155 IF_DEBUG(CVC3::debugger.setCurrentTime(runtime);) 00156 // Read the input file 00157 vc->loadFile(fileName, vc->getEM()->getInputLang(), 00158 flags["interactive"].getBool()); 00159 } catch(Exception& e) { 00160 cerr << "*** Fatal exception: " << e << endl; 00161 exit(1); 00162 } 00163 00164 IF_DEBUG(CVC3::debugger.setElapsed(runtime);) 00165 00166 // Print the debugging info 00167 IF_DEBUG(debugger.printAll();) 00168 // Print statistics 00169 if(vc->getFlags()["stats"].getBool()) vc->printStatistics(); 00170 // Destruct the system 00171 TRACE_MSG("delete", "Deleting ValidityChecker [last trace from main.cpp]"); 00172 try { 00173 delete vc; 00174 } catch(Exception& e) { 00175 cerr << "*** Fatal exception: " << e << endl; 00176 exit(1); 00177 } 00178 00179 return 0; 00180 } 00181 00182 void printUsage(const CLFlags& flags, bool followDisplay) { 00183 cout << "Usage: " << programName << " [options]\n" 00184 << programName << " will read the input from STDIN and \n" 00185 << "print the result on STDOUT.\n" 00186 << "Boolean (b) options are set 'on' by +option and 'off' by -option\n" 00187 << "(for instance, +model or -model).\n" 00188 << "Integer (i), string (s) and vector (v) options \n" 00189 << "require a parameter, e.g. -width 80\n" 00190 << "Also, (v) options can appear multiple times setting " 00191 << "args on and off,\n" 00192 << "as in +trace \"enable this\" -trace \"disable that\".\n" 00193 << "Option names can be abbreviated to the " 00194 << "shortest unambiguous prefix.\n\n" 00195 << "The options are:\n"; 00196 vector<string> names; 00197 // Get all the names of options (they all match the empty string) 00198 flags.countFlags("", names); 00199 for(size_t i=0,iend=names.size(); i!=iend; ++i) { 00200 const CLFlag& f(flags[names[i]]); 00201 if (f.display() != followDisplay) continue; 00202 string tpStr; // Print type of the option 00203 string pref; // Print + or - in front of the option 00204 string name(names[i]); // Print name and optionally the value 00205 CLFlagType tp = f.getType(); 00206 switch(tp) { 00207 case CLFLAG_NULL: tpStr = "(null)"; break; 00208 case CLFLAG_BOOL: 00209 tpStr = "(b)"; pref = (f.getBool())? "+" : "-"; 00210 break; 00211 case CLFLAG_INT: 00212 tpStr = "(i)"; pref = "-"; name = name+" "+int2string(f.getInt()); 00213 break; 00214 case CLFLAG_STRING: 00215 tpStr = "(s)"; pref = "-"; name = name+" "+f.getString(); 00216 break; 00217 case CLFLAG_STRVEC: 00218 tpStr = "(v)"; pref = "-"; name = name; 00219 break; 00220 default: 00221 DebugAssert(false, "printUsage: unknown flag type"); 00222 } 00223 cout << " " << tpStr << " " << pref << setw(25); 00224 cout.setf(ios::left); 00225 cout << name << " " << f.getHelp() << "\n"; 00226 } 00227 cout << endl; 00228 } 00229 00230 00231 void parse_args(int argc, char **argv, CLFlags &flags, string& fileName) { 00232 /* skip 0'th argument */ 00233 argv++; 00234 argc--; 00235 bool seenFileName(false); 00236 00237 for( ; argc > 0; argc--, argv++) { 00238 if((*argv)[0] == '-' || (*argv)[0] == '+') { 00239 // A command-line option 00240 vector<string> names; 00241 bool val = ((*argv)[0] == '+'); 00242 size_t n = flags.countFlags((*argv)+1, names); 00243 if(n == 0) 00244 throw CLException(string(*argv) + " does not match any known option"); 00245 else if(n > 1) { 00246 ostringstream ss; 00247 ss << *argv << " is ambiguous. Possible matches are:\n"; 00248 for(size_t i=0,iend=names.size(); i!=iend; ++i) { 00249 ss << " " << names[i] << "\n"; 00250 } 00251 throw CLException(ss.str()); 00252 } else { 00253 string name = names[0]; 00254 // Single match; process the option 00255 CLFlagType tp = flags[name].getType(); 00256 switch(tp) { 00257 case CLFLAG_BOOL: flags.setFlag(name, val); break; 00258 case CLFLAG_INT: 00259 argc--; 00260 if(argc <= 0) 00261 throw CLException(string(*argv)+" (-"+name 00262 +") expects an integer argument."); 00263 argv++; 00264 // FIXME: test for *argv being an integer string 00265 flags.setFlag(name, atoi(*argv)); 00266 break; 00267 case CLFLAG_STRING: 00268 argc--; 00269 if(argc <= 0) 00270 throw CLException(string(*argv)+" (-"+name 00271 +") expects a string argument."); 00272 argv++; 00273 flags.setFlag(name, *argv); 00274 break; 00275 case CLFLAG_STRVEC: 00276 argc--; 00277 if(argc <= 0) 00278 throw CLException(string(*argv)+" (-"+name 00279 +") expects a string argument."); 00280 argv++; 00281 flags.setFlag(name, pair<string,bool>(*argv,val)); 00282 break; 00283 default: 00284 DebugAssert(false, "parse_args: Bad flag type: "+int2string(tp)); 00285 } 00286 } 00287 } else if(seenFileName) { 00288 throw CLException("More than one file name given: "+fileName 00289 +" and "+string(*argv)); 00290 } else { 00291 fileName = string(*argv); 00292 seenFileName = true; 00293 } 00294 } 00295 }