about summary refs log tree commit diff homepage
path: root/lib/Solver
AgeCommit message (Collapse)Author
2017-07-08Corrected comment of Z3Solver classAndrew Santosa
2017-06-02hide backend solver declarations from public includeHoang M. Le
2017-06-02replace handleMetaSMT() with klee::createMetaSMTSolver() and move it into ↵Hoang M. Le
MetaSMTSolver.cpp so that the backend headers only need to be included once there
2017-06-01[Z3] Remove unused include.Dan Liew
2017-06-01[Z3] Add `-debug-z3-verbosity=<N>` option which behaves like Z3's `-v:<N>` ↵Dan Liew
option. This lets us see what Z3 is doing execution (e.g. which tactic is being applied) which is very useful for debugging.
2017-06-01[Z3] Switch from `Z3_mk_simple_solver()` to `Z3_mk_solver()`.Dan Liew
My discussions [1] with the Z3 team have revealed that `Z3_mk_simple_solver()` is the wrong solver to use. That solver basically runs the `simplify` tactic and then the `smt` tactic. This by-passes Z3's attempt to probe for different logics and apply its own specialized tactic. Using `Z3_mk_solver()` should be closer to the behaviour of the Z3 binary. This partially addresses #653. We still need to try rolling our own custom tactic. [1] https://github.com/Z3Prover/z3/issues/1035
2017-06-01[Z3] In `getConstraintLog()` use a separate builder from that of theDan Liew
solver. This is to avoid tampering with the cache of the builder the solver is using.
2017-06-01[Z3] Implement API logging.Dan Liew
Add `-debug-z3-log-api-interaction` option to allow Z3 API calls to be logged to a file. The files logged by this option can be replayed by the `z3` binary (using its `-log` option). This is incredibly useful because it allows to exactly replay Z3's behaviour outside of KLEE.
2017-06-01[Z3] Add option to manually validate Z3 models.Dan Liew
This can be enabled by passing the command line option `-debug-z3-validate-models`. Although Z3 has a global parameter `model_validate` (off by default) I don't trust it so do the validation manually. This also means we can potentially do validation on a per Z3Solver instance basis rather than globally. When failing to validate a Z3 model the solver state and model are dumped to standard error.
2017-06-01[Z3] Add the `-debug-z3-dump-queries=<path>` command line option. ThisDan Liew
is useful for getting access to the constraints being stored in the Z3 solver in the SMT-LIBv2.5 format.
2017-06-01[Z3] Move the `dump()` methods of the Z3NodeHandle<> specializationsDan Liew
into `Z3Builder.cpp` so they can be called from in gdb.
2017-06-01[Z3] Add assertions in Z3 builder to catch underflow with bad widths.Dan Liew
2017-06-01[Z3] Support another solver failure reason that Z3 might give. I'm goingDan Liew
to guess it means timeout but I'm not 100% sure about this.
2017-05-24llvm: make KLEE compile against LLVM 3.5 and 3.6Richard Trembecký
Based on work by @ccadeptic23 and @delcypher. Formatting fixed by @snf. Fix compiler warning by @martijnthe. Further fixes by @mchalupa. Refactored, so that changes can be reviewed -- no massive changes in whitespace and in the surrounding code. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-03-23[CMake] Unbreak build due to not adding AssignmentValidatingSolver.cppDan Liew
to list of source files. The cause of the breakage was me being to eager and merging #468 before forcing tests to re-run. That PR was written before the CMake build system existed.
2017-03-23Add `AssignmentValidatingSolver`. It's purpose is to check any computedDan Liew
assignments against the corresponding `Query` object and check the assignment evaluates correctly. This can be switched on using `-debug-assignment-validating-solver` on the command line.
2017-03-03Using klee_message instead of llvm:errsCristian Cadar
2017-02-22klee: remove use of deprecated 'register'Jiri Slaby
New compilers warn about using 'register' as follows: ConstantDivision.cpp:66:3: warning: 'register' storage class specifier is deprecated and incompatible with C++1z [-Wdeprecated-register] Remove the register specifier -- the compilers are clever enough to know what to do. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-14Added error message when STP fails to fork.Cristian Cadar
2016-11-23Renamed .pc to .kquery (kleaver query)Eric Rizzi
2016-11-18[CMake] Remove use of tabs in `CMakeLists.txt` files.Dan Liew
2016-11-18[CMake] Re-express LLVM and KLEE library dependencies asDan Liew
transitive dependencies on KLEE's libraries rather than on the final binaries. This is better because it means we can build other tools that use KLEE's libraries and not need to express the needed LLVM dependencies. It also makes it clearer what the dependencies are between KLEE libraries. This has illustrated a problem with the `kleeBasic` library. It contains `ConstructSolverChain.cpp` which clearly belongs in `kleaverSolver` not in `kleeBasic`. This will be fixed later.
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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 11:20:02 +0000