| Age | Commit message (Collapse) | Author |
|---|
|
with -m32 (i.e. for i386). Previously if this was attempt allocations
in the program being executed by KLEE would hit an assertion because
malloc() would return an address that doesn't fit in a 32-bit pointer.
The interface of MemoryManager has been changed so that it is necessary
to specify the pointer size on creation. The implementation has been
changed to use a MASSIVE HACK when the pointer width is less than
64-bits.
|
|
``__VERIFIER_assert()`` which conflicts with ours. Remove their
implementation if it is detected.
|
|
the --svcomp-runtime flag. This is accompanied with a set of tests
to check all the functions are callable.
Due to the fact that the SV-COMP benchmark suite contains a mixture
of i386 and x86_64 benchmarks it is necessary to compile the runtime
functions twice, once for i386 and once for x86_64 and then link the
right version in at runtime. An example function that is problematic
is ``__VERIFIER_nondet_long()`` which is a different size on i386
and x86_64.
|
|
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.
|
|
Fix assertion failure in getDirectCallTarget
|
|
New version of the get initial values functionality which makes use of the independent solver.
|
|
Option --readable-posix-inputs used to turn on/off POSIX-related CEX preferences
|
|
The super-set check in the CexCachingSolver takes MUCH longer than the
sub-set check. Upon closer inspection, the super-set check gets slower
and slower as more counterexamples fill the UBTree. Pretty quickly,
the cost of the super-set check becomes larger than the time required
to simply bypass it and go to the Solver.
|
|
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.
|
|
It failed when the function being called is a bitcasted alias.
|
|
and kleaver.
|
|
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
|
|
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.
|
|
the optimisation that rewrites existing constraints when an equality with a constant is added
|
|
|
|
|
|
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
|
|
This function should be used solely in assertion statements and is
intended as a sanity check to make sure that the solution constructed
by IndependentSolver::getInitialValues() produces and answer that in
fact satisfies the the query.
|
|
Previous implementation simply passed the entire constraint forward
without any factoring of the constraint at all. This is a problem
since it is highly likely that there are cached solutions to pieces
of the constraint. The new implementation breaks the entire
constraint down into its requisite factors and passes each piece
forward, one by one, down the solver chain. After an answer is
returned, it is integrated into a larger solution. Since, by
definition, no factor can affect another, we can safely create a
solution to the larger constraint from the answers of its smaller
pieces.
The reconstruction of the solution is done by analyzing which parts of
an array a factor touches. If the factor is the only one to reference
a particular array, then all of the values calculated in the solution
for that array are included in the final answer. If the factor
references a particular element of the array (for example, arr[1]),
then only the value in index 1 of array arr will be included in the
solution.
|
|
This functionality is necessary in order to more effectively handle
calls to IndependentSolver::getInitialValues. An incoming query will
be broken down into its smaller parts, and each piece will be solved
for. At the end, the pieces will be recombined into a larger solution.
The IndependentElementSet::getAllFactors() method takes a query and
breaks it down into all of it's non-interacting factors. The
IndependentElementSet::calculateArrays() method calculates which
arrays are involved in a particular factor.
|
|
|
|
|
|
|
|
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.
|
|
|
|
This is important for future changes to IndependentSolver::
getInitialValues() so that an incoming constraint can be broken
down into its smallest possible parts. Each of these individual
parts may then be solved for and then the solutions to each piece
combined to create a final answer.
Finally, several fields which had previously been private are now
public to facilitate the smaller solutions being combined into a
larger solution.
|
|
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
|
|
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
|
|
Shifting by bitwidth-1 is valid
|
|
|
|
|
