about summary refs log tree commit diff homepage
path: root/lib/Solver
AgeCommit message (Collapse)Author
2016-11-07Implement a CMake based build system for KLEE.Dan Liew
This is based off intial work by @jirislaby in #481. However it has been substantially modified. Notably it includes a separate build sytem to build the runtimes which is inspired by the old build system. The reason for doing this is because CMake is not well suited for building the runtime: * CMake is configured to use the host compiler, not the bitcode compiler. These are not the same thing. * Building the runtime using `add_custom_command()` is flawed because we can't automatically get transitive depencies (i.e. header file dependencies) unless the CMake generator is makefiles. (See `IMPLICIT_DEPENDS` of `add_custom_command()` in CMake). So for now we have a very simple build system for building the runtimes. In the future we can replace this with something more sophisticated if we need it. Support for all features of the old build system are implemented apart from recording the git revision and showing it in the output of `klee --help`. Another notable change is the CMake build system works much better with LLVM installs which don't ship with testing tools. The build system will download the sources for `FileCheck` and `not` tools if the corresponding binaries aren't available and will build them. However `lit` (availabe via `pip install lit`) and GTest must already be installed. Apart from better support for testing a significant advantage of the new CMake build system compared to the existing "Autoconf/Makefile" build system is that it is **not** coupled to LLVM's build system (unlike the existing build system). This means that LLVM's autoconf/Makefiles don't need to be installed somewhere on the system. Currently all tests pass. Support has been implemented in TravisCI and the Dockerfile for building with CMake. The existing "Autoconf/Makefile" build system has been left intact and so both build systems can coexist for a short while. We should remove the old build system as soon as possible though because it creates an unnecessary maintance burden.
2016-10-27apply clang-formatHoang M. Le
2016-10-27update commentsHoang M. Le
2016-10-27upgrade to boolector-2.2.0 & remove the no longer needed aux array vectorHoang M. Le
2016-10-26move the query creation part into runAndGetCex() (to be consistent with ↵Hoang M. Le
runAndGetCexForked())
2016-10-26change signature of runAndGetCex() to match runAndGetCexForked()Hoang M. Le
2016-10-26remove outdated FIXME (metaSMT-Z3 implements assumption via push/pop)Hoang M. Le
2016-09-29remove mimic_stp option and the associated ITE chain construction for shift ↵Hoang M. Le
operators
2016-09-26Modified logging information to steer the usage of klee_message, ↵Andrea Mattavelli
klee_warning, and klee_error
2016-09-15Add ``-debug-cross-check-core-solver`` option to allow cross-checkingDan Liew
with another solver. For example the core solver can be STP and the cross checking solver can be Z3. Unfortunately a few fragile tests don't pass when actually using this option.
2016-08-06Fix to #445Andrea Mattavelli
2016-08-03fprintf: convert to klee_warningJiri Slaby
In some Solver sources, some error outputs were missing \n. Instead of adding a new line to all of them, convert the fprintf's to klee_warning which adds \n automatically. ErrorHandling.h had to be included in MetaSMTSolver.cpp to have klee_warning declared there. Signed-off-by: Jiri Slaby <jslaby@suse.cz>
2016-07-31Merge pull request #422 from ccadar/div-zero-testCristian Cadar
Added test case exposing division by zero failure reported by @kren1 and made division total in STP to fix it.
2016-07-29Explicitely making division total in STP.Cristian Cadar
2016-07-09Fix variable shifting behavior with different sizesMartin Nowack
Generated STP equality expressions have to be the same type. If a shift with different types as operands was used, therefore equality expressions of different width were generated. Beside avoiding the different sizes, this patch restores the original behavior to extract just the part involved in shifting and therefore should generate smaller expressions. Enable sdiv test case
2016-07-08Support gzip-based compression of raw_outstreamsMartin Nowack
Provide initial zlib-based compression support for raw_outstreams. Replacing llvm::raw_fd_outstreams with compressed_fd_outstreams automatically compresses data in gzip format before writing to file. Options added: * --compress-log to compress all query log files (e.g. *.pc, *.smt2) on the fly. Every query log file gets extended with .gz. * --debug-compress-instructions to compress logfile for instruction stream on the fly.
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-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-10update Makefile for metaSMTHoang M. Le
2016-06-10clean up metaSMT includesHoang M. Le
2016-05-25add include in Z3Solver.cpp (did not compile with llvm-2.9)Hoang M. Le
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-09Generate unique STP and Z3 array names deterministicallyMartin Nowack
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-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-02-23Added missing copyright headers per klee/issue #301Marko Dimjašević
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.
2016-02-10Add some of the basic plumbing required to support a Z3 solver in KLEE.Dan Liew
2016-01-14MetaSMT build fixes.Dan Liew
2016-01-14Make it possible to build KLEE without using STP and only MetaSMT.Dan Liew
The default core solver is STP if KLEE is built with STP otherwise it is MetaSMT. Whilst I'm here rename SUPPORT_METASMT macro to ENABLE_METASMT for consistency.
2016-01-12Refactor setting the core solver (i.e. STP, MetaSMT or DummySolver) by providingDan Liew
a ``createCoreSolver()`` function. The solver used is set by the new ``--solver-backend`` command line argument. The default is STP. This change necessitated refactoring the MetaSMT stuff. That clearly didn't belong in the Executor! The MetaSMT command line option is now ``--metasmt-backend`` as this only picks the MetaSMT backend. In order to use MetaSMT ``--solver-backend=metasmt`` needs to be passed. Note I don't have MetaSMT built on my development machine so I don't know if the MetaSMT stuff even compiles...
2016-01-12Drop unnecessary ``#include``s from Solver.cpp.Dan Liew
2016-01-12Refactor MetaSMTSolver and MetaSMTSolverImpl out of Solver.cpp intoDan Liew
their own file ``MetaSMTSolver.cpp``. Whilst I'm here also clang-format the modified code. This might not be a NFC (non functional change) as there's a good chance this has broken the MetaSMT build of KLEE. I don't have a build of MetaSMT to hand and there is no TravisCI build. At this point because there is no maintainer for this code I think we should consider removing it as it is going bitrot.
2016-01-12[NFC] Refactor STPSolver and STPSolverImpl out of Solver.cpp into theirDan Liew
own file ``STPSolver.cpp``. Whilst I'm here also clang-format the modified code.
2016-01-12[NFC] Refactor DummySolver out of Solver.cpp into its own fileDan Liew
``DummySolver.cpp``. Whilst I'm here also clang-format the modified code.
2016-01-12[NFC] Refactor ValidatingSolver out of Solver.cpp into its own fileDan Liew
``ValidatingSolver.cpp``. Whilst I'm here also clang-format the modified code.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-11 04:18:29 +0000