Further improvements to dataflowanalyzer and solving proxy memptr

This commit is contained in:
hrkrshnn 2020-12-22 15:49:26 +01:00
parent b698618d03
commit f7624dff66
3 changed files with 77 additions and 5 deletions

View File

@ -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;
}

View File

@ -210,7 +210,7 @@ protected:
smtutil::Expression newVariable();
virtual smtutil::Expression newRestrictedVariable();
virtual smtutil::Expression newRestrictedVariable(bigint _maxValue = (bigint(1) << 256));
std::string uniqueName();

View File

@ -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))
// }
// }