| Age | Commit message (Collapse) | Author |
|---|
|
Use correct definition and declaration of main function
|
|
Add some missing header to silence
compiler warnings
|
|
also test a negative constant as the lhs.
|
|
between arrays created at the same location but with different sizes
|
|
|
|
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
|
|
Previously the check was done as
unsigned int a, b, c;
c = a * b;
if (c < a)
// error
but it is wrong, since it catches only a subset of all the
possible overflows.
This patch improves the check as
unsigned int a, b, c;
if ((a > 1) && (b > 1){
if ((UINT_MAX/a) < b)
// error
}
An additional case has been added to the tests, with two 32-bit
values that cause overflow and are not detected by the old check.
It is also necessary to break the lowering procedure in case the current
BasicBlock is splitted; in this case it was necessary in order not to
trigger the division by 0 error.
|
|
|
|
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
|
|
This patch introduces nested let-abbreviations in the ExprSMTLIBPrinter
to reduce the size of the SMTLIBv2 queries and the corresponding processing
time (bugfix for #170).
The current implementation of the let abbreviation mode does not consider
expression intra-dependencies and prints all abbreviations in the same
let scope. For a (simplified) example, it prints
(assert (let ( (?B1 (A + B)) (?B2 (A + B + C)) ) (= ?B1 ?B2) ) ).
This is extremely inefficient if the expressions (and there many of these!)
extensively reuse their subexpressions. Therefore, it's better to print
the query with nested let-expressions by reusing existing expression bindings
in the new let scope:
(assert (let ( (?B1 (A + B)) ) (let ( (?B2 (?B1 + C)) ) (= ?B1 ?B2) ) ) ).
This patch adds a new function ExprSMTLIBPrinter::scanBindingExprDeps() that
scans bindings for expression dependencies. The result is a vector of
new bindings (orderedBindings) that represents the expression dependency tree.
When printing in the let-abbreviation mode, the new code starts with
abbreviating expressions that have no dependencies and then gradually makes
these new bindings available in the upcoming let-scopes where expressions
with dependencies reuse them.
The effect of nested let-abbreviations is comparable to :named abbreviations.
However, the latter mode is not supported by the majority of the solvers.
|
|
Shifting by bitwidth-1 is valid
|
|
unconstrained buf[3]
|
|
single method with two different implementations.
There is one version of this method for human readability
(printHumanReadableQuery()) and a version for machine consumption
(printMachineReadableQuery()).
The reason for having two versions is because different behaviour is
needed in different scenarios
* In machine readable mode the entire query is printed inside a single
``(assert ...)``. This is done to allow ``(let ...)`` to abbreviate
as much as possible.
* In human readable mode each constraint and query expression is printed
inside its own ``(assert ...)`` unless the abbreviation mode is
ABBR_LET in which case all constraints and query expr are printed
inside a single ``(assert ...)`` much like in the machine readable mode
Whilst I was here I also fixed a bug handling identation when printing
``(let ...)`` expressions in printAssert()
|
|
* 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()
|
|
|
|
Changed _testingUtils to use stdint.h
|
|
The difference between a 64bit pointer truncated to 32 bits and the
original 64bit pointer would never be 0 if any of the high 32bits in
the pointer were test. If lli and klee had a different value for the
top 32bits of the address this test would be marked as failing.
Due to the 64bit printing buf in _testingUtils this was not exposed before.
The fix clears the top 32bits of the difference.
|
|
64bit numbers)
Fixing this bug will expose a failing test case for Concrete/ConstantExpr.ll
|
|
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.
|
|
varargs on x86_64.
|
|
This is for use with llvm-lit --param=klee_opts=...
Fixes lit.cfg to not have an extranous space behind the klee command.
Augments ConcreteTest to accept and pass arguments to klee.
Augments all the ConcreteTest cases to wrap %klee in quotes.
Without wrapping %klee the extra arguments will be seens as arguments
to ConcreteTest.py resulting in an unknown argument error.
|
|
|
|
Fix a possible deadlock.
|
|
available in LLVM's command line parser for a while (response files).
|
|
- 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.
|
|
- This makes KCachegrind output look nicer, as otherwise it assumes
instructions without debug info were inlined and shows some message to that
effect.
- This does however we might be lying a bit about the source line that an
instruction came from.
- This also adds a test case for our istats output, yay!
|
|
- This works fine for me on OS X now, and has been reported to work on Linux as
well. Enabling across the board although presumably Travis will still only
run single-threaded.
- Fixes #147.
|
|
- 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.
|
|
- If this is a problem for some reason, lets either fix the problem or move it
into Runtime tests.
|
|
|
|
|
|
Major issue was that puts was used for the succeed printf calls.
With newer gcc/clang versions, printf is always used.
The former took different code paths leading to much more possibilities
to trigger failed writes and therefore generating more test cases.
This patch avoids the generation of puts.
And checks for the 4 possible generated test cases for 2 possible errors.
|
|
prevents the hang we are seeing.
|
|
work)
|
|
- You can now make tests disabled, or expected to fail, by writing something like:
// XFAIL: llvm-3.4
or
// REQUIRES: not-llvm-3.4
- This mechanism doesn't support version comparisons, it is mostly intended to
help with switching over to new LLVM versions and incrementally working
through the test failures.
|
|
- LLVM changed the exception handling semantics a lot, and we can't write
compatible tests across the versions. Unfortunately I am afraid this probably
also means KLEE's exception handling semantics are broken for LLVM 3.4+, but
our C++ support is spotty at best. These tests should probably be replaced
with ones in a source language that supports exceptions if and when someone
wants to make that work.
|
|
|
|
Some additional cleaning in test/Makefile
|
|
|
|
- The change in 6829fb9 caused us to not allocation InstructionInfo objects for
instructions without source-level debug info, however, that means that all
such instructions end up sharing the one dummy InstructionInfo object, which
really breaks statistics tracking.
- This commit basically reverts that change, and also changes the code so we
don't ever use the dummy InstructionInfo object for instructions, so that
this problem can't be hit in other ways (e.g., if someone modifies the module
after the InstructionInfoTable construction). There is a FIXME for checking
the same thing for functions.
- Fixes #144.
|
|
- This ensures any stray klee-last files won't be picked up by my check to
prevent people from adding tests that don't use --output-dir.
|
|
which the LLVM JIT can't handle.
|
|
path.
- Otherwise this test takes a long time just hammering on the allocator trying
to get to the memory limit.
|
|
- This one test was taking about half the test time, and it definitely isn't
worth that much value as a test. We probably should have some kind of long
running tests infrastructure for things where we actually want to test KLEE
on real programs.
|
|
parallel.
- It would be nice if there was an easier way to do this that didn't involve
editing all of the tests (like running each test in its own directory), but
this approach fixes #146 and doesn't involve changing 'lit' or writing a
wrapper harness. My assumption is a lot of tests start are derived from
another one, so hopefully following this convention won't be burdensome, and
I updated 'make check' so that it will produce an error if any test runs klee
without --output-dir (by checking for the existing of klee-last files).
- This also helps with #147 but I still can't fully run tests in parallel (I
start hitting STP errors).
|
|
|
|
|
|
|
