Age | Commit message (Collapse) | Author |
|
appropriate existing directories and a new directory Statistics; a few missing renames.
|
|
|
|
using "../"
|
|
|
|
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 .
|