about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
2009-06-25Recognizing more SMTLIB expressions (bitwise, etc.). Some of themCristian Cadar
still need to actually be constructed. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74169 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25Added support for flets.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74167 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25Simplified grammar by properly factoring out the rule for optional annotations.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74165 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-25Flesh out support for arbitrary bit widths in some key places (STP & constantDaniel Dunbar
creation). - Not used yet. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74142 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-24Update for LLVM API change.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74075 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-24Added support for LET expressions. Added simple environment supportCristian Cadar
to SMTParser. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74055 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-22Update for changes in how JIT is linked in.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73868 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16Improve FastCexSolver: Daniel Dunbar
- Bug fix, unbreak Concat propogation (recent regression). - Also, add some simple propogation for Add. - These two knock off another 50% of the queries hitting STP from the first 30s of 'dd'. - Also, add some debugging code. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73488 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-16Added support for comparison and arithmetic expressions.Cristian Cadar
We need to add support for smod to Kleaver. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73459 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-16Added bitvector function/predicate names to the lexer.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73455 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16Added support for logical formulas in the SMTLIB parser.Cristian Cadar
Started to work on parsing bitvector terms. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73453 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-14Fail with an exec error on large (> 64-bit) floating point ops.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73330 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Remove some unused functionality.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73329 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14More ConstantExpr tweaks.Daniel Dunbar
- We can safely assume for now that array indices are within 32-bits (we will enforce this even on 64-bit targets). - We can also safely assume that address fit in 64-bits. - Always look up function pointers using 64-bits. - Protect a few other places by explicit checks that the type is <= 64-bits, when we can fallback to a safe path. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73328 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Change AddressSpace::resolveOne to take a ConstantExpr directly (and to allowDaniel Dunbar
64-bit addresses). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73327 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-13Switch to using constant arrays for non-symbolic objects.Daniel Dunbar
- Currently uses a dumb implementation which keeps the old flushing architecture, but converts to a constant array when the first ReadExpr is created. - Temporary --use-constant-arrays switch can be used to disable for testing. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73313 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-13Create new ObjectState constructor for explicitly creating symbolic objects.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73308 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-13Fix for the issue reported and diagnosed by Seungbeom, where KLEE wasCristian Cadar
skipping forks without reporting it. Added a warning the first time a fork is skipped for each of four different reasons. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73307 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
2009-06-13Removed bits of grammar dealing with quantifiers.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73280 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-13Support for parsing SMTLIB headers. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73278 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-13Changed SMTParser to return the parsed QueryCommand.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73277 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-12Removed parser_temp.h. Adapted the code to use SMTParser directly. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73215 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-12Removed unused file.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73214 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-10Move declaration of vc_DeleteExpr outside of function.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73173 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-10Updated the SMT test driver. Other small changes to parser_temp.h andCristian Cadar
smtlib.y. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73167 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 22:41:21 +0000