zcov: / tools/klee/main.cpp


Files: 1 Branches Taken: 53.2% 236 / 444
Generated: 2009-05-17 22:47 Branches Executed: 71.2% 316 / 444
Line Coverage: 70.2% 407 / 580


Programs: 1 Runs 371


       1                 : /* -*- mode: c++; c-basic-offset: 2; -*- */
       2                 : 
       3                 : // FIXME: This does not belong here.
       4                 : #include "../lib/Core/Common.h"
       5                 : 
       6                 : #include "klee/ExecutionState.h"
       7                 : #include "klee/Expr.h"
       8                 : #include "klee/Interpreter.h"
       9                 : #include "klee/Statistics.h"
      10                 : #include "klee/Config/config.h"
      11                 : #include "klee/Internal/ADT/BOut.h"
      12                 : #include "klee/Internal/ADT/TreeStream.h"
      13                 : #include "klee/Internal/Support/ModuleUtil.h"
      14                 : #include "klee/Internal/System/Time.h"
      15                 : 
      16                 : #include "llvm/Constants.h"
      17                 : #include "llvm/Module.h"
      18                 : #include "llvm/ModuleProvider.h"
      19                 : #include "llvm/Type.h"
      20                 : #include "llvm/InstrTypes.h"
      21                 : #include "llvm/Instruction.h"
      22                 : #include "llvm/Instructions.h"
      23                 : #include "llvm/Bitcode/ReaderWriter.h"
      24                 : #include "llvm/Support/CommandLine.h"
      25                 : #include "llvm/Support/ManagedStatic.h"
      26                 : #include "llvm/Support/MemoryBuffer.h"
      27                 : #include "llvm/System/Signals.h"
      28                 : #include <iostream>
      29                 : #include <fstream>
      30                 : #include <cerrno>
      31                 : #include <dirent.h>
      32                 : #include <errno.h>
      33                 : #include <sys/stat.h>
      34                 : #include <sys/wait.h>
      35                 : #include <signal.h>
      36                 : 
      37                 : #include <iostream>
      38                 : #include <iterator>
      39                 : #include <fstream>
      40                 : #include <sstream>
      41                 : 
      42                 : #include "klee/Internal/FIXME/sugar.h"
      43                 : 
      44                 : using namespace llvm;
      45                 : using namespace klee;
      46                 : 
      47                 : namespace {
      48                 :   cl::opt<std::string>
      49              206:   InputFile(cl::desc("<input bytecode>"), cl::Positional, cl::init("-"));
      50                 : 
      51                 :   cl::opt<std::string>
      52              103:   RunInDir("run-in", cl::desc("Change to the given directory prior to executing"));
      53                 : 
      54                 :   cl::opt<std::string>
      55              103:   Environ("environ", cl::desc("Parse environ from given file (in \"env\" format)"));
      56                 : 
      57                 :   cl::list<std::string>
      58              103:   InputArgv(cl::ConsumeAfter, 
      59              103:             cl::desc("<program arguments>..."));
      60                 : 
      61                 :   cl::opt<bool>
      62              103:   NoOutput("no-output", 
      63              103:            cl::desc("Don't generate test files"));
      64                 :     
      65                 :   cl::opt<bool>
      66              103:   WarnAllExternals("warn-all-externals", 
      67                 :                    cl::desc("Give initial warning for all externals."));
      68                 :     
      69                 :   cl::opt<bool>
      70              103:   WriteCVCs("write-cvcs", 
      71                 :             cl::desc("Write .cvc files for each test case"));
      72                 : 
      73                 :   cl::opt<bool>
      74              103:   WritePCs("write-pcs", 
      75              103:             cl::desc("Write .pc files for each test case"));
      76                 :   
      77                 :   cl::opt<bool>
      78              103:   WriteCov("write-cov", 
      79              103:            cl::desc("Write coverage information for each test case"));
      80                 :   
      81                 :   cl::opt<bool>
      82              103:   WritePaths("write-paths", 
      83                 :                 cl::desc("Write .path files for each test case"));
      84                 :     
      85                 :   cl::opt<bool>
      86              103:   WriteSymPaths("write-sym-paths", 
      87                 :                 cl::desc("Write .sym.path files for each test case"));
      88                 :     
      89                 :   cl::opt<bool>
      90              103:   ExitOnError("exit-on-error", 
      91                 :               cl::desc("Exit if errors occur"));
      92                 :     
      93                 : 
      94                 :   enum LibcType {
      95                 :     NoLibc, KleeLibc, UcLibc
      96                 :   };
      97                 : 
      98                 :   cl::opt<LibcType>
      99              103:   Libc("libc", 
     100                 :        cl::desc("Choose libc version (none by default)."),
     101                 :        cl::values(clEnumValN(NoLibc, "none", "Don't link in a libc"),
     102                 :                   clEnumValN(KleeLibc, "klee", "Link in klee libc"),
     103                 : 		  clEnumValN(UcLibc, "uclibc", "Link in uclibc (adapted for klee)"),
     104                 : 		  clEnumValEnd),
     105              206:        cl::init(NoLibc));
     106                 : 
     107                 :     
     108                 :   enum VersionType {
     109                 :     None, Debug, Release
     110                 :   };
     111                 : 
     112                 :   cl::opt<VersionType>
     113              103:   WithFileModel("with-file-model", 
     114                 : 		cl::desc("Link with file model"),
     115                 : 		cl::values(clEnumValN(Release, "release", "Release version"),
     116                 : 			   clEnumValN(Debug, "debug", "Debug version"),
     117                 : 			   clEnumValEnd),
     118              206: 		cl::init(None));
     119                 :     
     120                 :   cl::opt<bool>
     121              103:   OptimizeModule("optimize", 
     122              103:                  cl::desc("Optimize before execution"));
     123                 : 
     124                 :   cl::opt<bool>
     125              103:   CheckDivZero("check-div-zero", 
     126                 :                cl::desc("Inject checks for division-by-zero"),
     127              103:                cl::init(true));
     128                 :     
     129                 :   cl::opt<std::string>
     130              103:   OutputDir("output-dir", 
     131                 :             cl::desc("Directory to write results in (defaults to klee-out-N)"),
     132                 :             cl::init(""));
     133                 : 
     134                 :   // this is a fake entry, its automagically handled
     135                 :   cl::list<std::string>
     136              103:   ReadArgsFilesFake("read-args", 
     137                 :                     cl::desc("File to read arguments from (one arg per line)"));
     138                 :     
     139                 :   cl::opt<bool>
     140              103:   ReplayKeepSymbolic("replay-keep-symbolic", 
     141                 :                      cl::desc("Replay the test cases only by asserting"
     142                 :                               "the bytes, not necessarily making them concrete."));
     143                 :     
     144                 :   cl::list<std::string>
     145              103:   ReplayOutFile("replay-out",
     146                 :                 cl::desc("Specify an out file to replay"),
     147                 :                 cl::value_desc("out file"));
     148                 : 
     149                 :   cl::list<std::string>
     150              103:   ReplayOutDir("replay-out-dir",
     151                 : 	       cl::desc("Specify a directory to replay .out files from"),
     152                 : 	       cl::value_desc("output directory"));
     153                 : 
     154                 :   cl::opt<std::string>
     155              103:   ReplayPathFile("replay-path",
     156                 :                  cl::desc("Specify a path file to replay"),
     157                 :                  cl::value_desc("path file"));
     158                 : 
     159                 :   cl::list<std::string>
     160              103:   SeedOutFile("seed-out");
     161                 :   
     162                 :   cl::list<std::string>
     163              103:   SeedOutDir("seed-out-dir");
     164                 :   
     165                 :   cl::opt<unsigned>
     166              103:   DigitsInTest("digits-in-test",
     167                 :                cl::desc("For fucking annoying regression/ tests"),
     168              103:                cl::init(6));  
     169                 : 
     170                 :   cl::opt<unsigned>
     171              103:   MakeConcreteSymbolic("make-concrete-symbolic",
     172                 :                        cl::desc("Rate at which to make concrete reads symbolic (0=off)"),
     173              103:                        cl::init(0));
     174                 : 
     175                 :   cl::opt<bool>
     176              103:   InitEnv("init-env",
     177              103: 	  cl::desc("Create custom environment.  Options that can be passed as arguments to the programs are: --sym-argv <max-len>  --sym-argvs <min-argvs> <max-argvs> <max-len> + file model options"));
     178                 :  
     179                 :   cl::opt<bool>
     180              103:   ExcludeLibcCov("exclude-libc-cov",
     181                 : 		 cl::desc("Do not track coverage in libc"));
     182                 :   
     183                 :   cl::list<std::string>
     184              103:   ExcludeCovFiles("exclude-cov-file",
     185                 : 		  cl::desc("Filename to load function names to not track coverage for"));
     186                 : 
     187                 :   cl::opt<unsigned>
     188              103:   StopAfterNTests("stop-after-n-tests",
     189                 : 	     cl::desc("Stop execution after generating the given number of tests.  Extra tests corresponding to partially explored paths will also be dumped."),
     190              103: 	     cl::init(0));
     191                 : 
     192                 :   cl::opt<bool>
     193              103:   Watchdog("watchdog",
     194                 :            cl::desc("Use a watchdog process to enforce --max-time."),
     195              103:            cl::init(0));
     196                 : }
     197                 : 
     198                 : extern bool WriteTraces;
     199                 : extern cl::opt<double> MaxTime;
     200                 : 
     201                 : /***/
     202                 : 
     203                 : class KleeHandler : public InterpreterHandler {
     204                 : private:
     205                 :   Interpreter *m_interpreter;
     206                 :   TreeStreamWriter *m_pathWriter, *m_symPathWriter;
     207                 : 
     208                 :   char m_outputDirectory[1024];
     209                 :   unsigned m_testIndex;  // number of tests written so far
     210                 :   unsigned m_pathsExplored; // number of paths explored so far
     211                 : 
     212                 :   // used for writing .bout files
     213                 :   int m_argc;
     214                 :   char **m_argv;
     215                 : 
     216                 : public:
     217                 :   KleeHandler(int argc, char **argv);
     218                 :   ~KleeHandler();
     219                 : 
     220              103:   unsigned getNumTestCases() { return m_testIndex; }
     221                0:   unsigned getNumPathsExplored() { return m_pathsExplored; }
     222              790:   void incPathsExplored() { m_pathsExplored++; }
     223                 : 
     224                 :   void setInterpreter(Interpreter *i);
     225                 : 
     226                 :   void processTestCase(const ExecutionState  &state,
     227                 :                        const char *errorMessage, 
     228                 :                        const char *errorSuffix);
     229                 : 
     230                 :   std::string getOutputFilename(const std::string &filename);
     231                 :   std::ostream *openOutputFile(const std::string &filename);
     232                 :   std::string getTestFilename(const std::string &suffix, unsigned id);
     233                 :   std::ostream *openTestFile(const std::string &suffix, unsigned id);
     234                 : 
     235                 :   // load a .out file
     236                 :   static void loadOutFile(std::string name, 
     237                 :                           std::vector<unsigned char> &buffer);
     238                 : 
     239                 :   // load a .path file
     240                 :   static void loadPathFile(std::string name, 
     241                 :                            std::vector<bool> &buffer);
     242                 : 
     243                 :   static void getOutFiles(std::string path,
     244                 : 			  std::vector<std::string> &results);
     245                 : };
     246                 : 
     247              103: KleeHandler::KleeHandler(int argc, char **argv) 
     248                 :   : m_interpreter(0),
     249                 :     m_pathWriter(0),
     250                 :     m_symPathWriter(0),
     251                 :     m_testIndex(0),
     252                 :     m_pathsExplored(0),
     253                 :     m_argc(argc),
     254              206:     m_argv(argv) {
     255                 :   std::string theDir;
     256                 : 
                       99: branch 0 taken
                        4: branch 1 taken
                        4: branch 2 taken
                        4: branch 3 taken
     257              103:   if (OutputDir=="") {
     258               99:     llvm::sys::Path directory(InputFile);
     259               99:     std::string dirname = "";
     260               99:     directory.eraseComponent();
     261                 :     
                       99: branch 0 taken
                        0: branch 1 not taken
                        0: branch 2 not taken
                        0: branch 3 not taken
     262               99:     if (directory.isEmpty())
     263               99:       directory.set(".");
     264                 :     
     265            54379:     for (int i = 0; ; i++) {
     266                 :       char buf[256], tmp[64];
     267                 :       sprintf(tmp, "klee-out-%d", i);
     268                 :       dirname = tmp;
     269                 :       sprintf(buf, "%s/%s", directory.c_str(), tmp);
     270                 :       theDir = buf;
     271                 :       
                    54280: branch 1 taken
                       99: branch 2 taken
                        0: branch 4 not taken
                        0: branch 5 not taken
     272            54379:       if (DIR *dir = opendir(theDir.c_str())) {
     273            54280:         closedir(dir);
     274                 :       } else {
     275               99:         break;
     276                 :       }
     277                 :     }    
     278                 : 
     279               99:     llvm::cerr << "KLEE: using output directory \"" << dirname << "\"\n";
     280                 : 
     281                 :     llvm::sys::Path klee_last(directory);
     282               99:     klee_last.appendComponent("klee-last");
     283                 :       
                        0: branch 1 not taken
                       99: branch 2 taken
                        0: branch 4 not taken
                        0: branch 5 not taken
                        0: branch 6 not taken
                       99: branch 7 taken
                        0: branch 9 not taken
                        0: branch 10 not taken
                        0: branch 12 not taken
                        0: branch 13 not taken
                        0: branch 14 not taken
                        0: branch 15 not taken
     284               99:     if ((unlink(klee_last.c_str()) < 0) && (errno != ENOENT)) {
     285                0:       perror("Cannot unlink klee-last");
     286                0:       assert(0 && "exiting.");
     287                 :     }
     288                 :     
                        0: branch 1 not taken
                       99: branch 2 taken
                        0: branch 4 not taken
                        0: branch 5 not taken
     289               99:     if (symlink(dirname.c_str(), klee_last.c_str()) < 0) {
     290                0:       perror("Cannot make symlink");
     291                0:       assert(0 && "exiting.");
     292               99:     }
     293                 :   } else {
     294                 :     theDir = OutputDir;
     295                 :   }
     296                 :   
     297              103:   sys::Path p(theDir);
                      103: branch 1 taken
                        0: branch 2 not taken
                        0: branch 4 not taken
                        0: branch 5 not taken
     298              103:   if (!p.isAbsolute()) {
     299              103:     sys::Path cwd = sys::Path::GetCurrentDirectory();
     300              103:     cwd.appendComponent(theDir);
     301                 :     p = cwd;
     302                 :   }
     303              103:   strcpy(m_outputDirectory, p.c_str());
     304                 : 
                        0: branch 1 not taken
                      103: branch 2 taken
                        0: branch 4 not taken
                        0: branch 5 not taken
     305              103:   if (mkdir(m_outputDirectory, 0775) < 0) {
     306                 :     llvm::cerr << "KLEE: ERROR: Unable to make output directory: \"" 
     307                 :                << m_outputDirectory 
     308                0:                << "\", refusing to overwrite.\n";
     309                0:     exit(1);
     310                 :   }
     311                 : 
     312                 :   char fname[1024];
     313              103:   snprintf(fname, sizeof(fname), "%s/warnings.txt", m_outputDirectory);
     314              103:   klee_warning_file = fopen(fname, "w");
                        0: branch 0 not taken
                      103: branch 1 taken
                        0: branch 3 not taken
                        0: branch 4 not taken
     315              103:   assert(klee_warning_file);
     316                 : 
     317              103:   snprintf(fname, sizeof(fname), "%s/messages.txt", m_outputDirectory);
     318              103:   klee_message_file = fopen(fname, "w");
                        0: branch 0 not taken
                      103: branch 1 taken
                      103: branch 4 taken
                      103: branch 5 taken
     319              206:   assert(klee_message_file);
     320              103: }
     321                 : 
     322              103: KleeHandler::~KleeHandler() {
                        0: branch 0 not taken
                      103: branch 1 taken
                      103: branch 2 taken
                      103: branch 3 taken
                        0: branch 6 not taken
                        0: branch 7 not taken
                        0: branch 8 not taken
                        0: branch 9 not taken
                        0: branch 12 not taken
                        0: branch 13 not taken
                        0: branch 14 not taken
                        0: branch 15 not taken
     323              103:   if (m_pathWriter) delete m_pathWriter;
                        0: branch 0 not taken
                      103: branch 1 taken
                      103: branch 2 taken
                      103: branch 3 taken
                        0: branch 6 not taken
                        0: branch 7 not taken
                        0: branch 8 not taken
                        0: branch 9 not taken
                        0: branch 12 not taken
                        0: branch 13 not taken
                        0: branch 14 not taken
                        0: branch 15 not taken
     324              103:   if (m_symPathWriter) delete m_symPathWriter;
                      103: branch 0 taken
                        0: branch 1 not taken
                      103: branch 3 taken
                      103: branch 4 taken
                        0: branch 6 not taken
                        0: branch 7 not taken
     325              206: }
     326                 : 
     327              103: void KleeHandler::setInterpreter(Interpreter *i) {
     328              103:   m_interpreter = i;
     329                 : 
                        0: branch 0 not taken
                      103: branch 1 taken
     330              103:   if (WritePaths) {
     331                0:     m_pathWriter = new TreeStreamWriter(getOutputFilename("paths.ts"));
                        0: branch 1 not taken
                        0: branch 2 not taken
     332                0:     assert(m_pathWriter->good());
     333                0:     m_interpreter->setPathWriter(m_pathWriter);
     334                 :   }
     335                 : 
                        0: branch 0 not taken
                      103: branch 1 taken
     336              103:   if (WriteSymPaths) {
     337                0:     m_symPathWriter = new TreeStreamWriter(getOutputFilename("symPaths.ts"));
                        0: branch 1 not taken
                        0: branch 2 not taken
     338                0:     assert(m_symPathWriter->good());
     339                0:     m_interpreter->setSymbolicPathWriter(m_symPathWriter);
     340                 :   }
     341              103: }
     342                 : 
     343             2314: std::string KleeHandler::getOutputFilename(const std::string &filename) {
     344                 :   char outfile[1024];
     345             2314:   sprintf(outfile, "%s/%s", m_outputDirectory, filename.c_str());
     346             4628:   return outfile;
     347                 : }
     348                 : 
     349             1136: std::ostream *KleeHandler::openOutputFile(const std::string &filename) {
     350                 :   std::ios::openmode io_mode = std::ios::out | std::ios::trunc 
     351             1136:                              | std::ios::binary;
     352                 :   std::ostream *f;
     353             1136:   std::string path = getOutputFilename(filename);
     354             1136:   f = new std::ofstream(path.c_str(), io_mode);
                        0: branch 0 not taken
                     1136: branch 1 taken
     355             1136:   if (!f) {
     356                0:     klee_warning("out of memory");
                        0: branch 0 not taken
                     1136: branch 1 taken
     357             2272:   } else if (!f->good()) {
     358                0:     klee_warning("error opening: %s", filename.c_str());
                        0: branch 0 not taken
                        0: branch 1 not taken
     359                0:     delete f;
     360                0:     f = NULL;
     361                 :   }
     362                 : 
     363             1136:   return f;
     364                 : }
     365                 : 
     366              663: std::string KleeHandler::getTestFilename(const std::string &suffix, unsigned id) {
     367                 :   char filename[1024];
     368              663:   sprintf(filename, "test%0*d.%s", (int) DigitsInTest, id, suffix.c_str());
     369             1326:   return getOutputFilename(filename);
     370                 : }
     371                 : 
     372              724: std::ostream *KleeHandler::openTestFile(const std::string &suffix, unsigned id) {
     373                 :   char filename[1024];
     374              724:   sprintf(filename, "test%0*d.%s", (int) DigitsInTest, id, suffix.c_str());
     375             1448:   return openOutputFile(filename);
     376                 : }
     377                 : 
     378                 : 
     379                 : /* Outputs all files (.bout, .pc, .cov etc.) describing a test case */
     380                 : void KleeHandler::processTestCase(const ExecutionState &state,
     381                 :                                   const char *errorMessage, 
     382              671:                                   const char *errorSuffix) {
                       30: branch 0 taken
                      641: branch 1 taken
                        0: branch 2 not taken
                       30: branch 3 taken
                        0: branch 4 not taken
                      671: branch 5 taken
     383              701:   if (errorMessage && ExitOnError) {
     384                0:     llvm::cerr << "EXITING ON ERROR: " << errorMessage << "\n";
     385                0:     abort();
     386                 :   }
     387                 : 
                      663: branch 0 taken
                        8: branch 1 taken
     388              671:   if (!NoOutput) {
     389                 :     std::vector< std::pair<std::string, std::vector<unsigned char> > > out;
     390              663:     bool success = m_interpreter->getSymbolicSolution(state, out);
     391                 : 
                        0: branch 0 not taken
                      663: branch 1 taken
     392              663:     if (!success)
     393                0:       klee_warning("unable to get symbolic solution, losing test case");
     394                 : 
     395              663:     double start_time = util::getWallTime();
     396                 : 
     397              663:     unsigned id = ++m_testIndex;
     398                 : 
                      663: branch 0 taken
                        0: branch 1 not taken
     399              663:     if (success) {
     400                 :       BOut b;      
     401              663:       b.numArgs = m_argc;
     402              663:       b.args = m_argv;
     403              663:       b.symArgvs = 0;
     404              663:       b.symArgvLen = 0;
     405              663:       b.numObjects = out.size();
     406              663:       b.objects = new BOutObject[b.numObjects];
                        0: branch 0 not taken
                      663: branch 1 taken
     407              663:       assert(b.objects);
                      845: branch 0 taken
                      663: branch 1 taken
     408             1508:       for (unsigned i=0; i<b.numObjects; i++) {
     409              845:         BOutObject *o = &b.objects[i];
     410             1690:         o->name = const_cast<char*>(out[i].first.c_str());
     411             1690:         o->numBytes = out[i].second.size();
     412              845:         o->bytes = new unsigned char[o->numBytes];
                        0: branch 0 not taken
                      845: branch 1 taken
     413              845:         assert(o->bytes);
     414             3380:         std::copy(out[i].second.begin(), out[i].second.end(), o->bytes);
     415                 :       }
     416                 :       
                        0: branch 5 not taken
                      663: branch 6 taken
     417             1989:       if (!bOut_toFile(&b, getTestFilename("bout", id).c_str())) {
     418                0:         klee_warning("unable to write output test case, losing it");
     419                 :       }
     420                 :       
                      845: branch 0 taken
                      663: branch 1 taken
     421             1508:       for (unsigned i=0; i<b.numObjects; i++)
                      845: branch 0 taken
                        0: branch 1 not taken
     422              845:         delete[] b.objects[i].bytes;
                      663: branch 0 taken
                        0: branch 1 not taken
     423              663:       delete[] b.objects;
     424                 :     }
     425                 : 
                       29: branch 0 taken
                      634: branch 1 taken
     426              663:     if (errorMessage) {
     427               29:       std::ostream *f = openTestFile(errorSuffix, id);
     428               29:       *f << errorMessage;
                       29: branch 0 taken
                        0: branch 1 not taken
     429               29:       delete f;
     430                 :     }
     431                 :     
                        0: branch 0 not taken
                      663: branch 1 taken
     432              663:     if (m_pathWriter) {
     433                 :       std::vector<unsigned char> concreteBranches;
     434                 :       m_pathWriter->readStream(m_interpreter->getPathStreamID(state),
     435                0:                                concreteBranches);
     436                0:       std::ostream *f = openTestFile("path", id);
     437                 :       std::copy(concreteBranches.begin(), concreteBranches.end(), 
     438                0:                 std::ostream_iterator<unsigned char>(*f, "\n"));
                        0: branch 0 not taken
                        0: branch 1 not taken
     439                0:       delete f;
     440                 :     }
     441                 :    
                      634: branch 0 taken
                       29: branch 1 taken
                        0: branch 2 not taken
                      634: branch 3 taken
                       29: branch 4 taken
                      634: branch 5 taken
     442             1297:     if (errorMessage || WritePCs) {
     443                 :       std::string constraints;
     444               29:       m_interpreter->getConstraintLog(state, constraints);
     445               29:       std::ostream *f = openTestFile("pc", id);
     446               29:       *f << constraints;
                       29: branch 0 taken
                        0: branch 1 not taken
     447               29:       delete f;
     448                 :     }
     449                 : 
                        1: branch 0 taken
                      662: branch 1 taken
     450              663:     if (WriteCVCs) {
     451                 :       std::string constraints;
     452                1:       m_interpreter->getConstraintLog(state, constraints, true);
     453                1:       std::ostream *f = openTestFile("cvc", id);
     454                1:       *f << constraints;
                        1: branch 0 taken
                        0: branch 1 not taken
     455                1:       delete f;
     456                 :     }
     457                 :     
                        0: branch 0 not taken
                      663: branch 1 taken
     458              663:     if (m_symPathWriter) {
     459                 :       std::vector<unsigned char> symbolicBranches;
     460                 :       m_symPathWriter->readStream(m_interpreter->getSymbolicPathStreamID(state),
     461                0:                                   symbolicBranches);
     462                0:       std::ostream *f = openTestFile("sym.path", id);
     463                 :       std::copy(symbolicBranches.begin(), symbolicBranches.end(), 
     464                0:                 std::ostream_iterator<unsigned char>(*f, "\n"));
                        0: branch 0 not taken
                        0: branch 1 not taken
     465                0:       delete f;
     466                 :     }
     467                 : 
                        2: branch 0 taken
                      661: branch 1 taken
     468              663:     if (WriteCov) {
     469                 :       std::map<const std::string*, std::set<unsigned> > cov;
     470                2:       m_interpreter->getCoveredLines(state, cov);
     471                2:       std::ostream *f = openTestFile("cov", id);
                        2: branch 0 taken
                        2: branch 1 taken
     472                6:       foreach(it, cov.begin(), cov.end()) {
                        4: branch 0 taken
                        2: branch 1 taken
     473               12:         foreach(it2, it->second.begin(), it->second.end())
     474               12:           *f << *it->first << ":" << *it2 << "\n";
     475                 :       }
                        2: branch 0 taken
                        0: branch 1 not taken
     476                2:       delete f;
     477                 :     }
     478                 : 
                        0: branch 0 not taken
                      663: branch 1 taken
     479              663:     if (WriteTraces) {
     480                0:       std::ostream *f = openTestFile("trace", id);
     481                0:       state.exeTraceMgr.printAllEvents(*f);
                        0: branch 0 not taken
                        0: branch 1 not taken
     482                0:       delete f;
     483                 :     }
     484                 : 
                        0: branch 0 not taken
                      663: branch 1 taken
     485             1326:     if (m_testIndex == StopAfterNTests)
     486                0:       m_interpreter->setHaltExecution(true);
     487                 :     
     488              663:     double elapsed_time = util::getWallTime() - start_time;
     489              663:     std::ostream *f = openTestFile("info", id);
     490                 :     *f << "Time to generate test case: " 
     491             1326:        << elapsed_time << "s\n";
                      663: branch 0 taken
                        0: branch 1 not taken
     492              663:     delete f;
     493                 :   }
     494              671: }
     495                 : 
     496                 :   // load a .path file
     497                 : void KleeHandler::loadPathFile(std::string name, 
     498                1:                                      std::vector<bool> &buffer) {
     499                1:   std::ifstream f(name.c_str(), std::ios::in | std::ios::binary);
     500                 : 
                        0: branch 0 not taken
                        1: branch 1 taken
     501                1:   if (!f.good())
     502                0:     assert(0 && "unable to open path file");
     503                 : 
                        6: branch 0 taken
                        1: branch 1 taken
     504                7:   while (f.good()) {
     505                 :     unsigned value;
     506                 :     f >> value;
     507                6:     buffer.push_back(!!value);
     508                6:     f.get();
     509                1:   }
     510                1: }
     511                 : 
     512                 : void KleeHandler::getOutFiles(std::string path,
     513                1: 			      std::vector<std::string> &results) {
     514                1:   llvm::sys::Path p(path);
     515                 :   std::set<llvm::sys::Path> contents;
     516                 :   std::string error;
                        0: branch 1 not taken
                        1: branch 2 taken
     517                1:   if (p.getDirectoryContents(contents, &error)) {
     518                0:     llvm::cerr << "ERROR: unable to read output directory: " << path << ": " << error << "\n";
     519                0:     exit(1);
     520                 :   }
                        8: branch 1 taken
                        1: branch 2 taken
     521               18:   foreach(it, contents.begin(), contents.end()) {
     522                8:     std::string f = it->toString();
                        1: branch 2 taken
                        7: branch 3 taken
     523               16:     if (f.substr(f.size()-5,f.size()) == ".bout") {
     524                1:       results.push_back(f);
     525                 :     }
     526                1:   }
     527                1: }
     528                 : 
     529                 : //===----------------------------------------------------------------------===//
     530                 : // main Driver function
     531                 : //
     532                 : #if ENABLE_STPLOG == 1
     533                 : extern "C" void STPLOG_init(const char *);
     534                 : #endif
     535                 : 
     536                2: static std::string strip(std::string &in) {
     537                2:   unsigned len = in.size();
     538                2:   unsigned lead = 0, trail = len;
                        2: branch 0 taken
                        1: branch 1 taken
                        1: branch 3 taken
                        1: branch 4 taken
                        1: branch 5 taken
                        2: branch 6 taken
     539                7:   while (lead<len && isspace(in[lead]))
     540                1:     ++lead;
                        2: branch 0 taken
                        1: branch 1 taken
                        1: branch 3 taken
                        1: branch 4 taken
                        1: branch 5 taken
                        2: branch 6 taken
     541                5:   while (trail>lead && isspace(in[trail-1]))
     542                1:     --trail;
     543                2:   return in.substr(lead, trail-lead);
     544                 : }
     545                 : 
     546                1: static void readArgumentsFromFile(char *file, std::vector<std::string> &results) {
     547                1:   std::ifstream f(file);
                        0: branch 0 not taken
                        1: branch 1 taken
     548                1:   assert(f.is_open() && "unable to open input for reading arguments");
                        2: branch 1 taken
                        1: branch 2 taken
     549                5:   while (!f.eof()) {
     550                 :     std::string line;
     551                2:     std::getline(f, line);
     552                4:     line = strip(line);
                        1: branch 0 taken
                        1: branch 1 taken
     553                2:     if (!line.empty())
     554                1:       results.push_back(line);
     555                 :   }
     556                1:   f.close();
     557                1: }
     558                 : 
     559              103: static void parseArguments(int argc, char **argv) {
     560                 :   std::vector<std::string> arguments;
     561                 : 
                      270: branch 0 taken
                      103: branch 1 taken
     562              373:   for (int i=1; i<argc; i++) {
                        1: branch 1 taken
                      269: branch 2 taken
                        1: branch 3 taken
                        0: branch 4 not taken
     563              271:     if (!strcmp(argv[i],"--read-args") && i+1<argc) {
     564                1:       readArgumentsFromFile(argv[++i], arguments);
     565                 :     } else {
     566              269:       arguments.push_back(argv[i]);
     567                 :     }
     568                 :   }
     569                 :     
     570              103:   int numArgs = arguments.size() + 1;
     571              103:   const char **argArray = new const char*[numArgs+1];
     572              103:   argArray[0] = argv[0];
     573              103:   argArray[numArgs] = 0;
                      270: branch 0 taken
                      103: branch 1 taken
     574              373:   for (int i=1; i<numArgs; i++) {
     575              540:     argArray[i] = arguments[i-1].c_str();
     576                 :   }
     577                 : 
     578              103:   cl::ParseCommandLineOptions(numArgs, (char**) argArray, " klee\n");
                      103: branch 0 taken
                        0: branch 1 not taken
     579              103:   delete[] argArray;
     580              103: }
     581                 : 
     582                 : 
     583                 : 
     584                0: static int initEnv(Module *mainModule) {
     585                 : 
     586                 :   /*
     587                 :     nArgcP = alloc oldArgc->getType()
     588                 :     nArgvV = alloc oldArgv->getType()
     589                 :     store oldArgc nArgcP
     590                 :     store oldArgv nArgvP
     591                 :     klee_init_environment(nArgcP, nArgvP)
     592                 :     nArgc = load nArgcP
     593                 :     nArgv = load nArgvP
     594                 :     oldArgc->replaceAllUsesWith(nArgc)
     595                 :     oldArgv->replaceAllUsesWith(nArgv)
     596                 :   */
     597                 : 
     598                0:   Function *mainFn = mainModule->getFunction("main");
     599                 :     
                        0: branch 1 not taken
                        0: branch 2 not taken
     600                0:   if (mainFn->arg_size() < 2) {
     601                 :     llvm::cerr << "Cannot handle ""-init-env"" when main() has less than two arguments.\n";
     602                0:     return -1;
     603                 :   }
     604                 : 
     605                0:   Instruction* firstInst = mainFn->begin()->begin();
     606                 : 
     607                0:   Value* oldArgc = mainFn->arg_begin();
     608                0:   Value* oldArgv = ++mainFn->arg_begin();
     609                 :   
     610                0:   AllocaInst* argcPtr = new AllocaInst(oldArgc->getType(), "argcPtr", firstInst);
     611                0:   AllocaInst* argvPtr = new AllocaInst(oldArgv->getType(), "argvPtr", firstInst);
     612                 : 
     613                 :   /* Insert void klee_init_env(int* argc, char*** argv) */
     614                 :   std::vector<const Type*> params;
     615                0:   params.push_back(Type::Int32Ty);
     616                0:   params.push_back(Type::Int32Ty);
     617                 :   Function* initEnvFn = 
     618                 :     cast<Function>(mainModule->getOrInsertFunction("klee_init_env",
     619                 :                                                    Type::VoidTy,
     620                 :                                                    argcPtr->getType(),
     621                 :                                                    argvPtr->getType(),
     622                0:                                                    NULL));
                        0: branch 0 not taken
                        0: branch 1 not taken
     623                0:   assert(initEnvFn);    
     624                 :   std::vector<Value*> args;
     625                0:   args.push_back(argcPtr);
     626                0:   args.push_back(argvPtr);
     627                 :   Instruction* initEnvCall = CallInst::Create(initEnvFn, args.begin(), args.end(), 
     628                0: 					      "", firstInst);
     629                0:   Value *argc = new LoadInst(argcPtr, "newArgc", firstInst);
     630                0:   Value *argv = new LoadInst(argvPtr, "newArgv", firstInst);
     631                 :   
     632                0:   oldArgc->replaceAllUsesWith(argc);
     633                0:   oldArgv->replaceAllUsesWith(argv);
     634                 : 
     635                0:   new StoreInst(oldArgc, argcPtr, initEnvCall);
     636                0:   new StoreInst(oldArgv, argvPtr, initEnvCall);
     637                 : 
     638                0:   return 0;
     639                 : }
     640                 : 
     641                 : 
     642                 : // This is a terrible hack until we get some real modelling of the
     643                 : // system. All we do is check the undefined symbols and m and warn about
     644                 : // any "unrecognized" externals and about any obviously unsafe ones.
     645                 : 
     646                 : // Symbols we explicitly support
     647                 : static const char *modelledExternals[] = {
     648                 :   "_ZTVN10__cxxabiv117__class_type_infoE",
     649                 :   "_ZTVN10__cxxabiv120__si_class_type_infoE",
     650                 :   "_ZTVN10__cxxabiv121__vmi_class_type_infoE",
     651                 : 
     652                 :   // special functions
     653                 :   "_assert", 
     654                 :   "__assert_fail", 
     655                 :   "__assert_rtn", 
     656                 :   "calloc", 
     657                 :   "_exit", 
     658                 :   "exit", 
     659                 :   "free", 
     660                 :   "abort", 
     661                 :   "klee_abort", 
     662                 :   "klee_assume", 
     663                 :   "klee_check_memory_access",
     664                 :   "klee_define_fixed_object",
     665                 :   "klee_get_errno", 
     666                 :   "klee_get_value",
     667                 :   "klee_get_obj_size", 
     668                 :   "klee_is_symbolic", 
     669                 :   "klee_make_symbolic_name", 
     670                 :   "klee_mark_global", 
     671                 :   "klee_malloc_n", 
     672                 :   "klee_merge", 
     673                 :   "klee_prefer_cex",
     674                 :   "klee_print_expr", 
     675                 :   "klee_print_range", 
     676                 :   "klee_report_error", 
     677                 :   "klee_revirt_objects", 
     678                 :   "klee_set_forking",
     679                 :   "klee_silent_exit", 
     680                 :   "klee_under_constrained", 
     681                 :   "klee_warning", 
     682                 :   "klee_warning_once", 
     683                 :   "klee_alias_function",
     684                 :   "llvm.dbg.stoppoint", 
     685                 :   "llvm.va_start", 
     686                 :   "llvm.va_end", 
     687                 :   "malloc", 
     688                 :   "realloc", 
     689                 :   "_ZdaPv", 
     690                 :   "_ZdlPv", 
     691                 :   "_Znaj", 
     692                 :   "_Znwj", 
     693                 :   "_Znam", 
     694                 :   "_Znwm", 
     695                 : };
     696                 : // Symbols we aren't going to warn about
     697                 : static const char *dontCareExternals[] = {
     698                 : #if 0
     699                 :   // stdio
     700                 :   "fprintf",
     701                 :   "fflush",
     702                 :   "fopen",
     703                 :   "fclose",
     704                 :   "fputs_unlocked",
     705                 :   "putchar_unlocked",
     706                 :   "vfprintf",
     707                 :   "fwrite",
     708                 :   "puts",
     709                 :   "printf",
     710                 :   "stdin",
     711                 :   "stdout",
     712                 :   "stderr",
     713                 :   "_stdio_term",
     714                 :   "__errno_location",
     715                 :   "fstat",
     716                 : #endif
     717                 : 
     718                 :   // static information, pretty ok to return
     719                 :   "getegid",
     720                 :   "geteuid",
     721                 :   "getgid",
     722                 :   "getuid",
     723                 :   "getpid",
     724                 :   "gethostname",
     725                 :   "getpgrp",
     726                 :   "getppid",
     727                 :   "getpagesize",
     728                 :   "getpriority",
     729                 :   "getgroups",
     730                 :   "getdtablesize",
     731                 :   "getrlimit",
     732                 :   "getrlimit64",
     733                 :   "getcwd",
     734                 :   "getwd",
     735                 :   "gettimeofday",
     736                 :   "uname",
     737                 : 
     738                 :   // fp stuff we just don't worry about yet
     739                 :   "frexp",  
     740                 :   "ldexp",
     741                 :   "__isnan",
     742                 :   "__signbit",
     743                 : };
     744                 : // Extra symbols we aren't going to warn about with klee-libc
     745                 : static const char *dontCareKlee[] = {
     746                 :   "__ctype_b_loc",
     747                 :   "__ctype_get_mb_cur_max",
     748                 : 
     749                 :   // io system calls
     750                 :   "open",
     751                 :   "write",
     752                 :   "read",
     753                 :   "close",
     754                 : };
     755                 : // Extra symbols we aren't going to warn about with uclibc
     756                 : static const char *dontCareUclibc[] = {
     757                 :   "__dso_handle",
     758                 : 
     759                 :   // Don't warn about these since we explicitly commented them out of
     760                 :   // uclibc.
     761                 :   "printf",
     762                 :   "vprintf"
     763                 : };
     764                 : // Symbols we consider unsafe
     765                 : static const char *unsafeExternals[] = {
     766                 :   "fork", // oh lord
     767                 :   "exec", // heaven help us
     768                 :   "error", // calls _exit
     769                 :   "raise", // yeah
     770                 :   "kill", // mmmhmmm
     771                 : };
     772                 : #define NELEMS(array) (sizeof(array)/sizeof(array[0]))
     773              103: void externalsAndGlobalsCheck(const Module *m) {
     774                 :   std::map<std::string, bool> externals;
     775                 :   std::set<std::string> modelled(modelledExternals, 
     776              103:                                  modelledExternals+NELEMS(modelledExternals));
     777                 :   std::set<std::string> dontCare(dontCareExternals, 
     778              103:                                  dontCareExternals+NELEMS(dontCareExternals));
     779                 :   std::set<std::string> unsafe(unsafeExternals, 
     780              103:                                unsafeExternals+NELEMS(unsafeExternals));
     781                 : 
                        6: branch 0 taken
                        3: branch 1 taken
                       94: branch 2 taken
     782              103:   switch (Libc) {
     783                 :   case KleeLibc: 
     784                6:     dontCare.insert(dontCareKlee, dontCareKlee+NELEMS(dontCareKlee));
     785                 :     break;
     786                 :   case UcLibc:
     787                 :     dontCare.insert(dontCareUclibc,
     788                3:                     dontCareUclibc+NELEMS(dontCareUclibc));
     789                 :     break;
     790                 :   case NoLibc: /* silence compiler warning */
     791                 :     break;
     792                 :   }
     793                 :   
     794                 : 
                        0: branch 0 not taken
                      103: branch 1 taken
     795              103:   if (WithFileModel != None) {
     796                0:     dontCare.insert("syscall");
     797                 :   }
     798                 : 
                     1088: branch 1 taken
                      103: branch 2 taken
     799             2279:   foreach(fnIt, m->begin(), m->end()) {
                      568: branch 1 taken
                      520: branch 2 taken
                      471: branch 3 taken
                       97: branch 4 taken
                      471: branch 5 taken
                      617: branch 6 taken
     800             2224:     if (fnIt->isDeclaration() && !fnIt->use_empty())
     801             1884:       externals.insert(std::make_pair(fnIt->getName(), false));
                     8981: branch 1 taken
                     1088: branch 2 taken
     802            20138:     foreach(bbIt, fnIt->begin(), fnIt->end()) {
                    92853: branch 1 taken
                     8981: branch 2 taken
     803           203668:       foreach(it, bbIt->begin(), bbIt->end()) {
                     2484: branch 0 taken
                    90369: branch 1 taken
     804            92853:         if (const CallInst *ci = dyn_cast<CallInst>(it)) {
                        0: branch 0 not taken
                     2484: branch 1 taken
     805             4968:           if (isa<InlineAsm>(ci->getCalledValue())) {
     806                 :             klee_warning_once(&*fnIt,
     807                 :                               "function \"%s\" has inline asm", 
     808                0:                               fnIt->getName().c_str());
     809                 :           }
     810                 :         }
     811                 :       }
     812                 :     }
     813                 :   }
                     8205: branch 1 taken
                      103: branch 2 taken
     814            16616:   foreach(it, m->global_begin(), m->global_end())
                       12: branch 1 taken
                     8193: branch 2 taken
                       12: branch 3 taken
                        0: branch 4 not taken
                       12: branch 5 taken
                     8193: branch 6 taken
     815             8229:     if (it->isDeclaration() && !it->use_empty())
     816               48:       externals.insert(std::make_pair(it->getName(), true));
     817                 :   // and remove aliases (they define the symbol after global
     818                 :   // initialization)
                       10: branch 1 taken
                      103: branch 2 taken
     819              226:   foreach(it, m->alias_begin(), m->alias_end()) {
     820               20:     let(it2, externals.find(it->getName()));
                        0: branch 0 not taken
                       10: branch 1 taken
     821               10:     if (it2!=externals.end())
     822                0:       externals.erase(it2);
     823                 :   }
     824                 : 
     825                 :   std::map<std::string, bool> foundUnsafe;
                      483: branch 0 taken
                      103: branch 1 taken
     826              689:   foreach(it, externals.begin(), externals.end()) {
     827              483:     const std::string &ext = it->first;
                      108: branch 1 taken
                      375: branch 2 taken
                      108: branch 3 taken
                        0: branch 4 not taken
                       90: branch 6 taken
                       18: branch 7 taken
                       90: branch 8 taken
                      393: branch 9 taken
     828              591:     if (!modelled.count(ext) && (WarnAllExternals || 
     829                 :                                  !dontCare.count(ext))) {
                        2: branch 1 taken
                       88: branch 2 taken
     830               90:       if (unsafe.count(ext)) {
     831                 :         foundUnsafe.insert(*it);
     832                 :       } else {
     833                 :         klee_warning("undefined reference to %s: %s",
     834                 :                      it->second ? "variable" : "function",
                        9: branch 0 taken
                       79: branch 1 taken
     835               88:                      ext.c_str());
     836                 :       }
     837                 :     }
     838                 :   }
     839                 : 
                        2: branch 0 taken
                      103: branch 1 taken
     840              208:   foreach(it, foundUnsafe.begin(), foundUnsafe.end()) {
     841                2:     const std::string &ext = it->first;
     842                 :     klee_warning("undefined reference to %s: %s (UNSAFE)!",
     843                 :                  it->second ? "variable" : "function",
                        0: branch 0 not taken
                        2: branch 1 taken
     844                2:                  ext.c_str());
     845                 :   }
     846              103: }
     847                 : 
     848                 : static Interpreter *theInterpreter = 0;
     849                 : 
     850                 : static bool interrupted = false;
     851                 : 
     852                 : // Pulled out so it can be easily called from a debugger.
     853                 : extern "C"
     854                0: void halt_execution() {
     855                0:   theInterpreter->setHaltExecution(true);
     856                0: }
     857                 : 
     858                 : extern "C"
     859                0: void stop_forking() {
     860                0:   theInterpreter->setInhibitForking(true);
     861                0: }
     862                 : 
     863                0: static void interrupt_handle() {
                        0: branch 0 not taken
                        0: branch 1 not taken
                        0: branch 2 not taken
                        0: branch 3 not taken
     864                0:   if (!interrupted && theInterpreter) {
     865                 :     llvm::cerr << "KLEE: ctrl-c detected, requesting interpreter to halt.\n";
     866                0:     halt_execution();
     867                0:     sys::SetInterruptFunction(interrupt_handle);
     868                 :   } else {
     869                 :     llvm::cerr << "KLEE: ctrl-c detected, exiting.\n";
     870                0:     exit(1);
     871                 :   }
     872                0:   interrupted = true;
     873                0: }
     874                 : 
     875                 : // This is a temporary hack. If the running process has access to
     876                 : // externals then it can disable interrupts, which screws up the
     877                 : // normal "nice" watchdog termination process. We try to request the
     878                 : // interpreter to halt using this mechanism as a last resort to save
     879                 : // the state data before going ahead and killing it.
     880                 : static void halt_via_gdb(int pid) {
     881                 :   char buffer[256];
     882                 :   sprintf(buffer, 
     883                 :           "gdb --batch --eval-command=\"p halt_execution()\" "
     884                 :           "--eval-command=detach --pid=%d &> /dev/null",
     885                 :           pid);
     886                 :   //  fprintf(stderr, "KLEE: WATCHDOG: running: %s\n", buffer);
                        0: branch 1 not taken
                        0: branch 2 not taken
     887                0:   if (system(buffer)==-1) 
     888                0:     perror("system");
     889                 : }
     890                 : 
     891                 : // returns the end of the string put in buf
     892              103: static char *format_tdiff(char *buf, long seconds)
     893                 : {
                        0: branch 0 not taken
                      103: branch 1 taken
     894              103:   assert(seconds >= 0);
     895                 : 
     896              103:   long minutes = seconds / 60;  seconds %= 60;
     897              103:   long hours   = minutes / 60;  minutes %= 60;
     898              103:   long days    = hours   / 24;  hours   %= 24;
     899                 : 
     900              103:   buf = strrchr(buf, '\0');
                        0: branch 0 not taken
                      103: branch 1 taken
     901              103:   if (days > 0) buf += sprintf(buf, "%ld days, ", days);
     902              103:   buf += sprintf(buf, "%02ld:%02ld:%02ld", hours, minutes, seconds);
     903              103:   return buf;
     904                 : }
     905                 : 
     906                 : // FIXME: I don't belong here (or anywhere?)
     907                 : 
     908                 : #include <sys/stat.h>
     909                 : static const char *mostRecent(const char *a, const char *b) {
     910                 :   struct stat a_st, b_st;
                        0: branch 0 not taken
                        6: branch 1 taken
     911                6:   if (stat(a, &a_st)==-1) return b;
                        0: branch 0 not taken
                        6: branch 1 taken
     912                6:   if (stat(b, &b_st)==-1) return a;
                        0: branch 0 not taken
                        6: branch 1 taken
     913                6:   return (a_st.st_mtime < b_st.st_mtime) ? b : a;
     914                 : }
     915                 : 
     916                 : #ifndef KLEE_UCLIBC
     917                 : static llvm::Module *linkWithUclibc(llvm::Module *mainModule) {
     918                 :   fprintf(stderr, "error: invalid libc, no uclibc support!\n");
     919                 :   exit(1);
     920                 :   return 0;
     921                 : }
     922                 : #else
     923                3: static llvm::Module *linkWithUclibc(llvm::Module *mainModule) {
     924                 :   Function *f;
     925                 :   // force import of __uClibc_main
     926                 :   mainModule->getOrInsertFunction("__uClibc_main",
     927                 :                                   FunctionType::get(Type::VoidTy,
     928                 :                                                     std::vector<const Type*>(),
     929                9:                                                     true));
     930                 :   
     931                 :   // force various imports
                        0: branch 0 not taken
                        3: branch 1 taken
     932                3:   if (WithFileModel != None) {
     933                 :     mainModule->getOrInsertFunction("realpath",
     934                 :                                     PointerType::getUnqual(Type::Int8Ty),
     935                 :                                     PointerType::getUnqual(Type::Int8Ty),
     936                 :                                     PointerType::getUnqual(Type::Int8Ty),
     937                0:                                     NULL);
     938                 :     mainModule->getOrInsertFunction("getutent",
     939                 :                                     PointerType::getUnqual(Type::Int8Ty),
     940                0:                                     NULL);
     941                 :     mainModule->getOrInsertFunction("__fgetc_unlocked",
     942                 :                                     Type::Int32Ty,
     943                 :                                     PointerType::getUnqual(Type::Int8Ty),
     944                0:                                     NULL);
     945                 :     mainModule->getOrInsertFunction("__fputc_unlocked",
     946                 :                                     Type::Int32Ty,
     947                 :                                     Type::Int32Ty,
     948                 :                                     PointerType::getUnqual(Type::Int8Ty),
     949                0:                                     NULL);
     950                 :   }
     951                 : 
     952                3:   f = mainModule->getFunction("__ctype_get_mb_cur_max");
                        0: branch 0 not taken
                        3: branch 1 taken
     953                3:   if (f) f->setName("_stdlib_mb_cur_max");
     954                 : 
     955                 :   // Strip of asm prefixes for 64 bit versions because they are not
     956                 :   // present in uclibc and we want to make sure stuff will get
     957                 :   // linked. In the off chance that both prefixed and unprefixed
     958                 :   // versions are present in the module, make sure we don't create a
     959                 :   // naming conflict.
                       17: branch 1 taken
                        3: branch 2 taken
     960               37:   for (Module::iterator fi = mainModule->begin(), fe = mainModule->end();
     961                 :        fi != fe;) {
     962               17:     Function *f = fi;
     963               17:     ++fi;
     964               34:     const std::string &name = f->getName();
                        0: branch 0 not taken
                       17: branch 1 taken
     965               17:     if (name[0]=='\01') {
     966                0:       unsigned size = name.size();
                        0: branch 0 not taken
                        0: branch 1 not taken
                        0: branch 2 not taken
                        0: branch 3 not taken
                        0: branch 4 not taken
                        0: branch 5 not taken
     967                0:       if (name[size-2]=='6' && name[size-1]=='4') {
     968                0:         std::string unprefixed = name.substr(1);
     969                 : 
     970                 :         // See if the unprefixed version exists.
                        0: branch 1 not taken
                        0: branch 2 not taken
     971                0:         if (Function *f2 = mainModule->getFunction(unprefixed)) {
     972                0:           f->replaceAllUsesWith(f2);
     973                0:           f->eraseFromParent();
     974                 :         } else {
     975                0:           f->setName(unprefixed);
     976                0:         }
     977                 :       }
     978                 :     }
     979                 :   }
     980                 :   
     981                 :   mainModule = klee::linkWithLibrary(mainModule, 
     982                3:                                      KLEE_UCLIBC "/lib/libc.a");
                        0: branch 0 not taken
                        3: branch 1 taken
     983                3:   assert(mainModule && "unable to link with uclibc");
     984                 : 
     985                 :   // more sighs, this is horrible but just a temp hack
     986                 :   //    f = mainModule->getFunction("__fputc_unlocked");
     987                 :   //    if (f) f->setName("fputc_unlocked");
     988                 :   //    f = mainModule->getFunction("__fgetc_unlocked");
     989                 :   //    if (f) f->setName("fgetc_unlocked");
     990                 :   
     991                 :   Function *f2;
     992                3:   f = mainModule->getFunction("open");
     993                3:   f2 = mainModule->getFunction("__libc_open");
                        3: branch 0 taken
                        0: branch 1 not taken
     994                3:   if (f2) {
                        0: branch 0 not taken
                        3: branch 1 taken
     995                3:     if (f) {
     996                0:       f2->replaceAllUsesWith(f);
     997                0:       f2->eraseFromParent();
     998                 :     } else {
     999                3:       f2->setName("open");
                        0: branch 0 not taken
                        3: branch 1 taken
    1000                6:       assert(f2->getName() == "open");
    1001                 :     }
    1002                 :   }
    1003                 : 
    1004                3:   f = mainModule->getFunction("fcntl");
    1005                3:   f2 = mainModule->getFunction("__libc_fcntl");
                        3: branch 0 taken
                        0: branch 1 not taken
    1006                3:   if (f2) {
                        0: branch 0 not taken
                        3: branch 1 taken
    1007                3:     if (f) {
    1008                0:       f2->replaceAllUsesWith(f);
    1009                0:       f2->eraseFromParent();
    1010                 :     } else {
    1011                3:       f2->setName("fcntl");
                        0: branch 0 not taken
                        3: branch 1 taken
    1012                6:       assert(f2->getName() == "fcntl");
    1013                 :     }
    1014                 :   }
    1015                 : 
    1016                 :   // XXX we need to rearchitect so this can also be used with
    1017                 :   // programs externally linked with uclibc.
    1018                 : 
    1019                 :   // We now need to swap things so that __uClibc_main is the entry
    1020                 :   // point, in such a way that the arguments are passed to
    1021                 :   // __uClibc_main correctly. We do this by renaming the user main
    1022                 :   // and generating a stub function to call __uClibc_main. There is
    1023                 :   // also an implicit cooperation in that runFunctionAsMain sets up
    1024                 :   // the environment arguments to what uclibc expects (following
    1025                 :   // argv), since it does not explicitly take an envp argument.
    1026                3:   Function *userMainFn = mainModule->getFunction("main");
                        0: branch 0 not taken
                        3: branch 1 taken
    1027                3:   assert(userMainFn && "unable to get user main");    
    1028                3:   Function *uclibcMainFn = mainModule->getFunction("__uClibc_main");
                        0: branch 0 not taken
                        3: branch 1 taken
    1029                3:   assert(uclibcMainFn && "unable to get uclibc main");    
    1030                3:   userMainFn->setName("__user_main");
    1031                 : 
    1032                3:   const FunctionType *ft = uclibcMainFn->getFunctionType();
                        0: branch 0 not taken
                        3: branch 1 taken
    1033                3:   assert(ft->getNumParams() == 7);
    1034                 : 
    1035                 :   std::vector<const Type*> fArgs;
    1036                3:   fArgs.push_back(ft->getParamType(1)); // argc
    1037                3:   fArgs.push_back(ft->getParamType(2)); // argv
    1038                 :   Function *stub = Function::Create(FunctionType::get(Type::Int32Ty, fArgs, false),
    1039                 :       			      GlobalVariable::ExternalLinkage,
    1040                 :       			      "main",
    1041                6:       			      mainModule);
    1042                6:   BasicBlock *bb = BasicBlock::Create("entry", stub);
    1043                 : 
    1044                 :   std::vector<llvm::Value*> args;
    1045                 :   args.push_back(llvm::ConstantExpr::getBitCast(userMainFn, 
    1046                3:                                                 ft->getParamType(0)));
    1047                3:   args.push_back(stub->arg_begin()); // argc
    1048                3:   args.push_back(++stub->arg_begin()); // argv    
    1049                3:   args.push_back(Constant::getNullValue(ft->getParamType(3))); // app_init
    1050                3:   args.push_back(Constant::getNullValue(ft->getParamType(4))); // app_fini
    1051                3:   args.push_back(Constant::getNullValue(ft->getParamType(5))); // rtld_fini
    1052                3:   args.push_back(Constant::getNullValue(ft->getParamType(6))); // stack_end
    1053                9:   CallInst::Create(uclibcMainFn, args.begin(), args.end(), "", bb);
    1054                 :   
    1055                3:   new UnreachableInst(bb);
    1056                 : 
    1057                6:   return mainModule;
    1058                 : }
    1059                 : #endif
    1060                 : 
    1061              103: int main(int argc, char **argv, char **envp) {  
    1062                 : #if ENABLE_STPLOG == 1
    1063                 :   STPLOG_init("stplog.c");
    1064                 : #endif
    1065                 : 
    1066              103:   atexit(llvm_shutdown);  // Call llvm_shutdown() on exit.
    1067              103:   parseArguments(argc, argv);
    1068              103:   sys::PrintStackTraceOnErrorSignal();
    1069                 : 
                        0: branch 0 not taken
                      103: branch 1 taken
    1070              103:   if (Watchdog) {
                        0: branch 0 not taken
                        0: branch 1 not taken
    1071                0:     if (MaxTime==0) {
    1072                0:       klee_error("--watchdog used without --max-time");
    1073                 :     }
    1074                 : 
    1075                0:     int pid = fork();
                        0: branch 0 not taken
                        0: branch 1 not taken
    1076                0:     if (pid<0) {
    1077                0:       klee_error("unable to fork watchdog");
                        0: branch 0 not taken
                        0: branch 1 not taken
    1078                0:     } else if (pid) {
    1079                0:       fprintf(stderr, "KLEE: WATCHDOG: watching %d\n", pid);
    1080                0:       fflush(stderr);
    1081                 : 
    1082                0:       double nextStep = util::getWallTime() + MaxTime*1.1;
    1083                0:       int level = 0;
    1084                 : 
    1085                 :       // Simple stupid code...
    1086                 :       while (1) {
    1087                0:         sleep(1);
    1088                 : 
    1089                0:         int status, res = waitpid(pid, &status, WNOHANG);
    1090                 : 
                        0: branch 0 not taken
                        0: branch 1 not taken
    1091                0:         if (res < 0) {
                        0: branch 1 not taken
                        0: branch 2 not taken
    1092                0:           if (errno==ECHILD) { // No child, no need to watch but
    1093                 :                                // return error since we didn't catch
    1094                 :                                // the exit.
    1095                0:             fprintf(stderr, "KLEE: watchdog exiting (no child)\n");
    1096                0:             return 1;
                        0: branch 1 not taken
                        0: branch 2 not taken
    1097                0:           } else if (errno!=EINTR) {
    1098                0:             perror("watchdog waitpid");
    1099                0:             exit(1);
    1100                 :           }
                        0: branch 0 not taken
                        0: branch 1 not taken
                        0: branch 2 not taken
                        0: branch 3 not taken
    1101                0:         } else if (res==pid && WIFEXITED(status)) {
    1102                0:           return WEXITSTATUS(status);
    1103                 :         } else {
    1104                0:           double time = util::getWallTime();
    1105                 : 
                        0: branch 0 not taken
                        0: branch 1 not taken
    1106                0:           if (time > nextStep) {
    1107                0:             ++level;
    1108                 :             
                        0: branch 0 not taken
                        0: branch 1 not taken
    1109                0:             if (level==1) {
    1110                0:               fprintf(stderr, "KLEE: WATCHDOG: time expired, attempting halt via INT\n");
    1111                0:               kill(pid, SIGINT);
                        0: branch 0 not taken
                        0: branch 1 not taken
    1112                0:             } else if (level==2) {
    1113                0:               fprintf(stderr, "KLEE: WATCHDOG: time expired, attempting halt via gdb\n");
    1114                 :               halt_via_gdb(pid);
    1115                 :             } else {
    1116                0:               fprintf(stderr, "KLEE: WATCHDOG: kill(9)ing child (I tried to be nice)\n");
    1117                0:               kill(pid, SIGKILL);
    1118                0:               return 1; // what more can we do
    1119                 :             }
    1120                 : 
    1121                 :             // Ideally this triggers a dump, which may take a while,
    1122                 :             // so try and give the process extra time to clean up.
    1123                0:             nextStep = util::getWallTime() + std::max(15., MaxTime*.1);
    1124                 :           }
    1125                 :         }
    1126                 :       }
    1127                 : 
    1128                 :       return 0;
    1129                 :     }
    1130                 :   }
    1131                 : 
    1132              103:   sys::SetInterruptFunction(interrupt_handle);
    1133                 : 
    1134                 :   // Load the bytecode...
    1135                 :   std::string ErrorMsg;
    1136              103:   ModuleProvider *MP = 0;
                      103: branch 0 taken
                        0: branch 1 not taken
    1137              103:   if (MemoryBuffer *Buffer = MemoryBuffer::getFileOrSTDIN(InputFile, &ErrorMsg)) {
    1138              103:     MP = getBitcodeModuleProvider(Buffer, &ErrorMsg);
                        0: branch 0 not taken
                      103: branch 1 taken
                      103: branch 2 taken
                      103: branch 3 taken
    1139              103:     if (!MP) delete Buffer;
    1140                 :   }
    1141                 :   
                        0: branch 0 not taken
                      103: branch 1 taken
    1142              103:   if (!MP)
    1143                0:     klee_error("error loading program '%s': %s", InputFile.c_str(), ErrorMsg.c_str());
    1144                 : 
    1145              103:   Module *mainModule = MP->materializeModule();
    1146              103:   MP->releaseModule();
                      103: branch 0 taken
                        0: branch 1 not taken
    1147              103:   delete MP;
    1148                 : 
                        0: branch 0 not taken
                      103: branch 1 taken
    1149              103:   assert(mainModule && "unable to materialize");
    1150                 :   
                        0: branch 0 not taken
                      103: branch 1 taken
    1151              103:   if (WithFileModel != None)
    1152                0:     InitEnv = true;
    1153                 :   
    1154                 : 
                        0: branch 0 not taken
                      103: branch 1 taken
    1155              103:   if (InitEnv) {
    1156                0:     int r = initEnv(mainModule);
                        0: branch 0 not taken
                        0: branch 1 not taken
    1157                0:     if (r != 0)
    1158                0:       return r;
    1159                 :   }
    1160                 : 
    1161                 :   
                        6: branch 0 taken
                        3: branch 1 taken
                       94: branch 2 taken
    1162              103:   switch (Libc) {
    1163                 :   case NoLibc: /* silence compiler warning */
    1164                 :     break;
    1165                 : 
    1166                 :   case KleeLibc: {
    1167                 :     // FIXME: Find a reasonable solution for this.
    1168                 :     const char *kleeLibcPath = 
    1169                 :       mostRecent(KLEE_DIR"/Release/lib/libklee-libc.bca",
    1170                6:                  KLEE_DIR"/Debug/lib/libklee-libc.bca");
    1171                6:     mainModule = klee::linkWithLibrary(mainModule, kleeLibcPath);
                        0: branch 0 not taken
                        6: branch 1 taken
    1172                6:     assert(mainModule && "unable to link with klee-libc");
    1173                 :     break;
    1174                 :   }
    1175                 : 
    1176                 :   case UcLibc:
    1177                3:     mainModule = linkWithUclibc(mainModule);
    1178                 :     break;
    1179                 :   }
    1180                 : 
                        0: branch 0 not taken
                      103: branch 1 taken
    1181              103:   if (WithFileModel != None) {
    1182                 :     const char* lib;
                        0: branch 0 not taken
                        0: branch 1 not taken
    1183                0:     if (WithFileModel == Debug)
    1184                0:       lib = KLEE_DIR"/Debug/lib/libkleeRuntimePOSIX.bca";
    1185                 :     else
    1186                0:       lib = KLEE_DIR"/Release/lib/libkleeRuntimePOSIX.bca";
    1187                 :     
    1188                0:     klee_message("NOTE: using model: %s", lib);
    1189                0:     mainModule = klee::linkWithLibrary(mainModule, lib);
                        0: branch 0 not taken
                        0: branch 1 not taken
    1190                0:     assert(mainModule && "unable to link with simple model");
    1191                 :   }  
    1192                 : 
    1193                 :   // Get the desired main function.  klee_main initializes uClibc locale and other 
    1194                 :   // data and then calls main.
    1195              103:   Function *mainFn = mainModule->getFunction("main");
                        0: branch 0 not taken
                      103: branch 1 taken
    1196              103:   if (!mainFn) {
    1197                 :     llvm::cerr << "'main' function not found in module.\n";
    1198                0:     return -1;
    1199                 :   }
    1200                 : 
    1201                 :   // FIXME: Change me to std types.
    1202                 :   int pArgc;
    1203                 :   char **pArgv;
    1204                 :   char **pEnvp;
                        0: branch 0 not taken
                      103: branch 1 taken
    1205              103:   if (Environ != "") {
    1206                 :     std::vector<std::string> items;
    1207                0:     std::ifstream f(Environ.c_str());
                        0: branch 0 not taken
                        0: branch 1 not taken
    1208                0:     if (!f.good())
    1209                0:       klee_error("unable to open --environ file: %s", Environ.c_str());
                        0: branch 1 not taken
                        0: branch 2 not taken
    1210                0:     while (!f.eof()) {
    1211                 :       std::string line;
    1212                0:       std::getline(f, line);
    1213                0:       line = strip(line);
                        0: branch 0 not taken
                        0: branch 1 not taken
    1214                0:       if (!line.empty())
    1215                0:         items.push_back(line);
    1216                 :     }
    1217                0:     f.close();
    1218                0:     pEnvp = new char *[items.size()+1];
    1219                0:     unsigned i=0;
                        0: branch 0 not taken
                        0: branch 1 not taken
    1220                0:     foreach(it, items.begin(), items.end())
    1221                0:       pEnvp[i++] = strdup(it->c_str());
    1222                0:     pEnvp[i] = 0;
    1223                 :   } else {
    1224              103:     pEnvp = envp;
    1225                 :   }
    1226                 : 
    1227              103:   pArgc = InputArgv.size() + 1; 
    1228              103:   pArgv = new char *[pArgc];
                      112: branch 0 taken
                      103: branch 1 taken
    1229              430:   for (unsigned i=0; i<InputArgv.size()+1; i++) {
                        9: branch 0 taken
                      103: branch 1 taken
    1230              121:     std::string &arg = (i==0 ? InputFile : InputArgv[i-1]);
    1231              112:     unsigned size = arg.size() + 1;
    1232              112:     char *pArg = new char[size];
    1233                 :     
    1234              112:     std::copy(arg.begin(), arg.end(), pArg);
    1235              112:     pArg[size - 1] = 0;
    1236                 :     
    1237              112:     pArgv[i] = pArg;
    1238                 :   }
    1239                 : 
    1240                 :   std::vector<bool> replayPath;
    1241                 : 
                        1: branch 0 taken
                      102: branch 1 taken
    1242              103:   if (ReplayPathFile != "") {
    1243                1:     KleeHandler::loadPathFile(ReplayPathFile, replayPath);
    1244                 :   }
    1245                 : 
    1246                 :   Interpreter::InterpreterOptions IOpts;
    1247              103:   IOpts.MakeConcreteSymbolic = MakeConcreteSymbolic;
    1248              103:   KleeHandler *handler = new KleeHandler(pArgc, pArgv);
    1249                 :   Interpreter *interpreter = 
    1250              103:     theInterpreter = Interpreter::create(IOpts, handler);
    1251              103:   handler->setInterpreter(interpreter);
    1252                 :   
                        0: branch 0 not taken
                      103: branch 1 taken
    1253              103:   if (ExcludeLibcCov) {
                        0: branch 0 not taken
                        0: branch 1 not taken
    1254                0:     if (Libc == NoLibc) {
    1255                 :       llvm::cerr << " --exclude-libc-cov: need to specify --libc=klee or --libc=uclibc\n";
    1256                0:       return -1;
    1257                 :     }
    1258                 :     
    1259                 :     // FIXME: Replace this functionality with something else. We can
    1260                 :     // do the scan internally, for example.
    1261                 : #if 0
    1262                 :     ExcludeCovFiles.push_back(KLEE_DIR"/conf/microlibc-functions.txt");      
    1263                 :     ExcludeCovFiles.push_back(mostRecent(KLEE_DIR"/Release/lib/intrinsic-fns.txt",
    1264                 :                                          KLEE_DIR"/Debug/lib/intrinsic-fns.txt"));
    1265                 : #endif
    1266                 :   }
    1267                 :   
    1268                 :   Interpreter::ModuleOptions Opts(/*Optimize=*/OptimizeModule, 
    1269              206:                                   /*CheckDivZero=*/CheckDivZero);
    1270                 :   const Module *finalModule = 
    1271              103:     interpreter->setModule(mainModule, Opts, ExcludeCovFiles);
    1272              103:   externalsAndGlobalsCheck(finalModule);
    1273                 : 
                        1: branch 0 taken
                      102: branch 1 taken
    1274              103:   if (ReplayPathFile != "") {
    1275                1:     interpreter->setReplayPath(&replayPath);
    1276                 :   }
    1277                 : 
    1278              206:   std::ostream *infoFile = handler->openOutputFile("info");
                      374: branch 0 taken
                      103: branch 1 taken
    1279              477:   for (int i=0; i<argc; i++) {
                      271: branch 0 taken
                      103: branch 1 taken
    1280              374:     *infoFile << argv[i] << (i+1<argc ? " ":"\n");
    1281                 :   }
    1282              103:   *infoFile << "PID: " << getpid() << "\n";
    1283              206:   llvm::cerr << "KLEE: PID: " << getpid() << "\n";
    1284                 : 
    1285                 :   char buf[256];
    1286                 :   time_t t[2];
    1287              103:   t[0] = time(NULL);
    1288              103:   strftime(buf, sizeof(buf), "Started: %Y-%m-%d %H:%M:%S\n", localtime(&t[0]));
    1289                 :   llvm::cerr << "KLEE: " << buf;
    1290              103:   *infoFile << buf;
    1291              103:   infoFile->flush();
    1292                 : 
                      102: branch 0 taken
                        1: branch 1 taken
                        0: branch 2 not taken
                      102: branch 3 taken
                        1: branch 4 taken
                      102: branch 5 taken
    1293              205:   if (!ReplayOutDir.empty() || !ReplayOutFile.empty()) {
                        0: branch 0 not taken
                        1: branch 1 taken
    1294                1:     assert(SeedOutFile.empty());
                        0: branch 0 not taken
                        1: branch 1 taken
    1295                1:     assert(SeedOutDir.empty());
    1296                 : 
    1297                 :     std::vector<std::string> outFiles = ReplayOutFile;
                        1: branch 0 taken
                        1: branch 1 taken
    1298                3:     foreach(it, ReplayOutDir.begin(), ReplayOutDir.end())
    1299                1:       KleeHandler::getOutFiles(*it, outFiles);    
    1300                 :     std::vector<BOut*> bOuts;
                        1: branch 0 taken
                        1: branch 1 taken
    1301                3:     foreach(it, outFiles.begin(), outFiles.end()) {
    1302                1:       BOut *out = bOut_fromFile(it->c_str());
                        1: branch 0 taken
                        0: branch 1 not taken
    1303                1:       if (out) {
    1304                1:         bOuts.push_back(out);
    1305                 :       } else {
    1306                0:         llvm::cerr << "KLEE: unable to open: " << *it << "\n";
    1307                 :       }
    1308                 :     }
    1309                 : 
                        0: branch 0 not taken
                        1: branch 1 taken
    1310                1:     if (RunInDir != "") {
    1311                0:       int res = chdir(RunInDir.c_str());
                        0: branch 0 not taken
                        0: branch 1 not taken
    1312                0:       if (res < 0) {
    1313                0:         klee_error("Unable to change directory to: %s", RunInDir.c_str());
    1314                 :       }
    1315                 :     }
    1316                 : 
    1317                1:     unsigned i=0;
                        1: branch 0 taken
                        1: branch 1 taken
    1318                3:     foreach(it, bOuts.begin(), bOuts.end()) {
    1319                1:       BOut *out = *it;
    1320                1:       interpreter->setReplayOut(out);
    1321                 :       llvm::cerr << "KLEE: replaying: " << *it << " (" << bOut_numBytes(out) << " bytes)"
    1322                5:                  << " (" << ++i << "/" << outFiles.size() << ")\n";
    1323                 :       // XXX should put envp in .bout ?
    1324                1:       interpreter->runFunctionAsMain(mainFn, out->numArgs, out->args, pEnvp);
                        1: branch 0 taken
                        0: branch 1 not taken
    1325                1:       if (interrupted) break;
    1326                 :     }
    1327                1:     interpreter->setReplayOut(0);
                        1: branch 0 taken
                        1: branch 1 taken
    1328                3:     while (!bOuts.empty()) {
    1329                1:       bOut_free(bOuts.back());
    1330                 :       bOuts.pop_back();
    1331                1:     }
    1332                 :   } else {
    1333                 :     std::vector<BOut *> seeds;
                        1: branch 0 taken
                      102: branch 1 taken
    1334              205:     foreach(it, SeedOutFile.begin(), SeedOutFile.end()) {
    1335                1:       BOut *out = bOut_fromFile(it->c_str());
                        0: branch 0 not taken
                        1: branch 1 taken
    1336                1:       if (!out) {
    1337                0:         llvm::cerr << "KLEE: unable to open: " << *it << "\n";
    1338                0:         exit(1);
    1339                 :       }
    1340                1:       seeds.push_back(out);
    1341                 :     } 
                        0: branch 1 not taken
                      102: branch 2 taken
    1342              204:     foreach(it, SeedOutDir.begin(), SeedOutDir.end()) {
    1343                 :       std::vector<std::string> outFiles;
    1344                0:       KleeHandler::getOutFiles(*it, outFiles);
                        0: branch 0 not taken
                        0: branch 1 not taken
    1345                0:       foreach(it2, outFiles.begin(), outFiles.end()) {
    1346                0:         BOut *out = bOut_fromFile(it2->c_str());
                        0: branch 0 not taken
                        0: branch 1 not taken
    1347                0:         if (!out) {
    1348                0:           llvm::cerr << "KLEE: unable to open: " << *it2 << "\n";
    1349                0:           exit(1);
    1350                 :         }
    1351                0:         seeds.push_back(out);
    1352                 :       }
                        0: branch 0 not taken
                        0: branch 1 not taken
    1353                0:       if (outFiles.empty()) {
    1354                0:         llvm::cerr << "KLEE: seeds directory is empty: " << *it << "\n";
    1355                0:         exit(1);
    1356                 :       }
    1357                 :     }
    1358                 :        
                        1: branch 0 taken
                      101: branch 1 taken
    1359              102:     if (!seeds.empty()) {
    1360                1:       llvm::cerr << "KLEE: using " << seeds.size() << " seeds\n";
    1361                1:       interpreter->useSeeds(&seeds);
    1362                 :     }
                        0: branch 0 not taken
                      102: branch 1 taken
    1363              102:     if (RunInDir != "") {
    1364                0:       int res = chdir(RunInDir.c_str());
                        0: branch 0 not taken
                        0: branch 1 not taken
    1365                0:       if (res < 0) {
    1366                0:         klee_error("Unable to change directory to: %s", RunInDir.c_str());
    1367                 :       }
    1368                 :     }
    1369              102:     interpreter->runFunctionAsMain(mainFn, pArgc, pArgv, pEnvp);
    1370                 : 
                        1: branch 0 taken
                      102: branch 1 taken
    1371              205:     foreach(it, seeds.begin(), seeds.end()) {
    1372                1:       bOut_free(*it);
    1373                 :     }
    1374                 :   }
    1375                 :       
    1376              103:   t[1] = time(NULL);
    1377              103:   strftime(buf, sizeof(buf), "Finished: %Y-%m-%d %H:%M:%S\n", localtime(&t[1]));
    1378                 :   llvm::cerr << "KLEE: " << buf;
    1379              103:   *infoFile << buf;
    1380                 : 
    1381                 :   strcpy(buf, "Elapsed: ");
    1382              103:   strcpy(format_tdiff(buf, t[1] - t[0]), "\n");
    1383                 :   llvm::cerr << "KLEE: " << buf;
    1384              103:   *infoFile << buf;
                      103: branch 0 taken
                        0: branch 1 not taken
    1385              103:   delete infoFile;
    1386                 : 
    1387                 :   // Free all the args.
                      112: branch 0 taken
                      103: branch 1 taken
    1388              430:   for (unsigned i=0; i<InputArgv.size()+1; i++)
                      112: branch 0 taken
                        0: branch 1 not taken
    1389              112:     delete[] pArgv[i];
                      103: branch 0 taken
                        0: branch 1 not taken
    1390              103:   delete[] pArgv;
    1391                 : 
                      103: branch 0 taken
                        0: branch 1 not taken
    1392              103:   delete interpreter;
    1393                 : 
    1394                 :   uint64_t queries = 
    1395              206:     *theStatisticManager->getStatisticByName("Queries");
    1396                 :   uint64_t queriesValid = 
    1397              206:     *theStatisticManager->getStatisticByName("QueriesValid");
    1398                 :   uint64_t queriesInvalid = 
    1399              206:     *theStatisticManager->getStatisticByName("QueriesInvalid");
    1400                 :   uint64_t queryCounterexamples = 
    1401              206:     *theStatisticManager->getStatisticByName("QueriesCEX");
    1402                 :   uint64_t queryConstructs = 
    1403              206:     *theStatisticManager->getStatisticByName("QueriesConstructs");
    1404                 :   uint64_t instructions = 
    1405              206:     *theStatisticManager->getStatisticByName("Instructions");
    1406                 :   llvm::cerr << "KLEE: done: total queries = " << queries << " ("
    1407                 :              << "valid: " << queriesValid << ", "
    1408                 :              << "invalid: " << queriesInvalid << ", "
    1409              412:              << "cex: " << queryCounterexamples << ")\n";
                       67: branch 0 taken
                       36: branch 1 taken
    1410              103:   if (queries)
    1411                 :     llvm::cerr << "KLEE: done: avg. constructs per query = " 
    1412              134:                << queryConstructs / queries << "\n";
    1413                 :   llvm::cerr << "KLEE: done: total instructions = " 
    1414              103:              << instructions << "\n";
    1415                 :   llvm::cerr << "KLEE: done: total tests = " 
    1416              206:              << handler->getNumTestCases() << "\n";
    1417                 : 
                      103: branch 0 taken
                        0: branch 1 not taken
    1418              103:   delete handler;
    1419                 : 
    1420              206:   return 0;
                      103: branch 0 taken
                        0: branch 1 not taken
                      103: branch 2 taken
                        0: branch 3 not taken
    1421              309: }

Generated: 2009-05-17 22:47 by zcov