cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] Support selfdestruct

Browse Source
This commit is contained in:
Leo Alt 2022-05-15 16:46:35 +02:00
parent 80d49f3702
commit ed3b70b024
9 changed files with 86 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
libsolidity/formal/CHC.cpp
View File

@ -174,6 +174,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
smtutil::Expression zeroes(true);
for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
zeroes = zeroes && currentValue(*var) == smt::zeroValue(var->type());
zeroes = zeroes && state().destructedFlag() == 0;
// The contract's address might already have funds before deployment,
// so the balance must be at least `msg.value`, but not equals.
auto initialBalanceConstraint = state().balance(state().thisAddress()) >= state().txMember("msg.value");
@ -214,9 +215,12 @@ void CHC::endVisit(ContractDefinition const& _contract)
for (auto base: _contract.annotation().linearizedBaseContracts | ranges::views::reverse)
{
errorFlag().increaseIndex();
auto destructedPre = state().destructedFlag();
m_context.addAssertion(smt::constructorCall(*m_contractInitializers.at(&_contract).at(base), m_context));
connectBlocks(m_currentBlock, summary(_contract), errorFlag().currentValue() > 0);
auto destructedPost = state().destructedFlag();
m_context.addAssertion(errorFlag().currentValue() == 0);
m_context.addAssertion(state().newDestructedFlag() == destructedPre + destructedPost);
}
connectBlocks(m_currentBlock, summary(_contract));
@ -231,7 +235,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
if (!constructor || !constructor->isPayable())
txConstraints = txConstraints && state().txNonPayableConstraint();
m_queryPlaceholders[&_contract].push_back({txConstraints, errorFlag().currentValue(), m_currentBlock});
connectBlocks(m_currentBlock, interface(), txConstraints && errorFlag().currentValue() == 0);
connectBlocks(m_currentBlock, interface(), txConstraints && errorFlag().currentValue() == 0 && state().destructedFlag() == 0);
}
solAssert(m_scopes.back() == &_contract, "");
@ -258,7 +262,7 @@ bool CHC::visit(FunctionDefinition const& _function)
)
conj = conj && currentEqualInitialVarsConstraints(stateVariablesIncludingInheritedAndPrivate(_function));
conj = conj && errorFlag().currentValue() == 0;
conj = conj && errorFlag().currentValue() == 0 && state().destructedFlag() == 0;
addRule(smtutil::Expression::implies(conj, summary(_function)), "summary_function_" + to_string(_function.id()));
return false;
}
@ -335,7 +339,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
auto sum = externalSummary(_function);
m_queryPlaceholders[&_function].push_back({sum, errorFlag().currentValue(), ifacePre});
connectBlocks(ifacePre, interface(), sum && errorFlag().currentValue() == 0);
connectBlocks(ifacePre, interface(), sum && errorFlag().currentValue() == 0 && state().destructedFlag(0) == 0);
}
m_currentFunction = nullptr;
@ -565,6 +569,7 @@ void CHC::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::MulMod:
case FunctionType::Kind::Unwrap:
case FunctionType::Kind::Wrap:
case FunctionType::Kind::Selfdestruct:
[[fallthrough]];
default:
SMTEncoder::endVisit(_funCall);
@ -738,6 +743,8 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
m_callGraph[m_currentContract].insert(function);
}
auto destructedPre = state().destructedFlag();
m_context.addAssertion(predicate(_funCall));
solAssert(m_errorDest, "");
@ -747,6 +754,8 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
errorFlag().currentValue() > 0
);
m_context.addAssertion(errorFlag().currentValue() == 0);
auto destructedPost = state().destructedFlag();
m_context.addAssertion(state().newDestructedFlag() == destructedPre + destructedPost);
}
void CHC::externalFunctionCall(FunctionCall const& _funCall)
@ -811,6 +820,8 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
}
auto error = errorFlag().increaseIndex();
auto destructedPre = state().destructedFlag();
auto destructedPost = state().newDestructedFlag();
Predicate const& callPredicate = *createSymbolicBlock(
nondetInterfaceSort(*m_currentContract, state()),
@ -819,7 +830,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
&_funCall
);
auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
vector<smtutil::Expression> stateExprs{error, state().thisAddress(), state().abi(), state().crypto()};
vector<smtutil::Expression> stateExprs{error, destructedPost, state().thisAddress(), state().abi(), state().crypto()};
auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState);
auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
@ -838,6 +849,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
m_callGraph[m_currentFunction].insert(definedFunction);
m_context.addAssertion(errorFlag().currentValue() == 0);
m_context.addAssertion(state().newDestructedFlag() == destructedPre + destructedPost);
}
void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
@ -1176,11 +1188,17 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
auto state2 = stateVariablesAtIndex(2, *contract);
auto errorPre = errorFlag().currentValue();
auto destructedPre = state().destructedFlag();
auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
auto errorPost = errorFlag().increaseIndex();
auto destructedPost = state().newDestructedFlag();
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)};
auto destructedSummary = state().newDestructedFlag();
m_context.addAssertion(destructedPost == destructedPre + destructedSummary);
vector<smtutil::Expression> args{errorPost, destructedPre + destructedPost, 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)} +
@ -1218,6 +1236,7 @@ void CHC::defineExternalFunctionInterface(FunctionDefinition const& _function, C
state().addBalance(state().thisAddress(), k.currentValue());
errorFlag().increaseIndex();
state().newDestructedFlag();
m_context.addAssertion(summaryCall(_function));
connectBlocks(functionPred, externalSummary(_function));
@ -1249,9 +1268,13 @@ void CHC::defineContractInitializer(ContractDefinition const& _contract, Contrac
if (auto constructor = _contract.constructor())
{
errorFlag().increaseIndex();
auto destructedPre = state().destructedFlag();
state().newDestructedFlag();
m_context.addAssertion(smt::functionCall(*m_summaries.at(&_contextContract).at(constructor), &_contextContract, m_context));
connectBlocks(m_currentBlock, initializer(_contract, _contextContract), errorFlag().currentValue() > 0);
m_context.addAssertion(errorFlag().currentValue() == 0);
auto destructedPost = state().destructedFlag();
m_context.addAssertion(state().newDestructedFlag() == destructedPre + destructedPost);
}
connectBlocks(m_currentBlock, initializer(_contract, _contextContract));
@ -1495,7 +1518,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(), state().newDestructedFlag(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()};
auto const* contract = function->annotation().contract;
auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;

22
libsolidity/formal/Predicate.cpp
View File

@ -272,7 +272,7 @@ string Predicate::formatSummaryCall(
}
// Here we are interested in txData from the summary predicate.
auto txValues = readTxVars(_args.at(4));
auto txValues = readTxVars(_args.at(5));
vector<string> values;
for (auto const& _var: txVars)
if (auto v = txValues.at(_var))
@ -290,7 +290,7 @@ string Predicate::formatSummaryCall(
auto const* fun = programFunction();
solAssert(fun, "");
auto first = _args.begin() + 6 + static_cast<int>(stateVars->size());
auto first = _args.begin() + 7 + static_cast<int>(stateVars->size());
auto last = first + static_cast<int>(fun->parameters().size());
solAssert(first >= _args.begin() && first <= _args.end(), "");
solAssert(last >= _args.begin() && last <= _args.end(), "");
@ -334,12 +334,12 @@ vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expressio
vector<smtutil::Expression>::const_iterator stateLast;
if (auto const* function = programFunction())
{
stateFirst = _args.begin() + 6 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
stateFirst = _args.begin() + 7 + 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() + 7 + static_cast<int>(stateVars->size());
stateFirst = _args.begin() + 8 + static_cast<int>(stateVars->size());
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else
@ -366,7 +366,7 @@ vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expre
auto const& inParams = function->parameters();
auto first = _args.begin() + 6 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
auto first = _args.begin() + 7 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
auto last = first + static_cast<int>(inParams.size());
solAssert(first >= _args.begin() && first <= _args.end(), "");
@ -390,7 +390,7 @@ vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expr
auto const& inParams = function->parameters();
auto first = _args.begin() + 6 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
auto first = _args.begin() + 7 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
solAssert(first >= _args.begin() && first <= _args.end(), "");
@ -443,10 +443,10 @@ map<string, string> Predicate::expressionSubstitution(smtutil::Expression const&
if (isInterface())
{
solAssert(starts_with(predName, "interface"), "");
subst[_predExpr.arguments.at(0).name] = "address(this)";
solAssert(nArgs == stateVars.size() + 4, "");
subst[_predExpr.arguments.at(1).name] = "address(this)";
solAssert(nArgs == stateVars.size() + 5, "");
for (size_t i = nArgs - stateVars.size(); i < nArgs; ++i)
subst[_predExpr.arguments.at(i).name] = stateVars.at(i - 4)->name();
subst[_predExpr.arguments.at(i).name] = stateVars.at(i - 5)->name();
}
// The signature of a nondet interface predicate is
// nondet_interface(error, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
@ -459,8 +459,8 @@ map<string, string> Predicate::expressionSubstitution(smtutil::Expression const&
{
solAssert(starts_with(predName, "nondet_interface"), "");
subst[_predExpr.arguments.at(0).name] = "<errorCode>";
subst[_predExpr.arguments.at(1).name] = "address(this)";
solAssert(nArgs == stateVars.size() * 2 + 6, "");
subst[_predExpr.arguments.at(2).name] = "address(this)";
solAssert(nArgs == stateVars.size() * 2 + 7, "");
for (size_t i = nArgs - stateVars.size(), s = 0; i < nArgs; ++i, ++s)
subst[_predExpr.arguments.at(i).name] = stateVars.at(s)->name() + "'";
for (size_t i = nArgs - (stateVars.size() * 2 + 1), s = 0; i < nArgs - (stateVars.size() + 1); ++i, ++s)

14
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.destructedFlag(0), 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.destructedFlag(), state.thisAddress(0), state.abi(0), state.crypto(0), state.state()};
return _pred(stateExprs + currentStateVariables(_contract, _context));
}
@ -49,7 +49,7 @@ 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.destructedFlag(), state.thisAddress(), state.abi(), state.crypto()};
return _pred(
stateExprs +
vector<smtutil::Expression>{_context.state().state(_preIdx)} +
@ -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.destructedFlag(), 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,7 +77,7 @@ 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()};
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.destructedFlag(), 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);
@ -153,7 +153,7 @@ 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.destructedFlag(), 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()};
@ -170,7 +170,7 @@ 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.destructedFlag(), 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(); });

8
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.destructedFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
SortProvider::boolSort
);
}
@ -41,7 +41,7 @@ SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicSta
auto varSorts = stateSorts(_contract);
vector<SortPointer> stateSort{_state.stateSort()};
return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} +
vector<SortPointer>{_state.errorFlagSort(), _state.destructedFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} +
stateSort +
varSorts +
stateSort +
@ -58,7 +58,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
auto varSorts = stateSorts(_contract);
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.destructedFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
SortProvider::boolSort
);
}
@ -70,7 +70,7 @@ 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.destructedFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
varSorts +
inputSorts +
vector<SortPointer>{_state.stateSort()} +

10
libsolidity/formal/PredicateSort.h
View File

@ -33,25 +33,25 @@ namespace solidity::frontend::smt
*
* 1. Interface
* The idle state of a contract. Signature:
* interface(this, abiFunctions, cryptoFunctions, blockchainState, stateVariables).
* interface(destructed, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables).
*
* 2. Nondet interface
* The nondeterminism behavior of a contract. Signature:
* nondet_interface(error, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
* nondet_interface(error, destructed, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
*
* 3. Constructor entry/summary
* The summary of a contract's deployment procedure.
* Signature:
* If the contract has a constructor function, this is the same as the summary of that function. Otherwise:
* constructor_summary(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables, stateVariables').
* constructor_summary(error, destructed, this, abiFunctions, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables, stateVariables').
*
* 4. Function entry/summary
* The entry point of a function definition. Signature:
* function_entry(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
* function_entry(error, destructed, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
*
* 5. Function body
* Use for any predicate within a function. Signature:
* function_body(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables).
* function_body(error, destructed, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables).
*/
/// @returns the interface predicate sort for _contract.

12
libsolidity/formal/SMTEncoder.cpp
View File

@ -705,6 +705,9 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::ObjectCreation:
visitObjectCreation(_funCall);
return;
case FunctionType::Kind::Selfdestruct:
visitSelfDestruct(_funCall);
break;
case FunctionType::Kind::DelegateCall:
case FunctionType::Kind::BareCallCode:
case FunctionType::Kind::BareDelegateCall:
@ -909,6 +912,15 @@ void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
m_context.addAssertion(symbArray->elements() == zeroElements);
}
void SMTEncoder::visitSelfDestruct(FunctionCall const& _funCall)
{
auto const& args = _funCall.arguments();
solAssert(args.size() == 1);
solAssert(args.at(0));
state().transfer(state().thisAddress(), expr(*args.at(0)), state().balance(state().thisAddress()));
}
void SMTEncoder::endVisit(Identifier const& _identifier)
{
if (auto decl = identifierToVariable(_identifier))

1
libsolidity/formal/SMTEncoder.h
View File

@ -216,6 +216,7 @@ protected:
virtual void visitAddMulMod(FunctionCall const& _funCall);
void visitWrapUnwrap(FunctionCall const& _funCall);
void visitObjectCreation(FunctionCall const& _funCall);
void visitSelfDestruct(FunctionCall const& _funCall);
void visitTypeConversion(FunctionCall const& _funCall);
void visitStructConstructorCall(FunctionCall const& _funCall);
void visitFunctionIdentifier(Identifier const& _identifier);

1
libsolidity/formal/SymbolicState.cpp
View File

@ -74,6 +74,7 @@ smtutil::Expression BlockchainVariable::assignMember(string const& _member, smtu
void SymbolicState::reset()
{
m_error.resetIndex();
m_destructed.resetIndex();
m_thisAddress.resetIndex();
m_state.reset();
m_tx.reset();

16
libsolidity/formal/SymbolicState.h
View File

@ -59,6 +59,7 @@ private:
/**
* Symbolic representation of the blockchain context:
* - error flag
* - destructed (0: non-destructed, 1: destructed, 2: pending destruction)
* - this (the address of the currently executing contract)
* - state, represented as a tuple of:
* - balances
@ -94,6 +95,14 @@ public:
smtutil::SortPointer const& errorFlagSort() const { return m_error.sort(); }
//@}
/// Destructed flag.
//@{
smtutil::Expression destructedFlag() const { return m_destructed.currentValue(); }
smtutil::Expression destructedFlag(unsigned _idx) const { return m_destructed.valueAtIndex(_idx); }
smtutil::Expression newDestructedFlag() { return m_destructed.increaseIndex(); }
smtutil::SortPointer const& destructedFlagSort() const { return m_destructed.sort(); }
//@}
/// This.
//@{
/// @returns the symbolic value of the currently executing contract's address.
@ -180,6 +189,13 @@ private:
m_context
};
SymbolicIntVariable m_destructed{
TypeProvider::uint256(),
TypeProvider::uint256(),
"destructed",
m_context
};
SymbolicAddressVariable m_thisAddress{
"this",
m_context