about summary refs log tree commit diff homepage
path: root/lib/Solver
AgeCommit message (Collapse)Author
2009-06-09Kill off UpdateList::isRooted flag.Daniel Dunbar
- The right way to handle this is by using constant arrays, where the semantics are easier to define and implement. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73124 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Remove unnecessary include.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73123 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08FastCexSolver: Start implementing exact value propogation.Daniel Dunbar
- So far this just propogates obvious equalities and reads. For example, FastCexSolver can now prove that: -- array arr219[3] : w32 -> w8 = symbolic (query [(Eq 235 N0:(Read w8 0 arr219))] (Eq 235 N0)) -- is valid. Even though this is very basic, it is good enough to solve ~50% of the valid queries on pcresymtest-[34].pc (total reduction in # of queries is ~25%). Unfortunately, this only gives a 1-2% speedup, which is disappointing, but there is a lot more we can do. I'm a little surprised the speedup is so low, this may be an indicator that there are some other things going on, for example perhaps the STP expr construction cost for arrays is very high, and we inevitably will end up paying this unless we solve so many queries that some arrays never ever make it to STP. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73058 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08FastCexSolver: Stub out infrastructure for propogating exact values & provingDaniel Dunbar
validity. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73055 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08FastCexSolver: Add exact value contents to CexObjectData.Daniel Dunbar
- The exact contents are a conservative approximation for the values of each array location, to be used for proving valid queries. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73054 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08FastCexSolver: Rename forceExprTo* to propogatePossible*Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73053 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08FastCexSolver: Lazily initialize object values and kill off ObjectFinder class.Daniel Dunbar
Also, explicitly manage the object data to avoid copy overhead. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73051 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Kill off Concat::is[248]ByteConcat, and fix FastCexSolver for this case.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73049 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Add klee::createDummySolver, the dummy solver always fails.Daniel Dunbar
- Useful as an alternative backend to STP for testing. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73048 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Cleanup FastCexSolver:Daniel Dunbar
- Make CexObjectData members private. - Use std::vector instead of allocating memory by hand. - Factor out method which does the propogation from the various Solver routines. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73047 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Support the extended query command syntax.Daniel Dunbar
- There are two optional lists following the constraints and the query expression. The first is a list of expressions to give values for and the second is a list of arrays to provide values for. - Update ExprPPrinter to accept extra arguments to print these arguments. - Add Parser support. - Add more ArrayDecl support. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72938 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Clean up a number of unused variable warnings when building w/oDaniel Dunbar
asserts. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72924 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Sink getConstantValue into ConstantExpr.Daniel Dunbar
- Propogate ConstantExpr to various places, or cast as appropriate. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72862 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Change Solver::getValue to make explicit that result is a ConstantExpr.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72860 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Finish removing uses of Expr::isConstant.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72859 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Start removing uses of Expr::isConstant.Daniel Dunbar
- These should use cast<>, isa<>, or dyn_cast<> as appropriate (or better yet, changed to use ref<ConstantExpr> when the type is known). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72857 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Use cast<> instead of static_ref_cast.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72845 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Move isConstant from ref<> to Expr::Daniel Dunbar
- Ref.h is now freestanding. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72824 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-03Kill off specialized ref<> forwarding methods, in the interest of making it aDaniel Dunbar
more standard reference counting wrapper. - The only interesting changes here are in Ref.h, everything else is just updating foo.method to use foo->method instead. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72777 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-02Use ConstantExpr::alloc instead of ref<Expr> directlyDaniel Dunbar
- The "constant optimization" embedded inside ref<Expr> is going away. - No functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72730 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-25Add includes to get sprintf (STPBuilder) andDuncan Sands
fprintf, stderr etc (Solver) when compiling with gcc-4.4. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72381 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-22Add missing include (for FreeBSD build)Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72270 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-21Initial KLEE checkin.Daniel Dunbar
- Lots more tweaks, documentation, and web page content is needed, but this should compile & work on OS X & Linux. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-12-05 00:24:11 +0000