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 #9845 from ethereum/smt_state

Browse Source 
[SMTChecker] Add `this` and blockchain state to CHC
This commit is contained in:
Leonardo 2020-10-12 13:02:54 +02:00 committed by GitHub
commit e5fe524786
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
19 changed files with 341 additions and 123 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
libsolidity/formal/BMC.cpp
View File

@ -396,7 +396,6 @@ void BMC::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::Send:
case FunctionType::Kind::Transfer:
{
SMTEncoder::endVisit(_funCall);
auto value = _funCall.arguments().front();
solAssert(value, "");
smtutil::Expression thisBalance = m_context.state().balance();
@ -406,6 +405,8 @@ void BMC::endVisit(FunctionCall const& _funCall)
thisBalance < expr(*value),
&_funCall
);
SMTEncoder::endVisit(_funCall);
break;
}
case FunctionType::Kind::AddMod:

69
libsolidity/formal/CHC.cpp
View File

@ -101,7 +101,7 @@ bool CHC::visit(ContractDefinition const& _contract)
solAssert(m_currentContract, "");
m_constructorSummaryPredicate = createSymbolicBlock(
constructorSort(*m_currentContract),
constructorSort(*m_currentContract, state()),
"summary_constructor_" + contractSuffix(_contract),
PredicateType::ConstructorSummary,
&_contract
@ -114,15 +114,16 @@ bool CHC::visit(ContractDefinition const& _contract)
void CHC::endVisit(ContractDefinition const& _contract)
{
auto implicitConstructorPredicate = createSymbolicBlock(
implicitConstructorSort(),
implicitConstructorSort(state()),
"implicit_constructor_" + contractSuffix(_contract),
PredicateType::ImplicitConstructor,
&_contract
);
auto implicitConstructor = (*implicitConstructorPredicate)({});
addRule(implicitConstructor, implicitConstructor.name);
m_currentBlock = implicitConstructor;
m_context.addAssertion(errorFlag().currentValue() == 0);
addRule(
(*implicitConstructorPredicate)({0, state().thisAddress(), state().state()}),
implicitConstructorPredicate->functor().name
);
setCurrentBlock(*implicitConstructorPredicate);
if (auto constructor = _contract.constructor())
constructor->accept(*this);
@ -178,6 +179,7 @@ bool CHC::visit(FunctionDefinition const& _function)
m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var));
for (auto const& var: _function.parameters())
m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var));
m_context.addAssertion(state().state(0) == state().state());
connectBlocks(functionPred, bodyPred);
@ -215,7 +217,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id());
solAssert(m_currentContract, "");
auto constructorExit = createSymbolicBlock(
constructorSort(*m_currentContract),
constructorSort(*m_currentContract, state()),
"constructor_exit_" + suffix,
PredicateType::ConstructorSummary,
m_currentContract
@ -234,7 +236,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
setCurrentBlock(*m_interfaces.at(m_currentContract));
auto ifacePre = (*m_interfaces.at(m_currentContract))(initialStateVariables());
auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
if (_function.isPublic())
{
addAssertVerificationTarget(&_function, ifacePre, sum, assertionError);
@ -598,15 +600,21 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
for (auto var: function->returnParameters())
m_context.variable(*var)->increaseIndex();
auto preCallState = currentStateVariables();
auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall ||
function->stateMutability() == StateMutability::Pure ||
function->stateMutability() == StateMutability::View;
if (!usesStaticCall)
{
state().newState();
for (auto const* var: m_stateVariables)
m_context.variable(*var)->increaseIndex();
}
auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables());
auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + postCallState);
// TODO this could instead add the summary of the called function, where that summary
// basically has the nondet interface of this summary as a constraint.
m_context.addAssertion(nondet);
m_context.addAssertion(errorFlag().currentValue() == 0);
@ -775,6 +783,8 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
for (auto const& var: _function->localVariables())
m_context.variable(*var)->increaseIndex();
}
state().newState();
}
void CHC::setCurrentBlock(Predicate const& _block)
@ -800,7 +810,7 @@ set<frontend::Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTN
SortPointer CHC::sort(FunctionDefinition const& _function)
{
return functionSort(_function, m_currentContract);
return functionSort(_function, m_currentContract, state());
}
SortPointer CHC::sort(ASTNode const* _node)
@ -809,7 +819,7 @@ SortPointer CHC::sort(ASTNode const* _node)
return sort(*funDef);
solAssert(m_currentFunction, "");
return functionBodySort(*m_currentFunction, m_currentContract);
return functionBodySort(*m_currentFunction, m_currentContract, state());
}
Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node)
@ -825,8 +835,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
{
string suffix = contract->name() + "_" + to_string(contract->id());
m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract), "interface_" + suffix, PredicateType::Interface, contract);
m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract), "nondet_interface_" + suffix, PredicateType::NondetInterface, contract);
m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + suffix, PredicateType::Interface, contract);
m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + suffix, PredicateType::NondetInterface, contract);
for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*contract))
if (!m_context.knownVariable(*var))
@ -836,8 +846,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
/// 0 steps to be taken, used as base for the inductive
/// rule for each function.
auto const& iface = *m_nondetInterfaces.at(contract);
auto state0 = stateVariablesAtIndex(0, *contract);
addRule(iface(state0 + state0), "base_nondet");
addRule(smt::nondetInterface(iface, *contract, m_context, 0, 0), "base_nondet");
for (auto const* base: contract->annotation().linearizedBaseContracts)
for (auto const* function: base->definedFunctions())
@ -861,12 +870,13 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
auto state1 = stateVariablesAtIndex(1, *contract);
auto state2 = stateVariablesAtIndex(2, *contract);
auto nondetPre = iface(state0 + state1);
auto nondetPost = iface(state0 + state2);
auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
vector<smtutil::Expression> args{errorFlag().currentValue()};
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().state(1)};
args += state1 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
vector<smtutil::Expression>{state().state(2)} +
state2 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) +
applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
@ -930,7 +940,7 @@ Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType,
Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract)
{
auto block = createSymbolicBlock(
functionSort(_function, &_contract),
functionSort(_function, &_contract, state()),
"summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract),
PredicateType::FunctionSummary,
&_function
@ -1042,7 +1052,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
return smtutil::Expression(true);
errorFlag().increaseIndex();
vector<smtutil::Expression> args{errorFlag().currentValue()};
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().state()};
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
solAssert(funType.kind() == FunctionType::Kind::Internal, "");
@ -1058,11 +1068,17 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
auto const* calledContract = contract->isLibrary() ? contract : m_currentContract;
solAssert(calledContract, "");
bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View;
args += currentStateVariables(*calledContract);
args += symbolicArguments(_funCall);
if (!calledContract->isLibrary())
if (!calledContract->isLibrary() && !usesStaticCall)
{
state().newState();
for (auto const& var: m_stateVariables)
m_context.variable(*var)->increaseIndex();
}
args += vector<smtutil::Expression>{state().state()};
args += currentStateVariables(*calledContract);
for (auto var: function->parameters() + function->returnParameters())
@ -1152,7 +1168,7 @@ void CHC::addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type
addVerificationTarget(_scope, _type, summary(*m_currentContract), smtutil::Expression(true), _errorId);
else
{
auto iface = (*m_interfaces.at(m_currentContract))(initialStateVariables());
auto iface = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
auto sum = summary(*m_currentFunction);
addVerificationTarget(_scope, _type, iface, sum, _errorId);
}
@ -1444,7 +1460,12 @@ unsigned CHC::newErrorId(frontend::Expression const& _expr)
return errorId;
}
SymbolicState& CHC::state()
{
return m_context.state();
}
SymbolicIntVariable& CHC::errorFlag()
{
return m_context.state().errorFlag();
return state().errorFlag();
}

1
libsolidity/formal/CHC.h
View File

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

20
libsolidity/formal/Predicate.cpp
View File

@ -161,9 +161,9 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
auto const* fun = programFunction();
solAssert(fun, "");
/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
/// The signature of a function summary predicate is: summary(error, this, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in preInputVars.
vector<string>::const_iterator first = _args.begin() + static_cast<int>(stateVars->size()) + 1;
vector<string>::const_iterator first = _args.begin() + 3 + static_cast<int>(stateVars->size());
vector<string>::const_iterator last = first + static_cast<int>(fun->parameters().size());
solAssert(first >= _args.begin() && first <= _args.end(), "");
solAssert(last >= _args.begin() && last <= _args.end(), "");
@ -188,8 +188,8 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
/// The signature of an implicit constructor summary predicate is: summary(error, postStateVars).
/// The signature of a function summary predicate is: summary(error, this, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of an implicit constructor summary predicate is: summary(error, this, postBlockchainState, postStateVars).
/// Here we are interested in postStateVars.
auto stateVars = stateVariables();
@ -199,12 +199,12 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
vector<string>::const_iterator stateLast;
if (auto const* function = programFunction())
{
stateFirst = _args.begin() + 1 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size());
stateFirst = _args.begin() + 3 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else if (programContract())
{
stateFirst = _args.begin() + 1;
stateFirst = _args.begin() + 3;
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else
@ -220,7 +220,7 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
/// The signature of a function summary predicate is: summary(error, this, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in postInputVars.
auto const* function = programFunction();
solAssert(function, "");
@ -230,7 +230,7 @@ vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) co
auto const& inParams = function->parameters();
vector<string>::const_iterator first = _args.begin() + 1 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size());
vector<string>::const_iterator first = _args.begin() + 3 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
vector<string>::const_iterator last = first + static_cast<int>(inParams.size());
solAssert(first >= _args.begin() && first <= _args.end(), "");
@ -243,7 +243,7 @@ vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) co
vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
/// The signature of a function summary predicate is: summary(error, this, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in outputVars.
auto const* function = programFunction();
solAssert(function, "");
@ -253,7 +253,7 @@ vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) c
auto const& inParams = function->parameters();
vector<string>::const_iterator first = _args.begin() + 1 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2;
vector<string>::const_iterator first = _args.begin() + 3 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
solAssert(first >= _args.begin() && first <= _args.end(), "");

44
libsolidity/formal/PredicateInstance.cpp
View File

@ -27,10 +27,35 @@ using namespace solidity::smtutil;
namespace solidity::frontend::smt
{
smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
{
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.state(0)};
return _pred(stateExprs + initialStateVariables(_contract, _context));
}
smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
{
return _pred(currentStateVariables(_contract, _context));
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.state()};
return _pred(stateExprs + currentStateVariables(_contract, _context));
}
smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx)
{
return _pred(
vector<smtutil::Expression>{_context.state().state(_preIdx)} +
stateVariablesAtIndex(_preIdx, _contract, _context) +
vector<smtutil::Expression>{_context.state().state(_postIdx)} +
stateVariablesAtIndex(_postIdx, _contract, _context)
);
}
smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext& _context)
{
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state(0)};
return _pred(stateExprs);
}
smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
@ -38,16 +63,9 @@ smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const
if (auto const* constructor = _contract.constructor())
return _pred(currentFunctionVariables(*constructor, &_contract, _context));
return _pred(
vector<smtutil::Expression>{_context.state().errorFlag().currentValue()} +
currentStateVariables(_contract, _context)
);
}
/// Currently it does not have arguments but it will have tx data in the future.
smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext&)
{
return _pred({});
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state()};
return _pred(stateExprs + currentStateVariables(_contract, _context));
}
smtutil::Expression function(
@ -99,9 +117,11 @@ vector<smtutil::Expression> currentFunctionVariables(
EncodingContext& _context
)
{
vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue()};
auto& state = _context.state();
vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.state(0)};
exprs += _contract ? initialStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
exprs += vector<smtutil::Expression>{state.state()};
exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });

4
libsolidity/formal/PredicateInstance.h
View File

@ -30,8 +30,12 @@ class EncodingContext;
* The predicates follow the specification in PredicateSort.h.
* */
smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx);
smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);

31
libsolidity/formal/PredicateSort.cpp
View File

@ -28,49 +28,54 @@ using namespace solidity::smtutil;
namespace solidity::frontend::smt
{
SortPointer interfaceSort(ContractDefinition const& _contract)
SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
{
return make_shared<FunctionSort>(
stateSorts(_contract),
vector<SortPointer>{_state.thisAddressSort(), _state.stateSort()} + stateSorts(_contract),
SortProvider::boolSort
);
}
SortPointer nondetInterfaceSort(ContractDefinition const& _contract)
SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
{
auto varSorts = stateSorts(_contract);
vector<SortPointer> stateSort{_state.stateSort()};
return make_shared<FunctionSort>(
varSorts + varSorts,
stateSort + varSorts + stateSort + varSorts,
SortProvider::boolSort
);
}
SortPointer implicitConstructorSort()
SortPointer implicitConstructorSort(SymbolicState& _state)
{
return arity0FunctionSort();
return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()},
SortProvider::boolSort
);
}
SortPointer constructorSort(ContractDefinition const& _contract)
SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state)
{
if (auto const* constructor = _contract.constructor())
return functionSort(*constructor, &_contract);
return functionSort(*constructor, &_contract, _state);
return make_shared<FunctionSort>(
vector<SortPointer>{SortProvider::uintSort} + stateSorts(_contract),
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()} + stateSorts(_contract),
SortProvider::boolSort
);
}
SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract)
SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state)
{
auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
auto varSorts = _contract ? stateSorts(*_contract) : vector<SortPointer>{};
auto inputSorts = applyMap(_function.parameters(), smtSort);
auto outputSorts = applyMap(_function.returnParameters(), smtSort);
return make_shared<FunctionSort>(
vector<SortPointer>{SortProvider::uintSort} +
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()} +
varSorts +
inputSorts +
vector<SortPointer>{_state.stateSort()} +
varSorts +
inputSorts +
outputSorts,
@ -78,9 +83,9 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition
);
}
SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract)
SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state)
{
auto fSort = dynamic_pointer_cast<FunctionSort>(functionSort(_function, _contract));
auto fSort = dynamic_pointer_cast<FunctionSort>(functionSort(_function, _contract, _state));
solAssert(fSort, "");
auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };

26
libsolidity/formal/PredicateSort.h
View File

@ -20,6 +20,8 @@
#include <libsolidity/formal/Predicate.h>
#include <libsolidity/formal/SymbolicState.h>
#include <libsmtutil/Sorts.h>
namespace solidity::frontend::smt
@ -31,46 +33,46 @@ namespace solidity::frontend::smt
*
* 1. Interface
* The idle state of a contract. Signature:
* interface(stateVariables).
* interface(this, blockchainState, stateVariables).
*
* 2. Nondet interface
* The nondeterminism behavior of a contract. Signature:
* nondet_interface(stateVariables, stateVariables').
* nondet_interface(blockchainState, stateVariables, blockchainState', stateVariables').
*
* 3. Implicit constructor
* The implicit constructor of a contract, that is, without input parameters. Signature:
* implicit_constructor().
* implicit_constructor(error, this, blockchainState).
*
* 4. Constructor entry/summary
* The summary of an implicit constructor. Signature:
* constructor_summary(error, stateVariables').
* constructor_summary(error, this, blockchainState, blockchainState', stateVariables').
*
* 5. Function entry/summary
* The entry point of a function definition. Signature:
* function_entry(error, stateVariables, inputVariables, stateVariables', inputVariables', outputVariables').
* function_entry(error, this, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
*
* 6. Function body
* Use for any predicate within a function. Signature:
* function_body(error, stateVariables, inputVariables, stateVariables', inputVariables', outputVariables', localVariables).
* function_body(error, this, blockchainState, stateVariables, inputVariables, blockchainState' ,stateVariables', inputVariables', outputVariables', localVariables).
*/
/// @returns the interface predicate sort for _contract.
smtutil::SortPointer interfaceSort(ContractDefinition const& _contract);
smtutil::SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state);
/// @returns the nondeterminisc interface predicate sort for _contract.
smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _contract);
smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state);
/// @returns the implicit constructor predicate sort.
smtutil::SortPointer implicitConstructorSort();
smtutil::SortPointer implicitConstructorSort(SymbolicState& _state);
/// @returns the constructor entry/summary predicate sort for _contract.
smtutil::SortPointer constructorSort(ContractDefinition const& _contract);
smtutil::SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state);
/// @returns the function entry/summary predicate sort for _function contained in _contract.
smtutil::SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract);
smtutil::SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state);
/// @returns the function body predicate sort for _function contained in _contract.
smtutil::SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract);
smtutil::SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state);
/// @returns the sort of a predicate without parameters.
smtutil::SortPointer arity0FunctionSort();

1
libsolidity/formal/SMTEncoder.cpp
View File

@ -2162,6 +2162,7 @@ void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefin
for (auto const& var: _function->localVariables())
m_context.variable(*var)->resetIndex();
}
m_context.state().reset();
}
Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)

126
libsolidity/formal/SymbolicState.cpp
View File

@ -18,61 +18,118 @@
#include <libsolidity/formal/SymbolicState.h>
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsolidity/formal/EncodingContext.h>
using namespace std;
using namespace solidity;
using namespace solidity::smtutil;
using namespace solidity::frontend::smt;
SymbolicState::SymbolicState(EncodingContext& _context):
m_context(_context)
{
m_stateMembers.emplace("balances", make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort));
vector<string> members;
vector<SortPointer> sorts;
for (auto const& [component, sort]: m_stateMembers)
{
members.emplace_back(component);
sorts.emplace_back(sort);
m_componentIndices[component] = members.size() - 1;
}
m_stateTuple = make_unique<SymbolicTupleVariable>(
make_shared<smtutil::TupleSort>("state_type", members, sorts),
"state",
m_context
);
}
void SymbolicState::reset()
{
m_thisAddress.resetIndex();
m_balances.resetIndex();
m_error.resetIndex();
m_thisAddress.resetIndex();
m_stateTuple->resetIndex();
}
// Blockchain
smtutil::Expression SymbolicState::thisAddress()
{
return m_thisAddress.currentValue();
}
smtutil::Expression SymbolicState::balance()
{
return balance(m_thisAddress.currentValue());
}
smtutil::Expression SymbolicState::balance(smtutil::Expression _address)
{
return smtutil::Expression::select(m_balances.elements(), move(_address));
}
SymbolicIntVariable& SymbolicState::errorFlag()
{
return m_error;
}
SortPointer SymbolicState::errorFlagSort()
{
return m_error.sort();
}
smtutil::Expression SymbolicState::thisAddress()
{
return m_thisAddress.currentValue();
}
smtutil::Expression SymbolicState::thisAddress(unsigned _idx)
{
return m_thisAddress.valueAtIndex(_idx);
}
SortPointer SymbolicState::thisAddressSort()
{
return m_thisAddress.sort();
}
smtutil::Expression SymbolicState::state()
{
return m_stateTuple->currentValue();
}
smtutil::Expression SymbolicState::state(unsigned _idx)
{
return m_stateTuple->valueAtIndex(_idx);
}
SortPointer SymbolicState::stateSort()
{
return m_stateTuple->sort();
}
void SymbolicState::newState()
{
m_stateTuple->increaseIndex();
}
smtutil::Expression SymbolicState::balances()
{
return m_stateTuple->component(m_componentIndices.at("balances"));
}
smtutil::Expression SymbolicState::balance()
{
return balance(thisAddress());
}
smtutil::Expression SymbolicState::balance(smtutil::Expression _address)
{
return smtutil::Expression::select(balances(), move(_address));
}
void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
{
unsigned indexBefore = m_balances.index();
unsigned indexBefore = m_stateTuple->index();
addBalance(_from, 0 - _value);
addBalance(_to, move(_value));
unsigned indexAfter = m_balances.index();
unsigned indexAfter = m_stateTuple->index();
solAssert(indexAfter > indexBefore, "");
m_balances.increaseIndex();
m_stateTuple->increaseIndex();
/// Do not apply the transfer operation if _from == _to.
auto newBalances = smtutil::Expression::ite(
auto newState = smtutil::Expression::ite(
move(_from) == move(_to),
m_balances.valueAtIndex(indexBefore),
m_balances.valueAtIndex(indexAfter)
m_stateTuple->valueAtIndex(indexBefore),
m_stateTuple->valueAtIndex(indexAfter)
);
m_context.addAssertion(m_balances.currentValue() == newBalances);
m_context.addAssertion(m_stateTuple->currentValue() == newState);
}
/// Private helpers.
@ -80,13 +137,24 @@ void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to,
void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
{
auto newBalances = smtutil::Expression::store(
m_balances.elements(),
balances(),
_address,
balance(_address) + move(_value)
);
auto oldLength = m_balances.length();
m_balances.increaseIndex();
m_context.addAssertion(m_balances.elements() == newBalances);
m_context.addAssertion(m_balances.length() == oldLength);
assignStateMember("balances", newBalances);
}
smtutil::Expression SymbolicState::assignStateMember(string const& _member, smtutil::Expression const& _value)
{
vector<smtutil::Expression> args;
for (auto const& member: m_stateMembers)
if (member.first == _member)
args.emplace_back(_value);
else
args.emplace_back(m_stateTuple->component(m_componentIndices.at(member.first)));
m_stateTuple->increaseIndex();
auto tuple = m_stateTuple->currentValue();
auto sortExpr = smtutil::Expression(make_shared<smtutil::SortSort>(tuple.sort), tuple.name);
m_context.addAssertion(tuple == smtutil::Expression::tuple_constructor(sortExpr, args));
return m_stateTuple->currentValue();
}

56
libsolidity/formal/SymbolicState.h
View File

@ -27,9 +27,17 @@ namespace solidity::frontend::smt
{
class EncodingContext;
class SymbolicAddressVariable;
class SymbolicArrayVariable;
/**
* Symbolic representation of the blockchain state.
* Symbolic representation of the blockchain context:
* - error flag
* - this (the address of the currently executing contract)
* - state, represented as a tuple of:
* - balances
* - TODO: potentially storage of contracts
* - TODO transaction variables
*/
class SymbolicState
{
@ -40,15 +48,27 @@ public:
/// Blockchain.
//@{
/// Value of `this` address.
SymbolicIntVariable& errorFlag();
smtutil::SortPointer errorFlagSort();
/// @returns the symbolic value of the currently executing contract's address.
smtutil::Expression thisAddress();
smtutil::Expression thisAddress(unsigned _idx);
smtutil::SortPointer thisAddressSort();
/// @returns the state as a tuple.
smtutil::Expression state();
smtutil::Expression state(unsigned _idx);
smtutil::SortPointer stateSort();
void newState();
/// @returns the symbolic balances.
smtutil::Expression balances();
/// @returns the symbolic balance of address `this`.
smtutil::Expression balance();
/// @returns the symbolic balance of an address.
smtutil::Expression balance(smtutil::Expression _address);
SymbolicIntVariable& errorFlag();
/// Transfer _value from _from to _to.
void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value);
//@}
@ -57,27 +77,27 @@ private:
/// Adds _value to _account's balance.
void addBalance(smtutil::Expression _account, smtutil::Expression _value);
/// Generates a new tuple where _member is assigned _value.
smtutil::Expression assignStateMember(std::string const& _member, smtutil::Expression const& _value);
EncodingContext& m_context;
/// Symbolic `this` address.
SymbolicAddressVariable m_thisAddress{
"this",
m_context
};
/// Symbolic balances.
SymbolicArrayVariable m_balances{
std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort),
"balances",
m_context
};
smt::SymbolicIntVariable m_error{
SymbolicIntVariable m_error{
TypeProvider::uint256(),
TypeProvider::uint256(),
"error",
m_context
};
SymbolicAddressVariable m_thisAddress{
"this",
m_context
};
std::map<std::string, unsigned> m_componentIndices;
/// balances, TODO storage of other contracts
std::map<std::string, smtutil::SortPointer> m_stateMembers;
std::unique_ptr<SymbolicTupleVariable> m_stateTuple;
};
}

20
test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol Normal file
View File

@ -0,0 +1,20 @@
pragma experimental SMTChecker;
contract C {
uint t;
constructor() {
t = address(this).balance;
}
function f(address payable a, uint x) public {
require(address(this).balance >= x);
a.transfer(x);
}
function inv() public view {
// If only looking at `f`, it looks like this.balance always decreases.
// However, the edge case of a contract `selfdestruct` sending its remaining balance
// to this contract should make the claim false (since there's no fallback/receive here).
assert(address(this).balance == t);
}
}
// ----
// Warning 6328: (496-530): CHC: Assertion violation happens here.

12
test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol Normal file
View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract C {
address t;
constructor() {
t = address(this);
}
function inv() public view {
assert(address(this) == t);
}
}
// ----

18
test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol Normal file
View File

@ -0,0 +1,18 @@
pragma experimental SMTChecker;
abstract contract D {
function d() external virtual;
}
contract C {
address t;
constructor() {
t = address(this);
}
function f(D d) public {
address a = address(this);
d.d();
assert(address(this) == t);
assert(a == t);
}
}

15
test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol Normal file
View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract C {
address t;
constructor() {
t = address(this);
}
function f() public view {
g(address(this));
}
function g(address a) internal view {
assert(a == t);
assert(a == address(this));
}
}

13
test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C {
function f(address payable a) public {
require(address(this).balance > 1000);
a.transfer(666);
assert(address(this).balance > 100);
// Fails.
assert(address(this).balance > 500);
}
}
// ----
// Warning 6328: (199-234): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
View File

@ -17,4 +17,3 @@ contract C
}
}
// ----
// Warning 4661: (297-321): BMC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
View File

@ -15,3 +15,4 @@ contract C
}
// ----
// Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (296-309): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol
View File

@ -23,8 +23,6 @@ contract C {
assert(s1[2].a[2] == s2.a[2]);
s1[0].ts[3].y = 5;
assert(s1[0].ts[3].y == s2.ts[3].y);
s1[1].ts[4].a[5] = 6;
assert(s1[1].ts[4].a[5] == s2.ts[4].a[5]);
}
}
// ----
@ -32,4 +30,3 @@ contract C {
// Warning 6328: (327-354): CHC: Assertion violation happens here.
// Warning 6328: (376-405): CHC: Assertion violation happens here.
// Warning 6328: (430-465): CHC: Assertion violation happens here.
// Warning 6328: (493-534): CHC: Assertion violation happens here.