Merge pull request #5272 from ethereum/smt_special_vars

[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash

1 files changed, 10 insertions, 6 deletions

diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index f66693d2..95e01708 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -66,6 +66,7 @@ private:
 	virtual void endVisit(Identifier const& _node) override;
 	virtual void endVisit(Literal const& _node) override;
 	virtual void endVisit(Return const& _node) override;
+	virtual bool visit(MemberAccess const& _node) override;
 
 	void arithmeticOperation(BinaryOperation const& _op);
 	void compareOperation(BinaryOperation const& _op);
@@ -73,10 +74,14 @@ private:
 
 	void visitAssert(FunctionCall const&);
 	void visitRequire(FunctionCall const&);
+	void visitGasLeft(FunctionCall const&);
+	void visitBlockHash(FunctionCall const&);
 	/// Visits the FunctionDefinition of the called function
 	/// if available and inlines the return value.
 	void inlineFunctionCall(FunctionCall const&);
 
+	void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
+
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
 	smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
@@ -129,8 +134,6 @@ private:
 	/// This fails if the type is not supported.
 	bool createVariable(VariableDeclaration const& _varDecl);
 
-	static std::string uniqueSymbol(Expression const& _expr);
-
 	/// @returns true if _delc is a variable that is known at the current point, i.e.
 	/// has a valid index
 	bool knownVariable(VariableDeclaration const& _decl);
@@ -154,10 +157,13 @@ private:
 	/// Creates the expression (value can be arbitrary)
 	void createExpr(Expression const& _e);
 	/// Checks if expression was created
-	bool hasExpr(Expression const& _e) const;
+	bool knownExpr(Expression const& _e) const;
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smt::Expression _value);
 
+	/// Checks if special variable was seen.
+	bool knownSpecialVariable(std::string const& _var) const;
+
 	/// Adds a new path condition
 	void pushPathCondition(smt::Expression const& _e);
 	/// Remove the last path condition
@@ -172,9 +178,6 @@ private:
 	/// Removes local variables from the context.
 	void removeLocalVariables();
 
-	/// Checks if VariableDeclaration was seen.
-	bool hasVariable(VariableDeclaration const& _e) const;
-
 	/// Copy the SSA indices of m_variables.
 	VariableIndices copyVariableIndices();
 	/// Resets the variable indices.
@@ -187,6 +190,7 @@ private:
 	/// repeated calls to the same function.
 	std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
 	std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
+	std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_specialVariables;
 	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;