| Age | Commit message (Collapse) | Author |
|---|
|
The option now contains 4 different options:
1) all:stderr, which logs all instructions to file in format [src, inst_id, llvm_inst];
2) src:stderr, which logs all instructions to file in format [src, inst_id];
3) compact:stderr, which logs all instructions to file in format [inst_id];
4) all:file, which logs all instructions to file in format [src, inst_id, llvm_inst];
5) src:file, which logs all instructions to file in format [src, inst_id];
6) compact:file, which logs all instructions to file in format [inst_id];
Writing to file gives a speedup of ~50x.
|
|
AllocaInst.
|
|
* ``-replay-out`` to ``-replay-ktest-file``
* ``-replay-out-dir`` to ``-replay-ktest-dir``
and also rename
* help descriptions
* global variables corresponding to these options.
* Names used in ``KleeHandler``, ``Interpreter``, ``Executor``
and in KLEE's ``main()`` function.
The old name for the options/code was very unhelpful as it wasn't
obvious that "out" files are ``.ktest`` files unless you examine KLEE's
source code.
|
|
of some.
|
|
|
|
|
|
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...
|
|
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
|
|
Support directory
|
|
flag as suggested by @ccadar
|
|
infeasible assumptions.
|
|
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.
|
|
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
|
|
|
|
|
|
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
|
|
|
|
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.
|
|
|
|
patch.
|
|
holycrap872-ArrayFactory
|
|
The way that Arrays were handled in the past led to the possibility of
aliasing issues. This occured whenever a new branch discovered an array
for the first time. Each branch would create a new instance of the same
array without seeing if it had been created before. Therefore, should a
new branch encounter the same state as some previous branch, the
previous branch's solution wouldn't satisfy the new state since they
didn't recognize they were referencing the same array. By creating an
array factory that creates a single symbolic array, that problem is
handled. Note: Concrete arrays should not be created by the factory
method since their values are never shared between branches.
The factory works by seeing if an array with a similar hash has been
created before (the hash is based on the name and size of array). If
there has been it then searches through all of the arrays with the same
hash (stored in a vector) to see if there is one with an exact match.
If there is one, the address of this previously created equivalent
array is returned. Otherwise, the newly created array is unique, it is
added to the map, and it's address is returned.
This aliasing issue can be seen by comparing the output of the
Dogfood/ImmutableSet.cpp test cases with and with out this commit.
Both act correctly, but the number of queries making it to the solver
in the previous version is much greater 244 vs 211. This is because
the UBTree in the CexCachingSolver and the cache in the CachingSolver
do not recognize queries whose solutions were previously calculated
because it doesn't think the arrays in the two queries are the same.
While this does not cause an error, it does mean that extra calls are
made.
|
|
Instead of checking for every possible casse which result in overflow,
it is much simpler to perform the operation using integers with bigger
dimension and check if the result overflow
|
|
This requires clang with -fsanitize=unsigned-integer-overflow
tested with clang and llvm 3.4.2
|
|
Will redo the merge to preserve original commits.
This reverts commit a743d7072d9ccf11f96e3df45f25ad07da6ad9d6.
|
|
and mul operations. Refactored tests into two main cases, and
disabled them on LLVM 2.9, which does not support -fsanitized=*signed-integer-overflow.
|
|
Fix va args passing for big types
|
|
* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET)
* Remove the now defunct ExprSMTLIBLetPrinter
* Improve performance of ExprSMTLIBPrinter::scan() by keeping
track of visited Expr to avoid visiting them again
* Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr()
|
|
Removed XFAIL tag from the Feature/VarArgLongDouble.c test
Fixed Executor to (more) correctly handle the alignment of types larger than 64bit (such as long double) when those are passed in var_args on x86_64.
Specifically:
From http://www.x86-64.org/documentation/abi.pdf
AMD64-ABI 3.5.7p5: Step 7.
Align l->overflow_arg_area upwards to a 16 byte boundary if alignment needed by type exceeds 8 byte boundary.
|
|
by @hpalikareva).
|
|
Also use bold green text when KLEE finishes. This is done by taking
advantage of llvm::raw_ostream's nice API for controlling the console
text colour.
|
|
|
|
|
|
- Mostly fixed by removing unnecessary references.
|
|
|
|
- KCachegrind appears to expect the first function name to be preceeded by the
name of the file it appears in. Otherwise, it will end up creating two
different records for the function, one of which has no file name and won't
have any statistics.
|
|
- I suspect no one is using this feature, and I'm not sure it is well conceived
either. Ripping it out for now in lieu of bothering to maintain it.
|
|
FloatingPointOps.ll).
|
|
|
|
- This allows us to build in +Asserts mode even when LLVM isn't (by disabling
the checks in that mode).
- Eventually it would be nice to just move off of LLVM's DEBUG infrastructure
entirely and just have our own copy, but this works for now.
- Fixes #150.
|
|
|
|
config.h files.
- There seems to be a better solution for this by defining a macro prefix, per:
http://www.gnu.org/software/autoconf-archive/ax_prefix_config_h.html
but I have no experience with that and it looks like it might involve
rewriting a bunch of our macro checks.
|
|
(independently).
In our recently switch to llvm::raw_ostream (and friends) (I think this
is d934d983692c8952cdb887cbcd59f2df0001b9c0) we forgot to flush the
llvm::raw_string_ostream to the underlying string used for error report
files (e.g. test000001.overshift.err) so we would end up writing an
empty string to error report files.
Also added a test case to catch this.
|
