about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
2012-10-24Patch by Dan Liew: "Added SMTLIBLoggingSolver for logging queries in ↵Cristian Cadar
SMT-LIBv2 format." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166564 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Nice patch by Dan Liew that adds support for printing queries in theCristian Cadar
SMTLIB format (part of his MSc project work). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166556 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew: "Moved PrintContext class out of ExprPrinter.cpp soCristian Cadar
it can be used by other classes. It has also been improved so it can be used with the soon to be added ExprSMTLIBPrinter classes." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166555 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew: " Modified ConstantExpr::toString() to take anCristian Cadar
optional radix (base e.g. 2,10,16). This will be needed by the ExprSMTLIBPrinter that will soon be added." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166553 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-18Nice patch by Hristina Palikareva that removes the dependency on STPCristian Cadar
arrays from the Array and UpdateNode classes. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166214 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-08Fix to previous patch, which would not compile with LLVM 2.9.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@165413 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-08Make the changes in r165394 be conditional on post LLVM 3.1 changes.Micah Villmow
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@165405 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-08Move TargetData to DataLayout.Micah Villmow
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@165394 91177308-0d34-0410-b5e6-96231b3b80d8
2012-09-12Restructured the command-line options for setting the searchCristian Cadar
heuristics in KLEE. The new options are documented at http://klee.llvm.org/klee-options.html. Cleaned a bit the code in UserSearcher.cpp, and fixed some test cases to use the new options. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@163711 91177308-0d34-0410-b5e6-96231b3b80d8
2012-09-11Changed the default to --max-memory and documented randomize-fork.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@163632 91177308-0d34-0410-b5e6-96231b3b80d8
2012-07-31Patch by Dan Liew that removes our internal copy of STP, and makes the ↵Cristian Cadar
--with-stp option mandatory: "1. At configure time the --with-stp= option is now mandatory. 2. The HAVE_EXT_STP macro has been removed. 3. The ENABLE_EXT_STP autoconf replacement variable has been removed and consequently the Makefile variable of the same name has been removed." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161055 91177308-0d34-0410-b5e6-96231b3b80d8
2012-07-26Forgot a cl::desc in the previous patch...Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@160781 91177308-0d34-0410-b5e6-96231b3b80d8
2012-07-26Documented several KLEE options.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@160779 91177308-0d34-0410-b5e6-96231b3b80d8
2012-07-20Fixed bug FPToSI bug reported by Peng Li. Added a simple test case. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@160547 91177308-0d34-0410-b5e6-96231b3b80d8
2012-06-01Patch by Oscar Dustmann fixing a buffer overflow when long names areCristian Cadar
used: "patch for STPBuilder.cpp that allows for arbitrary length symbol names while still limiting the unique string to 32 bytes." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@157820 91177308-0d34-0410-b5e6-96231b3b80d8
2012-05-25Patch by Paul Marinescu that makes KLEE gracefully fail on assembly code.Cristian Cadar
Includes test case. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@157463 91177308-0d34-0410-b5e6-96231b3b80d8
2012-04-10Lowering support for the llvm.uadd.with.overflow intrinsic.Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154367 91177308-0d34-0410-b5e6-96231b3b80d8
2012-04-08Fixed --max-stp-time, which wasn't working unless --use-forked-stp wasCristian Cadar
also used. Thanks to Paul Marinescu for reporting and debugging this. The patch also disables the STP timeout by default. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154300 91177308-0d34-0410-b5e6-96231b3b80d8
2012-04-07Fix compilation with LLVM trunk.Peter Collingbourne
Patch by arrowdodger! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154238 91177308-0d34-0410-b5e6-96231b3b80d8
2012-04-07Catch up with hashing changes.Peter Collingbourne
Patch by arrowdodger! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154237 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-26STPBuilder: fix getShiftBits properly.Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@153475 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-26STPBuilder: fix bv{Zero,One,MinusOne} for the case where width>64Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@153474 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-26STPBuilder: fix ConstantExpr builder for the case where width>64 butPeter Collingbourne
is not a multiple of 64. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@153473 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-13Compatability fix for previous revision. By my mistake one string went out ↵Stepan Dyatkovskiy
of #if scobes. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@152625 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-11llvm::SwitchInstStepan Dyatkovskiy
Renamed methods caseBegin, caseEnd and caseDefault with case_begin, case_end, and case_default. Added some notes relative to case iterators. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@152534 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-08Taken into account Duncan's comments for r149481 dated by 2nd Feb 2012:Stepan Dyatkovskiy
http://lists.cs.uiuc.edu/pipermail/llvm-commits/Week-of-Mon-20120130/136146.html Implemented CaseIterator and it solves almost all described issues: we don't need to mix operand/case/successor indexing anymore. Base iterator class is implemented as a template since it may be initialized either from "const SwitchInst*" or from "SwitchInst*". ConstCaseIt is just a read-only iterator. CaseIt is read-write iterator; it allows to change case successor and case value. Usage of iterator allows totally remove resolveXXXX methods. All indexing convertions done automatically inside the iterator's getters. Main way of iterator usage looks like this: SwitchInst *SI = ... // intialize it somehow for (SwitchInst::CaseIt i = SI->caseBegin(), e = SI->caseEnd(); i != e; ++i) { BasicBlock *BB = i.getCaseSuccessor(); ConstantInt *V = i.getCaseValue(); // Do something. } If you want to convert case number to TerminatorInst successor index, just use getSuccessorIndex iterator's method. If you want initialize iterator from TerminatorInst successor index, use CaseIt::fromSuccessorIndex(...) method. There are also related changes in llvm-clients: klee and clang. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@152299 91177308-0d34-0410-b5e6-96231b3b80d8
2012-02-12Teach KLEE how to handle new ConstantDataSequential type.Peter Collingbourne
Patch by arrowdodger! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@150355 91177308-0d34-0410-b5e6-96231b3b80d8
2012-02-12Update for LLVM changes - there is no more "unwind" instruction.Peter Collingbourne
Patch by arrowdodger! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@150354 91177308-0d34-0410-b5e6-96231b3b80d8
2012-02-01Second compatability fix for SwitchInst refactoring (added compatability ↵Stepan Dyatkovskiy
with llvm versions < 3.1). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@149528 91177308-0d34-0410-b5e6-96231b3b80d8
2012-02-01Compatability fix for SwitchInst refactoring.Stepan Dyatkovskiy
The purpose of refactoring is to hide operand roles from SwitchInst user (programmer). If you want to play with operands directly, probably you will need lower level methods than SwitchInst ones (TerminatorInst or may be User). After this patch we can reorganize SwitchInst operands and successors as we want. What was done: 1. Changed semantics of index inside the getCaseValue method: getCaseValue(0) means "get first case", not a condition. Use getCondition() if you want to resolve the condition. I propose don't mix SwitchInst case indexing with low level indexing (TI successors indexing, User's operands indexing), since it may be dangerous. 2. By the same reason findCaseValue(ConstantInt*) returns actual number of case value. 0 means first case, not default. If there is no case with given value, ErrorIndex will returned. 3. Added getCaseSuccessor method. I propose to avoid usage of TerminatorInst::getSuccessor if you want to resolve case successor BB. Use getCaseSuccessor instead, since internal SwitchInst organization of operands/successors is hidden and may be changed in any moment. 4. Added resolveSuccessorIndex and resolveCaseIndex. The main purpose of these methods is to see how case successors are really mapped in TerminatorInst. 4.1 "resolveSuccessorIndex" was created if you need to level down from SwitchInst to TerminatorInst. It returns TerminatorInst's successor index for given case successor. 4.2 "resolveCaseIndex" converts low level successors index to case index that curresponds to the given successor. Note: There are also related compatability fix patches for dragonegg, klee, llvm-gcc-4.0, llvm-gcc-4.2, safecode, clang. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@149484 91177308-0d34-0410-b5e6-96231b3b80d8
2012-01-18Nice patch by Gang Hu, Heming Cui and Junfeng Yang fixing a memoryCristian Cadar
leak in KLEE. From Gang Hu: "The memory leak is caused by two reasons. First, the MemoryObject objects are not freed, until the MemoryManager is destroyed. Second, when KLEE allocates a non-fixed MemoryObject object, KLEE also allocates a block of memory which is the same as the object's size. This block of memory is never freed. So, this patch generally does reference counting on the MemoryObject objects, and frees them as soon as the reference count drops to zero." Many thanks to Paul Marinescu as well, who tested this patch thoroughly on the Coreutils benchmarks. On 1h runs, the memory consumption typically goes down by 1-5%, but some applications which see more significant gains. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@148402 91177308-0d34-0410-b5e6-96231b3b80d8
2011-12-13Fix STPBuilder::getShiftBits for non-power-of-2 bitwidths up to 64.Peter Collingbourne
(Yes, we should really be handling more bitwidths here.) git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@146510 91177308-0d34-0410-b5e6-96231b3b80d8
2011-12-11Patch by Ben Gras fixing a few minor issues: adds missing includes,Cristian Cadar
fixes the ntohs prototype in klee-libc, and removes some unused code. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@146352 91177308-0d34-0410-b5e6-96231b3b80d8
2011-12-11Patch by Paul Marinescu that fixes an issue causing KLEE to fail on some ↵Cristian Cadar
platforms with KLEE: ERROR: unable to load symbol(__dso_handle) while initializing globals. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@146351 91177308-0d34-0410-b5e6-96231b3b80d8
2011-12-08Update for changes in LLVM trunk. Original patch by arrowdodger!Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@146178 91177308-0d34-0410-b5e6-96231b3b80d8
2011-11-29Updates for LLVM 3.1.Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@145365 91177308-0d34-0410-b5e6-96231b3b80d8
2011-11-04Patch by Tom Bergan that fixes multi-byte reads on big-endian architectures.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@143693 91177308-0d34-0410-b5e6-96231b3b80d8
2011-10-17Fix some -Wunused-variable warnings.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@142310 91177308-0d34-0410-b5e6-96231b3b80d8
2011-09-02Applied patch from David Ramos that fixes a bug in minDistToUncoveredCristian Cadar
calculation: "Functions with a single instruction were erroneously treated as never returning. This propagated far, making many instructions unreachable according to this metric." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@139045 91177308-0d34-0410-b5e6-96231b3b80d8
2011-09-02Update location of TargetSelect.h and TargetRegistry.h for LLVM 3.0+Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@139026 91177308-0d34-0410-b5e6-96231b3b80d8
2011-08-09Disable the LowerSetJmpPass on LLVM 3.0+Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@137116 91177308-0d34-0410-b5e6-96231b3b80d8
2011-08-01Make the Executor capable of handling bitcasts of aliases, by rewriting thePeter Collingbourne
direct function call logic. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136605 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-29Sign extend, rather than zero extend, narrow gep indicesPeter Collingbourne
For example, clang creates these for ++ and -- operations on pointers on 64-bit platforms. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136474 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-24Applied patch by Leandro Sales that makes Kleaver compatible with theCristian Cadar
recent changes to array names. Modified FastCexSolver.pc to catch this issue. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135896 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-20Updates for LLVM 3.0. Based on changes by arrowdodger, thanks!Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135598 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-20Deprecate LLVM_VERSION_MAJOR and LLVM_VERSION_MINOR in favour ofPeter Collingbourne
version codes. This makes the preprocessor-based version tests more concise and less error prone. Also, fix the version tests in lib/Expr/Parser.cpp (immutable zext and trunc were introduced in LLVM 2.9); now 2.9 passes "make test". git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135583 91177308-0d34-0410-b5e6-96231b3b80d8
2011-06-23When extracting path from debug info, use file name on its own if it begins ↵Peter Collingbourne
with '/' Clang has been observed to use an absolute path in the 'filename' field. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@133740 91177308-0d34-0410-b5e6-96231b3b80d8
2011-06-09Patch from Martin Nowack for LLVM 2.9Cristian Cadar
(http://llvm.org/bugs/show_bug.cgi?id=9595) git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@132787 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-25Name symbolic arrays using the 3rd argument to klee_make_symbolic,Peter Collingbourne
and make sure the name is unique. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@132054 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-18Add ConstantStruct support to Executor::evalConstantPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131586 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-12-14 14:59:40 +0000