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

Add tx constraints to CHC

Browse Source
This commit is contained in:
Leonardo Alt 2020-09-29 14:26:30 +02:00
parent a2cdde1191
commit aec456021d
6 changed files with 26 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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.

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.