| Age | Commit message (Collapse) | Author |
|---|
|
My first attempt in b41cf33b6b726fd97e502c5c4818f5feeea0284b was wrong
because setting the CC and CXX Makefile variables in Makefile.config.in did not
work because LLVM's Makefile.config would override them.
Also detecting the C compiler is unnecessary because we already do this
(bitcode compiler detection)
|
|
|
|
|
|
runtime was incorrect.
|
|
the optimisation that rewrites existing constraints when an equality with a constant is added
|
|
needed by Clang.
|
|
ignore the C++ compiler detected and just use the compiler detected
during the LLVM configure.
|
|
fix travis build of upstream STP and also how KLEE links against STP.
|
|
|
|
|
|
|
|
Cleaner, more efficient timestamps
|
|
pull request.
This reverts commit badffc570e1be6b675dcab7e21829bd029c46287.
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
Use correct definition and declaration of main function
|
|
|
|
|
|
Add some missing header to silence
compiler warnings
|
|
|
|
|
|
|
|
details.
|
|
also test a negative constant as the lhs.
|
|
|
|
|
|
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.
|
|
[Core] Always warn if states get deleted due to memory limits
|
|
|
|
|
|
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.
|
|
|
|
|
|
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.
|
