Why3: Direct references to variables using `#`.

1 files changed, 68 insertions, 1 deletions

diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index 4c187a56..8a3b767b 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;
+}
+