1 /*
2 This file is part of solidity.
3
4 solidity is free software: you can redistribute it and/or modify
5 it under the terms of the GNU General Public License as published by
6 the Free Software Foundation, either version 3 of the License, or
7 (at your option) any later version.
8
9 solidity is distributed in the hope that it will be useful,
10 but WITHOUT ANY WARRANTY; without even the implied warranty of
11 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 GNU General Public License for more details.
13
14 You should have received a copy of the GNU General Public License
15 along with solidity. If not, see <http://www.gnu.org/licenses/>.
16 */
17 // SPDX-License-Identifier: GPL-3.0
18
19 #include <libsolidity/formal/PredicateSort.h>
20
21 #include <libsolidity/formal/SMTEncoder.h>
22 #include <libsolidity/formal/SymbolicTypes.h>
23
24 using namespace std;
25 using namespace solidity::util;
26 using namespace solidity::smtutil;
27
28 namespace solidity::frontend::smt
29 {
30
interfaceSort(ContractDefinition const & _contract,SymbolicState & _state)31 SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
32 {
33 return make_shared<FunctionSort>(
34 vector<SortPointer>{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
35 SortProvider::boolSort
36 );
37 }
38
nondetInterfaceSort(ContractDefinition const & _contract,SymbolicState & _state)39 SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
40 {
41 auto varSorts = stateSorts(_contract);
42 vector<SortPointer> stateSort{_state.stateSort()};
43 return make_shared<FunctionSort>(
44 vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} +
45 stateSort +
46 varSorts +
47 stateSort +
48 varSorts,
49 SortProvider::boolSort
50 );
51 }
52
constructorSort(ContractDefinition const & _contract,SymbolicState & _state)53 SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state)
54 {
55 if (auto const* constructor = _contract.constructor())
56 return functionSort(*constructor, &_contract, _state);
57
58 auto varSorts = stateSorts(_contract);
59 vector<SortPointer> stateSort{_state.stateSort()};
60 return make_shared<FunctionSort>(
61 vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
62 SortProvider::boolSort
63 );
64 }
65
functionSort(FunctionDefinition const & _function,ContractDefinition const * _contract,SymbolicState & _state)66 SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state)
67 {
68 auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
69 auto varSorts = _contract ? stateSorts(*_contract) : vector<SortPointer>{};
70 auto inputSorts = applyMap(_function.parameters(), smtSort);
71 auto outputSorts = applyMap(_function.returnParameters(), smtSort);
72 return make_shared<FunctionSort>(
73 vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
74 varSorts +
75 inputSorts +
76 vector<SortPointer>{_state.stateSort()} +
77 varSorts +
78 inputSorts +
79 outputSorts,
80 SortProvider::boolSort
81 );
82 }
83
functionBodySort(FunctionDefinition const & _function,ContractDefinition const * _contract,SymbolicState & _state)84 SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state)
85 {
86 auto fSort = dynamic_pointer_cast<FunctionSort>(functionSort(_function, _contract, _state));
87 solAssert(fSort, "");
88
89 auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
90 return make_shared<FunctionSort>(
91 fSort->domain + applyMap(SMTEncoder::localVariablesIncludingModifiers(_function, _contract), smtSort),
92 SortProvider::boolSort
93 );
94 }
95
arity0FunctionSort()96 SortPointer arity0FunctionSort()
97 {
98 return make_shared<FunctionSort>(
99 vector<SortPointer>(),
100 SortProvider::boolSort
101 );
102 }
103
104 /// Helpers
105
stateSorts(ContractDefinition const & _contract)106 vector<SortPointer> stateSorts(ContractDefinition const& _contract)
107 {
108 return applyMap(
109 SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
110 [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }
111 );
112 }
113
114 }
115