| Age | Commit message (Collapse) | Author |
|---|
|
Remove additional reference counting as part of UpdateNodeList and
UpdateNode. Simplifies code.
|
|
Value transformation operates on word instead of byte arrays.
That means the Read indicies need to be adjusted to reflect that.
Previously IndexCleanerVisitor tried to remove the multiplications in the index
to covert byte indicies to word indicies. However as the two added test cases show
this is not sufficent. Therefore we remove the IndexCleanerVisistor and just divide
the index with word size which should always be correct.
|
|
buildMixedSelectExpr was using the byte index for holes in the
select condition instead of the word based one. This only occured
if there was more than 1 hole.
|
|
The caching maps in ArrayExpr are broken, they only consider hashes
and don't check for structural equality. This can lead to hash collisions
and invalid Expr replacement. This is especially potetent for UpdateLists, who
only put the array name in the hash, so there can be a lot of colisions.
|
|
ArrayExprOptimizer read the UpdateList in the wrong order, which
meant that it used least recent update instead of the most recent one.
This patch fixes this as well as adds a test to illustrate the issue.
|
|
|
|
|
|
directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.
|
|
|
|
|
|
|
|
ObjectStates can be shared between multiple states.
A read expression of a symbolic object can be represented differently
depending on previous read expression on the same object.
If the read expression uses a symbolic index, all pending updates
will become entries in the update list of the object state.
If the same object state is read again, with a concrete index,
the latest update list item will be referenced, even though it might
contain more recent but non-essential updates.
If, instead, a concrete read will be executed first, it does not contain
the non-essential updates.
For both executions, the ReadExpr with a constant index will have two
different representations, which is not intented.
This patch makes sure, we do not include more recent, non-essential
updates for concrete reads.
Fixes #921
|
|
|
|
|
|
|
|
printing category
|
|
category for building and printing expressions
|
|
and "default=off" in --help
|
|
|
|
files
|
|
This was renamed in LLVM commit 54f0462d2b7f, so handle the rename.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Otherwise we see:
../lib/Expr/Expr.cpp:331:14: error: no member named 'integerPartWidth' in namespace 'llvm'; did you mean 'llvm::APFloatBase::integerPartWidth'?
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
|
|
* use `using` instead of typdef
* use `collection.empty()` instead of size
* use `auto` if clear
* use `emplace_back` where useful
* use `nullptr` instead of NULL
* use `override` if applicable
* use `explicit` for constructor to avoid implicit conversion
|
|
Don't pollute the project include directory with optimization specific
headers.
|
|
Remove unneeded headers from include files
|
|
Conditions are checked inside of `optimizeExpr()`
anyway. This simplifies the code a lot.
|
|
|
|
simplifies code a lot.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
configuration, TravisCI scripts and Dockerfile build appropriately.
There are a bunch of clean ups this enables but this commit doesn't
attempt them. We can do that in future commits.
|
|
Fixes klee/klee#717
delete on null pointer is always safe.
|
|
Request LLVM 3.4 as minimal requirement for KLEE
|
|
It became unnecessary when defining options and mainly undefined.
So introduce KLEE_LLVM_CL_VAL_END as suggested by @delcypher.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
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.
|
|
constant arrays.
|
|
* Making `Expr::compre(const Expr&, ExprEquivSet)` private and moving
its implementation into `Expr.cpp`.
* Document `Expr::compare(const Expr&)`.
This partially addresses #515 .
|
|
|
|
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.
|
|
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.
|
|
* Add unittest to check that the `Assignment` class can evaluate
expressions containing a `NotOptimizedExpr`.
* Fix the `AssignmentTest.FoldNotOptimized` unit test by
teaching the `ExprEvaluator` to fold `NotOptimizedExpr` nodes.
|
