1 //===-- Executor.cpp ------------------------------------------------------===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9
10 #include "Executor.h"
11
12 #include "Context.h"
13 #include "CoreStats.h"
14 #include "ExecutionState.h"
15 #include "ExternalDispatcher.h"
16 #include "GetElementPtrTypeIterator.h"
17 #include "ImpliedValue.h"
18 #include "Memory.h"
19 #include "MemoryManager.h"
20 #include "PTree.h"
21 #include "Searcher.h"
22 #include "SeedInfo.h"
23 #include "SpecialFunctionHandler.h"
24 #include "StatsTracker.h"
25 #include "TimingSolver.h"
26 #include "UserSearcher.h"
27
28 #include "klee/ADT/KTest.h"
29 #include "klee/ADT/RNG.h"
30 #include "klee/Config/Version.h"
31 #include "klee/Core/Interpreter.h"
32 #include "klee/Expr/ArrayExprOptimizer.h"
33 #include "klee/Expr/Assignment.h"
34 #include "klee/Expr/Expr.h"
35 #include "klee/Expr/ExprPPrinter.h"
36 #include "klee/Expr/ExprSMTLIBPrinter.h"
37 #include "klee/Expr/ExprUtil.h"
38 #include "klee/Module/Cell.h"
39 #include "klee/Module/InstructionInfoTable.h"
40 #include "klee/Module/KInstruction.h"
41 #include "klee/Module/KModule.h"
42 #include "klee/Solver/Common.h"
43 #include "klee/Solver/SolverCmdLine.h"
44 #include "klee/Solver/SolverStats.h"
45 #include "klee/Statistics/TimerStatIncrementer.h"
46 #include "klee/Support/Casting.h"
47 #include "klee/Support/ErrorHandling.h"
48 #include "klee/Support/FileHandling.h"
49 #include "klee/Support/FloatEvaluation.h"
50 #include "klee/Support/ModuleUtil.h"
51 #include "klee/Support/OptionCategories.h"
52 #include "klee/System/MemoryUsage.h"
53 #include "klee/System/Time.h"
54
55 #include "llvm/ADT/SmallPtrSet.h"
56 #include "llvm/ADT/StringExtras.h"
57 #include "llvm/IR/Attributes.h"
58 #include "llvm/IR/BasicBlock.h"
59 #if LLVM_VERSION_CODE < LLVM_VERSION(8, 0)
60 #include "llvm/IR/CallSite.h"
61 #endif
62 #include "llvm/IR/Constants.h"
63 #include "llvm/IR/DataLayout.h"
64 #include "llvm/IR/Function.h"
65 #include "llvm/IR/Instructions.h"
66 #include "llvm/IR/IntrinsicInst.h"
67 #include "llvm/IR/LLVMContext.h"
68 #include "llvm/IR/Module.h"
69 #include "llvm/IR/Operator.h"
70 #include "llvm/Support/CommandLine.h"
71 #include "llvm/Support/ErrorHandling.h"
72 #include "llvm/Support/FileSystem.h"
73 #include "llvm/Support/Path.h"
74 #include "llvm/Support/Process.h"
75 #if LLVM_VERSION_CODE >= LLVM_VERSION(10, 0)
76 #include "llvm/Support/TypeSize.h"
77 #else
78 typedef unsigned TypeSize;
79 #endif
80 #include "llvm/Support/raw_ostream.h"
81
82 #include <algorithm>
83 #include <cassert>
84 #include <cerrno>
85 #include <cstring>
86 #include <cxxabi.h>
87 #include <fstream>
88 #include <iomanip>
89 #include <iosfwd>
90 #include <limits>
91 #include <sstream>
92 #include <string>
93 #include <sys/mman.h>
94 #include <vector>
95
96 using namespace llvm;
97 using namespace klee;
98
99 namespace klee {
100 cl::OptionCategory DebugCat("Debugging options",
101 "These are debugging options.");
102
103 cl::OptionCategory ExtCallsCat("External call policy options",
104 "These options impact external calls.");
105
106 cl::OptionCategory SeedingCat(
107 "Seeding options",
108 "These options are related to the use of seeds to start exploration.");
109
110 cl::OptionCategory
111 TerminationCat("State and overall termination options",
112 "These options control termination of the overall KLEE "
113 "execution and of individual states.");
114
115 cl::OptionCategory TestGenCat("Test generation options",
116 "These options impact test generation.");
117
118 cl::opt<std::string> MaxTime(
119 "max-time",
120 cl::desc("Halt execution after the specified duration. "
121 "Set to 0s to disable (default=0s)"),
122 cl::init("0s"),
123 cl::cat(TerminationCat));
124 } // namespace klee
125
126 namespace {
127
128 /*** Test generation options ***/
129
130 cl::opt<bool> DumpStatesOnHalt(
131 "dump-states-on-halt",
132 cl::init(true),
133 cl::desc("Dump test cases for all active states on exit (default=true)"),
134 cl::cat(TestGenCat));
135
136 cl::opt<bool> OnlyOutputStatesCoveringNew(
137 "only-output-states-covering-new",
138 cl::init(false),
139 cl::desc("Only output test cases covering new code (default=false)"),
140 cl::cat(TestGenCat));
141
142 cl::opt<bool> EmitAllErrors(
143 "emit-all-errors", cl::init(false),
144 cl::desc("Generate tests cases for all errors "
145 "(default=false, i.e. one per (error,instruction) pair)"),
146 cl::cat(TestGenCat));
147
148
149 /* Constraint solving options */
150
151 cl::opt<unsigned> MaxSymArraySize(
152 "max-sym-array-size",
153 cl::desc(
154 "If a symbolic array exceeds this size (in bytes), symbolic addresses "
155 "into this array are concretized. Set to 0 to disable (default=0)"),
156 cl::init(0),
157 cl::cat(SolvingCat));
158
159 cl::opt<bool>
160 SimplifySymIndices("simplify-sym-indices",
161 cl::init(false),
162 cl::desc("Simplify symbolic accesses using equalities "
163 "from other constraints (default=false)"),
164 cl::cat(SolvingCat));
165
166 cl::opt<bool>
167 EqualitySubstitution("equality-substitution", cl::init(true),
168 cl::desc("Simplify equality expressions before "
169 "querying the solver (default=true)"),
170 cl::cat(SolvingCat));
171
172
173 /*** External call policy options ***/
174
175 enum class ExternalCallPolicy {
176 None, // No external calls allowed
177 Concrete, // Only external calls with concrete arguments allowed
178 All, // All external calls allowed
179 };
180
181 cl::opt<ExternalCallPolicy> ExternalCalls(
182 "external-calls",
183 cl::desc("Specify the external call policy"),
184 cl::values(
185 clEnumValN(
186 ExternalCallPolicy::None, "none",
187 "No external function calls are allowed. Note that KLEE always "
188 "allows some external calls with concrete arguments to go through "
189 "(in particular printf and puts), regardless of this option."),
190 clEnumValN(ExternalCallPolicy::Concrete, "concrete",
191 "Only external function calls with concrete arguments are "
192 "allowed (default)"),
193 clEnumValN(ExternalCallPolicy::All, "all",
194 "All external function calls are allowed. This concretizes "
195 "any symbolic arguments in calls to external functions.")
196 KLEE_LLVM_CL_VAL_END),
197 cl::init(ExternalCallPolicy::Concrete),
198 cl::cat(ExtCallsCat));
199
200 cl::opt<bool> SuppressExternalWarnings(
201 "suppress-external-warnings",
202 cl::init(false),
203 cl::desc("Supress warnings about calling external functions."),
204 cl::cat(ExtCallsCat));
205
206 cl::opt<bool> AllExternalWarnings(
207 "all-external-warnings",
208 cl::init(false),
209 cl::desc("Issue a warning everytime an external call is made, "
210 "as opposed to once per function (default=false)"),
211 cl::cat(ExtCallsCat));
212
213
214 /*** Seeding options ***/
215
216 cl::opt<bool> AlwaysOutputSeeds(
217 "always-output-seeds",
218 cl::init(true),
219 cl::desc(
220 "Dump test cases even if they are driven by seeds only (default=true)"),
221 cl::cat(SeedingCat));
222
223 cl::opt<bool> OnlyReplaySeeds(
224 "only-replay-seeds",
225 cl::init(false),
226 cl::desc("Discard states that do not have a seed (default=false)."),
227 cl::cat(SeedingCat));
228
229 cl::opt<bool> OnlySeed("only-seed",
230 cl::init(false),
231 cl::desc("Stop execution after seeding is done without "
232 "doing regular search (default=false)."),
233 cl::cat(SeedingCat));
234
235 cl::opt<bool>
236 AllowSeedExtension("allow-seed-extension",
237 cl::init(false),
238 cl::desc("Allow extra (unbound) values to become "
239 "symbolic during seeding (default=false)."),
240 cl::cat(SeedingCat));
241
242 cl::opt<bool> ZeroSeedExtension(
243 "zero-seed-extension",
244 cl::init(false),
245 cl::desc(
246 "Use zero-filled objects if matching seed not found (default=false)"),
247 cl::cat(SeedingCat));
248
249 cl::opt<bool> AllowSeedTruncation(
250 "allow-seed-truncation",
251 cl::init(false),
252 cl::desc("Allow smaller buffers than in seeds (default=false)."),
253 cl::cat(SeedingCat));
254
255 cl::opt<bool> NamedSeedMatching(
256 "named-seed-matching",
257 cl::init(false),
258 cl::desc("Use names to match symbolic objects to inputs (default=false)."),
259 cl::cat(SeedingCat));
260
261 cl::opt<std::string>
262 SeedTime("seed-time",
263 cl::desc("Amount of time to dedicate to seeds, before normal "
264 "search (default=0s (off))"),
265 cl::cat(SeedingCat));
266
267
268 /*** Termination criteria options ***/
269
270 cl::list<Executor::TerminateReason> ExitOnErrorType(
271 "exit-on-error-type",
272 cl::desc(
273 "Stop execution after reaching a specified condition (default=false)"),
274 cl::values(
275 clEnumValN(Executor::Abort, "Abort", "The program crashed"),
276 clEnumValN(Executor::Assert, "Assert", "An assertion was hit"),
277 clEnumValN(Executor::BadVectorAccess, "BadVectorAccess",
278 "Vector accessed out of bounds"),
279 clEnumValN(Executor::Exec, "Exec",
280 "Trying to execute an unexpected instruction"),
281 clEnumValN(Executor::External, "External",
282 "External objects referenced"),
283 clEnumValN(Executor::Free, "Free", "Freeing invalid memory"),
284 clEnumValN(Executor::Model, "Model", "Memory model limit hit"),
285 clEnumValN(Executor::Overflow, "Overflow", "An overflow occurred"),
286 clEnumValN(Executor::Ptr, "Ptr", "Pointer error"),
287 clEnumValN(Executor::ReadOnly, "ReadOnly", "Write to read-only memory"),
288 clEnumValN(Executor::ReportError, "ReportError",
289 "klee_report_error called"),
290 clEnumValN(Executor::User, "User", "Wrong klee_* functions invocation"),
291 clEnumValN(Executor::UncaughtException, "UncaughtException",
292 "Exception was not caught"),
293 clEnumValN(Executor::UnexpectedException, "UnexpectedException",
294 "An unexpected exception was thrown"),
295 clEnumValN(Executor::Unhandled, "Unhandled",
296 "Unhandled instruction hit") KLEE_LLVM_CL_VAL_END),
297 cl::ZeroOrMore,
298 cl::cat(TerminationCat));
299
300 cl::opt<unsigned long long> MaxInstructions(
301 "max-instructions",
302 cl::desc("Stop execution after this many instructions. Set to 0 to disable (default=0)"),
303 cl::init(0),
304 cl::cat(TerminationCat));
305
306 cl::opt<unsigned>
307 MaxForks("max-forks",
308 cl::desc("Only fork this many times. Set to -1 to disable (default=-1)"),
309 cl::init(~0u),
310 cl::cat(TerminationCat));
311
312 cl::opt<unsigned> MaxDepth(
313 "max-depth",
314 cl::desc("Only allow this many symbolic branches. Set to 0 to disable (default=0)"),
315 cl::init(0),
316 cl::cat(TerminationCat));
317
318 cl::opt<unsigned> MaxMemory("max-memory",
319 cl::desc("Refuse to fork when above this amount of "
320 "memory (in MB) (see -max-memory-inhibit) and terminate "
321 "states when additional 100MB allocated (default=2000)"),
322 cl::init(2000),
323 cl::cat(TerminationCat));
324
325 cl::opt<bool> MaxMemoryInhibit(
326 "max-memory-inhibit",
327 cl::desc(
328 "Inhibit forking when above memory cap (see -max-memory) (default=true)"),
329 cl::init(true),
330 cl::cat(TerminationCat));
331
332 cl::opt<unsigned> RuntimeMaxStackFrames(
333 "max-stack-frames",
334 cl::desc("Terminate a state after this many stack frames. Set to 0 to "
335 "disable (default=8192)"),
336 cl::init(8192),
337 cl::cat(TerminationCat));
338
339 cl::opt<double> MaxStaticForkPct(
340 "max-static-fork-pct", cl::init(1.),
341 cl::desc("Maximum percentage spent by an instruction forking out of the "
342 "forking of all instructions (default=1.0 (always))"),
343 cl::cat(TerminationCat));
344
345 cl::opt<double> MaxStaticSolvePct(
346 "max-static-solve-pct", cl::init(1.),
347 cl::desc("Maximum percentage of solving time that can be spent by a single "
348 "instruction over total solving time for all instructions "
349 "(default=1.0 (always))"),
350 cl::cat(TerminationCat));
351
352 cl::opt<double> MaxStaticCPForkPct(
353 "max-static-cpfork-pct", cl::init(1.),
354 cl::desc("Maximum percentage spent by an instruction of a call path "
355 "forking out of the forking of all instructions in the call path "
356 "(default=1.0 (always))"),
357 cl::cat(TerminationCat));
358
359 cl::opt<double> MaxStaticCPSolvePct(
360 "max-static-cpsolve-pct", cl::init(1.),
361 cl::desc("Maximum percentage of solving time that can be spent by a single "
362 "instruction of a call path over total solving time for all "
363 "instructions (default=1.0 (always))"),
364 cl::cat(TerminationCat));
365
366 cl::opt<std::string> TimerInterval(
367 "timer-interval",
368 cl::desc("Minimum interval to check timers. "
369 "Affects -max-time, -istats-write-interval, -stats-write-interval, and -uncovered-update-interval (default=1s)"),
370 cl::init("1s"),
371 cl::cat(TerminationCat));
372
373
374 /*** Debugging options ***/
375
376 /// The different query logging solvers that can switched on/off
377 enum PrintDebugInstructionsType {
378 STDERR_ALL, ///
379 STDERR_SRC,
380 STDERR_COMPACT,
381 FILE_ALL, ///
382 FILE_SRC, ///
383 FILE_COMPACT ///
384 };
385
386 llvm::cl::bits<PrintDebugInstructionsType> DebugPrintInstructions(
387 "debug-print-instructions",
388 llvm::cl::desc("Log instructions during execution."),
389 llvm::cl::values(
390 clEnumValN(STDERR_ALL, "all:stderr",
391 "Log all instructions to stderr "
392 "in format [src, inst_id, "
393 "llvm_inst]"),
394 clEnumValN(STDERR_SRC, "src:stderr",
395 "Log all instructions to stderr in format [src, inst_id]"),
396 clEnumValN(STDERR_COMPACT, "compact:stderr",
397 "Log all instructions to stderr in format [inst_id]"),
398 clEnumValN(FILE_ALL, "all:file",
399 "Log all instructions to file "
400 "instructions.txt in format [src, "
401 "inst_id, llvm_inst]"),
402 clEnumValN(FILE_SRC, "src:file",
403 "Log all instructions to file "
404 "instructions.txt in format [src, "
405 "inst_id]"),
406 clEnumValN(FILE_COMPACT, "compact:file",
407 "Log all instructions to file instructions.txt in format "
408 "[inst_id]") KLEE_LLVM_CL_VAL_END),
409 llvm::cl::CommaSeparated,
410 cl::cat(DebugCat));
411
412 #ifdef HAVE_ZLIB_H
413 cl::opt<bool> DebugCompressInstructions(
414 "debug-compress-instructions", cl::init(false),
415 cl::desc(
416 "Compress the logged instructions in gzip format (default=false)."),
417 cl::cat(DebugCat));
418 #endif
419
420 cl::opt<bool> DebugCheckForImpliedValues(
421 "debug-check-for-implied-values", cl::init(false),
422 cl::desc("Debug the implied value optimization"),
423 cl::cat(DebugCat));
424
425 } // namespace
426
427 // XXX hack
428 extern "C" unsigned dumpStates, dumpPTree;
429 unsigned dumpStates = 0, dumpPTree = 0;
430
431 const char *Executor::TerminateReasonNames[] = {
432 [ Abort ] = "abort",
433 [ Assert ] = "assert",
434 [ BadVectorAccess ] = "bad_vector_access",
435 [ Exec ] = "exec",
436 [ External ] = "external",
437 [ Free ] = "free",
438 [ Model ] = "model",
439 [ Overflow ] = "overflow",
440 [ Ptr ] = "ptr",
441 [ ReadOnly ] = "readonly",
442 [ ReportError ] = "reporterror",
443 [ User ] = "user",
444 [ UncaughtException ] = "uncaught_exception",
445 [ UnexpectedException ] = "unexpected_exception",
446 [ Unhandled ] = "xxx",
447 };
448
449
Executor(LLVMContext & ctx,const InterpreterOptions & opts,InterpreterHandler * ih)450 Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
451 InterpreterHandler *ih)
452 : Interpreter(opts), interpreterHandler(ih), searcher(0),
453 externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0),
454 pathWriter(0), symPathWriter(0), specialFunctionHandler(0), timers{time::Span(TimerInterval)},
455 replayKTest(0), replayPath(0), usingSeeds(0),
456 atMemoryLimit(false), inhibitForking(false), haltExecution(false),
457 ivcEnabled(false), debugLogBuffer(debugBufferString) {
458
459
460 const time::Span maxTime{MaxTime};
461 if (maxTime) timers.add(
__anon4d61836e0202null462 std::make_unique<Timer>(maxTime, [&]{
463 klee_message("HaltTimer invoked");
464 setHaltExecution(true);
465 }));
466
467 coreSolverTimeout = time::Span{MaxCoreSolverTime};
468 if (coreSolverTimeout) UseForkedCoreSolver = true;
469 Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
470 if (!coreSolver) {
471 klee_error("Failed to create core solver\n");
472 }
473
474 Solver *solver = constructSolverChain(
475 coreSolver,
476 interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME),
477 interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME),
478 interpreterHandler->getOutputFilename(ALL_QUERIES_KQUERY_FILE_NAME),
479 interpreterHandler->getOutputFilename(SOLVER_QUERIES_KQUERY_FILE_NAME));
480
481 this->solver = new TimingSolver(solver, EqualitySubstitution);
482 memory = new MemoryManager(&arrayCache);
483
484 initializeSearchOptions();
485
486 if (OnlyOutputStatesCoveringNew && !StatsTracker::useIStats())
487 klee_error("To use --only-output-states-covering-new, you need to enable --output-istats.");
488
489 if (DebugPrintInstructions.isSet(FILE_ALL) ||
490 DebugPrintInstructions.isSet(FILE_COMPACT) ||
491 DebugPrintInstructions.isSet(FILE_SRC)) {
492 std::string debug_file_name =
493 interpreterHandler->getOutputFilename("instructions.txt");
494 std::string error;
495 #ifdef HAVE_ZLIB_H
496 if (!DebugCompressInstructions) {
497 #endif
498 debugInstFile = klee_open_output_file(debug_file_name, error);
499 #ifdef HAVE_ZLIB_H
500 } else {
501 debug_file_name.append(".gz");
502 debugInstFile = klee_open_compressed_output_file(debug_file_name, error);
503 }
504 #endif
505 if (!debugInstFile) {
506 klee_error("Could not open file %s : %s", debug_file_name.c_str(),
507 error.c_str());
508 }
509 }
510 }
511
512 llvm::Module *
setModule(std::vector<std::unique_ptr<llvm::Module>> & modules,const ModuleOptions & opts)513 Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &modules,
514 const ModuleOptions &opts) {
515 assert(!kmodule && !modules.empty() &&
516 "can only register one module"); // XXX gross
517
518 kmodule = std::unique_ptr<KModule>(new KModule());
519
520 // Preparing the final module happens in multiple stages
521
522 // Link with KLEE intrinsics library before running any optimizations
523 SmallString<128> LibPath(opts.LibraryDir);
524 llvm::sys::path::append(LibPath,
525 "libkleeRuntimeIntrinsic" + opts.OptSuffix + ".bca");
526 std::string error;
527 if (!klee::loadFile(LibPath.c_str(), modules[0]->getContext(), modules,
528 error)) {
529 klee_error("Could not load KLEE intrinsic file %s", LibPath.c_str());
530 }
531
532 // 1.) Link the modules together
533 while (kmodule->link(modules, opts.EntryPoint)) {
534 // 2.) Apply different instrumentation
535 kmodule->instrument(opts);
536 }
537
538 // 3.) Optimise and prepare for KLEE
539
540 // Create a list of functions that should be preserved if used
541 std::vector<const char *> preservedFunctions;
542 specialFunctionHandler = new SpecialFunctionHandler(*this);
543 specialFunctionHandler->prepare(preservedFunctions);
544
545 preservedFunctions.push_back(opts.EntryPoint.c_str());
546
547 // Preserve the free-standing library calls
548 preservedFunctions.push_back("memset");
549 preservedFunctions.push_back("memcpy");
550 preservedFunctions.push_back("memcmp");
551 preservedFunctions.push_back("memmove");
552
553 kmodule->optimiseAndPrepare(opts, preservedFunctions);
554 kmodule->checkModule();
555
556 // 4.) Manifest the module
557 kmodule->manifest(interpreterHandler, StatsTracker::useStatistics());
558
559 specialFunctionHandler->bind();
560
561 if (StatsTracker::useStatistics() || userSearcherRequiresMD2U()) {
562 statsTracker =
563 new StatsTracker(*this,
564 interpreterHandler->getOutputFilename("assembly.ll"),
565 userSearcherRequiresMD2U());
566 }
567
568 // Initialize the context.
569 DataLayout *TD = kmodule->targetData.get();
570 Context::initialize(TD->isLittleEndian(),
571 (Expr::Width)TD->getPointerSizeInBits());
572
573 return kmodule->module.get();
574 }
575
~Executor()576 Executor::~Executor() {
577 delete memory;
578 delete externalDispatcher;
579 delete specialFunctionHandler;
580 delete statsTracker;
581 delete solver;
582 }
583
584 /***/
585
initializeGlobalObject(ExecutionState & state,ObjectState * os,const Constant * c,unsigned offset)586 void Executor::initializeGlobalObject(ExecutionState &state, ObjectState *os,
587 const Constant *c,
588 unsigned offset) {
589 const auto targetData = kmodule->targetData.get();
590 if (const ConstantVector *cp = dyn_cast<ConstantVector>(c)) {
591 unsigned elementSize =
592 targetData->getTypeStoreSize(cp->getType()->getElementType());
593 for (unsigned i=0, e=cp->getNumOperands(); i != e; ++i)
594 initializeGlobalObject(state, os, cp->getOperand(i),
595 offset + i*elementSize);
596 } else if (isa<ConstantAggregateZero>(c)) {
597 unsigned i, size = targetData->getTypeStoreSize(c->getType());
598 for (i=0; i<size; i++)
599 os->write8(offset+i, (uint8_t) 0);
600 } else if (const ConstantArray *ca = dyn_cast<ConstantArray>(c)) {
601 unsigned elementSize =
602 targetData->getTypeStoreSize(ca->getType()->getElementType());
603 for (unsigned i=0, e=ca->getNumOperands(); i != e; ++i)
604 initializeGlobalObject(state, os, ca->getOperand(i),
605 offset + i*elementSize);
606 } else if (const ConstantStruct *cs = dyn_cast<ConstantStruct>(c)) {
607 const StructLayout *sl =
608 targetData->getStructLayout(cast<StructType>(cs->getType()));
609 for (unsigned i=0, e=cs->getNumOperands(); i != e; ++i)
610 initializeGlobalObject(state, os, cs->getOperand(i),
611 offset + sl->getElementOffset(i));
612 } else if (const ConstantDataSequential *cds =
613 dyn_cast<ConstantDataSequential>(c)) {
614 unsigned elementSize =
615 targetData->getTypeStoreSize(cds->getElementType());
616 for (unsigned i=0, e=cds->getNumElements(); i != e; ++i)
617 initializeGlobalObject(state, os, cds->getElementAsConstant(i),
618 offset + i*elementSize);
619 } else if (!isa<UndefValue>(c) && !isa<MetadataAsValue>(c)) {
620 unsigned StoreBits = targetData->getTypeStoreSizeInBits(c->getType());
621 ref<ConstantExpr> C = evalConstant(c);
622
623 // Extend the constant if necessary;
624 assert(StoreBits >= C->getWidth() && "Invalid store size!");
625 if (StoreBits > C->getWidth())
626 C = C->ZExt(StoreBits);
627
628 os->write(offset, C);
629 }
630 }
631
addExternalObject(ExecutionState & state,void * addr,unsigned size,bool isReadOnly)632 MemoryObject * Executor::addExternalObject(ExecutionState &state,
633 void *addr, unsigned size,
634 bool isReadOnly) {
635 auto mo = memory->allocateFixed(reinterpret_cast<std::uint64_t>(addr),
636 size, nullptr);
637 ObjectState *os = bindObjectInState(state, mo, false);
638 for(unsigned i = 0; i < size; i++)
639 os->write8(i, ((uint8_t*)addr)[i]);
640 if(isReadOnly)
641 os->setReadOnly(true);
642 return mo;
643 }
644
645
646 extern void *__dso_handle __attribute__ ((__weak__));
647
initializeGlobals(ExecutionState & state)648 void Executor::initializeGlobals(ExecutionState &state) {
649 // allocate and initialize globals, done in two passes since we may
650 // need address of a global in order to initialize some other one.
651
652 // allocate memory objects for all globals
653 allocateGlobalObjects(state);
654
655 // initialize aliases first, may be needed for global objects
656 initializeGlobalAliases();
657
658 // finally, do the actual initialization
659 initializeGlobalObjects(state);
660 }
661
allocateGlobalObjects(ExecutionState & state)662 void Executor::allocateGlobalObjects(ExecutionState &state) {
663 const Module *m = kmodule->module.get();
664
665 if (m->getModuleInlineAsm() != "")
666 klee_warning("executable has module level assembly (ignoring)");
667 // represent function globals using the address of the actual llvm function
668 // object. given that we use malloc to allocate memory in states this also
669 // ensures that we won't conflict. we don't need to allocate a memory object
670 // since reading/writing via a function pointer is unsupported anyway.
671 for (const Function &f : *m) {
672 ref<ConstantExpr> addr;
673
674 // If the symbol has external weak linkage then it is implicitly
675 // not defined in this module; if it isn't resolvable then it
676 // should be null.
677 if (f.hasExternalWeakLinkage() &&
678 !externalDispatcher->resolveSymbol(f.getName().str())) {
679 addr = Expr::createPointer(0);
680 } else {
681 addr = Expr::createPointer(reinterpret_cast<std::uint64_t>(&f));
682 legalFunctions.insert(reinterpret_cast<std::uint64_t>(&f));
683 }
684
685 globalAddresses.emplace(&f, addr);
686 }
687
688 #ifndef WINDOWS
689 int *errno_addr = getErrnoLocation(state);
690 MemoryObject *errnoObj =
691 addExternalObject(state, (void *)errno_addr, sizeof *errno_addr, false);
692 // Copy values from and to program space explicitly
693 errnoObj->isUserSpecified = true;
694 #endif
695
696 // Disabled, we don't want to promote use of live externals.
697 #ifdef HAVE_CTYPE_EXTERNALS
698 #ifndef WINDOWS
699 #ifndef DARWIN
700 /* from /usr/include/ctype.h:
701 These point into arrays of 384, so they can be indexed by any `unsigned
702 char' value [0,255]; by EOF (-1); or by any `signed char' value
703 [-128,-1). ISO C requires that the ctype functions work for `unsigned */
704 const uint16_t **addr = __ctype_b_loc();
705 addExternalObject(state, const_cast<uint16_t*>(*addr-128),
706 384 * sizeof **addr, true);
707 addExternalObject(state, addr, sizeof(*addr), true);
708
709 const int32_t **lower_addr = __ctype_tolower_loc();
710 addExternalObject(state, const_cast<int32_t*>(*lower_addr-128),
711 384 * sizeof **lower_addr, true);
712 addExternalObject(state, lower_addr, sizeof(*lower_addr), true);
713
714 const int32_t **upper_addr = __ctype_toupper_loc();
715 addExternalObject(state, const_cast<int32_t*>(*upper_addr-128),
716 384 * sizeof **upper_addr, true);
717 addExternalObject(state, upper_addr, sizeof(*upper_addr), true);
718 #endif
719 #endif
720 #endif
721
722 for (const GlobalVariable &v : m->globals()) {
723 std::size_t globalObjectAlignment = getAllocationAlignment(&v);
724 Type *ty = v.getType()->getElementType();
725 std::uint64_t size = 0;
726 if (ty->isSized())
727 size = kmodule->targetData->getTypeStoreSize(ty);
728
729 if (v.isDeclaration()) {
730 // FIXME: We have no general way of handling unknown external
731 // symbols. If we really cared about making external stuff work
732 // better we could support user definition, or use the EXE style
733 // hack where we check the object file information.
734
735 if (!ty->isSized()) {
736 klee_warning("Type for %.*s is not sized",
737 static_cast<int>(v.getName().size()), v.getName().data());
738 }
739
740 // XXX - DWD - hardcode some things until we decide how to fix.
741 #ifndef WINDOWS
742 if (v.getName() == "_ZTVN10__cxxabiv117__class_type_infoE") {
743 size = 0x2C;
744 } else if (v.getName() == "_ZTVN10__cxxabiv120__si_class_type_infoE") {
745 size = 0x2C;
746 } else if (v.getName() == "_ZTVN10__cxxabiv121__vmi_class_type_infoE") {
747 size = 0x2C;
748 }
749 #endif
750
751 if (size == 0) {
752 klee_warning("Unable to find size for global variable: %.*s (use will "
753 "result in out of bounds access)",
754 static_cast<int>(v.getName().size()), v.getName().data());
755 }
756 }
757
758 MemoryObject *mo = memory->allocate(size, /*isLocal=*/false,
759 /*isGlobal=*/true, /*allocSite=*/&v,
760 /*alignment=*/globalObjectAlignment);
761 if (!mo)
762 klee_error("out of memory");
763 globalObjects.emplace(&v, mo);
764 globalAddresses.emplace(&v, mo->getBaseExpr());
765 }
766 }
767
initializeGlobalAlias(const llvm::Constant * c)768 void Executor::initializeGlobalAlias(const llvm::Constant *c) {
769 // aliasee may either be a global value or constant expression
770 const auto *ga = dyn_cast<GlobalAlias>(c);
771 if (ga) {
772 if (globalAddresses.count(ga)) {
773 // already resolved by previous invocation
774 return;
775 }
776 const llvm::Constant *aliasee = ga->getAliasee();
777 if (const auto *gv = dyn_cast<GlobalValue>(aliasee)) {
778 // aliasee is global value
779 auto it = globalAddresses.find(gv);
780 // uninitialized only if aliasee is another global alias
781 if (it != globalAddresses.end()) {
782 globalAddresses.emplace(ga, it->second);
783 return;
784 }
785 }
786 }
787
788 // resolve aliases in all sub-expressions
789 #if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
790 for (const auto *op : c->operand_values()) {
791 #else
792 for (auto &it : c->operands()) {
793 const auto *op = &*it;
794 #endif
795 initializeGlobalAlias(cast<Constant>(op));
796 }
797
798 if (ga) {
799 // aliasee is constant expression (or global alias)
800 globalAddresses.emplace(ga, evalConstant(ga->getAliasee()));
801 }
802 }
803
804 void Executor::initializeGlobalAliases() {
805 const Module *m = kmodule->module.get();
806 for (const GlobalAlias &a : m->aliases()) {
807 initializeGlobalAlias(&a);
808 }
809 }
810
811 void Executor::initializeGlobalObjects(ExecutionState &state) {
812 const Module *m = kmodule->module.get();
813
814 // remember constant objects to initialise their counter part for external
815 // calls
816 std::vector<ObjectState *> constantObjects;
817 for (const GlobalVariable &v : m->globals()) {
818 MemoryObject *mo = globalObjects.find(&v)->second;
819 ObjectState *os = bindObjectInState(state, mo, false);
820
821 if (v.isDeclaration() && mo->size) {
822 // Program already running -> object already initialized.
823 // Read concrete value and write it to our copy.
824 void *addr;
825 if (v.getName() == "__dso_handle") {
826 addr = &__dso_handle; // wtf ?
827 } else {
828 addr = externalDispatcher->resolveSymbol(v.getName().str());
829 }
830 if (!addr) {
831 klee_error("Unable to load symbol(%.*s) while initializing globals",
832 static_cast<int>(v.getName().size()), v.getName().data());
833 }
834 for (unsigned offset = 0; offset < mo->size; offset++) {
835 os->write8(offset, static_cast<unsigned char *>(addr)[offset]);
836 }
837 } else if (v.hasInitializer()) {
838 initializeGlobalObject(state, os, v.getInitializer(), 0);
839 if (v.isConstant())
840 constantObjects.emplace_back(os);
841 } else {
842 os->initializeToRandom();
843 }
844 }
845
846 // initialise constant memory that is potentially used with external calls
847 if (!constantObjects.empty()) {
848 // initialise the actual memory with constant values
849 state.addressSpace.copyOutConcretes();
850
851 // mark constant objects as read-only
852 for (auto obj : constantObjects)
853 obj->setReadOnly(true);
854 }
855 }
856
857
858 bool Executor::branchingPermitted(const ExecutionState &state) const {
859 if ((MaxMemoryInhibit && atMemoryLimit) ||
860 state.forkDisabled ||
861 inhibitForking ||
862 (MaxForks!=~0u && stats::forks >= MaxForks)) {
863
864 if (MaxMemoryInhibit && atMemoryLimit)
865 klee_warning_once(0, "skipping fork (memory cap exceeded)");
866 else if (state.forkDisabled)
867 klee_warning_once(0, "skipping fork (fork disabled on current path)");
868 else if (inhibitForking)
869 klee_warning_once(0, "skipping fork (fork disabled globally)");
870 else
871 klee_warning_once(0, "skipping fork (max-forks reached)");
872
873 return false;
874 }
875
876 return true;
877 }
878
879 void Executor::branch(ExecutionState &state,
880 const std::vector< ref<Expr> > &conditions,
881 std::vector<ExecutionState*> &result) {
882 TimerStatIncrementer timer(stats::forkTime);
883 unsigned N = conditions.size();
884 assert(N);
885
886 if (!branchingPermitted(state)) {
887 unsigned next = theRNG.getInt32() % N;
888 for (unsigned i=0; i<N; ++i) {
889 if (i == next) {
890 result.push_back(&state);
891 } else {
892 result.push_back(nullptr);
893 }
894 }
895 } else {
896 stats::forks += N-1;
897
898 // XXX do proper balance or keep random?
899 result.push_back(&state);
900 for (unsigned i=1; i<N; ++i) {
901 ExecutionState *es = result[theRNG.getInt32() % i];
902 ExecutionState *ns = es->branch();
903 addedStates.push_back(ns);
904 result.push_back(ns);
905 processTree->attach(es->ptreeNode, ns, es);
906 }
907 }
908
909 // If necessary redistribute seeds to match conditions, killing
910 // states if necessary due to OnlyReplaySeeds (inefficient but
911 // simple).
912
913 std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it =
914 seedMap.find(&state);
915 if (it != seedMap.end()) {
916 std::vector<SeedInfo> seeds = it->second;
917 seedMap.erase(it);
918
919 // Assume each seed only satisfies one condition (necessarily true
920 // when conditions are mutually exclusive and their conjunction is
921 // a tautology).
922 for (std::vector<SeedInfo>::iterator siit = seeds.begin(),
923 siie = seeds.end(); siit != siie; ++siit) {
924 unsigned i;
925 for (i=0; i<N; ++i) {
926 ref<ConstantExpr> res;
927 bool success = solver->getValue(
928 state.constraints, siit->assignment.evaluate(conditions[i]), res,
929 state.queryMetaData);
930 assert(success && "FIXME: Unhandled solver failure");
931 (void) success;
932 if (res->isTrue())
933 break;
934 }
935
936 // If we didn't find a satisfying condition randomly pick one
937 // (the seed will be patched).
938 if (i==N)
939 i = theRNG.getInt32() % N;
940
941 // Extra check in case we're replaying seeds with a max-fork
942 if (result[i])
943 seedMap[result[i]].push_back(*siit);
944 }
945
946 if (OnlyReplaySeeds) {
947 for (unsigned i=0; i<N; ++i) {
948 if (result[i] && !seedMap.count(result[i])) {
949 terminateState(*result[i]);
950 result[i] = NULL;
951 }
952 }
953 }
954 }
955
956 for (unsigned i=0; i<N; ++i)
957 if (result[i])
958 addConstraint(*result[i], conditions[i]);
959 }
960
961 Executor::StatePair
962 Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) {
963 Solver::Validity res;
964 std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it =
965 seedMap.find(¤t);
966 bool isSeeding = it != seedMap.end();
967
968 if (!isSeeding && !isa<ConstantExpr>(condition) &&
969 (MaxStaticForkPct!=1. || MaxStaticSolvePct != 1. ||
970 MaxStaticCPForkPct!=1. || MaxStaticCPSolvePct != 1.) &&
971 statsTracker->elapsed() > time::seconds(60)) {
972 StatisticManager &sm = *theStatisticManager;
973 CallPathNode *cpn = current.stack.back().callPathNode;
974 if ((MaxStaticForkPct<1. &&
975 sm.getIndexedValue(stats::forks, sm.getIndex()) >
976 stats::forks*MaxStaticForkPct) ||
977 (MaxStaticCPForkPct<1. &&
978 cpn && (cpn->statistics.getValue(stats::forks) >
979 stats::forks*MaxStaticCPForkPct)) ||
980 (MaxStaticSolvePct<1 &&
981 sm.getIndexedValue(stats::solverTime, sm.getIndex()) >
982 stats::solverTime*MaxStaticSolvePct) ||
983 (MaxStaticCPForkPct<1. &&
984 cpn && (cpn->statistics.getValue(stats::solverTime) >
985 stats::solverTime*MaxStaticCPSolvePct))) {
986 ref<ConstantExpr> value;
987 bool success = solver->getValue(current.constraints, condition, value,
988 current.queryMetaData);
989 assert(success && "FIXME: Unhandled solver failure");
990 (void) success;
991 addConstraint(current, EqExpr::create(value, condition));
992 condition = value;
993 }
994 }
995
996 time::Span timeout = coreSolverTimeout;
997 if (isSeeding)
998 timeout *= static_cast<unsigned>(it->second.size());
999 solver->setTimeout(timeout);
1000 bool success = solver->evaluate(current.constraints, condition, res,
1001 current.queryMetaData);
1002 solver->setTimeout(time::Span());
1003 if (!success) {
1004 current.pc = current.prevPC;
1005 terminateStateEarly(current, "Query timed out (fork).");
1006 return StatePair(0, 0);
1007 }
1008
1009 if (!isSeeding) {
1010 if (replayPath && !isInternal) {
1011 assert(replayPosition<replayPath->size() &&
1012 "ran out of branches in replay path mode");
1013 bool branch = (*replayPath)[replayPosition++];
1014
1015 if (res==Solver::True) {
1016 assert(branch && "hit invalid branch in replay path mode");
1017 } else if (res==Solver::False) {
1018 assert(!branch && "hit invalid branch in replay path mode");
1019 } else {
1020 // add constraints
1021 if(branch) {
1022 res = Solver::True;
1023 addConstraint(current, condition);
1024 } else {
1025 res = Solver::False;
1026 addConstraint(current, Expr::createIsZero(condition));
1027 }
1028 }
1029 } else if (res==Solver::Unknown) {
1030 assert(!replayKTest && "in replay mode, only one branch can be true.");
1031
1032 if (!branchingPermitted(current)) {
1033 TimerStatIncrementer timer(stats::forkTime);
1034 if (theRNG.getBool()) {
1035 addConstraint(current, condition);
1036 res = Solver::True;
1037 } else {
1038 addConstraint(current, Expr::createIsZero(condition));
1039 res = Solver::False;
1040 }
1041 }
1042 }
1043 }
1044
1045 // Fix branch in only-replay-seed mode, if we don't have both true
1046 // and false seeds.
1047 if (isSeeding &&
1048 (current.forkDisabled || OnlyReplaySeeds) &&
1049 res == Solver::Unknown) {
1050 bool trueSeed=false, falseSeed=false;
1051 // Is seed extension still ok here?
1052 for (std::vector<SeedInfo>::iterator siit = it->second.begin(),
1053 siie = it->second.end(); siit != siie; ++siit) {
1054 ref<ConstantExpr> res;
1055 bool success = solver->getValue(current.constraints,
1056 siit->assignment.evaluate(condition), res,
1057 current.queryMetaData);
1058 assert(success && "FIXME: Unhandled solver failure");
1059 (void) success;
1060 if (res->isTrue()) {
1061 trueSeed = true;
1062 } else {
1063 falseSeed = true;
1064 }
1065 if (trueSeed && falseSeed)
1066 break;
1067 }
1068 if (!(trueSeed && falseSeed)) {
1069 assert(trueSeed || falseSeed);
1070
1071 res = trueSeed ? Solver::True : Solver::False;
1072 addConstraint(current, trueSeed ? condition : Expr::createIsZero(condition));
1073 }
1074 }
1075
1076
1077 // XXX - even if the constraint is provable one way or the other we
1078 // can probably benefit by adding this constraint and allowing it to
1079 // reduce the other constraints. For example, if we do a binary
1080 // search on a particular value, and then see a comparison against
1081 // the value it has been fixed at, we should take this as a nice
1082 // hint to just use the single constraint instead of all the binary
1083 // search ones. If that makes sense.
1084 if (res==Solver::True) {
1085 if (!isInternal) {
1086 if (pathWriter) {
1087 current.pathOS << "1";
1088 }
1089 }
1090
1091 return StatePair(¤t, 0);
1092 } else if (res==Solver::False) {
1093 if (!isInternal) {
1094 if (pathWriter) {
1095 current.pathOS << "0";
1096 }
1097 }
1098
1099 return StatePair(0, ¤t);
1100 } else {
1101 TimerStatIncrementer timer(stats::forkTime);
1102 ExecutionState *falseState, *trueState = ¤t;
1103
1104 ++stats::forks;
1105
1106 falseState = trueState->branch();
1107 addedStates.push_back(falseState);
1108
1109 if (it != seedMap.end()) {
1110 std::vector<SeedInfo> seeds = it->second;
1111 it->second.clear();
1112 std::vector<SeedInfo> &trueSeeds = seedMap[trueState];
1113 std::vector<SeedInfo> &falseSeeds = seedMap[falseState];
1114 for (std::vector<SeedInfo>::iterator siit = seeds.begin(),
1115 siie = seeds.end(); siit != siie; ++siit) {
1116 ref<ConstantExpr> res;
1117 bool success = solver->getValue(current.constraints,
1118 siit->assignment.evaluate(condition),
1119 res, current.queryMetaData);
1120 assert(success && "FIXME: Unhandled solver failure");
1121 (void) success;
1122 if (res->isTrue()) {
1123 trueSeeds.push_back(*siit);
1124 } else {
1125 falseSeeds.push_back(*siit);
1126 }
1127 }
1128
1129 bool swapInfo = false;
1130 if (trueSeeds.empty()) {
1131 if (¤t == trueState) swapInfo = true;
1132 seedMap.erase(trueState);
1133 }
1134 if (falseSeeds.empty()) {
1135 if (¤t == falseState) swapInfo = true;
1136 seedMap.erase(falseState);
1137 }
1138 if (swapInfo) {
1139 std::swap(trueState->coveredNew, falseState->coveredNew);
1140 std::swap(trueState->coveredLines, falseState->coveredLines);
1141 }
1142 }
1143
1144 processTree->attach(current.ptreeNode, falseState, trueState);
1145
1146 if (pathWriter) {
1147 // Need to update the pathOS.id field of falseState, otherwise the same id
1148 // is used for both falseState and trueState.
1149 falseState->pathOS = pathWriter->open(current.pathOS);
1150 if (!isInternal) {
1151 trueState->pathOS << "1";
1152 falseState->pathOS << "0";
1153 }
1154 }
1155 if (symPathWriter) {
1156 falseState->symPathOS = symPathWriter->open(current.symPathOS);
1157 if (!isInternal) {
1158 trueState->symPathOS << "1";
1159 falseState->symPathOS << "0";
1160 }
1161 }
1162
1163 addConstraint(*trueState, condition);
1164 addConstraint(*falseState, Expr::createIsZero(condition));
1165
1166 // Kinda gross, do we even really still want this option?
1167 if (MaxDepth && MaxDepth<=trueState->depth) {
1168 terminateStateEarly(*trueState, "max-depth exceeded.");
1169 terminateStateEarly(*falseState, "max-depth exceeded.");
1170 return StatePair(0, 0);
1171 }
1172
1173 return StatePair(trueState, falseState);
1174 }
1175 }
1176
1177 void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
1178 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(condition)) {
1179 if (!CE->isTrue())
1180 llvm::report_fatal_error("attempt to add invalid constraint");
1181 return;
1182 }
1183
1184 // Check to see if this constraint violates seeds.
1185 std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it =
1186 seedMap.find(&state);
1187 if (it != seedMap.end()) {
1188 bool warn = false;
1189 for (std::vector<SeedInfo>::iterator siit = it->second.begin(),
1190 siie = it->second.end(); siit != siie; ++siit) {
1191 bool res;
1192 bool success = solver->mustBeFalse(state.constraints,
1193 siit->assignment.evaluate(condition),
1194 res, state.queryMetaData);
1195 assert(success && "FIXME: Unhandled solver failure");
1196 (void) success;
1197 if (res) {
1198 siit->patchSeed(state, condition, solver);
1199 warn = true;
1200 }
1201 }
1202 if (warn)
1203 klee_warning("seeds patched for violating constraint");
1204 }
1205
1206 state.addConstraint(condition);
1207 if (ivcEnabled)
1208 doImpliedValueConcretization(state, condition,
1209 ConstantExpr::alloc(1, Expr::Bool));
1210 }
1211
1212 const Cell& Executor::eval(KInstruction *ki, unsigned index,
1213 ExecutionState &state) const {
1214 assert(index < ki->inst->getNumOperands());
1215 int vnumber = ki->operands[index];
1216
1217 assert(vnumber != -1 &&
1218 "Invalid operand to eval(), not a value or constant!");
1219
1220 // Determine if this is a constant or not.
1221 if (vnumber < 0) {
1222 unsigned index = -vnumber - 2;
1223 return kmodule->constantTable[index];
1224 } else {
1225 unsigned index = vnumber;
1226 StackFrame &sf = state.stack.back();
1227 return sf.locals[index];
1228 }
1229 }
1230
1231 void Executor::bindLocal(KInstruction *target, ExecutionState &state,
1232 ref<Expr> value) {
1233 getDestCell(state, target).value = value;
1234 }
1235
1236 void Executor::bindArgument(KFunction *kf, unsigned index,
1237 ExecutionState &state, ref<Expr> value) {
1238 getArgumentCell(state, kf, index).value = value;
1239 }
1240
1241 ref<Expr> Executor::toUnique(const ExecutionState &state,
1242 ref<Expr> &e) {
1243 ref<Expr> result = e;
1244
1245 if (!isa<ConstantExpr>(e)) {
1246 ref<ConstantExpr> value;
1247 bool isTrue = false;
1248 e = optimizer.optimizeExpr(e, true);
1249 solver->setTimeout(coreSolverTimeout);
1250 if (solver->getValue(state.constraints, e, value, state.queryMetaData)) {
1251 ref<Expr> cond = EqExpr::create(e, value);
1252 cond = optimizer.optimizeExpr(cond, false);
1253 if (solver->mustBeTrue(state.constraints, cond, isTrue,
1254 state.queryMetaData) &&
1255 isTrue)
1256 result = value;
1257 }
1258 solver->setTimeout(time::Span());
1259 }
1260
1261 return result;
1262 }
1263
1264
1265 /* Concretize the given expression, and return a possible constant value.
1266 'reason' is just a documentation string stating the reason for concretization. */
1267 ref<klee::ConstantExpr>
1268 Executor::toConstant(ExecutionState &state,
1269 ref<Expr> e,
1270 const char *reason) {
1271 e = ConstraintManager::simplifyExpr(state.constraints, e);
1272 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
1273 return CE;
1274
1275 ref<ConstantExpr> value;
1276 bool success =
1277 solver->getValue(state.constraints, e, value, state.queryMetaData);
1278 assert(success && "FIXME: Unhandled solver failure");
1279 (void) success;
1280
1281 std::string str;
1282 llvm::raw_string_ostream os(str);
1283 os << "silently concretizing (reason: " << reason << ") expression " << e
1284 << " to value " << value << " (" << (*(state.pc)).info->file << ":"
1285 << (*(state.pc)).info->line << ")";
1286
1287 if (AllExternalWarnings)
1288 klee_warning("%s", os.str().c_str());
1289 else
1290 klee_warning_once(reason, "%s", os.str().c_str());
1291
1292 addConstraint(state, EqExpr::create(e, value));
1293
1294 return value;
1295 }
1296
1297 void Executor::executeGetValue(ExecutionState &state,
1298 ref<Expr> e,
1299 KInstruction *target) {
1300 e = ConstraintManager::simplifyExpr(state.constraints, e);
1301 std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it =
1302 seedMap.find(&state);
1303 if (it==seedMap.end() || isa<ConstantExpr>(e)) {
1304 ref<ConstantExpr> value;
1305 e = optimizer.optimizeExpr(e, true);
1306 bool success =
1307 solver->getValue(state.constraints, e, value, state.queryMetaData);
1308 assert(success && "FIXME: Unhandled solver failure");
1309 (void) success;
1310 bindLocal(target, state, value);
1311 } else {
1312 std::set< ref<Expr> > values;
1313 for (std::vector<SeedInfo>::iterator siit = it->second.begin(),
1314 siie = it->second.end(); siit != siie; ++siit) {
1315 ref<Expr> cond = siit->assignment.evaluate(e);
1316 cond = optimizer.optimizeExpr(cond, true);
1317 ref<ConstantExpr> value;
1318 bool success =
1319 solver->getValue(state.constraints, cond, value, state.queryMetaData);
1320 assert(success && "FIXME: Unhandled solver failure");
1321 (void) success;
1322 values.insert(value);
1323 }
1324
1325 std::vector< ref<Expr> > conditions;
1326 for (std::set< ref<Expr> >::iterator vit = values.begin(),
1327 vie = values.end(); vit != vie; ++vit)
1328 conditions.push_back(EqExpr::create(e, *vit));
1329
1330 std::vector<ExecutionState*> branches;
1331 branch(state, conditions, branches);
1332
1333 std::vector<ExecutionState*>::iterator bit = branches.begin();
1334 for (std::set< ref<Expr> >::iterator vit = values.begin(),
1335 vie = values.end(); vit != vie; ++vit) {
1336 ExecutionState *es = *bit;
1337 if (es)
1338 bindLocal(target, *es, *vit);
1339 ++bit;
1340 }
1341 }
1342 }
1343
1344 void Executor::printDebugInstructions(ExecutionState &state) {
1345 // print nothing if option unset
1346 if (DebugPrintInstructions.getBits() == 0)
1347 return;
1348
1349 // set output stream (stderr/file)
1350 llvm::raw_ostream *stream = nullptr;
1351 if (DebugPrintInstructions.isSet(STDERR_ALL) ||
1352 DebugPrintInstructions.isSet(STDERR_SRC) ||
1353 DebugPrintInstructions.isSet(STDERR_COMPACT))
1354 stream = &llvm::errs();
1355 else
1356 stream = &debugLogBuffer;
1357
1358 // print:
1359 // [all] src location:asm line:state ID:instruction
1360 // [compact] asm line:state ID
1361 // [src] src location:asm line:state ID
1362 if (!DebugPrintInstructions.isSet(STDERR_COMPACT) &&
1363 !DebugPrintInstructions.isSet(FILE_COMPACT)) {
1364 (*stream) << " " << state.pc->getSourceLocation() << ':';
1365 }
1366
1367 (*stream) << state.pc->info->assemblyLine << ':' << state.getID();
1368
1369 if (DebugPrintInstructions.isSet(STDERR_ALL) ||
1370 DebugPrintInstructions.isSet(FILE_ALL))
1371 (*stream) << ':' << *(state.pc->inst);
1372
1373 (*stream) << '\n';
1374
1375 // flush to file
1376 if (DebugPrintInstructions.isSet(FILE_ALL) ||
1377 DebugPrintInstructions.isSet(FILE_COMPACT) ||
1378 DebugPrintInstructions.isSet(FILE_SRC)) {
1379 debugLogBuffer.flush();
1380 (*debugInstFile) << debugLogBuffer.str();
1381 debugBufferString = "";
1382 }
1383 }
1384
1385 void Executor::stepInstruction(ExecutionState &state) {
1386 printDebugInstructions(state);
1387 if (statsTracker)
1388 statsTracker->stepInstruction(state);
1389
1390 ++stats::instructions;
1391 ++state.steppedInstructions;
1392 state.prevPC = state.pc;
1393 ++state.pc;
1394
1395 if (stats::instructions == MaxInstructions)
1396 haltExecution = true;
1397 }
1398
1399 static inline const llvm::fltSemantics *fpWidthToSemantics(unsigned width) {
1400 switch (width) {
1401 #if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
1402 case Expr::Int32:
1403 return &llvm::APFloat::IEEEsingle();
1404 case Expr::Int64:
1405 return &llvm::APFloat::IEEEdouble();
1406 case Expr::Fl80:
1407 return &llvm::APFloat::x87DoubleExtended();
1408 #else
1409 case Expr::Int32:
1410 return &llvm::APFloat::IEEEsingle;
1411 case Expr::Int64:
1412 return &llvm::APFloat::IEEEdouble;
1413 case Expr::Fl80:
1414 return &llvm::APFloat::x87DoubleExtended;
1415 #endif
1416 default:
1417 return 0;
1418 }
1419 }
1420
1421 MemoryObject *Executor::serializeLandingpad(ExecutionState &state,
1422 const llvm::LandingPadInst &lpi,
1423 bool &stateTerminated) {
1424 stateTerminated = false;
1425
1426 std::vector<unsigned char> serialized;
1427
1428 for (unsigned current_clause_id = 0; current_clause_id < lpi.getNumClauses();
1429 ++current_clause_id) {
1430 llvm::Constant *current_clause = lpi.getClause(current_clause_id);
1431 if (lpi.isCatch(current_clause_id)) {
1432 // catch-clause
1433 serialized.push_back(0);
1434
1435 std::uint64_t ti_addr = 0;
1436
1437 llvm::BitCastOperator *clause_bitcast =
1438 dyn_cast<llvm::BitCastOperator>(current_clause);
1439 if (clause_bitcast) {
1440 llvm::GlobalValue *clause_type =
1441 dyn_cast<GlobalValue>(clause_bitcast->getOperand(0));
1442
1443 ti_addr = globalAddresses[clause_type]->getZExtValue();
1444 } else if (current_clause->isNullValue()) {
1445 ti_addr = 0;
1446 } else {
1447 terminateStateOnError(
1448 state, "Internal: Clause is not a bitcast or null (catch-all)",
1449 Exec);
1450 stateTerminated = true;
1451 return nullptr;
1452 }
1453 const std::size_t old_size = serialized.size();
1454 serialized.resize(old_size + 8);
1455 memcpy(serialized.data() + old_size, &ti_addr, sizeof(ti_addr));
1456 } else if (lpi.isFilter(current_clause_id)) {
1457 if (current_clause->isNullValue()) {
1458 // special handling for a catch-all filter clause, i.e., "[0 x i8*]"
1459 // for this case we serialize 1 element..
1460 serialized.push_back(1);
1461 // which is a 64bit-wide 0.
1462 serialized.resize(serialized.size() + 8, 0);
1463 } else {
1464 llvm::ConstantArray const *ca =
1465 cast<llvm::ConstantArray>(current_clause);
1466
1467 // serialize `num_elements+1` as unsigned char
1468 unsigned const num_elements = ca->getNumOperands();
1469 unsigned char serialized_num_elements = 0;
1470
1471 if (num_elements >=
1472 std::numeric_limits<decltype(serialized_num_elements)>::max()) {
1473 terminateStateOnError(
1474 state, "Internal: too many elements in landingpad filter", Exec);
1475 stateTerminated = true;
1476 return nullptr;
1477 }
1478
1479 serialized_num_elements = num_elements;
1480 serialized.push_back(serialized_num_elements + 1);
1481
1482 // serialize the exception-types occurring in this filter-clause
1483 for (llvm::Value const *v : ca->operands()) {
1484 llvm::BitCastOperator const *bitcast =
1485 dyn_cast<llvm::BitCastOperator>(v);
1486 if (!bitcast) {
1487 terminateStateOnError(state,
1488 "Internal: expected value inside a "
1489 "filter-clause to be a bitcast",
1490 Exec);
1491 stateTerminated = true;
1492 return nullptr;
1493 }
1494
1495 llvm::GlobalValue const *clause_value =
1496 dyn_cast<GlobalValue>(bitcast->getOperand(0));
1497 if (!clause_value) {
1498 terminateStateOnError(state,
1499 "Internal: expected value inside a "
1500 "filter-clause bitcast to be a GlobalValue",
1501 Exec);
1502 stateTerminated = true;
1503 return nullptr;
1504 }
1505
1506 std::uint64_t const ti_addr =
1507 globalAddresses[clause_value]->getZExtValue();
1508
1509 const std::size_t old_size = serialized.size();
1510 serialized.resize(old_size + 8);
1511 memcpy(serialized.data() + old_size, &ti_addr, sizeof(ti_addr));
1512 }
1513 }
1514 }
1515 }
1516
1517 MemoryObject *mo =
1518 memory->allocate(serialized.size(), true, false, nullptr, 1);
1519 ObjectState *os = bindObjectInState(state, mo, false);
1520 for (unsigned i = 0; i < serialized.size(); i++) {
1521 os->write8(i, serialized[i]);
1522 }
1523
1524 return mo;
1525 }
1526
1527 void Executor::unwindToNextLandingpad(ExecutionState &state) {
1528 UnwindingInformation *ui = state.unwindingInformation.get();
1529 assert(ui && "unwinding without unwinding information");
1530
1531 std::size_t startIndex;
1532 std::size_t lowestStackIndex;
1533 bool popFrames;
1534
1535 if (auto *sui = dyn_cast<SearchPhaseUnwindingInformation>(ui)) {
1536 startIndex = sui->unwindingProgress;
1537 lowestStackIndex = 0;
1538 popFrames = false;
1539 } else if (auto *cui = dyn_cast<CleanupPhaseUnwindingInformation>(ui)) {
1540 startIndex = state.stack.size() - 1;
1541 lowestStackIndex = cui->catchingStackIndex;
1542 popFrames = true;
1543 } else {
1544 assert(false && "invalid UnwindingInformation subclass");
1545 }
1546
1547 for (std::size_t i = startIndex; i > lowestStackIndex; i--) {
1548 auto const &sf = state.stack.at(i);
1549
1550 Instruction *inst = sf.caller ? sf.caller->inst : nullptr;
1551
1552 if (popFrames) {
1553 state.popFrame();
1554 if (statsTracker != nullptr) {
1555 statsTracker->framePopped(state);
1556 }
1557 }
1558
1559 if (InvokeInst *invoke = dyn_cast<InvokeInst>(inst)) {
1560 // we found the next invoke instruction in the call stack, handle it
1561 // depending on the current phase.
1562 if (auto *sui = dyn_cast<SearchPhaseUnwindingInformation>(ui)) {
1563 // in the search phase, run personality function to check if this
1564 // landingpad catches the exception
1565
1566 LandingPadInst *lpi = invoke->getUnwindDest()->getLandingPadInst();
1567 assert(lpi && "unwind target of an invoke instruction did not lead to "
1568 "a landingpad");
1569
1570 // check if this is a pure cleanup landingpad first
1571 if (lpi->isCleanup() && lpi->getNumClauses() == 0) {
1572 // pure cleanup lpi, this can't be a handler, so skip it
1573 continue;
1574 }
1575
1576 bool stateTerminated = false;
1577 MemoryObject *clauses_mo =
1578 serializeLandingpad(state, *lpi, stateTerminated);
1579 assert((stateTerminated != bool(clauses_mo)) &&
1580 "illegal serializeLandingpad result");
1581
1582 if (stateTerminated) {
1583 return;
1584 }
1585
1586 assert(sui->serializedLandingpad == nullptr &&
1587 "serializedLandingpad should be reset");
1588 sui->serializedLandingpad = clauses_mo;
1589
1590 llvm::Function *personality_fn =
1591 kmodule->module->getFunction("_klee_eh_cxx_personality");
1592 KFunction *kf = kmodule->functionMap[personality_fn];
1593
1594 state.pushFrame(state.prevPC, kf);
1595 state.pc = kf->instructions;
1596 bindArgument(kf, 0, state, sui->exceptionObject);
1597 bindArgument(kf, 1, state, clauses_mo->getSizeExpr());
1598 bindArgument(kf, 2, state, clauses_mo->getBaseExpr());
1599
1600 if (statsTracker) {
1601 statsTracker->framePushed(state,
1602 &state.stack[state.stack.size() - 2]);
1603 }
1604
1605 // make sure we remember our search progress afterwards
1606 sui->unwindingProgress = i - 1;
1607 } else {
1608 // in the cleanup phase, redirect control flow
1609 transferToBasicBlock(invoke->getUnwindDest(), invoke->getParent(),
1610 state);
1611 }
1612
1613 // we are done, stop search/unwinding here
1614 return;
1615 }
1616 }
1617
1618 // no further invoke instruction/landingpad found
1619 if (isa<SearchPhaseUnwindingInformation>(ui)) {
1620 // in phase 1, simply stop unwinding. this will return
1621 // control flow back to _Unwind_RaiseException, which will
1622 // return the correct error.
1623
1624 // clean up unwinding state
1625 state.unwindingInformation.reset();
1626 } else {
1627 // in phase 2, this represent a situation that should
1628 // not happen, as we only progressed to phase 2 because
1629 // we found a handler in phase 1.
1630 // therefore terminate the state.
1631 terminateStateOnExecError(state,
1632 "Missing landingpad in phase 2 of unwinding");
1633 }
1634 }
1635
1636 ref<klee::ConstantExpr> Executor::getEhTypeidFor(ref<Expr> type_info) {
1637 // FIXME: Handling getEhTypeidFor is non-deterministic and depends on the
1638 // order states have been processed and executed.
1639 auto eh_type_iterator =
1640 std::find(std::begin(eh_typeids), std::end(eh_typeids), type_info);
1641 if (eh_type_iterator == std::end(eh_typeids)) {
1642 eh_typeids.push_back(type_info);
1643 eh_type_iterator = std::prev(std::end(eh_typeids));
1644 }
1645 // +1 because typeids must always be positive, so they can be distinguished
1646 // from 'no landingpad clause matched' which has value 0
1647 auto res = ConstantExpr::create(eh_type_iterator - std::begin(eh_typeids) + 1,
1648 Expr::Int32);
1649 return res;
1650 }
1651
1652 void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
1653 std::vector<ref<Expr>> &arguments) {
1654 Instruction *i = ki->inst;
1655 if (isa_and_nonnull<DbgInfoIntrinsic>(i))
1656 return;
1657 if (f && f->isDeclaration()) {
1658 switch (f->getIntrinsicID()) {
1659 case Intrinsic::not_intrinsic:
1660 // state may be destroyed by this call, cannot touch
1661 callExternalFunction(state, ki, f, arguments);
1662 break;
1663 case Intrinsic::fabs: {
1664 ref<ConstantExpr> arg =
1665 toConstant(state, arguments[0], "floating point");
1666 if (!fpWidthToSemantics(arg->getWidth()))
1667 return terminateStateOnExecError(
1668 state, "Unsupported intrinsic llvm.fabs call");
1669
1670 llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()),
1671 arg->getAPValue());
1672 Res = llvm::abs(Res);
1673
1674 bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
1675 break;
1676 }
1677
1678 #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0)
1679 case Intrinsic::fshr:
1680 case Intrinsic::fshl: {
1681 ref<Expr> op1 = eval(ki, 1, state).value;
1682 ref<Expr> op2 = eval(ki, 2, state).value;
1683 ref<Expr> op3 = eval(ki, 3, state).value;
1684 unsigned w = op1->getWidth();
1685 assert(w == op2->getWidth() && "type mismatch");
1686 assert(w == op3->getWidth() && "type mismatch");
1687 ref<Expr> c = ConcatExpr::create(op1, op2);
1688 // op3 = zeroExtend(op3 % w)
1689 op3 = URemExpr::create(op3, ConstantExpr::create(w, w));
1690 op3 = ZExtExpr::create(op3, w+w);
1691 if (f->getIntrinsicID() == Intrinsic::fshl) {
1692 // shift left and take top half
1693 ref<Expr> s = ShlExpr::create(c, op3);
1694 bindLocal(ki, state, ExtractExpr::create(s, w, w));
1695 } else {
1696 // shift right and take bottom half
1697 // note that LShr and AShr will have same behaviour
1698 ref<Expr> s = LShrExpr::create(c, op3);
1699 bindLocal(ki, state, ExtractExpr::create(s, 0, w));
1700 }
1701 break;
1702 }
1703 #endif
1704
1705 // va_arg is handled by caller and intrinsic lowering, see comment for
1706 // ExecutionState::varargs
1707 case Intrinsic::vastart: {
1708 StackFrame &sf = state.stack.back();
1709
1710 // varargs can be zero if no varargs were provided
1711 if (!sf.varargs)
1712 return;
1713
1714 // FIXME: This is really specific to the architecture, not the pointer
1715 // size. This happens to work for x86-32 and x86-64, however.
1716 Expr::Width WordSize = Context::get().getPointerWidth();
1717 if (WordSize == Expr::Int32) {
1718 executeMemoryOperation(state, true, arguments[0],
1719 sf.varargs->getBaseExpr(), 0);
1720 } else {
1721 assert(WordSize == Expr::Int64 && "Unknown word size!");
1722
1723 // x86-64 has quite complicated calling convention. However,
1724 // instead of implementing it, we can do a simple hack: just
1725 // make a function believe that all varargs are on stack.
1726 executeMemoryOperation(
1727 state, true,
1728 arguments[0],
1729 ConstantExpr::create(48, 32), 0); // gp_offset
1730 executeMemoryOperation(
1731 state, true,
1732 AddExpr::create(arguments[0], ConstantExpr::create(4, 64)),
1733 ConstantExpr::create(304, 32), 0); // fp_offset
1734 executeMemoryOperation(
1735 state, true,
1736 AddExpr::create(arguments[0], ConstantExpr::create(8, 64)),
1737 sf.varargs->getBaseExpr(), 0); // overflow_arg_area
1738 executeMemoryOperation(
1739 state, true,
1740 AddExpr::create(arguments[0], ConstantExpr::create(16, 64)),
1741 ConstantExpr::create(0, 64), 0); // reg_save_area
1742 }
1743 break;
1744 }
1745
1746 case Intrinsic::eh_typeid_for: {
1747 bindLocal(ki, state, getEhTypeidFor(arguments.at(0)));
1748 break;
1749 }
1750
1751 case Intrinsic::vaend:
1752 // va_end is a noop for the interpreter.
1753 //
1754 // FIXME: We should validate that the target didn't do something bad
1755 // with va_end, however (like call it twice).
1756 break;
1757
1758 case Intrinsic::vacopy:
1759 // va_copy should have been lowered.
1760 //
1761 // FIXME: It would be nice to check for errors in the usage of this as
1762 // well.
1763 default:
1764 klee_warning("unimplemented intrinsic: %s", f->getName().data());
1765 terminateStateOnError(state, "unimplemented intrinsic", Unhandled);
1766 return;
1767 }
1768
1769 // __cxa_throw & _rethrow are already handled in their
1770 // SpecialFunctionHandlers and have already been redirected to their unwind
1771 // destinations, so we must not transfer them to their regular targets.
1772 if (InvokeInst *ii = dyn_cast<InvokeInst>(i)) {
1773 if (f->getName() != std::string("__cxa_throw") &&
1774 f->getName() != std::string("__cxa_rethrow")) {
1775 transferToBasicBlock(ii->getNormalDest(), i->getParent(), state);
1776 }
1777 }
1778 } else {
1779 // Check if maximum stack size was reached.
1780 // We currently only count the number of stack frames
1781 if (RuntimeMaxStackFrames && state.stack.size() > RuntimeMaxStackFrames) {
1782 terminateStateEarly(state, "Maximum stack size reached.");
1783 klee_warning("Maximum stack size reached.");
1784 return;
1785 }
1786
1787 // FIXME: I'm not really happy about this reliance on prevPC but it is ok, I
1788 // guess. This just done to avoid having to pass KInstIterator everywhere
1789 // instead of the actual instruction, since we can't make a KInstIterator
1790 // from just an instruction (unlike LLVM).
1791 KFunction *kf = kmodule->functionMap[f];
1792
1793 state.pushFrame(state.prevPC, kf);
1794 state.pc = kf->instructions;
1795
1796 if (statsTracker)
1797 statsTracker->framePushed(state, &state.stack[state.stack.size() - 2]);
1798
1799 // TODO: support zeroext, signext, sret attributes
1800
1801 unsigned callingArgs = arguments.size();
1802 unsigned funcArgs = f->arg_size();
1803 if (!f->isVarArg()) {
1804 if (callingArgs > funcArgs) {
1805 klee_warning_once(f, "calling %s with extra arguments.",
1806 f->getName().data());
1807 } else if (callingArgs < funcArgs) {
1808 terminateStateOnError(state, "calling function with too few arguments",
1809 User);
1810 return;
1811 }
1812 } else {
1813 if (callingArgs < funcArgs) {
1814 terminateStateOnError(state, "calling function with too few arguments",
1815 User);
1816 return;
1817 }
1818
1819 // Only x86-32 and x86-64 are supported
1820 Expr::Width WordSize = Context::get().getPointerWidth();
1821 assert(((WordSize == Expr::Int32) || (WordSize == Expr::Int64)) &&
1822 "Unknown word size!");
1823
1824 uint64_t size = 0; // total size of variadic arguments
1825 bool requires16ByteAlignment = false;
1826
1827 uint64_t offsets[callingArgs]; // offsets of variadic arguments
1828 uint64_t argWidth; // width of current variadic argument
1829
1830 #if LLVM_VERSION_CODE >= LLVM_VERSION(8, 0)
1831 const CallBase &cs = cast<CallBase>(*i);
1832 #else
1833 const CallSite cs(i);
1834 #endif
1835 for (unsigned k = funcArgs; k < callingArgs; k++) {
1836 if (cs.isByValArgument(k)) {
1837 #if LLVM_VERSION_CODE >= LLVM_VERSION(9, 0)
1838 Type *t = cs.getParamByValType(k);
1839 #else
1840 auto arg = cs.getArgOperand(k);
1841 Type *t = arg->getType();
1842 assert(t->isPointerTy());
1843 t = t->getPointerElementType();
1844 #endif
1845 argWidth = kmodule->targetData->getTypeSizeInBits(t);
1846 } else {
1847 argWidth = arguments[k]->getWidth();
1848 }
1849
1850 if (WordSize == Expr::Int32) {
1851 offsets[k] = size;
1852 size += Expr::getMinBytesForWidth(argWidth);
1853 } else {
1854 #if LLVM_VERSION_CODE >= LLVM_VERSION(11, 0)
1855 MaybeAlign ma = cs.getParamAlign(k);
1856 unsigned alignment = ma ? ma->value() : 0;
1857 #elif LLVM_VERSION_CODE > LLVM_VERSION(4, 0)
1858 unsigned alignment = cs.getParamAlignment(k);
1859 #else
1860 // getParamAlignment() is buggy for LLVM <= 4, so we instead
1861 // get the attribute in a hacky way by parsing the textual
1862 // representation
1863 unsigned alignment = 0;
1864 std::string str;
1865 llvm::raw_string_ostream s(str);
1866 s << *cs.getArgument(k);
1867 size_t pos = str.find("align ");
1868 if (pos != std::string::npos)
1869 alignment = std::stoi(str.substr(pos + 6));
1870 #endif
1871
1872 // AMD64-ABI 3.5.7p5: Step 7. Align l->overflow_arg_area upwards to a
1873 // 16 byte boundary if alignment needed by type exceeds 8 byte
1874 // boundary.
1875 if (!alignment && argWidth > Expr::Int64) {
1876 alignment = 16;
1877 requires16ByteAlignment = true;
1878 }
1879
1880 if (!alignment)
1881 alignment = 8;
1882
1883 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 9)
1884 size = llvm::alignTo(size, alignment);
1885 #else
1886 size = llvm::RoundUpToAlignment(size, alignment);
1887 #endif
1888 offsets[k] = size;
1889
1890 // AMD64-ABI 3.5.7p5: Step 9. Set l->overflow_arg_area to:
1891 // l->overflow_arg_area + sizeof(type)
1892 // Step 10. Align l->overflow_arg_area upwards to an 8 byte boundary.
1893 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 9)
1894 size += llvm::alignTo(argWidth, WordSize) / 8;
1895 #else
1896 size += llvm::RoundUpToAlignment(argWidth, WordSize) / 8;
1897 #endif
1898 }
1899 }
1900
1901 StackFrame &sf = state.stack.back();
1902 MemoryObject *mo = sf.varargs =
1903 memory->allocate(size, true, false, state.prevPC->inst,
1904 (requires16ByteAlignment ? 16 : 8));
1905 if (!mo && size) {
1906 terminateStateOnExecError(state, "out of memory (varargs)");
1907 return;
1908 }
1909
1910 if (mo) {
1911 if ((WordSize == Expr::Int64) && (mo->address & 15) &&
1912 requires16ByteAlignment) {
1913 // Both 64bit Linux/Glibc and 64bit MacOSX should align to 16 bytes.
1914 klee_warning_once(
1915 0, "While allocating varargs: malloc did not align to 16 bytes.");
1916 }
1917
1918 ObjectState *os = bindObjectInState(state, mo, true);
1919
1920 for (unsigned k = funcArgs; k < callingArgs; k++) {
1921 if (!cs.isByValArgument(k)) {
1922 os->write(offsets[k], arguments[k]);
1923 } else {
1924 ConstantExpr *CE = dyn_cast<ConstantExpr>(arguments[k]);
1925 assert(CE); // byval argument needs to be a concrete pointer
1926
1927 ObjectPair op;
1928 state.addressSpace.resolveOne(CE, op);
1929 const ObjectState *osarg = op.second;
1930 assert(osarg);
1931 for (unsigned i = 0; i < osarg->size; i++)
1932 os->write(offsets[k] + i, osarg->read8(i));
1933 }
1934 }
1935 }
1936 }
1937
1938 unsigned numFormals = f->arg_size();
1939 for (unsigned k = 0; k < numFormals; k++)
1940 bindArgument(kf, k, state, arguments[k]);
1941 }
1942 }
1943
1944 void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src,
1945 ExecutionState &state) {
1946 // Note that in general phi nodes can reuse phi values from the same
1947 // block but the incoming value is the eval() result *before* the
1948 // execution of any phi nodes. this is pathological and doesn't
1949 // really seem to occur, but just in case we run the PhiCleanerPass
1950 // which makes sure this cannot happen and so it is safe to just
1951 // eval things in order. The PhiCleanerPass also makes sure that all
1952 // incoming blocks have the same order for each PHINode so we only
1953 // have to compute the index once.
1954 //
1955 // With that done we simply set an index in the state so that PHI
1956 // instructions know which argument to eval, set the pc, and continue.
1957
1958 // XXX this lookup has to go ?
1959 KFunction *kf = state.stack.back().kf;
1960 unsigned entry = kf->basicBlockEntry[dst];
1961 state.pc = &kf->instructions[entry];
1962 if (state.pc->inst->getOpcode() == Instruction::PHI) {
1963 PHINode *first = static_cast<PHINode*>(state.pc->inst);
1964 state.incomingBBIndex = first->getBasicBlockIndex(src);
1965 }
1966 }
1967
1968 /// Compute the true target of a function call, resolving LLVM aliases
1969 /// and bitcasts.
1970 Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) {
1971 SmallPtrSet<const GlobalValue*, 3> Visited;
1972
1973 Constant *c = dyn_cast<Constant>(calledVal);
1974 if (!c)
1975 return 0;
1976
1977 while (true) {
1978 if (GlobalValue *gv = dyn_cast<GlobalValue>(c)) {
1979 if (!Visited.insert(gv).second)
1980 return 0;
1981
1982 if (Function *f = dyn_cast<Function>(gv))
1983 return f;
1984 else if (GlobalAlias *ga = dyn_cast<GlobalAlias>(gv))
1985 c = ga->getAliasee();
1986 else
1987 return 0;
1988 } else if (llvm::ConstantExpr *ce = dyn_cast<llvm::ConstantExpr>(c)) {
1989 if (ce->getOpcode()==Instruction::BitCast)
1990 c = ce->getOperand(0);
1991 else
1992 return 0;
1993 } else
1994 return 0;
1995 }
1996 }
1997
1998 void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
1999 Instruction *i = ki->inst;
2000 switch (i->getOpcode()) {
2001 // Control flow
2002 case Instruction::Ret: {
2003 ReturnInst *ri = cast<ReturnInst>(i);
2004 KInstIterator kcaller = state.stack.back().caller;
2005 Instruction *caller = kcaller ? kcaller->inst : 0;
2006 bool isVoidReturn = (ri->getNumOperands() == 0);
2007 ref<Expr> result = ConstantExpr::alloc(0, Expr::Bool);
2008
2009 if (!isVoidReturn) {
2010 result = eval(ki, 0, state).value;
2011 }
2012
2013 if (state.stack.size() <= 1) {
2014 assert(!caller && "caller set on initial stack frame");
2015 terminateStateOnExit(state);
2016 } else {
2017 state.popFrame();
2018
2019 if (statsTracker)
2020 statsTracker->framePopped(state);
2021
2022 if (InvokeInst *ii = dyn_cast<InvokeInst>(caller)) {
2023 transferToBasicBlock(ii->getNormalDest(), caller->getParent(), state);
2024 } else {
2025 state.pc = kcaller;
2026 ++state.pc;
2027 }
2028
2029 if (ri->getFunction()->getName() == "_klee_eh_cxx_personality") {
2030 assert(dyn_cast<ConstantExpr>(result) &&
2031 "result from personality fn must be a concrete value");
2032
2033 auto *sui = dyn_cast_or_null<SearchPhaseUnwindingInformation>(
2034 state.unwindingInformation.get());
2035 assert(sui && "return from personality function outside of "
2036 "search phase unwinding");
2037
2038 // unbind the MO we used to pass the serialized landingpad
2039 state.addressSpace.unbindObject(sui->serializedLandingpad);
2040 sui->serializedLandingpad = nullptr;
2041
2042 if (result->isZero()) {
2043 // this lpi doesn't handle the exception, continue the search
2044 unwindToNextLandingpad(state);
2045 } else {
2046 // a clause (or a catch-all clause or filter clause) matches:
2047 // remember the stack index and switch to cleanup phase
2048 state.unwindingInformation =
2049 std::make_unique<CleanupPhaseUnwindingInformation>(
2050 sui->exceptionObject, cast<ConstantExpr>(result),
2051 sui->unwindingProgress);
2052 // this pointer is now invalidated
2053 sui = nullptr;
2054 // continue the unwinding process (which will now start with the
2055 // cleanup phase)
2056 unwindToNextLandingpad(state);
2057 }
2058
2059 // never return normally from the personality fn
2060 break;
2061 }
2062
2063 if (!isVoidReturn) {
2064 Type *t = caller->getType();
2065 if (t != Type::getVoidTy(i->getContext())) {
2066 // may need to do coercion due to bitcasts
2067 Expr::Width from = result->getWidth();
2068 Expr::Width to = getWidthForLLVMType(t);
2069
2070 if (from != to) {
2071 #if LLVM_VERSION_CODE >= LLVM_VERSION(8, 0)
2072 const CallBase &cs = cast<CallBase>(*caller);
2073 #else
2074 const CallSite cs(isa<InvokeInst>(caller)
2075 ? CallSite(cast<InvokeInst>(caller))
2076 : CallSite(cast<CallInst>(caller)));
2077 #endif
2078
2079 // XXX need to check other param attrs ?
2080 #if LLVM_VERSION_CODE >= LLVM_VERSION(5, 0)
2081 bool isSExt = cs.hasRetAttr(llvm::Attribute::SExt);
2082 #else
2083 bool isSExt = cs.paramHasAttr(0, llvm::Attribute::SExt);
2084 #endif
2085 if (isSExt) {
2086 result = SExtExpr::create(result, to);
2087 } else {
2088 result = ZExtExpr::create(result, to);
2089 }
2090 }
2091
2092 bindLocal(kcaller, state, result);
2093 }
2094 } else {
2095 // We check that the return value has no users instead of
2096 // checking the type, since C defaults to returning int for
2097 // undeclared functions.
2098 if (!caller->use_empty()) {
2099 terminateStateOnExecError(state, "return void when caller expected a result");
2100 }
2101 }
2102 }
2103 break;
2104 }
2105 case Instruction::Br: {
2106 BranchInst *bi = cast<BranchInst>(i);
2107 if (bi->isUnconditional()) {
2108 transferToBasicBlock(bi->getSuccessor(0), bi->getParent(), state);
2109 } else {
2110 // FIXME: Find a way that we don't have this hidden dependency.
2111 assert(bi->getCondition() == bi->getOperand(0) &&
2112 "Wrong operand index!");
2113 ref<Expr> cond = eval(ki, 0, state).value;
2114
2115 cond = optimizer.optimizeExpr(cond, false);
2116 Executor::StatePair branches = fork(state, cond, false);
2117
2118 // NOTE: There is a hidden dependency here, markBranchVisited
2119 // requires that we still be in the context of the branch
2120 // instruction (it reuses its statistic id). Should be cleaned
2121 // up with convenient instruction specific data.
2122 if (statsTracker && state.stack.back().kf->trackCoverage)
2123 statsTracker->markBranchVisited(branches.first, branches.second);
2124
2125 if (branches.first)
2126 transferToBasicBlock(bi->getSuccessor(0), bi->getParent(), *branches.first);
2127 if (branches.second)
2128 transferToBasicBlock(bi->getSuccessor(1), bi->getParent(), *branches.second);
2129 }
2130 break;
2131 }
2132 case Instruction::IndirectBr: {
2133 // implements indirect branch to a label within the current function
2134 const auto bi = cast<IndirectBrInst>(i);
2135 auto address = eval(ki, 0, state).value;
2136 address = toUnique(state, address);
2137
2138 // concrete address
2139 if (const auto CE = dyn_cast<ConstantExpr>(address.get())) {
2140 const auto bb_address = (BasicBlock *) CE->getZExtValue(Context::get().getPointerWidth());
2141 transferToBasicBlock(bb_address, bi->getParent(), state);
2142 break;
2143 }
2144
2145 // symbolic address
2146 const auto numDestinations = bi->getNumDestinations();
2147 std::vector<BasicBlock *> targets;
2148 targets.reserve(numDestinations);
2149 std::vector<ref<Expr>> expressions;
2150 expressions.reserve(numDestinations);
2151
2152 ref<Expr> errorCase = ConstantExpr::alloc(1, Expr::Bool);
2153 SmallPtrSet<BasicBlock *, 5> destinations;
2154 // collect and check destinations from label list
2155 for (unsigned k = 0; k < numDestinations; ++k) {
2156 // filter duplicates
2157 const auto d = bi->getDestination(k);
2158 if (destinations.count(d)) continue;
2159 destinations.insert(d);
2160
2161 // create address expression
2162 const auto PE = Expr::createPointer(reinterpret_cast<std::uint64_t>(d));
2163 ref<Expr> e = EqExpr::create(address, PE);
2164
2165 // exclude address from errorCase
2166 errorCase = AndExpr::create(errorCase, Expr::createIsZero(e));
2167
2168 // check feasibility
2169 bool result;
2170 bool success __attribute__((unused)) =
2171 solver->mayBeTrue(state.constraints, e, result, state.queryMetaData);
2172 assert(success && "FIXME: Unhandled solver failure");
2173 if (result) {
2174 targets.push_back(d);
2175 expressions.push_back(e);
2176 }
2177 }
2178 // check errorCase feasibility
2179 bool result;
2180 bool success __attribute__((unused)) = solver->mayBeTrue(
2181 state.constraints, errorCase, result, state.queryMetaData);
2182 assert(success && "FIXME: Unhandled solver failure");
2183 if (result) {
2184 expressions.push_back(errorCase);
2185 }
2186
2187 // fork states
2188 std::vector<ExecutionState *> branches;
2189 branch(state, expressions, branches);
2190
2191 // terminate error state
2192 if (result) {
2193 terminateStateOnExecError(*branches.back(), "indirectbr: illegal label address");
2194 branches.pop_back();
2195 }
2196
2197 // branch states to resp. target blocks
2198 assert(targets.size() == branches.size());
2199 for (std::vector<ExecutionState *>::size_type k = 0; k < branches.size(); ++k) {
2200 if (branches[k]) {
2201 transferToBasicBlock(targets[k], bi->getParent(), *branches[k]);
2202 }
2203 }
2204
2205 break;
2206 }
2207 case Instruction::Switch: {
2208 SwitchInst *si = cast<SwitchInst>(i);
2209 ref<Expr> cond = eval(ki, 0, state).value;
2210 BasicBlock *bb = si->getParent();
2211
2212 cond = toUnique(state, cond);
2213 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(cond)) {
2214 // Somewhat gross to create these all the time, but fine till we
2215 // switch to an internal rep.
2216 llvm::IntegerType *Ty = cast<IntegerType>(si->getCondition()->getType());
2217 ConstantInt *ci = ConstantInt::get(Ty, CE->getZExtValue());
2218 #if LLVM_VERSION_CODE >= LLVM_VERSION(5, 0)
2219 unsigned index = si->findCaseValue(ci)->getSuccessorIndex();
2220 #else
2221 unsigned index = si->findCaseValue(ci).getSuccessorIndex();
2222 #endif
2223 transferToBasicBlock(si->getSuccessor(index), si->getParent(), state);
2224 } else {
2225 // Handle possible different branch targets
2226
2227 // We have the following assumptions:
2228 // - each case value is mutual exclusive to all other values
2229 // - order of case branches is based on the order of the expressions of
2230 // the case values, still default is handled last
2231 std::vector<BasicBlock *> bbOrder;
2232 std::map<BasicBlock *, ref<Expr> > branchTargets;
2233
2234 std::map<ref<Expr>, BasicBlock *> expressionOrder;
2235
2236 // Iterate through all non-default cases and order them by expressions
2237 for (auto i : si->cases()) {
2238 ref<Expr> value = evalConstant(i.getCaseValue());
2239
2240 BasicBlock *caseSuccessor = i.getCaseSuccessor();
2241 expressionOrder.insert(std::make_pair(value, caseSuccessor));
2242 }
2243
2244 // Track default branch values
2245 ref<Expr> defaultValue = ConstantExpr::alloc(1, Expr::Bool);
2246
2247 // iterate through all non-default cases but in order of the expressions
2248 for (std::map<ref<Expr>, BasicBlock *>::iterator
2249 it = expressionOrder.begin(),
2250 itE = expressionOrder.end();
2251 it != itE; ++it) {
2252 ref<Expr> match = EqExpr::create(cond, it->first);
2253
2254 // skip if case has same successor basic block as default case
2255 // (should work even with phi nodes as a switch is a single terminating instruction)
2256 if (it->second == si->getDefaultDest()) continue;
2257
2258 // Make sure that the default value does not contain this target's value
2259 defaultValue = AndExpr::create(defaultValue, Expr::createIsZero(match));
2260
2261 // Check if control flow could take this case
2262 bool result;
2263 match = optimizer.optimizeExpr(match, false);
2264 bool success = solver->mayBeTrue(state.constraints, match, result,
2265 state.queryMetaData);
2266 assert(success && "FIXME: Unhandled solver failure");
2267 (void) success;
2268 if (result) {
2269 BasicBlock *caseSuccessor = it->second;
2270
2271 // Handle the case that a basic block might be the target of multiple
2272 // switch cases.
2273 // Currently we generate an expression containing all switch-case
2274 // values for the same target basic block. We spare us forking too
2275 // many times but we generate more complex condition expressions
2276 // TODO Add option to allow to choose between those behaviors
2277 std::pair<std::map<BasicBlock *, ref<Expr> >::iterator, bool> res =
2278 branchTargets.insert(std::make_pair(
2279 caseSuccessor, ConstantExpr::alloc(0, Expr::Bool)));
2280
2281 res.first->second = OrExpr::create(match, res.first->second);
2282
2283 // Only add basic blocks which have not been target of a branch yet
2284 if (res.second) {
2285 bbOrder.push_back(caseSuccessor);
2286 }
2287 }
2288 }
2289
2290 // Check if control could take the default case
2291 defaultValue = optimizer.optimizeExpr(defaultValue, false);
2292 bool res;
2293 bool success = solver->mayBeTrue(state.constraints, defaultValue, res,
2294 state.queryMetaData);
2295 assert(success && "FIXME: Unhandled solver failure");
2296 (void) success;
2297 if (res) {
2298 std::pair<std::map<BasicBlock *, ref<Expr> >::iterator, bool> ret =
2299 branchTargets.insert(
2300 std::make_pair(si->getDefaultDest(), defaultValue));
2301 if (ret.second) {
2302 bbOrder.push_back(si->getDefaultDest());
2303 }
2304 }
2305
2306 // Fork the current state with each state having one of the possible
2307 // successors of this switch
2308 std::vector< ref<Expr> > conditions;
2309 for (std::vector<BasicBlock *>::iterator it = bbOrder.begin(),
2310 ie = bbOrder.end();
2311 it != ie; ++it) {
2312 conditions.push_back(branchTargets[*it]);
2313 }
2314 std::vector<ExecutionState*> branches;
2315 branch(state, conditions, branches);
2316
2317 std::vector<ExecutionState*>::iterator bit = branches.begin();
2318 for (std::vector<BasicBlock *>::iterator it = bbOrder.begin(),
2319 ie = bbOrder.end();
2320 it != ie; ++it) {
2321 ExecutionState *es = *bit;
2322 if (es)
2323 transferToBasicBlock(*it, bb, *es);
2324 ++bit;
2325 }
2326 }
2327 break;
2328 }
2329 case Instruction::Unreachable:
2330 // Note that this is not necessarily an internal bug, llvm will
2331 // generate unreachable instructions in cases where it knows the
2332 // program will crash. So it is effectively a SEGV or internal
2333 // error.
2334 terminateStateOnExecError(state, "reached \"unreachable\" instruction");
2335 break;
2336
2337 case Instruction::Invoke:
2338 case Instruction::Call: {
2339 // Ignore debug intrinsic calls
2340 if (isa<DbgInfoIntrinsic>(i))
2341 break;
2342
2343 #if LLVM_VERSION_CODE >= LLVM_VERSION(8, 0)
2344 const CallBase &cs = cast<CallBase>(*i);
2345 Value *fp = cs.getCalledOperand();
2346 #else
2347 const CallSite cs(i);
2348 Value *fp = cs.getCalledValue();
2349 #endif
2350
2351 unsigned numArgs = cs.arg_size();
2352 Function *f = getTargetFunction(fp, state);
2353
2354 if (isa<InlineAsm>(fp)) {
2355 terminateStateOnExecError(state, "inline assembly is unsupported");
2356 break;
2357 }
2358 // evaluate arguments
2359 std::vector< ref<Expr> > arguments;
2360 arguments.reserve(numArgs);
2361
2362 for (unsigned j=0; j<numArgs; ++j)
2363 arguments.push_back(eval(ki, j+1, state).value);
2364
2365 if (f) {
2366 const FunctionType *fType =
2367 dyn_cast<FunctionType>(cast<PointerType>(f->getType())->getElementType());
2368 const FunctionType *fpType =
2369 dyn_cast<FunctionType>(cast<PointerType>(fp->getType())->getElementType());
2370
2371 // special case the call with a bitcast case
2372 if (fType != fpType) {
2373 assert(fType && fpType && "unable to get function type");
2374
2375 // XXX check result coercion
2376
2377 // XXX this really needs thought and validation
2378 unsigned i=0;
2379 for (std::vector< ref<Expr> >::iterator
2380 ai = arguments.begin(), ie = arguments.end();
2381 ai != ie; ++ai) {
2382 Expr::Width to, from = (*ai)->getWidth();
2383
2384 if (i<fType->getNumParams()) {
2385 to = getWidthForLLVMType(fType->getParamType(i));
2386
2387 if (from != to) {
2388 // XXX need to check other param attrs ?
2389 #if LLVM_VERSION_CODE >= LLVM_VERSION(5, 0)
2390 bool isSExt = cs.paramHasAttr(i, llvm::Attribute::SExt);
2391 #else
2392 bool isSExt = cs.paramHasAttr(i+1, llvm::Attribute::SExt);
2393 #endif
2394 if (isSExt) {
2395 arguments[i] = SExtExpr::create(arguments[i], to);
2396 } else {
2397 arguments[i] = ZExtExpr::create(arguments[i], to);
2398 }
2399 }
2400 }
2401
2402 i++;
2403 }
2404 }
2405
2406 executeCall(state, ki, f, arguments);
2407 } else {
2408 ref<Expr> v = eval(ki, 0, state).value;
2409
2410 ExecutionState *free = &state;
2411 bool hasInvalid = false, first = true;
2412
2413 /* XXX This is wasteful, no need to do a full evaluate since we
2414 have already got a value. But in the end the caches should
2415 handle it for us, albeit with some overhead. */
2416 do {
2417 v = optimizer.optimizeExpr(v, true);
2418 ref<ConstantExpr> value;
2419 bool success =
2420 solver->getValue(free->constraints, v, value, free->queryMetaData);
2421 assert(success && "FIXME: Unhandled solver failure");
2422 (void) success;
2423 StatePair res = fork(*free, EqExpr::create(v, value), true);
2424 if (res.first) {
2425 uint64_t addr = value->getZExtValue();
2426 if (legalFunctions.count(addr)) {
2427 f = (Function*) addr;
2428
2429 // Don't give warning on unique resolution
2430 if (res.second || !first)
2431 klee_warning_once(reinterpret_cast<void*>(addr),
2432 "resolved symbolic function pointer to: %s",
2433 f->getName().data());
2434
2435 executeCall(*res.first, ki, f, arguments);
2436 } else {
2437 if (!hasInvalid) {
2438 terminateStateOnExecError(state, "invalid function pointer");
2439 hasInvalid = true;
2440 }
2441 }
2442 }
2443
2444 first = false;
2445 free = res.second;
2446 } while (free);
2447 }
2448 break;
2449 }
2450 case Instruction::PHI: {
2451 ref<Expr> result = eval(ki, state.incomingBBIndex, state).value;
2452 bindLocal(ki, state, result);
2453 break;
2454 }
2455
2456 // Special instructions
2457 case Instruction::Select: {
2458 // NOTE: It is not required that operands 1 and 2 be of scalar type.
2459 ref<Expr> cond = eval(ki, 0, state).value;
2460 ref<Expr> tExpr = eval(ki, 1, state).value;
2461 ref<Expr> fExpr = eval(ki, 2, state).value;
2462 ref<Expr> result = SelectExpr::create(cond, tExpr, fExpr);
2463 bindLocal(ki, state, result);
2464 break;
2465 }
2466
2467 case Instruction::VAArg:
2468 terminateStateOnExecError(state, "unexpected VAArg instruction");
2469 break;
2470
2471 // Arithmetic / logical
2472
2473 case Instruction::Add: {
2474 ref<Expr> left = eval(ki, 0, state).value;
2475 ref<Expr> right = eval(ki, 1, state).value;
2476 bindLocal(ki, state, AddExpr::create(left, right));
2477 break;
2478 }
2479
2480 case Instruction::Sub: {
2481 ref<Expr> left = eval(ki, 0, state).value;
2482 ref<Expr> right = eval(ki, 1, state).value;
2483 bindLocal(ki, state, SubExpr::create(left, right));
2484 break;
2485 }
2486
2487 case Instruction::Mul: {
2488 ref<Expr> left = eval(ki, 0, state).value;
2489 ref<Expr> right = eval(ki, 1, state).value;
2490 bindLocal(ki, state, MulExpr::create(left, right));
2491 break;
2492 }
2493
2494 case Instruction::UDiv: {
2495 ref<Expr> left = eval(ki, 0, state).value;
2496 ref<Expr> right = eval(ki, 1, state).value;
2497 ref<Expr> result = UDivExpr::create(left, right);
2498 bindLocal(ki, state, result);
2499 break;
2500 }
2501
2502 case Instruction::SDiv: {
2503 ref<Expr> left = eval(ki, 0, state).value;
2504 ref<Expr> right = eval(ki, 1, state).value;
2505 ref<Expr> result = SDivExpr::create(left, right);
2506 bindLocal(ki, state, result);
2507 break;
2508 }
2509
2510 case Instruction::URem: {
2511 ref<Expr> left = eval(ki, 0, state).value;
2512 ref<Expr> right = eval(ki, 1, state).value;
2513 ref<Expr> result = URemExpr::create(left, right);
2514 bindLocal(ki, state, result);
2515 break;
2516 }
2517
2518 case Instruction::SRem: {
2519 ref<Expr> left = eval(ki, 0, state).value;
2520 ref<Expr> right = eval(ki, 1, state).value;
2521 ref<Expr> result = SRemExpr::create(left, right);
2522 bindLocal(ki, state, result);
2523 break;
2524 }
2525
2526 case Instruction::And: {
2527 ref<Expr> left = eval(ki, 0, state).value;
2528 ref<Expr> right = eval(ki, 1, state).value;
2529 ref<Expr> result = AndExpr::create(left, right);
2530 bindLocal(ki, state, result);
2531 break;
2532 }
2533
2534 case Instruction::Or: {
2535 ref<Expr> left = eval(ki, 0, state).value;
2536 ref<Expr> right = eval(ki, 1, state).value;
2537 ref<Expr> result = OrExpr::create(left, right);
2538 bindLocal(ki, state, result);
2539 break;
2540 }
2541
2542 case Instruction::Xor: {
2543 ref<Expr> left = eval(ki, 0, state).value;
2544 ref<Expr> right = eval(ki, 1, state).value;
2545 ref<Expr> result = XorExpr::create(left, right);
2546 bindLocal(ki, state, result);
2547 break;
2548 }
2549
2550 case Instruction::Shl: {
2551 ref<Expr> left = eval(ki, 0, state).value;
2552 ref<Expr> right = eval(ki, 1, state).value;
2553 ref<Expr> result = ShlExpr::create(left, right);
2554 bindLocal(ki, state, result);
2555 break;
2556 }
2557
2558 case Instruction::LShr: {
2559 ref<Expr> left = eval(ki, 0, state).value;
2560 ref<Expr> right = eval(ki, 1, state).value;
2561 ref<Expr> result = LShrExpr::create(left, right);
2562 bindLocal(ki, state, result);
2563 break;
2564 }
2565
2566 case Instruction::AShr: {
2567 ref<Expr> left = eval(ki, 0, state).value;
2568 ref<Expr> right = eval(ki, 1, state).value;
2569 ref<Expr> result = AShrExpr::create(left, right);
2570 bindLocal(ki, state, result);
2571 break;
2572 }
2573
2574 // Compare
2575
2576 case Instruction::ICmp: {
2577 CmpInst *ci = cast<CmpInst>(i);
2578 ICmpInst *ii = cast<ICmpInst>(ci);
2579
2580 switch(ii->getPredicate()) {
2581 case ICmpInst::ICMP_EQ: {
2582 ref<Expr> left = eval(ki, 0, state).value;
2583 ref<Expr> right = eval(ki, 1, state).value;
2584 ref<Expr> result = EqExpr::create(left, right);
2585 bindLocal(ki, state, result);
2586 break;
2587 }
2588
2589 case ICmpInst::ICMP_NE: {
2590 ref<Expr> left = eval(ki, 0, state).value;
2591 ref<Expr> right = eval(ki, 1, state).value;
2592 ref<Expr> result = NeExpr::create(left, right);
2593 bindLocal(ki, state, result);
2594 break;
2595 }
2596
2597 case ICmpInst::ICMP_UGT: {
2598 ref<Expr> left = eval(ki, 0, state).value;
2599 ref<Expr> right = eval(ki, 1, state).value;
2600 ref<Expr> result = UgtExpr::create(left, right);
2601 bindLocal(ki, state,result);
2602 break;
2603 }
2604
2605 case ICmpInst::ICMP_UGE: {
2606 ref<Expr> left = eval(ki, 0, state).value;
2607 ref<Expr> right = eval(ki, 1, state).value;
2608 ref<Expr> result = UgeExpr::create(left, right);
2609 bindLocal(ki, state, result);
2610 break;
2611 }
2612
2613 case ICmpInst::ICMP_ULT: {
2614 ref<Expr> left = eval(ki, 0, state).value;
2615 ref<Expr> right = eval(ki, 1, state).value;
2616 ref<Expr> result = UltExpr::create(left, right);
2617 bindLocal(ki, state, result);
2618 break;
2619 }
2620
2621 case ICmpInst::ICMP_ULE: {
2622 ref<Expr> left = eval(ki, 0, state).value;
2623 ref<Expr> right = eval(ki, 1, state).value;
2624 ref<Expr> result = UleExpr::create(left, right);
2625 bindLocal(ki, state, result);
2626 break;
2627 }
2628
2629 case ICmpInst::ICMP_SGT: {
2630 ref<Expr> left = eval(ki, 0, state).value;
2631 ref<Expr> right = eval(ki, 1, state).value;
2632 ref<Expr> result = SgtExpr::create(left, right);
2633 bindLocal(ki, state, result);
2634 break;
2635 }
2636
2637 case ICmpInst::ICMP_SGE: {
2638 ref<Expr> left = eval(ki, 0, state).value;
2639 ref<Expr> right = eval(ki, 1, state).value;
2640 ref<Expr> result = SgeExpr::create(left, right);
2641 bindLocal(ki, state, result);
2642 break;
2643 }
2644
2645 case ICmpInst::ICMP_SLT: {
2646 ref<Expr> left = eval(ki, 0, state).value;
2647 ref<Expr> right = eval(ki, 1, state).value;
2648 ref<Expr> result = SltExpr::create(left, right);
2649 bindLocal(ki, state, result);
2650 break;
2651 }
2652
2653 case ICmpInst::ICMP_SLE: {
2654 ref<Expr> left = eval(ki, 0, state).value;
2655 ref<Expr> right = eval(ki, 1, state).value;
2656 ref<Expr> result = SleExpr::create(left, right);
2657 bindLocal(ki, state, result);
2658 break;
2659 }
2660
2661 default:
2662 terminateStateOnExecError(state, "invalid ICmp predicate");
2663 }
2664 break;
2665 }
2666
2667 // Memory instructions...
2668 case Instruction::Alloca: {
2669 AllocaInst *ai = cast<AllocaInst>(i);
2670 unsigned elementSize =
2671 kmodule->targetData->getTypeStoreSize(ai->getAllocatedType());
2672 ref<Expr> size = Expr::createPointer(elementSize);
2673 if (ai->isArrayAllocation()) {
2674 ref<Expr> count = eval(ki, 0, state).value;
2675 count = Expr::createZExtToPointerWidth(count);
2676 size = MulExpr::create(size, count);
2677 }
2678 executeAlloc(state, size, true, ki);
2679 break;
2680 }
2681
2682 case Instruction::Load: {
2683 ref<Expr> base = eval(ki, 0, state).value;
2684 executeMemoryOperation(state, false, base, 0, ki);
2685 break;
2686 }
2687 case Instruction::Store: {
2688 ref<Expr> base = eval(ki, 1, state).value;
2689 ref<Expr> value = eval(ki, 0, state).value;
2690 executeMemoryOperation(state, true, base, value, 0);
2691 break;
2692 }
2693
2694 case Instruction::GetElementPtr: {
2695 KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(ki);
2696 ref<Expr> base = eval(ki, 0, state).value;
2697
2698 for (std::vector< std::pair<unsigned, uint64_t> >::iterator
2699 it = kgepi->indices.begin(), ie = kgepi->indices.end();
2700 it != ie; ++it) {
2701 uint64_t elementSize = it->second;
2702 ref<Expr> index = eval(ki, it->first, state).value;
2703 base = AddExpr::create(base,
2704 MulExpr::create(Expr::createSExtToPointerWidth(index),
2705 Expr::createPointer(elementSize)));
2706 }
2707 if (kgepi->offset)
2708 base = AddExpr::create(base,
2709 Expr::createPointer(kgepi->offset));
2710 bindLocal(ki, state, base);
2711 break;
2712 }
2713
2714 // Conversion
2715 case Instruction::Trunc: {
2716 CastInst *ci = cast<CastInst>(i);
2717 ref<Expr> result = ExtractExpr::create(eval(ki, 0, state).value,
2718 0,
2719 getWidthForLLVMType(ci->getType()));
2720 bindLocal(ki, state, result);
2721 break;
2722 }
2723 case Instruction::ZExt: {
2724 CastInst *ci = cast<CastInst>(i);
2725 ref<Expr> result = ZExtExpr::create(eval(ki, 0, state).value,
2726 getWidthForLLVMType(ci->getType()));
2727 bindLocal(ki, state, result);
2728 break;
2729 }
2730 case Instruction::SExt: {
2731 CastInst *ci = cast<CastInst>(i);
2732 ref<Expr> result = SExtExpr::create(eval(ki, 0, state).value,
2733 getWidthForLLVMType(ci->getType()));
2734 bindLocal(ki, state, result);
2735 break;
2736 }
2737
2738 case Instruction::IntToPtr: {
2739 CastInst *ci = cast<CastInst>(i);
2740 Expr::Width pType = getWidthForLLVMType(ci->getType());
2741 ref<Expr> arg = eval(ki, 0, state).value;
2742 bindLocal(ki, state, ZExtExpr::create(arg, pType));
2743 break;
2744 }
2745 case Instruction::PtrToInt: {
2746 CastInst *ci = cast<CastInst>(i);
2747 Expr::Width iType = getWidthForLLVMType(ci->getType());
2748 ref<Expr> arg = eval(ki, 0, state).value;
2749 bindLocal(ki, state, ZExtExpr::create(arg, iType));
2750 break;
2751 }
2752
2753 case Instruction::BitCast: {
2754 ref<Expr> result = eval(ki, 0, state).value;
2755 bindLocal(ki, state, result);
2756 break;
2757 }
2758
2759 // Floating point instructions
2760
2761 #if LLVM_VERSION_CODE >= LLVM_VERSION(8, 0)
2762 case Instruction::FNeg: {
2763 ref<ConstantExpr> arg =
2764 toConstant(state, eval(ki, 0, state).value, "floating point");
2765 if (!fpWidthToSemantics(arg->getWidth()))
2766 return terminateStateOnExecError(state, "Unsupported FNeg operation");
2767
2768 llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
2769 Res = llvm::neg(Res);
2770 bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
2771 break;
2772 }
2773 #endif
2774
2775 case Instruction::FAdd: {
2776 ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value,
2777 "floating point");
2778 ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value,
2779 "floating point");
2780 if (!fpWidthToSemantics(left->getWidth()) ||
2781 !fpWidthToSemantics(right->getWidth()))
2782 return terminateStateOnExecError(state, "Unsupported FAdd operation");
2783
2784 llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
2785 Res.add(APFloat(*fpWidthToSemantics(right->getWidth()),right->getAPValue()), APFloat::rmNearestTiesToEven);
2786 bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
2787 break;
2788 }
2789
2790 case Instruction::FSub: {
2791 ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value,
2792 "floating point");
2793 ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value,
2794 "floating point");
2795 if (!fpWidthToSemantics(left->getWidth()) ||
2796 !fpWidthToSemantics(right->getWidth()))
2797 return terminateStateOnExecError(state, "Unsupported FSub operation");
2798 llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
2799 Res.subtract(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven);
2800 bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
2801 break;
2802 }
2803
2804 case Instruction::FMul: {
2805 ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value,
2806 "floating point");
2807 ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value,
2808 "floating point");
2809 if (!fpWidthToSemantics(left->getWidth()) ||
2810 !fpWidthToSemantics(right->getWidth()))
2811 return terminateStateOnExecError(state, "Unsupported FMul operation");
2812
2813 llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
2814 Res.multiply(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven);
2815 bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
2816 break;
2817 }
2818
2819 case Instruction::FDiv: {
2820 ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value,
2821 "floating point");
2822 ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value,
2823 "floating point");
2824 if (!fpWidthToSemantics(left->getWidth()) ||
2825 !fpWidthToSemantics(right->getWidth()))
2826 return terminateStateOnExecError(state, "Unsupported FDiv operation");
2827
2828 llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
2829 Res.divide(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven);
2830 bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
2831 break;
2832 }
2833
2834 case Instruction::FRem: {
2835 ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value,
2836 "floating point");
2837 ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value,
2838 "floating point");
2839 if (!fpWidthToSemantics(left->getWidth()) ||
2840 !fpWidthToSemantics(right->getWidth()))
2841 return terminateStateOnExecError(state, "Unsupported FRem operation");
2842 llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
2843 Res.mod(
2844 APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()));
2845 bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
2846 break;
2847 }
2848
2849 case Instruction::FPTrunc: {
2850 FPTruncInst *fi = cast<FPTruncInst>(i);
2851 Expr::Width resultType = getWidthForLLVMType(fi->getType());
2852 ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
2853 "floating point");
2854 if (!fpWidthToSemantics(arg->getWidth()) || resultType > arg->getWidth())
2855 return terminateStateOnExecError(state, "Unsupported FPTrunc operation");
2856
2857 llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
2858 bool losesInfo = false;
2859 Res.convert(*fpWidthToSemantics(resultType),
2860 llvm::APFloat::rmNearestTiesToEven,
2861 &losesInfo);
2862 bindLocal(ki, state, ConstantExpr::alloc(Res));
2863 break;
2864 }
2865
2866 case Instruction::FPExt: {
2867 FPExtInst *fi = cast<FPExtInst>(i);
2868 Expr::Width resultType = getWidthForLLVMType(fi->getType());
2869 ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
2870 "floating point");
2871 if (!fpWidthToSemantics(arg->getWidth()) || arg->getWidth() > resultType)
2872 return terminateStateOnExecError(state, "Unsupported FPExt operation");
2873 llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
2874 bool losesInfo = false;
2875 Res.convert(*fpWidthToSemantics(resultType),
2876 llvm::APFloat::rmNearestTiesToEven,
2877 &losesInfo);
2878 bindLocal(ki, state, ConstantExpr::alloc(Res));
2879 break;
2880 }
2881
2882 case Instruction::FPToUI: {
2883 FPToUIInst *fi = cast<FPToUIInst>(i);
2884 Expr::Width resultType = getWidthForLLVMType(fi->getType());
2885 ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
2886 "floating point");
2887 if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64)
2888 return terminateStateOnExecError(state, "Unsupported FPToUI operation");
2889
2890 llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
2891 uint64_t value = 0;
2892 bool isExact = true;
2893 #if LLVM_VERSION_CODE >= LLVM_VERSION(5, 0)
2894 auto valueRef = makeMutableArrayRef(value);
2895 #else
2896 uint64_t *valueRef = &value;
2897 #endif
2898 Arg.convertToInteger(valueRef, resultType, false,
2899 llvm::APFloat::rmTowardZero, &isExact);
2900 bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
2901 break;
2902 }
2903
2904 case Instruction::FPToSI: {
2905 FPToSIInst *fi = cast<FPToSIInst>(i);
2906 Expr::Width resultType = getWidthForLLVMType(fi->getType());
2907 ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
2908 "floating point");
2909 if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64)
2910 return terminateStateOnExecError(state, "Unsupported FPToSI operation");
2911 llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
2912
2913 uint64_t value = 0;
2914 bool isExact = true;
2915 #if LLVM_VERSION_CODE >= LLVM_VERSION(5, 0)
2916 auto valueRef = makeMutableArrayRef(value);
2917 #else
2918 uint64_t *valueRef = &value;
2919 #endif
2920 Arg.convertToInteger(valueRef, resultType, true,
2921 llvm::APFloat::rmTowardZero, &isExact);
2922 bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
2923 break;
2924 }
2925
2926 case Instruction::UIToFP: {
2927 UIToFPInst *fi = cast<UIToFPInst>(i);
2928 Expr::Width resultType = getWidthForLLVMType(fi->getType());
2929 ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
2930 "floating point");
2931 const llvm::fltSemantics *semantics = fpWidthToSemantics(resultType);
2932 if (!semantics)
2933 return terminateStateOnExecError(state, "Unsupported UIToFP operation");
2934 llvm::APFloat f(*semantics, 0);
2935 f.convertFromAPInt(arg->getAPValue(), false,
2936 llvm::APFloat::rmNearestTiesToEven);
2937
2938 bindLocal(ki, state, ConstantExpr::alloc(f));
2939 break;
2940 }
2941
2942 case Instruction::SIToFP: {
2943 SIToFPInst *fi = cast<SIToFPInst>(i);
2944 Expr::Width resultType = getWidthForLLVMType(fi->getType());
2945 ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
2946 "floating point");
2947 const llvm::fltSemantics *semantics = fpWidthToSemantics(resultType);
2948 if (!semantics)
2949 return terminateStateOnExecError(state, "Unsupported SIToFP operation");
2950 llvm::APFloat f(*semantics, 0);
2951 f.convertFromAPInt(arg->getAPValue(), true,
2952 llvm::APFloat::rmNearestTiesToEven);
2953
2954 bindLocal(ki, state, ConstantExpr::alloc(f));
2955 break;
2956 }
2957
2958 case Instruction::FCmp: {
2959 FCmpInst *fi = cast<FCmpInst>(i);
2960 ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value,
2961 "floating point");
2962 ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value,
2963 "floating point");
2964 if (!fpWidthToSemantics(left->getWidth()) ||
2965 !fpWidthToSemantics(right->getWidth()))
2966 return terminateStateOnExecError(state, "Unsupported FCmp operation");
2967
2968 APFloat LHS(*fpWidthToSemantics(left->getWidth()),left->getAPValue());
2969 APFloat RHS(*fpWidthToSemantics(right->getWidth()),right->getAPValue());
2970 APFloat::cmpResult CmpRes = LHS.compare(RHS);
2971
2972 bool Result = false;
2973 switch( fi->getPredicate() ) {
2974 // Predicates which only care about whether or not the operands are NaNs.
2975 case FCmpInst::FCMP_ORD:
2976 Result = (CmpRes != APFloat::cmpUnordered);
2977 break;
2978
2979 case FCmpInst::FCMP_UNO:
2980 Result = (CmpRes == APFloat::cmpUnordered);
2981 break;
2982
2983 // Ordered comparisons return false if either operand is NaN. Unordered
2984 // comparisons return true if either operand is NaN.
2985 case FCmpInst::FCMP_UEQ:
2986 Result = (CmpRes == APFloat::cmpUnordered || CmpRes == APFloat::cmpEqual);
2987 break;
2988 case FCmpInst::FCMP_OEQ:
2989 Result = (CmpRes != APFloat::cmpUnordered && CmpRes == APFloat::cmpEqual);
2990 break;
2991
2992 case FCmpInst::FCMP_UGT:
2993 Result = (CmpRes == APFloat::cmpUnordered || CmpRes == APFloat::cmpGreaterThan);
2994 break;
2995 case FCmpInst::FCMP_OGT:
2996 Result = (CmpRes != APFloat::cmpUnordered && CmpRes == APFloat::cmpGreaterThan);
2997 break;
2998
2999 case FCmpInst::FCMP_UGE:
3000 Result = (CmpRes == APFloat::cmpUnordered || (CmpRes == APFloat::cmpGreaterThan || CmpRes == APFloat::cmpEqual));
3001 break;
3002 case FCmpInst::FCMP_OGE:
3003 Result = (CmpRes != APFloat::cmpUnordered && (CmpRes == APFloat::cmpGreaterThan || CmpRes == APFloat::cmpEqual));
3004 break;
3005
3006 case FCmpInst::FCMP_ULT:
3007 Result = (CmpRes == APFloat::cmpUnordered || CmpRes == APFloat::cmpLessThan);
3008 break;
3009 case FCmpInst::FCMP_OLT:
3010 Result = (CmpRes != APFloat::cmpUnordered && CmpRes == APFloat::cmpLessThan);
3011 break;
3012
3013 case FCmpInst::FCMP_ULE:
3014 Result = (CmpRes == APFloat::cmpUnordered || (CmpRes == APFloat::cmpLessThan || CmpRes == APFloat::cmpEqual));
3015 break;
3016 case FCmpInst::FCMP_OLE:
3017 Result = (CmpRes != APFloat::cmpUnordered && (CmpRes == APFloat::cmpLessThan || CmpRes == APFloat::cmpEqual));
3018 break;
3019
3020 case FCmpInst::FCMP_UNE:
3021 Result = (CmpRes == APFloat::cmpUnordered || CmpRes != APFloat::cmpEqual);
3022 break;
3023 case FCmpInst::FCMP_ONE:
3024 Result = (CmpRes != APFloat::cmpUnordered && CmpRes != APFloat::cmpEqual);
3025 break;
3026
3027 default:
3028 assert(0 && "Invalid FCMP predicate!");
3029 break;
3030 case FCmpInst::FCMP_FALSE:
3031 Result = false;
3032 break;
3033 case FCmpInst::FCMP_TRUE:
3034 Result = true;
3035 break;
3036 }
3037
3038 bindLocal(ki, state, ConstantExpr::alloc(Result, Expr::Bool));
3039 break;
3040 }
3041 case Instruction::InsertValue: {
3042 KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(ki);
3043
3044 ref<Expr> agg = eval(ki, 0, state).value;
3045 ref<Expr> val = eval(ki, 1, state).value;
3046
3047 ref<Expr> l = NULL, r = NULL;
3048 unsigned lOffset = kgepi->offset*8, rOffset = kgepi->offset*8 + val->getWidth();
3049
3050 if (lOffset > 0)
3051 l = ExtractExpr::create(agg, 0, lOffset);
3052 if (rOffset < agg->getWidth())
3053 r = ExtractExpr::create(agg, rOffset, agg->getWidth() - rOffset);
3054
3055 ref<Expr> result;
3056 if (l && r)
3057 result = ConcatExpr::create(r, ConcatExpr::create(val, l));
3058 else if (l)
3059 result = ConcatExpr::create(val, l);
3060 else if (r)
3061 result = ConcatExpr::create(r, val);
3062 else
3063 result = val;
3064
3065 bindLocal(ki, state, result);
3066 break;
3067 }
3068 case Instruction::ExtractValue: {
3069 KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(ki);
3070
3071 ref<Expr> agg = eval(ki, 0, state).value;
3072
3073 ref<Expr> result = ExtractExpr::create(agg, kgepi->offset*8, getWidthForLLVMType(i->getType()));
3074
3075 bindLocal(ki, state, result);
3076 break;
3077 }
3078 case Instruction::Fence: {
3079 // Ignore for now
3080 break;
3081 }
3082 case Instruction::InsertElement: {
3083 InsertElementInst *iei = cast<InsertElementInst>(i);
3084 ref<Expr> vec = eval(ki, 0, state).value;
3085 ref<Expr> newElt = eval(ki, 1, state).value;
3086 ref<Expr> idx = eval(ki, 2, state).value;
3087
3088 ConstantExpr *cIdx = dyn_cast<ConstantExpr>(idx);
3089 if (cIdx == NULL) {
3090 terminateStateOnError(
3091 state, "InsertElement, support for symbolic index not implemented",
3092 Unhandled);
3093 return;
3094 }
3095 uint64_t iIdx = cIdx->getZExtValue();
3096 const llvm::VectorType *vt = iei->getType();
3097 unsigned EltBits = getWidthForLLVMType(vt->getElementType());
3098
3099 if (iIdx >= vt->getNumElements()) {
3100 // Out of bounds write
3101 terminateStateOnError(state, "Out of bounds write when inserting element",
3102 BadVectorAccess);
3103 return;
3104 }
3105
3106 const unsigned elementCount = vt->getNumElements();
3107 llvm::SmallVector<ref<Expr>, 8> elems;
3108 elems.reserve(elementCount);
3109 for (unsigned i = elementCount; i != 0; --i) {
3110 auto of = i - 1;
3111 unsigned bitOffset = EltBits * of;
3112 elems.push_back(
3113 of == iIdx ? newElt : ExtractExpr::create(vec, bitOffset, EltBits));
3114 }
3115
3116 assert(Context::get().isLittleEndian() && "FIXME:Broken for big endian");
3117 ref<Expr> Result = ConcatExpr::createN(elementCount, elems.data());
3118 bindLocal(ki, state, Result);
3119 break;
3120 }
3121 case Instruction::ExtractElement: {
3122 ExtractElementInst *eei = cast<ExtractElementInst>(i);
3123 ref<Expr> vec = eval(ki, 0, state).value;
3124 ref<Expr> idx = eval(ki, 1, state).value;
3125
3126 ConstantExpr *cIdx = dyn_cast<ConstantExpr>(idx);
3127 if (cIdx == NULL) {
3128 terminateStateOnError(
3129 state, "ExtractElement, support for symbolic index not implemented",
3130 Unhandled);
3131 return;
3132 }
3133 uint64_t iIdx = cIdx->getZExtValue();
3134 const llvm::VectorType *vt = eei->getVectorOperandType();
3135 unsigned EltBits = getWidthForLLVMType(vt->getElementType());
3136
3137 if (iIdx >= vt->getNumElements()) {
3138 // Out of bounds read
3139 terminateStateOnError(state, "Out of bounds read when extracting element",
3140 BadVectorAccess);
3141 return;
3142 }
3143
3144 unsigned bitOffset = EltBits * iIdx;
3145 ref<Expr> Result = ExtractExpr::create(vec, bitOffset, EltBits);
3146 bindLocal(ki, state, Result);
3147 break;
3148 }
3149 case Instruction::ShuffleVector:
3150 // Should never happen due to Scalarizer pass removing ShuffleVector
3151 // instructions.
3152 terminateStateOnExecError(state, "Unexpected ShuffleVector instruction");
3153 break;
3154
3155 case Instruction::Resume: {
3156 auto *cui = dyn_cast_or_null<CleanupPhaseUnwindingInformation>(
3157 state.unwindingInformation.get());
3158
3159 if (!cui) {
3160 terminateStateOnExecError(
3161 state,
3162 "resume-instruction executed outside of cleanup phase unwinding");
3163 break;
3164 }
3165
3166 ref<Expr> arg = eval(ki, 0, state).value;
3167 ref<Expr> exceptionPointer = ExtractExpr::create(arg, 0, Expr::Int64);
3168 ref<Expr> selectorValue =
3169 ExtractExpr::create(arg, Expr::Int64, Expr::Int32);
3170
3171 if (!dyn_cast<ConstantExpr>(exceptionPointer) ||
3172 !dyn_cast<ConstantExpr>(selectorValue)) {
3173 terminateStateOnExecError(
3174 state, "resume-instruction called with non constant expression");
3175 break;
3176 }
3177
3178 if (!Expr::createIsZero(selectorValue)->isTrue()) {
3179 klee_warning("resume-instruction called with non-0 selector value");
3180 }
3181
3182 if (!EqExpr::create(exceptionPointer, cui->exceptionObject)->isTrue()) {
3183 terminateStateOnExecError(
3184 state, "resume-instruction called with unexpected exception pointer");
3185 break;
3186 }
3187
3188 unwindToNextLandingpad(state);
3189 break;
3190 }
3191
3192 case Instruction::LandingPad: {
3193 auto *cui = dyn_cast_or_null<CleanupPhaseUnwindingInformation>(
3194 state.unwindingInformation.get());
3195
3196 if (!cui) {
3197 terminateStateOnExecError(
3198 state, "Executing landing pad but not in unwinding phase 2");
3199 break;
3200 }
3201
3202 ref<ConstantExpr> exceptionPointer = cui->exceptionObject;
3203 ref<ConstantExpr> selectorValue;
3204
3205 // check on which frame we are currently
3206 if (state.stack.size() - 1 == cui->catchingStackIndex) {
3207 // we are in the target stack frame, return the selector value
3208 // that was returned by the personality fn in phase 1 and stop unwinding.
3209 selectorValue = cui->selectorValue;
3210
3211 // stop unwinding by cleaning up our unwinding information.
3212 state.unwindingInformation.reset();
3213
3214 // this would otherwise now be a dangling pointer
3215 cui = nullptr;
3216 } else {
3217 // we are not yet at the target stack frame. the landingpad might have
3218 // a cleanup clause or not, anyway, we give it the selector value "0",
3219 // which represents a cleanup, and expect it to handle it.
3220 // This is explicitly allowed by LLVM, see
3221 // https://llvm.org/docs/ExceptionHandling.html#id18
3222 selectorValue = ConstantExpr::create(0, Expr::Int32);
3223 }
3224
3225 // we have to return a {i8*, i32}
3226 ref<Expr> result = ConcatExpr::create(
3227 ZExtExpr::create(selectorValue, Expr::Int32), exceptionPointer);
3228
3229 bindLocal(ki, state, result);
3230
3231 break;
3232 }
3233
3234 case Instruction::AtomicRMW:
3235 terminateStateOnExecError(state, "Unexpected Atomic instruction, should be "
3236 "lowered by LowerAtomicInstructionPass");
3237 break;
3238 case Instruction::AtomicCmpXchg:
3239 terminateStateOnExecError(state,
3240 "Unexpected AtomicCmpXchg instruction, should be "
3241 "lowered by LowerAtomicInstructionPass");
3242 break;
3243 // Other instructions...
3244 // Unhandled
3245 default:
3246 terminateStateOnExecError(state, "illegal instruction");
3247 break;
3248 }
3249 }
3250
3251 void Executor::updateStates(ExecutionState *current) {
3252 if (searcher) {
3253 searcher->update(current, addedStates, removedStates);
3254 }
3255
3256 states.insert(addedStates.begin(), addedStates.end());
3257 addedStates.clear();
3258
3259 for (std::vector<ExecutionState *>::iterator it = removedStates.begin(),
3260 ie = removedStates.end();
3261 it != ie; ++it) {
3262 ExecutionState *es = *it;
3263 std::set<ExecutionState*>::iterator it2 = states.find(es);
3264 assert(it2!=states.end());
3265 states.erase(it2);
3266 std::map<ExecutionState*, std::vector<SeedInfo> >::iterator it3 =
3267 seedMap.find(es);
3268 if (it3 != seedMap.end())
3269 seedMap.erase(it3);
3270 processTree->remove(es->ptreeNode);
3271 delete es;
3272 }
3273 removedStates.clear();
3274 }
3275
3276 template <typename SqType, typename TypeIt>
3277 void Executor::computeOffsetsSeqTy(KGEPInstruction *kgepi,
3278 ref<ConstantExpr> &constantOffset,
3279 uint64_t index, const TypeIt it) {
3280 const auto *sq = cast<SqType>(*it);
3281 uint64_t elementSize =
3282 kmodule->targetData->getTypeStoreSize(sq->getElementType());
3283 const Value *operand = it.getOperand();
3284 if (const Constant *c = dyn_cast<Constant>(operand)) {
3285 ref<ConstantExpr> index =
3286 evalConstant(c)->SExt(Context::get().getPointerWidth());
3287 ref<ConstantExpr> addend = index->Mul(
3288 ConstantExpr::alloc(elementSize, Context::get().getPointerWidth()));
3289 constantOffset = constantOffset->Add(addend);
3290 } else {
3291 kgepi->indices.emplace_back(index, elementSize);
3292 }
3293 }
3294
3295 template <typename TypeIt>
3296 void Executor::computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) {
3297 ref<ConstantExpr> constantOffset =
3298 ConstantExpr::alloc(0, Context::get().getPointerWidth());
3299 uint64_t index = 1;
3300 for (TypeIt ii = ib; ii != ie; ++ii) {
3301 if (StructType *st = dyn_cast<StructType>(*ii)) {
3302 const StructLayout *sl = kmodule->targetData->getStructLayout(st);
3303 const ConstantInt *ci = cast<ConstantInt>(ii.getOperand());
3304 uint64_t addend = sl->getElementOffset((unsigned) ci->getZExtValue());
3305 constantOffset = constantOffset->Add(ConstantExpr::alloc(addend,
3306 Context::get().getPointerWidth()));
3307 #if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
3308 } else if (isa<ArrayType>(*ii)) {
3309 computeOffsetsSeqTy<ArrayType>(kgepi, constantOffset, index, ii);
3310 } else if (isa<VectorType>(*ii)) {
3311 computeOffsetsSeqTy<VectorType>(kgepi, constantOffset, index, ii);
3312 } else if (isa<PointerType>(*ii)) {
3313 computeOffsetsSeqTy<PointerType>(kgepi, constantOffset, index, ii);
3314 #else
3315 } else if (isa<SequentialType>(*ii)) {
3316 computeOffsetsSeqTy<SequentialType>(kgepi, constantOffset, index, ii);
3317 #endif
3318 } else
3319 assert("invalid type" && 0);
3320 index++;
3321 }
3322 kgepi->offset = constantOffset->getZExtValue();
3323 }
3324
3325 void Executor::bindInstructionConstants(KInstruction *KI) {
3326 if (GetElementPtrInst *gepi = dyn_cast<GetElementPtrInst>(KI->inst)) {
3327 KGEPInstruction *kgepi = static_cast<KGEPInstruction *>(KI);
3328 computeOffsets(kgepi, gep_type_begin(gepi), gep_type_end(gepi));
3329 } else if (InsertValueInst *ivi = dyn_cast<InsertValueInst>(KI->inst)) {
3330 KGEPInstruction *kgepi = static_cast<KGEPInstruction *>(KI);
3331 computeOffsets(kgepi, iv_type_begin(ivi), iv_type_end(ivi));
3332 assert(kgepi->indices.empty() && "InsertValue constant offset expected");
3333 } else if (ExtractValueInst *evi = dyn_cast<ExtractValueInst>(KI->inst)) {
3334 KGEPInstruction *kgepi = static_cast<KGEPInstruction *>(KI);
3335 computeOffsets(kgepi, ev_type_begin(evi), ev_type_end(evi));
3336 assert(kgepi->indices.empty() && "ExtractValue constant offset expected");
3337 }
3338 }
3339
3340 void Executor::bindModuleConstants() {
3341 for (auto &kfp : kmodule->functions) {
3342 KFunction *kf = kfp.get();
3343 for (unsigned i=0; i<kf->numInstructions; ++i)
3344 bindInstructionConstants(kf->instructions[i]);
3345 }
3346
3347 kmodule->constantTable =
3348 std::unique_ptr<Cell[]>(new Cell[kmodule->constants.size()]);
3349 for (unsigned i=0; i<kmodule->constants.size(); ++i) {
3350 Cell &c = kmodule->constantTable[i];
3351 c.value = evalConstant(kmodule->constants[i]);
3352 }
3353 }
3354
3355 bool Executor::checkMemoryUsage() {
3356 if (!MaxMemory) return true;
3357
3358 // We need to avoid calling GetTotalMallocUsage() often because it
3359 // is O(elts on freelist). This is really bad since we start
3360 // to pummel the freelist once we hit the memory cap.
3361 if ((stats::instructions & 0xFFFFU) != 0) // every 65536 instructions
3362 return true;
3363
3364 // check memory limit
3365 const auto mallocUsage = util::GetTotalMallocUsage() >> 20U;
3366 const auto mmapUsage = memory->getUsedDeterministicSize() >> 20U;
3367 const auto totalUsage = mallocUsage + mmapUsage;
3368 atMemoryLimit = totalUsage > MaxMemory; // inhibit forking
3369 if (!atMemoryLimit)
3370 return true;
3371
3372 // only terminate states when threshold (+100MB) exceeded
3373 if (totalUsage <= MaxMemory + 100)
3374 return true;
3375
3376 // just guess at how many to kill
3377 const auto numStates = states.size();
3378 auto toKill = std::max(1UL, numStates - numStates * MaxMemory / totalUsage);
3379 klee_warning("killing %lu states (over memory cap: %luMB)", toKill, totalUsage);
3380
3381 // randomly select states for early termination
3382 std::vector<ExecutionState *> arr(states.begin(), states.end()); // FIXME: expensive
3383 for (unsigned i = 0, N = arr.size(); N && i < toKill; ++i, --N) {
3384 unsigned idx = theRNG.getInt32() % N;
3385 // Make two pulls to try and not hit a state that
3386 // covered new code.
3387 if (arr[idx]->coveredNew)
3388 idx = theRNG.getInt32() % N;
3389
3390 std::swap(arr[idx], arr[N - 1]);
3391 terminateStateEarly(*arr[N - 1], "Memory limit exceeded.");
3392 }
3393
3394 return false;
3395 }
3396
3397 void Executor::doDumpStates() {
3398 if (!DumpStatesOnHalt || states.empty())
3399 return;
3400
3401 klee_message("halting execution, dumping remaining states");
3402 for (const auto &state : states)
3403 terminateStateEarly(*state, "Execution halting.");
3404 updateStates(nullptr);
3405 }
3406
3407 void Executor::run(ExecutionState &initialState) {
3408 bindModuleConstants();
3409
3410 // Delay init till now so that ticks don't accrue during optimization and such.
3411 timers.reset();
3412
3413 states.insert(&initialState);
3414
3415 if (usingSeeds) {
3416 std::vector<SeedInfo> &v = seedMap[&initialState];
3417
3418 for (std::vector<KTest*>::const_iterator it = usingSeeds->begin(),
3419 ie = usingSeeds->end(); it != ie; ++it)
3420 v.push_back(SeedInfo(*it));
3421
3422 int lastNumSeeds = usingSeeds->size()+10;
3423 time::Point lastTime, startTime = lastTime = time::getWallTime();
3424 ExecutionState *lastState = 0;
3425 while (!seedMap.empty()) {
3426 if (haltExecution) {
3427 doDumpStates();
3428 return;
3429 }
3430
3431 std::map<ExecutionState*, std::vector<SeedInfo> >::iterator it =
3432 seedMap.upper_bound(lastState);
3433 if (it == seedMap.end())
3434 it = seedMap.begin();
3435 lastState = it->first;
3436 ExecutionState &state = *lastState;
3437 KInstruction *ki = state.pc;
3438 stepInstruction(state);
3439
3440 executeInstruction(state, ki);
3441 timers.invoke();
3442 if (::dumpStates) dumpStates();
3443 if (::dumpPTree) dumpPTree();
3444 updateStates(&state);
3445
3446 if ((stats::instructions % 1000) == 0) {
3447 int numSeeds = 0, numStates = 0;
3448 for (std::map<ExecutionState*, std::vector<SeedInfo> >::iterator
3449 it = seedMap.begin(), ie = seedMap.end();
3450 it != ie; ++it) {
3451 numSeeds += it->second.size();
3452 numStates++;
3453 }
3454 const auto time = time::getWallTime();
3455 const time::Span seedTime(SeedTime);
3456 if (seedTime && time > startTime + seedTime) {
3457 klee_warning("seed time expired, %d seeds remain over %d states",
3458 numSeeds, numStates);
3459 break;
3460 } else if (numSeeds<=lastNumSeeds-10 ||
3461 time - lastTime >= time::seconds(10)) {
3462 lastTime = time;
3463 lastNumSeeds = numSeeds;
3464 klee_message("%d seeds remaining over: %d states",
3465 numSeeds, numStates);
3466 }
3467 }
3468 }
3469
3470 klee_message("seeding done (%d states remain)", (int) states.size());
3471
3472 if (OnlySeed) {
3473 doDumpStates();
3474 return;
3475 }
3476 }
3477
3478 searcher = constructUserSearcher(*this);
3479
3480 std::vector<ExecutionState *> newStates(states.begin(), states.end());
3481 searcher->update(0, newStates, std::vector<ExecutionState *>());
3482
3483 // main interpreter loop
3484 while (!states.empty() && !haltExecution) {
3485 ExecutionState &state = searcher->selectState();
3486 KInstruction *ki = state.pc;
3487 stepInstruction(state);
3488
3489 executeInstruction(state, ki);
3490 timers.invoke();
3491 if (::dumpStates) dumpStates();
3492 if (::dumpPTree) dumpPTree();
3493
3494 updateStates(&state);
3495
3496 if (!checkMemoryUsage()) {
3497 // update searchers when states were terminated early due to memory pressure
3498 updateStates(nullptr);
3499 }
3500 }
3501
3502 delete searcher;
3503 searcher = nullptr;
3504
3505 doDumpStates();
3506 }
3507
3508 std::string Executor::getAddressInfo(ExecutionState &state,
3509 ref<Expr> address) const{
3510 std::string Str;
3511 llvm::raw_string_ostream info(Str);
3512 info << "\taddress: " << address << "\n";
3513 uint64_t example;
3514 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) {
3515 example = CE->getZExtValue();
3516 } else {
3517 ref<ConstantExpr> value;
3518 bool success = solver->getValue(state.constraints, address, value,
3519 state.queryMetaData);
3520 assert(success && "FIXME: Unhandled solver failure");
3521 (void) success;
3522 example = value->getZExtValue();
3523 info << "\texample: " << example << "\n";
3524 std::pair<ref<Expr>, ref<Expr>> res =
3525 solver->getRange(state.constraints, address, state.queryMetaData);
3526 info << "\trange: [" << res.first << ", " << res.second <<"]\n";
3527 }
3528
3529 MemoryObject hack((unsigned) example);
3530 MemoryMap::iterator lower = state.addressSpace.objects.upper_bound(&hack);
3531 info << "\tnext: ";
3532 if (lower==state.addressSpace.objects.end()) {
3533 info << "none\n";
3534 } else {
3535 const MemoryObject *mo = lower->first;
3536 std::string alloc_info;
3537 mo->getAllocInfo(alloc_info);
3538 info << "object at " << mo->address
3539 << " of size " << mo->size << "\n"
3540 << "\t\t" << alloc_info << "\n";
3541 }
3542 if (lower!=state.addressSpace.objects.begin()) {
3543 --lower;
3544 info << "\tprev: ";
3545 if (lower==state.addressSpace.objects.end()) {
3546 info << "none\n";
3547 } else {
3548 const MemoryObject *mo = lower->first;
3549 std::string alloc_info;
3550 mo->getAllocInfo(alloc_info);
3551 info << "object at " << mo->address
3552 << " of size " << mo->size << "\n"
3553 << "\t\t" << alloc_info << "\n";
3554 }
3555 }
3556
3557 return info.str();
3558 }
3559
3560
3561 void Executor::terminateState(ExecutionState &state) {
3562 if (replayKTest && replayPosition!=replayKTest->numObjects) {
3563 klee_warning_once(replayKTest,
3564 "replay did not consume all objects in test input.");
3565 }
3566
3567 interpreterHandler->incPathsExplored();
3568
3569 std::vector<ExecutionState *>::iterator it =
3570 std::find(addedStates.begin(), addedStates.end(), &state);
3571 if (it==addedStates.end()) {
3572 state.pc = state.prevPC;
3573
3574 removedStates.push_back(&state);
3575 } else {
3576 // never reached searcher, just delete immediately
3577 std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it3 =
3578 seedMap.find(&state);
3579 if (it3 != seedMap.end())
3580 seedMap.erase(it3);
3581 addedStates.erase(it);
3582 processTree->remove(state.ptreeNode);
3583 delete &state;
3584 }
3585 }
3586
3587 void Executor::terminateStateEarly(ExecutionState &state,
3588 const Twine &message) {
3589 if (!OnlyOutputStatesCoveringNew || state.coveredNew ||
3590 (AlwaysOutputSeeds && seedMap.count(&state)))
3591 interpreterHandler->processTestCase(state, (message + "\n").str().c_str(),
3592 "early");
3593 terminateState(state);
3594 }
3595
3596 void Executor::terminateStateOnExit(ExecutionState &state) {
3597 if (!OnlyOutputStatesCoveringNew || state.coveredNew ||
3598 (AlwaysOutputSeeds && seedMap.count(&state)))
3599 interpreterHandler->processTestCase(state, 0, 0);
3600 terminateState(state);
3601 }
3602
3603 const InstructionInfo & Executor::getLastNonKleeInternalInstruction(const ExecutionState &state,
3604 Instruction ** lastInstruction) {
3605 // unroll the stack of the applications state and find
3606 // the last instruction which is not inside a KLEE internal function
3607 ExecutionState::stack_ty::const_reverse_iterator it = state.stack.rbegin(),
3608 itE = state.stack.rend();
3609
3610 // don't check beyond the outermost function (i.e. main())
3611 itE--;
3612
3613 const InstructionInfo * ii = 0;
3614 if (kmodule->internalFunctions.count(it->kf->function) == 0){
3615 ii = state.prevPC->info;
3616 *lastInstruction = state.prevPC->inst;
3617 // Cannot return yet because even though
3618 // it->function is not an internal function it might of
3619 // been called from an internal function.
3620 }
3621
3622 // Wind up the stack and check if we are in a KLEE internal function.
3623 // We visit the entire stack because we want to return a CallInstruction
3624 // that was not reached via any KLEE internal functions.
3625 for (;it != itE; ++it) {
3626 // check calling instruction and if it is contained in a KLEE internal function
3627 const Function * f = (*it->caller).inst->getParent()->getParent();
3628 if (kmodule->internalFunctions.count(f)){
3629 ii = 0;
3630 continue;
3631 }
3632 if (!ii){
3633 ii = (*it->caller).info;
3634 *lastInstruction = (*it->caller).inst;
3635 }
3636 }
3637
3638 if (!ii) {
3639 // something went wrong, play safe and return the current instruction info
3640 *lastInstruction = state.prevPC->inst;
3641 return *state.prevPC->info;
3642 }
3643 return *ii;
3644 }
3645
3646 bool Executor::shouldExitOn(enum TerminateReason termReason) {
3647 std::vector<TerminateReason>::iterator s = ExitOnErrorType.begin();
3648 std::vector<TerminateReason>::iterator e = ExitOnErrorType.end();
3649
3650 for (; s != e; ++s)
3651 if (termReason == *s)
3652 return true;
3653
3654 return false;
3655 }
3656
3657 void Executor::terminateStateOnError(ExecutionState &state,
3658 const llvm::Twine &messaget,
3659 enum TerminateReason termReason,
3660 const char *suffix,
3661 const llvm::Twine &info) {
3662 std::string message = messaget.str();
3663 static std::set< std::pair<Instruction*, std::string> > emittedErrors;
3664 Instruction * lastInst;
3665 const InstructionInfo &ii = getLastNonKleeInternalInstruction(state, &lastInst);
3666
3667 if (EmitAllErrors ||
3668 emittedErrors.insert(std::make_pair(lastInst, message)).second) {
3669 if (ii.file != "") {
3670 klee_message("ERROR: %s:%d: %s", ii.file.c_str(), ii.line, message.c_str());
3671 } else {
3672 klee_message("ERROR: (location information missing) %s", message.c_str());
3673 }
3674 if (!EmitAllErrors)
3675 klee_message("NOTE: now ignoring this error at this location");
3676
3677 std::string MsgString;
3678 llvm::raw_string_ostream msg(MsgString);
3679 msg << "Error: " << message << '\n';
3680 if (ii.file != "") {
3681 msg << "File: " << ii.file << '\n'
3682 << "Line: " << ii.line << '\n'
3683 << "assembly.ll line: " << ii.assemblyLine << '\n'
3684 << "State: " << state.getID() << '\n';
3685 }
3686 msg << "Stack: \n";
3687 state.dumpStack(msg);
3688
3689 std::string info_str = info.str();
3690 if (info_str != "")
3691 msg << "Info: \n" << info_str;
3692
3693 std::string suffix_buf;
3694 if (!suffix) {
3695 suffix_buf = TerminateReasonNames[termReason];
3696 suffix_buf += ".err";
3697 suffix = suffix_buf.c_str();
3698 }
3699
3700 interpreterHandler->processTestCase(state, msg.str().c_str(), suffix);
3701 }
3702
3703 terminateState(state);
3704
3705 if (shouldExitOn(termReason))
3706 haltExecution = true;
3707 }
3708
3709 // XXX shoot me
3710 static const char *okExternalsList[] = { "printf",
3711 "fprintf",
3712 "puts",
3713 "getpid" };
3714 static std::set<std::string> okExternals(okExternalsList,
3715 okExternalsList +
3716 (sizeof(okExternalsList)/sizeof(okExternalsList[0])));
3717
3718 void Executor::callExternalFunction(ExecutionState &state,
3719 KInstruction *target,
3720 Function *function,
3721 std::vector< ref<Expr> > &arguments) {
3722 // check if specialFunctionHandler wants it
3723 if (specialFunctionHandler->handle(state, function, target, arguments))
3724 return;
3725
3726 if (ExternalCalls == ExternalCallPolicy::None &&
3727 !okExternals.count(function->getName().str())) {
3728 klee_warning("Disallowed call to external function: %s\n",
3729 function->getName().str().c_str());
3730 terminateStateOnError(state, "external calls disallowed", User);
3731 return;
3732 }
3733
3734 // normal external function handling path
3735 // allocate 128 bits for each argument (+return value) to support fp80's;
3736 // we could iterate through all the arguments first and determine the exact
3737 // size we need, but this is faster, and the memory usage isn't significant.
3738 uint64_t *args = (uint64_t*) alloca(2*sizeof(*args) * (arguments.size() + 1));
3739 memset(args, 0, 2 * sizeof(*args) * (arguments.size() + 1));
3740 unsigned wordIndex = 2;
3741 for (std::vector<ref<Expr> >::iterator ai = arguments.begin(),
3742 ae = arguments.end(); ai!=ae; ++ai) {
3743 if (ExternalCalls == ExternalCallPolicy::All) { // don't bother checking uniqueness
3744 *ai = optimizer.optimizeExpr(*ai, true);
3745 ref<ConstantExpr> ce;
3746 bool success =
3747 solver->getValue(state.constraints, *ai, ce, state.queryMetaData);
3748 assert(success && "FIXME: Unhandled solver failure");
3749 (void) success;
3750 ce->toMemory(&args[wordIndex]);
3751 ObjectPair op;
3752 // Checking to see if the argument is a pointer to something
3753 if (ce->getWidth() == Context::get().getPointerWidth() &&
3754 state.addressSpace.resolveOne(ce, op)) {
3755 op.second->flushToConcreteStore(solver, state);
3756 }
3757 wordIndex += (ce->getWidth()+63)/64;
3758 } else {
3759 ref<Expr> arg = toUnique(state, *ai);
3760 if (ConstantExpr *ce = dyn_cast<ConstantExpr>(arg)) {
3761 // XXX kick toMemory functions from here
3762 ce->toMemory(&args[wordIndex]);
3763 wordIndex += (ce->getWidth()+63)/64;
3764 } else {
3765 terminateStateOnExecError(state,
3766 "external call with symbolic argument: " +
3767 function->getName());
3768 return;
3769 }
3770 }
3771 }
3772
3773 // Prepare external memory for invoking the function
3774 state.addressSpace.copyOutConcretes();
3775 #ifndef WINDOWS
3776 // Update external errno state with local state value
3777 int *errno_addr = getErrnoLocation(state);
3778 ObjectPair result;
3779 bool resolved = state.addressSpace.resolveOne(
3780 ConstantExpr::create((uint64_t)errno_addr, Expr::Int64), result);
3781 if (!resolved)
3782 klee_error("Could not resolve memory object for errno");
3783 ref<Expr> errValueExpr = result.second->read(0, sizeof(*errno_addr) * 8);
3784 ConstantExpr *errnoValue = dyn_cast<ConstantExpr>(errValueExpr);
3785 if (!errnoValue) {
3786 terminateStateOnExecError(state,
3787 "external call with errno value symbolic: " +
3788 function->getName());
3789 return;
3790 }
3791
3792 externalDispatcher->setLastErrno(
3793 errnoValue->getZExtValue(sizeof(*errno_addr) * 8));
3794 #endif
3795
3796 if (!SuppressExternalWarnings) {
3797
3798 std::string TmpStr;
3799 llvm::raw_string_ostream os(TmpStr);
3800 os << "calling external: " << function->getName().str() << "(";
3801 for (unsigned i=0; i<arguments.size(); i++) {
3802 os << arguments[i];
3803 if (i != arguments.size()-1)
3804 os << ", ";
3805 }
3806 os << ") at " << state.pc->getSourceLocation();
3807
3808 if (AllExternalWarnings)
3809 klee_warning("%s", os.str().c_str());
3810 else
3811 klee_warning_once(function, "%s", os.str().c_str());
3812 }
3813
3814 bool success = externalDispatcher->executeCall(function, target->inst, args);
3815 if (!success) {
3816 terminateStateOnError(state, "failed external call: " + function->getName(),
3817 External);
3818 return;
3819 }
3820
3821 if (!state.addressSpace.copyInConcretes()) {
3822 terminateStateOnError(state, "external modified read-only object",
3823 External);
3824 return;
3825 }
3826
3827 #ifndef WINDOWS
3828 // Update errno memory object with the errno value from the call
3829 int error = externalDispatcher->getLastErrno();
3830 state.addressSpace.copyInConcrete(result.first, result.second,
3831 (uint64_t)&error);
3832 #endif
3833
3834 Type *resultType = target->inst->getType();
3835 if (resultType != Type::getVoidTy(function->getContext())) {
3836 ref<Expr> e = ConstantExpr::fromMemory((void*) args,
3837 getWidthForLLVMType(resultType));
3838 bindLocal(target, state, e);
3839 }
3840 }
3841
3842 /***/
3843
3844 ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state,
3845 ref<Expr> e) {
3846 unsigned n = interpreterOpts.MakeConcreteSymbolic;
3847 if (!n || replayKTest || replayPath)
3848 return e;
3849
3850 // right now, we don't replace symbolics (is there any reason to?)
3851 if (!isa<ConstantExpr>(e))
3852 return e;
3853
3854 if (n != 1 && random() % n)
3855 return e;
3856
3857 // create a new fresh location, assert it is equal to concrete value in e
3858 // and return it.
3859
3860 static unsigned id;
3861 const Array *array =
3862 arrayCache.CreateArray("rrws_arr" + llvm::utostr(++id),
3863 Expr::getMinBytesForWidth(e->getWidth()));
3864 ref<Expr> res = Expr::createTempRead(array, e->getWidth());
3865 ref<Expr> eq = NotOptimizedExpr::create(EqExpr::create(e, res));
3866 llvm::errs() << "Making symbolic: " << eq << "\n";
3867 state.addConstraint(eq);
3868 return res;
3869 }
3870
3871 ObjectState *Executor::bindObjectInState(ExecutionState &state,
3872 const MemoryObject *mo,
3873 bool isLocal,
3874 const Array *array) {
3875 ObjectState *os = array ? new ObjectState(mo, array) : new ObjectState(mo);
3876 state.addressSpace.bindObject(mo, os);
3877
3878 // Its possible that multiple bindings of the same mo in the state
3879 // will put multiple copies on this list, but it doesn't really
3880 // matter because all we use this list for is to unbind the object
3881 // on function return.
3882 if (isLocal)
3883 state.stack.back().allocas.push_back(mo);
3884
3885 return os;
3886 }
3887
3888 void Executor::executeAlloc(ExecutionState &state,
3889 ref<Expr> size,
3890 bool isLocal,
3891 KInstruction *target,
3892 bool zeroMemory,
3893 const ObjectState *reallocFrom,
3894 size_t allocationAlignment) {
3895 size = toUnique(state, size);
3896 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(size)) {
3897 const llvm::Value *allocSite = state.prevPC->inst;
3898 if (allocationAlignment == 0) {
3899 allocationAlignment = getAllocationAlignment(allocSite);
3900 }
3901 MemoryObject *mo =
3902 memory->allocate(CE->getZExtValue(), isLocal, /*isGlobal=*/false,
3903 allocSite, allocationAlignment);
3904 if (!mo) {
3905 bindLocal(target, state,
3906 ConstantExpr::alloc(0, Context::get().getPointerWidth()));
3907 } else {
3908 ObjectState *os = bindObjectInState(state, mo, isLocal);
3909 if (zeroMemory) {
3910 os->initializeToZero();
3911 } else {
3912 os->initializeToRandom();
3913 }
3914 bindLocal(target, state, mo->getBaseExpr());
3915
3916 if (reallocFrom) {
3917 unsigned count = std::min(reallocFrom->size, os->size);
3918 for (unsigned i=0; i<count; i++)
3919 os->write(i, reallocFrom->read8(i));
3920 state.addressSpace.unbindObject(reallocFrom->getObject());
3921 }
3922 }
3923 } else {
3924 // XXX For now we just pick a size. Ideally we would support
3925 // symbolic sizes fully but even if we don't it would be better to
3926 // "smartly" pick a value, for example we could fork and pick the
3927 // min and max values and perhaps some intermediate (reasonable
3928 // value).
3929 //
3930 // It would also be nice to recognize the case when size has
3931 // exactly two values and just fork (but we need to get rid of
3932 // return argument first). This shows up in pcre when llvm
3933 // collapses the size expression with a select.
3934
3935 size = optimizer.optimizeExpr(size, true);
3936
3937 ref<ConstantExpr> example;
3938 bool success =
3939 solver->getValue(state.constraints, size, example, state.queryMetaData);
3940 assert(success && "FIXME: Unhandled solver failure");
3941 (void) success;
3942
3943 // Try and start with a small example.
3944 Expr::Width W = example->getWidth();
3945 while (example->Ugt(ConstantExpr::alloc(128, W))->isTrue()) {
3946 ref<ConstantExpr> tmp = example->LShr(ConstantExpr::alloc(1, W));
3947 bool res;
3948 bool success =
3949 solver->mayBeTrue(state.constraints, EqExpr::create(tmp, size), res,
3950 state.queryMetaData);
3951 assert(success && "FIXME: Unhandled solver failure");
3952 (void) success;
3953 if (!res)
3954 break;
3955 example = tmp;
3956 }
3957
3958 StatePair fixedSize = fork(state, EqExpr::create(example, size), true);
3959
3960 if (fixedSize.second) {
3961 // Check for exactly two values
3962 ref<ConstantExpr> tmp;
3963 bool success = solver->getValue(fixedSize.second->constraints, size, tmp,
3964 fixedSize.second->queryMetaData);
3965 assert(success && "FIXME: Unhandled solver failure");
3966 (void) success;
3967 bool res;
3968 success = solver->mustBeTrue(fixedSize.second->constraints,
3969 EqExpr::create(tmp, size), res,
3970 fixedSize.second->queryMetaData);
3971 assert(success && "FIXME: Unhandled solver failure");
3972 (void) success;
3973 if (res) {
3974 executeAlloc(*fixedSize.second, tmp, isLocal,
3975 target, zeroMemory, reallocFrom);
3976 } else {
3977 // See if a *really* big value is possible. If so assume
3978 // malloc will fail for it, so lets fork and return 0.
3979 StatePair hugeSize =
3980 fork(*fixedSize.second,
3981 UltExpr::create(ConstantExpr::alloc(1U<<31, W), size),
3982 true);
3983 if (hugeSize.first) {
3984 klee_message("NOTE: found huge malloc, returning 0");
3985 bindLocal(target, *hugeSize.first,
3986 ConstantExpr::alloc(0, Context::get().getPointerWidth()));
3987 }
3988
3989 if (hugeSize.second) {
3990
3991 std::string Str;
3992 llvm::raw_string_ostream info(Str);
3993 ExprPPrinter::printOne(info, " size expr", size);
3994 info << " concretization : " << example << "\n";
3995 info << " unbound example: " << tmp << "\n";
3996 terminateStateOnError(*hugeSize.second, "concretized symbolic size",
3997 Model, NULL, info.str());
3998 }
3999 }
4000 }
4001
4002 if (fixedSize.first) // can be zero when fork fails
4003 executeAlloc(*fixedSize.first, example, isLocal,
4004 target, zeroMemory, reallocFrom);
4005 }
4006 }
4007
4008 void Executor::executeFree(ExecutionState &state,
4009 ref<Expr> address,
4010 KInstruction *target) {
4011 address = optimizer.optimizeExpr(address, true);
4012 StatePair zeroPointer = fork(state, Expr::createIsZero(address), true);
4013 if (zeroPointer.first) {
4014 if (target)
4015 bindLocal(target, *zeroPointer.first, Expr::createPointer(0));
4016 }
4017 if (zeroPointer.second) { // address != 0
4018 ExactResolutionList rl;
4019 resolveExact(*zeroPointer.second, address, rl, "free");
4020
4021 for (Executor::ExactResolutionList::iterator it = rl.begin(),
4022 ie = rl.end(); it != ie; ++it) {
4023 const MemoryObject *mo = it->first.first;
4024 if (mo->isLocal) {
4025 terminateStateOnError(*it->second, "free of alloca", Free, NULL,
4026 getAddressInfo(*it->second, address));
4027 } else if (mo->isGlobal) {
4028 terminateStateOnError(*it->second, "free of global", Free, NULL,
4029 getAddressInfo(*it->second, address));
4030 } else {
4031 it->second->addressSpace.unbindObject(mo);
4032 if (target)
4033 bindLocal(target, *it->second, Expr::createPointer(0));
4034 }
4035 }
4036 }
4037 }
4038
4039 void Executor::resolveExact(ExecutionState &state,
4040 ref<Expr> p,
4041 ExactResolutionList &results,
4042 const std::string &name) {
4043 p = optimizer.optimizeExpr(p, true);
4044 // XXX we may want to be capping this?
4045 ResolutionList rl;
4046 state.addressSpace.resolve(state, solver, p, rl);
4047
4048 ExecutionState *unbound = &state;
4049 for (ResolutionList::iterator it = rl.begin(), ie = rl.end();
4050 it != ie; ++it) {
4051 ref<Expr> inBounds = EqExpr::create(p, it->first->getBaseExpr());
4052
4053 StatePair branches = fork(*unbound, inBounds, true);
4054
4055 if (branches.first)
4056 results.push_back(std::make_pair(*it, branches.first));
4057
4058 unbound = branches.second;
4059 if (!unbound) // Fork failure
4060 break;
4061 }
4062
4063 if (unbound) {
4064 terminateStateOnError(*unbound, "memory error: invalid pointer: " + name,
4065 Ptr, NULL, getAddressInfo(*unbound, p));
4066 }
4067 }
4068
4069 void Executor::executeMemoryOperation(ExecutionState &state,
4070 bool isWrite,
4071 ref<Expr> address,
4072 ref<Expr> value /* undef if read */,
4073 KInstruction *target /* undef if write */) {
4074 Expr::Width type = (isWrite ? value->getWidth() :
4075 getWidthForLLVMType(target->inst->getType()));
4076 unsigned bytes = Expr::getMinBytesForWidth(type);
4077
4078 if (SimplifySymIndices) {
4079 if (!isa<ConstantExpr>(address))
4080 address = ConstraintManager::simplifyExpr(state.constraints, address);
4081 if (isWrite && !isa<ConstantExpr>(value))
4082 value = ConstraintManager::simplifyExpr(state.constraints, value);
4083 }
4084
4085 address = optimizer.optimizeExpr(address, true);
4086
4087 // fast path: single in-bounds resolution
4088 ObjectPair op;
4089 bool success;
4090 solver->setTimeout(coreSolverTimeout);
4091 if (!state.addressSpace.resolveOne(state, solver, address, op, success)) {
4092 address = toConstant(state, address, "resolveOne failure");
4093 success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op);
4094 }
4095 solver->setTimeout(time::Span());
4096
4097 if (success) {
4098 const MemoryObject *mo = op.first;
4099
4100 if (MaxSymArraySize && mo->size >= MaxSymArraySize) {
4101 address = toConstant(state, address, "max-sym-array-size");
4102 }
4103
4104 ref<Expr> offset = mo->getOffsetExpr(address);
4105 ref<Expr> check = mo->getBoundsCheckOffset(offset, bytes);
4106 check = optimizer.optimizeExpr(check, true);
4107
4108 bool inBounds;
4109 solver->setTimeout(coreSolverTimeout);
4110 bool success = solver->mustBeTrue(state.constraints, check, inBounds,
4111 state.queryMetaData);
4112 solver->setTimeout(time::Span());
4113 if (!success) {
4114 state.pc = state.prevPC;
4115 terminateStateEarly(state, "Query timed out (bounds check).");
4116 return;
4117 }
4118
4119 if (inBounds) {
4120 const ObjectState *os = op.second;
4121 if (isWrite) {
4122 if (os->readOnly) {
4123 terminateStateOnError(state, "memory error: object read only",
4124 ReadOnly);
4125 } else {
4126 ObjectState *wos = state.addressSpace.getWriteable(mo, os);
4127 wos->write(offset, value);
4128 }
4129 } else {
4130 ref<Expr> result = os->read(offset, type);
4131
4132 if (interpreterOpts.MakeConcreteSymbolic)
4133 result = replaceReadWithSymbolic(state, result);
4134
4135 bindLocal(target, state, result);
4136 }
4137
4138 return;
4139 }
4140 }
4141
4142 // we are on an error path (no resolution, multiple resolution, one
4143 // resolution with out of bounds)
4144
4145 address = optimizer.optimizeExpr(address, true);
4146 ResolutionList rl;
4147 solver->setTimeout(coreSolverTimeout);
4148 bool incomplete = state.addressSpace.resolve(state, solver, address, rl,
4149 0, coreSolverTimeout);
4150 solver->setTimeout(time::Span());
4151
4152 // XXX there is some query wasteage here. who cares?
4153 ExecutionState *unbound = &state;
4154
4155 for (ResolutionList::iterator i = rl.begin(), ie = rl.end(); i != ie; ++i) {
4156 const MemoryObject *mo = i->first;
4157 const ObjectState *os = i->second;
4158 ref<Expr> inBounds = mo->getBoundsCheckPointer(address, bytes);
4159
4160 StatePair branches = fork(*unbound, inBounds, true);
4161 ExecutionState *bound = branches.first;
4162
4163 // bound can be 0 on failure or overlapped
4164 if (bound) {
4165 if (isWrite) {
4166 if (os->readOnly) {
4167 terminateStateOnError(*bound, "memory error: object read only",
4168 ReadOnly);
4169 } else {
4170 ObjectState *wos = bound->addressSpace.getWriteable(mo, os);
4171 wos->write(mo->getOffsetExpr(address), value);
4172 }
4173 } else {
4174 ref<Expr> result = os->read(mo->getOffsetExpr(address), type);
4175 bindLocal(target, *bound, result);
4176 }
4177 }
4178
4179 unbound = branches.second;
4180 if (!unbound)
4181 break;
4182 }
4183
4184 // XXX should we distinguish out of bounds and overlapped cases?
4185 if (unbound) {
4186 if (incomplete) {
4187 terminateStateEarly(*unbound, "Query timed out (resolve).");
4188 } else {
4189 terminateStateOnError(*unbound, "memory error: out of bound pointer", Ptr,
4190 NULL, getAddressInfo(*unbound, address));
4191 }
4192 }
4193 }
4194
4195 void Executor::executeMakeSymbolic(ExecutionState &state,
4196 const MemoryObject *mo,
4197 const std::string &name) {
4198 // Create a new object state for the memory object (instead of a copy).
4199 if (!replayKTest) {
4200 // Find a unique name for this array. First try the original name,
4201 // or if that fails try adding a unique identifier.
4202 unsigned id = 0;
4203 std::string uniqueName = name;
4204 while (!state.arrayNames.insert(uniqueName).second) {
4205 uniqueName = name + "_" + llvm::utostr(++id);
4206 }
4207 const Array *array = arrayCache.CreateArray(uniqueName, mo->size);
4208 bindObjectInState(state, mo, false, array);
4209 state.addSymbolic(mo, array);
4210
4211 std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it =
4212 seedMap.find(&state);
4213 if (it!=seedMap.end()) { // In seed mode we need to add this as a
4214 // binding.
4215 for (std::vector<SeedInfo>::iterator siit = it->second.begin(),
4216 siie = it->second.end(); siit != siie; ++siit) {
4217 SeedInfo &si = *siit;
4218 KTestObject *obj = si.getNextInput(mo, NamedSeedMatching);
4219
4220 if (!obj) {
4221 if (ZeroSeedExtension) {
4222 std::vector<unsigned char> &values = si.assignment.bindings[array];
4223 values = std::vector<unsigned char>(mo->size, '\0');
4224 } else if (!AllowSeedExtension) {
4225 terminateStateOnError(state, "ran out of inputs during seeding",
4226 User);
4227 break;
4228 }
4229 } else {
4230 if (obj->numBytes != mo->size &&
4231 ((!(AllowSeedExtension || ZeroSeedExtension)
4232 && obj->numBytes < mo->size) ||
4233 (!AllowSeedTruncation && obj->numBytes > mo->size))) {
4234 std::stringstream msg;
4235 msg << "replace size mismatch: "
4236 << mo->name << "[" << mo->size << "]"
4237 << " vs " << obj->name << "[" << obj->numBytes << "]"
4238 << " in test\n";
4239
4240 terminateStateOnError(state, msg.str(), User);
4241 break;
4242 } else {
4243 std::vector<unsigned char> &values = si.assignment.bindings[array];
4244 values.insert(values.begin(), obj->bytes,
4245 obj->bytes + std::min(obj->numBytes, mo->size));
4246 if (ZeroSeedExtension) {
4247 for (unsigned i=obj->numBytes; i<mo->size; ++i)
4248 values.push_back('\0');
4249 }
4250 }
4251 }
4252 }
4253 }
4254 } else {
4255 ObjectState *os = bindObjectInState(state, mo, false);
4256 if (replayPosition >= replayKTest->numObjects) {
4257 terminateStateOnError(state, "replay count mismatch", User);
4258 } else {
4259 KTestObject *obj = &replayKTest->objects[replayPosition++];
4260 if (obj->numBytes != mo->size) {
4261 terminateStateOnError(state, "replay size mismatch", User);
4262 } else {
4263 for (unsigned i=0; i<mo->size; i++)
4264 os->write8(i, obj->bytes[i]);
4265 }
4266 }
4267 }
4268 }
4269
4270 /***/
4271
4272 void Executor::runFunctionAsMain(Function *f,
4273 int argc,
4274 char **argv,
4275 char **envp) {
4276 std::vector<ref<Expr> > arguments;
4277
4278 // force deterministic initialization of memory objects
4279 srand(1);
4280 srandom(1);
4281
4282 MemoryObject *argvMO = 0;
4283
4284 // In order to make uclibc happy and be closer to what the system is
4285 // doing we lay out the environments at the end of the argv array
4286 // (both are terminated by a null). There is also a final terminating
4287 // null that uclibc seems to expect, possibly the ELF header?
4288
4289 int envc;
4290 for (envc=0; envp[envc]; ++envc) ;
4291
4292 unsigned NumPtrBytes = Context::get().getPointerWidth() / 8;
4293 KFunction *kf = kmodule->functionMap[f];
4294 assert(kf);
4295 Function::arg_iterator ai = f->arg_begin(), ae = f->arg_end();
4296 if (ai!=ae) {
4297 arguments.push_back(ConstantExpr::alloc(argc, Expr::Int32));
4298 if (++ai!=ae) {
4299 Instruction *first = &*(f->begin()->begin());
4300 argvMO =
4301 memory->allocate((argc + 1 + envc + 1 + 1) * NumPtrBytes,
4302 /*isLocal=*/false, /*isGlobal=*/true,
4303 /*allocSite=*/first, /*alignment=*/8);
4304
4305 if (!argvMO)
4306 klee_error("Could not allocate memory for function arguments");
4307
4308 arguments.push_back(argvMO->getBaseExpr());
4309
4310 if (++ai!=ae) {
4311 uint64_t envp_start = argvMO->address + (argc+1)*NumPtrBytes;
4312 arguments.push_back(Expr::createPointer(envp_start));
4313
4314 if (++ai!=ae)
4315 klee_error("invalid main function (expect 0-3 arguments)");
4316 }
4317 }
4318 }
4319
4320 ExecutionState *state = new ExecutionState(kmodule->functionMap[f]);
4321
4322 if (pathWriter)
4323 state->pathOS = pathWriter->open();
4324 if (symPathWriter)
4325 state->symPathOS = symPathWriter->open();
4326
4327
4328 if (statsTracker)
4329 statsTracker->framePushed(*state, 0);
4330
4331 assert(arguments.size() == f->arg_size() && "wrong number of arguments");
4332 for (unsigned i = 0, e = f->arg_size(); i != e; ++i)
4333 bindArgument(kf, i, *state, arguments[i]);
4334
4335 if (argvMO) {
4336 ObjectState *argvOS = bindObjectInState(*state, argvMO, false);
4337
4338 for (int i=0; i<argc+1+envc+1+1; i++) {
4339 if (i==argc || i>=argc+1+envc) {
4340 // Write NULL pointer
4341 argvOS->write(i * NumPtrBytes, Expr::createPointer(0));
4342 } else {
4343 char *s = i<argc ? argv[i] : envp[i-(argc+1)];
4344 int j, len = strlen(s);
4345
4346 MemoryObject *arg =
4347 memory->allocate(len + 1, /*isLocal=*/false, /*isGlobal=*/true,
4348 /*allocSite=*/state->pc->inst, /*alignment=*/8);
4349 if (!arg)
4350 klee_error("Could not allocate memory for function arguments");
4351 ObjectState *os = bindObjectInState(*state, arg, false);
4352 for (j=0; j<len+1; j++)
4353 os->write8(j, s[j]);
4354
4355 // Write pointer to newly allocated and initialised argv/envp c-string
4356 argvOS->write(i * NumPtrBytes, arg->getBaseExpr());
4357 }
4358 }
4359 }
4360
4361 initializeGlobals(*state);
4362
4363 processTree = std::make_unique<PTree>(state);
4364 run(*state);
4365 processTree = nullptr;
4366
4367 // hack to clear memory objects
4368 delete memory;
4369 memory = new MemoryManager(NULL);
4370
4371 globalObjects.clear();
4372 globalAddresses.clear();
4373
4374 if (statsTracker)
4375 statsTracker->done();
4376 }
4377
4378 unsigned Executor::getPathStreamID(const ExecutionState &state) {
4379 assert(pathWriter);
4380 return state.pathOS.getID();
4381 }
4382
4383 unsigned Executor::getSymbolicPathStreamID(const ExecutionState &state) {
4384 assert(symPathWriter);
4385 return state.symPathOS.getID();
4386 }
4387
4388 void Executor::getConstraintLog(const ExecutionState &state, std::string &res,
4389 Interpreter::LogType logFormat) {
4390
4391 switch (logFormat) {
4392 case STP: {
4393 Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
4394 char *log = solver->getConstraintLog(query);
4395 res = std::string(log);
4396 free(log);
4397 } break;
4398
4399 case KQUERY: {
4400 std::string Str;
4401 llvm::raw_string_ostream info(Str);
4402 ExprPPrinter::printConstraints(info, state.constraints);
4403 res = info.str();
4404 } break;
4405
4406 case SMTLIB2: {
4407 std::string Str;
4408 llvm::raw_string_ostream info(Str);
4409 ExprSMTLIBPrinter printer;
4410 printer.setOutput(info);
4411 Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
4412 printer.setQuery(query);
4413 printer.generateOutput();
4414 res = info.str();
4415 } break;
4416
4417 default:
4418 klee_warning("Executor::getConstraintLog() : Log format not supported!");
4419 }
4420 }
4421
4422 bool Executor::getSymbolicSolution(const ExecutionState &state,
4423 std::vector<
4424 std::pair<std::string,
4425 std::vector<unsigned char> > >
4426 &res) {
4427 solver->setTimeout(coreSolverTimeout);
4428
4429 ConstraintSet extendedConstraints(state.constraints);
4430 ConstraintManager cm(extendedConstraints);
4431
4432 // Go through each byte in every test case and attempt to restrict
4433 // it to the constraints contained in cexPreferences. (Note:
4434 // usually this means trying to make it an ASCII character (0-127)
4435 // and therefore human readable. It is also possible to customize
4436 // the preferred constraints. See test/Features/PreferCex.c for
4437 // an example) While this process can be very expensive, it can
4438 // also make understanding individual test cases much easier.
4439 for (unsigned i = 0; i != state.symbolics.size(); ++i) {
4440 const auto &mo = state.symbolics[i].first;
4441 std::vector< ref<Expr> >::const_iterator pi =
4442 mo->cexPreferences.begin(), pie = mo->cexPreferences.end();
4443 for (; pi != pie; ++pi) {
4444 bool mustBeTrue;
4445 // Attempt to bound byte to constraints held in cexPreferences
4446 bool success =
4447 solver->mustBeTrue(extendedConstraints, Expr::createIsZero(*pi),
4448 mustBeTrue, state.queryMetaData);
4449 // If it isn't possible to constrain this particular byte in the desired
4450 // way (normally this would mean that the byte can't be constrained to
4451 // be between 0 and 127 without making the entire constraint list UNSAT)
4452 // then just continue on to the next byte.
4453 if (!success) break;
4454 // If the particular constraint operated on in this iteration through
4455 // the loop isn't implied then add it to the list of constraints.
4456 if (!mustBeTrue)
4457 cm.addConstraint(*pi);
4458 }
4459 if (pi!=pie) break;
4460 }
4461
4462 std::vector< std::vector<unsigned char> > values;
4463 std::vector<const Array*> objects;
4464 for (unsigned i = 0; i != state.symbolics.size(); ++i)
4465 objects.push_back(state.symbolics[i].second);
4466 bool success = solver->getInitialValues(extendedConstraints, objects, values,
4467 state.queryMetaData);
4468 solver->setTimeout(time::Span());
4469 if (!success) {
4470 klee_warning("unable to compute initial values (invalid constraints?)!");
4471 ExprPPrinter::printQuery(llvm::errs(), state.constraints,
4472 ConstantExpr::alloc(0, Expr::Bool));
4473 return false;
4474 }
4475
4476 for (unsigned i = 0; i != state.symbolics.size(); ++i)
4477 res.push_back(std::make_pair(state.symbolics[i].first->name, values[i]));
4478 return true;
4479 }
4480
4481 void Executor::getCoveredLines(const ExecutionState &state,
4482 std::map<const std::string*, std::set<unsigned> > &res) {
4483 res = state.coveredLines;
4484 }
4485
4486 void Executor::doImpliedValueConcretization(ExecutionState &state,
4487 ref<Expr> e,
4488 ref<ConstantExpr> value) {
4489 abort(); // FIXME: Broken until we sort out how to do the write back.
4490
4491 if (DebugCheckForImpliedValues)
4492 ImpliedValue::checkForImpliedValues(solver->solver.get(), e, value);
4493
4494 ImpliedValueList results;
4495 ImpliedValue::getImpliedValues(e, value, results);
4496 for (ImpliedValueList::iterator it = results.begin(), ie = results.end();
4497 it != ie; ++it) {
4498 ReadExpr *re = it->first.get();
4499
4500 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
4501 // FIXME: This is the sole remaining usage of the Array object
4502 // variable. Kill me.
4503 const MemoryObject *mo = 0; //re->updates.root->object;
4504 const ObjectState *os = state.addressSpace.findObject(mo);
4505
4506 if (!os) {
4507 // object has been free'd, no need to concretize (although as
4508 // in other cases we would like to concretize the outstanding
4509 // reads, but we have no facility for that yet)
4510 } else {
4511 assert(!os->readOnly &&
4512 "not possible? read only object with static read?");
4513 ObjectState *wos = state.addressSpace.getWriteable(mo, os);
4514 wos->write(CE, it->second);
4515 }
4516 }
4517 }
4518 }
4519
4520 Expr::Width Executor::getWidthForLLVMType(llvm::Type *type) const {
4521 return kmodule->targetData->getTypeSizeInBits(type);
4522 }
4523
4524 size_t Executor::getAllocationAlignment(const llvm::Value *allocSite) const {
4525 // FIXME: 8 was the previous default. We shouldn't hard code this
4526 // and should fetch the default from elsewhere.
4527 const size_t forcedAlignment = 8;
4528 size_t alignment = 0;
4529 llvm::Type *type = NULL;
4530 std::string allocationSiteName(allocSite->getName().str());
4531 if (const GlobalObject *GO = dyn_cast<GlobalObject>(allocSite)) {
4532 alignment = GO->getAlignment();
4533 if (const GlobalVariable *globalVar = dyn_cast<GlobalVariable>(GO)) {
4534 // All GlobalVariables's have pointer type
4535 llvm::PointerType *ptrType =
4536 dyn_cast<llvm::PointerType>(globalVar->getType());
4537 assert(ptrType && "globalVar's type is not a pointer");
4538 type = ptrType->getElementType();
4539 } else {
4540 type = GO->getType();
4541 }
4542 } else if (const AllocaInst *AI = dyn_cast<AllocaInst>(allocSite)) {
4543 alignment = AI->getAlignment();
4544 type = AI->getAllocatedType();
4545 } else if (isa<InvokeInst>(allocSite) || isa<CallInst>(allocSite)) {
4546 // FIXME: Model the semantics of the call to use the right alignment
4547 #if LLVM_VERSION_CODE >= LLVM_VERSION(8, 0)
4548 const CallBase &cs = cast<CallBase>(*allocSite);
4549 #else
4550 llvm::Value *allocSiteNonConst = const_cast<llvm::Value *>(allocSite);
4551 const CallSite cs(isa<InvokeInst>(allocSiteNonConst)
4552 ? CallSite(cast<InvokeInst>(allocSiteNonConst))
4553 : CallSite(cast<CallInst>(allocSiteNonConst)));
4554 #endif
4555 llvm::Function *fn =
4556 klee::getDirectCallTarget(cs, /*moduleIsFullyLinked=*/true);
4557 if (fn)
4558 allocationSiteName = fn->getName().str();
4559
4560 klee_warning_once(fn != NULL ? fn : allocSite,
4561 "Alignment of memory from call \"%s\" is not "
4562 "modelled. Using alignment of %zu.",
4563 allocationSiteName.c_str(), forcedAlignment);
4564 alignment = forcedAlignment;
4565 } else {
4566 llvm_unreachable("Unhandled allocation site");
4567 }
4568
4569 if (alignment == 0) {
4570 assert(type != NULL);
4571 // No specified alignment. Get the alignment for the type.
4572 if (type->isSized()) {
4573 alignment = kmodule->targetData->getPrefTypeAlignment(type);
4574 } else {
4575 klee_warning_once(allocSite, "Cannot determine memory alignment for "
4576 "\"%s\". Using alignment of %zu.",
4577 allocationSiteName.c_str(), forcedAlignment);
4578 alignment = forcedAlignment;
4579 }
4580 }
4581
4582 // Currently we require alignment be a power of 2
4583 if (!bits64::isPowerOfTwo(alignment)) {
4584 klee_warning_once(allocSite, "Alignment of %zu requested for %s but this "
4585 "not supported. Using alignment of %zu",
4586 alignment, allocSite->getName().str().c_str(),
4587 forcedAlignment);
4588 alignment = forcedAlignment;
4589 }
4590 assert(bits64::isPowerOfTwo(alignment) &&
4591 "Returned alignment must be a power of two");
4592 return alignment;
4593 }
4594
4595 void Executor::prepareForEarlyExit() {
4596 if (statsTracker) {
4597 // Make sure stats get flushed out
4598 statsTracker->done();
4599 }
4600 }
4601
4602 /// Returns the errno location in memory
4603 int *Executor::getErrnoLocation(const ExecutionState &state) const {
4604 #if !defined(__APPLE__) && !defined(__FreeBSD__) && !defined(__DragonFly__)
4605 /* From /usr/include/errno.h: it [errno] is a per-thread variable. */
4606 return __errno_location();
4607 #else
4608 return __error();
4609 #endif
4610 }
4611
4612
4613 void Executor::dumpPTree() {
4614 if (!::dumpPTree) return;
4615
4616 char name[32];
4617 snprintf(name, sizeof(name),"ptree%08d.dot", (int) stats::instructions);
4618 auto os = interpreterHandler->openOutputFile(name);
4619 if (os) {
4620 processTree->dump(*os);
4621 }
4622
4623 ::dumpPTree = 0;
4624 }
4625
4626 void Executor::dumpStates() {
4627 if (!::dumpStates) return;
4628
4629 auto os = interpreterHandler->openOutputFile("states.txt");
4630
4631 if (os) {
4632 for (ExecutionState *es : states) {
4633 *os << "(" << es << ",";
4634 *os << "[";
4635 auto next = es->stack.begin();
4636 ++next;
4637 for (auto sfIt = es->stack.begin(), sf_ie = es->stack.end();
4638 sfIt != sf_ie; ++sfIt) {
4639 *os << "('" << sfIt->kf->function->getName().str() << "',";
4640 if (next == es->stack.end()) {
4641 *os << es->prevPC->info->line << "), ";
4642 } else {
4643 *os << next->caller->info->line << "), ";
4644 ++next;
4645 }
4646 }
4647 *os << "], ";
4648
4649 StackFrame &sf = es->stack.back();
4650 uint64_t md2u = computeMinDistToUncovered(es->pc,
4651 sf.minDistToUncoveredOnReturn);
4652 uint64_t icnt = theStatisticManager->getIndexedValue(stats::instructions,
4653 es->pc->info->id);
4654 uint64_t cpicnt = sf.callPathNode->statistics.getValue(stats::instructions);
4655
4656 *os << "{";
4657 *os << "'depth' : " << es->depth << ", ";
4658 *os << "'queryCost' : " << es->queryMetaData.queryCost << ", ";
4659 *os << "'coveredNew' : " << es->coveredNew << ", ";
4660 *os << "'instsSinceCovNew' : " << es->instsSinceCovNew << ", ";
4661 *os << "'md2u' : " << md2u << ", ";
4662 *os << "'icnt' : " << icnt << ", ";
4663 *os << "'CPicnt' : " << cpicnt << ", ";
4664 *os << "}";
4665 *os << ")\n";
4666 }
4667 }
4668
4669 ::dumpStates = 0;
4670 }
4671
4672 ///
4673
4674 Interpreter *Interpreter::create(LLVMContext &ctx, const InterpreterOptions &opts,
4675 InterpreterHandler *ih) {
4676 return new Executor(ctx, opts, ih);
4677 }
4678