| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
Add SimplifyExpressions command line option
|
|
iostream injects static constructor function into every compilation unit.
Remove this to avoid it.
|
|
According to LLVM: lightweight and simpler implementation of streams.
|
|
|
|
Allow users to bypass ConstraintManager::simplifyExpr(ref<Expr>).
|
|
Fix handling of memory usage in KLEE.
|
|
clang warning.
|
|
|
|
Memory usage API in LLVM since 3.3 is not working the way it is
intended by KLEE. This ports the pre 3.3. version to KLEE.
Fixes the malloc test case.
|
|
instead it was reporting real user ID of the process.
|
|
has been removed in LLVM3.4
|
|
of old V1 path API.
LLVM2.9 supports LLVM's V2 path API. Because that is the minimum
version we support we should just use this API everywhere so we
reduce the number of #if LLVM_VERSION_CODE macros and duplicated
code.
|
|
Old Path API was removed
|
|
|
|
that clients can access HandlerInfo nicely.
|
