about summary refs log tree commit diff homepage
path: root/lib/Expr
AgeCommit message (Collapse)Author
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-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
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-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-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-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-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-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-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
2010-07-15Fix a -Wbool-conversion warning.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108404 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Fix some const cast warnings.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102867 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-05Add long double support, patch by David Ramos.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100421 91177308-0d34-0410-b5e6-96231b3b80d8
2009-09-05Applied patch submitted by Pongsin Poosankam that fixes a bug in theCristian Cadar
parser. Fixed bug in the parses. Patch reported by git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@81056 91177308-0d34-0410-b5e6-96231b3b80d8
2009-09-01Update for LLVM ostream changes.Daniel Dunbar
- Includes patch by Michael Stone! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@80665 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-01Add Expr::dumpDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77802 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-28Move Machine constants into Context object, initialized based on the targetDaniel Dunbar
data. - This is the first step towards having KLEE be fully target independent, its not particularly beautiful but its expedient. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77306 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-11Removed the Nz macro.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75377 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Updated the Not operation for constants. Added extra test case for this.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75282 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Added support for bitwise not. Replacing "false == " with Not inCristian Cadar
the canonical form. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75239 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Replaced createNot() by createIsZero() and "Not" macro by "Nz". Cristian Cadar
Not will become bitwise not. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75224 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-27Start move to using APFloat (support long double).Daniel Dunbar
- Incomplete, still have to move some conversion operations. - Also, there isn't support yet for copying long double values to native memory. - Still, should be a monotonic improvement and we are no longer faking long double support. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74363 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-26More large integer support.Daniel Dunbar
- Allow constructing a ConstantExpr from an APInt, too painful otherwise. - Parser support for large integers. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74278 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25Kill off last getConstantValue uses.Daniel Dunbar
- ConstantExpr should now fully support arbitrary width operations. - Still numerous holes in parsing, solver, etc. to plug. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74151 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25Remove some more uses of getConstantValue.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74149 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25Switch to using APInt math operations.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74148 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-22Remove unnecessary width field, the width is part of the APInt.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73872 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-22Store ConstantExpr's value as an APInt.Daniel Dunbar
- In anticipation of supporting large constant values. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73871 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-22Add ConstantExpr::toString (instead of using getConstantValue()).Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73870 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16Add basic constant folding / simplification for Eq.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73467 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16Add (very) basic constant folding for And,Or,Xor.Daniel Dunbar
- Lots more important goodness can be done here. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73461 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16Add (very) basic constant folding for Mul.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73460 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16Start SimplifyingExprBuilderDaniel Dunbar
- Normalize Ne, Ugt, Uge, Slt, Sge git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73458 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-15Support partial folding for Sub in new constant folding builder.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73377 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-15Support partial folding for Add in new constant folding builder.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73363 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Rename FoldingExprBuilder -> SimplifyingExprBuilderDaniel Dunbar
Also, start printing query # with -print-ast (for testing purposes). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73350 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Kill off ExtractExpr::createByteOff.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73348 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14The expansion for Read{MSB,LSB} needs to continue to use the folding methods,Daniel Dunbar
otherwise we build expressions that won't be matched later when we print them. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73347 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Use ExprBuilder for constructing expressions in the Parser.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73345 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Remove the (A < constant) => (A == 0 || A == 1 ... || A == constant - 1)Daniel Dunbar
optimization, its not the kind of thing we should always be performing. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73340 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Add ExprBuilder base class, and start of implementations.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73339 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14More ConstantExpr cleanup.Daniel Dunbar
- Change Executor::evalConstant to return ConstantExpr. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73337 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Add ConstantExpr::{getLimitedValue,getZExtValue}.Daniel Dunbar
- For use in situations where the range of the constant is known to fit in a uint64 (or smaller), or the extra bits don't matter. - No (intended) functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73326 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Rewrite ImpliedValue to use ConstantExpr operations.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73325 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Add several ConstantExpr utility functions and move clients over.Daniel Dunbar
- Reducing uses of getConstantValue() so we can move to arbitrary precision constants. - No (intended) functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73324 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Add constant folding operations to ConstantExpr.Daniel Dunbar
- No (intended) functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73322 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-13Reverted last change that added createIff. Since we only handleCristian Cadar
bitvectors, we can just use Eq. The parser can distinguish between boolean formulas and bitvector terms. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73309 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-13Added a helper function to construct IFF expressions.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73283 91177308-0d34-0410-b5e6-96231b3b80d8