cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

toFormalType reports errors by an exception

Browse Source 
This allows error reporting without passing `ASTNode` to `toFormalType()`
This commit is contained in:
Yoichi Hirai 2016-09-07 20:16:46 +02:00
parent c861cf579d
commit ac7c6ae7d2
2 changed files with 71 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

87
libsolidity/formal/Why3Translator.cpp
View File

@ -80,9 +80,9 @@ string Why3Translator::toFormalType(Type const& _type) const
{ {
if (!type->isByteArray() && type->isDynamicallySized() && type->dataStoredIn(DataLocation::Memory)) if (!type->isByteArray() && type->isDynamicallySized() && type->dataStoredIn(DataLocation::Memory))
{ {
// Not catching NoFormalType exception. Let the caller deal with it.
string base = toFormalType(*type->baseType()); string base = toFormalType(*type->baseType());
if (!base.empty()) return "array " + base;
return "array " + base;
} }
} }
else if (auto mappingType = dynamic_cast<MappingType const*>(&_type)) else if (auto mappingType = dynamic_cast<MappingType const*>(&_type))
@ -92,13 +92,15 @@ string Why3Translator::toFormalType(Type const& _type) const
{ {
//@TODO Use the information from the key type and specify the length of the array as an invariant. //@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. // Also the constructor need to specify the length of the array.
string valueType = toFormalType(*mappingType->valueType()); solAssert(mappingType->valueType(), "A mappingType misses a valueType.");
if (!valueType.empty()) // Not catching NoFormalType exception. Let the caller deal with it.
return "array " + valueType; string valueTypeFormal = toFormalType(*mappingType->valueType());
return "array " + valueTypeFormal;
} }
} }
return ""; BOOST_THROW_EXCEPTION(NoFormalType()
<< errinfo_noFormalTypeFrom(_type.toString(true)));
} }
void Why3Translator::addLine(string const& _line) void Why3Translator::addLine(string const& _line)
@ -156,9 +158,17 @@ bool Why3Translator::visit(ContractDefinition const& _contract)
m_currentContract.stateVariables = _contract.stateVariables(); m_currentContract.stateVariables = _contract.stateVariables();
for (VariableDeclaration const* variable: m_currentContract.stateVariables) for (VariableDeclaration const* variable: m_currentContract.stateVariables)
{ {
string varType = toFormalType(*variable->annotation().type); string varType;
if (varType.empty()) try
fatalError(*variable, "Type not supported for state variable."); {
varType = toFormalType(*variable->annotation().type);
}
catch (NoFormalType &err)
{
string const* typeNamePtr = boost::get_error_info<errinfo_noFormalTypeFrom>(err);
string typeName = typeNamePtr ? " \"" + *typeNamePtr + "\"" : "";
fatalError(*variable, "Type" + typeName + " not supported for state variable.");
}
addLine("mutable _" + variable->name() + ": " + varType); addLine("mutable _" + variable->name() + ": " + varType);
} }
unindent(); unindent();
@ -232,9 +242,16 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
add(" (this: account)"); add(" (this: account)");
for (auto const& param: _function.parameters()) for (auto const& param: _function.parameters())
{ {
string paramType = toFormalType(*param->annotation().type); string paramType;
if (paramType.empty()) try
error(*param, "Parameter type not supported."); {
paramType = toFormalType(*param->annotation().type);
}
catch (NoFormalType &err)
{
string const* typeName = boost::get_error_info<errinfo_noFormalTypeFrom>(err);
error(*param, "Parameter type \"" + (typeName ? *typeName : "") + "\" not supported.");
}
if (param->name().empty()) if (param->name().empty())
error(*param, "Anonymous function parameters not supported."); error(*param, "Anonymous function parameters not supported.");
add(" (arg_" + param->name() + ": " + paramType + ")"); add(" (arg_" + param->name() + ": " + paramType + ")");
@ -246,9 +263,16 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
string retString = "("; string retString = "(";
for (auto const& retParam: _function.returnParameters()) for (auto const& retParam: _function.returnParameters())
{ {
string paramType = toFormalType(*retParam->annotation().type); string paramType;
if (paramType.empty()) try
error(*retParam, "Parameter type not supported."); {
paramType = toFormalType(*retParam->annotation().type);
}
catch (NoFormalType &err)
{
string const* typeName = boost::get_error_info<errinfo_noFormalTypeFrom>(err);
error(*retParam, "Parameter type " + (typeName ? *typeName : "") + " not supported.");
}
if (retString.size() != 1) if (retString.size() != 1)
retString += ", "; retString += ", ";
retString += paramType; retString += paramType;
@ -278,14 +302,32 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
{ {
if (variable->name().empty()) if (variable->name().empty())
error(*variable, "Unnamed return variables not yet supported."); error(*variable, "Unnamed return variables not yet supported.");
string varType = toFormalType(*variable->annotation().type); string varType;
try
{
varType = toFormalType(*variable->annotation().type);
}
catch (NoFormalType &err)
{
string const* typeNamePtr = boost::get_error_info<errinfo_noFormalTypeFrom>(err);
error(*variable, "Type " + (typeNamePtr ? *typeNamePtr : "") + "in return parameter not yet supported.");
}
addLine("let _" + variable->name() + ": ref " + varType + " = ref (of_int 0) in"); addLine("let _" + variable->name() + ": ref " + varType + " = ref (of_int 0) in");
} }
for (VariableDeclaration const* variable: _function.localVariables()) for (VariableDeclaration const* variable: _function.localVariables())
{ {
if (variable->name().empty()) if (variable->name().empty())
error(*variable, "Unnamed variables not yet supported."); error(*variable, "Unnamed variables not yet supported.");
string varType = toFormalType(*variable->annotation().type); string varType;
try
{
varType = toFormalType(*variable->annotation().type);
}
catch (NoFormalType &err)
{
string const* typeNamePtr = boost::get_error_info<errinfo_noFormalTypeFrom>(err);
error(*variable, "Type " + (typeNamePtr ? *typeNamePtr : "") + "in variable declaration not yet supported.");
}
addLine("let _" + variable->name() + ": ref " + varType + " = ref (of_int 0) in"); addLine("let _" + variable->name() + ": ref " + varType + " = ref (of_int 0) in");
} }
addLine("try"); addLine("try");
@ -448,8 +490,15 @@ bool Why3Translator::visit(TupleExpression const& _node)
bool Why3Translator::visit(UnaryOperation const& _unaryOperation) bool Why3Translator::visit(UnaryOperation const& _unaryOperation)
{ {
if (toFormalType(*_unaryOperation.annotation().type).empty()) try
error(_unaryOperation, "Type not supported in unary operation."); {
toFormalType(*_unaryOperation.annotation().type);
}
catch (NoFormalType &err)
{
string const* typeNamePtr = boost::get_error_info<errinfo_noFormalTypeFrom>(err);
error(_unaryOperation, "Type \"" + (typeNamePtr ? *typeNamePtr : "") + "\" supported in unary operation.");
}
switch (_unaryOperation.getOperator()) switch (_unaryOperation.getOperator())
{ {

5
libsolidity/formal/Why3Translator.h
View File

@ -60,9 +60,10 @@ private:
/// Appends imports and constants use throughout the formal code. /// Appends imports and constants use throughout the formal code.
void appendPreface(); void appendPreface();
/// @returns a string representation of the corresponding formal type or the empty string /// @returns a string representation of the corresponding formal type or throws NoFormalType exception.
/// if the type is not supported.
std::string toFormalType(Type const& _type) const; std::string toFormalType(Type const& _type) const;
using errinfo_noFormalTypeFrom = boost::error_info<struct tag_noFormalTypeFrom, std::string /* name of the type that cannot be translated */ >;
struct NoFormalType: virtual Exception {};
void indent() { newLine(); m_lines.back().indentation++; } void indent() { newLine(); m_lines.back().indentation++; }
void unindent(); void unindent();