about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2009-07-11Report an error in the SMT parser when encountering the few operatorsCristian Cadar
not supported yet: bvneg, bvsmod, bvxnor, rotate_left, rotate_right, repeat. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75319 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Removed debug info.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75313 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Fixed order of offsets in Extract.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75311 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Added xfail test: (query [false] true) should return INVALID.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75310 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Added support for not, zero_extend, and sign_extend to the SMTLIB parser.Cristian Cadar
Added support for n-ary and, or and xor. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75299 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-10Simple propagation rules for boolean not in the fast cex solver.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75242 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Small test for non-boolean Not.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75241 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-07-08Added support for bitvector variables to the SMTLIB parser (currentlyCristian Cadar
widths have to be multiples of 8). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74990 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-02Added support for bitvector constants to the SMTLIB parser. OnlyCristian Cadar
variable and array support left. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74690 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-27emacs .pc mode: Numbers should be recognized before identifiersDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74365 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-26Simplify read/write code.Daniel Dunbar
- Get rid of unnecessary special cases. - Support read/write of large integers. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74286 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-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-25Didn't mean to check this in.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74144 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-20KQuery documentation: division and shift operations.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73814 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-16kleaver: Add some command line options for choosing the Solver.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73485 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-14Add NonConstantExpr, so it is possible to statically type an expression that isDaniel Dunbar
known to be not-constant. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73352 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Start test case for ConstantFoldingExprBuilderDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73351 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-14Fixup syntax coloring for emacs .pc mode.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73344 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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-02-03 01:45:28 +0000