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 #pragma once 20 21 #include <libsolidity/formal/SymbolicState.h> 22 #include <libsolidity/formal/SymbolicVariables.h> 23 24 #include <libsmtutil/SolverInterface.h> 25 26 #include <map> 27 28 namespace solidity::frontend::smt 29 { 30 31 /** 32 * Stores the context of the SMT encoding. 33 */ 34 class EncodingContext 35 { 36 public: 37 EncodingContext(); 38 39 /// Resets the entire context except for symbolic variables which stay 40 /// alive because of state variables and inlined function calls. 41 /// To be used in the beginning of a root function visit. 42 void reset(); 43 /// Resets the fresh id for slack variables. 44 void resetUniqueId(); 45 /// Returns the current fresh slack id and increments it. 46 unsigned newUniqueId(); 47 /// Clears the entire context, erasing everything. 48 /// To be used before a model checking engine starts. 49 void clear(); 50 51 /// Sets the current solver used by the current engine for 52 /// SMT variable declaration. setSolver(smtutil::SolverInterface * _solver)53 void setSolver(smtutil::SolverInterface* _solver) 54 { 55 solAssert(_solver, ""); 56 m_solver = _solver; 57 } 58 59 /// Sets whether the context should conjoin assertions in the assertion stack. setAssertionAccumulation(bool _acc)60 void setAssertionAccumulation(bool _acc) { m_accumulateAssertions = _acc; } 61 62 /// Forwards variable creation to the solver. newVariable(std::string _name,smtutil::SortPointer _sort)63 smtutil::Expression newVariable(std::string _name, smtutil::SortPointer _sort) 64 { 65 solAssert(m_solver, ""); 66 return m_solver->newVariable(move(_name), move(_sort)); 67 } 68 69 struct IdCompare 70 { operatorIdCompare71 bool operator()(ASTNode const* lhs, ASTNode const* rhs) const 72 { 73 return lhs->id() < rhs->id(); 74 } 75 }; 76 77 /// Variables. 78 //@{ 79 /// @returns the symbolic representation of a program variable. 80 std::shared_ptr<SymbolicVariable> variable(frontend::VariableDeclaration const& _varDecl); 81 /// @returns all symbolic variables. variables()82 std::map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>, IdCompare> const& variables() const { return m_variables; } 83 84 /// Creates a symbolic variable and 85 /// @returns true if a variable's type is not supported and is therefore abstract. 86 bool createVariable(frontend::VariableDeclaration const& _varDecl); 87 /// @returns true if variable was created. 88 bool knownVariable(frontend::VariableDeclaration const& _varDecl); 89 90 /// Resets a specific variable. 91 void resetVariable(frontend::VariableDeclaration const& _variable); 92 /// Resets a set of variables. 93 void resetVariables(std::set<frontend::VariableDeclaration const*> const& _variables); 94 /// Resets variables according to a predicate. 95 void resetVariables(std::function<bool(frontend::VariableDeclaration const&)> const& _filter); 96 ///Resets all variables. 97 void resetAllVariables(); 98 99 /// Allocates a new index for the declaration, updates the current 100 /// index to this value and returns the expression. 101 smtutil::Expression newValue(frontend::VariableDeclaration const& _decl); 102 /// Sets the value of the declaration to zero. 103 void setZeroValue(frontend::VariableDeclaration const& _decl); 104 void setZeroValue(SymbolicVariable& _variable); 105 /// Resets the variable to an unknown value (in its range). 106 void setUnknownValue(frontend::VariableDeclaration const& decl); 107 void setUnknownValue(SymbolicVariable& _variable); 108 //@} 109 110 /// Expressions. 111 ////@{ 112 /// @returns the symbolic representation of an AST node expression. 113 std::shared_ptr<SymbolicVariable> expression(frontend::Expression const& _e); 114 /// @returns all symbolic expressions. expressions()115 std::map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>, IdCompare> const& expressions() const { return m_expressions; } 116 117 /// Creates the expression (value can be arbitrary). 118 /// @returns true if type is not supported. 119 bool createExpression(frontend::Expression const& _e, std::shared_ptr<SymbolicVariable> _symbExpr = nullptr); 120 /// Checks if expression was created. 121 bool knownExpression(frontend::Expression const& _e) const; 122 //@} 123 124 /// Global variables and functions. 125 //@{ 126 /// Global variables and functions. 127 std::shared_ptr<SymbolicVariable> globalSymbol(std::string const& _name); 128 /// @returns all symbolic globals. globalSymbols()129 std::map<std::string, std::shared_ptr<SymbolicVariable>> const& globalSymbols() const { return m_globalContext; } 130 131 /// Defines a new global variable or function 132 /// and @returns true if type was abstracted. 133 bool createGlobalSymbol(std::string const& _name, frontend::Expression const& _expr); 134 /// Checks if special variable or function was seen. 135 bool knownGlobalSymbol(std::string const& _var) const; 136 //@} 137 138 /// Solver. 139 //@{ 140 /// @returns conjunction of all added assertions. 141 smtutil::Expression assertions(); 142 void pushSolver(); 143 void popSolver(); 144 void addAssertion(smtutil::Expression const& _e); solverStackHeigh()145 size_t solverStackHeigh() { return m_assertions.size(); } const solver()146 smtutil::SolverInterface* solver() 147 { 148 solAssert(m_solver, ""); 149 return m_solver; 150 } 151 //@} 152 state()153 SymbolicState& state() { return m_state; } 154 155 private: 156 /// Symbolic expressions. 157 //{@ 158 /// Symbolic variables. 159 std::map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>, IdCompare> m_variables; 160 161 /// Symbolic expressions. 162 std::map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>, IdCompare> m_expressions; 163 164 /// Symbolic representation of global symbols including 165 /// variables and functions. 166 std::map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext; 167 168 /// Symbolic representation of the blockchain state. 169 SymbolicState m_state; 170 //@} 171 172 /// Solver related. 173 //@{ 174 /// Solver can be SMT solver or Horn solver in the future. 175 smtutil::SolverInterface* m_solver = nullptr; 176 177 /// Assertion stack. 178 std::vector<smtutil::Expression> m_assertions; 179 180 /// Whether to conjoin assertions in the assertion stack. 181 bool m_accumulateAssertions = true; 182 //@} 183 184 /// Central source of unique ids. 185 unsigned m_nextUniqueId = 0; 186 }; 187 188 } 189