aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYoichi Hirai <i@yoichihirai.com>2016-09-08 02:16:46 +0800
committerYoichi Hirai <i@yoichihirai.com>2016-09-10 02:15:08 +0800
commitac7c6ae7d240516b0c530d51645742320634430d (patch)
treed42b7df48c2d03486dfe11864c29bbd6c1fc6023
parentc861cf579dc4c1303d6d215b5b31f930e1d6477e (diff)
downloaddexon-solidity-ac7c6ae7d240516b0c530d51645742320634430d.tar
dexon-solidity-ac7c6ae7d240516b0c530d51645742320634430d.tar.gz
dexon-solidity-ac7c6ae7d240516b0c530d51645742320634430d.tar.bz2
dexon-solidity-ac7c6ae7d240516b0c530d51645742320634430d.tar.lz
dexon-solidity-ac7c6ae7d240516b0c530d51645742320634430d.tar.xz
dexon-solidity-ac7c6ae7d240516b0c530d51645742320634430d.tar.zst
dexon-solidity-ac7c6ae7d240516b0c530d51645742320634430d.zip
toFormalType reports errors by an exception
This allows error reporting without passing `ASTNode` to `toFormalType()`
-rw-r--r--libsolidity/formal/Why3Translator.cpp87
-rw-r--r--libsolidity/formal/Why3Translator.h5
2 files changed, 71 insertions, 21 deletions
diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index 9a4a5cf5..64aa9b4c 100644
--- a/libsolidity/formal/Why3Translator.cpp
+++ b/libsolidity/formal/Why3Translator.cpp
@@ -80,9 +80,9 @@ string Why3Translator::toFormalType(Type const& _type) const
{
if (!type->isByteArray() && type->isDynamicallySized() && type->dataStoredIn(DataLocation::Memory))
{
+ // Not catching NoFormalType exception. Let the caller deal with it.
string base = toFormalType(*type->baseType());
- if (!base.empty())
- return "array " + base;
+ return "array " + base;
}
}
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.
// Also the constructor need to specify the length of the array.
- string valueType = toFormalType(*mappingType->valueType());
- if (!valueType.empty())
- return "array " + valueType;
+ solAssert(mappingType->valueType(), "A mappingType misses a valueType.");
+ // Not catching NoFormalType exception. Let the caller deal with it.
+ string valueTypeFormal = toFormalType(*mappingType->valueType());
+ return "array " + valueTypeFormal;
}
}
- return "";
+ BOOST_THROW_EXCEPTION(NoFormalType()
+ << errinfo_noFormalTypeFrom(_type.toString(true)));
}
void Why3Translator::addLine(string const& _line)
@@ -156,9 +158,17 @@ bool Why3Translator::visit(ContractDefinition const& _contract)
m_currentContract.stateVariables = _contract.stateVariables();
for (VariableDeclaration const* variable: m_currentContract.stateVariables)
{
- string varType = toFormalType(*variable->annotation().type);
- if (varType.empty())
- fatalError(*variable, "Type not supported for state variable.");
+ string varType;
+ try
+ {
+ 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);
}
unindent();
@@ -232,9 +242,16 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
add(" (this: account)");
for (auto const& param: _function.parameters())
{
- string paramType = toFormalType(*param->annotation().type);
- if (paramType.empty())
- error(*param, "Parameter type not supported.");
+ string paramType;
+ try
+ {
+ 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())
error(*param, "Anonymous function parameters not supported.");
add(" (arg_" + param->name() + ": " + paramType + ")");
@@ -246,9 +263,16 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
string retString = "(";
for (auto const& retParam: _function.returnParameters())
{
- string paramType = toFormalType(*retParam->annotation().type);
- if (paramType.empty())
- error(*retParam, "Parameter type not supported.");
+ string paramType;
+ try
+ {
+ 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)
retString += ", ";
retString += paramType;
@@ -278,14 +302,32 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
{
if (variable->name().empty())
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");
}
for (VariableDeclaration const* variable: _function.localVariables())
{
if (variable->name().empty())
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("try");
@@ -448,8 +490,15 @@ bool Why3Translator::visit(TupleExpression const& _node)
bool Why3Translator::visit(UnaryOperation const& _unaryOperation)
{
- if (toFormalType(*_unaryOperation.annotation().type).empty())
- error(_unaryOperation, "Type not supported in unary operation.");
+ try
+ {
+ 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())
{
diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h
index 1b80ed61..22bfff89 100644
--- a/libsolidity/formal/Why3Translator.h
+++ b/libsolidity/formal/Why3Translator.h
@@ -60,9 +60,10 @@ private:
/// Appends imports and constants use throughout the formal code.
void appendPreface();
- /// @returns a string representation of the corresponding formal type or the empty string
- /// if the type is not supported.
+ /// @returns a string representation of the corresponding formal type or throws NoFormalType exception.
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 unindent();