From 82a6ab486d6ee1fa565db1d0b02f2b34c855e796 Mon Sep 17 00:00:00 2001
From: chriseth <c@ethdev.com>
Date: Mon, 23 Nov 2015 00:26:04 +0100
Subject: [PATCH] Why3: Direct references to variables using `#`.

---
 libsolidity/formal/Why3Translator.cpp | 69 ++++++++++++++++++++++++++-
 libsolidity/formal/Why3Translator.h   |  7 +++
 2 files changed, 75 insertions(+), 1 deletion(-)

diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index 4c187a56b..8a3b767bc 100644
--- a/libsolidity/formal/Why3Translator.cpp
+++ b/libsolidity/formal/Why3Translator.cpp
@@ -198,6 +198,14 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
 		return false;
 	}
 
+	m_localVariables.clear();
+	for (auto const& var: _function.parameters())
+		m_localVariables[var->name()] = var.get();
+	for (auto const& var: _function.returnParameters())
+		m_localVariables[var->name()] = var.get();
+	for (auto const& var: _function.localVariables())
+		m_localVariables[var->name()] = var;
+
 	add("let rec _" + _function.name());
 	add(" (state: state)");
 	for (auto const& param: _function.parameters())
@@ -268,6 +276,11 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
 	return false;
 }
 
+void Why3Translator::endVisit(FunctionDefinition const&)
+{
+	m_localVariables.clear();
+}
+
 bool Why3Translator::visit(Block const& _node)
 {
 	addSourceFromDocStrings(_node.annotation());
@@ -569,6 +582,28 @@ bool Why3Translator::isStateVariable(VariableDeclaration const* _var) const
 	return false;
 }
 
+bool Why3Translator::isStateVariable(string const& _name) const
+{
+	solAssert(!!m_stateVariables, "");
+	for (auto const& var: *m_stateVariables)
+		if (var->name() == _name)
+			return true;
+	return false;
+}
+
+bool Why3Translator::isLocalVariable(VariableDeclaration const* _var) const
+{
+	for (auto const& var: m_localVariables)
+		if (var.second == _var)
+			return true;
+	return false;
+}
+
+bool Why3Translator::isLocalVariable(string const& _name) const
+{
+	return m_localVariables.count(_name);
+}
+
 void Why3Translator::visitIndentedUnlessBlock(Statement const& _statement)
 {
 	bool isBlock = !!dynamic_cast<Block const*>(&_statement);
@@ -587,5 +622,37 @@ void Why3Translator::addSourceFromDocStrings(DocumentedAnnotation const& _annota
 {
 	auto why3Range = _annotation.docTags.equal_range("why3");
 	for (auto i = why3Range.first; i != why3Range.second; ++i)
-		addLine(i->second.content);
+		addLine(transformVariableReferences(i->second.content));
 }
+
+string Why3Translator::transformVariableReferences(string const& _annotation)
+{
+	string ret;
+	auto pos = _annotation.begin();
+	while (true)
+	{
+
+		auto hash = find(pos, _annotation.end(), '#');
+		ret.append(pos, hash);
+		if (hash == _annotation.end())
+			break;
+
+		auto hashEnd = find_if(hash + 1, _annotation.end(), [](char _c)
+		{
+			return _c != '_' && _c != '$' && !('a' <= _c && _c <= 'z') && !('A' <= _c && _c <= 'Z') && !('0' <= _c && _c <= '9');
+		});
+		string varName(hash + 1, hashEnd);
+		if (isLocalVariable(varName))
+			ret += "(to_int !_" + varName + ")";
+		else if (isStateVariable(varName))
+			ret += "(to_int !(state._" + varName + "))";
+		else if (varName == "result") //@todo actually use the name of the return parameters
+			ret += "(to_int result)";
+		else
+			ret.append(hash, hashEnd);
+
+		pos = hashEnd;
+	}
+	return ret;
+}
+
diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h
index 989047e84..21dafa3c3 100644
--- a/libsolidity/formal/Why3Translator.h
+++ b/libsolidity/formal/Why3Translator.h
@@ -74,6 +74,7 @@ private:
 	virtual bool visit(ContractDefinition const& _contract) override;
 	virtual void endVisit(ContractDefinition const& _contract) override;
 	virtual bool visit(FunctionDefinition const& _function) override;
+	virtual void endVisit(FunctionDefinition const& _function) override;
 	virtual bool visit(Block const&) override;
 	virtual bool visit(IfStatement const& _node) override;
 	virtual bool visit(WhileStatement const& _node) override;
@@ -98,12 +99,17 @@ private:
 	}
 
 	bool isStateVariable(VariableDeclaration const* _var) const;
+	bool isStateVariable(std::string const& _name) const;
+	bool isLocalVariable(VariableDeclaration const* _var) const;
+	bool isLocalVariable(std::string const& _name) const;
 
 	/// Visits the givin statement and indents it unless it is a block
 	/// (which does its own indentation).
 	void visitIndentedUnlessBlock(Statement const& _statement);
 
 	void addSourceFromDocStrings(DocumentedAnnotation const& _annotation);
+	/// Transforms substring like `#varName` and `#stateVarName` to code that evaluates to their value.
+	std::string transformVariableReferences(std::string const& _annotation);
 
 	size_t m_indentationAtLineStart = 0;
 	size_t m_indentation = 0;
@@ -114,6 +120,7 @@ private:
 	bool m_errorOccured = false;
 
 	std::vector<ASTPointer<VariableDeclaration>> const* m_stateVariables = nullptr;
+	std::map<std::string, VariableDeclaration const*> m_localVariables;
 
 	std::string m_result;
 	ErrorList& m_errors;