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

Remove all use of datatypes and arrays

Browse Source
This commit is contained in:
Leo Alt 2021-08-09 12:27:44 +02:00
parent ce0e0c48fb
commit cae0b8316c
6 changed files with 58 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
libsmtutil/Z3CHCInterface.cpp
View File

@ -80,6 +80,7 @@ void Z3CHCInterface::addRule(Expression const& _expr, string const& _name)
pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr)
{
CheckResult result;
cout << m_solver << endl;
try
{
z3::expr z3Expr = m_z3Interface->toZ3Expr(_expr);

38
libsolidity/formal/CHC.cpp
View File

@ -756,14 +756,14 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
for (auto var: function->returnParameters())
m_context.variable(*var)->increaseIndex();
auto preCallState = vector<smtutil::Expression>{state().state()} + 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();
//state().newState();
for (auto const* var: m_stateVariables)
m_context.variable(*var)->increaseIndex();
}
@ -776,8 +776,8 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
PredicateType::ExternalCallUntrusted,
&_funCall
);
auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
vector<smtutil::Expression> stateExprs{error, state().thisAddress(), state().abi(), state().crypto()};
auto postCallState = /*vector<smtutil::Expression>{state().state()} +*/ currentStateVariables();
vector<smtutil::Expression> stateExprs{error, state().thisAddress()/*, state().abi(), state().crypto()*/};
auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState);
auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
@ -809,21 +809,21 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
return;
// External call creates a new transaction.
auto originalTx = state().tx();
auto txOrigin = state().txMember("tx.origin");
state().newTx();
//auto originalTx = state().tx();
//auto txOrigin = state().txMember("tx.origin");
//state().newTx();
// set the transaction sender as this contract
m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress());
//m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress());
// set the origin to be the current transaction origin
m_context.addAssertion(state().txMember("tx.origin") == txOrigin);
//m_context.addAssertion(state().txMember("tx.origin") == txOrigin);
smtutil::Expression pred = predicate(_funCall);
auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(*function);
m_context.addAssertion(pred && txConstraints);
// restore the original transaction data
state().newTx();
m_context.addAssertion(originalTx == state().tx());
//state().newTx();
//m_context.addAssertion(originalTx == state().tx());
solAssert(m_errorDest, "");
connectBlocks(
@ -1002,7 +1002,7 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
m_context.variable(*var)->increaseIndex();
}
state().newState();
//state().newState();
}
void CHC::setCurrentBlock(Predicate const& _block)
@ -1125,10 +1125,10 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
auto errorPost = errorFlag().increaseIndex();
auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
vector<smtutil::Expression> args{errorPost, state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)};
vector<smtutil::Expression> args{errorPost, state().thisAddress()/*, state().abi(), state().crypto(), state().tx(), state().state(1)*/};
args += state1 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
vector<smtutil::Expression>{state().state(2)} +
//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); });
@ -1272,7 +1272,7 @@ void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression co
smtutil::Expression CHC::initialConstraints(ContractDefinition const& _contract, FunctionDefinition const* _function)
{
smtutil::Expression conj = state().state() == state().state(0);
smtutil::Expression conj(true);// = state().state() == state().state(0);
conj = conj && errorFlag().currentValue() == 0;
conj = conj && currentEqualInitialVarsConstraints(stateVariablesIncludingInheritedAndPrivate(_contract));
@ -1387,7 +1387,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
solAssert(false, "Unreachable!");
};
errorFlag().increaseIndex();
vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()};
vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall)/*, state().abi(), state().crypto(), state().tx(), state().state()*/};
auto const* contract = function->annotation().contract;
auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
@ -1399,11 +1399,11 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
args += symbolicArguments(_funCall, m_currentContract);
if (!m_currentContract->isLibrary() && !usesStaticCall)
{
state().newState();
//state().newState();
for (auto const& var: m_stateVariables)
m_context.variable(*var)->increaseIndex();
}
args += vector<smtutil::Expression>{state().state()};
//args += vector<smtutil::Expression>{state().state()};
args += currentStateVariables(*m_currentContract);
for (auto var: function->parameters() + function->returnParameters())
@ -1660,6 +1660,7 @@ void CHC::checkAndReportTarget(
else if (result == CheckResult::SATISFIABLE)
{
solAssert(!_satMsg.empty(), "");
/*
auto cex = generateCounterexample(model, error().name);
if (cex)
m_unsafeTargets[_target.errorNode][_target.type] = {
@ -1668,6 +1669,7 @@ void CHC::checkAndReportTarget(
"CHC: " + _satMsg + "\nCounterexample:\n" + *cex
};
else
*/
m_unsafeTargets[_target.errorNode][_target.type] = {
_errorReporterId,
location,

28
libsolidity/formal/PredicateInstance.cpp
View File

@ -30,14 +30,14 @@ 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.abi(0), state.crypto(0), state.state(0)};
vector<smtutil::Expression> stateExprs{state.thisAddress(0)/*, state.abi(0), state.crypto(0), state.state(0)*/};
return _pred(stateExprs + initialStateVariables(_contract, _context));
}
smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
{
auto const& state = _context.state();
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()};
vector<smtutil::Expression> stateExprs{state.thisAddress(0)/*, state.abi(0), state.crypto(0), state.state()*/};
return _pred(stateExprs + currentStateVariables(_contract, _context));
}
@ -49,12 +49,12 @@ smtutil::Expression nondetInterface(
unsigned _postIdx)
{
auto const& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(), state.abi(), state.crypto()};
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress()/*, state.abi(), state.crypto()*/};
return _pred(
stateExprs +
vector<smtutil::Expression>{_context.state().state(_preIdx)} +
//vector<smtutil::Expression>{_context.state().state(_preIdx)} +
stateVariablesAtIndex(_preIdx, _contract, _context) +
vector<smtutil::Expression>{_context.state().state(_postIdx)} +
//vector<smtutil::Expression>{_context.state().state(_postIdx)} +
stateVariablesAtIndex(_postIdx, _contract, _context)
);
}
@ -66,7 +66,7 @@ smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _contex
return _pred(currentFunctionVariablesForDefinition(*constructor, &contract, _context));
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0), state.state()};
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0)/*, state.abi(0), state.crypto(0), state.tx(0), state.state(0), state.state()*/};
return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context));
}
@ -77,9 +77,9 @@ smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _co
return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context));
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
state.newState();
stateExprs += vector<smtutil::Expression>{state.state()};
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0)/*, state.abi(0), state.crypto(0), state.tx(0), state.state()*/};
//state.newState();
//stateExprs += vector<smtutil::Expression>{state.state()};
stateExprs += currentStateVariables(contract, _context);
stateExprs += newStateVariables(contract, _context);
return _pred(stateExprs);
@ -153,10 +153,10 @@ vector<smtutil::Expression> currentFunctionVariablesForDefinition(
)
{
auto& state = _context.state();
vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0)};
vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0)/*, state.abi(0), state.crypto(0), state.tx(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 += 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(); });
@ -170,13 +170,13 @@ vector<smtutil::Expression> currentFunctionVariablesForCall(
)
{
auto& state = _context.state();
vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0)/*, state.abi(0), state.crypto(0), state.tx(0), state.state()*/};
exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
state.newState();
//state.newState();
exprs += vector<smtutil::Expression>{state.state()};
//exprs += vector<smtutil::Expression>{state.state()};
exprs += _contract ? newStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->increaseIndex(); });
exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });

18
libsolidity/formal/PredicateSort.cpp
View File

@ -31,7 +31,7 @@ namespace solidity::frontend::smt
SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
{
return make_shared<FunctionSort>(
vector<SortPointer>{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
vector<SortPointer>{_state.thisAddressSort()/*, _state.abiSort(), _state.cryptoSort(), _state.stateSort()*/} + stateSorts(_contract),
SortProvider::boolSort
);
}
@ -39,12 +39,12 @@ SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _s
SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
{
auto varSorts = stateSorts(_contract);
vector<SortPointer> stateSort{_state.stateSort()};
//vector<SortPointer> stateSort{_state.stateSort()};
return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} +
stateSort +
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort()/*, _state.abiSort(), _state.cryptoSort()*/} +
//stateSort +
varSorts +
stateSort +
//stateSort +
varSorts,
SortProvider::boolSort
);
@ -56,9 +56,9 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
return functionSort(*constructor, &_contract, _state);
auto varSorts = stateSorts(_contract);
vector<SortPointer> stateSort{_state.stateSort()};
//vector<SortPointer> stateSort{_state.stateSort()};
return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort()/*, _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()*/} + varSorts + varSorts,
SortProvider::boolSort
);
}
@ -70,10 +70,10 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition
auto inputSorts = applyMap(_function.parameters(), smtSort);
auto outputSorts = applyMap(_function.returnParameters(), smtSort);
return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort()/*, _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()*/} +
varSorts +
inputSorts +
vector<SortPointer>{_state.stateSort()} +
//vector<SortPointer>{_state.stateSort()} +
varSorts +
inputSorts +
outputSorts,

19
libsolidity/formal/SymbolicState.cpp
View File

@ -75,13 +75,13 @@ void SymbolicState::reset()
{
m_error.resetIndex();
m_thisAddress.resetIndex();
m_state.reset();
m_tx.reset();
m_crypto.reset();
//m_state.reset();
//m_tx.reset();
//m_crypto.reset();
/// We don't reset m_abi's pointer nor clear m_abiMembers on purpose,
/// since it only helps to keep the already generated types.
solAssert(m_abi, "");
m_abi->reset();
//solAssert(m_abi, "");
//m_abi->reset();
}
smtutil::Expression SymbolicState::balances() const
@ -128,6 +128,8 @@ smtutil::Expression SymbolicState::txMember(string const& _member) const
smtutil::Expression SymbolicState::txTypeConstraints() const
{
return smtutil::Expression(true);
return smt::symbolicUnknownConstraints(m_tx.member("block.chainid"), TypeProvider::uint256()) &&
smt::symbolicUnknownConstraints(m_tx.member("block.coinbase"), TypeProvider::address()) &&
smt::symbolicUnknownConstraints(m_tx.member("block.difficulty"), TypeProvider::uint256()) &&
@ -142,11 +144,14 @@ smtutil::Expression SymbolicState::txTypeConstraints() const
smtutil::Expression SymbolicState::txNonPayableConstraint() const
{
return smtutil::Expression(true);
return m_tx.member("msg.value") == 0;
}
smtutil::Expression SymbolicState::txFunctionConstraints(FunctionDefinition const& _function) const
{
return smtutil::Expression(true);
smtutil::Expression conj = _function.isPayable() ? smtutil::Expression(true) : txNonPayableConstraint();
if (_function.isPartOfExternalInterface())
{
@ -169,12 +174,14 @@ smtutil::Expression SymbolicState::txFunctionConstraints(FunctionDefinition cons
return conj;
}
void SymbolicState::prepareForSourceUnit(SourceUnit const& _source)
void SymbolicState::prepareForSourceUnit(SourceUnit const& /*_source*/)
{
/*
set<FunctionCall const*> abiCalls = SMTEncoder::collectABICalls(&_source);
for (auto const& source: _source.referencedSourceUnits(true))
abiCalls += SMTEncoder::collectABICalls(source);
buildABIFunctions(abiCalls);
*/
}
/// Private helpers.

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

@ -24,7 +24,7 @@ contract C {
// Fails due to j.
function i() public view {
// Disabled because Spacer 4.8.9 seg faults.
//assert(x < 2);
assert(x < 2);
}
}
// ====