about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2016-03-10Merge pull request #355 from delcypher/wrong_not_expr_in_enumCristian Cadar
Fix incorrect position of ``Not`` in ``Expr::Kind``
2016-03-09Fix incorrect position of ``Not`` in ``Expr::Kind`` which meant it was includedDan Liew
in the range of ``BinaryKindFirst`` and ``BinaryKindLast``. ``NotExpr`` is a unary expr not a binary expression.
2016-03-06Merge pull request #353 from lszekeres/selinux-fixMartinNowack
Fix SELinux signatures in runtime
2016-03-05Fix SELinux signatures in runtimeLaszlo Szekeres
The SELinux function signatures have changed between version 2.2 and 2.3. In particular, the type of the "security context" parameter was changed from char * to const char *, with the following patch: SELinuxProject/selinux@9eb9c9327563014ad6a807814e7975424642d5b9. Recent Linux distributions (e.g. Ubuntu 15.10) ship with the updated version of libselinux. This change makes the SELinux runtime compatible with the newer versions of the library by replacing security_context_t with its original char * definition and defining it as const only if the installed library does so. Whether the system uses const char * types is detected with the configure script. Fixes klee/klee#303.
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-27Travis: Run TCMalloc runs explicitlyMartin Nowack
2016-02-27Merge pull request #342 from delcypher/expr_fixesMartinNowack
A few Expr related clean ups
2016-02-27Merge pull request #345 from mdimjasevic/masterMartinNowack
Added missing copyright headers per klee/issue #301
2016-02-27Update travis configuration to use tcmallocMartin Nowack
We have to build our own tcmalloc, as the version provided with Ubtuntu 12.04 is too old.
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-26Merge pull request #346 from omeranson/libraries_squashedMartinNowack
Added support to load libraries from command line
2016-02-25Added support to load libraries from command lineOmer Anson
This allows a user to invoke klee with specific libraries to load from command line. This is an attempt to allow klee to run on applications linked to external libraries. The libraries still have to be compiled specially for klee, in a manner similar to klee-uclibc, i.e. archives (build with llvm-ar) of llvm IR files.
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-22Make the declaration of ``ConstantExpr`` the last declared ``Expr``Dan Liew
sub-class rather than the first. Whilst I'm here clang-format the moved code. The motivation for this is that ``ConstantExpr`` may need to refer to a type that cannot be forward declared (e.g. some kind of enum) in the other ``Expr`` sub-classes. For example if an Expr sub-class is ever introduced that has contains an enum that is used for its constructor then the previous ordering would prevent a Constant evaluation method (e.g. ``ConstantExpr::MyNewExprType(const ref<ConstantExpr> &RHS, MyNewType::SpecialEnum p)``) from being implemented because the ``MyNewType::SpecialEnum`` type has not yet been declared.
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-22Merge pull request #339 from yotann/fix-valueisonlycalledDan Liew
Fix valueIsOnlyCalled() used by MD2U.
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-14Try to fix the TravisCI build when using Z3 as the solver. TheDan Liew
``test/Feature/SolverTimeout.c`` test fails there. The error message I see in TravisCI is ``` Command 2: "/home/travis/build/klee/build/klee/Release+Asserts/bin/klee" "--output-dir=/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out" "--max-solver-time=1" "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp1.bc" Command 2 Result: -11 Command 2 Output: Command 2 Stderr: KLEE: output directory is "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out" KLEE: WARNING: undefined reference to function: printf KLEE: ERROR: (location information missing) divide by zero KLEE: NOTE: now ignoring this error at this location 0 klee 0x0000000000da87d2 llvm::sys::PrintStackTrace(_IO_FILE*) + 34 1 klee 0x0000000000da85c9 2 libpthread.so.0 0x00007fca19936cb0 3 libz3.so 0x00007fca19079826 4 librt.so.1 0x00007fca1747640c 5 libpthread.so.0 0x00007fca1992ee9a 6 libc.so.6 0x00007fca1776c38d clone + 109 ``` The issue appears to be racey as I had to run several copies of KLEE in parallel for the bug to occur using Z3 4.4.1. I managed to get a coredump and got the backtrace from gdb for the crash which is ``` #0 0x00007f4841b11c46 in scoped_timer::imp::sig_handler (s=..., s@entry=...) at ../src/util/scoped_timer.cpp:112 #1 0x00007f484031e0ff in timer_sigev_thread (arg=0x7f48380008c0) at ../nptl/sysdeps/unix/sysv/linux/timer_routines.c:63 #2 0x00007f484291c182 in start_thread (arg=0x7f483db46700) at pthread_create.c:312 #3 0x00007f484061b47d in clone () at ../sysdeps/unix/sysv/linux/x86_64/clone.S:111 ``` The crash appears to be in Z3 itself but I can't reproduce the issue when using the version of Z3 from the master branch. For now we simply workaround the issue by not running the ``test/Feature/SolverTimeout.c`` test when using Z3 as the solver. We should revisit this issue when another stable release of Z3 is made.
2016-02-14Add TravisCI and Docker support for building KLEE with Z3 supportDan Liew
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-02-10Teach the configure script to configure the build to use the Z3 SMTDan Liew
solver using the new ``--with-z3=`` option.
2016-02-09Merge pull request #335 from mdimjasevic/spelling-error-fixesMartinNowack
Fixed two spelling errors.
2016-02-08Fixed two spelling errors.Marko Dimjašević
2016-01-14Try to unbreak the Docker build broken byDan Liew
cece05cadf6a624afd188e81720ae7701736a703
2016-01-14Output a message reporting if the MetaSMT backend is enabled whenDan Liew
running the Configure script.
2016-01-14Remove unnecessary MetaSMT includes from kleaver's ``main.cpp``.Dan Liew
2016-01-14Refactor the MetaSMT makefile commands into its own file which canDan Liew
be included by tools that needs to link against MetaSMT. Apart from making the Makefile code cleaner this allowed the Solver unit test linking to succeed when not building with STP support. Unfortunately when using MetaSMT as the core solver the Solver unit tests do not pass. Clearly no one tried this before... :(
2016-01-14Fix linking with stp via MetaSMT when not building with direct STPDan Liew
support
2016-01-14MetaSMT build fixes.Dan Liew
2016-01-14Fix behaviour of --with-metasmt when passed a path that doesn't exist.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.
2016-01-07[NFC] Refactor SolverImpl out of Solver.cpp into its own fileDan Liew
(SolverImpl.cpp). Whilst I'm here also clang-format the modified code.
2016-01-05Merge pull request #325 from delcypher/fix_independence_solver_leakCristian Cadar
Fix independence solver leak
2015-12-26Merge pull request #326 from domainexpert/upstreamDan Liew
Removed Language: Cpp Entry from .clang-format
2015-12-25Removed Language: Cpp entry from .clang-format due to incompatibility with ↵Andrew Santosa
Clang 3.4.2
2015-12-23Fix memory leak detected by ASan whenDan Liew
``IndependentSolver::computeInitialValues()`` was called where at least one of the constraint sets computed by ``getAllIndependentConstraintsSets()`` is either unsatisfiable or the solver failed. To make things (a little) clearer I've made it so that no ``std::list<>*`` is passed to``getAllIndependentConstraintsSets()``. Instead ``getAllIndependentConstraintsSets()`` now returns a ``std::list<>*`` that the caller is responsible for cleaning up. The behaviour previously was really confusing because it was unclear if the caller or callee was responsible for the clean up. This fixes #322
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-27 08:01:23 +0000