about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
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-25Patch from Ben Gras which "makes Klee look for the libraries in theCristian Cadar
install location instead of the compile-tree location if a compile-time macro is enabled." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@148961 91177308-0d34-0410-b5e6-96231b3b80d8
2012-01-18Updated uclibc archives to work with current installation instructions.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@148405 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-16Fixed help message in klee-stats.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@146741 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 for MINIX: no stat64 under MINIX.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@146353 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-11This is a workaround for the infinite loop reported at Cristian Cadar
http://keeda.stanford.edu/pipermail/klee-dev/2011-August/000723.html KLEE needs to use --fno-builtin when compiling its version of memset. However, this patch also adds the workaround suggested by Paul in the thread above, since support for --fno-builtin was added to llvm-gcc only after LLVM 2.9 was released. More details about this issue can be found here: http://lists.cs.uiuc.edu/pipermail/llvm-commits/Week-of-Mon-20110411/119376.html http://lists.cs.uiuc.edu/pipermail/llvm-commits/Week-of-Mon-20110711/124131.html Thanks to Paul and arrowdodger for their explanations and patches. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@146350 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-10Added new publication from Columbia.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@144295 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-27Changed Tutorial 1, which was causing confusion due to differences inCristian Cadar
LLVM code generation before and after LLVM 2.8. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@140602 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-22Added new publication from RWTH Aachen.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@138232 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-28Added two publications from EPFL, fixed a typo. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136350 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-26Added a link to the searchable archive created by David R.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136104 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-24Added the CAV 2011 paper from Stanford.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135895 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-24Improved installation instructions a bit, and changed theCristian Cadar
"officially supported" version of LLVM from 2.7 to 2.8. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135894 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-21Add our EuroSys paper to the publications listPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135677 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-06-09Patch from arrowdodger for fixing FreeBSD build..Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@132786 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-26Added instructions from Philip Guo about trying out KLEE via CDE. Cristian Cadar
Added a menu on the Getting Started webpage. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@132142 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
2011-05-18Maintain an equivalence set during comparison operationsPeter Collingbourne
This results in a significant speedup of certain comparisons involving large partially shared expression trees. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131585 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-18Use local Makefile.rulesPeter Collingbourne
This patch changes the build system to use its own copy of Makefile.rules (taken from a recent svn snapshot). Also added a --with-llvm-build-mode flag and changed the default runtime library configuration to Release+Asserts. Makefile.rules was modified to support --with-llvm-build-mode and older versions of LLVM (tested 2.7 and 2.8). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131584 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-18Support for arbitrary sized types in ConstantExpr::fromMemoryPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131583 91177308-0d34-0410-b5e6-96231b3b80d8
2011-04-23Fixed bug reported by Li Xuan Ji and Ayrat Khalimov.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@130070 91177308-0d34-0410-b5e6-96231b3b80d8
2011-04-23Transformed the assert() checking for overlapping objects into a callCristian Cadar
to klee_error() to make sure the check is done even when assertions are disabled. This makes the AsmAddresses test pass with assertions disabled. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@130067 91177308-0d34-0410-b5e6-96231b3b80d8
2011-04-23Patch by arrowdodger ↵Cristian Cadar
(http://keeda.stanford.edu/pipermail/klee-dev/2011-April/000617.html) for compiling KLEE with the latest LLVM changes. Tested against LLVM 2.7 and 2.8. The AsmAddresses test fails in 2.8 unless assertions are explicitely enabled (--enable-assertions). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@130065 91177308-0d34-0410-b5e6-96231b3b80d8
2011-04-22Add a note about the git mirrorPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@129989 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-27 23:16:16 +0000