cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #10884 from blishko/smt-refactor

Browse Source 
[SMTChecker] Small refactoring
This commit is contained in:
Leonardo 2021-02-03 17:26:53 +01:00 committed by GitHub
commit 43ce5d3f79
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 33 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libsolidity/formal/BMC.cpp
View File

@ -162,7 +162,7 @@ bool BMC::visit(FunctionDefinition const& _function)
{ {
reset(); reset();
initFunction(_function); initFunction(_function);
m_context.addAssertion(m_context.state().txTypeConstraints() && m_context.state().txFunctionConstraints(_function)); m_context.addAssertion(state().txTypeConstraints() && state().txFunctionConstraints(_function));
resetStateVariables(); resetStateVariables();
} }
@ -440,7 +440,7 @@ void BMC::endVisit(FunctionCall const& _funCall)
{ {
auto value = _funCall.arguments().front(); auto value = _funCall.arguments().front();
solAssert(value, ""); solAssert(value, "");
smtutil::Expression thisBalance = m_context.state().balance(); smtutil::Expression thisBalance = state().balance();
addVerificationTarget( addVerificationTarget(
VerificationTargetType::Balance, VerificationTargetType::Balance,
@ -561,8 +561,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
else else
{ {
m_externalFunctionCallHappened = true; m_externalFunctionCallHappened = true;
resetStateVariables(); resetStorageVariables();
resetStorageReferences();
} }
} }
@ -624,11 +623,6 @@ pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
return values; return values;
} }
void BMC::resetStorageReferences()
{
m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); });
}
void BMC::reset() void BMC::reset()
{ {
m_externalFunctionCallHappened = false; m_externalFunctionCallHappened = false;

1
libsolidity/formal/BMC.h
View File

@ -123,7 +123,6 @@ private:
Expression const& _expression Expression const& _expression
) override; ) override;
void resetStorageReferences();
void reset(); void reset();
std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> modelExpressions(); std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> modelExpressions();

8
libsolidity/formal/CHC.cpp
View File

@ -880,8 +880,7 @@ void CHC::resetContractAnalysis()
void CHC::eraseKnowledge() void CHC::eraseKnowledge()
{ {
resetStateVariables(); resetStorageVariables();
m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); });
} }
void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function) void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
@ -1691,11 +1690,6 @@ unsigned CHC::newErrorId()
return errorId; return errorId;
} }
SymbolicState& CHC::state()
{
return m_context.state();
}
SymbolicIntVariable& CHC::errorFlag() SymbolicIntVariable& CHC::errorFlag()
{ {
return state().errorFlag(); return state().errorFlag();

1
libsolidity/formal/CHC.h
View File

@ -258,7 +258,6 @@ private:
/// it into m_errorIds. /// it into m_errorIds.
unsigned newErrorId(); unsigned newErrorId();
smt::SymbolicState& state();
smt::SymbolicIntVariable& errorFlag(); smt::SymbolicIntVariable& errorFlag();
//@} //@}

33
libsolidity/formal/SMTEncoder.cpp
View File

@ -79,7 +79,7 @@ bool SMTEncoder::analyze(SourceUnit const& _source)
if (!analysis) if (!analysis)
return false; return false;
m_context.state().prepareForSourceUnit(_source); state().prepareForSourceUnit(_source);
return true; return true;
} }
@ -697,7 +697,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
visitCryptoFunction(_funCall); visitCryptoFunction(_funCall);
break; break;
case FunctionType::Kind::BlockHash: case FunctionType::Kind::BlockHash:
defineExpr(_funCall, m_context.state().blockhash(expr(*_funCall.arguments().at(0)))); defineExpr(_funCall, state().blockhash(expr(*_funCall.arguments().at(0))));
break; break;
case FunctionType::Kind::AddMod: case FunctionType::Kind::AddMod:
case FunctionType::Kind::MulMod: case FunctionType::Kind::MulMod:
@ -711,10 +711,10 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
auto const& value = args.front(); auto const& value = args.front();
solAssert(value, ""); solAssert(value, "");
smtutil::Expression thisBalance = m_context.state().balance(); smtutil::Expression thisBalance = state().balance();
setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context); setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context);
m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value)); state().transfer(state().thisAddress(), expr(address), expr(*value));
break; break;
} }
case FunctionType::Kind::ArrayPush: case FunctionType::Kind::ArrayPush:
@ -799,8 +799,8 @@ void SMTEncoder::visitRequire(FunctionCall const& _funCall)
void SMTEncoder::visitABIFunction(FunctionCall const& _funCall) void SMTEncoder::visitABIFunction(FunctionCall const& _funCall)
{ {
auto symbFunction = m_context.state().abiFunction(&_funCall); auto symbFunction = state().abiFunction(&_funCall);
auto const& [name, inTypes, outTypes] = m_context.state().abiFunctionTypes(&_funCall); auto const& [name, inTypes, outTypes] = state().abiFunctionTypes(&_funCall);
auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type); auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
auto kind = funType.kind(); auto kind = funType.kind();
@ -848,14 +848,14 @@ void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall)
auto arg0 = expr(*_funCall.arguments().at(0)); auto arg0 = expr(*_funCall.arguments().at(0));
optional<smtutil::Expression> result; optional<smtutil::Expression> result;
if (kind == FunctionType::Kind::KECCAK256) if (kind == FunctionType::Kind::KECCAK256)
result = smtutil::Expression::select(m_context.state().cryptoFunction("keccak256"), arg0); result = smtutil::Expression::select(state().cryptoFunction("keccak256"), arg0);
else if (kind == FunctionType::Kind::SHA256) else if (kind == FunctionType::Kind::SHA256)
result = smtutil::Expression::select(m_context.state().cryptoFunction("sha256"), arg0); result = smtutil::Expression::select(state().cryptoFunction("sha256"), arg0);
else if (kind == FunctionType::Kind::RIPEMD160) else if (kind == FunctionType::Kind::RIPEMD160)
result = smtutil::Expression::select(m_context.state().cryptoFunction("ripemd160"), arg0); result = smtutil::Expression::select(state().cryptoFunction("ripemd160"), arg0);
else if (kind == FunctionType::Kind::ECRecover) else if (kind == FunctionType::Kind::ECRecover)
{ {
auto e = m_context.state().cryptoFunction("ecrecover"); auto e = state().cryptoFunction("ecrecover");
auto arg0 = expr(*_funCall.arguments().at(0)); auto arg0 = expr(*_funCall.arguments().at(0));
auto arg1 = expr(*_funCall.arguments().at(1)); auto arg1 = expr(*_funCall.arguments().at(1));
auto arg2 = expr(*_funCall.arguments().at(2)); auto arg2 = expr(*_funCall.arguments().at(2));
@ -953,7 +953,7 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
defineGlobalVariable(_identifier.name(), _identifier); defineGlobalVariable(_identifier.name(), _identifier);
else if (_identifier.name() == "this") else if (_identifier.name() == "this")
{ {
defineExpr(_identifier, m_context.state().thisAddress()); defineExpr(_identifier, state().thisAddress());
m_uninterpretedTerms.insert(&_identifier); m_uninterpretedTerms.insert(&_identifier);
} }
// Ignore type identifiers // Ignore type identifiers
@ -1299,7 +1299,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
{ {
auto const& name = identifier->name(); auto const& name = identifier->name();
solAssert(name == "block" || name == "msg" || name == "tx", ""); solAssert(name == "block" || name == "msg" || name == "tx", "");
defineExpr(_memberAccess, m_context.state().txMember(name + "." + _memberAccess.memberName())); defineExpr(_memberAccess, state().txMember(name + "." + _memberAccess.memberName()));
} }
else if (auto magicType = dynamic_cast<MagicType const*>(exprType); magicType->kind() == MagicType::Kind::MetaType) else if (auto magicType = dynamic_cast<MagicType const*>(exprType); magicType->kind() == MagicType::Kind::MetaType)
{ {
@ -1360,7 +1360,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
_memberAccess.expression().accept(*this); _memberAccess.expression().accept(*this);
if (_memberAccess.memberName() == "balance") if (_memberAccess.memberName() == "balance")
{ {
defineExpr(_memberAccess, m_context.state().balance(expr(_memberAccess.expression()))); defineExpr(_memberAccess, state().balance(expr(_memberAccess.expression())));
setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_context); setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_context);
m_uninterpretedTerms.insert(&_memberAccess); m_uninterpretedTerms.insert(&_memberAccess);
return false; return false;
@ -2571,7 +2571,7 @@ void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefin
for (auto const& var: localVariablesIncludingModifiers(*_function, _contract)) for (auto const& var: localVariablesIncludingModifiers(*_function, _contract))
m_context.variable(*var)->resetIndex(); m_context.variable(*var)->resetIndex();
} }
m_context.state().reset(); state().reset();
} }
Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess) Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
@ -3009,3 +3009,8 @@ vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _f
return args; return args;
} }
smt::SymbolicState& SMTEncoder::state()
{
return m_context.state();
}

2
libsolidity/formal/SMTEncoder.h
View File

@ -424,6 +424,8 @@ protected:
/// Stores the context of the encoding. /// Stores the context of the encoding.
smt::EncodingContext& m_context; smt::EncodingContext& m_context;
smt::SymbolicState& state();
}; };
} }

8
test/libsolidity/smtCheckerTests/types/address_call.sol
View File

@ -20,8 +20,8 @@ contract C
// ---- // ----
// Warning 2072: (224-240): Unused local variable. // Warning 2072: (224-240): Unused local variable.
// Warning 4588: (244-256): Assertion checker does not yet implement this type of function call. // Warning 4588: (244-256): Assertion checker does not yet implement this type of function call.
// Warning 6328: (260-275): CHC: Assertion violation happens here. // Warning 6328: (260-275): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 6328: (279-293): CHC: Assertion violation happens here. // Warning 6328: (279-293): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 6328: (297-316): CHC: Assertion violation happens here. // Warning 6328: (297-316): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 6328: (320-344): CHC: Assertion violation happens here. // Warning 6328: (320-344): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 4588: (244-256): Assertion checker does not yet implement this type of function call. // Warning 4588: (244-256): Assertion checker does not yet implement this type of function call.

8
test/libsolidity/smtCheckerTests/types/address_delegatecall.sol
View File

@ -20,8 +20,8 @@ contract C
// ---- // ----
// Warning 2072: (224-240): Unused local variable. // Warning 2072: (224-240): Unused local variable.
// Warning 4588: (244-264): Assertion checker does not yet implement this type of function call. // Warning 4588: (244-264): Assertion checker does not yet implement this type of function call.
// Warning 6328: (268-283): CHC: Assertion violation happens here. // Warning 6328: (268-283): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 6328: (287-301): CHC: Assertion violation happens here. // Warning 6328: (287-301): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 6328: (305-324): CHC: Assertion violation happens here. // Warning 6328: (305-324): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 6328: (328-352): CHC: Assertion violation happens here. // Warning 6328: (328-352): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 4588: (244-264): Assertion checker does not yet implement this type of function call. // Warning 4588: (244-264): Assertion checker does not yet implement this type of function call.