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

removed extra parameter from PredicateInstance::nondetInterface

Browse Source
This commit is contained in:
Martin Blicha 2020-12-28 19:48:48 +01:00
parent 58731056a3
commit bb0003f5ea
4 changed files with 10 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libsolidity/formal/CHC.cpp
View File

@ -899,7 +899,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
/// 0 steps to be taken, used as base for the inductive /// 0 steps to be taken, used as base for the inductive
/// rule for each function. /// rule for each function.
auto const& iface = *m_nondetInterfaces.at(contract); auto const& iface = *m_nondetInterfaces.at(contract);
addRule(smt::nondetInterface(iface, *contract, m_context, smtutil::Expression(size_t(0)), 0, 0), "base_nondet"); addRule(smtutil::Expression::implies(errorFlag().currentValue() == 0, smt::nondetInterface(iface, *contract, m_context, 0, 0)), "base_nondet");
for (auto const* function: contractFunctions(*contract)) for (auto const* function: contractFunctions(*contract))
{ {
@ -917,10 +917,12 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
auto state1 = stateVariablesAtIndex(1, *contract); auto state1 = stateVariablesAtIndex(1, *contract);
auto state2 = stateVariablesAtIndex(2, *contract); auto state2 = stateVariablesAtIndex(2, *contract);
auto nondetPre = smt::nondetInterface(iface, *contract, m_context, smtutil::Expression(size_t(0)), 0, 1); auto errorPre = errorFlag().currentValue();
auto nondetPost = smt::nondetInterface(iface, *contract, m_context, errorFlag().currentValue(), 0, 2); auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
auto errorPost = errorFlag().increaseIndex();
auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
vector<smtutil::Expression> args{errorFlag().currentValue(), 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 + 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)} +
@ -928,7 +930,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) + applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) +
applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }); applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
connectBlocks(nondetPre, nondetPost, (*m_summaries.at(contract).at(function))(args)); connectBlocks(nondetPre, nondetPost, errorPre == 0 && (*m_summaries.at(contract).at(function))(args));
} }
} }
} }

3
libsolidity/formal/PredicateInstance.cpp
View File

@ -45,12 +45,11 @@ smtutil::Expression nondetInterface(
Predicate const& _pred, Predicate const& _pred,
ContractDefinition const& _contract, ContractDefinition const& _contract,
EncodingContext& _context, EncodingContext& _context,
smtutil::Expression const& _error,
unsigned _preIdx, unsigned _preIdx,
unsigned _postIdx) unsigned _postIdx)
{ {
auto const& state = _context.state(); auto const& state = _context.state();
vector<smtutil::Expression> stateExprs{_error, state.thisAddress(), state.abi(), state.crypto()}; vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(), state.abi(), state.crypto()};
return _pred( return _pred(
stateExprs + stateExprs +
vector<smtutil::Expression>{_context.state().state(_preIdx)} + vector<smtutil::Expression>{_context.state().state(_preIdx)} +

2
libsolidity/formal/PredicateInstance.h
View File

@ -34,7 +34,7 @@ smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition cons
smtutil::Expression interface(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, smtutil::Expression const& _error, unsigned _preIdx, unsigned _postIdx); smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx);
smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _context); smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _context);
smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context); smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context);

1
libsolidity/formal/SymbolicState.h
View File

@ -88,6 +88,7 @@ public:
/// Error flag. /// Error flag.
//@{ //@{
SymbolicIntVariable& errorFlag() { return m_error; } SymbolicIntVariable& errorFlag() { return m_error; }
SymbolicIntVariable const& errorFlag() const { return m_error; }
smtutil::SortPointer const& errorFlagSort() const { return m_error.sort(); } smtutil::SortPointer const& errorFlagSort() const { return m_error.sort(); }
//@} //@}