Merge pull request #241 from chriseth/why3VariablesInConditions

Why3 variables in conditions

2 files changed, 114 insertions, 18 deletions

diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index 4c187a56..356a336c 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());
@@ -452,29 +465,48 @@ bool Why3Translator::visit(FunctionCall const& _node)
 		return true;
 	}
 	FunctionType const& function = dynamic_cast<FunctionType const&>(*_node.expression().annotation().type);
-	if (function.location() != FunctionType::Location::Internal)
+	switch (function.location())
 	{
-		error(_node, "Only internal function calls supported.");
-		return true;
-	}
-	if (!_node.names().empty())
+	case FunctionType::Location::AddMod:
+	case FunctionType::Location::MulMod:
 	{
-		error(_node, "Function calls with named arguments not supported.");
-		return true;
+		//@todo require that third parameter is not zero
+		add("(of_int (mod (Int.(");
+		add(function.location() == FunctionType::Location::AddMod ? "+" : "*");
+		add(") (to_int ");
+		_node.arguments().at(0)->accept(*this);
+		add(") (to_int ");
+		_node.arguments().at(1)->accept(*this);
+		add(")) (to_int ");
+		_node.arguments().at(2)->accept(*this);
+		add(")))");
+		return false;
 	}
+	case FunctionType::Location::Internal:
+	{
+		if (!_node.names().empty())
+		{
+			error(_node, "Function calls with named arguments not supported.");
+			return true;
+		}
 
-	//@TODO check type conversions
+		//@TODO check type conversions
 
-	add("(");
-	_node.expression().accept(*this);
-	add(" state");
-	for (auto const& arg: _node.arguments())
-	{
-		add(" ");
-		arg->accept(*this);
+		add("(");
+		_node.expression().accept(*this);
+		add(" state");
+		for (auto const& arg: _node.arguments())
+		{
+			add(" ");
+			arg->accept(*this);
+		}
+		add(")");
+		return false;
+	}
+	default:
+		error(_node, "Only internal function calls supported.");
+		return true;
 	}
-	add(")");
-	return false;
 }
 
 bool Why3Translator::visit(MemberAccess const& _node)
@@ -569,6 +601,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 +641,40 @@ 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 989047e8..21dafa3c 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;