solidity/libsolidity/formal/EncodingContext.h

187 lines
6.2 KiB
C
Raw Normal View History

2019-04-17 13:55:46 +00:00
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#pragma once
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/formal/SymbolicVariables.h>
#include <unordered_map>
#include <set>
2019-12-11 16:31:36 +00:00
namespace solidity::frontend::smt
2019-04-17 13:55:46 +00:00
{
/**
* Stores the context of the SMT encoding.
*/
class EncodingContext
{
public:
EncodingContext();
2019-04-17 13:55:46 +00:00
/// Resets the entire context except for symbolic variables which stay
/// alive because of state variables and inlined function calls.
/// To be used in the beginning of a root function visit.
2019-04-17 13:55:46 +00:00
void reset();
/// Clears the entire context, erasing everything.
/// To be used before a model checking engine starts.
void clear();
2019-04-17 13:55:46 +00:00
/// Sets the current solver used by the current engine for
/// SMT variable declaration.
void setSolver(SolverInterface* _solver)
{
solAssert(_solver, "");
m_solver = _solver;
}
/// Sets whether the context should conjoin assertions in the assertion stack.
void setAssertionAccumulation(bool _acc) { m_accumulateAssertions = _acc; }
/// Forwards variable creation to the solver.
Expression newVariable(std::string _name, SortPointer _sort)
{
solAssert(m_solver, "");
return m_solver->newVariable(move(_name), move(_sort));
}
/// Variables.
//@{
/// @returns the symbolic representation of a program variable.
2019-12-11 16:31:36 +00:00
std::shared_ptr<SymbolicVariable> variable(frontend::VariableDeclaration const& _varDecl);
/// @returns all symbolic variables.
2019-12-11 16:31:36 +00:00
std::unordered_map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> const& variables() const { return m_variables; }
/// Creates a symbolic variable and
/// @returns true if a variable's type is not supported and is therefore abstract.
2019-12-11 16:31:36 +00:00
bool createVariable(frontend::VariableDeclaration const& _varDecl);
/// @returns true if variable was created.
2019-12-11 16:31:36 +00:00
bool knownVariable(frontend::VariableDeclaration const& _varDecl);
/// Resets a specific variable.
2019-12-11 16:31:36 +00:00
void resetVariable(frontend::VariableDeclaration const& _variable);
/// Resets a set of variables.
2019-12-11 16:31:36 +00:00
void resetVariables(std::set<frontend::VariableDeclaration const*> const& _variables);
/// Resets variables according to a predicate.
2019-12-11 16:31:36 +00:00
void resetVariables(std::function<bool(frontend::VariableDeclaration const&)> const& _filter);
///Resets all variables.
void resetAllVariables();
2019-04-17 13:55:46 +00:00
/// Allocates a new index for the declaration, updates the current
/// index to this value and returns the expression.
2019-12-11 16:31:36 +00:00
Expression newValue(frontend::VariableDeclaration const& _decl);
/// Sets the value of the declaration to zero.
2019-12-11 16:31:36 +00:00
void setZeroValue(frontend::VariableDeclaration const& _decl);
void setZeroValue(SymbolicVariable& _variable);
/// Resets the variable to an unknown value (in its range).
2019-12-11 16:31:36 +00:00
void setUnknownValue(frontend::VariableDeclaration const& decl);
void setUnknownValue(SymbolicVariable& _variable);
//@}
/// Expressions.
////@{
/// @returns the symbolic representation of an AST node expression.
2019-12-11 16:31:36 +00:00
std::shared_ptr<SymbolicVariable> expression(frontend::Expression const& _e);
/// @returns all symbolic expressions.
2019-12-11 16:31:36 +00:00
std::unordered_map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>> const& expressions() const { return m_expressions; }
/// Creates the expression (value can be arbitrary).
/// @returns true if type is not supported.
2019-12-11 16:31:36 +00:00
bool createExpression(frontend::Expression const& _e, std::shared_ptr<SymbolicVariable> _symbExpr = nullptr);
/// Checks if expression was created.
2019-12-11 16:31:36 +00:00
bool knownExpression(frontend::Expression const& _e) const;
//@}
/// Global variables and functions.
//@{
/// Global variables and functions.
std::shared_ptr<SymbolicVariable> globalSymbol(std::string const& _name);
/// @returns all symbolic globals.
std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> const& globalSymbols() const { return m_globalContext; }
/// Defines a new global variable or function
/// and @returns true if type was abstracted.
2019-12-11 16:31:36 +00:00
bool createGlobalSymbol(std::string const& _name, frontend::Expression const& _expr);
/// Checks if special variable or function was seen.
bool knownGlobalSymbol(std::string const& _var) const;
//@}
/// Blockchain.
//@{
/// Value of `this` address.
Expression thisAddress();
2019-04-11 16:14:48 +00:00
/// @returns the symbolic balance of address `this`.
Expression balance();
2019-04-11 16:14:48 +00:00
/// @returns the symbolic balance of an address.
Expression balance(Expression _address);
2019-04-11 16:14:48 +00:00
/// Transfer _value from _from to _to.
void transfer(Expression _from, Expression _to, Expression _value);
//@}
2019-04-11 16:14:48 +00:00
/// Solver.
//@{
/// @returns conjunction of all added assertions.
Expression assertions();
void pushSolver();
void popSolver();
void addAssertion(Expression const& _e);
SolverInterface* solver()
{
solAssert(m_solver, "");
return m_solver;
}
//@}
2019-04-17 13:55:46 +00:00
private:
2019-04-11 16:14:48 +00:00
/// Adds _value to _account's balance.
void addBalance(Expression _account, Expression _value);
2019-04-11 16:14:48 +00:00
/// Symbolic expressions.
//{@
/// Symbolic variables.
2019-12-11 16:31:36 +00:00
std::unordered_map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
/// Symbolic expressions.
2019-12-11 16:31:36 +00:00
std::unordered_map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
/// Symbolic representation of global symbols including
/// variables and functions.
std::unordered_map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
2019-04-17 13:55:46 +00:00
/// Symbolic `this` address.
std::unique_ptr<SymbolicAddressVariable> m_thisAddress;
2019-04-11 16:14:48 +00:00
/// Symbolic balances.
std::unique_ptr<SymbolicVariable> m_balances;
//@}
/// Solver related.
//@{
/// Solver can be SMT solver or Horn solver in the future.
SolverInterface* m_solver = nullptr;
/// Assertion stack.
std::vector<Expression> m_assertions;
/// Whether to conjoin assertions in the assertion stack.
bool m_accumulateAssertions = true;
//@}
2019-04-17 13:55:46 +00:00
};
}