Age | Commit message (Collapse) | Author |
|
Background
==========
Context-dependent objects store their older version in the pointer
`d_pContextObjRestore`. Additionally, each object is part of a
doubly-linked list of objects in the same scope (i.e. the same level).
When a scope is popped, all objects in the linked list look up their
previous version and insert themselves into the linked list at the level
of the previous version. If an object does not have an older version,
the `d_pContextObjRestore` pointer is `null` and restoring the older
version does not do anything.
When we destroy an object (which should be called from the destructor of
a context-dependent object), remove the object from all scopes by
repeatedly removing it from the current scope, restoring the older
version, removing it from the older scope and so on.
A side note: The doubly-linked lists used are somewhat unusual: Instead
of holding a pointer to the previous object, the context-dependent
objects store a pointer to the next pointer of the previous object.
Problem
=======
The mechanisms described above may be problematic under rare
circumstances. Specifically, this came up because Clang 6.0's ASAN
detected a stack-user-after-scope issue in the
`testTopScopeContextObj()` unit test in context_black.h. Note that Clang
5.0's ASAN was not able to detect this issue. In this unit test the
following happened:
1. We push our context.
2. We create two context-dependent objects: `x` at level 1 (by setting
`allocatedInCMM` to true when calling the `ContextObj` constructor) and
`y` at level 0. At this point, scope 0 has `y` in its linked list and
scope 1 has `x` in its linked list.
3. We call `makeCurrent()` on both objects. This does nothing for `x`
because it already is at level 1. For `y` it creates a backup of the
current information and inserts `y` into the scope 1. Scope 0 now has a
backup of `y` in its linked list and scope 1 has both `x` and `y` in its
linked list. Note that `x`'s `prev()` now points to `y`'s `next()`.
4. We do an additional push, another call to `makeCurrent` on both
objects, and a first `pop()`. After those operations, we have the same
state as after 3.
5. We pop our context again, which restores the original `y` in scope 0.
We now only have scope 0 with `y` in it. As described above, `x` is
untouched because there is no older version to restore.
6. We are at the end of the function and because `y` was created after
`x`, it is destroyed first (standard destruction order of stack objects
in C++). When destroying `x`, `x`'s `prev()` still points to `y`'s
`next()`, so we are doing an invalid write and ASAN complains.
Solution
========
The solution that this commit implements is fairly simple. We can detect
that `x`'s `prev()`/`next()` pointers are stale by checking whether the
objects level is greater than the context's level. If it is, we know
that this object is invalid and that we do not have any old versions to
remove. Note that this situation should be very rare because objects
with `allocatedInCMM` should usually be allocated in context memory,
where they get cleaned up automatically when the context is popped below
the level that they are associated with.
|
|
|
|
Previously, all util functions for the BV instantiator were static functions
in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding
unit test, it was therefore required to include this cpp file in order to
test these functions. This factors out these functions into a
theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h).
Asan reported errors for the corresponing unit test because of this.
|
|
Previously, all invertibility condition functions were static functions
in theory/quantifiers/bv_inverter.cpp. For the corresponding unit test,
it was therefore required to include this cpp file in order to test
these functions. This factors out these functions into a
theory/quantifiers/bv_inverter_utils.(cpp|h).
|
|
|
|
|
|
|
|
|
|
With older versions of CMake, skipped tests are reported as failures,
which is undesirable. This commit changes the CMakeLists file to only
use the `SKIP_RETURN_CODE` property if a newer version of CMake is used.
|
|
|
|
|
|
|
|
|
|
Currently, the run_regression.py script just returns 0 when we skip a
test due to a feature not supported by the current configuration.
Returning 0 marks those tests as passed. To make it more clear which
tests were skipped, this commit adds the `SKIP_RETURN_CODE` [0] property
to the regression tests and changes the regression script to return 77
for skipped tests. The feature is supported since at least CMake 3.0 [0].
For backwards compatibility with autotools, returning 77 for skipped
tests is only active when `--cmake` is passed to the run_regression.py
script.
[0] https://cmake.org/cmake/help/v3.0/prop_test/SKIP_RETURN_CODE.html
|
|
When parsing with `--strict-parsing`, we are checking whether the
operators that we encounter have been explicitly added to the
`d_logicOperators` set in the `Parser` class. We did not do that for the
indexed operator `(_ to_fp ...)` (which is represented by the kind
`FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator.
|
|
|
|
(#2562)
|
|
When using the `TS_ASSERT_THROWS` marco from CxxTest, we have to make
sure that we use a reference type for the exception, otherwise the unit
test tries to catch the exception by value, resulting in "catching
polymorphic type by value" warnings.
|
|
|
|
|
|
|
|
Right now, we are adding the Java tests even when we are not building
unit tests. This commit changes the build system to only add the Java
tests when unit tests are enabled. There are two reasons for this
change:
- building a production version of CVC4 should not require JUnit
- it seems more intuitive (to me at least) to disable JUnit tests when
unit tests are disabled
This change also simplifies building the Java bindings in our homebrew
formula.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in.
After the change, we are +61-7 on SMT LIB:
https://www.starexec.org/starexec/secure/details/job.jsp?id=30581
|
|
|
|
This commit changes the unit test for the string rewriter to use the
extended rewriter instead of the regular rewriter to make it more
robust, e.g. to different orderings in conjunctions.
|
|
|
|
|
|
|
|
Required for consistent naming of tests, unit test names now also use
the test naming scheme <category>/<subdir>/<test name>, e.g.,
unit/theory/theory_bv_white.
|
|
|
|
|
|
|
|
|
|
Targets 'check', 'units', 'systemtests' and 'regress' are now run in
parallel with the number of available cores by default. This can be
overriden by passing ARGS=-jN.
|
|
The sources of all previous libraries are now added to libcvc4 and built as
libcvc4. This removes circular dependencies between libcvc4 and libexpr.
Further, we now only have one parser library and don't build additional
libraries for each language.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|