| Age | Commit message (Collapse) | Author |
|---|
|
``test/Feature/SolverTimeout.c`` test fails there.
The error message I see in TravisCI is
```
Command 2: "/home/travis/build/klee/build/klee/Release+Asserts/bin/klee" "--output-dir=/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out" "--max-solver-time=1" "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp1.bc"
Command 2 Result: -11
Command 2 Output:
Command 2 Stderr:
KLEE: output directory is "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out"
KLEE: WARNING: undefined reference to function: printf
KLEE: ERROR: (location information missing) divide by zero
KLEE: NOTE: now ignoring this error at this location
0 klee 0x0000000000da87d2 llvm::sys::PrintStackTrace(_IO_FILE*) + 34
1 klee 0x0000000000da85c9
2 libpthread.so.0 0x00007fca19936cb0
3 libz3.so 0x00007fca19079826
4 librt.so.1 0x00007fca1747640c
5 libpthread.so.0 0x00007fca1992ee9a
6 libc.so.6 0x00007fca1776c38d clone + 109
```
The issue appears to be racey as I had to run several copies of KLEE in
parallel for the bug to occur using Z3 4.4.1. I managed to get a
coredump and got the backtrace from gdb for the crash which is
```
#0 0x00007f4841b11c46 in scoped_timer::imp::sig_handler (s=..., s@entry=...) at ../src/util/scoped_timer.cpp:112
#1 0x00007f484031e0ff in timer_sigev_thread (arg=0x7f48380008c0) at ../nptl/sysdeps/unix/sysv/linux/timer_routines.c:63
#2 0x00007f484291c182 in start_thread (arg=0x7f483db46700) at pthread_create.c:312
#3 0x00007f484061b47d in clone () at ../sysdeps/unix/sysv/linux/x86_64/clone.S:111
```
The crash appears to be in Z3 itself but I can't reproduce the issue when using the
version of Z3 from the master branch.
For now we simply workaround the issue by not running the
``test/Feature/SolverTimeout.c`` test when using Z3 as the solver.
We should revisit this issue when another stable release of Z3 is made.
|
|
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...
|
|
introduced in LLVM 2.7. Previously KLEE would emit the following error
message when ``IntrinsicLowering::LowerIntrinsicCall()`` was called on
the intrinsic
```
LLVM ERROR: Code generator does not support intrinsic function 'llvm.objectsize.i64.p0i8'!
```
The ``IntrinsicCleaner`` pass now lowers this intrinsic to a constant
integer depending on the second argument to the intrinsic. This
corresponds to the case where the size of the object pointed to by the
first argument is unknown.
An alternative design would be to handle this intrinsic in the Executor
where is actually possible to know the size of objects during execution.
However that would be much more complicated because if the pointer is
symbolic we would have to fork for every object that could be pointed
to.
The implementation is similar to #260 but we handle the second argument
to the intrinsic correctly and also have a simple test case.
Unfortunately we have to have a different version of the test case
for LLVM 2.9 because the expected suffix for the intrinsic is different
in LLVM 2.9.
|
|
for it
|
|
MemorySanitzer and ThreadSanitizer environment variables when running
lit tests.
This makes it easy suppress errors in sanitized versions of KLEE
|
|
``--silent-klee-assume=0`` is no longer passed. This ensures that we
also check that ``--silent-klee-assume`` is off by default.
|
|
infeasible assumptions.
|
|
[STPBuilder] Generate SRrem expressions correctly
|
|
This causes problems on a shared machine where multiple users are running the
KLEE unit tests.
|
|
The '%' operater in C is not Gauss Modulo
but remainder operations.
Using a negative number as right operand
can result in a negative number.
Fix appropriate SRem building
Note: MetaSMTlib implementation doesn't have that bug.
|
|
Fix signed division by constant 1/ -1
|
|
|
|
Division by constant divisor get optimized
using shift and multiplication operations in STP builder.
The used method cannot be applied for divisor 1 and -1.
In that case use slow path.
|
|
Added option to specify a different entry point from main(). Remove some whitespaces.
|
|
|
|
It failed when the function being called is a bitcasted alias.
|
|
compilation.
|
|
|
|
The test contains the program proposed by Eric Rizzi in https://github.com/klee/klee/issues/227, and shows a case in which a constant constraint results after the optimisation.
|
|
always goes to zero (matches LLVM's APInt::ashr(...)). This is meant
to partially address issue #218.
There are a few problems with this commit
* It is possible for AShrExpr to not be abbreviated because the scan
methods will not see that we print the 0th child of the AShrExpr twice
* The added test case should really be run through an SMT solver (
i.e. STP) but that requires infrastructure changes.
|
|
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.
|
