| 223 | } |
| 224 | |
| 225 | void KnownState::reduceToCommonKnowledge(KnownState const& _other, bool _combineSequenceNumbers) |
| 226 | { |
| 227 | int stackDiff = m_stackHeight - _other.m_stackHeight; |
| 228 | for (auto it = m_stackElements.begin(); it != m_stackElements.end();) |
| 229 | if (_other.m_stackElements.count(it->first - stackDiff)) |
| 230 | { |
| 231 | Id other = _other.m_stackElements.at(it->first - stackDiff); |
| 232 | if (it->second == other) |
| 233 | ++it; |
| 234 | else |
| 235 | { |
| 236 | std::set<u256> theseTags = tagsInExpression(it->second); |
| 237 | std::set<u256> otherTags = tagsInExpression(other); |
| 238 | if (!theseTags.empty() && !otherTags.empty()) |
| 239 | { |
| 240 | theseTags.insert(otherTags.begin(), otherTags.end()); |
| 241 | it->second = tagUnion(theseTags); |
| 242 | ++it; |
| 243 | } |
| 244 | else |
| 245 | it = m_stackElements.erase(it); |
| 246 | } |
| 247 | } |
| 248 | else |
| 249 | it = m_stackElements.erase(it); |
| 250 | |
| 251 | // Use the smaller stack height. Essential to terminate in case of loops. |
| 252 | if (m_stackHeight > _other.m_stackHeight) |
| 253 | { |
| 254 | std::map<int, Id> shiftedStack; |
| 255 | for (auto const& stackElement: m_stackElements) |
| 256 | shiftedStack[stackElement.first - stackDiff] = stackElement.second; |
| 257 | m_stackElements = std::move(shiftedStack); |
| 258 | m_stackHeight = _other.m_stackHeight; |
| 259 | } |
| 260 | |
| 261 | intersect(m_storageContent, _other.m_storageContent); |
| 262 | intersect(m_memoryContent, _other.m_memoryContent); |
| 263 | if (_combineSequenceNumbers) |
| 264 | m_sequenceNumber = std::max(m_sequenceNumber, _other.m_sequenceNumber); |
| 265 | } |
| 266 | |
| 267 | bool KnownState::operator==(KnownState const& _other) const |
| 268 | { |