The shape of a sharing map is now different than before, as now leafs can be
directly attached to internal nodes. This adapts the various unit tests that
check that the map has a certain shape.
Previously the leaf nodes were a separate type, and internal nodes and container
nodes were represented by the same type. This changes the representation such
that all nodes are represented by sharing_nodet. This will allow an internal
node to directly point to a leaf node (instead of having to point to a container
node which in turn points to a leaf node).
This reduces the size of an irept by 5 pointers (i.e., 40 bytes on
64-bit systems). On SV-COMP's ReachSafety-ECA with this change we can
perform 3819.81 symex_step calls per second, compared to 2752.28 calls
per second with the std::map configuration. The performance improvements
are spread across various `irept`-related operations.
We were doing this in multiple places, this should make it a bit easier to keep
set properties consistent among different places.
Ideally we could eventually move away from mentioning targets from modules here
on the top level (and instead have each module call cprover_default_properties)
but this isn't done in this commit.
Because memory analyzer depends on GDB being present and further uses platform
specific functionality at the moment it had some ifdef functionality to disable
itself.
This made the code a bit more complicated than it needed to be, and also lead to
the code effectively building defunct executables. This removes these ifdefs and
instead excludes memory-analyzer (and related tests) from the build unless
requested (via WITH_MEMORY_ANALYZER environment variable or CMake option
depending on whether it is a Make or CMake build respectively).
Also force building memory-analyzer on Linux and test it there by
default (unless explicitly unset). Behaviour on other platforms should be
preserved.
This update the gdb api to return more information about pointers (via the
method get_memory() which returns an object of type pointer_valuet describing
the pointer and pointed-to data). Unit tests for the new functionality are
included.
This replaces small_shared_two_way_ptrt with small_shared_n_way_ptrt. The new
shared pointer type allows more than two types for the managed objects. This can
be useful e.g. for implementing graph data structures with sharing where there
are more than two different node types.
1) pointer_object((T1 *)NULL) equals pointer_object((T2 *)NULL) for any
types T1, T2. Previously, this would return false, unless T1==T2.
2) Do not restrict the above to NULL, but instead let the existing logic
in simplify_inequality fully simplify this.
3) Add a unit test of this code, which highlighted further bugs and
limitations: the unit test previously did not set the instance of the
desired dynamic object, and address-of inequalities over dynamic objects
can also be simplified.
On some SV-COMP benchmark categories, hashing accounts for >20% of CPU
time (with profiling enabled) - top five:
* ReachSafety-BitVectors: 29.29% (470.54 seconds, which reduces to 4.39
seconds; for benchmarks not timing out we save 170 seconds (25%) in
non-profiling mode)
* Systems_BusyBox_NoOverflows: 27.98% (284.15 seconds, which reduces to
1.74 seconds; for the 1 benchmark not timing out we save 23 seconds
(6%) in non-profiling mode)
* Systems_BusyBox_MemSafety: 24.24% (194.74 seconds, which reduces to
0.93 seconds; no measurable difference on the 2 benchmarks not
failing/timing out)
* NoOverflows-Other: 18.84% (1127.61 seconds, which reduces to
23.57 seconds; for benchmarks not timing out we save 5 seconds (7%) in
non-profiling mode)
* ReachSafety-ControlFlow: 17.75% (1194.04 seconds, which reduces to
29.17 seconds; for benchmarks not timing out we save 200 seconds (25%)
in non-profiling mode)
For ReachSafety-ECA it's only 4.7%, which still amounts to 3006.7
seconds. With this change this reduces to 323.07 seconds. On
ReachSafety-ECA, this enables 3055.35 symex_step calls per second over
2752.28 calls per second without this change.
The previous implementation only supported codepoints up to 0x7f as
characters, and all remaining codepoints up to 0xff as integers.
The new implementation supports all codepoints in the BMP, i.e. up to
0xffff.
Previously, if a JSON file contained a string in hexadecimal Unicode
representation, e.g. "\u0001", the JSON parser would discard the "\u"
part and store the string as "0001". This commit fixes this so the
resulting string is equal to "\u0001".
This adds sharing map unit tests to check that operations fail as expected. For
example, calling map.replace(key, value) when the key does not exist in the map
should fail.
This adds unit tests to check that the references into the sharing map in the
views and delta views remain valid after operations erase(), insert(), and
replace(). The references should remain valid to those elements that are not
changed by the respective operations.
This permits an in-place update, avoiding needless copy-out / mutate / move-in cycles for
expensive-to-copy value types without leaking a non-const reference to a value.
These were accidentally disabled when distinguishing ID_is_dynamic_object (a predicate that tests
whether an object is dynamic) from ID_dynamic_object (a reference to the object itself, similar to
symbol_exprt). I also take the opportunity to restore pretty-printing of dynamic object expressions
(while also keeping pretty-printing of the predicate).
Previously we fixed the extracted bytes to be unsigned bitvectors, but
we should not actually impose (un)signedness as we do not actually
interpret the bytes as numeric values. This fixes byte operators over
floating-point values, and makes various SMT-solver tests pass as the
SMT back-end is more strict about typing and therefore was more
frequently affected by this bug.
To make all this work it was also necessary to extend and fix the
simplifier's handling of bv_typet expressions, and also cover one more
case of type casts in the bitvector back-end.
The tests
Array_operations1/test.desc
Float-equality1/test_no_equality.desc
memory_allocation1/test.desc
union12/test.desc
union6/test.desc
union7/test.desc
continue to fail on Windows and thus cannot yet be enabled.
check_for_gdb() could only return true since if the gdb invocation in its body
failed a REQUIRE(...) in its body would fail. This changes check_for_gdb() the
return type of check_for_gdb() to void and refactors its callees.
Previously when sharing_map.erase(key) was called, two traversals of the path to
the leaf to erase were done. One to check whether the key was in the map, and if
it was, a second one to copy and detach the nodes on the path to the leaf to
erase. This commit changes erase() to require that the given key exists in the
map. This simplifies the implementation and avoids two traversals of the path to
the leaf to erase when it is known that the key exists. If it is not known
whether the key exists, sharing_map.has_key(key) should be explicitely called
first.
Michael Tautschnig