aboutsummaryrefslogtreecommitdiffstats
path: root/KnownState.cpp
diff options
context:
space:
mode:
authorchriseth <c@ethdev.com>2015-05-11 22:40:28 +0800
committerchriseth <c@ethdev.com>2015-05-11 22:40:28 +0800
commit2870281fe8cd70a27d69cbdc6ab97b6d48c11409 (patch)
tree77767538a766c8b3ea362c970ee6696b925e0c85 /KnownState.cpp
parent2fbcb5b9c81e7922e7cc58a4d75da12ec600e536 (diff)
downloaddexon-solidity-2870281fe8cd70a27d69cbdc6ab97b6d48c11409.tar.gz
dexon-solidity-2870281fe8cd70a27d69cbdc6ab97b6d48c11409.tar.zst
dexon-solidity-2870281fe8cd70a27d69cbdc6ab97b6d48c11409.zip
Compute state intersection.
Diffstat (limited to 'KnownState.cpp')
-rw-r--r--KnownState.cpp47
1 files changed, 35 insertions, 12 deletions
diff --git a/KnownState.cpp b/KnownState.cpp
index 41ac4802..d6fbde2d 100644
--- a/KnownState.cpp
+++ b/KnownState.cpp
@@ -160,23 +160,46 @@ KnownState::StoreOperation KnownState::feedItem(AssemblyItem const& _item, bool
return op;
}
-void KnownState::reduceToCommonKnowledge(KnownState const& /*_other*/)
+/// Helper function for KnownState::reduceToCommonKnowledge, removes everything from
+/// _this which is not in or not equal to the value in _other.
+template <class _Mapping, class _KeyType = ExpressionClasses::Id> void intersect(
+ _Mapping& _this,
+ _Mapping const& _other,
+ function<_KeyType(_KeyType)> const& _keyTrans = [](_KeyType _k) { return _k; }
+)
+{
+ for (auto it = _this.begin(); it != _this.end();)
+ if (_other.count(_keyTrans(it->first)) && _other.at(_keyTrans(it->first)) == it->second)
+ ++it;
+ else
+ it = _this.erase(it);
+}
+
+void KnownState::reduceToCommonKnowledge(KnownState const& _other)
{
- //@todo
- *this = KnownState(m_expressionClasses);
+ int stackDiff = m_stackHeight - _other.m_stackHeight;
+ function<int(int)> stackKeyTransform = [=](int _key) -> int { return _key - stackDiff; };
+ intersect(m_stackElements, _other.m_stackElements, stackKeyTransform);
+ // Use the smaller stack height. Essential to terminate in case of loops.
+ if (m_stackHeight > _other.m_stackHeight)
+ {
+ map<int, Id> shiftedStack;
+ for (auto const& stackElement: m_stackElements)
+ shiftedStack[stackElement.first - stackDiff] = stackElement.second;
+ m_stackElements = move(shiftedStack);
+ m_stackHeight = _other.m_stackHeight;
+ }
+
+ intersect(m_storageContent, _other.m_storageContent);
+ intersect(m_memoryContent, _other.m_memoryContent);
}
bool KnownState::operator==(const KnownState& _other) const
{
- //@todo
- return (
- m_stackElements.empty() &&
- _other.m_stackElements.empty() &&
- m_storageContent.empty() &&
- _other.m_storageContent.empty() &&
- m_memoryContent.empty() &&
- _other.m_memoryContent.empty()
- );
+ return m_storageContent == _other.m_storageContent &&
+ m_memoryContent == _other.m_memoryContent &&
+ m_stackHeight == _other.m_stackHeight &&
+ m_stackElements == _other.m_stackElements;
}
ExpressionClasses::Id KnownState::stackElement(int _stackHeight, SourceLocation const& _location)