Skip to content

Commit 1d701f5

Browse files
authored
Minor optimization to search (#1170)
In the final version of the ULM, we want to enforce that semantics are deterministic. We do this using the search feature and the `--execute-to-branch` option which treats all states with more than one successor as final states and does not rewrite them further. I tested this by running the ethereum test suite with this option and all the tests passed (with a few trivial changes to the semantics). A minor change resulted from this effort: if only a single state is active at a given time, we do not need to do the expensive equality check performed by `erase`. It is sufficient to simply clear the hash set.
1 parent 3a0b23d commit 1d701f5

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

runtime/util/search.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,11 @@ std::unordered_set<block *, hash_block, k_eq> take_search_steps(
7272
while (!states.empty() && depth != 0) {
7373
state = states.front();
7474
states.pop_front();
75-
states_set.erase(state);
75+
if (states.empty()) {
76+
states_set.clear();
77+
} else {
78+
states_set.erase(state);
79+
}
7680

7781
if (depth > 0) {
7882
depth--;

0 commit comments

Comments
 (0)