From f7624dff66cfb9ea4957a9fa6d4f641c6e1d36f9 Mon Sep 17 00:00:00 2001
From: hrkrshnn <webmail.hari@gmail.com>
Date: Tue, 22 Dec 2020 15:49:26 +0100
Subject: [PATCH] Further improvements to dataflowanalyzer and solving proxy
 memptr

---
 libyul/optimiser/DataFlowAnalyzer.cpp         | 21 +++++--
 libyul/optimiser/DataFlowAnalyzer.h           |  2 +-
 .../yulOptimizerTests/fullSuite/proxy.yul     | 59 +++++++++++++++++++
 3 files changed, 77 insertions(+), 5 deletions(-)
 create mode 100644 test/libyul/yulOptimizerTests/fullSuite/proxy.yul

diff --git a/libyul/optimiser/DataFlowAnalyzer.cpp b/libyul/optimiser/DataFlowAnalyzer.cpp
index d6f96346e..433ebfe5e 100644
--- a/libyul/optimiser/DataFlowAnalyzer.cpp
+++ b/libyul/optimiser/DataFlowAnalyzer.cpp
@@ -20,6 +20,7 @@
  * Common Subexpression Eliminator.
  */
 
+
 #include <libyul/optimiser/DataFlowAnalyzer.h>
 
 #include <libyul/optimiser/NameCollector.h>
@@ -38,7 +39,7 @@
 #include <libevmasm/Instruction.h>
 
 #include <libsmtutil/SMTPortfolio.h>
-#include <libsmtutil/Z3Interface.h>
+#include <libsmtutil/SolverInterface.h>
 #include <libsmtutil/Helpers.h>
 #include <libyul/Utilities.h>
 #include <libsolutil/Visitor.h>
@@ -95,7 +96,10 @@ void DataFlowAnalyzer::operator()(ExpressionStatement& _statement)
 		ASTModifier::operator()(_statement);
 		set<YulString> keysToErase;
 		for (auto const& item: m_memory.values)
-			if (!m_knowledgeBase.knownToBeDifferentByAtLeast32(vars->first, item.first))
+			if (!(
+				m_knowledgeBase.knownToBeDifferentByAtLeast32(vars->first, item.first) ||
+				!invalidatesMemoryLocation(item.first, _statement.expression))
+			)
 				keysToErase.insert(item.first);
 		for (YulString const& key: keysToErase)
 			m_memory.eraseKey(key);
@@ -534,6 +538,15 @@ smtutil::Expression DataFlowAnalyzer::encodeEVMBuiltin(
 			constantValue(0),
 			arguments.at(0) / arguments.at(1)
 		);
+
+	// Restrictions from EIP-1985
+	case evmasm::Instruction::CALLDATASIZE:
+	case evmasm::Instruction::CODESIZE:
+	case evmasm::Instruction::EXTCODESIZE:
+	case evmasm::Instruction::MSIZE:
+	case evmasm::Instruction::RETURNDATASIZE:
+		return newRestrictedVariable(bigint(1) << 32);
+		break;
 	default:
 		break;
 	}
@@ -545,10 +558,10 @@ smtutil::Expression DataFlowAnalyzer::newVariable()
 	return m_solver->newVariable(uniqueName(), defaultSort());
 }
 
-smtutil::Expression DataFlowAnalyzer::newRestrictedVariable()
+smtutil::Expression DataFlowAnalyzer::newRestrictedVariable(bigint _maxValue)
 {
 	smtutil::Expression var = newVariable();
-	m_solver->addAssertion(0 <= var && var < smtutil::Expression(bigint(1) << 256));
+	m_solver->addAssertion(0 <= var && var < smtutil::Expression(_maxValue));
 	return var;
 }
 
diff --git a/libyul/optimiser/DataFlowAnalyzer.h b/libyul/optimiser/DataFlowAnalyzer.h
index 824be97ba..1a11e085d 100644
--- a/libyul/optimiser/DataFlowAnalyzer.h
+++ b/libyul/optimiser/DataFlowAnalyzer.h
@@ -210,7 +210,7 @@ protected:
 
 
 	smtutil::Expression newVariable();
-	virtual smtutil::Expression newRestrictedVariable();
+	virtual smtutil::Expression newRestrictedVariable(bigint _maxValue = (bigint(1) << 256));
 	std::string uniqueName();
 
 
diff --git a/test/libyul/yulOptimizerTests/fullSuite/proxy.yul b/test/libyul/yulOptimizerTests/fullSuite/proxy.yul
new file mode 100644
index 000000000..f5944c014
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/fullSuite/proxy.yul
@@ -0,0 +1,59 @@
+{
+    mstore(64, 128)
+    if callvalue() { revert(0, 0) }
+    let _1 := 0
+    calldatacopy(128, _1, calldatasize())
+    mstore(add(128, calldatasize()), _1)
+    pop(delegatecall(gas(), 25, 128, calldatasize(), _1, _1))
+    let data := _1
+    switch returndatasize()
+    case 0 { data := 96 }
+    default {
+        let result := and(add(returndatasize(), 63), not(31))
+        let memPtr := mload(64)
+        let newFreePtr := add(memPtr, result)
+        if or(gt(newFreePtr, 0xffffffffffffffff), lt(newFreePtr, memPtr))
+        {
+            mstore(_1, shl(224, 0x4e487b71))
+            mstore(4, 0x41)
+            revert(_1, 0x24)
+        }
+        mstore(64, newFreePtr)
+        data := memPtr
+        mstore(memPtr, returndatasize())
+        returndatacopy(add(memPtr, 0x20), _1, returndatasize())
+    }
+    return(add(data, 0x20), mload(data))
+}
+
+// ----
+// step: fullSuite
+//
+// {
+//     {
+//         let _1 := 128
+//         mstore(64, _1)
+//         if callvalue() { revert(0, 0) }
+//         let _2 := 0
+//         calldatacopy(_1, _2, calldatasize())
+//         mstore(add(_1, calldatasize()), _2)
+//         pop(delegatecall(gas(), 25, _1, calldatasize(), _2, _2))
+//         let data := _2
+//         switch returndatasize()
+//         case 0 { data := 96 }
+//         default {
+//             let newFreePtr := add(_1, and(add(returndatasize(), 63), not(31)))
+//             if or(gt(newFreePtr, 0xffffffffffffffff), lt(newFreePtr, _1))
+//             {
+//                 mstore(_2, shl(224, 0x4e487b71))
+//                 mstore(4, 0x41)
+//                 revert(_2, 0x24)
+//             }
+//             mstore(64, newFreePtr)
+//             data := _1
+//             mstore(_1, returndatasize())
+//             returndatacopy(160, _2, returndatasize())
+//         }
+//         return(add(data, 0x20), mload(data))
+//     }
+// }