| Age | Commit message (Collapse) | Author |
|---|
|
Reformat ``getAllIndependentConstraintsSets()`` using clang-format.
It was not formatted correctly and was consequently a little hard
to read. Also add braces around a for loop body.
The original code for this function came from
d9bcbba2c94086039c11c86200670639ee2ec19f
|
|
Implement support for lowering the ``llvm.objectsize`` intrinsic
|
|
Fix a leak detected by ASan in the KQuery parser where on destruction of
|
|
introduced in LLVM 2.7. Previously KLEE would emit the following error
message when ``IntrinsicLowering::LowerIntrinsicCall()`` was called on
the intrinsic
```
LLVM ERROR: Code generator does not support intrinsic function 'llvm.objectsize.i64.p0i8'!
```
The ``IntrinsicCleaner`` pass now lowers this intrinsic to a constant
integer depending on the second argument to the intrinsic. This
corresponds to the case where the size of the object pointed to by the
first argument is unknown.
An alternative design would be to handle this intrinsic in the Executor
where is actually possible to know the size of objects during execution.
However that would be much more complicated because if the pointer is
symbolic we would have to fork for every object that could be pointed
to.
The implementation is similar to #260 but we handle the second argument
to the intrinsic correctly and also have a simple test case.
Unfortunately we have to have a different version of the test case
for LLVM 2.9 because the expected suffix for the intrinsic is different
in LLVM 2.9.
|
|
the ``ParserImpl`` it wouldn't free allocated ``Identifier``s
|
|
so that it is possible to ``#include "klee/util/ArrayExprHash.h"``
|
|
Some of these leaks were introduced by the factory constructor for Array
objects (f049ff3bc04daead8c3bb9f06e89e71e2054c82a) but a few others have
been around for far longer.
This leak was fixed by introducing a ``ArrayCache`` object which has two
purposes
* Retains ownership of all created ``Array`` objects and destroys them when
the ``ArrayCache`` destructor is called.
* Mimic the caching behaviour for symbolic arrays that was introduced
by f049ff3bc04daead8c3bb9f06e89e71e2054c82a where arrays with the same
name and size get "uniqued".
The Executor now maintains a ``arrayCache`` member that it uses and
passes by pointer to objects that need to construct ``Array`` objects (i.e.
``ObjectState``). This way when the Executor is destroyed all the
``Array`` objects get freed which seems like the right time to do this.
For Kleaver the ``ParserImpl`` has a ``TheArrayCache`` member that is
used for building ``Array`` objects. This means that the Parser must
live as long as the built expressions will be used otherwise we will
have a use after free. I'm not sure this is the right design choice.
It might be better to transfer ownership of the ``Array`` objects to
the root ``Decl`` returned by the parser.
|
|
helper functions.
|
|
for it
|
|
Use "-debug-dump-stp-queries" argument for KLEE/Kleaver
to print out each STP query sent to the STP Solver.
Queries have the format which `stp` frontend can understand.
|
|
|
|
|
|
Support directory
|
|
The overloaded assignment operator previously only deleted the head
``UpdateNode`` if the ``UpdateList`` had exclusive ownership which left the remaining
list of ``UpdateNode``s dangling if those nodes had ``refCount`` of 1.
To fix this the logic that was previously in the ``UpdateList`` destructor
for deleting nodes that were exclusively referenced by the UpdateList
has been moved into ``UpdateList::tryFreeNodes()`` so that it can be
called from ``UpdateList::operator=()``.
It looks like this bug has been in KLEE since the beginning.
|
|
flag as suggested by @ccadar
|
|
infeasible assumptions.
|
|
``stp/stplog.h`` header file in the current version of STP
and no support in the build system for setting this define so
this code is completly dead.
|
|
|
|
The '%' operater in C is not Gauss Modulo
but remainder operations.
Using a negative number as right operand
can result in a negative number.
Fix appropriate SRem building
Note: MetaSMTlib implementation doesn't have that bug.
|
|
Fix signed division by constant 1/ -1
|
|
|
|
Division by constant divisor get optimized
using shift and multiplication operations in STP builder.
The used method cannot be applied for divisor 1 and -1.
In that case use slow path.
|
|
Fix assertion failure in getDirectCallTarget
|
|
New version of the get initial values functionality which makes use of the independent solver.
|
|
Option --readable-posix-inputs used to turn on/off POSIX-related CEX preferences
|
|
The super-set check in the CexCachingSolver takes MUCH longer than the
sub-set check. Upon closer inspection, the super-set check gets slower
and slower as more counterexamples fill the UBTree. Pretty quickly,
the cost of the super-set check becomes larger than the time required
to simply bypass it and go to the Solver.
|
|
preferences added in the POSIX model. Removed option --prefer-cex which controlled all CEX preferences.
|
|
Previously, default Klee would go through every byte in a test case
and attempt to bound it to be between 0 and 127, making it human
readable. While this may be useful when attempting to understand Klee,
it also means that the time required to create large test suites was
greatly increased. By making this behavior default off, unsuspecting
users won't incur these additional costs.
|
|
It failed when the function being called is a bitcasted alias.
|
|
and kleaver.
|
|
when they are given the --version command line option.
Unfortunately to make the build type and git revision available we
need to check this for every build which means KLEE's support library
will be rebuilt for every build which will slow down incremental builds.
This addresses issue #231
|
|
always goes to zero (matches LLVM's APInt::ashr(...)). This is meant
to partially address issue #218.
There are a few problems with this commit
* It is possible for AShrExpr to not be abbreviated because the scan
methods will not see that we print the 0th child of the AShrExpr twice
* The added test case should really be run through an SMT solver (
i.e. STP) but that requires infrastructure changes.
|
|
the optimisation that rewrites existing constraints when an equality with a constant is added
|
|
|
|
|
|
Cleaner, more efficient timestamps
|
|
|
|
mistake in the last cleanup commit.
|
|
* Removed unused member ShadowObjects in ExecutionState
* Added documentation of members and reorder according to categories
|
|
This function should be used solely in assertion statements and is
intended as a sanity check to make sure that the solution constructed
by IndependentSolver::getInitialValues() produces and answer that in
fact satisfies the the query.
|
|
Previous implementation simply passed the entire constraint forward
without any factoring of the constraint at all. This is a problem
since it is highly likely that there are cached solutions to pieces
of the constraint. The new implementation breaks the entire
constraint down into its requisite factors and passes each piece
forward, one by one, down the solver chain. After an answer is
returned, it is integrated into a larger solution. Since, by
definition, no factor can affect another, we can safely create a
solution to the larger constraint from the answers of its smaller
pieces.
The reconstruction of the solution is done by analyzing which parts of
an array a factor touches. If the factor is the only one to reference
a particular array, then all of the values calculated in the solution
for that array are included in the final answer. If the factor
references a particular element of the array (for example, arr[1]),
then only the value in index 1 of array arr will be included in the
solution.
|
|
This functionality is necessary in order to more effectively handle
calls to IndependentSolver::getInitialValues. An incoming query will
be broken down into its smaller parts, and each piece will be solved
for. At the end, the pieces will be recombined into a larger solution.
The IndependentElementSet::getAllFactors() method takes a query and
breaks it down into all of it's non-interacting factors. The
IndependentElementSet::calculateArrays() method calculates which
arrays are involved in a particular factor.
|
|
|
|
|
|
|
|
Replaced inefficient llvm::sys::Process::GetTimeUsage() with TimeValue::now(),
because in many cases only the wall clock time is needed, not the user
and sys times (which are significantly more expensive to get).
Updated TimingSolver and WallTimer accordingly.
|
|
|
|
This is important for future changes to IndependentSolver::
getInitialValues() so that an incoming constraint can be broken
down into its smallest possible parts. Each of these individual
parts may then be solved for and then the solutions to each piece
combined to create a final answer.
Finally, several fields which had previously been private are now
public to facilitate the smaller solutions being combined into a
larger solution.
|
|
patch.
|
|
holycrap872-ArrayFactory
|
