cerc-io/solidity
11
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

[SMTChecker] Added transaction constraints also for contract deployment

Browse Source
This commit is contained in:
Martin Blicha
2021-02-01 16:46:34 +01:00
committed by Martin Blicha
parent c7d1e1911e
commit a49950cdf3
47 changed files with 1378 additions and 1147 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+1 -1
View File
@@ -162,7 +162,7 @@ bool BMC::visit(FunctionDefinition const& _function)
{
reset();
initFunction(_function);
m_context.addAssertion(m_context.state().txConstraints(_function));
m_context.addAssertion(m_context.state().txTypeConstraints() && m_context.state().txFunctionConstraints(_function));
resetStateVariables();
}
libsolidity/formal/CHC.cpp
+8 -4
View File
@@ -196,8 +196,12 @@ void CHC::endVisit(ContractDefinition const& _contract)
connectBlocks(m_currentBlock, summary(_contract));
setCurrentBlock(*m_constructorSummaries.at(&_contract));
m_queryPlaceholders[&_contract].push_back({smtutil::Expression(true), errorFlag().currentValue(), m_currentBlock});
connectBlocks(m_currentBlock, interface(), errorFlag().currentValue() == 0);
auto constructor = _contract.constructor();
auto txConstraints = state().txTypeConstraints();
if (!constructor || !constructor->isPayable())
txConstraints = txConstraints && state().txNonPayableConstraint();
m_queryPlaceholders[&_contract].push_back({txConstraints, errorFlag().currentValue(), m_currentBlock});
connectBlocks(m_currentBlock, interface(), txConstraints && errorFlag().currentValue() == 0);
SMTEncoder::endVisit(_contract);
}
@@ -262,7 +266,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
{
auto sum = summary(_function);
auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
auto txConstraints = m_context.state().txConstraints(_function);
auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(_function);
m_queryPlaceholders[&_function].push_back({txConstraints && sum, errorFlag().currentValue(), ifacePre});
connectBlocks(ifacePre, interface(), txConstraints && sum && errorFlag().currentValue() == 0);
}
@@ -738,7 +742,7 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
smtutil::Expression pred = predicate(_funCall);
auto txConstraints = m_context.state().txConstraints(*function);
auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(*function);
m_context.addAssertion(pred && txConstraints);
// restore the original transaction data
state().newTx();
libsolidity/formal/SymbolicState.cpp
+11 -5
View File
@@ -126,9 +126,9 @@ smtutil::Expression SymbolicState::txMember(string const& _member) const
return m_tx.member(_member);
}
smtutil::Expression SymbolicState::txConstraints(FunctionDefinition const& _function) const
smtutil::Expression SymbolicState::txTypeConstraints() const
{
smtutil::Expression conj = smt::symbolicUnknownConstraints(m_tx.member("block.chainid"), TypeProvider::uint256()) &&
return smt::symbolicUnknownConstraints(m_tx.member("block.chainid"), TypeProvider::uint256()) &&
smt::symbolicUnknownConstraints(m_tx.member("block.coinbase"), TypeProvider::address()) &&
smt::symbolicUnknownConstraints(m_tx.member("block.difficulty"), TypeProvider::uint256()) &&
smt::symbolicUnknownConstraints(m_tx.member("block.gaslimit"), TypeProvider::uint256()) &&
@@ -138,14 +138,20 @@ smtutil::Expression SymbolicState::txConstraints(FunctionDefinition const& _func
smt::symbolicUnknownConstraints(m_tx.member("msg.value"), TypeProvider::uint256()) &&
smt::symbolicUnknownConstraints(m_tx.member("tx.origin"), TypeProvider::address()) &&
smt::symbolicUnknownConstraints(m_tx.member("tx.gasprice"), TypeProvider::uint256());
}
smtutil::Expression SymbolicState::txNonPayableConstraint() const
{
return m_tx.member("msg.value") == 0;
}
smtutil::Expression SymbolicState::txFunctionConstraints(FunctionDefinition const& _function) const
{
smtutil::Expression conj = _function.isPayable() ? smtutil::Expression(true) : txNonPayableConstraint();
if (_function.isPartOfExternalInterface())
{
auto sig = TypeProvider::function(_function)->externalIdentifier();
conj = conj && m_tx.member("msg.sig") == sig;
if (!_function.isPayable())
conj = conj && m_tx.member("msg.value") == 0;
auto b0 = sig >> (3 * 8);
auto b1 = (sig & 0x00ff0000) >> (2 * 8);
auto b2 = (sig & 0x0000ff00) >> (1 * 8);
libsolidity/formal/SymbolicState.h
+3 -1
View File
@@ -126,7 +126,9 @@ public:
smtutil::SortPointer const& txSort() const { return m_tx.sort(); }
void newTx() { m_tx.newVar(); }
smtutil::Expression txMember(std::string const& _member) const;
smtutil::Expression txConstraints(FunctionDefinition const& _function) const;
smtutil::Expression txFunctionConstraints(FunctionDefinition const& _function) const;
smtutil::Expression txTypeConstraints() const;
smtutil::Expression txNonPayableConstraint() const;
smtutil::Expression blockhash(smtutil::Expression _blockNumber) const;
//@}