cerc-io/solidity
16
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

Sort variables and expressions by AST id

Browse Source
This commit is contained in:
Leonardo Alt 2020-11-06 11:47:31 +00:00
parent f55f5c2424
commit 646be53f2f
3 changed files with 19 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/CHC.cpp
View File

@ -71,7 +71,7 @@ void CHC::analyze(SourceUnit const& _source)
resetSourceAnalysis();
set<SourceUnit const*, IdCompare> sources;
set<SourceUnit const*, EncodingContext::IdCompare> sources;
sources.insert(&_source);
for (auto const& source: _source.referencedSourceUnits(true))
sources.insert(source);

14
libsolidity/formal/CHC.h
View File

@ -100,14 +100,6 @@ private:
) override;
//@}
struct IdCompare
{
bool operator()(ASTNode const* lhs, ASTNode const* rhs) const
{
return lhs->id() < rhs->id();
}
};
/// Helpers.
//@{
void resetSourceAnalysis();
@ -287,12 +279,12 @@ private:
/// Query placeholders for constructors, if the key has type ContractDefinition*,
/// or external functions, if the key has type FunctionDefinition*.
/// A placeholder is created for each possible context of a function (e.g. multiple contracts in contract inheritance hierarchy).
std::map<ASTNode const*, std::vector<CHCQueryPlaceholder>, IdCompare> m_queryPlaceholders;
std::map<ASTNode const*, std::vector<CHCQueryPlaceholder>, smt::EncodingContext::IdCompare> m_queryPlaceholders;
/// Records verification conditions IDs per function encountered during an analysis of that function.
/// The key is the ASTNode of the function where the verification condition has been encountered,
/// or the ASTNode of the contract if the verification condition happens inside an implicit constructor.
std::map<ASTNode const*, std::vector<unsigned>, IdCompare> m_functionTargetIds;
std::map<ASTNode const*, std::vector<unsigned>, smt::EncodingContext::IdCompare> m_functionTargetIds;
/// Helper mapping unique IDs to actual verification targets.
std::map<unsigned, CHCVerificationTarget> m_verificationTargets;
@ -306,7 +298,7 @@ private:
//@{
FunctionDefinition const* m_currentFunction = nullptr;
std::map<ASTNode const*, std::set<ASTNode const*, IdCompare>, IdCompare> m_callGraph;
std::map<ASTNode const*, std::set<ASTNode const*, smt::EncodingContext::IdCompare>, smt::EncodingContext::IdCompare> m_callGraph;
/// The current block.
smtutil::Expression m_currentBlock = smtutil::Expression(true);

23
libsolidity/formal/EncodingContext.h
View File

@ -23,8 +23,7 @@
#include <libsmtutil/SolverInterface.h>
#include <unordered_map>
#include <set>
#include <map>
namespace solidity::frontend::smt
{
@ -67,12 +66,20 @@ public:
return m_solver->newVariable(move(_name), move(_sort));
}
struct IdCompare
{
bool operator()(ASTNode const* lhs, ASTNode const* rhs) const
{
return lhs->id() < rhs->id();
}
};
/// Variables.
//@{
/// @returns the symbolic representation of a program variable.
std::shared_ptr<SymbolicVariable> variable(frontend::VariableDeclaration const& _varDecl);
/// @returns all symbolic variables.
std::unordered_map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> const& variables() const { return m_variables; }
std::map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>, IdCompare> 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.
@ -105,7 +112,7 @@ public:
/// @returns the symbolic representation of an AST node expression.
std::shared_ptr<SymbolicVariable> expression(frontend::Expression const& _e);
/// @returns all symbolic expressions.
std::unordered_map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>> const& expressions() const { return m_expressions; }
std::map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>, IdCompare> const& expressions() const { return m_expressions; }
/// Creates the expression (value can be arbitrary).
/// @returns true if type is not supported.
@ -119,7 +126,7 @@ public:
/// 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; }
std::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.
@ -149,14 +156,14 @@ private:
/// Symbolic expressions.
//{@
/// Symbolic variables.
std::unordered_map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
std::map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>, IdCompare> m_variables;
/// Symbolic expressions.
std::unordered_map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
std::map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>, IdCompare> m_expressions;
/// Symbolic representation of global symbols including
/// variables and functions.
std::unordered_map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
std::map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
/// Symbolic representation of the blockchain state.
SymbolicState m_state;