| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.
|
|
to have only solver options.
|
|
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...
|
|
Some of these leaks were introduced by the factory constructor for Array
objects (f049ff3bc04daead8c3bb9f06e89e71e2054c82a) but a few others have
been around for far longer.
This leak was fixed by introducing a ``ArrayCache`` object which has two
purposes
* Retains ownership of all created ``Array`` objects and destroys them when
the ``ArrayCache`` destructor is called.
* Mimic the caching behaviour for symbolic arrays that was introduced
by f049ff3bc04daead8c3bb9f06e89e71e2054c82a where arrays with the same
name and size get "uniqued".
The Executor now maintains a ``arrayCache`` member that it uses and
passes by pointer to objects that need to construct ``Array`` objects (i.e.
``ObjectState``). This way when the Executor is destroyed all the
``Array`` objects get freed which seems like the right time to do this.
For Kleaver the ``ParserImpl`` has a ``TheArrayCache`` member that is
used for building ``Array`` objects. This means that the Parser must
live as long as the built expressions will be used otherwise we will
have a use after free. I'm not sure this is the right design choice.
It might be better to transfer ownership of the ``Array`` objects to
the root ``Decl`` returned by the parser.
|
|
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.
|
|
|
|
- Includes patch by Michael Stone!
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@80665 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- The sole remaining client was IVC, which is currently disabled for other
correctness issues. I patched it to compile and left a FIXME that we will
have to resolve this before we can reenable IVC.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73129 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73128 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
constructors I missed.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73127 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Lots more tweaks, documentation, and web page content is needed,
but this should compile & work on OS X & Linux.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
|
