about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
2016-06-28add assertions to check the pre-condition of bvVar*Shift that both operands ↵Hoang M. Le
have the same bv width
2016-06-27change bitwidth of expr_shpost in MetaSMTBuilder::constructSDivByConstant to ↵Hoang M. Le
64, so that the first two arguments of the call bvVarRightShift(extend_npm, expr_shpost, 64) have the same bitwidth of 64.
2016-06-23Merge pull request #415 from andreamattavelli/termination_infoCristian Cadar
Use klee_message for timeout information
2016-06-23Use klee_message for timeout informationAndrea Mattavelli
2016-06-10apply clang-formatHoang M. Le
2016-06-10remove now unused getShiftBits()Hoang M. Le
2016-06-10remove bitmasking shift amount in bvVarArithRightShiftHoang M. Le
2016-06-10remove bitmasking shift amount in bvVarRightShiftHoang M. Le
2016-06-10remove bitmasking shift amount in bvVarLeftShiftHoang M. Le
2016-06-10remove bitmasking shift amount in constructAShrByConstant and make it return ↵Hoang M. Le
0 when overshifting
2016-06-10remove bitmasking shift amount in bvRightShiftHoang M. Le
2016-06-10remove bitmasking shift amount in bvLeftShiftHoang M. Le
2016-06-10handle special cases of sdiv 1 and -1Hoang M. Le
2016-06-10rename the configure option --with-metasmt-default-solver to ↵Hoang M. Le
--with-metasmt-default-backend and improve the associated CXX flag
2016-06-10use default metaSMT solver as defined in configurationHoang M. Le
2016-06-10update Makefile for metaSMTHoang M. Le
2016-06-10clean up metaSMT includesHoang M. Le
2016-05-27Merge pull request #396 from andreamattavelli/fix_kleaver_parserCristian Cadar
Fixed bug #375 in Kleaver's parser and added --clear-array-decls-after-query option to Kleaver.
2016-05-25add include in Z3Solver.cpp (did not compile with llvm-2.9)Hoang M. Le
2016-05-24Fixed bug #375 in Kleaver's parserAndrea Mattavelli
2016-05-18Modified -debug-print-instructions to allow to write directly on log file.Andrea Mattavelli
The option now contains 4 different options: 1) all:stderr, which logs all instructions to file in format [src, inst_id, llvm_inst]; 2) src:stderr, which logs all instructions to file in format [src, inst_id]; 3) compact:stderr, which logs all instructions to file in format [inst_id]; 4) all:file, which logs all instructions to file in format [src, inst_id, llvm_inst]; 5) src:file, which logs all instructions to file in format [src, inst_id]; 6) compact:file, which logs all instructions to file in format [inst_id]; Writing to file gives a speedup of ~50x.
2016-04-19Merge pull request #369 from MartinNowack/fix_determ_solver_arrayMartinNowack
Generate unique STP and Z3 array names deterministically
2016-04-17Merge pull request #359 from delcypher/fix_indep_solver_bugCristian Cadar
Bug fix in IndependentSolver
2016-04-14Disabling --solver-optimize-divides by default, as the optimization is ↵Cristian Cadar
currently buggy, and we keep hitting this bug... See https://github.com/klee/klee/issues/334 for details.
2016-04-12Merge pull request #364 from MartinNowack/feat_partial_loggingCristian Cadar
Partial logging of queries
2016-04-09Generate unique STP and Z3 array names deterministicallyMartin Nowack
2016-04-08Remove computation of ``isLocal`` that is always true when handlingDan Liew
AllocaInst.
2016-04-08Rename KLEE command line options fromDan Liew
* ``-replay-out`` to ``-replay-ktest-file`` * ``-replay-out-dir`` to ``-replay-ktest-dir`` and also rename * help descriptions * global variables corresponding to these options. * Names used in ``KleeHandler``, ``Interpreter``, ``Executor`` and in KLEE's ``main()`` function. The old name for the options/code was very unhelpful as it wasn't obvious that "out" files are ``.ktest`` files unless you examine KLEE's source code.
2016-03-23Refactoring of conditional flush into own function.Martin Nowack
@delcypher: Thanks a lot Dan!
2016-03-23Fix comment + Clang FormattingMartin Nowack
2016-03-23Add option to log partial solver queries before calling itMartin Nowack
2016-03-22Properly assert that an assignment computed inDan Liew
``IndependentSolver::computeInitialValues(...)`` satisfies the whole query. The previous commit only checked expressions evaluated to true where there was an assignment for ``Array`` objects that the caller asked for. This is incomplete and may miss problems with the assignment. Instead in ``assertCreatedPointEvaluatesToTrue()`` augment the ``Assignment`` object with additional arrays in the ``retMap`` map.
2016-03-22ExprPPrinter: Print out arrays deterministicallyMartin Nowack
The address of KLEE-internal data structures should not influence the order arrays are printed out. Order arrays by name.
2016-03-22Try to fix #348Dan Liew
The problem was that ``assertCreatedPointEvaluatesToTrue()`` used in the IndependentSolver assumed that it would be given an assignment for every array. If this wasn't the case the ``Assignment`` object by default would just replace every read of an unknown array with a byte filled with zeros. This problem would appear if ``IndependentSolver::getInitialValues(...)`` was called without asking for assignment for used arrays. I saw two ways of fixing this * Get an assignment for all arrays even if the client didn't ask for them. This guarantees that is the query is satisfiable then we can compute a concrete assignment. * Just do a "best effort" check and only check expressions that can be fully assigned to. I chose the latter because the first option seems pretty wasteful, especially for an assert. The second option isn't ideal though as it would be possible to compute an assignment that for the whole query leads to "unsat" but we wouldn't notice.
2016-03-16push_back usage for values vectorvpushkar
2016-03-16Wrong std::vector 'values' usage after vector's capacity reserve. It is the ↵vpushkar
error to use [] operator for accessing vector's elements after reserving. In such cases push_back/emplace methods should be used. But in this source code the usage of std::vector is redundant. So vector 'values' was iliminated.
2016-03-01Documented default values for various options and improved the description ↵Cristian Cadar
of some.
2016-02-29Merge pull request #344 from MartinNowack/feat_mallocMartinNowack
Add support for tcmalloc
2016-02-27Merge pull request #342 from delcypher/expr_fixesMartinNowack
A few Expr related clean ups
2016-02-27Use klee-provided GetMallocUsage for consistencyMartin Nowack
2016-02-27Refactoring: Extract checking memory limit into own functionMartin Nowack
2016-02-27Add support for tcmallocMartin Nowack
Beside improving performance of KLEE, tcmalloc allows to track used memory correctly. If available, tcmalloc is automatically used during compile time. This can be forced to be: - disabled using --without-tcmalloc - enabled using --with-tcmalloc In the second case, configure will fail if tcmalloc is not found or usable. Both versions of tcmalloc a minimal and normal version.
2016-02-23Added missing copyright headers per klee/issue #301Marko Dimjašević
2016-02-23When calling ``Assignment::dump()`` if there are no bindings emitDan Liew
a message stating this.
2016-02-23Move ``Assignment::dump()`` into its own implementation file soDan Liew
that it's possible to call it from gdb.
2016-02-22Remove stray STP function declaration.Dan Liew
2016-02-22Move Array constructor out of ``Expr.h`` and into ``Expr.cpp``.Dan Liew
The implementation of the constructor calls a method on a ``ConstantExpr`` which means the type must be complete (i.e. a forward declaration of ``ConstantExpr`` is insufficient) which creates an unnecessary ordering Dependency in ``Expr.h``.
2016-02-20Fix valueIsOnlyCalled() used by MD2U.Sean Bartell
CallInst::getOperand() uses incompatible operand orders across LLVM versions. Use CallSite::hasArgument() instead. This bug prevented the MD2U searcher from working correctly.
2016-02-14Handle Z3 API change between 4.4.1 and the current master branchDan Liew
for the ``Z3_get_error_msg()`` function.
2016-02-14Add basic implementation of Z3Builder and Z3Solver and Z3SolverImplDan Liew
which is based on the work of Andrew Santosa (see PR #295) but fixes many bugs in that implementation. The implementation communicates with Z3 via it's C API. This implementation is based of the STPSolver and STPBuilder and so it inherits a lot of its flaws (See TODOs and FIXMEs). I have also ripped out some of the optimisations (constructMulByConstant, constructSDivByConstant and constructUDivByConstant) that were used in the STPBuilder because * I don't trust them * Z3 can probably do these for us in the future if we use the ``Z3_simplify()`` At a glance its performance seems worse than STP but future work can look at improving this.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 05:26:18 +0000