<commit_before>/*
	This file is part of cpp-ethereum.

	cpp-ethereum is free software: you can redistribute it and/or modify
	it under the terms of the GNU General Public License as published by
	the Free Software Foundation, either version 3 of the License, or
	(at your option) any later version.

	cpp-ethereum is distributed in the hope that it will be useful,
	but WITHOUT ANY WARRANTY; without even the implied warranty of
	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
	GNU General Public License for more details.

	You should have received a copy of the GNU General Public License
	along with cpp-ethereum.  If not, see <http://www.gnu.org/licenses/>.
*/
/**
 * @author Christian <<EMAIL>>
 * @date 2015
 * Component that translates Solidity code into the why3 programming language.
 */

#include <libsolidity/formal/Why3Translator.h>
#include <boost/algorithm/string/predicate.hpp>

using namespace std;
using namespace dev;
using namespace dev::solidity;

bool Why3Translator::process(SourceUnit const& _source)
{
	try
	{
		if (m_lines.size() != 1 || !m_lines.back().contents.empty())
			fatalError(_source, "Multiple source units not yet supported");
		appendPreface();
		_source.accept(*this);
	}
	catch (FatalError& /*_e*/)
	{
		solAssert(m_errorOccured, "");
	}
	return !m_errorOccured;
}

string Why3Translator::translation() const
{
	string result;
	for (auto const& line: m_lines)
		result += string(line.indentation, '\t') + line.contents + "\n";
	return result;
}

void Why3Translator::error(ASTNode const& _node, string const& _description)
{
	auto err = make_shared<Error>(Error::Type::Why3TranslatorError);
	*err <<
		errinfo_sourceLocation(_node.location()) <<
		errinfo_comment(_description);
	m_errors.push_back(err);
	m_errorOccured = true;
}

void Why3Translator::fatalError(ASTNode const& _node, string const& _description)
{
	error(_node, _description);
	BOOST_THROW_EXCEPTION(FatalError());
}

string Why3Translator::toFormalType(Type const& _type) const
{
	if (_type.category() == Type::Category::Bool)
		return "bool";
	else if (auto type = dynamic_cast<IntegerType const*>(&_type))
	{
		if (!type->isAddress() && !type->isSigned() && type->numBits() == 256)
			return "uint256";
	}
	else if (auto type = dynamic_cast<ArrayType const*>(&_type))
		if (!type->isByteArray() && type->isDynamicallySized() && type->dataStoredIn(DataLocation::Memory))
		{
			string base = toFormalType(*type->baseType());
			if (!base.empty())
				return "array " + base;
		}

	return "";
}<commit_msg>Translate mapping types into Why3 arrays when keys are integers<commit_after>/*
	This file is part of cpp-ethereum.

	cpp-ethereum is free software: you can redistribute it and/or modify
	it under the terms of the GNU General Public License as published by
	the Free Software Foundation, either version 3 of the License, or
	(at your option) any later version.

	cpp-ethereum is distributed in the hope that it will be useful,
	but WITHOUT ANY WARRANTY; without even the implied warranty of
	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
	GNU General Public License for more details.

	You should have received a copy of the GNU General Public License
	along with cpp-ethereum.  If not, see <http://www.gnu.org/licenses/>.
*/
/**
 * @author Christian <<EMAIL>>
 * @date 2015
 * Component that translates Solidity code into the why3 programming language.
 */

#include <libsolidity/formal/Why3Translator.h>
#include <boost/algorithm/string/predicate.hpp>

using namespace std;
using namespace dev;
using namespace dev::solidity;

bool Why3Translator::process(SourceUnit const& _source)
{
	try
	{
		if (m_lines.size() != 1 || !m_lines.back().contents.empty())
			fatalError(_source, "Multiple source units not yet supported");
		appendPreface();
		_source.accept(*this);
	}
	catch (FatalError& /*_e*/)
	{
		solAssert(m_errorOccured, "");
	}
	return !m_errorOccured;
}

string Why3Translator::translation() const
{
	string result;
	for (auto const& line: m_lines)
		result += string(line.indentation, '\t') + line.contents + "\n";
	return result;
}

void Why3Translator::error(ASTNode const& _node, string const& _description)
{
	auto err = make_shared<Error>(Error::Type::Why3TranslatorError);
	*err <<
		errinfo_sourceLocation(_node.location()) <<
		errinfo_comment(_description);
	m_errors.push_back(err);
	m_errorOccured = true;
}

void Why3Translator::fatalError(ASTNode const& _node, string const& _description)
{
	error(_node, _description);
	BOOST_THROW_EXCEPTION(FatalError());
}

string Why3Translator::toFormalType(Type const& _type) const
{
	if (_type.category() == Type::Category::Bool)
		return "bool";
	else if (auto type = dynamic_cast<IntegerType const*>(&_type))
	{
		if (!type->isAddress() && !type->isSigned() && type->numBits() == 256)
			return "uint256";
	}
	else if (auto type = dynamic_cast<ArrayType const*>(&_type))
	{
		if (!type->isByteArray() && type->isDynamicallySized() && type->dataStoredIn(DataLocation::Memory))
		{
			string base = toFormalType(*type->baseType());
			if (!base.empty())
				return "array " + base;
		}
	}
	else if (auto mappingType = dynamic_cast<MappingType const*>(&_type))
	{
		solAssert(mappingType->keyType(), "A mappingType misses a keyType.");
		if (dynamic_cast<IntegerType const*>(&*mappingType->keyType()))
		{
			//@TODO Use the information from the key type and specify the length of the array as an invariant.
			// Also the constructor need to specify the length of the array.
			string valueType = toFormalType(*mappingType->valueType());
			if (!valueType.empty())
				return "array " + valueType;
		}
	}

	return "";
}
{'fraction_non_alphanumeric': 0.12517755681818182, 'fraction_numerical': 0.007279829545454545, 'mean_word_length': 4.837305699481865, 'pattern_counts': {'":': 0, '<': 29, '<?xml version=': 0, '>': 38, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2217059', 'n_tokens_mistral': 1887, 'n_tokens_neox': 1772, 'n_words': 541}