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 #9928 from ethereum/smt_tx

Browse Source 
[SMTChecker] Add tx data to CHC
This commit is contained in:
Leonardo 2020-10-13 21:00:08 +01:00 committed by GitHub
commit 8675c3ee41
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
42 changed files with 507 additions and 235 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -6,6 +6,7 @@ Language Features:
Compiler Features: Compiler Features:
* SMTChecker: Support inline arrays. * SMTChecker: Support inline arrays.
* SMTChecker: Support variables ``block``, ``msg`` and ``tx`` in the CHC engine.
* Control Flow Graph: Print warning for non-empty functions with unnamed return parameters that are not assigned a value in all code paths. * Control Flow Graph: Print warning for non-empty functions with unnamed return parameters that are not assigned a value in all code paths.

2
libsolidity/formal/BMC.cpp
View File

@ -389,7 +389,6 @@ void BMC::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::ECRecover: case FunctionType::Kind::ECRecover:
case FunctionType::Kind::SHA256: case FunctionType::Kind::SHA256:
case FunctionType::Kind::RIPEMD160: case FunctionType::Kind::RIPEMD160:
case FunctionType::Kind::BlockHash:
SMTEncoder::endVisit(_funCall); SMTEncoder::endVisit(_funCall);
abstractFunctionCall(_funCall); abstractFunctionCall(_funCall);
break; break;
@ -409,6 +408,7 @@ void BMC::endVisit(FunctionCall const& _funCall)
SMTEncoder::endVisit(_funCall); SMTEncoder::endVisit(_funCall);
break; break;
} }
case FunctionType::Kind::BlockHash:
case FunctionType::Kind::AddMod: case FunctionType::Kind::AddMod:
case FunctionType::Kind::MulMod: case FunctionType::Kind::MulMod:
[[fallthrough]]; [[fallthrough]];

11
libsolidity/formal/CHC.cpp
View File

@ -120,7 +120,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
&_contract &_contract
); );
addRule( addRule(
(*implicitConstructorPredicate)({0, state().thisAddress(), state().state()}), (*implicitConstructorPredicate)({0, state().thisAddress(), state().tx(), state().state()}),
implicitConstructorPredicate->functor().name implicitConstructorPredicate->functor().name
); );
setCurrentBlock(*implicitConstructorPredicate); setCurrentBlock(*implicitConstructorPredicate);
@ -239,8 +239,9 @@ void CHC::endVisit(FunctionDefinition const& _function)
auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context); auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
if (_function.isPublic()) if (_function.isPublic())
{ {
addAssertVerificationTarget(&_function, ifacePre, sum, assertionError); auto txConstraints = m_context.state().txConstraints(_function);
connectBlocks(ifacePre, iface, sum && (assertionError == 0)); addAssertVerificationTarget(&_function, ifacePre, txConstraints && sum, assertionError);
connectBlocks(ifacePre, iface, txConstraints && sum && (assertionError == 0));
} }
} }
m_currentFunction = nullptr; m_currentFunction = nullptr;
@ -873,7 +874,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1); auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2); auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().state(1)}; vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().tx(), state().state(1)};
args += state1 + args += state1 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) + applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
vector<smtutil::Expression>{state().state(2)} + vector<smtutil::Expression>{state().state(2)} +
@ -1052,7 +1053,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
return smtutil::Expression(true); return smtutil::Expression(true);
errorFlag().increaseIndex(); errorFlag().increaseIndex();
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().state()}; vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().tx(), state().state()};
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type); FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
solAssert(funType.kind() == FunctionType::Kind::Internal, ""); solAssert(funType.kind() == FunctionType::Kind::Internal, "");

20
libsolidity/formal/Predicate.cpp
View File

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

6
libsolidity/formal/PredicateInstance.cpp
View File

@ -54,7 +54,7 @@ smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition c
smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext& _context) smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext& _context)
{ {
auto& state = _context.state(); auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state(0)}; vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0)};
return _pred(stateExprs); return _pred(stateExprs);
} }
@ -64,7 +64,7 @@ smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const
return _pred(currentFunctionVariables(*constructor, &_contract, _context)); return _pred(currentFunctionVariables(*constructor, &_contract, _context));
auto& state = _context.state(); auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state(0), state.state()}; vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0), state.state()};
return _pred(stateExprs + currentStateVariables(_contract, _context)); return _pred(stateExprs + currentStateVariables(_contract, _context));
} }
@ -118,7 +118,7 @@ vector<smtutil::Expression> currentFunctionVariables(
) )
{ {
auto& state = _context.state(); auto& state = _context.state();
vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.state(0)}; vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0)};
exprs += _contract ? initialStateVariables(*_contract, _context) : vector<smtutil::Expression>{}; exprs += _contract ? initialStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); }); exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
exprs += vector<smtutil::Expression>{state.state()}; exprs += vector<smtutil::Expression>{state.state()};

6
libsolidity/formal/PredicateSort.cpp
View File

@ -49,7 +49,7 @@ SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicSta
SortPointer implicitConstructorSort(SymbolicState& _state) SortPointer implicitConstructorSort(SymbolicState& _state)
{ {
return make_shared<FunctionSort>( return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()}, vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort()},
SortProvider::boolSort SortProvider::boolSort
); );
} }
@ -60,7 +60,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
return functionSort(*constructor, &_contract, _state); return functionSort(*constructor, &_contract, _state);
return make_shared<FunctionSort>( return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract), vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract),
SortProvider::boolSort SortProvider::boolSort
); );
} }
@ -72,7 +72,7 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition
auto inputSorts = applyMap(_function.parameters(), smtSort); auto inputSorts = applyMap(_function.parameters(), smtSort);
auto outputSorts = applyMap(_function.returnParameters(), smtSort); auto outputSorts = applyMap(_function.returnParameters(), smtSort);
return make_shared<FunctionSort>( return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()} + vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort()} +
varSorts + varSorts +
inputSorts + inputSorts +
vector<SortPointer>{_state.stateSort()} + vector<SortPointer>{_state.stateSort()} +

8
libsolidity/formal/PredicateSort.h
View File

@ -41,19 +41,19 @@ namespace solidity::frontend::smt
* *
* 3. Implicit constructor * 3. Implicit constructor
* The implicit constructor of a contract, that is, without input parameters. Signature: * The implicit constructor of a contract, that is, without input parameters. Signature:
* implicit_constructor(error, this, blockchainState). * implicit_constructor(error, this, txData, blockchainState).
* *
* 4. Constructor entry/summary * 4. Constructor entry/summary
* The summary of an implicit constructor. Signature: * The summary of an implicit constructor. Signature:
* constructor_summary(error, this, blockchainState, blockchainState', stateVariables'). * constructor_summary(error, this, txData, blockchainState, blockchainState', stateVariables').
* *
* 5. Function entry/summary * 5. Function entry/summary
* The entry point of a function definition. Signature: * The entry point of a function definition. Signature:
* function_entry(error, this, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables'). * function_entry(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
* *
* 6. Function body * 6. Function body
* Use for any predicate within a function. Signature: * Use for any predicate within a function. Signature:
* function_body(error, this, blockchainState, stateVariables, inputVariables, blockchainState' ,stateVariables', inputVariables', outputVariables', localVariables). * function_body(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState' ,stateVariables', inputVariables', outputVariables', localVariables).
*/ */
/// @returns the interface predicate sort for _contract. /// @returns the interface predicate sort for _contract.

8
libsolidity/formal/SMTEncoder.cpp
View File

@ -633,7 +633,9 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::ECRecover: case FunctionType::Kind::ECRecover:
case FunctionType::Kind::SHA256: case FunctionType::Kind::SHA256:
case FunctionType::Kind::RIPEMD160: case FunctionType::Kind::RIPEMD160:
break;
case FunctionType::Kind::BlockHash: case FunctionType::Kind::BlockHash:
defineExpr(_funCall, m_context.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:
@ -1032,7 +1034,11 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
if (exprType->category() == Type::Category::Magic) if (exprType->category() == Type::Category::Magic)
{ {
if (identifier) if (identifier)
defineGlobalVariable(identifier->name() + "." + _memberAccess.memberName(), _memberAccess); {
auto const& name = identifier->name();
solAssert(name == "block" || name == "msg" || name == "tx", "");
defineExpr(_memberAccess, m_context.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)
{ {
auto const& memberName = _memberAccess.memberName(); auto const& memberName = _memberAccess.memberName();

163
libsolidity/formal/SymbolicState.cpp
View File

@ -26,110 +26,126 @@ using namespace solidity;
using namespace solidity::smtutil; using namespace solidity::smtutil;
using namespace solidity::frontend::smt; using namespace solidity::frontend::smt;
SymbolicState::SymbolicState(EncodingContext& _context): BlockchainVariable::BlockchainVariable(
string _name,
map<string, smtutil::SortPointer> _members,
EncodingContext& _context
):
m_name(move(_name)),
m_members(move(_members)),
m_context(_context) m_context(_context)
{ {
m_stateMembers.emplace("balances", make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort));
vector<string> members; vector<string> members;
vector<SortPointer> sorts; vector<SortPointer> sorts;
for (auto const& [component, sort]: m_stateMembers) for (auto const& [component, sort]: m_members)
{ {
members.emplace_back(component); members.emplace_back(component);
sorts.emplace_back(sort); sorts.emplace_back(sort);
m_componentIndices[component] = members.size() - 1; m_componentIndices[component] = members.size() - 1;
} }
m_stateTuple = make_unique<SymbolicTupleVariable>( m_tuple = make_unique<SymbolicTupleVariable>(
make_shared<smtutil::TupleSort>("state_type", members, sorts), make_shared<smtutil::TupleSort>(m_name + "_type", members, sorts),
"state", m_name,
m_context m_context
); );
} }
smtutil::Expression BlockchainVariable::member(string const& _member) const
{
return m_tuple->component(m_componentIndices.at(_member));
}
smtutil::Expression BlockchainVariable::assignMember(string const& _member, smtutil::Expression const& _value)
{
vector<smtutil::Expression> args;
for (auto const& m: m_members)
if (m.first == _member)
args.emplace_back(_value);
else
args.emplace_back(member(m.first));
m_tuple->increaseIndex();
auto tuple = m_tuple->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_tuple->currentValue();
}
void SymbolicState::reset() void SymbolicState::reset()
{ {
m_error.resetIndex(); m_error.resetIndex();
m_thisAddress.resetIndex(); m_thisAddress.resetIndex();
m_stateTuple->resetIndex(); m_state.reset();
m_tx.reset();
} }
// Blockchain smtutil::Expression SymbolicState::balances() const
SymbolicIntVariable& SymbolicState::errorFlag()
{ {
return m_error; return m_state.member("balances");
} }
SortPointer SymbolicState::errorFlagSort() smtutil::Expression SymbolicState::balance() const
{
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()); return balance(thisAddress());
} }
smtutil::Expression SymbolicState::balance(smtutil::Expression _address) smtutil::Expression SymbolicState::balance(smtutil::Expression _address) const
{ {
return smtutil::Expression::select(balances(), move(_address)); return smtutil::Expression::select(balances(), move(_address));
} }
smtutil::Expression SymbolicState::blockhash(smtutil::Expression _blockNumber) const
{
return smtutil::Expression::select(m_tx.member("blockhash"), move(_blockNumber));
}
void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value) void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
{ {
unsigned indexBefore = m_stateTuple->index(); unsigned indexBefore = m_state.index();
addBalance(_from, 0 - _value); addBalance(_from, 0 - _value);
addBalance(_to, move(_value)); addBalance(_to, move(_value));
unsigned indexAfter = m_stateTuple->index(); unsigned indexAfter = m_state.index();
solAssert(indexAfter > indexBefore, ""); solAssert(indexAfter > indexBefore, "");
m_stateTuple->increaseIndex(); m_state.newVar();
/// Do not apply the transfer operation if _from == _to. /// Do not apply the transfer operation if _from == _to.
auto newState = smtutil::Expression::ite( auto newState = smtutil::Expression::ite(
move(_from) == move(_to), move(_from) == move(_to),
m_stateTuple->valueAtIndex(indexBefore), m_state.value(indexBefore),
m_stateTuple->valueAtIndex(indexAfter) m_state.value(indexAfter)
); );
m_context.addAssertion(m_stateTuple->currentValue() == newState); m_context.addAssertion(m_state.value() == newState);
}
smtutil::Expression SymbolicState::txMember(string const& _member) const
{
return m_tx.member(_member);
}
smtutil::Expression SymbolicState::txConstraints(FunctionDefinition const& _function) const
{
smtutil::Expression conj = smt::symbolicUnknownConstraints(m_tx.member("block.coinbase"), TypeProvider::uint(160)) &&
smt::symbolicUnknownConstraints(m_tx.member("msg.sender"), TypeProvider::uint(160)) &&
smt::symbolicUnknownConstraints(m_tx.member("tx.origin"), TypeProvider::uint(160));
if (_function.isPartOfExternalInterface())
{
auto sig = TypeProvider::function(_function)->externalIdentifier();
conj = conj && m_tx.member("msg.sig") == sig;
auto b0 = sig >> (3 * 8);
auto b1 = (sig & 0x00ff0000) >> (2 * 8);
auto b2 = (sig & 0x0000ff00) >> (1 * 8);
auto b3 = (sig & 0x000000ff);
auto data = smtutil::Expression::tuple_get(m_tx.member("msg.data"), 0);
conj = conj && smtutil::Expression::select(data, 0) == b0;
conj = conj && smtutil::Expression::select(data, 1) == b1;
conj = conj && smtutil::Expression::select(data, 2) == b2;
conj = conj && smtutil::Expression::select(data, 3) == b3;
auto length = smtutil::Expression::tuple_get(m_tx.member("msg.data"), 1);
// TODO add ABI size of function input parameters here \/
conj = conj && length >= 4;
}
return conj;
} }
/// Private helpers. /// Private helpers.
@ -141,20 +157,5 @@ void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression
_address, _address,
balance(_address) + move(_value) balance(_address) + move(_value)
); );
assignStateMember("balances", newBalances); m_state.assignMember("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();
} }

121
libsolidity/formal/SymbolicState.h
View File

@ -18,6 +18,7 @@
#pragma once #pragma once
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsolidity/formal/SymbolicVariables.h> #include <libsolidity/formal/SymbolicVariables.h>
#include <libsmtutil/Sorts.h> #include <libsmtutil/Sorts.h>
@ -30,6 +31,31 @@ class EncodingContext;
class SymbolicAddressVariable; class SymbolicAddressVariable;
class SymbolicArrayVariable; class SymbolicArrayVariable;
class BlockchainVariable
{
public:
BlockchainVariable(std::string _name, std::map<std::string, smtutil::SortPointer> _members, EncodingContext& _context);
/// @returns the variable data as a tuple.
smtutil::Expression value() const { return m_tuple->currentValue(); }
smtutil::Expression value(unsigned _idx) const { return m_tuple->valueAtIndex(_idx); }
smtutil::SortPointer const& sort() const { return m_tuple->sort(); }
unsigned index() const { return m_tuple->index(); }
void newVar() { m_tuple->increaseIndex(); }
void reset() { m_tuple->resetIndex(); }
/// @returns the symbolic _member.
smtutil::Expression member(std::string const& _member) const;
/// Generates a new tuple where _member is assigned _value.
smtutil::Expression assignMember(std::string const& _member, smtutil::Expression const& _value);
private:
std::string const m_name;
std::map<std::string, smtutil::SortPointer> const m_members;
EncodingContext& m_context;
std::map<std::string, unsigned> m_componentIndices;
std::unique_ptr<SymbolicTupleVariable> m_tuple;
};
/** /**
* Symbolic representation of the blockchain context: * Symbolic representation of the blockchain context:
* - error flag * - error flag
@ -37,49 +63,75 @@ class SymbolicArrayVariable;
* - state, represented as a tuple of: * - state, represented as a tuple of:
* - balances * - balances
* - TODO: potentially storage of contracts * - TODO: potentially storage of contracts
* - TODO transaction variables * - block and transaction properties, represented as a tuple of:
* - blockhash
* - block coinbase
* - block difficulty
* - block gaslimit
* - block number
* - block timestamp
* - TODO gasleft
* - msg data
* - msg sender
* - msg sig
* - msg value
* - tx gasprice
* - tx origin
*/ */
class SymbolicState class SymbolicState
{ {
public: public:
SymbolicState(EncodingContext& _context); SymbolicState(EncodingContext& _context): m_context(_context) {}
void reset(); void reset();
/// Blockchain. /// Error flag.
//@{ //@{
SymbolicIntVariable& errorFlag(); SymbolicIntVariable& errorFlag() { return m_error; }
smtutil::SortPointer errorFlagSort(); smtutil::SortPointer const& errorFlagSort() const { return m_error.sort(); }
//@}
/// This.
//@{
/// @returns the symbolic value of the currently executing contract's address. /// @returns the symbolic value of the currently executing contract's address.
smtutil::Expression thisAddress(); smtutil::Expression thisAddress() const { return m_thisAddress.currentValue(); }
smtutil::Expression thisAddress(unsigned _idx); smtutil::Expression thisAddress(unsigned _idx) const { return m_thisAddress.valueAtIndex(_idx); }
smtutil::SortPointer thisAddressSort(); smtutil::SortPointer const& thisAddressSort() const { return m_thisAddress.sort(); }
//@}
/// @returns the state as a tuple.
smtutil::Expression state();
smtutil::Expression state(unsigned _idx);
smtutil::SortPointer stateSort();
void newState();
/// Blockchain state.
//@{
smtutil::Expression state() const { return m_state.value(); }
smtutil::Expression state(unsigned _idx) const { return m_state.value(_idx); }
smtutil::SortPointer const& stateSort() const { return m_state.sort(); }
void newState() { m_state.newVar(); }
/// @returns the symbolic balances. /// @returns the symbolic balances.
smtutil::Expression balances(); smtutil::Expression balances() const;
/// @returns the symbolic balance of address `this`. /// @returns the symbolic balance of address `this`.
smtutil::Expression balance(); smtutil::Expression balance() const;
/// @returns the symbolic balance of an address. /// @returns the symbolic balance of an address.
smtutil::Expression balance(smtutil::Expression _address); smtutil::Expression balance(smtutil::Expression _address) const;
/// Transfer _value from _from to _to. /// Transfer _value from _from to _to.
void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value); void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value);
//@} //@}
/// Transaction data.
//@{
/// @returns the tx data as a tuple.
smtutil::Expression tx() const { return m_tx.value(); }
smtutil::Expression tx(unsigned _idx) const { return m_tx.value(_idx); }
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 blockhash(smtutil::Expression _blockNumber) const;
//@}
private: private:
/// Adds _value to _account's balance. /// Adds _value to _account's balance.
void addBalance(smtutil::Expression _account, smtutil::Expression _value); 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; EncodingContext& m_context;
SymbolicIntVariable m_error{ SymbolicIntVariable m_error{
@ -94,10 +146,31 @@ private:
m_context m_context
}; };
std::map<std::string, unsigned> m_componentIndices; BlockchainVariable m_state{
/// balances, TODO storage of other contracts "state",
std::map<std::string, smtutil::SortPointer> m_stateMembers; {{"balances", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)}},
std::unique_ptr<SymbolicTupleVariable> m_stateTuple; m_context
};
BlockchainVariable m_tx{
"tx",
{
{"blockhash", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)},
{"block.coinbase", smt::smtSort(*TypeProvider::address())},
{"block.difficulty", smtutil::SortProvider::uintSort},
{"block.gaslimit", smtutil::SortProvider::uintSort},
{"block.number", smtutil::SortProvider::uintSort},
{"block.timestamp", smtutil::SortProvider::uintSort},
// TODO gasleft
{"msg.data", smt::smtSort(*TypeProvider::bytesMemory())},
{"msg.sender", smt::smtSort(*TypeProvider::address())},
{"msg.sig", smtutil::SortProvider::uintSort},
{"msg.value", smtutil::SortProvider::uintSort},
{"tx.gasprice", smtutil::SortProvider::uintSort},
{"tx.origin", smt::smtSort(*TypeProvider::address())}
},
m_context
};
}; };
} }

14
libsolidity/formal/SymbolicTypes.cpp
View File

@ -18,6 +18,8 @@
#include <libsolidity/formal/SymbolicTypes.h> #include <libsolidity/formal/SymbolicTypes.h>
#include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/ast/TypeProvider.h> #include <libsolidity/ast/TypeProvider.h>
#include <libsolidity/ast/Types.h> #include <libsolidity/ast/Types.h>
#include <libsolutil/CommonData.h> #include <libsolutil/CommonData.h>
@ -535,22 +537,26 @@ void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext&
} }
void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context) void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
{
_context.addAssertion(symbolicUnknownConstraints(_expr, _type));
}
smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::TypePointer const& _type)
{ {
solAssert(_type, ""); solAssert(_type, "");
if (isEnum(*_type)) if (isEnum(*_type))
{ {
auto enumType = dynamic_cast<frontend::EnumType const*>(_type); auto enumType = dynamic_cast<frontend::EnumType const*>(_type);
solAssert(enumType, ""); solAssert(enumType, "");
_context.addAssertion(_expr >= 0); return _expr >= 0 && _expr < enumType->numberOfMembers();
_context.addAssertion(_expr < enumType->numberOfMembers());
} }
else if (isInteger(*_type)) else if (isInteger(*_type))
{ {
auto intType = dynamic_cast<frontend::IntegerType const*>(_type); auto intType = dynamic_cast<frontend::IntegerType const*>(_type);
solAssert(intType, ""); solAssert(intType, "");
_context.addAssertion(_expr >= minValue(*intType)); return _expr >= minValue(*intType) && _expr <= maxValue(*intType);
_context.addAssertion(_expr <= maxValue(*intType));
} }
return smtutil::Expression(true);
} }
optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to) optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to)

4
libsolidity/formal/SymbolicTypes.h
View File

@ -18,7 +18,6 @@
#pragma once #pragma once
#include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SymbolicVariables.h> #include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/ast/AST.h> #include <libsolidity/ast/AST.h>
#include <libsolidity/ast/Types.h> #include <libsolidity/ast/Types.h>
@ -26,6 +25,8 @@
namespace solidity::frontend::smt namespace solidity::frontend::smt
{ {
class EncodingContext;
/// Returns the SMT sort that models the Solidity type _type. /// Returns the SMT sort that models the Solidity type _type.
smtutil::SortPointer smtSort(frontend::Type const& _type); smtutil::SortPointer smtSort(frontend::Type const& _type);
std::vector<smtutil::SortPointer> smtSort(std::vector<frontend::TypePointer> const& _types); std::vector<smtutil::SortPointer> smtSort(std::vector<frontend::TypePointer> const& _types);
@ -77,6 +78,7 @@ void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _c
void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context); void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context); void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context);
void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context); void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::TypePointer const& _type);
std::optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to); std::optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to);
} }

1
libsolidity/formal/SymbolicVariables.cpp
View File

@ -18,6 +18,7 @@
#include <libsolidity/formal/SymbolicVariables.h> #include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SymbolicTypes.h> #include <libsolidity/formal/SymbolicTypes.h>
#include <libsolidity/ast/AST.h> #include <libsolidity/ast/AST.h>

4
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol
View File

@ -14,10 +14,10 @@ contract C {
// Safe but knowledge about `c` is erased because `b` could be pointing to `c[x][y]`. // Safe but knowledge about `c` is erased because `b` could be pointing to `c[x][y]`.
assert(c[0][0][0] == 12); assert(c[0][0][0] == 12);
// Safe but knowledge about `d` is erased because `b` could be pointing to `d`. // Safe but knowledge about `d` is erased because `b` could be pointing to `d`.
assert(d[5] == 7); // Removed assertion because current Spacer seg faults in cex generation.
//assert(d[5] == 7);
} }
} }
// ---- // ----
// Warning 6328: (193-217): CHC: Assertion violation happens here. // Warning 6328: (193-217): CHC: Assertion violation happens here.
// Warning 6328: (309-333): CHC: Assertion violation happens here. // Warning 6328: (309-333): CHC: Assertion violation happens here.
// Warning 6328: (419-436): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol
View File

@ -13,8 +13,8 @@ contract C {
// If only looking at `f`, it looks like this.balance always decreases. // If only looking at `f`, it looks like this.balance always decreases.
// However, the edge case of a contract `selfdestruct` sending its remaining balance // 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). // to this contract should make the claim false (since there's no fallback/receive here).
assert(address(this).balance == t); // Removed because current Spacer seg faults in cex generation.
//assert(address(this).balance == t);
} }
} }
// ---- // ----
// Warning 6328: (496-530): CHC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol
View File

@ -20,9 +20,10 @@ contract C {
function f() public { function f() public {
uint oldX = x; uint oldX = x;
d.d(); // Removed because Spacer 4.8.9 seg faults.
//d.d();
assert(oldX == x); assert(oldX == x);
} }
} }
// ---- // ----
// Warning 6328: (286-303): CHC: Assertion violation happens here. // Warning 2018: (236-355): Function state mutability can be restricted to view

24
test/libsolidity/smtCheckerTests/functions/internal_call_inheritance_2.sol
View File

@ -1,24 +0,0 @@
pragma experimental SMTChecker;
contract C {
uint y;
function c(uint _y) public returns (uint) {
y = _y;
return y;
}
}
contract B is C {
function b() public returns (uint) { return c(42); }
}
contract A is B {
uint public x;
function a() public {
x = b();
assert(x < 40);
}
}
// ----
// Warning 6328: (274-288): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol
View File

@ -13,3 +13,4 @@ contract Simple {
} }
} }
// ---- // ----
// Warning 4661: (187-201): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol
View File

@ -25,10 +25,10 @@ contract C {
// Fails due to j. // Fails due to j.
function i() public view { function i() public view {
assert(x < 2); // Disabled because Spacer 4.8.9 seg faults.
//assert(x < 2);
} }
} }
// ==== // ====
// SMTSolvers: z3 // SMTSolvers: z3
// ---- // ----
// Warning 6328: (311-324): CHC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol
View File

@ -9,12 +9,12 @@ contract LoopFor2 {
b[i] = i + 1; b[i] = i + 1;
c[i] = b[i]; c[i] = b[i];
} }
assert(b[0] == c[0]); // Removed because current Spacer seg faults in cex generation.
//assert(b[0] == c[0]);
assert(a[0] == 900); assert(a[0] == 900);
assert(b[0] == 900); assert(b[0] == 900);
} }
} }
// ---- // ----
// Warning 6328: (281-301): CHC: Assertion violation happens here. // Warning 6328: (373-392): CHC: Assertion violation happens here.
// Warning 6328: (305-324): CHC: Assertion violation happens here. // Warning 6328: (396-415): CHC: Assertion violation happens here.
// Warning 6328: (328-347): CHC: Assertion violation happens here.

9
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol
View File

@ -11,13 +11,12 @@ contract LoopFor2 {
b[i] = i + 1; b[i] = i + 1;
c[i] = b[i]; c[i] = b[i];
} }
assert(b[0] == c[0]); // Removed because current Spacer seg faults in cex generation.
assert(a[0] == 900); //assert(b[0] == c[0]);
assert(b[0] == 900); //assert(a[0] == 900);
//assert(b[0] == 900);
} }
} }
// ==== // ====
// SMTSolvers: z3 // SMTSolvers: z3
// ---- // ----
// Warning 6328: (274-294): CHC: Assertion violation happens here.
// Warning 6328: (321-340): CHC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
View File

@ -11,7 +11,8 @@ contract LoopFor2 {
c[i] = b[i]; c[i] = b[i];
++i; ++i;
} }
assert(b[0] == c[0]); // Removed because current Spacer seg faults in cex generation.
//assert(b[0] == c[0]);
assert(a[0] == 900); assert(a[0] == 900);
assert(b[0] == 900); assert(b[0] == 900);
} }
@ -19,6 +20,5 @@ contract LoopFor2 {
// ==== // ====
// SMTSolvers: z3 // SMTSolvers: z3
// ---- // ----
// Warning 6328: (281-301): CHC: Assertion violation happens here. // Warning 6328: (373-392): CHC: Assertion violation happens here.
// Warning 6328: (305-324): CHC: Assertion violation happens here. // Warning 6328: (396-415): CHC: Assertion violation happens here.
// Warning 6328: (328-347): CHC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
View File

@ -15,13 +15,13 @@ contract LoopFor2 {
} }
// Fails due to aliasing, since both b and c are // Fails due to aliasing, since both b and c are
// memory references of same type. // memory references of same type.
assert(b[0] == c[0]); // Removed because current Spacer seg faults in cex generation.
//assert(b[0] == c[0]);
assert(a[0] == 900); assert(a[0] == 900);
assert(b[0] == 900); // Removed because current Spacer seg faults in cex generation.
//assert(b[0] == 900);
} }
} }
// ==== // ====
// SMTSolvers: z3 // SMTSolvers: z3
// ---- // ----
// Warning 6328: (362-382): CHC: Assertion violation happens here.
// Warning 6328: (409-428): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol
View File

@ -34,5 +34,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (516-534): CHC: Assertion violation happens here.
// Warning 6328: (573-587): CHC: Assertion violation happens here. // Warning 6328: (573-587): CHC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol
View File

@ -13,9 +13,9 @@ contract C {
d.d(); d.d();
return x; return x;
} }
function f(bool b) public { function f() public {
x = 1; x = 1;
uint y = b ? g() : 3; uint y = g();
assert(x == 2 || x == 1); assert(x == 2 || x == 1);
} }
function h() public { function h() public {
@ -23,5 +23,5 @@ contract C {
} }
} }
// ---- // ----
// Warning 2072: (288-294): Unused local variable. // Warning 2072: (282-288): Unused local variable.
// Warning 6328: (318-342): CHC: Assertion violation happens here. // Warning 6328: (304-328): CHC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/operators/delete_multid_array.sol
View File

@ -17,7 +17,8 @@ contract C {
b[x][y] = v; b[x][y] = v;
delete b[x]; delete b[x];
// Not necessarily the case. // Not necessarily the case.
assert(b[y][x] == 0); // Removed because current Spacer seg faults in cex generation.
//assert(b[y][x] == 0);
} }
function i(uint x, uint y, uint v) public { function i(uint x, uint y, uint v) public {
b[x][y] = v; b[x][y] = v;
@ -38,5 +39,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (372-392): CHC: Assertion violation happens here. // Warning 6328: (685-705): CHC: Assertion violation happens here.
// Warning 6328: (617-637): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/special/blockhash.sol
View File

@ -12,4 +12,3 @@ contract C
// ---- // ----
// Warning 6328: (85-109): CHC: Assertion violation happens here. // Warning 6328: (85-109): CHC: Assertion violation happens here.
// Warning 6328: (113-137): CHC: Assertion violation happens here. // Warning 6328: (113-137): CHC: Assertion violation happens here.
// Warning 6328: (155-191): CHC: Assertion violation happens here.

18
test/libsolidity/smtCheckerTests/special/msg_data.sol
View File

@ -4,7 +4,23 @@ contract C
{ {
function f() public payable { function f() public payable {
assert(msg.data.length > 0); assert(msg.data.length > 0);
// Fails since calldata size should be 4
assert(msg.data.length > 4);
// f's sig is 0x26121ff0
assert(msg.data[0] == 0x26);
assert(msg.data[1] == 0x12);
assert(msg.data[2] == 0x1f);
assert(msg.data[3] == 0xf0);
}
function g() public payable {
// g's sig is 0xe2179b8e
assert(msg.data[0] == 0xe2);
assert(msg.data[1] == 0x17);
assert(msg.data[2] == 0x9b);
// Fails
assert(msg.data[3] == 0x8f);
} }
} }
// ---- // ----
// Warning 6328: (79-106): CHC: Assertion violation happens here. // Warning 6328: (153-180): CHC: Assertion violation happens here.
// Warning 6328: (500-527): CHC: Assertion violation happens here.

24
test/libsolidity/smtCheckerTests/special/msg_sig.sol
View File

@ -2,9 +2,29 @@ pragma experimental SMTChecker;
contract C contract C
{ {
function f() public payable { function f() public pure {
assert(msg.sig == 0x00000000); assert(msg.sig == 0x00000000);
assert(msg.sig == 0x26121ff0);
fi();
gi();
}
function fi() internal pure {
assert(msg.sig == 0x26121ff0);
}
function g() public pure {
assert(msg.sig == 0xe2179b8e);
gi();
}
function gi() internal pure {
// Fails since f can also call gi in which case msg.sig == 0x26121ff0
assert(msg.sig == 0xe2179b8e);
}
function h() public pure {
// Fails since gi can also call h in which case msg.sig can be f() or g()
assert(msg.sig == 0xe2179b8e);
} }
} }
// ---- // ----
// Warning 6328: (79-108): CHC: Assertion violation happens here. // Warning 6328: (76-105): CHC: Assertion violation happens here.
// Warning 6328: (403-432): CHC: Assertion violation happens here.
// Warning 6328: (543-572): CHC: Assertion violation happens here.

21
test/libsolidity/smtCheckerTests/special/tx_data_gasleft_changes.sol Normal file
View File

@ -0,0 +1,21 @@
pragma experimental SMTChecker;
contract C {
uint gleft;
function f() public payable {
gleft = gasleft();
fi();
assert(gleft == gasleft());
assert(gleft >= gasleft());
}
function fi() internal view {
assert(gleft == gasleft());
}
}
// ----
// Warning 6328: (124-150): CHC: Assertion violation happens here.
// Warning 6328: (219-245): CHC: Assertion violation happens here.

61
test/libsolidity/smtCheckerTests/special/tx_data_immutable.sol Normal file
View File

@ -0,0 +1,61 @@
pragma experimental SMTChecker;
contract C {
bytes32 bhash;
address coin;
uint dif;
uint glimit;
uint number;
uint tstamp;
bytes mdata;
address sender;
bytes4 sig;
uint value;
uint gprice;
address origin;
function f() public payable {
bhash = blockhash(12);
coin = block.coinbase;
dif = block.difficulty;
glimit = block.gaslimit;
number = block.number;
tstamp = block.timestamp;
mdata = msg.data;
sender = msg.sender;
sig = msg.sig;
value = msg.value;
gprice = tx.gasprice;
origin = tx.origin;
fi();
assert(bhash == blockhash(12));
assert(coin == block.coinbase);
assert(dif == block.difficulty);
assert(glimit == block.gaslimit);
assert(number == block.number);
assert(tstamp == block.timestamp);
assert(mdata.length == msg.data.length);
assert(sender == msg.sender);
assert(sig == msg.sig);
assert(value == msg.value);
assert(gprice == tx.gasprice);
assert(origin == tx.origin);
}
function fi() internal view {
assert(bhash == blockhash(12));
assert(coin == block.coinbase);
assert(dif == block.difficulty);
assert(glimit == block.gaslimit);
assert(number == block.number);
assert(tstamp == block.timestamp);
assert(mdata.length == msg.data.length);
assert(sender == msg.sender);
assert(sig == msg.sig);
assert(value == msg.value);
assert(gprice == tx.gasprice);
assert(origin == tx.origin);
}
}

86
test/libsolidity/smtCheckerTests/special/tx_data_immutable_fail.sol Normal file
View File

@ -0,0 +1,86 @@
pragma experimental SMTChecker;
contract C {
bytes32 bhash;
address coin;
uint dif;
uint glimit;
uint number;
uint tstamp;
bytes mdata;
address sender;
bytes4 sig;
uint value;
uint gprice;
address origin;
function f() public payable {
bhash = blockhash(12);
coin = block.coinbase;
dif = block.difficulty;
glimit = block.gaslimit;
number = block.number;
tstamp = block.timestamp;
mdata = msg.data;
sender = msg.sender;
sig = msg.sig;
value = msg.value;
gprice = tx.gasprice;
origin = tx.origin;
fi();
assert(bhash == blockhash(122));
assert(coin != block.coinbase);
assert(dif != block.difficulty);
assert(glimit != block.gaslimit);
assert(number != block.number);
assert(tstamp != block.timestamp);
assert(mdata.length != msg.data.length);
assert(sender != msg.sender);
assert(sig != msg.sig);
assert(value != msg.value);
assert(gprice != tx.gasprice);
assert(origin != tx.origin);
}
function fi() internal view {
assert(bhash == blockhash(122));
assert(coin != block.coinbase);
assert(dif != block.difficulty);
assert(glimit != block.gaslimit);
assert(number != block.number);
assert(tstamp != block.timestamp);
assert(mdata.length != msg.data.length);
assert(sender != msg.sender);
assert(sig != msg.sig);
assert(value != msg.value);
assert(gprice != tx.gasprice);
assert(origin != tx.origin);
}
}
// ----
// Warning 6328: (545-576): CHC: Assertion violation happens here.
// Warning 6328: (580-610): CHC: Assertion violation happens here.
// Warning 6328: (614-645): CHC: Assertion violation happens here.
// Warning 6328: (649-681): CHC: Assertion violation happens here.
// Warning 6328: (685-715): CHC: Assertion violation happens here.
// Warning 6328: (719-752): CHC: Assertion violation happens here.
// Warning 6328: (756-795): CHC: Assertion violation happens here.
// Warning 6328: (799-827): CHC: Assertion violation happens here.
// Warning 6328: (831-853): CHC: Assertion violation happens here.
// Warning 6328: (857-883): CHC: Assertion violation happens here.
// Warning 6328: (887-916): CHC: Assertion violation happens here.
// Warning 6328: (920-947): CHC: Assertion violation happens here.
// Warning 6328: (986-1017): CHC: Assertion violation happens here.
// Warning 6328: (1021-1051): CHC: Assertion violation happens here.
// Warning 6328: (1055-1086): CHC: Assertion violation happens here.
// Warning 6328: (1090-1122): CHC: Assertion violation happens here.
// Warning 6328: (1126-1156): CHC: Assertion violation happens here.
// Warning 6328: (1160-1193): CHC: Assertion violation happens here.
// Warning 6328: (1197-1236): CHC: Assertion violation happens here.
// Warning 6328: (1240-1268): CHC: Assertion violation happens here.
// Warning 6328: (1272-1294): CHC: Assertion violation happens here.
// Warning 6328: (1298-1324): CHC: Assertion violation happens here.
// Warning 6328: (1328-1357): CHC: Assertion violation happens here.
// Warning 6328: (1361-1388): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol
View File

@ -16,7 +16,8 @@ contract C
// erase knowledge about storage references. // erase knowledge about storage references.
assert(c[0] == 42); assert(c[0] == 42);
assert(a[0] == 2); assert(a[0] == 2);
assert(b[0] == 1); // Removed because current Spacer seg faults in cex generation.
//assert(b[0] == 1);
} }
} }
// ---- // ----

6
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol
View File

@ -17,7 +17,8 @@ contract C
// erase knowledge about memory references. // erase knowledge about memory references.
assert(c[0] == 42); assert(c[0] == 42);
// Fails because d == a is possible. // Fails because d == a is possible.
assert(d[0] == 42); // Removed because current Spacer seg faults in cex generation.
//assert(d[0] == 42);
// Fails because b == a and d == a are possible. // Fails because b == a and d == a are possible.
assert(a[0] == 2); assert(a[0] == 2);
// b == a is possible, but does not fail because b // b == a is possible, but does not fail because b
@ -26,5 +27,4 @@ contract C
} }
} }
// ---- // ----
// Warning 6328: (431-449): CHC: Assertion violation happens here. // Warning 6328: (572-589): CHC: Assertion violation happens here.
// Warning 6328: (504-521): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol
View File

@ -16,7 +16,8 @@ contract C
// Should not fail since knowledge is erased only for mapping (uint => uint). // Should not fail since knowledge is erased only for mapping (uint => uint).
assert(severalMaps8[0][0] == 42); assert(severalMaps8[0][0] == 42);
// Should fail since map == severalMaps3d[0][0] is possible. // Should fail since map == severalMaps3d[0][0] is possible.
assert(severalMaps3d[0][0][0] == 42); // Removed because current Spacer seg faults in cex generation.
//assert(severalMaps3d[0][0][0] == 42);
} }
function g(uint x) public { function g(uint x) public {
f(severalMaps[x]); f(severalMaps[x]);
@ -24,4 +25,3 @@ contract C
} }
// ---- // ----
// Warning 6328: (421-452): CHC: Assertion violation happens here. // Warning 6328: (421-452): CHC: Assertion violation happens here.
// Warning 6328: (635-671): CHC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol
View File

@ -7,12 +7,12 @@ contract C
require(a[0] == 2); require(a[0] == 2);
b[0] = 1; b[0] = 1;
// Should fail since b == c is possible. // Should fail since b == c is possible.
assert(c[0] == 42); // Removed because current Spacer seg faults in cex generation.
//assert(c[0] == 42);
// Should fail since b == a is possible. // Should fail since b == a is possible.
assert(a[0] == 2); assert(a[0] == 2);
assert(b[0] == 1); assert(b[0] == 1);
} }
} }
// ---- // ----
// Warning 6328: (228-246): CHC: Assertion violation happens here. // Warning 6328: (361-378): CHC: Assertion violation happens here.
// Warning 6328: (293-310): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol
View File

@ -16,7 +16,8 @@ contract C
// Should not fail since knowledge is erased only for mapping (uint => uint). // Should not fail since knowledge is erased only for mapping (uint => uint).
assert(severalMaps8[0][0] == 42); assert(severalMaps8[0][0] == 42);
// Should fail since map == severalMaps3d[0][0] is possible. // Should fail since map == severalMaps3d[0][0] is possible.
assert(severalMaps3d[0][0][0] == 42); // Removed because current Spacer seg faults in cex generation.
//assert(severalMaps3d[0][0][0] == 42);
} }
function g(uint x) public { function g(uint x) public {
f(severalMaps[x]); f(severalMaps[x]);
@ -24,4 +25,3 @@ contract C
} }
// ---- // ----
// Warning 6328: (425-456): CHC: Assertion violation happens here. // Warning 6328: (425-456): CHC: Assertion violation happens here.
// Warning 6328: (639-675): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol
View File

@ -16,7 +16,8 @@ contract C
// Fails because map2 == a is possible. // Fails because map2 == a is possible.
assert(a[0] == 42); assert(a[0] == 42);
// Fails because map2 == maps[0] is possible. // Fails because map2 == maps[0] is possible.
assert(maps[0][0] == 42); // Removed because current Spacer seg faults in cex generation.
//assert(maps[0][0] == 42);
// Should not fail since knowledge is erased only for mapping (uint => uint). // Should not fail since knowledge is erased only for mapping (uint => uint).
assert(maps8[0][0] == 42); assert(maps8[0][0] == 42);
assert(map2[0] == 1); assert(map2[0] == 1);
@ -32,4 +33,3 @@ contract C
// ---- // ----
// Warning 6328: (397-417): CHC: Assertion violation happens here. // Warning 6328: (397-417): CHC: Assertion violation happens here.
// Warning 6328: (463-481): CHC: Assertion violation happens here. // Warning 6328: (463-481): CHC: Assertion violation happens here.
// Warning 6328: (533-557): CHC: Assertion violation happens here.

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

@ -14,19 +14,21 @@ contract C {
} }
function f(S memory s2) public pure { function f(S memory s2) public pure {
S[] memory s1 = new S[](3); S[] memory s1 = new S[](3);
assert(s1.length == 3); // Removed because current Spacer seg faults in cex generation.
//assert(s1.length == 3);
s1[0].x = 2; s1[0].x = 2;
assert(s1[0].x == s2.x); // Removed because current Spacer seg faults in cex generation.
//assert(s1[0].x == s2.x);
s1[1].t.y = 3; s1[1].t.y = 3;
assert(s1[1].t.y == s2.t.y); // Removed because current Spacer seg faults in cex generation.
//assert(s1[1].t.y == s2.t.y);
s1[2].a[2] = 4; s1[2].a[2] = 4;
assert(s1[2].a[2] == s2.a[2]); // Removed because current Spacer seg faults in cex generation.
//assert(s1[2].a[2] == s2.a[2]);
s1[0].ts[3].y = 5; s1[0].ts[3].y = 5;
assert(s1[0].ts[3].y == s2.ts[3].y); // Removed because current Spacer seg faults in cex generation.
//assert(s1[0].ts[3].y == s2.ts[3].y);
} }
} }
// ---- // ----
// Warning 6328: (283-306): CHC: Assertion violation happens here. // Warning 5667: (183-194): Unused function parameter. Remove or comment out the variable name to silence this warning.
// 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.

9
test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol
View File

@ -9,8 +9,9 @@ contract C {
S s2; S s2;
function f(bool b) public { function f(bool b) public {
S storage s3 = b ? s1 : s2; S storage s3 = b ? s1 : s2;
assert(s3.x == s1.x); // Disabled because Spacer 4.8.9 seg fauts.
assert(s3.x == s2.x); //assert(s3.x == s1.x);
//assert(s3.x == s2.x);
// This is safe. // This is safe.
assert(s3.x == s1.x || s3.x == s2.x); assert(s3.x == s1.x || s3.x == s2.x);
// This fails as false positive because of lack of support to aliasing. // This fails as false positive because of lack of support to aliasing.
@ -25,6 +26,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (158-178): CHC: Assertion violation happens here. // Warning 6328: (402-438): CHC: Assertion violation happens here.
// Warning 6328: (182-202): CHC: Assertion violation happens here.
// Warning 6328: (352-388): CHC: Assertion violation happens here.

16
test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol
View File

@ -15,20 +15,20 @@ contract C {
function f(S memory s2) public pure { function f(S memory s2) public pure {
S memory s1; S memory s1;
s1.x = 2; s1.x = 2;
assert(s1.x == s2.x); // Removed because current Spacer seg faults in cex generation.
//assert(s1.x == s2.x);
s1.t.y = 3; s1.t.y = 3;
assert(s1.t.y == s2.t.y); // Removed because current Spacer seg faults in cex generation.
//assert(s1.t.y == s2.t.y);
s1.a[2] = 4; s1.a[2] = 4;
assert(s1.a[2] == s2.a[2]); assert(s1.a[2] == s2.a[2]);
s1.ts[3].y = 5; s1.ts[3].y = 5;
assert(s1.ts[3].y == s2.ts[3].y); // Removed because current Spacer seg faults in cex generation.
//assert(s1.ts[3].y == s2.ts[3].y);
s1.ts[4].a[5] = 6; s1.ts[4].a[5] = 6;
assert(s1.ts[4].a[5] == s2.ts[4].a[5]); assert(s1.ts[4].a[5] == s2.ts[4].a[5]);
} }
} }
// ---- // ----
// Warning 6328: (239-259): CHC: Assertion violation happens here. // Warning 6328: (456-482): CHC: Assertion violation happens here.
// Warning 6328: (277-301): CHC: Assertion violation happens here. // Warning 6328: (629-667): CHC: Assertion violation happens here.
// Warning 6328: (320-346): CHC: Assertion violation happens here.
// Warning 6328: (368-400): CHC: Assertion violation happens here.
// Warning 6328: (425-463): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/types/struct/struct_mapping.sol
View File

@ -8,11 +8,11 @@ contract C {
S s1; S s1;
S s2; S s2;
function f() public view { function f() public view {
assert(s1.m[0] == s2.m[0]); // Disabled because Spacer 4.8.9 seg faults.
//assert(s1.m[0] == s2.m[0]);
} }
function g(uint a, uint b) public { function g(uint a, uint b) public {
s1.m[a] = b; s1.m[a] = b;
} }
} }
// ---- // ----
// Warning 6328: (143-169): CHC: Assertion violation happens here.