From aec456021d4ac223852227f242952e4d241b0a55 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 29 Sep 2020 14:26:30 +0200 Subject: [PATCH] Add tx constraints to CHC --- libsolidity/formal/CHC.cpp | 11 +++++---- libsolidity/formal/Predicate.cpp | 20 ++++++++-------- libsolidity/formal/PredicateInstance.cpp | 6 ++--- libsolidity/formal/PredicateSort.cpp | 6 ++--- libsolidity/formal/PredicateSort.h | 8 +++---- .../functions/internal_call_inheritance_2.sol | 24 ------------------- 6 files changed, 26 insertions(+), 49 deletions(-) delete mode 100644 test/libsolidity/smtCheckerTests/functions/internal_call_inheritance_2.sol diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index f959c0fed..2356a2b14 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -120,7 +120,7 @@ void CHC::endVisit(ContractDefinition const& _contract) &_contract ); addRule( - (*implicitConstructorPredicate)({0, state().thisAddress(), state().state()}), + (*implicitConstructorPredicate)({0, state().thisAddress(), state().tx(), state().state()}), implicitConstructorPredicate->functor().name ); 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); if (_function.isPublic()) { - addAssertVerificationTarget(&_function, ifacePre, sum, assertionError); - connectBlocks(ifacePre, iface, sum && (assertionError == 0)); + auto txConstraints = m_context.state().txConstraints(_function); + addAssertVerificationTarget(&_function, ifacePre, txConstraints && sum, assertionError); + connectBlocks(ifacePre, iface, txConstraints && sum && (assertionError == 0)); } } m_currentFunction = nullptr; @@ -873,7 +874,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1); auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2); - vector args{errorFlag().currentValue(), state().thisAddress(), state().state(1)}; + vector args{errorFlag().currentValue(), state().thisAddress(), state().tx(), state().state(1)}; args += state1 + applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) + vector{state().state(2)} + @@ -1052,7 +1053,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) return smtutil::Expression(true); errorFlag().increaseIndex(); - vector args{errorFlag().currentValue(), state().thisAddress(), state().state()}; + vector args{errorFlag().currentValue(), state().thisAddress(), state().tx(), state().state()}; FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); solAssert(funType.kind() == FunctionType::Kind::Internal, ""); diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index ca77c3d8d..cdb1ef749 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -161,9 +161,9 @@ string Predicate::formatSummaryCall(vector const& _args) const auto const* fun = programFunction(); 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. - vector::const_iterator first = _args.begin() + 3 + static_cast(stateVars->size()); + vector::const_iterator first = _args.begin() + 4 + static_cast(stateVars->size()); vector::const_iterator last = first + static_cast(fun->parameters().size()); solAssert(first >= _args.begin() && first <= _args.end(), ""); solAssert(last >= _args.begin() && last <= _args.end(), ""); @@ -188,8 +188,8 @@ string Predicate::formatSummaryCall(vector const& _args) const vector Predicate::summaryStateValues(vector const& _args) const { - /// The signature of a function summary predicate is: summary(error, this, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). - /// The signature of an implicit constructor summary predicate is: summary(error, this, postBlockchainState, postStateVars). + /// 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, txData, postBlockchainState, postStateVars). /// Here we are interested in postStateVars. auto stateVars = stateVariables(); @@ -199,12 +199,12 @@ vector Predicate::summaryStateValues(vector const& _args) const vector::const_iterator stateLast; if (auto const* function = programFunction()) { - stateFirst = _args.begin() + 3 + static_cast(stateVars->size()) + static_cast(function->parameters().size()) + 1; + stateFirst = _args.begin() + 4 + static_cast(stateVars->size()) + static_cast(function->parameters().size()) + 1; stateLast = stateFirst + static_cast(stateVars->size()); } else if (programContract()) { - stateFirst = _args.begin() + 3; + stateFirst = _args.begin() + 4; stateLast = stateFirst + static_cast(stateVars->size()); } else @@ -220,7 +220,7 @@ vector Predicate::summaryStateValues(vector const& _args) const vector Predicate::summaryPostInputValues(vector 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. auto const* function = programFunction(); solAssert(function, ""); @@ -230,7 +230,7 @@ vector Predicate::summaryPostInputValues(vector const& _args) co auto const& inParams = function->parameters(); - vector::const_iterator first = _args.begin() + 3 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) + 1; + vector::const_iterator first = _args.begin() + 4 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) + 1; vector::const_iterator last = first + static_cast(inParams.size()); solAssert(first >= _args.begin() && first <= _args.end(), ""); @@ -243,7 +243,7 @@ vector Predicate::summaryPostInputValues(vector const& _args) co vector Predicate::summaryPostOutputValues(vector 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. auto const* function = programFunction(); solAssert(function, ""); @@ -253,7 +253,7 @@ vector Predicate::summaryPostOutputValues(vector const& _args) c auto const& inParams = function->parameters(); - vector::const_iterator first = _args.begin() + 3 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2 + 1; + vector::const_iterator first = _args.begin() + 4 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2 + 1; solAssert(first >= _args.begin() && first <= _args.end(), ""); diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp index 90fceab3c..a6c3adb1c 100644 --- a/libsolidity/formal/PredicateInstance.cpp +++ b/libsolidity/formal/PredicateInstance.cpp @@ -54,7 +54,7 @@ smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition c smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext& _context) { auto& state = _context.state(); - vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state(0)}; + vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0)}; return _pred(stateExprs); } @@ -64,7 +64,7 @@ smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const return _pred(currentFunctionVariables(*constructor, &_contract, _context)); auto& state = _context.state(); - vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state(0), state.state()}; + vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0), state.state()}; return _pred(stateExprs + currentStateVariables(_contract, _context)); } @@ -118,7 +118,7 @@ vector currentFunctionVariables( ) { auto& state = _context.state(); - vector exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.state(0)}; + vector exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0)}; exprs += _contract ? initialStateVariables(*_contract, _context) : vector{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); }); exprs += vector{state.state()}; diff --git a/libsolidity/formal/PredicateSort.cpp b/libsolidity/formal/PredicateSort.cpp index b9e1c1d40..2d5536d19 100644 --- a/libsolidity/formal/PredicateSort.cpp +++ b/libsolidity/formal/PredicateSort.cpp @@ -49,7 +49,7 @@ SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicSta SortPointer implicitConstructorSort(SymbolicState& _state) { return make_shared( - vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()}, + vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort()}, SortProvider::boolSort ); } @@ -60,7 +60,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& return functionSort(*constructor, &_contract, _state); return make_shared( - vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract), + vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract), SortProvider::boolSort ); } @@ -72,7 +72,7 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition auto inputSorts = applyMap(_function.parameters(), smtSort); auto outputSorts = applyMap(_function.returnParameters(), smtSort); return make_shared( - vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()} + + vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort()} + varSorts + inputSorts + vector{_state.stateSort()} + diff --git a/libsolidity/formal/PredicateSort.h b/libsolidity/formal/PredicateSort.h index a2f25e7e4..341f7b7a4 100644 --- a/libsolidity/formal/PredicateSort.h +++ b/libsolidity/formal/PredicateSort.h @@ -41,19 +41,19 @@ namespace solidity::frontend::smt * * 3. Implicit constructor * 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 * 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 * 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 * 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. diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_inheritance_2.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_inheritance_2.sol deleted file mode 100644 index c15affa5c..000000000 --- a/test/libsolidity/smtCheckerTests/functions/internal_call_inheritance_2.sol +++ /dev/null @@ -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.