Make sharing map iteration independent of tree depth #4582
Conversation
danpoe
requested review from
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
There was a problem hiding this comment.
Looks ok to me, but given my judgement wasn't exactly spot-on on an earlier PR it would be great if @smowton could please review and approve.
| @@ -894,6 +894,8 @@ SHARING_MAPT2(, innert *)::get_container_node(const key_type &k) | |||
| key >>= chunk; | |||
| } | |||
|
|
|||
| SM_ASSERT(ip->is_container()); | |||
There was a problem hiding this comment.
Why is it not is_defined_container here?
There was a problem hiding this comment.
The non-const version of get_container_node() adds empty nodes if the key doesn't exist yet in the map. In this case, !empty() will not hold.
| @@ -378,6 +378,9 @@ TEST_CASE("Sharing map views and iteration", "[core][util]") | |||
| SECTION("Iterate") | |||
| { | |||
| sharing_map_standardt sm; | |||
|
|
|||
| sm.iterate([](const irep_idt &key, const std::string &value) {}); | |||
There was a problem hiding this comment.
So ... what does this test other than that it compiles?
There was a problem hiding this comment.
This just checks that calling iterate() on an empty map doesn't violate an internal assertion of the map.
src/util/sharing_map.h
Outdated
| std::function<void(const key_type &k, const mapped_type &m)> f) const; | ||
|
|
||
| void gather_all(const baset &n, const unsigned depth, delta_viewt &delta_view) | ||
| void gather_all(const innert &n, delta_viewt &delta_view) |
There was a problem hiding this comment.
clang-format would like the const; on this line as well.
src/util/sharing_map.h
Outdated
|
|
||
| for(const auto &l1 : ip1->get_container()) | ||
| { | ||
| const key_type &k1=l1.get_key(); |
| SM_ASSERT(!ip1->empty()); | ||
| SM_ASSERT(!ip2->empty()); | ||
|
|
||
| if(ip1->is_internal() && ip2->is_container()) |
There was a problem hiding this comment.
Why only this way around? Also, if a node is internal in tree 1 and a leaf in tree 2, why is it guaranteed to have a single child?
There was a problem hiding this comment.
The other cases are handled further down in the method.
A container node can only contain more than one element if it is at the very bottom of the tree (which happens when the hash codes of two different keys are the same). Since the corresponding node of the first map is an internal node, the node can't be at the bottom, since the bottom nodes always have to be container nodes.
There was a problem hiding this comment.
Aha, got you. Suggest putting that in a comment!
There was a problem hiding this comment.
Ok, added a comment to explain this.
danpoe
force-pushed
the
refactor/sharing-map-iteration
branch
2 times, most recently
from
d69b9bb to
0283845
Compare
Previously the depth of a node was used to determine its type. This changes the iterate() method to use is_internal() or is_container() to determine the node type instead.
danpoe
force-pushed
the
refactor/sharing-map-iteration
branch
from
0283845 to
16dae89
Compare
This makes the various methods that iterate over a sharing map independent of the depth of the nodes in the tree. This is in preparation to support variable height trees.