| Age | Commit message (Collapse) | Author |
|---|
|
Add some missing header to silence
compiler warnings
|
|
|
|
|
|
|
|
details.
|
|
also test a negative constant as the lhs.
|
|
|
|
|
|
[Core] Always warn if states get deleted due to memory limits
|
|
|
|
|
|
|
|
between arrays created at the same location but with different sizes
|
|
|
|
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.
|
|
than writing "(not (= a b))". This makes the code simpler and queries
slightly simpler.
|
|
|
|
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.
|
|
|
|
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
|
|
|
|
klee: let user override path to runtime library
|
|
ExprSMTLIBPrinter
|
|
|
|
|
|
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.
|
|
Fix overshift check
|
|
Handling overshift behaviour in MetaSMTBuilder
|
|
Shifting by bitwidth-1 is valid
|
|
Fixed test /Feature/PreferCex.c: Z3 instantiates different value for unc...
|
|
|
|
unconstrained buf[3]
|
|
unordered_map and unordered_set from leaking out into other compilation
units. This should be removed entirely when C++11 support lands.
|
|
|
|
|
|
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()
|
|
When looking for runtime library, look first
into KLEE_RUNTIME_LIBRARY_PATH environment variable.
This allows to use klee not only in 'hardcoded' environment.
Signed-off-by: Marek Chalupa <mchqwerty@gmail.com>
|
|
|
|
tools: prepend DESTDIR when installing
|
|
Some tools prepend DESTDIR properly, some not. ktest-tool and
klee-stats do not, so 'make install' chokes with an error:
llvm[2]: Installing Release+Asserts /usr/bin/ktest-tool
/usr/bin/install: cannot create regular file '/usr/bin/ktest-tool': Permission denied
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Allow stp installed in root
|
|
configure/Makefile code that adds Boost as a depdendency because We
don't need to support old versions of STP that needed Boost.
|
|
I have stp in standard paths: /usr/include and /usr/lib64. Allow that
by correct STP_CFLAGS + STP_LDFLAGS instead of STP_ROOT. Those are
empty when --with-stp is not passed.
configure is regenerated by autoconf too.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
